Documentation

Init.Data.List.Perm

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.

@[simp]
theorem List.Perm.refl {α : Type u_1} (l : List α) :
l.Perm l
theorem List.Perm.rfl {α : Type u_1} {l : List α} :
l.Perm l
theorem List.Perm.of_eq :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ = l₂l₁.Perm l₂
theorem List.Perm.symm {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁.Perm l₂) :
l₂.Perm l₁
theorem List.perm_comm {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁.Perm l₂ l₂.Perm l₁
theorem List.Perm.swap' {α : Type u_1} (x : α) (y : α) {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
(y :: x :: l₁).Perm (x :: y :: l₂)
theorem List.Perm.recOnSwap' {α : Type u_1} {motive : (l₁ l₂ : List α) → l₁.Perm l₂Prop} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) (nil : motive [] [] ) (cons : ∀ (x : α) {l₁ l₂ : List α} (h : l₁.Perm l₂), motive l₁ l₂ hmotive (x :: l₁) (x :: l₂) ) (swap' : ∀ (x y : α) {l₁ l₂ : List α} (h : l₁.Perm l₂), motive l₁ l₂ hmotive (y :: x :: l₁) (x :: y :: l₂) ) (trans : ∀ {l₁ l₂ l₃ : List α} (h₁ : l₁.Perm l₂) (h₂ : l₂.Perm l₃), motive l₁ l₂ h₁motive l₂ l₃ h₂motive l₁ l₃ ) :
motive l₁ l₂ p

Similar to Perm.recOn, but the swap case is generalized to Perm.swap', where the tail of the lists are not necessarily the same.

