decidable existence of mem of finset

Stream: lean4

[Kayla Thomas]

Is the existence of a member of a finite set undecidable? This gives me failed to synthesize instance Decidable (∃ n, n ∈ S):

import Mathlib.Data.Finset.Basic

set_option autoImplicit false

def blah (S : Finset Nat) := if ∃ (n : Nat), n ∈ S then true else false

but this works:

import Mathlib.Data.Finset.Basic

set_option autoImplicit false

def blah (S : Finset Nat) (m : Nat) := if ∃ (n : Nat), n ∈ S ∧ m = n then true else false

[Mario Carneiro]

You could put True in there

[Mario Carneiro]

I guess there is no instance for this

[Kayla Thomas]

True gives the same error.

[Kayla Thomas]

What is the simplest way to make an instance of it?

[Mario Carneiro]

this works for me:

def blah (S : Finset Nat) (m : Nat) := if ∃ (n : Nat), n ∈ S ∧ True then true else false

[Kayla Thomas]

oh, I thought you meant change true to True.

[Eric Wieser]

I think the meta-answer is that you're supposed to be using docs#Finset.Nonempty

[Eric Wieser]

Channeling the docs:

It should be used in theorem assumptions instead of ∃ x, x ∈ s

[Mario Carneiro]

instance {α} (S : Finset α) : Decidable (∃ a, a ∈ S) := inferInstanceAs (Decidable S.Nonempty)

[Kayla Thomas]

Shouldn't it be decidable if it is empty too?

[Eric Wieser]

def blah (S : Finset Nat) (m : Nat) := if S.Nonempty then true else false

[Kayla Thomas]

To the question mark, I don't understand why we need the additional hypothesis that the set is not empty for membership to be decidable.

[Kayla Thomas]

In the non mwe, it could be empty.

[Eric Wieser]

Where do you think you are seeing that hypothesis?

[Eric Wieser]

Neither Mario nor I are suggesting you add h : S.Nonempty

[Kayla Thomas]

Oh, oops, misread instance {α} (S : Finset α) : Decidable (∃ a, a ∈ S) := inferInstanceAs (Decidable S.Nonempty).

[Kayla Thomas]

Sorry, thank you.