Commit 7256c32f authored by Heiko Becker's avatar Heiko Becker

Forgot to add file...

parent a15e51d7
......@@ -388,37 +388,6 @@ Proof.
intros x; destruct (x =? n); try auto.
Qed.
Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2:
(forall n, Gamma1 n = Gamma2 n) ->
eval_expr E Gamma1 e vR m ->
eval_expr E Gamma2 e vR m.
Proof.
revert E vR Gamma1 Gamma2 m;
induction e; intros * Gamma_eq eval_e;
inversion eval_e; subst; simpl in *;
try eauto.
apply Var_load; try auto.
rewrite <- Gamma_eq; auto.
Qed.
Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 :
(forall n, Gamma1 n = Gamma2 n) ->
bstep f E Gamma1 vR m ->
bstep f E Gamma2 vR m.
Proof.
revert E Gamma1 Gamma2;
induction f; intros * Gamma_eq eval_f.
- inversion eval_f; subst.
econstructor; try eauto.
+ eapply swap_Gamma_eval_expr; eauto.
+ apply (IHf _ (updDefVars n m0 Gamma1) _); try eauto.
intros n1.
unfold updDefVars.
case (n1 =? n); auto.
- inversion eval_f; subst.
econstructor; try eauto.
eapply swap_Gamma_eval_expr; eauto.
Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
forall Gamma E fVars dVars outVars P,
......
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