Fnorm.v

(****************************************************************************                                                                                         IEEE754  :  Fnorm                                                                                                                                              Laurent Thery  &  Sylvie Boldo                                                                                                                                   ***************************************************************************** *)
Require Import Float.
Require Import Fcomp.
Require Import Fop.
Section Fbounded_Def.
Variable radix:nat.
Hypothesis radixMoreThanOne:(lt (1) radix).

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

Record Fbound: Set := Bound {
   vNum: nat;
   dExp: nat }.

Definition Fbounded :=
   [b:Fbound] [d:float]
   ((Zle (Zopp (vNum b)) (Fnum d)) /\ (Zle (Fnum d) (vNum b))) /\
   (Zle (Zopp (dExp b)) (Fexp d)).

Theorem isBounded: (b:Fbound) (p:float){(Fbounded b p)}+{~ (Fbounded b p)}.

Theorem pBounded_absolu:
  (b:Fbound) (p:float) (Fbounded b p) ->(le (absolu (Fnum p)) (vNum b)).

Theorem FzeroisZero: (b:Fbound)<R> (Fzero (Zopp (dExp b)))==R0.

Theorem FboundedFzero: (b:Fbound)(Fbounded b (Fzero (Zopp (dExp b)))).

Theorem FboundedZeroSameExp:
  (b:Fbound) (p:float) (Fbounded b p) ->(Fbounded b (Fzero (Fexp p))).

Theorem FBoundedScale:
  (b:Fbound) (p:float) (n:nat) (Fbounded b p) ->
  (Fbounded b (Float (Fnum p) (Zplus (Fexp p) n))).

Theorem FvalScale:
  (b:Fbound) (p:float) (n:nat)
  <R> (Float (Fnum p) (Zplus (Fexp p) n))==(Rmult (powerRZ radix n) p).

Theorem Fbounded_Zabs:
  (b:Fbound) (f:float) (Fbounded b f) ->(Zle (Zabs (Fnum f)) (vNum b)).

Theorem oppBounded: (b:Fbound) (x:float) (Fbounded b x) ->(Fbounded b (Fopp x)).

Theorem oppBoundedInv:
  (b:Fbound) (x:float) (Fbounded b (Fopp x)) ->(Fbounded b x).

Theorem FopRepAux:
  (b:Fbound)
  (z:Z)
  (p:R)
  ((ex float [r:float]<R> r==(Ropp p) /\ ((Fbounded b r) /\ (Fexp r)=z))) ->
  (ex float [r:float]<R> r==p /\ ((Fbounded b r) /\ (Fexp r)=z)).

Theorem absFBounded:
  (b:Fbound) (f:float) (Fbounded b f) ->(Fbounded b (Fabs f)).

Theorem FboundedEqExpPos:
  (b:Fbound)
  (p, q:float)
  (Fbounded b p) -> <R> p==q -> (Rle (Fexp p) (Fexp q)) -> (Rle R0 q) ->
  (Fbounded b q).

Theorem FboundedEqExp:
  (b:Fbound)
  (p, q:float) (Fbounded b p) -> <R> p==q -> (Rle (Fexp p) (Fexp q)) ->
  (Fbounded b q).

Theorem eqExpLess:
  (b:Fbound) (p, q:float) (Fbounded b p) -> <R> p==q ->
  (Ex [r:float] (Fbounded b r) /\ (<R> r==q /\ (Rle (Fexp q) (Fexp r)))).

Theorem FboundAlt:
  (b:Fbound)
  (p:float) (Zle (Zabs (Fnum p)) (vNum b)) -> (Zle (Zopp (dExp b)) (Fexp p)) ->
  (Fbounded b p).

Theorem FboundedShiftLess:
  (b:Fbound) (f:float) (n, m:nat) (le m n) -> (Fbounded b (Fshift radix n f)) ->
  (Fbounded b (Fshift radix m f)).

Theorem eqExpMax:
  (b:Fbound)
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> (Rle (Fabs p) q) ->
  (Ex [r:float] (Fbounded b r) /\ (<R> r==p /\ (Zle (Fexp r) (Fexp q)))).

Theorem LessExpBound:
  (b:Fbound)
  (p, q:float)
  (Fbounded b p) ->
  (Fbounded b q) -> (Zle (Fexp q) (Fexp p)) -> (Rle R0 p) -> (Rle p q) ->
  (Ex [m:Z] <R> (Float m (Fexp q))==p /\ (Fbounded b (Float m (Fexp q)))).

Theorem maxFbounded:
  (b:Fbound) (z:Z) (Zle (Zopp (dExp b)) z) ->(Fbounded b (Float (vNum b) z)).

