From d4513f41c54869c9b4ba96ab79d50933a1d5c25a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 28 Dec 2020 15:53:36 +0100
Subject: Update Flocq to 3.4.0 (#383)

---
 flocq/Calc/Sqrt.v | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

(limited to 'flocq/Calc/Sqrt.v')

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