FroundProp.v

(****************************************************************************                                                                                         IEEE754  :  FroundProp                                                                                                                                              Laurent Thery  &  Sylvie Boldo                                                                                                                                     ***************************************************************************** *)
Require Export Fround.
Require Export MSB.
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)).

Definition Fulp :=
   [p:float](powerRZ radix (Fexp (Fnormalize radix b precision p))).

Theorem FulpComp:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> <R> p==q ->(Fulp p)==(Fulp q).

Theorem FulpLe: (p:float) (Fbounded b p) ->(Rle (Fulp p) (Float (1) (Fexp p))).

Theorem Fulp_zero:
  (x:float) (is_Fzero x) ->(Fulp x)==(powerRZ radix (Zopp (dExp b))).

Theorem FulpSucCan:
  (p:float) (Fcanonic radix b precision p) ->
  (Rle (Rminus (FSucc b radix precision p) p) (Fulp p)).

Theorem FulpSuc:
  (p:float) (Fbounded b p) ->
  (Rle (Rminus (FNSucc b radix precision p) p) (Fulp p)).

Theorem FulpPredCan:
  (p:float) (Fcanonic radix b precision p) ->
  (Rle (Rminus p (FPred b radix precision p)) (Fulp p)).

Theorem FulpPred:
  (p:float) (Fbounded b p) ->
  (Rle (Rminus p (FNPred b radix precision p)) (Fulp p)).

Theorem RoundedModeUlp:
  (P:?) (RoundedModeP b radix P) ->
  (p, q:float) (P p q) ->(Rlt (Rabsolu (Rminus p q)) (Fulp q)).

Theorem RoundedModeUlp2:
  (P:?) (RoundedModeP b radix P) ->
  (p:R) (q:float) (P p q) ->(Rlt (Rabsolu (Rminus p q)) (Fulp q)).

Theorem RoundedModeErrorExpStrict:
  (P:?) (RoundedModeP b radix P) ->
  (p, q:float)
  (x:R)
  (Fbounded b p) ->
  (Fbounded b q) -> (P x p) -> <R> q==(Rminus x p) -> ~ <R> q==R0 ->
  (Zlt (Fexp q) (Fexp p)).

Theorem RoundedModeProjectorIdem:
  (P:?) (p:float) (RoundedModeP b radix P) -> (Fbounded b p) ->(P p p).

Theorem RoundedModeBounded:
  (P:?) (r:R) (q:float) (RoundedModeP b radix P) -> (P r q) ->(Fbounded b q).

Theorem RoundedModeProjectorIdemEq:
  (P:R -> float ->Prop)
  (p, q:float)
  (RoundedModeP b radix P) -> (Fbounded b p) -> (P (FtoR radix p) q) -><R> p==q.