Theorem maxMax:
  (b:Fbound) (p:float) (z:Z) (Fbounded b p) -> (Zle (Fexp p) z) ->
  (Rle (Fabs p) (Float (vNum b) z)).
End Fbounded_Def.
Section Fnormalized_Def.
Variable radix:nat.
Hypothesis radixMoreThanOne:(lt (1) radix).

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Variable b:Fbound.
Variable precision:nat.
Hypothesis precisionNotZero:~ precision=O.
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).

Theorem FboundNext:
  (p:float) (Fbounded b p) ->
  (Ex [q:float] (Fbounded b q) /\ <R> q==(Float (Zs (Fnum p)) (Fexp p))).

Theorem lt_vNum: (lt O (vNum b)).

Theorem digitVNumiSPrecision: (digit radix (vNum b))=precision.

Theorem vNumPrecision: (n:nat) (le (digit radix n) precision) ->(le n (vNum b)).

Theorem pGivesDigit: (p:float) (Fbounded b p) ->(le (Fdigit radix p) precision).

Theorem digitGivesBoundedNum:
  (p:float) (le (Fdigit radix p) precision) ->
  (Zle (Zopp (vNum b)) (Fnum p)) /\ (Zle (Fnum p) (vNum b)).

Theorem FboundedOne: (z:Z) (Zle (Zopp (dExp b)) z) ->(Fbounded b (Float (1) z)).

Theorem FboundedMbound:
  (z:Z) (m:nat) (le m (exp radix precision)) -> (Zle (Zopp (dExp b)) z) ->
  (Ex [c:float] (Fbounded b c) /\ <R> c==(Rmult m (powerRZ radix z))).

Definition Fnormal := [p:float](Fbounded b p) /\ (Fdigit radix p)=precision.

Theorem FnormalNotZero: (p:float) (Fnormal p) ->~ (is_Fzero p).

Theorem FnormalUnique:
  (p, q:float) (Fnormal p) -> (Fnormal q) -> <R> p==q ->p=q.

Theorem FnormalFop: (p:float) (Fnormal p) ->(Fnormal (Fopp p)).

Theorem FnormalLtPos:
  (p, q:float) (Fnormal p) -> (Fnormal q) -> (Rle R0 p) -> (Rlt p q) ->
  (Zlt (Fexp p) (Fexp q)) \/ (Fexp p)=(Fexp q) /\ (Zlt (Fnum p) (Fnum q)).

Theorem FnormalLtNeg:
  (p, q:float) (Fnormal p) -> (Fnormal q) -> (Rle q R0) -> (Rlt p q) ->
  (Zlt (Fexp q) (Fexp p)) \/ (Fexp p)=(Fexp q) /\ (Zlt (Fnum p) (Fnum q)).

Definition nNormMin := (exp radix (pred precision)).

Theorem nNormNotZero: ~ nNormMin=O.

Theorem digitnNormMin: (digit radix nNormMin)=precision.

Theorem nNrMMimLevNum: (le nNormMin (vNum b)).

Definition firstNormalPos := (Float nNormMin (Zopp (dExp b))).

Theorem firstNormalPosNormal: (Fnormal firstNormalPos).

Theorem pNormal_absolu_min:
  (p:float) (Fnormal p) ->(le nNormMin (absolu (Fnum p))).

Theorem maxMaxBis:
  (p:float) (z:Z) (Fbounded b p) -> (Zlt (Fexp p) z) ->
  (Rlt (Fabs p) (Float nNormMin z)).

Theorem FnormalLtFirstNormalPos:
  (p:float) (Fnormal p) -> (Rle R0 p) ->(Rle firstNormalPos p).

Theorem FnormalLtFirstNormalNeg:
  (p:float) (Fnormal p) -> (Rle p R0) ->(Rle p (Fopp firstNormalPos)).

Theorem FnormalBoundAbs:
  (p:float) (Fnormal p) ->(Rlt (Float (vNum b) (Zpred (Fexp p))) (Fabs p)).

Theorem FnormalBoundAbs2:
  (p:float) (Fnormal p) ->
  (Rle (Rmult (plus (vNum b) (1)) (Float (1) (Zpred (Fexp p)))) (Fabs p)).

Definition Fsubnormal :=
   [p:float]
   (Fbounded b p) /\
   ((Fexp p)=(Zopp (dExp b)) /\ (lt (Fdigit radix p) precision)).

Theorem FsubnormFopp: (p:float) (Fsubnormal p) ->(Fsubnormal (Fopp p)).

Theorem FsubnormalUnique:
  (p, q:float) (Fsubnormal p) -> (Fsubnormal q) -> <R> p==q ->p=q.

Theorem FsubnormalLt:
  (p, q:float) (Fsubnormal p) -> (Fsubnormal q) -> (Rlt p q) ->
  (Zlt (Fnum p) (Fnum q)).

