Float.v

(****************************************************************************                                                                                         IEEE754  :  Float                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** ****************************************************** Module Float.v     Inspired by the Diadic of Patrick Loiseleur *******************************************************)
Require Export Omega.
Require Export Zcomplements.
Require Export Zpower.
Require Export Arith.
Require Export Compare.
Require Export Reals.
Require Export Rpower.
Require Export Faux.
Require Export NDiv.
Require Export Digit.
Require Export sTactic.
Section definitions.
Variable radix:nat.

Local zradix := (inject_nat radix).
Hypothesis radixMoreThanOne:(lt (S O) radix).

Theorem ltzbO: (Zlt ZERO zradix).
(* The type float represents the set of numbers who can be written:   x = n*b^p with  n and p in Z. (pdic numbers) n = Fnum and p = Fexp *)

Record float: Set := Float {
   Fnum: Z;
   Fexp: Z }.

Theorem floatEq: (p, q:float) (Fnum p)=(Fnum q) -> (Fexp p)=(Fexp q) ->p=q.

Theorem floatDec: (x, y:float){x=y}+{~ x=y}.

Definition Fzero := [x:Z](Float ZERO x).

Definition is_Fzero := [x:float](Fnum x)=ZERO.

Theorem is_FzeroP: (x:float)(is_Fzero x) \/ ~ (is_Fzero x).
Coercion IZR : Z >-> R.
Coercion INR : nat >-> R.
Coercion inject_nat : nat >-> Z.

Definition FtoR := [x:float](Rmult (Fnum x) (powerRZ (INR radix) (Fexp x))).
Coercion FtoR : float >-> R.

Theorem FzeroisReallyZero: (z:Z)<R> (Fzero z)==R0.

Theorem is_Fzero_rep1: (x:float) (is_Fzero x) -><R> x==R0.

Theorem is_Fzero_rep2: (x:float) <R> x==R0 ->(is_Fzero x).

Theorem NisFzeroComp: (x, y:float) ~ (is_Fzero x) -> <R> x==y ->~ (is_Fzero y).

Theorem not_ZERO_IZR: (z:Z) ~ z=ZERO ->~ (IZR z)==R0.
(* Some inegalities that will be helpful *)

Theorem Rlt_monotony_exp:
  (x, y:R) (z:Z) (Rlt x y) ->
  (Rlt (Rmult x (powerRZ radix z)) (Rmult y (powerRZ radix z))).

Theorem Rle_monotone_exp:
  (x, y:R) (z:Z) (Rle x y) ->
  (Rle (Rmult x (powerRZ radix z)) (Rmult y (powerRZ radix z))).

Theorem Rlt_mult_anticompatibility_exp:
  (x, y:R)
  (z:Z) (Rlt (Rmult x (powerRZ radix z)) (Rmult y (powerRZ radix z))) ->
  (Rlt x y).

Theorem Rle_mult_anticompatibility_exp:
  (x, y:R)
  (z:Z) (Rle (Rmult x (powerRZ radix z)) (Rmult y (powerRZ radix z))) ->
  (Rle x y).

Theorem FtoREqInv1:
  (p, q:float) ~ (is_Fzero p) -> <R> p==q -> (Fnum p)=(Fnum q) ->p=q.

Theorem FtoREqInv2: (p, q:float) <R> p==q -> (Fexp p)=(Fexp q) ->p=q.

Theorem Rlt_Float_Zlt: (p, q, r:Z) (Rlt (Float p r) (Float q r)) ->(Zlt p q).

Theorem Rle_Float_Zle: (p, q, r:Z) (Rle (Float p r) (Float q r)) ->(Zle p q).
(* Properties for floats with 1 as mantissa *)

Theorem oneExp_le: (x, y:Z) (Zle x y) ->(Rle (Float (1) x) (Float (1) y)).

Theorem oneExp_lt: (x, y:Z) (Rlt (Float (1) x) (Float (1) y)) ->(Zlt x y).

Theorem oneExp_Zle: (x, y:Z) (Rle (Float (1) x) (Float (1) y)) ->(Zle x y).

Definition Fdigit := [p:float](digit radix (absolu (Fnum p))).

Definition Fshift :=
   [n:nat] [x:float]
   (Float (Zmult (Fnum x) (Zpower_nat zradix n)) (Zminus (Fexp x) n)).

Theorem sameExpEq: (p, q:float) <R> p==q -> (Fexp p)=(Fexp q) ->p=q.

Theorem FshiftFdigit:
  (n:nat) (x:float) ~ (is_Fzero x) ->(Fdigit (Fshift n x))=(plus (Fdigit x) n).

Theorem FshiftCorrect: (n:nat) (x:float)<R> (Fshift n x)==x.

Theorem FshiftCorrectInv:
  (x, y:float) <R> x==y -> (Zle (Fexp x) (Fexp y)) ->
  (Fshift (absolu (Zminus (Fexp y) (Fexp x))) y)=x.

Theorem FshiftO: (x:float)(Fshift O x)=x.

Theorem FshiftCorrectSym:
  (x, y:float) <R> x==y ->(Ex [n:nat] (Ex [m:nat] (Fshift n x)=(Fshift m y))).

Theorem FshiftAdd:
  (n, m:nat) (p:float)(Fshift (plus n m) p)=(Fshift n (Fshift m p)).

Theorem ReqGivesEqwithSameExp:
  (p, q:float)
  (Ex [r:float] (Ex [s:float] <R> p==r /\ (<R> q==s /\ (Fexp r)=(Fexp s)))).

Theorem FdigitEq:
  (x, y:float) ~ (is_Fzero x) -> <R> x==y -> (Fdigit x)=(Fdigit y) ->x=y.
End definitions.

30/05/01, 17:57