Commit c8016fa9 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Proved Rnd_ZR_pt_monotone and satisfies_any_imp_ZR.

parent 417753b7
......@@ -54,13 +54,13 @@ Theorem satisfies_any_imp_UP :
satisfies_any F ->
rounding_pred (Rnd_UP_pt F).
Proof.
intros F Hsat.
intros F Hany.
split.
intros x.
destruct (rounding_val_of_pred (Rnd_DN_pt F) (satisfies_any_imp_DN F Hsat) (-x)) as (f, Hf).
destruct (proj1 (satisfies_any_imp_DN F Hany) (-x)) as (f, Hf).
exists (-f).
apply Rnd_DN_UP_pt_sym.
apply Hsat.
apply Hany.
now rewrite Ropp_involutive.
apply Rnd_UP_pt_monotone.
Qed.
......@@ -68,34 +68,41 @@ Qed.
Theorem satisfies_any_imp_ZR :
forall F : R -> Prop,
satisfies_any F ->
{ rnd : R -> R | Rnd_ZR F rnd }.
rounding_pred (Rnd_ZR_pt F).
Proof.
intros F S.
destruct (rounding_fun_of_pred _ (satisfies_any_imp_DN F S)) as (rndd, Hd).
destruct (rounding_fun_of_pred _ (satisfies_any_imp_UP F S)) as (rndu, Hu).
exists (fun x =>
match Rle_dec 0 x with
| left _ => rndd x
| right _ => rndu x
end).
intros F Hany.
split.
intros x.
destruct (Rle_dec 0 x) as [Hx|Hx] ; split.
(* positive or zero *)
intros _.
apply Hd.
destruct (Rle_or_lt 0 x) as [Hx|Hx].
(* positive *)
destruct (proj1 (satisfies_any_imp_DN F Hany) x) as (f, Hf).
exists f.
split.
now intros _.
intros Hx'.
replace x with 0 by now apply Rle_antisym.
generalize S. intros (S0,_,_).
rewrite Rnd_0 with F rndd ; trivial.
repeat split ; auto with real.
(* zero *)
assert (x = 0).
now apply Rle_antisym.
rewrite H in Hf |- *.
clear Hx Hx'.
rewrite Rnd_DN_pt_idempotent with (1 := Hf).
split.
now apply Rnd_DN_monotone with F.
now apply Rnd_DN_idempotent.
apply Hany.
split.
apply Rle_refl.
now intros.
apply Hany.
(* negative *)
destruct (proj1 (satisfies_any_imp_UP F Hany) x) as (f, Hf).
exists f.
split.
intros Hx'.
elim (Hx Hx').
intros Hx'.
apply Hu.
elim (Rlt_irrefl 0).
now apply Rle_lt_trans with x.
now intros _.
(* . *)
apply Rnd_ZR_pt_monotone.
apply Hany.
Qed.
Theorem satisfies_any_imp_NG :
......
......@@ -396,6 +396,32 @@ auto with real.
apply (proj2 (H x)) ; auto with real.
Qed.
Theorem Rnd_ZR_pt_monotone :
forall F : R -> Prop, F 0 ->
rounding_pred_monotone (Rnd_ZR_pt F).
Proof.
intros F F0 x y f g (Hx1, Hx2) (Hy1, Hy2) Hxy.
destruct (Rle_or_lt 0 x) as [Hx|Hx].
(* . *)
apply Hy1.
now apply Rle_trans with x.
now apply Hx1.
apply Rle_trans with (2 := Hxy).
now apply Hx1.
(* . *)
apply Rlt_le in Hx.
destruct (Rle_or_lt 0 y) as [Hy|Hy].
apply Rle_trans with 0.
now apply Hx2.
now apply Hy1.
apply Rlt_le in Hy.
apply Hx2.
exact Hx.
now apply Hy2.
apply Rle_trans with (1 := Hxy).
now apply Hy2.
Qed.
Theorem Rnd_N_pt_DN_or_UP :
forall F : R -> Prop,
forall x f : R,
......
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