List permutations
- nil : ∀ {α : Type uu}, list.nil ~ list.nil
- cons : ∀ {α : Type uu} (x : α) {l₁ l₂ : list α}, l₁ ~ l₂ → x :: l₁ ~ x :: l₂
- swap : ∀ {α : Type uu} (x y : α) (l : list α), y :: x :: l ~ x :: y :: l
- trans : ∀ {α : Type uu} {l₁ l₂ l₃ : list α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
perm l₁ l₂ or l₁ ~ l₂ asserts that l₁ and l₂ are permutations
of each other. This is defined by induction using pairwise swaps.
@[instance]
@[simp]
theorem
list.perm_repeat
{α : Type uu}
{a : α}
{n : ℕ}
{l : list α} :
l ~ list.repeat a n ↔ l = list.repeat a n
@[simp]
theorem
list.repeat_perm
{α : Type uu}
{a : α}
{n : ℕ}
{l : list α} :
list.repeat a n ~ l ↔ list.repeat a n = l
theorem
list.perm.filter_map
{α : Type uu}
{β : Type vv}
(f : α → option β)
{l₁ l₂ : list α} :
l₁ ~ l₂ → list.filter_map f l₁ ~ list.filter_map f l₂
theorem
list.perm.filter
{α : Type uu}
(p : α → Prop)
[decidable_pred p]
{l₁ l₂ : list α} :
l₁ ~ l₂ → list.filter p l₁ ~ list.filter p l₂
theorem
list.perm_comp_forall₂
{α : Type uu}
{β : Type vv}
{r : α → β → Prop}
{l u : list α}
{v : list β} :
l ~ u → list.forall₂ r u v → relation.comp (list.forall₂ r) list.perm l v
theorem
list.forall₂_comp_perm_eq_perm_comp_forall₂
{α : Type uu}
{β : Type vv}
{r : α → β → Prop} :
theorem
list.rel_perm
{α : Type uu}
{β : Type vv}
{r : α → β → Prop} :
relator.bi_unique r → (list.forall₂ r ⇒ list.forall₂ r ⇒ iff) list.perm list.perm
subperm l₁ l₂, denoted l₁ <+~ l₂, means that l₁ is a sublist of
a permutation of l₂. This is an analogue of l₁ ⊆ l₂ which respects
multiplicities of elements, and is used for the ≤ relation on multisets.
theorem
list.perm.countp_eq
{α : Type uu}
(p : α → Prop)
[decidable_pred p]
{l₁ l₂ : list α} :
l₁ ~ l₂ → list.countp p l₁ = list.countp p l₂
theorem
list.subperm.countp_le
{α : Type uu}
(p : α → Prop)
[decidable_pred p]
{l₁ l₂ : list α} :
l₁ <+~ l₂ → list.countp p l₁ ≤ list.countp p l₂
theorem
list.perm.count_eq
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α}
(p : l₁ ~ l₂)
(a : α) :
list.count a l₁ = list.count a l₂
theorem
list.subperm.count_le
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α}
(s : l₁ <+~ l₂)
(a : α) :
list.count a l₁ ≤ list.count a l₂
theorem
list.perm.foldl_eq'
{α : Type uu}
{β : Type vv}
{f : β → α → β}
{l₁ l₂ : list α}
(p : l₁ ~ l₂)
(a : ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₁ → ∀ (z : β), f (f z x) y = f (f z y) x)
(b : β) :
list.foldl f b l₁ = list.foldl f b l₂
theorem
list.perm.foldl_eq
{α : Type uu}
{β : Type vv}
{f : β → α → β}
{l₁ l₂ : list α}
(rcomm : right_commutative f)
(p : l₁ ~ l₂)
(b : β) :
list.foldl f b l₁ = list.foldl f b l₂
theorem
list.perm.foldr_eq
{α : Type uu}
{β : Type vv}
{f : α → β → β}
{l₁ l₂ : list α}
(lcomm : left_commutative f)
(p : l₁ ~ l₂)
(b : β) :
list.foldr f b l₁ = list.foldr f b l₂
theorem
list.perm.fold_op_eq
{α : Type uu}
{op : α → α → α}
[is_associative α op]
[is_commutative α op]
{l₁ l₂ : list α}
{a : α} :
l₁ ~ l₂ → list.foldl op a l₁ = list.foldl op a l₂
theorem
list.subperm.diff_right
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α}
(h : l₁ <+~ l₂)
(t : list α) :
theorem
list.perm_iff_count
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α} :
l₁ ~ l₂ ↔ ∀ (a : α), list.count a l₁ = list.count a l₂
@[instance]
Equations
- (a :: l₁).decidable_perm l₂ = decidable_of_iff' (a ∈ l₂ ∧ l₁ ~ l₂.erase a) _
- list.nil.decidable_perm (b :: l₂) = decidable.is_false _
- list.nil.decidable_perm list.nil = decidable.is_true list.decidable_perm._main._proof_1
theorem
list.perm.insert
{α : Type uu}
[decidable_eq α]
(a : α)
{l₁ l₂ : list α} :
l₁ ~ l₂ → has_insert.insert a l₁ ~ has_insert.insert a l₂
theorem
list.perm_insert_swap
{α : Type uu}
[decidable_eq α]
(x y : α)
(l : list α) :
has_insert.insert x (has_insert.insert y l) ~ has_insert.insert y (has_insert.insert x l)
theorem
list.perm.pairwise_iff
{α : Type uu}
{R : α → α → Prop}
(S : symmetric R)
{l₁ l₂ : list α} :
l₁ ~ l₂ → (list.pairwise R l₁ ↔ list.pairwise R l₂)
theorem
list.perm_lookmap
{α : Type uu}
(f : α → option α)
{l₁ l₂ : list α} :
list.pairwise (λ (a b : α), ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → l₁ ~ l₂ → list.lookmap f l₁ ~ list.lookmap f l₂
theorem
list.perm.erasep
{α : Type uu}
(f : α → Prop)
[decidable_pred f]
{l₁ l₂ : list α} :
list.pairwise (λ (a b : α), f a → f b → false) l₁ → l₁ ~ l₂ → list.erasep f l₁ ~ list.erasep f l₂
theorem
list.permutations_aux2_fst
{α : Type uu}
{β : Type vv}
(t : α)
(ts : list α)
(r : list β)
(ys : list α)
(f : list α → β) :
(list.permutations_aux2 t ts r ys f).fst = ys ++ ts
@[simp]
theorem
list.permutations_aux2_snd_nil
{α : Type uu}
{β : Type vv}
(t : α)
(ts : list α)
(r : list β)
(f : list α → β) :
(list.permutations_aux2 t ts r list.nil f).snd = r
@[simp]
theorem
list.permutations_aux2_append
{α : Type uu}
{β : Type vv}
(t : α)
(ts : list α)
(r : list β)
(ys : list α)
(f : list α → β) :
(list.permutations_aux2 t ts list.nil ys f).snd ++ r = (list.permutations_aux2 t ts r ys f).snd
theorem
list.length_permutations_aux2
{α : Type uu}
{β : Type vv}
(t : α)
(ts ys : list α)
(f : list α → β) :
theorem
list.foldr_permutations_aux2
{α : Type uu}
(t : α)
(ts : list α)
(r L : list (list α)) :
list.foldr (λ (y : list α) (r : list (list α)), (list.permutations_aux2 t ts r y id).snd) r L = L.bind (λ (y : list α), (list.permutations_aux2 t ts list.nil y id).snd) ++ r
theorem
list.mem_foldr_permutations_aux2
{α : Type uu}
{t : α}
{ts : list α}
{r L : list (list α)}
{l' : list α} :
theorem
list.length_foldr_permutations_aux2
{α : Type uu}
(t : α)
(ts : list α)
(r L : list (list α)) :
(list.foldr (λ (y : list α) (r : list (list α)), (list.permutations_aux2 t ts r y id).snd) r L).length = (list.map list.length L).sum + r.length
theorem
list.perm_of_mem_permutations_aux
{α : Type uu}
{ts is l : list α} :
l ∈ ts.permutations_aux is → l ~ ts ++ is
theorem
list.perm_of_mem_permutations
{α : Type uu}
{l₁ l₂ : list α} :
l₁ ∈ l₂.permutations → l₁ ~ l₂
theorem
list.length_permutations
{α : Type uu}
(l : list α) :
l.permutations.length = l.length.fact
@[simp]