Commit 1db30802 authored by Heiko Becker's avatar Heiko Becker

Simplify coq proofs a little

parent b8a5ce0c
......@@ -4,15 +4,16 @@ This shortens soundness proofs later.
Bounds are explained in section 5, Deriving Computable Error Bounds
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps Daisy.Expressions.
Require Import Daisy.Environments.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
Lemma const_abs_err_bounded (P:precond) (n:R) (nR:R) (nF:R) (VarEnv ParamEnv:env):
eval_exp 0%R VarEnv ParamEnv P (Const n) nR ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P (Const n) nF ->
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 eval_real eval_float.
intros approxCEnv eval_real eval_float.
inversion eval_real; subst.
rewrite delta_0_deterministic; auto.
inversion eval_float; subst.
......@@ -21,12 +22,13 @@ Proof.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (VarEnv ParamEnv:env):
eval_exp 0%R VarEnv ParamEnv P (Param R n) nR ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P (Param R n) nF ->
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 eval_real eval_float.
intros approxCEnv eval_real eval_float.
inversion eval_real; subst.
rewrite delta_0_deterministic; auto.
inversion eval_float; subst.
......@@ -37,7 +39,7 @@ 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:
(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 ->
......
......@@ -53,7 +53,7 @@ Fixpoint validErrorboundCmd (f:cmd Q) (env:analysisResult) {struct f} : bool :=
(validErrorbound e env) && (Qeq_bool (snd (env e)) (snd (env (Var Q x)))) &&
validErrorboundCmd g env
|Ret _ e => validErrorbound e env && (Qeq_bool (snd (env e)) (snd (env (Var Q 0))))
|Nop _ => true
|Nop _ => false
end.
(**
......@@ -116,29 +116,23 @@ Lemma validErrorboundCorrectConstant:
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.
eapply Rle_trans.
eapply const_abs_err_bounded; eauto.
unfold validErrorbound in error_valid.
inversion eval_real; subst.
rewrite delta_0_deterministic in *; auto.
clear delta H0.
inversion eval_float; subst.
rewrite absenv_const in *; simpl in *.
unfold perturb; simpl.
rewrite Rabs_err_simpl.
rewrite absenv_const in *; simpl in *.
andb_to_prop error_valid.
rename R into error_valid.
inversion eval_real; subst.
rewrite delta_0_deterministic in *; auto.
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
destruct intv_valid.
eapply Rle_trans.
- rewrite Rabs_mult.
eapply Rmult_le_compat_l; [ apply Rabs_pos | eauto ].
- eapply Rmult_le_compat_r.
apply mEps_geq_zero.
apply RmaxAbs; eauto.
- rewrite Q2R_mult in error_valid.
eapply Rle_trans.
+ eapply Rmult_le_compat_r.
apply mEps_geq_zero.
destruct intv_valid.
apply RmaxAbs; eauto.
+ rewrite <- maxAbs_impl_RmaxAbs in error_valid.
auto.
rewrite <- maxAbs_impl_RmaxAbs in error_valid; auto.
Qed.
Lemma validErrorboundCorrectParam:
......@@ -155,17 +149,18 @@ Lemma validErrorboundCorrectParam:
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.
unfold validErrorbound in error_valid.
rewrite absenv_param in error_valid.
eapply Rle_trans.
eapply param_abs_err_bounded; eauto.
inversion eval_real; subst.
rewrite delta_0_deterministic in *; auto.
rewrite delta_0_deterministic in H1; auto.
rewrite delta_0_deterministic in H1; auto.
inversion eval_float; subst.
rewrite delta_0_deterministic in H3; auto.
rewrite delta_0_deterministic in H3; auto.
unfold validErrorbound in error_valid.
rewrite absenv_param in error_valid.
specialize (absenv_approx_p v).
assert (exists ivlo ivhi, (ivlo,ivhi) = P v) by (destruct (P v) as [ivlo ivhi]; repeat eexists).
destruct H as [ivlo [ivhi P_eq]].
rewrite <- P_eq in absenv_approx_p, H1.
rewrite <- P_eq in absenv_approx_p, H3.
rewrite absenv_param in absenv_approx_p.
unfold freeVars in absenv_approx_p; simpl in absenv_approx_p.
assert (v = v \/ False) by auto.
......@@ -175,26 +170,21 @@ Proof.
destruct absenv_approx_p as [plo_le_ivlo ivhi_le_phi].
apply Is_true_eq_true, Qle_bool_iff in plo_le_ivlo.
apply Is_true_eq_true, Qle_bool_iff in ivhi_le_phi.
simpl in H1;destruct H1.
simpl in H3; destruct H3.
apply Qle_Rle in plo_le_ivlo; apply Qle_Rle in ivhi_le_phi.
andb_to_prop error_valid.
rename R into error_valid.
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
rewrite Q2R_mult in error_valid.
unfold perturb.
rewrite Rabs_err_simpl.
rewrite Rabs_mult.
eapply Rle_trans;[ | apply error_valid].
apply Rmult_le_compat;try (apply Rabs_pos);[ | apply H2].
pose proof (Rle_trans (Q2R plo) (Q2R ivlo) (PEnv v) plo_le_ivlo H1).
pose proof (Rle_trans (PEnv v) (Q2R ivhi) (Q2R phi) H4 ivhi_le_phi).
pose proof (RmaxAbs (Q2R plo) (PEnv v) (Q2R phi) H5 H6).
pose proof (maxAbs_impl_RmaxAbs plo phi).
rewrite <- H8;unfold RmaxAbsFun; simpl; auto.
apply Rmult_le_compat_r;try (apply Rabs_pos).
apply mEps_geq_zero.
rewrite <- maxAbs_impl_RmaxAbs.
destruct intv_valid.
eapply RmaxAbs; auto.
Qed.
(* TODO: Maybe extract subproof for ivbounds of operands into main lemma *)
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 :
......
......@@ -188,7 +188,7 @@ Proof.
destruct intv as [abslo abshi]; simpl in *.
apply andb_prop_elim in env_approx_p.
destruct env_approx_p as [abslo_le_ivlo ivhi_le_abshi].
destruct H1.
destruct H3.
apply Is_true_eq_true in abslo_le_ivlo; apply Is_true_eq_true in ivhi_le_abshi.
unfold Qleb in abslo_le_ivlo, ivhi_le_abshi.
apply Qle_bool_iff in abslo_le_ivlo; apply Qle_bool_iff in ivhi_le_abshi.
......
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