From d4513f41c54869c9b4ba96ab79d50933a1d5c25a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 28 Dec 2020 15:53:36 +0100 Subject: Update Flocq to 3.4.0 (#383) --- flocq/Calc/Bracket.v | 40 ++-- flocq/Calc/Div.v | 13 +- flocq/Calc/Operations.v | 6 +- flocq/Calc/Round.v | 21 +- flocq/Calc/Sqrt.v | 21 +- flocq/Core/Defs.v | 4 + flocq/Core/Digits.v | 93 ++++----- flocq/Core/FIX.v | 11 +- flocq/Core/FLT.v | 254 ++++++++++++++++------- flocq/Core/FLX.v | 12 +- flocq/Core/FTZ.v | 32 +-- flocq/Core/Float_prop.v | 12 +- flocq/Core/Generic_fmt.v | 123 ++++++++++-- flocq/Core/Raux.v | 32 ++- flocq/Core/Round_NE.v | 18 +- flocq/Core/Round_pred.v | 282 ++++++++++++++++++++++++++ flocq/Core/Ulp.v | 222 ++++++++++++++++---- flocq/Core/Zaux.v | 29 ++- flocq/IEEE754/Binary.v | 103 +++++++--- flocq/IEEE754/Bits.v | 138 ++++++++----- flocq/IEEE754/SpecFloatCompat.v | 435 ++++++++++++++++++++++++++++++++++++++++ flocq/Prop/Div_sqrt_error.v | 30 ++- flocq/Prop/Double_rounding.v | 417 +++++++++++++++++++------------------- flocq/Prop/Mult_error.v | 43 +++- flocq/Prop/Plus_error.v | 23 +-- flocq/Prop/Relative.v | 24 +-- flocq/Prop/Round_odd.v | 36 ++-- flocq/Prop/Sterbenz.v | 2 +- flocq/Version.v | 2 +- 29 files changed, 1840 insertions(+), 638 deletions(-) create mode 100644 flocq/IEEE754/SpecFloatCompat.v (limited to 'flocq') diff --git a/flocq/Calc/Bracket.v b/flocq/Calc/Bracket.v index 83714e87..838cadfa 100644 --- a/flocq/Calc/Bracket.v +++ b/flocq/Calc/Bracket.v @@ -19,15 +19,19 @@ COPYING file for more details. (** * Locations: where a real number is positioned with respect to its rounded-down value in an arbitrary format. *) +From Coq Require Import Lia. Require Import Raux Defs Float_prop. +Require Import SpecFloatCompat. + +Notation location := location (only parsing). +Notation loc_Exact := loc_Exact (only parsing). +Notation loc_Inexact := loc_Inexact (only parsing). Section Fcalc_bracket. Variable d u : R. Hypothesis Hdu : (d < u)%R. -Inductive location := loc_Exact | loc_Inexact : comparison -> location. - Variable x : R. Definition inbetween_loc := @@ -233,7 +237,7 @@ apply Rplus_le_compat_l. apply Rmult_le_compat_r. now apply Rlt_le. apply IZR_le. -omega. +lia. (* . *) now rewrite middle_range. Qed. @@ -246,7 +250,7 @@ Theorem inbetween_step_Lo : Proof. intros x k l Hx Hk1 Hk2. apply inbetween_step_not_Eq with (1 := Hx). -omega. +lia. apply Rcompare_Lt. assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx). apply Rlt_le_trans with (1 := proj2 Hx'). @@ -255,7 +259,7 @@ rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. apply Rcompare_not_Lt. rewrite <- mult_IZR. apply IZR_le. -omega. +lia. exact Hstep. Qed. @@ -267,7 +271,7 @@ Theorem inbetween_step_Hi : Proof. intros x k l Hx Hk1 Hk2. apply inbetween_step_not_Eq with (1 := Hx). -omega. +lia. apply Rcompare_Gt. assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx). apply Rlt_le_trans with (2 := proj1 Hx'). @@ -276,7 +280,7 @@ rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. apply Rcompare_Lt. rewrite <- mult_IZR. apply IZR_lt. -omega. +lia. exact Hstep. Qed. @@ -331,7 +335,7 @@ Theorem inbetween_step_any_Mi_odd : Proof. intros x k l Hx Hk. apply inbetween_step_not_Eq with (1 := Hx). -omega. +lia. inversion_clear Hx as [|l' _ Hl]. now rewrite (middle_odd _ Hk) in Hl. Qed. @@ -344,7 +348,7 @@ Theorem inbetween_step_Lo_Mi_Eq_odd : Proof. intros x k Hx Hk. apply inbetween_step_not_Eq with (1 := Hx). -omega. +lia. inversion_clear Hx as [Hl|]. rewrite Hl. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r. @@ -365,7 +369,7 @@ Theorem inbetween_step_Hi_Mi_even : Proof. intros x k l Hx Hl Hk. apply inbetween_step_not_Eq with (1 := Hx). -omega. +lia. apply Rcompare_Gt. assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl). apply Rle_lt_trans with (2 := proj1 Hx'). @@ -387,7 +391,7 @@ Theorem inbetween_step_Mi_Mi_even : Proof. intros x k Hx Hk. apply inbetween_step_not_Eq with (1 := Hx). -omega. +lia. apply Rcompare_Eq. inversion_clear Hx as [Hx'|]. rewrite Hx', <- Hk, mult_IZR. @@ -433,10 +437,10 @@ now apply inbetween_step_Lo_not_Eq with (2 := H1). destruct (Zcompare_spec (2 * k) nb_steps) as [Hk1|Hk1|Hk1]. (* . 2 * k < nb_steps *) apply inbetween_step_Lo with (1 := Hx). -omega. +lia. destruct (Zeven_ex nb_steps). rewrite He in H. -omega. +lia. (* . 2 * k = nb_steps *) set (l' := match l with loc_Exact => Eq | _ => Gt end). assert ((l = loc_Exact /\ l' = Eq) \/ (l <> loc_Exact /\ l' = Gt)). @@ -490,7 +494,7 @@ now apply inbetween_step_Lo_not_Eq with (2 := H1). destruct (Zcompare_spec (2 * k + 1) nb_steps) as [Hk1|Hk1|Hk1]. (* . 2 * k + 1 < nb_steps *) apply inbetween_step_Lo with (1 := Hx) (3 := Hk1). -omega. +lia. (* . 2 * k + 1 = nb_steps *) destruct l. apply inbetween_step_Lo_Mi_Eq_odd with (1 := Hx) (2 := Hk1). @@ -499,7 +503,7 @@ apply inbetween_step_any_Mi_odd with (1 := Hx) (2 := Hk1). apply inbetween_step_Hi with (1 := Hx). destruct (Zeven_ex nb_steps). rewrite Ho in H. -omega. +lia. apply Hk. Qed. @@ -612,7 +616,7 @@ clear -Hk. intros m. rewrite (F2R_change_exp beta e). apply (f_equal (fun r => F2R (Float beta (m * Zpower _ r) e))). ring. -omega. +lia. assert (Hp: (Zpower beta k > 0)%Z). apply Z.lt_gt. apply Zpower_gt_0. @@ -622,7 +626,7 @@ rewrite 2!Hr. rewrite Zmult_plus_distr_l, Zmult_1_l. unfold F2R at 2. simpl. rewrite plus_IZR, Rmult_plus_distr_r. -apply new_location_correct. +apply new_location_correct; unfold F2R; simpl. apply bpow_gt_0. now apply Zpower_gt_1. now apply Z_mod_lt. @@ -665,7 +669,7 @@ rewrite <- Hm in H'. clear -H H'. apply inbetween_unique with (1 := H) (2 := H'). destruct (inbetween_float_bounds x m e l H) as (H1,H2). destruct (inbetween_float_bounds x m' e l' H') as (H3,H4). -cut (m < m' + 1 /\ m' < m + 1)%Z. clear ; omega. +cut (m < m' + 1 /\ m' < m + 1)%Z. clear ; lia. now split ; apply lt_F2R with beta e ; apply Rle_lt_trans with x. Qed. diff --git a/flocq/Calc/Div.v b/flocq/Calc/Div.v index 65195562..48e3bb51 100644 --- a/flocq/Calc/Div.v +++ b/flocq/Calc/Div.v @@ -19,6 +19,7 @@ COPYING file for more details. (** * Helper function and theorem for computing the rounded quotient of two floating-point numbers. *) +From Coq Require Import Lia. Require Import Raux Defs Generic_fmt Float_prop Digits Bracket. Set Implicit Arguments. @@ -80,7 +81,7 @@ assert ((F2R (Float beta m1 e1) / F2R (Float beta m2 e2) = IZR m1' / IZR m2' * b destruct (Zle_bool e (e1 - e2)) eqn:He' ; injection Hm ; intros ; subst. - split ; try easy. apply Zle_bool_imp_le in He'. - rewrite mult_IZR, IZR_Zpower by omega. + rewrite mult_IZR, IZR_Zpower by lia. unfold Zminus ; rewrite 2!bpow_plus, 2!bpow_opp. field. repeat split ; try apply Rgt_not_eq, bpow_gt_0. @@ -88,8 +89,8 @@ assert ((F2R (Float beta m1 e1) / F2R (Float beta m2 e2) = IZR m1' / IZR m2' * b - apply Z.leb_gt in He'. split ; cycle 1. { apply Z.mul_pos_pos with (1 := Hm2). - apply Zpower_gt_0 ; omega. } - rewrite mult_IZR, IZR_Zpower by omega. + apply Zpower_gt_0 ; lia. } + rewrite mult_IZR, IZR_Zpower by lia. unfold Zminus ; rewrite bpow_plus, bpow_opp, bpow_plus, bpow_opp. field. repeat split ; try apply Rgt_not_eq, bpow_gt_0. @@ -113,7 +114,7 @@ destruct (Z_lt_le_dec 1 m2') as [Hm2''|Hm2'']. now apply IZR_neq, Zgt_not_eq. field. now apply IZR_neq, Zgt_not_eq. -- assert (r = 0 /\ m2' = 1)%Z as [-> ->] by (clear -Hr Hm2'' ; omega). +- assert (r = 0 /\ m2' = 1)%Z as [-> ->] by (clear -Hr Hm2'' ; lia). unfold Rdiv. rewrite Rmult_1_l, Rplus_0_r, Rinv_1, Rmult_1_r. now constructor. @@ -150,10 +151,10 @@ unfold cexp. destruct (Zle_lt_or_eq _ _ H1) as [H|H]. - replace (fexp (mag _ _)) with (fexp (e + 1)). apply Z.le_min_r. - clear -H1 H2 H ; apply f_equal ; omega. + clear -H1 H2 H ; apply f_equal ; lia. - replace (fexp (mag _ _)) with (fexp e). apply Z.le_min_l. - clear -H1 H2 H ; apply f_equal ; omega. + clear -H1 H2 H ; apply f_equal ; lia. Qed. End Fcalc_div. diff --git a/flocq/Calc/Operations.v b/flocq/Calc/Operations.v index 3416cb4e..ac93d412 100644 --- a/flocq/Calc/Operations.v +++ b/flocq/Calc/Operations.v @@ -17,7 +17,9 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. *) -(** Basic operations on floats: alignment, addition, multiplication *) +(** * Basic operations on floats: alignment, addition, multiplication *) + +From Coq Require Import Lia. Require Import Raux Defs Float_prop. Set Implicit Arguments. @@ -50,7 +52,7 @@ case (Zle_bool e1 e2) ; intros He ; split ; trivial. now rewrite <- F2R_change_exp. rewrite <- F2R_change_exp. apply refl_equal. -omega. +lia. Qed. Theorem Falign_spec_exp: diff --git a/flocq/Calc/Round.v b/flocq/Calc/Round.v index 5bde6af4..704a1ab2 100644 --- a/flocq/Calc/Round.v +++ b/flocq/Calc/Round.v @@ -19,6 +19,7 @@ COPYING file for more details. (** * Helper function for computing the rounded value of a real number. *) +From Coq Require Import Lia. Require Import Core Digits Float_prop Bracket. Section Fcalc_round. @@ -88,7 +89,7 @@ destruct Px as [Px|Px]. destruct Bx as [Bx1 Bx2]. apply lt_0_F2R in Bx1. apply gt_0_F2R in Bx2. - omega. + lia. Qed. (** Relates location and rounding. *) @@ -585,7 +586,7 @@ apply Zlt_succ. rewrite Zle_bool_true with (1 := Hm). rewrite Zle_bool_false. now case Rlt_bool. -omega. +lia. Qed. Definition truncate_aux t k := @@ -674,7 +675,7 @@ unfold cexp. rewrite mag_F2R_Zdigits. 2: now apply Zgt_not_eq. unfold k in Hk. clear -Hk. -omega. +lia. rewrite <- Hm', F2R_0. apply generic_format_0. Qed. @@ -717,14 +718,14 @@ simpl. apply Zfloor_div. intros H. generalize (Zpower_pos_gt_0 beta k) (Zle_bool_imp_le _ _ (radix_prop beta)). -omega. +lia. rewrite scaled_mantissa_generic with (1 := Fx). now rewrite Zfloor_IZR. (* *) split. apply refl_equal. unfold k in Hk. -omega. +lia. Qed. Theorem truncate_correct_partial' : @@ -744,7 +745,7 @@ destruct Zlt_bool ; intros Hk. now apply inbetween_float_new_location. ring. - apply (conj H1). - omega. + lia. Qed. Theorem truncate_correct_partial : @@ -790,7 +791,7 @@ intros x m e l [Hx|Hx] H1 H2. destruct Zlt_bool. intros H. apply False_ind. - omega. + lia. intros _. apply (conj H1). right. @@ -803,7 +804,7 @@ intros x m e l [Hx|Hx] H1 H2. rewrite mag_F2R_Zdigits with (1 := Zm). now apply Zlt_le_weak. - assert (Hm: m = 0%Z). - cut (m <= 0 < m + 1)%Z. omega. + cut (m <= 0 < m + 1)%Z. lia. assert (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R as Hx'. apply inbetween_float_bounds with (1 := H1). rewrite <- Hx in Hx'. @@ -1156,7 +1157,7 @@ exact H1. unfold k in Hk. destruct H2 as [H2|H2]. left. -omega. +lia. right. split. exact H2. @@ -1165,7 +1166,7 @@ inversion_clear H1. rewrite H. apply generic_format_F2R. unfold cexp. -omega. +lia. Qed. End Fcalc_round. diff --git a/flocq/Calc/Sqrt.v b/flocq/Calc/Sqrt.v index 8843d21e..4d267d21 100644 --- a/flocq/Calc/Sqrt.v +++ b/flocq/Calc/Sqrt.v @@ -19,6 +19,7 @@ COPYING file for more details. (** * Helper functions and theorems for computing the rounded square root of a floating-point number. *) +From Coq Require Import Lia. Require Import Raux Defs Digits Generic_fmt Float_prop Bracket. Set Implicit Arguments. @@ -86,7 +87,7 @@ assert (sqrt (F2R (Float beta m1 e1)) = sqrt (IZR m') * bpow e)%R as Hf. { rewrite <- (sqrt_Rsqr (bpow e)) by apply bpow_ge_0. rewrite <- sqrt_mult. unfold Rsqr, m'. - rewrite mult_IZR, IZR_Zpower by omega. + rewrite mult_IZR, IZR_Zpower by lia. rewrite Rmult_assoc, <- 2!bpow_plus. now replace (_ + _)%Z with e1 by ring. now apply IZR_le. @@ -106,7 +107,7 @@ fold (Rsqr (IZR q)). rewrite sqrt_Rsqr. now constructor. apply IZR_le. -clear -Hr ; omega. +clear -Hr ; lia. (* .. r <> 0 *) constructor. split. @@ -117,14 +118,14 @@ fold (Rsqr (IZR q)). rewrite sqrt_Rsqr. apply Rle_refl. apply IZR_le. -clear -Hr ; omega. +clear -Hr ; lia. apply sqrt_lt_1. rewrite mult_IZR. apply Rle_0_sqr. rewrite <- Hq. now apply IZR_le. apply IZR_lt. -omega. +lia. apply Rlt_le_trans with (sqrt (IZR ((q + 1) * (q + 1)))). apply sqrt_lt_1. rewrite <- Hq. @@ -133,13 +134,13 @@ rewrite mult_IZR. apply Rle_0_sqr. apply IZR_lt. ring_simplify. -omega. +lia. rewrite mult_IZR. fold (Rsqr (IZR (q + 1))). rewrite sqrt_Rsqr. apply Rle_refl. apply IZR_le. -clear -Hr ; omega. +clear -Hr ; lia. (* ... location *) rewrite Rcompare_half_r. generalize (Rcompare_sqr (2 * sqrt (IZR (q * q + r))) (IZR q + IZR (q + 1))). @@ -154,14 +155,14 @@ replace ((q + (q + 1)) * (q + (q + 1)))%Z with (4 * (q * q) + 4 * q + 1)%Z by ri generalize (Zle_cases r q). case (Zle_bool r q) ; intros Hr''. change (4 * (q * q + r) < 4 * (q * q) + 4 * q + 1)%Z. -omega. +lia. change (4 * (q * q + r) > 4 * (q * q) + 4 * q + 1)%Z. -omega. +lia. rewrite <- Hq. now apply IZR_le. rewrite <- plus_IZR. apply IZR_le. -clear -Hr ; omega. +clear -Hr ; lia. apply Rmult_le_pos. now apply IZR_le. apply sqrt_ge_0. @@ -188,7 +189,7 @@ set (e := Z.min _ _). assert (2 * e <= e1)%Z as He. { assert (e <= Z.div2 e1)%Z by apply Z.le_min_r. rewrite (Zdiv2_odd_eqn e1). - destruct Z.odd ; omega. } + destruct Z.odd ; lia. } generalize (Fsqrt_core_correct m1 e1 e Hm1 He). destruct Fsqrt_core as [m l]. apply conj. diff --git a/flocq/Core/Defs.v b/flocq/Core/Defs.v index f5c6f33b..27342df9 100644 --- a/flocq/Core/Defs.v +++ b/flocq/Core/Defs.v @@ -80,4 +80,8 @@ Definition Rnd_NA_pt (F : R -> Prop) (x f : R) := Rnd_N_pt F x f /\ forall f2 : R, Rnd_N_pt F x f2 -> (Rabs f2 <= Rabs f)%R. +Definition Rnd_N0_pt (F : R -> Prop) (x f : R) := + Rnd_N_pt F x f /\ + forall f2 : R, Rnd_N_pt F x f2 -> (Rabs f <= Rabs f2)%R. + End RND. diff --git a/flocq/Core/Digits.v b/flocq/Core/Digits.v index bed2e20a..a18ff8d6 100644 --- a/flocq/Core/Digits.v +++ b/flocq/Core/Digits.v @@ -17,8 +17,13 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. *) -Require Import ZArith Zquot. +From Coq Require Import Lia ZArith Zquot. + Require Import Zaux. +Require Import SpecFloatCompat. + +Notation digits2_pos := digits2_pos (only parsing). +Notation Zdigits2 := Zdigits2 (only parsing). (** Number of bits (radix 2) of a positive integer. @@ -41,9 +46,9 @@ intros n d. unfold d. clear. assert (Hp: forall m, (Zpower_nat 2 (S m) = 2 * Zpower_nat 2 m)%Z) by easy. induction n ; simpl digits2_Pnat. rewrite Zpos_xI, 2!Hp. -omega. +lia. rewrite (Zpos_xO n), 2!Hp. -omega. +lia. now split. Qed. @@ -185,13 +190,13 @@ apply Zgt_not_eq. now apply Zpower_gt_0. now apply Zle_minus_le_0. destruct (Zle_or_lt 0 k) as [H0|H0]. -rewrite (Zdigit_lt n) by omega. +rewrite (Zdigit_lt n) by lia. unfold Zdigit. replace k' with (k' - k + k)%Z by ring. rewrite Zpower_plus with (2 := H0). rewrite Zmult_assoc, Z_quot_mult. replace (k' - k)%Z with (k' - k - 1 + 1)%Z by ring. -rewrite Zpower_exp by omega. +rewrite Zpower_exp by lia. rewrite Zmult_assoc. change (Zpower beta 1) with (beta * 1)%Z. rewrite Zmult_1_r. @@ -203,7 +208,7 @@ now apply Zlt_le_weak. rewrite Zdigit_lt with (1 := H0). apply sym_eq. apply Zdigit_lt. -omega. +lia. Qed. Theorem Zdigit_div_pow : @@ -227,7 +232,7 @@ unfold Zdigit. rewrite <- 2!ZOdiv_mod_mult. apply (f_equal (fun x => Z.quot x (beta ^ k))). replace k' with (k + 1 + (k' - (k + 1)))%Z by ring. -rewrite Zpower_exp by omega. +rewrite Zpower_exp by lia. rewrite Zmult_comm. rewrite Zpower_plus by easy. change (Zpower beta 1) with (beta * 1)%Z. @@ -449,7 +454,7 @@ unfold Zscale. case Zle_bool_spec ; intros Hk. now apply Zdigit_mul_pow. apply Zdigit_div_pow with (1 := Hk'). -omega. +lia. Qed. Theorem Zscale_0 : @@ -492,7 +497,7 @@ now rewrite Zpower_plus. now apply Zplus_le_0_compat. case Zle_bool_spec ; intros Hk''. pattern k at 1 ; replace k with (k + k' + -k')%Z by ring. -assert (0 <= -k')%Z by omega. +assert (0 <= -k')%Z by lia. rewrite Zpower_plus by easy. rewrite Zmult_assoc, Z_quot_mult. apply refl_equal. @@ -503,7 +508,7 @@ rewrite Zpower_plus with (2 := Hk). apply Zquot_mult_cancel_r. apply Zgt_not_eq. now apply Zpower_gt_0. -omega. +lia. Qed. Theorem Zscale_scale : @@ -532,7 +537,7 @@ rewrite Zdigit_mod_pow by apply Hk. rewrite Zdigit_scale by apply Hk. unfold Zminus. now rewrite Z.opp_involutive, Zplus_comm. -omega. +lia. Qed. Theorem Zdigit_slice_out : @@ -589,16 +594,16 @@ destruct (Zle_or_lt k2' k) as [Hk''|Hk'']. now apply Zdigit_slice_out. rewrite Zdigit_slice by now split. apply Zdigit_slice_out. -zify ; omega. -rewrite Zdigit_slice by (zify ; omega). +zify ; lia. +rewrite Zdigit_slice by (zify ; lia). rewrite (Zdigit_slice n (k1 + k1')) by now split. rewrite Zdigit_slice. now rewrite Zplus_assoc. -zify ; omega. +zify ; lia. unfold Zslice. rewrite Z.min_r. now rewrite Zle_bool_false. -omega. +lia. Qed. Theorem Zslice_mul_pow : @@ -624,14 +629,14 @@ case Zle_bool_spec ; intros Hk2. apply (f_equal (fun x => Z.rem x (beta ^ k2))). unfold Zscale. case Zle_bool_spec ; intros Hk1'. -replace k1 with Z0 by omega. +replace k1 with Z0 by lia. case Zle_bool_spec ; intros Hk'. -replace k with Z0 by omega. +replace k with Z0 by lia. simpl. now rewrite Z.quot_1_r. rewrite Z.opp_involutive. apply Zmult_1_r. -rewrite Zle_bool_false by omega. +rewrite Zle_bool_false by lia. rewrite 2!Z.opp_involutive, Zplus_comm. rewrite Zpower_plus by assumption. apply Zquot_Zquot. @@ -646,7 +651,7 @@ unfold Zscale. case Zle_bool_spec; intros Hk. now apply Zslice_mul_pow. apply Zslice_div_pow with (2 := Hk1). -omega. +lia. Qed. Theorem Zslice_div_pow_scale : @@ -666,7 +671,7 @@ apply Zdigit_slice_out. now apply Zplus_le_compat_l. rewrite Zdigit_slice by now split. destruct (Zle_or_lt 0 (k1 + k')) as [Hk1'|Hk1']. -rewrite Zdigit_slice by omega. +rewrite Zdigit_slice by lia. rewrite Zdigit_div_pow by assumption. apply f_equal. ring. @@ -685,15 +690,15 @@ rewrite Zdigit_plus. rewrite Zdigit_scale with (1 := Hk). destruct (Zle_or_lt (l1 + l2) k) as [Hk2|Hk2]. rewrite Zdigit_slice_out with (1 := Hk2). -now rewrite 2!Zdigit_slice_out by omega. +now rewrite 2!Zdigit_slice_out by lia. rewrite Zdigit_slice with (1 := conj Hk Hk2). destruct (Zle_or_lt l1 k) as [Hk1|Hk1]. rewrite Zdigit_slice_out with (1 := Hk1). -rewrite Zdigit_slice by omega. +rewrite Zdigit_slice by lia. simpl ; apply f_equal. ring. rewrite Zdigit_slice with (1 := conj Hk Hk1). -rewrite (Zdigit_lt _ (k - l1)) by omega. +rewrite (Zdigit_lt _ (k - l1)) by lia. apply Zplus_0_r. rewrite Zmult_comm. apply Zsame_sign_trans_weak with n. @@ -713,7 +718,7 @@ left. now apply Zdigit_slice_out. right. apply Zdigit_lt. -omega. +lia. Qed. Section digits_aux. @@ -788,7 +793,7 @@ pattern (radix_val beta) at 2 5 ; replace (radix_val beta) with (Zpower beta 1) rewrite <- Zpower_plus. rewrite Zplus_comm. apply IHu. -clear -Hv ; omega. +clear -Hv ; lia. split. now ring_simplify (1 + v - 1)%Z. now rewrite Zplus_assoc. @@ -928,7 +933,7 @@ intros x y Zx Hxy. assert (Hx := Zdigits_correct x). assert (Hy := Zdigits_correct y). apply (Zpower_lt_Zpower beta). -zify ; omega. +zify ; lia. Qed. Theorem lt_Zdigits : @@ -938,7 +943,7 @@ Theorem lt_Zdigits : (x < y)%Z. Proof. intros x y Hy. -cut (y <= x -> Zdigits y <= Zdigits x)%Z. omega. +cut (y <= x -> Zdigits y <= Zdigits x)%Z. lia. now apply Zdigits_le. Qed. @@ -951,7 +956,7 @@ intros e x Hex. destruct (Zdigits_correct x) as [H1 H2]. apply Z.le_trans with (2 := H1). apply Zpower_le. -clear -Hex ; omega. +clear -Hex ; lia. Qed. Theorem Zdigits_le_Zpower : @@ -961,7 +966,7 @@ Theorem Zdigits_le_Zpower : Proof. intros e x. generalize (Zpower_le_Zdigits e x). -omega. +lia. Qed. Theorem Zpower_gt_Zdigits : @@ -982,7 +987,7 @@ Theorem Zdigits_gt_Zpower : Proof. intros e x Hex. generalize (Zpower_gt_Zdigits e x). -omega. +lia. Qed. (** Number of digits of a product. @@ -1010,8 +1015,8 @@ apply Zdigits_correct. apply Zlt_le_succ. rewrite <- (Z.abs_eq y) at 1 by easy. apply Zdigits_correct. -clear -Hx ; omega. -clear -Hy ; omega. +clear -Hx ; lia. +clear -Hy ; lia. change Z0 with (0 + 0 + 0)%Z. apply Zplus_le_compat. now apply Zplus_le_compat. @@ -1031,7 +1036,7 @@ apply Zdigits_le. apply Zabs_pos. rewrite Zabs_Zmult. generalize (Zabs_pos x) (Zabs_pos y). -omega. +lia. apply Zdigits_mult_strong ; apply Zabs_pos. Qed. @@ -1041,7 +1046,7 @@ Theorem Zdigits_mult_ge : (Zdigits x + Zdigits y - 1 <= Zdigits (x * y))%Z. Proof. intros x y Zx Zy. -cut ((Zdigits x - 1) + (Zdigits y - 1) < Zdigits (x * y))%Z. omega. +cut ((Zdigits x - 1) + (Zdigits y - 1) < Zdigits (x * y))%Z. lia. apply Zdigits_gt_Zpower. rewrite Zabs_Zmult. rewrite Zpower_exp. @@ -1052,8 +1057,8 @@ apply Zpower_le_Zdigits. apply Zlt_pred. apply Zpower_ge_0. apply Zpower_ge_0. -generalize (Zdigits_gt_0 x). omega. -generalize (Zdigits_gt_0 y). omega. +generalize (Zdigits_gt_0 x). lia. +generalize (Zdigits_gt_0 y). lia. Qed. Theorem Zdigits_div_Zpower : @@ -1073,7 +1078,7 @@ destruct (Zle_lt_or_eq _ _ (proj2 He)) as [He'|He']. replace (Zdigits m - e - 1)%Z with (Zdigits m - 1 - e)%Z by ring. rewrite Z.pow_sub_r. 2: apply Zgt_not_eq, radix_gt_0. - 2: clear -He He' ; omega. + 2: clear -He He' ; lia. apply Z_div_le with (2 := H1). now apply Z.lt_gt, Zpower_gt_0. apply Zmult_lt_reg_r with (Zpower beta e). @@ -1118,13 +1123,6 @@ rewrite <- Zpower_nat_Z. apply digits2_Pnat_correct. Qed. -Fixpoint digits2_pos (n : positive) : positive := - match n with - | xH => xH - | xO p => Pos.succ (digits2_pos p) - | xI p => Pos.succ (digits2_pos p) - end. - Theorem Zpos_digits2_pos : forall m : positive, Zpos (digits2_pos m) = Zdigits radix2 (Zpos m). @@ -1137,13 +1135,6 @@ induction m ; simpl ; try easy ; apply f_equal, IHm. Qed. -Definition Zdigits2 n := - match n with - | Z0 => n - | Zpos p => Zpos (digits2_pos p) - | Zneg p => Zpos (digits2_pos p) - end. - Lemma Zdigits2_Zdigits : forall n, Zdigits2 n = Zdigits radix2 n. Proof. diff --git a/flocq/Core/FIX.v b/flocq/Core/FIX.v index 4e0a25e6..779d94cb 100644 --- a/flocq/Core/FIX.v +++ b/flocq/Core/FIX.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * Fixed-point format *) + +From Coq Require Import Lia. Require Import Raux Defs Round_pred Generic_fmt Ulp Round_NE. Section RND_FIX. @@ -86,9 +88,16 @@ intros x; unfold ulp. case Req_bool_spec; intros Zx. case (negligible_exp_spec FIX_exp). intros T; specialize (T (emin-1)%Z); contradict T. -unfold FIX_exp; omega. +unfold FIX_exp; lia. intros n _; reflexivity. reflexivity. Qed. +Global Instance exists_NE_FIX : + Exists_NE beta FIX_exp. +Proof. +unfold Exists_NE, FIX_exp; simpl. +right; split; auto. +Qed. + End RND_FIX. diff --git a/flocq/Core/FLT.v b/flocq/Core/FLT.v index bd48d4b7..7301328d 100644 --- a/flocq/Core/FLT.v +++ b/flocq/Core/FLT.v @@ -46,7 +46,7 @@ intros k. unfold FLT_exp. generalize (prec_gt_0 prec). repeat split ; - intros ; zify ; omega. + intros ; zify ; lia. Qed. Theorem generic_format_FLT : @@ -93,24 +93,28 @@ simpl in ex. specialize (He Hx0). apply Rlt_le_trans with (1 := proj2 He). apply bpow_le. -cut (ex' - prec <= ex)%Z. omega. +cut (ex' - prec <= ex)%Z. lia. unfold ex, FLT_exp. apply Z.le_max_l. apply Z.le_max_r. Qed. - -Theorem FLT_format_bpow : +Theorem generic_format_FLT_bpow : forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e). Proof. intros e He. apply generic_format_bpow; unfold FLT_exp. apply Z.max_case; try assumption. -unfold Prec_gt_0 in prec_gt_0_; omega. +unfold Prec_gt_0 in prec_gt_0_; lia. Qed. - - +Theorem FLT_format_bpow : + forall e, (emin <= e)%Z -> FLT_format (bpow e). +Proof. +intros e He. +apply FLT_format_generic. +now apply generic_format_FLT_bpow. +Qed. Theorem FLT_format_satisfies_any : satisfies_any FLT_format. @@ -136,12 +140,40 @@ apply Zmax_left. destruct (mag beta x) as (ex, He). unfold FLX_exp. simpl. specialize (He Hx0). -cut (emin + prec - 1 < ex)%Z. omega. +cut (emin + prec - 1 < ex)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1 := Hx). apply He. Qed. +(** FLT is a nice format: it has a monotone exponent... *) +Global Instance FLT_exp_monotone : Monotone_exp FLT_exp. +Proof. +intros ex ey. +unfold FLT_exp. +zify ; lia. +Qed. + +(** and it allows a rounding to nearest, ties to even. *) +Global Instance exists_NE_FLT : + (Z.even beta = false \/ (1 < prec)%Z) -> + Exists_NE beta FLT_exp. +Proof. +intros [H|H]. +now left. +right. +intros e. +unfold FLT_exp. +destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ; + rewrite H2 ; clear H2. +generalize (Zmax_spec (e + 1 - prec) emin). +generalize (Zmax_spec (e - prec + 1 - prec) emin). +lia. +generalize (Zmax_spec (e + 1 - prec) emin). +generalize (Zmax_spec (emin + 1 - prec) emin). +lia. +Qed. + (** Links between FLT and FLX *) Theorem generic_format_FLT_FLX : forall x : R, @@ -192,7 +224,7 @@ apply Zmax_right. unfold FIX_exp. destruct (mag beta x) as (ex, Hex). simpl. -cut (ex - 1 < emin + prec)%Z. omega. +cut (ex - 1 < emin + prec)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (2 := Hx). now apply Hex. @@ -222,7 +254,7 @@ apply generic_inclusion_le... intros e He. unfold FIX_exp. apply Z.max_lub. -omega. +lia. apply Z.le_refl. Qed. @@ -238,45 +270,53 @@ destruct (Z.max_spec (n - prec) emin) as [(Hm, Hm')|(Hm, Hm')]. revert Hn prec_gt_0_; unfold FLT_exp, Prec_gt_0; rewrite Hm'; lia. Qed. -Theorem generic_format_FLT_1 (Hemin : (emin <= 0)%Z) : +Theorem generic_format_FLT_1 : + (emin <= 0)%Z -> generic_format beta FLT_exp 1. Proof. -unfold generic_format, scaled_mantissa, cexp, F2R; simpl. -rewrite Rmult_1_l, (mag_unique beta 1 1). -{ unfold FLT_exp. - destruct (Z.max_spec_le (1 - prec) emin) as [(H,Hm)|(H,Hm)]; rewrite Hm; - (rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]); - (rewrite Ztrunc_IZR, IZR_Zpower, <-bpow_plus; - [|unfold Prec_gt_0 in prec_gt_0_; omega]); - now replace (_ + _)%Z with Z0 by ring. } -rewrite Rabs_R1; simpl; split; [now right|]. -rewrite IZR_Zpower_pos; simpl; rewrite Rmult_1_r; apply IZR_lt. -apply (Z.lt_le_trans _ 2); [omega|]; apply Zle_bool_imp_le, beta. +intros Hemin. +now apply (generic_format_FLT_bpow 0). Qed. -Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R -> - ulp beta FLT_exp x = bpow emin. -Proof with auto with typeclass_instances. +Theorem ulp_FLT_0 : + ulp beta FLT_exp 0 = bpow emin. +Proof. +unfold ulp. +rewrite Req_bool_true by easy. +case negligible_exp_spec. +- intros T. + elim Zle_not_lt with (2 := T emin). + apply Z.le_max_r. +- intros n Hn. + apply f_equal. + assert (H: FLT_exp emin = emin). + apply Z.max_r. + generalize (prec_gt_0 prec). + clear ; lia. + rewrite <- H. + apply fexp_negligible_exp_eq. + apply FLT_exp_valid. + exact Hn. + rewrite H. + apply Z.le_refl. +Qed. + +Theorem ulp_FLT_small : + forall x, (Rabs x < bpow (emin + prec))%R -> + ulp beta FLT_exp x = bpow emin. +Proof. intros x Hx. -unfold ulp; case Req_bool_spec; intros Hx2. -(* x = 0 *) -case (negligible_exp_spec FLT_exp). -intros T; specialize (T (emin-1)%Z); contradict T. -apply Zle_not_lt; unfold FLT_exp. -apply Z.le_trans with (2:=Z.le_max_r _ _); omega. -assert (V:FLT_exp emin = emin). -unfold FLT_exp; apply Z.max_r. -unfold Prec_gt_0 in prec_gt_0_; omega. -intros n H2; rewrite <-V. -apply f_equal, fexp_negligible_exp_eq... -omega. -(* x <> 0 *) -apply f_equal; unfold cexp, FLT_exp. +destruct (Req_dec x 0%R) as [Zx|Zx]. +{ rewrite Zx. + apply ulp_FLT_0. } +rewrite ulp_neq_0 by easy. +apply f_equal. apply Z.max_r. -assert (mag beta x-1 < emin+prec)%Z;[idtac|omega]. -destruct (mag beta x) as (e,He); simpl. +destruct (mag beta x) as [e He]. +simpl. +cut (e - 1 < emin + prec)%Z. lia. apply lt_bpow with beta. -apply Rle_lt_trans with (2:=Hx). +apply Rle_lt_trans with (2 := Hx). now apply He. Qed. @@ -295,8 +335,8 @@ apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R. rewrite <- bpow_plus. right; apply f_equal. replace (e - 1 + (1 - prec))%Z with (e - prec)%Z by ring. -apply Z.max_l. -assert (emin+prec-1 < e)%Z; try omega. +apply Z.max_l; simpl. +assert (emin+prec-1 < e)%Z; try lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=Hx). now apply He. @@ -334,7 +374,7 @@ unfold ulp; rewrite Req_bool_false; [|now intro H; apply Nzx, (Rmult_eq_reg_r (bpow e)); [rewrite Rmult_0_l|apply Rgt_not_eq, Rlt_gt, bpow_gt_0]]. rewrite (Req_bool_false _ _ Nzx), <- bpow_plus; f_equal; unfold cexp, FLT_exp. -rewrite (mag_mult_bpow _ _ _ Nzx), !Z.max_l; omega. +rewrite (mag_mult_bpow _ _ _ Nzx), !Z.max_l; lia. Qed. Lemma succ_FLT_exact_shift_pos : @@ -375,32 +415,106 @@ fold (Req_bool (-x) (bpow (mag beta (-x) - 1))); case Req_bool. rewrite ulp_FLT_exact_shift; [ring|lra| |]; rewrite mag_opp; lia. Qed. -(** FLT is a nice format: it has a monotone exponent... *) -Global Instance FLT_exp_monotone : Monotone_exp FLT_exp. -Proof. -intros ex ey. -unfold FLT_exp. -zify ; omega. -Qed. - -(** and it allows a rounding to nearest, ties to even. *) -Hypothesis NE_prop : Z.even beta = false \/ (1 < prec)%Z. - -Global Instance exists_NE_FLT : Exists_NE beta FLT_exp. +Theorem ulp_FLT_pred_pos : + forall x, + generic_format beta FLT_exp x -> + (0 <= x)%R -> + ulp beta FLT_exp (pred beta FLT_exp x) = ulp beta FLT_exp x \/ + (x = bpow (mag beta x - 1) /\ ulp beta FLT_exp (pred beta FLT_exp x) = (ulp beta FLT_exp x / IZR beta)%R). Proof. -destruct NE_prop as [H|H]. -now left. -right. -intros e. -unfold FLT_exp. -destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ; - rewrite H2 ; clear H2. -generalize (Zmax_spec (e + 1 - prec) emin). -generalize (Zmax_spec (e - prec + 1 - prec) emin). -omega. -generalize (Zmax_spec (e + 1 - prec) emin). -generalize (Zmax_spec (emin + 1 - prec) emin). -omega. +intros x Fx [Hx|Hx] ; cycle 1. +{ rewrite <- Hx. + rewrite pred_0. + rewrite ulp_opp. + left. + apply ulp_ulp_0. + apply FLT_exp_valid. + typeclasses eauto. } +assert (Hp: (0 <= pred beta FLT_exp x)%R). +{ apply pred_ge_gt ; try easy. + apply FLT_exp_valid. + apply generic_format_0. } +destruct (Rle_or_lt (bpow (emin + prec)) x) as [Hs|Hs]. +- unfold ulp. + rewrite Req_bool_false ; cycle 1. + { intros Zp. + apply Rle_not_lt with (1 := Hs). + generalize (f_equal (succ beta FLT_exp) Zp). + rewrite succ_pred. + rewrite succ_0, ulp_FLT_0. + intros H. + rewrite H. + apply bpow_lt. + generalize (prec_gt_0 prec). + lia. + apply FLT_exp_valid. + exact Fx. } + rewrite Req_bool_false by now apply Rgt_not_eq. + unfold cexp. + destruct (mag beta x) as [e He]. + simpl. + specialize (He (Rgt_not_eq _ _ Hx)). + rewrite Rabs_pos_eq in He by now apply Rlt_le. + destruct (proj1 He) as [Hb|Hb]. + + left. + apply (f_equal (fun v => bpow (FLT_exp v))). + apply mag_unique. + rewrite Rabs_pos_eq by easy. + split. + * apply pred_ge_gt ; try easy. + apply FLT_exp_valid. + apply generic_format_FLT_bpow. + apply Z.lt_le_pred. + apply lt_bpow with beta. + apply Rle_lt_trans with (2 := proj2 He). + apply Rle_trans with (2 := Hs). + apply bpow_le. + generalize (prec_gt_0 prec). + lia. + * apply pred_lt_le. + now apply Rgt_not_eq. + now apply Rlt_le. + + right. + split. + easy. + replace (FLT_exp _) with (FLT_exp e + -1)%Z. + rewrite bpow_plus. + now rewrite <- (Zmult_1_r beta). + rewrite <- Hb. + unfold FLT_exp at 1 2. + replace (mag_val _ _ (mag _ _)) with (e - 1)%Z. + rewrite <- Hb in Hs. + apply le_bpow in Hs. + zify ; lia. + apply eq_sym, mag_unique. + rewrite Hb. + rewrite Rabs_pos_eq by easy. + split ; cycle 1. + { apply pred_lt_id. + now apply Rgt_not_eq. } + apply pred_ge_gt. + apply FLT_exp_valid. + apply generic_format_FLT_bpow. + cut (emin + 1 < e)%Z. lia. + apply lt_bpow with beta. + apply Rle_lt_trans with (2 := proj2 He). + apply Rle_trans with (2 := Hs). + apply bpow_le. + generalize (prec_gt_0 prec). + lia. + exact Fx. + apply Rlt_le_trans with (2 := proj1 He). + apply bpow_lt. + apply Z.lt_pred_l. +- left. + rewrite (ulp_FLT_small x). + apply ulp_FLT_small. + rewrite Rabs_pos_eq by easy. + apply pred_lt_le. + now apply Rgt_not_eq. + now apply Rlt_le. + rewrite Rabs_pos_eq by now apply Rlt_le. + exact Hs. Qed. End RND_FLT. diff --git a/flocq/Core/FLX.v b/flocq/Core/FLX.v index 803d96ef..78bffba5 100644 --- a/flocq/Core/FLX.v +++ b/flocq/Core/FLX.v @@ -48,7 +48,7 @@ Proof. intros k. unfold FLX_exp. generalize prec_gt_0. -repeat split ; intros ; omega. +repeat split ; intros ; lia. Qed. Theorem FIX_format_FLX : @@ -212,7 +212,7 @@ Proof. case (negligible_exp_spec FLX_exp). intros _; reflexivity. intros n H2; contradict H2. -unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega. +unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; lia. Qed. Theorem generic_format_FLX_1 : @@ -221,13 +221,13 @@ Proof. unfold generic_format, scaled_mantissa, cexp, F2R; simpl. rewrite Rmult_1_l, (mag_unique beta 1 1). { unfold FLX_exp. - rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]. - rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]. + rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; lia]. + rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; lia]. rewrite <- bpow_plus. now replace (_ + _)%Z with Z0 by ring. } rewrite Rabs_R1; simpl; split; [now right|]. unfold Z.pow_pos; simpl; rewrite Zmult_1_r; apply IZR_lt. -assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); omega. +assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); lia. Qed. Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R. @@ -356,7 +356,7 @@ destruct NE_prop as [H|H]. now left. right. unfold FLX_exp. -split ; omega. +split ; lia. Qed. End RND_FLX. diff --git a/flocq/Core/FTZ.v b/flocq/Core/FTZ.v index 1a93bcd9..d6bae6ea 100644 --- a/flocq/Core/FTZ.v +++ b/flocq/Core/FTZ.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * Floating-point format with abrupt underflow *) + +From Coq Require Import Lia. Require Import Raux Defs Round_pred Generic_fmt. Require Import Float_prop Ulp FLX. @@ -48,22 +50,22 @@ unfold FTZ_exp. generalize (Zlt_cases (k - prec) emin). case (Zlt_bool (k - prec) emin) ; intros H1. split ; intros H2. -omega. +lia. split. generalize (Zlt_cases (emin + prec + 1 - prec) emin). case (Zlt_bool (emin + prec + 1 - prec) emin) ; intros H3. -omega. +lia. generalize (Zlt_cases (emin + prec - 1 + 1 - prec) emin). generalize (prec_gt_0 prec). -case (Zlt_bool (emin + prec - 1 + 1 - prec) emin) ; omega. +case (Zlt_bool (emin + prec - 1 + 1 - prec) emin) ; lia. intros l H3. generalize (Zlt_cases (l - prec) emin). -case (Zlt_bool (l - prec) emin) ; omega. +case (Zlt_bool (l - prec) emin) ; lia. split ; intros H2. generalize (Zlt_cases (k + 1 - prec) emin). -case (Zlt_bool (k + 1 - prec) emin) ; omega. +case (Zlt_bool (k + 1 - prec) emin) ; lia. generalize (prec_gt_0 prec). -split ; intros ; omega. +split ; intros ; lia. Qed. Theorem FLXN_format_FTZ : @@ -94,7 +96,7 @@ rewrite Zlt_bool_false. apply Z.le_refl. rewrite Hx1, mag_F2R with (1 := Zxm). cut (prec - 1 < mag beta (IZR xm))%Z. -clear -Hx3 ; omega. +clear -Hx3 ; lia. apply mag_gt_Zpower with (1 := Zxm). apply Hx2. apply generic_format_FLXN. @@ -135,7 +137,7 @@ change (0 < F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))) (e rewrite F2R_Zabs, <- Hx2. now apply Rabs_pos_lt. apply bpow_le. -omega. +lia. rewrite Hx2. eexists ; repeat split ; simpl. apply le_IZR. @@ -186,7 +188,7 @@ intros e He. unfold FTZ_exp. rewrite Zlt_bool_false. apply Z.le_refl. -omega. +lia. Qed. Theorem ulp_FTZ_0 : @@ -196,12 +198,12 @@ unfold ulp; rewrite Req_bool_true; trivial. case (negligible_exp_spec FTZ_exp). intros T; specialize (T (emin-1)%Z); contradict T. apply Zle_not_lt; unfold FTZ_exp; unfold Prec_gt_0 in prec_gt_0_. -rewrite Zlt_bool_true; omega. +rewrite Zlt_bool_true; lia. assert (V:(FTZ_exp (emin+prec-1) = emin+prec-1)%Z). -unfold FTZ_exp; rewrite Zlt_bool_true; omega. +unfold FTZ_exp; rewrite Zlt_bool_true; lia. intros n H2; rewrite <-V. apply f_equal, fexp_negligible_exp_eq... -omega. +lia. Qed. @@ -290,12 +292,12 @@ apply Rle_trans with (2 := proj1 He). apply bpow_le. unfold FLX_exp. generalize (prec_gt_0 prec). -clear -He' ; omega. +clear -He' ; lia. apply bpow_ge_0. unfold FLX_exp, FTZ_exp. rewrite Zlt_bool_false. apply refl_equal. -clear -He' ; omega. +clear -He' ; lia. Qed. Theorem round_FTZ_small : @@ -331,7 +333,7 @@ intros He'. elim Rlt_not_le with (1 := Hx). apply Rle_trans with (2 := proj1 He). apply bpow_le. -omega. +lia. apply bpow_ge_0. Qed. diff --git a/flocq/Core/Float_prop.v b/flocq/Core/Float_prop.v index 804dd397..a1f48d04 100644 --- a/flocq/Core/Float_prop.v +++ b/flocq/Core/Float_prop.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * Basic properties of floating-point formats: lemmas about mantissa, exponent... *) + +From Coq Require Import Lia. Require Import Raux Defs Digits. Section Float_prop. @@ -360,7 +362,7 @@ unfold F2R. simpl. apply Rmult_le_compat_r. apply bpow_ge_0. apply IZR_le. -omega. +lia. Qed. Theorem F2R_lt_bpow : @@ -379,7 +381,7 @@ rewrite <-IZR_Zpower. 2: now apply Zle_left. now apply IZR_lt. elim Zlt_not_le with (1 := Hm). simpl. -cut (e' - e < 0)%Z. 2: omega. +cut (e' - e < 0)%Z. 2: lia. clear. case (e' - e)%Z ; try easy. intros p _. @@ -413,7 +415,7 @@ now elim (Zle_not_lt _ _ (Zabs_pos m)). (* . *) replace (e - e' + p)%Z with (e - (e' - p))%Z by ring. apply F2R_change_exp. -cut (e' - 1 < e + p)%Z. omega. +cut (e' - 1 < e + p)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1 := Hf). rewrite <- F2R_Zabs, Zplus_comm, bpow_plus. @@ -472,10 +474,10 @@ assert (Hd := Zdigits_correct beta n). assert (Hd' := Zdigits_gt_0 beta n). apply Zle_antisym ; apply (bpow_lt_bpow beta). apply Rle_lt_trans with (2 := proj2 He). -rewrite <- IZR_Zpower by omega. +rewrite <- IZR_Zpower by lia. now apply IZR_le. apply Rle_lt_trans with (1 := proj1 He). -rewrite <- IZR_Zpower by omega. +rewrite <- IZR_Zpower by lia. now apply IZR_lt. Qed. diff --git a/flocq/Core/Generic_fmt.v b/flocq/Core/Generic_fmt.v index cb37bd91..af1bf3c1 100644 --- a/flocq/Core/Generic_fmt.v +++ b/flocq/Core/Generic_fmt.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * What is a real number belonging to a format, and many properties. *) + +From Coq Require Import Lia. Require Import Raux Defs Round_pred Float_prop. Section Generic. @@ -52,7 +54,7 @@ apply Znot_ge_lt. intros Hl. apply Z.ge_le in Hl. assert (H' := proj2 (proj2 (valid_exp l) Hl) k). -omega. +lia. Qed. Theorem valid_exp_large' : @@ -67,7 +69,7 @@ apply Z.ge_le in H'. assert (Hl := Z.le_trans _ _ _ H H'). apply valid_exp in Hl. assert (H1 := proj2 Hl k H'). -omega. +lia. Qed. Definition cexp x := @@ -425,7 +427,7 @@ rewrite Gx. replace (Ztrunc (scaled_mantissa x)) with Z0. apply F2R_0. cut (Z.abs (Ztrunc (scaled_mantissa x)) < 1)%Z. -clear ; zify ; omega. +clear ; zify ; lia. apply lt_IZR. rewrite abs_IZR. now rewrite <- scaled_mantissa_generic. @@ -522,7 +524,7 @@ specialize (Ex Hxz). apply Rlt_le_trans with (1 := proj2 Ex). apply bpow_le. specialize (Hp ex). -omega. +lia. Qed. Theorem generic_format_bpow_inv' : @@ -544,7 +546,7 @@ apply bpow_gt_0. split. apply bpow_ge_0. apply (bpow_lt _ _ 0). -clear -He ; omega. +clear -He ; lia. Qed. Theorem generic_format_bpow_inv : @@ -555,7 +557,7 @@ Proof. intros e He. apply generic_format_bpow_inv' in He. assert (H := valid_exp_large' (e + 1) e). -omega. +lia. Qed. Section Fcore_generic_round_pos. @@ -587,7 +589,7 @@ rewrite <- (Zrnd_IZR (Zceil x)). apply Zrnd_le. apply Zceil_ub. rewrite Zceil_floor_neq. -omega. +lia. intros H. rewrite <- H in Hx. rewrite Zfloor_IZR, Zrnd_IZR in Hx. @@ -630,7 +632,7 @@ apply Rmult_le_compat_r. apply bpow_ge_0. assert (Hf: IZR (Zpower beta (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)). apply IZR_Zpower. -omega. +lia. rewrite <- Hf. apply IZR_le. apply Zfloor_lub. @@ -657,7 +659,7 @@ apply Rmult_le_compat_r. apply bpow_ge_0. assert (Hf: IZR (Zpower beta (ex - fexp ex)) = bpow (ex - fexp ex)). apply IZR_Zpower. -omega. +lia. rewrite <- Hf. apply IZR_le. apply Zceil_glb. @@ -738,7 +740,7 @@ destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1]. apply bpow_le. apply valid_exp, proj2 in Hx1. specialize (Hx1 ey). - omega. + lia. apply Rle_trans with (bpow ex). now apply round_bounded_large_pos. apply bpow_le. @@ -1380,7 +1382,7 @@ specialize (He (Rgt_not_eq _ _ Hx)). rewrite Rabs_pos_eq in He. 2: now apply Rlt_le. apply Rle_trans with (bpow (ex - 1)). apply bpow_le. -cut (e < ex)%Z. omega. +cut (e < ex)%Z. lia. apply (lt_bpow beta). now apply Rle_lt_trans with (2 := proj2 He). destruct (Zle_or_lt ex (fexp ex)). @@ -1389,7 +1391,7 @@ rewrite Hr in Hd. elim Rlt_irrefl with (1 := Hd). rewrite Hr. apply bpow_le. -omega. +lia. apply (round_bounded_large_pos rnd x ex H He). Qed. @@ -1526,7 +1528,7 @@ unfold cexp. set (ex := mag beta x). generalize (exp_not_FTZ ex). generalize (proj2 (proj2 (valid_exp _) He) (fexp ex + 1)%Z). -omega. +lia. rewrite <- H. rewrite <- mult_IZR, Ztrunc_IZR. unfold F2R. simpl. @@ -1802,7 +1804,7 @@ Theorem Znearest_imp : Proof. intros x n Hd. cut (Z.abs (Znearest x - n) < 1)%Z. -clear ; zify ; omega. +clear ; zify ; lia. apply lt_IZR. rewrite abs_IZR, minus_IZR. replace (IZR (Znearest x) - IZR n)%R with (- (x - IZR (Znearest x)) + (x - IZR n))%R by ring. @@ -1937,7 +1939,7 @@ replace (- _ + _)%Z with 0%Z by ring; simpl; rewrite Rmult_1_r. apply (Rlt_le_trans _ _ _ (proj2 Hex)). apply Rle_trans with (bpow (fexp (mag beta x) - 1)). - apply bpow_le. - rewrite (mag_unique beta x ex); [omega|]. + rewrite (mag_unique beta x ex); [lia|]. now rewrite Rabs_right. - unfold Zminus; rewrite bpow_plus. rewrite Rmult_comm. @@ -2012,6 +2014,68 @@ Qed. End rndNA. +Notation Znearest0 := (Znearest (fun x => (Zlt_bool x 0))). + +Section rndN0. + +Global Instance valid_rnd_N0 : Valid_rnd Znearest0 := valid_rnd_N _. + +Theorem round_N0_pt : + forall x, + Rnd_N0_pt generic_format x (round Znearest0 x). +Proof. +intros x. +generalize (round_N_pt (fun t => Zlt_bool t 0) x). +set (f := round (Znearest (fun t => Zlt_bool t 0)) x). +intros Rxf. +destruct (Req_dec (x - round Zfloor x) (round Zceil x - x)) as [Hm|Hm]. +(* *) +apply Rnd_N0_pt_N. +apply generic_format_0. +exact Rxf. +destruct (Rle_or_lt 0 x) as [Hx|Hx]. +(* . *) +rewrite Rabs_pos_eq with (1 := Hx). +rewrite Rabs_pos_eq. +unfold f. +rewrite round_N_middle with (1 := Hm). +rewrite Zlt_bool_false. +now apply round_DN_pt. +apply Zfloor_lub. +apply Rmult_le_pos with (1 := Hx). +apply bpow_ge_0. +apply Rnd_N_pt_ge_0 with (2 := Hx) (3 := Rxf). +apply generic_format_0. +(* . *) +rewrite Rabs_left with (1 := Hx). +rewrite Rabs_left1. +apply Ropp_le_contravar. +unfold f. +rewrite round_N_middle with (1 := Hm). +rewrite Zlt_bool_true. +now apply round_UP_pt. +apply lt_IZR. +apply Rle_lt_trans with (scaled_mantissa x). +apply Zfloor_lb. +simpl. +rewrite <- (Rmult_0_l (bpow (- (cexp x))%Z)%R). +apply Rmult_lt_compat_r with (2 := Hx). +apply bpow_gt_0. +apply Rnd_N_pt_le_0 with (3 := Rxf). +apply generic_format_0. +now apply Rlt_le. +(* *) +split. +apply Rxf. +intros g Rxg. +rewrite Rnd_N_pt_unique with (3 := Hm) (4 := Rxf) (5 := Rxg). +apply Rle_refl. +apply round_DN_pt; easy. +apply round_UP_pt; easy. +Qed. + +End rndN0. + Section rndN_opp. Theorem Znearest_opp : @@ -2055,6 +2119,31 @@ rewrite opp_IZR. now rewrite Ropp_mult_distr_l_reverse. Qed. +Lemma round_N0_opp : + forall x, + (round Znearest0 (- x) = - round Znearest0 x)%R. +Proof. +intros x. +rewrite round_N_opp. +apply Ropp_eq_compat. +apply round_ext. +clear x; intro x. +unfold Znearest. +case_eq (Rcompare (x - IZR (Zfloor x)) (/ 2)); intro C; +[|reflexivity|reflexivity]. +apply Rcompare_Eq_inv in C. +assert (H : negb (- (Zfloor x + 1) @@ -1305,9 +1317,9 @@ rewrite Ropp_inv_permute with (1 := Zy'). rewrite <- 2!opp_IZR. rewrite <- Zmod_opp_opp. apply H. -clear -Hy. omega. +clear -Hy. lia. apply H. -clear -Zy Hy. omega. +clear -Zy Hy. lia. (* *) split. pattern (IZR (x / y)) at 1 ; rewrite <- Rplus_0_r. @@ -1454,7 +1466,7 @@ rewrite <- (Rmult_1_r (bpow e1)). rewrite bpow_plus. apply Rmult_lt_compat_l. apply bpow_gt_0. -assert (0 < e2 - e1)%Z by omega. +assert (0 < e2 - e1)%Z by lia. destruct (e2 - e1)%Z ; try discriminate H0. clear. rewrite <- IZR_Zpower by easy. @@ -1756,7 +1768,7 @@ rewrite Rabs_right in Hex; [|now apply Rle_ge; apply Rlt_le]. rewrite Rabs_right in Hey; [|now apply Rle_ge; apply Rlt_le]. apply (Rlt_le_trans _ _ _ Hex). apply Rle_trans with (bpow (ey - 1)); [|exact Hey]. -now apply bpow_le; omega. +now apply bpow_le; lia. Qed. Theorem mag_bpow : @@ -1900,7 +1912,7 @@ apply bpow_le. now apply Zlt_le_weak. apply IZR_le. clear -Zm. -zify ; omega. +zify ; lia. Qed. Lemma mag_mult : @@ -1999,7 +2011,7 @@ assert (Hbeta : (2 <= r)%Z). { destruct r as (beta_val,beta_prop). now apply Zle_bool_imp_le. } intros x y Px Py Hln. -assert (Oxy : (y < x)%R); [apply lt_mag;[assumption|omega]|]. +assert (Oxy : (y < x)%R); [apply lt_mag;[assumption|lia]|]. destruct (mag x) as (ex,Hex). destruct (mag y) as (ey,Hey). simpl in Hln |- *. @@ -2096,7 +2108,7 @@ split. unfold Rsqr ; rewrite <- bpow_plus. apply bpow_le. generalize (Zdiv2_odd_eqn (e + 1)). - destruct Z.odd ; intros ; omega. + destruct Z.odd ; intros ; lia. - rewrite <- (Rabs_pos_eq (bpow _)) by apply bpow_ge_0. apply Rsqr_lt_abs_0. rewrite Rsqr_sqrt by now apply Rlt_le. @@ -2104,7 +2116,7 @@ split. unfold Rsqr ; rewrite <- bpow_plus. apply bpow_le. generalize (Zdiv2_odd_eqn (e + 1)). - destruct Z.odd ; intros ; omega. + destruct Z.odd ; intros ; lia. Qed. Lemma mag_1 : mag 1 = 1%Z :> Z. @@ -2324,7 +2336,7 @@ refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _). refine (H _ _ Py). apply INR_lt in Hy. clear -Hy HyN. - omega. + lia. now apply Rlt_le, Rinv_0_lt_compat. rewrite S_INR, HN. ring_simplify (IZR (up (/ l)) - 1 + 1)%R. @@ -2369,7 +2381,7 @@ rewrite <- (Z.opp_involutive n). rewrite <- (Z.abs_neq n). rewrite <- Zabs2Nat.id_abs. apply K. -omega. +lia. Qed. diff --git a/flocq/Core/Round_NE.v b/flocq/Core/Round_NE.v index 20b60ef5..b7387a62 100644 --- a/flocq/Core/Round_NE.v +++ b/flocq/Core/Round_NE.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * Rounding to nearest, ties to even: existence, unicity... *) + +From Coq Require Import Lia. Require Import Raux Defs Round_pred Generic_fmt Float_prop Ulp. Notation ZnearestE := (Znearest (fun x => negb (Z.even x))). @@ -148,7 +150,7 @@ split. apply (round_DN_pt beta fexp x). apply generic_format_bpow. ring_simplify (ex - 1 + 1)%Z. -omega. +lia. apply Hex. apply Rle_lt_trans with (2 := proj2 Hex). apply (round_DN_pt beta fexp x). @@ -209,14 +211,14 @@ rewrite Z.even_add. rewrite eqb_sym. simpl. fold (negb (Z.even (beta ^ (ex - fexp ex)))). rewrite Bool.negb_involutive. -rewrite (Z.even_pow beta (ex - fexp ex)). 2: omega. +rewrite (Z.even_pow beta (ex - fexp ex)) by lia. destruct exists_NE_. rewrite H. apply Zeven_Zpower_odd with (2 := H). now apply Zle_minus_le_0. apply Z.even_pow. specialize (H ex). -omega. +lia. (* - xu < bpow ex *) revert Hud. rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. @@ -413,18 +415,18 @@ now rewrite Hs in Hr. destruct (Hs ex) as (H,_). rewrite Z.even_pow. exact Hr. -omega. +lia. assert (Z.even (Zfloor mx) = true). 2: now rewrite H in Hmx. -replace (Zfloor mx) with (Zceil mx + -1)%Z by omega. +replace (Zfloor mx) with (Zceil mx + -1)%Z by lia. rewrite Z.even_add. apply eqb_true. unfold mx. replace (Zceil (scaled_mantissa beta fexp x)) with (Zpower beta (ex - fexp ex)). rewrite Zeven_Zpower_odd with (2 := Hr). easy. -omega. +lia. apply eq_IZR. -rewrite IZR_Zpower. 2: omega. +rewrite IZR_Zpower by lia. apply Rmult_eq_reg_r with (bpow (fexp ex)). unfold Zminus. rewrite bpow_plus. @@ -434,7 +436,7 @@ now apply sym_eq. apply Rgt_not_eq. apply bpow_gt_0. generalize (proj1 (valid_exp ex) He). -omega. +lia. (* .. small pos *) assert (Z.even (Zfloor mx) = true). 2: now rewrite H in Hmx. unfold mx, scaled_mantissa. diff --git a/flocq/Core/Round_pred.v b/flocq/Core/Round_pred.v index 428a4bac..b7b6778f 100644 --- a/flocq/Core/Round_pred.v +++ b/flocq/Core/Round_pred.v @@ -42,6 +42,9 @@ Definition Rnd_NG (F : R -> Prop) (P : R -> R -> Prop) (rnd : R -> R) := Definition Rnd_NA (F : R -> Prop) (rnd : R -> R) := forall x : R, Rnd_NA_pt F x (rnd x). +Definition Rnd_N0 (F : R -> Prop) (rnd : R -> R) := + forall x : R, Rnd_N0_pt F x (rnd x). + Theorem round_val_of_pred : forall rnd : R -> R -> Prop, round_pred rnd -> @@ -1021,6 +1024,251 @@ intros F x f (Hf,_) Hx. now apply Rnd_N_pt_idempotent with F. Qed. +Theorem Rnd_N0_NG_pt : + forall F : R -> Prop, + F 0 -> + forall x f, + Rnd_N0_pt F x f <-> Rnd_NG_pt F (fun x f => Rabs f <= Rabs x) x f. +Proof. +intros F HF x f. +destruct (Rle_or_lt 0 x) as [Hx|Hx]. +(* *) +split ; intros (H1, H2). +(* . *) +assert (Hf := Rnd_N_pt_ge_0 F HF x f Hx H1). +split. +exact H1. +destruct (Rnd_N_pt_DN_or_UP _ _ _ H1) as [H3|H3]. +(* . . *) +left. +rewrite Rabs_pos_eq with (1 := Hf). +rewrite Rabs_pos_eq with (1 := Hx). +apply H3. +(* . . *) +right. +intros f2 Hxf2. +specialize (H2 _ Hxf2). +destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H4|H4]. +apply Rle_antisym. +apply Rle_trans with x. +apply H4. +apply H3. +rewrite Rabs_pos_eq with (1 := Hf) in H2. +rewrite Rabs_pos_eq in H2. +exact H2. +now apply Rnd_N_pt_ge_0 with F x. +eapply Rnd_UP_pt_unique ; eassumption. +(* . *) +split. +exact H1. +intros f2 Hxf2. +destruct H2 as [H2|H2]. +assert (Hf := Rnd_N_pt_ge_0 F HF x f Hx H1). +assert (Hf2 := Rnd_N_pt_ge_0 F HF x f2 Hx Hxf2). +rewrite 2!Rabs_pos_eq ; trivial. +rewrite 2!Rabs_pos_eq in H2 ; trivial. +destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H3|H3]. +apply H3. +apply H1. +apply H2. +apply Rle_trans with (1 := H2). +apply H3. +rewrite (H2 _ Hxf2). +apply Rle_refl. +(* *) +assert (Hx' := Rlt_le _ _ Hx). +clear Hx. rename Hx' into Hx. +split ; intros (H1, H2). +(* . *) +assert (Hf := Rnd_N_pt_le_0 F HF x f Hx H1). +split. +exact H1. +destruct (Rnd_N_pt_DN_or_UP _ _ _ H1) as [H3|H3]. +(* . . *) +right. +intros f2 Hxf2. +specialize (H2 _ Hxf2). +destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H4|H4]. +eapply Rnd_DN_pt_unique ; eassumption. +apply Rle_antisym. +2: apply Rle_trans with x. +2: apply H3. +2: apply H4. +rewrite Rabs_left1 with (1 := Hf) in H2. +rewrite Rabs_left1 in H2. +now apply Ropp_le_cancel. +now apply Rnd_N_pt_le_0 with F x. +(* . . *) +left. +rewrite Rabs_left1 with (1 := Hf). +rewrite Rabs_left1 with (1 := Hx). +apply Ropp_le_contravar. +apply H3. +(* . *) +split. +exact H1. +intros f2 Hxf2. +destruct H2 as [H2|H2]. +assert (Hf := Rnd_N_pt_le_0 F HF x f Hx H1). +assert (Hf2 := Rnd_N_pt_le_0 F HF x f2 Hx Hxf2). +rewrite 2!Rabs_left1 ; trivial. +rewrite 2!Rabs_left1 in H2 ; trivial. +apply Ropp_le_contravar. +apply Ropp_le_cancel in H2. +destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H3|H3]. +2: apply H3. +2: apply H1. +2: apply H2. +apply Rle_trans with (2 := H2). +apply H3. +rewrite (H2 _ Hxf2). +apply Rle_refl. +Qed. + +Lemma Rnd_N0_pt_unique_prop : + forall F : R -> Prop, + F 0 -> + Rnd_NG_pt_unique_prop F (fun x f => Rabs f <= Rabs x). +Proof. +intros F HF x d u Hxd1 Hxd2 Hxu1 Hxu2 Hd Hu. +apply Rle_antisym. +apply Rle_trans with x. +apply Hxd1. +apply Hxu1. +destruct (Rle_or_lt 0 x) as [Hx|Hx]. +apply Hxd1. +apply Hxu1. +rewrite Rabs_pos_eq with (1 := Hx) in Hu. +rewrite Rabs_pos_eq in Hu. +exact Hu. +apply Rle_trans with (1:=Hx). +apply Hxu1. +(* *) +apply Hxu1. +apply Hxd1. +rewrite Rabs_left with (1 := Hx) in Hd. +rewrite Rabs_left1 in Hd. +now apply Ropp_le_cancel. +apply Rlt_le, Rle_lt_trans with (2:=Hx). +apply Hxd1. +Qed. + +Theorem Rnd_N0_pt_unique : + forall F : R -> Prop, + F 0 -> + forall x f1 f2 : R, + Rnd_N0_pt F x f1 -> Rnd_N0_pt F x f2 -> + f1 = f2. +Proof. +intros F HF x f1 f2 H1 H2. +apply (Rnd_NG_pt_unique F _ (Rnd_N0_pt_unique_prop F HF) x). +now apply -> Rnd_N0_NG_pt. +now apply -> Rnd_N0_NG_pt. +Qed. + +Theorem Rnd_N0_pt_N : + forall F : R -> Prop, + F 0 -> + forall x f : R, + Rnd_N_pt F x f -> + (Rabs f <= Rabs x)%R -> + Rnd_N0_pt F x f. +Proof. +intros F HF x f Rxf Hxf. +split. +apply Rxf. +intros g Rxg. +destruct (Rabs_eq_Rabs (f - x) (g - x)) as [H|H]. +apply Rle_antisym. +apply Rxf. +apply Rxg. +apply Rxg. +apply Rxf. +(* *) +replace g with f. +apply Rle_refl. +apply Rplus_eq_reg_r with (1 := H). +(* *) +assert (g = 2 * x - f)%R. +replace (2 * x - f)%R with (x - (f - x))%R by ring. +rewrite H. +ring. +destruct (Rle_lt_dec 0 x) as [Hx|Hx]. +(* . *) +revert Hxf. +rewrite Rabs_pos_eq with (1 := Hx). +rewrite 2!Rabs_pos_eq ; try ( apply (Rnd_N_pt_ge_0 F HF x) ; assumption ). +intros Hxf. +rewrite H0. +apply Rplus_le_reg_r with f. +ring_simplify. +apply Rmult_le_compat_l with (2 := Hxf). +now apply IZR_le. +(* . *) +revert Hxf. +apply Rlt_le in Hx. +rewrite Rabs_left1 with (1 := Hx). +rewrite 2!Rabs_left1 ; try ( apply (Rnd_N_pt_le_0 F HF x) ; assumption ). +intros Hxf. +rewrite H0. +apply Ropp_le_contravar. +apply Rplus_le_reg_r with f. +ring_simplify. +apply Rmult_le_compat_l. +now apply IZR_le. +now apply Ropp_le_cancel. +Qed. + +Theorem Rnd_N0_unique : + forall (F : R -> Prop), + F 0 -> + forall rnd1 rnd2 : R -> R, + Rnd_N0 F rnd1 -> Rnd_N0 F rnd2 -> + forall x, rnd1 x = rnd2 x. +Proof. +intros F HF rnd1 rnd2 H1 H2 x. +now apply Rnd_N0_pt_unique with F x. +Qed. + +Theorem Rnd_N0_pt_monotone : + forall F : R -> Prop, + F 0 -> + round_pred_monotone (Rnd_N0_pt F). +Proof. +intros F HF x y f g Hxf Hyg Hxy. +apply (Rnd_NG_pt_monotone F _ (Rnd_N0_pt_unique_prop F HF) x y). +now apply -> Rnd_N0_NG_pt. +now apply -> Rnd_N0_NG_pt. +exact Hxy. +Qed. + +Theorem Rnd_N0_pt_refl : + forall F : R -> Prop, + forall x : R, F x -> + Rnd_N0_pt F x x. +Proof. +intros F x Hx. +split. +now apply Rnd_N_pt_refl. +intros f Hxf. +apply Req_le. +apply f_equal. +now apply sym_eq, Rnd_N_pt_idempotent with (1 := Hxf). +Qed. + +Theorem Rnd_N0_pt_idempotent : + forall F : R -> Prop, + forall x f : R, + Rnd_N0_pt F x f -> F x -> + f = x. +Proof. +intros F x f (Hf,_) Hx. +now apply Rnd_N_pt_idempotent with F. +Qed. + + + + Theorem round_pred_ge_0 : forall P : R -> R -> Prop, round_pred_monotone P -> @@ -1405,4 +1653,38 @@ apply Rnd_NA_pt_monotone. apply Hany. Qed. +Theorem satisfies_any_imp_N0 : + forall F : R -> Prop, + F 0 -> satisfies_any F -> + round_pred (Rnd_N0_pt F). +Proof. +intros F HF0 Hany. +split. +assert (H : round_pred_total (Rnd_NG_pt F (fun a b => (Rabs b <= Rabs a)%R))). +apply satisfies_any_imp_NG. +apply Hany. +intros x d u Hf Hd Hu. +destruct (Rle_lt_dec 0 x) as [Hx|Hx]. +right. +rewrite Rabs_pos_eq with (1 := Hx). +rewrite Rabs_pos_eq. +apply Hd. +apply Hd; try easy. +left. +rewrite Rabs_left with (1 := Hx). +rewrite Rabs_left1. +apply Ropp_le_contravar. +apply Hu. +apply Hu; try easy. +now apply Rlt_le. +intros x. +destruct (H x) as (f, Hf). +exists f. +apply <- Rnd_N0_NG_pt. +apply Hf. +apply HF0. +apply Rnd_N0_pt_monotone. +apply HF0. +Qed. + End RND_prop. diff --git a/flocq/Core/Ulp.v b/flocq/Core/Ulp.v index 4f4a5674..c42b3e65 100644 --- a/flocq/Core/Ulp.v +++ b/flocq/Core/Ulp.v @@ -57,7 +57,7 @@ Proof. unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn]. now apply negligible_Some. apply negligible_None. -intros n; specialize (Hn n); omega. +intros n; specialize (Hn n); lia. Qed. Lemma negligible_exp_spec': (negligible_exp = None /\ forall n, (fexp n < n)%Z) @@ -66,7 +66,7 @@ Proof. unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn]. right; simpl; exists n; now split. left; split; trivial. -intros n; specialize (Hn n); omega. +intros n; specialize (Hn n); lia. Qed. Context { valid_exp : Valid_exp fexp }. @@ -75,8 +75,8 @@ Lemma fexp_negligible_exp_eq: forall n m, (n <= fexp n)%Z -> (m <= fexp m)%Z -> Proof. intros n m Hn Hm. case (Zle_or_lt n m); intros H. -apply valid_exp; omega. -apply sym_eq, valid_exp; omega. +apply valid_exp; lia. +apply sym_eq, valid_exp; lia. Qed. @@ -198,6 +198,17 @@ rewrite V. apply generic_format_0. Qed. +Theorem ulp_canonical : + forall m e, + m <> 0%Z -> + canonical beta fexp (Float beta m e) -> + ulp (F2R (Float beta m e)) = bpow e. +Proof. +intros m e Hm Hc. +rewrite ulp_neq_0 by now apply F2R_neq_0. +apply f_equal. +now apply sym_eq. +Qed. Theorem ulp_bpow : forall e, ulp (bpow e) = bpow (fexp (e + 1)). @@ -216,7 +227,6 @@ apply bpow_ge_0. apply Rgt_not_eq, Rlt_gt, bpow_gt_0. Qed. - Lemma generic_format_ulp_0 : F (ulp 0). Proof. @@ -238,17 +248,17 @@ rewrite Req_bool_true; trivial. case negligible_exp_spec. intros H1 _. apply generic_format_bpow. -specialize (H1 (e+1)%Z); omega. +specialize (H1 (e+1)%Z); lia. intros n H1 H2. apply generic_format_bpow. case (Zle_or_lt (e+1) (fexp (e+1))); intros H4. absurd (e+1 <= e)%Z. -omega. +lia. apply Z.le_trans with (1:=H4). replace (fexp (e+1)) with (fexp n). now apply le_bpow with beta. now apply fexp_negligible_exp_eq. -omega. +lia. Qed. (** The three following properties are equivalent: @@ -300,10 +310,10 @@ case (Zle_or_lt l (fexp l)); intros Hl. rewrite (fexp_negligible_exp_eq n l); trivial; apply Z.le_refl. case (Zle_or_lt (fexp n) (fexp l)); trivial; intros K. absurd (fexp n <= fexp l)%Z. -omega. +lia. apply Z.le_trans with (2:= H _). apply Zeq_le, sym_eq, valid_exp; trivial. -omega. +lia. Qed. Lemma not_FTZ_ulp_ge_ulp_0: @@ -374,8 +384,6 @@ rewrite Hn1 in H; discriminate. now apply bpow_mag_le. Qed. - - (** Definition and properties of pred and succ *) Definition pred_pos x := @@ -432,6 +440,17 @@ unfold pred. now rewrite Ropp_involutive. Qed. +Theorem pred_bpow : + forall e, pred (bpow e) = (bpow e - bpow (fexp e))%R. +Proof. +intros e. +rewrite pred_eq_pos by apply bpow_ge_0. +unfold pred_pos. +rewrite mag_bpow. +replace (e + 1 - 1)%Z with e by ring. +now rewrite Req_bool_true. +Qed. + (** pred and succ are in the format *) (* cannont be x <> ulp 0, due to the counter-example 1-bit FP format fexp: e -> e-1 *) @@ -450,7 +469,7 @@ apply gt_0_F2R with beta (cexp beta fexp x). rewrite <- Fx. apply Rle_lt_trans with (2:=Hx). apply bpow_ge_0. -omega. +lia. case (Zle_lt_or_eq _ _ H); intros Hm. (* *) pattern x at 1 ; rewrite Fx. @@ -533,7 +552,7 @@ rewrite ulp_neq_0. intro H. assert (ex-1 < cexp beta fexp x < ex)%Z. split ; apply (lt_bpow beta) ; rewrite <- H ; easy. -clear -H0. omega. +clear -H0. lia. now apply Rgt_not_eq. apply Ex'. apply Rle_lt_trans with (2 := proj2 Ex'). @@ -555,7 +574,7 @@ apply gt_0_F2R with beta (cexp beta fexp x). rewrite <- Fx. apply Rle_lt_trans with (2:=proj1 Ex'). apply bpow_ge_0. -omega. +lia. now apply Rgt_not_eq. Qed. @@ -579,7 +598,7 @@ rewrite minus_IZR, IZR_Zpower. rewrite Rmult_minus_distr_r, Rmult_1_l. rewrite <- bpow_plus. now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring. -omega. +lia. rewrite H. apply generic_format_F2R. intros _. @@ -592,7 +611,7 @@ split. apply Rplus_le_reg_l with (bpow (fexp (e-1))). ring_simplify. apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. -apply Rplus_le_compat ; apply bpow_le ; omega. +apply Rplus_le_compat ; apply bpow_le ; lia. apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. apply Rle_trans with (bpow 1*bpow (e - 2))%R. apply Rmult_le_compat_r. @@ -614,7 +633,7 @@ apply Ropp_lt_contravar. apply bpow_gt_0. apply Rle_ge; apply Rle_0_minus. apply bpow_le. -omega. +lia. replace f with 0%R. apply generic_format_0. unfold f. @@ -842,7 +861,7 @@ assert (ex - 1 < fexp ex < ex)%Z. split ; apply (lt_bpow beta) ; rewrite <- M by easy. lra. apply Hex. -omega. +lia. rewrite 2!ulp_neq_0 by lra. apply f_equal. unfold cexp ; apply f_equal. @@ -907,7 +926,7 @@ split. apply Rplus_le_reg_l with (bpow (fexp (e-1))). ring_simplify. apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. -apply Rplus_le_compat; apply bpow_le; omega. +apply Rplus_le_compat; apply bpow_le; lia. apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. apply Rle_trans with (bpow 1*bpow (e - 2))%R. apply Rmult_le_compat_r. @@ -930,7 +949,7 @@ apply bpow_gt_0. apply Rle_ge; apply Rle_0_minus. rewrite Hxe. apply bpow_le. -omega. +lia. (* *) contradict Zp. rewrite Hxe, He; ring. @@ -953,12 +972,12 @@ unfold ulp; rewrite Req_bool_true; trivial. case negligible_exp_spec. intros K. specialize (K (e-1)%Z). -contradict K; omega. +contradict K; lia. intros n Hn. rewrite H3; apply f_equal. case (Zle_or_lt n (e-1)); intros H6. -apply valid_exp; omega. -apply sym_eq, valid_exp; omega. +apply valid_exp; lia. +apply sym_eq, valid_exp; lia. Qed. (** The following one is false for x = 0 in FTZ *) @@ -1081,7 +1100,7 @@ exfalso ; lra. intros n Hn H. assert (fexp (mag beta eps) = fexp n). apply valid_exp; try assumption. -assert(mag beta eps-1 < fexp n)%Z;[idtac|omega]. +assert(mag beta eps-1 < fexp n)%Z;[idtac|lia]. apply lt_bpow with beta. apply Rle_lt_trans with (2:=proj2 H). destruct (mag beta eps) as (e,He). @@ -1105,7 +1124,6 @@ rewrite <- P, round_0; trivial. apply valid_rnd_DN. Qed. - Theorem round_UP_plus_eps_pos : forall x, (0 <= x)%R -> F x -> forall eps, (0 < eps <= ulp x)%R -> @@ -1147,7 +1165,7 @@ lra. intros n Hn H. assert (fexp (mag beta eps) = fexp n). apply valid_exp; try assumption. -assert(mag beta eps-1 < fexp n)%Z;[idtac|omega]. +assert(mag beta eps-1 < fexp n)%Z;[idtac|lia]. apply lt_bpow with beta. apply Rle_lt_trans with (2:=H). destruct (mag beta eps) as (e,He). @@ -1172,7 +1190,6 @@ apply round_generic... apply generic_format_ulp_0. Qed. - Theorem round_UP_pred_plus_eps_pos : forall x, (0 < x)%R -> F x -> forall eps, (0 < eps <= ulp (pred x) )%R -> @@ -1210,7 +1227,6 @@ apply Ropp_lt_contravar. now apply Heps. Qed. - Theorem round_DN_plus_eps: forall x, F x -> forall eps, (0 <= eps < if (Rle_bool 0 x) then (ulp x) @@ -1248,7 +1264,6 @@ now apply Ropp_0_gt_lt_contravar. now apply generic_format_opp. Qed. - Theorem round_UP_plus_eps : forall x, F x -> forall eps, (0 < eps <= if (Rle_bool 0 x) then (ulp x) @@ -1334,11 +1349,11 @@ now apply Rgt_not_eq. case (Zle_lt_or_eq _ _ H2); intros Hexy. assert (fexp ex = fexp (ey-1))%Z. apply valid_exp. -omega. +lia. rewrite <- H1. -omega. +lia. absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z. -omega. +lia. split. apply gt_0_F2R with beta (cexp beta fexp x). now rewrite <- Fx. @@ -1380,9 +1395,9 @@ apply sym_eq; apply mag_unique. rewrite H1, Rabs_right. split. apply bpow_le. -omega. +lia. apply bpow_lt. -omega. +lia. apply Rle_ge; apply bpow_ge_0. apply mag_unique. apply Hey. @@ -1527,7 +1542,7 @@ rewrite mag_bpow. replace (fexp n + 1 - 1)%Z with (fexp n) by ring. rewrite Req_bool_true; trivial. apply Rminus_diag_eq, f_equal. -apply sym_eq, valid_exp; omega. +apply sym_eq, valid_exp; lia. Qed. Theorem succ_0 : @@ -1904,7 +1919,7 @@ rewrite ulp_neq_0; trivial. apply f_equal. unfold cexp. apply valid_exp; trivial. -assert (mag beta x -1 < fexp n)%Z;[idtac|omega]. +assert (mag beta x -1 < fexp n)%Z;[idtac|lia]. apply lt_bpow with beta. destruct (mag beta x) as (e,He). simpl. @@ -2252,9 +2267,9 @@ rewrite Hn1; easy. now apply ulp_ge_ulp_0. Qed. - -Lemma ulp_succ_pos : forall x, F x -> (0 < x)%R -> - ulp (succ x) = ulp x \/ succ x = bpow (mag beta x). +Lemma ulp_succ_pos : + forall x, F x -> (0 < x)%R -> + ulp (succ x) = ulp x \/ succ x = bpow (mag beta x). Proof with auto with typeclass_instances. intros x Fx Hx. generalize (Rlt_le _ _ Hx); intros Hx'. @@ -2281,6 +2296,39 @@ apply ulp_ge_0. now apply sym_eq, mag_unique_pos. Qed. +Theorem ulp_pred_pos : + forall x, F x -> (0 < pred x)%R -> + ulp (pred x) = ulp x \/ x = bpow (mag beta x - 1). +Proof. +intros x Fx Hx. +assert (Hx': (0 < x)%R). + apply Rlt_le_trans with (1 := Hx). + apply pred_le_id. +assert (Zx : x <> 0%R). + now apply Rgt_not_eq. +rewrite (ulp_neq_0 x) by easy. +unfold cexp. +destruct (mag beta x) as [e He]. +simpl. +assert (bpow (e - 1) <= x < bpow e)%R. + rewrite <- (Rabs_pos_eq x) by now apply Rlt_le. + now apply He. +destruct (proj1 H) as [H1|H1]. +2: now right. +left. +apply pred_ge_gt with (2 := Fx) in H1. +rewrite ulp_neq_0 by now apply Rgt_not_eq. +apply (f_equal (fun e => bpow (fexp e))). +apply mag_unique_pos. +apply (conj H1). +apply Rle_lt_trans with (2 := proj2 H). +apply pred_le_id. +apply generic_format_bpow. +apply Z.lt_le_pred. +replace (_ + 1)%Z with e by ring. +rewrite <- (mag_unique_pos _ _ _ H). +now apply mag_generic_gt. +Qed. Lemma ulp_round_pos : forall { Not_FTZ_ : Exp_not_FTZ fexp}, @@ -2333,7 +2381,6 @@ replace (fexp n) with (fexp e); try assumption. now apply fexp_negligible_exp_eq. Qed. - Theorem ulp_round : forall { Not_FTZ_ : Exp_not_FTZ fexp}, forall rnd { Zrnd : Valid_rnd rnd } x, ulp (round beta fexp rnd x) = ulp x @@ -2373,6 +2420,18 @@ destruct (round_DN_or_UP beta fexp rnd x) as [Hr|Hr]; rewrite Hr. apply succ_ge_id. Qed. +Lemma pred_round_le_id : + forall rnd { Zrnd : Valid_rnd rnd } x, + (pred (round beta fexp rnd x) <= x)%R. +Proof. +intros rnd Vrnd x. +apply (Rle_trans _ (round beta fexp Raux.Zfloor x)). +2: now apply round_DN_pt. +destruct (round_DN_or_UP beta fexp rnd x) as [Hr|Hr]; rewrite Hr. +2: now apply pred_UP_le_DN. +apply pred_le_id. +Qed. + (** Properties of rounding to nearest and ulp *) Theorem round_N_le_midp: forall choice u v, @@ -2432,6 +2491,73 @@ unfold pred. right; field. Qed. +Lemma round_N_ge_ge_midp : forall choice u v, + F u -> + (u <= round beta fexp (Znearest choice) v)%R -> + ((u + pred u) / 2 <= v)%R. +Proof with auto with typeclass_instances. +intros choice u v Hu H2. +assert (K: ((u=0)%R /\ negligible_exp = None) \/ (pred u < u)%R). +case (Req_dec u 0); intros Zu. +case_eq (negligible_exp). +intros n Hn; right. +rewrite Zu, pred_0. +unfold ulp; rewrite Req_bool_true, Hn; try easy. +rewrite <- Ropp_0. +apply Ropp_lt_contravar, bpow_gt_0. +intros _; left; split; easy. +right. +apply pred_lt_id... +(* *) +case K. +intros (K1,K2). +(* . *) +rewrite K1, pred_0. +unfold ulp; rewrite Req_bool_true, K2; try easy. +replace ((0+-0)/2)%R with 0%R by field. +case (Rle_or_lt 0 v); try easy. +intros H3; contradict H2. +rewrite K1; apply Rlt_not_le. +assert (H4: (round beta fexp (Znearest choice) v <= 0)%R). +apply round_le_generic... +apply generic_format_0... +now left. +case H4; try easy. +intros H5. +absurd (v=0)%R; try auto with real. +apply eq_0_round_0_negligible_exp with (Znearest choice)... +(* . *) +intros K1. +case (Rle_or_lt ((u + pred u) / 2) v); try easy. +intros H3. +absurd (u <= round beta fexp (Znearest choice) v)%R; try easy. +apply Rlt_not_le. +apply Rle_lt_trans with (2:=K1). +apply round_N_le_midp... +apply generic_format_pred... +rewrite succ_pred... +apply Rlt_le_trans with (1:=H3). +right; f_equal; ring. +Qed. + + +Lemma round_N_le_le_midp : forall choice u v, + F u -> + (round beta fexp (Znearest choice) v <= u)%R -> + (v <= (u + succ u) / 2)%R. +Proof with auto with typeclass_instances. +intros choice u v Hu H2. +apply Ropp_le_cancel. +apply Rle_trans with (((-u)+pred (-u))/2)%R. +rewrite pred_opp; right; field. +apply round_N_ge_ge_midp with + (choice := fun t:Z => negb (choice (- (t + 1))%Z))... +apply generic_format_opp... +rewrite <- (Ropp_involutive (round _ _ _ _)). +rewrite <- round_N_opp, Ropp_involutive. +apply Ropp_le_contravar; easy. +Qed. + Lemma round_N_eq_DN: forall choice x, let d:=round beta fexp Zfloor x in @@ -2518,4 +2644,18 @@ rewrite round_generic; [now apply succ_le_plus_ulp|now simpl|]. now apply generic_format_plus_ulp, generic_format_round. Qed. + +Lemma round_N_eq_ties: forall c1 c2 x, + (x - round beta fexp Zfloor x <> round beta fexp Zceil x - x)%R -> + (round beta fexp (Znearest c1) x = round beta fexp (Znearest c2) x)%R. +Proof with auto with typeclass_instances. +intros c1 c2 x. +pose (d:=round beta fexp Zfloor x); pose (u:=round beta fexp Zceil x); fold d; fold u; intros H. +case (Rle_or_lt ((d+u)/2) x); intros L. +2:rewrite 2!round_N_eq_DN... +destruct L as [L|L]. +rewrite 2!round_N_eq_UP... +contradict H; rewrite <- L; field. +Qed. + End Fcore_ulp. diff --git a/flocq/Core/Zaux.v b/flocq/Core/Zaux.v index e21d93a4..b40b0c4f 100644 --- a/flocq/Core/Zaux.v +++ b/flocq/Core/Zaux.v @@ -17,8 +17,12 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. *) -Require Import ZArith Omega. -Require Import Zquot. +From Coq Require Import ZArith Lia Zquot. + +Require Import SpecFloatCompat. + +Notation cond_Zopp := cond_Zopp (only parsing). +Notation iter_pos := iter_pos (only parsing). Section Zmissing. @@ -262,7 +266,7 @@ apply Z.le_refl. split. easy. apply Zpower_gt_1. -clear -He ; omega. +clear -He ; lia. apply Zle_minus_le_0. now apply Zlt_le_weak. revert H1. @@ -282,7 +286,7 @@ apply Znot_gt_le. intros H. apply Zlt_not_le with (1 := He). apply Zpower_le. -clear -H ; omega. +clear -H ; lia. Qed. Theorem Zpower_gt_id : @@ -302,7 +306,7 @@ clear. apply Zlt_0_minus_lt. replace (r * (Z_of_nat n0 + 1) - (Z_of_nat n0 + 1))%Z with ((r - 1) * (Z_of_nat n0 + 1))%Z by ring. apply Zmult_lt_0_compat. -cut (2 <= r)%Z. omega. +cut (2 <= r)%Z. lia. apply Zle_bool_imp_le. apply r. apply (Zle_lt_succ 0). @@ -420,7 +424,7 @@ apply Z.opp_inj. rewrite <- Zquot_opp_l, Z.opp_0. apply Z.quot_small. generalize (Zabs_non_eq a). -omega. +lia. Qed. Theorem ZOmod_small_abs : @@ -437,7 +441,7 @@ apply Z.opp_inj. rewrite <- Zrem_opp_l. apply Z.rem_small. generalize (Zabs_non_eq a). -omega. +lia. Qed. Theorem ZOdiv_plus : @@ -702,8 +706,6 @@ End Zcompare. Section cond_Zopp. -Definition cond_Zopp (b : bool) m := if b then Z.opp m else m. - Theorem cond_Zopp_negb : forall x y, cond_Zopp (negb x) y = Z.opp (cond_Zopp x y). Proof. @@ -921,16 +923,9 @@ intros x. apply IHp. Qed. -Fixpoint iter_pos (n : positive) (x : A) {struct n} : A := - match n with - | xI n' => iter_pos n' (iter_pos n' (f x)) - | xO n' => iter_pos n' (iter_pos n' x) - | xH => f x - end. - Lemma iter_pos_nat : forall (p : positive) (x : A), - iter_pos p x = iter_nat (Pos.to_nat p) x. + iter_pos f p x = iter_nat (Pos.to_nat p) x. Proof. induction p ; intros x. rewrite Pos2Nat.inj_xI. diff --git a/flocq/IEEE754/Binary.v b/flocq/IEEE754/Binary.v index ac38c761..35d15cb3 100644 --- a/flocq/IEEE754/Binary.v +++ b/flocq/IEEE754/Binary.v @@ -627,6 +627,52 @@ Proof. now rewrite Pcompare_antisym. Qed. +Theorem bounded_le_emax_minus_prec : + forall mx ex, + bounded mx ex = true -> + (F2R (Float radix2 (Zpos mx) ex) + <= bpow radix2 emax - bpow radix2 (emax - prec))%R. +Proof. +intros mx ex Hx. +destruct (andb_prop _ _ Hx) as (H1,H2). +generalize (Zeq_bool_eq _ _ H1). clear H1. intro H1. +generalize (Zle_bool_imp_le _ _ H2). clear H2. intro H2. +generalize (mag_F2R_Zdigits radix2 (Zpos mx) ex). +destruct (mag radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex). +unfold mag_val. +intros H. +elim Ex; [|now apply Rgt_not_eq, F2R_gt_0]; intros _. +rewrite <-F2R_Zabs; simpl; clear Ex; intros Ex. +generalize (Rmult_lt_compat_r (bpow radix2 (-ex)) _ _ (bpow_gt_0 _ _) Ex). +unfold F2R; simpl; rewrite Rmult_assoc, <-!bpow_plus. +rewrite H; [|intro H'; discriminate H']. +rewrite <-Z.add_assoc, Z.add_opp_diag_r, Z.add_0_r, Rmult_1_r. +rewrite <-(IZR_Zpower _ _ (Zdigits_ge_0 _ _)); clear Ex; intro Ex. +generalize (Zlt_le_succ _ _ (lt_IZR _ _ Ex)); clear Ex; intro Ex. +generalize (IZR_le _ _ Ex). +rewrite succ_IZR; clear Ex; intro Ex. +generalize (Rplus_le_compat_r (-1) _ _ Ex); clear Ex; intro Ex. +ring_simplify in Ex; revert Ex. +rewrite (IZR_Zpower _ _ (Zdigits_ge_0 _ _)); intro Ex. +generalize (Rmult_le_compat_r (bpow radix2 ex) _ _ (bpow_ge_0 _ _) Ex). +intro H'; apply (Rle_trans _ _ _ H'). +rewrite Rmult_minus_distr_r, Rmult_1_l, <-bpow_plus. +revert H1; unfold fexp, FLT_exp; intro H1. +generalize (Z.le_max_l (Z.pos (digits2_pos mx) + ex - prec) emin). +rewrite H1; intro H1'. +generalize (proj1 (Z.le_sub_le_add_r _ _ _) H1'). +rewrite Zpos_digits2_pos; clear H1'; intro H1'. +apply (Rle_trans _ _ _ (Rplus_le_compat_r _ _ _ (bpow_le _ _ _ H1'))). +replace emax with (emax - prec - ex + (ex + prec))%Z at 1 by ring. +replace (emax - prec)%Z with (emax - prec - ex + ex)%Z at 2 by ring. +do 2 rewrite (bpow_plus _ (emax - prec - ex)). +rewrite <-Rmult_minus_distr_l. +rewrite <-(Rmult_1_l (_ + _)). +apply Rmult_le_compat_r. +{ apply Rle_0_minus, bpow_le; unfold Prec_gt_0 in prec_gt_0_; lia. } +change 1%R with (bpow radix2 0); apply bpow_le; lia. +Qed. + Theorem bounded_lt_emax : forall mx ex, bounded mx ex = true -> @@ -651,7 +697,7 @@ rewrite H. 2: discriminate. revert H1. clear -H2. rewrite Zpos_digits2_pos. unfold fexp, FLT_exp. -intros ; zify ; omega. +intros ; zify ; lia. Qed. Theorem bounded_ge_emin : @@ -679,7 +725,18 @@ unfold fexp, FLT_exp. clear -prec_gt_0_. unfold Prec_gt_0 in prec_gt_0_. clearbody emin. -intros ; zify ; omega. +intros ; zify ; lia. +Qed. + +Theorem abs_B2R_le_emax_minus_prec : + forall x, + (Rabs (B2R x) <= bpow radix2 emax - bpow radix2 (emax - prec))%R. +Proof. +intros [sx|sx|sx plx Hx|sx mx ex Hx] ; simpl ; + [rewrite Rabs_R0 ; apply Rle_0_minus, bpow_le ; + revert prec_gt_0_; unfold Prec_gt_0; lia..|]. +rewrite <- F2R_Zabs, abs_cond_Zopp. +now apply bounded_le_emax_minus_prec. Qed. Theorem abs_B2R_lt_emax : @@ -728,7 +785,7 @@ rewrite Cx. unfold cexp, fexp, FLT_exp. destruct (mag radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex). simpl. apply Z.max_lub. -cut (e' - 1 < emax)%Z. clear ; omega. +cut (e' - 1 < emax)%Z. clear ; lia. apply lt_bpow with radix2. apply Rle_lt_trans with (2 := Bx). change (Zpos mx) with (Z.abs (Zpos mx)). @@ -738,7 +795,7 @@ apply Rgt_not_eq. now apply F2R_gt_0. unfold emin. generalize (prec_gt_0 prec). -clear -Hmax ; omega. +clear -Hmax ; lia. Qed. (** Truncation *) @@ -889,7 +946,7 @@ now inversion H. (* *) intros p Hp. assert (He: (e <= fexp (Zdigits radix2 m + e))%Z). -clear -Hp ; zify ; omega. +clear -Hp ; zify ; lia. destruct (inbetween_float_ex radix2 m e l) as (x, Hx). generalize (inbetween_shr x m e l (fexp (Zdigits radix2 m + e) - e) Hm Hx). assert (Hx0 : (0 <= x)%R). @@ -1091,18 +1148,18 @@ rewrite Zpos_digits2_pos. replace (Zdigits radix2 (Zpos (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end))) with prec. unfold fexp, FLT_exp, emin. generalize (prec_gt_0 prec). -clear -Hmax ; zify ; omega. +clear -Hmax ; zify ; lia. change 2%Z with (radix_val radix2). case_eq (Zpower radix2 prec - 1)%Z. simpl Zdigits. generalize (Zpower_gt_1 radix2 prec (prec_gt_0 prec)). -clear ; omega. +clear ; lia. intros p Hp. apply Zle_antisym. -cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; omega. +cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; lia. apply Zdigits_gt_Zpower. simpl Z.abs. rewrite <- Hp. -cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; omega. +cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; lia. apply lt_IZR. rewrite 2!IZR_Zpower. 2: now apply Zlt_le_weak. apply bpow_lt. @@ -1113,7 +1170,7 @@ simpl Z.abs. rewrite <- Hp. apply Zlt_pred. intros p Hp. generalize (Zpower_gt_1 radix2 _ (prec_gt_0 prec)). -clear -Hp ; zify ; omega. +clear -Hp ; zify ; lia. apply Rnot_lt_le. intros Hx. generalize (refl_equal (bounded m2 e2)). @@ -1271,18 +1328,18 @@ rewrite Zpos_digits2_pos. replace (Zdigits radix2 (Zpos (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end))) with prec. unfold fexp, FLT_exp, emin. generalize (prec_gt_0 prec). -clear -Hmax ; zify ; omega. +clear -Hmax ; zify ; lia. change 2%Z with (radix_val radix2). case_eq (Zpower radix2 prec - 1)%Z. simpl Zdigits. generalize (Zpower_gt_1 radix2 prec (prec_gt_0 prec)). -clear ; omega. +clear ; lia. intros p Hp. apply Zle_antisym. -cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; omega. +cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; lia. apply Zdigits_gt_Zpower. simpl Z.abs. rewrite <- Hp. -cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; omega. +cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; lia. apply lt_IZR. rewrite 2!IZR_Zpower. 2: now apply Zlt_le_weak. apply bpow_lt. @@ -1293,7 +1350,7 @@ simpl Z.abs. rewrite <- Hp. apply Zlt_pred. intros p Hp. generalize (Zpower_gt_1 radix2 _ (prec_gt_0 prec)). -clear -Hp ; zify ; omega. +clear -Hp ; zify ; lia. apply Rnot_lt_le. intros Hx. generalize (refl_equal (bounded m2 e2)). @@ -1370,7 +1427,7 @@ clear -Hmax. unfold emin. intros dx dy dxy Hx Hy Hxy. zify ; intros ; subst. -omega. +lia. (* *) case sx ; case sy. apply Rlt_bool_false. @@ -1479,7 +1536,7 @@ case_eq (ex' - ex)%Z ; simpl. intros H. now rewrite Zminus_eq with (1 := H). intros p. -clear -He ; zify ; omega. +clear -He ; zify ; lia. intros. apply refl_equal. Qed. @@ -1580,7 +1637,7 @@ now rewrite is_finite_FF2B. rewrite Bsign_FF2B, Rz''. rewrite Rcompare_Gt... apply F2R_gt_0. -simpl. zify; omega. +simpl. zify; lia. intros Hz' (Vz, Rz). rewrite B2FF_FF2B, Rz. apply f_equal. @@ -1599,7 +1656,7 @@ now rewrite is_finite_FF2B. rewrite Bsign_FF2B, Rz''. rewrite Rcompare_Lt... apply F2R_lt_0. -simpl. zify; omega. +simpl. zify; lia. intros Hz' (Vz, Rz). rewrite B2FF_FF2B, Rz. apply f_equal. @@ -2150,7 +2207,7 @@ set (e' := Z.min _ _). assert (2 * e' <= ex)%Z as He. { assert (e' <= Z.div2 ex)%Z by apply Z.le_min_r. rewrite (Zdiv2_odd_eqn ex). - destruct Z.odd ; omega. } + destruct Z.odd ; lia. } generalize (Fsqrt_core_correct radix2 (Zpos mx) ex e' eq_refl He). unfold Fsqrt_core. set (mx' := match (ex - 2 * e')%Z with Z0 => _ | _ => _ end). @@ -2187,7 +2244,7 @@ apply Rlt_le_trans with (1 := Heps). fold (bpow radix2 0). apply bpow_le. generalize (prec_gt_0 prec). -clear ; omega. +clear ; lia. apply Rsqr_incrst_0. 3: apply bpow_ge_0. rewrite Rsqr_mult. @@ -2211,7 +2268,7 @@ now apply IZR_le. change 4%R with (bpow radix2 2). apply bpow_le. generalize (prec_gt_0 prec). -clear -Hmax ; omega. +clear -Hmax ; lia. apply Rmult_le_pos. apply sqrt_ge_0. rewrite <- (Rplus_opp_r 1). @@ -2230,7 +2287,7 @@ unfold Rsqr. rewrite <- bpow_plus. apply bpow_le. unfold emin. -clear -Hmax ; omega. +clear -Hmax ; lia. apply generic_format_ge_bpow with fexp. intros. apply Z.le_max_r. diff --git a/flocq/IEEE754/Bits.v b/flocq/IEEE754/Bits.v index 3a84edfe..68bc541a 100644 --- a/flocq/IEEE754/Bits.v +++ b/flocq/IEEE754/Bits.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * IEEE-754 encoding of binary floating-point data *) + +From Coq Require Import Lia. Require Import Core Digits Binary. Section Binary_Bits. @@ -43,10 +45,10 @@ Proof. intros s m e Hm He. assert (0 <= mw)%Z as Hmw. destruct mw as [|mw'|mw'] ; try easy. - clear -Hm ; simpl in Hm ; omega. + clear -Hm ; simpl in Hm ; lia. assert (0 <= ew)%Z as Hew. destruct ew as [|ew'|ew'] ; try easy. - clear -He ; simpl in He ; omega. + clear -He ; simpl in He ; lia. unfold join_bits. rewrite Z.shiftl_mul_pow2 by easy. split. @@ -54,9 +56,9 @@ split. rewrite <- (Zmult_0_l (2^mw)). apply Zmult_le_compat_r. case s. - clear -He ; omega. + clear -He ; lia. now rewrite Zmult_0_l. - clear -Hm ; omega. + clear -Hm ; lia. - apply Z.lt_le_trans with (((if s then 2 ^ ew else 0) + e + 1) * 2 ^ mw)%Z. rewrite (Zmult_plus_distr_l _ 1). apply Zplus_lt_compat_l. @@ -65,9 +67,9 @@ split. apply Zmult_le_compat_r. rewrite Zpower_plus by easy. change (2^1)%Z with 2%Z. - case s ; clear -He ; omega. - clear -Hm ; omega. - clear -Hew ; omega. + case s ; clear -He ; lia. + clear -Hm ; lia. + clear -Hew ; lia. easy. Qed. @@ -85,10 +87,10 @@ Proof. intros s m e Hm He. assert (0 <= mw)%Z as Hmw. destruct mw as [|mw'|mw'] ; try easy. - clear -Hm ; simpl in Hm ; omega. + clear -Hm ; simpl in Hm ; lia. assert (0 <= ew)%Z as Hew. destruct ew as [|ew'|ew'] ; try easy. - clear -He ; simpl in He ; omega. + clear -He ; simpl in He ; lia. unfold split_bits, join_bits. rewrite Z.shiftl_mul_pow2 by easy. apply f_equal2 ; [apply f_equal2|]. @@ -99,7 +101,7 @@ apply f_equal2 ; [apply f_equal2|]. apply Zplus_le_0_compat. apply Zmult_le_0_compat. apply He. - clear -Hm ; omega. + clear -Hm ; lia. apply Hm. + apply Zle_bool_false. apply Zplus_lt_reg_l with (2^mw * (-e))%Z. @@ -108,12 +110,12 @@ apply f_equal2 ; [apply f_equal2|]. apply Z.lt_le_trans with (2^mw * 1)%Z. now apply Zmult_lt_compat_r. apply Zmult_le_compat_l. - clear -He ; omega. - clear -Hm ; omega. + clear -He ; lia. + clear -Hm ; lia. - rewrite Zplus_comm. rewrite Z_mod_plus_full. now apply Zmod_small. -- rewrite Z_div_plus_full_l by (clear -Hm ; omega). +- rewrite Z_div_plus_full_l by (clear -Hm ; lia). rewrite Zdiv_small with (1 := Hm). rewrite Zplus_0_r. case s. @@ -175,7 +177,7 @@ rewrite Zdiv_Zdiv. apply sym_eq. case Zle_bool_spec ; intros Hs. apply Zle_antisym. -cut (x / (2^mw * 2^ew) < 2)%Z. clear ; omega. +cut (x / (2^mw * 2^ew) < 2)%Z. clear ; lia. apply Zdiv_lt_upper_bound. now apply Zmult_lt_0_compat. rewrite <- Zpower_exp ; try ( apply Z.le_ge ; apply Zlt_le_weak ; assumption ). @@ -244,8 +246,8 @@ Theorem split_bits_of_binary_float_correct : split_bits (bits_of_binary_float x) = split_bits_of_binary_float x. Proof. intros [sx|sx|sx plx Hplx|sx mx ex Hx] ; - try ( simpl ; apply split_join_bits ; split ; try apply Z.le_refl ; try apply Zlt_pred ; trivial ; omega ). -simpl. apply split_join_bits; split; try (zify; omega). + try ( simpl ; apply split_join_bits ; split ; try apply Z.le_refl ; try apply Zlt_pred ; trivial ; lia ). +simpl. apply split_join_bits; split; try (zify; lia). destruct (digits2_Pnat_correct plx). unfold nan_pl in Hplx. rewrite Zpos_digits2_pos, <- Z_of_nat_S_digits2_Pnat in Hplx. @@ -253,7 +255,7 @@ rewrite Zpower_nat_Z in H0. eapply Z.lt_le_trans. apply H0. change 2%Z with (radix_val radix2). apply Zpower_le. rewrite Z.ltb_lt in Hplx. -unfold prec in *. zify; omega. +unfold prec in *. zify; lia. (* *) unfold bits_of_binary_float, split_bits_of_binary_float. assert (Hf: (emin <= ex /\ Zdigits radix2 (Zpos mx) <= prec)%Z). @@ -263,14 +265,14 @@ rewrite Zpos_digits2_pos in Hx'. generalize (Zeq_bool_eq _ _ Hx'). unfold FLT_exp. unfold emin. -clear ; zify ; omega. +clear ; zify ; lia. case Zle_bool_spec ; intros H ; [ apply -> Z.le_0_sub in H | apply -> Z.lt_sub_0 in H ] ; apply split_join_bits ; try now split. (* *) split. -clear -He_gt_0 H ; omega. -cut (Zpos mx < 2 * 2^mw)%Z. clear ; omega. +clear -He_gt_0 H ; lia. +cut (Zpos mx < 2 * 2^mw)%Z. clear ; lia. replace (2 * 2^mw)%Z with (2^prec)%Z. apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)). apply Hf. @@ -282,12 +284,12 @@ now apply Zlt_le_weak. (* *) split. generalize (proj1 Hf). -clear ; omega. +clear ; lia. destruct (andb_prop _ _ Hx) as (_, Hx'). unfold emin. replace (2^ew)%Z with (2 * emax)%Z. generalize (Zle_bool_imp_le _ _ Hx'). -clear ; omega. +clear ; lia. apply sym_eq. rewrite (Zsucc_pred ew). unfold Z.succ. @@ -305,7 +307,7 @@ intros [sx|sx|sx pl pl_range|sx mx ex H]. - apply join_bits_range ; now split. - apply join_bits_range. now split. - clear -He_gt_0 ; omega. + clear -He_gt_0 ; lia. - apply Z.ltb_lt in pl_range. apply join_bits_range. split. @@ -313,7 +315,7 @@ intros [sx|sx|sx pl pl_range|sx mx ex H]. apply (Zpower_gt_Zdigits radix2 _ (Zpos pl)). apply Z.lt_succ_r. now rewrite <- Zdigits2_Zdigits. - clear -He_gt_0 ; omega. + clear -He_gt_0 ; lia. - unfold bounded in H. apply Bool.andb_true_iff in H ; destruct H as [A B]. apply Z.leb_le in B. @@ -321,22 +323,22 @@ intros [sx|sx|sx pl pl_range|sx mx ex H]. case Zle_bool_spec ; intros H. + apply join_bits_range. * split. - clear -H ; omega. + clear -H ; lia. rewrite Zpos_digits2_pos in A. cut (Zpos mx < 2 ^ prec)%Z. unfold prec. - rewrite Zpower_plus by (clear -Hmw ; omega). + rewrite Zpower_plus by (clear -Hmw ; lia). change (2^1)%Z with 2%Z. - clear ; omega. + clear ; lia. apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)). - clear -A ; zify ; omega. + clear -A ; zify ; lia. * split. - unfold emin ; clear -A ; zify ; omega. + unfold emin ; clear -A ; zify ; lia. replace ew with ((ew - 1) + 1)%Z by ring. - rewrite Zpower_plus by (clear - Hew ; omega). + rewrite Zpower_plus by (clear - Hew ; lia). unfold emin, emax in *. change (2^1)%Z with 2%Z. - clear -B ; omega. + clear -B ; lia. + apply -> Z.lt_sub_0 in H. apply join_bits_range ; now split. Qed. @@ -370,7 +372,7 @@ unfold binary_float_of_bits_aux, split_bits. assert (Hnan: nan_pl prec 1 = true). apply Z.ltb_lt. simpl. unfold prec. - clear -Hmw ; omega. + clear -Hmw ; lia. case Zeq_bool_spec ; intros He1. case_eq (x mod 2^mw)%Z ; try easy. (* subnormal *) @@ -389,7 +391,7 @@ unfold Fexp, FLT_exp. apply sym_eq. apply Zmax_right. clear -H Hprec. -unfold prec ; omega. +unfold prec ; lia. apply Rnot_le_lt. intros H0. refine (_ (mag_le radix2 _ _ _ H0)). @@ -397,20 +399,20 @@ rewrite mag_bpow. rewrite mag_F2R_Zdigits. 2: discriminate. unfold emin, prec. apply Zlt_not_le. -cut (0 < emax)%Z. clear -H Hew ; omega. +cut (0 < emax)%Z. clear -H Hew ; lia. apply (Zpower_gt_0 radix2). -clear -Hew ; omega. +clear -Hew ; lia. apply bpow_gt_0. case Zeq_bool_spec ; intros He2. case_eq (x mod 2 ^ mw)%Z; try easy. (* nan *) intros plx Eqplx. apply Z.ltb_lt. rewrite Zpos_digits2_pos. -assert (forall a b, a <= b -> a < b+1)%Z by (intros; omega). apply H. clear H. +assert (forall a b, a <= b -> a < b+1)%Z by (intros; lia). apply H. clear H. apply Zdigits_le_Zpower. simpl. rewrite <- Eqplx. edestruct Z_mod_lt; eauto. change 2%Z with (radix_val radix2). -apply Z.lt_gt, Zpower_gt_0. omega. +apply Z.lt_gt, Zpower_gt_0. lia. case_eq (x mod 2^mw + 2^mw)%Z ; try easy. (* normal *) intros px Hm. @@ -452,7 +454,7 @@ revert He1. fold ex. cut (0 <= ex)%Z. unfold emin. -clear ; intros H1 H2 ; omega. +clear ; intros H1 H2 ; lia. eapply Z_mod_lt. apply Z.lt_gt. apply (Zpower_gt_0 radix2). @@ -471,12 +473,12 @@ revert He2. set (ex := ((x / 2^mw) mod 2^ew)%Z). cut (ex < 2^ew)%Z. replace (2^ew)%Z with (2 * emax)%Z. -clear ; intros H1 H2 ; omega. +clear ; intros H1 H2 ; lia. replace ew with (1 + (ew - 1))%Z by ring. rewrite Zpower_exp. apply refl_equal. discriminate. -clear -Hew ; omega. +clear -Hew ; lia. eapply Z_mod_lt. apply Z.lt_gt. apply (Zpower_gt_0 radix2). @@ -503,13 +505,13 @@ apply refl_equal. simpl. rewrite Zeq_bool_false. now rewrite Zeq_bool_true. -cut (1 < 2^ew)%Z. clear ; omega. +cut (1 < 2^ew)%Z. clear ; lia. now apply (Zpower_gt_1 radix2). (* *) simpl. rewrite Zeq_bool_false. rewrite Zeq_bool_true; auto. -cut (1 < 2^ew)%Z. clear ; omega. +cut (1 < 2^ew)%Z. clear ; lia. now apply (Zpower_gt_1 radix2). (* *) unfold split_bits_of_binary_float. @@ -522,19 +524,19 @@ destruct (andb_prop _ _ Bx) as (_, H1). generalize (Zle_bool_imp_le _ _ H1). unfold emin. replace (2^ew)%Z with (2 * emax)%Z. -clear ; omega. +clear ; lia. replace ew with (1 + (ew - 1))%Z by ring. rewrite Zpower_exp. apply refl_equal. discriminate. -clear -Hew ; omega. +clear -Hew ; lia. destruct (andb_prop _ _ Bx) as (H1, _). generalize (Zeq_bool_eq _ _ H1). rewrite Zpos_digits2_pos. unfold FLT_exp, emin. generalize (Zdigits radix2 (Zpos mx)). clear. -intros ; zify ; omega. +intros ; zify ; lia. (* . *) rewrite Zeq_bool_true. 2: apply refl_equal. simpl. @@ -547,7 +549,7 @@ apply -> Z.lt_sub_0 in Hm. generalize (Zdigits_le_Zpower radix2 _ (Zpos mx) Hm). generalize (Zdigits radix2 (Zpos mx)). clear. -intros ; zify ; omega. +intros ; zify ; lia. Qed. Theorem bits_of_binary_float_of_bits : @@ -588,12 +590,12 @@ case Zeq_bool_spec ; intros He2. case_eq mx; intros Hm. now rewrite He2. now rewrite He2. -intros. zify; omega. +intros. zify; lia. (* normal *) case_eq (mx + 2 ^ mw)%Z. intros Hm. apply False_ind. -clear -Bm Hm ; omega. +clear -Bm Hm ; lia. intros p Hm Jx Cx. rewrite <- Hm. rewrite Zle_bool_true. @@ -601,7 +603,7 @@ now ring_simplify (mx + 2^mw - 2^mw)%Z (ex + emin - 1 - emin + 1)%Z. now ring_simplify. intros p Hm. apply False_ind. -clear -Bm Hm ; zify ; omega. +clear -Bm Hm ; zify ; lia. Qed. End Binary_Bits. @@ -623,6 +625,12 @@ Proof. apply refl_equal. Qed. +Let Hemax : (3 <= 128)%Z. +Proof. +intros H. +discriminate H. +Qed. + Definition default_nan_pl32 : { nan : binary32 | is_nan 24 128 nan = true } := exist _ (@B754_nan 24 128 false (iter_nat xO 22 xH) (refl_equal true)) (refl_equal true). @@ -639,16 +647,28 @@ Definition binop_nan_pl32 (f1 f2 : binary32) : { nan : binary32 | is_nan 24 128 | _, _ => default_nan_pl32 end. +Definition ternop_nan_pl32 (f1 f2 f3 : binary32) : { nan : binary32 | is_nan 24 128 nan = true } := + match f1, f2, f3 with + | B754_nan s1 pl1 Hpl1, _, _ => exist _ (B754_nan s1 pl1 Hpl1) (refl_equal true) + | _, B754_nan s2 pl2 Hpl2, _ => exist _ (B754_nan s2 pl2 Hpl2) (refl_equal true) + | _, _, B754_nan s3 pl3 Hpl3 => exist _ (B754_nan s3 pl3 Hpl3) (refl_equal true) + | _, _, _ => default_nan_pl32 + end. + Definition b32_erase : binary32 -> binary32 := erase 24 128. Definition b32_opp : binary32 -> binary32 := Bopp 24 128 unop_nan_pl32. Definition b32_abs : binary32 -> binary32 := Babs 24 128 unop_nan_pl32. -Definition b32_sqrt : mode -> binary32 -> binary32 := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl32. +Definition b32_pred : binary32 -> binary32 := Bpred _ _ Hprec Hprec_emax Hemax unop_nan_pl32. +Definition b32_succ : binary32 -> binary32 := Bsucc _ _ Hprec Hprec_emax Hemax unop_nan_pl32. +Definition b32_sqrt : mode -> binary32 -> binary32 := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl32. Definition b32_plus : mode -> binary32 -> binary32 -> binary32 := Bplus _ _ Hprec Hprec_emax binop_nan_pl32. Definition b32_minus : mode -> binary32 -> binary32 -> binary32 := Bminus _ _ Hprec Hprec_emax binop_nan_pl32. Definition b32_mult : mode -> binary32 -> binary32 -> binary32 := Bmult _ _ Hprec Hprec_emax binop_nan_pl32. Definition b32_div : mode -> binary32 -> binary32 -> binary32 := Bdiv _ _ Hprec Hprec_emax binop_nan_pl32. +Definition b32_fma : mode -> binary32 -> binary32 -> binary32 -> binary32 := Bfma _ _ Hprec Hprec_emax ternop_nan_pl32. + Definition b32_compare : binary32 -> binary32 -> option comparison := Bcompare 24 128. Definition b32_of_bits : Z -> binary32 := binary_float_of_bits 23 8 (refl_equal _) (refl_equal _) (refl_equal _). Definition bits_of_b32 : binary32 -> Z := bits_of_binary_float 23 8. @@ -672,6 +692,12 @@ Proof. apply refl_equal. Qed. +Let Hemax : (3 <= 1024)%Z. +Proof. +intros H. +discriminate H. +Qed. + Definition default_nan_pl64 : { nan : binary64 | is_nan 53 1024 nan = true } := exist _ (@B754_nan 53 1024 false (iter_nat xO 51 xH) (refl_equal true)) (refl_equal true). @@ -688,9 +714,19 @@ Definition binop_nan_pl64 (f1 f2 : binary64) : { nan : binary64 | is_nan 53 1024 | _, _ => default_nan_pl64 end. +Definition ternop_nan_pl64 (f1 f2 f3 : binary64) : { nan : binary64 | is_nan 53 1024 nan = true } := + match f1, f2, f3 with + | B754_nan s1 pl1 Hpl1, _, _ => exist _ (B754_nan s1 pl1 Hpl1) (refl_equal true) + | _, B754_nan s2 pl2 Hpl2, _ => exist _ (B754_nan s2 pl2 Hpl2) (refl_equal true) + | _, _, B754_nan s3 pl3 Hpl3 => exist _ (B754_nan s3 pl3 Hpl3) (refl_equal true) + | _, _, _ => default_nan_pl64 + end. + Definition b64_erase : binary64 -> binary64 := erase 53 1024. Definition b64_opp : binary64 -> binary64 := Bopp 53 1024 unop_nan_pl64. Definition b64_abs : binary64 -> binary64 := Babs 53 1024 unop_nan_pl64. +Definition b64_pred : binary64 -> binary64 := Bpred _ _ Hprec Hprec_emax Hemax unop_nan_pl64. +Definition b64_succ : binary64 -> binary64 := Bsucc _ _ Hprec Hprec_emax Hemax unop_nan_pl64. Definition b64_sqrt : mode -> binary64 -> binary64 := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl64. Definition b64_plus : mode -> binary64 -> binary64 -> binary64 := Bplus _ _ Hprec Hprec_emax binop_nan_pl64. @@ -698,6 +734,8 @@ Definition b64_minus : mode -> binary64 -> binary64 -> binary64 := Bminus _ _ Hp Definition b64_mult : mode -> binary64 -> binary64 -> binary64 := Bmult _ _ Hprec Hprec_emax binop_nan_pl64. Definition b64_div : mode -> binary64 -> binary64 -> binary64 := Bdiv _ _ Hprec Hprec_emax binop_nan_pl64. +Definition b64_fma : mode -> binary64 -> binary64 -> binary64 -> binary64 := Bfma _ _ Hprec Hprec_emax ternop_nan_pl64. + Definition b64_compare : binary64 -> binary64 -> option comparison := Bcompare 53 1024. Definition b64_of_bits : Z -> binary64 := binary_float_of_bits 52 11 (refl_equal _) (refl_equal _) (refl_equal _). Definition bits_of_b64 : binary64 -> Z := bits_of_binary_float 52 11. diff --git a/flocq/IEEE754/SpecFloatCompat.v b/flocq/IEEE754/SpecFloatCompat.v new file mode 100644 index 00000000..e2ace4d5 --- /dev/null +++ b/flocq/IEEE754/SpecFloatCompat.v @@ -0,0 +1,435 @@ +(** +This file is part of the Flocq formalization of floating-point +arithmetic in Coq: http://flocq.gforge.inria.fr/ + +Copyright (C) 2018-2019 Guillaume Bertholon +#
# +Copyright (C) 2018-2019 Érik Martin-Dorel +#
# +Copyright (C) 2018-2019 Pierre Roux + +This library is free software; you can redistribute it and/or +modify it under the terms of the GNU Lesser General Public +License as published by the Free Software Foundation; either +version 3 of the License, or (at your option) any later version. + +This library is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +COPYING file for more details. +*) + +Require Import ZArith. + +(** ** Inductive specification of floating-point numbers + +Similar to [IEEE754.Binary.full_float], but with no NaN payload. *) +Variant spec_float := + | S754_zero (s : bool) + | S754_infinity (s : bool) + | S754_nan + | S754_finite (s : bool) (m : positive) (e : Z). + +(** ** Parameterized definitions + +[prec] is the number of bits of the mantissa including the implicit one; +[emax] is the exponent of the infinities. + +For instance, Binary64 is defined by [prec = 53] and [emax = 1024]. *) +Section FloatOps. + Variable prec emax : Z. + + Definition emin := (3-emax-prec)%Z. + Definition fexp e := Z.max (e - prec) emin. + + Section Zdigits2. + Fixpoint digits2_pos (n : positive) : positive := + match n with + | xH => xH + | xO p => Pos.succ (digits2_pos p) + | xI p => Pos.succ (digits2_pos p) + end. + + Definition Zdigits2 n := + match n with + | Z0 => n + | Zpos p => Zpos (digits2_pos p) + | Zneg p => Zpos (digits2_pos p) + end. + End Zdigits2. + + Section ValidBinary. + Definition canonical_mantissa m e := + Zeq_bool (fexp (Zpos (digits2_pos m) + e)) e. + + Definition bounded m e := + andb (canonical_mantissa m e) (Zle_bool e (emax - prec)). + + Definition valid_binary x := + match x with + | S754_finite _ m e => bounded m e + | _ => true + end. + End ValidBinary. + + Section Iter. + Context {A : Type}. + Variable (f : A -> A). + + Fixpoint iter_pos (n : positive) (x : A) {struct n} : A := + match n with + | xI n' => iter_pos n' (iter_pos n' (f x)) + | xO n' => iter_pos n' (iter_pos n' x) + | xH => f x + end. + End Iter. + + Section Rounding. + Inductive location := loc_Exact | loc_Inexact : comparison -> location. + + Record shr_record := { shr_m : Z ; shr_r : bool ; shr_s : bool }. + + Definition shr_1 mrs := + let '(Build_shr_record m r s) := mrs in + let s := orb r s in + match m with + | Z0 => Build_shr_record Z0 false s + | Zpos xH => Build_shr_record Z0 true s + | Zpos (xO p) => Build_shr_record (Zpos p) false s + | Zpos (xI p) => Build_shr_record (Zpos p) true s + | Zneg xH => Build_shr_record Z0 true s + | Zneg (xO p) => Build_shr_record (Zneg p) false s + | Zneg (xI p) => Build_shr_record (Zneg p) true s + end. + + Definition loc_of_shr_record mrs := + match mrs with + | Build_shr_record _ false false => loc_Exact + | Build_shr_record _ false true => loc_Inexact Lt + | Build_shr_record _ true false => loc_Inexact Eq + | Build_shr_record _ true true => loc_Inexact Gt + end. + + Definition shr_record_of_loc m l := + match l with + | loc_Exact => Build_shr_record m false false + | loc_Inexact Lt => Build_shr_record m false true + | loc_Inexact Eq => Build_shr_record m true false + | loc_Inexact Gt => Build_shr_record m true true + end. + + Definition shr mrs e n := + match n with + | Zpos p => (iter_pos shr_1 p mrs, (e + n)%Z) + | _ => (mrs, e) + end. + + Definition shr_fexp m e l := + shr (shr_record_of_loc m l) e (fexp (Zdigits2 m + e) - e). + + Definition round_nearest_even mx lx := + match lx with + | loc_Exact => mx + | loc_Inexact Lt => mx + | loc_Inexact Eq => if Z.even mx then mx else (mx + 1)%Z + | loc_Inexact Gt => (mx + 1)%Z + end. + + Definition binary_round_aux sx mx ex lx := + let '(mrs', e') := shr_fexp mx ex lx in + let '(mrs'', e'') := shr_fexp (round_nearest_even (shr_m mrs') (loc_of_shr_record mrs')) e' loc_Exact in + match shr_m mrs'' with + | Z0 => S754_zero sx + | Zpos m => if Zle_bool e'' (emax - prec) then S754_finite sx m e'' else S754_infinity sx + | _ => S754_nan + end. + + Definition shl_align mx ex ex' := + match (ex' - ex)%Z with + | Zneg d => (shift_pos d mx, ex') + | _ => (mx, ex) + end. + + Definition binary_round sx mx ex := + let '(mz, ez) := shl_align mx ex (fexp (Zpos (digits2_pos mx) + ex))in + binary_round_aux sx (Zpos mz) ez loc_Exact. + + Definition binary_normalize m e szero := + match m with + | Z0 => S754_zero szero + | Zpos m => binary_round false m e + | Zneg m => binary_round true m e + end. + End Rounding. + + (** ** Define operations *) + + Definition SFopp x := + match x with + | S754_nan => S754_nan + | S754_infinity sx => S754_infinity (negb sx) + | S754_finite sx mx ex => S754_finite (negb sx) mx ex + | S754_zero sx => S754_zero (negb sx) + end. + + Definition SFabs x := + match x with + | S754_nan => S754_nan + | S754_infinity sx => S754_infinity false + | S754_finite sx mx ex => S754_finite false mx ex + | S754_zero sx => S754_zero false + end. + + Definition SFcompare f1 f2 := + match f1, f2 with + | S754_nan , _ | _, S754_nan => None + | S754_infinity s1, S754_infinity s2 => + Some match s1, s2 with + | true, true => Eq + | false, false => Eq + | true, false => Lt + | false, true => Gt + end + | S754_infinity s, _ => Some (if s then Lt else Gt) + | _, S754_infinity s => Some (if s then Gt else Lt) + | S754_finite s _ _, S754_zero _ => Some (if s then Lt else Gt) + | S754_zero _, S754_finite s _ _ => Some (if s then Gt else Lt) + | S754_zero _, S754_zero _ => Some Eq + | S754_finite s1 m1 e1, S754_finite s2 m2 e2 => + Some match s1, s2 with + | true, false => Lt + | false, true => Gt + | false, false => + match Z.compare e1 e2 with + | Lt => Lt + | Gt => Gt + | Eq => Pcompare m1 m2 Eq + end + | true, true => + match Z.compare e1 e2 with + | Lt => Gt + | Gt => Lt + | Eq => CompOpp (Pcompare m1 m2 Eq) + end + end + end. + + Definition SFeqb f1 f2 := + match SFcompare f1 f2 with + | Some Eq => true + | _ => false + end. + + Definition SFltb f1 f2 := + match SFcompare f1 f2 with + | Some Lt => true + | _ => false + end. + + Definition SFleb f1 f2 := + match SFcompare f1 f2 with + | Some (Lt | Eq) => true + | _ => false + end. + + Variant float_class : Set := + | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN. + + Definition SFclassify f := + match f with + | S754_nan => NaN + | S754_infinity false => PInf + | S754_infinity true => NInf + | S754_zero false => NZero + | S754_zero true => PZero + | S754_finite false m _ => + if (digits2_pos m =? Z.to_pos prec)%positive then PNormal + else PSubn + | S754_finite true m _ => + if (digits2_pos m =? Z.to_pos prec)%positive then NNormal + else NSubn + end. + + Definition SFmul x y := + match x, y with + | S754_nan, _ | _, S754_nan => S754_nan + | S754_infinity sx, S754_infinity sy => S754_infinity (xorb sx sy) + | S754_infinity sx, S754_finite sy _ _ => S754_infinity (xorb sx sy) + | S754_finite sx _ _, S754_infinity sy => S754_infinity (xorb sx sy) + | S754_infinity _, S754_zero _ => S754_nan + | S754_zero _, S754_infinity _ => S754_nan + | S754_finite sx _ _, S754_zero sy => S754_zero (xorb sx sy) + | S754_zero sx, S754_finite sy _ _ => S754_zero (xorb sx sy) + | S754_zero sx, S754_zero sy => S754_zero (xorb sx sy) + | S754_finite sx mx ex, S754_finite sy my ey => + binary_round_aux (xorb sx sy) (Zpos (mx * my)) (ex + ey) loc_Exact + end. + + Definition cond_Zopp (b : bool) m := if b then Z.opp m else m. + + Definition SFadd x y := + match x, y with + | S754_nan, _ | _, S754_nan => S754_nan + | S754_infinity sx, S754_infinity sy => + if Bool.eqb sx sy then x else S754_nan + | S754_infinity _, _ => x + | _, S754_infinity _ => y + | S754_zero sx, S754_zero sy => + if Bool.eqb sx sy then x else + S754_zero false + | S754_zero _, _ => y + | _, S754_zero _ => x + | S754_finite sx mx ex, S754_finite sy my ey => + let ez := Z.min ex ey in + binary_normalize (Zplus (cond_Zopp sx (Zpos (fst (shl_align mx ex ez)))) (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))) + ez false + end. + + Definition SFsub x y := + match x, y with + | S754_nan, _ | _, S754_nan => S754_nan + | S754_infinity sx, S754_infinity sy => + if Bool.eqb sx (negb sy) then x else S754_nan + | S754_infinity _, _ => x + | _, S754_infinity sy => S754_infinity (negb sy) + | S754_zero sx, S754_zero sy => + if Bool.eqb sx (negb sy) then x else + S754_zero false + | S754_zero _, S754_finite sy my ey => S754_finite (negb sy) my ey + | _, S754_zero _ => x + | S754_finite sx mx ex, S754_finite sy my ey => + let ez := Z.min ex ey in + binary_normalize (Zminus (cond_Zopp sx (Zpos (fst (shl_align mx ex ez)))) (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))) + ez false + end. + + Definition new_location_even nb_steps k := + if Zeq_bool k 0 then loc_Exact + else loc_Inexact (Z.compare (2 * k) nb_steps). + + Definition new_location_odd nb_steps k := + if Zeq_bool k 0 then loc_Exact + else + loc_Inexact + match Z.compare (2 * k + 1) nb_steps with + | Lt => Lt + | Eq => Lt + | Gt => Gt + end. + + Definition new_location nb_steps := + if Z.even nb_steps then new_location_even nb_steps else new_location_odd nb_steps. + + Definition SFdiv_core_binary m1 e1 m2 e2 := + let d1 := Zdigits2 m1 in + let d2 := Zdigits2 m2 in + let e' := Z.min (fexp (d1 + e1 - (d2 + e2))) (e1 - e2) in + let s := (e1 - e2 - e')%Z in + let m' := + match s with + | Zpos _ => Z.shiftl m1 s + | Z0 => m1 + | Zneg _ => Z0 + end in + let '(q, r) := Z.div_eucl m' m2 in + (q, e', new_location m2 r). + + Definition SFdiv x y := + match x, y with + | S754_nan, _ | _, S754_nan => S754_nan + | S754_infinity sx, S754_infinity sy => S754_nan + | S754_infinity sx, S754_finite sy _ _ => S754_infinity (xorb sx sy) + | S754_finite sx _ _, S754_infinity sy => S754_zero (xorb sx sy) + | S754_infinity sx, S754_zero sy => S754_infinity (xorb sx sy) + | S754_zero sx, S754_infinity sy => S754_zero (xorb sx sy) + | S754_finite sx _ _, S754_zero sy => S754_infinity (xorb sx sy) + | S754_zero sx, S754_finite sy _ _ => S754_zero (xorb sx sy) + | S754_zero sx, S754_zero sy => S754_nan + | S754_finite sx mx ex, S754_finite sy my ey => + let '(mz, ez, lz) := SFdiv_core_binary (Zpos mx) ex (Zpos my) ey in + binary_round_aux (xorb sx sy) mz ez lz + end. + + Definition SFsqrt_core_binary m e := + let d := Zdigits2 m in + let e' := Z.min (fexp (Z.div2 (d + e + 1))) (Z.div2 e) in + let s := (e - 2 * e')%Z in + let m' := + match s with + | Zpos p => Z.shiftl m s + | Z0 => m + | Zneg _ => Z0 + end in + let (q, r) := Z.sqrtrem m' in + let l := + if Zeq_bool r 0 then loc_Exact + else loc_Inexact (if Zle_bool r q then Lt else Gt) in + (q, e', l). + + Definition SFsqrt x := + match x with + | S754_nan => S754_nan + | S754_infinity false => x + | S754_infinity true => S754_nan + | S754_finite true _ _ => S754_nan + | S754_zero _ => x + | S754_finite sx mx ex => + let '(mz, ez, lz) := SFsqrt_core_binary (Zpos mx) ex in + binary_round_aux false mz ez lz + end. + + Definition SFnormfr_mantissa f := + match f with + | S754_finite _ mx ex => + if Z.eqb ex (-prec) then Npos mx else 0%N + | _ => 0%N + end. + + Definition SFldexp f e := + match f with + | S754_finite sx mx ex => binary_round sx mx (ex+e) + | _ => f + end. + + Definition SFfrexp f := + match f with + | S754_finite sx mx ex => + if (Z.to_pos prec <=? digits2_pos mx)%positive then + (S754_finite sx mx (-prec), (ex+prec)%Z) + else + let d := (prec - Z.pos (digits2_pos mx))%Z in + (S754_finite sx (shift_pos (Z.to_pos d) mx) (-prec), (ex+prec-d)%Z) + | _ => (f, (-2*emax-prec)%Z) + end. + + Definition SFone := binary_round false 1 0. + + Definition SFulp x := SFldexp SFone (fexp (snd (SFfrexp x))). + + Definition SFpred_pos x := + match x with + | S754_finite _ mx _ => + let d := + if (mx~0 =? shift_pos (Z.to_pos prec) 1)%positive then + SFldexp SFone (fexp (snd (SFfrexp x) - 1)) + else + SFulp x in + SFsub x d + | _ => x + end. + + Definition SFmax_float := + S754_finite false (shift_pos (Z.to_pos prec) 1 - 1) (emax - prec). + + Definition SFsucc x := + match x with + | S754_zero _ => SFldexp SFone emin + | S754_infinity false => x + | S754_infinity true => SFopp SFmax_float + | S754_nan => x + | S754_finite false _ _ => SFadd x (SFulp x) + | S754_finite true _ _ => SFopp (SFpred_pos (SFopp x)) + end. + + Definition SFpred f := SFopp (SFsucc (SFopp f)). +End FloatOps. diff --git a/flocq/Prop/Div_sqrt_error.v b/flocq/Prop/Div_sqrt_error.v index 79220438..9aa9c508 100644 --- a/flocq/Prop/Div_sqrt_error.v +++ b/flocq/Prop/Div_sqrt_error.v @@ -42,9 +42,7 @@ rewrite H; apply generic_format_0. rewrite Hx, Hy, <- F2R_plus. apply generic_format_F2R. intros _. -case_eq (Fplus fx fy). -intros mz ez Hz. -rewrite <- Hz. +change (F2R _) with (F2R (Fplus fx fy)). apply Z.le_trans with (Z.min (Fexp fx) (Fexp fy)). rewrite F2R_plus, <- Hx, <- Hy. unfold cexp. @@ -52,7 +50,7 @@ apply Z.le_trans with (1:=Hfexp _). apply Zplus_le_reg_l with prec; ring_simplify. apply mag_le_bpow with (1 := H). now apply Z.min_case. -rewrite <- Fexp_Fplus, Hz. +rewrite <- Fexp_Fplus. apply Z.le_refl. Qed. @@ -100,7 +98,7 @@ apply Rlt_le_trans with (1 := Heps1). change 1%R with (bpow 0). apply bpow_le. generalize (prec_gt_0 prec). -clear ; omega. +clear ; lia. rewrite Rmult_1_r. rewrite Hx2, <- Hx1. unfold cexp. @@ -193,7 +191,7 @@ now apply IZR_lt. rewrite <- Rmult_assoc, Rinv_r, Rmult_1_l. apply Rle_trans with (bpow (-1)). apply bpow_le. -omega. +lia. replace (2 * (-1 + 5 / 4))%R with (/2)%R by field. apply Rinv_le. now apply IZR_lt. @@ -280,11 +278,11 @@ apply Rle_not_lt. rewrite <- Hr1. apply abs_round_ge_generic... apply generic_format_bpow. -unfold FLX_exp; omega. +unfold FLX_exp; lia. apply Es. apply Rlt_le_trans with (1:=H). apply bpow_le. -omega. +lia. now apply Rlt_le. Qed. @@ -319,7 +317,7 @@ rewrite <- bpow_plus; apply bpow_le; unfold e; set (mxm1 := (_ - 1)%Z). replace (_ * _)%Z with (2 * (mxm1 / 2) + mxm1 mod 2 - mxm1 mod 2)%Z by ring. rewrite <- Z.div_mod; [|now simpl]. apply (Zplus_le_reg_r _ _ (mxm1 mod 2 - mag beta x)%Z). -unfold mxm1; destruct (Z.mod_bound_or (mag beta x - 1) 2); omega. +unfold mxm1; destruct (Z.mod_bound_or (mag beta x - 1) 2); lia. Qed. Notation u_ro := (u_ro beta prec). @@ -346,7 +344,7 @@ assert (Hulp1p2eps : (ulp beta (FLX_exp prec) (1 + 2 * u_ro) = 2 * u_ro)%R). rewrite succ_FLX_1, mag_1, bpow_1, <- H2eps; simpl. apply (Rlt_le_trans _ 2); [apply Rplus_lt_compat_l|]. { unfold u_ro; rewrite <-Rmult_assoc, Rinv_r, Rmult_1_l; [|lra]. - change R1 with (bpow 0); apply bpow_lt; omega. } + change R1 with (bpow 0); apply bpow_lt; lia. } apply IZR_le, Zle_bool_imp_le, radix_prop. } assert (Hsucc1p2eps : (succ beta (FLX_exp prec) (1 + 2 * u_ro) = 1 + 4 * u_ro)%R). @@ -383,7 +381,7 @@ ring_simplify; apply Rsqr_incr_0_var. apply Rmult_le_pos; [|now apply pow_le]. assert (Heps_le_half : (u_ro <= 1 / 2)%R). { unfold u_ro, Rdiv; rewrite Rmult_comm; apply Rmult_le_compat_r; [lra|]. - change 1%R with (bpow 0); apply bpow_le; omega. } + change 1%R with (bpow 0); apply bpow_le; lia. } apply (Rle_trans _ (-8 * u_ro + 4)); [lra|]. apply Rplus_le_compat_r, Rmult_le_compat_r; [apply Pu_ro|]. now assert (H : (0 <= u_ro ^ 2)%R); [apply pow2_ge_0|lra]. } @@ -447,13 +445,13 @@ destruct (sqrt_error_N_FLX_aux2 _ Fmu HmuGe1) as [Hmu'|[Hmu'|Hmu']]. { rewrite Rminus_diag_eq, Rabs_R0; [|now simpl]. now apply Rmult_le_pos; [|apply Rabs_pos]. } apply generic_format_bpow'; [now apply FLX_exp_valid|]. - unfold FLX_exp; omega. } + unfold FLX_exp; lia. } { assert (Hsqrtmu : (1 <= sqrt mu < 1 + u_ro)%R); [rewrite Hmu'; split|]. { rewrite <- sqrt_1 at 1; apply sqrt_le_1_alt; lra. } { rewrite <- sqrt_square; [|lra]; apply sqrt_lt_1_alt; split; [lra|]. ring_simplify; assert (0 < u_ro ^ 2)%R; [apply pow_lt|]; lra. } assert (Fbpowe : generic_format beta (FLX_exp prec) (bpow e)). - { apply generic_format_bpow; unfold FLX_exp; omega. } + { apply generic_format_bpow; unfold FLX_exp; lia. } assert (Hrt : rt = bpow e :> R). { unfold rt; fold t; rewrite Ht; simpl; apply Rle_antisym. { apply round_N_le_midp; [now apply FLX_exp_valid|exact Fbpowe|]. @@ -495,7 +493,7 @@ assert (Hulpt : (ulp beta (FLX_exp prec) t = 2 * u_ro * bpow e)%R). { apply sqrt_lt_1_alt; split; [lra|]. apply (Rlt_le_trans _ _ _ HmuLtsqradix); right. now unfold bpow, Z.pow_pos; simpl; rewrite Zmult_1_r, mult_IZR. } - apply IZR_le, (Z.le_trans _ 2), Zle_bool_imp_le, radix_prop; omega. } + apply IZR_le, (Z.le_trans _ 2), Zle_bool_imp_le, radix_prop; lia. } rewrite Hmagt; ring. } rewrite Ht; apply Rmult_lt_0_compat; [|now apply bpow_gt_0]. now apply (Rlt_le_trans _ 1); [lra|rewrite <- sqrt_1; apply sqrt_le_1_alt]. } @@ -656,7 +654,7 @@ apply Fourier_util.Rle_mult_inv_pos; assumption. case (Zle_lt_or_eq 0 n); try exact H. clear H; intros H. case (Zle_lt_or_eq 1 n). -omega. +lia. clear H; intros H. set (ex := cexp beta fexp x). set (ey := cexp beta fexp y). @@ -715,7 +713,7 @@ rewrite Rinv_l, Rmult_1_r, Rmult_1_l. assert (mag beta x < mag beta y)%Z. case (Zle_or_lt (mag beta y) (mag beta x)); try easy. intros J; apply monotone_exp in J; clear -J Hexy. -unfold ex, ey, cexp in Hexy; omega. +unfold ex, ey, cexp in Hexy; lia. left; apply lt_mag with beta; easy. (* n = 1 -> Sterbenz + rnd_small *) intros Hn'; fold n; rewrite <- Hn'. diff --git a/flocq/Prop/Double_rounding.v b/flocq/Prop/Double_rounding.v index 055409bb..3e942fe0 100644 --- a/flocq/Prop/Double_rounding.v +++ b/flocq/Prop/Double_rounding.v @@ -122,7 +122,7 @@ destruct (Req_dec x'' 0) as [Zx''|Nzx'']. apply (Rle_lt_trans _ _ _ Hr1). apply Rmult_lt_compat_l; [lra|]. apply bpow_lt. - omega. + lia. - (* x'' <> 0 *) assert (Lx'' : mag x'' = mag x :> Z). { apply Zle_antisym. @@ -203,7 +203,7 @@ destruct (Req_dec x' 0) as [Zx'|Nzx']. replace (2 * (/ 2 * _)) with (bpow (fexp1 (mag x) - mag x)) by field. apply Rle_trans with 1; [|lra]. change 1 with (bpow 0); apply bpow_le. - omega. + lia. - (* x' <> 0 *) assert (Px' : 0 < x'). { assert (0 <= x'); [|lra]. @@ -314,10 +314,10 @@ Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx Hx'. destruct (Zle_or_lt (fexp1 (mag x)) (fexp2 (mag x))) as [Hf2'|Hf2']. - (* fexp1 (mag x) <= fexp2 (mag x) *) - assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z); [omega|]. + assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z) by lia. now apply round_round_lt_mid_same_place. - (* fexp2 (mag x) < fexp1 (mag x) *) - assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z); [omega|]. + assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia. generalize (Hx' Hf2''); intro Hx''. now apply round_round_lt_mid_further_place. Qed. @@ -380,7 +380,7 @@ destruct (Req_dec x'' 0) as [Zx''|Nzx'']. apply (Rle_lt_trans _ _ _ Hr1). apply Rmult_lt_compat_l; [lra|]. apply bpow_lt. - omega. + lia. - (* x'' <> 0 *) assert (Lx'' : mag x'' = mag x :> Z). { apply Zle_antisym. @@ -460,11 +460,11 @@ assert (Hx''pow : x'' = bpow (mag x)). unfold x'', round, F2R, scaled_mantissa, cexp; simpl. apply (Rmult_le_reg_r (bpow (- fexp2 (mag x)))); [now apply bpow_gt_0|]. bpow_simplify. - rewrite <- (IZR_Zpower _ (_ - _)); [|omega]. + rewrite <- (IZR_Zpower _ (_ - _)); [|lia]. apply IZR_le. apply Zlt_succ_le; unfold Z.succ. apply lt_IZR. - rewrite plus_IZR; rewrite IZR_Zpower; [|omega]. + rewrite plus_IZR; rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (fexp2 (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_plus_distr_r; rewrite Rmult_1_l. bpow_simplify. @@ -482,12 +482,12 @@ assert (Hr : Rabs (x - x'') < / 2 * ulp beta fexp1 x). - apply Rmult_lt_compat_l; [lra|]. rewrite 2!ulp_neq_0; try now apply Rgt_not_eq. unfold cexp; apply bpow_lt. - omega. } + lia. } unfold round, F2R, scaled_mantissa, cexp; simpl. assert (Hf : (0 <= mag x - fexp1 (mag x''))%Z). { rewrite Hx''pow. rewrite mag_bpow. - assert (fexp1 (mag x + 1) <= mag x)%Z; [|omega]. + assert (fexp1 (mag x + 1) <= mag x)%Z; [|lia]. destruct (Zle_or_lt (mag x) (fexp1 (mag x))) as [Hle|Hlt]; [|now apply Vfexp1]. assert (H : (mag x = fexp1 (mag x) :> Z)%Z); @@ -497,9 +497,9 @@ assert (Hf : (0 <= mag x - fexp1 (mag x''))%Z). rewrite (Znearest_imp _ _ (beta ^ (mag x - fexp1 (mag x'')))%Z). - rewrite (Znearest_imp _ _ (beta ^ (mag x - fexp1 (mag x)))%Z). + rewrite IZR_Zpower; [|exact Hf]. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. now bpow_simplify. - + rewrite IZR_Zpower; [|omega]. + + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; [|now apply Rle_ge; apply bpow_ge_0]. @@ -588,10 +588,10 @@ Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx Hx'. destruct (Zle_or_lt (fexp1 (mag x)) (fexp2 (mag x))) as [Hf2'|Hf2']. - (* fexp1 (mag x) <= fexp2 (mag x) *) - assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z); [omega|]. + assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z) by lia. now apply round_round_gt_mid_same_place. - (* fexp2 (mag x) < fexp1 (mag x) *) - assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z); [omega|]. + assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia. generalize (Hx' Hf2''); intro Hx''. now apply round_round_gt_mid_further_place. Qed. @@ -606,7 +606,7 @@ Lemma mag_mult_disj : Proof. intros x y Zx Zy. destruct (mag_mult beta x y Zx Zy). -omega. +lia. Qed. Definition round_round_mult_hyp fexp1 fexp2 := @@ -691,7 +691,7 @@ intros Hprec x y Fx Fy. apply round_round_mult; [|now apply generic_format_FLX|now apply generic_format_FLX]. unfold round_round_mult_hyp; split; intros ex ey; unfold FLX_exp; -omega. +lia. Qed. End Double_round_mult_FLX. @@ -721,7 +721,7 @@ generalize (Zmax_spec (ex + ey - prec') emin'); generalize (Zmax_spec (ex + ey - 1 - prec') emin'); generalize (Zmax_spec (ex - prec) emin); generalize (Zmax_spec (ey - prec) emin); -omega. +lia. Qed. End Double_round_mult_FLT. @@ -753,7 +753,7 @@ destruct (Z.ltb_spec (ex + ey - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex + ey - 1 - prec') emin'); -omega. +lia. Qed. End Double_round_mult_FTZ. @@ -770,7 +770,7 @@ Lemma mag_plus_disj : Proof. intros x y Py Hxy. destruct (mag_plus beta x y Py Hxy). -omega. +lia. Qed. Lemma mag_plus_separated : @@ -798,10 +798,10 @@ Lemma mag_minus_disj : \/ (mag (x - y) = (mag x - 1)%Z :> Z)). Proof. intros x y Px Py Hln. -assert (Hxy : y < x); [now apply (lt_mag beta); [ |omega]|]. +assert (Hxy : y < x); [now apply (lt_mag beta); [ |lia]|]. generalize (mag_minus beta x y Py Hxy); intro Hln2. generalize (mag_minus_lb beta x y Px Py Hln); intro Hln3. -omega. +lia. Qed. Lemma mag_minus_separated : @@ -831,7 +831,7 @@ split. apply succ_le_lt; [apply Vfexp|idtac|exact Fx|assumption]. apply (generic_format_bpow beta fexp (mag x - 1)). replace (_ + _)%Z with (mag x : Z) by ring. - assert (fexp (mag x) < mag x)%Z; [|omega]. + assert (fexp (mag x) < mag x)%Z; [|lia]. now apply mag_generic_gt; [|now apply Rgt_not_eq|]. - rewrite Rabs_right. + apply Rlt_trans with x. @@ -884,7 +884,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. rewrite Rmult_plus_distr_r. rewrite <- Fx. rewrite mult_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. bpow_simplify. now rewrite <- Fy. } apply generic_format_F2R' with (f := fxy); [now rewrite Hxy|]. @@ -904,7 +904,7 @@ intros fexp1 fexp2 x y Hlnx Hlny Fx Fy. destruct (Z.le_gt_cases (fexp1 (mag x)) (fexp1 (mag y))) as [Hle|Hgt]. - now apply (round_round_plus_aux0_aux_aux fexp1). - rewrite Rplus_comm in Hlnx, Hlny |- *. - now apply (round_round_plus_aux0_aux_aux fexp1); [omega| | | |]. + now apply (round_round_plus_aux0_aux_aux fexp1); [lia| | | |]. Qed. (* fexp1 (mag x) - 1 <= mag y : @@ -927,20 +927,20 @@ destruct (Z.le_gt_cases (mag y) (fexp1 (mag x))) as [Hle|Hgt]. [now apply (mag_plus_separated fexp1)|]. apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption]; rewrite Lxy. - + now apply Hexp4; omega. - + now apply Hexp3; omega. + + now apply Hexp4; lia. + + now apply Hexp3; lia. - (* fexp1 (mag x) < mag y *) apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption]. destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - + now apply Hexp4; omega. + + now apply Hexp4; lia. + apply Hexp2; apply (mag_le beta y x Py) in Hyx. replace (_ - _)%Z with (mag x : Z) by ring. - omega. + lia. + destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - * now apply Hexp3; omega. + * now apply Hexp3; lia. * apply Hexp2. replace (_ - _)%Z with (mag x : Z) by ring. - omega. + lia. Qed. Lemma round_round_plus_aux1_aux : @@ -983,7 +983,7 @@ assert (UB : y * bpow (- fexp (mag x)) < / IZR (beta ^ k)). + bpow_simplify. rewrite bpow_opp. destruct k. - * omega. + * lia. * simpl; unfold Raux.bpow, Z.pow_pos. now apply Rle_refl. * casetype False; apply (Z.lt_irrefl 0). @@ -1003,7 +1003,7 @@ rewrite (Zfloor_imp mx). apply (Rlt_le_trans _ _ _ UB). rewrite bpow_opp. apply Rinv_le; [now apply bpow_gt_0|]. - now rewrite IZR_Zpower; [right|omega]. } + now rewrite IZR_Zpower; [right|lia]. } split. - rewrite <- Rplus_0_r at 1; apply Rplus_le_compat_l. now apply Rlt_le. @@ -1014,7 +1014,7 @@ split. apply Rlt_trans with (bpow (mag y)). + rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le]. apply bpow_mag_gt. - + apply bpow_lt; omega. + + apply bpow_lt; lia. Qed. (* mag y <= fexp1 (mag x) - 2 : round_round_lt_mid applies. *) @@ -1034,18 +1034,18 @@ assert (Hbeta : (2 <= beta)%Z). now apply Zle_bool_imp_le. } intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Hly Fx. assert (Lxy : mag (x + y) = mag x :> Z); - [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |omega]|]. + [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |lia]|]. destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z); - [now apply Hexp4; omega|]. + [now apply Hexp4; lia|]. assert (Bpow2 : bpow (- 2) <= / 2 * / 2). { replace (/2 * /2) with (/4) by field. rewrite (bpow_opp _ 2). apply Rinv_le; [lra|]. apply (IZR_le (2 * 2) (beta * (beta * 1))). rewrite Zmult_1_r. - now apply Zmult_le_compat; omega. } -assert (P2 : (0 < 2)%Z) by omega. + now apply Zmult_le_compat; lia. } +assert (P2 : (0 < 2)%Z) by lia. unfold round_round_eq. apply round_round_lt_mid. - exact Vfexp1. @@ -1053,7 +1053,7 @@ apply round_round_lt_mid. - lra. - now rewrite Lxy. - rewrite Lxy. - assert (fexp1 (mag x) < mag x)%Z; [|omega]. + assert (fexp1 (mag x) < mag x)%Z; [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - unfold midp. apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))). @@ -1088,10 +1088,10 @@ apply round_round_lt_mid. replace (_ - _) with (- (/ 2)) by lra. apply Ropp_le_contravar. { apply Rle_trans with (bpow (- 1)). - - apply bpow_le; omega. + - apply bpow_le; lia. - unfold Raux.bpow, Z.pow_pos; simpl. apply Rinv_le; [lra|]. - apply IZR_le; omega. } + apply IZR_le; lia. } Qed. (* round_round_plus_aux{0,1} together *) @@ -1115,7 +1115,7 @@ destruct (Zle_or_lt (mag y) (fexp1 (mag x) - 2)) as [Hly|Hly]. rewrite (round_generic beta fexp2). + reflexivity. + now apply valid_rnd_N. - + assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z); [omega|]. + + assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z) by lia. now apply (round_round_plus_aux0 fexp1). Qed. @@ -1140,7 +1140,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. + reflexivity. + now apply valid_rnd_N. + apply (generic_inclusion_mag beta fexp1). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fy. - (* x <> 0 *) destruct (Req_dec y 0) as [Zy|Nzy]. @@ -1151,7 +1151,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * reflexivity. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fx. + (* y <> 0 *) assert (Px : 0 < x); [lra|]. @@ -1199,21 +1199,21 @@ assert (Lyx : (mag y <= mag x)%Z); destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge]. - (* mag x - 2 < mag y *) assert (Hor : (mag y = mag x :> Z) - \/ (mag y = mag x - 1 :> Z)%Z); [omega|]. + \/ (mag y = mag x - 1 :> Z)%Z) by lia. destruct Hor as [Heq|Heqm1]. + (* mag y = mag x *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. * rewrite Heq. apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. + (* mag y = mag x - 1 *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. * rewrite Heqm1. apply Hexp4. @@ -1224,7 +1224,7 @@ destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge]. + (* mag (x - y) = mag x *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - omega. + lia. * now rewrite Lxmy; apply Hexp3. + (* mag (x - y) = mag x - 1 *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]; @@ -1261,8 +1261,8 @@ assert (Hfy : (fexp1 (mag y) < mag y)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. - apply Z.le_trans with (fexp1 (mag (x - y))). - + apply Hexp4; omega. - + omega. + + apply Hexp4; lia. + + lia. - now apply Hexp3. Qed. @@ -1289,7 +1289,7 @@ assert (Hfy : (fexp (mag y) < mag y)%Z); destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx]. - (* bpow (mag x - 1) < x *) assert (Lxy : mag (x - y) = mag x :> Z); - [now apply (mag_minus_separated fexp); [| | | | | |omega]|]. + [now apply (mag_minus_separated fexp); [| | | | | |lia]|]. assert (Rxy : round beta fexp Zceil (x - y) = x). { unfold round, F2R, scaled_mantissa, cexp; simpl. rewrite Lxy. @@ -1311,7 +1311,7 @@ destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx]. + rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le]. apply bpow_mag_gt. + apply bpow_le. - omega. + lia. - rewrite <- (Rplus_0_r (IZR _)) at 2. apply Rplus_le_compat_l. rewrite <- Ropp_0; apply Ropp_le_contravar. @@ -1334,9 +1334,9 @@ destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx]. now intro Hx'; rewrite Hx' in Hxy; apply (Rlt_irrefl y). + rewrite Rabs_right; lra. - apply (mag_minus_lb beta x y Px Py). - omega. } + lia. } assert (Hfx1 : (fexp (mag x - 1) < mag x - 1)%Z); - [now apply (valid_exp_large fexp (mag y)); [|omega]|]. + [now apply (valid_exp_large fexp (mag y)); [|lia]|]. assert (Rxy : round beta fexp Zceil (x - y) <= x). { rewrite Xpow at 2. unfold round, F2R, scaled_mantissa, cexp; simpl. @@ -1344,10 +1344,10 @@ destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx]. apply (Rmult_le_reg_r (bpow (- fexp (mag x - 1)%Z))); [now apply bpow_gt_0|]. bpow_simplify. - rewrite <- (IZR_Zpower beta (_ - _ - _)); [|omega]. + rewrite <- (IZR_Zpower beta (_ - _ - _)); [|lia]. apply IZR_le. apply Zceil_glb. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. rewrite Xpow at 1. rewrite Rmult_minus_distr_r. bpow_simplify. @@ -1383,7 +1383,7 @@ intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hxy Hly Hly' Fx Fy. assert (Px := Rlt_trans 0 y x Py Hxy). destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z); - [now apply Hexp4; omega|]. + [now apply Hexp4; lia|]. assert (Hfx : (fexp1 (mag x) < mag x)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. assert (Bpow2 : bpow (- 2) <= / 2 * / 2). @@ -1392,7 +1392,7 @@ assert (Bpow2 : bpow (- 2) <= / 2 * / 2). apply Rinv_le; [lra|]. apply (IZR_le (2 * 2) (beta * (beta * 1))). rewrite Zmult_1_r. - now apply Zmult_le_compat; omega. } + now apply Zmult_le_compat; lia. } assert (Ly : y < bpow (mag y)). { apply Rabs_lt_inv. apply bpow_mag_gt. } @@ -1401,19 +1401,19 @@ apply round_round_gt_mid. - exact Vfexp1. - exact Vfexp2. - lra. -- apply Hexp4; omega. -- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|omega]. +- apply Hexp4; lia. +- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|lia]. apply (valid_exp_large fexp1 (mag x - 1)). - + apply (valid_exp_large fexp1 (mag y)); [|omega]. + + apply (valid_exp_large fexp1 (mag y)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - + now apply mag_minus_lb; [| |omega]. + + now apply mag_minus_lb; [| |lia]. - unfold midp'. apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y))). ring_simplify. replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring. apply Rlt_le_trans with (bpow (fexp1 (mag (x - y)) - 2)). + apply Rle_lt_trans with y; - [now apply round_round_minus_aux2_aux; try assumption; omega|]. + [now apply round_round_minus_aux2_aux; try assumption; lia|]. apply (Rlt_le_trans _ _ _ Ly). now apply bpow_le. + rewrite ulp_neq_0;[idtac|now apply sym_not_eq, Rlt_not_eq, Rgt_minus]. @@ -1428,7 +1428,7 @@ apply round_round_gt_mid. rewrite Zmult_1_r; apply Rinv_le. lra. now apply IZR_le. - * apply bpow_le; omega. + * apply bpow_le; lia. - intro Hf2'. unfold midp'. apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y) @@ -1436,7 +1436,7 @@ apply round_round_gt_mid. ring_simplify. replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring. apply Rle_lt_trans with y; - [now apply round_round_minus_aux2_aux; try assumption; omega|]. + [now apply round_round_minus_aux2_aux; try assumption; lia|]. apply (Rlt_le_trans _ _ _ Ly). apply Rle_trans with (bpow (fexp1 (mag (x - y)) - 2)); [now apply bpow_le|]. @@ -1501,12 +1501,12 @@ destruct (Req_dec y x) as [Hy|Hy]. { rewrite (round_generic beta fexp2). - reflexivity. - now apply valid_rnd_N. - - assert (Hf1 : (fexp1 (mag (x - y)) - 1 <= mag y)%Z); [omega|]. + - assert (Hf1 : (fexp1 (mag (x - y)) - 1 <= mag y)%Z) by lia. now apply (round_round_minus_aux1 fexp1). } + rewrite (round_generic beta fexp2). * reflexivity. * now apply valid_rnd_N. - * assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z); [omega|]. + * assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z) by lia. now apply (round_round_minus_aux0 fexp1). Qed. @@ -1532,7 +1532,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fy. - (* x <> 0 *) destruct (Req_dec y 0) as [Zy|Nzy]. @@ -1543,7 +1543,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fx. + (* y <> 0 *) assert (Px : 0 < x); [lra|]. @@ -1626,9 +1626,9 @@ Proof. intros Hprec. unfold FLX_exp. unfold round_round_plus_hyp; split; [|split; [|split]]; -intros ex ey; try omega. +intros ex ey; try lia. unfold Prec_gt_0 in prec_gt_0_. -omega. +lia. Qed. Theorem round_round_plus_FLX : @@ -1683,19 +1683,19 @@ unfold round_round_plus_hyp; split; [|split; [|split]]; intros ex ey. - generalize (Zmax_spec (ex + 1 - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - 1 - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - unfold Prec_gt_0 in prec_gt_0_. generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. Qed. Theorem round_round_plus_FLT : @@ -1753,18 +1753,18 @@ unfold round_round_plus_hyp; split; [|split; [|split]]; intros ex ey. - destruct (Z.ltb_spec (ex + 1 - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - 1 - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. Qed. Theorem round_round_plus_FTZ : @@ -1832,20 +1832,20 @@ destruct (Z.le_gt_cases (mag y) (fexp1 (mag x))) as [Hle|Hgt]. [now apply (mag_plus_separated fexp1)|]. apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption]; rewrite Lxy. - + now apply Hexp4; omega. - + now apply Hexp3; omega. + + now apply Hexp4; lia. + + now apply Hexp3; lia. - (* fexp1 (mag x) < mag y *) apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption]. destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - + now apply Hexp4; omega. + + now apply Hexp4; lia. + apply Hexp2; apply (mag_le beta y x Py) in Hyx. replace (_ - _)%Z with (mag x : Z) by ring. - omega. + lia. + destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - * now apply Hexp3; omega. + * now apply Hexp3; lia. * apply Hexp2. replace (_ - _)%Z with (mag x : Z) by ring. - omega. + lia. Qed. (* mag y <= fexp1 (mag x) - 1 : round_round_lt_mid applies. *) @@ -1863,16 +1863,16 @@ Lemma round_round_plus_radix_ge_3_aux1 : Proof. intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Hly Fx. assert (Lxy : mag (x + y) = mag x :> Z); - [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |omega]|]. + [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |lia]|]. destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z); - [now apply Hexp4; omega|]. + [now apply Hexp4; lia|]. assert (Bpow3 : bpow (- 1) <= / 3). { unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r. apply Rinv_le; [lra|]. now apply IZR_le. } -assert (P1 : (0 < 1)%Z) by omega. +assert (P1 : (0 < 1)%Z) by lia. unfold round_round_eq. apply round_round_lt_mid. - exact Vfexp1. @@ -1880,7 +1880,7 @@ apply round_round_lt_mid. - lra. - now rewrite Lxy. - rewrite Lxy. - assert (fexp1 (mag x) < mag x)%Z; [|omega]. + assert (fexp1 (mag x) < mag x)%Z; [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - unfold midp. apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))). @@ -1914,7 +1914,7 @@ apply round_round_lt_mid. apply (Rplus_le_reg_r (- 1)); ring_simplify. replace (_ - _) with (- (/ 3)) by lra. apply Ropp_le_contravar. - now apply Rle_trans with (bpow (- 1)); [apply bpow_le; omega|]. + now apply Rle_trans with (bpow (- 1)); [apply bpow_le; lia|]. Qed. (* round_round_plus_radix_ge_3_aux{0,1} together *) @@ -1940,7 +1940,7 @@ destruct (Zle_or_lt (mag y) (fexp1 (mag x) - 1)) as [Hly|Hly]. rewrite (round_generic beta fexp2). + reflexivity. + now apply valid_rnd_N. - + assert (Hf1 : (fexp1 (mag x) <= mag y)%Z); [omega|]. + + assert (Hf1 : (fexp1 (mag x) <= mag y)%Z) by lia. now apply (round_round_plus_radix_ge_3_aux0 fexp1). Qed. @@ -1966,7 +1966,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. + reflexivity. + now apply valid_rnd_N. + apply (generic_inclusion_mag beta fexp1). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fy. - (* x <> 0 *) destruct (Req_dec y 0) as [Zy|Nzy]. @@ -1977,7 +1977,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * reflexivity. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fx. + (* y <> 0 *) assert (Px : 0 < x); [lra|]. @@ -2009,21 +2009,21 @@ assert (Lyx : (mag y <= mag x)%Z); destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge]. - (* mag x - 2 < mag y *) assert (Hor : (mag y = mag x :> Z) - \/ (mag y = mag x - 1 :> Z)%Z); [omega|]. + \/ (mag y = mag x - 1 :> Z)%Z) by lia. destruct Hor as [Heq|Heqm1]. + (* mag y = mag x *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. * rewrite Heq. apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. + (* mag y = mag x - 1 *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. * rewrite Heqm1. apply Hexp4. @@ -2034,7 +2034,7 @@ destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge]. + (* mag (x - y) = mag x *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - omega. + lia. * now rewrite Lxmy; apply Hexp3. + (* mag (x - y) = mag x - 1 *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]; @@ -2071,8 +2071,8 @@ assert (Hfy : (fexp1 (mag y) < mag y)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. - apply Z.le_trans with (fexp1 (mag (x - y))). - + apply Hexp4; omega. - + omega. + + apply Hexp4; lia. + + lia. - now apply Hexp3. Qed. @@ -2097,7 +2097,7 @@ intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hxy Hly Hly' assert (Px := Rlt_trans 0 y x Py Hxy). destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z); - [now apply Hexp4; omega|]. + [now apply Hexp4; lia|]. assert (Hfx : (fexp1 (mag x) < mag x)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. assert (Bpow3 : bpow (- 1) <= / 3). @@ -2113,12 +2113,12 @@ apply round_round_gt_mid. - exact Vfexp1. - exact Vfexp2. - lra. -- apply Hexp4; omega. -- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|omega]. +- apply Hexp4; lia. +- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|lia]. apply (valid_exp_large fexp1 (mag x - 1)). - + apply (valid_exp_large fexp1 (mag y)); [|omega]. + + apply (valid_exp_large fexp1 (mag y)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - + now apply mag_minus_lb; [| |omega]. + + now apply mag_minus_lb; [| |lia]. - unfold midp'. apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y))). ring_simplify. @@ -2135,7 +2135,7 @@ apply round_round_gt_mid. apply Rmult_le_compat_r; [now apply bpow_ge_0|]. unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le; [lra|]. - now apply IZR_le; omega. + now apply IZR_le; lia. - intro Hf2'. unfold midp'. apply (Rplus_lt_reg_r (/ 2 * (ulp beta fexp1 (x - y) @@ -2164,7 +2164,7 @@ apply round_round_gt_mid. replace (_ - _) with (- / 3) by field. apply Ropp_le_contravar. apply Rle_trans with (bpow (- 1)). - * apply bpow_le; omega. + * apply bpow_le; lia. * unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le; [lra|]. now apply IZR_le. @@ -2204,12 +2204,12 @@ destruct (Req_dec y x) as [Hy|Hy]. { rewrite (round_generic beta fexp2). - reflexivity. - now apply valid_rnd_N. - - assert (Hf1 : (fexp1 (mag (x - y)) <= mag y)%Z); [omega|]. + - assert (Hf1 : (fexp1 (mag (x - y)) <= mag y)%Z) by lia. now apply (round_round_minus_radix_ge_3_aux1 fexp1). } + rewrite (round_generic beta fexp2). * reflexivity. * now apply valid_rnd_N. - * assert (Hf1 : (fexp1 (mag x) <= mag y)%Z); [omega|]. + * assert (Hf1 : (fexp1 (mag x) <= mag y)%Z) by lia. now apply (round_round_minus_radix_ge_3_aux0 fexp1). Qed. @@ -2236,7 +2236,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fy. - (* x <> 0 *) destruct (Req_dec y 0) as [Zy|Nzy]. @@ -2247,7 +2247,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fx. + (* y <> 0 *) assert (Px : 0 < x); [lra|]. @@ -2332,9 +2332,9 @@ Proof. intros Hprec. unfold FLX_exp. unfold round_round_plus_radix_ge_3_hyp; split; [|split; [|split]]; -intros ex ey; try omega. +intros ex ey; try lia. unfold Prec_gt_0 in prec_gt_0_. -omega. +lia. Qed. Theorem round_round_plus_radix_ge_3_FLX : @@ -2393,19 +2393,19 @@ unfold round_round_plus_radix_ge_3_hyp; split; [|split; [|split]]; intros ex ey. - generalize (Zmax_spec (ex + 1 - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - 1 - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - unfold Prec_gt_0 in prec_gt_0_. generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. Qed. Theorem round_round_plus_radix_ge_3_FLT : @@ -2467,18 +2467,18 @@ unfold round_round_plus_radix_ge_3_hyp; split; [|split; [|split]]; intros ex ey. - destruct (Z.ltb_spec (ex + 1 - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - 1 - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. Qed. Theorem round_round_plus_radix_ge_3_FTZ : @@ -2546,11 +2546,11 @@ intros Cmid. destruct (generic_format_EM beta fexp1 x) as [Fx|Nfx]. - (* generic_format beta fexp1 x *) rewrite (round_generic beta fexp2); [reflexivity|now apply valid_rnd_N|]. - now apply (generic_inclusion_mag beta fexp1); [omega|]. + now apply (generic_inclusion_mag beta fexp1); [lia|]. - (* ~ generic_format beta fexp1 x *) assert (Hceil : round beta fexp1 Zceil x = rd + u1); [now apply round_UP_DN_ulp|]. - assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z); [omega|]. + assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia. destruct (Rlt_or_le (x - rd) (/ 2 * (u1 - u2))). + (* x - rd < / 2 * (u1 - u2) *) apply round_round_lt_mid_further_place; try assumption. @@ -2587,7 +2587,7 @@ Proof. intros x Px. rewrite (mag_sqrt beta x Px). generalize (Zdiv2_odd_eqn (mag x + 1)). -destruct Z.odd ; intros ; omega. +destruct Z.odd ; intros ; lia. Qed. Lemma round_round_sqrt_aux : @@ -2638,7 +2638,7 @@ assert (Pb : 0 < b). apply Rlt_Rminus. unfold u2, u1. apply bpow_lt. - omega. } + lia. } assert (Pb' : 0 < b'). { now unfold b'; rewrite Rmult_plus_distr_l; apply Rplus_lt_0_compat. } assert (Hr : sqrt x <= a + b'). @@ -2654,7 +2654,7 @@ assert (Hf1 : (2 * fexp1 (mag (sqrt x)) <= fexp1 (mag (x)))%Z); [destruct (mag_sqrt_disj x Px) as [H'|H']; rewrite H'; apply Hexp|]. assert (Hlx : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z). { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (mag x)); [|omega]. + - apply (valid_exp_large fexp1 (mag x)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - rewrite <- Hlx. now apply mag_generic_gt; [|apply Rgt_not_eq|]. } @@ -2698,7 +2698,7 @@ destruct (Req_dec a 0) as [Za|Nza]. unfold b'; change (bpow _) with u1. apply Rlt_le_trans with (/ 2 * (u1 + u1)); [|lra]. apply Rmult_lt_compat_l; [lra|]; apply Rplus_lt_compat_l. - unfold u2, u1, ulp, cexp; apply bpow_lt; omega. + unfold u2, u1, ulp, cexp; apply bpow_lt; lia. - (* a <> 0 *) assert (Pa : 0 < a); [lra|]. assert (Hla : (mag a = mag (sqrt x) :> Z)). @@ -2731,7 +2731,7 @@ destruct (Req_dec a 0) as [Za|Nza]. * apply pow2_ge_0. * unfold Raux.bpow, Z.pow_pos; simpl; rewrite Zmult_1_r. apply Rinv_le; [lra|]. - change 4%Z with (2 * 2)%Z; apply IZR_le, Zmult_le_compat; omega. + change 4%Z with (2 * 2)%Z; apply IZR_le, Zmult_le_compat; lia. * rewrite <- (Rplus_0_l (u1 ^ 2)) at 1; apply Rplus_le_compat_r. apply pow2_ge_0. } assert (Hr' : x <= a * a + u1 * a). @@ -2744,11 +2744,11 @@ destruct (Req_dec a 0) as [Za|Nza]. apply (Rmult_le_reg_r (bpow (- 2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite Fx at 1; bpow_simplify. - rewrite <- IZR_Zpower; [|omega]. + rewrite <- IZR_Zpower; [|lia]. rewrite <- plus_IZR, <- 2!mult_IZR. apply IZR_le, Zlt_succ_le, lt_IZR. unfold Z.succ; rewrite plus_IZR; do 2 rewrite mult_IZR; rewrite plus_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite <- Fx. @@ -2787,12 +2787,12 @@ destruct (Req_dec a 0) as [Za|Nza]. apply Rinv_le; [lra|]. apply IZR_le. rewrite <- (Zmult_1_l 2). - apply Zmult_le_compat; omega. + apply Zmult_le_compat; lia. + assert (u2 ^ 2 < u1 ^ 2); [|unfold b'; lra]. unfold pow; do 2 rewrite Rmult_1_r. assert (H' : 0 <= u2); [unfold u2, ulp; apply bpow_ge_0|]. assert (u2 < u1); [|now apply Rmult_lt_compat]. - unfold u1, u2, ulp, cexp; apply bpow_lt; omega. } + unfold u1, u2, ulp, cexp; apply bpow_lt; lia. } apply (Rlt_irrefl (a * a + u1 * a)). apply Rlt_le_trans with (a * a + u1 * a - u2 * a + b * b). + rewrite <- (Rplus_0_r (a * a + _)) at 1. @@ -2835,7 +2835,8 @@ destruct (Rle_or_lt x 0) as [Npx|Px]. generalize ((proj1 (proj2 Hexp)) 1%Z). replace (_ - 1)%Z with 1%Z by ring. intro Hexp10. - assert (Hf0 : (fexp1 1 < 1)%Z); [omega|clear Hexp10]. + assert (Hf0 : (fexp1 1 < 1)%Z) by lia. + clear Hexp10. apply (valid_exp_large fexp1 1); [exact Hf0|]. apply mag_ge_bpow. rewrite Zeq_minus; [|reflexivity]. @@ -2847,18 +2848,18 @@ destruct (Rle_or_lt x 0) as [Npx|Px]. assert (Hf2 : (fexp2 (mag (sqrt x)) <= fexp1 (mag (sqrt x)) - 1)%Z). { assert (H : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z). { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (mag x)); [|omega]. + - apply (valid_exp_large fexp1 (mag x)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - rewrite <- Hlx. now apply mag_generic_gt; [|apply Rgt_not_eq|]. } generalize ((proj2 (proj2 Hexp)) (mag (sqrt x)) H). - omega. } + lia. } apply round_round_mid_cases. + exact Vfexp1. + exact Vfexp2. + now apply sqrt_lt_R0. - + omega. - + omega. + + lia. + + lia. + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid). apply (round_round_sqrt_aux fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx). Qed. @@ -2878,7 +2879,7 @@ Proof. intros Hprec. unfold FLX_exp. unfold Prec_gt_0 in prec_gt_0_. -unfold round_round_sqrt_hyp; split; [|split]; intro ex; omega. +unfold round_round_sqrt_hyp; split; [|split]; intro ex; lia. Qed. Theorem round_round_sqrt_FLX : @@ -2919,14 +2920,14 @@ unfold Prec_gt_0 in prec_gt_0_. unfold round_round_sqrt_hyp; split; [|split]; intros ex. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (2 * ex - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (2 * ex - 1 - prec) emin). - omega. + lia. - generalize (Zmax_spec (2 * ex - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ex - prec) emin). - omega. + lia. Qed. Theorem round_round_sqrt_FLT : @@ -2969,18 +2970,18 @@ unfold Prec_gt_0 in *. unfold round_round_sqrt_hyp; split; [|split]; intros ex. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (2 * ex - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (2 * ex - 1 - prec) emin); - omega. + lia. - intro H. destruct (Zle_or_lt emin (2 * ex - prec)) as [H'|H']. + destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); - omega. + lia. + casetype False. rewrite (Zlt_bool_true _ _ H') in H. - omega. + lia. Qed. Theorem round_round_sqrt_FTZ : @@ -3057,7 +3058,7 @@ assert (Pb : 0 < b). apply Rlt_Rminus. unfold u2, u1, ulp, cexp. apply bpow_lt. - omega. } + lia. } assert (Pb' : 0 < b'). { now unfold b'; rewrite Rmult_plus_distr_l; apply Rplus_lt_0_compat. } assert (Hr : sqrt x <= a + b'). @@ -3073,7 +3074,7 @@ assert (Hf1 : (2 * fexp1 (mag (sqrt x)) <= fexp1 (mag (x)))%Z); [destruct (mag_sqrt_disj x Px) as [H'|H']; rewrite H'; apply Hexp|]. assert (Hlx : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z). { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (mag x)); [|omega]. + - apply (valid_exp_large fexp1 (mag x)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - rewrite <- Hlx. now apply mag_generic_gt; [|apply Rgt_not_eq|]. } @@ -3117,7 +3118,7 @@ destruct (Req_dec a 0) as [Za|Nza]. unfold b'; change (bpow _) with u1. apply Rlt_le_trans with (/ 2 * (u1 + u1)); [|lra]. apply Rmult_lt_compat_l; [lra|]; apply Rplus_lt_compat_l. - unfold u2, u1, ulp, cexp; apply bpow_lt; omega. + unfold u2, u1, ulp, cexp; apply bpow_lt; lia. - (* a <> 0 *) assert (Pa : 0 < a); [lra|]. assert (Hla : (mag a = mag (sqrt x) :> Z)). @@ -3162,11 +3163,11 @@ destruct (Req_dec a 0) as [Za|Nza]. apply (Rmult_le_reg_r (bpow (- 2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite Fx at 1; bpow_simplify. - rewrite <- IZR_Zpower; [|omega]. + rewrite <- IZR_Zpower; [|lia]. rewrite <- plus_IZR, <- 2!mult_IZR. apply IZR_le, Zlt_succ_le, lt_IZR. unfold Z.succ; rewrite plus_IZR; do 2 rewrite mult_IZR; rewrite plus_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite <- Fx. @@ -3203,12 +3204,12 @@ destruct (Req_dec a 0) as [Za|Nza]. unfold Raux.bpow; simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r. apply Rinv_le; [lra|]. - apply IZR_le; omega. + apply IZR_le; lia. + assert (u2 ^ 2 < u1 ^ 2); [|unfold b'; lra]. unfold pow; do 2 rewrite Rmult_1_r. assert (H' : 0 <= u2); [unfold u2, ulp; apply bpow_ge_0|]. assert (u2 < u1); [|now apply Rmult_lt_compat]. - unfold u1, u2, ulp, cexp; apply bpow_lt; omega. } + unfold u1, u2, ulp, cexp; apply bpow_lt; lia. } apply (Rlt_irrefl (a * a + u1 * a)). apply Rlt_le_trans with (a * a + u1 * a - u2 * a + b * b). + rewrite <- (Rplus_0_r (a * a + _)) at 1. @@ -3263,7 +3264,8 @@ destruct (Rle_or_lt x 0) as [Npx|Px]. generalize ((proj1 (proj2 Hexp)) 1%Z). replace (_ - 1)%Z with 1%Z by ring. intro Hexp10. - assert (Hf0 : (fexp1 1 < 1)%Z); [omega|clear Hexp10]. + assert (Hf0 : (fexp1 1 < 1)%Z) by lia. + clear Hexp10. apply (valid_exp_large fexp1 1); [exact Hf0|]. apply mag_ge_bpow. rewrite Zeq_minus; [|reflexivity]. @@ -3275,18 +3277,18 @@ destruct (Rle_or_lt x 0) as [Npx|Px]. assert (Hf2 : (fexp2 (mag (sqrt x)) <= fexp1 (mag (sqrt x)) - 1)%Z). { assert (H : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z). { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (mag x)); [|omega]. + - apply (valid_exp_large fexp1 (mag x)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - rewrite <- Hlx. now apply mag_generic_gt; [|apply Rgt_not_eq|]. } generalize ((proj2 (proj2 Hexp)) (mag (sqrt x)) H). - omega. } + lia. } apply round_round_mid_cases. + exact Vfexp1. + exact Vfexp2. + now apply sqrt_lt_R0. - + omega. - + omega. + + lia. + + lia. + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid). apply (round_round_sqrt_radix_ge_4_aux Hbeta fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx). @@ -3307,7 +3309,7 @@ Proof. intros Hprec. unfold FLX_exp. unfold Prec_gt_0 in prec_gt_0_. -unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intro ex; omega. +unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intro ex; lia. Qed. Theorem round_round_sqrt_radix_ge_4_FLX : @@ -3350,14 +3352,14 @@ unfold Prec_gt_0 in prec_gt_0_. unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intros ex. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (2 * ex - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (2 * ex - 1 - prec) emin). - omega. + lia. - generalize (Zmax_spec (2 * ex - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ex - prec) emin). - omega. + lia. Qed. Theorem round_round_sqrt_radix_ge_4_FLT : @@ -3402,18 +3404,18 @@ unfold Prec_gt_0 in *. unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intros ex. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (2 * ex - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (2 * ex - 1 - prec) emin); - omega. + lia. - intro H. destruct (Zle_or_lt emin (2 * ex - prec)) as [H'|H']. + destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); - omega. + lia. + casetype False. rewrite (Zlt_bool_true _ _ H') in H. - omega. + lia. Qed. Theorem round_round_sqrt_radix_ge_4_FTZ : @@ -3479,7 +3481,7 @@ assert (Hf : F2R f = x). rewrite plus_IZR. rewrite Rmult_plus_distr_r. rewrite mult_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. unfold cexp at 2; bpow_simplify. unfold Zminus; rewrite bpow_plus. rewrite (Rmult_comm _ (bpow (- 1))). @@ -3489,11 +3491,11 @@ assert (Hf : F2R f = x). rewrite Ebeta. rewrite (mult_IZR 2). rewrite Rinv_mult_distr; - [|simpl; lra | apply IZR_neq; omega]. + [|simpl; lra | apply IZR_neq; lia]. rewrite <- Rmult_assoc; rewrite (Rmult_comm (IZR n)); rewrite (Rmult_assoc _ (IZR n)). rewrite Rinv_r; - [rewrite Rmult_1_r | apply IZR_neq; omega]. + [rewrite Rmult_1_r | apply IZR_neq; lia]. simpl; fold (cexp beta fexp1 x). rewrite <- 2!ulp_neq_0; try now apply Rgt_not_eq. fold u; rewrite Xmid at 2. @@ -3525,12 +3527,12 @@ assert (Hf : F2R f = x). unfold round, F2R, scaled_mantissa, cexp; simpl. bpow_simplify. rewrite Lrd. - rewrite <- (IZR_Zpower _ (_ - _)); [|omega]. + rewrite <- (IZR_Zpower _ (_ - _)); [|lia]. rewrite <- mult_IZR. rewrite (Zfloor_imp (Zfloor (x * bpow (- fexp1 (mag x))) * beta ^ (fexp1 (mag x) - fexp2 (mag x)))). + rewrite mult_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. bpow_simplify. now unfold rd. + split; [now apply Rle_refl|]. @@ -3557,7 +3559,7 @@ assert (Hlx : bpow (mag x - 1) <= x < bpow (mag x)). apply Hex. now apply Rgt_not_eq. } unfold round_round_eq. -rewrite (round_N_small_pos beta fexp1 _ x (mag x)); [|exact Hlx|omega]. +rewrite (round_N_small_pos beta fexp1 _ x (mag x)); [|exact Hlx|lia]. set (x'' := round beta fexp2 (Znearest choice2) x). destruct (Req_dec x'' 0) as [Zx''|Nzx'']; [now rewrite Zx''; rewrite round_0; [|apply valid_rnd_N]|]. @@ -3566,7 +3568,7 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)). destruct (Rlt_or_le x'' (bpow (mag x))). + (* x'' < bpow (mag x) *) rewrite (round_N_small_pos beta fexp1 _ _ (mag x)); - [reflexivity|split; [|exact H0]|omega]. + [reflexivity|split; [|exact H0]|lia]. apply round_large_pos_ge_bpow; [now apply valid_rnd_N| |now apply Hlx]. fold x''; assert (0 <= x''); [|lra]; unfold x''. rewrite <- (round_0 beta fexp2 (Znearest choice2)). @@ -3581,7 +3583,7 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)). unfold round, F2R, scaled_mantissa, cexp; simpl. rewrite mag_bpow. assert (Hf11 : (fexp1 (mag x + 1) = fexp1 (mag x) :> Z)%Z); - [apply Vfexp1; omega|]. + [apply Vfexp1; lia|]. rewrite Hf11. apply (Rmult_eq_reg_r (bpow (- fexp1 (mag x)))); [|now apply Rgt_not_eq; apply bpow_gt_0]. @@ -3590,7 +3592,7 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)). apply Znearest_imp. simpl; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. rewrite Rabs_right; [|now apply Rle_ge; apply bpow_ge_0]. - apply Rle_lt_trans with (bpow (- 2)); [now apply bpow_le; omega|]. + apply Rle_lt_trans with (bpow (- 2)); [now apply bpow_le; lia|]. unfold Raux.bpow, Z.pow_pos; simpl; rewrite Zmult_1_r. assert (Hbeta : (2 <= beta)%Z). { destruct beta as (beta_val,beta_prop); simpl. @@ -3598,11 +3600,11 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)). apply Rinv_lt_contravar. * apply Rmult_lt_0_compat; [lra|]. rewrite mult_IZR; apply Rmult_lt_0_compat; - apply IZR_lt; omega. + apply IZR_lt; lia. * apply IZR_lt. apply (Z.le_lt_trans _ _ _ Hbeta). rewrite <- (Zmult_1_r beta) at 1. - apply Zmult_lt_compat_l; omega. + apply Zmult_lt_compat_l; lia. - (* mag x < fexp2 (mag x) *) casetype False; apply Nzx''. now apply (round_N_small_pos beta _ _ _ (mag x)). @@ -3630,11 +3632,11 @@ assert (Hlx : bpow (mag x - 1) <= x < bpow (mag x)). apply Hex. now apply Rgt_not_eq. } rewrite (round_N_small_pos beta fexp1 choice1 x (mag x)); - [|exact Hlx|omega]. + [|exact Hlx|lia]. destruct (Req_dec x'' 0) as [Zx''|Nzx'']; [now rewrite Zx''; rewrite round_0; [reflexivity|apply valid_rnd_N]|]. rewrite (round_N_small_pos beta _ _ x'' (mag x)); - [reflexivity| |omega]. + [reflexivity| |lia]. split. - apply round_large_pos_ge_bpow. + now apply valid_rnd_N. @@ -3680,19 +3682,19 @@ set (u2 := ulp beta fexp2 x). intros Cz Clt Ceq Cgt. destruct (Ztrichotomy (mag x) (fexp1 (mag x) - 1)) as [Hlt|[Heq|Hgt]]. - (* mag x < fexp1 (mag x) - 1 *) - assert (H : (mag x <= fexp1 (mag x) - 2)%Z) by omega. + assert (H : (mag x <= fexp1 (mag x) - 2)%Z) by lia. now apply round_round_really_zero. - (* mag x = fexp1 (mag x) - 1 *) - assert (H : (fexp1 (mag x) = (mag x + 1))%Z) by omega. + assert (H : (fexp1 (mag x) = (mag x + 1))%Z) by lia. destruct (Rlt_or_le x (bpow (mag x) - / 2 * u2)) as [Hlt'|Hge']. + now apply round_round_zero. + now apply Cz. - (* mag x > fexp1 (mag x) - 1 *) - assert (H : (fexp1 (mag x) <= mag x)%Z) by omega. + assert (H : (fexp1 (mag x) <= mag x)%Z) by lia. destruct (Rtotal_order x (midp fexp1 x)) as [Hlt'|[Heq'|Hgt']]. + (* x < midp fexp1 x *) destruct (Rlt_or_le x (midp fexp1 x - / 2 * u2)) as [Hlt''|Hle'']. - * now apply round_round_lt_mid_further_place; [| | |omega| |]. + * now apply round_round_lt_mid_further_place; [| | |lia| |]. * now apply Clt; [|split]. + (* x = midp fexp1 x *) now apply Ceq. @@ -3703,12 +3705,11 @@ destruct (Ztrichotomy (mag x) (fexp1 (mag x) - 1)) as [Hlt|[Heq|Hgt]]. - (* generic_format beta fexp1 x *) unfold round_round_eq; rewrite (round_generic beta fexp2); [reflexivity|now apply valid_rnd_N|]. - now apply (generic_inclusion_mag beta fexp1); [omega|]. + now apply (generic_inclusion_mag beta fexp1); [lia|]. - (* ~ generic_format beta fexp1 x *) assert (Hceil : round beta fexp1 Zceil x = x' + u1); [now apply round_UP_DN_ulp|]. - assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z); - [omega|]. + assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia. assert (midp' fexp1 x + / 2 * ulp beta fexp2 x < x); [|now apply round_round_gt_mid_further_place]. revert Hle''; unfold midp, midp'; fold x'. @@ -3724,7 +3725,7 @@ Lemma mag_div_disj : Proof. intros x y Px Py. generalize (mag_div beta x y (Rgt_not_eq _ _ Px) (Rgt_not_eq _ _ Py)). -omega. +lia. Qed. Definition round_round_div_hyp fexp1 fexp2 := @@ -3829,7 +3830,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y) replace (_ - _ + 1)%Z with ((mag x + 1) - mag y)%Z by ring. apply Hexp. { now assert (fexp1 (mag x + 1) <= mag x)%Z; - [apply valid_exp|omega]. } + [apply valid_exp|lia]. } { assumption. } replace (_ + 1 - _)%Z with (mag x - mag y + 1)%Z by ring. now rewrite <- Hxy. @@ -3842,7 +3843,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y) bpow_simplify. rewrite (Rmult_comm p). unfold p; bpow_simplify. - rewrite <- IZR_Zpower; [|omega]. + rewrite <- IZR_Zpower; [|lia]. rewrite <- mult_IZR. rewrite <- minus_IZR. apply IZR_le. @@ -3850,7 +3851,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y) apply Zlt_le_succ. apply lt_IZR. rewrite mult_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|bpow_simplify]. rewrite <- Fx. @@ -4000,7 +4001,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) replace (_ - _ + 1)%Z with ((mag x + 1) - mag y)%Z by ring. apply Hexp. { now assert (fexp1 (mag x + 1) <= mag x)%Z; - [apply valid_exp|omega]. } + [apply valid_exp|lia]. } { assumption. } replace (_ + 1 - _)%Z with (mag x - mag y + 1)%Z by ring. now rewrite <- Hxy. @@ -4016,7 +4017,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) rewrite (Rmult_comm u1). unfold x', u1, round, F2R, ulp, scaled_mantissa, cexp; simpl. bpow_simplify. - rewrite <- (IZR_Zpower _ (_ - _)%Z); [|omega]. + rewrite <- (IZR_Zpower _ (_ - _)%Z); [|lia]. do 5 rewrite <- mult_IZR. rewrite <- plus_IZR. rewrite <- minus_IZR. @@ -4026,7 +4027,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) apply lt_IZR. rewrite plus_IZR. do 5 rewrite mult_IZR; simpl. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_assoc. @@ -4063,7 +4064,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) apply (Zplus_le_reg_r _ _ (- mag y)); ring_simplify. rewrite (Zplus_comm (- _)). destruct (mag_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; - apply Hexp; try assumption; rewrite <- Hxy; omega. + apply Hexp; try assumption; rewrite <- Hxy; lia. Qed. Lemma round_round_div_aux2 : @@ -4139,7 +4140,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) replace (_ - _ + 1)%Z with ((mag x + 1) - mag y)%Z by ring. apply Hexp. { now assert (fexp1 (mag x + 1) <= mag x)%Z; - [apply valid_exp|omega]. } + [apply valid_exp|lia]. } { assumption. } replace (_ + 1 - _)%Z with (mag x - mag y + 1)%Z by ring. now rewrite <- Hxy. @@ -4213,7 +4214,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) apply (Zplus_le_reg_r _ _ (- mag y)); ring_simplify. rewrite (Zplus_comm (- _)). destruct (mag_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; - apply Hexp; try assumption; rewrite <- Hxy; omega. + apply Hexp; try assumption; rewrite <- Hxy; lia. + apply Rge_le; rewrite Fx at 1; apply Rle_ge. rewrite Fy at 1 2. apply (Rmult_le_reg_r (bpow (- fexp1 (mag x)))); @@ -4225,7 +4226,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) rewrite (Rmult_comm u1). unfold x', u1, round, F2R, ulp, scaled_mantissa, cexp; simpl. bpow_simplify. - rewrite <- (IZR_Zpower _ (_ - _)%Z); [|omega]. + rewrite <- (IZR_Zpower _ (_ - _)%Z); [|lia]. do 5 rewrite <- mult_IZR. do 2 rewrite <- plus_IZR. apply IZR_le. @@ -4233,7 +4234,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) apply lt_IZR. rewrite plus_IZR. do 5 rewrite mult_IZR; simpl. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite (Rmult_assoc _ (IZR mx)). @@ -4379,8 +4380,8 @@ intros Hprec. unfold Prec_gt_0 in prec_gt_0_. unfold FLX_exp. unfold round_round_div_hyp. -split; [now intro ex; omega|]. -split; [|split; [|split]]; intros ex ey; omega. +split; [now intro ex; lia|]. +split; [|split; [|split]]; intros ex ey; lia. Qed. Theorem round_round_div_FLX : @@ -4425,27 +4426,27 @@ unfold round_round_div_hyp. split; [intro ex|split; [|split; [|split]]; intros ex ey]. - generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ex - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ey - prec) emin). generalize (Zmax_spec (ex - ey - prec) emin). generalize (Zmax_spec (ex - ey - prec') emin'). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ey - prec) emin). generalize (Zmax_spec (ex - ey + 1 - prec) emin). generalize (Zmax_spec (ex - ey + 1 - prec') emin'). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ey - prec) emin). generalize (Zmax_spec (ex - ey - prec) emin). generalize (Zmax_spec (ex - ey - prec') emin'). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ey - prec) emin). generalize (Zmax_spec (ex - ey - prec) emin). generalize (Zmax_spec (ex - ey - prec') emin'). - omega. + lia. Qed. Theorem round_round_div_FLT : @@ -4493,27 +4494,27 @@ unfold round_round_div_hyp. split; [intro ex|split; [|split; [|split]]; intros ex ey]. - destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec') emin'); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey + 1 - prec) emin); destruct (Z.ltb_spec (ex - ey + 1 - prec') emin'); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec') emin'); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec') emin'); - omega. + lia. Qed. Theorem round_round_div_FTZ : diff --git a/flocq/Prop/Mult_error.v b/flocq/Prop/Mult_error.v index 57a3856f..f4467025 100644 --- a/flocq/Prop/Mult_error.v +++ b/flocq/Prop/Mult_error.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * Error of the multiplication is in the FLX/FLT format *) + +From Coq Require Import Lia. Require Import Core Operations Plus_error. Section Fprop_mult_error. @@ -71,7 +73,7 @@ unfold cexp, FLX_exp. rewrite mag_unique with (1 := Hex). rewrite mag_unique with (1 := Hey). rewrite mag_unique with (1 := Hexy). -cut (exy - 1 < ex + ey)%Z. omega. +cut (exy - 1 < ex + ey)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1 := proj1 Hexy). rewrite Rabs_mult. @@ -89,7 +91,7 @@ rewrite mag_unique with (1 := Hey). rewrite mag_unique with (1 := Hexy). cut ((ex - 1) + (ey - 1) < exy)%Z. generalize (prec_gt_0 prec). -clear ; omega. +clear ; lia. apply (lt_bpow beta). apply Rle_lt_trans with (2 := proj2 Hexy). rewrite Rabs_mult. @@ -163,7 +165,7 @@ apply (generic_format_F2R' _ _ _ f). { now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. } intro Nzmx; unfold mx, ex; rewrite <- Fx. unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx). -unfold FLX_exp; omega. +unfold FLX_exp; lia. Qed. End Fprop_mult_error. @@ -209,10 +211,10 @@ assumption. apply Rle_trans with (2:=Hxy). apply bpow_le. generalize (prec_gt_0 prec). -clear ; omega. +clear ; lia. rewrite <- (round_FLT_FLX beta emin) in H1. 2:apply Rle_trans with (2:=Hxy). -2:apply bpow_le ; generalize (prec_gt_0 prec) ; clear ; omega. +2:apply bpow_le ; generalize (prec_gt_0 prec) ; clear ; lia. unfold f; rewrite <- H1. apply generic_format_F2R. intros _. @@ -242,7 +244,7 @@ specialize (Ex Hx0). destruct (mag beta y) as (ey,Ey) ; simpl. specialize (Ey Hy0). assert (emin + 2 * prec -1 < ex + ey)%Z. -2: omega. +2: lia. apply (lt_bpow beta). apply Rle_lt_trans with (1:=Hxy). rewrite Rabs_mult, bpow_plus. @@ -262,7 +264,7 @@ intros Hy _. rewrite <- (Rmult_1_l (bpow _)) at 1. apply Rmult_le_compat_r. apply bpow_ge_0. -apply IZR_le; omega. +apply IZR_le; lia. intros H1 H2; contradict H2. replace ny with 0%Z. simpl; ring. @@ -296,7 +298,7 @@ destruct (mag beta x) as (ex,Hx). destruct (mag beta y) as (ey,Hy). simpl; apply Z.le_trans with ((ex-prec)+(ey-prec))%Z. 2: apply Zplus_le_compat; apply Z.le_max_l. -assert (e + 2*prec -1< ex+ey)%Z;[idtac|omega]. +assert (e + 2*prec -1< ex+ey)%Z;[idtac|lia]. apply lt_bpow with beta. apply Rle_lt_trans with (1:=H1). rewrite Rabs_mult, bpow_plus. @@ -327,9 +329,30 @@ apply (generic_format_F2R' _ _ _ f). { now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. } intro Nzmx; unfold mx, ex; rewrite <- Fx. unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx). -unfold FLT_exp; rewrite Z.max_l; [|omega]; rewrite <- Z.add_max_distr_r. -set (n := (_ - _ + _)%Z); apply (Z.le_trans _ n); [unfold n; omega|]. +unfold FLT_exp; rewrite Z.max_l; [|lia]; rewrite <- Z.add_max_distr_r. +set (n := (_ - _ + _)%Z); apply (Z.le_trans _ n); [unfold n; lia|]. apply Z.le_max_l. Qed. +Lemma mult_bpow_pos_exact_FLT : + forall x e, + format x -> + (0 <= e)%Z -> + format (x * bpow e)%R. +Proof. +intros x e Fx He. +destruct (Req_dec x 0) as [Zx|Nzx]. +{ rewrite Zx, Rmult_0_l; apply generic_format_0. } +rewrite Fx. +set (mx := Ztrunc _); set (ex := cexp _). +pose (f := {| Fnum := mx; Fexp := ex + e |} : float beta). +apply (generic_format_F2R' _ _ _ f). +{ now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. } +intro Nzmx; unfold mx, ex; rewrite <- Fx. +unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx). +unfold FLT_exp; rewrite <-Z.add_max_distr_r. +replace (_ - _ + e)%Z with (mag beta x + e - prec)%Z; [ |ring]. +apply Z.max_le_compat_l; lia. +Qed. + End Fprop_mult_error_FLT. diff --git a/flocq/Prop/Plus_error.v b/flocq/Prop/Plus_error.v index 42f80093..514d3aab 100644 --- a/flocq/Prop/Plus_error.v +++ b/flocq/Prop/Plus_error.v @@ -50,19 +50,19 @@ destruct (Zle_or_lt e' e) as [He|He]. exists m. unfold F2R at 2. simpl. rewrite Rmult_assoc, <- bpow_plus. -rewrite <- IZR_Zpower. 2: omega. +rewrite <- IZR_Zpower by lia. rewrite <- mult_IZR, Zrnd_IZR... unfold F2R. simpl. rewrite mult_IZR. rewrite Rmult_assoc. -rewrite IZR_Zpower. 2: omega. +rewrite IZR_Zpower by lia. rewrite <- bpow_plus. apply (f_equal (fun v => IZR m * bpow v)%R). ring. exists ((rnd (IZR m * bpow (e - e'))) * Zpower beta (e' - e))%Z. unfold F2R. simpl. rewrite mult_IZR. -rewrite IZR_Zpower. 2: omega. +rewrite IZR_Zpower by lia. rewrite 2!Rmult_assoc. rewrite <- 2!bpow_plus. apply (f_equal (fun v => _ * bpow v)%R). @@ -326,8 +326,7 @@ exists (Ztrunc (scaled_mantissa beta fexp x)*Zpower beta (cexp x -e))%Z. rewrite Fx at 1; unfold F2R; simpl. rewrite mult_IZR, Rmult_assoc. f_equal. -rewrite IZR_Zpower. -2: omega. +rewrite IZR_Zpower by lia. rewrite <- bpow_plus; f_equal; ring. Qed. @@ -351,7 +350,7 @@ case (Zle_or_lt (mag beta (x/IZR beta)) (mag beta y)); intros H1. pose (e:=cexp (x / IZR beta)). destruct (ex_shift x e) as (nx, Hnx); try exact Fx. apply monotone_exp. -rewrite <- (mag_minus1 x Zx); omega. +rewrite <- (mag_minus1 x Zx); lia. destruct (ex_shift y e) as (ny, Hny); try assumption. apply monotone_exp... destruct (round_repr_same_exp beta fexp rnd (nx+ny) e) as (n,Hn). @@ -406,11 +405,11 @@ apply V; left. apply lt_mag with beta. now apply Rabs_pos_lt. rewrite <- mag_minus1 in H1; try assumption. -rewrite 2!mag_abs; omega. +rewrite 2!mag_abs; lia. (* . *) destruct U as [U|U]. rewrite U; apply Z.le_trans with (mag beta x). -omega. +lia. rewrite <- mag_abs. apply mag_le. now apply Rabs_pos_lt. @@ -424,13 +423,13 @@ now apply Rabs_pos_lt. rewrite 2!mag_abs. assert (mag beta y < mag beta x - 1)%Z. now rewrite (mag_minus1 x Zx). -omega. +lia. apply cexp_round_ge... apply round_plus_neq_0... contradict H1; apply Zle_not_lt. rewrite <- (mag_minus1 x Zx). replace y with (-x)%R. -rewrite mag_opp; omega. +rewrite mag_opp; lia. lra. now exists n. Qed. @@ -520,7 +519,7 @@ rewrite <- mag_minus1; try assumption. unfold FLT_exp; apply bpow_le. apply Z.le_trans with (2:=Z.le_max_l _ _). destruct (mag beta x) as (n,Hn); simpl. -assert (e + prec < n)%Z; try omega. +assert (e + prec < n)%Z; try lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=He). now apply Hn. @@ -568,7 +567,7 @@ unfold cexp. rewrite <- mag_minus1 by easy. unfold FLX_exp; apply bpow_le. destruct (mag beta x) as (n,Hn); simpl. -assert (e + prec < n)%Z; try omega. +assert (e + prec < n)%Z; try lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=He). now apply Hn. diff --git a/flocq/Prop/Relative.v b/flocq/Prop/Relative.v index 5f87bd84..6b8e8f77 100644 --- a/flocq/Prop/Relative.v +++ b/flocq/Prop/Relative.v @@ -147,7 +147,7 @@ apply (lt_bpow beta). apply Rle_lt_trans with (2 := proj2 He). exact Hx. generalize (Hmin ex). -omega. +lia. apply Rmult_le_compat_l. apply bpow_ge_0. apply He. @@ -218,7 +218,7 @@ apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R. rewrite <- bpow_plus. apply bpow_le. generalize (Hmin ex). -omega. +lia. apply Rmult_le_compat_l. apply bpow_ge_0. generalize He. @@ -230,7 +230,7 @@ now apply round_le. apply generic_format_bpow. ring_simplify (ex - 1 + 1)%Z. generalize (Hmin ex). -omega. +lia. Qed. Theorem relative_error_round_F2R_emin : @@ -283,7 +283,7 @@ apply (lt_bpow beta). apply Rle_lt_trans with (2 := proj2 He). exact Hx. generalize (Hmin ex). -omega. +lia. apply Rmult_le_compat_l. apply bpow_ge_0. apply He. @@ -375,7 +375,7 @@ apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R. rewrite <- bpow_plus. apply bpow_le. generalize (Hmin ex). -omega. +lia. apply Rmult_le_compat_l. apply bpow_ge_0. generalize He. @@ -387,7 +387,7 @@ now apply round_le. apply generic_format_bpow. ring_simplify (ex - 1 + 1)%Z. generalize (Hmin ex). -omega. +lia. Qed. Theorem relative_error_N_round_F2R_emin : @@ -425,7 +425,7 @@ Lemma relative_error_FLX_aux : Proof. intros k. unfold FLX_exp. -omega. +lia. Qed. Variable rnd : R -> Z. @@ -505,7 +505,7 @@ Proof. unfold u_ro; apply (Rmult_lt_reg_l 2); [lra|]. rewrite <-Rmult_assoc, Rinv_r, Rmult_1_l, Rmult_1_r; [|lra]. apply (Rle_lt_trans _ (bpow 0)); - [apply bpow_le; omega|simpl; lra]. + [apply bpow_le; lia|simpl; lra]. Qed. Lemma u_rod1pu_ro_pos : (0 <= u_ro / (1 + u_ro))%R. @@ -659,7 +659,7 @@ Proof. intros k Hk. unfold FLT_exp. generalize (Zmax_spec (k - prec) emin). -omega. +lia. Qed. Variable rnd : R -> Z. @@ -843,7 +843,7 @@ destruct relative_error_N_ex with (FLT_exp emin prec) (emin+prec)%Z prec choice as (eps,(Heps1,Heps2)). now apply FLT_exp_valid. intros; unfold FLT_exp. -rewrite Zmax_left; omega. +lia. rewrite Rabs_right;[assumption|apply Rle_ge; now left]. exists eps; exists 0%R. split;[assumption|split]. @@ -869,14 +869,14 @@ rewrite ulp_neq_0. apply bpow_le. unfold FLT_exp, cexp. rewrite Zmax_right. -omega. +lia. destruct (mag beta x) as (e,He); simpl. assert (e-1 < emin+prec)%Z. apply (lt_bpow beta). apply Rle_lt_trans with (2:=Hx). rewrite <- (Rabs_pos_eq x) by now apply Rlt_le. now apply He, Rgt_not_eq. -omega. +lia. split ; ring. Qed. diff --git a/flocq/Prop/Round_odd.v b/flocq/Prop/Round_odd.v index df2952cc..a433c381 100644 --- a/flocq/Prop/Round_odd.v +++ b/flocq/Prop/Round_odd.v @@ -68,7 +68,7 @@ assert (H0:(Zfloor x <= Zfloor y)%Z) by now apply Zfloor_le. case (Zle_lt_or_eq _ _ H0); intros H1. apply Rle_trans with (1:=Zceil_ub _). rewrite Zceil_floor_neq. -apply IZR_le; omega. +apply IZR_le; lia. now apply sym_not_eq. contradict Hy2. rewrite <- H1, Hx2; discriminate. @@ -503,7 +503,7 @@ Proof. intros x Hx. apply generic_inclusion_mag with fexp; trivial; intros Hx2. generalize (fexpe_fexp (mag beta x)). -omega. +lia. Qed. @@ -525,7 +525,7 @@ rewrite Rmult_assoc, <- bpow_plus. rewrite <- Hg1; unfold F2R. apply f_equal, f_equal. ring. -omega. +lia. split; trivial. split. unfold canonical, cexp. @@ -536,7 +536,7 @@ rewrite Z.even_pow. rewrite Even_beta. apply Bool.orb_true_intro. now right. -omega. +lia. Qed. @@ -713,7 +713,7 @@ rewrite Zmult_1_r; apply Rinv_le. exact Rlt_0_2. apply IZR_le. specialize (radix_gt_1 beta). -omega. +lia. apply Rlt_le_trans with (bpow (fexp e)*1)%R. 2: right; ring. unfold Rdiv; apply Rmult_lt_compat_l. @@ -766,7 +766,7 @@ rewrite Zplus_comm; unfold Zminus; apply f_equal2. rewrite Fexp_Fplus. rewrite Z.min_l. now rewrite Fexp_d. -rewrite Hu'2; omega. +rewrite Hu'2; lia. Qed. Lemma m_eq_0: (0 = F2R d)%R -> exists f:float beta, @@ -797,7 +797,7 @@ Lemma fexp_m_eq_0: (0 = F2R d)%R -> Proof with auto with typeclass_instances. intros Y. assert ((fexp (mag beta (F2R u) - 1) <= fexp (mag beta (F2R u))))%Z. -2: omega. +2: lia. destruct (mag beta x) as (e,He). rewrite Rabs_right in He. 2: now left. @@ -812,8 +812,8 @@ ring_simplify (fexp e + 1 - 1)%Z. replace (fexp (fexp e)) with (fexp e). case exists_NE_; intros V. contradict V; rewrite Even_beta; discriminate. -rewrite (proj2 (V e)); omega. -apply sym_eq, valid_exp; omega. +rewrite (proj2 (V e)); lia. +apply sym_eq, valid_exp; lia. Qed. Lemma Fm: generic_format beta fexpe m. @@ -829,7 +829,7 @@ rewrite <- Fexp_d; trivial. rewrite Cd. unfold cexp. generalize (fexpe_fexp (mag beta (F2R d))). -omega. +lia. (* *) destruct m_eq_0 as (g,(Hg1,Hg2)); trivial. apply generic_format_F2R' with g. @@ -838,7 +838,7 @@ intros H; unfold cexp; rewrite Hg2. rewrite mag_m_0; try assumption. apply Z.le_trans with (1:=fexpe_fexp _). generalize (fexp_m_eq_0 Y). -omega. +lia. Qed. @@ -857,7 +857,7 @@ rewrite <- Fexp_d; trivial. rewrite Cd. unfold cexp. generalize (fexpe_fexp (mag beta (F2R d))). -omega. +lia. (* *) destruct m_eq_0 as (g,(Hg1,Hg2)); trivial. apply exists_even_fexp_lt. @@ -866,7 +866,7 @@ rewrite Hg2. rewrite mag_m_0; trivial. apply Z.le_lt_trans with (1:=fexpe_fexp _). generalize (fexp_m_eq_0 Y). -omega. +lia. Qed. @@ -952,7 +952,7 @@ eexists; split. apply sym_eq, Y. simpl; unfold cexp. apply Z.le_lt_trans with (1:=fexpe_fexp _). -omega. +lia. absurd (true=false). discriminate. rewrite <- Hk3, <- Hk'3. @@ -1105,14 +1105,14 @@ intros _; rewrite Zx, round_0... destruct (mag beta x) as (e,He); simpl; intros H. apply mag_unique; split. apply abs_round_ge_generic... -apply FLT_format_bpow... -auto with zarith. +apply generic_format_FLT_bpow... +now apply Z.lt_le_pred. now apply He. assert (V: (Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) <= bpow beta e)%R). apply abs_round_le_generic... -apply FLT_format_bpow... -auto with zarith. +apply generic_format_FLT_bpow... +now apply Zlt_le_weak. left; now apply He. case V; try easy; intros K. assert (H0:Rnd_odd_pt beta (FLT_exp emin prec) x (round beta (FLT_exp emin prec) Zrnd_odd x)). diff --git a/flocq/Prop/Sterbenz.v b/flocq/Prop/Sterbenz.v index 746b7026..9594ac5d 100644 --- a/flocq/Prop/Sterbenz.v +++ b/flocq/Prop/Sterbenz.v @@ -67,7 +67,7 @@ rewrite <- F2R_plus. apply generic_format_F2R. intros _. case_eq (Fplus fx fy). -intros mxy exy Pxy. +intros mxy exy Pxy; simpl. rewrite <- Pxy, F2R_plus, <- Hx, <- Hy. unfold cexp. replace exy with (fexp (Z.min ex ey)). diff --git a/flocq/Version.v b/flocq/Version.v index d0e36a57..aebb0d76 100644 --- a/flocq/Version.v +++ b/flocq/Version.v @@ -29,4 +29,4 @@ Definition Flocq_version := Eval vm_compute in parse t major (minor * 10 + N_of_ascii h - N_of_ascii "0"%char)%N | Empty_string => (major * 100 + minor)%N end in - parse "3.1.0"%string N0 N0. + parse "3.4.0"%string N0 N0. -- cgit