Zulip Chat Archive

Stream: new members

Topic: How to prove decidable_eq for a basic inductive type


view this post on Zulip Sebastián Galkin (Aug 13 2020 at 20:35):

I have a trivial type:

inductive Foo : Type
| A : Foo
| B : Foo
-- .... a few more constructors with no arguments

Trying to prove it is a fintype I need to prove decidable_eq Foo. How would I do that without listing all possible combinations of members of foo in a long pattern match?

instance : decidable_eq Foo
| Foo.A Foo.A := is_true rfl
| Foo.B Foo.B := is_true rfl
-- .....  and now I still need all the possible false combinations

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

Add @[derive decidable_eq] on the line before inductive Foo

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

Over in a different thread https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/integrable_on/near/206626876 we talked about these proofs very recently too.

view this post on Zulip Sebastián Galkin (Aug 13 2020 at 20:43):

Oh that's how you automatically derive instances! Thank you!

Is this covered in some reference manual?

view this post on Zulip Bryan Gin-ge Chen (Aug 13 2020 at 20:46):

Sadly, no. There's an open issue for basic docs here: #3533

view this post on Zulip Chris B (Aug 13 2020 at 20:51):

I've always meant to ask this; why does instance : decidable_eq MyType := by tactic.mk_dec_eq_instance work in some cases when deriving with @[derive decidable_eq] fails? I don't have an example on hand but I swear this is a thing.

view this post on Zulip Mario Carneiro (Aug 13 2020 at 21:16):

I've never witnessed that. Please share the example if you find it

view this post on Zulip Sebastián Galkin (Aug 13 2020 at 21:26):

On the same problem, what is the best way to provide a finset for Foo? (goal is still to prove Foo is a fintype). I have this:

elms  := [A, B].to_finset

but it forces me to list explicitly every constructor. What would be a better way?

In general, shouldn't the fact that Foo is a fintype be automatically derivable?

view this post on Zulip Kenny Lau (Aug 13 2020 at 21:32):

click on the link.

view this post on Zulip Sebastián Galkin (Aug 13 2020 at 21:50):

I couldn't find a strategy in there that doesn't involve an exhaustive listing of all constructors. Am I missing one?

view this post on Zulip Mario Carneiro (Aug 13 2020 at 21:50):

this is on my todo list

view this post on Zulip Mario Carneiro (Aug 13 2020 at 21:51):

ideally you could write @[derive fintype] but the derive handler isn't written

view this post on Zulip Mario Carneiro (Aug 13 2020 at 21:51):

so you have to list the constructors for now

view this post on Zulip Sebastián Galkin (Aug 13 2020 at 21:54):

Thanks for your help folks!

view this post on Zulip Mario Carneiro (Aug 14 2020 at 07:23):

@Sebastián Galkin This has been checked off the todo list as of #3772:

@[derive fintype]
inductive foo (α : Type)
| A : α  foo
| B : α  α  foo
| C : α × α  foo
| D : foo

view this post on Zulip Kenny Lau (Aug 15 2020 at 17:24):

Mario Carneiro said:

Sebastián Galkin This has been checked off the todo list as of #3772:

@[derive fintype]
inductive foo (α : Type)
| A : α  foo
| B : α  α  foo
| C : α × α  foo
| D : foo

which has now been merged


Last updated: May 14 2021 at 13:24 UTC