Fexp.v

Require Export FroundPlus.
Require Export FroundMult.
Require Export PolyList.
Section mf.
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)).
(* because the flow of algorithm goes from the smallest element of the     expansion to the biggest, expansion are defined as list of the smallest     to the biggest *)

Inductive IsExpansion: (list float) ->Prop :=
     IsExpansionNil: (IsExpansion (nil ?))
    | IsExpansionSingle:
        (x:float) (Fbounded b x) ->(IsExpansion (cons x (nil ?)))
    | IsExpansionTop1:
        (x:float)
        (L:(list float)) (is_Fzero x) -> (Fbounded b x) -> (IsExpansion L) ->
        (IsExpansion (cons x L))
    | IsExpansionTop2:
        (x, y:float)
        (L:(list float))
        (Fbounded b x) ->
        (is_Fzero y) -> (Fbounded b y) -> (IsExpansion (cons x L)) ->
        (IsExpansion (cons x (cons y L)))
    | IsExpansionTop:
        (x, y:float)
        (L:(list float))
        ~ (is_Fzero x) ->
        ~ (is_Fzero y) ->
        (Fbounded b x) ->
        (Fbounded b y) ->
        (Zlt (MSB radix x) (LSB radix y)) -> (IsExpansion (cons y L)) ->
        (IsExpansion (cons x (cons y L))) .

Theorem Zlt_MSB_LSB:
  (x, y:float) ~ (is_Fzero y) -> (Zlt (MSB radix x) (LSB radix y)) ->
  (Rlt (Fabs x) (Fabs y)).

Theorem IsExpansion_comp1:
  (L:(list float))
  (x, y:float) (Fbounded b y) -> <R> x==y -> (IsExpansion (cons x L)) ->
  (IsExpansion (cons y L)).

Theorem IsExpansion_comp2:
  (L:(list float))
  (x, y, z:float)
  (Fbounded b z) -> <R> y==z -> (IsExpansion (cons x (cons y L))) ->
  (IsExpansion (cons x (cons z L))).

Fixpoint expValue[L:(list float)]: float :=
   Cases L of
       nil => (Fzero ZERO)
      | (cons x L1) => (Fplus radix x (expValue L1))
   end.

Fixpoint expNormalize[L:(list float)]: (list float) :=
   Cases L of
       nil => (nil ?)
      | (cons x L1) => Cases (Fnum x) of
                           ZERO => (expNormalize L1)
                          | (POS p) => (cons x (expNormalize L1))
                          | (NEG p) => (cons x (expNormalize L1))
                       end
   end.

Theorem expInv:
  (a:float) (L:(list float)) (IsExpansion (cons a L)) ->(IsExpansion L).

Theorem expBoundedInv:
  (a:float) (L:(list float)) (IsExpansion (cons a L)) ->(Fbounded b a).

Theorem expNormalizeCorrect:
  (L:(list float))<R> (expValue L)==(expValue (expNormalize L)).

Theorem expNormalizeExp:
  (L:(list float)) (IsExpansion L) ->(IsExpansion (expNormalize L)).
(*A notion of expansion without zero*)

Inductive IsNzExpansion: (list float) ->Prop :=
     IsNzExpansionNil: (IsNzExpansion (nil ?))
    | IsNzExpansionSingle:
        (x:float) ~ (is_Fzero x) -> (Fbounded b x) ->
        (IsNzExpansion (cons x (nil ?)))
    | IsNzExpansionTop:
        (x, y:float)
        (L:(list float))
        ~ (is_Fzero x) ->
        ~ (is_Fzero y) ->
        (Fbounded b x) ->
        (Fbounded b y) ->
        (Zlt (MSB radix x) (LSB radix y)) -> (IsNzExpansion (cons y L)) ->
        (IsNzExpansion (cons x (cons y L))) .

Theorem isNzExpansionIsExpansion:
  (l:(list float)) (IsNzExpansion l) ->(IsExpansion l).

Theorem IsNzExpansionInv:
  (a:float) (l:(list float)) (IsNzExpansion (cons a l)) ->(IsNzExpansion l).
(*A notion of expansion without zero. in reverse order*)

Inductive IsNzExpansionR: (list float) ->Prop :=
     IsNzExpansionNilR: (IsNzExpansionR (nil ?))
    | IsNzExpansionSingleR:
        (x:float) ~ (is_Fzero x) -> (Fbounded b x) ->
        (IsNzExpansionR (cons x (nil ?)))
    | IsNzExpansionTopR:
        (x, y:float)
        (L:(list float))
        ~ (is_Fzero x) ->
        ~ (is_Fzero y) ->
        (Fbounded b x) ->
        (Fbounded b y) ->
        (Zlt (MSB radix y) (LSB radix x)) -> (IsNzExpansionR (cons y L)) ->
        (IsNzExpansionR (cons x (cons y L))) .

Theorem isNzExpansionRIsNzExpansion:
  (l:(list float)) (IsNzExpansionR l) ->(IsNzExpansion (rev l)).

Theorem IsNzExpansionRInv:
  (a:float) (l:(list float)) (IsNzExpansionR (cons a l)) ->(IsNzExpansionR l).

Theorem mkIsNzAux:
  (n:nat)
  (p:float)
  (Zle (Zopp (dExp b)) (LSB radix p)) ->
  (Zlt (MSB radix p) (Zplus (Zopp (dExp b)) n)) ->
  (Ex [l:(list float)] (IsNzExpansionR l) /\ (<R> p==(expValue l) /\ Cases l of
                                                                         (cons
                                                                            a _)
                                                                           =>
                                                                           (ToZeroP
                                                                              b
                                                                              radix
                                                                              p
                                                                              a)
                                                                        | nil =>
                                                                            True
                                                                     end)).

Theorem expValueApp:
  (l1, l2:(list float))
  <R> (expValue (app l1 l2))==(Rplus (expValue l1) (expValue l2)).

Theorem expValueRev: (l:(list float))<R> (expValue (rev l))==(expValue l).

Theorem existExp:
  (p:float) (Zle (Zopp (dExp b)) (LSB radix p)) ->
  (Ex [l:(list float)] (IsExpansion l) /\ <R> p==(expValue l)).
End mf.

30/05/01, 17:47