## Stream: new members

### Topic: Choosing, classically

#### Cody Roux (Nov 28 2020 at 19:21):

Ok, I'll ask something I could probably figure out on my own but seems to be eluding me: how does one classically, given a finset A, case over whether it is empty or not, and get some arbitrary element if it isn't?

#### Cody Roux (Nov 28 2020 at 19:22):

Basically, if I can switch over s.nonempty I'm good, but I don't know how to switch!

#### Marc Huisinga (Nov 28 2020 at 19:26):

is this what you're looking for? docs#finset.eq_empty_or_nonempty

#### Cody Roux (Nov 28 2020 at 19:27):

Sure, along with a way to switch on either possibility...

#### Rob Lewis (Nov 28 2020 at 19:27):

Are you in term mode or tactic mode? In general you have many options for classical case splits, all boiling down to classical.prop_decidable.

import data.finset

open_locale classical

example {α} (s : finset α) : true :=
if hs : s.nonempty then trivial else trivial

example {α} (s : finset α) : true :=
begin
by_cases hs : s.nonempty,
{ trivial },
{ trivial }
end


#### Rob Lewis (Nov 28 2020 at 19:28):

The open_locale line gives you a local instance that says "every proposition is decidable."

term mode

#### Rob Lewis (Nov 28 2020 at 19:29):

Marc Huisinga said:

is this what you're looking for? docs#finset.eq_empty_or_nonempty

Or, if you get the disjunction from here, you can use or.elim (term mode) or cases (tactic mode)

#### Cody Roux (Nov 28 2020 at 19:29):

oh can you use that hs in the if statement?

#### Cody Roux (Nov 28 2020 at 19:30):

brilliant! Here's what I have so far:

noncomputable def finset_take : ∀ (n : ℕ) (s : finset α), finset α
| 0 := λ _, ∅
| (nat.succ n) := λ s,
if hs : s.nonempty then
let a := classical.choice hs s in
cons a (finset_take n (s.erase a))
else ∅


#### Cody Roux (Nov 28 2020 at 19:31):

classical.choice doesn't seem to be in love with this particular version of nonempty. Should I use inhabited?

#### Cody Roux (Nov 28 2020 at 19:32):

Can or.elim eliminate to Type?

#### Cody Roux (Nov 28 2020 at 19:32):

(sorry for the question rapid fire)

#### Rob Lewis (Nov 28 2020 at 19:40):

Sorry, or.by_cases, not or.elim

#### Rob Lewis (Nov 28 2020 at 19:42):

Not quite sure what the issue is there with classical.choice, mathlib favors classical.some

#### Rob Lewis (Nov 28 2020 at 19:43):

But it should be basically the same

#### Rob Lewis (Nov 28 2020 at 19:43):

I have to run, maybe someone else can figure out what's wrong there

#### Cody Roux (Nov 28 2020 at 19:43):

Thanks a bunch Rob!

#### Cody Roux (Nov 28 2020 at 19:43):

Hope things are good!

#### Bryan Gin-ge Chen (Nov 28 2020 at 19:52):

This is progress, I think:

import tactic
open_locale classical
variables (α : Type*)

noncomputable def finset_take : ℕ → finset α → finset α
| 0 _ := ∅
| (nat.succ n) s :=
if hs : s.nonempty then
let a := classical.some hs in
finset.cons a (finset_take n (s.erase a)) sorry
else ∅


Not quite sure how to fill in the sorry, which is asking for a proof that a ∉ finset_take n (s.erase a).

#### Bryan Gin-ge Chen (Nov 28 2020 at 19:53):

Oh, I guess you could also use insert instead of finset.cons:

import tactic
open_locale classical
variables (α : Type*)

noncomputable def finset_take : ℕ → finset α → finset α
| 0 _ := ∅
| (nat.succ n) s :=
if hs : s.nonempty then
let a := classical.some hs in
insert a (finset_take n (s.erase a))
else ∅


#### Kenny Lau (Nov 28 2020 at 19:55):

why not just choose a list representative

#### Cody Roux (Nov 29 2020 at 03:54):

I'm avoiding going down to lists, since it makes proofs a bit harder, it seems.

#### Mario Carneiro (Nov 29 2020 at 05:09):

what properties do you want this take function to have?

