Module docstring
{"# List Permutations
This file develops theory about the List.Perm relation.
Notation
The notation ~ is used for permutation equivalence.
"}
List.perm_rfl
theorem
: l ~ l
Informal description
For any list $l$, the permutation relation holds between $l$ and itself, i.e., $l \sim l$.
List.instIsSymmPerm
instance
: IsSymm (List α) Perm
Full source
instance : IsSymm (List α) Perm := ⟨fun _ _ ↦ .symm⟩Informal description
For any type $\alpha$, the permutation relation `~` on lists of type $\alpha$ is symmetric. That is, for any two lists $l_1$ and $l_2$, if $l_1 ~ l_2$, then $l_2 ~ l_1$.
List.Perm.subset_congr_left
theorem
{l₁ l₂ l₃ : List α} (h : l₁ ~ l₂) : l₁ ⊆ l₃ ↔ l₂ ⊆ l₃
Full source
theorem Perm.subset_congr_left {l₁ l₂ l₃ : List α} (h : l₁ ~ l₂) : l₁ ⊆ l₃l₁ ⊆ l₃ ↔ l₂ ⊆ l₃ :=
⟨h.symm.subset.trans, h.subset.trans⟩Informal description
For any lists $l_1$, $l_2$, and $l_3$ 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_3$ if and only if $l_2$ is a subset of $l_3$.
List.Perm.subset_congr_right
theorem
{l₁ l₂ l₃ : List α} (h : l₁ ~ l₂) : l₃ ⊆ l₁ ↔ l₃ ⊆ l₂
Full source
theorem Perm.subset_congr_right {l₁ l₂ l₃ : List α} (h : l₁ ~ l₂) : l₃ ⊆ l₁l₃ ⊆ l₁ ↔ l₃ ⊆ l₂ :=
⟨fun h' => h'.trans h.subset, fun h' => h'.trans h.symm.subset⟩Informal description
For any lists $l_1$, $l_2$, and $l_3$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then $l_3$ is a subset of $l_1$ if and only if $l_3$ is a subset of $l_2$.
List.set_perm_cons_eraseIdx
theorem
{n : ℕ} (h : n < l.length) (a : α) : l.set n a ~ a :: l.eraseIdx n
Full source
theorem set_perm_cons_eraseIdx {n : ℕ} (h : n < l.length) (a : α) :
l.set n a ~ a :: l.eraseIdx n := by
rw [← insertIdx_eraseIdx h.ne]
apply perm_insertIdx
rw [length_eraseIdx_of_lt h]
exact Nat.le_sub_one_of_lt hInformal description
For any list $l$ of elements of type $\alpha$, natural number $n$ such that $n < \text{length}(l)$, and element $a \in \alpha$, the list obtained by setting the $n$-th element of $l$ to $a$ is a permutation of the list obtained by prepending $a$ to the list where the $n$-th element of $l$ has been removed. In other words:
\[ l[n \mapsto a] \sim a :: l \setminus \{l[n]\} \]
where $\sim$ denotes permutation equivalence, $l[n \mapsto a]$ denotes the list with the $n$-th element set to $a$, and $l \setminus \{l[n]\}$ denotes the list with the $n$-th element removed.
List.getElem_cons_eraseIdx_perm
theorem
{n : ℕ} (h : n < l.length) : l[n] :: l.eraseIdx n ~ l
Full source
theorem getElem_cons_eraseIdx_perm {n : ℕ} (h : n < l.length) :
l[n]l[n] :: l.eraseIdx nl[n] :: l.eraseIdx n ~ l := by
simpa [h] using (set_perm_cons_eraseIdx h l[n]).symmInformal description
For any list $l$ of elements of type $\alpha$ and natural number $n$ such that $n < \text{length}(l)$, the list obtained by prepending the $n$-th element of $l$ to the list where the $n$-th element has been removed is a permutation of the original list $l$. In other words:
\[ l[n] :: l \setminus \{l[n]\} \sim l \]
where $\sim$ denotes permutation equivalence, $l[n]$ denotes the $n$-th element of $l$, and $l \setminus \{l[n]\}$ denotes the list with the $n$-th element removed.
List.perm_insertIdx_iff_of_le
theorem
{l₁ l₂ : List α} {m n : ℕ} (hm : m ≤ l₁.length) (hn : n ≤ l₂.length) (a : α) :
l₁.insertIdx m a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
Full source
theorem perm_insertIdx_iff_of_le {l₁ l₂ : List α} {m n : ℕ} (hm : m ≤ l₁.length)
(hn : n ≤ l₂.length) (a : α) : l₁.insertIdx m a ~ l₂.insertIdx n al₁.insertIdx m a ~ l₂.insertIdx n a ↔ l₁ ~ l₂ := by
rw [rel_congr_left (perm_insertIdx _ _ hm), rel_congr_right (perm_insertIdx _ _ hn), perm_cons]Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, natural numbers $m$ and $n$ such that $m \leq \text{length}(l_1)$ and $n \leq \text{length}(l_2)$, and an element $a \in \alpha$, the following equivalence holds:
\[ l_1.\text{insertIdx}(m, a) \sim l_2.\text{insertIdx}(n, a) \quad \text{if and only if} \quad l_1 \sim l_2. \]
Here, $\sim$ denotes the permutation relation, and $\text{insertIdx}(k, x)$ denotes the list obtained by inserting $x$ at position $k$ in the list.
List.perm_insertIdx_iff
theorem
{l₁ l₂ : List α} {n : ℕ} {a : α} : l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
Full source
@[simp]
theorem perm_insertIdx_iff {l₁ l₂ : List α} {n : ℕ} {a : α} :
l₁.insertIdx n a ~ l₂.insertIdx n al₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂ := by
wlog hle : length l₁ ≤ length l₂ generalizing l₁ l₂
· rw [perm_comm, this (le_of_not_le hle), perm_comm]
cases Nat.lt_or_ge (length l₁) n with
| inl hn₁ =>
rw [insertIdx_of_length_lt hn₁]
cases Nat.lt_or_ge (length l₂) n with
| inl hn₂ => rw [insertIdx_of_length_lt hn₂]
| inr hn₂ =>
apply iff_of_false
· intro h
rw [h.length_eq] at hn₁
exact (hn₁.trans_le hn₂).not_le (length_le_length_insertIdx ..)
· exact fun h ↦ (hn₁.trans_le hn₂).not_le h.length_eq.ge
| inr hn₁ =>
exact perm_insertIdx_iff_of_le hn₁ (le_trans hn₁ hle) _Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, a natural number $n$, and an element $a \in \alpha$, the following equivalence holds:
\[ l_1.\text{insertIdx}(n, a) \sim l_2.\text{insertIdx}(n, a) \quad \text{if and only if} \quad l_1 \sim l_2. \]
Here, $\sim$ denotes the permutation relation, and $\text{insertIdx}(k, x)$ denotes the list obtained by inserting $x$ at position $k$ in the list.
List.Perm.insertIdx
theorem
{l₁ l₂ : List α} (h : l₁ ~ l₂) (n : ℕ) (a : α) : l₁.insertIdx n a ~ l₂.insertIdx n a
Full source
@[gcongr]
protected theorem Perm.insertIdx {l₁ l₂ : List α} (h : l₁ ~ l₂) (n : ℕ) (a : α) :
l₁.insertIdx n a ~ l₂.insertIdx n a :=
perm_insertIdx_iff.mpr hInformal description
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$), any natural number $n$, and any element $a \in \alpha$, the lists obtained by inserting $a$ at position $n$ in both $l_1$ and $l_2$ remain permutations of each other. That is, $l_1.\text{insertIdx}(n, a) \sim l_2.\text{insertIdx}(n, a)$.
List.perm_eraseIdx_of_getElem?_eq
theorem
{l₁ l₂ : List α} {m n : ℕ} (h : l₁[m]? = l₂[n]?) : eraseIdx l₁ m ~ eraseIdx l₂ n ↔ l₁ ~ l₂
Full source
theorem perm_eraseIdx_of_getElem?_eq {l₁ l₂ : List α} {m n : ℕ} (h : l₁[m]? = l₂[n]?) :
eraseIdxeraseIdx l₁ m ~ eraseIdx l₂ neraseIdx l₁ m ~ eraseIdx l₂ n ↔ l₁ ~ l₂ := by
cases Nat.lt_or_ge m l₁.length with
| inl hm =>
rw [getElem?_eq_getElem hm, eq_comm, getElem?_eq_some_iff] at h
cases h with
| intro hn hnm =>
rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
rel_congr_right (getElem_cons_eraseIdx_perm ..)]
| inr hm =>
rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h
rw [eraseIdx_of_length_le h, eraseIdx_of_length_le hm]Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, and natural numbers $m$ and $n$ such that the $m$-th element of $l_1$ is equal to the $n$-th element of $l_2$ (or both are undefined), the following equivalence holds:
\[ l_1 \setminus \{l_1[m]\} \sim l_2 \setminus \{l_2[n]\} \quad \text{if and only if} \quad l_1 \sim l_2 \]
where $\sim$ denotes permutation equivalence, and $l \setminus \{l[k]\}$ denotes the list with the $k$-th element removed (if it exists).
List.perm_comp_perm
theorem
: (Perm ∘r Perm : List α → List α → Prop) = Perm
Full source
theorem perm_comp_perm : (PermPerm ∘r Perm : List α → List α → Prop) = Perm := by
funext a c; apply propext
constructor
· exact fun ⟨b, hab, hba⟩ => Perm.trans hab hba
· exact fun h => ⟨a, Perm.refl a, h⟩Informal description
The composition of the permutation relation with itself, denoted as $\text{Perm} \circ \text{Perm}$, is equal to the permutation relation $\text{Perm}$ on lists of type $\alpha$. In other words, for any two lists $l$ and $l'$ of type $\alpha$, the relation $(\text{Perm} \circ \text{Perm}) \, l \, l'$ holds if and only if $\text{Perm} \, l \, l'$ holds.
List.perm_comp_forall₂
theorem
{l u v} (hlu : Perm l u) (huv : Forall₂ r u v) : (Forall₂ r ∘r Perm) l v
Full source
theorem perm_comp_forall₂ {l u v} (hlu : Perm l u) (huv : Forall₂ r u v) :
(Forall₂Forall₂ r ∘r Perm) l v := by
induction hlu generalizing v with
| nil => cases huv; exact ⟨[], Forall₂.nil, Perm.nil⟩
| cons u _hlu ih =>
obtain - | ⟨hab, huv'⟩ := huv
rcases ih huv' with ⟨l₂, h₁₂, h₂₃⟩
exact ⟨_ :: l₂, Forall₂.cons hab h₁₂, h₂₃.cons _⟩
| swap a₁ a₂ h₂₃ =>
obtain - | ⟨h₁, hr₂₃⟩ := huv
obtain - | ⟨h₂, h₁₂⟩ := hr₂₃
exact ⟨_, Forall₂.cons h₂ (Forall₂.cons h₁ h₁₂), Perm.swap _ _ _⟩
| trans _ _ ih₁ ih₂ =>
rcases ih₂ huv with ⟨lb₂, hab₂, h₂₃⟩
rcases ih₁ hab₂ with ⟨lb₁, hab₁, h₁₂⟩
exact ⟨lb₁, hab₁, Perm.trans h₁₂ h₂₃⟩Informal description
For any lists $l$, $u$, and $v$ of type $\alpha$, if $l$ is a permutation of $u$ (denoted $l \sim u$) and there exists a relation `Forall₂ r u v$ (meaning the elements of $u$ and $v$ are pairwise related by $r$), then the composition of relations `Forall₂ r ∘ Perm` holds between $l$ and $v$.
List.forall₂_comp_perm_eq_perm_comp_forall₂
theorem
: Forall₂ r ∘r Perm = Perm ∘r Forall₂ r
Full source
theorem forall₂_comp_perm_eq_perm_comp_forall₂ : Forall₂Forall₂ r ∘r Perm = PermPerm ∘r Forall₂ r := by
funext l₁ l₃; apply propext
constructor
· intro h
rcases h with ⟨l₂, h₁₂, h₂₃⟩
have : Forall₂ (flip r) l₂ l₁ := h₁₂.flip
rcases perm_comp_forall₂ h₂₃.symm this with ⟨l', h₁, h₂⟩
exact ⟨l', h₂.symm, h₁.flip⟩
· exact fun ⟨l₂, h₁₂, h₂₃⟩ => perm_comp_forall₂ h₁₂ h₂₃Informal description
For any relation $r$, the composition of the pairwise relation `Forall₂ r` with the permutation relation `Perm` is equal to the composition of `Perm` with `Forall₂ r`. In other words, the following equality of relations holds for lists:
\[ \text{Forall₂}\, r \circ \text{Perm} = \text{Perm} \circ \text{Forall₂}\, r \]
where $\circ$ denotes the composition of relations.
List.rel_perm_imp
theorem
(hr : RightUnique r) : (Forall₂ r ⇒ Forall₂ r ⇒ (· → ·)) Perm Perm
Full source
theorem rel_perm_imp (hr : RightUnique r) : (Forall₂Forall₂ r ⇒ Forall₂ r ⇒ (· → ·)) Perm Perm :=
fun a b h₁ c d h₂ h =>
have : (flipflip (Forall₂ r) ∘r Perm ∘r Forall₂ r) b d := ⟨a, h₁, c, h, h₂⟩
have : ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d := by
rwa [← forall₂_comp_perm_eq_perm_comp_forall₂, ← Relation.comp_assoc] at this
let ⟨b', ⟨_, hbc, hcb⟩, hbd⟩ := this
have : b' = b := right_unique_forall₂' hr hcb hbc
this ▸ hbdInformal description
For any right-unique relation $r$, if two lists $l_1$ and $l_2$ are related by the pairwise relation $\text{Forall₂}\, r$, and $l_1$ is a permutation of another list $l_1'$, then there exists a list $l_2'$ such that $l_2$ is a permutation of $l_2'$ and $l_1'$ and $l_2'$ are related by $\text{Forall₂}\, r$. In other words, the following implication holds:
\[ \text{Forall₂}\, r\, l_1\, l_2 \land \text{Perm}\, l_1\, l_1' \implies \exists l_2', \text{Perm}\, l_2\, l_2' \land \text{Forall₂}\, r\, l_1'\, l_2'. \]
List.rel_perm
theorem
(hr : BiUnique r) : (Forall₂ r ⇒ Forall₂ r ⇒ (· ↔ ·)) Perm Perm
Full source
theorem rel_perm (hr : BiUnique r) : (Forall₂Forall₂ r ⇒ Forall₂ r ⇒ (· ↔ ·)) Perm Perm :=
fun _a _b hab _c _d hcd =>
Iff.intro (rel_perm_imp hr.2 hab hcd) (rel_perm_imp hr.left.flip hab.flip hcd.flip)Informal description
For any bi-unique relation $r$, two lists $l_1$ and $l_2$ are related pairwise by $\text{Forall₂}\, r$ if and only if for any permutations $l_1'$ of $l_1$ and $l_2'$ of $l_2$, the lists $l_1'$ and $l_2'$ are also related pairwise by $\text{Forall₂}\, r$. In other words, the following equivalence holds:
\[ \text{Forall₂}\, r\, l_1\, l_2 \leftrightarrow \forall l_1'\, l_2', \text{Perm}\, l_1\, l_1' \land \text{Perm}\, l_2\, l_2' \rightarrow \text{Forall₂}\, r\, l_1'\, l_2'. \]
List.count_eq_count_filter_add
theorem
[DecidableEq α] (P : α → Prop) [DecidablePred P] (l : List α) (a : α) :
count a l = count a (l.filter P) + count a (l.filter (¬P ·))
Full source
lemma count_eq_count_filter_add [DecidableEq α] (P : α → Prop) [DecidablePred P]
(l : List α) (a : α) :
count a l = count a (l.filter P) + count a (l.filter (¬ P ·)) := by
convert countP_eq_countP_filter_add l _ P
simp only [decide_not]Informal description
Let $\alpha$ be a type with decidable equality, and let $P : \alpha \to \text{Prop}$ be a decidable predicate on $\alpha$. For any list $l$ of elements of $\alpha$ and any element $a \in \alpha$, the count of $a$ in $l$ is equal to the sum of the counts of $a$ in the sublists obtained by filtering $l$ with $P$ and its negation $\neg P$. That is,
\[
\text{count}(a, l) = \text{count}(a, \text{filter}(P, l)) + \text{count}(a, \text{filter}(\neg P, l)).
\]
List.Perm.foldl_eq
theorem
{f : β → α → β} {l₁ l₂ : List α} [rcomm : RightCommutative f] (p : l₁ ~ l₂) : ∀ b, foldl f b l₁ = foldl f b l₂
Full source
theorem Perm.foldl_eq {f : β → α → β} {l₁ l₂ : List α} [rcomm : RightCommutative f] (p : l₁ ~ l₂) :
∀ b, foldl f b l₁ = foldl f b l₂ :=
p.foldl_eq' fun x _hx y _hy z => rcomm.right_comm z x yInformal description
Let $f : \beta \to \alpha \to \beta$ be a right-commutative operation, and let $l_1$ and $l_2$ be two lists of elements of type $\alpha$ that are permutations of each other (denoted $l_1 \sim l_2$). Then for any initial value $b \in \beta$, the left fold of $f$ over $l_1$ starting with $b$ is equal to the left fold of $f$ over $l_2$ starting with $b$, i.e.,
\[
\text{foldl}~f~b~l_1 = \text{foldl}~f~b~l_2.
\]
List.Perm.foldr_eq
theorem
{f : α → β → β} {l₁ l₂ : List α} [lcomm : LeftCommutative f] (p : l₁ ~ l₂) : ∀ b, foldr f b l₁ = foldr f b l₂
Full source
theorem Perm.foldr_eq {f : α → β → β} {l₁ l₂ : List α} [lcomm : LeftCommutative f] (p : l₁ ~ l₂) :
∀ b, foldr f b l₁ = foldr f b l₂ := by
intro b
induction p using Perm.recOnSwap' generalizing b with
| nil => rfl
| cons _ _ r => simp [r b]
| swap' _ _ _ r => simp only [foldr_cons]; rw [lcomm.left_comm, r b]
| trans _ _ r₁ r₂ => exact Eq.trans (r₁ b) (r₂ b)Informal description
Let $f : \alpha \to \beta \to \beta$ be a left-commutative operation, and let $l_1$ and $l_2$ be two lists of elements of type $\alpha$ that are permutations of each other (denoted $l_1 \sim l_2$). Then for any initial value $b \in \beta$, the right fold of $f$ over $l_1$ starting with $b$ is equal to the right fold of $f$ over $l_2$ starting with $b$, i.e.,
\[
\text{foldr}~f~b~l_1 = \text{foldr}~f~b~l_2.
\]
List.Perm.foldl_op_eq
theorem
{l₁ l₂ : List α} {a : α} (h : l₁ ~ l₂) : (l₁ <*> a) = l₂ <*> a
Informal description
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 binary operation $\text{op} : \alpha \to \alpha \to \alpha$ and initial value $a \in \alpha$, the left fold of $\text{op}$ over $l_1$ starting with $a$ is equal to the left fold of $\text{op}$ over $l_2$ starting with $a$, i.e.,
\[
\text{foldl}~\text{op}~a~l_1 = \text{foldl}~\text{op}~a~l_2.
\]
List.Perm.foldr_op_eq
theorem
{l₁ l₂ : List α} {a : α} (h : l₁ ~ l₂) : l₁.foldr op a = l₂.foldr op a
Informal description
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 binary operation $\text{op} : \alpha \to \alpha \to \alpha$ and initial value $a \in \alpha$, the right fold of $\text{op}$ over $l_1$ starting with $a$ is equal to the right fold of $\text{op}$ over $l_2$ starting with $a$, i.e.,
\[
\text{foldr}~\text{op}~a~l_1 = \text{foldr}~\text{op}~a~l_2.
\]
List.perm_option_toList
theorem
{o₁ o₂ : Option α} : o₁.toList ~ o₂.toList ↔ o₁ = o₂
Full source
theorem perm_option_toList {o₁ o₂ : Option α} : o₁.toList ~ o₂.toListo₁.toList ~ o₂.toList ↔ o₁ = o₂ := by
refine ⟨fun p => ?_, fun e => e ▸ Perm.refl _⟩
rcases o₁ with - | a <;> rcases o₂ with - | b; · rfl
· cases p.length_eq
· cases p.length_eq
· exact Option.mem_toList.1 (p.symm.subset <| by simp)Informal description
For any two options `o₁` and `o₂` of type `Option α`, the lists obtained by converting these options to lists (via `toList`) are permutation-equivalent (denoted by `~`) if and only if the options themselves are equal. In other words, `o₁.toList ~ o₂.toList ↔ o₁ = o₂`.
List.perm_replicate_append_replicate
theorem
[DecidableEq α] {l : List α} {a b : α} {m n : ℕ} (h : a ≠ b) :
l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]
Full source
theorem perm_replicate_append_replicate
[DecidableEq α] {l : List α} {a b : α} {m n : ℕ} (h : a ≠ b) :
l ~ replicate m a ++ replicate n bl ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b] := by
rw [perm_iff_count, ← Decidable.and_forall_ne a, ← Decidable.and_forall_ne b]
suffices l ⊆ [a, b]l ⊆ [a, b] ↔ ∀ c, c ≠ b → c ≠ a → c ∉ l by
simp +contextual [count_replicate, h, this, count_eq_zero, Ne.symm]
trans ∀ c, c ∈ l → c = b ∨ c = a
· simp [subset_def, or_comm]
· exact forall_congr' fun _ => by rw [← and_imp, ← not_or, not_imp_not]Informal description
Let $\alpha$ be a type with decidable equality, and let $l$ be a list of elements of $\alpha$. For any distinct elements $a, b \in \alpha$ and natural numbers $m, n$, the list $l$ is a permutation of the concatenation of $m$ copies of $a$ and $n$ copies of $b$ (i.e., $l \sim \text{replicate } m\ a +\!+\ \text{replicate } n\ b$) if and only if the count of $a$ in $l$ is $m$, the count of $b$ in $l$ is $n$, and all elements of $l$ are either $a$ or $b$.
List.map_perm_map_iff
theorem
{l' : List α} {f : α → β} (hf : f.Injective) : map f l ~ map f l' ↔ l ~ l'
Full source
theorem map_perm_map_iff {l' : List α} {f : α → β} (hf : f.Injective) :
mapmap f l ~ map f l'map f l ~ map f l' ↔ l ~ l' := calc
map f l ~ map f l' ↔ Relation.Comp (· = map f ·) (· ~ ·) (map f l) l' := by rw [eq_map_comp_perm]
_ ↔ l ~ l' := by simp [Relation.Comp, map_inj_right hf]Informal description
For any injective function $f : \alpha \to \beta$ and any two lists $l, l'$ of type $\alpha$, the mapped lists $f \circ l$ and $f \circ l'$ are permutations of each other if and only if the original lists $l$ and $l'$ are permutations of each other. In symbols:
\[ \text{map } f \, l \sim \text{map } f \, l' \leftrightarrow l \sim l' \]
List.Perm.flatMap_left
theorem
(l : List α) {f g : α → List β} (h : ∀ a ∈ l, f a ~ g a) : l.flatMap f ~ l.flatMap g
Full source
@[gcongr]
theorem Perm.flatMap_left (l : List α) {f g : α → List β} (h : ∀ a ∈ l, f a ~ g a) :
l.flatMap f ~ l.flatMap g :=
Perm.flatten_congr <| by
rwa [List.forall₂_map_right_iff, List.forall₂_map_left_iff, List.forall₂_same]Informal description
For any list `l` of type `α` and any two functions `f, g : α → List β`, if for every element `a ∈ l` the lists `f a` and `g a` are permutations of each other (i.e., `f a ~ g a`), then the flatMap of `f` over `l` is a permutation of the flatMap of `g` over `l` (i.e., `l.flatMap f ~ l.flatMap g`).
List.Perm.flatMap
theorem
{l₁ l₂ : List α} {f g : α → List β} (h : l₁ ~ l₂) (hfg : ∀ a ∈ l₁, f a ~ g a) : l₁.flatMap f ~ l₂.flatMap g
Full source
@[gcongr]
protected theorem Perm.flatMap {l₁ l₂ : List α} {f g : α → List β} (h : l₁ ~ l₂)
(hfg : ∀ a ∈ l₁, f a ~ g a) : l₁.flatMap f ~ l₂.flatMap g :=
.trans (.flatMap_left _ hfg) (h.flatMap_right _)Informal description
For any two lists $l₁$ and $l₂$ of type $\alpha$ and any two functions $f, g : \alpha \to \text{List } \beta$, if $l₁$ is a permutation of $l₂$ (i.e., $l₁ \sim l₂$) and for every element $a \in l₁$ the lists $f a$ and $g a$ are permutations of each other (i.e., $f a \sim g a$), then the flatMap of $f$ over $l₁$ is a permutation of the flatMap of $g$ over $l₂$ (i.e., $l₁.\text{flatMap } f \sim l₂.\text{flatMap } g$).
List.flatMap_append_perm
theorem
(l : List α) (f g : α → List β) : l.flatMap f ++ l.flatMap g ~ l.flatMap fun x => f x ++ g x
Full source
theorem flatMap_append_perm (l : List α) (f g : α → List β) :
l.flatMap f ++ l.flatMap g ~ l.flatMap fun x => f x ++ g x := by
induction l with | nil => simp | cons a l IH => ?_
simp only [flatMap_cons, append_assoc]
refine (Perm.trans ?_ (IH.append_left _)).append_left _
rw [← append_assoc, ← append_assoc]
exact perm_append_comm.append_right _Informal description
For any list $l$ of elements of type $\alpha$ and any two functions $f, g : \alpha \to \text{List } \beta$, the concatenation of the flat-mapped lists $l.\text{flatMap } f$ and $l.\text{flatMap } g$ is permutation-equivalent to the flat-mapped list obtained by applying the function $\lambda x, f x \mathbin{+\!\!+} g x$ to each element of $l$. That is,
$$ l.\text{flatMap } f \mathbin{+\!\!+} l.\text{flatMap } g \sim l.\text{flatMap } (\lambda x, f x \mathbin{+\!\!+} g x). $$
List.map_append_flatMap_perm
theorem
(l : List α) (f : α → β) (g : α → List β) : l.map f ++ l.flatMap g ~ l.flatMap fun x => f x :: g x
Full source
theorem map_append_flatMap_perm (l : List α) (f : α → β) (g : α → List β) :
l.map f ++ l.flatMap g ~ l.flatMap fun x => f x :: g x := by
simpa [← map_eq_flatMap] using flatMap_append_perm l (fun x => [f x]) gInformal description
For any list $l$ of elements of type $\alpha$, any function $f : \alpha \to \beta$, and any function $g : \alpha \to \text{List } \beta$, the concatenation of the mapped list $l.\text{map } f$ and the flat-mapped list $l.\text{flatMap } g$ is permutation-equivalent to the flat-mapped list obtained by applying the function $\lambda x, f x :: g x$ to each element of $l$. That is,
$$ l.\text{map } f \mathbin{+\!\!+} l.\text{flatMap } g \sim l.\text{flatMap } (\lambda x, f x :: g x). $$
List.Perm.product_right
theorem
{l₁ l₂ : List α} (t₁ : List β) (p : l₁ ~ l₂) : product l₁ t₁ ~ product l₂ t₁
Full source
@[gcongr]
theorem Perm.product_right {l₁ l₂ : List α} (t₁ : List β) (p : l₁ ~ l₂) :
productproduct l₁ t₁ ~ product l₂ t₁ :=
p.flatMap_right _Informal description
For any two lists $l₁$ and $l₂$ of type $\alpha$ and any list $t₁$ of type $\beta$, if $l₁$ is a permutation of $l₂$ (denoted $l₁ \sim l₂$), then the Cartesian product of $l₁$ with $t₁$ is a permutation of the Cartesian product of $l₂$ with $t₁$. That is, $l₁ \times t₁ \sim l₂ \times t₁$.
List.Perm.product_left
theorem
(l : List α) {t₁ t₂ : List β} (p : t₁ ~ t₂) : product l t₁ ~ product l t₂
Full source
@[gcongr]
theorem Perm.product_left (l : List α) {t₁ t₂ : List β} (p : t₁ ~ t₂) :
productproduct l t₁ ~ product l t₂ :=
(Perm.flatMap_left _) fun _ _ => p.map _Informal description
For any list $l$ of type $\alpha$ and any two lists $t_1, t_2$ of type $\beta$, if $t_1$ is a permutation of $t_2$ (denoted $t_1 \sim t_2$), then the Cartesian product of $l$ with $t_1$ is a permutation of the Cartesian product of $l$ with $t_2$. That is, $l \times t_1 \sim l \times t_2$.
List.Perm.product
theorem
{l₁ l₂ : List α} {t₁ t₂ : List β} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : product l₁ t₁ ~ product l₂ t₂
Full source
@[gcongr]
theorem Perm.product {l₁ l₂ : List α} {t₁ t₂ : List β} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) :
productproduct l₁ t₁ ~ product l₂ t₂ :=
(p₁.product_right t₁).trans (p₂.product_left l₂)Informal description
For any two lists $l₁$ and $l₂$ of type $\alpha$ and any two lists $t₁$ and $t₂$ of type $\beta$, if $l₁$ is a permutation of $l₂$ (denoted $l₁ \sim l₂$) and $t₁$ is a permutation of $t₂$ (denoted $t₁ \sim t₂$), then the Cartesian product of $l₁$ with $t₁$ is a permutation of the Cartesian product of $l₂$ with $t₂$. That is, $l₁ \times t₁ \sim l₂ \times t₂$.