Commit 022240d7 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Modified ulp_pred_succ_pt so that it directly describes the next rounded value.

parent 0e06838e
......@@ -140,6 +140,9 @@ apply Hxd.
apply generic_format_0.
now apply Rlt_le.
assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now eapply valid_fexp.
assert (Hud: (F2R xu = F2R xd + ulp beta fexp x)%R).
apply Rnd_UP_pt_unicity with (1 := Hxu).
now apply ulp_DN_UP_pt.
destruct (total_order_T (bpow ex) (F2R xu)) as [[Hu2|Hu2]|Hu2].
(* - xu > bpow ex *)
elim (Rlt_not_le _ _ Hu2).
......@@ -166,8 +169,6 @@ apply F2R_bpow.
exact Hxe2.
assert (Hd3: xd = Float beta (Zpower (radix_val beta) (ex - fexp ex) - 1) (fexp ex)).
assert (H: F2R xd = F2R (Float beta (Zpower (radix_val beta) (ex - fexp ex) - 1) (fexp ex))).
generalize (ulp_pred_succ_pt beta _ valid_fexp x (F2R xd) (F2R xu) Hfx Hxd Hxu).
intros Hud.
unfold F2R. simpl.
rewrite minus_Z2R.
unfold Rminus.
......@@ -209,7 +210,7 @@ apply Zodd_Zpower with (2 := Hdo).
apply Zle_minus_le_0.
exact Hxe2.
(* - xu < bpow ex *)
generalize (ulp_pred_succ_pt beta _ valid_fexp x (F2R xd) (F2R xu) Hfx Hxd Hxu).
revert Hud.
unfold ulp, F2R.
rewrite Hd, Hu.
unfold canonic_exponent.
......
......@@ -18,18 +18,21 @@ Definition ulp x := bpow (canonic_exponent beta fexp x).
Definition F := generic_format beta fexp.
Theorem ulp_pred_succ_pt :
forall x xd xu,
Theorem ulp_DN_UP_pt :
forall x xd,
~ F x ->
Rnd_DN_pt F x xd -> Rnd_UP_pt F x xu ->
(xu = xd + ulp x)%R.
Rnd_DN_pt F x xd ->
Rnd_UP_pt F x (xd + ulp x)%R.
Proof.
intros x xd xu Fx Hd1 Hu1.
intros x xd Fx Hd1.
set (ex := canonic_exponent beta fexp x).
assert (Hd2 := generic_DN_pt beta _ prop_exp x).
assert (Hu2 := generic_UP_pt beta _ prop_exp x).
generalize (generic_UP_pt beta _ prop_exp x).
fold ex in Hd2 |- *.
replace (F2R (Float beta (Zceil (x * bpow (- ex))) ex)) with (xd + ulp x)%R.
easy.
rewrite (Rnd_DN_pt_unicity _ _ _ _ Hd1 Hd2).
rewrite (Rnd_UP_pt_unicity _ _ _ _ Hu1 Hu2).
unfold ulp.
unfold ulp. fold ex.
unfold F2R. simpl.
rewrite Zceil_floor_neq.
rewrite plus_Z2R. simpl.
......@@ -38,6 +41,7 @@ intros H.
apply Fx.
unfold F, generic_format.
unfold F2R. simpl.
fold ex.
rewrite <- H.
rewrite Ztrunc_Z2R.
rewrite H.
......@@ -62,7 +66,8 @@ apply Rlt_not_le with (1 := Hxd).
apply Req_le.
apply sym_eq.
now apply Rnd_DN_pt_idempotent with (1 := Hd).
destruct (proj1 (satisfies_any_imp_UP F Hs) x) as (u, Hu).
assert (Hu := ulp_DN_UP_pt _ _ Fx Hd).
set (u := (d + ulp x)%R).
assert (Hxu : (x < u)%R).
destruct (Rle_lt_or_eq_dec x u) as [Hxu|Hxu].
apply Hu.
......@@ -70,7 +75,6 @@ exact Hxu.
elim Fx.
rewrite Hxu.
apply Hu.
rewrite (ulp_pred_succ_pt _ _ _ Fx Hd Hu) in Hxu, Hu.
destruct (Rnd_DN_or_UP_pt _ _ Hrnd _ _ _ Hd Hu) as [Hr|Hr] ;
rewrite Hr ; clear Hr.
rewrite <- Ropp_minus_distr.
......@@ -111,8 +115,7 @@ apply Rlt_not_le with (1 := Hxd).
apply Req_le.
apply sym_eq.
now apply Rnd_DN_pt_idempotent with (1 := Hd).
destruct (proj1 (satisfies_any_imp_UP F Hs) x) as (u, Hu).
rewrite (ulp_pred_succ_pt _ _ _ Fx Hd Hu) in Hu.
assert (Hu := ulp_DN_UP_pt _ _ Fx Hd).
destruct Hxr as (Hr1, Hr2).
assert (Hdx : (Rabs (d - x) = x - d)%R).
rewrite <- Ropp_minus_distr.
......
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