Fop.v

(****************************************************************************                                                                                         IEEE754  :  Fop                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Import Float.
Require Import Fcomp.
Section operations.
Variable radix:nat.

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixNotZero:~ radix=O.

Definition Fplus :=
   [x, y:float]
   (Float
      (Zplus
         (Zmult
            (Fnum x)
            (Zpower_nat
               (inject_nat radix)
               (absolu (Zminus (Fexp x) (Zmin (Fexp x) (Fexp y))))))
         (Zmult
            (Fnum y)
            (Zpower_nat
               (inject_nat radix)
               (absolu (Zminus (Fexp y) (Zmin (Fexp x) (Fexp y)))))))
      (Zmin (Fexp x) (Fexp y))).

Theorem Fplus_correct: (x, y:float)<R> (Fplus x y)==(Rplus x y).

Definition Fopp := [x:float](Float (Zopp (Fnum x)) (Fexp x)).

Theorem Fopp_correct: (x:float)<R> (Fopp x)==(Ropp x).

Theorem Fopp_Fopp: (p:float)(Fopp (Fopp p))=p.

Theorem Fzero_opp: (f:float) ~ (is_Fzero f) ->~ (is_Fzero (Fopp f)).

Theorem Fdigit_opp: (x:float)(Fdigit radix (Fopp x))=(Fdigit radix x).

Definition Fabs := [x:float](Float (Zabs (Fnum x)) (Fexp x)).

Theorem Fabs_correct1: (x:float) (Rle R0 (FtoR radix x)) -><R> (Fabs x)==x.

Theorem Fabs_correct2:
  (x:float) (Rle (FtoR radix x) R0) -><R> (Fabs x)==(Ropp x).

Theorem Fabs_correct: (x:float)<R> (Fabs x)==(Rabsolu x).

Theorem RleFexpFabs:
  (p:float) ~ <R> p==R0 ->(Rle (Float (1) (Fexp p)) (Fabs p)).

Theorem Fabs_Fzero: (x:float) ~ (is_Fzero x) ->~ (is_Fzero (Fabs x)).

Theorem Fdigit_abs: (x:float)(Fdigit radix (Fabs x))=(Fdigit radix x).

Definition Fminus := [x, y:float](Fplus x (Fopp y)).

Theorem Fminus_correct: (x, y:float)<R> (Fminus x y)==(Rminus x y).

Theorem Fopp_Fminus: (p, q:float)(Fopp (Fminus p q))=(Fminus q p).

Theorem Fopp_Fminus_dist:
  (p, q:float)(Fopp (Fminus p q))=(Fminus (Fopp p) (Fopp q)).

Theorem minusSameExp:
  (x, y:float) (Fexp x)=(Fexp y) ->
  (Fminus x y)=(Float (Zminus (Fnum x) (Fnum y)) (Fexp x)).

Definition Fmult :=
   [x, y:float](Float (Zmult (Fnum x) (Fnum y)) (Zplus (Fexp x) (Fexp y))).

Definition Fmult_correct: (x, y:float)<R> (Fmult x y)==(Rmult x y).

Theorem oneZplus:
  (x, y:Z)(Float (1) (Zplus x y))=(Fmult (Float (1) x) (Float (1) y)).
End operations.

30/05/01, 18:09