From 5bb9627f73d54346bef7c0df038fb0ac2be1b6bd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 1 Jun 2021 16:56:43 +0200
Subject: [PATCH 1/6] =?UTF-8?q?Make=20`elem=5Fof=5FPermutation`=20a=20`?=
 =?UTF-8?q?=E2=86=94`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/list.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index f2d9a5d0..b1cc30e7 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1753,8 +1753,12 @@ Proof.
   revert i; induction l as [|y l IH]; intros [|i] ?; simplify_eq/=; auto.
   by rewrite Permutation_swap, <-(IH i).
 Qed.
-Lemma elem_of_Permutation l x : x ∈ l → ∃ k, l ≡ₚ x :: k.
-Proof. intros [i ?]%elem_of_list_lookup. eauto using delete_Permutation. Qed.
+Lemma elem_of_Permutation l x : x ∈ l ↔ ∃ k, l ≡ₚ x :: k.
+Proof.
+  split.
+  - intros [i ?]%elem_of_list_lookup. eexists. by apply delete_Permutation.
+  - intros [k ->]. by left.
+Qed.
 
 Lemma Permutation_cons_inv l k x :
   k ≡ₚ x :: l → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
-- 
GitLab


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 2/6] 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


From 3f893ee40f6b7cb0224ff955b42074d5177682d3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 1 Jun 2021 17:02:43 +0200
Subject: [PATCH 3/6] Remove instances from stdlib.

---
 theories/list.v | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index f6a83135..abcd8055 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -31,7 +31,6 @@ Global Instance: Params (@drop) 1 := {}.
 
 Global Arguments Permutation {_} _ _ : assert.
 Global Arguments Forall_cons {_} _ _ _ _ _ : assert.
-Global Remove Hints Permutation_cons : typeclass_instances.
 
 Notation "(::)" := cons (only parsing) : list_scope.
 Notation "( x ::.)" := (cons x) (only parsing) : list_scope.
@@ -1705,10 +1704,6 @@ Proof. apply perm_swap. Qed.
 Lemma Permutation_singleton_inj x y : [x] ≡ₚ [y] → x = y.
 Proof. apply Permutation_length_1. Qed.
 
-Global Instance Permutation_cons x : Proper ((≡ₚ) ==> (≡ₚ)) (@cons A x).
-Proof. by constructor. Qed.
-Global Existing Instance Permutation_app'.
-
 Global Instance elem_of_list_permutation_proper x : Proper ((≡ₚ) ==> iff) (x ∈.).
 Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
 Global Instance NoDup_proper: Proper ((≡ₚ) ==> iff) (@NoDup A).
@@ -1812,7 +1807,7 @@ Proof.
     induction l1 as [|x l1 IH]; intros l2 f Hlen Hf Hl; [by destruct l2|].
     rewrite (delete_Permutation l2 (f 0) x) by (by rewrite <-Hl).
     pose (g n := let m := f (S n) in if lt_eq_lt_dec m (f 0) then m else m - 1).
-    eapply Permutation_cons, (IH _ g).
+    apply Permutation_skip, (IH _ g).
     + rewrite length_delete by (rewrite <-Hl; eauto); simpl in *; lia.
     + unfold g. intros i j Hg.
       repeat destruct (lt_eq_lt_dec _ _) as [[?|?]|?]; simplify_eq/=; try lia.
-- 
GitLab


From 0bb21a4f01a1617712e8c0b97db7c10b6ca297e6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 1 Jun 2021 17:07:07 +0200
Subject: [PATCH 4/6] Name instances for `Permutation` and add new instance
 `cons_Permutation_inj_l`.

Naming scheme: `operation_Permutation_{Proper,inj,inj_l,inj_r}`.
---
 theories/list.v | 27 +++++++++++++++++----------
 1 file changed, 17 insertions(+), 10 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index abcd8055..deb74608 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1704,9 +1704,11 @@ Proof. apply perm_swap. Qed.
 Lemma Permutation_singleton_inj x y : [x] ≡ₚ [y] → x = y.
 Proof. apply Permutation_length_1. Qed.
 
-Global Instance elem_of_list_permutation_proper x : Proper ((≡ₚ) ==> iff) (x ∈.).
+Global Instance length_Permutation_proper : Proper ((≡ₚ) ==> (=)) (@length A).
+Proof. induction 1; simpl; auto with lia. Qed.
+Global Instance elem_of_Permutation_proper x : Proper ((≡ₚ) ==> iff) (x ∈.).
 Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
