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 α✝} (h : l₁ = l₂) : l₁.Perm l₂

theorem List.Perm.symm {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) : l₂.Perm l₁

@[instance_reducible]

instance List.instTransPerm {α : Type u_1} : Trans Perm Perm Perm

Equations

• List.instTransPerm = { trans := ⋯ }

theorem List.perm_comm {α : Type u_1} {l₁ l₂ : List α} : l₁.Perm l₂ ↔ l₂.Perm l₁

theorem List.Perm.congr_left {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) (l₃ : List α) : l₁.Perm l₃ ↔ l₂.Perm l₃

theorem List.Perm.congr_right {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) (l₃ : List α) : l₃.Perm l₁ ↔ l₃.Perm l₂

theorem List.Perm.swap' {α : Type u_1} (x y : α) {l₁ 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₁ l₂ : List α} (p : l₁.Perm l₂) (nil : motive [] [] ⋯) (cons : ∀ (x : α) {l₁ l₂ : List α} (h : l₁.Perm l₂), motive l₁ l₂ h → motive (x :: l₁) (x :: l₂) ⋯) (swap' : ∀ (x y : α) {l₁ l₂ : List α} (h : l₁.Perm l₂), motive l₁ l₂ h → motive (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 Perm

@[instance_reducible]

instance List.isSetoid (α : Type u_1) : Setoid (List α)

Equations

• List.isSetoid α = { r := List.Perm, iseqv := ⋯ }

theorem List.Perm.mem_iff {α : Type u_1} {a : α} {l₁ l₂ : List α} (p : l₁.Perm l₂) : a ∈ l₁ ↔ a ∈ l₂

theorem List.Perm.subset {α : Type u_1} {l₁ l₂ : List α} (p : l₁.Perm l₂) : l₁ ⊆ l₂

theorem List.Perm.append_right {α : Type u_1} {l₁ l₂ : List α} (t₁ : List α) (p : l₁.Perm l₂) : (l₁ ++ t₁).Perm (l₂ ++ t₁)

theorem List.Perm.append_left {α : Type u_1} {t₁ t₂ : List α} (l : List α) : t₁.Perm t₂ → (l ++ t₁).Perm (l ++ t₂)

theorem List.Perm.append {α : Type u_1} {l₁ l₂ t₁ t₂ : List α} (p₁ : l₁.Perm l₂) (p₂ : t₁.Perm t₂) : (l₁ ++ t₁).Perm (l₂ ++ t₂)

theorem List.Perm.append_cons {α : Type u_1} (a : α) {l₁ l₂ r₁ r₂ : List α} (p₁ : l₁.Perm l₂) (p₂ : r₁.Perm r₂) : (l₁ ++ a :: r₁).Perm (l₂ ++ a :: r₂)

@[simp]

theorem List.perm_middle {α : Type u_1} {a : α} {l₁ 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₁ l₂ : List α} : (l₁ ++ l₂).Perm (l₂ ++ l₁)

theorem List.perm_append_comm_assoc {α : Type u_1} (l₁ l₂ 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₁ l₂ : List α} (p : l₁.Perm l₂) : l₁.length = l₂.length

theorem List.Perm.contains_eq {α : Type u_1} [BEq α] {l₁ l₂ : List α} (h : l₁.Perm l₂) {a : α} : l₁.contains a = l₂.contains a

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 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 l₁ 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 (replicate n a) ↔ l = replicate n a

@[simp]

theorem List.replicate_perm {α : Type u_1} {n : Nat} {a : α} {l : List α} : (replicate n a).Perm l ↔ 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 : α✝} (h : l.Perm [a]) : l = [a]

