Commit a4ed3d8a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Named property for NG rounding.

parent bdd4d892
......@@ -102,10 +102,13 @@ apply Rnd_ZR_pt_monotone.
apply Hany.
Qed.
Definition NG_existence_prop (F : R -> Prop) (P : R -> R -> Prop) :=
forall x d u, Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> P x u \/ P x d.
Theorem satisfies_any_imp_NG :
forall (F : R -> Prop) (P : R -> R -> Prop),
satisfies_any F ->
( forall x d u, Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> { P x u } + { P x d } ) ->
NG_existence_prop F P ->
rounding_pred_total (Rnd_NG_pt F P).
Proof.
intros F P Hany HP x.
......
......@@ -187,6 +187,17 @@ destruct Hxf as (Hxf1,_).
now apply Rnd_N_pt_idempotent with format.
Qed.
(*
Theorem Rnd_gNE_pt_total :
rounding_pred_total Rnd_gNE_pt.
Proof.
apply satisfies_any_imp_NG.
now apply generic_format_satisfies_any.
unfold NG_existence_prop, gNE_prop.
intros x d u Hd Hu.
Abort.
*)
Definition NE_prop (_ : R) f :=
exists g : float beta, canonic f g /\ Zeven (Fnum g).
......
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