FSucc.v

(****************************************************************************                                                                                         IEEE754  :  FSucc                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Import PolyList.
Require Import Float.
Require Import Fnorm.
Require Import Fop.
Require Import Fcomp.
Section suc.
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 FSucc :=
   [x:float]
      Cases (Z_eq_dec (Fnum x) (vNum b)) of
          (left _) => (Float (nNormMin radix precision) (Zs (Fexp x)))
         | (right _) =>
             Cases (Z_eq_dec (Fnum x) (Zopp (nNormMin radix precision))) of
                 (left _) => Cases (Z_eq_dec (Fexp x) (Zopp (dExp b))) of
                                 (left _) => (Float (Zs (Fnum x)) (Fexp x))
                                | (right _) =>
                                    (Float (Zopp (vNum b)) (Zpred (Fexp x)))
                             end
                | (right _) => (Float (Zs (Fnum x)) (Fexp x))
             end
      end.

Theorem FSuccSimpl1:
  (x:float) (Fnum x)=(vNum b) ->
  (FSucc x)=(Float (nNormMin radix precision) (Zs (Fexp x))).

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

Theorem FSuccSimpl3:
  (FSucc (Float (Zopp (nNormMin radix precision)) (Zopp (dExp b))))=
  (Float (Zs (Zopp (nNormMin radix precision))) (Zopp (dExp b))).

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

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

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

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

Theorem FSuccNormPos:
  (a:float) (Rle R0 a) -> (Fnormal radix b precision a) ->
  (Fnormal radix b precision (FSucc a)).

Theorem FSuccSubnormNotNearNormMin:
  (a:float)
  (Fsubnormal radix b precision a) ->
  ~ (Fnum a)=(pred (nNormMin radix precision)) ->
  (Fsubnormal radix b precision (FSucc a)).

Theorem FSuccSubnormNearNormMin:
  (a:float)
  (Fsubnormal radix b precision a) ->
  (Fnum a)=(pred (nNormMin radix precision)) ->
  (Fnormal radix b precision (FSucc a)).

Theorem FBoundedSuc: (f:float) (Fbounded b f) ->(Fbounded b (FSucc f)).

Theorem FSuccSubnormal:
  (a:float) (Fsubnormal radix b precision a) ->
  (Fcanonic radix b precision (FSucc a)).

Theorem FSuccPosNotMax:
  (a:float) (Rle R0 a) -> (Fcanonic radix b precision a) ->
  (Fcanonic radix b precision (FSucc a)).

Theorem FSuccNormNegNotNormMin:
  (a:float)
  (Rle a R0) ->
  (Fnormal radix b precision a) ->
  ~ a=(Float (Zopp (nNormMin radix precision)) (Zopp (dExp b))) ->
  (Fnormal radix b precision (FSucc a)).

Theorem FSuccNormNegNormMin:
  (Fsubnormal
     radix b precision
     (FSucc (Float (Zopp (nNormMin radix precision)) (Zopp (dExp b))))).

Theorem FSuccNegCanonic:
  (a:float) (Rle a R0) -> (Fcanonic radix b precision a) ->
  (Fcanonic radix b precision (FSucc a)).

Theorem FSuccCanonic:
  (a:float) (Fcanonic radix b precision a) ->
  (Fcanonic radix b precision (FSucc a)).

Theorem FSuccLt: (a:float)(Rlt a (FSucc a)).

Theorem FSuccPropPos:
  (x, y:float)
  (Rle R0 x) ->
  (Fcanonic radix b precision x) ->
  (Fcanonic radix b precision y) -> (Rlt x y) ->(Rle (FSucc x) y).

Theorem R0RltRleSucc: (x:float) (Rlt x R0) ->(Rle (FSucc x) R0).

Theorem FSuccPropNeg:
  (x, y:float)
  (Rlt x R0) ->
  (Fcanonic radix b precision x) ->
  (Fcanonic radix b precision y) -> (Rlt x y) ->(Rle (FSucc x) y).

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

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

Definition FNSucc := [x:?](FSucc (Fnormalize radix b precision x)).

Theorem FNSuccCanonic:
  (a:float) (Fbounded b a) ->(Fcanonic radix b precision (FNSucc a)).

Theorem FNSuccLt: (a:float)(Rlt a (FNSucc a)).

Theorem FNSuccProp:
  (x, y:float) (Fbounded b x) -> (Fbounded b y) -> (Rlt x y) ->
  (Rle (FNSucc x) y).

Theorem FNSuccEq:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> <R> p==q ->
  (FNSucc p)=(FNSucc q).
End suc.
Section suc1.
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:(lt (S O) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).

Theorem nNormMimLtvNum: (lt (nNormMin radix precision) (vNum b)).

Theorem FSucFSucMid:
  (p:float)
  ~ (Fnum (FSucc b radix precision p))=(nNormMin radix precision) ->
  ~ (Fnum (FSucc b radix precision p))=(Zopp (nNormMin radix precision)) ->
  <R>
    (Fminus
       radix (FSucc b radix precision (FSucc b radix precision p))
       (FSucc b radix precision p))==
    (Fminus radix (FSucc b radix precision p) p).

Theorem FNSuccFNSuccMid:
  (p:float)
  (Fbounded b p) ->
  ~ (Fnum (FNSucc b radix precision p))=(nNormMin radix precision) ->
  ~ (Fnum (FNSucc b radix precision p))=(Zopp (nNormMin radix precision)) ->
  <R>
    (Fminus
       radix (FNSucc b radix precision (FNSucc b radix precision p))
       (FNSucc b radix precision p))==
    (Fminus radix (FNSucc b radix precision p) p).
End suc1.
Hints Resolve nNormMimLtvNum :float.

30/05/01, 17:35