How to prove decidable_eq for a basic inductive type

Stream: new members

[Sebastián Galkin]

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

[Alex J. Best]

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

[Alex J. Best]

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.

[Sebastián Galkin]

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

Is this covered in some reference manual?

[Bryan Gin-ge Chen]

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

[Chris B]

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.

[Mario Carneiro]

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

[Sebastián Galkin]

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?

[Kenny Lau]

click on the link.

[Sebastián Galkin]

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

[Mario Carneiro]

this is on my todo list

[Mario Carneiro]

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

[Mario Carneiro]

so you have to list the constructors for now

[Sebastián Galkin]

Thanks for your help folks!

[Mario Carneiro]

@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

[Kenny Lau]

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