Commit fc6c63d2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Move Z2R into IZR.

parent 76316860
......@@ -85,9 +85,9 @@ rewrite Rabs_mult; rewrite (Rabs_right (bpow e)).
rewrite bpow_plus.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
rewrite <- Z2R_abs.
rewrite <- Z2R_Zpower.
now apply Z2R_lt.
rewrite <- abs_IZR.
rewrite <- IZR_Zpower.
now apply IZR_lt.
now apply Zlt_le_weak.
Qed.
......@@ -214,9 +214,9 @@ 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 (Z2R 2).
rewrite <- (Z2R_abs 2).
now apply (Z2R_le 1 2).
change 2 with (IZR 2).
rewrite <- (abs_IZR 2).
now apply (IZR_le 1 2).
(* *)
rewrite cexp_FLT_FIX.
rewrite cexp_FLT_FIX; trivial.
......@@ -226,7 +226,7 @@ apply bpow_le; omega.
lra.
rewrite Rabs_mult.
rewrite Rabs_pos_eq.
2: now apply (Z2R_le 0 2).
2: now apply (IZR_le 0 2).
apply Rlt_le_trans with (2*bpow (emin + prec - 1)).
apply Rmult_lt_compat_l with (1 := Rlt_0_2).
assumption.
......@@ -519,7 +519,7 @@ rewrite Zeven_opp.
rewrite Zeven_Zpower.
reflexivity.
unfold Prec_gt_0 in prec_gt_0_; omega.
apply eq_Z2R.
apply eq_IZR.
rewrite <- scaled_mantissa_DN...
2: rewrite H4; assumption.
rewrite H4.
......@@ -543,9 +543,9 @@ replace 2 with (bpow 1) by reflexivity.
rewrite <- bpow_plus.
rewrite H0.
rewrite Rmult_minus_distr_r, <- 2!bpow_plus.
rewrite Z2R_minus.
rewrite minus_IZR.
apply f_equal2.
rewrite Z2R_Zpower.
rewrite IZR_Zpower.
apply f_equal.
ring.
unfold Prec_gt_0 in prec_gt_0_; omega.
......@@ -1077,22 +1077,22 @@ Qed.
Lemma avg_half_sub_no_underflow_aux_aux: forall z:Z, (0 < z)%Z ->
(ZnearestE (Z2R z / 2) < z)%Z.
(ZnearestE (IZR z / 2) < z)%Z.
Proof.
intros z H1.
case (Zle_lt_or_eq 1 z); [omega|intros H2|intros H2].
apply lt_Z2R.
apply Rplus_lt_reg_r with (- ((Z2R z)/2)).
apply Rle_lt_trans with (-(((Z2R z) /2) - Z2R (ZnearestE (Z2R z / 2)))).
apply lt_IZR.
apply Rplus_lt_reg_r with (- ((IZR z)/2)).
apply Rle_lt_trans with (-(((IZR z) /2) - IZR (ZnearestE (IZR z / 2)))).
right; ring.
apply Rle_lt_trans with (1:= RRle_abs _).
rewrite Rabs_Ropp.
apply Rle_lt_trans with (1:=Znearest_N (fun x => negb (Zeven x)) _).
apply Rle_lt_trans with (1*/2);[right; ring|idtac].
apply Rlt_le_trans with ((Z2R z)*/2);[idtac|right; field].
apply Rlt_le_trans with ((IZR z)*/2);[idtac|right; field].
apply Rmult_lt_compat_r.
lra.
now apply (Z2R_lt 1).
now apply (IZR_lt 1).
rewrite <- H2.
unfold Znearest; simpl.
replace (Zfloor (1 / 2)) with 0%Z.
......@@ -1134,16 +1134,16 @@ rewrite H1; unfold F2R; simpl.
rewrite <- H4.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
apply Z2R_lt.
replace (Z2R (Fnum g) * bpow emin / 2 * bpow (- emin)) with (Z2R (Fnum g) /2).
apply IZR_lt.
replace (IZR (Fnum g) * bpow emin / 2 * bpow (- emin)) with (IZR (Fnum g) /2).
apply avg_half_sub_no_underflow_aux_aux.
apply lt_Z2R.
apply lt_IZR.
apply Rmult_lt_reg_r with (bpow (Fexp g)).
apply bpow_gt_0.
rewrite Rmult_0_l.
apply Rlt_le_trans with (1:=Hf1).
right; rewrite H1; reflexivity.
unfold Rdiv; apply trans_eq with (Z2R (Fnum g) * / 2 * (bpow (- emin)*bpow emin)).
unfold Rdiv; apply trans_eq with (IZR (Fnum g) * / 2 * (bpow (- emin)*bpow emin)).
rewrite <- bpow_plus.
ring_simplify (-emin+emin)%Z.
simpl; ring.
......@@ -1162,8 +1162,8 @@ rewrite (bpow_plus _ prec _).
apply Rmult_lt_compat.
apply Rabs_pos.
apply bpow_ge_0.
rewrite <- Z2R_Zpower, <- Z2R_abs.
now apply Z2R_lt.
rewrite <- IZR_Zpower, <- abs_IZR.
now apply IZR_lt.
unfold Prec_gt_0 in prec_gt_0_; omega.
rewrite <- H4; apply bpow_lt.
omega.
......@@ -1274,14 +1274,14 @@ apply generic_format_FIX_FLT,FIX_format_generic in Fv.
destruct Fu as [[nu eu] J1 J2].
destruct Fv as [[nv ev] J3 J4]; simpl in J2, J4.
(* b is bpow emin /2 *)
assert (b = Z2R (nu+nv) * bpow (emin-1)).
assert (b = IZR (nu+nv) * bpow (emin-1)).
unfold b; rewrite J1, J3; unfold F2R; rewrite J2,J4; simpl.
unfold Zminus; rewrite bpow_plus, Z2R_plus.
unfold Zminus; rewrite bpow_plus, plus_IZR.
change (bpow (-(1))) with (/2).
field.
assert (Z.abs (nu+nv) = 1)%Z.
assert (0 < Z.abs (nu+nv) < 2)%Z;[idtac|omega].
split; apply lt_Z2R; simpl; rewrite Z2R_abs;
split; apply lt_IZR; simpl; rewrite abs_IZR;
apply Rmult_lt_reg_l with (bpow (emin-1)); try apply bpow_gt_0.
rewrite Rmult_0_r.
apply Rlt_le_trans with (1:=H1).
......@@ -1301,7 +1301,7 @@ field.
(* only 2 possible values for u and v *)
assert (((nu=0)/\ (nv=1)) \/ ((nu=-1)/\(nv=0)))%Z.
assert (nu <= nv)%Z.
apply le_Z2R.
apply le_IZR.
apply Rmult_le_reg_r with (bpow emin).
apply bpow_gt_0.
apply Rle_trans with u.
......@@ -1369,9 +1369,9 @@ apply Rle_trans with (1*bpow emin).
right; ring.
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply (Z2R_le 1 3).
now apply (IZR_le 1 3).
apply Rmult_le_compat_l.
now apply (Z2R_le 0 3).
now apply (IZR_le 0 3).
rewrite ulp_neq_0.
2: apply Rmult_integral_contrapositive_currified.
2: apply Rgt_not_eq, bpow_gt_0.
......@@ -1405,9 +1405,9 @@ apply Rle_trans with (1*bpow emin).
right; ring.
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply (Z2R_le 1 3).
now apply (IZR_le 1 3).
apply Rmult_le_compat_l.
now apply (Z2R_le 0 3).
now apply (IZR_le 0 3).
rewrite ulp_neq_0.
2: apply Rmult_integral_contrapositive_currified.
2: apply Rgt_not_eq, bpow_gt_0.
......@@ -1503,7 +1503,7 @@ rewrite <- (Rmult_1_l (Rabs b)).
rewrite (T b).
apply Rmult_le_compat_r.
apply Rabs_pos.
now apply (Z2R_le 1 2).
now apply (IZR_le 1 2).
rewrite <- (T b).
rewrite <- ulp_abs.
apply FLT_ulp_le_id...
......@@ -1517,7 +1517,7 @@ destruct Fv as [fv J3 J4].
apply generic_format_FIX.
exists (Float radix2 (Fnum fu+Fnum fv) emin).
rewrite J1,J3; unfold F2R; simpl.
rewrite J2,J4, Z2R_plus; ring.
rewrite J2,J4, plus_IZR; ring.
easy.
apply FIX_format_generic in H.
destruct H as [[n e] J1 J2].
......@@ -1528,9 +1528,9 @@ rewrite (Rabs_right (bpow emin)).
2: apply Rle_ge, bpow_ge_0.
apply Rmult_le_compat_r.
apply bpow_ge_0.
rewrite <- Z2R_abs.
replace 1 with (Z2R 1) by reflexivity.
apply Z2R_le.
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.
intros M; apply K1.
......@@ -1615,7 +1615,7 @@ replace (v-v) with 0 by ring.
rewrite Rabs_R0.
apply Rmult_le_pos.
apply Rmult_le_pos.
now apply (Z2R_le 0 3).
now apply (IZR_le 0 3).
lra.
apply ulp_ge_0.
Qed.
......
......@@ -132,8 +132,8 @@ generalize (method_error t Bt).
intros Ef.
rewrite bpow_plus, Rmult_assoc.
assert (exp x = pow2 (Zfloor k) * exp (x - k * ln 2)) as ->.
assert (exists k', k = Z2R k') as [k' ->] by (eexists ; apply Rmult_1_r).
rewrite Zfloor_Z2R, bpow_exp, <- exp_plus.
assert (exists k', k = IZR k') as [k' ->] by (eexists ; apply Rmult_1_r).
rewrite Zfloor_IZR, bpow_exp, <- exp_plus.
apply f_equal.
simpl ; ring.
rewrite <- Rmult_minus_distr_l.
......
......@@ -16,8 +16,8 @@ field.
now apply Rgt_not_eq.
Qed.
Lemma FIX_format_Z2R :
forall beta x, FIX_format beta 0 (Z2R x).
Lemma FIX_format_IZR :
forall beta x, FIX_format beta 0 (IZR x).
Proof.
intros beta x.
exists (Float beta x 0).
......@@ -48,15 +48,15 @@ now apply Rplus_le_reg_r with a.
now apply Rplus_lt_reg_r with a.
Qed.
Coercion Z2R : Z >-> R.
Coercion IZR : Z >-> R.
Lemma Z2R_le_le :
Lemma IZR_le_le :
forall a b c,
(a <= b <= c)%Z ->
a <= b <= c.
Proof.
intros a b c.
now split ; apply Z2R_le.
now split ; apply IZR_le.
Qed.
Notation pow2 := (bpow radix2).
......@@ -89,29 +89,29 @@ set (q0 := fma a y0 0).
set (e0 := fnma b y0 (1 + pow2 (-17))).
set (q1 := fma e0 q0 q0).
apply Zfloor_imp.
rewrite Z2R_plus.
rewrite plus_IZR.
simpl.
apply Rmult_le_lt_reg_l with b.
apply (Z2R_lt 0) ; lia.
apply (IZR_lt 0) ; 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.
rewrite <- Z2R_mult, <- Z2R_minus.
rewrite <- mult_IZR, <- minus_IZR.
rewrite <- Zmod_eq_full by lia.
cut (0 <= b * q1 - a < 1).
cut (0 <= Zmod a b <= b - 1).
lra.
change 1 with (Z2R 1).
rewrite <- Z2R_minus.
apply (Z2R_le_le 0).
change 1 with (IZR 1).
rewrite <- minus_IZR.
apply (IZR_le_le 0).
generalize (Z_mod_lt a b).
lia.
assert (Ba': 1 <= a <= 65535).
change (1%Z <= a <= 65535%Z).
now split ; apply Z2R_le.
now split ; apply IZR_le.
assert (Bb': 1 <= b <= 65535).
change (1%Z <= b <= 65535%Z).
now split ; apply Z2R_le.
now split ; apply IZR_le.
refine (let '(conj H1 H2) := _ in conj H1 (Rnot_le_lt _ _ H2)).
set (err := (q1 - a / b) / (a / b)).
replace (b * q1 - a) with (a * err) by abstract (unfold err ; field ; lra).
......@@ -123,6 +123,6 @@ assert (H: (Mq1 - a / b) / (a / b) = -(eps0 * eps0) + (1 + eps0) * pow2 (-17))
by abstract (unfold Mq1, Me0, Mq0, eps0 ; field ; lra).
revert H.
unfold Mq1, Me0, Mq0, eps0, err, q1, e0, q0, y0.
generalize (frcpa_spec b) (FIX_format_Z2R radix2 a) (FIX_format_Z2R radix2 b).
generalize (frcpa_spec b) (FIX_format_IZR radix2 a) (FIX_format_IZR radix2 b).
gappa.
Qed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -131,21 +131,21 @@ now apply Zle_lt_trans with r.
exact Hq'.
(* . the location is correctly computed *)
unfold inbetween_float, F2R. simpl.
rewrite bpow_plus, Z2R_plus.
rewrite Hq, Z2R_plus, Z2R_mult.
replace ((Z2R m2 * Z2R q + Z2R r) * (bpow e' * bpow e2) / (Z2R m2 * bpow e2))%R
with ((Z2R q + Z2R r / Z2R m2) * bpow e')%R.
rewrite bpow_plus, plus_IZR.
rewrite Hq, plus_IZR, mult_IZR.
replace ((IZR m2 * IZR q + IZR r) * (bpow e' * bpow e2) / (IZR m2 * bpow e2))%R
with ((IZR q + IZR r / IZR m2) * bpow e')%R.
apply inbetween_mult_compat.
apply bpow_gt_0.
destruct (Z_lt_le_dec 1 m2) as [Hm2''|Hm2''].
replace (Z2R 1) with (Z2R m2 * /Z2R m2)%R.
replace (IZR 1) with (IZR m2 * /IZR m2)%R.
apply new_location_correct ; try easy.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0).
now apply (IZR_lt 0).
now constructor.
apply Rinv_r.
apply Rgt_not_eq.
now apply (Z2R_lt 0).
now apply (IZR_lt 0).
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 (Z2R_lt 0).
now apply (IZR_lt 0).
Qed.
End Fcalc_div.
......@@ -98,7 +98,7 @@ destruct (Falign f1 f2) as ((m1, m2), e).
intros (H1, H2).
rewrite H1, H2.
unfold F2R. simpl.
rewrite Z2R_plus.
rewrite plus_IZR.
apply Rmult_plus_distr_r.
Qed.
......@@ -154,7 +154,7 @@ Theorem F2R_mult :
Proof.
intros (m1, e1) (m2, e2).
unfold Fmult, F2R. simpl.
rewrite Z2R_mult, bpow_plus.
rewrite mult_IZR, bpow_plus.
ring.
Qed.
......
......@@ -44,7 +44,7 @@ Theorem inbetween_float_round :
Proof.
intros rnd choice Hc x m l e Hl.
unfold round, F2R. simpl.
apply (f_equal (fun m => (Z2R m * bpow e)%R)).
apply (f_equal (fun m => (IZR m * bpow e)%R)).
apply Hc.
apply inbetween_mult_reg with (bpow e).
apply bpow_gt_0.
......@@ -63,7 +63,7 @@ Theorem inbetween_float_round_sign :
round beta fexp rnd x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l)) e).
Proof.
intros rnd choice Hc x m l e Hx.
apply (f_equal (fun m => (Z2R m * bpow e)%R)).
apply (f_equal (fun m => (IZR m * bpow e)%R)).
simpl.
replace (Rlt_bool x 0) with (Rlt_bool (scaled_mantissa beta fexp x) 0).
(* *)
......@@ -96,7 +96,7 @@ Proof.
intros x m l Hl.
refine (Zfloor_imp m _ _).
apply inbetween_bounds with (2 := Hl).
apply Z2R_lt.
apply IZR_lt.
apply Zlt_succ.
Qed.
......@@ -128,23 +128,23 @@ destruct (Rcase_abs x) as [Zx|Zx] .
rewrite Rlt_bool_true with (1 := Zx).
inversion_clear Hl ; simpl.
rewrite <- (Ropp_involutive x).
rewrite H, <- Z2R_opp.
apply Zfloor_Z2R.
rewrite H, <- opp_IZR.
apply Zfloor_IZR.
apply Zfloor_imp.
split.
apply Rlt_le.
rewrite Z2R_opp.
rewrite opp_IZR.
apply Ropp_lt_cancel.
now rewrite Ropp_involutive.
ring_simplify (- (m + 1) + 1)%Z.
rewrite Z2R_opp.
rewrite opp_IZR.
apply Ropp_lt_cancel.
now rewrite Ropp_involutive.
(* *)
rewrite Rlt_bool_false.
inversion_clear Hl ; simpl.
rewrite H.
apply Zfloor_Z2R.
apply Zfloor_IZR.
apply Zfloor_imp.
split.
now apply Rlt_le.
......@@ -183,7 +183,7 @@ destruct Hl' as [Hl'|(Hl1, Hl2)].
rewrite Hl'.
destruct Hl ; try easy.
rewrite H.
exact (Zceil_Z2R _).
exact (Zceil_IZR _).
(* not Exact *)
rewrite Hl2.
simpl.
......@@ -224,7 +224,7 @@ unfold Zceil.
apply f_equal.
inversion_clear Hl ; simpl.
rewrite H.
apply Zfloor_Z2R.
apply Zfloor_IZR.
apply Zfloor_imp.
split.
now apply Rlt_le.
......@@ -234,7 +234,7 @@ rewrite Rlt_bool_false.
simpl.
inversion_clear Hl ; simpl.
rewrite H.
apply Zceil_Z2R.
apply Zceil_IZR.
apply Zceil_imp.
split.
change (m + 1 - 1)%Z with (Zpred (Zsucc m)).
......@@ -270,7 +270,7 @@ intros x m l Hl.
inversion_clear Hl as [Hx|l' Hx Hl'].
(* Exact *)
rewrite Hx.
rewrite Zrnd_Z2R...
rewrite Zrnd_IZR...
(* not Exact *)
unfold Ztrunc.
assert (Hm: Zfloor x = m).
......@@ -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 (Z2R_le 0).
now apply (IZR_le 0).
elim Rle_not_lt with (1 := Hx').
apply Rlt_le_trans with (1 := proj2 Hx).
apply (Z2R_le _ 0).
apply (IZR_le _ 0).
now apply Zlt_le_succ.
rewrite Hm.
now apply Rlt_not_eq.
......@@ -321,7 +321,7 @@ apply f_equal.
apply Zfloor_imp.
rewrite <- Rabs_left with (1 := Zx).
apply inbetween_bounds with (2 := Hl).
apply Z2R_lt.
apply IZR_lt.
apply Zlt_succ.
(* *)
rewrite Rlt_bool_false with (1 := Zx).
......@@ -329,7 +329,7 @@ simpl.
apply Zfloor_imp.
rewrite <- Rabs_pos_eq with (1 := Zx).
apply inbetween_bounds with (2 := Hl).
apply Z2R_lt.
apply IZR_lt.
apply Zlt_succ.
Qed.
......@@ -362,7 +362,7 @@ intros choice x m l Hl.
inversion_clear Hl as [Hx|l' Hx Hl'].
(* Exact *)
rewrite Hx.
rewrite Zrnd_Z2R...
rewrite Zrnd_IZR...
(* not Exact *)
unfold Znearest.
assert (Hm: Zfloor x = m).
......@@ -370,13 +370,13 @@ apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
rewrite Zceil_floor_neq.
rewrite Hm.
replace (Rcompare (x - Z2R m) (/2)) with l'.
replace (Rcompare (x - IZR m) (/2)) with l'.
now case l'.
rewrite <- Hl'.
rewrite Z2R_plus.
rewrite <- (Rcompare_plus_r (- Z2R m) x).
rewrite plus_IZR.
rewrite <- (Rcompare_plus_r (- IZR m) x).
apply f_equal.
simpl (Z2R 1).
simpl (IZR 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
......@@ -399,20 +399,20 @@ rewrite Znearest_opp.
apply f_equal.
inversion_clear Hl as [Hx|l' Hx Hl'].
rewrite Hx.
apply Zrnd_Z2R...
apply Zrnd_IZR...
assert (Hm: Zfloor (-x) = m).
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
unfold Znearest.
rewrite Zceil_floor_neq.
rewrite Hm.
replace (Rcompare (- x - Z2R m) (/2)) with l'.
replace (Rcompare (- x - IZR m) (/2)) with l'.
now case l'.
rewrite <- Hl'.
rewrite Z2R_plus.
rewrite <- (Rcompare_plus_r (- Z2R m) (-x)).
rewrite plus_IZR.
rewrite <- (Rcompare_plus_r (- IZR m) (-x)).
apply f_equal.
simpl (Z2R 1).
simpl (IZR 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
......@@ -423,20 +423,20 @@ rewrite Rlt_bool_false with (1 := Zx).
simpl.
inversion_clear Hl as [Hx|l' Hx Hl'].
rewrite Hx.
apply Zrnd_Z2R...
apply Zrnd_IZR...
assert (Hm: Zfloor x = m).
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
unfold Znearest.
rewrite Zceil_floor_neq.
rewrite Hm.
replace (Rcompare (x - Z2R m) (/2)) with l'.
replace (Rcompare (x - IZR m) (/2)) with l'.
now case l'.
rewrite <- Hl'.
rewrite Z2R_plus.
rewrite <- (Rcompare_plus_r (- Z2R m) x).
rewrite plus_IZR.
rewrite <- (Rcompare_plus_r (- IZR m) x).
apply f_equal.
simpl (Z2R 1).
simpl (IZR 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
......@@ -520,11 +520,11 @@ erewrite inbetween_int_N_sign with (choice := Zle_bool 0).
apply f_equal.
assert (Hm: (0 <= m)%Z).
apply Zlt_succ_le.
apply lt_Z2R.
apply lt_IZR.
apply Rle_lt_trans with (Rabs x).
apply Rabs_pos.
refine (proj2 (inbetween_bounds _ _ _ _ _ Hl)).
apply Z2R_lt.
apply IZR_lt.
apply Zlt_succ.
rewrite Zle_bool_true with (1 := Hm).
rewrite Zle_bool_false.
......@@ -648,8 +648,8 @@ unfold k. ring.
refine (conj _ H).
rewrite <- H.
apply F2R_eq_compat.
replace (scaled_mantissa beta fexp x) with (Z2R (Zfloor (scaled_mantissa beta fexp x))).
rewrite Ztrunc_Z2R.
replace (scaled_mantissa beta fexp x) with (IZR (Zfloor (scaled_mantissa beta fexp x))).
rewrite Ztrunc_IZR.
unfold scaled_mantissa.
rewrite <- H.
unfold x, F2R. simpl.
......@@ -663,7 +663,7 @@ intros H.
generalize (Zpower_pos_gt_0 beta k) (Zle_bool_imp_le _ _ (radix_prop beta)).
omega.
rewrite scaled_mantissa_generic with (1 := Fx).
now rewrite Zfloor_Z2R.
now rewrite Zfloor_IZR.
(* *)
split.
apply refl_equal.
......@@ -848,7 +848,7 @@ rewrite Hl.
replace (choice m loc_Exact) with m.
rewrite <- H.
apply round_generic...
rewrite <- (Zrnd_Z2R rnd m) at 1.
rewrite <- (Zrnd_IZR rnd m) at 1.
apply inbetween_int_valid.
now constructor.
Qed.
......@@ -914,11 +914,11 @@ destruct (Rlt_bool_spec x 0) as [Zx|Zx].
(* . *)
apply Zopp_inj.
change (- m = cond_Zopp true (choice true m loc_Exact))%Z.
rewrite <- (Zrnd_Z2R rnd (-m)) at 1.
assert (Z2R (-m) < 0)%R.
rewrite Z2R_opp.
rewrite <- (Zrnd_IZR rnd (-m)) at 1.
assert (IZR (-m) < 0)%R.
rewrite opp_IZR.
apply Ropp_lt_gt_0_contravar.
apply (Z2R_lt 0).
apply (IZR_lt 0).
apply F2R_gt_0_reg with beta e.
rewrite <- H.
apply Rabs_pos_lt.
......@@ -927,13 +927,13 @@ rewrite <- Rlt_bool_true with (1 := H0).
apply inbetween_int_valid.
constructor.
rewrite Rabs_left with (1 := H0).
rewrite Z2R_opp.
rewrite opp_IZR.
apply Ropp_involutive.
(* . *)
change (m = cond_Zopp false (choice false m loc_Exact))%Z.
rewrite <- (Zrnd_Z2R rnd m) at 1.
assert (0 <= Z2R m)%R.
apply (Z2R_le 0).
rewrite <- (Zrnd_IZR rnd m) at 1.
assert (0 <= IZR m)%R.
apply (IZR_le 0).
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 (Z2R_le 0) ; apply Zlt_le_weak.
2: now apply (IZR_le 0) ; apply 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.
......@@ -168,56 +168,56 @@ apply bpow_gt_0.
rewrite Hq.
case Zeq_bool_spec ; intros Hr'.
(* .. r = 0 *)
rewrite Hr', Zplus_0_r, Z2R_mult.
fold (Rsqr (Z2R q)).
rewrite Hr', Zplus_0_r, mult_IZR.
fold (Rsqr (IZR q)).
rewrite sqrt_Rsqr.
now constructor.
apply (Z2R_le 0).
apply (IZR_le 0).
omega.
(* .. r <> 0 *)
constructor.
split.
(* ... bounds *)
apply Rle_lt_trans with (sqrt (Z2R (q * q))).
rewrite Z2R_mult.
fold (Rsqr (Z2R q)).
apply Rle_lt_trans with (sqrt (IZR (q * q))).
rewrite mult_IZR.
fold (Rsqr (IZR q)).
rewrite sqrt_Rsqr.
apply Rle_refl.
apply (Z2R_le 0).
apply (IZR_le 0).
omega.
apply sqrt_lt_1.
rewrite Z2R_mult.
rewrite mult_IZR.
apply Rle_0_sqr.
rewrite <- Hq.
apply (Z2R_le 0).
apply (IZR_le 0).
now apply Zlt_le_weak.
apply Z2R_lt.
apply IZR_lt.
omega.
apply Rlt_le_trans with (sqrt (Z2R ((q + 1) * (q + 1)))).
apply Rlt_le_trans with (sqrt (IZR ((q + 1) * (q + 1)))).
apply sqrt_lt_1.
rewrite <- Hq.
apply (Z2R_le 0).
apply (IZR_le 0).
now apply Zlt_le_weak.
rewrite Z2R_mult.
rewrite mult_IZR.
apply Rle_0_sqr.
apply Z2R_lt.
apply IZR_lt.
ring_simplify.
omega.
rewrite Z2R_mult.
fold (Rsqr (Z2R (q + 1))).
rewrite mult_IZR.
fold (Rsqr (IZR (q + 1))).
rewrite sqrt_Rsqr.
apply Rle_refl.
apply (Z2R_le 0).
apply (IZR_le 0).
omega.
(* ... location *)
rewrite Rcompare_half_r.
rewrite <- Rcompare_sqr.
replace ((2 * sqrt (Z2R (q * q + r))) * (2 * sqrt (Z2R (q * q + r))))%R
with (4 * Rsqr (sqrt (Z2R (q * q + r))))%R by (unfold Rsqr ; ring).
replace ((2 * sqrt (IZR (q * q + r))) * (2 * sqrt (IZR (q * q + r))))%R
with (4 * Rsqr (sqrt (IZR (q * q + r))))%R by (unfold Rsqr ; ring).
rewrite Rsqr_sqrt.
change 4%R with (Z2R 4).
rewrite <- Z2R_plus, <- 2!Z2R_mult.
rewrite Rcompare_Z2R.
change 4%R with (IZR 4).
rewrite <- plus_IZR, <- 2!mult_IZR.
rewrite Rcompare_IZR.
replace ((q + (q + 1)) * (q + (q + 1)))%Z with (4 * (q * q) + 4 * q + 1)%Z by ring.
generalize (Zle_cases r q).