Zulip Chat Archive

Stream: Is there code for X?

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


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

view this post on Zulip Thomas Browning (Dec 10 2020 at 20:49):

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

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

view this post on Zulip Bhavik Mehta (Dec 10 2020 at 20:51):

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

view this post on Zulip Thomas Browning (Dec 11 2020 at 19:32):

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

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 20:09):

you could take the finset apart I guess.

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

view this post on Zulip Thomas Browning (Dec 11 2020 at 20:44):

I guess maybe a list with nodup would be enough

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 20:46):

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

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

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

view this post on Zulip Bryan Gin-ge Chen (Dec 12 2020 at 07:29):

Should there be a tactic that does this?

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

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