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/Core/Raux.v | 32 ++++++++++++++++++++++---------- 1 file changed, 22 insertions(+), 10 deletions(-) (limited to 'flocq/Core/Raux.v') diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v index 8273a55b..58d1a630 100644 --- a/flocq/Core/Raux.v +++ b/flocq/Core/Raux.v @@ -907,6 +907,18 @@ rewrite Ropp_involutive. apply Zfloor_lb. Qed. +Theorem Zceil_lb : + forall x : R, + (IZR (Zceil x) < x + 1)%R. +Proof. +intros x. +unfold Zceil. +rewrite opp_IZR. +rewrite <-(Ropp_involutive (x + 1)), Ropp_plus_distr. +apply Ropp_lt_contravar, (Rplus_lt_reg_r 1); ring_simplify. +apply Zfloor_ub. +Qed. + Theorem Zceil_glb : forall n x, (x <= IZR n)%R -> @@ -1305,9 +1317,9 @@ rewrite Ropp_inv_permute with (1 := Zy'). rewrite <- 2!opp_IZR. rewrite <- Zmod_opp_opp. apply H. -clear -Hy. omega. +clear -Hy. lia. apply H. -clear -Zy Hy. omega. +clear -Zy Hy. lia. (* *) split. pattern (IZR (x / y)) at 1 ; rewrite <- Rplus_0_r. @@ -1454,7 +1466,7 @@ rewrite <- (Rmult_1_r (bpow e1)). rewrite bpow_plus. apply Rmult_lt_compat_l. apply bpow_gt_0. -assert (0 < e2 - e1)%Z by omega. +assert (0 < e2 - e1)%Z by lia. destruct (e2 - e1)%Z ; try discriminate H0. clear. rewrite <- IZR_Zpower by easy. @@ -1756,7 +1768,7 @@ rewrite Rabs_right in Hex; [|now apply Rle_ge; apply Rlt_le]. rewrite Rabs_right in Hey; [|now apply Rle_ge; apply Rlt_le]. apply (Rlt_le_trans _ _ _ Hex). apply Rle_trans with (bpow (ey - 1)); [|exact Hey]. -now apply bpow_le; omega. +now apply bpow_le; lia. Qed. Theorem mag_bpow : @@ -1900,7 +1912,7 @@ apply bpow_le. now apply Zlt_le_weak. apply IZR_le. clear -Zm. -zify ; omega. +zify ; lia. Qed. Lemma mag_mult : @@ -1999,7 +2011,7 @@ assert (Hbeta : (2 <= r)%Z). { destruct r as (beta_val,beta_prop). now apply Zle_bool_imp_le. } intros x y Px Py Hln. -assert (Oxy : (y < x)%R); [apply lt_mag;[assumption|omega]|]. +assert (Oxy : (y < x)%R); [apply lt_mag;[assumption|lia]|]. destruct (mag x) as (ex,Hex). destruct (mag y) as (ey,Hey). simpl in Hln |- *. @@ -2096,7 +2108,7 @@ split. unfold Rsqr ; rewrite <- bpow_plus. apply bpow_le. generalize (Zdiv2_odd_eqn (e + 1)). - destruct Z.odd ; intros ; omega. + destruct Z.odd ; intros ; lia. - rewrite <- (Rabs_pos_eq (bpow _)) by apply bpow_ge_0. apply Rsqr_lt_abs_0. rewrite Rsqr_sqrt by now apply Rlt_le. @@ -2104,7 +2116,7 @@ split. unfold Rsqr ; rewrite <- bpow_plus. apply bpow_le. generalize (Zdiv2_odd_eqn (e + 1)). - destruct Z.odd ; intros ; omega. + destruct Z.odd ; intros ; lia. Qed. Lemma mag_1 : mag 1 = 1%Z :> Z. @@ -2324,7 +2336,7 @@ refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _). refine (H _ _ Py). apply INR_lt in Hy. clear -Hy HyN. - omega. + lia. now apply Rlt_le, Rinv_0_lt_compat. rewrite S_INR, HN. ring_simplify (IZR (up (/ l)) - 1 + 1)%R. @@ -2369,7 +2381,7 @@ rewrite <- (Z.opp_involutive n). rewrite <- (Z.abs_neq n). rewrite <- Zabs2Nat.id_abs. apply K. -omega. +lia. Qed. -- cgit From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- flocq/Core/Raux.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'flocq/Core/Raux.v') diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v index 58d1a630..455190dc 100644 --- a/flocq/Core/Raux.v +++ b/flocq/Core/Raux.v @@ -18,7 +18,7 @@ COPYING file for more details. *) (** * Missing definitions/lemmas *) -Require Import Psatz. +Require Export Psatz. Require Export Reals ZArith. Require Export Zaux. -- cgit