Commit 1867c955 authored by BOLDO Sylvie's avatar BOLDO Sylvie

wip rnd_odd

parent 96436d36
......@@ -15,7 +15,7 @@ Variable prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format beta (FLX_exp prec)).
Notation round_flx :=(round beta (FLX_exp prec) ZnearestE).
Notation round_flx :=(round beta (FLX_exp prec) ZnearestE). (*** choice ?? *)
Notation ulp_flx :=(ulp beta (FLX_exp prec)).
Notation pred_flx := (pred beta (FLX_exp prec)).
......@@ -28,6 +28,7 @@ Hypothesis Fx: format x.
Let y:=round_flx(x*x).
Let z:=round_flx(sqrt y).
(* -> Fcore_ulp : rnd_N_le_half_an_ulp and rnd_N_ge_half_an_ulp *)
Theorem round_le_half_an_ulp: forall u v, format u -> 0 < u -> v < u + (ulp_flx u)/2 -> round_flx v <= u.
Proof with auto with typeclass_instances.
......@@ -346,6 +346,7 @@ apply Rgt_not_eq, bpow_gt_0.
End Fcore_rnd_odd.
Section Odd_prop.
Variable beta : radix.
......@@ -363,6 +364,73 @@ Context { exists_NE_e : Exists_NE beta fexpe }.
Hypothesis fexpe_fexp: forall e, (fexpe e <= fexp e -2)%Z. (* ??? *)
Variable choice:Z->bool.
Variable x:R.
Hypothesis xPos: (0 < x)%R.
Let d:= round beta fexp Zfloor x.
Let u:= round beta fexp Zceil x.
Let m:= ((d+u)/2)%R.
Lemma toto: (d<=x<m)%R ->
round beta fexp (Znearest choice) x = d.
Proof with auto with typeclass_instances.
intros H.
apply Rnd_N_pt_unicity with (generic_format beta fexp) x d u.
apply round_DN_pt...
apply round_UP_pt...
intros Y.
absurd (x < m)%R; try apply H.
apply Rle_not_lt; right.
apply Rplus_eq_reg_r with (-x)%R.
apply trans_eq with (- (x-d)/2 + (u-x)/2)%R.
unfold m; field.
rewrite Y; field.
apply round_N_pt...
apply Rnd_DN_UP_pt_N with d u...
apply generic_format_round...
apply round_DN_pt...
apply round_UP_pt...
right; apply trans_eq with (-(d-x))%R;[idtac|ring].
apply Rabs_left1.
apply Rplus_le_reg_l with x; ring_simplify.
apply H.
rewrite Rabs_left1.
apply Rplus_le_reg_l with (d+x)%R.
apply Rmult_le_reg_l with (/2)%R.
auto with real.
apply Rle_trans with x.
right; field.
apply Rle_trans with m.
now left.
right; unfold m; field.
apply Rplus_le_reg_l with x; ring_simplify.
apply H.
; ring_simplify.
SearchAbout Znearest.
SearchPattern (Rnd_N_pt _ _ _).
apply Rle_antisym.
apply rnd_N_le_half_an_ulp...
and rnd_N_ge_half_an_ulp
Theorem rnd_opp: forall x,
round beta fexp ZnearestE (round beta fexpe Zrnd_odd x) =
round beta fexp ZnearestE x.
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