Commit 4161c990 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make compatible with future version of IZR.

parent b28d90f7
......@@ -1392,20 +1392,20 @@ apply Z.le_max_r.
unfold b, average3.
rewrite J1,J3,J2,J4,T1,T2; unfold F2R; simpl.
rewrite Rmult_0_l, Rplus_0_r.
replace (0 - -1 * bpow emin) with (bpow emin) by ring.
rewrite (round_generic _ _ _ (bpow (emin)))...
replace (0 - _ * bpow emin) with (bpow emin) by ring.
rewrite (round_generic _ _ _ (bpow emin))...
2: apply FLT_format_bpow...
2: omega.
rewrite G1.
replace (-1 * bpow emin + 0) with (-bpow emin) by ring.
replace (_ * bpow emin + 0) with (-bpow emin) by ring.
rewrite round_generic...
2: apply generic_format_opp.
2: apply FLT_format_bpow...
2: omega.
replace (- bpow emin - -1 * bpow emin / 2) with (-((bpow emin)/2)) by field.
replace (- bpow emin - _ * bpow emin / 2) with (-(bpow emin/2)) by field.
rewrite Rabs_Ropp.
rewrite Rabs_right.
replace (-1 * bpow emin / 2) with (-((bpow emin/2))) by field.
replace (_ * bpow emin / 2) with (-(bpow emin/2)) by field.
rewrite ulp_opp.
apply Rle_trans with ((3*ulp_flt (bpow emin / 2))/2);[idtac|right; unfold Rdiv; ring].
unfold Rdiv; apply Rmult_le_compat_r.
......
......@@ -403,7 +403,7 @@ Definition Z2R n :=
match n with
| Zpos p => P2R p
| Zneg p => Ropp (P2R p)
| Z0 => R0
| Z0 => 0%R
end.
Theorem P2R_INR :
......@@ -432,10 +432,13 @@ Theorem Z2R_IZR :
forall n, Z2R n = IZR n.
Proof.
intro.
case n ; intros ; simpl.
case n ; intros ; unfold Z2R.
apply refl_equal.
rewrite <- positive_nat_Z, <- INR_IZR_INZ.
apply P2R_INR.
change (IZR (Zneg p)) with (Ropp (IZR (Zpos p))).
apply Ropp_eq_compat.
rewrite <- positive_nat_Z, <- INR_IZR_INZ.
apply P2R_INR.
Qed.
......@@ -1193,7 +1196,7 @@ unfold Ztrunc.
case Rlt_bool_spec ; intro H.
apply refl_equal.
rewrite (Rle_antisym _ _ Hx H).
fold (Z2R 0).
change 0%R with (Z2R 0).
rewrite Zceil_Z2R.
apply Zfloor_Z2R.
Qed.
......@@ -1304,7 +1307,7 @@ unfold Zaway.
case Rlt_bool_spec ; intro H.
apply refl_equal.
rewrite (Rle_antisym _ _ Hx H).
fold (Z2R 0).
change 0%R with (Z2R 0).
rewrite Zfloor_Z2R.
apply Zceil_Z2R.
Qed.
......
......@@ -755,7 +755,7 @@ Theorem round_0 :
Proof.
unfold round, scaled_mantissa.
rewrite Rmult_0_l.
fold (Z2R 0).
change 0%R with (Z2R 0).
rewrite Zrnd_Z2R.
apply F2R_0.
Qed.
......@@ -1177,7 +1177,7 @@ rewrite <- (Rmult_0_l (bpow (- canonic_exp x))).
apply Rmult_le_compat_r with (2 := Hx).
apply bpow_ge_0.
rewrite <- H.
change R0 with (Z2R 0).
change 0%R with (Z2R 0).
now rewrite Zfloor_Z2R, Zceil_Z2R.
Qed.
......@@ -1212,7 +1212,7 @@ rewrite <- (Rmult_0_l (bpow (- canonic_exp x))).
apply Rmult_le_compat_r with (2 := Hx).
apply bpow_ge_0.
rewrite <- H.
change R0 with (Z2R 0).
change 0%R with (Z2R 0).
now rewrite Zfloor_Z2R, Zceil_Z2R.
Qed.
......
......@@ -370,7 +370,7 @@ destruct (Rle_or_lt (round beta fexp Zfloor x) 0) as [Hr|Hr].
rewrite (Rle_antisym _ _ Hr).
unfold scaled_mantissa.
rewrite Rmult_0_l.
change R0 with (Z2R 0).
change 0%R with (Z2R 0).
now rewrite (Ztrunc_Z2R 0).
rewrite <- (round_0 beta fexp Zfloor).
apply round_le...
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment