Commit 42118aed authored by BOLDO Sylvie's avatar BOLDO Sylvie

I need the predecessor :-/

parent 3d44b057
......@@ -8,7 +8,7 @@ Notation bpow e := (bpow beta e).
Variable prec : Z.
Variable Hp : Zlt 0 prec.
(* FLX ou FLT ? *)
(* FLX ou FLT ou aussi FTZ ou ? *)
Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exponent beta (FLX_exp prec)).
......@@ -33,7 +33,7 @@ now apply H.
Qed.
Theorem implies_DN_lt_ulp_f:
Theorem implies_DN_lt_ulp:
forall x f, format f ->
(0 < f <= x)%R ->
(Rabs (f-x) < ulp f)%R ->
......@@ -49,22 +49,47 @@ rewrite Rabs_left1; trivial.
now apply Rle_minus.
Qed.
Theorem implies_DN_lt_ulp:
Theorem implies_MinOrMax_not_bpow:
forall x f, format f ->
(0 < f <= x)%R ->
(Rabs (f-x) < ulp x)%R ->
(f = rounding beta (FLX_exp prec) ZrndDN x)%R.
intros x f Hf Hxf1 Hxf2.
apply implies_DN_lt_ulp_f; trivial.
Admitted.
(0 < f)%R ->
f <> bpow (projT1 (ln_beta beta f)) ->
(Rabs (f-x) < ulp f)%R ->
MinOrMax x f.
intros x f Hf1 Hf2 Hf3 Hxf1.
case (Rlt_or_le x f); intros Hxf2.
(* *)
(* assert (ulp (f-ulp f) = ulp f)%R.
admit.
right; apply sym_eq.
replace f with ((f-ulp f) + (ulp (f-ulp f)))%R.
2: rewrite H; ring.
replace x with ((f-ulp f)+-(f-ulp f-x))%R by ring.
apply rounding_UP_succ; trivial.
apply Hxf1.
replace (- (f - x))%R with (Rabs (f-x)).
split; trivial; apply Rabs_pos.
rewrite Rabs_left1; trivial.
now apply Rle_minus.
*)
Theorem implies_MinOrMax_quarter:
admit.
(* *)
left.
apply implies_DN_lt_ulp; try split; easy.
Qed.
Theorem implies_MinOrMax_bpow:
forall x f, format f ->
(Rabs (f-x) < /4* ulp x)%R ->
f = bpow (projT1 (ln_beta beta f)) ->
(Rabs (f-x) < /2* ulp f)%R ->
MinOrMax x f.
intros x f Hf Hxf.
intros x f Hf1 Hf2 Hxf.
Admitted.
......
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