FPred.v

(****************************************************************************                                                                                         IEEE754  :  FPred                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Import PolyList.
Require Import Float.
Require Import Fnorm.
Require Import Fop.
Require Import Fcomp.
Require Import FSucc.
Section pred.
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.

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

Definition FPred :=
   [x:float]
      Cases (Z_eq_dec (Fnum x) (Zopp (vNum b))) of
          (left _) => (Float (Zopp (nNormMin radix precision)) (Zs (Fexp x)))
         | (right _) => Cases (Z_eq_dec (Fnum x) (nNormMin radix precision)) of
                            (left _) =>
                              Cases (Z_eq_dec (Fexp x) (Zopp (dExp b))) of
                                  (left _) => (Float (Zpred (Fnum x)) (Fexp x))
                                 | (right _) =>
                                     (Float (vNum b) (Zpred (Fexp x)))
                              end
                           | (right _) => (Float (Zpred (Fnum x)) (Fexp x))
                        end
      end.

Theorem FPredSimpl1:
  (x:float) (Fnum x)=(Zopp (vNum b)) ->
  (FPred x)=(Float (Zopp (nNormMin radix precision)) (Zs (Fexp x))).

Theorem FPredSimpl2:
  (x:float) (Fnum x)=(nNormMin radix precision) -> ~ (Fexp x)=(Zopp (dExp b)) ->
  (FPred x)=(Float (vNum b) (Zpred (Fexp x))).

Theorem FPredSimpl3:
  (FPred (Float (nNormMin radix precision) (Zopp (dExp b))))=
  (Float (Zpred (nNormMin radix precision)) (Zopp (dExp b))).

Theorem FPredSimpl4:
  (x:float)
  ~ (Fnum x)=(Zopp (vNum b)) -> ~ (Fnum x)=(nNormMin radix precision) ->
  (FPred x)=(Float (Zpred (Fnum x)) (Fexp x)).

Theorem FPredFopFSucc:
  (x:float)(FPred x)=(Fopp (FSucc b radix precision (Fopp x))).

Theorem FPredDiff1:
  (x:float) ~ (Fnum x)=(nNormMin radix precision) ->
  <R> (Fminus radix x (FPred x))==(Float (1) (Fexp x)).

Theorem FPredDiff2:
  (x:float) (Fnum x)=(nNormMin radix precision) -> (Fexp x)=(Zopp (dExp b)) ->
  <R> (Fminus radix x (FPred x))==(Float (1) (Fexp x)).

Theorem FPredDiff3:
  (x:float) (Fnum x)=(nNormMin radix precision) -> ~ (Fexp x)=(Zopp (dExp b)) ->
  <R> (Fminus radix x (FPred x))==(Float (1) (Zpred (Fexp x))).

Theorem FBoundedPred: (f:float) (Fbounded b f) ->(Fbounded b (FPred f)).

Theorem FPredCanonic:
  (a:float) (Fcanonic radix b precision a) ->
  (Fcanonic radix b precision (FPred a)).

Theorem FPredLt: (a:float)(Rlt (FPred a) a).

Theorem R0RltRlePred: (x:float) (Rlt R0 x) ->(Rle R0 (FPred x)).

Theorem FPredProp:
  (x, y:float)
  (Fcanonic radix b precision x) ->
  (Fcanonic radix b precision y) -> (Rlt x y) ->(Rle x (FPred y)).

Theorem FPredZleEq:
  (p, q:float) (Rlt (FPred p) q) -> (Rle q p) -> (Zle (Fexp p) (Fexp q)) ->
  <R> p==q.

Definition FNPred := [x:float](FPred (Fnormalize radix b precision x)).

Theorem FNPredFopFNSucc:
  (x:float)(FNPred x)=(Fopp (FNSucc b radix precision (Fopp x))).

Theorem FNPredCanonic:
  (a:float) (Fbounded b a) ->(Fcanonic radix b precision (FNPred a)).

Theorem FNPredLt: (a:float)(Rlt (FNPred a) a).

Theorem FNPredProp:
  (x, y:float) (Fbounded b x) -> (Fbounded b y) -> (Rlt x y) ->
  (Rle x (FNPred y)).

Theorem FPredSuc:
  (x:float) (Fcanonic radix b precision x) ->
  (FPred (FSucc b radix precision x))=x.

Theorem FSucPred:
  (x:float) (Fcanonic radix b precision x) ->
  (FSucc b radix precision (FPred x))=x.

Theorem FNPredSuc:
  (x:float) (Fbounded b x) -><R> (FNPred (FNSucc b radix precision x))==x.

Theorem FNPredSucEq:
  (x:float) (Fcanonic radix b precision x) ->
  (FNPred (FNSucc b radix precision x))=x.

Theorem FNSucPred:
  (x:float) (Fbounded b x) -><R> (FNSucc b radix precision (FNPred x))==x.

Theorem FNSucPredEq:
  (x:float) (Fcanonic radix b precision x) ->
  (FNSucc b radix precision (FNPred x))=x.
End pred.

30/05/01, 17:32