-Global Instance NoDup_proper: Proper ((≡ₚ) ==> iff) (@NoDup A).
+Global Instance NoDup_Permutation_proper: Proper ((≡ₚ) ==> iff) (@NoDup A).
 Proof.
   induction 1 as [|x l k Hlk IH | |].
   - by rewrite !NoDup_nil.
@@ -1715,23 +1717,28 @@ Proof.
   - intuition.
 Qed.
 
-Global Instance: Proper ((≡ₚ) ==> (=)) (@length A).
-Proof. induction 1; simpl; auto with lia. Qed.
-Global Instance: Comm (≡ₚ) (@app A).
+Global Instance app_Permutation_comm : Comm (≡ₚ) (@app A).
 Proof.
   intros l1. induction l1 as [|x l1 IH]; intros l2; simpl.
   - by rewrite (right_id_L [] (++)).
   - rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
 Qed.
-Global Instance: ∀ x : A, Inj (≡ₚ) (≡ₚ) (x ::.).
+
+Global Instance cons_Permutation_inj_r x : Inj (≡ₚ) (≡ₚ) (x ::.).
 Proof. red. eauto using Permutation_cons_inv. Qed.
-Global Instance: ∀ k : list A, Inj (≡ₚ) (≡ₚ) (k ++.).
+Global Instance app_Permutation_inj_r k : Inj (≡ₚ) (≡ₚ) (k ++.).
 Proof.
-  intros k. induction k as [|x k IH]; intros l1 l2; simpl; auto.
+  induction k as [|x k IH]; intros l1 l2; simpl; auto.
   intros. by apply IH, (inj (x ::.)).
 Qed.
-Global Instance: ∀ k : list A, Inj (≡ₚ) (≡ₚ) (.++ k).
-Proof. intros k l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++.)). Qed.
+Global Instance cons_Permutation_inj_l k : Inj (=) (≡ₚ) (.:: k).
+Proof.
+  intros x1 x2 Hperm. apply Permutation_singleton_inj.
+  apply (inj (k ++.)). by rewrite !(comm (++) k).
+Qed.
+Global Instance app_Permutation_inj_l k : Inj (≡ₚ) (≡ₚ) (.++ k).
+Proof. intros l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++.)). Qed.
+
 Lemma replicate_Permutation n x l : replicate n x ≡ₚ l → replicate n x = l.
 Proof.
   intros Hl. apply replicate_as_elem_of. split.
-- 
GitLab


From 33b3cd0dcabac33383f66bf5abb662443de5543a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 1 Jun 2021 17:27:08 +0200
Subject: [PATCH 5/6] Rename `Permutation_nil` and `Permutation_singleton` into
 `Permutation_nil_r` and `Permutation_singleton_r`.

Add lemmas `Permutation_nil_l` and `Permutation_singleton_l`.
---
 theories/fin_maps.v |  2 +-
 theories/fin_sets.v |  4 ++--
 theories/list.v     | 13 ++++++++++---
 theories/sorting.v  |  2 +-
 4 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 45a0cc67..1d1dd5ca 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -938,7 +938,7 @@ Qed.
 Lemma map_to_list_singleton {A} i (x : A) :
   map_to_list ({[i:=x]} : M A) = [(i,x)].
 Proof.
-  apply Permutation_singleton. unfold singletonM, map_singleton.
+  apply Permutation_singleton_r. unfold singletonM, map_singleton.
   by rewrite map_to_list_insert, map_to_list_empty by eauto using lookup_empty.
 Qed.
 Lemma map_to_list_delete {A} (m : M A) i x :
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 21b71cc6..a4581571 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -85,7 +85,7 @@ Qed.
 Lemma elements_empty' X : elements X = [] ↔ X ≡ ∅.
 Proof.
   split; intros HX; [by apply elements_empty_inv|].
-  by rewrite <-Permutation_nil, HX, elements_empty.
+  by rewrite <-Permutation_nil_r, HX, elements_empty.
 Qed.
 
 Lemma elements_union_singleton (X : C) x :
@@ -99,7 +99,7 @@ Proof.
 Qed.
 Lemma elements_singleton x : elements ({[ x ]} : C) = [x].
 Proof.
-  apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}),
+  apply Permutation_singleton_r. by rewrite <-(right_id ∅ (∪) {[x]}),
     elements_union_singleton, elements_empty by set_solver.
 Qed.
 Lemma elements_disj_union (X Y : C) :
