Commit 2ec532a8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Clean occurrences of IZR and friends.

parent 78e75ff1
......@@ -214,9 +214,8 @@ rewrite Rabs_mult.
pattern (Rabs u) at 1; rewrite <- (Rmult_1_l (Rabs u)).
apply Rmult_le_compat_r.
apply Rabs_pos.
change 2 with (IZR 2).
rewrite <- (abs_IZR 2).
now apply (IZR_le 1 2).
now apply IZR_le.
(* *)
rewrite cexp_FLT_FIX.
rewrite cexp_FLT_FIX; trivial.
......@@ -226,7 +225,7 @@ apply bpow_le; omega.
lra.
rewrite Rabs_mult.
rewrite Rabs_pos_eq.
2: now apply (IZR_le 0 2).
2: now apply IZR_le.
apply Rlt_le_trans with (2*bpow (emin + prec - 1)).
apply Rmult_lt_compat_l with (1 := Rlt_0_2).
assumption.
......@@ -1092,7 +1091,7 @@ apply Rle_lt_trans with (1*/2);[right; ring|idtac].
apply Rlt_le_trans with ((IZR z)*/2);[idtac|right; field].
apply Rmult_lt_compat_r.
lra.
now apply (IZR_lt 1).
now apply IZR_lt.
rewrite <- H2.
unfold Znearest; simpl.
replace (Zfloor (1 / 2)) with 0%Z.
......@@ -1369,9 +1368,9 @@ apply Rle_trans with (1*bpow emin).
right; ring.
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply (IZR_le 1 3).
now apply IZR_le.
apply Rmult_le_compat_l.
now apply (IZR_le 0 3).
now apply IZR_le.
rewrite ulp_neq_0.
2: apply Rmult_integral_contrapositive_currified.
2: apply Rgt_not_eq, bpow_gt_0.
......@@ -1405,9 +1404,9 @@ apply Rle_trans with (1*bpow emin).
right; ring.
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply (IZR_le 1 3).
now apply IZR_le.
apply Rmult_le_compat_l.
now apply (IZR_le 0 3).
now apply IZR_le.
rewrite ulp_neq_0.
2: apply Rmult_integral_contrapositive_currified.
2: apply Rgt_not_eq, bpow_gt_0.
......@@ -1503,7 +1502,7 @@ rewrite <- (Rmult_1_l (Rabs b)).
rewrite (T b).
apply Rmult_le_compat_r.
apply Rabs_pos.
now apply (IZR_le 1 2).
now apply IZR_le.
rewrite <- (T b).
rewrite <- ulp_abs.
apply FLT_ulp_le_id...
......@@ -1529,7 +1528,6 @@ rewrite (Rabs_right (bpow emin)).
apply Rmult_le_compat_r.
apply bpow_ge_0.
rewrite <- abs_IZR.
replace 1 with (IZR 1) by reflexivity.
apply IZR_le.
assert (0 < Z.abs n)%Z;[idtac|omega].
apply Z.abs_pos.
......@@ -1615,7 +1613,7 @@ replace (v-v) with 0 by ring.
rewrite Rabs_R0.
apply Rmult_le_pos.
apply Rmult_le_pos.
now apply (IZR_le 0 3).
now apply IZR_le.
lra.
apply ulp_ge_0.
Qed.
......
......@@ -92,7 +92,7 @@ apply Zfloor_imp.
rewrite plus_IZR.
simpl.
apply Rmult_le_lt_reg_l with b.
apply (IZR_lt 0) ; lia.
apply IZR_lt ; lia.
apply Rplus_le_lt_reg_r with (-a).
replace (b * (a / b)%Z + - a) with (-(a - (a / b)%Z * b)) by ring.
replace (b * ((a / b)%Z + 1) + - a) with (b - (a - (a / b)%Z * b)) by ring.
......@@ -101,9 +101,8 @@ rewrite <- Zmod_eq_full by lia.
cut (0 <= b * q1 - a < 1).
cut (0 <= Zmod a b <= b - 1).
lra.
change 1 with (IZR 1).
rewrite <- minus_IZR.
apply (IZR_le_le 0).
apply IZR_le_le.
generalize (Z_mod_lt a b).
lia.
assert (Ba': 1 <= a <= 65535).
......
This diff is collapsed.
......@@ -196,7 +196,7 @@ rewrite (bpow_plus _ 1%Z).
apply Rmult_le_compat_r.
apply bpow_ge_0.
rewrite bpow_1.
replace 2%R with (IZR 2) by reflexivity; apply IZR_le.
apply IZR_le.
generalize (radix_gt_1 beta).
omega.
apply bpow_le.
......@@ -339,7 +339,7 @@ rewrite <- bpow_plus.
apply f_equal; ring.
apply bpow_1.
generalize (radix_gt_0 beta); intros.
replace 0 with (IZR 0) by reflexivity; left; now apply IZR_lt.
left; now apply IZR_lt.
rewrite H.
apply Rlt_le_trans with (2 * bpow (e-1) * bpow (e - prec)).
rewrite Rmult_assoc, Rmult_plus_distr_r, Rmult_1_l.
......@@ -505,7 +505,6 @@ apply Rle_lt_trans with (2:=Hn).
apply Rle_trans with (IZR n*(ulp_flx x*((1*1)*(1+0))));[right; ring|idtac].
apply Rle_trans with (IZR n*(ulp_flx x*(2*bpow (prec - 1)* (1 + bpow (1 - prec) / 2))));[idtac|right; ring].
apply Rmult_le_compat_l.
replace 0 with (IZR 0) by reflexivity.
now apply IZR_le.
apply Rmult_le_compat_l.
unfold ulp; apply ulp_ge_0.
......@@ -623,7 +622,6 @@ omega.
rewrite minus_IZR; right.
simpl; field.
apply Rgt_not_eq, Rlt_gt.
replace 0 with (IZR 0) by reflexivity.
apply IZR_lt, radix_gt_0.
right; rewrite Rmult_assoc; apply f_equal.
rewrite <- bpow_1, <- bpow_plus.
......@@ -690,7 +688,6 @@ Proof.
apply Rle_lt_trans with x.
apply Rplus_le_reg_l with (-xk); unfold xk; ring_simplify.
apply Rmult_le_pos.
replace 0 with (IZR 0) by reflexivity.
apply IZR_le, kpos.
apply ulp_ge_0.
apply Rle_lt_trans with (1:=RRle_abs _).
......@@ -873,7 +870,7 @@ unfold Rdiv; apply Rmult_lt_compat_r.
apply Rinv_0_lt_compat, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1.
exact Rlt_0_1.
assert (0 <= IZR k + / 2).
replace 0 with (IZR 0+0) by (simpl; ring); apply Rplus_le_compat.
replace 0 with (0+0) by (simpl; ring); apply Rplus_le_compat.
apply IZR_le, kpos.
apply Rlt_le, Rinv_0_lt_compat, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1.
now apply Rmult_le_0_lt_compat.
......@@ -928,7 +925,7 @@ assert (((radix_val beta = 2)%Z \/ (radix_val beta=3)%Z) \/ (radix_val beta=4)%Z
generalize (radix_gt_1 beta); omega.
destruct H.
(* .. radix is 2 or 3 *)
apply Rle_trans with (x-IZR 0 * ulp_flx x).
apply Rle_trans with (x - 0 * ulp_flx x).
right; simpl; ring.
apply round_flx_sqr_sqrt_aux1...
omega.
......@@ -989,7 +986,6 @@ apply Rlt_le_trans with (4*bpow (mag beta x - 1)).
apply Rmult_lt_compat_r.
apply bpow_gt_0.
interval.
replace 4 with (IZR 4) by reflexivity.
rewrite <- H, <- bpow_1, <- bpow_plus.
right; apply f_equal; ring.
rewrite H2, Rmult_1_l.
......@@ -1004,7 +1000,7 @@ simpl; unfold Z.pow_pos; simpl; omega.
apply (Zpower_le (Build_radix 4 eq_refl)).
now apply Zlt_le_weak.
(* ... *)
apply Rle_trans with (x-IZR 0 * ulp_flx x).
apply Rle_trans with (x - 0 * ulp_flx x).
right; simpl; ring.
apply round_flx_sqr_sqrt_aux1...
omega.
......@@ -1033,6 +1029,7 @@ Qed.
Let k:=(Zceil (x*bpow (1-mag beta x)/(2+bpow (1-prec))) -1)%Z.
Lemma kpos: (0 <= k)%Z.
Proof.
assert (0 < x*bpow (1-mag beta x)/(2+bpow (1-prec))).
apply Fourier_util.Rlt_mult_inv_pos.
apply Rmult_lt_0_compat.
......@@ -1041,13 +1038,14 @@ apply bpow_gt_0.
rewrite Rplus_comm, <-Rplus_assoc; apply Rle_lt_0_plus_1, Rlt_le, Rle_lt_0_plus_1.
apply bpow_ge_0.
assert (0 < Zceil (x * bpow (1 - mag beta x) / (2+bpow (1-prec))))%Z.
apply lt_IZR; simpl (IZR 0).
apply lt_IZR.
apply Rlt_le_trans with (1:=H).
apply Zceil_ub.
unfold k; omega.
Qed.
Lemma kLe: (k < radix_val beta)%Z.
Proof.
cut (Zceil (x * bpow (1 - mag beta x) / (2+bpow (1-prec))) <= beta)%Z.
unfold k; omega.
apply Zceil_glb.
......@@ -1072,6 +1070,7 @@ rewrite bpow_1; right; field.
Qed.
Lemma kLe2: (k <= Zceil (IZR(radix_val beta)/ 2) -1)%Z.
Proof.
cut (Zceil (x * bpow (1 - mag beta x) / (2+bpow (1-prec)))
<= Zceil (IZR(radix_val beta)/ 2))%Z.
unfold k; omega.
......@@ -1109,7 +1108,7 @@ Proof.
intros H; destruct H.
(* radix=5 *)
destruct H as (H1,H2).
apply Rle_trans with (sqrt (IZR beta) + / (4 *IZR (beta))).
apply Rle_trans with (sqrt (IZR beta) + / (4 *IZR beta)).
apply Rplus_le_compat_l.
rewrite (Rinv_mult_distr 4).
apply Rmult_le_compat_l.
......@@ -1158,7 +1157,6 @@ apply bpow_le; omega.
right; reflexivity.
rewrite Rmult_1_r.
assert (6 <= IZR beta).
replace 6 with (IZR 6) by reflexivity.
apply IZR_le; omega.
apply Rle_trans with (IZR beta*(12/25)).
apply Rplus_le_reg_l with (-sqrt (IZR beta)); ring_simplify.
......@@ -1235,7 +1233,7 @@ rewrite bpow_plus, <- Rmult_assoc.
apply Rmult_le_compat_r.
apply bpow_ge_0.
assert (0 <= IZR k + / 2).
replace 0 with (IZR 0+0) by (simpl;ring); apply Rplus_le_compat.
replace 0 with (0+0) by (simpl;ring); apply Rplus_le_compat.
apply IZR_le, kpos.
apply Rlt_le, Rinv_0_lt_compat, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1.
assert (IZR k + / 2 <= IZR beta / 2).
......@@ -1247,7 +1245,7 @@ generalize (beta); intros n.
case (Zeven_odd_dec n); intros V.
apply Zeven_ex_iff in V; destruct V as (m, Hm).
rewrite Hm, mult_IZR.
replace (IZR 2*IZR m/2) with (IZR m).
replace (2*IZR m / 2) with (IZR m).
rewrite Zceil_IZR.
apply Rplus_le_reg_l with (-IZR m + /2).
field_simplify.
......@@ -1258,7 +1256,7 @@ apply Rlt_le, Rlt_0_1.
simpl; field.
apply Zodd_ex_iff in V; destruct V as (m, Hm).
rewrite Hm, plus_IZR, mult_IZR.
replace ((IZR 2*IZR m+IZR 1)/2) with (IZR m+/2).
replace ((2*IZR m + 1)/2) with (IZR m+/2).
replace (Zceil (IZR m + / 2)) with (m+1)%Z.
rewrite plus_IZR; simpl; right; field.
apply sym_eq, Zceil_imp.
......@@ -1352,14 +1350,13 @@ apply bpow_ge_0.
apply Rplus_le_compat_r.
apply Rmult_le_compat_l.
apply Rlt_le, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1.
rewrite minus_IZR; simpl (IZR 1).
rewrite minus_IZR.
apply Rplus_le_compat_r.
apply Zceil_ub.
apply Rmult_lt_compat_l.
apply Rle_lt_0_plus_1.
apply Rmult_le_pos.
apply Rlt_le, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1.
replace 0 with (IZR 0) by reflexivity.
apply IZR_le, Y.
assumption.
(* *)
......
......@@ -87,6 +87,7 @@ Lemma FLXN_le_exp: forall f1 f2:float beta,
((Zpower beta (prec - 1) <= Zabs (Fnum f1) < Zpower beta prec)%Z) ->
((Zpower beta (prec - 1) <= Zabs (Fnum f2) < Zpower beta prec))%Z ->
0 <= F2R f1 -> F2R f1 <= F2R f2 -> (Fexp f1 <= Fexp f2)%Z.
Proof.
intros f1 f2 H1 H2 H3 H4.
case (Zle_or_lt (Fexp f1) (Fexp f2)).
trivial.
......@@ -788,31 +789,23 @@ apply Rle_trans with (15/2*/100+26*/100).
apply Rplus_le_compat.
apply Rmult_le_compat_l.
unfold Rdiv; apply Rmult_le_pos.
replace 0 with (IZR 0) by reflexivity.
replace 15 with (IZR 15) by reflexivity.
apply IZR_le; auto with zarith.
auto with real.
assumption.
rewrite Rmult_assoc.
apply Rmult_le_compat_l.
replace 0 with (IZR 0) by reflexivity.
replace 26 with (IZR 26) by reflexivity.
apply IZR_le; auto with zarith.
rewrite <- (Rmult_1_l (/100)).
apply Rmult_le_compat.
apply epsPos.
apply epsPos.
apply Rle_trans with (1:=prec_suff).
replace 100 with (IZR 100) by reflexivity.
apply Rmult_le_reg_l with (IZR 100).
replace 0 with (IZR 0) by reflexivity.
apply Rmult_le_reg_l with 100%R.
apply IZR_lt; auto with zarith.
rewrite Rinv_r.
rewrite Rmult_1_r.
replace 1 with (IZR 1) by reflexivity.
apply IZR_le; auto with zarith.
apply Rgt_not_eq, Rlt_gt.
replace 0 with (IZR 0) by reflexivity.
apply IZR_lt; auto with zarith.
assumption.
rewrite <- Rmult_plus_distr_r.
......@@ -884,31 +877,23 @@ apply Rle_trans with (15/2*/100+26*/100).
apply Rplus_le_compat.
apply Rmult_le_compat_l.
unfold Rdiv; apply Rmult_le_pos.
replace 0 with (IZR 0) by reflexivity.
replace 15 with (IZR 15) by reflexivity.
apply IZR_le; auto with zarith.
auto with real.
assumption.
rewrite Rmult_assoc.
apply Rmult_le_compat_l.
replace 0 with (IZR 0) by reflexivity.
replace 26 with (IZR 26) by reflexivity.
apply IZR_le; auto with zarith.
rewrite <- (Rmult_1_l (/100)).
apply Rmult_le_compat.
apply epsPos.
apply epsPos.
apply Rle_trans with (1:=prec_suff).
replace 100 with (IZR 100) by reflexivity.
apply Rmult_le_reg_l with (IZR 100).
replace 0 with (IZR 0) by reflexivity.
apply Rmult_le_reg_l with 100%R.
apply IZR_lt; auto with zarith.
rewrite Rinv_r.
rewrite Rmult_1_r.
replace 1 with (IZR 1) by reflexivity.
apply IZR_le; auto with zarith.
apply Rgt_not_eq, Rlt_gt.
replace 0 with (IZR 0) by reflexivity.
apply IZR_lt; auto with zarith.
assumption.
interval.
......@@ -978,6 +963,7 @@ Definition radix2 := Build_radix 2 (refl_equal true).
Definition radix10 := Build_radix 10 (refl_equal true).
Lemma prec_suff_2: forall prec:Z, (7 <= prec)%Z -> (/2*bpow radix2 (1-prec) <= /100)%R.
Proof.
intros p Hp.
apply Rle_trans with (/2* bpow radix2 (-6))%R.
apply Rmult_le_compat_l.
......@@ -985,25 +971,20 @@ intuition.
apply bpow_le.
omega.
simpl; rewrite <- Rinv_mult_distr.
replace 100%R with (IZR 100) by reflexivity.
replace 128%R with (IZR 128) by reflexivity.
apply Rle_Rinv.
replace 0%R with (IZR 0) by reflexivity.
apply IZR_lt; auto with zarith.
replace 0%R with (IZR 0) by reflexivity.
apply IZR_lt; auto with zarith.
apply IZR_le; auto with zarith.
apply Rgt_not_eq, Rlt_gt.
apply Rle_lt_0_plus_1; apply Rlt_le; exact Rlt_0_1.
apply Rgt_not_eq, Rlt_gt.
replace 0%R with (IZR 0) by reflexivity.
replace 64%R with (IZR 64) by reflexivity.
apply IZR_lt; auto with zarith.
Qed.
Lemma prec_suff_10: forall prec:Z, (3 <= prec)%Z -> (/2*bpow radix10 (1-prec) <= /100)%R.
Proof.
intros p Hp.
apply Rle_trans with (/2* bpow radix10 (-2))%R.
apply Rmult_le_compat_l.
......@@ -1011,19 +992,13 @@ intuition.
apply bpow_le.
omega.
simpl; rewrite <- Rinv_mult_distr.
replace 200%R with (IZR 200) by reflexivity.
replace 100%R with (IZR 100) by reflexivity.
apply Rle_Rinv.
replace 0%R with (IZR 0) by reflexivity.
apply IZR_lt; auto with zarith.
replace 0%R with (IZR 0) by reflexivity.
apply IZR_lt; auto with zarith.
apply IZR_le; auto with zarith.
apply Rgt_not_eq, Rlt_gt.
apply Rle_lt_0_plus_1; apply Rlt_le; exact Rlt_0_1.
apply Rgt_not_eq, Rlt_gt.
replace 0%R with (IZR 0) by reflexivity.
replace 100%R with (IZR 100) by reflexivity.
apply IZR_lt; auto with zarith.
Qed.
......@@ -1636,7 +1611,7 @@ apply Rmult_le_reg_l with 2%R.
intuition.
apply Rplus_le_reg_l with (-IZR (emin+prec-1)).
apply Rle_trans with (IZR (emin + prec - 1));[right; ring|idtac].
apply Rle_trans with (IZR 0);[idtac|right;simpl;field].
apply Rle_trans with 0%R;[idtac|right;simpl;field].
apply IZR_le.
omega.
apply Rle_trans with (sqrt (bpow (emin + prec - 1))).
......@@ -1645,7 +1620,7 @@ apply Rle_trans with (sqrt (bpow (2*Zceil (IZR (emin + prec - 1) / 2)))).
apply sqrt_le_1_alt.
apply bpow_le.
apply le_IZR.
rewrite mult_IZR; simpl (IZR 2).
rewrite mult_IZR.
apply Rle_trans with ( 2 * ((IZR (emin + prec - 1) / 2))).
right; field.
apply Rmult_le_compat_l.
......@@ -1973,7 +1948,7 @@ intuition.
unfold Rdiv; rewrite Rmult_assoc.
rewrite Rinv_l.
rewrite Rmult_1_r.
replace 2%R with (IZR 2) by reflexivity; rewrite <- mult_IZR.
rewrite <- mult_IZR.
apply IZR_le.
omega.
apply Rgt_not_eq; intuition.
......@@ -2024,7 +1999,7 @@ apply Rmult_le_reg_l with 2%R.
intuition.
apply Rplus_le_reg_l with (-IZR (emin+prec-1)).
apply Rle_trans with (IZR (emin + prec - 1));[right; ring|idtac].
apply Rle_trans with (IZR 0);[idtac|right;simpl;field].
apply Rle_trans with 0%R;[idtac|right;simpl;field].
apply IZR_le.
omega.
rewrite Rabs_right.
......@@ -2039,9 +2014,9 @@ apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rle_trans with (IZR (radix_val beta)*IZR (radix_val beta)).
apply Rmult_le_compat;[intuition|intuition|idtac|idtac]; clear.
replace 2%R with (IZR 2) by reflexivity; apply IZR_le.
apply IZR_le.
apply Zle_bool_imp_le; now destruct beta.
replace 2%R with (IZR 2) by reflexivity; apply IZR_le.
apply IZR_le.
apply Zle_bool_imp_le; now destruct beta.
right; simpl.
unfold Zpower_pos; simpl.
......@@ -2054,7 +2029,7 @@ intuition.
unfold Rdiv; rewrite Rmult_assoc.
rewrite Rinv_l.
rewrite Rmult_1_r.
replace 2%R with (IZR 2) by reflexivity; rewrite <- mult_IZR.
rewrite <- mult_IZR.
apply IZR_le.
omega.
apply Rgt_not_eq.
......@@ -2129,7 +2104,7 @@ intuition.
unfold Rdiv; rewrite Rmult_assoc.
rewrite Rinv_l.
rewrite Rmult_1_r.
replace 2%R with (IZR 2) by reflexivity; rewrite <- mult_IZR.
rewrite <- mult_IZR.
apply IZR_le.
omega.
apply Rgt_not_eq; intuition.
......@@ -2179,7 +2154,7 @@ apply Rmult_le_reg_l with 2%R.
intuition.
apply Rplus_le_reg_l with (-IZR (emin+prec-1)).
apply Rle_trans with (IZR (emin + prec - 1));[right; ring|idtac].
apply Rle_trans with (IZR 0);[idtac|right;simpl;field].
apply Rle_trans with 0%R;[idtac|right;simpl;field].
apply IZR_le.
omega.
(* *)
......@@ -2248,7 +2223,7 @@ intuition.
unfold Rdiv; rewrite Rmult_assoc.
rewrite Rinv_l.
rewrite Rmult_1_r.
replace 2%R with (IZR 2) by reflexivity; rewrite <- mult_IZR.
rewrite <- mult_IZR.
apply IZR_le.
omega.
apply Rgt_not_eq; intuition.
......
......@@ -144,23 +144,17 @@ assert (0 < v < 1)%R.
split.
unfold v, Rdiv.
apply Rmult_lt_0_compat.
case l.
now apply (IZR_lt 0 2).
now apply (IZR_lt 0 1).
now apply (IZR_lt 0 3).
case l ; now apply IZR_lt.
apply Rinv_0_lt_compat.
now apply (IZR_lt 0 4).
now apply IZR_lt.
unfold v, Rdiv.
apply Rmult_lt_reg_r with 4%R.
now apply (IZR_lt 0 4).
now apply IZR_lt.
rewrite Rmult_assoc, Rinv_l.
rewrite Rmult_1_r, Rmult_1_l.
case l.
now apply (IZR_lt 2 4).
now apply (IZR_lt 1 4).
now apply (IZR_lt 3 4).
case l ; now apply IZR_lt.
apply Rgt_not_eq.
now apply (IZR_lt 0 4).
now apply IZR_lt.
split.
apply Rplus_lt_reg_r with (d * (v - 1))%R.
ring_simplify.
......@@ -177,7 +171,7 @@ exact Hdu.
set (v := (match l with Lt => 1 | Eq => 2 | Gt => 3 end)%R).
rewrite <- (Rcompare_plus_r (- (d + u) / 2)).
rewrite <- (Rcompare_mult_r 4).
2: now apply (IZR_lt 0 4).
2: now apply IZR_lt.
replace (((d + u) / 2 + - (d + u) / 2) * 4)%R with ((u - d) * 0)%R by field.
replace ((d + v / 4 * (u - d) + - (d + u) / 2) * 4)%R with ((u - d) * (v - 2))%R by field.
rewrite Rcompare_mult_l.
......@@ -185,10 +179,7 @@ rewrite Rcompare_mult_l.
rewrite <- (Rcompare_plus_r 2).
ring_simplify (v - 2 + 2)%R (0 + 2)%R.
unfold v.
case l.
exact (Rcompare_IZR 2 2).
exact (Rcompare_IZR 1 2).
exact (Rcompare_IZR 3 2).
case l ; apply Rcompare_IZR.
Qed.
Section Fcalc_bracket_step.
......@@ -235,7 +226,7 @@ apply Rlt_le_trans with (2 := proj1 Hx').
rewrite <- (Rplus_0_r start) at 1.
apply Rplus_lt_compat_l.
apply Rmult_lt_0_compat.
now apply (IZR_lt 0).
now apply IZR_lt.
exact Hstep.
apply Rlt_le_trans with (1 := proj2 Hx').
apply Rplus_le_compat_l.
......@@ -262,7 +253,6 @@ apply Rlt_le_trans with (1 := proj2 Hx').
apply Rcompare_not_Lt_inv.
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
apply Rcompare_not_Lt.
change 2%R with (IZR 2).
rewrite <- mult_IZR.
apply IZR_le.
omega.
......@@ -284,7 +274,6 @@ apply Rlt_le_trans with (2 := proj1 Hx').
apply Rcompare_Lt_inv.
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
apply Rcompare_Lt.
change 2%R with (IZR 2).
rewrite <- mult_IZR.
apply IZR_lt.
omega.
......@@ -308,7 +297,7 @@ apply Rplus_lt_compat_l.
rewrite <- (Rmult_1_l step) at 1.
apply Rmult_lt_compat_r.
exact Hstep.
now apply (IZR_lt 1).
now apply IZR_lt.
(* . *)
apply Rcompare_Lt.
apply Rlt_le_trans with (1 := proj2 Hx').
......@@ -318,7 +307,7 @@ rewrite <- (Rmult_1_l step) at 2.
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
rewrite Rmult_1_r.
apply Rcompare_not_Lt.
apply (IZR_le 2).
apply IZR_le.
now apply (Zlt_le_succ 1).
exact Hstep.
Qed.
......@@ -360,7 +349,6 @@ inversion_clear Hx as [Hl|].
rewrite Hl.
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r.
apply Rcompare_Lt.
change 2%R with (IZR 2).
rewrite <- mult_IZR.
apply IZR_lt.
rewrite <- Hk.
......@@ -383,7 +371,6 @@ assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl).
apply Rle_lt_trans with (2 := proj1 Hx').
apply Rcompare_not_Lt_inv.
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r.
change 2%R with (IZR 2).
rewrite <- mult_IZR.
apply Rcompare_not_Lt.
apply IZR_le.
......@@ -404,7 +391,6 @@ omega.
apply Rcompare_Eq.
inversion_clear Hx as [Hx'|].
rewrite Hx', <- Hk, mult_IZR.
simpl (IZR 2).
field.
Qed.
......
......@@ -138,14 +138,14 @@ replace ((IZR m2 * IZR q + IZR r) * (bpow e' * bpow e2) / (IZR m2 * bpow e2))%R
apply inbetween_mult_compat.
apply bpow_gt_0.
destruct (Z_lt_le_dec 1 m2) as [Hm2''|Hm2''].
replace (IZR 1) with (IZR m2 * /IZR m2)%R.
replace 1%R with (IZR m2 * /IZR m2)%R.
apply new_location_correct ; try easy.
apply Rinv_0_lt_compat.
now apply (IZR_lt 0).
now apply IZR_lt.
now constructor.
apply Rinv_r.
apply Rgt_not_eq.
now apply (IZR_lt 0).
now apply IZR_lt.
assert (r = 0 /\ m2 = 1)%Z by (clear -Hr Hm2'' ; omega).
rewrite (proj1 H), (proj2 H).
unfold Rdiv.
......@@ -154,7 +154,7 @@ now constructor.
field.
split ; apply Rgt_not_eq.
apply bpow_gt_0.
now apply (IZR_lt 0).
now apply IZR_lt.
Qed.
End Fcalc_div.
......@@ -285,10 +285,10 @@ case Rlt_bool_spec ; intros Hx' ;
elim Rlt_not_le with (1 := Hx').
apply Rlt_le.
apply Rle_lt_trans with (2 := proj1 Hx).
now apply (IZR_le 0).
now apply IZR_le.
elim Rle_not_lt with (1 := Hx').
apply Rlt_le_trans with (1 := proj2 Hx).
apply (IZR_le _ 0).
apply IZR_le.
now apply Zlt_le_succ.
rewrite Hm.
now apply Rlt_not_eq.
......@@ -376,7 +376,6 @@ rewrite <- Hl'.
rewrite plus_IZR.
rewrite <- (Rcompare_plus_r (- IZR m) x).
apply f_equal.
simpl (IZR 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
......@@ -412,7 +411,6 @@ rewrite <- Hl'.
rewrite plus_IZR.
rewrite <- (Rcompare_plus_r (- IZR m) (-x)).
apply f_equal.
simpl (IZR 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
......@@ -436,7 +434,6 @@ rewrite <- Hl'.
rewrite plus_IZR.
rewrite <- (Rcompare_plus_r (- IZR m) x).
apply f_equal.
simpl (IZR 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
......@@ -918,7 +915,7 @@ rewrite <- (Zrnd_IZR rnd (-m)) at 1.
assert (IZR (-m) < 0)%R.
rewrite opp_IZR.
apply Ropp_lt_gt_0_contravar.
apply (IZR_lt 0).
apply IZR_lt.
apply F2R_gt_0_reg with beta e.
rewrite <- H.
apply Rabs_pos_lt.
......@@ -933,7 +930,7 @@ apply Ropp_involutive.
change (m = cond_Zopp false (choice false m loc_Exact))%Z.
rewrite <- (Zrnd_IZR rnd m) at 1.
assert (0 <= IZR m)%R.
apply (IZR_le 0).
apply IZR_le.
apply F2R_ge_0_reg with beta e.
rewrite <- H.
apply Rabs_pos.
......
......@@ -152,7 +152,7 @@ omega.
(* . round *)
unfold inbetween_float, F2R. simpl.
rewrite sqrt_mult.
2: now apply (IZR_le 0) ; apply Zlt_le_weak.
2: now apply IZR_le, Zlt_le_weak.
2: apply Rlt_le ; apply bpow_gt_0.
destruct (Zeven_ex e') as (e2, Hev).
rewrite He1, Zplus_0_r in Hev. clear He1.
......@@ -172,8 +172,8 @@ rewrite Hr', Zplus_0_r, mult_IZR.
fold (Rsqr (IZR q)).
rewrite sqrt_Rsqr.
now constructor.
apply (IZR_le 0).
omega.
apply IZR_le.
clear -Hr ; omega.
(* .. r <> 0 *)
constructor.
split.
......@@ -183,20 +183,20 @@ rewrite mult_IZR.
fold (Rsqr (IZR q)).
rewrite sqrt_Rsqr.
apply Rle_refl.
apply (IZR_le 0).
omega.
apply IZR_le.
clear -Hr ; omega.
apply sqrt_lt_1.
rewrite mult_IZR.
apply Rle_0_sqr.
rewrite <- Hq.
apply (IZR_le 0).
apply IZR_le.
now apply Zlt_le_weak.
apply IZR_lt.
omega.
apply Rlt_le_trans with (sqrt (IZR ((q + 1) * (q + 1)))).
apply sqrt_lt_1.
rewrite <- Hq.
apply (IZR_le 0).
apply IZR_le.
now apply Zlt_le_weak.
rewrite mult_IZR.
apply Rle_0_sqr.
......@@ -207,15 +207,14 @@ rewrite mult_IZR.
fold (Rsqr (IZR (q + 1))).
rewrite sqrt_Rsqr.
apply Rle_refl.
apply (IZR_le 0).
omega.
apply IZR_le.
clear -Hr ; omega.
(* ... location *)
rewrite Rcompare_half_r.
rewrite <- Rcompare_sqr.
replace ((2 * sqrt (IZR (q * q + r))) * (2 * sqrt (IZR (q * q + r))))%R
with (4 * Rsqr (sqrt (IZR (q * q + r))))%R by (