ClosestProp.v

(****************************************************************************                                                                                         IEEE754  :  ClosestProp                                                                                                                                              Laurent Thery    & Sylvie Boldo                                                                                                                          ***************************************************************************** *)
Require Export FroundProp.
Require Export Closest.
Section Fclosestp.
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 Rltdouble: (r:R) (Rlt R0 r) ->(Rlt r (Rmult (2) r)).

Theorem RleFexpFabs:
  (p:float) ~ <R> p==R0 ->(Rle (Float (1) (Fexp p)) (Fabs p)).

Theorem ClosestOpp:
  (p:float) (r:R) (Closest b radix r p) ->(Closest b radix (Ropp r) (Fopp p)).

Theorem ClosestFabs:
  (p:float) (r:R) (Closest b radix r p) ->(Closest b radix (Rabsolu r) (Fabs p)).

Theorem ClosestUlp:
  (p:R) (q:float) (Closest b radix p q) ->
  (Rle (Rmult (2) (Rabsolu (Rminus p q))) (Fulp b radix precision q)).

Theorem ClosestExp:
  (p:R) (q:float) (Closest b radix p q) ->
  (Rle (Rmult (2) (Rabsolu (Rminus p q))) (powerRZ radix (Fexp q))).

Theorem ClosestErrorExpStrict:
  (p, q:float)
  (x:R)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Closest b radix x p) -> <R> q==(Rminus x p) -> ~ <R> q==R0 ->
  (Zlt (Fexp q) (Fexp p)).

Theorem ClosestIdem:
  (p, q:float) (Fbounded b p) -> (Closest b radix p q) -><R> p==q.

Theorem ClosestM1:
  (r1, r2:R)
  (min, max, p, q:float)
  (isMin b radix r1 min) ->
  (isMax b radix r1 max) ->
  (Rlt (Rplus min max) (Rmult (2) r2)) ->
  (Closest b radix r1 p) -> (Closest b radix r2 q) ->(Rle p q).

Theorem FmultRadixInv:
  (x, z:float)
  (y:R)
  (Fbounded b x) -> (Closest b radix y z) -> (Rlt (Rmult (Rinv (2)) x) y) ->
  (Rle (Rmult (Rinv (2)) x) z).

Theorem ClosestErrorBound:
  (p, q:float)
  (x:R) (Fbounded b p) -> (Closest b radix x p) -> <R> q==(Rminus x p) ->
  (Rle (Rabsolu q) (Rmult (Float (1) (Fexp p)) (Rinv (2)))).

Theorem ClosestErrorExp:
  (p, q:float)
  (x:R)
  (Fbounded b p) ->
  (Fbounded b q) -> (Closest b radix x p) -> <R> q==(Rminus x p) ->
  (Ex [error:float]
  (Fbounded b error) /\
  (<R> error==q /\
   (Zle (Fexp error) (Zmax (Zminus (Fexp p) precision) (Zopp (dExp b)))))).
End Fclosestp.

30/05/01, 17:28