Library Flocq.Core.Fcore_rnd

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

Copyright (C) 2010-2011 Sylvie Boldo
Copyright (C) 2010-2011 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 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 }.

Theorem round_fun_of_pred :
  forall rnd : R -> R -> Prop,
  round_pred rnd ->
  { f : R -> R | forall x, rnd x (f x) }.

Theorem round_unicity :
  forall rnd : R -> R -> Prop,
  round_pred_monotone rnd ->
  forall x f1 f2,
  rnd x f1 ->
  rnd x f2 ->
  f1 = f2.

Theorem Rnd_DN_pt_monotone :
  forall F : R -> Prop,
  round_pred_monotone (Rnd_DN_pt F).

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.

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.

Theorem Rnd_UP_pt_monotone :
  forall F : R -> Prop,
  round_pred_monotone (Rnd_UP_pt F).

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.

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.

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

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

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.

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

Theorem Rnd_DN_pt_refl :
  forall F : R -> Prop,
  forall x : R, F x ->
  Rnd_DN_pt F x x.

Theorem Rnd_DN_pt_idempotent :
  forall F : R -> Prop,
  forall x f : R,
  Rnd_DN_pt F x f -> F x ->
  f = x.

Theorem Rnd_UP_pt_refl :
  forall F : R -> Prop,
  forall x : R, F x ->
  Rnd_UP_pt F x x.

Theorem Rnd_UP_pt_idempotent :
  forall F : R -> Prop,
  forall x f : R,
  Rnd_UP_pt F x f -> F x ->
  f = x.

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.

Theorem Rnd_ZR_abs :
  forall (F : R -> Prop) (rnd: R-> R),
  Rnd_ZR F rnd ->
  forall x : R, (Rabs (rnd x) <= Rabs x)%R.

Theorem Rnd_ZR_pt_monotone :
  forall F : R -> Prop, F 0 ->
  round_pred_monotone (Rnd_ZR_pt F).

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.

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.

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.

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.

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.

Theorem Rnd_N_pt_refl :
  forall F : R -> Prop,
  forall x : R, F x ->
  Rnd_N_pt F x x.

Theorem Rnd_N_pt_idempotent :
  forall F : R -> Prop,
  forall x f : R,
  Rnd_N_pt F x f -> F x ->
  f = x.

Theorem Rnd_N_pt_0 :
  forall F : R -> Prop,
  F 0 ->
  Rnd_N_pt F 0 0.

Theorem Rnd_N_pt_pos :
  forall F : R -> Prop, F 0 ->
  forall x f, 0 <= x ->
  Rnd_N_pt F x f ->
  0 <= f.

Theorem Rnd_N_pt_neg :
  forall F : R -> Prop, F 0 ->
  forall x f, x <= 0 ->
  Rnd_N_pt F x f ->
  f <= 0.

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

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.

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.

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.

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.

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

Theorem Rnd_NG_pt_refl :
  forall (F : R -> Prop) (P : R -> R -> Prop),
  forall x, F x -> Rnd_NG_pt F P x x.

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.

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.

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.

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

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.

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.

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.

Theorem Rnd_NA_pt_monotone :
  forall F : R -> Prop,
  F 0 ->
  round_pred_monotone (Rnd_NA_pt F).

Theorem Rnd_NA_pt_refl :
  forall F : R -> Prop,
  forall x : R, F x ->
  Rnd_NA_pt F x x.

Theorem Rnd_NA_pt_idempotent :
  forall F : R -> Prop,
  forall x f : R,
  Rnd_NA_pt F x f -> F x ->
  f = x.

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.

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.

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.

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.

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.

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.

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.

Theorem satisfies_any_imp_DN :
  forall F : R -> Prop,
  satisfies_any F ->
  round_pred (Rnd_DN_pt F).

Theorem satisfies_any_imp_UP :
  forall F : R -> Prop,
  satisfies_any F ->
  round_pred (Rnd_UP_pt F).

Theorem satisfies_any_imp_ZR :
  forall F : R -> Prop,
  satisfies_any F ->
  round_pred (Rnd_ZR_pt F).

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

Theorem satisfies_any_imp_NA :
  forall F : R -> Prop,
  satisfies_any F ->
  round_pred (Rnd_NA_pt F).

End RND_prop.