diff options
Diffstat (limited to 'lib/Floats.v')
| -rw-r--r-- | lib/Floats.v | 329 |
1 files changed, 199 insertions, 130 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index 3ce8f4b4..13350dd0 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -16,15 +16,15 @@ (** Formalization of floating-point numbers, using the Flocq library. *) -Require Import Coqlib. -Require Import Integers. +Require Import Coqlib Zbits Integers. (*From Flocq*) Require Import Binary Bits Core. -Require Import Fappli_IEEE_extra. +Require Import IEEE754_extra. Require Import Program. Require Archi. Close Scope R_scope. +Open Scope Z_scope. Definition float := binary64. (**r the type of IEE754 double-precision FP numbers *) Definition float32 := binary32. (**r the type of IEE754 single-precision FP numbers *) @@ -94,21 +94,53 @@ Proof. destruct x as [[]|]; simpl; intros; discriminate. Qed. -(** Relation between number of bits and base-2 logarithm *) +(** Normalization of NaN payloads *) -Lemma digits2_log2: - forall p, Z.pos (Digits.digits2_pos p) = Z.succ (Z.log2 (Z.pos p)). +Lemma normalized_nan: forall prec n p, + Z.of_nat n = prec - 1 -> 1 < prec -> + nan_pl prec (Z.to_pos (P_mod_two_p p n)) = true. Proof. - assert (E: forall p, Digits.digits2_pos p = Pos.size p). - { induction p; simpl; rewrite ?IHp; auto. } - intros p. rewrite E. - destruct p; simpl; rewrite ?Pos.add_1_r; reflexivity. + intros. unfold nan_pl. apply Z.ltb_lt. rewrite Digits.Zpos_digits2_pos. + set (p' := P_mod_two_p p n). + assert (A: 0 <= p' < 2 ^ Z.of_nat n). + { rewrite <- two_power_nat_equiv; apply P_mod_two_p_range. } + assert (B: Digits.Zdigits radix2 p' <= prec - 1). + { apply Digits.Zdigits_le_Zpower. rewrite <- H. rewrite Z.abs_eq; tauto. } + destruct (zeq p' 0). +- rewrite e. simpl; auto. +- rewrite Z2Pos.id by omega. omega. Qed. +(** Transform a Nan payload to a quiet Nan payload. *) + +Definition quiet_nan_64_payload (p: positive) := + Z.to_pos (P_mod_two_p (Pos.lor p ((iter_nat xO 51 1%positive))) 52%nat). + +Lemma quiet_nan_64_proof: forall p, nan_pl 53 (quiet_nan_64_payload p) = true. +Proof. intros; apply normalized_nan; auto; omega. Qed. + +Definition quiet_nan_64 (sp: bool * positive) : {x :float | is_nan _ _ x = true} := + let (s, p) := sp in + exist _ (B754_nan 53 1024 s (quiet_nan_64_payload p) (quiet_nan_64_proof p)) (eq_refl true). + +Definition default_nan_64 := quiet_nan_64 Archi.default_nan_64. + +Definition quiet_nan_32_payload (p: positive) := + Z.to_pos (P_mod_two_p (Pos.lor p ((iter_nat xO 22 1%positive))) 23%nat). + +Lemma quiet_nan_32_proof: forall p, nan_pl 24 (quiet_nan_32_payload p) = true. +Proof. intros; apply normalized_nan; auto; omega. Qed. + +Definition quiet_nan_32 (sp: bool * positive) : {x :float32 | is_nan _ _ x = true} := + let (s, p) := sp in + exist _ (B754_nan 24 128 s (quiet_nan_32_payload p) (quiet_nan_32_proof p)) (eq_refl true). + +Definition default_nan_32 := quiet_nan_32 Archi.default_nan_32. + Local Notation __ := (eq_refl Datatypes.Lt). -Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt). -Local Hint Extern 1 (_ < _) => exact (eq_refl Datatypes.Lt). +Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt) : core. +Local Hint Extern 1 (_ < _) => exact (eq_refl Datatypes.Lt) : core. (** * Double-precision FP numbers *) @@ -119,68 +151,44 @@ Module Float. (** The following definitions are not part of the IEEE754 standard but apply to all architectures supported by CompCert. *) -(** Transform a Nan payload to a quiet Nan payload. *) - -Lemma transform_quiet_nan_proof (p : positive) : - nan_pl 53 p = true -> - nan_pl 53 (Pos.lor p (iter_nat xO 51 1%positive)) = true. -Proof. - unfold nan_pl. intros K. - simpl. rewrite Z.ltb_lt, digits2_log2 in *. - change (Z.pos (Pos.lor p 2251799813685248)) with (Z.lor (Z.pos p) 2251799813685248%Z). - rewrite Z.log2_lor by xomega. - now apply Z.max_case. -Qed. - -Definition transform_quiet_nan s p H : {x :float | is_nan _ _ x = true} := - exist _ (B754_nan 53 1024 s _ (transform_quiet_nan_proof p H)) (eq_refl true). - (** Nan payload operations for single <-> double conversions. *) +Definition expand_nan_payload (p: positive) := Pos.shiftl_nat p 29. + Lemma expand_nan_proof (p : positive) : nan_pl 24 p = true -> - nan_pl 53 (Pos.shiftl_nat p 29) = true. + nan_pl 53 (expand_nan_payload p) = true. Proof. - unfold nan_pl. intros K. + unfold nan_pl, expand_nan_payload. intros K. rewrite Z.ltb_lt in *. unfold Pos.shiftl_nat, nat_rect, Digits.digits2_pos. fold (Digits.digits2_pos p). zify; omega. Qed. -Definition expand_nan s p H : {x | is_nan 53 1024 x = true} := - exist _ (B754_nan 53 1024 s _ (expand_nan_proof p H)) (eq_refl true). +Definition expand_nan s p H : {x | is_nan _ _ x = true} := + exist _ (B754_nan 53 1024 s (expand_nan_payload p) (expand_nan_proof p H)) (eq_refl true). Definition of_single_nan (f : float32) : { x : float | is_nan _ _ x = true } := match f with | B754_nan s p H => if Archi.float_of_single_preserves_sNaN then expand_nan s p H - else transform_quiet_nan s _ (expand_nan_proof p H) - | _ => Archi.default_nan_64 + else quiet_nan_64 (s, expand_nan_payload p) + | _ => default_nan_64 end. -Lemma reduce_nan_proof (p : positive) : - nan_pl 53 p = true -> - nan_pl 24 (Pos.shiftr_nat p 29) = true. -Proof. - unfold nan_pl. intros K. - rewrite Z.ltb_lt in *. - unfold Pos.shiftr_nat, nat_rect. - assert (H : forall x, Digits.digits2_pos (Pos.div2 x) = (Digits.digits2_pos x - 1)%positive) - by (destruct x; simpl; auto; rewrite Pplus_one_succ_r, Pos.add_sub; auto). - rewrite !H, !Pos2Z.inj_sub_max. - repeat (apply Z.max_lub_lt; [reflexivity |apply Z.lt_sub_lt_add_l]). - exact K. -Qed. - -Definition reduce_nan s p H : {x : float32 | is_nan _ _ x = true} := - exist _ (B754_nan 24 128 s _ (reduce_nan_proof p H)) (eq_refl true). +Definition reduce_nan_payload (p: positive) := + (* The [quiet_nan_64_payload p] before the right shift is redundant with + the [quiet_nan_32_payload p] performed after, in [to_single_nan]. + However the former ensures that the result of the right shift is + not 0 and therefore representable as a positive. *) + Pos.shiftr_nat (quiet_nan_64_payload p) 29. Definition to_single_nan (f : float) : { x : float32 | is_nan _ _ x = true } := match f with - | B754_nan s p H => reduce_nan s _ (transform_quiet_nan_proof p H) - | _ => Archi.default_nan_32 + | B754_nan s p H => quiet_nan_32 (s, reduce_nan_payload p) + | _ => default_nan_32 end. (** NaN payload operations for opposite and absolute value. *) @@ -188,33 +196,62 @@ Definition to_single_nan (f : float) : { x : float32 | is_nan _ _ x = true } := Definition neg_nan (f : float) : { x : float | is_nan _ _ x = true } := match f with | B754_nan s p H => exist _ (B754_nan 53 1024 (negb s) p H) (eq_refl true) - | _ => Archi.default_nan_64 + | _ => default_nan_64 end. Definition abs_nan (f : float) : { x : float | is_nan _ _ x = true } := match f with | B754_nan s p H => exist _ (B754_nan 53 1024 false p H) (eq_refl true) - | _ => Archi.default_nan_64 + | _ => default_nan_64 end. -(** The NaN payload operations for two-argument arithmetic operations - are not part of the IEEE754 standard, but all architectures of - Compcert share a similar NaN behavior, parameterized by: -- a "default" payload which occurs when an operation generates a NaN from - non-NaN arguments; -- a choice function determining which of the payload arguments to choose, - when an operation is given two NaN arguments. *) +(** When an arithmetic operation returns a NaN, the sign and payload + of this NaN are not fully specified by the IEEE standard, and vary + among the architectures supported by CompCert. However, the following + behavior applies to all the supported architectures: the payload is either +- a default payload, independent of the arguments, or +- the payload of one of the NaN arguments, if any. + +For each supported architecture, the functions [Archi.choose_nan_64] +and [Archi.choose_nan_32] determine the payload of the result as a +function of the payloads of the NaN arguments. + +Additionally, signaling NaNs are converted to quiet NaNs, as required by the standard. +*) + +Definition cons_pl (x: float) (l: list (bool * positive)) := + match x with B754_nan s p _ => (s, p) :: l | _ => l end. -Definition binop_nan (x y : float) : {x : float | is_nan 53 1024 x = true} := - if Archi.fpu_returns_default_qNaN then Archi.default_nan_64 else +Definition unop_nan (x: float) : {x : float | is_nan _ _ x = true} := + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x [])). + +Definition binop_nan (x y: float) : {x : float | is_nan _ _ x = true} := + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y []))). + +(** For fused multiply-add, the order in which arguments are examined + to select a NaN payload varies across platforms. E.g. in [fma x y z], + x86 considers [x] first, then [y], then [z], while ARM considers [z] first, + then [x], then [y]. The corresponding permutation is defined + for each target, as function [Archi.fma_order]. *) + +Definition fma_nan_1 (x y z: float) : {x : float | is_nan _ _ x = true} := + let '(a, b, c) := Archi.fma_order x y z in + quiet_nan_64 (Archi.choose_nan_64 (cons_pl a (cons_pl b (cons_pl c [])))). + +(** One last wrinkle for fused multiply-add: [fma zero infinity nan] + can return either the quiesced [nan], or the default NaN arising out + of the invalid operation [zero * infinity]. Of our target platforms, + only ARM honors the latter case. The choice between the default NaN + and [nan] is done as in the case of two-argument arithmetic operations. *) + +Definition fma_nan (x y z: float) : {x : float | is_nan _ _ x = true} := match x, y with - | B754_nan s1 pl1 H1, B754_nan s2 pl2 H2 => - if Archi.choose_binop_pl_64 pl1 pl2 - then transform_quiet_nan s2 pl2 H2 - else transform_quiet_nan s1 pl1 H1 - | B754_nan s1 pl1 H1, _ => transform_quiet_nan s1 pl1 H1 - | _, B754_nan s2 pl2 H2 => transform_quiet_nan s2 pl2 H2 - | _, _ => Archi.default_nan_64 + | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => + if Archi.fma_invalid_mul_is_nan + then quiet_nan_64 (Archi.choose_nan_64 (Archi.default_nan_64 :: cons_pl z [])) + else fma_nan_1 x y z + | _, _ => + fma_nan_1 x y z end. (** ** Operations over double-precision floats *) @@ -227,6 +264,8 @@ Definition eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2} := Beq_dec _ _. Definition neg: float -> float := Bopp _ _ neg_nan. (**r opposite (change sign) *) Definition abs: float -> float := Babs _ _ abs_nan. (**r absolute value (set sign to [+]) *) +Definition sqrt: float -> float := + Bsqrt 53 1024 __ __ unop_nan mode_NE. (**r square root *) Definition add: float -> float -> float := Bplus 53 1024 __ __ binop_nan mode_NE. (**r addition *) Definition sub: float -> float -> float := @@ -235,6 +274,8 @@ Definition mul: float -> float -> float := Bmult 53 1024 __ __ binop_nan mode_NE. (**r multiplication *) Definition div: float -> float -> float := Bdiv 53 1024 __ __ binop_nan mode_NE. (**r division *) +Definition fma: float -> float -> float -> float := + Bfma 53 1024 __ __ fma_nan mode_NE. (**r fused multiply-add [x * y + z] *) Definition compare (f1 f2: float) : option Datatypes.comparison := (**r general comparison *) Bcompare 53 1024 f1 f2. Definition cmp (c:comparison) (f1 f2: float) : bool := (**r Boolean comparison *) @@ -302,19 +343,15 @@ Ltac smart_omega := Theorem add_commut: forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> add x y = add y x. Proof. - intros. apply Bplus_commut. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x, y; try reflexivity. - now destruct H. + intros. apply Bplus_commut. + destruct x, y; try reflexivity; now destruct H. Qed. Theorem mul_commut: forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> mul x y = mul y x. Proof. - intros. apply Bmult_commut. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x, y; try reflexivity. - now destruct H. + intros. apply Bmult_commut. + destruct x, y; try reflexivity; now destruct H. Qed. (** Multiplication by 2 is diagonal addition. *) @@ -324,9 +361,8 @@ Theorem mul2_add: Proof. intros. apply Bmult2_Bplus. intros x y Hx Hy. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x as [| |sx px Nx|]; try discriminate. - now destruct y, Archi.choose_binop_pl_64. + destruct x; try discriminate. simpl. rewrite Archi.choose_nan_64_idem. + destruct y; reflexivity || discriminate. Qed. (** Divisions that can be turned into multiplication by an inverse. *) @@ -338,9 +374,8 @@ Theorem div_mul_inverse: Proof. intros. apply Bdiv_mult_inverse. 2: easy. intros x0 y0 z0 Hx Hy Hz. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x0 as [| |sx px Nx|]; try discriminate. - now destruct y0, z0. + destruct x0; try discriminate. + destruct y0, z0; reflexivity || discriminate. Qed. (** Properties of comparisons. *) @@ -414,6 +449,7 @@ Qed. to emulate the former.) *) Definition ox8000_0000 := Int.repr Int.half_modulus. (**r [0x8000_0000] *) +Definition ox7FFF_FFFF := Int.repr Int.max_signed. (**r [0x7FFF_FFFF] *) Theorem of_intu_of_int_1: forall x, @@ -444,6 +480,46 @@ Proof. compute_this (Int.unsigned ox8000_0000); smart_omega. Qed. +Theorem of_intu_of_int_3: + forall x, + of_intu x = sub (of_int (Int.and x ox7FFF_FFFF)) (of_int (Int.and x ox8000_0000)). +Proof. + intros. + set (hi := Int.and x ox8000_0000). + 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. } + 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. + - rewrite <- Int.and_or_distrib. apply Int.and_mone. + - rewrite Int.and_assoc. rewrite (Int.and_commut ox8000_0000). rewrite Int.and_assoc. + change (Int.and ox7FFF_FFFF ox8000_0000) with Int.zero. rewrite ! Int.and_zero; auto. + } + assert (RNG: 0 <= Int.unsigned lo < two_p 31). + { unfold lo. change ox7FFF_FFFF with (Int.repr (two_p 31 - 1)). rewrite <- Int.zero_ext_and by omega. + apply Int.zero_ext_range. compute_this Int.zwordsize. omega. } + assert (B: forall i, 0 <= i < Int.zwordsize -> Int.testbit ox8000_0000 i = if zeq i 31 then true else false). + { intros; unfold Int.testbit. change (Int.unsigned ox8000_0000) with (2^31). + destruct (zeq i 31). subst i; auto. apply Z.pow2_bits_false; auto. } + assert (EITHER: hi = Int.zero \/ hi = ox8000_0000). + { unfold hi; destruct (Int.testbit x 31) eqn:B31; [right|left]; + Int.bit_solve; rewrite B by auto. + - destruct (zeq i 31). subst i; rewrite B31; auto. apply andb_false_r. + - destruct (zeq i 31). subst i; rewrite B31; auto. apply andb_false_r. + } + assert (SU: - Int.signed hi = Int.unsigned hi). + { destruct EITHER as [EQ|EQ]; rewrite EQ; reflexivity. } + unfold Z.sub; rewrite SU, <- E. + unfold Int.add; rewrite Int.unsigned_repr, Int.signed_eq_unsigned. omega. + - assert (Int.max_signed = two_p 31 - 1) by reflexivity. omega. + - assert (Int.unsigned hi = 0 \/ Int.unsigned hi = two_p 31) + by (destruct EITHER as [EQ|EQ]; rewrite EQ; [left|right]; reflexivity). + assert (Int.max_unsigned = two_p 31 + two_p 31 - 1) by reflexivity. + omega. +Qed. + Theorem to_intu_to_int_1: forall x n, cmp Clt x (of_intu ox8000_0000) = true -> @@ -919,44 +995,39 @@ End Float. Module Float32. -(** ** NaN payload manipulations *) - -Lemma transform_quiet_nan_proof (p : positive) : - nan_pl 24 p = true -> - nan_pl 24 (Pos.lor p (iter_nat xO 22 1%positive)) = true. -Proof. - unfold nan_pl. intros K. - simpl. rewrite Z.ltb_lt, digits2_log2 in *. - change (Z.pos (Pos.lor p 4194304)) with (Z.lor (Z.pos p) 4194304%Z). - rewrite Z.log2_lor by xomega. - now apply Z.max_case. -Qed. - -Definition transform_quiet_nan s p H : {x : float32 | is_nan _ _ x = true} := - exist _ (B754_nan 24 128 s _ (transform_quiet_nan_proof p H)) (eq_refl true). - Definition neg_nan (f : float32) : { x : float32 | is_nan _ _ x = true } := match f with | B754_nan s p H => exist _ (B754_nan 24 128 (negb s) p H) (eq_refl true) - | _ => Archi.default_nan_32 + | _ => default_nan_32 end. Definition abs_nan (f : float32) : { x : float32 | is_nan _ _ x = true } := match f with | B754_nan s p H => exist _ (B754_nan 24 128 false p H) (eq_refl true) - | _ => Archi.default_nan_32 + | _ => default_nan_32 end. -Definition binop_nan (x y : float32) : {x : float32 | is_nan _ _ x = true} := - if Archi.fpu_returns_default_qNaN then Archi.default_nan_32 else +Definition cons_pl (x: float32) (l: list (bool * positive)) := + match x with B754_nan s p _ => (s, p) :: l | _ => l end. + +Definition unop_nan (x: float32) : {x : float32 | is_nan _ _ x = true} := + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x [])). + +Definition binop_nan (x y: float32) : {x : float32 | is_nan _ _ x = true} := + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y []))). + +Definition fma_nan_1 (x y z: float32) : {x : float32 | is_nan _ _ x = true} := + let '(a, b, c) := Archi.fma_order x y z in + quiet_nan_32 (Archi.choose_nan_32 (cons_pl a (cons_pl b (cons_pl c [])))). + +Definition fma_nan (x y z: float32) : {x : float32 | is_nan _ _ x = true} := match x, y with - | B754_nan s1 pl1 H1, B754_nan s2 pl2 H2 => - if Archi.choose_binop_pl_32 pl1 pl2 - then transform_quiet_nan s2 pl2 H2 - else transform_quiet_nan s1 pl1 H1 - | B754_nan s1 pl1 H1, _ => transform_quiet_nan s1 pl1 H1 - | _, B754_nan s2 pl2 H2 => transform_quiet_nan s2 pl2 H2 - | _, _ => Archi.default_nan_32 + | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => + if Archi.fma_invalid_mul_is_nan + then quiet_nan_32 (Archi.choose_nan_32 (Archi.default_nan_32 :: cons_pl z [])) + else fma_nan_1 x y z + | _, _ => + fma_nan_1 x y z end. (** ** Operations over single-precision floats *) @@ -969,6 +1040,8 @@ Definition eq_dec: forall (f1 f2: float32), {f1 = f2} + {f1 <> f2} := Beq_dec _ Definition neg: float32 -> float32 := Bopp _ _ neg_nan. (**r opposite (change sign) *) Definition abs: float32 -> float32 := Babs _ _ abs_nan. (**r absolute value (set sign to [+]) *) +Definition sqrt: float32 -> float32 := + Bsqrt 24 128 __ __ unop_nan mode_NE. (**r square root *) Definition add: float32 -> float32 -> float32 := Bplus 24 128 __ __ binop_nan mode_NE. (**r addition *) Definition sub: float32 -> float32 -> float32 := @@ -977,6 +1050,8 @@ Definition mul: float32 -> float32 -> float32 := Bmult 24 128 __ __ binop_nan mode_NE. (**r multiplication *) Definition div: float32 -> float32 -> float32 := Bdiv 24 128 __ __ binop_nan mode_NE. (**r division *) +Definition fma: float32 -> float32 -> float32 -> float32 := + Bfma 24 128 __ __ fma_nan mode_NE. (**r fused multiply-add [x * y + z] *) Definition compare (f1 f2: float32) : option Datatypes.comparison := (**r general comparison *) Bcompare 24 128 f1 f2. Definition cmp (c:comparison) (f1 f2: float32) : bool := (**r comparison *) @@ -1024,19 +1099,15 @@ Definition of_bits (b: int): float32 := b32_of_bits (Int.unsigned b). Theorem add_commut: forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> add x y = add y x. Proof. - intros. apply Bplus_commut. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x, y; try reflexivity. - now destruct H. + intros. apply Bplus_commut. + destruct x, y; try reflexivity; now destruct H. Qed. Theorem mul_commut: forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> mul x y = mul y x. Proof. - intros. apply Bmult_commut. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x, y; try reflexivity. - now destruct H. + intros. apply Bmult_commut. + destruct x, y; try reflexivity; now destruct H. Qed. (** Multiplication by 2 is diagonal addition. *) @@ -1046,9 +1117,8 @@ Theorem mul2_add: Proof. intros. apply Bmult2_Bplus. intros x y Hx Hy. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x as [| |sx px Nx|]; try discriminate. - now destruct y, Archi.choose_binop_pl_32. + destruct x; try discriminate. simpl. rewrite Archi.choose_nan_32_idem. + destruct y; reflexivity || discriminate. Qed. (** Divisions that can be turned into multiplication by an inverse. *) @@ -1060,9 +1130,8 @@ Theorem div_mul_inverse: Proof. intros. apply Bdiv_mult_inverse. 2: easy. intros x0 y0 z0 Hx Hy Hz. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x0 as [| |sx px Nx|]; try discriminate. - now destruct y0, z0. + destruct x0; try discriminate. + destruct y0, z0; reflexivity || discriminate. Qed. (** Properties of comparisons. *) @@ -1218,15 +1287,15 @@ Proof. set (m := n mod 2^p + (2^p-1)) in *. assert (C: m / 2^p = if zeq (n mod 2^p) 0 then 0 else 1). { unfold m. destruct (zeq (n mod 2^p) 0). - rewrite e. apply Zdiv_small. omega. - eapply Zdiv_unique with (n mod 2^p - 1). ring. omega. } + rewrite e. apply Z.div_small. omega. + eapply Coqlib.Zdiv_unique with (n mod 2^p - 1). ring. omega. } assert (D: Z.testbit m p = if zeq (n mod 2^p) 0 then false else true). { destruct (zeq (n mod 2^p) 0). apply Z.testbit_false; auto. rewrite C; auto. apply Z.testbit_true; auto. rewrite C; auto. } assert (E: forall i, p < i -> Z.testbit m i = false). { intros. apply Z.testbit_false. omega. - replace (m / 2^i) with 0. auto. symmetry. apply Zdiv_small. + replace (m / 2^i) with 0. auto. symmetry. apply Z.div_small. unfold m. split. omega. apply Z.lt_le_trans with (2 * 2^p). omega. change 2 with (2^1) at 1. rewrite <- (Zpower_plus radix2) by omega. apply Zpower_le. omega. } @@ -1356,9 +1425,9 @@ Proof. rewrite Int64.testbit_repr by auto. f_equal. f_equal. unfold Int64.and. change (Int64.unsigned (Int64.repr 2047)) with 2047. change 2047 with (Z.ones 11). rewrite ! Z.land_ones by omega. - rewrite Int64.unsigned_repr. apply Int64.eqmod_mod_eq. + rewrite Int64.unsigned_repr. apply eqmod_mod_eq. apply Z.lt_gt. apply (Zpower_gt_0 radix2); omega. - apply Int64.eqmod_divides with (2^64). apply Int64.eqm_signed_unsigned. + apply eqmod_divides with (2^64). apply Int64.eqm_signed_unsigned. exists (2^(64-11)); auto. exploit (Z_mod_lt (Int64.unsigned n) (2^11)). compute; auto. assert (2^11 < Int64.max_unsigned) by (compute; auto). omega. |