mathlib3 documentation

data.list.permutation

Permutations of a list #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove properties about list.permutations, a list of all permutations of a list. It is defined in data.list.defs.

Order of the permutations #

Designed for performance, the order in which the permutations appear in list.permutations is rather intricate and not very amenable to induction. That's why we also provide list.permutations' as a less efficient but more straightforward way of listing permutations.

`list.permutations` #

TODO. In the meantime, you can try decrypting the docstrings.

`list.permutations'` #

The list of partitions is built by recursion. The permutations of [] are [[]]. Then, the permutations of a :: l are obtained by taking all permutations of l in order and adding a in all positions. Hence, to build [0, 1, 2, 3].permutations', it does

[[]]
[[3]]
[[2, 3], [3, 2]]]
[[1, 2, 3], [2, 1, 3], [2, 3, 1], [1, 3, 2], [3, 1, 2], [3, 2, 1]]
[[0, 1, 2, 3], [1, 0, 2, 3], [1, 2, 0, 3], [1, 2, 3, 0], [0, 2, 1, 3], [2, 0, 1, 3], [2, 1, 0, 3], [2, 1, 3, 0], [0, 2, 3, 1], [2, 0, 3, 1], [2, 3, 0, 1], [2, 3, 1, 0], [0, 1, 3, 2], [1, 0, 3, 2], [1, 3, 0, 2], [1, 3, 2, 0], [0, 3, 1, 2], [3, 0, 1, 2], [3, 1, 0, 2], [3, 1, 2, 0], [0, 3, 2, 1], [3, 0, 2, 1], [3, 2, 0, 1], [3, 2, 1, 0]]

TODO #

Show that l.nodup → l.permutations.nodup. See data.fintype.list.

theorem list.permutations_aux2_fst {α : Type u_1} {β : Type u_2} (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 u_1} {β : Type u_2} (t : α) (ts : list α) (r : list β) (f : list α → β) :

(list.permutations_aux2 t ts r list.nil f).snd = r

@[simp]

theorem list.permutations_aux2_snd_cons {α : Type u_1} {β : Type u_2} (t : α) (ts : list α) (r : list β) (y : α) (ys : list α) (f : list α → β) :

(list.permutations_aux2 t ts r (y :: ys) f).snd = f (t :: y :: ys ++ ts) :: (list.permutations_aux2 t ts r ys (λ (x : list α), f (y :: x))).snd

theorem list.permutations_aux2_append {α : Type u_1} {β : Type u_2} (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

The r argument to permutations_aux2 is the same as appending.

theorem list.permutations_aux2_comp_append {α : Type u_1} {β : Type u_2} {t : α} {ts ys : list α} {r : list β} (f : list α → β) :

(list.permutations_aux2 t list.nil r ys (λ (x : list α), f (x ++ ts))).snd = (list.permutations_aux2 t ts r ys f).snd

The ts argument to permutations_aux2 can be folded into the f argument.

theorem list.map_permutations_aux2' {α : Type u_1} {β : Type u_2} {α' : Type u_3} {β' : Type u_4} (g : α → α') (g' : β → β') (t : α) (ts ys : list α) (r : list β) (f : list α → β) (f' : list α' → β') (H : ∀ (a : list α), g' (f a) = f' (list.map g a)) :

list.map g' (list.permutations_aux2 t ts r ys f).snd = (list.permutations_aux2 (g t) (list.map g ts) (list.map g' r) (list.map g ys) f').snd

theorem list.map_permutations_aux2 {α : Type u_1} {β : Type u_2} (t : α) (ts ys : list α) (f : list α → β) :

list.map f (list.permutations_aux2 t ts list.nil ys id).snd = (list.permutations_aux2 t ts list.nil ys f).snd

The f argument to permutations_aux2 when r = [] can be eliminated.

theorem list.permutations_aux2_snd_eq {α : Type u_1} {β : Type u_2} (t : α) (ts : list α) (r : list β) (ys : list α) (f : list α → β) :

(list.permutations_aux2 t ts r ys f).snd = list.map (λ (x : list α), f (x ++ ts)) (list.permutations_aux2 t list.nil list.nil ys id).snd ++ r

An expository lemma to show how all of ts, r, and f can be eliminated from permutations_aux2.

(permutations_aux2 t [] [] ys id).2, which appears on the RHS, is a list whose elements are produced by inserting t into every non-terminal position of ys in order. As an example:

