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.
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₂ 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.
Equations
- List.isSetoid α = { r := List.Perm, iseqv := ⋯ }
@[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
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.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.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)))
:
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 α}
:
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₂
instance
List.decidablePerm
{α : Type u_1}
[DecidableEq α]
(l₁ : List α)
(l₂ : List α)
:
Decidable (l₁.Perm l₂)
Equations
- l₁.decidablePerm l₂ = decidable_of_iff (l₁.isPerm l₂ = true) ⋯
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 α)
:
(List.insert x (List.insert y l)).Perm (List.insert y (List.insert x l))
theorem
List.Perm.pairwise_iff
{α : Type u_1}
{R : α → α → Prop}
(S : ∀ {x y : α}, R x y → R y x)
{l₁ : List α}
{l₂ : List α}
(_p : l₁.Perm l₂)
:
List.Pairwise R l₁ ↔ List.Pairwise R 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 y → R y x)
:
List.Pairwise R l'
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 y → R y x)
:
List.Pairwise R l'
theorem
List.Perm.eq_of_sorted
{α : Type u_1}
{le : α → α → Prop}
{l₁ : List α}
{l₂ : List α}
:
(∀ (a b : α), a ∈ l₁ → b ∈ l₂ → le a b → le b a → a = 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.eraseP
{α : Type u_1}
(f : α → Bool)
{l₁ : List α}
{l₂ : List α}
(H : List.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₂)