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.
- 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.
@[protected, 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.subperm.filter
{α : Type uu}
(p : α → Prop)
[decidable_pred p]
⦃l l' : list α⦄
(h : l <+~ l') :
list.filter p l <+~ list.filter p l'
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 α} :
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₂) :
(∀ (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₂
theorem
list.subperm_append_diff_self_of_count_le
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α}
(h : ∀ (x : α), x ∈ l₁ → list.count x l₁ ≤ list.count x l₂) :
The list version of add_tsub_cancel_of_le for multisets.
theorem
list.subperm_ext_iff
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α} :
l₁ <+~ l₂ ↔ ∀ (x : α), x ∈ l₁ → list.count x l₁ ≤ list.count x l₂
The list version of multiset.le_iff_count.
theorem
list.subperm.cons_left
{α : Type uu}
[decidable_eq α]
{l₁ l₂ : list α}
(h : l₁ <+~ l₂)
(x : α)
(hx : list.count x l₁ < list.count x l₂) :
@[protected, 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_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.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 α}
(h : l₁ ∈ l₂.permutations) :
l₁ ~ l₂
@[simp]
theorem
list.perm_permutations'_aux_comm
{α : Type uu}
(a b : α)
(l : list α) :
(list.permutations'_aux a l).bind (list.permutations'_aux b) ~ (list.permutations'_aux b l).bind (list.permutations'_aux a)
theorem
list.permutations_perm_permutations'
{α : Type uu}
(ts : list α) :
ts.permutations ~ ts.permutations'
@[simp]
@[simp]
theorem
list.perm_permutations_iff
{α : Type uu}
{s t : list α} :
s.permutations ~ t.permutations ↔ s ~ t
@[simp]
theorem
list.perm_permutations'_iff
{α : Type uu}
{s t : list α} :
s.permutations' ~ t.permutations' ↔ s ~ t
theorem
list.nth_le_permutations'_aux
{α : Type uu}
(s : list α)
(x : α)
(n : ℕ)
(hn : n < (list.permutations'_aux x s).length) :
(list.permutations'_aux x s).nth_le n hn = list.insert_nth n x s
theorem
list.count_permutations'_aux_self
{α : Type uu}
[decidable_eq α]
(l : list α)
(x : α) :
list.count (x :: l) (list.permutations'_aux x l) = (list.take_while (eq x) l).length + 1
@[simp]
theorem
list.length_permutations'_aux
{α : Type uu}
(s : list α)
(x : α) :
(list.permutations'_aux x s).length = s.length + 1
@[simp]
theorem
list.permutations'_aux_nth_le_zero
{α : Type uu}
(s : list α)
(x : α)
(hn : 0 < (list.permutations'_aux x s).length := _) :
(list.permutations'_aux x s).nth_le 0 hn = x :: s
theorem
list.nodup_permutations'_aux_of_not_mem
{α : Type uu}
(s : list α)
(x : α)
(hx : x ∉ s) :
(list.permutations'_aux x s).nodup
theorem
list.nodup_permutations'_aux_iff
{α : Type uu}
{s : list α}
{x : α} :
(list.permutations'_aux x s).nodup ↔ x ∉ s