FroundMult.v

(****************************************************************************                                                                                         IEEE754  :  FroundMult                                                                                                                                          Laurent Thery  &  Sylvie Boldo                                                                                                                                     ***************************************************************************** *)
Require Export FroundProp.
Section FRoundP.
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)).

Theorem minRepMult:
  (p, q, fmin:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Rle R0 p) ->
  (Rle R0 q) ->
  (Zle (Zopp (dExp b)) (Zplus (Fexp p) (Fexp q))) ->
  (isMin b radix (Rmult p q) fmin) ->
  (Ex [r:float]
  r==(Rminus (Rmult p q) fmin) /\
  ((Fbounded b r) /\ (Fexp r)=(Zplus (Fexp p) (Fexp q)))).

Theorem maxRepMult:
  (p, q, fmax:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Rle R0 p) ->
  (Rle R0 q) ->
  (Zle (Zopp (dExp b)) (Zplus (Fexp p) (Fexp q))) ->
  (isMax b radix (Rmult p q) fmax) ->
  (Ex [r:float]
  r==(Rminus (Rmult p q) fmax) /\
  ((Fbounded b r) /\ (Fexp r)=(Zplus (Fexp p) (Fexp q)))).

Theorem multExpMin:
  (P:?) (RoundedModeP b radix P) ->
  (p, q, pq:float) (P (Rmult p q) pq) ->
  (Ex [s:float]
  (Fbounded b s) /\ (<R> s==pq /\ (Zle (Zplus (Fexp p) (Fexp q)) (Fexp s)))).

Theorem multExpUpperBound:
  (P:?) (RoundedModeP b radix P) ->
  (p, q, pq:float)
  (P (Rmult p q) pq) ->
  (Fbounded b p) ->
  (Fbounded b q) -> (Zle (Zopp (dExp b)) (Zplus (Fexp p) (Fexp q))) ->
  (Ex [r:float]
  (Fbounded b r) /\
  (<R> r==pq /\ (Zle (Fexp r) (Zplus precision (Zplus (Fexp p) (Fexp q)))))).

Theorem RepMult:
  (P:?) (RoundedModeP b radix P) ->
  (p, q, f:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Rle R0 p) ->
  (Rle R0 q) ->
  (Zle (Zopp (dExp b)) (Zplus (Fexp p) (Fexp q))) -> (P (Rmult p q) f) ->
  (Ex [r:float]
  r==(Rminus (Rmult p q) f) /\
  ((Fbounded b r) /\ (Fexp r)=(Zplus (Fexp p) (Fexp q)))).

Theorem multExactExp_aux:
  (n1, n2:Z)
  (Zle (Zabs n1) (vNum b)) ->
  (Zle (Zabs n2) (vNum b)) ->
  (Ex [ny:Z]
  (Ex [ey:Z]
  <R> (Rmult n1 n2)==(Rmult ny (powerRZ radix ey)) /\ (Zle (Zabs ny) (vNum b)))) ->
  (Ex [nx:Z]
  (Ex [ex:Z]
  <R> (Rmult n1 n2)==(Rmult nx (powerRZ radix ex)) /\
  ((Zle (Zabs nx) (vNum b)) /\ ((Zle ZERO ex) /\ (Zle ex precision))))).

Theorem Zabs_Fbounded1:
  (a:Z) (Zle (Zabs a) (vNum b)) ->(Zle (Zopp (vNum b)) a) /\ (Zle a (vNum b)).

Theorem multExactExp:
  (P:?) (RoundedModeP b radix P) ->
  (p, q, pq:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Rle R0 p) ->
  (Rle R0 q) ->
  (P (Rmult p q) pq) -> (Zle (Zopp (dExp b)) (Zplus (Fexp p) (Fexp q))) ->
  (ex
     float
     [r:float]
     (ex
        float
        [s:float]
        (Fbounded b r) /\
        ((Fbounded b s) /\
         (<R> r==pq /\
          (<R> s==(Rminus (Rmult p q) r) /\
           (<Z> (Fexp s)=(Zplus (Fexp p) (Fexp q)) /\
            ((Zle (Fexp s) (Fexp r)) /\
             (Zle (Fexp r) (Zplus precision (Zplus (Fexp p) (Fexp q))))))))))).
End FRoundP.

30/05/01, 18:14