diff options
Diffstat (limited to 'lib/Floats.v')
| -rw-r--r-- | lib/Floats.v | 74 |
1 files changed, 39 insertions, 35 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index fd0a3d32..33e48524 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -17,8 +17,9 @@ (** Formalization of floating-point numbers, using the Flocq library. *) +Require Import Reals. Require Import Coqlib Zbits Integers. -From Flocq Require Import Binary Bits Core. +From Flocq Require Import BinarySingleNaN Binary Bits Core. Require Import IEEE754_extra. Require Import Program. Require Archi. @@ -31,6 +32,12 @@ Set Asymmetric Patterns. Definition float := binary64. (**r the type of IEE754 double-precision FP numbers *) Definition float32 := binary32. (**r the type of IEE754 single-precision FP numbers *) +Lemma integer_representable_n : + forall n : Z, - 2 ^ 53 <= n <= 2 ^ 53 -> integer_representable 53 1024 n. +Proof. +now apply integer_representable_n. +Qed. + (** Boolean-valued comparisons *) Definition cmp_of_comparison (c: comparison) (x: option Datatypes.comparison) : bool := @@ -477,9 +484,9 @@ Proof. set (y := Int.sub x ox8000_0000). pose proof (Int.unsigned_range x); pose proof (Int.signed_range y). assert (Ry: integer_representable 53 1024 (Int.signed y)). - { apply integer_representable_n; auto; smart_omega. } + { apply integer_representable_n. smart_omega. } assert (R8: integer_representable 53 1024 (Int.unsigned ox8000_0000)). - { apply integer_representable_2p with (p := 31);auto; smart_omega. } + { apply integer_representable_2p with (p := 31); easy. } rewrite BofZ_plus by auto. f_equal. unfold Int.ltu in H. destruct zlt in H; try discriminate. @@ -496,7 +503,7 @@ Proof. set (lo := Int.and x ox7FFF_FFFF). assert (R: forall n, integer_representable 53 1024 (Int.signed n)). { intros. pose proof (Int.signed_range n). - apply integer_representable_n; auto; smart_omega. } + apply integer_representable_n. smart_omega. } unfold sub, of_int. rewrite BofZ_minus by auto. unfold of_intu. f_equal. assert (E: Int.add hi lo = x). { unfold hi, lo. rewrite Int.add_is_or. @@ -645,8 +652,8 @@ Proof. intros. pose proof (Int.unsigned_range x). rewrite ! from_words_eq. unfold sub. rewrite BofZ_minus. unfold of_intu. apply (f_equal (BofZ 53 1024 __ __)). rewrite Int.unsigned_zero. lia. - apply integer_representable_n; auto; smart_omega. - apply integer_representable_n; auto; rewrite Int.unsigned_zero; smart_omega. + apply integer_representable_n. smart_omega. + apply integer_representable_n. easy. Qed. Lemma ox8000_0000_signed_unsigned: @@ -672,8 +679,8 @@ Proof. change (Int.unsigned ox8000_0000) with Int.half_modulus. unfold sub. rewrite BofZ_minus. unfold of_int. apply f_equal. lia. - apply integer_representable_n; auto; smart_omega. - apply integer_representable_n; auto; smart_omega. + apply integer_representable_n. smart_omega. + apply integer_representable_n. easy. Qed. Definition ox4530_0000 := Int.repr 1160773632. (**r [0x4530_0000] *) @@ -718,7 +725,7 @@ Proof. destruct (BofZ_representable 53 1024 __ __ (2^84 + Int.unsigned x * 2^32)) as (D & E & F). replace (2^84 + Int.unsigned x * 2^32) with ((2^52 + Int.unsigned x) * 2^32) by ring. - apply integer_representable_n2p; auto. smart_omega. lia. lia. + apply integer_representable_n2p; try easy. smart_omega. apply B2R_Bsign_inj; auto. rewrite A, D. rewrite <- IZR_Zpower by lia. rewrite <- plus_IZR. auto. rewrite C, F. symmetry. apply Zlt_bool_false. @@ -748,13 +755,13 @@ Proof. unfold of_longu. f_equal. rewrite <- (Int64.ofwords_recompose l) at 1. rewrite Int64.ofwords_add'. fold xh; fold xl. compute_this (two_p 32); compute_this p20; ring. - apply integer_representable_n2p; auto. - compute_this p20; smart_omega. lia. lia. - apply integer_representable_n; auto; smart_omega. + apply integer_representable_n2p; try easy. + compute_this p20; smart_omega. + apply integer_representable_n. smart_omega. replace (2^84 + xh * 2^32) with ((2^52 + xh) * 2^32) by ring. - apply integer_representable_n2p; auto. smart_omega. lia. lia. + apply integer_representable_n2p; try easy. smart_omega. change (2^84 + p20 * 2^32) with ((2^52 + 1048576) * 2^32). - apply integer_representable_n2p; auto. lia. lia. + apply integer_representable_n2p; easy. Qed. Theorem of_long_from_words: @@ -782,16 +789,15 @@ Proof. unfold of_long. apply f_equal. rewrite <- (Int64.ofwords_recompose l) at 1. rewrite Int64.ofwords_add''. fold xh; fold xl. compute_this (two_p 32); ring. - apply integer_representable_n2p; auto. - compute_this (2^20); smart_omega. lia. lia. - apply integer_representable_n; auto; smart_omega. + apply integer_representable_n2p; try easy. + compute_this (2^20); smart_omega. + apply integer_representable_n. smart_omega. replace (2^84 + (xh + Int.half_modulus) * 2^32) with ((2^52 + xh + Int.half_modulus) * 2^32) by (compute_this Int.half_modulus; ring). - apply integer_representable_n2p; auto. smart_omega. lia. lia. + apply integer_representable_n2p; try easy. smart_omega. change (2^84 + p * 2^32) with ((2^52 + p) * 2^32). - apply integer_representable_n2p; auto. - compute_this p; smart_omega. lia. + apply integer_representable_n2p; easy. Qed. (** Conversions from 64-bit integers can be expressed in terms of @@ -813,11 +819,11 @@ Proof. assert (DECOMP: x = yh * 2^32 + yl). { unfold x. rewrite <- (Int64.ofwords_recompose l). apply Int64.ofwords_add'. } rewrite BofZ_mult. rewrite BofZ_plus. rewrite DECOMP; auto. - apply integer_representable_n2p; auto. smart_omega. lia. lia. - apply integer_representable_n; auto; smart_omega. - apply integer_representable_n; auto; smart_omega. - apply integer_representable_n; auto; smart_omega. - compute; auto. + apply integer_representable_n2p; try easy. smart_omega. + apply integer_representable_n. smart_omega. + apply integer_representable_n. smart_omega. + apply integer_representable_n. easy. + easy. Qed. Theorem of_long_decomp: @@ -836,11 +842,11 @@ Proof. assert (DECOMP: x = yh * 2^32 + yl). { unfold x. rewrite <- (Int64.ofwords_recompose l), Int64.ofwords_add''. auto. } rewrite BofZ_mult. rewrite BofZ_plus. rewrite DECOMP; auto. - apply integer_representable_n2p; auto. smart_omega. lia. lia. - apply integer_representable_n; auto; smart_omega. - apply integer_representable_n; auto; smart_omega. - apply integer_representable_n; auto. compute; intuition congruence. - compute; auto. + apply integer_representable_n2p; try easy. smart_omega. + apply integer_representable_n. smart_omega. + apply integer_representable_n. smart_omega. + apply integer_representable_n. easy. + easy. Qed. (** Conversions from unsigned longs can be expressed in terms of conversions from signed longs. @@ -901,7 +907,7 @@ Proof. } assert (EQ: Int64.signed n * 2 = int_round_odd (Int64.unsigned x) 1). { - symmetry. apply int_round_odd_bits. lia. + symmetry. apply int_round_odd_bits. easy. intros. rewrite NB2 by lia. replace i with 0 by lia. auto. rewrite NB2 by lia. rewrite dec_eq_false by lia. rewrite dec_eq_true. rewrite orb_comm. unfold Int64.testbit. change (2^1) with 2. @@ -1221,7 +1227,7 @@ Theorem of_int_double: forall n, of_int n = of_double (Float.of_int n). Proof. intros. symmetry. apply Bconv_BofZ. - apply integer_representable_n; auto. generalize (Int.signed_range n); Float.smart_omega. + apply integer_representable_n. generalize (Int.signed_range n); Float.smart_omega. Qed. Theorem of_intu_double: @@ -1337,11 +1343,9 @@ Proof. apply Z.le_trans with (2^64). lia. compute; intuition congruence. lia. exact (proj1 H). - unfold int_round_odd. apply integer_representable_n2p_wide. auto. lia. + unfold int_round_odd. apply integer_representable_n2p_wide; try easy. unfold int_round_odd in H0, H1. split; (apply Zmult_le_reg_r with (2^11); [compute; auto | assumption]). - lia. - lia. Qed. Theorem of_longu_double_1: |