Commit 939af786 authored by Heiko Becker's avatar Heiko Becker
Browse files

Simplifications and admit currently unsolved goals

parent 723edf12
......@@ -2079,36 +2079,6 @@ Proof.
- andb_to_prop R1; auto. }
Lemma validErrorbound_subset e absenv dVars dVars':
validErrorbound e absenv dVars = true ->
NatSet.Subset dVars dVars' ->
validErrorbound e absenv dVars' = true.
induction e; intros validBound_e_dV subset_dV; simpl in *; try auto.
- destruct (absenv (Var Q n)); simpl in *.
andb_to_prop validBound_e_dV.
apply Is_true_eq_true; apply andb_prop_intro; split.
+ apply Is_true_eq_left in L; auto.
+ case_eq (NatSet.mem n dVars);
intros case_mem; rewrite case_mem in *; simpl in *.
* hnf in subset_dV.
rewrite NatSet.mem_spec in case_mem.
specialize (subset_dV n case_mem).
rewrite <- NatSet.mem_spec in subset_dV.
rewrite subset_dV.
apply Is_true_eq_left; auto.
* case_eq (NatSet.mem n dVars'); intros case_mem';
apply Is_true_eq_left; auto.
- destruct (absenv (Binop b e1 e2)); simpl in *.
rewrite <- andb_lazy_alt in *.
andb_to_prop validBound_e_dV.
rewrite andb_true_iff; split; try auto.
destruct (absenv e1); destruct (absenv e2).
rewrite <- andb_lazy_alt.
rewrite andb_true_iff; split; try auto.
repeat (rewrite andb_true_iff; split); auto.
Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
forall E1 E2 outVars fVars dVars vR vF elo ehi err P,
approxEnv E1 absenv fVars dVars E2 ->
......@@ -393,11 +393,8 @@ Qed.
Fixpoint let_subst (f:cmd Q) :=
match f with
| Let x e1 g =>
match (let_subst g) with
|Some e' => Some (exp_subst e' x e1)
|None => None
| Ret e1 => Some e1
exp_subst (let_subst g) x e1
| Ret e1 => e1
Lemma eval_subst_subexp E e' n e vR:
......@@ -484,14 +481,13 @@ Proof.
destruct x_live as [x_used | x_live].
+ eapply eval_subst_subexp; eauto.
+ edestruct IHg as [v0 eval_v0]; eauto.
Theorem let_free_agree f E vR inVars outVars e:
ssa f inVars outVars ->
(forall v, NatSet.In v (definedVars f) ->
NatSet.In v (liveVars f)) ->
let_subst f = Some e ->
let_subst f = e ->
bstep (toRCmd (Ret e)) E 0 vR ->
bstep (toRCmd f) E 0 vR.
......@@ -503,7 +499,8 @@ Proof.
(* Let Case, prove that the value of the let binding must be used somewhere *)
- case_eq (let_subst s).
+ intros e0 subst_s; rewrite subst_s in *.
inversion subst_step; subst.
(*inversion subst_step; subst.
clear subst_s subst_step.
inversion bstep_e; subst.
specialize (dVars_live x).
......@@ -519,14 +516,12 @@ Proof.
eapply let_b.
Focus 2.
eapply IHssa_f; try auto.
eapply IHssa_f; try auto. *)
Theorem let_free_form f E vR inVars outVars e:
ssa f inVars outVars ->
bstep (toRCmd f) E 0 vR ->
let_subst f = Some e ->
let_subst f = e ->
bstep (toRCmd (Ret e)) E 0 vR.
revert E vR inVars outVars e;
......@@ -535,8 +530,8 @@ Proof.
- simpl.
inversion bstep_f; subst.
inversion ssa_f; subst.
simpl in subst_step.
case_eq (let_subst f).
(* case_eq (let_subst f).
+ intros f_subst subst_f_eq.
specialize (IHf (updEnv n v E) vR (NatSet.add n inVars) outVars f_subst H8 H6 subst_f_eq).
rewrite subst_f_eq in subst_step.
......@@ -552,6 +547,7 @@ Proof.
inversion subst_step; subst.
Lemma ssa_non_stuck (f:cmd Q) (inVars outVars:NatSet.t) (VarEnv:var_env)
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