Fast2Diff.v

(****************************************************************************                                                                                         IEEE754  :  Fast2Diff                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export EFast2Sum.
Section EDiff.
Variable b:Fbound.
Variable precision:nat.

Local FtoRradix := (FtoR (2)).
Coercion FtoRradix : float >-> R.
Hypothesis precisionGreaterThanOne:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp (2) precision) (1)).
Variable Iplus:float -> float ->float.
Hypothesis IplusCorrect:
           (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
           (Closest b (2) (Rplus p q) (Iplus p q)).
Hypothesis IplusComp:
           (p, q, r, s:float)
           (Fbounded b p) ->
           (Fbounded b q) ->
           (Fbounded b r) -> (Fbounded b s) -> <R> p==r -> <R> q==s ->
           <R> (Iplus p q)==(Iplus r s).
Hypothesis IplusSym:(p, q:float)(Iplus p q)=(Iplus q p).
Hypothesis IplusOp:(p, q:float)(Fopp (Iplus p q))=(Iplus (Fopp p) (Fopp q)).
Variable Iminus:float -> float ->float.
Hypothesis IminusPlus:(p, q:float)(Iminus p q)=(Iplus p (Fopp q)).

Theorem MDekkerDiffAux1:
  (p, q:float)
  <R> (Iminus p (Iminus p q))==(Rminus p (Iminus p q)) ->
  (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iminus p (Iminus p q)) q)==(Rminus (Rminus p q) (Iminus p q)).

Theorem MDekkerDiff:
  (p, q:float)
  (Fbounded b p) -> (Fbounded b q) -> (Rle (Rabsolu q) (Rabsolu p)) ->
  <R> (Iminus p (Iminus p q))==(Rminus p (Iminus p q)).

Theorem DekkerDiff:
  (p, q:float)
  (Fbounded b p) -> (Fbounded b q) -> (Rle (Rabsolu q) (Rabsolu p)) ->
  <R> (Iminus (Iminus p (Iminus p q)) q)==(Rminus (Rminus p q) (Iminus p q)).

Theorem ExtMDekkerDiff:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> (Zle (Fexp q) (Fexp p)) ->
  <R> (Iminus p (Iminus p q))==(Rminus p (Iminus p q)).

Theorem ExtDekkerDiff:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> (Zle (Fexp q) (Fexp p)) ->
  <R> (Iminus (Iminus p (Iminus p q)) q)==(Rminus (Rminus p q) (Iminus p q)).
End EDiff.

30/05/01, 17:35