inductive fintype membership

Stream: new members

[Logan Murphy]

this is probably simple, but I'm having some trouble managing it, how can I prove that set membership of an enumerated inductive type is decidable? Looking through Zulip I see that I can derive fintype, but I'm not sure how to leverage it

import data.set tactic
open set


@[derive [fintype, decidable_eq]] inductive atoms
| a
| b
| c
| d

def atom_decidable (s : set atoms) (e : atoms) : decidable (e ∈ s) := sorry

[Alex J. Best]

docs#set.decidable_mem_of_fintype looks like what you want, but its not an instance so apply_instance wouldn't find it.

[Alex J. Best]

Probably you should make this a local instance

[Logan Murphy]

Yeah I tried using that definition, I'm not exactly sure what it means to make it a local instance. If I try to use that definition, I end up with

failed to synthesize type class instance for
s : set atoms,
e : atoms
⊢ fintype ↥s

Do I have to make a separate fintype instance for whatever the coercion on s is?

[Adam Topaz]

It looks like you need a fintype instance for the subtype associated to your set.

[Adam Topaz]

docs#set_fintype

[Reid Barton]

I think this is a common misconception for those not used to constructive reasoning. Decidability of membership in a set has very little to do with the underlying type. For example, {x | p} is a set atoms for every p : Prop, and (for example) a belongs to this set iff p holds, which is not decidable in general.

[Reid Barton]

So your atom_decidable is not valid, or more precisely, equivalent to decidability of all propositions.

[Adam Topaz]

import data.set tactic
open set

@[derive [fintype, decidable_eq]] inductive atoms
| a
| b
| c
| d

def atom_decidable (s : atoms → bool) (e : atoms) : decidable (s e = true) := by apply_instance

:upside_down:

[Adam Topaz]

(And now I'll go back to my mathematician's cave where I can choose things that exist and decide on everything.)

[Logan Murphy]

Thanks guys, appreciate the pointers :)