ClosestPlus.v

(****************************************************************************                                                                                         IEEE754  :  ClosestPlus                                                                                                                                              Laurent Thery    & Sylvie Boldo                                                                                                                          ***************************************************************************** *)
Require Export FroundPlus.
Require Export ClosestProp.
Section ClosestP.
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne:(lt (S O) radix).
Hypothesis precisionGreaterThanOne:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).

Theorem errorBoundedPlusLe:
  (p, q, pq:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Zle (Fexp p) (Fexp q)) -> (Closest b radix (Rplus p q) pq) ->
  (Ex [error:float]
  <R> error==(Rabsolu (Rminus (Rplus p q) pq)) /\
  ((Fbounded b error) /\ (Fexp error)=(Zmin (Fexp p) (Fexp q)))).

Theorem errorBoundedPlusAbs:
  (p, q, pq:float)
  (Fbounded b p) -> (Fbounded b q) -> (Closest b radix (Rplus p q) pq) ->
  (Ex [error:float]
  <R> error==(Rabsolu (Rminus (Rplus p q) pq)) /\
  ((Fbounded b error) /\ (Fexp error)=(Zmin (Fexp p) (Fexp q)))).

Theorem errorBoundedPlus:
  (p, q, pq:float)
  (Fbounded b p) -> (Fbounded b q) -> (Closest b radix (Rplus p q) pq) ->
  (Ex [error:float]
  <R> error==(Rminus (Rplus p q) pq) /\
  ((Fbounded b error) /\ (Fexp error)=(Zmin (Fexp p) (Fexp q)))).

Theorem plusExact1:
  (p, q, r:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Closest b radix (Rplus p q) r) -> (Zle (Fexp r) (Zmin (Fexp p) (Fexp q))) ->
  <R> r==(Rplus p q).

Theorem plusExact1bis:
  (p, q, r:float)
  (Fbounded b p) ->
  (Fbounded b q) -> (Closest b radix (Rplus p q) r) -> ~ <R> r==(Rplus p q) ->
  (Zlt (Zmin (Fexp p) (Fexp q)) (Fexp r)).

Theorem plusExact2Aux:
  (p, q, r:float)
  (Rle R0 p) ->
  (Fcanonic radix b precision p) ->
  (Fbounded b q) ->
  (Closest b radix (Rplus p q) r) -> (Zlt (Fexp r) (Zpred (Fexp p))) ->
  <R> r==(Rplus p q).

Theorem plusExact2:
  (p, q, r:float)
  (Fcanonic radix b precision p) ->
  (Fbounded b q) ->
  (Closest b radix (Rplus p q) r) -> (Zlt (Fexp r) (Zpred (Fexp p))) ->
  <R> r==(Rplus p q).

Theorem plusExactR0:
  (p, q, r:float)
  (Fbounded b p) ->
  (Fbounded b q) -> (Closest b radix (Rplus p q) r) -> <R> r==R0 ->
  <R> r==(Rplus p q).

Theorem plusErrorBound1:
  (p, q, r:float)
  (Fbounded b p) ->
  (Fbounded b q) -> (Closest b radix (Rplus p q) r) -> ~ (is_Fzero r) ->
  (Rlt
     (Rabsolu (Rminus r (Rplus p q)))
     (Rmult (Rmult (Rabsolu r) (Rinv (2))) (Rmult radix (Rinv (vNum b))))).

Theorem plusErrorBound1bis:
  (p, q, r:float)
  (Fbounded b p) ->
  (Fbounded b q) -> (Closest b radix (Rplus p q) r) -> ~ (is_Fzero r) ->
  (Rle
     (Rabsolu (Rminus r (Rplus p q)))
     (Rmult
        (Rmult (Rabsolu r) (Rinv (2))) (Rmult radix (Rinv (plus (vNum b) (1)))))).

Theorem plusErrorBound1withZero:
  (p, q, r:float)
  (Fbounded b p) -> (Fbounded b q) -> (Closest b radix (Rplus p q) r) ->
  (Rle
     (Rabsolu (Rminus r (Rplus p q)))
     (Rmult (Rmult (Rabsolu r) (Rinv (2))) (Rmult radix (Rinv (vNum b))))).

Theorem RoundBound:
  (x, y, p:float)
  (Fbounded b x) ->
  (Fbounded b y) ->
  (Fbounded b p) ->
  (Closest b radix (Rplus x y) p) -> (lt radix (mult (2) (vNum b))) ->
  (Rle
     (Rabsolu p)
     (Rmult
        (Rabsolu (Rplus x y))
        (Rmult (Rmult (2) (vNum b)) (Rinv (Rminus (Rmult (2) (vNum b)) radix))))).

Theorem plusExactExp:
  (p, q, pq:float)
  (Fbounded b p) -> (Fbounded b q) -> (Closest b radix (Rplus p q) pq) ->
  (ex
     float
     [r:float]
     (ex
        float
        [s:float]
        (Fbounded b r) /\
        ((Fbounded b s) /\
         (<R> s==pq /\
          (<R> r==(Rminus (Rplus p q) s) /\
           (<Z> (Fexp r)=(Zmin (Fexp p) (Fexp q)) /\
            ((Zle (Fexp r) (Fexp s)) /\
             (Zle (Fexp s) (Zs (Zmax (Fexp p) (Fexp q))))))))))).

Theorem plusExactExpCanonic:
  (c, d, p, q:float)
  (Fbounded b c) ->
  (Fbounded b d) ->
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Closest b radix (Rplus c d) p) ->
  <R> q==(Rminus (Rplus c d) p) -> ~ <R> q==R0 ->
  (ex
     float
     [r:float]
     (ex
        float
        [s:float]
        (Fcanonic radix b precision s) /\
        ((Fbounded b r) /\
         (<R> s==p /\
          (<R> r==(Rminus (Rplus c d) s) /\
           (<Z> (Fexp r)=(Zmin (Fexp c) (Fexp d)) /\
            ((Zlt (Fexp r) (Fexp s)) /\
             (Zle (Fexp s) (Zs (Zmax (Fexp c) (Fexp d))))))))))).
End ClosestP.

30/05/01, 17:27