refactor for #92

2 files changed, 31 insertions, 5 deletions

diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
index 3023ad8a..d1950209 100644
--- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
+++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
@@ -211,7 +211,33 @@ Proof.
   intros; eapply res_eq_trans. eapply alt_bblock_equiv_refl; eauto.
   eauto.
 Qed.
- 
+
+
+Lemma run_app p1: forall m1 p2,
+   run (p1++p2) m1 = 
+     match run p1 m1 with 
+     | Some m2 => run p2 m2 
+     | None => None
+     end.
+Proof.
+   induction p1; simpl; try congruence.
+   intros; destruct (inst_run _ _ _); simpl; auto.
+Qed.
+
+Lemma run_app_None p1 m1 p2:
+   run p1 m1 = None ->
+   run (p1++p2) m1 = None.
+Proof.
+   intro H; rewrite run_app. rewrite H; auto.
+Qed.
+
+Lemma run_app_Some p1 m1 m2 p2:
+   run p1 m1 = Some m2 ->
+   run (p1++p2) m1 = run p2 m2.
+Proof.
+   intros H; rewrite run_app. rewrite H; auto.
+Qed.
+
 End SEQLANG.
 
 End MkSeqLanguage.
diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v
index d1971e57..eae7b672 100644
--- a/mppa_k1c/abstractbb/Parallelizability.v
+++ b/mppa_k1c/abstractbb/Parallelizability.v
@@ -91,18 +91,18 @@ Proof.
    intros; destruct (inst_prun _ _ _); simpl; auto.
 Qed.
 
-Lemma prun_iw_app_None p1: forall m1 old p2,
+Lemma prun_iw_app_None p1 m1 old p2:
    prun_iw p1 m1 old = None ->
    prun_iw (p1++p2) m1 old = None.
 Proof.
-   intros m1 old p2 H; rewrite prun_iw_app. rewrite H; auto.
+   intros H; rewrite prun_iw_app. rewrite H; auto.
 Qed.
 
-Lemma prun_iw_app_Some p1: forall m1 old m2 p2,
+Lemma prun_iw_app_Some p1 m1 old m2 p2:
    prun_iw p1 m1 old = Some m2 ->
    prun_iw (p1++p2) m1 old = prun_iw p2 m2 old.
 Proof.
-   intros m1 old m2 p2 H; rewrite prun_iw_app. rewrite H; auto.
+   intros H; rewrite prun_iw_app. rewrite H; auto.
 Qed.
 
 End PARALLEL.