Fexp2.v

(****************************************************************************                                                                                         IEEE754  :  Fexp2                                                                                                                                                     Sylvie Boldo                                                                                                                          ***************************************************************************** *)
Require Export ThreeSumProps.
Require Export PolyList.
Section Fexp2.
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)).
Hypothesis Ngd:(Rle R1 (Rmult (vNum b) (Rminus R1 (Rinv (2))))).
Hypothesis Ngd2:
           (Rle (6) (Rmult (vNum b) (Rminus R1 (Rmult (Rinv (2)) (Rinv (2)))))).

Inductive IsExp: (list float) ->Prop :=
     IsExpNil: (IsExp (nil ?))
    | IsExpSingle: (x:float) (Fbounded b x) ->(IsExp (cons x (nil ?)))
    | IsExpTop:
        (x, y:float)
        (L:(list float))
        (Fbounded b x) ->
        (Fbounded b y) -> (Zle (Fexp y) (Fexp x)) -> (IsExp (cons y L)) ->
        (IsExp (cons x (cons y L))) .

Inductive NearEqual: (list float) -> (list float) ->Prop :=
     IsEqual: (x:(list float))(NearEqual x x)
    | OneMoreR:
        (x:(list float)) (e:float) (Fbounded b e) ->(NearEqual x (cons e x)) .

Fixpoint sum[L:(list float)]: R :=
   Cases L of
       nil => R0
      | (cons x L1) => (Rplus (FtoRradix x) (sum L1))
   end.

Definition hdexp :=
   [L:(list float)]
      Cases L of
          nil => (Zopp (dExp b))
         | (cons x L1) => (Fexp x)
      end.

Fixpoint lastexp[L:(list float)]: Z :=
   Cases L of
       nil => (Zopp (dExp b))
      | (cons x nil) => (Fexp x)
      | (cons x L1) => (lastexp L1)
   end.

Definition hd :=
   [L:(list float)]
      Cases L of
          nil => (Fzero (Zopp (dExp b)))
         | (cons x L1) => x
      end.

Theorem IsExpZle:
  (i:float) (L:(list float)) (IsExp (cons i L)) ->(Zle (hdexp L) (Fexp i)).

Theorem sum_IsExp:
  (L:(list float))
  (x:float) (m:R) (IsExp (cons x L)) -> (Rle (Float (vNum b) (Fexp x)) m) ->
  (Rle (Rabsolu (sum (cons x L))) (Rmult (length (cons x L)) m)).

Inductive IsRleExp: (list float) ->Prop :=
     IsRleExpNil: (IsRleExp (nil ?))
    | IsRleExpSingle: (x:float) (Fbounded b x) ->(IsRleExp (cons x (nil ?)))
    | IsRleExpTop:
        (x, y:float)
        (L:(list float))
        (Fbounded b x) ->
        (Fbounded b y) ->
        (Rle (Rabsolu x) (Rabsolu y)) -> (IsRleExp (cons y L)) ->
        (IsRleExp (cons x (cons y L))) .

Inductive EqListFloat: (list float) -> (list float) ->Prop :=
     EqListFloatnil: (EqListFloat (nil float) (nil float))
    | EqListFloatTop:
        (x, y:float)
        (L, L':(list float))
        (Fbounded b x) -> (Fbounded b y) -> <R> x==y -> (EqListFloat L L') ->
        (EqListFloat (cons x L) (cons y L')) .

Theorem sum_app:
  (L:(list float)) (x:float)
  <R> (Rplus x (sum L))==((sum (app L (cons x (nil float))))).

Theorem cons_neq: (x:float) (L:(list float))~ <(list float)> (cons x L)=L.

Definition endof :=
   [all, part:(list float)](Ex [rest:(list float)] all=(app rest part)).

Theorem app_length:
  (l1, l2:(list float))(length (app l1 l2))=(plus (length l1) (length l2)).

Theorem endof_length:
  (L, l:(list float)) (endof L l) ->(le (length l) (length L)).

Inductive IsCanExp: (list float) ->Prop :=
     IsCanExpNil: (IsCanExp (nil ?))
    | IsCanExpTop:
        (x:float)
        (L:(list float)) (Fcanonic (2) b precision x) -> (IsCanExp L) ->
        (IsCanExp (cons x L)) .

Theorem IsCanExpBounded:
  (i:float) (L:(list float)) (IsCanExp (cons i L)) ->(Fbounded b i).

Inductive IsRleExpRev: (list float) ->Prop :=
     IsRleExpRevNil: (IsRleExpRev (nil ?))
    | IsRleExpRevSingle:
        (x:float) (Fbounded b x) ->(IsRleExpRev (cons x (nil ?)))
    | IsRleRevExpTop:
        (x, y:float)
        (L:(list float))
        (Fbounded b x) ->
        (Fbounded b y) ->
        (Rle (Rabsolu y) (Rabsolu x)) -> (IsRleExpRev (cons y L)) ->
        (IsRleExpRev (cons x (cons y L))) .

Theorem IsRleExpRevIsExp:
  (L:(list float)) (IsRleExpRev L) ->
  (Ex [L':(list float)]
  (IsCanExp L') /\ ((IsRleExpRev L') /\ ((EqListFloat L L') /\ (IsExp L')))).

Fixpoint last[L:(list float)]: float :=
   Cases L of
       nil => (Fzero (Zopp (dExp b)))
      | (cons x nil) => x
      | (cons x L1) => (last L1)
   end.

Theorem ExpRev_aux:
  (l:(list float))
  (x:float)
  (Fbounded b x) -> (IsRleExpRev l) -> (Rle (Rabsolu x) (Rabsolu (last l))) ->
  (IsRleExpRev (app l (cons x (nil float)))).

Theorem Exp_aux:
  (l:(list float))
  (x:float)
  (Fbounded b x) -> (IsRleExp l) -> (Rle (Rabsolu (last l)) (Rabsolu x)) ->
  (IsRleExp (app l (cons x (nil float)))).

Theorem last_hd: (l:(list float))(last l)=(hd (rev l)).

Theorem IsRleExpRev_IsRleExp:
  (l:(list float)) (IsRleExpRev l) ->(IsRleExp (rev l)).

Theorem IsRleExp_IsRleExpRev:
  (l:(list float)) (IsRleExp l) ->(IsRleExpRev (rev l)).

Theorem EqListFloat_length:
  (l, l':(list float)) (EqListFloat l l') ->(length l)=(length l').

Theorem EqListFloat_sum:
  (l, l':(list float)) (EqListFloat l l') -><R> ((sum l))==((sum l')).

Theorem rev_sum: (l:(list float))<R> ((sum l))==((sum (rev l))).

Theorem rev_length: (l:(list float))(length l)=(length (rev l)).
End Fexp2.

30/05/01, 17:49