all partitions of a list

Stream: Is there code for X?

[Paige Thomas]

I was wondering if someone might know of a more elegant algorithm than this, that is simpler to prove results about.

def List.partitions
  {α : Type} :
  List α → List (List (List α))
  | [] => [[]]
  | [x] => [[[x]]]
  | (x :: xs) =>
    let partitions := List.partitions xs
    let l := partitions.map
      (fun (part : List (List α)) => ((x :: part.headI) :: part.tail))
    let r := partitions.map
      (fun (part : List (List α)) => [x] :: part)
    l ++ r

#eval List.partitions ['a', 'b', 'c', 'd', 'e']
/-
[[['a', 'b', 'c', 'd', 'e']],
 [['a', 'b', 'c', 'd'], ['e']],
 [['a', 'b', 'c'], ['d', 'e']],
 [['a', 'b', 'c'], ['d'], ['e']],
 [['a', 'b'], ['c', 'd', 'e']],
 [['a', 'b'], ['c', 'd'], ['e']],
 [['a', 'b'], ['c'], ['d', 'e']],
 [['a', 'b'], ['c'], ['d'], ['e']],
 [['a'], ['b', 'c', 'd', 'e']],
 [['a'], ['b', 'c', 'd'], ['e']],
 [['a'], ['b', 'c'], ['d', 'e']],
 [['a'], ['b', 'c'], ['d'], ['e']],
 [['a'], ['b'], ['c', 'd', 'e']],
 [['a'], ['b'], ['c', 'd'], ['e']],
 [['a'], ['b'], ['c'], ['d', 'e']],
 [['a'], ['b'], ['c'], ['d'], ['e']]]
-/

[Daniel Weber]

There is an equivalence to docs#List.sublists, perhaps you can take inspiration from how it's implemented?

[Daniel Weber]

def List.partitions
  {α : Type} (l : List α) : List (List (List α)) :=
  l.foldr (fun a acc ↦ acc.bind fun x ↦ [(a :: x.headI) :: x.tail, [a] :: x]) [[]]

[Paige Thomas]

Thank you. Is it possible to somehow incorporate a proof that the partition list is not empty to avoid the need for List.headI, either in mine or yours?

[Paige Thomas]

Or, better yet, a way to construct the definition such that it is not needed.

[Daniel Weber]

The headI there is actually used for the first step. I'm not sure how the definition could be stated without it, I'll think about it