Fast2Sum.v

(****************************************************************************                                                                                         IEEE754  :  Fast2Sum                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export Closest2Plus.
Section Fast.
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 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 IminusCorrect:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
  (Closest b (2) (Rminus p q) (Iminus p q)).

Theorem ErrorBoundedIplus:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
  (Ex [error:float]
  <R> error==(Rminus (Rplus p q) (Iplus p q)) /\ (Fbounded b error)).

Theorem IplusOr:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> <R> q==R0 ->
  <R> (Iplus p q)==p.

Theorem IminusId:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> <R> p==q ->
  <R> (Iminus p q)==R0.

Theorem IminusOl:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> <R> p==R0 ->
  <R> (Iminus p q)==(Ropp q).

Theorem IplusBounded:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->(Fbounded b (Iplus p q)).

Theorem IminusBounded:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->(Fbounded b (Iminus p q)).

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

Theorem IminusFminus:
  (p, q:float)
  (Fbounded b p) -> (Fbounded b q) -> (Fbounded b (Fminus (2) p q)) ->
  <R> (Iminus p q)==(Fminus (2) p q).

Theorem MDekkerAux1:
  (p, q:float)
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p) ->
  (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus q (Iminus (Iplus p q) p))==(Rminus (Rplus p q) (Iplus p q)).

Theorem MDekkerAux2:
  (p, q:float)
  <R> (Iplus p q)==(Rplus p q) -> (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).

Theorem MDekkerAux3:
  (p, q:float)
  (Fbounded b (Fplus (2) p q)) -> (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).

Theorem MDekkerAux4:
  (p, q:float)
  (Fbounded b (Fminus (2) (Iplus p q) p)) -> (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).

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

Theorem Dekker2:
  (p, q:float)
  (Rle R0 p) ->
  (Rle (Ropp q) p) ->
  (Rle p (Rmult (2) (Ropp q))) -> (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).

Theorem Dekker3:
  (p, q:float)
  (Rle q R0) ->
  (Rlt (Rmult (2) (Ropp q)) p) -> (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).

Theorem MDekkerAux5:
  (p, q:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  <R>
    (Iminus (Iplus (Fopp p) (Fopp q)) (Fopp p))==
    (Rminus (Iplus (Fopp p) (Fopp q)) (Fopp p)) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).

Theorem MDekker:
  (p, q:float)
  (Fbounded b p) -> (Fbounded b q) -> (Rle (Rabsolu q) (Rabsolu p)) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).

Theorem Dekker:
  (p, q:float)
  (Fbounded b p) -> (Fbounded b q) -> (Rle (Rabsolu q) (Rabsolu p)) ->
  <R> (Iminus q (Iminus (Iplus p q) p))==(Rminus (Rplus p q) (Iplus p q)).
End Fast.

30/05/01, 17:37