Fprop.v

(****************************************************************************                                                                                         IEEE754  :  Fprop                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Import Float.
Require Import Fcomp.
Require Import Fop.
Require Import Fnorm.
Section Fprop.
Variable radix:nat.
Hypothesis radixMoreThanOne:(lt (1) radix).

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Variable b:Fbound.

Theorem SterbenzAux:
  (x, y:float)
  (Fbounded b x) -> (Fbounded b y) -> (Rle y x) -> (Rle x (Rmult (2) y)) ->
  (Fbounded b (Fminus radix x y)).

Theorem Sterbenz:
  (x, y:float)
  (Fbounded b x) ->
  (Fbounded b y) -> (Rle (Rmult (Rinv (2)) y) x) -> (Rle x (Rmult (2) y)) ->
  (Fbounded b (Fminus radix x y)).

Theorem BminusSameExpAux:
  (x, y:float)
  (Fbounded b x) ->
  (Fbounded b y) -> (Rle R0 y) -> (Rle y x) -> (Fexp x)=(Fexp y) ->
  (Fbounded b (Fminus radix x y)).

Theorem BminusSameExp:
  (x, y:float)
  (Fbounded b x) ->
  (Fbounded b y) -> (Rle R0 x) -> (Rle R0 y) -> (Fexp x)=(Fexp y) ->
  (Fbounded b (Fminus radix x y)).

Theorem BminusSameExpNeg:
  (x, y:float)
  (Fbounded b x) ->
  (Fbounded b y) -> (Rle x R0) -> (Rle y R0) -> (Fexp x)=(Fexp y) ->
  (Fbounded b (Fminus radix x y)).
End Fprop.

30/05/01, 18:09