FroundPlus.v

(****************************************************************************                                                                                         IEEE754  :  FroundPlus                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export FroundProp.
Require Import Finduct.
Section FRoundP.
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 plusExpMin:
  (P:?) (RoundedModeP b radix P) ->
  (p, q, pq:float) (P (Rplus p q) pq) ->
  (Ex [s:float]
  (Fbounded b s) /\ (<R> s==pq /\ (Zle (Zmin (Fexp p) (Fexp q)) (Fexp s)))).

Theorem plusExpUpperBound:
  (P:?) (RoundedModeP b radix P) ->
  (p, q, pq:float) (P (Rplus p q) pq) -> (Fbounded b p) -> (Fbounded b q) ->
  (Ex [r:float]
  (Fbounded b r) /\ (<R> r==pq /\ (Zle (Fexp r) (Zs (Zmax (Fexp p) (Fexp q)))))).

Theorem plusExpBound:
  (P:?) (RoundedModeP b radix P) ->
  (p, q, pq:float) (P (Rplus p q) pq) -> (Fbounded b p) -> (Fbounded b q) ->
  (Ex [r:float]
  (Fbounded b r) /\
  (<R> r==pq /\
   ((Zle (Zmin (Fexp p) (Fexp q)) (Fexp r)) /\
    (Zle (Fexp r) (Zs (Zmax (Fexp p) (Fexp q))))))).

Theorem minusRoundRep:
  (P:?) (RoundedModeP b radix P) ->
  (p, q, qmp, qmmp:float)
  (Rle R0 p) ->
  (Rle p q) -> (P (Rminus q p) qmp) -> (Fbounded b p) -> (Fbounded b q) ->
  (Ex [r:float] (Fbounded b r) /\ r==(Rminus q qmp)).

Theorem radixRangeBoundExp:
  (p, q:float)
  (Fcanonic radix b precision p) ->
  (Fcanonic radix b precision q) ->
  (Rle R0 p) -> (Rlt p q) -> (Rlt q (Rmult radix p)) ->
  (Fexp p)=(Fexp q) \/ (Zs (Fexp p))=(Fexp q).

Theorem ExactMinusIntervalAux:
  (P:?) (RoundedModeP b radix P) ->
  (p, q:float)
  (Rlt R0 p) ->
  (Rlt (Rmult (2) p) q) ->
  (Fcanonic radix b precision p) ->
  (Fcanonic radix b precision q) ->
  (Ex [r:float] (Fbounded b r) /\ r==(Rminus q p)) ->
  (r:float)
  (Fcanonic radix b precision r) -> (Rlt (Rmult (2) p) r) -> (Rle r q) ->
  (Ex [r':float] (Fbounded b r') /\ r'==(Rminus r p)).

Theorem ExactMinusIntervalAux1:
  (P:?) (RoundedModeP b radix P) ->
  (p, q:float)
  (Rle R0 p) ->
  (Rle p q) ->
  (Fcanonic radix b precision p) ->
  (Fcanonic radix b precision q) ->
  (Ex [r:float] (Fbounded b r) /\ r==(Rminus q p)) ->
  (r:float) (Fcanonic radix b precision r) -> (Rle p r) -> (Rle r q) ->
  (Ex [r':float] (Fbounded b r') /\ r'==(Rminus r p)).

Theorem ExactMinusInterval:
  (P:?) (RoundedModeP b radix P) ->
  (p, q:float)
  (Rle R0 p) ->
  (Rle p q) ->
  (Fbounded b p) ->
  (Fbounded b q) -> (Ex [r:float] (Fbounded b r) /\ r==(Rminus q p)) ->
  (r:float) (Fbounded b r) -> (Rle p r) -> (Rle r q) ->
  (Ex [r':float] (Fbounded b r') /\ r'==(Rminus r p)).
(* Properties concerning LSB MSB *)

Theorem MSBroundLSB:
  (P:R -> float ->Prop) (RoundedModeP b radix P) ->
  (f1, f2:float) (P f1 f2) -> ~ (is_Fzero (Fminus radix f1 f2)) ->
  (Zlt (MSB radix (Fminus radix f1 f2)) (LSB radix f2)).

Theorem LSBMinus:
  (p, q:float) ~ (is_Fzero (Fminus radix p q)) ->
  (Zle (Zmin (LSB radix p) (LSB radix q)) (LSB radix (Fminus radix p q))).

Theorem LSBPlus:
  (p, q:float) ~ (is_Fzero (Fplus radix p q)) ->
  (Zle (Zmin (LSB radix p) (LSB radix q)) (LSB radix (Fplus radix p q))).
End FRoundP.

30/05/01, 18:12