Commit 95dac28a authored by Heiko Becker's avatar Heiko Becker

Simplify coq error bound proof

parent 7ab24f19
......@@ -37,16 +37,17 @@ Proof.
Qed.
Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) (absenv:analysisResult):
(vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond)
(err1 err2 :Q) (absenv:analysisResult):
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
eval_exp 0%R VarEnv1 ParamEnv P (Binop Plus (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Plus (Var R 1) (Var R 2)) vF ->
(Rabs (e1R - e1F) <= Q2R (snd (absenv e1)))%R ->
(Rabs (e2R - e2F) <= Q2R (snd (absenv e2)))%R ->
(Rabs (vR - vF) <= Q2R (snd(absenv e1)) + Q2R (snd (absenv e2)) + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R.
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R.
Proof.
intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
......
......@@ -207,15 +207,12 @@ Proof.
err1_bounded err2_bounded.
eapply Rle_trans.
apply
(add_abs_err_bounded e1 nR1 nF1 e2 nR2 nF2 nR nF VarEnv1 VarEnv2 ParamEnv P absenv);
(add_abs_err_bounded e1 nR1 nF1 e2 nR2 nF2 nR nF VarEnv1 VarEnv2 ParamEnv P err1 err2);
try auto.
rewrite absenv_e1; auto.
rewrite absenv_e2; auto.
unfold validErrorbound in valid_error at 1.
rewrite absenv_add, absenv_e1, absenv_e2 in valid_error.
andb_to_prop valid_error.
rename R into valid_error.
rewrite absenv_e1, absenv_e2; simpl.
eapply Rle_trans.
apply Rplus_le_compat_l.
eapply Rmult_le_compat_r.
......
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