Zulip Chat Archive

Stream: new members

Topic: inductive fintype membership


view this post on Zulip Logan Murphy (Oct 13 2020 at 20:27):

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

view this post on Zulip Alex J. Best (Oct 13 2020 at 20:33):

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

view this post on Zulip Alex J. Best (Oct 13 2020 at 20:34):

Probably you should make this a local instance

view this post on Zulip Logan Murphy (Oct 13 2020 at 20:37):

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?

view this post on Zulip Adam Topaz (Oct 13 2020 at 20:38):

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

view this post on Zulip Adam Topaz (Oct 13 2020 at 20:38):

docs#set_fintype

view this post on Zulip Reid Barton (Oct 13 2020 at 20:42):

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.

view this post on Zulip Reid Barton (Oct 13 2020 at 20:44):

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

view this post on Zulip Adam Topaz (Oct 13 2020 at 20:50):

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:

view this post on Zulip Adam Topaz (Oct 13 2020 at 20:55):

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

view this post on Zulip Logan Murphy (Oct 13 2020 at 20:56):

Thanks guys, appreciate the pointers :)


Last updated: May 18 2021 at 15:14 UTC