diff options
Diffstat (limited to 'lib/Floats.v')
| -rw-r--r-- | lib/Floats.v | 220 |
1 files changed, 111 insertions, 109 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index b7769420..43caebb0 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -7,10 +7,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -25,6 +26,7 @@ Import ListNotations. Close Scope R_scope. Open Scope Z_scope. +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 *) @@ -108,7 +110,7 @@ Proof. { 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. +- rewrite Z2Pos.id by lia. lia. Qed. (** Transform a Nan payload to a quiet Nan payload. *) @@ -117,7 +119,7 @@ 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. +Proof. intros; apply normalized_nan; auto; lia. Qed. Definition quiet_nan_64 (sp: bool * positive) : {x :float | is_nan _ _ x = true} := let (s, p) := sp in @@ -129,7 +131,7 @@ 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. +Proof. intros; apply normalized_nan; auto; lia. Qed. Definition quiet_nan_32 (sp: bool * positive) : {x :float32 | is_nan _ _ x = true} := let (s, p) := sp in @@ -163,7 +165,7 @@ Proof. rewrite Z.ltb_lt in *. unfold Pos.shiftl_nat, nat_rect, Digits.digits2_pos. fold (Digits.digits2_pos p). - zify; omega. + zify; lia. Qed. Definition expand_nan s p H : {x | is_nan _ _ x = true} := @@ -336,7 +338,7 @@ Ltac smart_omega := compute_this Int64.modulus; compute_this Int64.half_modulus; compute_this Int64.max_unsigned; compute_this (Z.pow_pos 2 1024); compute_this (Z.pow_pos 2 53); compute_this (Z.pow_pos 2 52); compute_this (Z.pow_pos 2 32); - zify; omega. + zify; lia. (** Commutativity properties of addition and multiplication. *) @@ -432,7 +434,7 @@ Proof. intros; unfold of_bits, to_bits, bits_of_b64, b64_of_bits. rewrite Int64.unsigned_repr, binary_float_of_bits_of_binary_float; [reflexivity|]. generalize (bits_of_binary_float_range 52 11 __ __ f). - change (2^(52+11+1)) with (Int64.max_unsigned + 1). omega. + change (2^(52+11+1)) with (Int64.max_unsigned + 1). lia. Qed. Theorem to_of_bits: @@ -476,7 +478,7 @@ Proof. rewrite BofZ_plus by auto. f_equal. unfold Int.ltu in H. destruct zlt in H; try discriminate. - unfold y, Int.sub. rewrite Int.signed_repr. omega. + unfold y, Int.sub. rewrite Int.signed_repr. lia. compute_this (Int.unsigned ox8000_0000); smart_omega. Qed. @@ -498,8 +500,8 @@ Proof. 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. } + { unfold lo. change ox7FFF_FFFF with (Int.repr (two_p 31 - 1)). rewrite <- Int.zero_ext_and by lia. + apply Int.zero_ext_range. compute_this Int.zwordsize. lia. } 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. } @@ -512,12 +514,12 @@ Proof. 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. + unfold Int.add; rewrite Int.unsigned_repr, Int.signed_eq_unsigned. lia. + - assert (Int.max_signed = two_p 31 - 1) by reflexivity. lia. - 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. + lia. Qed. Theorem to_intu_to_int_1: @@ -540,14 +542,14 @@ Proof. { rewrite ZofB_correct in C. destruct (is_finite _ _ x) eqn:FINx; congruence. } destruct (zeq p 0). subst p; smart_omega. - destruct (ZofB_range_pos 53 1024 __ __ x p C) as [P Q]. omega. + destruct (ZofB_range_pos 53 1024 __ __ x p C) as [P Q]. lia. assert (CMP: Bcompare _ _ x y = Some Lt). { unfold cmp, cmp_of_comparison, compare in H. destruct (Bcompare _ _ x y) as [[]|]; auto; discriminate. } rewrite Bcompare_correct in CMP by auto. inv CMP. apply Rcompare_Lt_inv in H1. rewrite EQy in H1. assert (p < Int.unsigned ox8000_0000). { apply lt_IZR. apply Rle_lt_trans with (1 := P) (2 := H1). } - change Int.max_signed with (Int.unsigned ox8000_0000 - 1). omega. + change Int.max_signed with (Int.unsigned ox8000_0000 - 1). lia. Qed. Theorem to_intu_to_int_2: @@ -579,7 +581,7 @@ Proof. compute_this (Int.unsigned ox8000_0000). smart_omega. apply Rge_le; auto. } - unfold to_int; rewrite EQ. simpl. unfold Int.sub. rewrite Int.unsigned_repr by omega. auto. + unfold to_int; rewrite EQ. simpl. unfold Int.sub. rewrite Int.unsigned_repr by lia. auto. Qed. (** Conversions from ints to floats can be defined as bitwise manipulations @@ -598,8 +600,8 @@ Proof. - f_equal. rewrite Int64.ofwords_add'. reflexivity. - apply split_join_bits. generalize (Int.unsigned_range x). - compute_this Int.modulus; compute_this (2^52); omega. - compute_this (2^11); omega. + compute_this Int.modulus; compute_this (2^52); lia. + compute_this (2^11); lia. Qed. Lemma from_words_value: @@ -637,7 +639,7 @@ Theorem of_intu_from_words: 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. omega. + 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. Qed. @@ -664,7 +666,7 @@ Proof. rewrite ! from_words_eq. rewrite ox8000_0000_signed_unsigned. change (Int.unsigned ox8000_0000) with Int.half_modulus. unfold sub. rewrite BofZ_minus. - unfold of_int. apply f_equal. omega. + unfold of_int. apply f_equal. lia. apply integer_representable_n; auto; smart_omega. apply integer_representable_n; auto; smart_omega. Qed. @@ -680,8 +682,8 @@ Proof. - f_equal. rewrite Int64.ofwords_add'. reflexivity. - apply split_join_bits. generalize (Int.unsigned_range x). - compute_this Int.modulus; compute_this (2^52); omega. - compute_this (2^11); omega. + compute_this Int.modulus; compute_this (2^52); lia. + compute_this (2^11); lia. Qed. Lemma from_words_value': @@ -711,11 +713,11 @@ 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. omega. omega. + apply integer_representable_n2p; auto. smart_omega. lia. lia. apply B2R_Bsign_inj; auto. - rewrite A, D. rewrite <- IZR_Zpower by omega. rewrite <- plus_IZR. auto. + rewrite A, D. rewrite <- IZR_Zpower by lia. rewrite <- plus_IZR. auto. rewrite C, F. symmetry. apply Zlt_bool_false. - compute_this (2^84); compute_this (2^32); omega. + compute_this (2^84); compute_this (2^32); lia. Qed. Theorem of_longu_from_words: @@ -742,12 +744,12 @@ Proof. 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. omega. omega. + compute_this p20; smart_omega. lia. lia. apply integer_representable_n; auto; smart_omega. replace (2^84 + xh * 2^32) with ((2^52 + xh) * 2^32) by ring. - apply integer_representable_n2p; auto. smart_omega. omega. omega. + apply integer_representable_n2p; auto. smart_omega. lia. lia. change (2^84 + p20 * 2^32) with ((2^52 + 1048576) * 2^32). - apply integer_representable_n2p; auto. omega. omega. + apply integer_representable_n2p; auto. lia. lia. Qed. Theorem of_long_from_words: @@ -776,15 +778,15 @@ Proof. 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. omega. omega. + compute_this (2^20); smart_omega. lia. lia. apply integer_representable_n; auto; 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. omega. omega. + apply integer_representable_n2p; auto. smart_omega. lia. lia. change (2^84 + p * 2^32) with ((2^52 + p) * 2^32). apply integer_representable_n2p; auto. - compute_this p; smart_omega. omega. + compute_this p; smart_omega. lia. Qed. (** Conversions from 64-bit integers can be expressed in terms of @@ -806,7 +808,7 @@ 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. omega. omega. + 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. @@ -829,7 +831,7 @@ 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. omega. omega. + 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. @@ -871,53 +873,53 @@ Proof. { intros; unfold n; autorewrite with ints; auto. rewrite Int64.unsigned_one. rewrite Int64.bits_one. compute_this Int64.zwordsize. destruct (zeq i 0); simpl proj_sumbool. - rewrite zlt_true by omega. rewrite andb_true_r. subst i; auto. + rewrite zlt_true by lia. rewrite andb_true_r. subst i; auto. rewrite andb_false_r, orb_false_r. - destruct (zeq i 63). subst i. apply zlt_false; omega. - apply zlt_true; omega. } + destruct (zeq i 63). subst i. apply zlt_false; lia. + apply zlt_true; lia. } assert (NB2: forall i, 0 <= i -> Z.testbit (Int64.signed n * 2^1) i = if zeq i 0 then false else if zeq i 1 then Int64.testbit x 1 || Int64.testbit x 0 else Int64.testbit x i). - { intros. rewrite Z.mul_pow2_bits by omega. destruct (zeq i 0). - apply Z.testbit_neg_r; omega. - rewrite Int64.bits_signed by omega. compute_this Int64.zwordsize. + { intros. rewrite Z.mul_pow2_bits by lia. destruct (zeq i 0). + apply Z.testbit_neg_r; lia. + rewrite Int64.bits_signed by lia. compute_this Int64.zwordsize. destruct (zlt (i-1) 64). - rewrite NB by omega. destruct (zeq i 1). + rewrite NB by lia. destruct (zeq i 1). subst. rewrite dec_eq_true by auto. auto. - rewrite dec_eq_false by omega. destruct (zeq (i - 1) 63). - symmetry. apply Int64.bits_above. compute_this Int64.zwordsize; omega. - f_equal; omega. - rewrite NB by omega. rewrite dec_eq_false by omega. rewrite dec_eq_true by auto. - rewrite dec_eq_false by omega. symmetry. apply Int64.bits_above. compute_this Int64.zwordsize; omega. + rewrite dec_eq_false by lia. destruct (zeq (i - 1) 63). + symmetry. apply Int64.bits_above. compute_this Int64.zwordsize; lia. + f_equal; lia. + rewrite NB by lia. rewrite dec_eq_false by lia. rewrite dec_eq_true by auto. + rewrite dec_eq_false by lia. symmetry. apply Int64.bits_above. compute_this Int64.zwordsize; lia. } assert (EQ: Int64.signed n * 2 = int_round_odd (Int64.unsigned x) 1). { - symmetry. apply (int_round_odd_bits 53 1024). omega. - intros. rewrite NB2 by omega. replace i with 0 by omega. auto. - rewrite NB2 by omega. rewrite dec_eq_false by omega. rewrite dec_eq_true. + symmetry. apply int_round_odd_bits. lia. + 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. destruct (Z.testbit (Int64.unsigned x) 0) eqn:B0; - [rewrite Z.testbit_true in B0 by omega|rewrite Z.testbit_false in B0 by omega]; + [rewrite Z.testbit_true in B0 by lia|rewrite Z.testbit_false in B0 by lia]; change (2^0) with 1 in B0; rewrite Zdiv_1_r in B0; rewrite B0; auto. - intros. rewrite NB2 by omega. rewrite ! dec_eq_false by omega. auto. + intros. rewrite NB2 by lia. rewrite ! dec_eq_false by lia. auto. } unfold mul, of_long, of_longu. rewrite BofZ_mult_2p. - change (2^1) with 2. rewrite EQ. apply BofZ_round_odd with (p := 1). -+ omega. ++ lia. + apply Z.le_trans with Int64.modulus; trivial. smart_omega. -+ omega. -+ apply Z.le_trans with (2^63). compute; intuition congruence. xomega. ++ lia. ++ apply Z.le_trans with (2^63). compute; intuition congruence. extlia. - apply Z.le_trans with Int64.modulus; trivial. pose proof (Int64.signed_range n). compute_this Int64.min_signed; compute_this Int64.max_signed; - compute_this Int64.modulus; xomega. + compute_this Int64.modulus; extlia. - assert (2^63 <= int_round_odd (Int64.unsigned x) 1). - { change (2^63) with (int_round_odd (2^63) 1). apply (int_round_odd_le 0 0); omega. } - rewrite <- EQ in H1. compute_this (2^63). compute_this (2^53). xomega. -- omega. + { change (2^63) with (int_round_odd (2^63) 1). apply int_round_odd_le; lia. } + rewrite <- EQ in H1. compute_this (2^63). compute_this (2^53). extlia. +- lia. Qed. (** Conversions to/from 32-bit integers can be implemented by going through 64-bit integers. *) @@ -931,8 +933,8 @@ Proof. intros. exploit ZofB_range_inversion; eauto. intros (A & B & C). unfold ZofB_range; rewrite C. replace (min2 <=? n) with true. replace (n <=? max2) with true. auto. - symmetry; apply Z.leb_le; omega. - symmetry; apply Z.leb_le; omega. + symmetry; apply Z.leb_le; lia. + symmetry; apply Z.leb_le; lia. Qed. Theorem to_int_to_long: @@ -954,7 +956,7 @@ Proof. exploit ZofB_range_inversion; eauto. intros (A & B & C). replace (ZofB_range 53 1024 f 0 Int64.max_unsigned) with (Some z). simpl. rewrite Int.unsigned_repr; auto. - symmetry; eapply ZofB_range_widen; eauto. omega. compute; congruence. + symmetry; eapply ZofB_range_widen; eauto. lia. compute; congruence. Qed. Theorem to_intu_to_long: @@ -1183,7 +1185,7 @@ Theorem cmp_double: forall f1 f2 c, cmp c f1 f2 = Float.cmp c (to_double f1) (to_double f2). Proof. unfold cmp, Float.cmp; intros. f_equal. symmetry. apply Bcompare_Bconv_widen. - red; omega. omega. omega. + red; lia. lia. lia. Qed. (** Properties of conversions to/from in-memory representation. @@ -1195,7 +1197,7 @@ Proof. intros; unfold of_bits, to_bits, bits_of_b32, b32_of_bits. rewrite Int.unsigned_repr, binary_float_of_bits_of_binary_float; [reflexivity|]. generalize (bits_of_binary_float_range 23 8 __ __ f). - change (2^(23+8+1)) with (Int.max_unsigned + 1). omega. + change (2^(23+8+1)) with (Int.max_unsigned + 1). lia. Qed. Theorem to_of_bits: @@ -1235,7 +1237,7 @@ Proof. unfold to_int in H. destruct (ZofB_range _ _ f Int.min_signed Int.max_signed) as [n'|] eqn:E; inv H. unfold Float.to_int, to_double, Float.of_single. - erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. + erewrite ZofB_range_Bconv; eauto. auto. lia. lia. lia. lia. Qed. Theorem to_intu_double: @@ -1245,7 +1247,7 @@ Proof. unfold to_intu in H. destruct (ZofB_range _ _ f 0 Int.max_unsigned) as [n'|] eqn:E; inv H. unfold Float.to_intu, to_double, Float.of_single. - erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. + erewrite ZofB_range_Bconv; eauto. auto. lia. lia. lia. lia. Qed. Theorem to_long_double: @@ -1255,7 +1257,7 @@ Proof. unfold to_long in H. destruct (ZofB_range _ _ f Int64.min_signed Int64.max_signed) as [n'|] eqn:E; inv H. unfold Float.to_long, to_double, Float.of_single. - erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. + erewrite ZofB_range_Bconv; eauto. auto. lia. lia. lia. lia. Qed. Theorem to_longu_double: @@ -1265,7 +1267,7 @@ Proof. unfold to_longu in H. destruct (ZofB_range _ _ f 0 Int64.max_unsigned) as [n'|] eqn:E; inv H. unfold Float.to_longu, to_double, Float.of_single. - erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. + erewrite ZofB_range_Bconv; eauto. auto. lia. lia. lia. lia. Qed. (** Conversions from 64-bit integers to single-precision floats can be expressed @@ -1280,37 +1282,37 @@ Proof. intros. assert (POS: 0 < 2^p) by (apply (Zpower_gt_0 radix2); auto). assert (A: Z.land n (2^p-1) = n mod 2^p). - { rewrite <- Z.land_ones by auto. f_equal. rewrite Z.ones_equiv. omega. } + { rewrite <- Z.land_ones by auto. f_equal. rewrite Z.ones_equiv. lia. } rewrite A. assert (B: 0 <= n mod 2^p < 2^p). - { apply Z_mod_lt. omega. } + { apply Z_mod_lt. lia. } 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 Z.div_small. omega. - eapply Coqlib.Zdiv_unique with (n mod 2^p - 1). ring. omega. } + rewrite e. apply Z.div_small. lia. + eapply Coqlib.Zdiv_unique with (n mod 2^p - 1). ring. lia. } 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. + { intros. apply Z.testbit_false. lia. 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. } + unfold m. split. lia. apply Z.lt_le_trans with (2 * 2^p). lia. + change 2 with (2^1) at 1. rewrite <- (Zpower_plus radix2) by lia. + apply Zpower_le. lia. } assert (F: forall i, 0 <= i -> Z.testbit (-2^p) i = if zlt i p then false else true). { intros. rewrite Z.bits_opp by auto. rewrite <- Z.ones_equiv. destruct (zlt i p). - rewrite Z.ones_spec_low by omega. auto. - rewrite Z.ones_spec_high by omega. auto. } + rewrite Z.ones_spec_low by lia. auto. + rewrite Z.ones_spec_high by lia. auto. } apply int_round_odd_bits; auto. - - intros. rewrite Z.land_spec, F, zlt_true by omega. apply andb_false_r. - - rewrite Z.land_spec, Z.lor_spec, D, F, zlt_false, andb_true_r by omega. + - intros. rewrite Z.land_spec, F, zlt_true by lia. apply andb_false_r. + - rewrite Z.land_spec, Z.lor_spec, D, F, zlt_false, andb_true_r by lia. destruct (Z.eqb (n mod 2^p) 0) eqn:Z. rewrite Z.eqb_eq in Z. rewrite Z, zeq_true. apply orb_false_r. rewrite Z.eqb_neq in Z. rewrite zeq_false by auto. apply orb_true_r. - - intros. rewrite Z.land_spec, Z.lor_spec, E, F, zlt_false, andb_true_r by omega. + - intros. rewrite Z.land_spec, Z.lor_spec, E, F, zlt_false, andb_true_r by lia. apply orb_false_r. Qed. @@ -1319,22 +1321,22 @@ Lemma of_long_round_odd: 2^36 <= Z.abs n < 2^64 -> BofZ 24 128 __ __ n = Bconv _ _ 24 128 __ __ conv_nan mode_NE (BofZ 53 1024 __ __ (Z.land (Z.lor n ((Z.land n 2047) + 2047)) (-2048))). Proof. - intros. rewrite <- (int_round_odd_plus 11) by omega. + intros. rewrite <- (int_round_odd_plus 11) by lia. assert (-2^64 <= int_round_odd n 11). - { change (-2^64) with (int_round_odd (-2^64) 11). apply (int_round_odd_le 0 0); xomega. } + { change (-2^64) with (int_round_odd (-2^64) 11). apply int_round_odd_le; extlia. } assert (int_round_odd n 11 <= 2^64). - { change (2^64) with (int_round_odd (2^64) 11). apply (int_round_odd_le 0 0); xomega. } + { change (2^64) with (int_round_odd (2^64) 11). apply int_round_odd_le; extlia. } rewrite Bconv_BofZ. apply BofZ_round_odd with (p := 11). - omega. - apply Z.le_trans with (2^64). omega. compute; intuition congruence. - omega. + lia. + 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. omega. + unfold int_round_odd. apply integer_representable_n2p_wide. auto. lia. unfold int_round_odd in H0, H1. split; (apply Zmult_le_reg_r with (2^11); [compute; auto | assumption]). - omega. - omega. + lia. + lia. Qed. Theorem of_longu_double_1: @@ -1343,7 +1345,7 @@ Theorem of_longu_double_1: of_longu n = of_double (Float.of_longu n). Proof. intros. symmetry; apply Bconv_BofZ. apply integer_representable_n; auto. - pose proof (Int64.unsigned_range n); omega. + pose proof (Int64.unsigned_range n); lia. Qed. Theorem of_longu_double_2: @@ -1361,14 +1363,14 @@ Proof. unfold of_double, Float.to_single. instantiate (1 := Float.to_single_nan). f_equal. unfold Float.of_longu. f_equal. set (n' := Z.land (Z.lor (Int64.unsigned n) (Z.land (Int64.unsigned n) 2047 + 2047)) (-2048)). - assert (int_round_odd (Int64.unsigned n) 11 = n') by (apply int_round_odd_plus; omega). + assert (int_round_odd (Int64.unsigned n) 11 = n') by (apply int_round_odd_plus; lia). assert (0 <= n'). - { rewrite <- H1. change 0 with (int_round_odd 0 11). apply (int_round_odd_le 0 0); omega. } + { rewrite <- H1. change 0 with (int_round_odd 0 11). apply int_round_odd_le; lia. } assert (n' < Int64.modulus). { apply Z.le_lt_trans with (int_round_odd (Int64.modulus - 1) 11). - rewrite <- H1. apply (int_round_odd_le 0 0); omega. + rewrite <- H1. apply int_round_odd_le; lia. compute; auto. } - rewrite <- (Int64.unsigned_repr n') by (unfold Int64.max_unsigned; omega). + rewrite <- (Int64.unsigned_repr n') by (unfold Int64.max_unsigned; lia). f_equal. Int64.bit_solve. rewrite Int64.testbit_repr by auto. unfold n'. rewrite Z.land_spec, Z.lor_spec. f_equal. f_equal. unfold Int64.testbit. rewrite Int64.add_unsigned. @@ -1377,11 +1379,11 @@ Proof. Int64.unsigned (Int64.repr 2047))) i). rewrite Int64.testbit_repr by auto. f_equal. f_equal. unfold Int64.and. symmetry. apply Int64.unsigned_repr. change 2047 with (Z.ones 11). - rewrite Z.land_ones by omega. + rewrite Z.land_ones by lia. exploit (Z_mod_lt (Int64.unsigned n) (2^11)). compute; auto. - assert (2^11 < Int64.max_unsigned) by (compute; auto). omega. + assert (2^11 < Int64.max_unsigned) by (compute; auto). lia. apply Int64.same_bits_eqm; auto. exists (-1); auto. - split. xomega. change (2^64) with Int64.modulus. xomega. + split. extlia. change (2^64) with Int64.modulus. extlia. Qed. Theorem of_long_double_1: @@ -1389,7 +1391,7 @@ Theorem of_long_double_1: Z.abs (Int64.signed n) <= 2^53 -> of_long n = of_double (Float.of_long n). Proof. - intros. symmetry; apply Bconv_BofZ. apply integer_representable_n; auto. xomega. + intros. symmetry; apply Bconv_BofZ. apply integer_representable_n; auto. extlia. Qed. Theorem of_long_double_2: @@ -1407,34 +1409,34 @@ Proof. unfold of_double, Float.to_single. instantiate (1 := Float.to_single_nan). f_equal. unfold Float.of_long. f_equal. set (n' := Z.land (Z.lor (Int64.signed n) (Z.land (Int64.signed n) 2047 + 2047)) (-2048)). - assert (int_round_odd (Int64.signed n) 11 = n') by (apply int_round_odd_plus; omega). + assert (int_round_odd (Int64.signed n) 11 = n') by (apply int_round_odd_plus; lia). assert (Int64.min_signed <= n'). - { rewrite <- H1. change Int64.min_signed with (int_round_odd Int64.min_signed 11). apply (int_round_odd_le 0 0); omega. } + { rewrite <- H1. change Int64.min_signed with (int_round_odd Int64.min_signed 11). apply int_round_odd_le; lia. } assert (n' <= Int64.max_signed). { apply Z.le_trans with (int_round_odd Int64.max_signed 11). - rewrite <- H1. apply (int_round_odd_le 0 0); omega. + rewrite <- H1. apply int_round_odd_le; lia. compute; intuition congruence. } - rewrite <- (Int64.signed_repr n') by omega. + rewrite <- (Int64.signed_repr n') by lia. f_equal. Int64.bit_solve. rewrite Int64.testbit_repr by auto. unfold n'. rewrite Z.land_spec, Z.lor_spec. f_equal. f_equal. - rewrite Int64.bits_signed by omega. rewrite zlt_true by omega. auto. + rewrite Int64.bits_signed by lia. rewrite zlt_true by lia. auto. unfold Int64.testbit. rewrite Int64.add_unsigned. fold (Int64.testbit (Int64.repr (Int64.unsigned (Int64.and n (Int64.repr 2047)) + Int64.unsigned (Int64.repr 2047))) i). 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. + change 2047 with (Z.ones 11). rewrite ! Z.land_ones by lia. rewrite Int64.unsigned_repr. apply eqmod_mod_eq. - apply Z.lt_gt. apply (Zpower_gt_0 radix2); omega. + apply Z.lt_gt. apply (Zpower_gt_0 radix2); lia. 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. + assert (2^11 < Int64.max_unsigned) by (compute; auto). lia. apply Int64.same_bits_eqm; auto. exists (-1); auto. split. auto. assert (-2^64 < Int64.min_signed) by (compute; auto). assert (Int64.max_signed < 2^64) by (compute; auto). - xomega. + extlia. Qed. End Float32. |