Module docstring
{"# List Permutations
This file introduces the List.Perm relation, which is true if two lists are permutations of one
another.
Notation
The notation ~ is used for permutation equivalence.
"}
List.Perm.refl
theorem
: ∀ l : List α, l ~ l
Informal description
For any list $l$ of elements of type $\alpha$, the list $l$ is a permutation of itself, i.e., $l \sim l$.
List.Perm.rfl
theorem
{l : List α} : l ~ l
Informal description
For any list $l$ of elements of type $\alpha$, the list $l$ is a permutation of itself, i.e., $l \sim l$.
List.Perm.of_eq
theorem
(h : l₁ = l₂) : l₁ ~ l₂
Full source
theorem Perm.of_eq (h : l₁ = l₂) : l₁ ~ l₂ := h ▸ .rflInformal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1 = l_2$, then $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$).
List.Perm.symm
theorem
{l₁ l₂ : List α} (h : l₁ ~ l₂) : l₂ ~ l₁
Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, if $l₁$ is a permutation of $l₂$ (denoted $l₁ \sim l₂$), then $l₂$ is also a permutation of $l₁$ (i.e., $l₂ \sim l₁$).
List.instTransPerm
instance
: Trans (Perm (α := α)) (Perm (α := α)) (Perm (α := α))
Informal description
The permutation relation `~` on lists is transitive. That is, for any lists $l_1$, $l_2$, and $l_3$ of type $\alpha$, if $l_1 \sim l_2$ and $l_2 \sim l_3$, then $l_1 \sim l_3$.
List.perm_comm
theorem
{l₁ l₂ : List α} : l₁ ~ l₂ ↔ l₂ ~ l₁
Full source
theorem perm_comm {l₁ l₂ : List α} : l₁ ~ l₂l₁ ~ l₂ ↔ l₂ ~ l₁ := ⟨Perm.symm, Perm.symm⟩Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, $l_1$ is a permutation of $l_2$ if and only if $l_2$ is a permutation of $l_1$. In other words, the permutation relation $\sim$ is symmetric.
List.Perm.congr_left
theorem
{l₁ l₂ : List α} (h : l₁ ~ l₂) (l₃ : List α) : l₁ ~ l₃ ↔ l₂ ~ l₃
Full source
protected theorem Perm.congr_left {l₁ l₂ : List α} (h : l₁ ~ l₂) (l₃ : List α) :
l₁ ~ l₃l₁ ~ l₃ ↔ l₂ ~ l₃ :=
⟨h.symm.trans, h.trans⟩Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$ such that $l₁$ is a permutation of $l₂$ (denoted $l₁ \sim l₂$), and for any list $l₃$ of type $\alpha$, the statement $l₁ \sim l₃$ holds if and only if $l₂ \sim l₃$ holds.
List.Perm.congr_right
theorem
{l₁ l₂ : List α} (h : l₁ ~ l₂) (l₃ : List α) : l₃ ~ l₁ ↔ l₃ ~ l₂
Full source
protected theorem Perm.congr_right {l₁ l₂ : List α} (h : l₁ ~ l₂) (l₃ : List α) :
l₃ ~ l₁l₃ ~ l₁ ↔ l₃ ~ l₂ :=
⟨fun h' => h'.trans h, fun h' => h'.trans h.symm⟩Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$ such that $l₁$ is a permutation of $l₂$ (denoted $l₁ \sim l₂$), and for any list $l₃$ of elements of type $\alpha$, the list $l₃$ is a permutation of $l₁$ if and only if $l₃$ is a permutation of $l₂$. In other words, $l₃ \sim l₁ \leftrightarrow l₃ \sim l₂$.
List.Perm.swap'
theorem
(x y : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : y :: x :: l₁ ~ x :: y :: l₂
Full source
theorem Perm.swap' (x y : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : y :: x :: l₁y :: x :: l₁ ~ x :: y :: l₂ :=
(swap ..).trans <| p.cons _ |>.cons _Informal description
For any elements $x$ and $y$ of type $\alpha$ and any lists $l_1$ and $l_2$ of type $\alpha$ such that $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), the list $y :: x :: l_1$ is a permutation of $x :: y :: l_2$.
List.Perm.recOnSwap'
theorem
{motive : (l₁ : List α) → (l₂ : List α) → l₁ ~ l₂ → Prop} {l₁ l₂ : List α} (p : l₁ ~ l₂) (nil : motive [] [] .nil)
(cons : ∀ x {l₁ l₂}, (h : l₁ ~ l₂) → motive l₁ l₂ h → motive (x :: l₁) (x :: l₂) (.cons x h))
(swap' : ∀ x y {l₁ l₂}, (h : l₁ ~ l₂) → motive l₁ l₂ h → motive (y :: x :: l₁) (x :: y :: l₂) (.swap' _ _ h))
(trans :
∀ {l₁ l₂ l₃}, (h₁ : l₁ ~ l₂) → (h₂ : l₂ ~ l₃) → motive l₁ l₂ h₁ → motive l₂ l₃ h₂ → motive l₁ l₃ (.trans h₁ h₂)) :
motive l₁ l₂ p
Full source
/--
Similar to `Perm.recOn`, but the `swap` case is generalized to `Perm.swap'`,
where the tail of the lists are not necessarily the same.
-/
@[elab_as_elim] theorem Perm.recOnSwap'
{motive : (l₁ : List α) → (l₂ : List α) → l₁ ~ l₂ → Prop} {l₁ l₂ : List α} (p : l₁ ~ l₂)
(nil : motive [] [] .nil)
(cons : ∀ x {l₁ l₂}, (h : l₁ ~ l₂) → motive l₁ l₂ h → motive (x :: l₁) (x :: l₂) (.cons x h))
(swap' : ∀ x y {l₁ l₂}, (h : l₁ ~ l₂) → motive l₁ l₂ h →
motive (y :: x :: l₁) (x :: y :: l₂) (.swap' _ _ h))
(trans : ∀ {l₁ l₂ l₃}, (h₁ : l₁ ~ l₂) → (h₂ : l₂ ~ l₃) → motive l₁ l₂ h₁ → motive l₂ l₃ h₂ →
motive l₁ l₃ (.trans h₁ h₂)) : motive l₁ l₂ p :=
have motive_refl l : motive l l (.refl l) :=
List.recOn l nil fun x xs ih => cons x (.refl xs) ih
Perm.recOn p nil cons (fun x y l => swap' x y (.refl l) (motive_refl l)) transInformal description
Given a predicate `motive` on pairs of lists and a proof that they are permutations, and given proofs that:
1. `motive` holds for the empty lists,
2. for any element `x` and lists `l₁`, `l₂` with `l₁ ~ l₂`, if `motive l₁ l₂` holds then `motive (x :: l₁) (x :: l₂)` holds,
3. for any elements `x`, `y` and lists `l₁`, `l₂` with `l₁ ~ l₂`, if `motive l₁ l₂` holds then `motive (y :: x :: l₁) (x :: y :: l₂)` holds, and
4. for any lists `l₁`, `l₂`, `l₃` with `l₁ ~ l₂` and `l₂ ~ l₃`, if `motive l₁ l₂` and `motive l₂ l₃` hold then `motive l₁ l₃` holds,
then `motive l₁ l₂` holds for any two lists `l₁` and `l₂` with `l₁ ~ l₂`.
List.Perm.eqv
theorem
(α) : Equivalence (@Perm α)
Full source
theorem Perm.eqv (α) : Equivalence (@Perm α) := ⟨.refl, .symm, .trans⟩Informal description
For any type $\alpha$, the permutation relation `~` on lists of type $\alpha$ is an equivalence relation. That is, it satisfies:
1. Reflexivity: For any list $l$, $l \sim l$.
2. Symmetry: For any lists $l_1$ and $l_2$, if $l_1 \sim l_2$, then $l_2 \sim l_1$.
3. Transitivity: For any lists $l_1$, $l_2$, and $l_3$, if $l_1 \sim l_2$ and $l_2 \sim l_3$, then $l_1 \sim l_3$.
List.isSetoid
instance
(α) : Setoid (List α)
Informal description
For any type $\alpha$, the set of lists of elements of type $\alpha$ forms a setoid, where the equivalence relation is given by list permutation (denoted by $\sim$). This means the permutation relation is reflexive, symmetric, and transitive.
List.Perm.mem_iff
theorem
{a : α} {l₁ l₂ : List α} (p : l₁ ~ l₂) : a ∈ l₁ ↔ a ∈ l₂
Full source
theorem Perm.mem_iff {a : α} {l₁ l₂ : List α} (p : l₁ ~ l₂) : a ∈ l₁a ∈ l₁ ↔ a ∈ l₂ := by
induction p with
| nil => rfl
| cons _ _ ih => simp only [mem_cons, ih]
| swap => simp only [mem_cons, or_left_comm]
| trans _ _ ih₁ ih₂ => simp only [ih₁, ih₂]Informal description
For any element $a$ of type $\alpha$ and any two lists $l_1$ and $l_2$ of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then $a$ is an element of $l_1$ if and only if $a$ is an element of $l_2$. In other words, $a \in l_1 \leftrightarrow a \in l_2$.
List.Perm.subset
theorem
{l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁ ⊆ l₂
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then $l_1$ is a subset of $l_2$ (i.e., every element of $l_1$ appears in $l_2$).
List.Perm.append_right
theorem
{l₁ l₂ : List α} (t₁ : List α) (p : l₁ ~ l₂) : l₁ ++ t₁ ~ l₂ ++ t₁
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then for any list $t_1$ of elements of type $\alpha$, the concatenation $l_1 \mathbin{+\kern-0.5em+} t_1$ is a permutation of $l_2 \mathbin{+\kern-0.5em+} t_1$ (i.e., $l_1 \mathbin{+\kern-0.5em+} t_1 \sim l_2 \mathbin{+\kern-0.5em+} t_1$).
List.Perm.append_left
theorem
{t₁ t₂ : List α} : ∀ l : List α, t₁ ~ t₂ → l ++ t₁ ~ l ++ t₂
Full source
theorem Perm.append_left {t₁ t₂ : List α} : ∀ l : List α, t₁ ~ t₂ → l ++ t₁ ~ l ++ t₂
| [], p => p
| x :: xs, p => (p.append_left xs).cons xInformal description
For any two lists $t_1$ and $t_2$ of elements of type $\alpha$, if $t_1$ is a permutation of $t_2$ (denoted $t_1 \sim t_2$), then for any list $l$ of elements of type $\alpha$, the concatenation $l \mathbin{+\!\!+} t_1$ is a permutation of $l \mathbin{+\!\!+} t_2$.
List.Perm.append
theorem
{l₁ l₂ t₁ t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : l₁ ++ t₁ ~ l₂ ++ t₂
Full source
theorem Perm.append {l₁ l₂ t₁ t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : l₁ ++ t₁ ~ l₂ ++ t₂ :=
(p₁.append_right t₁).trans (p₂.append_left l₂)Informal description
For any four lists $l_1, l_2, t_1, t_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$) and $t_1$ is a permutation of $t_2$ (denoted $t_1 \sim t_2$), then the concatenation $l_1 \mathbin{+\!\!+} t_1$ is a permutation of $l_2 \mathbin{+\!\!+} t_2$ (i.e., $l_1 \mathbin{+\!\!+} t_1 \sim l_2 \mathbin{+\!\!+} t_2$).
List.Perm.append_cons
theorem
(a : α) {l₁ l₂ r₁ r₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : r₁ ~ r₂) : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂
Full source
theorem Perm.append_cons (a : α) {l₁ l₂ r₁ r₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : r₁ ~ r₂) :
l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ := p₁.append (p₂.cons a)Informal description
For any element $a$ of type $\alpha$ and any four lists $l_1, l_2, r_1, r_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$) and $r_1$ is a permutation of $r_2$ (denoted $r_1 \sim r_2$), then the concatenation $l_1 \mathbin{+\kern-0.5em+} (a :: r_1)$ is a permutation of $l_2 \mathbin{+\kern-0.5em+} (a :: r_2)$.
List.perm_middle
theorem
{a : α} : ∀ {l₁ l₂ : List α}, l₁ ++ a :: l₂ ~ a :: (l₁ ++ l₂)
Full source
@[simp] theorem perm_middle {a : α} : ∀ {l₁ l₂ : List α}, l₁ ++ a :: l₂ ~ a :: (l₁ ++ l₂)
| [], _ => .refl _
| b :: _, _ => (Perm.cons _ perm_middle).trans (swap a b _)Informal description
For any element $a$ of type $\alpha$ and any two lists $l_1, l_2$ of elements of type $\alpha$, the list obtained by appending $l_1$ with $a$ followed by $l_2$ is a permutation of the list obtained by prepending $a$ to the concatenation of $l_1$ and $l_2$. In other words, $l_1 ++ (a :: l_2) \sim a :: (l_1 ++ l_2)$.
List.perm_append_singleton
theorem
(a : α) (l : List α) : l ++ [a] ~ a :: l
Full source
@[simp] theorem perm_append_singleton (a : α) (l : List α) : l ++ [a] ~ a :: l :=
perm_middle.trans <| by rw [append_nil]Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the concatenation of $l$ with the singleton list $[a]$ is a permutation of the list obtained by prepending $a$ to $l$. In other words, $l \mathbin{+\kern-0.5em+} [a] \sim a :: l$.
List.perm_append_comm
theorem
: ∀ {l₁ l₂ : List α}, l₁ ++ l₂ ~ l₂ ++ l₁
Full source
theorem perm_append_comm : ∀ {l₁ l₂ : List α}, l₁ ++ l₂ ~ l₂ ++ l₁
| [], _ => by simp
| _ :: _, _ => (perm_append_comm.cons _).trans perm_middle.symmInformal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the concatenation $l_1 \mathbin{+\kern-0.5em+} l_2$ is a permutation of $l_2 \mathbin{+\kern-0.5em+} l_1$, i.e., $l_1 \mathbin{+\kern-0.5em+} l_2 \sim l_2 \mathbin{+\kern-0.5em+} l_1$.
List.perm_append_comm_assoc
theorem
(l₁ l₂ l₃ : List α) : (l₁ ++ (l₂ ++ l₃)) ~ (l₂ ++ (l₁ ++ l₃))
Full source
theorem perm_append_comm_assoc (l₁ l₂ l₃ : List α) :
(l₁ ++ (l₂ ++ l₃)) ~ (l₂ ++ (l₁ ++ l₃)) := by
simpa only [List.append_assoc] using perm_append_comm.append_right _Informal description
For any three lists $l_1$, $l_2$, and $l_3$ of elements of type $\alpha$, the concatenation $l_1 \mathbin{+\kern-0.5em+} (l_2 \mathbin{+\kern-0.5em+} l_3)$ is a permutation of $l_2 \mathbin{+\kern-0.5em+} (l_1 \mathbin{+\kern-0.5em+} l_3)$, i.e.,
$$(l_1 \mathbin{+\kern-0.5em+} l_2) \mathbin{+\kern-0.5em+} l_3 \sim l_2 \mathbin{+\kern-0.5em+} (l_1 \mathbin{+\kern-0.5em+} l_3).$$
List.concat_perm
theorem
(l : List α) (a : α) : concat l a ~ a :: l
Full source
theorem concat_perm (l : List α) (a : α) : concatconcat l a ~ a :: l := by simpInformal description
For any list $l$ of elements of type $\alpha$ and any element $a$ of type $\alpha$, the list obtained by appending $a$ to the end of $l$ (denoted $\text{concat}(l, a)$) is a permutation of the list obtained by prepending $a$ to $l$ (denoted $a :: l$). In other words, $\text{concat}(l, a) \sim a :: l$.
List.Perm.length_eq
theorem
{l₁ l₂ : List α} (p : l₁ ~ l₂) : length l₁ = length l₂
Full source
theorem Perm.length_eq {l₁ l₂ : List α} (p : l₁ ~ l₂) : length l₁ = length l₂ := by
induction p with
| nil => rfl
| cons _ _ ih => simp only [length_cons, ih]
| swap => rfl
| trans _ _ ih₁ ih₂ => simp only [ih₁, ih₂]Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, if $l₁$ is a permutation of $l₂$ (denoted $l₁ \sim l₂$), then their lengths are equal, i.e., $\text{length}(l₁) = \text{length}(l₂)$.
List.Perm.contains_eq
theorem
[BEq α] {l₁ l₂ : List α} (h : l₁ ~ l₂) {a : α} : l₁.contains a = l₂.contains a
Full source
theorem Perm.contains_eq [BEq α] {l₁ l₂ : List α} (h : l₁ ~ l₂) {a : α} :
l₁.contains a = l₂.contains a := by
induction h with
| nil => rfl
| cons => simp_all
| swap => simp only [contains_cons, ← Bool.or_assoc, Bool.or_comm]
| trans => simp_allInformal description
For any type $\alpha$ with a boolean equality relation, and for any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then for any element $a \in \alpha$, the boolean membership check $a \in l_1$ is equal to $a \in l_2$.
List.Perm.nil_eq
theorem
{l : List α} (p : [] ~ l) : [] = l
Informal description
For any list $l$ of elements of type $\alpha$, if the empty list is a permutation of $l$ (denoted $[] \sim l$), then $l$ must be equal to the empty list (i.e., $l = []$).
List.perm_nil
theorem
{l₁ : List α} : l₁ ~ [] ↔ l₁ = []
Full source
@[simp] theorem perm_nil {l₁ : List α} : l₁ ~ []l₁ ~ [] ↔ l₁ = [] :=
⟨fun p => p.eq_nil, fun e => e ▸ .rfl⟩Informal description
For any list $l_1$ of elements of type $\alpha$, $l_1$ is a permutation of the empty list if and only if $l_1$ is equal to the empty list, i.e., $l_1 \sim [] \leftrightarrow l_1 = []$.
List.nil_perm
theorem
{l₁ : List α} : [] ~ l₁ ↔ l₁ = []
Informal description
For any list $l_1$ of elements of type $\alpha$, the empty list is a permutation of $l_1$ if and only if $l_1$ is equal to the empty list, i.e., $[] \sim l_1 \leftrightarrow l_1 = []$.
List.not_perm_nil_cons
theorem
(x : α) (l : List α) : ¬[] ~ x :: l
Full source
theorem not_perm_nil_cons (x : α) (l : List α) : ¬[] ~ x :: l := (nomatch ·.symm.eq_nil)Informal description
For any element $x$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the empty list is not a permutation of the list obtained by prepending $x$ to $l$ (i.e., $\neg ([] \sim x :: l)$).
List.not_perm_cons_nil
theorem
{l : List α} {a : α} : ¬((a :: l) ~ [])
Full source
theorem not_perm_cons_nil {l : List α} {a : α} : ¬((a::l) ~ []) :=
fun h => by simpa using h.length_eqInformal description
For any list $l$ of elements of type $\alpha$ and any element $a \in \alpha$, the list obtained by prepending $a$ to $l$ (denoted $a :: l$) is not a permutation of the empty list (denoted $[]$). In other words, $\neg (a :: l \sim [])$.
List.Perm.isEmpty_eq
theorem
{l l' : List α} (h : Perm l l') : l.isEmpty = l'.isEmpty
Full source
theorem Perm.isEmpty_eq {l l' : List α} (h : Perm l l') : l.isEmpty = l'.isEmpty := by
cases l <;> cases l' <;> simp_allInformal description
For any two lists $l$ and $l'$ of elements of type $\alpha$, if $l$ is a permutation of $l'$ (denoted $l \sim l'$), then the emptiness check of $l$ is equal to the emptiness check of $l'$, i.e., $\text{isEmpty}(l) = \text{isEmpty}(l')$.
List.reverse_perm
theorem
: ∀ l : List α, reverse l ~ l
Full source
@[simp] theorem reverse_perm : ∀ l : List α, reversereverse l ~ l
| [] => .nil
| a :: l => reverse_cons .. ▸ (perm_append_singleton _ _).trans ((reverse_perm l).cons a)Informal description
For any list $l$ of elements of type $\alpha$, the reverse of $l$ is a permutation of $l$. In other words, $\text{reverse}(l) \sim l$.
List.perm_cons_append_cons
theorem
{l l₁ l₂ : List α} (a : α) (p : l ~ l₁ ++ l₂) : a :: l ~ l₁ ++ a :: l₂
Full source
theorem perm_cons_append_cons {l l₁ l₂ : List α} (a : α) (p : l ~ l₁ ++ l₂) :
a :: la :: l ~ l₁ ++ a :: l₂ := (p.cons a).trans perm_middle.symmInformal description
For any element $a$ of type $\alpha$ and any lists $l, l_1, l_2$ of elements of type $\alpha$, if $l$ is a permutation of $l_1 ++ l_2$ (denoted $l \sim l_1 ++ l_2$), then the list obtained by prepending $a$ to $l$ is a permutation of the list obtained by appending $l_1$ with $a$ followed by $l_2$ (i.e., $a :: l \sim l_1 ++ (a :: l_2)$).
List.perm_replicate
theorem
{n : Nat} {a : α} {l : List α} : l ~ replicate n a ↔ l = replicate n a
Full source
@[simp] theorem perm_replicate {n : Nat} {a : α} {l : List α} :
l ~ replicate n al ~ replicate n a ↔ l = replicate n a := by
refine ⟨fun p => eq_replicate_iff.2 ?_, fun h => h ▸ .rfl⟩
exact ⟨p.length_eq.trans <| length_replicate .., fun _b m => eq_of_mem_replicate <| p.subset m⟩Informal description
For any natural number $n$, any element $a$ of type $\alpha$, and any list $l$ of elements of type $\alpha$, the list $l$ is a permutation of the list $\mathrm{replicate}\,n\,a$ (which contains $n$ copies of $a$) if and only if $l$ is equal to $\mathrm{replicate}\,n\,a$. In other words, the only permutation of a list consisting of $n$ identical elements is the list itself.
List.replicate_perm
theorem
{n : Nat} {a : α} {l : List α} : replicate n a ~ l ↔ replicate n a = l
Full source
@[simp] theorem replicate_perm {n : Nat} {a : α} {l : List α} :
replicatereplicate n a ~ lreplicate n a ~ l ↔ replicate n a = l := (perm_comm.trans perm_replicate).trans eq_commInformal description
For any natural number $n$, any element $a$ of type $\alpha$, and any list $l$ of elements of type $\alpha$, the list $\mathrm{replicate}\,n\,a$ (containing $n$ copies of $a$) is a permutation of $l$ if and only if $\mathrm{replicate}\,n\,a$ is equal to $l$.
List.perm_singleton
theorem
{a : α} {l : List α} : l ~ [a] ↔ l = [a]
Full source
@[simp] theorem perm_singleton {a : α} {l : List α} : l ~ [a]l ~ [a] ↔ l = [a] := perm_replicate (n := 1)Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list $l$ is a permutation of the singleton list $[a]$ if and only if $l$ is equal to $[a]$.
List.singleton_perm
theorem
{a : α} {l : List α} : [a] ~ l ↔ [a] = l
Full source
@[simp] theorem singleton_perm {a : α} {l : List α} : [a][a] ~ l[a] ~ l ↔ [a] = l := replicate_perm (n := 1)Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the singleton list $[a]$ is a permutation of $l$ if and only if $[a] = l$.
List.Perm.singleton_eq
theorem
(h : [a] ~ l) : [a] = l
Full source
theorem Perm.singleton_eq (h : [a][a] ~ l) : [a] = l := singleton_perm.mp hInformal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, if the singleton list $[a]$ is a permutation of $l$, then $[a] = l$.
List.singleton_perm_singleton
theorem
{a b : α} : [a] ~ [b] ↔ a = b
Full source
theorem singleton_perm_singleton {a b : α} : [a][a] ~ [b][a] ~ [b] ↔ a = b := by simpInformal description
For any two elements $a$ and $b$ of type $\alpha$, the singleton list $[a]$ is a permutation of $[b]$ if and only if $a = b$.
List.perm_cons_erase
theorem
[DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : l ~ a :: l.erase a
Full source
theorem perm_cons_erase [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : l ~ a :: l.erase a :=
let ⟨_, _, _, e₁, e₂⟩ := exists_erase_eq h
e₂ ▸ e₁ ▸ perm_middleInformal description
For any type $\alpha$ with decidable equality, any element $a \in \alpha$, and any list $l$ of elements of $\alpha$ containing $a$, the list $l$ is a permutation of the list obtained by prepending $a$ to the result of removing the first occurrence of $a$ from $l$. In other words, $l \sim a :: \text{erase } l a$.
List.Perm.filterMap
theorem
(f : α → Option β) {l₁ l₂ : List α} (p : l₁ ~ l₂) : filterMap f l₁ ~ filterMap f l₂
Full source
theorem Perm.filterMap (f : α → Option β) {l₁ l₂ : List α} (p : l₁ ~ l₂) :
filterMapfilterMap f l₁ ~ filterMap f l₂ := by
induction p with
| nil => simp
| cons x _p IH => cases h : f x <;> simp [h, filterMap_cons, IH, Perm.cons]
| swap x y l₂ => cases hx : f x <;> cases hy : f y <;> simp [hx, hy, filterMap_cons, swap]
| trans _p₁ _p₂ IH₁ IH₂ => exact IH₁.trans IH₂Informal description
For any function $f : \alpha \to \text{Option } \beta$ and any two lists $l_1, l_2 : \text{List } \alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the filtered and mapped lists $\text{filterMap } f l_1$ and $\text{filterMap } f l_2$ are also permutations of each other.
List.Perm.map
theorem
(f : α → β) {l₁ l₂ : List α} (p : l₁ ~ l₂) : map f l₁ ~ map f l₂
Full source
theorem Perm.map (f : α → β) {l₁ l₂ : List α} (p : l₁ ~ l₂) : mapmap f l₁ ~ map f l₂ :=
filterMap_eq_map ▸ p.filterMap _Informal description
For any function $f : \alpha \to \beta$ and any two lists $l_1, l_2 : \text{List } \alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the mapped lists $\text{map } f l_1$ and $\text{map } f l_2$ are also permutations of each other.
List.Perm.pmap
theorem
{p : α → Prop} (f : ∀ a, p a → β) {l₁ l₂ : List α} (p : l₁ ~ l₂) {H₁ H₂} : pmap f l₁ H₁ ~ pmap f l₂ H₂
Full source
theorem Perm.pmap {p : α → Prop} (f : ∀ a, p a → β) {l₁ l₂ : List α} (p : l₁ ~ l₂) {H₁ H₂} :
pmappmap f l₁ H₁ ~ pmap f l₂ H₂ := by
induction p with
| nil => simp
| cons x _p IH => simp [IH, Perm.cons]
| swap x y => simp [swap]
| trans _p₁ p₂ IH₁ IH₂ => exact IH₁.trans (IH₂ (H₁ := fun a m => H₂ a (p₂.subset m)))Informal description
Let $p : \alpha \to \text{Prop}$ be a predicate, and let $f : \forall a, p(a) \to \beta$ be a function that maps elements of $\alpha$ satisfying $p$ to elements of $\beta$. For any two lists $l_1$ and $l_2$ of elements of type $\alpha$ that are permutations of each other (denoted $l_1 \sim l_2$), and for any proofs $H_1$ and $H_2$ that all elements of $l_1$ and $l_2$ respectively satisfy $p$, the mapped lists $\text{pmap}\ f\ l_1\ H_1$ and $\text{pmap}\ f\ l_2\ H_2$ are also permutations of each other.
List.Perm.filter
theorem
(p : α → Bool) {l₁ l₂ : List α} (s : l₁ ~ l₂) : filter p l₁ ~ filter p l₂
Full source
theorem Perm.filter (p : α → Bool) {l₁ l₂ : List α} (s : l₁ ~ l₂) :
filterfilter p l₁ ~ filter p l₂ := by rw [← filterMap_eq_filter]; apply s.filterMapInformal description
For any predicate $p : \alpha \to \text{Bool}$ and any two lists $l_1, l_2 : \text{List } \alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the filtered lists $\text{filter } p l_1$ and $\text{filter } p l_2$ are also permutations of each other.
List.filter_append_perm
theorem
(p : α → Bool) (l : List α) : filter p l ++ filter (fun x => !p x) l ~ l
Full source
theorem filter_append_perm (p : α → Bool) (l : List α) :
filterfilter p l ++ filter (fun x => !p x) l ~ l := by
induction l with
| nil => rfl
| cons x l ih =>
by_cases h : p x <;> simp [h]
· exact ih.cons x
· exact Perm.trans (perm_append_comm.trans (perm_append_comm.cons _)) (ih.cons x)Informal description
For any predicate $p : \alpha \to \text{Bool}$ and any list $l$ of elements of type $\alpha$, the concatenation of the sublist of elements satisfying $p$ and the sublist of elements not satisfying $p$ is a permutation of the original list $l$. That is, $\text{filter}\ p\ l \mathbin{+\kern-0.5em+} \text{filter}\ (\lambda x, \neg p\ x)\ l \sim l$.
List.exists_perm_sublist
theorem
{l₁ l₂ l₂' : List α} (s : l₁ <+ l₂) (p : l₂ ~ l₂') : ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂'
Full source
theorem exists_perm_sublist {l₁ l₂ l₂' : List α} (s : l₁ <+ l₂) (p : l₂ ~ l₂') :
∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂' := by
induction p generalizing l₁ with
| nil => exact ⟨[], sublist_nil.mp s ▸ .rfl, nil_sublist _⟩
| cons x _ IH =>
match s with
| .cons _ s => let ⟨l₁', p', s'⟩ := IH s; exact ⟨l₁', p', s'.cons _⟩
| .cons₂ _ s => let ⟨l₁', p', s'⟩ := IH s; exact ⟨x :: l₁', p'.cons x, s'.cons₂ _⟩
| swap x y l' =>
match s with
| .cons _ (.cons _ s) => exact ⟨_, .rfl, (s.cons _).cons _⟩
| .cons _ (.cons₂ _ s) => exact ⟨x :: _, .rfl, (s.cons _).cons₂ _⟩
| .cons₂ _ (.cons _ s) => exact ⟨y :: _, .rfl, (s.cons₂ _).cons _⟩
| .cons₂ _ (.cons₂ _ s) => exact ⟨x :: y :: _, .swap .., (s.cons₂ _).cons₂ _⟩
| trans _ _ IH₁ IH₂ =>
let ⟨_, pm, sm⟩ := IH₁ s
let ⟨r₁, pr, sr⟩ := IH₂ sm
exact ⟨r₁, pr.trans pm, sr⟩Informal description
For any lists $l₁$, $l₂$, and $l₂'$ of elements of type $\alpha$, if $l₁$ is a sublist of $l₂$ (denoted $l₁ <+ l₂$) and $l₂$ is a permutation of $l₂'$ (denoted $l₂ \sim l₂'$), then there exists a list $l₁'$ such that $l₁'$ is a permutation of $l₁$ and $l₁'$ is a sublist of $l₂'$.
List.Perm.sizeOf_eq_sizeOf
theorem
[SizeOf α] {l₁ l₂ : List α} (h : l₁ ~ l₂) : sizeOf l₁ = sizeOf l₂
Informal description
For any type $\alpha$ equipped with a size function, if two lists $l_1$ and $l_2$ of elements of type $\alpha$ are permutations of each other (denoted $l_1 \sim l_2$), then their sizes are equal, i.e., $\text{sizeOf}(l_1) = \text{sizeOf}(l_2)$.
List.Sublist.exists_perm_append
theorem
{l₁ l₂ : List α} : l₁ <+ l₂ → ∃ l, l₂ ~ l₁ ++ l
Full source
theorem Sublist.exists_perm_append {l₁ l₂ : List α} : l₁ <+ l₂ → ∃ l, l₂ ~ l₁ ++ l
| Sublist.slnil => ⟨nil, .rfl⟩
| Sublist.cons a s =>
let ⟨l, p⟩ := Sublist.exists_perm_append s
⟨a :: l, (p.cons a).trans perm_middle.symm⟩
| Sublist.cons₂ a s =>
let ⟨l, p⟩ := Sublist.exists_perm_append s
⟨l, p.cons a⟩Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then there exists a list $l$ such that $l_2$ is a permutation of the concatenation of $l_1$ and $l$ (i.e., $l_2 \sim l_1 ++ l$).
List.Perm.countP_eq
theorem
(p : α → Bool) {l₁ l₂ : List α} (s : l₁ ~ l₂) : countP p l₁ = countP p l₂
Full source
theorem Perm.countP_eq (p : α → Bool) {l₁ l₂ : List α} (s : l₁ ~ l₂) :
countP p l₁ = countP p l₂ := by
simp only [countP_eq_length_filter]
exact (s.filter _).length_eqInformal description
For any predicate $p : \alpha \to \text{Bool}$ and any two lists $l_1, l_2 : \text{List } \alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the number of elements in $l_1$ satisfying $p$ is equal to the number of elements in $l_2$ satisfying $p$, i.e., $\text{countP}_p(l_1) = \text{countP}_p(l_2)$.
List.Perm.countP_congr
theorem
{l₁ l₂ : List α} (s : l₁ ~ l₂) {p p' : α → Bool} (hp : ∀ x ∈ l₁, p x = p' x) : l₁.countP p = l₂.countP p'
Full source
theorem Perm.countP_congr {l₁ l₂ : List α} (s : l₁ ~ l₂) {p p' : α → Bool}
(hp : ∀ x ∈ l₁, p x = p' x) : l₁.countP p = l₂.countP p' := by
rw [← s.countP_eq p']
clear s
induction l₁ with
| nil => rfl
| cons y s hs =>
simp only [mem_cons, forall_eq_or_imp] at hp
simp only [countP_cons, hs hp.2, hp.1]Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), and for every element $x$ in $l_1$ the predicates $p$ and $p'$ agree (i.e., $p(x) = p'(x)$), then the count of elements in $l_1$ satisfying $p$ is equal to the count of elements in $l_2$ satisfying $p'$. That is,
\[ \text{countP}_p(l_1) = \text{countP}_{p'}(l_2). \]
List.countP_eq_countP_filter_add
theorem
(l : List α) (p q : α → Bool) : l.countP p = (l.filter q).countP p + (l.filter fun a => !q a).countP p
Full source
theorem countP_eq_countP_filter_add (l : List α) (p q : α → Bool) :
l.countP p = (l.filter q).countP p + (l.filter fun a => !q a).countP p :=
countP_append .. ▸ Perm.countP_eq _ (filter_append_perm _ _).symmInformal description
For any list $l$ of elements of type $\alpha$ and any two predicates $p, q : \alpha \to \text{Bool}$, the count of elements in $l$ satisfying $p$ is equal to the sum of the counts of elements satisfying $p$ in the sublists obtained by filtering $l$ with $q$ and its negation $\neg q$. That is,
\[
\text{countP}_p(l) = \text{countP}_p(\text{filter}_q(l)) + \text{countP}_p(\text{filter}_{\neg q}(l)).
\]
List.Perm.count_eq
theorem
[DecidableEq α] {l₁ l₂ : List α} (p : l₁ ~ l₂) (a) : count a l₁ = count a l₂
Full source
theorem Perm.count_eq [DecidableEq α] {l₁ l₂ : List α} (p : l₁ ~ l₂) (a) :
count a l₁ = count a l₂ := p.countP_eq _Informal description
For any type $\alpha$ with decidable equality, if two lists $l_1$ and $l_2$ are permutations of each other (denoted $l_1 \sim l_2$), then for any element $a \in \alpha$, the count of $a$ in $l_1$ is equal to its count in $l_2$, i.e., $\text{count}(a, l_1) = \text{count}(a, l_2)$.
List.Perm.foldl_eq'
theorem
{f : β → α → β} {l₁ l₂ : List α} (p : l₁ ~ l₂) (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f (f z x) y = f (f z y) x) (init) :
foldl f init l₁ = foldl f init l₂
Full source
theorem Perm.foldl_eq' {f : β → α → β} {l₁ l₂ : List α} (p : l₁ ~ l₂)
(comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f (f z x) y = f (f z y) x)
(init) : foldl f init l₁ = foldl f init l₂ := by
induction p using recOnSwap' generalizing init with
| nil => simp
| cons x _p IH =>
simp only [foldl]
apply IH; intros; apply comm <;> exact .tail _ ‹_›
| swap' x y _p IH =>
simp only [foldl]
rw [comm x (.tail _ <| .head _) y (.head _)]
apply IH; intros; apply comm <;> exact .tail _ (.tail _ ‹_›)
| trans p₁ _p₂ IH₁ IH₂ =>
refine (IH₁ comm init).trans (IH₂ ?_ _)
intros; apply comm <;> apply p₁.symm.subset <;> assumptionInformal description
Let $f : \beta \to \alpha \to \beta$ be a binary operation, and let $l_1$ and $l_2$ be two lists of elements of type $\alpha$ such that $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$). If $f$ satisfies the commutativity-like condition that for all $x, y \in l_1$ and for all $z \in \beta$, $f(f(z, x), y) = f(f(z, y), x)$, then for any initial value $\text{init} \in \beta$, the left fold of $f$ over $l_1$ with initial value $\text{init}$ is equal to the left fold of $f$ over $l_2$ with the same initial value, i.e.,
$$\text{foldl}\ f\ \text{init}\ l_1 = \text{foldl}\ f\ \text{init}\ l_2.$$
List.Perm.foldr_eq'
theorem
{f : α → β → β} {l₁ l₂ : List α} (p : l₁ ~ l₂) (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f y (f x z) = f x (f y z)) (init) :
foldr f init l₁ = foldr f init l₂
Full source
theorem Perm.foldr_eq' {f : α → β → β} {l₁ l₂ : List α} (p : l₁ ~ l₂)
(comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f y (f x z) = f x (f y z))
(init) : foldr f init l₁ = foldr f init l₂ := by
induction p using recOnSwap' generalizing init with
| nil => simp
| cons x _p IH =>
simp only [foldr]
congr 1
apply IH; intros; apply comm <;> exact .tail _ ‹_›
| swap' x y _p IH =>
simp only [foldr]
rw [comm x (.tail _ <| .head _) y (.head _)]
congr 2
apply IH; intros; apply comm <;> exact .tail _ (.tail _ ‹_›)
| trans p₁ _p₂ IH₁ IH₂ =>
refine (IH₁ comm init).trans (IH₂ ?_ _)
intros; apply comm <;> apply p₁.symm.subset <;> assumptionInformal description
For any binary function $f : \alpha \to \beta \to \beta$, lists $l_1$ and $l_2$ of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$) and $f$ satisfies the commutativity condition that for all $x, y \in l_1$ and any $z \in \beta$, $f y (f x z) = f x (f y z)$, then the right folds of $f$ over $l_1$ and $l_2$ with initial value $\text{init}$ are equal, i.e., $\text{foldr } f \text{ init } l_1 = \text{foldr } f \text{ init } l_2$.
List.Perm.rec_heq
theorem
{β : List α → Sort _} {f : ∀ a l, β l → β (a :: l)} {b : β []} {l l' : List α} (hl : l ~ l')
(f_congr : ∀ {a l l' b b'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b'))
(f_swap : ∀ {a a' l b}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))) :
HEq (@List.rec α β b f l) (@List.rec α β b f l')
Full source
theorem Perm.rec_heq {β : List α → Sort _} {f : ∀ a l, β l → β (a :: l)} {b : β []} {l l' : List α}
(hl : l ~ l') (f_congr : ∀ {a l l' b b'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b'))
(f_swap : ∀ {a a' l b}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))) :
HEq (@List.rec α β b f l) (@List.rec α β b f l') := by
induction hl with
| nil => rfl
| cons a h ih => exact f_congr h ih
| swap a a' l => exact f_swap
| trans _h₁ _h₂ ih₁ ih₂ => exact ih₁.trans ih₂Informal description
Let $\beta$ be a type-valued function on lists of type $\alpha$, and let $f$ be a function that for any element $a : \alpha$ and list $l : \text{List } \alpha$, maps $\beta(l)$ to $\beta(a :: l)$. Given a base case $b : \beta([])$ and two lists $l, l' : \text{List } \alpha$ that are permutations of each other ($l \sim l'$), if:
1. $f$ respects permutation equivalence (i.e., for any $a$, lists $l \sim l'$, and $b \approx b'$, we have $f(a, l, b) \approx f(a, l', b')$), and
2. $f$ satisfies a swap condition (i.e., for any $a, a'$ and $l$, $f(a, a' :: l, f(a', l, b)) \approx f(a', a :: l, f(a, l, b))$),
then the two list recursions $\text{List.rec } \beta \, b \, f \, l$ and $\text{List.rec } \beta \, b \, f \, l'$ are heterogeneously equal.
List.perm_inv_core
theorem
{a : α} {l₁ l₂ r₁ r₂ : List α} : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂ ++ r₂
Full source
/-- Lemma used to destruct perms element by element. -/
theorem perm_inv_core {a : α} {l₁ l₂ r₁ r₂ : List α} :
l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂ ++ r₂ := by
-- Necessary generalization for `induction`
suffices ∀ s₁ s₂ (_ : s₁ ~ s₂) {l₁ l₂ r₁ r₂},
l₁ ++ a :: r₁ = s₁ → l₂ ++ a :: r₂ = s₂ → l₁ ++ r₁ ~ l₂ ++ r₂ from (this _ _ · rfl rfl)
intro s₁ s₂ p
induction p using Perm.recOnSwap' with intro l₁ l₂ r₁ r₂ e₁ e₂
| nil =>
simp at e₁
| cons x p IH =>
cases l₁ <;> cases l₂ <;>
dsimp at e₁ e₂ <;> injections <;> subst_vars
· exact p
· exact p.trans perm_middle
· exact perm_middle.symm.trans p
· exact (IH rfl rfl).cons _
| swap' x y p IH =>
obtain _ | ⟨y, _ | ⟨z, l₁⟩⟩ := l₁
<;> obtain _ | ⟨u, _ | ⟨v, l₂⟩⟩ := l₂
<;> dsimp at e₁ e₂ <;> injections <;> subst_vars
<;> try exact p.cons _
· exact (p.trans perm_middle).cons u
· exact ((p.trans perm_middle).cons _).trans (swap _ _ _)
· exact (perm_middle.symm.trans p).cons y
· exact (swap _ _ _).trans ((perm_middle.symm.trans p).cons u)
· exact (IH rfl rfl).swap' _ _
| trans p₁ p₂ IH₁ IH₂ =>
subst e₁ e₂
obtain ⟨l₂, r₂, rfl⟩ := append_of_mem (a := a) (p₁.subset (by simp))
exact (IH₁ rfl rfl).trans (IH₂ rfl rfl)Informal description
For any element $a$ of type $\alpha$ and any four lists $l_1, l_2, r_1, r_2$ of type $\alpha$, if the concatenated lists $l_1 ++ (a :: r_1)$ and $l_2 ++ (a :: r_2)$ are permutations of each other (denoted $l_1 ++ (a :: r_1) \sim l_2 ++ (a :: r_2)$), then the concatenated lists $l_1 ++ r_1$ and $l_2 ++ r_2$ are also permutations of each other ($l_1 ++ r_1 \sim l_2 ++ r_2$).
List.Perm.cons_inv
theorem
{a : α} {l₁ l₂ : List α} : a :: l₁ ~ a :: l₂ → l₁ ~ l₂
Full source
theorem Perm.cons_inv {a : α} {l₁ l₂ : List α} : a :: l₁a :: l₁ ~ a :: l₂ → l₁ ~ l₂ :=
perm_inv_core (l₁ := []) (l₂ := [])Informal description
For any element $a$ of type $\alpha$ and any two lists $l_1, l_2$ of type $\alpha$, if the lists $a :: l_1$ and $a :: l_2$ are permutations of each other (denoted $a :: l_1 \sim a :: l_2$), then $l_1$ and $l_2$ are also permutations of each other ($l_1 \sim l_2$).
List.perm_cons
theorem
(a : α) {l₁ l₂ : List α} : a :: l₁ ~ a :: l₂ ↔ l₁ ~ l₂
Full source
@[simp] theorem perm_cons (a : α) {l₁ l₂ : List α} : a :: l₁a :: l₁ ~ a :: l₂a :: l₁ ~ a :: l₂ ↔ l₁ ~ l₂ :=
⟨.cons_inv, .cons a⟩Informal description
For any element $a$ of type $\alpha$ and any two lists $l_1, l_2$ of type $\alpha$, the lists $a :: l_1$ and $a :: l_2$ are permutations of each other (denoted $a :: l_1 \sim a :: l_2$) if and only if $l_1$ and $l_2$ are permutations of each other ($l_1 \sim l_2$).
List.perm_append_left_iff
theorem
{l₁ l₂ : List α} : ∀ l, l ++ l₁ ~ l ++ l₂ ↔ l₁ ~ l₂
Full source
theorem perm_append_left_iff {l₁ l₂ : List α} : ∀ l, l ++ l₁ ~ l ++ l₂l ++ l₁ ~ l ++ l₂ ↔ l₁ ~ l₂
| [] => .rfl
| a :: l => (perm_cons a).trans (perm_append_left_iff l)Informal description
For any two lists $l_1$ and $l_2$ of type $\alpha$, and for any list $l$ of type $\alpha$, the concatenated lists $l \mathbin{+\kern-0.5em+} l_1$ and $l \mathbin{+\kern-0.5em+} l_2$ are permutations of each other (denoted $l \mathbin{+\kern-0.5em+} l_1 \sim l \mathbin{+\kern-0.5em+} l_2$) if and only if $l_1$ and $l_2$ are permutations of each other ($l_1 \sim l_2$).
List.perm_append_right_iff
theorem
{l₁ l₂ : List α} (l) : l₁ ++ l ~ l₂ ++ l ↔ l₁ ~ l₂
Full source
theorem perm_append_right_iff {l₁ l₂ : List α} (l) : l₁ ++ l ~ l₂ ++ ll₁ ++ l ~ l₂ ++ l ↔ l₁ ~ l₂ := by
refine ⟨fun p => ?_, .append_right _⟩
exact (perm_append_left_iff _).1 <| perm_append_comm.trans <| p.trans perm_append_commInformal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, and for any list $l$ of type $\alpha$, the concatenated lists $l_1 \mathbin{+\kern-0.5em+} l$ and $l_2 \mathbin{+\kern-0.5em+} l$ are permutations of each other (denoted $l_1 \mathbin{+\kern-0.5em+} l \sim l_2 \mathbin{+\kern-0.5em+} l$) if and only if $l_1$ and $l_2$ are permutations of each other ($l_1 \sim l_2$).
List.Perm.erase
theorem
(a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁.erase a ~ l₂.erase a
Full source
theorem Perm.erase (a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁.erase a ~ l₂.erase a :=
if h₁ : a ∈ l₁ then
have h₂ : a ∈ l₂ := p.subset h₁
.cons_inv <| (perm_cons_erase h₁).symm.trans <| p.trans (perm_cons_erase h₂)
else by
have h₂ : a ∉ l₂ := mt p.mem_iff.2 h₁
rw [erase_of_not_mem h₁, erase_of_not_mem h₂]; exact pInformal description
For any element $a$ of type $\alpha$ and any two lists $l_1$ and $l_2$ of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the lists obtained by removing the first occurrence of $a$ from $l_1$ and $l_2$ are also permutations of each other, i.e., $\text{erase } l_1 a \sim \text{erase } l_2 a$.
List.cons_perm_iff_perm_erase
theorem
{a : α} {l₁ l₂ : List α} : a :: l₁ ~ l₂ ↔ a ∈ l₂ ∧ l₁ ~ l₂.erase a
Full source
theorem cons_perm_iff_perm_erase {a : α} {l₁ l₂ : List α} :
a :: l₁a :: l₁ ~ l₂a :: l₁ ~ l₂ ↔ a ∈ l₂ ∧ l₁ ~ l₂.erase a := by
refine ⟨fun h => ?_, fun ⟨m, h⟩ => (h.cons a).trans (perm_cons_erase m).symm⟩
have : a ∈ l₂ := h.subset mem_cons_self
exact ⟨this, (h.trans <| perm_cons_erase this).cons_inv⟩Informal description
For any element $a$ of type $\alpha$ and any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the list $a :: l_1$ is a permutation of $l_2$ if and only if $a$ is an element of $l_2$ and $l_1$ is a permutation of the list obtained by removing the first occurrence of $a$ from $l_2$. In other words:
$$ a :: l_1 \sim l_2 \leftrightarrow a \in l_2 \land l_1 \sim \text{erase } l_2 a $$
List.perm_iff_count
theorem
{l₁ l₂ : List α} : l₁ ~ l₂ ↔ ∀ a, count a l₁ = count a l₂
Full source
theorem perm_iff_count {l₁ l₂ : List α} : l₁ ~ l₂l₁ ~ l₂ ↔ ∀ a, count a l₁ = count a l₂ := by
refine ⟨Perm.count_eq, fun H => ?_⟩
induction l₁ generalizing l₂ with
| nil =>
match l₂ with
| nil => rfl
| cons b l₂ =>
specialize H b
simp at H
| cons a l₁ IH =>
have : a ∈ l₂ := count_pos_iff.mp (by rw [← H]; simp)
refine ((IH fun b => ?_).cons a).trans (perm_cons_erase this).symm
specialize H b
rw [(perm_cons_erase this).count_eq] at H
by_cases h : b = a <;> simpa [h, count_cons, Nat.succ_inj'] using HInformal description
Two lists $l_1$ and $l_2$ of elements of type $\alpha$ are permutations of each other (denoted $l_1 \sim l_2$) if and only if for every element $a \in \alpha$, the count of $a$ in $l_1$ equals its count in $l_2$.
List.isPerm_iff
theorem
: ∀ {l₁ l₂ : List α}, l₁.isPerm l₂ ↔ l₁ ~ l₂
Full source
theorem isPerm_iff : ∀ {l₁ l₂ : List α}, l₁.isPerm l₂ ↔ l₁ ~ l₂
| [], [] => by simp [isPerm, isEmpty]
| [], _ :: _ => by simp [isPerm, isEmpty, Perm.nil_eq]
| a :: l₁, l₂ => by simp [isPerm, isPerm_iff, cons_perm_iff_perm_erase]Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the boolean function `isPerm` returns `true` if and only if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), meaning they contain the same elements with the same multiplicities but possibly in different orders.
List.decidablePerm
instance
(l₁ l₂ : List α) : Decidable (l₁ ~ l₂)
Full source
instance decidablePerm (l₁ l₂ : List α) : Decidable (l₁ ~ l₂) := decidable_of_iff _ isPerm_iffInformal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the proposition that $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$) is decidable. This means there is an algorithm that can determine whether $l_1$ and $l_2$ contain the same elements with the same multiplicities, regardless of order.
List.Perm.insert
theorem
(a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁.insert a ~ l₂.insert a
Informal description
For any element $a$ of type $\alpha$ and any two lists $l_1$ and $l_2$ of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then inserting $a$ into $l_1$ yields a permutation of inserting $a$ into $l_2$ (i.e., $l_1.\text{insert}(a) \sim l_2.\text{insert}(a)$).
List.perm_insert_swap
theorem
(x y : α) (l : List α) : List.insert x (List.insert y l) ~ List.insert y (List.insert x l)
Full source
theorem perm_insert_swap (x y : α) (l : List α) :
List.insertList.insert x (List.insert y l) ~ List.insert y (List.insert x l) := by
by_cases xl : x ∈ l <;> by_cases yl : y ∈ l <;> simp [xl, yl]
if xy : x = y then simp [xy] else
simp [List.insert, xl, yl, xy, Ne.symm xy]
constructorInformal description
For any elements $x$ and $y$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list obtained by first inserting $x$ and then inserting $y$ into $l$ is a permutation of the list obtained by first inserting $y$ and then inserting $x$ into $l$. That is, $\text{insert}(x, \text{insert}(y, l)) \sim \text{insert}(y, \text{insert}(x, l))$, where $\sim$ denotes the permutation relation.
List.Perm.pairwise_iff
theorem
{R : α → α → Prop} (S : ∀ {x y}, R x y → R y x) : ∀ {l₁ l₂ : List α} (_p : l₁ ~ l₂), Pairwise R l₁ ↔ Pairwise R l₂
Full source
theorem Perm.pairwise_iff {R : α → α → Prop} (S : ∀ {x y}, R x y → R y x) :
∀ {l₁ l₂ : List α} (_p : l₁ ~ l₂), PairwisePairwise R l₁ ↔ Pairwise R l₂ :=
suffices ∀ {l₁ l₂}, l₁ ~ l₂ → Pairwise R l₁ → Pairwise R l₂
from fun p => ⟨this p, this p.symm⟩
fun {l₁ l₂} p d => by
induction d generalizing l₂ with
| nil => rw [← p.nil_eq]; constructor
| cons h _ IH =>
have : _ ∈ l₂ := p.subset mem_cons_self
obtain ⟨s₂, t₂, rfl⟩ := append_of_mem this
have p' := (p.trans perm_middle).cons_inv
refine (pairwise_middle S).2 (pairwise_cons.2 ⟨fun b m => ?_, IH p'⟩)
exact h _ (p'.symm.subset m)Informal description
For any symmetric relation $R$ on a type $\alpha$ (i.e., $R(x,y) \implies R(y,x)$ for all $x,y \in \alpha$), and for any two lists $l_1$ and $l_2$ of elements of type $\alpha$ that are permutations of each other ($l_1 \sim l_2$), the pairwise relation $R$ holds for $l_1$ if and only if it holds for $l_2$.
In other words, if $R$ is symmetric, then the property of being $R$-pairwise is invariant under list permutations.
List.Pairwise.perm
theorem
{R : α → α → Prop} {l l' : List α} (hR : l.Pairwise R) (hl : l ~ l') (hsymm : ∀ {x y}, R x y → R y x) : l'.Pairwise R
Full source
theorem Pairwise.perm {R : α → α → Prop} {l l' : List α} (hR : l.Pairwise R) (hl : l ~ l')
(hsymm : ∀ {x y}, R x y → R y x) : l'.Pairwise R := (hl.pairwise_iff hsymm).mp hRInformal description
For any symmetric relation $R$ on a type $\alpha$ (i.e., $R(x,y) \implies R(y,x)$ for all $x,y \in \alpha$), if a list $l$ satisfies the pairwise relation $R$ and $l$ is a permutation of another list $l'$ (denoted $l \sim l'$), then $l'$ also satisfies the pairwise relation $R$.
List.Perm.pairwise
theorem
{R : α → α → Prop} {l l' : List α} (hl : l ~ l') (hR : l.Pairwise R) (hsymm : ∀ {x y}, R x y → R y x) : l'.Pairwise R
Informal description
Let $R$ be a symmetric relation on a type $\alpha$ (i.e., $R(x,y) \implies R(y,x)$ for all $x,y \in \alpha$). If two lists $l$ and $l'$ of elements of type $\alpha$ are permutations of each other (denoted $l \sim l'$) and $l$ satisfies the pairwise relation $R$, then $l'$ also satisfies the pairwise relation $R$.
List.Nodup.perm
theorem
{l l' : List α} (hR : l.Nodup) (hl : l ~ l') : l'.Nodup
Full source
theorem Nodup.perm {l l' : List α} (hR : l.Nodup) (hl : l ~ l') : l'.Nodup :=
Pairwise.perm hR hl (by intro x y h h'; simp_all)Informal description
For any two lists $l$ and $l'$ of elements of type $\alpha$, if $l$ has no duplicate elements and $l$ is a permutation of $l'$ (denoted $l \sim l'$), then $l'$ also has no duplicate elements.
List.Perm.nodup
theorem
{l l' : List α} (hl : l ~ l') (hR : l.Nodup) : l'.Nodup
Informal description
For any two lists $l$ and $l'$ of elements of type $\alpha$, if $l$ is a permutation of $l'$ (denoted $l \sim l'$) and $l$ has no duplicate elements, then $l'$ also has no duplicate elements.
List.Perm.nodup_iff
theorem
{l₁ l₂ : List α} : l₁ ~ l₂ → (Nodup l₁ ↔ Nodup l₂)
Full source
theorem Perm.nodup_iff {l₁ l₂ : List α} : l₁ ~ l₂ → (NodupNodup l₁ ↔ Nodup l₂) :=
Perm.pairwise_iff <| @Ne.symm αInformal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then $l_1$ has no duplicate elements if and only if $l_2$ has no duplicate elements.
List.Perm.flatten
theorem
{l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatten ~ l₂.flatten
Full source
theorem Perm.flatten {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatten ~ l₂.flatten := by
induction h with
| nil => rfl
| cons _ _ ih => simp only [flatten_cons, perm_append_left_iff, ih]
| swap => simp only [flatten_cons, ← append_assoc, perm_append_right_iff]; exact perm_append_comm ..
| trans _ _ ih₁ ih₂ => exact trans ih₁ ih₂Informal description
For any two lists of lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the concatenation of all inner lists in $l_1$ is a permutation of the concatenation of all inner lists in $l_2$, i.e., $\text{flatten}(l_1) \sim \text{flatten}(l_2)$.
List.Perm.join
abbrev
Full source
@[deprecated Perm.flatten (since := "2024-10-14")] abbrev Perm.join := @Perm.flattenInformal description
Given two lists of lists `l₁` and `l₂` of elements of type `α`, if `l₁` is a permutation of `l₂` (denoted `l₁ ~ l₂`), then the concatenation of all inner lists in `l₁` is a permutation of the concatenation of all inner lists in `l₂`, i.e., `join(l₁) ~ join(l₂)`.
List.cons_append_cons_perm
theorem
{a b : α} {as bs : List α} : a :: as ++ b :: bs ~ b :: as ++ a :: bs
Full source
theorem cons_append_cons_perm {a b : α} {as bs : List α} :
a :: asa :: as ++ b :: bs ~ b :: as ++ a :: bs := by
suffices [[a], as, [b], bs][[a], as, [b], bs].flatten ~ [[b], as, [a], bs].flatten by simpa
apply Perm.flatten
calc
[[a], as, [b], bs] ~ [as, [a], [b], bs] := Perm.swap as [a] _
_ ~ [as, [b], [a], bs]calc
[[a], as, [b], bs] ~ [as, [a], [b], bs] := Perm.swap as [a] _
_ ~ [as, [b], [a], bs] := Perm.cons _ (Perm.swap [b] [a] _)
_ ~ [[b], as, [a], bs] := Perm.swap [b] as _Informal description
For any elements $a, b$ of type $\alpha$ and any lists $as, bs$ of type $\alpha$, the list $a :: as \mathbin{+\kern-0.5em+} b :: bs$ is a permutation of the list $b :: as \mathbin{+\kern-0.5em+} a :: bs$, where $\mathbin{+\kern-0.5em+}$ denotes list concatenation and $::$ denotes list cons operation.
List.Perm.flatMap_right
theorem
{l₁ l₂ : List α} (f : α → List β) (p : l₁ ~ l₂) : l₁.flatMap f ~ l₂.flatMap f
Full source
theorem Perm.flatMap_right {l₁ l₂ : List α} (f : α → List β) (p : l₁ ~ l₂) : l₁.flatMap f ~ l₂.flatMap f :=
(p.map _).flattenInformal description
For any two lists $l_1$ and $l_2$ of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), and for any function $f : \alpha \to \text{List}\ \beta$, then the flatMap of $f$ over $l_1$ is a permutation of the flatMap of $f$ over $l_2$, i.e., $\text{flatMap}\ f\ l_1 \sim \text{flatMap}\ f\ l_2$.
List.Perm.bind_right
abbrev
Full source
@[deprecated Perm.flatMap_right (since := "2024-10-16")] abbrev Perm.bind_right := @Perm.flatMap_rightInformal description
For any two lists $l_1$ and $l_2$ of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), and for any function $f : \alpha \to \text{List}\ \beta$, then the list obtained by applying `flatMap` (or equivalently, monadic bind) of $f$ over $l_1$ is a permutation of the list obtained by applying `flatMap` of $f$ over $l_2$, i.e., $\text{flatMap}\ f\ l_1 \sim \text{flatMap}\ f\ l_2$.
List.Perm.eraseP
theorem
(f : α → Bool) {l₁ l₂ : List α} (H : Pairwise (fun a b => f a → f b → False) l₁) (p : l₁ ~ l₂) :
eraseP f l₁ ~ eraseP f l₂
Full source
theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
(H : Pairwise (fun a b => f a → f b → False) l₁) (p : l₁ ~ l₂) : erasePeraseP f l₁ ~ eraseP f l₂ := by
induction p with
| nil => simp
| cons a p IH =>
if h : f a then simp [h, p]
else simp [h]; exact IH (pairwise_cons.1 H).2
| swap a b l =>
by_cases h₁ : f a <;> by_cases h₂ : f b <;> simp [h₁, h₂]
· cases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) h₂ h₁
· apply swap
| trans p₁ _ IH₁ IH₂ =>
refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))
exact fun h h₁ h₂ => h h₂ h₁Informal description
Let $f : \alpha \to \text{Bool}$ be a predicate and $l_1, l_2$ be two lists of elements of type $\alpha$. If $l_1$ is pairwise such that for any two distinct elements $a, b \in l_1$, if $f(a)$ and $f(b)$ both hold, then we have a contradiction, and if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the lists obtained by removing the first element satisfying $f$ from $l_1$ and $l_2$ respectively are also permutations of each other, i.e., $\text{eraseP}\,f\,l_1 \sim \text{eraseP}\,f\,l_2$.
List.perm_insertIdx
theorem
{α} (x : α) (l : List α) {i} (h : i ≤ l.length) : l.insertIdx i x ~ x :: l
Full source
theorem perm_insertIdx {α} (x : α) (l : List α) {i} (h : i ≤ l.length) :
l.insertIdx i x ~ x :: l := by
induction l generalizing i with
| nil =>
cases i with
| zero => rfl
| succ => cases h
| cons _ _ ih =>
cases i with
| zero => simp [insertIdx]
| succ =>
simp only [insertIdx, modifyTailIdx]
refine .trans (.cons _ (ih (Nat.le_of_succ_le_succ h))) (.swap ..)Informal description
For any element $x$ of type $\alpha$, any list $l$ of elements of type $\alpha$, and any natural number index $i$ such that $i \leq \text{length}(l)$, the list obtained by inserting $x$ at position $i$ in $l$ is a permutation of the list $x :: l$ (i.e., the list formed by prepending $x$ to $l$).