ssem_exit_fallthrough_upto_exit finally done - it was very simple actually

1 files changed, 7 insertions, 64 deletions

diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v
index 495b544e..8ea4f9a7 100644
--- a/mppa_k1c/lib/RTLpathSE_theory.v
+++ b/mppa_k1c/lib/RTLpathSE_theory.v
@@ -331,76 +331,19 @@ Proof.
   - destruct H as (ext & lx & ALLFU & SABORT). inv ALLFU. eapply ssem_local_exclude_sabort_exit; eauto.
 Qed.
 
-Lemma is_tail_revcons_left {A: Type}:
-  forall l l' (a: A),
-  ~ (In a l') ->
-  is_tail l' (a::l) ->
-  is_tail (a::l') (a::l).
-Proof.
-  induction l.
-  - intros l' a NOTIN TAIL. inv TAIL.
-    + contradict NOTIN. econstructor; eauto.
-    + inv H1. econstructor; eauto.
-  - intros l' b NOTIN TAIL. inv TAIL.
-    + contradict NOTIN. repeat (econstructor; eauto).
-    +
-Abort.
-
-Lemma is_tail_exists {A: Type}:
-  forall l l' (a' a: A),
-  In a' l ->
-  is_tail (a'::l') (a::l) ->
-     (a' = a /\ l' = l)
-  \/ (exists x, In x (a::l) /\ is_tail (x::a'::l') (a::l)).
-Proof.
-  induction l.
-  - intros. inv H.
-  - intros l' a' b INH TAIL. destruct INH as [EQA|INH]; subst.
-    + inv TAIL.
-      ++ left. econstructor; eauto.
-      ++ admit.
-    + inv TAIL.
-      ++ left. repeat (econstructor; eauto).
-      ++ eapply IHl in INH; eauto. inv INH.
-        +++ inv H. right. exists b. constructor.
-            * repeat (econstructor; eauto).
-            * econstructor; eauto.
-        +++ right. destruct H as (x & INX & TAIL). exists x.
-            constructor. eapply in_cons; eauto. eapply is_tail_cons; eauto.  
-Abort.
-
-Remark ssem_exit_fallthrough_upto_exit' ge sp ext ext' lx lx' exits rs m rs' m' pc':
-  ssem_exit ge sp ext rs m rs' m' pc' ->
-  all_fallthrough_upto_exit ge sp ext lx exits rs m ->
-  all_fallthrough_upto_exit ge sp ext' lx' exits rs m ->
-  (ext = ext' /\ lx = lx') \/ exists i, is_tail (i::ext'::lx') (ext::lx).
-Proof.
-  intros EXIT ALLFU ALLFU'.
-  destruct EXIT as (COND & _ & _).
-  destruct ALLFU as (TAIL & ALLFU).
-  destruct ALLFU' as (TAIL' & ALLFU').
-  destruct (is_tail_bounded_total (ext::lx) (ext'::lx') exits); eauto.
-  - destruct (is_tail_inv_left ext ext' lx lx') as [EQ|TAIL2]; eauto.
-    destruct TAIL2 as (INEXT & _). eapply ALLFU' in INEXT. congruence.
-  - destruct (is_tail_inv_left ext' ext lx' lx) as [EQ|TAIL2]; eauto.
-    + left. intuition eauto.
-    + right. destruct TAIL2 as (INN & TAIL2).
-      exploit (is_tail_exists lx); eauto.
-      intros H'. inv H'.
-      * inv H0. eapply ALLFU in INN. congruence. (* absurd case *)
-      * destruct H0 as (x & _ & TAIL3). eauto.
-Qed.
-
 Lemma ssem_exit_fallthrough_upto_exit ge sp ext ext' lx lx' exits rs m rs' m' pc':
   ssem_exit ge sp ext rs m rs' m' pc' ->
   all_fallthrough_upto_exit ge sp ext lx exits rs m ->
   all_fallthrough_upto_exit ge sp ext' lx' exits rs m ->
   is_tail (ext'::lx') (ext::lx).
 Proof.
-  intros. exploit ssem_exit_fallthrough_upto_exit'; eauto. intro.
-  destruct H2 as [(A & B) | (i & TAIL)].
-  - subst. econstructor; eauto.
-  - eapply is_tail_cons_left; eauto.
+  intros SSEME ALLFU ALLFU'.
+  destruct ALLFU as (ISTAIL & ALLFU). destruct ALLFU' as (ISTAIL' & ALLFU').
+  destruct (is_tail_bounded_total (ext::lx) (ext'::lx') exits); eauto.
+  inv H.
+  - econstructor; eauto.
+  - eapply is_tail_in in H2. eapply ALLFU' in H2.
+    destruct SSEME as (SEVAL & _). congruence.
 Qed.
 
 Lemma ssem_exit_exclude_sabort_exit ge sp ext rs m rs' m' pc':