Commit fd74178e authored by BOLDO Sylvie's avatar BOLDO Sylvie

A little Axpy

parent bb571876
......@@ -12,6 +12,64 @@ Variable Hp : Zlt 0 prec.
Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exponent beta (FLX_exp prec)).
Notation ulp := (ulp beta (FLX_exp prec)).
Definition MinOrMax x f :=
((f = rounding beta (FLX_exp prec) ZrndDN x)
\/ (f = rounding beta (FLX_exp prec) ZrndUP x)).
Theorem MinOrMax_opp: forall x f,
MinOrMax x f <-> MinOrMax (-x) (-f).
assert (forall x f, MinOrMax x f -> MinOrMax (- x) (- f)).
unfold MinOrMax; intros x f [H|H].
now rewrite H, rounding_UP_opp.
now rewrite H, rounding_DN_opp.
intros x f; split; intros H1.
now apply H.
rewrite <- (Ropp_involutive x), <- (Ropp_involutive f).
now apply H.
Theorem implies_MinOrMax_le:
forall x f, format f ->
(f <= x)%R ->
(Rabs (f-x) < ulp x)%R ->
MinOrMax x f.
intros x f Hf Hxf1 Hxf2.
left; apply sym_eq.
apply Rnd_DN_pt_unicity with format x.
apply generic_DN_pt.
now apply FLX_exp_correct.
intros g Hg Hxg.
case (Rle_or_lt g f); trivial; intros Hfg.
contradict Hxf2.
apply Rle_not_lt.
rewrite Rabs_left1.
2: apply Rle_minus; assumption.
replace (-(f-x))%R with ((x-g)+(g-f))%R by ring.
rewrite <- (Rplus_0_l (ulp x)).
apply Rplus_le_compat.
apply Rle_0_minus; assumption.
Theorem implies_MinOrMax_quarter:
forall x f, format f ->
(Rabs (f-x) < /4* ulp x)%R ->
MinOrMax x f.
intros x f Hf Hxf.
Variable choice : R -> bool.
......@@ -23,9 +81,7 @@ Hypothesis Hy: format y.
Notation t := (rounding beta (FLX_exp prec) (ZrndN choice) (a*x)).
Notation u := (rounding beta (FLX_exp prec) (ZrndN choice) (t+y)).
Notation MinOrMax x f :=
((f = rounding beta (FLX_exp prec) ZrndUP x)
\/ (f = rounding beta (FLX_exp prec) ZrndDN x)).
Theorem Axpy_opt :
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