Permutations of a list

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.permutationsAux2_fst {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β) : (List.permutationsAux2 t ts r ys f).1 = ys ++ ts

@[simp]

theorem List.permutationsAux2_snd_nil {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (f : List α → β) : (List.permutationsAux2 t ts r [] f).2 = r

@[simp]

theorem List.permutationsAux2_snd_cons {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (y : α) (ys : List α) (f : List α → β) : (List.permutationsAux2 t ts r (y :: ys) f).2 = f (t :: y :: ys ++ ts) :: (List.permutationsAux2 t ts r ys fun (x : List α) => f (y :: x)).2

theorem List.permutationsAux2_append {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β) : (List.permutationsAux2 t ts [] ys f).2 ++ r = (List.permutationsAux2 t ts r ys f).2

The r argument to permutationsAux2 is the same as appending.

theorem List.permutationsAux2_comp_append {α : Type u_1} {β : Type u_2} {t : α} {ts : List α} {ys : List α} {r : List β} (f : List α → β) : (List.permutationsAux2 t [] r ys fun (x : List α) => f (x ++ ts)).2 = (List.permutationsAux2 t ts r ys f).2

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

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

theorem List.map_permutationsAux2 {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (ys : List α) (f : List α → β) : List.map f (List.permutationsAux2 t ts [] ys id).2 = (List.permutationsAux2 t ts [] ys f).2

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

theorem List.permutationsAux2_snd_eq {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β) : (List.permutationsAux2 t ts r ys f).2 = List.map (fun (x : List α) => f (x ++ ts)) (List.permutationsAux2 t [] [] ys id).2 ++ r

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

(permutationsAux2 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 permutationsAux2 1 [] [] [2, 3, 4] id
-- [[1, 2, 3, 4], [2, 1, 3, 4], [2, 3, 1, 4]]

theorem List.map_map_permutationsAux2 {α : Type u_1} {α' : Type u_3} (g : α → α') (t : α) (ts : List α) (ys : List α) : List.map (List.map g) (List.permutationsAux2 t ts [] ys id).2 = (List.permutationsAux2 (g t) (List.map g ts) [] (List.map g ys) id).2

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_permutationsAux2 {α : Type u_1} (t : α) (ts : List α) : List.permutations'Aux t ts = (List.permutationsAux2 t [] [ts ++ [t]] ts id).2

theorem List.mem_permutationsAux2 {α : Type u_1} {t : α} {ts : List α} {ys : List α} {l : List α} {l' : List α} : l' ∈ (List.permutationsAux2 t ts [] ys fun (x : List α) => l ++ x).2 ↔ ∃ (l₁ : List α) (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

theorem List.mem_permutationsAux2' {α : Type u_1} {t : α} {ts : List α} {ys : List α} {l : List α} : l ∈ (List.permutationsAux2 t ts [] ys id).2 ↔ ∃ (l₁ : List α) (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts

theorem List.length_permutationsAux2 {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (ys : List α) (f : List α → β) : (List.permutationsAux2 t ts [] ys f).2.length = ys.length

theorem List.foldr_permutationsAux2 {α : Type u_1} (t : α) (ts : List α) (r : List (List α)) (L : List (List α)) : List.foldr (fun (y : List α) (r : List (List α)) => (List.permutationsAux2 t ts r y id).2) r L = (L.bind fun (y : List α) => (List.permutationsAux2 t ts [] y id).2) ++ r

theorem List.mem_foldr_permutationsAux2 {α : Type u_1} {t : α} {ts : List α} {r : List (List α)} {L : List (List α)} {l' : List α} : l' ∈ List.foldr (fun (y : List α) (r : List (List α)) => (List.permutationsAux2 t ts r y id).2) r L ↔ l' ∈ r ∨ ∃ (l₁ : List α) (l₂ : List α), l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts

theorem List.length_foldr_permutationsAux2 {α : Type u_1} (t : α) (ts : List α) (r : List (List α)) (L : List (List α)) : (List.foldr (fun (y : List α) (r : List (List α)) => (List.permutationsAux2 t ts r y id).2) r L).length = Nat.sum (List.map List.length L) + r.length

theorem List.length_foldr_permutationsAux2' {α : Type u_1} (t : α) (ts : List α) (r : List (List α)) (L : List (List α)) (n : ℕ) (H : ∀ l ∈ L, l.length = n) : (List.foldr (fun (y : List α) (r : List (List α)) => (List.permutationsAux2 t ts r y id).2) r L).length = n * L.length + r.length

@[simp]

theorem List.permutationsAux_nil {α : Type u_1} (is : List α) : [].permutationsAux is = []

@[simp]

theorem List.permutationsAux_cons {α : Type u_1} (t : α) (ts : List α) (is : List α) : (t :: ts).permutationsAux is = List.foldr (fun (y : List α) (r : List (List α)) => (List.permutationsAux2 t ts r y id).2) (ts.permutationsAux (t :: is)) is.permutations

@[simp]

theorem List.permutations_nil {α : Type u_1} : [].permutations = [[]]

theorem List.map_permutationsAux {α : Type u_1} {β : Type u_2} (f : α → β) (ts : List α) (is : List α) : List.map (List.map f) (ts.permutationsAux is) = (List.map f ts).permutationsAux (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.permutationsAux_append {α : Type u_1} (is : List α) (is' : List α) (ts : List α) : (is ++ ts).permutationsAux is' = List.map (fun (x : List α) => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')

theorem List.permutations_append {α : Type u_1} (is : List α) (ts : List α) : (is ++ ts).permutations = List.map (fun (x : List α) => x ++ ts) is.permutations ++ ts.permutationsAux is.reverse

theorem List.perm_of_mem_permutationsAux {α : Type u_1} {ts : List α} {is : List α} {l : List α} : l ∈ ts.permutationsAux is → l.Perm (ts ++ is)

theorem List.perm_of_mem_permutations {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ ∈ l₂.permutations) : l₁.Perm l₂

theorem List.length_permutationsAux {α : Type u_1} (ts : List α) (is : List α) : (ts.permutationsAux is).length + is.length.factorial = (ts.length + is.length).factorial

theorem List.length_permutations {α : Type u_1} (l : List α) : l.permutations.length = l.length.factorial

theorem List.mem_permutations_of_perm_lemma {α : Type u_1} {is : List α} {l : List α} (H : l.Perm ([] ++ is) → (∃ (ts' : List α) (_ : ts'.Perm []), l = ts' ++ is) ∨ l ∈ is.permutationsAux []) : l.Perm is → l ∈ is.permutations

theorem List.mem_permutationsAux_of_perm {α : Type u_1} {ts : List α} {is : List α} {l : List α} : l.Perm (is ++ ts) → (∃ (is' : List α) (_ : is'.Perm is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux is

@[simp]

theorem List.mem_permutations {α : Type u_1} {s : List α} {t : List α} : s ∈ t.permutations ↔ s.Perm t

theorem List.perm_permutations'Aux_comm {α : Type u_1} (a : α) (b : α) (l : List α) : ((List.permutations'Aux a l).bind (List.permutations'Aux b)).Perm ((List.permutations'Aux b l).bind (List.permutations'Aux a))

theorem List.Perm.permutations' {α : Type u_1} {s : List α} {t : List α} (p : s.Perm t) : s.permutations'.Perm t.permutations'

theorem List.permutations_perm_permutations' {α : Type u_1} (ts : List α) : ts.permutations.Perm ts.permutations'

@[simp]

theorem List.mem_permutations' {α : Type u_1} {s : List α} {t : List α} : s ∈ t.permutations' ↔ s.Perm t

theorem List.Perm.permutations {α : Type u_1} {s : List α} {t : List α} (h : s.Perm t) : s.permutations.Perm t.permutations

@[simp]

theorem List.perm_permutations_iff {α : Type u_1} {s : List α} {t : List α} : s.permutations.Perm t.permutations ↔ s.Perm t

@[simp]

theorem List.perm_permutations'_iff {α : Type u_1} {s : List α} {t : List α} : s.permutations'.Perm t.permutations' ↔ s.Perm t

theorem List.getElem_permutations'Aux {α : Type u_1} (s : List α) (x : α) (n : ℕ) (hn : n < (List.permutations'Aux x s).length) : (List.permutations'Aux x s)[n] = List.insertIdx n x s

theorem List.get_permutations'Aux {α : Type u_1} (s : List α) (x : α) (n : ℕ) (hn : n < (List.permutations'Aux x s).length) : (List.permutations'Aux x s).get ⟨n, hn⟩ = List.insertIdx n x s

theorem List.count_permutations'Aux_self {α : Type u_1} [DecidableEq α] (l : List α) (x : α) : List.count (x :: l) (List.permutations'Aux x l) = (List.takeWhile (fun (x_1 : α) => decide (x = x_1)) l).length + 1

@[simp]

theorem List.length_permutations'Aux {α : Type u_1} (s : List α) (x : α) : (List.permutations'Aux x s).length = s.length + 1

@[deprecated]

theorem List.permutations'Aux_get_zero {α : Type u_1} (s : List α) (x : α) (hn : optParam (0 < (List.permutations'Aux x s).length) ⋯) : (List.permutations'Aux x s).get ⟨0, hn⟩ = x :: s

theorem List.injective_permutations'Aux {α : Type u_1} (x : α) : Function.Injective (List.permutations'Aux x)

theorem List.nodup_permutations'Aux_of_not_mem {α : Type u_1} (s : List α) (x : α) (hx : x ∉ s) : (List.permutations'Aux x s).Nodup

theorem List.nodup_permutations'Aux_iff {α : Type u_1} {s : List α} {x : α} : (List.permutations'Aux x s).Nodup ↔ x ∉ s

theorem List.nodup_permutations {α : Type u_1} (s : List α) (hs : s.Nodup) : s.permutations.Nodup

theorem List.permutations_take_two {α : Type u_1} (x : α) (y : α) (s : List α) : List.take 2 (x :: y :: s).permutations = [x :: y :: s, y :: x :: s]

@[simp]

theorem List.nodup_permutations_iff {α : Type u_1} {s : List α} : s.permutations.Nodup ↔ s.Nodup