Fcomp.v

(****************************************************************************                                                                                         IEEE754  :  Fcomp                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Import Float.
Section comparisons.
Variable radix:nat.
Hypothesis radixMoreThanOne:(lt (S O) radix).

Local zr := (inject_nat radix).

Definition Fdiff :=
   [x, y:float]
   (Zminus
      (Zmult
         (Fnum x)
         (Zpower_nat zr (absolu (Zminus (Fexp x) (Zmin (Fexp x) (Fexp y))))))
      (Zmult
         (Fnum y)
         (Zpower_nat zr (absolu (Zminus (Fexp y) (Zmin (Fexp x) (Fexp y))))))).

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.

Theorem Fdiff_correct:
  (x, y:float)
  (Rmult (Fdiff x y) (powerRZ radix (Zmin (Fexp x) (Fexp y))))==(Rminus x y).

(* Definition of  comparison functions*)

Definition Feq := [x, y:float]<R> x==y.

Definition Fle := [x, y:float](Rle x y).

Definition Flt := [x, y:float](Rlt x y).

Definition Fge := [x, y:float](Rge x y).

Definition Fgt := [x, y:float](Rgt x y).

Definition Fcompare := [x, y:float](Zcompare ZERO (Fdiff x y)).

Definition Feq_bool :=
   [x, y:float]
      Cases (Fcompare x y) of
          EGAL => true
         | _ => false
      end.

Theorem Feq_bool_correct_t: (x, y:float) (Feq_bool x y)=true ->(Feq x y).

Theorem Feq_bool_correct_r: (x, y:float) (Feq x y) ->(Feq_bool x y)=true.

Theorem Feq_bool_correct_f: (x, y:float) (Feq_bool x y)=false ->~ (Feq x y).

Definition Flt_bool :=
   [x, y:float]
      Cases (Fcompare x y) of
          SUPERIEUR => true
         | _ => false
      end.

Theorem Flt_bool_correct_t: (x, y:float) (Flt_bool x y)=true ->(Flt x y).

Theorem Flt_bool_correct_r: (x, y:float) (Flt x y) ->(Flt_bool x y)=true.

Theorem Flt_bool_correct_f: (x, y:float) (Flt_bool x y)=false ->(Fle y x).

Definition Fle_bool :=
   [x, y:float]
      Cases (Fcompare x y) of
          SUPERIEUR => true
         | EGAL => true
         | _ => false
      end.

Theorem Fle_bool_correct_t: (x, y:float) (Fle_bool x y)=true ->(Fle x y).

Theorem Fle_bool_correct_r: (x, y:float) (Fle x y) ->(Fle_bool x y)=true.

Theorem Fle_bool_correct_f: (x, y:float) (Fle_bool x y)=false ->(Flt y x).

Lemma Fle_Zle: (n1, n2, d:Z) (Zle n1 n2) ->(Fle (Float n1 d) (Float n2 d)).

Lemma Flt_Zlt: (n1, n2, d:Z) (Zlt n1 n2) ->(Flt (Float n1 d) (Float n2 d)).

Lemma Fle_Fge: (x, y:float) (Fle x y) ->(Fge y x).

Lemma Fge_Zge: (n1, n2, d:Z) (Zge n1 n2) ->(Fge (Float n1 d) (Float n2 d)).

Lemma Flt_Fgt: (x, y:float) (Flt x y) ->(Fgt y x).

Lemma Fgt_Zgt: (n1, n2, d:Z) (Zgt n1 n2) ->(Fgt (Float n1 d) (Float n2 d)).
(* Arithmetic properties on F : Fle is reflexive, transitive, antisymmetric *)

Lemma Fle_refl: (x, y:float) (Feq x y) ->(Fle x y).

Lemma Fle_trans: (x, y, z:float) (Fle x y) -> (Fle y z) ->(Fle x z).

Theorem Rlt_Fexp_eq_Zlt:
  (x, y:float) (Rlt x y) -> (Fexp x)=(Fexp y) ->(Zlt (Fnum x) (Fnum y)).

Theorem Rle_Fexp_eq_Zle:
  (x, y:float) (Rle x y) -> (Fexp x)=(Fexp y) ->(Zle (Fnum x) (Fnum y)).

Theorem LtR0Fnum: (p:float) (Rlt R0 p) ->(Zlt ZERO (Fnum p)).

Theorem LeR0Fnum: (p:float) (Rle R0 p) ->(Zle ZERO (Fnum p)).

Theorem LeFnumZERO: (x:float) (Zle ZERO (Fnum x)) ->(Rle R0 x).

Theorem R0LtFnum: (p:float) (Rlt p R0) ->(Zlt (Fnum p) ZERO).

Theorem R0LeFnum: (p:float) (Rle p R0) ->(Zle (Fnum p) ZERO).

Theorem LeZEROFnum: (x:float) (Zle (Fnum x) ZERO) ->(Rle x R0).
End comparisons.

30/05/01, 17:46