Zulip Chat Archive

Stream: new members

Topic: choosing from difference of finsets


Bryan Gin-ge Chen (Sep 09 2018 at 17:57):

Here's my "Tactic State":

α : Type u_1,
_inst_1 : decidable_eq α,
x y S : finset α,
hx : x  S,
hy : y  S,
hcard : finset.card x < finset.card y
  (e : α), e  y \ x

I've been digging through finset and am not sure what I need to do to kill this goal. Any pointers? It looks like I need to invoke classical.choice, but does that mean I need to turn things into fintypes?

Mario Carneiro (Sep 09 2018 at 18:10):

You could prove that finset.card (y \ x) != 0

Bryan Gin-ge Chen (Sep 09 2018 at 18:44):

Oops, I should have showed that S is nonempty before this point. But I'm still not seeing how to easily work with finset.card. Perhaps I should be working with multiset.card instead?

Kevin Buzzard (Sep 09 2018 at 19:58):

The interface should all be there, although it might require reading finset.lean...

Kevin Buzzard (Sep 09 2018 at 20:01):

So my algorithm for doing questions like this is to type import finset, see what auto-complete suggests, find that finset.lean is in data/, then open finset.lean and search the file for card to see what's there.

Kevin Buzzard (Sep 09 2018 at 20:04):

theorem eq_of_subset_of_card_le {s t : finset α} (h : s ⊆ t) (h₂ : card t ≤ card s) : s = t := .... Can I work classically?

Patrick Massot (Sep 09 2018 at 20:04):

Yes!

Patrick Massot (Sep 09 2018 at 20:05):

(didn't read the code part)

Mario Carneiro (Sep 09 2018 at 20:05):

You should have decidable whatever in this context

Kevin Buzzard (Sep 09 2018 at 20:22):

import data.finset
import logic.basic

local attribute [instance, priority 0] classical.prop_decidable

example (α) [decidable_eq α] (x y : finset α) (hcard : finset.card x < finset.card y)
:  (e : α), e  y \ x :=
begin
  have hnsub : ¬ (y  x),
    intro hsub,
    have Heq := finset.eq_of_subset_of_card_le hsub (le_of_lt hcard),
    rw Heq at hcard,
    revert hcard,simp,
  by_contra hnotex,
  have h2 := forall_not_of_not_exists hnotex,
  apply hnsub,
  intros b Hb,
  have h3 := h2 b,
  revert Hb,
  revert h3,
  simp,
end

Amateurish approach. I don't know if I need decidability.

Mario Carneiro (Sep 09 2018 at 20:24):

does removing the local instance break the proof?

Chris Hughes (Sep 09 2018 at 20:25):

I think the by_contra will break.

Kevin Buzzard (Sep 09 2018 at 20:25):

by_contra hnotex breaks

Bryan Gin-ge Chen (Sep 09 2018 at 20:25):

I tried to do the following as a warmup for the above:

import data.fintype
variable {α : Type*}
variable [decidable_eq α]

noncomputable def chosen {S : finset α} (h : ¬(S = )) : α := begin
rw [ne] at h,
have SS : fintype (S : set α) := finset_coe.fintype S,
have hSS : nonempty (S : set α) := set.nonempty_iff_univ_ne_empty.mpr _,
exact ((classical.choice hSS) : α)
end

I'm having trouble turning h : S ≠ ∅ into ⊢ @set.univ ↥↑S ≠ ∅. Probably I'm just scared by the ↥↑ since I'm not too comfortable with coercions.

I've also been following something like your algorithm @Kevin Buzzard but I wanted to check in and make sure I wasn't missing some obscure lemma elsewhere. Thanks for your solution, I'll study it carefully now!

Kenny Lau (Sep 09 2018 at 20:26):

if you make the statement bounded then by_contra will not break

Mario Carneiro (Sep 09 2018 at 20:26):

chosen is definitely noncomputable, but you can use finset.exists_mem_of_ne_empty to prove that easily

Chris Hughes (Sep 09 2018 at 20:27):

classical.sone (exists_mem_of_ne_empty h)

Kevin Buzzard (Sep 09 2018 at 20:27):

@Bryan Gin-ge Chen you should try and understand Kenny's golfed solution :-)

Bryan Gin-ge Chen (Sep 09 2018 at 20:28):

Thanks Mario and Chris!

Kevin Buzzard (Sep 09 2018 at 20:29):

I'm having trouble getting your warm-up to compile. What are the imports and variables?

Bryan Gin-ge Chen (Sep 09 2018 at 20:31):

Sorry about that, see the edit.

Kevin Buzzard (Sep 09 2018 at 20:32):

My Lean has never heard of set.nonempty_iff_univ_ne_empty.mpr

Mario Carneiro (Sep 09 2018 at 20:33):

example (α) [decidable_eq α] (x y : finset α) (hcard : finset.card x < finset.card y) : ∃ (e : α), e ∈ y \ x :=
classical.by_contradiction $ λ h,
not_le_of_lt hcard (finset.card_le_of_subset $ by simpa using h)

Kevin Buzzard (Sep 09 2018 at 20:34):

Oh sorry, I meant Mario's golfed solution.

Mario Carneiro (Sep 09 2018 at 20:34):

there is a way to prove it without classical stuff, but I will let kenny do that

Bryan Gin-ge Chen (Sep 09 2018 at 20:34):

it's in data.set.basic; I guess it was added quite recently https://github.com/leanprover/mathlib/pull/295

Kevin Buzzard (Sep 09 2018 at 20:34):

Oh yes, I have an old project open. Thanks!

Kevin Buzzard (Sep 09 2018 at 20:40):

I guess ↥↑S means the subtype corresponding to the set corresponding to S.

Kenny Lau (Sep 09 2018 at 20:41):

there is a way to prove it without classical stuff, but I will let kenny do that

roger that

example (α) [decidable_eq α] (x y : finset α) (hcard : finset.card x < finset.card y) :  (e : α), e  y \ x :=
suffices  e  y, e  x, by simpa,
by_contradiction $ λ H, not_le_of_lt hcard (finset.card_le_of_subset $ by simpa using H)

Mario Carneiro (Sep 09 2018 at 20:44):

lol, that was easy

Kevin Buzzard (Sep 09 2018 at 20:50):

noncomputable def chosen {S : finset α} (h : ¬(S = )) : α := begin
  rw [ne] at h,
  rw finset.card_pos at h,
  change 0 < multiset.card S.val at h, -- switching to multisets
  rw multiset.card_pos_iff_exists_mem at h, -- there's now a one-liner that I forgot
  have hinhabited := classical.inhabited_of_exists h,
  cases hinhabited with a,
  exact a
end

Kevin Buzzard (Sep 09 2018 at 20:51):

lol, that was easy

oh come on, he just copied your answer ;-)

Patrick Massot (Sep 09 2018 at 20:57):

the last three lines can be abbreviated to exact (classical.inhabited_of_exists h).default

Kenny Lau (Sep 09 2018 at 21:04):

noncomputable def chosen {α} {S : finset α} (h : ¬(S = )) : α :=
classical.some $ classical.not_forall.1 $
mt finset.eq_empty_of_forall_not_mem h

Last updated: Dec 20 2023 at 11:08 UTC