Update Flocq to 3.4.0 (#383)

5 files changed, 55 insertions, 46 deletions

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.