Finduct.v

(****************************************************************************                                                                                         IEEE754  :  Finduct                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** Define an induction principle on float*)
Require Import PolyList.
Require Import Float.
Require Import Fnorm.
Require Import Fop.
Require Import Fcomp.
Require Import FSucc.
Require Import FPred.
Section finduct.
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne:(lt (S O) radix).
Hypothesis precisionNotZero:~ precision=O.
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).

Definition Fweight :=
   [p:float](Zplus (Fnum p) (Zmult (Fexp p) (exp radix precision))).

Theorem FweightLt:
  (p, q:float)
  (Fcanonic radix b precision p) ->
  (Fcanonic radix b precision q) -> (Rle R0 p) -> (Rlt p q) ->
  (Zlt (Fweight p) (Fweight q)).

Theorem FweightEq:
  (p, q:float)
  (Fcanonic radix b precision p) ->
  (Fcanonic radix b precision q) -> <R> p==q ->(Fweight p)=(Fweight q).

Theorem FweightZle:
  (p, q:float)
  (Fcanonic radix b precision p) ->
  (Fcanonic radix b precision q) -> (Rle R0 p) -> (Rle p q) ->
  (Zle (Fweight p) (Fweight q)).

Theorem FinductPosAux:
  (P:float ->Prop)
  (p:float)
  (Rle R0 p) ->
  (Fcanonic radix b precision p) ->
  (P p) ->
  ((q:float) (Fcanonic radix b precision q) -> (Rle p q) -> (P q) ->
   (P (FSucc b radix precision q))) ->
  (x:Z) (Zle ZERO x) ->
  (q:float)
  x=(Zminus (Fweight q) (Fweight p)) ->
  (Fcanonic radix b precision q) -> (Rle p q) ->(P q).

Theorem FinductPos:
  (P:float ->Prop)
  (p:float)
  (Rle R0 p) ->
  (Fcanonic radix b precision p) ->
  (P p) ->
  ((q:float) (Fcanonic radix b precision q) -> (Rle p q) -> (P q) ->
   (P (FSucc b radix precision q))) ->
  (q:float) (Fcanonic radix b precision q) -> (Rle p q) ->(P q).

Theorem FinductNegAux:
  (P:float ->Prop)
  (p:float)
  (Rle R0 p) ->
  (Fcanonic radix b precision p) ->
  (P p) ->
  ((q:float)
   (Fcanonic radix b precision q) -> (Rlt R0 q) -> (Rle q p) -> (P q) ->
   (P (FPred b radix precision q))) ->
  (x:Z) (Zle ZERO x) ->
  (q:float)
  x=(Zminus (Fweight p) (Fweight q)) ->
  (Fcanonic radix b precision q) -> (Rle R0 q) -> (Rle q p) ->(P q).

Theorem FinductNeg:
  (P:float ->Prop)
  (p:float)
  (Rle R0 p) ->
  (Fcanonic radix b precision p) ->
  (P p) ->
  ((q:float)
   (Fcanonic radix b precision q) -> (Rlt R0 q) -> (Rle q p) -> (P q) ->
   (P (FPred b radix precision q))) ->
  (q:float) (Fcanonic radix b precision q) -> (Rle R0 q) -> (Rle q p) ->(P q).

Theorem radixRangeBoundExp:
  (p, q:float)
  (Fcanonic radix b precision p) ->
  (Fcanonic radix b precision q) ->
  (Rle R0 p) -> (Rlt p q) -> (Rlt q (Rmult radix p)) ->
  (Fexp p)=(Fexp q) \/ (Zs (Fexp p))=(Fexp q).
End finduct.

30/05/01, 17:56