PradixE.v

(****************************************************************************                                                                                         IEEE754  :  PradixE.v                                                                                                                                        Laurent Thery  & Laurence Rideau                                                                                                                   ***************************************************************************** Same as Pradix but without correctness *)
Require Export FroundPlus.
Section prog.

(* Usual hypothesis *)
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.

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

(* An arbitrary rounding mode *)
Variable P:R -> float ->Prop.
Hypothesis ProundedMode:(RoundedModeP b radix P).

(* The operations + - *  and their property *)
Variable fplus:float -> float ->float.
Variable fminus:float -> float ->float.
Variable fmult:float -> float ->float.
Hypothesis fplusCorrect:
           (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
           (P (Rplus p q) (fplus p q)).
Hypothesis fminusCorrect:
           (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
           (P (Rminus p q) (fminus p q)).
Hypothesis fmultCorrect:
           (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
           (P (Rmult p q) (fmult p q)).

(* 0,1 et 2 *)
Variables f0, f1, f2:float.
Variable f0Bounded:(Fbounded b f0).
Variable f0Correct:<R> f0==O.
Variable f1Bounded:(Fbounded b f1).
Variable f1Correct:<R> f1==(1).
Variable f2Bounded:(Fbounded b f2).
Variable f2Correct:<R> f2==(2).

Theorem FcanonicLePos:
  (p, q:float)
  (Fcanonic radix b precision p) ->
  (Fcanonic radix b precision q) -> (Rle R0 p) -> (Rle p q) ->
  (Zlt (Fexp p) (Fexp q)) \/ (Fexp p)=(Fexp q) /\ (Zle (Fnum p) (Fnum q)).

Theorem boundedNorMinGivesExp:
  (x:Z)
  (p:float)
  (Fbounded b p) ->
  (Zle (Zopp (dExp b)) x) ->
  (Rle (Float (nNormMin radix precision) x) p) -> (Rle p (Float (vNum b) x)) ->
  (Fexp (Fnormalize radix b precision p))=x.

Theorem LtFnumZERO: (x:float) (Zlt ZERO (Fnum x)) ->(Rlt R0 x).

Theorem InBinade:
  (p, q, r:float)
  (e:Z)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (P (Rplus p q) r) ->
  (Zle (Zopp (dExp b)) e) ->
  (Rle (Float (exp radix (pred precision)) e) p) ->
  (Rle p (Float (vNum b) e)) -> (Rlt O q) -> (Rlt q (powerRZ radix e)) ->
  <R> r==p \/ <R> r==(Rplus p (powerRZ radix e)).
(* Properties to conclude for the first loop *)

Theorem Loop0:
  (p:float) (Fbounded b p) ->
  (n:nat) (le (1) n) -> (le n (vNum b)) -> <R> p==n ->
  <R> (fplus p f1)==(Rplus p f1).

Theorem Loop1:
  (p:float) (Fbounded b p) ->
  (n:nat) (lt (vNum b) n) -> (le n (mult radix (vNum b))) -> <R> p==n ->
  <R> (fplus p f1)==p \/ <R> (fplus p f1)==(Rplus p radix).

Theorem Loop2:
  (p:float) (Fbounded b p) ->
  (n:nat) (le (1) n) -> (le n (vNum b)) -> <R> p==n ->
  <R> (fminus (fplus p f1) p)==f1.

Theorem Loop3:
  (p:float) (Fbounded b p) ->
  (n:nat) (lt (vNum b) n) -> (le n (mult radix (vNum b))) -> <R> p==n ->
  ~ <R> (fminus (fplus p f1) p)==f1.

Theorem Loop4:
  (p:float) (Fbounded b p) ->
  (n:nat) (le (1) n) -> (le n (vNum b)) -> <R> p==n ->(Rlt p (fmult f2 p)).
(* Properties to conclude for the second loop *)

Theorem BLoop1:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
  (m, n:nat)
  (le (exp radix precision) m) ->
  (le m (mult radix (vNum b))) ->
  <R> p==m -> (le (1) n) -> (lt n radix) -> <R> q==n ->
  <R> (fplus p q)==p \/ <R> (fplus p q)==(Rplus p radix).

Theorem BLoop2:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
  (m, n:nat)
  (le (exp radix precision) m) ->
  (le m (mult radix (vNum b))) ->
  <R> p==m -> (le (1) n) -> (lt n radix) -> <R> q==n ->
  ~ <R> (fminus (fplus p q) p)==q.

Theorem BLoop3:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
  (m:nat)
  (le (exp radix precision) m) ->
  (le m (mult radix (vNum b))) -> <R> p==m -> <R> q==radix ->
  <R> (fminus (fplus p q) p)==q.

Theorem BLoop4:
  (p:float) (Fbounded b p) ->
  (n:nat) (le (1) n) -> (lt n radix) -> <R> p==n ->(Rlt p (fplus p f1)).

Lemma Loop6c:
  (p, b0:float) (Fbounded b p) ->
  (n:nat)
  (le (1) n) ->
  (le n (vNum b)) -> <R> p==n -> (Fbounded b b0) /\ <R> b0==radix ->
  (Rlt p (fmult p b0)).

Local feq := (Feq_bool radix).

Theorem Goal1:
  (x0:float)
  (Pre2:((ex
            nat [m:nat](le (1) m) /\ ((le m (mult radix (vNum b))) /\ <R> x0==m)))
        /\ (Fbounded b x0)) (Test1:(feq (fminus (fplus x0 f1) x0) f1)=true)
  (lt
     (minus (mult radix (vNum b)) (absolu (Int_part (fmult f2 x0))))
     (minus (mult radix (vNum b)) (absolu (Int_part x0)))) /\
  (((ex
       nat
       [m:nat]
       (le (1) m) /\ ((le m (mult radix (vNum b))) /\ <R> (fmult f2 x0)==m))) /\
   (Fbounded b (fmult f2 x0))).

Theorem Goal2:
  (x0:float)
  (Pre2:((ex
            nat [m:nat](le (1) m) /\ ((le m (mult radix (vNum b))) /\ <R> x0==m)))
        /\ (Fbounded b x0)) (Test1:(feq (fminus (fplus x0 f1) x0) f1)=false)
  ((ex
      nat
      [m:nat]
      (le (exp radix precision) m) /\
      ((le m (mult radix (vNum b))) /\ <R> x0==m))) /\ (Fbounded b x0).

Theorem Goal3:
  ((ex nat [m:nat](le (1) m) /\ ((le m (mult radix (vNum b))) /\ <R> f1==m))) /\
  (Fbounded b f1).

Theorem Goal4:
  (x0, y0:float)
  (Post2:((ex
             nat
             [m:nat]
             (le (exp radix precision) m) /\
             ((le m (mult radix (vNum b))) /\ <R> x0==m))) /\ (Fbounded b x0))
  (Pre4:((ex nat [m:nat](le (1) m) /\ ((le m radix) /\ <R> y0==m))) /\
        (Fbounded b y0)) (Test2:(feq (fminus (fplus x0 y0) x0) y0)=false)
  (lt
     (minus radix (absolu (Int_part (fplus y0 f1))))
     (minus radix (absolu (Int_part y0)))) /\
  (((ex nat [m:nat](le (1) m) /\ ((le m radix) /\ <R> (fplus y0 f1)==m))) /\
   (Fbounded b (fplus y0 f1))).

Theorem Goal5_6b:
  ((ex nat [m:nat](le (1) m) /\ ((le m radix) /\ <R> f1==m))) /\ (Fbounded b f1).

Theorem Goal5b:
  (x0, y0:float)
  (Post3:((ex
             nat
             [m:nat]
             (le (exp radix precision) m) /\
             ((le m (mult radix (vNum b))) /\ <R> x0==m))) /\ (Fbounded b x0))
  (Pre4:((ex nat [m:nat](le (1) m) /\ ((le m radix) /\ <R> y0==m))) /\
        (Fbounded b y0)) (Test2:(feq (fminus (fplus x0 y0) x0) y0)=true)
  (Fbounded b y0) /\ <R> y0==radix.

Theorem Goal6:
  (x0, y0:float)
  (Post2:((ex
             nat
             [m:nat]
             (le (exp radix precision) m) /\
             ((le m (mult radix (vNum b))) /\ <R> x0==m))) /\ (Fbounded b x0))
  (Post1:(((ex nat [m:nat](le (1) m) /\ ((le m radix) /\ <R> y0==m))) /\
          (Fbounded b y0)) /\ (feq (fminus (fplus x0 y0) x0) y0)=true)
  <R> y0==radix.

Theorem Goal7b:
  (b0, a2:float)
  (n0:nat)
  (Post2:(Fbounded b b0) /\ <R> b0==radix)
  (Pre6:((ex
            nat
            [m:nat]
            ((le (1) m) /\ ((le m (mult radix (vNum b))) /\ <R> a2==m)) /\
            m=(exp radix n0))) /\ (Fbounded b a2))
  (Test3:(feq (fminus (fplus a2 f1) a2) f1)=true)
  (lt
     (minus (mult radix (vNum b)) (absolu (Int_part (fmult a2 b0))))
     (minus (mult radix (vNum b)) (absolu (Int_part a2)))) /\
  (((ex
       nat
       [m:nat]
       ((le (1) m) /\ ((le m (mult radix (vNum b))) /\ <R> (fmult a2 b0)==m)) /\
       m=(exp radix (S n0)))) /\ (Fbounded b (fmult a2 b0))).

Theorem Goal8b:
  (ex
     nat
     [m:nat]
     ((le (1) m) /\ ((le m (mult radix (vNum b))) /\ <R> f1==m)) /\
     m=(exp radix (0))).

Theorem Goal9b:
  (a0, b0, a2:float)
  (n0:nat)
  (Post2:(Fbounded b b0) /\ <R> b0==radix)
  (Post1:(((ex
              nat
              [m:nat]
              ((le (1) m) /\ ((le m (mult radix (vNum b))) /\ <R> a2==m)) /\
              m=(exp radix n0))) /\ (Fbounded b a2)) /\
         (feq (fminus (fplus a2 f1) a2) f1)=false)<R> b0==radix /\ n0=precision.
End prog.

30/05/01, 18:25