theorem List.Perm.singleton_eq {α✝ : Type u_1} {a : α✝} {l : List α✝} (h : [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} [BEq α] [LawfulBEq α] {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₁ 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₁ 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₁ l₂ : List α} : 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.unattach {α : Type u} {p : α → Prop} {l₁ l₂ : List { x : α // p x }} (h : l₁.Perm l₂) : l₁.unattach.Perm l₂.unattach

theorem List.Perm.filter {α : Type u_1} (p : α → Bool) {l₁ 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 α) : (filter p l ++ filter (fun (x : α) => !p x) l).Perm l

theorem List.exists_perm_sublist {α : Type u_1} {l₁ l₂ 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₁ l₂ : List α} (h : l₁.Perm l₂) : sizeOf l₁ = sizeOf l₂

theorem List.Sublist.exists_perm_append {α : Type u_1} {l₁ l₂ : List α} : l₁.Sublist l₂ → ∃ (l : List α), l₂.Perm (l₁ ++ l)

theorem List.Perm.countP_eq {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α} (s : l₁.Perm l₂) : countP p l₁ = countP p l₂

theorem List.Perm.countP_congr {α : Type u_1} {l₁ l₂ : List α} (s : l₁.Perm l₂) {p p' : α → Bool} (hp : ∀ (x : α), x ∈ l₁ → p x = p' x) : countP p l₁ = countP p' l₂

theorem List.countP_eq_countP_filter_add {α : Type u_1} (l : List α) (p q : α → Bool) : countP p l = countP p (filter q l) + countP p (filter (fun (a : α) => !q a) l)

theorem List.Perm.count_eq {α : Type u_1} [BEq α] {l₁ 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₁ 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 : β) : foldl f init l₁ = foldl f init l₂

This theorem is a variant of Perm.foldl_eq defined in Mathlib which uses typeclasses rather than the explicit comm argument.

theorem List.Perm.foldr_eq' {α : Type u_1} {β : Type u_2} {f : α → β → β} {l₁ 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 : β) : foldr f init l₁ = foldr f init l₂

This theorem is a variant of Perm.foldr_eq defined in Mathlib which uses typeclasses rather than the explicit comm argument.

theorem List.Perm.rec_heq {α : Type u_1} {β : List α → Sort u_2} {f : (a : α) → (l : List α) → β l → β (a :: l)} {b : β []} {l l' : List α} (hl : l.Perm l') (f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l.Perm l' → b ≍ b' → f a l b ≍ f a l' b') (f_swap : ∀ {a a' : α} {l : List α} {b : β l}, f a (a' :: l) (f a' l b) ≍ f a' (a :: l) (f a l b)) : List.rec b f l ≍ List.rec b f l'

theorem List.perm_inv_core {α : Type u_1} {a : α} {l₁ l₂ r₁ 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₁ l₂ : List α} : (a :: l₁).Perm (a :: l₂) → l₁.Perm l₂

@[simp]

theorem List.perm_cons {α : Type u_1} (a : α) {l₁ l₂ : List α} : (a :: l₁).Perm (a :: l₂) ↔ l₁.Perm l₂

theorem List.perm_append_left_iff {α : Type u_1} {l₁ l₂ : List α} (l : List α) : (l ++ l₁).Perm (l ++ l₂) ↔ l₁.Perm l₂

theorem List.perm_append_right_iff {α : Type u_1} {l₁ l₂ : List α} (l : List α) : (l₁ ++ l).Perm (l₂ ++ l) ↔ l₁.Perm l₂

theorem List.Perm.erase {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) {l₁ l₂ : List α} (p : l₁.Perm l₂) : (l₁.erase a).Perm (l₂.erase a)

theorem List.cons_perm_iff_perm_erase {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α} : (a :: l₁).Perm l₂ ↔ a ∈ l₂ ∧ l₁.Perm (l₂.erase a)

theorem List.perm_iff_count {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : l₁.Perm l₂ ↔ ∀ (a : α), count a l₁ = count a l₂

theorem List.Perm.count {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} (h : l₁.Perm l₂) (a : α) : List.count a l₁ = List.count a l₂

theorem List.isPerm_iff {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : l₁.isPerm l₂ = true ↔ l₁.Perm l₂

@[instance_reducible]

instance List.decidablePerm {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁.Perm l₂)

Equations

• l₁.decidablePerm l₂ = decidable_of_iff (l₁.isPerm l₂ = true) ⋯

theorem List.Perm.insert {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) {l₁ l₂ : List α} (p : l₁.Perm l₂) : (List.insert a l₁).Perm (List.insert a l₂)

theorem List.perm_insert_swap {α : Type u_1} [BEq α] [LawfulBEq α] (x y : α) (l : List α) : (List.insert x (List.insert y l)).Perm (List.insert y (List.insert x l))

theorem List.perm_ext_iff_of_nodup {α : Type u_1} {l₁ l₂ : List α} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) : l₁.Perm l₂ ↔ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂

Two lists without duplicates are permutations of each other if and only if they have the same elements.

theorem List.Nodup.length_le_of_subset {α : Type u_1} {l₁ l₂ : List α} (h₁ : l₁.Nodup) (hsub : l₁ ⊆ l₂) : l₁.length ≤ l₂.length

A list with no duplicates that is a subset of another list is no longer than that list.

theorem List.Perm.pairwise_iff {α : Type u_1} {R : α → α → Prop} (S : ∀ {x y : α}, R x y → R y x) {l₁ l₂ : List α} (_p : l₁.Perm l₂) : Pairwise R l₁ ↔ Pairwise R l₂

theorem List.Pairwise.perm {α : Type u_1} {R : α → α → Prop} {l l' : List α} (hR : Pairwise R l) (hl : l.Perm l') (hsymm : ∀ {x y : α}, R x y → R y x) : Pairwise R l'

theorem List.Perm.pairwise {α : Type u_1} {R : α → α → Prop} {l l' : List α} (hl : l.Perm l') (hR : Pairwise R l) (hsymm : ∀ {x y : α}, R x y → R y x) : Pairwise R l'

theorem List.Perm.eq_of_pairwise {α : Type u_1} {le : α → α → Prop} {l₁ l₂ : List α} : (∀ (a b : α), a ∈ l₁ → b ∈ l₂ → le a b → le b a → a = b) → Pairwise le l₁ → 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 l' : List α} (hR : l.Nodup) (hl : l.Perm l') : l'.Nodup

theorem List.Perm.nodup {α : Type u_1} {l l' : List α} (hl : l.Perm l') (hR : l.Nodup) : l'.Nodup

theorem List.Perm.nodup_iff {α : Type u_1} {l₁ l₂ : List α} : l₁.Perm l₂ → (l₁.Nodup ↔ l₂.Nodup)

theorem List.Perm.flatten {α : Type u_1} {l₁ l₂ : List (List α)} (h : l₁.Perm l₂) : l₁.flatten.Perm l₂.flatten

theorem List.cons_append_cons_perm {α : Type u_1} {a b : α} {as bs : List α} : (a :: as ++ b :: bs).Perm (b :: as ++ a :: bs)

theorem List.Perm.flatMap_right {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (f : α → List β) (p : l₁.Perm l₂) : (flatMap f l₁).Perm (flatMap f l₂)

theorem List.Perm.eraseP {α : Type u_1} (f : α → Bool) {l₁ l₂ : List α} (H : Pairwise (fun (a b : α) => f a = true → f b = true → False) l₁) (p : l₁.Perm l₂) : (List.eraseP f l₁).Perm (List.eraseP f l₂)

theorem List.perm_insertIdx {α : Type u_1} (x : α) (l : List α) {i : Nat} (h : i ≤ l.length) : (l.insertIdx i x).Perm (x :: l)

theorem List.Perm.take {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) {i : Nat} (w : (List.drop i l₁).Perm (List.drop i l₂)) : (List.take i l₁).Perm (List.take i l₂)

theorem List.Perm.drop {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) {i : Nat} (w : (List.take i l₁).Perm (List.take i l₂)) : (List.drop i l₁).Perm (List.drop i l₂)

theorem List.Perm.sum_nat {l₁ l₂ : List Nat} (h : l₁.Perm l₂) : l₁.sum = l₂.sum

theorem List.Perm.prod_nat {l₁ l₂ : List Nat} (h : l₁.Perm l₂) : l₁.prod = l₂.prod

theorem List.Perm.all_eq {α : Type u_1} {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.all f = l₂.all f

theorem List.Perm.any_eq {α : Type u_1} {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.any f = l₂.any f