TwoSum.v

(****************************************************************************                                                                                         IEEE754  :  TwoSum                                                                                                                                           Laurent Thery & Sylvie Boldo                                                                                                                       ***************************************************************************** *)
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 IplusOl:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> <R> p==R0 ->
  <R> (Iplus p q)==q.

Local IminusCorrect := (IminusCorrect b Iplus IplusCorrect Iminus IminusPlus).

Local IplusBounded := (IplusBounded b Iplus IplusCorrect).

Local IminusBounded := (IminusBounded b Iplus IplusCorrect Iminus IminusPlus).

Local IminusId := (IminusId b Iplus IplusCorrect Iminus IminusPlus).

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

Theorem IplusCorrectEq:
  (p, q, pq:float)
  (r:R)
  (Fbounded b p) ->
  (Fbounded b q) -> (Fbounded b pq) -> <R> r==pq -> <R> (Rplus p q)==pq ->
  <R> (Iplus p q)==r.

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

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

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

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

Theorem IminusOp: (p, q:float)(Fopp (Iminus p q))=(Iminus (Fopp p) (Fopp q)).

Theorem MKnuthOpp:
  (p, q:float)
  <R>
    (Iplus
       (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
       (Iminus q (Iminus (Iplus p q) p)))==
    (Fopp
       (Iplus
          (Iminus
             (Fopp p)
             (Iminus
                (Iplus (Fopp p) (Fopp q))
                (Iminus (Iplus (Fopp p) (Fopp q)) (Fopp p))))
          (Iminus (Fopp q) (Iminus (Iplus (Fopp p) (Fopp q)) (Fopp p))))).

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

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

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

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

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

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

30/05/01, 18:30