Stream: Is there code for X?

Topic: Best way to choose five distinct elements from a set?

Jordan Brown (Dec 10 2020 at 20:48):

What is the best way to choose five distinct elements of a set of cardinality at least five? Is there anything easier than converting a fintype to a list and choosing, say, the first five elements of the list?

Thomas Browning (Dec 10 2020 at 20:49):

In particular, we want to construct explicit permutations on this set (i.e., a 3-cycle)

Bhavik Mehta (Dec 10 2020 at 20:51):

There's https://leanprover-community.github.io/mathlib_docs/data/finset/basic.html#finset.exists_smaller_set but I'm not sure how much it helps in your case

Bhavik Mehta (Dec 10 2020 at 20:51):

It gives you a finset with 5 elements in it, which are certainly distinct

Thomas Browning (Dec 11 2020 at 19:32):

But I guess the question is how to get your hands on those 5 elements.

Kevin Buzzard (Dec 11 2020 at 20:09):

you could take the finset apart I guess.

Kevin Buzzard (Dec 11 2020 at 20:09):

There is almost certainly a more elegant way to do it though. What do you mean by "get your hands on"?

Thomas Browning (Dec 11 2020 at 20:44):

I guess maybe a list with nodup would be enough

Kevin Buzzard (Dec 11 2020 at 20:46):

then just take it apart, unless there's an officially sanctioned way

Floris van Doorn (Dec 12 2020 at 00:06):

This gives you a list without duplicates with at least 5 elements. I'm already planning to PR the first lemma soon.

import data.fintype.basic data.set.function

open function list finset set
open_locale classical

variables {α : Type*}

lemma to_finset_surj_on : surj_on to_finset { l : list α | l.nodup} univ :=
begin
rintro s -,
induction s with t hl,
induction t using quot.ind with l,
refine ⟨l, hl, (to_finset_eq hl).symm⟩
end

example (s : finset α) (h : 5 ≤ s.card) : true :=
begin
rcases to_finset_surj_on (mem_univ s) with ⟨l, h1l, rfl⟩,
rw [mem_set_of_eq] at h1l,
rw [to_finset_card_of_nodup h1l] at h,
trivial
end


Mario Carneiro (Dec 12 2020 at 07:27):

Extending that, here's how you can get 5 variables out of the list:

example (s : finset α) (h : 5 ≤ s.card) : true :=
begin
rcases to_finset_surj_on (mem_univ s) with ⟨l, h1l, rfl⟩,
rw [mem_set_of_eq] at h1l,
rw [to_finset_card_of_nodup h1l] at h,
rcases l with _|⟨a,_|⟨b,_|⟨c,_|⟨d,_|⟨e,l⟩⟩⟩⟩⟩,
iterate 5 {exact absurd h dec_trivial},
clear h,
trivial
end


Bryan Gin-ge Chen (Dec 12 2020 at 07:29):

Should there be a tactic that does this?

Mario Carneiro (Dec 12 2020 at 09:15):

Well I should also mention this method:

def to_as_true {c : Prop} [h₁ : decidable c] (h : c) : as_true c :=
match h₁, h with
| (is_true h_c),  h := trivial
| (is_false h_c), h := h_c h
end

example (s : finset α) (h : 5 ≤ s.card) : true :=
begin
rcases to_finset_surj_on (mem_univ s) with ⟨l, h1l, rfl⟩,
rw [mem_set_of_eq] at h1l,
rw [to_finset_card_of_nodup h1l] at h,
exact match l, to_as_true h, h1l with
| a::b::c::d::e::l, _, nd := _
end
end


You can almost do this with rcases:

example (s : finset α) (h : 5 ≤ s.card) : true :=
begin
rcases to_finset_surj_on (mem_univ s) with ⟨l, h1l, rfl⟩,
rw [mem_set_of_eq] at h1l,
rw [to_finset_card_of_nodup h1l] at h,
rcases ⟨l, to_as_true h⟩ with ⟨_|⟨a,_|⟨b,_|⟨c,_|⟨d,_|⟨e,l⟩⟩⟩⟩⟩, ⟨⟩⟩,
end


but it complains about not being able to match on decidable.rec, possibly it's not using whnf as much as it should

Mario Carneiro (Dec 12 2020 at 09:15):

(also I'm surprised to find that to_as_true is not proven)

Last updated: May 07 2021 at 21:10 UTC