EFast2Sum.v

(****************************************************************************                                                                                         IEEE754  :  EFast2Sum                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export Fast2Sum.
Section EFast.
Variable b:Fbound.
Variable precision:nat.

Local FtoRradix := (FtoR (2)).
Coercion FtoRradix : float >-> R.
Hypothesis precisionGreaterThanOne:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp (2) precision) (1)).
Variable Iplus:float -> float ->float.
Hypothesis IplusCorrect:
           (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
           (Closest b (2) (Rplus p q) (Iplus p q)).
Hypothesis IplusComp:
           (p, q, r, s:float)
           (Fbounded b p) ->
           (Fbounded b q) ->
           (Fbounded b r) -> (Fbounded b s) -> <R> p==r -> <R> q==s ->
           <R> (Iplus p q)==(Iplus r s).
Hypothesis IplusSym:(p, q:float)(Iplus p q)=(Iplus q p).
Hypothesis IplusOp:(p, q:float)(Fopp (Iplus p q))=(Iplus (Fopp p) (Fopp q)).
Variable Iminus:float -> float ->float.
Hypothesis IminusPlus:(p, q:float)(Iminus p q)=(Iplus p (Fopp q)).

Theorem IminusComp:
  (p, q, r, s:float)
  (Fbounded b p) ->
  (Fbounded b q) -> (Fbounded b r) -> (Fbounded b s) -> <R> p==r -> <R> q==s ->
  <R> (Iminus p q)==(Iminus r s).

Theorem EvenBound:
  (p:float)
  (m:Z)
  (Even (absolu m)) ->
  (Zle (minus (exp (2) precision) (1)) m) ->
  (Zle m (minus (exp (2) (S precision)) (2))) -> (Fbounded b p) ->
  (Ex [q:float] (Fbounded b q) /\ <R> q==(Float m (Fexp p))).

Theorem ExtMDekker1:
  (p, q:float)
  (Fbounded b p) -> (Fbounded b q) -> (Zle (Fexp q) (Fexp p)) -> (Rle R0 p) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).

Theorem ExtMDekker:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> (Zle (Fexp q) (Fexp p)) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).

Theorem ExtDekker:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> (Zle (Fexp q) (Fexp p)) ->
  <R> (Iminus q (Iminus (Iplus p q) p))==(Rminus (Rplus p q) (Iplus p q)).
End EFast.

30/05/01, 17:30