Theorem LtFsubnormal:
  (p, q:float) (Fsubnormal p) -> (Fsubnormal q) -> (Zlt (Fnum p) (Fnum q)) ->
  (Rlt p q).

Theorem pSubnormal_absolu_min:
  (p:float) (Fsubnormal p) ->(lt (absolu (Fnum p)) nNormMin).

Theorem FsubnormalLtFirstNormalPos:
  (p:float) (Fsubnormal p) -> (Rle R0 p) ->(Rlt p firstNormalPos).

Theorem FsubnormalnormalLtPos:
  (p, q:float) (Fsubnormal p) -> (Fnormal q) -> (Rle R0 p) -> (Rle R0 q) ->
  (Rlt p q).

Theorem FsubnormalnormalLtNeg:
  (p, q:float) (Fsubnormal p) -> (Fnormal q) -> (Rle p R0) -> (Rle q R0) ->
  (Rlt q p).

Definition Fnormalize :=
   [p:float]
      Cases (Z_zerop (Fnum p)) of
          (left _) => (Float ZERO (Zopp (dExp b)))
         | (right _) =>
             (Fshift
                radix
                (min
                   (minus precision (Fdigit radix p))
                   (absolu (Zplus (dExp b) (Fexp p)))) p)
      end.

Theorem FnormalizeCorrect: (p:float)<R> (Fnormalize p)==p.

Theorem Fnormalize_Fopp: (p:float)(Fnormalize (Fopp p))=(Fopp (Fnormalize p)).

Theorem FnormalizeBounded:
  (p:float) (Fbounded b p) ->(Fbounded b (Fnormalize p)).

Definition Fcanonic := [a:float](Fnormal a) \/ (Fsubnormal a).

Theorem FcanonicBound: (p:float) (Fcanonic p) ->(Fbounded b p).

Theorem pUCanonic_absolu:
  (p:float) (Fcanonic p) ->(le (absolu (Fnum p)) (vNum b)).

Theorem FcanonicFopp: (p:float) (Fcanonic p) ->(Fcanonic (Fopp p)).

Theorem FcanonicFabs: (p:float) (Fcanonic p) ->(Fcanonic (Fabs p)).

Theorem FnormalizeCanonic: (p:float) (Fbounded b p) ->(Fcanonic (Fnormalize p)).

Theorem FcanonicLtPos:
  (p, q:float) (Fcanonic p) -> (Fcanonic q) -> (Rle R0 p) -> (Rlt p q) ->
  (Zlt (Fexp p) (Fexp q)) \/ (Fexp p)=(Fexp q) /\ (Zlt (Fnum p) (Fnum q)).

Theorem FcanonicLtNeg:
  (p, q:float) (Fcanonic p) -> (Fcanonic q) -> (Rle q R0) -> (Rlt p q) ->
  (Zlt (Fexp q) (Fexp p)) \/ (Fexp p)=(Fexp q) /\ (Zlt (Fnum p) (Fnum q)).

Theorem NormalNotSubNormal: (p:float)~ ((Fnormal p) /\ (Fsubnormal p)).

Theorem NormalAndSubNormalNotEq:
  (p, q:float) (Fnormal p) -> (Fsubnormal q) ->~ <R> p==q.

Theorem FcanonicUnique:
  (p, q:float) (Fcanonic p) -> (Fcanonic q) -> <R> p==q ->p=q.

Theorem FcanonicFormalizeEq: (p:float) (Fcanonic p) ->(Fnormalize p)=p.

Theorem FcanonicPosFexpRlt:
  (x, y:float)
  (Rle R0 x) ->
  (Rle R0 y) -> (Fcanonic x) -> (Fcanonic y) -> (Zlt (Fexp x) (Fexp y)) ->
  (Rlt x y).

Theorem FcanonicNegFexpRlt:
  (x, y:float)
  (Rle x R0) ->
  (Rle y R0) -> (Fcanonic x) -> (Fcanonic y) -> (Zlt (Fexp x) (Fexp y)) ->
  (Rlt y x).

Theorem MaxFloat:
  (x:float) (Fbounded b x) ->(Rle (Rabsolu x) (Float (vNum b) (Fexp x))).

Theorem FcanonicLeastExp:
  (x, y:float) <R> x==y -> (Fbounded b x) -> (Fcanonic y) ->
  (Zle (Fexp y) (Fexp x)).

Theorem Fcanonic_Rle_Zle:
  (x, y:float) (Fcanonic x) -> (Fcanonic y) -> (Rle (Rabsolu x) (Rabsolu y)) ->
  (Zle (Fexp x) (Fexp y)).
End Fnormalized_Def.

30/05/01, 18:04