Zulip Chat Archive

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."

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

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