# 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_3} {β : Type u_4} {α' : Type u_5} {β' : Type u_6} (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_3} {α' : Type u_4} (g : αα') (t : α) (ts : List α) (ys : List α) :
List.map () (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 α) :
theorem List.permutations'Aux_eq_permutationsAux2 {α : Type u_1} (t : α) (ts : List α) :
= (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 : List α), l Ll.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 () (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 () ts.permutations = (List.map f ts).permutations
theorem List.map_permutations' {α : Type u_1} {β : Type u_2} (f : αβ) (ts : List α) :
List.map () 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