Roundings: properties and/or functions
Require Import Fcore_Raux.
Require Import Fcore_defs.
Section RND_prop.
Open Scope R_scope.
Theorem round_val_of_pred :
forall rnd :
R ->
R ->
Prop,
round_pred rnd ->
forall x, {
f :
R |
rnd x f }.
Proof.
intros rnd (
H1,
H2)
x.
specialize (
H1 x).
. *)
assert (
H3 :
bound (
rnd x)).
destruct H1 as (
f,
H1).
exists f.
intros g Hg.
now apply H2 with (3 :=
Rle_refl x).
. *)
exists (
proj1_sig (
completeness _ H3 H1)).
destruct completeness as (
f1, (
H4,
H5)).
simpl.
destruct H1 as (
f2,
H1).
assert (
f1 =
f2).
apply Rle_antisym.
apply H5.
intros f3 H.
now apply H2 with (3 :=
Rle_refl x).
now apply H4.
now rewrite H.
Qed.
Theorem round_fun_of_pred :
forall rnd :
R ->
R ->
Prop,
round_pred rnd ->
{
f :
R ->
R |
forall x,
rnd x (
f x) }.
Proof.
Theorem round_unicity :
forall rnd :
R ->
R ->
Prop,
round_pred_monotone rnd ->
forall x f1 f2,
rnd x f1 ->
rnd x f2 ->
f1 =
f2.
Proof.
Theorem Rnd_DN_pt_monotone :
forall F :
R ->
Prop,
round_pred_monotone (
Rnd_DN_pt F).
Proof.
intros F x y f g (
Hx1,(
Hx2,
_)) (
Hy1,(
_,
Hy2))
Hxy.
apply Hy2.
apply Hx1.
now apply Rle_trans with (2 :=
Hxy).
Qed.
Theorem Rnd_DN_pt_unicity :
forall F :
R ->
Prop,
forall x f1 f2 :
R,
Rnd_DN_pt F x f1 ->
Rnd_DN_pt F x f2 ->
f1 =
f2.
Proof.
Theorem Rnd_DN_unicity :
forall F :
R ->
Prop,
forall rnd1 rnd2 :
R ->
R,
Rnd_DN F rnd1 ->
Rnd_DN F rnd2 ->
forall x,
rnd1 x =
rnd2 x.
Proof.
Theorem Rnd_UP_pt_monotone :
forall F :
R ->
Prop,
round_pred_monotone (
Rnd_UP_pt F).
Proof.
intros F x y f g (
Hx1,(
_,
Hx2)) (
Hy1,(
Hy2,
_))
Hxy.
apply Hx2.
apply Hy1.
now apply Rle_trans with (1 :=
Hxy).
Qed.
Theorem Rnd_UP_pt_unicity :
forall F :
R ->
Prop,
forall x f1 f2 :
R,
Rnd_UP_pt F x f1 ->
Rnd_UP_pt F x f2 ->
f1 =
f2.
Proof.
Theorem Rnd_UP_unicity :
forall F :
R ->
Prop,
forall rnd1 rnd2 :
R ->
R,
Rnd_UP F rnd1 ->
Rnd_UP F rnd2 ->
forall x,
rnd1 x =
rnd2 x.
Proof.
Theorem Rnd_DN_UP_pt_sym :
forall F :
R ->
Prop,
(
forall x,
F x ->
F (-
x) ) ->
forall x f :
R,
Rnd_DN_pt F x f ->
Rnd_UP_pt F (-
x) (-
f).
Proof.
Theorem Rnd_UP_DN_pt_sym :
forall F :
R ->
Prop,
(
forall x,
F x ->
F (-
x) ) ->
forall x f :
R,
Rnd_UP_pt F x f ->
Rnd_DN_pt F (-
x) (-
f).
Proof.
Theorem Rnd_DN_UP_sym :
forall F :
R ->
Prop,
(
forall x,
F x ->
F (-
x) ) ->
forall rnd1 rnd2 :
R ->
R,
Rnd_DN F rnd1 ->
Rnd_UP F rnd2 ->
forall x,
rnd1 (-
x) = -
rnd2 x.
Proof.
Theorem Rnd_DN_UP_pt_split :
forall F :
R ->
Prop,
forall x d u,
Rnd_DN_pt F x d ->
Rnd_UP_pt F x u ->
forall f,
F f ->
(
f <=
d) \/ (
u <=
f).
Proof.
intros F x d u Hd Hu f Hf.
destruct (
Rle_or_lt f x).
left.
now apply Hd.
right.
assert (
H' :=
Rlt_le _ _ H).
now apply Hu.
Qed.
Theorem Rnd_DN_pt_refl :
forall F :
R ->
Prop,
forall x :
R,
F x ->
Rnd_DN_pt F x x.
Proof.
intros F x Hx.
repeat split.
exact Hx.
apply Rle_refl.
now intros.
Qed.
Theorem Rnd_DN_pt_idempotent :
forall F :
R ->
Prop,
forall x f :
R,
Rnd_DN_pt F x f ->
F x ->
f =
x.
Proof.
intros F x f (
_,(
Hx1,
Hx2))
Hx.
apply Rle_antisym.
exact Hx1.
apply Hx2.
exact Hx.
apply Rle_refl.
Qed.
Theorem Rnd_UP_pt_refl :
forall F :
R ->
Prop,
forall x :
R,
F x ->
Rnd_UP_pt F x x.
Proof.
intros F x Hx.
repeat split.
exact Hx.
apply Rle_refl.
now intros.
Qed.
Theorem Rnd_UP_pt_idempotent :
forall F :
R ->
Prop,
forall x f :
R,
Rnd_UP_pt F x f ->
F x ->
f =
x.
Proof.
intros F x f (
_,(
Hx1,
Hx2))
Hx.
apply Rle_antisym.
apply Hx2.
exact Hx.
apply Rle_refl.
exact Hx1.
Qed.
Theorem Only_DN_or_UP :
forall F :
R ->
Prop,
forall x fd fu f :
R,
Rnd_DN_pt F x fd ->
Rnd_UP_pt F x fu ->
F f -> (
fd <=
f <=
fu)%
R ->
f =
fd \/
f =
fu.
Proof.
intros F x fd fu f Hd Hu Hf [
Hdf Hfu].
destruct (
Rle_or_lt x f) ; [
right|
left].
apply Rle_antisym with (1 :=
Hfu).
now apply Hu.
apply Rlt_le in H.
apply Rle_antisym with (2 :=
Hdf).
now apply Hd.
Qed.
Theorem Rnd_ZR_abs :
forall (
F :
R ->
Prop) (
rnd:
R->
R),
Rnd_ZR F rnd ->
forall x :
R, (
Rabs (
rnd x) <=
Rabs x)%
R.
Proof.
Theorem Rnd_ZR_pt_monotone :
forall F :
R ->
Prop,
F 0 ->
round_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,
Rnd_N_pt F x f ->
Rnd_DN_pt F x f \/
Rnd_UP_pt F x f.
Proof.
Theorem Rnd_N_pt_DN_or_UP_eq :
forall F :
R ->
Prop,
forall x fd fu f :
R,
Rnd_DN_pt F x fd ->
Rnd_UP_pt F x fu ->
Rnd_N_pt F x f ->
f =
fd \/
f =
fu.
Proof.
Theorem Rnd_N_pt_sym :
forall F :
R ->
Prop,
(
forall x,
F x ->
F (-
x) ) ->
forall x f :
R,
Rnd_N_pt F (-
x) (-
f) ->
Rnd_N_pt F x f.
Proof.
intros F HF x f (
H1,
H2).
rewrite <- (
Ropp_involutive f).
repeat split.
apply HF.
apply H1.
intros g H3.
rewrite Ropp_involutive.
replace (
f -
x)%
R with (-(-
f - -
x))%
R by ring.
replace (
g -
x)%
R with (-(-
g - -
x))%
R by ring.
rewrite 2!
Rabs_Ropp.
apply H2.
now apply HF.
Qed.
Theorem Rnd_N_pt_monotone :
forall F :
R ->
Prop,
forall x y f g :
R,
Rnd_N_pt F x f ->
Rnd_N_pt F y g ->
x <
y ->
f <=
g.
Proof.
Theorem Rnd_N_pt_unicity :
forall F :
R ->
Prop,
forall x d u f1 f2 :
R,
Rnd_DN_pt F x d ->
Rnd_UP_pt F x u ->
x -
d <>
u -
x ->
Rnd_N_pt F x f1 ->
Rnd_N_pt F x f2 ->
f1 =
f2.
Proof.
Theorem Rnd_N_pt_refl :
forall F :
R ->
Prop,
forall x :
R,
F x ->
Rnd_N_pt F x x.
Proof.
Theorem Rnd_N_pt_idempotent :
forall F :
R ->
Prop,
forall x f :
R,
Rnd_N_pt F x f ->
F x ->
f =
x.
Proof.
Theorem Rnd_N_pt_0 :
forall F :
R ->
Prop,
F 0 ->
Rnd_N_pt F 0 0.
Proof.
Theorem Rnd_N_pt_pos :
forall F :
R ->
Prop,
F 0 ->
forall x f, 0 <=
x ->
Rnd_N_pt F x f ->
0 <=
f.
Proof.
Theorem Rnd_N_pt_neg :
forall F :
R ->
Prop,
F 0 ->
forall x f,
x <= 0 ->
Rnd_N_pt F x f ->
f <= 0.
Proof.
Theorem Rnd_N_pt_abs :
forall F :
R ->
Prop,
F 0 ->
(
forall x,
F x ->
F (-
x) ) ->
forall x f :
R,
Rnd_N_pt F x f ->
Rnd_N_pt F (
Rabs x) (
Rabs f).
Proof.
Theorem Rnd_DN_UP_pt_N :
forall F :
R ->
Prop,
forall x d u f :
R,
F f ->
Rnd_DN_pt F x d ->
Rnd_UP_pt F x u ->
(
Rabs (
f -
x) <=
x -
d)%
R ->
(
Rabs (
f -
x) <=
u -
x)%
R ->
Rnd_N_pt F x f.
Proof.
Theorem Rnd_DN_pt_N :
forall F :
R ->
Prop,
forall x d u :
R,
Rnd_DN_pt F x d ->
Rnd_UP_pt F x u ->
(
x -
d <=
u -
x)%
R ->
Rnd_N_pt F x d.
Proof.
Theorem Rnd_UP_pt_N :
forall F :
R ->
Prop,
forall x d u :
R,
Rnd_DN_pt F x d ->
Rnd_UP_pt F x u ->
(
u -
x <=
x -
d)%
R ->
Rnd_N_pt F x u.
Proof.
Definition Rnd_NG_pt_unicity_prop F P :=
forall x d u,
Rnd_DN_pt F x d ->
Rnd_N_pt F x d ->
Rnd_UP_pt F x u ->
Rnd_N_pt F x u ->
P x d ->
P x u ->
d =
u.
Theorem Rnd_NG_pt_unicity :
forall (
F :
R ->
Prop) (
P :
R ->
R ->
Prop),
Rnd_NG_pt_unicity_prop F P ->
forall x f1 f2 :
R,
Rnd_NG_pt F P x f1 ->
Rnd_NG_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 H2a H1c H1a).
eapply Rnd_UP_pt_unicity ;
eassumption.
now apply H2b.
apply sym_eq.
now apply H1b.
Qed.
Theorem Rnd_NG_pt_monotone :
forall (
F :
R ->
Prop) (
P :
R ->
R ->
Prop),
Rnd_NG_pt_unicity_prop F P ->
round_pred_monotone (
Rnd_NG_pt F P).
Proof.
Theorem Rnd_NG_pt_refl :
forall (
F :
R ->
Prop) (
P :
R ->
R ->
Prop),
forall x,
F x ->
Rnd_NG_pt F P x x.
Proof.
Theorem Rnd_NG_pt_sym :
forall (
F :
R ->
Prop) (
P :
R ->
R ->
Prop),
(
forall x,
F x ->
F (-
x) ) ->
(
forall x f,
P x f ->
P (-
x) (-
f) ) ->
forall x f :
R,
Rnd_NG_pt F P (-
x) (-
f) ->
Rnd_NG_pt F P x f.
Proof.
Theorem Rnd_NG_unicity :
forall (
F :
R ->
Prop) (
P :
R ->
R ->
Prop),
Rnd_NG_pt_unicity_prop F P ->
forall rnd1 rnd2 :
R ->
R,
Rnd_NG F P rnd1 ->
Rnd_NG F P rnd2 ->
forall x,
rnd1 x =
rnd2 x.
Proof.
Theorem Rnd_NA_NG_pt :
forall F :
R ->
Prop,
F 0 ->
forall x f,
Rnd_NA_pt F x f <->
Rnd_NG_pt F (
fun x f =>
Rabs x <=
Rabs f)
x f.
Proof.
Theorem Rnd_NA_pt_unicity_prop :
forall F :
R ->
Prop,
F 0 ->
Rnd_NG_pt_unicity_prop F (
fun a b => (
Rabs a <=
Rabs b)%
R).
Proof.
Theorem Rnd_NA_pt_unicity :
forall F :
R ->
Prop,
F 0 ->
forall x f1 f2 :
R,
Rnd_NA_pt F x f1 ->
Rnd_NA_pt F x f2 ->
f1 =
f2.
Proof.
Theorem Rnd_NA_N_pt :
forall F :
R ->
Prop,
F 0 ->
forall x f :
R,
Rnd_N_pt F x f ->
(
Rabs x <=
Rabs f)%
R ->
Rnd_NA_pt F x f.
Proof.
Theorem Rnd_NA_unicity :
forall (
F :
R ->
Prop),
F 0 ->
forall rnd1 rnd2 :
R ->
R,
Rnd_NA F rnd1 ->
Rnd_NA F rnd2 ->
forall x,
rnd1 x =
rnd2 x.
Proof.
Theorem Rnd_NA_pt_monotone :
forall F :
R ->
Prop,
F 0 ->
round_pred_monotone (
Rnd_NA_pt F).
Proof.
Theorem Rnd_NA_pt_refl :
forall F :
R ->
Prop,
forall x :
R,
F x ->
Rnd_NA_pt F x x.
Proof.
Theorem Rnd_NA_pt_idempotent :
forall F :
R ->
Prop,
forall x f :
R,
Rnd_NA_pt F x f ->
F x ->
f =
x.
Proof.
Theorem round_pred_ge_0 :
forall P :
R ->
R ->
Prop,
round_pred_monotone P ->
P 0 0 ->
forall x f,
P x f -> 0 <=
x -> 0 <=
f.
Proof.
intros P HP HP0 x f Hxf Hx.
now apply (HP 0 x).
Qed.
Theorem round_pred_gt_0 :
forall P :
R ->
R ->
Prop,
round_pred_monotone P ->
P 0 0 ->
forall x f,
P x f -> 0 <
f -> 0 <
x.
Proof.
intros P HP HP0 x f Hxf Hf.
apply Rnot_le_lt.
intros Hx.
apply Rlt_not_le with (1 :=
Hf).
now apply (
HP x 0).
Qed.
Theorem round_pred_le_0 :
forall P :
R ->
R ->
Prop,
round_pred_monotone P ->
P 0 0 ->
forall x f,
P x f ->
x <= 0 ->
f <= 0.
Proof.
intros P HP HP0 x f Hxf Hx.
now apply (HP x 0).
Qed.
Theorem round_pred_lt_0 :
forall P :
R ->
R ->
Prop,
round_pred_monotone P ->
P 0 0 ->
forall x f,
P x f ->
f < 0 ->
x < 0.
Proof.
intros P HP HP0 x f Hxf Hf.
apply Rnot_le_lt.
intros Hx.
apply Rlt_not_le with (1 :=
Hf).
now apply (
HP 0
x).
Qed.
Theorem Rnd_DN_pt_equiv_format :
forall F1 F2 :
R ->
Prop,
forall a b :
R,
F1 a ->
(
forall x,
a <=
x <=
b -> (
F1 x <->
F2 x) ) ->
forall x f,
a <=
x <=
b ->
Rnd_DN_pt F1 x f ->
Rnd_DN_pt F2 x f.
Proof.
intros F1 F2 a b Ha HF x f Hx (
H1, (
H2,
H3)).
split.
apply ->
HF.
exact H1.
split.
now apply H3.
now apply Rle_trans with (1 :=
H2).
split.
exact H2.
intros k Hk Hl.
destruct (
Rlt_or_le k a)
as [
H|
H].
apply Rlt_le.
apply Rlt_le_trans with (1 :=
H).
now apply H3.
apply H3.
apply <-
HF.
exact Hk.
split.
exact H.
now apply Rle_trans with (1 :=
Hl).
exact Hl.
Qed.
Theorem Rnd_UP_pt_equiv_format :
forall F1 F2 :
R ->
Prop,
forall a b :
R,
F1 b ->
(
forall x,
a <=
x <=
b -> (
F1 x <->
F2 x) ) ->
forall x f,
a <=
x <=
b ->
Rnd_UP_pt F1 x f ->
Rnd_UP_pt F2 x f.
Proof.
intros F1 F2 a b Hb HF x f Hx (
H1, (
H2,
H3)).
split.
apply ->
HF.
exact H1.
split.
now apply Rle_trans with (2 :=
H2).
now apply H3.
split.
exact H2.
intros k Hk Hl.
destruct (
Rle_or_lt k b)
as [
H|
H].
apply H3.
apply <-
HF.
exact Hk.
split.
now apply Rle_trans with (2 :=
Hl).
exact H.
exact Hl.
apply Rlt_le.
apply Rle_lt_trans with (2 :=
H).
now apply H3.
Qed.
ensures a real number can always be rounded
Inductive satisfies_any (
F :
R ->
Prop) :=
Satisfies_any :
F 0 -> (
forall x :
R,
F x ->
F (-
x) ) ->
round_pred_total (
Rnd_DN_pt F) ->
satisfies_any F.
Theorem satisfies_any_eq :
forall F1 F2 :
R ->
Prop,
(
forall x,
F1 x <->
F2 x ) ->
satisfies_any F1 ->
satisfies_any F2.
Proof.
intros F1 F2 Heq (Hzero, Hsym, Hrnd).
split.
now apply -> Heq.
intros x Hx.
apply -> Heq.
apply Hsym.
now apply <- Heq.
intros x.
destruct (Hrnd x) as (f, (H1, (H2, H3))).
exists f.
split.
now apply -> Heq.
split.
exact H2.
intros g Hg Hgx.
apply H3.
now apply <- Heq.
exact Hgx.
Qed.
Theorem satisfies_any_imp_DN :
forall F :
R ->
Prop,
satisfies_any F ->
round_pred (
Rnd_DN_pt F).
Proof.
Theorem satisfies_any_imp_UP :
forall F :
R ->
Prop,
satisfies_any F ->
round_pred (
Rnd_UP_pt F).
Proof.
Theorem satisfies_any_imp_ZR :
forall F :
R ->
Prop,
satisfies_any F ->
round_pred (
Rnd_ZR_pt F).
Proof.
Definition NG_existence_prop (
F :
R ->
Prop) (
P :
R ->
R ->
Prop) :=
forall x d u, ~
F x ->
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 ->
NG_existence_prop F P ->
round_pred_total (
Rnd_NG_pt F P).
Proof.
Theorem satisfies_any_imp_NA :
forall F :
R ->
Prop,
satisfies_any F ->
round_pred (
Rnd_NA_pt F).
Proof.
End RND_prop.