prove logical popping lemma

theories/lang/stbor/stbor_sim.v

@@ -446,7 +446,7 @@ Lemma stack_sub_tail_no_sharedro stklog stkparsed :
   stack_sub_tail stklog stkparsed → ¬ ∃ tgs stklog', stklog = ItSharedRO tgs :: stklog'.
 Proof.
   intros Hsub.
-  induction Hsub as [|? ? ? ? ? IH|? ? ? ? ? Hsubit|z w x y p].
+  induction Hsub as [|? ? ? ? ? IH|? ? ? ? ? Hsubit|].
   - intros (? & ? & Heq). inversion Heq.
   - apply IH.
   - intros (? & ? & Heq). inversion Hsubit; subst; inversion Heq.
@@ -481,10 +481,51 @@ Qed.
 (** * Retagging (SharedRW) extend *)
 
 (** * Logical popping *)
+Lemma pop_prefix_preserve_tail stkparsed stklog1 stklog2 :
+  stklog2 `suffix_of` stklog1 →
+  stack_sub_tail stklog1 stkparsed →
+  stack_sub_tail stklog2 stkparsed.
+Proof.
+  intros (stkdead & Hsuffix) Hsub.
+  generalize dependent stkdead.
+  induction Hsub as [|? ? ? ? ? IH|? ? ? ? ? ? ? IH|? ? ? ? ? ? ? ? ? IH]; intros stkdead Hsuffix.
+  - symmetry in Hsuffix. apply app_eq_nil in Hsuffix as [-> ->].
+    apply stack_sub_tail_empty.
+  - apply stack_sub_tail_drop_both. eapply IH. eassumption.
+  - destruct stkdead as [|itdead stkdead].
+    + simpl in Hsuffix. rewrite -Hsuffix.
+      by apply stack_sub_tail_drop_one.
+    + rewrite -app_comm_cons in Hsuffix. inversion Hsuffix.
+      apply stack_sub_tail_drop_both. eapply IH. eassumption.
+  - destruct stkdead as [|itdead1 [|itdead2 stkdead]].
+    + simpl in Hsuffix. rewrite -Hsuffix.
+      by apply stack_sub_tail_keep.
+    + inversion Hsuffix.
+      by apply stack_sub_tail_drop_one.
+    + inversion Hsuffix.
+      apply stack_sub_tail_drop_both. eapply IH. eassumption.
+Qed.
+
 Lemma pop_prefix_preserve stkphys stklog1 stklog2 :
   stklog2 `suffix_of` stklog1 →
   stack_rel_stack stkphys stklog1 →
   stack_rel_stack stkphys stklog2.
-Proof. Admitted.
+Proof.
+  intros (stkdead & Hsuffix) (stkparsed & Hparse & Hsub).
+  destruct Hsub.
+  - destruct stkdead as [|itdead stkdead].
+    + simpl in Hsuffix. rewrite -Hsuffix.
+      eexists; split; first apply Hparse.
+      by apply stack_sub_keep_shared.
+    + rewrite -app_comm_cons in Hsuffix. inversion Hsuffix.
+      eexists; split; first apply Hparse.
+      apply stack_sub_drop_shared.
+      eapply pop_prefix_preserve_tail; last eassumption.
+      by exists stkdead.
+  - eexists; split; first apply Hparse.
+    apply stack_sub_drop_shared.
+    eapply pop_prefix_preserve_tail; last eassumption.
+    by exists stkdead.
+Qed.
 
 (** * Logical disabling *)