From 3b9d41188618b2c1e007091e46e2bf09a4e23ed5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 1 Jun 2021 16:57:09 +0200
Subject: [PATCH] Add lemma `Permutation_cross_split`.

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

diff --git a/theories/list.v b/theories/list.v
index b1cc30e7..f6a83135 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1771,6 +1771,27 @@ Proof.
     by rewrite <-Hk, <-(delete_Permutation k) by done.
 Qed.
 
+Lemma Permutation_cross_split l la lb lc ld :
+  la ++ lb ≡ₚ l →
+  lc ++ ld ≡ₚ l →
+  ∃ lac lad lbc lbd,
+    lac ++ lad ≡ₚ la ∧ lbc ++ lbd ≡ₚ lb ∧ lac ++ lbc ≡ₚ lc ∧ lad ++ lbd ≡ₚ ld.
+Proof.
+  intros <-. revert lc ld.
+  induction la as [|x la IH]; simpl; intros lc ld Hperm.
+  { exists [], [], lc, ld. by rewrite !(right_id_L [] (++)). }
+  assert (x ∈ lc ++ ld)
+    as [[lc' Hlc]%elem_of_Permutation|[ld' Hld]%elem_of_Permutation]%elem_of_app.
+  { rewrite Hperm, elem_of_cons. auto. }
+  - rewrite Hlc in Hperm. simpl in Hperm. apply (inj (x ::.)) in Hperm.
+    apply IH in Hperm as (lac&lad&lbc&lbd&Ha&Hb&Hc&Hd).
+    exists (x :: lac), lad, lbc, lbd; simpl. by rewrite Ha, Hb, Hc, Hd.
+  - rewrite Hld, <-Permutation_middle in Hperm. apply (inj (x ::.)) in Hperm.
+    apply IH in Hperm as (lac&lad&lbc&lbd&Ha&Hb&Hc&Hd).
+    exists lac, (x :: lad), lbc, lbd; simpl.
+    by rewrite <-Permutation_middle, Ha, Hb, Hc, Hd.
+Qed.
+
 Lemma Permutation_inj l1 l2 :
   Permutation l1 l2 ↔
     length l1 = length l2 ∧
-- 
GitLab