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_induction_on
{α : Type uu}
{P : list α → list α → Prop}
{l₁ l₂ : list α}
(p : l₁ ~ l₂)
(h₁ : P list.nil list.nil)
(h₂ : ∀ (x : α) (l₁ l₂ : list α), l₁ ~ l₂ → P l₁ l₂ → P (x :: l₁) (x :: l₂))
(h₃ : ∀ (x y : α) (l₁ l₂ : list α), l₁ ~ l₂ → P l₁ l₂ → P (y :: x :: l₁) (x :: y :: l₂))
(h₄ : ∀ (l₁ l₂ l₃ : list α), l₁ ~ l₂ → l₂ ~ l₃ → P l₁ l₂ → P l₂ l₃ → P l₁ l₃) :
P l₁ l₂
theorem
list.perm.filter_map
{α : Type uu}
{β : Type vv}
(f : α → option β)
{l₁ l₂ : list α}
(p : 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 α}
(s : l₁ ~ l₂) :
list.filter p l₁ ~ list.filter p l₂
theorem
list.perm.sizeof_eq_sizeof
{α : Type uu}
[has_sizeof α]
{l₁ l₂ : list α}
(h : l₁ ~ l₂) :
l₁.sizeof = l₂.sizeof
theorem
list.perm_comp_forall₂
{α : Type uu}
{β : Type vv}
{r : α → β → Prop}
{l u : list α}
{v : list β}
(hlu : l ~ u)
(huv : 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_imp
{α : Type uu}
{β : Type vv}
{r : α → β → Prop}
(hr : relator.right_unique r) :
theorem
list.rel_perm
{α : Type uu}
{β : Type vv}
{r : α → β → Prop}
(hr : 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 α}
(s : 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 α}
(a : 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.rec_heq
{α : Type uu}
{β : list α → Sort u_1}
{f : Π (a : α) (l : list α), β l → β (a :: l)}
{b : β list.nil}
{l l' : list α}
(hl : l ~ l')
(f_congr : ∀ {a : α} {l l' : list α} {b : β l} {b' : β l'}, l ~ 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.fold_op_eq
{α : Type uu}
{op : α → α → α}
[is_associative α op]
[is_commutative α op]
{l₁ l₂ : list α}
{a : α}
(h : l₁ ~ l₂) :
list.foldl op a l₁ = list.foldl op a l₂
theorem
list.perm.sum_eq'
{α : Type uu}
[add_monoid α]
{l₁ l₂ : list α}
(h : l₁ ~ l₂)
(hc : list.pairwise (λ (x y : α), x + y = y + x) l₁) :
theorem
list.subperm.erase
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α}
(a : α)
(h : l₁ <+~ l₂) :
theorem
list.perm.diff_right
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α}
(t : list α)
(h : l₁ ~ l₂) :
theorem
list.perm.diff_left
{α : Type uu}
[decidable_eq α]
(l : list α)
{t₁ t₂ : list α}
(h : t₁ ~ t₂) :
theorem
list.perm.diff
{α : Type uu}
[decidable_eq α]
{l₁ l₂ t₁ t₂ : list α}
(hl : l₁ ~ l₂)
(ht : t₁ ~ t₂) :
theorem
list.subperm.diff_right
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α}
(h : l₁ <+~ l₂)
(t : list α) :
theorem
list.perm.bag_inter_right
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α}
(t : list α)
(h : l₁ ~ l₂) :
theorem
list.perm.bag_inter_left
{α : Type uu}
[decidable_eq α]
(l : list α)
{t₁ t₂ : list α}
(p : t₁ ~ t₂) :
theorem
list.perm.bag_inter
{α : Type uu}
[decidable_eq α]
{l₁ l₂ t₁ t₂ : list α}
(hl : l₁ ~ l₂)
(ht : t₁ ~ t₂) :
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₂) = is_false _
- list.nil.decidable_perm list.nil = is_true list.decidable_perm._main._proof_1
theorem
list.perm_insert_nth
{α : Type u_1}
(x : α)
(l : list α)
{n : ℕ}
(h : n ≤ l.length) :
list.insert_nth n x l ~ x :: l
theorem
list.perm.union_right
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α}
(t₁ : list α)
(h : l₁ ~ l₂) :
theorem
list.perm.union_left
{α : Type uu}
[decidable_eq α]
(l : list α)
{t₁ t₂ : list α}
(h : t₁ ~ t₂) :
theorem
list.perm.union
{α : Type uu}
[decidable_eq α]
{l₁ l₂ t₁ t₂ : list α}
(p₁ : l₁ ~ l₂)
(p₂ : t₁ ~ t₂) :
theorem
list.perm.inter_right
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α}
(t₁ : list α)
(a : l₁ ~ l₂) :
theorem
list.perm.inter_left
{α : Type uu}
[decidable_eq α]
(l : list α)
{t₁ t₂ : list α}
(p : t₁ ~ t₂) :
theorem
list.perm.inter
{α : Type uu}
[decidable_eq α]
{l₁ l₂ t₁ t₂ : list α}
(p₁ : l₁ ~ l₂)
(p₂ : t₁ ~ t₂) :
theorem
list.perm.pairwise_iff
{α : Type uu}
{R : α → α → Prop}
(S : symmetric R)
{l₁ l₂ : list α}
(p : l₁ ~ l₂) :
list.pairwise R l₁ ↔ list.pairwise R l₂
theorem
list.perm_lookmap
{α : Type uu}
(f : α → option α)
{l₁ l₂ : list α}
(H : list.pairwise (λ (a b : α), ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁)
(p : l₁ ~ l₂) :
list.lookmap f l₁ ~ list.lookmap f l₂
theorem
list.perm.erasep
{α : Type uu}
(f : α → Prop)
[decidable_pred f]
{l₁ l₂ : list α}
(H : list.pairwise (λ (a b : α), f a → f b → false) l₁)
(p : l₁ ~ l₂) :
list.erasep f l₁ ~ list.erasep f l₂
theorem
list.perm.slice_inter
{α : Type u_1}
[decidable_eq α]
{xs ys : list α}
(n m : ℕ)
(h : xs ~ ys)
(h' : ys.nodup) :
list.slice n m xs ~ ys ∩ list.slice n m xs
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 α}
(a : l ∈ ts.permutations_aux is) :
theorem
list.perm_of_mem_permutations
{α : Type uu}
{l₁ l₂ : list α}
(h : l₁ ∈ l₂.permutations) :
l₁ ~ l₂
@[simp]