diff --git a/theories/list.v b/theories/list.v
index deb74608..1f8f5ed0 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1692,10 +1692,14 @@ Proof.
 Qed.
 
 (** ** Properties of the [Permutation] predicate *)
-Lemma Permutation_nil l : l ≡ₚ [] ↔ l = [].
+Lemma Permutation_nil_r l : l ≡ₚ [] ↔ l = [].
 Proof. split; [by intro; apply Permutation_nil | by intros ->]. Qed.
-Lemma Permutation_singleton l x : l ≡ₚ [x] ↔ l = [x].
+Lemma Permutation_singleton_r l x : l ≡ₚ [x] ↔ l = [x].
 Proof. split; [by intro; apply Permutation_length_1_inv | by intros ->]. Qed.
+Lemma Permutation_nil_l l : [] ≡ₚ l ↔ [] = l.
+Proof. by rewrite (symmetry_iff (≡ₚ)), Permutation_nil_r. Qed.
+Lemma Permutation_singleton_l l x : [x] ≡ₚ l ↔ [x] = l.
+Proof. by rewrite (symmetry_iff (≡ₚ)), Permutation_singleton_r. Qed.
 
 Lemma Permutation_skip x l l' : l ≡ₚ l' → x :: l ≡ₚ x :: l'.
 Proof. apply perm_skip. Qed.
@@ -1762,7 +1766,7 @@ Proof.
   - intros [k ->]. by left.
 Qed.
 
-Lemma Permutation_cons_inv l k x :
+Lemma Permutation_cons_inv_r l k x :
   k ≡ₚ x :: l → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
 Proof.
   intros Hk. assert (∃ i, k !! i = Some x) as [i Hi].
@@ -1772,6 +1776,9 @@ Proof.
   - rewrite <-delete_take_drop. apply (inj (x ::.)).
     by rewrite <-Hk, <-(delete_Permutation k) by done.
 Qed.
+Lemma Permutation_cons_inv_l l k x :
+  x :: l ≡ₚ k → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
+Proof. by intros ?%(symmetry_iff (≡ₚ))%Permutation_cons_inv_r. Qed.
 
 Lemma Permutation_cross_split l la lb lc ld :
   la ++ lb ≡ₚ l →
diff --git a/theories/sorting.v b/theories/sorting.v
index 3f019e54..afd9da0b 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -77,7 +77,7 @@ Section sorted.
     intros Hl1; revert l2. induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hl2 E.
     { symmetry. by apply Permutation_nil. }
     destruct Hl2 as [|x2 l2 ? Hx2].
-    { by apply Permutation_nil in E. }
+    { by apply Permutation_nil_r in E. }
     assert (x1 = x2); subst.
     { rewrite Forall_forall in Hx1, Hx2.
       assert (x2 ∈ x1 :: l1) as Hx2' by (by rewrite E; left).
-- 
GitLab


From c2d434915a0a49722db26dd18a00db6e7b836d55 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 1 Jun 2021 23:25:57 +0200
Subject: [PATCH 6/6] CHANGELOG.

---
 CHANGELOG.md | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 43ca289c..5b8d421e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -30,6 +30,13 @@ API-breaking change is listed.
 - Add `Countable` instance for decidable Sigma types. (by Simon Gregersen)
 - Add tactics `compute_done` and `compute_by` for solving goals by computation.
 - Add `Inj` instances for `fmap` on option and maps.
+- Various changes to `Permutation` lemmas:
+  + Rename `Permutation_nil` → `Permutation_nil_r` and
+    and `Permutation_singleton` → `Permutation_singleton_r`.
+  + Add lemmas `Permutation_nil_l` and `Permutation_singleton_l`.
+  + Add new instance `cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k).`.
+  + Add lemma `Permutation_cross_split`.
+  + Make lemma `elem_of_Permutation` a biimplication
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -37,6 +44,9 @@ The following `sed` script should perform most of the renaming
 sed -i -E '
 s/\bdecide_left\b/decide_True_pi/g
 s/\bdecide_right\b/decide_False_pi/g
+# Permutation
+s/\bPermutation_nil\b/Permutation_nil_r/g
+s/\bPermutation_singleton\b/Permutation_singleton_r/g
 ' $(find theories -name "*.v")
 ```
 
-- 
GitLab