Commit 2e65b5a9 authored by Heiko Becker's avatar Heiko Becker

Simplify some coq proofs

parent de4bf712
......@@ -8,12 +8,11 @@ Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSim
Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
Lemma const_abs_err_bounded (P:precond) (n:R) (nR:R) (nF:R) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult):
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (Const n) nR ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (Const n) nF ->
(Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R.
Proof.
intros approxCEnv eval_real eval_float.
intros eval_real eval_float.
inversion eval_real; subst.
rewrite delta_0_deterministic; auto.
inversion eval_float; subst.
......@@ -23,12 +22,11 @@ Proof.
Qed.
Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult):
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (Param R n) nR ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (Param R n) nF ->
(Rabs (nR - nF) <= Rabs (ParamEnv n) * (Q2R machineEpsilon))%R.
Proof.
intros approxCEnv eval_real eval_float.
intros eval_real eval_float.
inversion eval_real; subst.
rewrite delta_0_deterministic; auto.
inversion eval_float; subst.
......@@ -40,7 +38,6 @@ 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):
approxEnv VarEnv1 absenv VarEnv2 ->
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 ->
......@@ -51,7 +48,7 @@ Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F: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.
Proof.
intros approxCEnv e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
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 *)
inversion plus_real; subst.
rewrite delta_0_deterministic in plus_real; auto.
......@@ -100,19 +97,18 @@ Qed.
Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
**)
Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
(e2F:R) (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:nat->R) P absenv:
approxEnv VarEnv1 absenv VarEnv2 ->
(e2F:R) (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:nat->R) P err1 err2:
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 Sub (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Sub (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 approxCEnv e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
inversion sub_real; subst.
rewrite delta_0_deterministic in sub_real; auto.
......@@ -154,8 +150,7 @@ Proof.
Qed.
Lemma mult_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:
approxEnv VarEnv1 absenv VarEnv2 ->
(vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond):
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 ->
......@@ -164,7 +159,7 @@ Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Mult (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R.
Proof.
intros approxCEnv e1_real e1_float e2_real e2_float mult_real mult_float.
intros e1_real e1_float e2_real e2_float mult_real mult_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion mult_real; subst.
rewrite delta_0_deterministic in mult_real; auto.
......@@ -200,8 +195,7 @@ Proof.
Qed.
Lemma div_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:
approxEnv VarEnv1 absenv VarEnv2 ->
(vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond):
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 ->
......@@ -210,7 +204,7 @@ Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Div (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R.
Proof.
intros approxCenv e1_real e1_float e2_real e2_float div_real div_float.
intros e1_real e1_float e2_real e2_float div_real div_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion div_real; subst.
rewrite delta_0_deterministic in div_real; auto.
......
......@@ -106,7 +106,6 @@ Qed.
Lemma validErrorboundCorrectConstant:
forall VarEnv1 VarEnv2 ParamEnv absenv (n:Q) nR nF e nlo nhi (P:precond),
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (Const (Q2R n)) nR ->
eval_exp (Q2R (RationalSimps.machineEpsilon)) VarEnv2 ParamEnv P (Const (Q2R n)) nF ->
validErrorbound (Const n) absenv = true ->
......@@ -115,7 +114,7 @@ Lemma validErrorboundCorrectConstant:
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros cenv1 cenv2 PEnv absenv n nR nF e nlo nhi P.
intros approx_CEnv eval_real eval_float error_valid intv_valid absenv_const.
intros eval_real eval_float error_valid intv_valid absenv_const.
eapply Rle_trans.
eapply const_abs_err_bounded; eauto.
unfold validErrorbound in error_valid.
......@@ -137,7 +136,6 @@ Qed.
Lemma validErrorboundCorrectParam:
forall VarEnv1 VarEnv2 ParamEnv absenv (v:nat) nR nF e P plo phi,
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp (Param Q v)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) VarEnv2 ParamEnv P (toRExp (Param Q v)) nF ->
validErrorbound (Param Q v) absenv = true ->
......@@ -148,7 +146,7 @@ Lemma validErrorboundCorrectParam:
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros cenv1 cenv2 PEnv absenv v nR nF e P plo phi.
intros approx_CEnv eval_real eval_float error_valid intv_valid absenv_approx_p absenv_param.
intros eval_real eval_float error_valid intv_valid absenv_approx_p absenv_param.
eapply Rle_trans.
eapply param_abs_err_bounded; eauto.
inversion eval_real; subst.
......@@ -188,7 +186,6 @@ Qed.
Lemma validErrorboundCorrectAddition VarEnv1 VarEnv2 ParamEnv absenv
(e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) P :
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) nR1 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) nR2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp (Binop Plus e1 e2)) nR ->
......@@ -205,7 +202,7 @@ Lemma validErrorboundCorrectAddition VarEnv1 VarEnv2 ParamEnv absenv
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros approx_CEnv e1_real e2_real eval_real e1_float e2_float eval_float
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_add
err1_bounded err2_bounded.
eapply Rle_trans.
......@@ -260,7 +257,6 @@ Qed.
Lemma validErrorboundCorrectSubtraction VarEnv1 VarEnv2 ParamEnv absenv
(e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) P :
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) nR1 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) nR2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp (Binop Sub e1 e2)) nR ->
......@@ -277,22 +273,19 @@ Lemma validErrorboundCorrectSubtraction VarEnv1 VarEnv2 ParamEnv absenv
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros approxCEnv e1_real e2_real eval_real e1_float e2_float eval_float
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_sub
err1_bounded err2_bounded.
eapply Rle_trans.
eapply subtract_abs_err_bounded.
apply approxCEnv.
apply e1_real.
apply e1_float.
apply e2_real.
apply e2_float.
apply eval_real.
apply eval_float.
rewrite absenv_e1; simpl;
apply err1_bounded.
rewrite absenv_e2; simpl;
apply err2_bounded.
apply err1_bounded.
apply err2_bounded.
unfold validErrorbound in valid_error at 1.
rewrite absenv_sub, absenv_e1, absenv_e2 in valid_error.
andb_to_prop valid_error.
......@@ -305,7 +298,6 @@ Proof.
repeat rewrite <- Rabs_eq_Qabs in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
rewrite absenv_e1, absenv_e2; simpl.
eapply Rle_trans.
apply Rplus_le_compat_l.
eapply Rmult_le_compat_r.
......@@ -344,7 +336,6 @@ Qed.
Lemma validErrorboundCorrectMult VarEnv1 VarEnv2 ParamEnv absenv
(e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) P :
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) nR1 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) nR2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp (Binop Mult e1 e2)) nR ->
......@@ -361,7 +352,7 @@ Lemma validErrorboundCorrectMult VarEnv1 VarEnv2 ParamEnv absenv
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros approxCEnv e1_real e2_real eval_real e1_float e2_float eval_float
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_e1 valid_e2 absenv_e1 absenv_e2 absenv_mult
err1_bounded err2_bounded.
eapply Rle_trans.
......@@ -869,7 +860,6 @@ Qed.
Lemma validErrorboundCorrectDiv VarEnv1 VarEnv2 ParamEnv absenv
(e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) P :
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) nR1 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) nR2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp (Binop Div e1 e2)) nR ->
......@@ -887,11 +877,11 @@ Lemma validErrorboundCorrectDiv VarEnv1 VarEnv2 ParamEnv absenv
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros approxCEnv e1_real e2_real eval_real e1_float e2_float eval_float
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real absenv_e1
absenv_e2 absenv_div err1_bounded err2_bounded.
eapply Rle_trans.
apply (div_abs_err_bounded e1 nR1 nF1 e2 nR2 nF2 nR nF VarEnv1 VarEnv2 ParamEnv P absenv); auto.
apply (div_abs_err_bounded e1 nR1 nF1 e2 nR2 nF2 nR nF VarEnv1 VarEnv2 ParamEnv P); auto.
unfold validErrorbound in valid_error at 1.
rewrite absenv_div, absenv_e1, absenv_e2 in valid_error.
andb_to_prop valid_error.
......@@ -925,7 +915,7 @@ Proof.
apply valid_error.
apply Rplus_le_compat.
(* Error Propagation proof *)
+ clear approxCEnv absenv_e1 absenv_e2 valid_error eval_float eval_real e1_float
+ clear absenv_e1 absenv_e2 valid_error eval_float eval_real e1_float
e1_real e2_float e2_real absenv_div
valid_err_e1 valid_err_e2 VarEnv1 VarEnv2 ParamEnv absenv alo ahi nR nF e1 e2 e P.
unfold IntervalArith.contained, widenInterval in *.
......
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