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
Alias of the forward direction of List.perm_singleton
.
Alias of the forward direction of List.singleton_perm
.
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.Sublist.subperm
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
(s : l₁.Sublist l₂)
:
l₁.Subperm l₂
theorem
List.Perm.subperm
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
(p : l₁.Perm l₂)
:
l₁.Subperm l₂
theorem
List.Subperm.antisymm
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
(h₁ : l₁.Subperm l₂)
(h₂ : l₂.Subperm l₁)
:
l₁.Perm l₂
theorem
List.Subperm.filter
{α : Type u_1}
(p : α → Bool)
⦃l : List α⦄
⦃l' : List α⦄
(h : l.Subperm l')
:
(List.filter p l).Subperm (List.filter p 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.Subperm.countP_le
{α : Type u_1}
(p : α → Bool)
{l₁ : List α}
{l₂ : List α}
:
l₁.Subperm 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.Subperm.count_le
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(s : l₁.Subperm 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.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.cons_subperm_of_not_mem_of_mem
{α : Type u_1}
{a : α}
{l₁ : List α}
{l₂ : List α}
(h₁ : ¬a ∈ l₁)
(h₂ : a ∈ l₂)
(s : l₁.Subperm l₂)
:
(a :: l₁).Subperm l₂
Weaker version of Subperm.cons_left
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.subperm_cons_erase
{α : Type u_1}
[DecidableEq α]
(a : α)
(l : List α)
:
l.Subperm (a :: l.erase a)
theorem
List.erase_subperm
{α : Type u_1}
[DecidableEq α]
(a : α)
(l : List α)
:
(l.erase a).Subperm l
theorem
List.Subperm.erase
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(a : α)
(h : l₁.Subperm l₂)
:
(l₁.erase a).Subperm (l₂.erase a)
theorem
List.Perm.diff_right
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(t : List α)
(h : l₁.Perm l₂)
:
(l₁.diff t).Perm (l₂.diff t)
theorem
List.Perm.diff_left
{α : Type u_1}
[DecidableEq α]
(l : List α)
{t₁ : List α}
{t₂ : List α}
(h : t₁.Perm t₂)
:
l.diff t₁ = l.diff t₂
theorem
List.Perm.diff
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
{t₁ : List α}
{t₂ : List α}
(hl : l₁.Perm l₂)
(ht : t₁.Perm t₂)
:
(l₁.diff t₁).Perm (l₂.diff t₂)
theorem
List.Subperm.diff_right
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(h : l₁.Subperm l₂)
(t : List α)
:
(l₁.diff t).Subperm (l₂.diff t)
theorem
List.erase_cons_subperm_cons_erase
{α : Type u_1}
[DecidableEq α]
(a : α)
(b : α)
(l : List α)
:
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₂
theorem
List.subperm_append_diff_self_of_count_le
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(h : ∀ (x : α), x ∈ l₁ → List.count x l₁ ≤ List.count x l₂)
:
(l₁ ++ l₂.diff l₁).Perm l₂
The list version of add_tsub_cancel_of_le
for multisets.
theorem
List.subperm_ext_iff
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
:
l₁.Subperm l₂ ↔ ∀ (x : α), x ∈ l₁ → List.count x l₁ ≤ List.count x l₂
The list version of Multiset.le_iff_count
.
instance
List.decidableSubperm
{α : Type u_1}
[DecidableEq α]
:
DecidableRel fun (x x_1 : List α) => x.Subperm x_1
Equations
- x✝.decidableSubperm x = decidable_of_iff (x✝.isSubperm x = true) ⋯
theorem
List.Subperm.cons_left
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(h : l₁.Subperm l₂)
(x : α)
(hx : List.count x l₁ < List.count x l₂)
:
(x :: l₁).Subperm 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_insertNth
{α : Type u_1}
(x : α)
(l : List α)
{n : Nat}
(h : n ≤ l.length)
:
(List.insertNth n x l).Perm (x :: l)
theorem
List.Perm.union_right
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(t₁ : List α)
(h : l₁.Perm l₂)
:
theorem
List.Perm.union_left
{α : Type u_1}
[DecidableEq α]
(l : List α)
{t₁ : List α}
{t₂ : List α}
(h : t₁.Perm t₂)
:
theorem
List.Perm.union
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
{t₁ : List α}
{t₂ : List α}
(p₁ : l₁.Perm l₂)
(p₂ : t₁.Perm t₂)
:
theorem
List.Perm.inter_right
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(t₁ : List α)
:
theorem
List.Perm.inter_left
{α : Type u_1}
[DecidableEq α]
(l : List α)
{t₁ : List α}
{t₂ : List α}
(p : t₁.Perm t₂)
:
theorem
List.Perm.inter
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
{t₁ : List α}
{t₂ : List α}
(p₁ : l₁.Perm l₂)
(p₂ : t₁.Perm t₂)
:
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.join_congr
{α : Type u_1}
{l₁ : List (List α)}
{l₂ : List (List α)}
:
List.Forall₂ (fun (x x_1 : List α) => x.Perm x_1) l₁ l₂ → l₁.join.Perm l₂.join
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₂)
@[irreducible]
theorem
List.perm_merge
{α : Type u_1}
(s : α → α → Bool)
(l : List α)
(r : List α)
:
(List.merge s l r).Perm (l ++ r)
theorem
List.Perm.merge
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{r₁ : List α}
{r₂ : List α}
(s₁ : α → α → Bool)
(s₂ : α → α → Bool)
(hl : l₁.Perm l₂)
(hr : r₁.Perm r₂)
:
(List.merge s₁ l₁ r₁).Perm (List.merge s₂ l₂ r₂)