FexpAdd.v
(****************************************************************************
IEEE754 : FexpAdd
Sylvie Boldo
*****************************************************************************
*)
Require Export ThreeSumProps.
Require Export PolyList.
Require Export Fexp2.
Section FexpAdd.
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
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)) .
Definition
Step :=
[x, y, i, x', y':float] [input, output, output':(list float)]
(Fbounded b x') /\
((Fbounded b y') /\
((NearEqual output output') /\
(<R>
(Rplus x (Rplus y (Rplus (sum (cons i input)) (sum output))))==
(Rplus x' (Rplus y' (Rplus (sum input) (sum output')))) /\
((Zle (Fexp i) (Fexp y')) /\
((Zle (Fexp y') (Fexp x')) /\
((IsExp b (cons i input)) /\
((<R> x'==R0 \/
(<R> y'==R0 \/
(Rle
(Rabsolu y')
(Rmult
(vNum b)
(Rminus (Float (1) (Fexp x')) (Float (1) (hdexp b input)))))
/\
(Rle
(Rabsolu y')
(Rmult
(vNum b) (Rminus (Float (1) (Fexp x')) (Float (1) (Fexp i)))))))
/\
((output'=output \/
(Rle
(Rabsolu (Rplus x' y'))
(Rmult
(Rmult (Rmult (3) (2)) (Rinv (vNum b)))
(Rabsolu (hd b output'))))) /\
(output'=(nil float) \/
(Rle
(Rabsolu (hd b input))
(Rmult
(3)
(Rmult
(2)
(Rmult
(Rabsolu (hd b output')) (Rinv (Rminus (vNum b) (1)))))))
/\
(input=(nil float) \/
(Rle
(Float (vNum b) (Fexp (hd b input)))
(Rmult
(3)
(Rmult
(2)
(Rmult
(Rabsolu (hd b output')) (Rinv (Rminus (vNum b) (1)))))))
/\
(Rle
(Rabsolu (sum input))
(Rmult
(length input)
(Rmult
(3)
(Rmult
(2)
(Rmult
(Rabsolu (hd b output'))
(Rinv (Rminus (vNum b) (1)))))))))))))))))).
Theorem
AddStep:
(x, y, i:float)
(input, output:(list float))
(Fbounded b x) ->
(Fbounded b y) ->
(IsExp b (cons i input)) ->
(Zle (Fexp i) (Fexp y)) ->
(Zle (Fexp y) (Fexp x)) ->
(<R> (FtoR (2) x)==R0 \/ (<R> (FtoR (2) y)==R0 \/ <R> (FtoR (2) i)==R0)) \/
(Rle
(Rabsolu (FtoR (2) y))
(Rmult
(vNum b)
(Rminus (FtoR (2) (Float (1) (Fexp x))) (FtoR (2) (Float (1) (Fexp i)))))) ->
output=(nil float) \/
(Rle
(Rabsolu i)
(Rmult
(3)
(Rmult (2) (Rmult (Rabsolu (hd b output)) (Rinv (Rminus (vNum b) (1)))))))
/\
((Rle
(Float (vNum b) (Fexp i))
(Rmult
(3)
(Rmult
(2) (Rmult (Rabsolu (hd b output)) (Rinv (Rminus (vNum b) (1)))))))
/\
(Rle
(Rabsolu (sum (cons i input)))
(Rmult
(length (cons i input))
(Rmult
(3)
(Rmult
(2) (Rmult (Rabsolu (hd b output)) (Rinv (Rminus (vNum b) (1))))))))) ->
(Ex [x':float]
(Ex [y':float]
(Ex [output':(list float)] (Step x y i x' y' input output output')))).
Definition
endof :=
[all, part:(list float)](Ex [rest:(list float)] all=(app rest part)).
Theorem
endof_length:
(L, l:(list float)) (endof L l) ->(le (length l) (length L)).
Variable input:(list float).
Inductive
IsRleEpsExp: (list float) ->Prop :=
IsRleEpsExpNil: (IsRleEpsExp (nil ?))
| IsRleEpsExpSingle:
(x:float) (Fbounded b x) ->(IsRleEpsExp (cons x (nil ?)))
| IsRleEpsExpTop:
(x, y:float)
(L:(list float))
(Fbounded b x) ->
(Fbounded b y) ->
(Rle
(Rabsolu x)
(Rmult
(Rmult
(Rplus (Rmult (6) (length input)) (6))
(Rinv
(Rminus (Rminus (vNum b) (1)) (Rmult (6) (length input)))))
(Rabsolu y))) -> (IsRleEpsExp (cons y L)) ->
(IsRleEpsExp (cons x (cons y L))) .
Theorem
endof_Rle_length:
(P, Q:(list float)) (k:float) (endof input (app P (cons k Q))) ->
(Rle (length P) (Rminus (length input) R1)).
Theorem
FexpAdd_aux:
(L, output:(list float))
(x, y:float)
(endof input L) ->
(Rlt (Rmult (Rmult (6) (length input)) (Rinv (Rminus (vNum b) (1)))) R1) ->
(IsExp b L) ->
(IsRleEpsExp output) ->
output=(nil float) \/
(Rle
(Rabsolu (Rplus x y))
(Rmult
(Rmult
(Rmult (Rminus (vNum b) (1)) (Rinv (vNum b)))
(Rmult
(Rplus (Rmult (6) (length input)) (6))
(Rinv (Rminus (Rminus (vNum b) (1)) (Rmult (6) (length input))))))
(Rabsolu (hd b output)))) ->
output=(nil float) \/
(Ex [L1:(list float)]
(Ex [x1:float]
(Ex [y1:float]
(IsExp b (app L1 L)) /\
((endof input (app L1 L)) /\
(<R> (Rplus x1 (Rplus y1 (sum L1)))==(Rplus x y) /\
((Rle
(Rabsolu (sum L1))
(Rmult
(length L1)
(Rmult
(3)
(Rmult
(2)
(Rmult (Rabsolu (hd b output)) (Rinv (Rminus (vNum b) (1))))))))
/\
(Rle
(Rabsolu (Rplus x1 y1))
(Rmult (Rmult (Rmult (3) (2)) (Rinv (vNum b))) (Rabsolu (hd b output)))))))))) ->
(Fbounded b x) ->
(Fbounded b y) ->
(Zle (hdexp b L) (Fexp y)) ->
(Zle (Fexp y) (Fexp x)) ->
(<R> (FtoR (2) x)==R0 \/ <R> (FtoR (2) y)==R0) \/
(Rle
(Rabsolu (FtoR (2) y))
(Rmult
(vNum b)
(Rminus
(FtoR (2) (Float (1) (Fexp x))) (FtoR (2) (Float (1) (hdexp b L)))))) ->
output=(nil float) \/
(L=(nil float) \/
(Rle
(Rabsolu (hd b L))
(Rmult
(3)
(Rmult
(2) (Rmult (Rabsolu (hd b output)) (Rinv (Rminus (vNum b) (1)))))))
/\
((Rle
(Float (vNum b) (Fexp (hd b L)))
(Rmult
(3)
(Rmult
(2) (Rmult (Rabsolu (hd b output)) (Rinv (Rminus (vNum b) (1)))))))
/\
(Rle
(Rabsolu (sum L))
(Rmult
(length L)
(Rmult
(3)
(Rmult
(2) (Rmult (Rabsolu (hd b output)) (Rinv (Rminus (vNum b) (1)))))))))) ->
(Ex [x':float]
(Ex [y':float]
(Ex [output':(list float)]
(Fbounded b x') /\
((Fbounded b y') /\
(<R>
(Rplus x (Rplus y (Rplus (sum output) (sum L))))==
(Rplus x' (Rplus y' (sum output'))) /\
((le (length output') (plus (length L) (length output))) /\
((Zle (Fexp y') (Fexp x')) /\
((IsRleEpsExp output') /\
((output=(nil float) \/
(Ex [L1:(list float)]
(Ex [x1:float]
(Ex [y1:float]
(IsExp b (app L1 L)) /\
((endof input (app L1 L)) /\
(<R> (Rplus x1 (Rplus y1 (sum L1)))==(Rplus x y) /\
((Rle
(Rabsolu (sum L1))
(Rmult
(length L1)
(Rmult
(3)
(Rmult
(2)
(Rmult
(Rabsolu (hd b output)) (Rinv (Rminus (vNum b) (1))))))))
/\
(Rle
(Rabsolu (Rplus x1 y1))
(Rmult
(Rmult (Rmult (3) (2)) (Rinv (vNum b)))
(Rabsolu (hd b output))))))))))) /\
((endof output' output) /\
(output'=(nil float) \/
(Rle
(Rabsolu (Rplus x' y'))
(Rmult
(Rmult
(Rmult (Rminus (vNum b) (1)) (Rinv (vNum b)))
(Rmult
(Rplus (Rmult (6) (length input)) (6))
(Rinv
(Rminus
(Rminus (vNum b) (1)) (Rmult (6) (length input))))))
(Rabsolu (hd b output'))))))))))))))).
Theorem
FexpAdd_aux2:
(L:(list float))
L=input ->
(IsExp b input) ->
(Rlt (Rmult (Rmult (6) (length input)) (Rinv (Rminus (vNum b) (1)))) R1) ->
(Ex [output:(list float)]
(~ input==(nil float) ->(le (length output) (S (length input)))) /\
(<R> ((sum input))==((sum output)) /\ (IsRleEpsExp output))).
Theorem
FexpAdd_main:
(IsExp b input) ->
(Rlt (Rmult (Rmult (6) (length input)) (Rinv (Rminus (vNum b) (1)))) R1) ->
(Ex [output:(list float)]
(~ input==(nil float) ->(le (length output) (S (length input)))) /\
(<R> ((sum input))==((sum output)) /\ (IsRleEpsExp output))).
End FexpAdd.
30/05/01, 17:51