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 +++++++++++---------- 5 files changed, 55 insertions(+), 46 deletions(-) (limited to 'flocq/Calc') 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. -- cgit