theorem List.Perm.eqv (α : Type u_1) :
Equivalence List.Perm
instance List.isSetoid (α : Type u_1) :
Equations
theorem List.Perm.mem_iff {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
a l₁ a l₂
theorem List.Perm.subset {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
l₁ l₂
theorem List.Perm.append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} (t₁ : List α) (p : l₁.Perm l₂) :
(l₁ ++ t₁).Perm (l₂ ++ t₁)
theorem List.Perm.append_left {α : Type u_1} {t₁ : List α} {t₂ : List α} (l : List α) :
t₁.Perm t₂(l ++ t₁).Perm (l ++ t₂)
theorem List.Perm.append {α : Type u_1} {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : l₁.Perm l₂) (p₂ : t₁.Perm t₂) :
(l₁ ++ t₁).Perm (l₂ ++ t₂)
theorem List.Perm.append_cons {α : Type u_1} (a : α) {h₁ : List α} {h₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : h₁.Perm h₂) (p₂ : t₁.Perm t₂) :
(h₁ ++ a :: t₁).Perm (h₂ ++ a :: t₂)
@[simp]
theorem List.perm_middle {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} :
(l₁ ++ a :: l₂).Perm (a :: (l₁ ++ l₂))
@[simp]
theorem List.perm_append_singleton {α : Type u_1} (a : α) (l : List α) :
(l ++ [a]).Perm (a :: l)
theorem List.perm_append_comm {α : Type u_1} {l₁ : List α} {l₂ : List α} :
(l₁ ++ l₂).Perm (l₂ ++ l₁)
theorem List.perm_append_comm_assoc {α : Type u_1} (l₁ : List α) (l₂ : List α) (l₃ : List α) :
(l₁ ++ (l₂ ++ l₃)).Perm (l₂ ++ (l₁ ++ l₃))
theorem List.concat_perm {α : Type u_1} (l : List α) (a : α) :
(l.concat a).Perm (a :: l)
theorem List.Perm.length_eq {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
l₁.length = l₂.length
theorem List.Perm.eq_nil {α : Type u_1} {l : List α} (p : l.Perm []) :
l = []
theorem List.Perm.nil_eq {α : Type u_1} {l : List α} (p : [].Perm l) :
[] = l
@[simp]
theorem List.perm_nil {α : Type u_1} {l₁ : List α} :
l₁.Perm [] l₁ = []
@[simp]
theorem List.nil_perm {α : Type u_1} {l₁ : List α} :
[].Perm l₁ l₁ = []
theorem List.not_perm_nil_cons {α : Type u_1} (x : α) (l : List α) :
¬[].Perm (x :: l)
theorem List.not_perm_cons_nil {α : Type u_1} {l : List α} {a : α} :
¬(a :: l).Perm []
theorem List.Perm.isEmpty_eq {α : Type u_1} {l : List α} {l' : List α} (h : l.Perm l') :
l.isEmpty = l'.isEmpty
@[simp]
theorem List.reverse_perm {α : Type u_1} (l : List α) :
l.reverse.Perm l
theorem List.perm_cons_append_cons {α : Type u_1} {l : List α} {l₁ : List α} {l₂ : List α} (a : α) (p : l.Perm (l₁ ++ l₂)) :
(a :: l).Perm (l₁ ++ a :: l₂)
@[simp]
theorem List.perm_replicate {α : Type u_1} {n : Nat} {a : α} {l : List α} :
l.Perm (List.replicate n a) l = List.replicate n a
@[simp]
theorem List.replicate_perm {α : Type u_1} {n : Nat} {a : α} {l : List α} :
(List.replicate n a).Perm l List.replicate n a = l
@[simp]
theorem List.perm_singleton {α : Type u_1} {a : α} {l : List α} :
l.Perm [a] l = [a]
@[simp]
theorem List.singleton_perm {α : Type u_1} {a : α} {l : List α} :
[a].Perm l [a] = l
theorem List.Perm.eq_singleton :
∀ {α : Type u_1} {l : List α} {a : α}, l.Perm [a]l = [a]
theorem List.Perm.singleton_eq :
∀ {α : Type u_1} {a : α} {l : List α}, [a].Perm l[a] = l
theorem List.singleton_perm_singleton {α : Type u_1} {a : α} {b : α} :
[a].Perm [b] a = b
theorem List.perm_cons_erase {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a l) :
l.Perm (a :: l.erase a)
theorem List.Perm.filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
(List.filterMap f l₁).Perm (List.filterMap f l₂)
theorem List.Perm.map {α : Type u_1} {β : Type u_2} (f : αβ) {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
(List.map f l₁).Perm (List.map f l₂)
theorem List.Perm.pmap {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p✝ aβ) {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) {H₁ : ∀ (a : α), a l₁p✝ a} {H₂ : ∀ (a : α), a l₂p✝ a} :
(List.pmap f l₁ H₁).Perm (List.pmap f l₂ H₂)
theorem List.Perm.filter {α : Type u_1} (p : αBool) {l₁ : List α} {l₂ : List α} (s : l₁.Perm l₂) :
(List.filter p l₁).Perm (List.filter p l₂)
theorem List.filter_append_perm {α : Type u_1} (p : αBool) (l : List α) :
(List.filter p l ++ List.filter (fun (x : α) => !p x) l).Perm l
theorem List.exists_perm_sublist {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₂' : List α} (s : l₁.Sublist l₂) (p : l₂.Perm l₂') :
∃ (l₁' : List α), l₁'.Perm l₁ l₁'.Sublist l₂'
theorem List.Perm.sizeOf_eq_sizeOf {α : Type u_1} [SizeOf α] {l₁ : List α} {l₂ : List α} (h : l₁.Perm l₂) :
sizeOf l₁ = sizeOf l₂
theorem List.Sublist.exists_perm_append {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁.Sublist l₂∃ (l : List α), l₂.Perm (l₁ ++ l)
theorem List.Perm.countP_eq {α : Type u_1} (p : αBool) {l₁ : List α} {l₂ : List α} (s : l₁.Perm l₂) :
List.countP p l₁ = List.countP p l₂
theorem List.Perm.countP_congr {α : Type u_1} {l₁ : List α} {l₂ : List α} (s : l₁.Perm l₂) {p : αBool} {p' : αBool} (hp : ∀ (x : α), x l₁p x = p' x) :
List.countP p l₁ = List.countP p' l₂
theorem List.countP_eq_countP_filter_add {α : Type u_1} (l : List α) (p : αBool) (q : αBool) :
List.countP p l = List.countP p (List.filter q l) + List.countP p (List.filter (fun (a : α) => !q a) l)
theorem List.Perm.count_eq {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) (a : α) :
List.count a l₁ = List.count a l₂
theorem List.Perm.foldl_eq' {β : Type u_1} {α : Type u_2} {f : βαβ} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) (comm : ∀ (x : α), x l₁∀ (y : α), y l₁∀ (z : β), f (f z x) y = f (f z y) x) (init : β) :
List.foldl f init l₁ = List.foldl f init l₂
theorem List.Perm.foldr_eq' {α : Type u_1} {β : Type u_2} {f : αββ} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) (comm : ∀ (x : α), x l₁∀ (y : α), y l₁∀ (z : β), f y (f x z) = f x (f y z)) (init : β) :
List.foldr f init l₁ = List.foldr f init l₂
theorem List.Perm.rec_heq {α : Type u_1} {β : List αSort u_2} {f : (a : α) → (l : List α) → β lβ (a :: l)} {b : β []} {l : List α} {l' : List α} (hl : l.Perm l') (f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l.Perm l'HEq b b'HEq (f a l b) (f a l' b')) (f_swap : ∀ {a a' : α} {l : List α} {b : β l}, 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')
theorem List.perm_inv_core {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} {r₁ : List α} {r₂ : List α} :
(l₁ ++ a :: r₁).Perm (l₂ ++ a :: r₂)(l₁ ++ r₁).Perm (l₂ ++ r₂)

Lemma used to destruct perms element by element.

theorem List.Perm.cons_inv {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} :
(a :: l₁).Perm (a :: l₂)l₁.Perm l₂
@[simp]
theorem List.perm_cons {α : Type u_1} (a : α) {l₁ : List α} {l₂ : List α} :
(a :: l₁).Perm (a :: l₂) l₁.Perm l₂
theorem List.perm_append_left_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} (l : List α) :
(l ++ l₁).Perm (l ++ l₂) l₁.Perm l₂
theorem List.perm_append_right_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} (l : List α) :
(l₁ ++ l).Perm (l₂ ++ l) l₁.Perm l₂
theorem List.Perm.erase {α : Type u_1} [DecidableEq α] (a : α) {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
(l₁.erase a).Perm (l₂.erase a)
theorem List.cons_perm_iff_perm_erase {α : Type u_1} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} :
(a :: l₁).Perm l₂ a l₂ l₁.Perm (l₂.erase a)
theorem List.perm_iff_count {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} :
l₁.Perm l₂ ∀ (a : α), List.count a l₁ = List.count a l₂
theorem List.isPerm_iff {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} :
l₁.isPerm l₂ = true l₁.Perm l₂
instance List.decidablePerm {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
Decidable (l₁.Perm l₂)
Equations
theorem List.Perm.insert {α : Type u_1} [DecidableEq α] (a : α) {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
(List.insert a l₁).Perm (List.insert a l₂)
theorem List.perm_insert_swap {α : Type u_1} [DecidableEq α] (x : α) (y : α) (l : List α) :
theorem List.Perm.pairwise_iff {α : Type u_1} {R : ααProp} (S : ∀ {x y : α}, R x yR y x) {l₁ : List α} {l₂ : List α} (_p : l₁.Perm l₂) :
theorem List.Pairwise.perm {α : Type u_1} {R : ααProp} {l : List α} {l' : List α} (hR : List.Pairwise R l) (hl : l.Perm l') (hsymm : ∀ {x y : α}, R x yR y x) :
theorem List.Perm.pairwise {α : Type u_1} {R : ααProp} {l : List α} {l' : List α} (hl : l.Perm l') (hR : List.Pairwise R l) (hsymm : ∀ {x y : α}, R x yR y x) :
theorem List.Perm.eq_of_sorted {α : Type u_1} {le : ααProp} {l₁ : List α} {l₂ : List α} :
(∀ (a b : α), a l₁b l₂le a ble b aa = b)List.Pairwise le l₁List.Pairwise le l₂l₁.Perm l₂l₁ = l₂

If two lists are sorted by an antisymmetric relation, and permutations of each other, they must be equal.

theorem List.Nodup.perm {α : Type u_1} {l : List α} {l' : List α} (hR : l.Nodup) (hl : l.Perm l') :
l'.Nodup
theorem List.Perm.nodup {α : Type u_1} {l : List α} {l' : List α} (hl : l.Perm l') (hR : l.Nodup) :
l'.Nodup
theorem List.Perm.nodup_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁.Perm l₂(l₁.Nodup l₂.Nodup)
theorem List.Perm.join {α : Type u_1} {l₁ : List (List α)} {l₂ : List (List α)} (h : l₁.Perm l₂) :
l₁.join.Perm l₂.join
theorem List.Perm.bind_right {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (f : αList β) (p : l₁.Perm l₂) :
(l₁.bind f).Perm (l₂.bind f)
theorem List.Perm.eraseP {α : Type u_1} (f : αBool) {l₁ : List α} {l₂ : List α} (H : List.Pairwise (fun (a b : α) => f a = truef b = trueFalse) l₁) (p : l₁.Perm l₂) :
(List.eraseP f l₁).Perm (List.eraseP f l₂)