diff options
Diffstat (limited to 'flocq/Prop')
-rw-r--r-- | flocq/Prop/Div_sqrt_error.v | 3 | ||||
-rw-r--r-- | flocq/Prop/Double_rounding.v | 65 | ||||
-rw-r--r-- | flocq/Prop/Mult_error.v | 10 | ||||
-rw-r--r-- | flocq/Prop/Plus_error.v | 10 | ||||
-rw-r--r-- | flocq/Prop/Relative.v | 4 | ||||
-rw-r--r-- | flocq/Prop/Round_odd.v | 3 | ||||
-rw-r--r-- | flocq/Prop/Sterbenz.v | 4 |
7 files changed, 51 insertions, 48 deletions
diff --git a/flocq/Prop/Div_sqrt_error.v b/flocq/Prop/Div_sqrt_error.v index 9aa9c508..49c46b7e 100644 --- a/flocq/Prop/Div_sqrt_error.v +++ b/flocq/Prop/Div_sqrt_error.v @@ -19,7 +19,8 @@ COPYING file for more details. (** * Remainder of the division and square root are in the FLX format *) -Require Import Psatz. +From Coq Require Import ZArith Reals Psatz. + Require Import Core Operations Relative Sterbenz Mult_error. Section Fprop_divsqrt_error. diff --git a/flocq/Prop/Double_rounding.v b/flocq/Prop/Double_rounding.v index 3e942fe0..0580ab5e 100644 --- a/flocq/Prop/Double_rounding.v +++ b/flocq/Prop/Double_rounding.v @@ -21,8 +21,9 @@ COPYING file for more details. (** * Conditions for innocuous double rounding. *) -Require Import Psatz. -Require Import Raux Defs Generic_fmt Operations Ulp FLX FLT FTZ. +From Coq Require Import ZArith Reals Psatz. + +Require Import Core FTZ. Open Scope R_scope. @@ -460,11 +461,11 @@ assert (Hx''pow : x'' = bpow (mag x)). unfold x'', round, F2R, scaled_mantissa, cexp; simpl. apply (Rmult_le_reg_r (bpow (- fexp2 (mag x)))); [now apply bpow_gt_0|]. bpow_simplify. - rewrite <- (IZR_Zpower _ (_ - _)); [|lia]. + rewrite <- (IZR_Zpower _ (_ - _)) by lia. apply IZR_le. apply Zlt_succ_le; unfold Z.succ. apply lt_IZR. - rewrite plus_IZR; rewrite IZR_Zpower; [|lia]. + rewrite plus_IZR; rewrite IZR_Zpower by lia. apply (Rmult_lt_reg_r (bpow (fexp2 (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_plus_distr_r; rewrite Rmult_1_l. bpow_simplify. @@ -487,7 +488,7 @@ unfold round, F2R, scaled_mantissa, cexp; simpl. assert (Hf : (0 <= mag x - fexp1 (mag x''))%Z). { rewrite Hx''pow. rewrite mag_bpow. - assert (fexp1 (mag x + 1) <= mag x)%Z; [|lia]. + cut (fexp1 (mag x + 1) <= mag x)%Z. lia. destruct (Zle_or_lt (mag x) (fexp1 (mag x))) as [Hle|Hlt]; [|now apply Vfexp1]. assert (H : (mag x = fexp1 (mag x) :> Z)%Z); @@ -496,10 +497,10 @@ assert (Hf : (0 <= mag x - fexp1 (mag x''))%Z). now apply Vfexp1. } rewrite (Znearest_imp _ _ (beta ^ (mag x - fexp1 (mag x'')))%Z). - rewrite (Znearest_imp _ _ (beta ^ (mag x - fexp1 (mag x)))%Z). - + rewrite IZR_Zpower; [|exact Hf]. - rewrite IZR_Zpower; [|lia]. + + rewrite IZR_Zpower by exact Hf. + rewrite IZR_Zpower by lia. now bpow_simplify. - + rewrite IZR_Zpower; [|lia]. + + rewrite IZR_Zpower by lia. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; [|now apply Rle_ge; apply bpow_ge_0]. @@ -831,7 +832,7 @@ split. apply succ_le_lt; [apply Vfexp|idtac|exact Fx|assumption]. apply (generic_format_bpow beta fexp (mag x - 1)). replace (_ + _)%Z with (mag x : Z) by ring. - assert (fexp (mag x) < mag x)%Z; [|lia]. + cut (fexp (mag x) < mag x)%Z. lia. now apply mag_generic_gt; [|now apply Rgt_not_eq|]. - rewrite Rabs_right. + apply Rlt_trans with x. @@ -884,7 +885,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. rewrite Rmult_plus_distr_r. rewrite <- Fx. rewrite mult_IZR. - rewrite IZR_Zpower; [|lia]. + rewrite IZR_Zpower by lia. bpow_simplify. now rewrite <- Fy. } apply generic_format_F2R' with (f := fxy); [now rewrite Hxy|]. @@ -1053,7 +1054,7 @@ apply round_round_lt_mid. - lra. - now rewrite Lxy. - rewrite Lxy. - assert (fexp1 (mag x) < mag x)%Z; [|lia]. + cut (fexp1 (mag x) < mag x)%Z. lia. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - unfold midp. apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))). @@ -1198,8 +1199,7 @@ assert (Lyx : (mag y <= mag x)%Z); [now apply mag_le; [|apply Rlt_le]|]. destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge]. - (* mag x - 2 < mag y *) - assert (Hor : (mag y = mag x :> Z) - \/ (mag y = mag x - 1 :> Z)%Z) by lia. + assert (Hor : (mag y = mag x :> Z) \/ (mag y = mag x - 1 :> Z)%Z) by lia. destruct Hor as [Heq|Heqm1]. + (* mag y = mag x *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. @@ -1344,10 +1344,10 @@ destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx]. apply (Rmult_le_reg_r (bpow (- fexp (mag x - 1)%Z))); [now apply bpow_gt_0|]. bpow_simplify. - rewrite <- (IZR_Zpower beta (_ - _ - _)); [|lia]. + rewrite <- (IZR_Zpower beta (_ - _ - _)) by lia. apply IZR_le. apply Zceil_glb. - rewrite IZR_Zpower; [|lia]. + rewrite IZR_Zpower by lia. rewrite Xpow at 1. rewrite Rmult_minus_distr_r. bpow_simplify. @@ -1402,7 +1402,7 @@ apply round_round_gt_mid. - exact Vfexp2. - lra. - apply Hexp4; lia. -- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|lia]. +- cut (fexp1 (mag (x - y)) < mag (x - y))%Z. lia. apply (valid_exp_large fexp1 (mag x - 1)). + apply (valid_exp_large fexp1 (mag y)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. @@ -1880,7 +1880,7 @@ apply round_round_lt_mid. - lra. - now rewrite Lxy. - rewrite Lxy. - assert (fexp1 (mag x) < mag x)%Z; [|lia]. + cut (fexp1 (mag x) < mag x)%Z. lia. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - unfold midp. apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))). @@ -2008,8 +2008,7 @@ assert (Lyx : (mag y <= mag x)%Z); [now apply mag_le; [|apply Rlt_le]|]. destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge]. - (* mag x - 2 < mag y *) - assert (Hor : (mag y = mag x :> Z) - \/ (mag y = mag x - 1 :> Z)%Z) by lia. + assert (Hor : (mag y = mag x :> Z) \/ (mag y = mag x - 1 :> Z)%Z) by lia. destruct Hor as [Heq|Heqm1]. + (* mag y = mag x *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. @@ -2114,7 +2113,7 @@ apply round_round_gt_mid. - exact Vfexp2. - lra. - apply Hexp4; lia. -- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|lia]. +- cut (fexp1 (mag (x - y)) < mag (x - y))%Z. lia. apply (valid_exp_large fexp1 (mag x - 1)). + apply (valid_exp_large fexp1 (mag y)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. @@ -2744,11 +2743,11 @@ destruct (Req_dec a 0) as [Za|Nza]. apply (Rmult_le_reg_r (bpow (- 2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite Fx at 1; bpow_simplify. - rewrite <- IZR_Zpower; [|lia]. + rewrite <- IZR_Zpower by lia. rewrite <- plus_IZR, <- 2!mult_IZR. apply IZR_le, Zlt_succ_le, lt_IZR. unfold Z.succ; rewrite plus_IZR; do 2 rewrite mult_IZR; rewrite plus_IZR. - rewrite IZR_Zpower; [|lia]. + rewrite IZR_Zpower by lia. apply (Rmult_lt_reg_r (bpow (2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite <- Fx. @@ -3163,11 +3162,11 @@ destruct (Req_dec a 0) as [Za|Nza]. apply (Rmult_le_reg_r (bpow (- 2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite Fx at 1; bpow_simplify. - rewrite <- IZR_Zpower; [|lia]. + rewrite <- IZR_Zpower by lia. rewrite <- plus_IZR, <- 2!mult_IZR. apply IZR_le, Zlt_succ_le, lt_IZR. unfold Z.succ; rewrite plus_IZR; do 2 rewrite mult_IZR; rewrite plus_IZR. - rewrite IZR_Zpower; [|lia]. + rewrite IZR_Zpower by lia. apply (Rmult_lt_reg_r (bpow (2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite <- Fx. @@ -3481,7 +3480,7 @@ assert (Hf : F2R f = x). rewrite plus_IZR. rewrite Rmult_plus_distr_r. rewrite mult_IZR. - rewrite IZR_Zpower; [|lia]. + rewrite IZR_Zpower by lia. unfold cexp at 2; bpow_simplify. unfold Zminus; rewrite bpow_plus. rewrite (Rmult_comm _ (bpow (- 1))). @@ -3527,12 +3526,12 @@ assert (Hf : F2R f = x). unfold round, F2R, scaled_mantissa, cexp; simpl. bpow_simplify. rewrite Lrd. - rewrite <- (IZR_Zpower _ (_ - _)); [|lia]. + rewrite <- (IZR_Zpower _ (_ - _)) by lia. rewrite <- mult_IZR. rewrite (Zfloor_imp (Zfloor (x * bpow (- fexp1 (mag x))) * beta ^ (fexp1 (mag x) - fexp2 (mag x)))). + rewrite mult_IZR. - rewrite IZR_Zpower; [|lia]. + rewrite IZR_Zpower by lia. bpow_simplify. now unfold rd. + split; [now apply Rle_refl|]. @@ -3843,7 +3842,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y) bpow_simplify. rewrite (Rmult_comm p). unfold p; bpow_simplify. - rewrite <- IZR_Zpower; [|lia]. + rewrite <- IZR_Zpower by lia. rewrite <- mult_IZR. rewrite <- minus_IZR. apply IZR_le. @@ -3851,7 +3850,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y) apply Zlt_le_succ. apply lt_IZR. rewrite mult_IZR. - rewrite IZR_Zpower; [|lia]. + rewrite IZR_Zpower by lia. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|bpow_simplify]. rewrite <- Fx. @@ -4017,7 +4016,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) rewrite (Rmult_comm u1). unfold x', u1, round, F2R, ulp, scaled_mantissa, cexp; simpl. bpow_simplify. - rewrite <- (IZR_Zpower _ (_ - _)%Z); [|lia]. + rewrite <- (IZR_Zpower _ (_ - _)%Z) by lia. do 5 rewrite <- mult_IZR. rewrite <- plus_IZR. rewrite <- minus_IZR. @@ -4027,7 +4026,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) apply lt_IZR. rewrite plus_IZR. do 5 rewrite mult_IZR; simpl. - rewrite IZR_Zpower; [|lia]. + rewrite IZR_Zpower by lia. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_assoc. @@ -4226,7 +4225,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) rewrite (Rmult_comm u1). unfold x', u1, round, F2R, ulp, scaled_mantissa, cexp; simpl. bpow_simplify. - rewrite <- (IZR_Zpower _ (_ - _)%Z); [|lia]. + rewrite <- (IZR_Zpower _ (_ - _)%Z) by lia. do 5 rewrite <- mult_IZR. do 2 rewrite <- plus_IZR. apply IZR_le. @@ -4234,7 +4233,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) apply lt_IZR. rewrite plus_IZR. do 5 rewrite mult_IZR; simpl. - rewrite IZR_Zpower; [|lia]. + rewrite IZR_Zpower by lia. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite (Rmult_assoc _ (IZR mx)). diff --git a/flocq/Prop/Mult_error.v b/flocq/Prop/Mult_error.v index f4467025..ce909350 100644 --- a/flocq/Prop/Mult_error.v +++ b/flocq/Prop/Mult_error.v @@ -19,7 +19,8 @@ COPYING file for more details. (** * Error of the multiplication is in the FLX/FLT format *) -From Coq Require Import Lia. +From Coq Require Import ZArith Reals Lia. + Require Import Core Operations Plus_error. Section Fprop_mult_error. @@ -243,8 +244,7 @@ destruct (mag beta x) as (ex,Ex) ; simpl. specialize (Ex Hx0). destruct (mag beta y) as (ey,Ey) ; simpl. specialize (Ey Hy0). -assert (emin + 2 * prec -1 < ex + ey)%Z. -2: lia. +cut (emin + 2 * prec -1 < ex + ey)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1:=Hxy). rewrite Rabs_mult, bpow_plus. @@ -298,7 +298,7 @@ destruct (mag beta x) as (ex,Hx). destruct (mag beta y) as (ey,Hy). simpl; apply Z.le_trans with ((ex-prec)+(ey-prec))%Z. 2: apply Zplus_le_compat; apply Z.le_max_l. -assert (e + 2*prec -1< ex+ey)%Z;[idtac|lia]. +cut (e + 2*prec -1< ex+ey)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=H1). rewrite Rabs_mult, bpow_plus. @@ -329,7 +329,7 @@ apply (generic_format_F2R' _ _ _ f). { now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. } intro Nzmx; unfold mx, ex; rewrite <- Fx. unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx). -unfold FLT_exp; rewrite Z.max_l; [|lia]; rewrite <- Z.add_max_distr_r. +unfold FLT_exp; rewrite Z.max_l by lia; rewrite <- Z.add_max_distr_r. set (n := (_ - _ + _)%Z); apply (Z.le_trans _ n); [unfold n; lia|]. apply Z.le_max_l. Qed. diff --git a/flocq/Prop/Plus_error.v b/flocq/Prop/Plus_error.v index 514d3aab..bf0b28cd 100644 --- a/flocq/Prop/Plus_error.v +++ b/flocq/Prop/Plus_error.v @@ -19,11 +19,9 @@ COPYING file for more details. (** * Error of the rounded-to-nearest addition is representable. *) -Require Import Psatz. -Require Import Raux Defs Float_prop Generic_fmt. -Require Import FIX FLX FLT Ulp Operations. -Require Import Relative. +From Coq Require Import ZArith Reals Psatz. +Require Import Core Operations Relative. Section Fprop_plus_error. @@ -519,7 +517,7 @@ rewrite <- mag_minus1; try assumption. unfold FLT_exp; apply bpow_le. apply Z.le_trans with (2:=Z.le_max_l _ _). destruct (mag beta x) as (n,Hn); simpl. -assert (e + prec < n)%Z; try lia. +cut (e + prec < n)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=He). now apply Hn. @@ -567,7 +565,7 @@ unfold cexp. rewrite <- mag_minus1 by easy. unfold FLX_exp; apply bpow_le. destruct (mag beta x) as (n,Hn); simpl. -assert (e + prec < n)%Z; try lia. +cut (e + prec < n)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=He). now apply Hn. diff --git a/flocq/Prop/Relative.v b/flocq/Prop/Relative.v index 6b8e8f77..a87e5666 100644 --- a/flocq/Prop/Relative.v +++ b/flocq/Prop/Relative.v @@ -18,8 +18,10 @@ COPYING file for more details. *) (** * Relative error of the roundings *) + +From Coq Require Import ZArith Reals Psatz. + Require Import Core. -Require Import Psatz. (* for lra *) Section Fprop_relative. diff --git a/flocq/Prop/Round_odd.v b/flocq/Prop/Round_odd.v index a433c381..a7d98eb4 100644 --- a/flocq/Prop/Round_odd.v +++ b/flocq/Prop/Round_odd.v @@ -20,7 +20,8 @@ COPYING file for more details. (** * Rounding to odd and its properties, including the equivalence between rnd_NE and double rounding with rnd_odd and then rnd_NE *) -Require Import Reals Psatz. +From Coq Require Import ZArith Reals Psatz. + Require Import Core Operations. Definition Zrnd_odd x := match Req_EM_T x (IZR (Zfloor x)) with diff --git a/flocq/Prop/Sterbenz.v b/flocq/Prop/Sterbenz.v index 9594ac5d..8f516d0e 100644 --- a/flocq/Prop/Sterbenz.v +++ b/flocq/Prop/Sterbenz.v @@ -19,7 +19,9 @@ COPYING file for more details. (** * Sterbenz conditions for exact subtraction *) -Require Import Raux Defs Generic_fmt Operations. +From Coq Require Import ZArith Reals. + +Require Import Zaux Raux Defs Generic_fmt Operations. Section Fprop_Sterbenz. |