Zulip Chat Archive

Stream: general

Topic: n-permutations of a list


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 29 2020 at 20:39):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 29 2020 at 20:48):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 29 2020 at 20:50):

by laziness

view this post on Zulip Vaibhav Karve (Jul 29 2020 at 20:51):

Yeah, I meant combinations. I fixed the question.

view this post on Zulip 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?

view this post on Zulip 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