Skip to content

GitLab

Commit b07718c2 authored by Heiko Becker's avatar Heiko Becker
Browse files

Proof subtraction sound

parent f36f9610
Hide whitespace changes
Inline Side-by-side
hol/ErrorValidation.hl
View file @ b07718c2
......@@ -122,38 +122,136 @@ let validErrorboundCorrectParam =
];
auto]
);;
g `!(cenv:env_ty) (absenv:analysisResult) (e1:(real)exp) (e2:(real)exp) nR nR1
nR2 nF (nF1:real) (nF2:real) (e:error) err1 err2 alo ahi e1lo e1hi e2lo e2hi (P:precond).
envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
eval_exp (&0) cenv e1 nR1 /\
eval_exp (&0) cenv e2 nR2 /\
eval_exp (&0) cenv (Binop Plus e1 e2) nR /\
eval_exp machineEpsilon cenv e1 nF1 /\
eval_exp machineEpsilon cenv e2 nF2 /\
eval_exp machineEpsilon (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (Binop Plus (Var 1) (Var 2)) nF /\
validErrorbound (Binop Plus e1 e2) absenv /\
validIntervalbounds (Binop Plus e1 e2) absenv P /\
absenv e1 = ((e1lo,e1hi),err1) /\
absenv e2 = ((e2lo, e2hi),err2) /\
absenv (Binop Plus e1 e2) = ((alo,ahi),e) /\
(abs (nR1 - nF1) <= err1) /\
(abs (nR2 - nF2) <= err2) ==>
(abs (nR - nF) <= e)`;;
e (intros "!cenv absenv e1 e2 nR nR1 nR2 nF nF1 nF2 e err1 err2 alo ahi e1lo e1hi e2lo e2hi P;
let validErrorboundCorrectAddition = prove (
`!(cenv:env_ty) (absenv:analysisResult) (e1:(real)exp) (e2:(real)exp) nR nR1
nR2 nF (nF1:real) (nF2:real) (e:error) err1 err2 alo ahi e1lo e1hi e2lo e2hi (P:precond).
envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
eval_exp (&0) cenv e1 nR1 /\
eval_exp (&0) cenv e2 nR2 /\
eval_exp (&0) cenv (Binop Plus e1 e2) nR /\
eval_exp machineEpsilon cenv e1 nF1 /\
eval_exp machineEpsilon cenv e2 nF2 /\
eval_exp machineEpsilon (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (Binop Plus (Var 1) (Var 2)) nF /\
validErrorbound (Binop Plus e1 e2) absenv /\
validIntervalbounds (Binop Plus e1 e2) absenv P /\
absenv e1 = ((e1lo,e1hi),err1) /\
absenv e2 = ((e2lo, e2hi),err2) /\
absenv (Binop Plus e1 e2) = ((alo,ahi),e) /\
(abs (nR1 - nF1) <= err1) /\
(abs (nR2 - nF2) <= err2) ==>
(abs (nR - nF) <= e)`,
intros "!cenv absenv e1 e2 nR nR1 nR2 nF nF1 nF2 e err1 err2 alo ahi e1lo e1hi e2lo e2hi P;
env_approx_p p_valid e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded"
THEN pose add_abs_err_bounded [`e1:(real)exp`; `nR1:real`; `nF1:real`; `e2:(real)exp`; `nR2:real`; `nF2:real`; `nR:real`; `nF:real`; `cenv:env_ty`; `err1:real`; `err2:real`] "add_bounded"
THEN pose add_abs_err_bounded [`e1:(real)exp`; `nR1:real`; `nF1:real`; `e2:(real)exp`; `nR2:real`; `nF2:real`; `nR:real`; `nF:real`; `cenv:env_ty`; `err1:real`; `err2:real`] "add_bounded"
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `(err1:real) + (err2:real) + abs ((nF1:real) + (nF2:real)) * machineEpsilon`
THEN split
THENL [
mp_asm "add_bounded" THEN clear["add_bounded"] THEN auto;
clear ["add_bounded"]
THEN rewrite validErrorbound "valid_error"
THEN rewrite_asm "absenv_add" "valid_error"
THEN simplify "valid_error"
THEN rewrite_asm "absenv_e1" "valid_error"
THEN rewrite_asm "absenv_e2" "valid_error"
THEN rewrite validIntervalbounds "valid_intv"
THEN destruct "valid_intv" "valid_e1 valid_e2 valid_bin"
THEN REPEAT (simplify "valid_error")
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `err1 + err2 + (abs (maxAbsFun (e1lo,e1hi) + (err1:real)) + abs (maxAbsFun (e2lo,e2hi) + err2)) * machineEpsilon`
THEN split
THENL [
mp REAL_LE_LADD_IMP
THEN mp REAL_LE_LADD_IMP
THEN mp REAL_LE_RMUL
THEN split
THENL [
mp REAL_LE_TRANS
THEN EXISTS_TAC `abs nF1 + abs (nF2:real)`
THEN split
THENL [
SIMP_TAC[REAL_ABS_TRIANGLE];
mp REAL_LE_ADD2
THEN split
THENL [
pose validIntervalbounds_correct
[`e1:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR1:real`]
"valid_bounds_e1"
THEN SUBGOAL_TAC "e1_bound_prems"
`envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
(validIntervalbounds e1 absenv P <=> T) /\
eval_exp (&0) cenv e1 nR1`
[auto]
THEN mp_spec "valid_bounds_e1" "e1_bound_prems"
THEN mp (SPEC `nR1:real` Rabs_error_bounded_maxAbs)
THEN SIMP_TAC[contained; IVlo; IVhi]
THEN rewrite_asm "absenv_e1" "valid_bounds_e1"
THEN rewrite FST "valid_bounds_e1"
THEN rewrite FST "valid_bounds_e1"
THEN split THEN auto
;
pose validIntervalbounds_correct
[`e2:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR2:real`]
"valid_bounds_e2"
THEN SUBGOAL_TAC "e2_bound_prems"
`envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
(validIntervalbounds e2 absenv P <=> T) /\
eval_exp (&0) cenv e2 nR2`
[auto]
THEN mp_spec "valid_bounds_e2" "e2_bound_prems"
THEN mp (SPEC `nR2:real` Rabs_error_bounded_maxAbs)
THEN SIMP_TAC[contained; IVlo; IVhi]
THEN rewrite_asm "absenv_e2" "valid_bounds_e2"
THEN rewrite FST "valid_bounds_e2"
THEN rewrite FST "valid_bounds_e2"
THEN split THEN auto
]
];
SIMP_TAC[mEps_geq_zero]
];
auto
]
]);;
let validErrorboundCorrectSubtraction = prove (
`!(cenv:env_ty) (absenv:analysisResult) (e1:(real)exp) (e2:(real)exp) nR nR1
nR2 nF (nF1:real) (nF2:real) (e:error) err1 err2 alo ahi e1lo e1hi e2lo e2hi (P:precond).
envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
eval_exp (&0) cenv e1 nR1 /\
eval_exp (&0) cenv e2 nR2 /\
eval_exp (&0) cenv (Binop Sub e1 e2) nR /\
eval_exp machineEpsilon cenv e1 nF1 /\
eval_exp machineEpsilon cenv e2 nF2 /\
eval_exp machineEpsilon (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (Binop Sub (Var 1) (Var 2)) nF /\
validErrorbound (Binop Sub e1 e2) absenv /\
validIntervalbounds (Binop Sub e1 e2) absenv P /\
absenv e1 = ((e1lo,e1hi),err1) /\
absenv e2 = ((e2lo, e2hi),err2) /\
absenv (Binop Sub e1 e2) = ((alo,ahi),e) /\
(abs (nR1 - nF1) <= err1) /\
(abs (nR2 - nF2) <= err2) ==>
(abs (nR - nF) <= e)`,
intros "!cenv absenv e1 e2 nR nR1 nR2 nF nF1 nF2 e err1 err2 alo ahi e1lo e1hi e2lo e2hi P;
env_approx_p p_valid e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_sub err1_bounded err2_bounded"
THEN pose sub_abs_err_bounded [`e1:(real)exp`; `nR1:real`; `nF1:real`; `e2:(real)exp`; `nR2:real`; `nF2:real`; `nR:real`; `nF:real`; `cenv:env_ty`; `err1:real`; `err2:real`] "sub_bounded"
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `(err1:real) + (err2:real) + abs ((nF1:real) + (nF2:real)) * machineEpsilon`
THEN EXISTS_TAC `(err1:real) + (err2:real) + (abs (nF1:real) + abs (nF2:real)) * machineEpsilon`
THEN split
THENL [
mp_asm "add_bounded" THEN clear["add_bounded"] THEN auto;
clear ["add_bounded"]
mp_asm "sub_bounded" THEN clear["sub_bounded"] THEN auto;
clear ["sub_bounded"]
THEN rewrite validErrorbound "valid_error"
THEN rewrite_asm "absenv_add" "valid_error"
THEN rewrite_asm "absenv_sub" "valid_error"
THEN simplify "valid_error"
THEN rewrite_asm "absenv_e1" "valid_error"
THEN rewrite_asm "absenv_e2" "valid_error"
THEN rewrite validIntervalbounds "valid_intv"
THEN destruct "valid_intv" "valid_e1 valid_e2 valid_bin"
THEN REPEAT (simplify "valid_error")
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `err1 + err2 + (abs (maxAbsFun (e1lo,e1hi) + (err1:real)) + abs (maxAbsFun (e2lo,e2hi) + err2)) * machineEpsilon`
......@@ -168,15 +266,48 @@ e (intros "!cenv absenv e1 e2 nR nR1 nR2 nF nF1 nF2 e err1 err2 alo ahi e1lo e1h
THEN EXISTS_TAC `abs nF1 + abs (nF2:real)`
THEN split
THENL [
SIMP_TAC[REAL_ABS_TRIANGLE];
SIMP_TAC[REAL_LE_REFL];
mp REAL_LE_ADD2
THEN split
THENL [
rewrite REAL_ABS_SUB "err1_bounded";(* TODO *)
rewrite REAL_ABS_SUB "err2_bounded"
pose validIntervalbounds_correct
[`e1:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR1:real`]
"valid_bounds_e1"
THEN SUBGOAL_TAC "e1_bound_prems"
`envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
(validIntervalbounds e1 absenv P <=> T) /\
eval_exp (&0) cenv e1 nR1`
[auto]
THEN mp_spec "valid_bounds_e1" "e1_bound_prems"
THEN mp (SPEC `nR1:real` Rabs_error_bounded_maxAbs)
THEN SIMP_TAC[contained; IVlo; IVhi]
THEN rewrite_asm "absenv_e1" "valid_bounds_e1"
THEN rewrite FST "valid_bounds_e1"
THEN rewrite FST "valid_bounds_e1"
THEN split THEN auto
;
pose validIntervalbounds_correct
[`e2:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR2:real`]
"valid_bounds_e2"
THEN SUBGOAL_TAC "e2_bound_prems"
`envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
(validIntervalbounds e2 absenv P <=> T) /\
eval_exp (&0) cenv e2 nR2`
[auto]
THEN mp_spec "valid_bounds_e2" "e2_bound_prems"
THEN mp (SPEC `nR2:real` Rabs_error_bounded_maxAbs)
THEN SIMP_TAC[contained; IVlo; IVhi]
THEN rewrite_asm "absenv_e2" "valid_bounds_e2"
THEN rewrite FST "valid_bounds_e2"
THEN rewrite FST "valid_bounds_e2"
THEN split THEN auto
]
];
auto];
auto ]
SIMP_TAC[mEps_geq_zero]
];
auto
]
]);;
search [ `abs ((a:real) - b)`];;
search [ `(a:real) <= a`];;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment