choosing from difference of finsets

Stream: new members

[Bryan Gin-ge Chen]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Kevin Buzzard]

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]

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]

Yes!

[Patrick Massot]

(didn't read the code part)

[Mario Carneiro]

You should have decidable whatever in this context

[Kevin Buzzard]

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]

does removing the local instance break the proof?

[Chris Hughes]

I think the by_contra will break.

[Kevin Buzzard]

by_contra hnotex breaks

[Bryan Gin-ge Chen]

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]

if you make the statement bounded then by_contra will not break

[Mario Carneiro]

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

[Chris Hughes]

classical.sone (exists_mem_of_ne_empty h)

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

Thanks Mario and Chris!

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

Sorry about that, see the edit.

[Kevin Buzzard]

My Lean has never heard of set.nonempty_iff_univ_ne_empty.mpr

[Mario Carneiro]

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]

Oh sorry, I meant Mario's golfed solution.

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

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]

lol, that was easy

[Kevin Buzzard]

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]

lol, that was easy

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

[Patrick Massot]

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

[Kenny Lau]

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