List Permutations #
This file develops theory about the List.Perm relation.
Notation #
The notation ~ is used for permutation equivalence.
theorem
List.Perm.subset_congr_left
{α : Type u_1}
{l₁ l₂ l₃ : List α}
(h : l₁.Perm l₂)
:
l₁ ⊆ l₃ ↔ l₂ ⊆ l₃
theorem
List.Perm.subset_congr_right
{α : Type u_1}
{l₁ l₂ l₃ : List α}
(h : l₁.Perm l₂)
:
l₃ ⊆ l₁ ↔ l₃ ⊆ l₂
theorem
List.set_perm_cons_eraseIdx
{α : Type u_1}
{l : List α}
{n : ℕ}
(h : n < l.length)
(a : α)
:
(l.set n a).Perm (a :: l.eraseIdx n)
theorem
List.getElem_cons_eraseIdx_perm
{α : Type u_1}
{l : List α}
{n : ℕ}
(h : n < l.length)
:
(l[n] :: l.eraseIdx n).Perm l
theorem
List.perm_insertIdx_iff_of_le
{α : Type u_1}
{l₁ l₂ : List α}
{m n : ℕ}
(hm : m ≤ l₁.length)
(hn : n ≤ l₂.length)
(a : α)
:
(l₁.insertIdx m a).Perm (l₂.insertIdx n a) ↔ l₁.Perm l₂
theorem
List.Perm.insertIdx_of_le
{α : Type u_1}
{l₁ l₂ : List α}
{m n : ℕ}
(hm : m ≤ l₁.length)
(hn : n ≤ l₂.length)
(a : α)
:
l₁.Perm l₂ → (l₁.insertIdx m a).Perm (l₂.insertIdx n a)
Alias of the reverse direction of List.perm_insertIdx_iff_of_le.
@[simp]
theorem
List.perm_insertIdx_iff
{α : Type u_1}
{l₁ l₂ : List α}
{n : ℕ}
{a : α}
:
(l₁.insertIdx n a).Perm (l₂.insertIdx n a) ↔ l₁.Perm l₂
theorem
List.Perm.insertIdx
{α : Type u_1}
{l₁ l₂ : List α}
(h : l₁.Perm l₂)
(n : ℕ)
(a : α)
:
(l₁.insertIdx n a).Perm (l₂.insertIdx n a)
theorem
List.perm_eraseIdx_of_getElem?_eq
{α : Type u_1}
{l₁ l₂ : List α}
{m n : ℕ}
(h : l₁[m]? = l₂[n]?)
:
(l₁.eraseIdx m).Perm (l₂.eraseIdx n) ↔ l₁.Perm l₂
theorem
List.Perm.eraseIdx_of_getElem?_eq
{α : Type u_1}
{l₁ l₂ : List α}
{m n : ℕ}
(h : l₁[m]? = l₂[n]?)
:
l₁.Perm l₂ → (l₁.eraseIdx m).Perm (l₂.eraseIdx n)
Alias of the reverse direction of List.perm_eraseIdx_of_getElem?_eq.
theorem
List.perm_comp_forall₂
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{l u : List α}
{v : List β}
(hlu : l.Perm u)
(huv : Forall₂ r u v)
:
Relation.Comp (Forall₂ r) Perm l v
theorem
List.forall₂_comp_perm_eq_perm_comp_forall₂
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
:
Relation.Comp (Forall₂ r) Perm = Relation.Comp Perm (Forall₂ r)
theorem
List.eq_map_comp_perm
{α : Type u_1}
{β : Type u_2}
(f : α → β)
:
(Relation.Comp (fun (x1 : List β) (x2 : List α) => x1 = map f x2) fun (x1 x2 : List α) => x1.Perm x2) = fun (x1 : List β) (x2 : List α) => x1.Perm (map f x2)
theorem
List.rel_perm_imp
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
(hr : Relator.RightUnique r)
:
Relator.LiftFun (Forall₂ r) (Relator.LiftFun (Forall₂ r) fun (x1 x2 : Prop) => x1 → x2) Perm Perm
theorem
List.rel_perm
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
(hr : Relator.BiUnique r)
:
Relator.LiftFun (Forall₂ r) (Relator.LiftFun (Forall₂ r) fun (x1 x2 : Prop) => x1 ↔ x2) Perm Perm
theorem
List.count_eq_count_filter_add
{α : Type u_1}
[DecidableEq α]
(P : α → Prop)
[DecidablePred P]
(l : List α)
(a : α)
:
count a l = count a (filter (fun (b : α) => decide (P b)) l) + count a (filter (fun (x : α) => decide ¬P x) l)
theorem
List.Perm.foldl_eq
{α : Type u_1}
{β : Type u_2}
{f : β → α → β}
{l₁ l₂ : List α}
[rcomm : RightCommutative f]
(p : l₁.Perm l₂)
(b : β)
:
foldl f b l₁ = foldl f b l₂
theorem
List.Perm.foldr_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β → β}
{l₁ l₂ : List α}
[lcomm : LeftCommutative f]
(p : l₁.Perm l₂)
(b : β)
:
foldr f b l₁ = foldr f b l₂
theorem
List.Perm.foldl_op_eq
{α : Type u_1}
{op : α → α → α}
[IA : Std.Associative op]
[IC : Std.Commutative op]
{l₁ l₂ : List α}
{a : α}
(h : l₁.Perm l₂)
:
foldl op a l₁ = foldl op a l₂
theorem
List.Perm.foldr_op_eq
{α : Type u_1}
{op : α → α → α}
[IA : Std.Associative op]
[IC : Std.Commutative op]
{l₁ l₂ : List α}
{a : α}
(h : l₁.Perm l₂)
:
foldr op a l₁ = foldr op a l₂
theorem
List.perm_option_toList
{α : Type u_1}
{o₁ o₂ : Option α}
:
o₁.toList.Perm o₂.toList ↔ o₁ = o₂
theorem
List.perm_replicate_append_replicate
{α : Type u_1}
[DecidableEq α]
{l : List α}
{a b : α}
{m n : ℕ}
(h : a ≠ b)
:
l.Perm (replicate m a ++ replicate n b) ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]
theorem
List.map_perm_map_iff
{α : Type u_1}
{β : Type u_2}
{l l' : List α}
{f : α → β}
(hf : Function.Injective f)
:
(map f l).Perm (map f l') ↔ l.Perm l'
theorem
List.Perm.flatMap_left
{α : Type u_1}
{β : Type u_2}
(l : List α)
{f g : α → List β}
(h : ∀ a ∈ l, (f a).Perm (g a))
:
(flatMap f l).Perm (flatMap g l)
theorem
List.Perm.flatMap
{α : Type u_1}
{β : Type u_2}
{l₁ l₂ : List α}
{f g : α → List β}
(h : l₁.Perm l₂)
(hfg : ∀ a ∈ l₁, (f a).Perm (g a))
:
(flatMap f l₁).Perm (flatMap g l₂)
theorem
List.flatMap_append_perm
{α : Type u_1}
{β : Type u_2}
(l : List α)
(f g : α → List β)
:
(flatMap f l ++ flatMap g l).Perm (flatMap (fun (x : α) => f x ++ g x) l)
theorem
List.map_append_flatMap_perm
{α : Type u_1}
{β : Type u_2}
(l : List α)
(f : α → β)
(g : α → List β)
:
(map f l ++ flatMap g l).Perm (flatMap (fun (x : α) => f x :: g x) l)
theorem
List.Perm.product_right
{α : Type u_1}
{β : Type u_2}
{l₁ l₂ : List α}
(t₁ : List β)
(p : l₁.Perm l₂)
:
(l₁.product t₁).Perm (l₂.product t₁)
theorem
List.Perm.product_left
{α : Type u_1}
{β : Type u_2}
(l : List α)
{t₁ t₂ : List β}
(p : t₁.Perm t₂)
:
(l.product t₁).Perm (l.product t₂)
theorem
List.Perm.product
{α : Type u_1}
{β : Type u_2}
{l₁ l₂ : List α}
{t₁ t₂ : List β}
(p₁ : l₁.Perm l₂)
(p₂ : t₁.Perm t₂)
:
(l₁.product t₁).Perm (l₂.product t₂)