Closest.v

Require Export Fround.
Section Fclosest.
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 Closest :=
   [r:R] [p:float]
   (Fbounded b p) /\
   ((f:float) (Fbounded b f) ->
    (Rle (Rabsolu (Rminus p r)) (Rabsolu (Rminus f r)))).

Theorem ClosestTotal: (TotalP Closest).

Theorem ClosestCompatible: (CompatibleP b radix Closest).

Theorem ClosestMin:
  (r:R)
  (min, max:float)
  (isMin b radix r min) ->
  (isMax b radix r max) -> (Rle (Rmult (2) r) (Rplus min max)) ->(Closest r min).

Theorem ClosestMax:
  (r:R)
  (min, max:float)
  (isMin b radix r min) ->
  (isMax b radix r max) -> (Rle (Rplus min max) (Rmult (2) r)) ->(Closest r max).

Theorem ClosestMinOrMax: (MinOrMaxP b radix Closest).

Theorem ClosestMinEq:
  (r:R)
  (min, max, p:float)
  (isMin b radix r min) ->
  (isMax b radix r max) ->
  (Rlt (Rmult (2) r) (Rplus min max)) -> (Closest r p) -><R> p==min.

Theorem ClosestMaxEq:
  (r:R)
  (min, max, p:float)
  (isMin b radix r min) ->
  (isMax b radix r max) ->
  (Rlt (Rplus min max) (Rmult (2) r)) -> (Closest r p) -><R> p==max.

Theorem ClosestMonotone: (MonotoneP radix Closest).

Theorem ClosestRoundedModeP: (RoundedModeP b radix Closest).
Split; Try Exact ClosestTotal.
Split; Try Exact ClosestCompatible.
Split; Try Exact ClosestMinOrMax.
Try Exact ClosestMonotone.
Qed.

Definition EvenClosest :=
   [r:R] [p:float]
   (Closest r p) /\
   ((FNeven b radix precision p) \/ ((q:float) (Closest r q) -><R> q==p)).

Theorem EvenClosestTotal: (TotalP EvenClosest).

Theorem EvenClosestCompatible: (CompatibleP b radix EvenClosest).

Theorem EvenClosestMinOrMax: (MinOrMaxP b radix EvenClosest).

Theorem EvenClosestMonotone: (MonotoneP radix EvenClosest).

Theorem EvenClosestRoundedModeP: (RoundedModeP b radix EvenClosest).

Theorem EvenClosestUniqueP: (UniqueP radix EvenClosest).

Theorem ClosestSymmetric: (SymmetricP Closest).

Theorem EvenClosestSymmetric: (SymmetricP EvenClosest).
End Fclosest.

30/05/01, 17:23