n-permutations of a list

Stream: general

[Vaibhav Karve]

We already have list.permutations : list A -> list (list A). Is there a version of this that takes an argument n : nat and gives all possible n-permutations n-combinations (sublists of size n without ordering)? Should I be using list.sublists and then filtering for the ones with length n?

Edit: I changed permutations to combinations.

[Mario Carneiro]

sublists and permutations are not the same thing. Are reorderings being considered?

[Mario Carneiro]

namespace list

def n_sublists_aux {α} : ℕ → list α → (list α → list α) → list (list α) → list (list α)
| 0 _ f r := f [] :: r
| (n+1) [] f r := r
| (n+1) (a::l) f r := n_sublists_aux n l (λ x, f (a :: x)) (n_sublists_aux (n+1) l f r)

def n_sublists {α} (n : ℕ) (l : list α) : list (list α) := n_sublists_aux n l id []

#eval n_sublists 2 [1,2,3,4,5]
-- [[1, 2], [1, 3], [1, 4], [1, 5], [2, 3], [2, 4], [2, 5], [3, 4], [3, 5], [4, 5]]

end list

[Mario Carneiro]

I leave the proof of correctness as an exercise for the reader

[Patrick Massot]

Mario Carneiro said:

I leave the proof of correctness as an exercise for the reader

This is also my favorite tactic.

[Mario Carneiro]

by laziness

[Vaibhav Karve]

Yeah, I meant combinations. I fixed the question.

[Vaibhav Karve]

I think it would be nice to have a function for n-combinations as well as n-permutaions in mathlib?

[Mario Carneiro]

Yes, that function should be in data.list.defs