#### Kenny Lau (Nov 29 2020 at 05:11):

yeah, what's the defining properties (aka API) of your take

#### Cody Roux (Nov 30 2020 at 02:47):

I just want take n s to return exactly n distinct arbitrary members of s, if n < card s. This is actually a first step, just to get a taste of classical reasoning. Second step is building all possible such sets, and then building some well-founded induction principles, if the existing one on <+ proves insufficient.

This seems like a pretty common thing to do in additive combinatorics, along the lines of "pick an arbitrary n element set from an n+1 element set. Either this set has the k property or it doesn't in which case it has the k-1 property by IH, and we'll carefully add a new element in it, by cases".

#### Mario Carneiro (Nov 30 2020 at 03:21):

I would suggest proving the theorem first, and then using choice to extract it as a function after:

import tactic
open_locale classical
variables {α : Type*}

theorem exists_finset_take (n) (s: finset α) (h : n ≤ s.card) : ∃ t : finset α, t.card = n ∧ t ⊆ s :=
begin
have : ∀ n (s: finset α), n = s.card → ∃ t : finset α, t.card = n ∧ t ⊆ s,
{ rintro _ s rfl, refine ⟨s, rfl, _⟩, refl },
refine finset.induction (λ h, _) (λ a s ha IH h, _) s h,
{ exact this n ∅ (le_zero_iff_eq.1 h) },
rw [finset.card_insert_of_not_mem ha] at h,
obtain h | h := lt_or_eq_of_le h,
{ obtain ⟨t, te, st⟩ := IH (nat.lt_succ_iff.1 h),
refine ⟨t, te, finset.subset.trans st (finset.subset_insert _ _)⟩ },
{ apply this, rwa [finset.card_insert_of_not_mem ha] }
end

noncomputable def finset_take (n) (s: finset α) : finset α :=
if h : n ≤ s.card then classical.some (exists_finset_take n s h) else ∅

theorem card_finset_take (n) (s : finset α) (h : n ≤ s.card) : (finset_take n s).card = n :=
by rw [finset_take, dif_pos h]; exact (classical.some_spec (exists_finset_take n s h)).1

theorem finset_take_subset (n) (s : finset α) : finset_take n s ⊆ s :=
begin
rw finset_take, split_ifs,
{ exact (classical.some_spec (exists_finset_take n s h)).2 },
{ apply finset.empty_subset }
end


#### Cody Roux (Nov 30 2020 at 03:32):

Thanks a bunch @Mario Carneiro ! I have to meditate on this a bit, and figure out what finset induction is, what rintro is, etc.

#### Mario Carneiro (Nov 30 2020 at 03:32):

tactic#rintro is like intro but you can do pattern matching while introducing variables, like the equation compiler

#### Cody Roux (Nov 30 2020 at 03:33):

Cool! Well this is all very fun. I'm sure I'll be back around when I try my next baby proof.

#### Mario Carneiro (Nov 30 2020 at 03:33):

docs#finset.induction is a convenient way to do induction on finsets by adding elements disjoint from everything so far, which seems relevant for your additive combinatorics example

#### Bhavik Mehta (Nov 30 2020 at 04:00):

You could alternatively use https://leanprover-community.github.io/mathlib_docs/data/finset/basic.html#finset.exists_intermediate_set or the lemma after that :)

#### Bhavik Mehta (Nov 30 2020 at 04:01):

which, unsurprisingly, I needed for doing combinatorics in Lean as well!

#### Floris van Doorn (Nov 30 2020 at 04:02):

Ah nice! I was already surprised that Mario's lemma exists_finset_take apparently didn't exist yet.

#### Cody Roux (Nov 30 2020 at 18:23):

Oh dang, I thought I had looked! Sheesh, these libs are quite detailed. I'm actually a little surprised no-one's tried Ramsey's theorem.

#### Johan Commelin (Nov 30 2020 at 18:32):

@Cody Roux I don't know anything about Ramsey, but it has been tried afaik

#### Johan Commelin (Nov 30 2020 at 18:32):

https://github.com/b-mehta/combinatorics/blob/extras/src/inf_ramsey.lean

#### Alex J. Best (Nov 30 2020 at 18:34):

(deleted)

Last updated: May 14 2021 at 03:27 UTC