Library Flocq.Core.Round_pred
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: https://flocq.gitlabpages.inria.fr/
Copyright (C) 2009-2018 Sylvie Boldo
Copyright (C) 2009-2018 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Copyright (C) 2009-2018 Guillaume Melquiond
Roundings: properties and/or functions
From Coq Require Import Reals.
Require Import Raux Defs.
Section RND_prop.
Open Scope R_scope.
Definition Rnd_DN (F : R → Prop) (rnd : R → R) :=
∀ x : R, Rnd_DN_pt F x (rnd x).
Definition Rnd_UP (F : R → Prop) (rnd : R → R) :=
∀ x : R, Rnd_UP_pt F x (rnd x).
Definition Rnd_ZR (F : R → Prop) (rnd : R → R) :=
∀ x : R, Rnd_ZR_pt F x (rnd x).
Definition Rnd_N (F : R → Prop) (rnd : R → R) :=
∀ x : R, Rnd_N_pt F x (rnd x).
Definition Rnd_NG (F : R → Prop) (P : R → R → Prop) (rnd : R → R) :=
∀ x : R, Rnd_NG_pt F P x (rnd x).
Definition Rnd_NA (F : R → Prop) (rnd : R → R) :=
∀ x : R, Rnd_NA_pt F x (rnd x).
Definition Rnd_N0 (F : R → Prop) (rnd : R → R) :=
∀ x : R, Rnd_N0_pt F x (rnd x).
Theorem round_val_of_pred :
∀ rnd : R → R → Prop,
round_pred rnd →
∀ x, { f : R | rnd x f }.
Theorem round_fun_of_pred :
∀ rnd : R → R → Prop,
round_pred rnd →
{ f : R → R | ∀ x, rnd x (f x) }.
Theorem round_unique :
∀ rnd : R → R → Prop,
round_pred_monotone rnd →
∀ x f1 f2,
rnd x f1 →
rnd x f2 →
f1 = f2.
Theorem Rnd_DN_pt_monotone :
∀ F : R → Prop,
round_pred_monotone (Rnd_DN_pt F).
Theorem Rnd_DN_pt_unique :
∀ F : R → Prop,
∀ x f1 f2 : R,
Rnd_DN_pt F x f1 → Rnd_DN_pt F x f2 →
f1 = f2.
Theorem Rnd_DN_unique :
∀ F : R → Prop,
∀ rnd1 rnd2 : R → R,
Rnd_DN F rnd1 → Rnd_DN F rnd2 →
∀ x, rnd1 x = rnd2 x.
Theorem Rnd_UP_pt_monotone :
∀ F : R → Prop,
round_pred_monotone (Rnd_UP_pt F).
Theorem Rnd_UP_pt_unique :
∀ F : R → Prop,
∀ x f1 f2 : R,
Rnd_UP_pt F x f1 → Rnd_UP_pt F x f2 →
f1 = f2.
Theorem Rnd_UP_unique :
∀ F : R → Prop,
∀ rnd1 rnd2 : R → R,
Rnd_UP F rnd1 → Rnd_UP F rnd2 →
∀ x, rnd1 x = rnd2 x.
Theorem Rnd_UP_pt_opp :
∀ F : R → Prop,
( ∀ x, F x → F (- x) ) →
∀ x f : R,
Rnd_DN_pt F x f → Rnd_UP_pt F (-x) (-f).
Theorem Rnd_DN_pt_opp :
∀ F : R → Prop,
( ∀ x, F x → F (- x) ) →
∀ x f : R,
Rnd_UP_pt F x f → Rnd_DN_pt F (-x) (-f).
Theorem Rnd_DN_opp :
∀ F : R → Prop,
( ∀ x, F x → F (- x) ) →
∀ rnd1 rnd2 : R → R,
Rnd_DN F rnd1 → Rnd_UP F rnd2 →
∀ x, rnd1 (- x) = - rnd2 x.
Theorem Rnd_DN_UP_pt_split :
∀ F : R → Prop,
∀ x d u,
Rnd_DN_pt F x d →
Rnd_UP_pt F x u →
∀ f, F f →
(f ≤ d) ∨ (u ≤ f).
Theorem Rnd_DN_pt_refl :
∀ F : R → Prop,
∀ x : R, F x →
Rnd_DN_pt F x x.
Theorem Rnd_DN_pt_idempotent :
∀ F : R → Prop,
∀ x f : R,
Rnd_DN_pt F x f → F x →
f = x.
Theorem Rnd_UP_pt_refl :
∀ F : R → Prop,
∀ x : R, F x →
Rnd_UP_pt F x x.
Theorem Rnd_UP_pt_idempotent :
∀ F : R → Prop,
∀ x f : R,
Rnd_UP_pt F x f → F x →
f = x.
Theorem Only_DN_or_UP :
∀ F : R → Prop,
∀ 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.
Theorem Rnd_ZR_abs :
∀ (F : R → Prop) (rnd: R→ R),
Rnd_ZR F rnd →
∀ x : R, (Rabs (rnd x) ≤ Rabs x)%R.
Theorem Rnd_ZR_pt_monotone :
∀ F : R → Prop, F 0 →
round_pred_monotone (Rnd_ZR_pt F).
Theorem Rnd_N_pt_DN_or_UP :
∀ F : R → Prop,
∀ x f : R,
Rnd_N_pt F x f →
Rnd_DN_pt F x f ∨ Rnd_UP_pt F x f.
Theorem Rnd_N_pt_DN_or_UP_eq :
∀ F : R → Prop,
∀ 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.
Theorem Rnd_N_pt_opp_inv :
∀ F : R → Prop,
( ∀ x, F x → F (- x) ) →
∀ x f : R,
Rnd_N_pt F (-x) (-f) → Rnd_N_pt F x f.
Theorem Rnd_N_pt_monotone :
∀ F : R → Prop,
∀ x y f g : R,
Rnd_N_pt F x f → Rnd_N_pt F y g →
x < y → f ≤ g.
Theorem Rnd_N_pt_unique :
∀ F : R → Prop,
∀ 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.
Theorem Rnd_N_pt_refl :
∀ F : R → Prop,
∀ x : R, F x →
Rnd_N_pt F x x.
Theorem Rnd_N_pt_idempotent :
∀ F : R → Prop,
∀ x f : R,
Rnd_N_pt F x f → F x →
f = x.
Theorem Rnd_N_pt_0 :
∀ F : R → Prop,
F 0 →
Rnd_N_pt F 0 0.
Theorem Rnd_N_pt_ge_0 :
∀ F : R → Prop, F 0 →
∀ x f, 0 ≤ x →
Rnd_N_pt F x f →
0 ≤ f.
Theorem Rnd_N_pt_le_0 :
∀ F : R → Prop, F 0 →
∀ x f, x ≤ 0 →
Rnd_N_pt F x f →
f ≤ 0.
Theorem Rnd_N_pt_abs :
∀ F : R → Prop,
F 0 →
( ∀ x, F x → F (- x) ) →
∀ x f : R,
Rnd_N_pt F x f → Rnd_N_pt F (Rabs x) (Rabs f).
Theorem Rnd_N_pt_DN_UP :
∀ F : R → Prop,
∀ 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.
Theorem Rnd_N_pt_DN :
∀ F : R → Prop,
∀ 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.
Theorem Rnd_N_pt_UP :
∀ F : R → Prop,
∀ 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.
Definition Rnd_NG_pt_unique_prop F P :=
∀ 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_unique :
∀ (F : R → Prop) (P : R → R → Prop),
Rnd_NG_pt_unique_prop F P →
∀ x f1 f2 : R,
Rnd_NG_pt F P x f1 → Rnd_NG_pt F P x f2 →
f1 = f2.
Theorem Rnd_NG_pt_monotone :
∀ (F : R → Prop) (P : R → R → Prop),
Rnd_NG_pt_unique_prop F P →
round_pred_monotone (Rnd_NG_pt F P).
Theorem Rnd_NG_pt_refl :
∀ (F : R → Prop) (P : R → R → Prop),
∀ x, F x → Rnd_NG_pt F P x x.
Theorem Rnd_NG_pt_opp_inv :
∀ (F : R → Prop) (P : R → R → Prop),
( ∀ x, F x → F (-x) ) →
( ∀ x f, P x f → P (-x) (-f) ) →
∀ x f : R,
Rnd_NG_pt F P (-x) (-f) → Rnd_NG_pt F P x f.
Theorem Rnd_NG_unique :
∀ (F : R → Prop) (P : R → R → Prop),
Rnd_NG_pt_unique_prop F P →
∀ rnd1 rnd2 : R → R,
Rnd_NG F P rnd1 → Rnd_NG F P rnd2 →
∀ x, rnd1 x = rnd2 x.
Theorem Rnd_NA_NG_pt :
∀ F : R → Prop,
F 0 →
∀ x f,
Rnd_NA_pt F x f ↔ Rnd_NG_pt F (fun x f ⇒ Rabs x ≤ Rabs f) x f.
Lemma Rnd_NA_pt_unique_prop :
∀ F : R → Prop,
F 0 →
Rnd_NG_pt_unique_prop F (fun a b ⇒ (Rabs a ≤ Rabs b)%R).
Theorem Rnd_NA_pt_unique :
∀ F : R → Prop,
F 0 →
∀ x f1 f2 : R,
Rnd_NA_pt F x f1 → Rnd_NA_pt F x f2 →
f1 = f2.
Theorem Rnd_NA_pt_N :
∀ F : R → Prop,
F 0 →
∀ x f : R,
Rnd_N_pt F x f →
(Rabs x ≤ Rabs f)%R →
Rnd_NA_pt F x f.
Theorem Rnd_NA_unique :
∀ (F : R → Prop),
F 0 →
∀ rnd1 rnd2 : R → R,
Rnd_NA F rnd1 → Rnd_NA F rnd2 →
∀ x, rnd1 x = rnd2 x.
Theorem Rnd_NA_pt_monotone :
∀ F : R → Prop,
F 0 →
round_pred_monotone (Rnd_NA_pt F).
Theorem Rnd_NA_pt_refl :
∀ F : R → Prop,
∀ x : R, F x →
Rnd_NA_pt F x x.
Theorem Rnd_NA_pt_idempotent :
∀ F : R → Prop,
∀ x f : R,
Rnd_NA_pt F x f → F x →
f = x.
Theorem Rnd_N0_NG_pt :
∀ F : R → Prop,
F 0 →
∀ x f,
Rnd_N0_pt F x f ↔ Rnd_NG_pt F (fun x f ⇒ Rabs f ≤ Rabs x) x f.
Lemma Rnd_N0_pt_unique_prop :
∀ F : R → Prop,
F 0 →
Rnd_NG_pt_unique_prop F (fun x f ⇒ Rabs f ≤ Rabs x).
Theorem Rnd_N0_pt_unique :
∀ F : R → Prop,
F 0 →
∀ x f1 f2 : R,
Rnd_N0_pt F x f1 → Rnd_N0_pt F x f2 →
f1 = f2.
Theorem Rnd_N0_pt_N :
∀ F : R → Prop,
F 0 →
∀ x f : R,
Rnd_N_pt F x f →
(Rabs f ≤ Rabs x)%R →
Rnd_N0_pt F x f.
Theorem Rnd_N0_unique :
∀ (F : R → Prop),
F 0 →
∀ rnd1 rnd2 : R → R,
Rnd_N0 F rnd1 → Rnd_N0 F rnd2 →
∀ x, rnd1 x = rnd2 x.
Theorem Rnd_N0_pt_monotone :
∀ F : R → Prop,
F 0 →
round_pred_monotone (Rnd_N0_pt F).
Theorem Rnd_N0_pt_refl :
∀ F : R → Prop,
∀ x : R, F x →
Rnd_N0_pt F x x.
Theorem Rnd_N0_pt_idempotent :
∀ F : R → Prop,
∀ x f : R,
Rnd_N0_pt F x f → F x →
f = x.
Theorem round_pred_ge_0 :
∀ P : R → R → Prop,
round_pred_monotone P →
P 0 0 →
∀ x f, P x f → 0 ≤ x → 0 ≤ f.
Theorem round_pred_gt_0 :
∀ P : R → R → Prop,
round_pred_monotone P →
P 0 0 →
∀ x f, P x f → 0 < f → 0 < x.
Theorem round_pred_le_0 :
∀ P : R → R → Prop,
round_pred_monotone P →
P 0 0 →
∀ x f, P x f → x ≤ 0 → f ≤ 0.
Theorem round_pred_lt_0 :
∀ P : R → R → Prop,
round_pred_monotone P →
P 0 0 →
∀ x f, P x f → f < 0 → x < 0.
Theorem Rnd_DN_pt_equiv_format :
∀ F1 F2 : R → Prop,
∀ a b : R,
F1 a →
( ∀ x, a ≤ x ≤ b → (F1 x ↔ F2 x) ) →
∀ x f, a ≤ x ≤ b → Rnd_DN_pt F1 x f → Rnd_DN_pt F2 x f.
Theorem Rnd_UP_pt_equiv_format :
∀ F1 F2 : R → Prop,
∀ a b : R,
F1 b →
( ∀ x, a ≤ x ≤ b → (F1 x ↔ F2 x) ) →
∀ x f, a ≤ x ≤ b → Rnd_UP_pt F1 x f → Rnd_UP_pt F2 x f.
ensures a real number can always be rounded
Inductive satisfies_any (F : R → Prop) :=
Satisfies_any :
F 0 → ( ∀ x : R, F x → F (-x) ) →
round_pred_total (Rnd_DN_pt F) → satisfies_any F.
Theorem satisfies_any_eq :
∀ F1 F2 : R → Prop,
( ∀ x, F1 x ↔ F2 x ) →
satisfies_any F1 →
satisfies_any F2.
Theorem satisfies_any_imp_DN :
∀ F : R → Prop,
satisfies_any F →
round_pred (Rnd_DN_pt F).
Theorem satisfies_any_imp_UP :
∀ F : R → Prop,
satisfies_any F →
round_pred (Rnd_UP_pt F).
Theorem satisfies_any_imp_ZR :
∀ F : R → Prop,
satisfies_any F →
round_pred (Rnd_ZR_pt F).
Definition NG_existence_prop (F : R → Prop) (P : R → R → Prop) :=
∀ 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 :
∀ (F : R → Prop) (P : R → R → Prop),
satisfies_any F →
NG_existence_prop F P →
round_pred_total (Rnd_NG_pt F P).
Theorem satisfies_any_imp_NA :
∀ F : R → Prop,
satisfies_any F →
round_pred (Rnd_NA_pt F).
Theorem satisfies_any_imp_N0 :
∀ F : R → Prop,
F 0 → satisfies_any F →
round_pred (Rnd_N0_pt F).
End RND_prop.
Satisfies_any :
F 0 → ( ∀ x : R, F x → F (-x) ) →
round_pred_total (Rnd_DN_pt F) → satisfies_any F.
Theorem satisfies_any_eq :
∀ F1 F2 : R → Prop,
( ∀ x, F1 x ↔ F2 x ) →
satisfies_any F1 →
satisfies_any F2.
Theorem satisfies_any_imp_DN :
∀ F : R → Prop,
satisfies_any F →
round_pred (Rnd_DN_pt F).
Theorem satisfies_any_imp_UP :
∀ F : R → Prop,
satisfies_any F →
round_pred (Rnd_UP_pt F).
Theorem satisfies_any_imp_ZR :
∀ F : R → Prop,
satisfies_any F →
round_pred (Rnd_ZR_pt F).
Definition NG_existence_prop (F : R → Prop) (P : R → R → Prop) :=
∀ 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 :
∀ (F : R → Prop) (P : R → R → Prop),
satisfies_any F →
NG_existence_prop F P →
round_pred_total (Rnd_NG_pt F P).
Theorem satisfies_any_imp_NA :
∀ F : R → Prop,
satisfies_any F →
round_pred (Rnd_NA_pt F).
Theorem satisfies_any_imp_N0 :
∀ F : R → Prop,
F 0 → satisfies_any F →
round_pred (Rnd_N0_pt F).
End RND_prop.