Theorem RoundedModeMult:
  (P:?) (RoundedModeP b radix P) ->
  (r:R) (q, q':float) (P r q) -> (Fbounded b q') -> (Rle r (Rmult radix q')) ->
  (Rle q (Rmult radix q')).

Theorem RoundedModeMultLess:
  (P:?) (RoundedModeP b radix P) ->
  (r:R) (q, q':float) (P r q) -> (Fbounded b q') -> (Rle (Rmult radix q') r) ->
  (Rle (Rmult radix q') q).

Theorem RleMinR0:
  (r:R) (min:float) (Rle R0 r) -> (isMin b radix r min) ->(Rle R0 min).

Theorem RleRoundedR0:
  (P:R -> float ->Prop)
  (p:float) (r:R) (RoundedModeP b radix P) -> (P r p) -> (Rle R0 r) ->(Rle R0 p).

Theorem RleMaxR0:
  (r:R) (max:float) (Rle r R0) -> (isMax b radix r max) ->(Rle max R0).

Theorem RleRoundedLessR0:
  (P:R -> float ->Prop)
  (p:float) (r:R) (RoundedModeP b radix P) -> (P r p) -> (Rle r R0) ->(Rle p R0).

Theorem PminPos:
  (p:float)
  (min:float)
  (Rle R0 p) -> (Fbounded b p) -> (isMin b radix (Rmult (Rinv (2)) p) min) ->
  (Ex [c:float] (Fbounded b c) /\ <R> c==(Rminus p min)).

Theorem div2IsBetweenPos:
  (p:float)
  (min, max:float)
  (Rle R0 p) ->
  (Fbounded b p) ->
  (isMin b radix (Rmult (Rinv (2)) p) min) ->
  (isMax b radix (Rmult (Rinv (2)) p) max) -><R> p==(Rplus min max).

Theorem div2IsBetween:
  (p:float)
  (min, max:float)
  (Fbounded b p) ->
  (isMin b radix (Rmult (Rinv (2)) p) min) ->
  (isMax b radix (Rmult (Rinv (2)) p) max) -><R> p==(Rplus min max).

Theorem RoundedModeMultAbs:
  (P:?) (RoundedModeP b radix P) ->
  (r:R)
  (q, q':float)
  (P r q) -> (Fbounded b q') -> (Rle (Rabsolu r) (Rmult radix q')) ->
  (Rle (Rabsolu q) (Rmult radix q')).

Theorem isMinComp:
  (r1, r2:R)
  (min, max:float)
  (isMin b radix r1 min) ->
  (isMax b radix r1 max) -> (Rlt min r2) -> (Rlt r2 max) ->
  (isMin b radix r2 min).

Theorem isMaxComp:
  (r1, r2:R)
  (min, max:float)
  (isMin b radix r1 min) ->
  (isMax b radix r1 max) -> (Rlt min r2) -> (Rlt r2 max) ->
  (isMax b radix r2 max).

Theorem roundedModeLessMult:
  (P:R -> float ->Prop)
  (p:float)
  (r:R)
  (RoundedModeP b radix P) -> (P r p) -> (Rle (Float (1) (Zopp (dExp b))) r) ->
  (Rle p (Rmult radix r)).

Theorem roundedModeMoreMult:
  (P:R -> float ->Prop)
  (p:float)
  (r:R)
  (RoundedModeP b radix P) ->
  (P r p) -> (Rle r (Float (Zopp (1)) (Zopp (dExp b)))) ->
  (Rle (Rmult radix r) p).

Theorem roundedModeAbsMult:
  (P:R -> float ->Prop)
  (p:float)
  (r:R)
  (RoundedModeP b radix P) ->
  (P r p) -> (Rle (Float (1) (Zopp (dExp b))) (Rabsolu r)) ->
  (Rle (Rabsolu p) (Rmult radix (Rabsolu r))).

Theorem RleBoundRoundl:
  (P:?) (RoundedModeP b radix P) ->
  (p, q:float) (r:R) (Fbounded b p) -> (Rle p r) -> (P r q) ->(Rle p q).

Theorem RleBoundRoundr:
  (P:?) (RoundedModeP b radix P) ->
  (p, q:float) (r:R) (Fbounded b p) -> (Rle r p) -> (P r q) ->(Rle q p).

Theorem RoundAbsMonotoner:
  (P:R -> float ->Prop)
  (p:R)
  (q, r:float)
  (RoundedModeP b radix P) ->
  (Fbounded b r) -> (P p q) -> (Rle (Rabsolu p) r) ->(Rle (Rabsolu q) r).

Theorem RoundAbsMonotonel:
  (P:R -> float ->Prop)
  (p:R)
  (q, r:float)
  (RoundedModeP b radix P) ->
  (Fbounded b r) -> (P p q) -> (Rle r (Rabsolu p)) ->(Rle r (Rabsolu q)).
(* Rounded of natural numbers are natural *)

Theorem ZroundZ:
  (P:R -> float ->Prop) (z:Z) (p:float) (RoundedModeP b radix P) -> (P z p) ->
  (Ex [z':Z] <R> p==z').

Theorem NroundN:
  (P:R -> float ->Prop) (n:nat) (p:float) (RoundedModeP b radix P) -> (P n p) ->
  (Ex [n':nat] <R> p==n').
(* Properties of LSB and MSB *)

Theorem FUlp_Le_LSigB:
  (x:float) (Fbounded b x) ->(Rle (Fulp x) (Float (1) (LSB radix x))).

Theorem MSBisMin:
  (f1, f2:float)
  (Rle R0 f1) -> (isMin b radix f1 f2) -> ~ (is_Fzero f1) -> ~ (is_Fzero f2) ->
  (MSB radix f1)=(MSB radix f2).

Theorem MSBtoZero:
  (f1, f2:float)
  (ToZeroP b radix f1 f2) -> ~ (is_Fzero f1) -> ~ (is_Fzero f2) ->
  (MSB radix f1)=(MSB radix f2).

Theorem MSBBoundNotZero:
  (P:R -> float ->Prop) (RoundedModeP b radix P) ->
  (f1, f2:float)
  (P f1 f2) -> ~ <R> f1==R0 -> (Zle (Zopp (dExp b)) (MSB radix f1)) ->
  ~ <R> f2==R0.

Theorem RoundMSBmax:
  (P:R -> float ->Prop)
  (p, q:float)
  (RoundedModeP b radix P) ->
  (P p q) -> ~ <R> p==R0 -> (Zle (Zopp (dExp b)) (MSB radix p)) ->
  (Zle (MSB radix q) (Zs (MSB radix p))).

Theorem RoundMSBmin:
  (P:R -> float ->Prop)
  (p, q:float)
  (RoundedModeP b radix P) ->
  (P p q) -> ~ <R> p==R0 -> (Zle (Zopp (dExp b)) (MSB radix p)) ->
  (Zle (MSB radix p) (MSB radix q)).

Theorem RoundLSBMax:
  (P:R -> float ->Prop)
  (p, q:float) (RoundedModeP b radix P) -> (P p q) -> ~ (is_Fzero q) ->
  (Zle (LSB radix p) (LSB radix q)).
End FRoundP.

30/05/01, 18:17