ThreeSum2.v

(****************************************************************************                                                                                         IEEE754  :  ThreeSum2                                                                                                                                        Laurent Thery & Sylvie Boldo                                                                                                                       ***************************************************************************** *)
Require Export Closest2Plus.
Section F2.
Variable b:Fbound.
Variable precision:nat.

Local FtoRradix := (FtoR (2)).
Coercion FtoRradix : float >-> R.

Theorem TwoMoreThanOne: (lt (S O) (2)).
Auto.
Qed.
Hints Resolve TwoMoreThanOne.
Hypothesis precisionNotZero:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp (2) precision) (1)).
Variables p, q, r, u, v, w, p', q', r':float.
Hypothesis Fp:(Fbounded b p).
Hypothesis Fq:(Fbounded b q).
Hypothesis Fr:(Fbounded b r).
Hypothesis Fu:(Fbounded b u).
Hypothesis Fv:(Fbounded b v).
Hypothesis Fw:(Fbounded b w).
Hypothesis Fp':(Fbounded b p').
Hypothesis Fq':(Fbounded b q').
Hypothesis Fr':(Fbounded b r').
Hypothesis epq:(Zle (Fexp q) (Fexp p)).
Hypothesis eqr:(Zle (Fexp r) (Fexp q)).
Hypothesis uDef:(Closest b (2) (Rplus q r) u).
Hypothesis vDef:<R> v==(Rminus (Rplus q r) u).
Hypothesis p'Def:(Closest b (2) (Rplus p u) p').
Hypothesis wDef:<R> w==(Rminus (Rplus p u) p').
Hypothesis q'Def:(Closest b (2) (Rplus w v) q').
Hypothesis r'Def:<R> r'==(Rminus (Rplus w v) q').

Theorem vNumPos: (Rle R0 (vNum b)).

Theorem TwoSumNul:
  (f, g, x:float)
  (Closest b (2) (Rplus f g) x) ->
  <R> x==R0 -> (Fbounded b f) -> (Fbounded b g) ->(Rminus (Rplus f g) x)==R0.

Theorem bound3Sum:
  ~ <R> r'==R0 ->
  (Rlt
     (Rabsolu (Rplus q' r'))
     (Rmult (Rmult (Rmult (3) (2)) (Rinv (vNum b))) (Rabsolu p'))).

Theorem exp3Sum:
  (Ex [p'':float]
  (Ex [q'':float]
  (Ex [r'':float]
  ((Fbounded b p'') /\ ((Fbounded b q'') /\ (Fbounded b r''))) /\
  ((<R> p''==p' /\ (<R> q''==q' /\ <R> r''==r')) /\
   ((Zle (Fexp r) (Fexp r'')) /\
    (((Zle (Fexp r'') (Fexp q'')) /\ (Zle (Fexp q'') (Fexp p''))) /\
     (Fexp r'')=(Fexp r))))))).

Theorem OutSum3:
  ~ <R> r'==R0 ->
  (Rlt
     (Float (1) (Fexp r))
     (Rmult
        (3)
        (Rmult
           (2)
           (Rmult
              (2)
              (Rmult
                 (Rabsolu p')
                 (Rinv (Rmult (vNum b) (Rminus (Rmult (2) (vNum b)) (2))))))))).

Theorem TwoSumNonNul:
  (p, q, r, pq:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Closest b (2) (Rplus p q) pq) ->
  <R> r==(Rminus (Rplus p q) pq) -> ~ <R> r==R0 ->~ <R> pq==R0.

Theorem TwoSumOneNul:
  (p, q, pq:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Fbounded b pq) -> (Closest b (2) (Rplus p q) pq) -> <R> p==R0 -><R> pq==q.

Theorem TwoSumOneNul2:
  (p, q, pq, r:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Fbounded b pq) ->
  (Closest b (2) (Rplus p q) pq) ->
  <R> p==R0 -> <R> r==(Rminus (Rplus p q) pq) -><R> r==R0.
End F2.

30/05/01, 18:28