Zulip Chat Archive

Stream: new members

Topic: Choosing, classically


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

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

view this post on Zulip Marc Huisinga (Nov 28 2020 at 19:26):

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

view this post on Zulip Cody Roux (Nov 28 2020 at 19:27):

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

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

view this post on Zulip Rob Lewis (Nov 28 2020 at 19:28):

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

view this post on Zulip Cody Roux (Nov 28 2020 at 19:29):

term mode

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

view this post on Zulip Cody Roux (Nov 28 2020 at 19:29):

oh can you use that hs in the if statement?

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

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

view this post on Zulip Cody Roux (Nov 28 2020 at 19:32):

Can or.elim eliminate to Type?

view this post on Zulip Cody Roux (Nov 28 2020 at 19:32):

(sorry for the question rapid fire)

view this post on Zulip Rob Lewis (Nov 28 2020 at 19:40):

Sorry, or.by_cases, not or.elim

view this post on Zulip Rob Lewis (Nov 28 2020 at 19:42):

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

view this post on Zulip Rob Lewis (Nov 28 2020 at 19:43):

But it should be basically the same

view this post on Zulip Rob Lewis (Nov 28 2020 at 19:43):

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

view this post on Zulip Cody Roux (Nov 28 2020 at 19:43):

Thanks a bunch Rob!

view this post on Zulip Cody Roux (Nov 28 2020 at 19:43):

Hope things are good!

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

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

view this post on Zulip Kenny Lau (Nov 28 2020 at 19:55):

why not just choose a list representative

view this post on Zulip Cody Roux (Nov 29 2020 at 03:54):

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

view this post on Zulip Mario Carneiro (Nov 29 2020 at 05:09):

what properties do you want this take function to have?

view this post on Zulip Kenny Lau (Nov 29 2020 at 05:11):

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

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

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

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

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

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

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

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

view this post on Zulip Bhavik Mehta (Nov 30 2020 at 04:01):

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

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

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

view this post on Zulip Johan Commelin (Nov 30 2020 at 18:32):

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

view this post on Zulip Johan Commelin (Nov 30 2020 at 18:32):

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

view this post on Zulip Alex J. Best (Nov 30 2020 at 18:34):

(deleted)


Last updated: May 14 2021 at 03:27 UTC