Library Flocq.Core.Round_pred

This file is part of the Flocq formalization of floating-point arithmetic in Coq: https://flocq.gitlabpages.inria.fr/

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.

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.