Pradix.v

(****************************************************************************                                                                                         IEEE754  :  PradixE.v                                                                                                                                        Laurent Thery  & Laurence Rideau                                                                                                                   ***************************************************************************** Proof of Malcom's test program *)
Require Import Programs.
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).

Correctness i_exp
  let x = ref f1 in
  let y = ref f1 in
  let n = ref O in
  begin
    while (feq (fminus (fplus !x f1) !x) f1) do
        { invariant (Ex [m:nat] ((le (1) m)/\ (le m (mult radix (vNum b)))/\
                                <R> x == m)) /\ (Fbounded b x)
          variant (minus (mult radix (vNum b)) (absolu (Int_part x))) for lt }
        x := (fmult f2 !x)
      done
     {(Ex [m:nat] ((le (exp radix precision) m)/\ (le m (mult radix (vNum b)))/\
                                <R> x == m)) /\ (Fbounded b x)
     }
    ;
    while (not (feq (fminus (fplus !x !y) !x) !y)) do
        { invariant (Ex [m:nat] (le (1) m)/\ (le m radix) /\
                                <R> y == m) /\ (Fbounded b y)
          variant (minus radix (absolu (Int_part y))) for lt }
        y := (fplus !y f1)
      done {(Fbounded b y)/\<R> y == radix};
    x:=f1;
    while (feq (fminus (fplus !x f1) !x) f1) do
        { invariant (Ex [m:nat] ((le (1) m)/\ (le m (mult radix (vNum b)))/\
                                <R> x == m)/\ m= (exp radix n)) /\ (Fbounded b x)
          variant (minus (mult radix (vNum b)) (absolu (Int_part x))) for lt }
        x := (fmult !x !y); n := (S !n)
      done
    end
    { <R> y == radix /\ n = precision }
.
End prog.

30/05/01, 18:23