All Combinations in a List

Stream: Is there code for X?

[Christian K]

How would I get all Possible Combinations of two Elements in List, excluding Duplicates. If i have a List [a,b,c], I want [[a,b],[b,c],[a,c]]. List.product does not work for me because it would return [a,a], [b,b] and [c,c] as well for this example. Is there a function that does this?

[Junyan Xu]

docs#List.sublistsLen is the mathlib function but not in the order you requested. Composing with docs#List.reverse probably works. docs#List.sublists is also in the right order so you may docs#List.filter by length.

[Christian K]

Ok, thank you very much, this works for me. But how can i get these Lists with the length 2 as pairs -> (a,b), (b,c) etc.

[Junyan Xu]

You can define a function from List α to α × α if α is inhabited; otherwise you can still define a function from {l : List α // l.length = 2}to α × α and you can use docs#List.map and docs#List.attach with it.

[Eric Wieser]

You might also be interested in docs#Finset.offDiag

[Christian K]

Oh, this looks very interesting. I know the {w : a | prop} Notation, but what does the {w :a // prop } Notation do? The same thing as the other one?

[Ruben Van de Velde]

Almost: | defines a set and // defines a type

[Kyle Miller]

docs#List.sym2 is similar to your original question, but it gives [(a,a),(a,b),(a,c),(b,b),(b,c),(c,c)]. That's different from List.product since each pair is unordered (that's what docs#Sym2 is, unordered pairs, the so-called "symmetric square").

[Kyle Miller]

If you change the definition of List.sym2 to

def pairs : List α → List (Sym2 α)
  | [] => []
  | x :: xs => xs.map (fun y => s(x, y)) ++ pairs xs

then it should do what you are asking. If you don't want Sym2, you can change that to

def pairs : List α → List (α × α)
  | [] => []
  | x :: xs => xs.map (fun y => (x, y)) ++ pairs xs

or modify that to use {l : List α // l.length = 2} instead.

[Christian K]

Thank you for these great suggestions, the last option works perfectly