FexpPlus.v

Require Export Fexp.
Section mf.
Variable radix:nat.
Hypothesis radixMoreThanOne:(lt (1) radix).

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Require Import PolyList.
Require Import ClosestPlus.
Variable b:Fbound.
Variable precision:nat.
Hypothesis precisionGreaterThanOne:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).
Variable TwoSum:float -> float ->float * float.
Hypothesis TwoSum1:
           (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
           (Closest b radix (Rplus p q) (Fst (TwoSum p q))).
Hypothesis TwoSum2:
           (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
           <R> (Snd (TwoSum p q))==(Rminus (Rplus p q) (Fst (TwoSum p q))).
Hypothesis TwoSum3:
           (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
           (Fbounded b (Fst (TwoSum p q))).
Hypothesis TwoSum4:
           (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
           (Fbounded b (Snd (TwoSum p q))).
Hypothesis TwoSumEq1:
           (p, q, r, s:float)
           (Fbounded b p) ->
           (Fbounded b q) ->
           (Fbounded b r) -> (Fbounded b s) -> <R> p==q -> <R> r==s ->
           <R> (Fst (TwoSum p r))==(Fst (TwoSum q s)).
Hypothesis TwoSumEq2:
           (p, q, r, s:float)
           (Fbounded b p) ->
           (Fbounded b q) ->
           (Fbounded b r) -> (Fbounded b s) -> <R> p==q -> <R> r==s ->
           <R> (Snd (TwoSum p r))==(Snd (TwoSum q s)).

Fixpoint growExp[p:float; L:(list float)]: (list float) :=
   Cases L of
       nil => (cons p (nil ?))
      | (cons x L1) => Cases (TwoSum p x) of
                           (pair h c) => (cons c (growExp h L1))
                       end
   end.

Theorem TwoSumExp:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
  (IsExpansion
     b radix (cons (Snd (TwoSum p q)) (cons (Fst (TwoSum p q)) (nil ?)))).

Theorem TwoSumOl1:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> (is_Fzero q) ->
  <R> (Fst (TwoSum p q))==p.

Theorem TwoSumOl2:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> (is_Fzero q) ->
  <R> (Snd (TwoSum p q))==R0.

Theorem TwoSumOr1:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> (is_Fzero p) ->
  <R> (Fst (TwoSum p q))==q.

Theorem TwoSumOr2:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> (is_Fzero p) ->
  <R> (Snd (TwoSum p q))==R0.

Theorem growExpIsVal:
  (L:(list float)) (IsExpansion b radix L) ->
  (p:float) (Fbounded b p) ->
  <R> (expValue radix (growExp p L))==(Rplus p (expValue radix L)).

Theorem IsExpansionCons:
  (L:(list float)) (IsExpansion b radix L) ->
  (p:float)
  ~ (is_Fzero p) ->
  (Fbounded b p) ->
  ((q:float) (In q L) -> ~ (is_Fzero q) ->(Zlt (MSB radix p) (LSB radix q))) ->
  (IsExpansion b radix (cons p L)).

Theorem IsExpansionConsInvAux:
  (L:(list float)) (IsExpansion b radix L) ->
  (L':(list float))
  (p, q:float) ~ (is_Fzero p) -> L=(cons p L') -> (In q L') -> ~ (is_Fzero q) ->
  (Zlt (MSB radix p) (LSB radix q)).

Theorem IsExpansionConsInv:
  (L:(list float))
  (p, q:float)
  ~ (is_Fzero p) ->
  (IsExpansion b radix (cons p L)) -> (In q L) -> ~ (is_Fzero q) ->
  (Zlt (MSB radix p) (LSB radix q)).

Theorem IsExpansionSkip:
  (L:(list float)) (p, q:float) (IsExpansion b radix (cons p (cons q L))) ->
  (IsExpansion b radix (cons p L)).

Theorem TwoSumLt1:
  (p, q:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  ~ (is_Fzero p) -> ~ (is_Fzero q) -> ~ (is_Fzero (Fst (TwoSum p q))) ->
  (Zle (Zmin (LSB radix p) (LSB radix q)) (LSB radix (Fst (TwoSum p q)))).

Theorem TwoSumLt2:
  (p, q:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  ~ (is_Fzero p) -> ~ (is_Fzero q) -> ~ (is_Fzero (Snd (TwoSum p q))) ->
  (Zle (Zmin (LSB radix p) (LSB radix q)) (LSB radix (Snd (TwoSum p q)))).

Theorem IsExpansionGrowConsInvAux:
  (L:(list float)) (IsExpansion b radix L) ->
  (L':(list float))
  (p, q, r:float)
  (Fbounded b r) ->
  ~ (is_Fzero p) -> L=(cons p L') -> (In q (growExp r L')) -> ~ (is_Fzero q) ->
  ((is_Fzero r) ->(Zlt (MSB radix p) (LSB radix q))) /\
  (~ (is_Fzero r) ->
   (Zlt (MSB radix p) (LSB radix q)) \/ (Zle (LSB radix r) (LSB radix q))).

Theorem growExpIsExp:
  (L:(list float)) (IsExpansion b radix L) ->
  (p:float) (Fbounded b p) ->(IsExpansion b radix (growExp p L)).

Fixpoint addExp[L1:(list float)]: (list float) ->(list float) :=
   [L2:(list float)]
      Cases L1 of
          nil => L2
         | (cons x L'1) => Cases (growExp x L2) of
                               nil => L'1
                              | (cons y L'2) => (cons y (addExp L'1 L'2))
                           end
      end.

Theorem addExpIsVal:
  (L1, L2:(list float)) (IsExpansion b radix L1) -> (IsExpansion b radix L2) ->
  <R>
    (expValue radix (addExp L1 L2))==
    (Rplus (expValue radix L1) (expValue radix L2)).

Theorem IsExpansionAddInv:
  (L1, L2:(list float))
  (p, q:float)
  ~ (is_Fzero p) ->
  ~ (is_Fzero q) ->
  (IsExpansion b radix (cons p L1)) ->
  (IsExpansion b radix (cons p L2)) -> (In q (addExp L1 L2)) ->
  (Zlt (MSB radix p) (LSB radix q)).

Theorem addExpIsExp:
  (L1, L2:(list float)) (IsExpansion b radix L1) -> (IsExpansion b radix L2) ->
  (IsExpansion b radix (addExp L1 L2)).
End mf.

30/05/01, 17:54