Commit e5dfbe02 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Generalized definition of rounding to nearest.

parent 7cbd3090
......@@ -96,6 +96,20 @@ Definition Rnd_N_pt (F : R -> Prop) (x f : R) :=
Definition Rnd_N (F : R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_N_pt F x (rnd x).
Definition Rnd_N1_pt (F : R -> Prop) (P : R -> Prop) (x f : R) :=
Rnd_N_pt F x f /\
( P f \/ forall f2 : R, Rnd_N_pt F x f2 -> f2 = f ).
Definition Rnd_N1 (F : R -> Prop) (P : R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_N1_pt F P x (rnd x).
Definition Rnd_N2_pt (F : R -> Prop) (P : R -> R -> Prop) (x f : R) :=
Rnd_N_pt F x f /\
forall f2 : R, Rnd_N_pt F x f2 -> P f f2.
Definition Rnd_N2 (F : R -> Prop) (P : R -> R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_N2_pt F P x (rnd x).
Definition Rnd_NA_pt (F : R -> Prop) (x f : R) :=
Rnd_N_pt F x f /\
forall f2 : R, Rnd_N_pt F x f2 ->
......
......@@ -91,18 +91,19 @@ intros Hx'.
apply Hu.
Qed.
Theorem satisfies_any_imp_NA :
forall F : R -> Prop,
Theorem satisfies_any_imp_N2 :
forall (F : R -> Prop) (P : R -> R -> Prop),
satisfies_any F ->
{ rnd : R -> R | Rnd_NA F rnd }.
( forall x d u, Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> { P u d } + { P d u } ) ->
{ rnd : R -> R | Rnd_N2 F P rnd }.
Proof.
intros F Hany.
intros F P Hany HP.
destruct (satisfies_any_imp_DN F Hany) as (rndd, Hd).
destruct (satisfies_any_imp_UP F Hany) as (rndu, Hu).
exists (fun x =>
match total_order_T (Rabs (rndu x - x)) (Rabs (rndd x - x)) with
| inleft (left _ ) => rndu x
| inleft (right _ ) => match (Rle_dec (Rabs (rndd x)) (Rabs (rndu x))) with
| inleft (right _ ) => match HP x _ _ (Hd _) (Hu _) with
left _ => rndu x
| right _ => rndd x
end
......@@ -111,7 +112,7 @@ exists (fun x =>
split.
(* *** nearest *)
destruct (total_order_T (Rabs (rndu x - x)) (Rabs (rndd x - x))) as [[H|H]|H].
(* |up(x) - x| < [dn(x) - x| *)
(* |up(x) - x| < |dn(x) - x| *)
destruct (Hu x) as (H3,(H4,H5)).
split.
exact H3.
......@@ -130,7 +131,7 @@ rewrite Rabs_right.
rewrite Rabs_right.
apply Rplus_le_compat_l.
apply Ropp_le_contravar.
now eapply Hd ;auto with real.
now eapply Hd ; try apply Rlt_le.
apply Rge_minus.
apply Rle_ge.
now left.
......@@ -138,8 +139,8 @@ apply Rge_minus.
apply Rle_ge.
now eapply Hd.
(* |up(x) - x| = [dn(x) - x| *)
destruct (Rle_dec (Rabs (rndd x)) (Rabs (rndu x))) as [H'|H'].
(* - |dn(x)| <= |up(x)| *)
destruct (HP x _ _ (Hd x) (Hu x)) as [H'|H'].
(* - u >> d *)
split.
now eapply Hu.
intros.
......@@ -166,7 +167,7 @@ now left.
apply Rge_minus.
apply Rle_ge.
now eapply Hd.
(* - |dn(x)| > |up(x)| *)
(* - d >> u *)
split.
now eapply Hd.
intros.
......@@ -185,11 +186,12 @@ rewrite Rabs_left1.
rewrite Rabs_left1.
apply Ropp_le_contravar.
apply Rplus_le_compat_r.
now eapply Hd ; auto with real.
auto with real.
now eapply Hd ; try apply Rlt_le.
apply Rle_minus.
now apply Rlt_le.
apply Rle_minus.
now eapply Hd.
(* |up(x) - x| > [dn(x) - x| *)
(* |up(x) - x| > |dn(x) - x| *)
destruct (Hd x) as (H3,(H4,H5)).
split.
exact H3.
......@@ -208,29 +210,87 @@ now eapply Hu.
repeat rewrite Rabs_left1.
apply Ropp_le_contravar.
apply Rplus_le_compat_r.
now eapply Hd ; auto with real.
auto with real.
now eapply Hd ; try apply Rlt_le.
apply Rle_minus.
now apply Rlt_le.
apply Rle_minus.
now eapply Hd.
(* *** away *)
intros f Hf.
destruct (Rnd_N_pt_DN_or_UP_eq F x (rndd x) (rndu x) f) as [K|K] ; trivial.
rewrite K.
destruct (total_order_T (Rabs (rndu x - x)) (Rabs (rndd x - x))) as [[H|H]|H] ;
try apply Rle_refl.
assert (HPr: forall x, F x -> P x x).
clear -HP.
intros x HF.
destruct (HP x x x) as [H|H] ;
repeat split ; trivial ; apply Rle_refl.
destruct (Rnd_N_pt_DN_or_UP_eq F x _ _ f (Hd x) (Hu x) Hf) as [K|K] ; rewrite K.
destruct (total_order_T (Rabs (rndu x - x)) (Rabs (rndd x - x))) as [[H|H]|H].
elim Rlt_not_le with (1 := H).
rewrite <- K.
apply Hf.
eapply Hu.
destruct (Rle_dec (Rabs (rndd x)) (Rabs (rndu x))) ; auto with real.
rewrite K.
destruct (total_order_T (Rabs (rndu x - x)) (Rabs (rndd x - x))) as [[H|H]|H] ;
try apply Rle_refl.
destruct (Rle_dec (Rabs (rndd x)) (Rabs (rndu x))) ; auto with real.
destruct (HP x _ _ (Hd x) (Hu x)) as [H'|H'].
exact H'.
apply HPr.
eapply Hd.
apply HPr.
eapply Hd.
destruct (total_order_T (Rabs (rndu x - x)) (Rabs (rndd x - x))) as [[H|H]|H].
apply HPr.
eapply Hu.
destruct (HP x _ _ (Hd x) (Hu x)) as [H'|H'].
apply HPr.
eapply Hu.
exact H'.
elim Rgt_not_le with (1 := H).
rewrite <- K.
apply Hf.
eapply Hd.
Qed.
Theorem satisfies_any_imp_N1 :
forall (F : R -> Prop) (P : R -> Prop),
satisfies_any F ->
( forall x, F x -> P x \/ ~ P x ) ->
( forall x d u, ~ F x -> Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> { P d } + { P u } ) ->
{ rnd : R -> R | Rnd_N1 F P rnd }.
Proof.
intros F P Hany EM HP.
destruct (satisfies_any_imp_N2 F (fun f g => P f \/ g = f) Hany) as (rnd, Hr).
(* . *)
intros x d u Hxd Hxu.
destruct (Req_EM_T d u) as [Hdu|Hdu].
now left ; right.
destruct (HP x d u) as [H|H] ; trivial.
intros HF.
apply Hdu.
apply trans_eq with x.
now apply Rnd_DN_pt_idempotent with F.
apply sym_eq.
now apply Rnd_UP_pt_idempotent with F.
now right ; left.
now left ; left.
(* . *)
exists rnd.
intros x.
apply <- Rnd_N1_N2_pt.
apply (Hr x).
intros f g Hf Hg.
apply iff_refl.
exact EM.
Qed.
Theorem satisfies_any_imp_NA :
forall F : R -> Prop,
satisfies_any F ->
{ rnd : R -> R | Rnd_NA F rnd }.
Proof.
intros F Hany.
apply (satisfies_any_imp_N2 F (fun a b => (Rabs b <= Rabs a)%R) Hany).
intros x d u Hxd Hxu.
destruct (Rle_lt_dec (Rabs d) (Rabs u)) as [H|H].
now left.
right.
now apply Rlt_le.
Qed.
End RND_ex.
......@@ -532,55 +532,144 @@ now rewrite <- Hx.
exact HF.
Qed.
Theorem Rnd_NA_pt_monotone :
Theorem Rnd_N1_N2_pt :
forall F : R -> Prop,
F 0 ->
forall (P1 : R -> Prop) (P2 : R -> R -> Prop),
( forall h, F h -> P1 h \/ ~P1 h ) ->
( forall f g, F f -> F g -> (P1 f \/ g = f <-> P2 f g) ) ->
forall x f,
Rnd_N1_pt F P1 x f <-> Rnd_N2_pt F P2 x f.
Proof.
intros F P1 P2 HP1 HP12 x f.
split ; intros (H, Hf) ; ( split ; [ exact H | .. ] ).
(* . *)
intros g Hg.
apply (proj1 (HP12 _ _ (proj1 H) (proj1 Hg))).
destruct Hf as [Hf|Hf].
now left.
right.
now apply Hf.
(* . *)
destruct (HP1 _ (proj1 H)) as [H1|H1].
now left.
right.
intros f2 H2.
destruct (proj2 (HP12 _ _ (proj1 H) (proj1 H2))) as [H3|H3].
now apply Hf.
now elim H1.
exact H3.
Qed.
Definition Rnd_N1_pt_unicity_prop F P :=
forall x d u, Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> P d -> P u -> d = u.
Theorem Rnd_N1_pt_unicity :
forall (F : R -> Prop) (P : R -> Prop),
Rnd_N1_pt_unicity_prop F P ->
forall x f1 f2 : R,
Rnd_N1_pt F P x f1 -> Rnd_N1_pt F P x f2 ->
f1 = f2.
Proof.
intros F P HP x f1 f2 (H1a,H1b) (H2a,H2b).
destruct H1b as [H1b|H1b].
destruct H2b as [H2b|H2b].
destruct (Rnd_N_pt_DN_or_UP _ _ _ H1a) as [H1c|H1c] ;
destruct (Rnd_N_pt_DN_or_UP _ _ _ H2a) as [H2c|H2c].
eapply Rnd_DN_pt_unicity ; eassumption.
now apply (HP x f1 f2).
apply sym_eq.
now apply (HP x f2 f1 H2c H1c).
eapply Rnd_UP_pt_unicity ; eassumption.
now apply H2b.
apply sym_eq.
now apply H1b.
Qed.
Theorem Rnd_N1_pt_monotone :
forall (F : R -> Prop) (P : R -> Prop),
Rnd_N1_pt_unicity_prop F P ->
forall x y f g : R,
Rnd_NA_pt F x f -> Rnd_NA_pt F y g ->
Rnd_N1_pt F P x f -> Rnd_N1_pt F P y g ->
x <= y -> f <= g.
Proof.
intros F HF x y f g (Hf,Hx) (Hg,Hy) [Hxy|Hxy].
intros F P HP x y f g (Hf,Hx) (Hg,Hy) [Hxy|Hxy].
now apply Rnd_N_pt_monotone with F x y.
apply Req_le.
rewrite <- Hxy in Hg, Hy.
clear y Hxy.
assert (K: f = g \/ f = -g).
apply Rabs_eq_Rabs.
apply Rle_antisym.
now apply Hy.
now apply Hx.
destruct K as [K|K].
eapply Rnd_N1_pt_unicity ; try split ; eassumption.
Qed.
Definition Rnd_N2_pt_unicity_prop F P :=
forall x d u, Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> P d u -> P u d -> d = u.
Theorem Rnd_N2_pt_unicity :
forall (F : R -> Prop) (P : R -> R -> Prop),
Rnd_N2_pt_unicity_prop F P ->
forall x f1 f2 : R,
Rnd_N2_pt F P x f1 -> Rnd_N2_pt F P x f2 ->
f1 = f2.
Proof.
intros F P HP x f1 f2 (H1a,H1b) (H2a,H2b).
destruct (Rnd_N_pt_DN_or_UP _ _ _ H1a) as [H1c|H1c] ;
destruct (Rnd_N_pt_DN_or_UP _ _ _ H2a) as [H2c|H2c].
eapply Rnd_DN_pt_unicity ; eassumption.
apply (HP x f1 f2 H1c H2c).
now apply H1b.
now apply H2b.
apply sym_eq.
apply (HP x f2 f1 H2c H1c).
now apply H2b.
now apply H1b.
eapply Rnd_UP_pt_unicity ; eassumption.
Qed.
Theorem Rnd_N2_pt_monotone :
forall (F : R -> Prop) (P : R -> R -> Prop),
Rnd_N2_pt_unicity_prop F P ->
forall x y f g : R,
Rnd_N2_pt F P x f -> Rnd_N2_pt F P y g ->
x <= y -> f <= g.
Proof.
intros F P HP x y f g (Hf,Hx) (Hg,Hy) [Hxy|Hxy].
now apply Rnd_N_pt_monotone with F x y.
apply Req_le.
rewrite <- Hxy in Hg, Hy.
eapply Rnd_N2_pt_unicity ; try split ; eassumption.
Qed.
Theorem Rnd_NA_pt_monotone :
forall F : R -> Prop,
F 0 ->
forall x y f g : R,
Rnd_NA_pt F x f -> Rnd_NA_pt F y g ->
x <= y -> f <= g.
Proof.
intros F HF x y f g Hxf Hyg Hxy.
apply Rnd_N2_pt_monotone with F (fun a b => (Rabs b <= Rabs a)%R) x y ; try assumption.
clear -HF.
intros x d u Hd Hu Hud Hdu.
destruct (Rabs_eq_Rabs d u) as [K|K].
now apply Rle_antisym.
exact K.
rewrite K.
rewrite K in Hf.
clear f Hx Hy K.
unfold Rnd_N_pt in Hf, Hg.
assert (L: g + x = g - x \/ g + x = x - g).
rewrite <- (Ropp_minus_distr g x).
apply Rabs_eq_Rabs.
rewrite <- Rabs_Ropp.
rewrite Ropp_plus_distr.
fold (-g - x).
clear Hud Hdu.
apply Rle_antisym.
now apply Hf.
now apply Hg.
destruct L as [L|L].
assert (g = 0).
apply Rnd_N_pt_idempotent with F.
replace 0 with x.
exact Hg.
apply Rmult_eq_reg_l with 2.
rewrite Rmult_0_r.
rewrite <- (Rminus_diag_eq _ _ L).
ring.
now apply (Z2R_neq 2 0).
apply Rle_trans with x.
apply Hd.
apply Hu.
destruct (Rle_or_lt u 0) as [H1|H1].
apply Rle_trans with (1 := H1).
rewrite K.
apply Ropp_0_ge_le_contravar.
now apply Rle_ge.
elim Rlt_not_le with (1 := H1).
destruct (Rle_or_lt x 0) as [H2|H2].
now apply Hu.
rewrite <- (Ropp_involutive u), <- K.
apply Rge_le.
apply Ropp_0_le_ge_contravar.
apply Hd.
exact HF.
rewrite H.
apply Ropp_0.
apply Rplus_eq_reg_l with x.
fold (x - g).
rewrite <- L.
apply Rplus_comm.
now apply Rlt_le.
Qed.
Theorem Rnd_NA_monotone :
......
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