Commit 96493068 authored by Heiko Becker's avatar Heiko Becker

Rework proofs for Interval and Error checker based on soundness theorem

for precondition checker, write composiing checker function and compose
soundness proofs into one theorem
parent 6faaa5f4
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.PreconditionValidation.
Definition CertificateCheker (e:exp Q) (absenv:analysisResult) (P:precond) :=
andb (andb (validIntervalbounds e absenv P) (approximatesPrecond e absenv P)) (validErrorbound e absenv).
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
forall (cenv:env_ty) (vR:R) (vF:R),
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e) vR ->
eval_exp machineEpsilon cenv (toRExp e) vF ->
CertificateCheker e absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
Proof.
intros cenv vR vF precondValid eval_real eval_float certificate_valid.
unfold CertificateCheker in certificate_valid.
apply Is_true_eq_left in certificate_valid.
apply andb_prop_elim in certificate_valid.
destruct certificate_valid as [iv_precond_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 precond_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).
destruct H0 as [iv [err absenv_eq]].
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
destruct H0 as [ivlo [ ivhi iv_eq]].
subst; rewrite absenv_eq in *; simpl in *.
eapply (validErrorbound_sound e cenv absenv vR vF err P); eauto.
rewrite mEps_eq_Rmeps; auto.
Qed.
\ No newline at end of file
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals Coq.Lists.List.
(*Coq.QArith.Qcanon.*)
Require Import Coq.micromega.Psatz Coq.Reals.Reals Interval.Interval_tactic.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.RationalConstruction Daisy.Infra.RealSimps.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArith Daisy.ErrorBounds Daisy.IntervalValidation.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArith Daisy.IntervalArithQ.
Require Import Daisy.ErrorBounds Daisy.IntervalValidation Daisy.PreconditionValidation.
Section ComputableErrors.
......@@ -123,10 +124,11 @@ Section ComputableErrors.
Lemma validErrorboundCorrectParam:
forall cenv absenv (v:nat) nR nF e P plo phi,
envApproximatesPrecond P absenv ->
(forall n, List.In n (freeVars Q (Param Q v)) ->
Is_true(isSupersetIntv (P n) (fst (absenv (Param Q n))))) ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (Param R v) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (Param R v) nF ->
eval_exp 0%R cenv (toRExp (Param Q v)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp (Param Q v)) nF ->
validErrorbound (Param Q v) absenv = true ->
validIntervalbounds (Param Q v) absenv P = true ->
absenv (Param Q v) = ((plo,phi),e) ->
......@@ -147,23 +149,30 @@ Section ComputableErrors.
destruct H as [ivlo [ivhi P_eq]].
rewrite <- P_eq in absenv_approx_p, cenv_approx_p.
rewrite absenv_param in absenv_approx_p.
unfold freeVars in absenv_approx_p; simpl in absenv_approx_p.
assert (v = v \/ False) by auto.
specialize (absenv_approx_p H).
unfold isSupersetIntv in absenv_approx_p.
apply andb_prop_elim in absenv_approx_p.
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.
destruct cenv_approx_p as [ivlo_le_cenv cenv_le_ivhi].
apply Qle_Rle in plo_le_ivlo; apply Qle_Rle in ivhi_le_phi.
pose proof (Rle_trans (Q2R plo) (Q2R ivlo) (cenv v) plo_le_ivlo ivlo_le_cenv).
pose proof (Rle_trans (cenv v) (Q2R ivhi) (Q2R phi) cenv_le_ivhi ivhi_le_phi).
pose proof (RmaxAbs (Q2R plo) (cenv v) (Q2R phi) H H2).
pose proof (RmaxAbs (Q2R plo) (cenv v) (Q2R phi) H2 H3).
unfold perturb.
rewrite Rabs_err_simpl.
rewrite Rabs_mult.
eapply Rle_trans.
eapply Rmult_le_compat; [ apply Rabs_pos | apply Rabs_pos | | ].
apply H3.
apply H4.
apply H1.
pose proof (maxAbs_impl_RmaxAbs plo phi).
unfold RmaxAbsFun in H4.
simpl in H4.
rewrite H4.
unfold RmaxAbsFun in H5.
simpl in H5.
rewrite H5.
apply Is_true_eq_left in error_valid.
apply andb_prop_elim in error_valid.
destruct error_valid as [_ error_valid].
......@@ -175,7 +184,8 @@ Section ComputableErrors.
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 :
envApproximatesPrecond P absenv ->
(forall v, List.In v (freeVars Q (Binop Plus e1 e2)) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
......@@ -240,31 +250,42 @@ Section ComputableErrors.
eapply Rle_trans.
eapply Rabs_triang.
eapply Rplus_le_compat.
- pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
apply (Rabs_error_bounded_maxAbs nR1); try auto.
unfold contained; rewrite absenv_e1 in valid_bounds_e1; auto.
- pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p 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.
- assert (forall v : nat, List.In v (freeVars Q e1 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e1.
+ 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).
+ pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e1 p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
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.
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 :
envApproximatesPrecond P absenv ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Sub e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Sub e1 e2) absenv = true ->
validIntervalbounds (Binop Sub e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
absenv e2 = ((e2lo, e2hi),err2) ->
absenv (Binop Sub e1 e2) = ((alo,ahi),e)->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
(forall v, List.In v (freeVars Q (Binop Sub e1 e2)) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Sub e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Sub e1 e2) absenv = true ->
validIntervalbounds (Binop Sub e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
absenv e2 = ((e2lo, e2hi),err2) ->
absenv (Binop Sub e1 e2) = ((alo,ahi),e)->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
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_sub
......@@ -313,31 +334,42 @@ Section ComputableErrors.
Focus 2.
apply valid_error.
eapply Rplus_le_compat.
- pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
apply (Rabs_error_bounded_maxAbs nR1); try auto.
unfold contained; rewrite absenv_e1 in valid_bounds_e1; auto.
- pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p 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.
- assert (forall v : nat, List.In v (freeVars Q e1 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e1.
+ 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).
+ pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e1 p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
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.
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 :
envApproximatesPrecond P absenv ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Mult e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Mult e1 e2) absenv = true ->
validIntervalbounds (Binop Mult e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
absenv e2 = ((e2lo, e2hi),err2) ->
absenv (Binop Mult e1 e2) = ((alo,ahi),e)->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
(forall v, List.In v (freeVars Q (Binop Mult e1 e2)) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Mult e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Mult e1 e2) absenv = true ->
validIntervalbounds (Binop Mult e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
absenv e2 = ((e2lo, e2hi),err2) ->
absenv (Binop Mult e1 e2) = ((alo,ahi),e)->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
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_mult
......@@ -386,8 +418,18 @@ Section ComputableErrors.
apply andb_prop_elim in valid_rec.
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.
pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p p_valid valid_iv_e1 e1_real) as valid_e1.
pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p p_valid valid_iv_e2 e2_real) as valid_e2.
assert (forall v : nat, List.In v (freeVars Q e1 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e1
by (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)).
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.
......@@ -942,9 +984,10 @@ Section ComputableErrors.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
Lemma validErrorboundCorrect (e:exp Q):
Lemma validErrorbound_sound (e:exp Q):
forall cenv absenv nR nF err P elo ehi,
envApproximatesPrecond P absenv ->
(forall v, List.In v (freeVars Q e) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e) nF ->
......@@ -1012,6 +1055,14 @@ Section ComputableErrors.
{ apply andb_prop_intro.
split; 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.
simpl.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
......@@ -1029,6 +1080,14 @@ Section ComputableErrors.
{ apply andb_prop_intro.
split; 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.
simpl.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
......@@ -1046,6 +1105,14 @@ Section ComputableErrors.
{ apply andb_prop_intro.
split; 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.
Qed.
......
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax.
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RationalConstruction Daisy.Infra.RealRationalProps.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps Daisy.PreconditionValidation.
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
let (intv, _) := absenv e in
......@@ -50,9 +50,10 @@ Qed.
Ltac env_assert absenv e name :=
assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).
Lemma validIntervalbounds_correct (e:exp Q):
Theorem validIntervalbounds_sound (e:exp Q):
forall (absenv:analysisResult) (P:precond) cenv vR,
envApproximatesPrecond P absenv ->
(forall v, In v (freeVars Q e) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv ->
validIntervalbounds e absenv P = true ->
eval_exp 0%R cenv (toRExp e) vR ->
......@@ -70,19 +71,25 @@ Proof.
destruct absenv_n as [intv [err absenv_n]].
rewrite absenv_n in valid_bounds.
unfold precondValidForExec in precond_valid.
unfold envApproximatesPrecond in env_approx_p.
specialize (env_approx_p n).
assert (exists ivlo ivhi, P n = (ivlo, ivhi)) as p_n
by (destruct (P n); repeat eexists; auto).
destruct p_n as [ivlo [ivhi p_n]].
unfold isSupersetIntv, freeVars in env_approx_p.
assert (In n (n::nil)) by (unfold In; auto).
specialize (env_approx_p H).
rewrite p_n, absenv_n in env_approx_p.
specialize (precond_valid n); rewrite p_n in precond_valid.
inversion eval_e; subst.
rewrite absenv_n; simpl.
rewrite perturb_0_val; auto.
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 precond_valid as [ivlo_le_env env_le_ivhi].
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.
apply Qle_Rle in abslo_le_ivlo; apply Qle_Rle in ivhi_le_abshi.
split.
+ eapply Rle_trans.
......@@ -127,36 +134,46 @@ Proof.
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_e1 valid_e2].
apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2.
specialize (IHe1 absenv P cenv v1 env_approx_p valid_precond valid_e1 H4);
specialize (IHe2 absenv P cenv v2 env_approx_p valid_precond valid_e2 H5).
rewrite absenv_e1 in IHe1.
rewrite absenv_e2 in IHe2.
destruct b; simpl in *.
+ pose proof (additionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add.
unfold validIntervalAdd in valid_add.
specialize (valid_add v1 v2 IHe1 IHe2).
unfold contained in valid_add.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct valid_add as [valid_add_lo valid_add_hi].
split.
* eapply Rle_trans. apply valid_lo.
unfold ivlo. unfold addIntv.
simpl in valid_add_lo.
repeat rewrite <- Q2R_plus in valid_add_lo.
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.
assert (forall v : nat, In v (freeVars Q e1 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e1.
+ intros v in_fV_e1.
assert (In v (freeVars Q (Binop b e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
+ assert (forall v : nat, 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 (In v (freeVars Q (Binop b e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
* specialize (IHe1 absenv P cenv v1 env_approx_e1 valid_precond valid_e1 H4);
specialize (IHe2 absenv P cenv v2 env_approx_e2 valid_precond valid_e2 H5).
rewrite absenv_e1 in IHe1.
rewrite absenv_e2 in IHe2.
destruct b; simpl in *.
* pose proof (additionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add.
unfold validIntervalAdd in valid_add.
specialize (valid_add v1 v2 IHe1 IHe2).
unfold contained in valid_add.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct valid_add as [valid_add_lo valid_add_hi].
split.
{ eapply Rle_trans. apply valid_lo.
unfold ivlo. unfold addIntv.
simpl in valid_add_lo.
repeat rewrite <- Q2R_plus in valid_add_lo.
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.
specialize (valid_sub v1 v2 IHe1 IHe2).
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