Fround.v

(****************************************************************************                                                                                         IEEE754  :  Fround                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export Float.
Require Export Fnorm.
Require Export Fop.
Require Export Fcomp.
Require Export FSucc.
Require Export FPred.
Require Export Fmin.
Require Export Fodd.
Require Export Fprop.
Section FRound.
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 TotalP := [P:R -> float ->Prop] (r:R)(Ex [p:float] (P r p)).

Definition UniqueP :=
   [P:R -> float ->Prop] (r:R) (p, q:float) (P r p) -> (P r q) -><R> p==q.

Definition CompatibleP :=
   [P:R -> float ->Prop]
   (r1, r2:R) (p, q:float) (P r1 p) -> r1==r2 -> <R> p==q -> (Fbounded b q) ->
   (P r2 q).

Definition MinOrMaxP :=
   [P:R -> float ->Prop] (r:R) (p:float) (P r p) ->
   (isMin b radix r p) \/ (isMax b radix r p).

Definition RoundedModeP :=
   [P:R -> float ->Prop]
   (TotalP P) /\ ((CompatibleP P) /\ ((MinOrMaxP P) /\ (MonotoneP radix P))).

Theorem RoundedProjector: (P:?) (RoundedModeP P) ->(ProjectorP b radix P).

Theorem MinCompatible: (CompatibleP (isMin b radix)).

Theorem MinRoundedModeP: (RoundedModeP (isMin b radix)).

Theorem MaxCompatible: (CompatibleP (isMax b radix)).

Theorem MaxRoundedModeP: (RoundedModeP (isMax b radix)).

Definition ToZeroP :=
   [r:R] [p:float]
   (Rle R0 r) /\ (isMin b radix r p) \/ (Rle r R0) /\ (isMax b radix r p).

Theorem ToZeroTotal: (TotalP ToZeroP).

Theorem ToZeroCompatible: (CompatibleP ToZeroP).

Theorem ToZeroMinOrMax: (MinOrMaxP ToZeroP).

Theorem ToZeroMonotone: (MonotoneP radix ToZeroP).

Theorem ToZeroRoundedModeP: (RoundedModeP ToZeroP).

Definition ToInfinityP :=
   [r:R] [p:float]
   (Rle r R0) /\ (isMin b radix r p) \/ (Rle R0 r) /\ (isMax b radix r p).

Theorem ToInfinityTotal: (TotalP ToInfinityP).

Theorem ToInfinityCompatible: (CompatibleP ToInfinityP).

Theorem ToInfinityMinOrMax: (MinOrMaxP ToInfinityP).

Theorem ToInfinityMonotone: (MonotoneP radix ToInfinityP).

Theorem ToInfinityRoundedModeP: (RoundedModeP ToInfinityP).

Theorem MinUniqueP: (UniqueP (isMin b radix)).

Theorem MaxUniqueP: (UniqueP (isMax b radix)).

Theorem ToZeroUniqueP: (UniqueP ToZeroP).

Theorem ToInfinityUniqueP: (UniqueP ToInfinityP).

Theorem FnOddNEven:
  (n:float) (FNodd b radix precision n) ->~ (FNeven b radix precision n).

Theorem MinOrMaxRep:
  (P:?) (MinOrMaxP P) ->
  (p, q:float) (P p q) ->(Ex [m:Z] <R> q==(Float m (Fexp p))).

Theorem RoundedModeRep:
  (P:?) (RoundedModeP P) ->
  (p, q:float) (P p q) ->(Ex [m:Z] <R> q==(Float m (Fexp p))).

Definition SymmetricP :=
   [P:R -> float ->Prop] (r:R) (p:float) (P r p) ->(P (Ropp r) (Fopp p)).

Theorem ToZeroSymmetric: (SymmetricP ToZeroP).

Theorem ToInfinitySymmetric: (SymmetricP ToInfinityP).

Theorem RoundLessThanIsMax:
  (P:?) (RoundedModeP P) ->
  (p, m:float) (x:R) (P x p) -> (isMax b radix x m) ->(Rle p m).
End FRound.

30/05/01, 18:11