Proving admitted ssem_exit_fallthrough_upto_exit -> need to prove is_tail_exists

1 files changed, 38 insertions, 30 deletions

diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v
index fae3c557..07cdc65d 100644
--- a/mppa_k1c/lib/RTLpathSE_theory.v
+++ b/mppa_k1c/lib/RTLpathSE_theory.v
@@ -304,13 +304,15 @@ Proof.
 Qed.
 
 (* Actually this lemma isn't used *)
-Remark is_tail_cons_eq {A: Type} (a a': A) l l':
+Remark is_tail_inv_left {A: Type} (a a': A) l l':
   is_tail (a::l) (a'::l') ->
-  a = a' \/ (In a l').
+  (a = a' /\ l = l') \/ (In a l' /\ is_tail l (a'::l')).
 Proof.
   intros. inv H.
-  - left. reflexivity.
-  - right. eapply is_tail_in; eauto.
+  - left. eauto.
+  - right. econstructor.
+    + eapply is_tail_in; eauto.
+    + eapply is_tail_cons_left; eauto.
 Qed.
 
 Lemma ssem_determ ge sp st rs m is1 is2:
@@ -344,31 +346,6 @@ Proof.
   inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
 Qed.
 
-(* Lemma ssem_local_exclude_sabort_exits ge sp st rs m rs' m':
-  ssem_local ge sp (si_local st) rs m rs' m' ->
-  all_fallthrough ge sp (si_exits st) rs m ->
-  sabort_exits ge sp (si_exits st) rs m ->
-  False.
-Proof.
-  intros SIML ALLF ABORT. inv ABORT.
-  - exploit ALLF; eauto. congruence.
-  - exploit ALLF; eauto. congruence.
-Qed. *)
-
-(* Lemma all_fallthrough_exclude_sabort_exit ge sp ext lx rs m:
-  In ext lx ->
-  all_fallthrough ge sp lx rs m ->
-  sabort_exit ge sp ext rs m ->
-  False.
-Proof.
-  intros INL ALLF ABORT. inv ABORT.
-  - unfold all_fallthrough in ALLF. eapply ALLF in INL. congruence.
-  - unfold all_fallthrough in ALLF. eapply ALLF in INL. unfold sabort_local in H. congruence.
-  intros SIML ALLF ABORT. inv ABORT.
-  - exploit ALLF; eauto. congruence.
-  - exploit ALLF; eauto. congruence.
-Qed. *)
-
 Lemma ssem_local_exclude_sabort_exit ge sp st ext lx rs m rs' m':
   ssem_local ge sp (si_local st) rs m rs' m' ->
   all_fallthrough ge sp (si_exits st) rs m ->
@@ -396,13 +373,44 @@ Proof.
   - destruct H as (ext & lx & ALLFU & SABORT). inv ALLFU. eapply ssem_local_exclude_sabort_exit; eauto.
 Qed.
 
+Lemma is_tail_exists {A: Type}:
+  forall l l' (a' a: A),
+  In a' l ->
+  is_tail (a'::l') (a::l) ->
+  exists x, is_tail (x::a'::l') (a::l).
+Proof.
+Admitted. (* should be provable by inference on l ? hopefully *)
+
+
+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). eapply is_tail_exists; 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.
-Admitted.
+  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.
+Qed.
 
 Lemma ssem_exit_exclude_sabort_exit ge sp ext rs m rs' m' pc':
   ssem_exit ge sp ext rs m rs' m' pc' ->