chore: de-mathlib List.Perm (#89)

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>

Std.lean

@@ -50,6 +50,7 @@ import Std.Data.List.Init.Attach
 import Std.Data.List.Init.Lemmas
 import Std.Data.List.Lemmas
 import Std.Data.List.Pairwise
+import Std.Data.List.Perm
 import Std.Data.MLList.Basic
 import Std.Data.MLList.Heartbeats
 import Std.Data.Nat.Basic

Std/Data/List/Basic.lean

@@ -1636,4 +1636,43 @@ protected def traverse [Applicative F] (f : α → F β) : List α → F (List 
   | [] => pure []
   | x :: xs => List.cons <$> f x <*> List.traverse f xs
 
+/--
+`Perm l₁ l₂` or `l₁ ~ l₂` asserts that `l₁` and `l₂` are permutations
+of each other. This is defined by induction using pairwise swaps.
+-/
+inductive Perm : List α → List α → Prop
+  /-- `[] ~ []` -/
+  | nil : Perm [] []
+  /-- `l₁ ~ l₂ → x::l₁ ~ x::l₂` -/
+  | cons (x : α) {l₁ l₂ : List α} : Perm l₁ l₂ → Perm (x :: l₁) (x :: l₂)
+  /-- `x::y::l ~ y::x::l` -/
+  | swap (x y : α) (l : List α) : Perm (y :: x :: l) (x :: y :: l)
+  /-- `Perm` is transitive. -/
+  | trans {l₁ l₂ l₃ : List α} : Perm l₁ l₂ → Perm l₂ l₃ → Perm l₁ l₃
+
+@[inherit_doc] scoped infixl:50 " ~ " => Perm
+
+/--
+`O(|l₁| * |l₂|)`. Computes whether `l₁` is a permutation of `l₂`. See `isPerm_iff` for a
+characterization in terms of `List.Perm`.
+-/
+def isPerm [BEq α] : List α → List α → Bool
+  | [], l₂ => l₂.isEmpty
+  | a :: l₁, l₂ => l₂.contains a && l₁.isPerm (l₂.erase a)
+
+/--
+`Subperm l₁ l₂`, denoted `l₁ <+~ l₂`, means that `l₁` is a sublist of
+a permutation of `l₂`. This is an analogue of `l₁ ⊆ l₂` which respects
+multiplicities of elements, and is used for the `≤` relation on multisets.
+-/
+def Subperm (l₁ l₂ : List α) : Prop := ∃ l, l ~ l₁ ∧ l <+ l₂
+
+@[inherit_doc] scoped infixl:50 " <+~ " => Subperm
+
+/--
+`O(|l₁| * (|l₁| + |l₂|))`. Computes whether `l₁` is a sublist of a permutation of `l₂`.
+See `isSubperm_iff` for a characterization in terms of `List.Subperm`.
+-/
+def isSubperm [BEq α] (l₁ l₂ : List α) : Bool := ∀ x ∈ l₁, count x l₁ ≤ count x l₂
+
 end List

Std/Data/List/Pairwise.lean

@@ -10,7 +10,7 @@ import Std.Data.Fin.Lemmas
 # Pairwise relations on a list
 
 This file provides basic results about `List.Pairwise` and `List.pwFilter` (definitions are in
-`Std.Data.List.Defs`).
+`Std.Data.List.Basic`).
 `Pairwise r [a 0, ..., a (n - 1)]` means `∀ i j, i < j → r (a i) (a j)`. For example,
 `Pairwise (≠) l` means that all elements of `l` are distinct, and `Pairwise (<) l` means that `l`
 is strictly increasing.