From be4eb64840d1d69dc44d098d1a3c6ef55c4575c4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 26 Nov 2018 16:03:37 +0100
Subject: [PATCH] Versions of `elem_of_list_split` that give first or last
 element.

---
 theories/list.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 56a35631..b74c1a13 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -647,6 +647,28 @@ Proof.
   induction 1 as [x l|x y l ? [l1 [l2 ->]]]; [by eexists [], l|].
   by exists (y :: l1), l2.
 Qed.
+Lemma elem_of_list_split_l `{EqDecision A} l x :
+  x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2 ∧ x ∉ l1.
+Proof.
+  induction 1 as [x l|x y l ? IH].
+  { exists [], l. rewrite elem_of_nil. naive_solver. }
+  destruct (decide (x = y)) as [->|?].
+  - exists [], l. rewrite elem_of_nil. naive_solver.
+  - destruct IH as (l1 & l2 & -> & ?).
+    exists (y :: l1), l2. rewrite elem_of_cons. naive_solver.
+Qed.
+Lemma elem_of_list_split_r `{EqDecision A} l x :
+  x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2 ∧ x ∉ l2.
+Proof.
+  induction l as [|y l IH] using rev_ind.
+  { by rewrite elem_of_nil. }
+  destruct (decide (x = y)) as [->|].
+  - exists l, []. rewrite elem_of_nil. naive_solver.
+  - rewrite elem_of_app, elem_of_list_singleton. intros [?| ->]; try done.
+    destruct IH as (l1 & l2 & -> & ?); auto.
+    exists l1, (l2 ++ [y]).
+    rewrite elem_of_app, elem_of_list_singleton, <-(assoc_L (++)). naive_solver.
+Qed.
 Lemma elem_of_list_lookup_1 l x : x ∈ l → ∃ i, l !! i = Some x.
 Proof.
   induction 1 as [|???? IH]; [by exists 0 |].
-- 
GitLab