From 594682479ec177f9df3cd5f78864822388bdc4b8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 14 Jan 2022 14:09:19 +0100
Subject: [PATCH] Add lemmas `app_cons_eq_inv_{l,r}`.

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

diff --git a/theories/list.v b/theories/list.v
index cf0eef6f..afeb2145 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -988,6 +988,27 @@ Proof.
   destruct (nth_lookup_or_length l i d); [done | by lia].
 Qed.
 
+Lemma app_cons_eq_inv_l x y l1 l2 k1 k2 :
+  x ∉ k1 → y ∉ l1 →
+  l1 ++ x :: l2 = k1 ++ y :: k2 →
+  l1 = k1 ∧ x = y ∧ l2 = k2.
+Proof.
+  revert k1. induction l1 as [|x' l1 IH]; intros [|y' k1] Hx Hy ?; simplify_eq/=;
+    try apply not_elem_of_cons in Hx as [??];
+    try apply not_elem_of_cons in Hy as [??]; naive_solver.
+Qed.
+Lemma app_cons_eq_inv_r x y l1 l2 k1 k2 :
+  x ∉ k2 → y ∉ l2 →
+  l1 ++ x :: l2 = k1 ++ y :: k2 →
+  l1 = k1 ∧ x = y ∧ l2 = k2.
+Proof.
+  intros. destruct (app_cons_eq_inv_l x y (reverse l2) (reverse l1)
+    (reverse k2) (reverse k1)); [..|naive_solver].
+  - by rewrite elem_of_reverse.
+  - by rewrite elem_of_reverse.
+  - rewrite <-!reverse_snoc, <-!reverse_app, <-!(assoc_L (++)). by f_equal.
+Qed.
+
 (** ** Properties of the [NoDup] predicate *)
 Lemma NoDup_nil : NoDup (@nil A) ↔ True.
 Proof. split; constructor. Qed.
-- 
GitLab