Commit 19801404 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Uniformize a few names.

parent 7f989b09
......@@ -519,8 +519,11 @@ now apply Rcompare_Eq.
now apply Rcompare_Lt.
Qed.
Lemma Rcompare_Ropp x y : Rcompare (- x) (- y) = Rcompare y x.
Lemma Rcompare_opp :
forall x y,
Rcompare (- x) (- y) = Rcompare y x.
Proof.
intros x y.
destruct (Rcompare_spec y x);
destruct (Rcompare_spec (- x) (- y));
try reflexivity; exfalso; lra.
......@@ -752,8 +755,13 @@ rewrite <- negb_Rlt_bool.
now rewrite Rle_bool_true.
Qed.
Lemma Rlt_bool_Ropp x y : Rlt_bool (- x) (- y) = Rlt_bool y x.
Proof. now unfold Rlt_bool; rewrite Rcompare_Ropp. Qed.
Lemma Rlt_bool_opp :
forall x y,
Rlt_bool (- x) (- y) = Rlt_bool y x.
Proof.
intros x y.
now unfold Rlt_bool; rewrite Rcompare_opp.
Qed.
End Rlt_bool.
......
......@@ -2503,14 +2503,16 @@ rewrite Rnd_DN_pt_unique with F x (round beta fexp Zfloor x) d; try assumption.
apply round_DN_pt...
Qed.
Lemma plus_ulp_rnd_ge : forall { Hm : Monotone_exp fexp } choice x,
let rx := round beta fexp (Znearest choice) x in
(x <= round beta fexp (Znearest choice) (rx + ulp rx))%R.
Lemma round_N_plus_ulp_ge :
forall { Hm : Monotone_exp fexp } choice1 choice2 x,
let rx := round beta fexp (Znearest choice2) x in
(x <= round beta fexp (Znearest choice1) (rx + ulp rx))%R.
Proof.
intros Hm choice x.
intros Hm choice1 choice2 x.
simpl.
set (rx := round _ _ _ x).
assert (Vrnd : Valid_rnd (Znearest choice)); [now apply valid_rnd_N|].
assert (Vrnd1 : Valid_rnd (Znearest choice1)) by now apply valid_rnd_N.
assert (Vrnd2 : Valid_rnd (Znearest choice2)) by now apply valid_rnd_N.
apply (Rle_trans _ (succ rx)); [now apply succ_round_ge_id|].
rewrite round_generic; [now apply succ_le_plus_ulp|now simpl|].
now apply generic_format_plus_ulp, generic_format_round.
......
......@@ -2794,7 +2794,7 @@ intros pred_nan x Fx.
assert (Fox : is_finite (Bopp pred_nan x) = true).
{ now rewrite is_finite_Bopp. }
rewrite <-(Ropp_involutive (B2R x)), <-(B2R_Bopp pred_nan).
rewrite pred_opp, Rlt_bool_Ropp.
rewrite pred_opp, Rlt_bool_opp.
generalize (Bsucc_correct pred_nan _ Fox).
case (Rlt_bool _ _).
- intros (HR, (HF, HS)); unfold Bpred.
......
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