Require Import Flocq_Raux.

Section Def.

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) * epow beta (Fexp f))%R.

Definition MonotoneP (rnd : R -> R) :=
  forall x y : R,
  (x <= y)%R -> (rnd x <= rnd y)%R.

Definition IdempotentP (F : R -> Prop) (rnd : R -> R) :=
    (forall x : R, F (rnd x))
        /\ (forall x : R, F x -> rnd x = x). 

Definition Rounding_for_Format (F : R -> Prop) (rnd : R -> R) :=
   MonotoneP rnd /\ IdempotentP F rnd.

End Def.

Implicit Arguments Fnum [[beta]].
Implicit Arguments Fexp [[beta]].
Implicit Arguments F2R [[beta]].

Section RND.

(* property of being a rounding 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 rounding 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 rounding 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).

Theorem toto :
  forall (F : R -> Prop) (rnd: R-> R), 
  Rnd_ZR F rnd ->
  forall x : R,  (Rabs (rnd x) <= Rabs x)%R.
Proof.
intros F rnd H x.
assert (F 0%R).
replace 0%R with (rnd 0%R).
eapply H.
apply Rle_refl.
destruct (H 0%R) as (H1, H2).
apply Rle_antisym.
apply H1.
apply Rle_refl.
apply H2.
apply Rle_refl.
(* . *)
destruct (Rle_or_lt 0 x).
(* positive *)
rewrite Rabs_right.
rewrite Rabs_right; auto with real.
now apply (proj1 (H x)).
apply Rle_ge.
now apply (proj1 (H x)).
(* negative *)
rewrite Rabs_left1.
rewrite Rabs_left1 ; auto with real.
apply Ropp_le_contravar.
apply (proj2 (H x)).
auto with real.
apply (proj2 (H x)) ; auto with real.
Qed.

(* property of being a rounding 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_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.