diff options
Diffstat (limited to 'flocq/Calc/Sqrt.v')
| -rw-r--r-- | flocq/Calc/Sqrt.v | 21 |
1 files changed, 11 insertions, 10 deletions
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. |