Best way to choose five distinct elements from a set?

Stream: Is there code for X?

[Jordan Brown]

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]

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

[Bhavik Mehta]

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]

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

[Thomas Browning]

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

[Kevin Buzzard]

you could take the finset apart I guess.

[Kevin Buzzard]

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

[Thomas Browning]

I guess maybe a list with nodup would be enough

[Kevin Buzzard]

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

[Floris van Doorn]

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]

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]

Should there be a tactic that does this?

[Mario Carneiro]

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]

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