Library Flocq.Core.Round_pred

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.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.

Roundings: properties and/or functions

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).

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 fRabs 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 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).

End RND_prop.