ThreeSumProps.v

(****************************************************************************                                                                                         IEEE754  :  ThreeSumProps                                                                                                                                    Sylvie Boldo                                                                                                                         ***************************************************************************** *)
Require Import Arith.
Require Import Omega.
Require Export Float.
Require Export Fop.
Require Export Fnorm.
Require Export MSB.
Require Export ThreeSum2.
Section F2.
Variable b:Fbound.
Variable precision:nat.

Local FtoRradix := (FtoR (2)).
Coercion FtoRradix : float >-> R.
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').
Hypothesis Ngd:(Rle R1 (Rmult (vNum b) (Rminus R1 (Rinv (2))))).
Hypothesis Hplus:
           (<R> p==R0 \/ (<R> q==R0 \/ <R> r==R0)) \/
           (Rle
              (Rabsolu q)
              (Rmult
                 (vNum b) (Rminus (Float (1) (Fexp p)) (Float (1) (Fexp r))))).
Hypothesis Ngd2:
           (Rle (6) (Rmult (vNum b) (Rminus R1 (Rmult (Rinv (2)) (Rinv (2)))))).

Theorem FTS:
  (Rle
     (Rabsolu q)
     (Rmult (vNum b) (Rminus (Float (1) (Fexp p)) (Float (1) (Fexp r))))) ->
  (Ex [u'':float] <R> u''==u /\ ((Fbounded b u'') /\ (Zle (Fexp u'') (Fexp p)))).

Theorem FTSinSum3_allcases:
  ~ <R> p==R0 ->
  (Ex [u'':float] <R> u''==u /\ ((Fbounded b u'') /\ (Zle (Fexp u'') (Fexp p)))).

Theorem PuissLessThanHalf:
  (z:Z)(Rle (Rmult (Float (1) z) (Rinv (2))) (Float (1) z)).

Theorem ThreeSumLoop:
  (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)))) /\
   (<R> r'==R0 /\
    (<R> p''==R0 \/
     (Rle
        (Rabsolu q'')
        (Rmult (vNum b) (Rminus (Float (1) (Fexp p'')) (Float (1) (Fexp r))))))
    \/
    ~ <R> r'==R0 /\
    (Rle
       (Rabsolu r'')
       (Rmult (vNum b) (Rminus (Float (1) (Fexp q'')) (Float (1) (Fexp r)))))))))).
End F2.

30/05/01, 18:29