diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2020-12-28 15:53:36 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-28 15:53:36 +0100 |
commit | d4513f41c54869c9b4ba96ab79d50933a1d5c25a (patch) | |
tree | b5ef5b74c19f386791d1f572c45b6b7af0e90451 /flocq/Calc/Sqrt.v | |
parent | 548e62be073aa5a7b39d5826cd72681daef7c6a1 (diff) | |
download | compcert-kvx-d4513f41c54869c9b4ba96ab79d50933a1d5c25a.tar.gz compcert-kvx-d4513f41c54869c9b4ba96ab79d50933a1d5c25a.zip |
Update Flocq to 3.4.0 (#383)
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. |