#eval permutations_aux2 1 [] [] [2, 3, 4] id
-- [[1, 2, 3, 4], [2, 1, 3, 4], [2, 3, 1, 4]]

theorem list.map_map_permutations_aux2 {α : Type u_1} {α' : Type u_2} (g : α → α') (t : α) (ts ys : list α) :

list.map (list.map g) (list.permutations_aux2 t ts list.nil ys id).snd = (list.permutations_aux2 (g t) (list.map g ts) list.nil (list.map g ys) id).snd

theorem list.map_map_permutations'_aux {α : Type u_1} {β : Type u_2} (f : α → β) (t : α) (ts : list α) :

list.map (list.map f) (list.permutations'_aux t ts) = list.permutations'_aux (f t) (list.map f ts)

theorem list.permutations'_aux_eq_permutations_aux2 {α : Type u_1} (t : α) (ts : list α) :

list.permutations'_aux t ts = (list.permutations_aux2 t list.nil [ts ++ [t]] ts id).snd

theorem list.mem_permutations_aux2 {α : Type u_1} {t : α} {ts ys l l' : list α} :

l' ∈ (list.permutations_aux2 t ts list.nil ys (has_append.append l)).snd ↔ ∃ (l₁ l₂ : list α), l₂ ≠ list.nil ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

theorem list.mem_permutations_aux2' {α : Type u_1} {t : α} {ts ys l : list α} :

l ∈ (list.permutations_aux2 t ts list.nil ys id).snd ↔ ∃ (l₁ l₂ : list α), l₂ ≠ list.nil ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts

theorem list.length_permutations_aux2 {α : Type u_1} {β : Type u_2} (t : α) (ts ys : list α) (f : list α → β) :

(list.permutations_aux2 t ts list.nil ys f).snd.length = ys.length

theorem list.foldr_permutations_aux2 {α : Type u_1} (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 u_1} {t : α} {ts : list α} {r L : list (list α)} {l' : list α} :

l' ∈ list.foldr (λ (y : list α) (r : list (list α)), (list.permutations_aux2 t ts r y id).snd) r L ↔ l' ∈ r ∨ ∃ (l₁ l₂ : list α), l₁ ++ l₂ ∈ L ∧ l₂ ≠ list.nil ∧ l' = l₁ ++ t :: l₂ ++ ts

theorem list.length_foldr_permutations_aux2 {α : Type u_1} (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.length_foldr_permutations_aux2' {α : Type u_1} (t : α) (ts : list α) (r L : list (list α)) (n : ℕ) (H : ∀ (l : list α), l ∈ L → l.length = n) :

(list.foldr (λ (y : list α) (r : list (list α)), (list.permutations_aux2 t ts r y id).snd) r L).length = n * L.length + r.length

@[simp]

theorem list.permutations_aux_nil {α : Type u_1} (is : list α) :

list.nil.permutations_aux is = list.nil

@[simp]

theorem list.permutations_aux_cons {α : Type u_1} (t : α) (ts is : list α) :

(t :: ts).permutations_aux is = list.foldr (λ (y : list α) (r : list (list α)), (list.permutations_aux2 t ts r y id).snd) (ts.permutations_aux (t :: is)) is.permutations

@[simp]

theorem list.permutations_nil {α : Type u_1} :

list.nil.permutations = [list.nil]

theorem list.map_permutations_aux {α : Type u_1} {β : Type u_2} (f : α → β) (ts is : list α) :

list.map (list.map f) (ts.permutations_aux is) = (list.map f ts).permutations_aux (list.map f is)

theorem list.map_permutations {α : Type u_1} {β : Type u_2} (f : α → β) (ts : list α) :

list.map (list.map f) ts.permutations = (list.map f ts).permutations

theorem list.map_permutations' {α : Type u_1} {β : Type u_2} (f : α → β) (ts : list α) :

list.map (list.map f) ts.permutations' = (list.map f ts).permutations'

theorem list.permutations_aux_append {α : Type u_1} (is is' ts : list α) :

(is ++ ts).permutations_aux is' = list.map (λ (_x : list α), _x ++ ts) (is.permutations_aux is') ++ ts.permutations_aux (is.reverse ++ is')

theorem list.permutations_append {α : Type u_1} (is ts : list α) :

(is ++ ts).permutations = list.map (λ (_x : list α), _x ++ ts) is.permutations ++ ts.permutations_aux is.reverse