Commit 8a990caf authored by Heiko Becker's avatar Heiko Becker
Browse files

Remove unused precondition checker in Coq dev

parent e2b3a688
...@@ -10,7 +10,7 @@ Require Export Coq.QArith.QArith. ...@@ -10,7 +10,7 @@ Require Export Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs. Require Export Daisy.Infra.ExpressionAbbrevs.
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) := Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
andb (andb (validIntervalbounds e absenv P) (approximatesPrecond e absenv P)) (validErrorbound e absenv). andb (validIntervalbounds e absenv P) (validErrorbound e absenv).
(** (**
Soundness proof. Soundness proof.
...@@ -27,18 +27,13 @@ Proof. ...@@ -27,18 +27,13 @@ Proof.
unfold CertificateChecker in certificate_valid. unfold CertificateChecker in certificate_valid.
apply Is_true_eq_left in certificate_valid. apply Is_true_eq_left in certificate_valid.
apply andb_prop_elim in certificate_valid. apply andb_prop_elim in certificate_valid.
destruct certificate_valid as [iv_precond_valid errorbound_valid]. destruct certificate_valid as [iv_valid errorbound_valid].
apply andb_prop_elim in iv_precond_valid.
destruct iv_precond_valid as [iv_valid precond_valid].
apply Is_true_eq_true in iv_valid; apply Is_true_eq_true in iv_valid;
apply Is_true_eq_true in precond_valid;
apply Is_true_eq_true in errorbound_valid. apply Is_true_eq_true in errorbound_valid.
pose proof (approximatesPrecond_sound e absenv P precond_valid).
clear precond_valid.
assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); repeat eexists). assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); repeat eexists).
destruct H0 as [iv [err absenv_eq]]. destruct H as [iv [err absenv_eq]].
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists). assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
destruct H0 as [ivlo [ ivhi iv_eq]]. destruct H as [ivlo [ ivhi iv_eq]].
subst; rewrite absenv_eq in *; simpl in *. subst; rewrite absenv_eq in *; simpl in *.
eapply (validErrorbound_sound e cenv absenv vR vF err P); eauto. eapply (validErrorbound_sound e cenv absenv vR vF err P); eauto.
rewrite mEps_eq_Rmeps; auto. rewrite mEps_eq_Rmeps; auto.
......
...@@ -123,8 +123,6 @@ Qed. ...@@ -123,8 +123,6 @@ Qed.
Lemma validErrorboundCorrectParam: Lemma validErrorboundCorrectParam:
forall cenv absenv (v:nat) nR nF e P plo phi, forall cenv absenv (v:nat) nR nF e P plo phi,
(forall n, List.In n (freeVars Q (Param Q v)) ->
Is_true(isSupersetIntv (P n) (fst (absenv (Param Q n))))) ->
precondValidForExec P cenv -> precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp (Param Q v)) nR -> eval_exp 0%R cenv (toRExp (Param Q v)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp (Param Q v)) nF -> eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp (Param Q v)) nF ->
...@@ -133,7 +131,8 @@ Lemma validErrorboundCorrectParam: ...@@ -133,7 +131,8 @@ Lemma validErrorboundCorrectParam:
absenv (Param Q v) = ((plo,phi),e) -> absenv (Param Q v) = ((plo,phi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R. (Rabs (nR - nF) <= (Q2R e))%R.
Proof. Proof.
intros cenv absenv v nR nF e P plo phi absenv_approx_p cenv_approx_p eval_real eval_float error_valid intv_valid absenv_param. intros cenv absenv v nR nF e P plo phi cenv_approx_p eval_real eval_float error_valid intv_valid absenv_param.
pose proof (ivbounds_approximatesPrecond_sound (Param Q v) absenv P intv_valid) as absenv_approx_p.
unfold validErrorbound in error_valid. unfold validErrorbound in error_valid.
rewrite absenv_param in error_valid. rewrite absenv_param in error_valid.
inversion eval_real; subst. inversion eval_real; subst.
...@@ -182,8 +181,6 @@ Proof. ...@@ -182,8 +181,6 @@ Proof.
Qed. Qed.
Lemma validErrorboundCorrectAddition cenv 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 : Lemma validErrorboundCorrectAddition cenv 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 :
(forall v, List.In v (freeVars Q (Binop Plus e1 e2)) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv -> precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 -> eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 -> eval_exp 0%R cenv (toRExp e2) nR2 ->
...@@ -200,7 +197,8 @@ Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 n ...@@ -200,7 +197,8 @@ Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 n
(Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R. (Rabs (nR - nF) <= (Q2R e))%R.
Proof. Proof.
intros 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. intros 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.
pose proof (ivbounds_approximatesPrecond_sound (Binop Plus e1 e2) absenv P valid_intv) as env_approx_p.
eapply Rle_trans. eapply Rle_trans.
eapply add_abs_err_bounded. eapply add_abs_err_bounded.
apply e1_real. apply e1_real.
...@@ -248,27 +246,15 @@ Proof. ...@@ -248,27 +246,15 @@ Proof.
eapply Rle_trans. eapply Rle_trans.
eapply Rabs_triang. eapply Rabs_triang.
eapply Rplus_le_compat. eapply Rplus_le_compat.
- assert (forall v : nat, List.In v (freeVars Q e1 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v))))) - pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
as env_approx_e1. apply (Rabs_error_bounded_maxAbs nR1); try auto.
+ intros v in_fV_e1. unfold contained; rewrite absenv_e1 in valid_bounds_e1; auto.
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto). - pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
apply (env_approx_p v H). apply (Rabs_error_bounded_maxAbs nR2); try auto.
+ pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e1 p_valid valid_iv_e1 e1_real) as valid_bounds_e1. unfold contained; rewrite absenv_e2 in valid_bounds_e2; auto.
apply (Rabs_error_bounded_maxAbs nR1); try auto.
unfold contained; rewrite absenv_e1 in valid_bounds_e1; auto.
- assert (forall v : nat, List.In v (freeVars Q e2 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e2.
+ intros v in_fV_e2.
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e2 p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
apply (Rabs_error_bounded_maxAbs nR2); try auto.
unfold contained; rewrite absenv_e2 in valid_bounds_e2; auto.
Qed. Qed.
Lemma validErrorboundCorrectSubtraction cenv 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 : Lemma validErrorboundCorrectSubtraction cenv 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 :
(forall v, List.In v (freeVars Q (Binop Sub e1 e2)) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv -> precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 -> eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 -> eval_exp 0%R cenv (toRExp e2) nR2 ->
...@@ -285,9 +271,10 @@ Lemma validErrorboundCorrectSubtraction cenv absenv (e1:exp Q) (e2:exp Q) (nR nR ...@@ -285,9 +271,10 @@ Lemma validErrorboundCorrectSubtraction cenv absenv (e1:exp Q) (e2:exp Q) (nR nR
(Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R. (Rabs (nR - nF) <= (Q2R e))%R.
Proof. Proof.
intros env_approx_p p_valid e1_real e2_real eval_real e1_float e2_float eval_float intros p_valid e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv absenv_e1 absenv_e2 absenv_sub valid_error valid_intv absenv_e1 absenv_e2 absenv_sub
err1_bounded err2_bounded. err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Sub e1 e2) absenv P valid_intv) as env_approx_p.
eapply Rle_trans. eapply Rle_trans.
eapply subtract_abs_err_bounded. eapply subtract_abs_err_bounded.
apply e1_real. apply e1_real.
...@@ -332,27 +319,15 @@ Proof. ...@@ -332,27 +319,15 @@ Proof.
Focus 2. Focus 2.
apply valid_error. apply valid_error.
eapply Rplus_le_compat. eapply Rplus_le_compat.
- assert (forall v : nat, List.In v (freeVars Q e1 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v))))) - pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
as env_approx_e1. apply (Rabs_error_bounded_maxAbs nR1); try auto.
+ intros v in_fV_e1. unfold contained; rewrite absenv_e1 in valid_bounds_e1; auto.
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto). - pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
apply (env_approx_p v H). apply (Rabs_error_bounded_maxAbs nR2); try auto.
+ pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e1 p_valid valid_iv_e1 e1_real) as valid_bounds_e1. unfold contained; rewrite absenv_e2 in valid_bounds_e2; auto.
apply (Rabs_error_bounded_maxAbs nR1); try auto.
unfold contained; rewrite absenv_e1 in valid_bounds_e1; auto.
- assert (forall v : nat, List.In v (freeVars Q e2 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e2.
+ intros v in_fV_e2.
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e2 p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
apply (Rabs_error_bounded_maxAbs nR2); try auto.
unfold contained; rewrite absenv_e2 in valid_bounds_e2; auto.
Qed. Qed.
Lemma validErrorboundCorrectMult cenv 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 : Lemma validErrorboundCorrectMult cenv 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 :
(forall v, List.In v (freeVars Q (Binop Mult e1 e2)) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv -> precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 -> eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 -> eval_exp 0%R cenv (toRExp e2) nR2 ->
...@@ -369,9 +344,10 @@ Lemma validErrorboundCorrectMult cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 n ...@@ -369,9 +344,10 @@ Lemma validErrorboundCorrectMult cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 n
(Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R. (Rabs (nR - nF) <= (Q2R e))%R.
Proof. Proof.
intros env_approx_p p_valid e1_real e2_real eval_real e1_float e2_float eval_float intros p_valid e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv absenv_e1 absenv_e2 absenv_mult valid_error valid_intv absenv_e1 absenv_e2 absenv_mult
err1_bounded err2_bounded. err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Mult e1 e2) absenv P valid_intv) as env_approx_p.
eapply Rle_trans. eapply Rle_trans.
eapply (mult_abs_err_bounded (toRExp e1) _ _ (toRExp e2)); eauto. eapply (mult_abs_err_bounded (toRExp e1) _ _ (toRExp e2)); eauto.
rewrite <- mEps_eq_Rmeps. rewrite <- mEps_eq_Rmeps.
...@@ -416,21 +392,10 @@ Proof. ...@@ -416,21 +392,10 @@ Proof.
apply andb_prop_elim in valid_rec. apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_iv_e1 valid_iv_e2]. destruct valid_rec as [valid_iv_e1 valid_iv_e2].
apply Is_true_eq_true in valid_iv_e1; apply Is_true_eq_true in valid_iv_e2. apply Is_true_eq_true in valid_iv_e1; apply Is_true_eq_true in valid_iv_e2.
assert (forall v : nat, List.In v (freeVars Q e1 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v))))) pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_e1.
as env_approx_e1 pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_e2.
by (intros v in_fV_e1; apply Rplus_le_compat.
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto); - unfold Rabs in err1_bounded.
apply (env_approx_p v H)).
pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e1 p_valid valid_iv_e1 e1_real) as valid_e1.
assert (forall v : nat, List.In v (freeVars Q e2 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e2.
by ( intros v in_fV_e2;
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto);
apply (env_approx_p v H)).
pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e2 p_valid valid_iv_e2 e2_real) as valid_e2.
apply Rplus_le_compat.
-
unfold Rabs in err1_bounded.
unfold Rabs in err2_bounded. unfold Rabs in err2_bounded.
(* Before doing case distinction, prove bounds that will be used many times: *) (* Before doing case distinction, prove bounds that will be used many times: *)
assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R
...@@ -984,8 +949,6 @@ Ltac iv_assert iv name:= ...@@ -984,8 +949,6 @@ Ltac iv_assert iv name:=
Lemma validErrorbound_sound (e:exp Q): Lemma validErrorbound_sound (e:exp Q):
forall cenv absenv nR nF err P elo ehi, forall cenv absenv nR nF err P elo ehi,
(forall v, List.In v (freeVars Q e) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv -> precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e) nR -> eval_exp 0%R cenv (toRExp e) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e) nF -> eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e) nF ->
...@@ -996,10 +959,11 @@ Lemma validErrorbound_sound (e:exp Q): ...@@ -996,10 +959,11 @@ Lemma validErrorbound_sound (e:exp Q):
Proof. Proof.
induction e. induction e.
- intros; simpl in *. - intros; simpl in *.
rewrite H5 in H3; rewrite H5 in H4; inversion H3. rewrite H4 in H2; rewrite H4 in H3; inversion H2.
- intros; eapply validErrorboundCorrectParam; eauto. - intros; eapply validErrorboundCorrectParam; eauto.
- intros; eapply validErrorboundCorrectConstant; eauto. - intros; eapply validErrorboundCorrectConstant; eauto.
- intros cenv absenv nR nF err P elo ehi env_approx_p p_valid eval_real eval_float valid_error valid_intv absenv_eq. - intros cenv absenv nR nF err P elo ehi p_valid eval_real eval_float valid_error valid_intv absenv_eq.
pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p.
simpl in valid_error. simpl in valid_error.
env_assert absenv e1 absenv_e1. env_assert absenv e1 absenv_e1.
env_assert absenv e2 absenv_e2. env_assert absenv e2 absenv_e2.
...@@ -1049,18 +1013,10 @@ Proof. ...@@ -1049,18 +1013,10 @@ Proof.
* unfold validIntervalbounds. * unfold validIntervalbounds.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl. rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true. apply Is_true_eq_true.
apply andb_prop_intro; split. apply andb_prop_intro; split; try auto.
{ apply andb_prop_intro. { apply andb_prop_intro.
split; apply Is_true_eq_left; auto. } split; apply Is_true_eq_left; auto. }
{ apply Is_true_eq_left; auto. } * apply Is_true_eq_left; auto.
* apply (IHe1 cenv absenv _ _ _ P ivlo1 ivhi1); auto.
intros v in_fV_e1.
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
* apply (IHe2 cenv absenv _ _ _ P ivlo2 ivhi2); auto.
intros v in_fV_e2.
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
+ eapply (validErrorboundCorrectSubtraction cenv absenv e1 e2); eauto. + eapply (validErrorboundCorrectSubtraction cenv absenv e1 e2); eauto.
simpl. simpl.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl. rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
...@@ -1078,14 +1034,6 @@ Proof. ...@@ -1078,14 +1034,6 @@ Proof.
{ apply andb_prop_intro. { apply andb_prop_intro.
split; apply Is_true_eq_left; auto. } split; apply Is_true_eq_left; auto. }
{ apply Is_true_eq_left; auto. } { apply Is_true_eq_left; auto. }
* apply (IHe1 cenv absenv _ _ _ P ivlo1 ivhi1); auto.
intros v in_fV_e1.
assert (List.In v (freeVars Q (Binop Sub e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
* apply (IHe2 cenv absenv _ _ _ P ivlo2 ivhi2); auto.
intros v in_fV_e2.
assert (List.In v (freeVars Q (Binop Sub e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
+ eapply (validErrorboundCorrectMult cenv absenv e1 e2); eauto. + eapply (validErrorboundCorrectMult cenv absenv e1 e2); eauto.
simpl. simpl.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl. rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
...@@ -1103,13 +1051,5 @@ Proof. ...@@ -1103,13 +1051,5 @@ Proof.
{ apply andb_prop_intro. { apply andb_prop_intro.
split; apply Is_true_eq_left; auto. } split; apply Is_true_eq_left; auto. }
{ apply Is_true_eq_left; auto. } { apply Is_true_eq_left; auto. }
* apply (IHe1 cenv absenv _ _ _ P ivlo1 ivhi1); auto.
intros v in_fV_e1.
assert (List.In v (freeVars Q (Binop Mult e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
* apply (IHe2 cenv absenv _ _ _ P ivlo2 ivhi2); auto.
intros v in_fV_e2.
assert (List.In v (freeVars Q (Binop Mult e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
+ inversion valid_error. + inversion valid_error.
Qed. Qed.
...@@ -34,6 +34,38 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):= ...@@ -34,6 +34,38 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
andb rec opres andb rec opres
end. end.
Theorem ivbounds_approximatesPrecond_sound e absenv P:
validIntervalbounds e absenv P = true ->
forall v, In v (freeVars Q e) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
Proof.
induction e; unfold validIntervalbounds.
- intros approx_true v v_in_fV; simpl in *; contradiction.
- intros approx_true v v_in_fV; simpl in *.
unfold isSupersetIntv.
destruct v_in_fV; try contradiction.
subst.
destruct (P v); destruct (absenv (Param Q v)); simpl in *.
destruct i; simpl in *.
apply Is_true_eq_left in approx_true; auto.
- intros approx_true v0 v_in_fV; simpl in *; contradiction.
- intros approx_bin_true v v_in_fV.
unfold freeVars in v_in_fV.
apply in_app_or in v_in_fV.
unfold approximatesPrecond in approx_bin_true.
apply Is_true_eq_left in approx_bin_true.
destruct (absenv (Binop b e1 e2)); destruct (absenv e1); destruct (absenv e2); simpl in *.
apply andb_prop_elim in approx_bin_true.
destruct approx_bin_true.
apply andb_prop_elim in H.
destruct H.
destruct v_in_fV as [v_in_fV_e1 | v_in_fV_e2].
+ apply IHe1; auto.
apply Is_true_eq_true; auto.
+ apply IHe2; auto.
apply Is_true_eq_true; auto.
Qed.
Corollary Q2R_max4 a b c d: Corollary Q2R_max4 a b c d:
Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d). Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
...@@ -52,18 +84,18 @@ Ltac env_assert absenv e name := ...@@ -52,18 +84,18 @@ Ltac env_assert absenv e name :=
Theorem validIntervalbounds_sound (e:exp Q): Theorem validIntervalbounds_sound (e:exp Q):
forall (absenv:analysisResult) (P:precond) cenv vR, forall (absenv:analysisResult) (P:precond) cenv vR,
(forall v, In v (freeVars Q e) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv -> precondValidForExec P cenv ->
validIntervalbounds e absenv P = true -> validIntervalbounds e absenv P = true ->
eval_exp 0%R cenv (toRExp e) vR -> eval_exp 0%R cenv (toRExp e) vR ->
(Q2R (fst (fst(absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R. (Q2R (fst (fst(absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R.
Proof. Proof.
induction e. induction e.
- intros absenv P cenv vR env_approx_p precond_valid valid_bounds eval_e. - intros absenv P cenv vR precond_valid valid_bounds eval_e.
pose proof (ivbounds_approximatesPrecond_sound (Var Q n) absenv P valid_bounds) as env_approx_p.
unfold validIntervalbounds in valid_bounds. unfold validIntervalbounds in valid_bounds.
destruct (absenv (Var Q n)); inversion valid_bounds. destruct (absenv (Var Q n)); inversion valid_bounds.
- intros absenv P cenv vR env_approx_p precond_valid valid_bounds eval_e. - intros absenv P cenv vR precond_valid valid_bounds eval_e.
pose proof (ivbounds_approximatesPrecond_sound (Param Q n) absenv P valid_bounds) as env_approx_p.
unfold validIntervalbounds in valid_bounds. unfold validIntervalbounds in valid_bounds.
assert (exists intv err, absenv (Param Q n) = (intv,err)) assert (exists intv err, absenv (Param Q n) = (intv,err))
as absenv_n as absenv_n
...@@ -98,7 +130,8 @@ Proof. ...@@ -98,7 +130,8 @@ Proof.
+ eapply Rle_trans. + eapply Rle_trans.
apply env_le_ivhi. apply env_le_ivhi.
apply ivhi_le_abshi. apply ivhi_le_abshi.
- intros absenv P cenv vR env_approx_p valid_precond valid_bounds eval_e. - intros absenv P cenv vR valid_precond valid_bounds eval_e.
pose proof (ivbounds_approximatesPrecond_sound (Const v) absenv P valid_bounds) as env_approx_p.
unfold validIntervalbounds in valid_bounds. unfold validIntervalbounds in valid_bounds.
destruct (absenv (Const v)) as [intv err]. destruct (absenv (Const v)) as [intv err].
simpl. simpl.
...@@ -117,8 +150,9 @@ Proof. ...@@ -117,8 +150,9 @@ Proof.
unfold Qleb in *. unfold Qleb in *.
apply Qle_bool_iff in valid_hi. apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_hi; auto. apply Qle_Rle in valid_hi; auto.
- intros absenv P cenv vR env_approx_p valid_precond valid_bounds eval_e; - intros absenv P cenv vR valid_precond valid_bounds eval_e;
inversion eval_e; subst. inversion eval_e; subst.
pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_bounds) as env_approx_p.
rewrite perturb_0_val in eval_e; auto. rewrite perturb_0_val in eval_e; auto.
rewrite perturb_0_val; auto. rewrite perturb_0_val; auto.
simpl in valid_bounds. simpl in valid_bounds.
...@@ -134,46 +168,36 @@ Proof. ...@@ -134,46 +168,36 @@ Proof.
apply andb_prop_elim in valid_rec. apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_e1 valid_e2]. destruct valid_rec as [valid_e1 valid_e2].
apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2. apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2.
assert (forall v : nat, In v (freeVars Q e1 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v))))) specialize (IHe1 absenv P cenv v1 valid_precond valid_e1 H4);
as env_approx_e1. specialize (IHe2 absenv P cenv v2 valid_precond valid_e2 H5).
+ intros v in_fV_e1. rewrite absenv_e1 in IHe1.
assert (In v (freeVars Q (Binop b e1 e2))) by (unfold freeVars; apply in_or_app; auto). rewrite absenv_e2 in IHe2.
apply (env_approx_p v H). destruct b; simpl in *.
+ assert (forall v : nat, In v (freeVars Q e2 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v))))) + pose proof (additionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add.
as env_approx_e2. unfold validIntervalAdd in valid_add.
* intros v in_fV_e2. specialize (valid_add v1 v2 IHe1 IHe2).
assert (In v (freeVars Q (Binop b e1 e2))) by (unfold freeVars; apply in_or_app; auto). unfold contained in valid_add.
apply (env_approx_p v H). unfold isSupersetIntv in valid_bin.
* specialize (IHe1 absenv P cenv v1 env_approx_e1 valid_precond valid_e1 H4); apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
specialize (IHe2 absenv P cenv v2 env_approx_e2 valid_precond valid_e2 H5). apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
rewrite absenv_e1 in IHe1. apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
rewrite absenv_e2 in IHe2. apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct b; simpl in *. destruct valid_add as [valid_add_lo valid_add_hi].
* pose proof (additionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add. split.
unfold validIntervalAdd in valid_add. { eapply Rle_trans. apply valid_lo.
specialize (valid_add v1 v2 IHe1 IHe2). unfold ivlo. unfold addIntv.
unfold contained in valid_add. simpl in valid_add_lo.
unfold isSupersetIntv in valid_bin. repeat rewrite <- Q2R_plus in valid_add_lo.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi]. rewrite <- Q2R_min4 in valid_add_lo.
apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. unfold absIvUpd; auto. }
apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. { eapply Rle_trans.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. Focus 2.
destruct valid_add as [valid_add_lo valid_add_hi]. apply valid_hi.
split. unfold ivlo, addIntv.
{ eapply Rle_trans. apply valid_lo. simpl in valid_add_hi.
unfold ivlo. unfold addIntv. repeat rewrite <- Q2R_plus in valid_add_hi.
simpl in valid_add_lo. rewrite <- Q2R_max4 in valid_add_hi.
repeat rewrite <- Q2R_plus in valid_add_lo. unfold absIvUpd; auto. }
rewrite <- Q2R_min4 in valid_add_lo.
unfold absIvUpd; auto. }
{ eapply Rle_trans.
Focus 2.
apply valid_hi.
unfold ivlo, addIntv.
simpl in valid_add_hi.
repeat rewrite <- Q2R_plus in valid_add_hi.
rewrite <- Q2R_max4 in valid_add_hi.
unfold absIvUpd; auto. }
+ pose proof (subtractionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_sub. + pose proof (subtractionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_sub.
specialize (valid_sub v1 v2 IHe1 IHe2). specialize (valid_sub v1 v2 IHe1 IHe2).
unfold contained in valid_sub. unfold contained in valid_sub.
......
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