Closest2Plus.v

(****************************************************************************                                                                                         IEEE754  :  Closest2Plus                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export ClosestPlus.
Require Export Closest2Prop.
Section F2.
Variable b:Fbound.
Variable precision:nat.

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

Theorem TwoMoreThanOne: (lt (S O) (2)).
Hypothesis precisionNotZero:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp (2) precision) (1)).

Theorem plusUpperBound:
  (P:?) (RoundedModeP b (2) P) ->
  (p, q, pq:float) (P (Rplus p q) pq) -> (Fbounded b p) -> (Fbounded b q) ->
  (Rle (Rabsolu pq) (Rmult (2) (Rmax (Rabsolu p) (Rabsolu q)))).

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

Theorem plusClosestLowerBoundAux1:
  (p, q, pq:float)
  (Rle (Rabsolu q) p) ->
  (Closest b (2) (Rplus p q) pq) ->
  (Fbounded b p) -> (Fbounded b q) -> ~ pq==(Rplus p q) ->
  (Rle (Rmult (Rinv (2)) p) pq).

Theorem plusClosestLowerBoundAux2:
  (p, q, pq:float)
  (Closest b (2) (Rplus p q) pq) ->
  (Fbounded b p) ->
  (Fbounded b q) -> ~ pq==(Rplus p q) -> (Rle (Rabsolu p) (Rabsolu q)) ->
  (Rle (Rmult (Rinv (2)) (Rabsolu q)) (Rabsolu pq)).

Theorem plusClosestLowerBound:
  (p, q, pq:float)
  (Closest b (2) (Rplus p q) pq) ->
  (Fbounded b p) -> (Fbounded b q) -> ~ pq==(Rplus p q) ->
  (Rle (Rmult (Rinv (2)) (Rmax (Rabsolu p) (Rabsolu q))) (Rabsolu pq)).
End F2.

30/05/01, 17:24