1 files changed, 101 insertions, 0 deletions
diff --git a/flocq/Core/Fcore_defs.v b/flocq/Core/Fcore_defs.v
new file mode 100644
index 00000000..fda3a858
--- /dev/null
+++ b/flocq/Core/Fcore_defs.v
@@ -0,0 +1,101 @@
+(**
+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
+#<br />#
+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.
+*)
+
+(** * Basic definitions: float and rounding property *)
+Require Import Fcore_Raux.
+
+Section Def.
+
+(** Definition of a floating-point number *)
+Record float (beta : radix) := Float { Fnum : Z ; Fexp : Z }.
+
+Implicit Arguments Fnum [[beta]].
+Implicit Arguments Fexp [[beta]].
+
+Variable beta : radix.
+
+Definition F2R (f : float beta) :=
+  (Z2R (Fnum f) * bpow beta (Fexp f))%R.
+
+(** Requirements on a rounding mode *)
+Definition round_pred_total (P : R -> R -> Prop) :=
+  forall x, exists f, P x f.
+
+Definition round_pred_monotone (P : R -> R -> Prop) :=
+  forall x y f g, P x f -> P y g -> (x <= y)%R -> (f <= g)%R.
+
+Definition round_pred (P : R -> R -> Prop) :=
+  round_pred_total P /\
+  round_pred_monotone P.
+
+End Def.
+
+Implicit Arguments Fnum [[beta]].
+Implicit Arguments Fexp [[beta]].
+Implicit Arguments F2R [[beta]].
+
+Section RND.
+
+(** property of being a round toward -inf *)
+Definition Rnd_DN_pt (F : R -> Prop) (x f : R) :=
+  F f /\ (f <= x)%R /\
+  forall g : R, F g -> (g <= x)%R -> (g <= f)%R.
+
+Definition Rnd_DN (F : R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_DN_pt F x (rnd x).
+
+(** property of being a round toward +inf *)
+Definition Rnd_UP_pt (F : R -> Prop) (x f : R) :=
+  F f /\ (x <= f)%R /\
+  forall g : R, F g -> (x <= g)%R -> (f <= g)%R.
+
+Definition Rnd_UP (F : R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_UP_pt F x (rnd x).
+
+(** property of being a round toward zero *)
+Definition Rnd_ZR_pt (F : R -> Prop) (x f : R) :=
+  ( (0 <= x)%R -> Rnd_DN_pt F x f ) /\
+  ( (x <= 0)%R -> Rnd_UP_pt F x f ).
+
+Definition Rnd_ZR (F : R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_ZR_pt F x (rnd x).
+
+(** property of being a round to nearest *)
+Definition Rnd_N_pt (F : R -> Prop) (x f : R) :=
+  F f /\
+  forall g : R, F g -> (Rabs (f - x) <= Rabs (g - x))%R.
+
+Definition Rnd_N (F : R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_N_pt F x (rnd x).
+
+Definition Rnd_NG_pt (F : R -> Prop) (P : R -> R -> Prop) (x f : R) :=
+  Rnd_N_pt F x f /\
+  ( P x f \/ forall f2 : R, Rnd_N_pt F x f2 -> f2 = f ).
+
+Definition Rnd_NG (F : R -> Prop) (P : R -> R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_NG_pt F P x (rnd x).
+
+Definition Rnd_NA_pt (F : R -> Prop) (x f : R) :=
+  Rnd_N_pt F x f /\
+  forall f2 : R, Rnd_N_pt F x f2 -> (Rabs f2 <= Rabs f)%R.
+
+Definition Rnd_NA (F : R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_NA_pt F x (rnd x).
+
+End RND.