## Stream: general

### Topic: n-permutations of a list

#### Vaibhav Karve (Jul 29 2020 at 20:34):

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 (Jul 29 2020 at 20:39):

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

#### Mario Carneiro (Jul 29 2020 at 20:48):

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 (Jul 29 2020 at 20:48):

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

#### Patrick Massot (Jul 29 2020 at 20:49):

Mario Carneiro said:

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

This is also my favorite tactic.

#### Mario Carneiro (Jul 29 2020 at 20:50):

by laziness

#### Vaibhav Karve (Jul 29 2020 at 20:51):

Yeah, I meant combinations. I fixed the question.

#### Vaibhav Karve (Jul 29 2020 at 20:55):

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

#### Mario Carneiro (Jul 29 2020 at 21:09):

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

Last updated: May 10 2021 at 00:31 UTC