proving simple inductive types are decidably equal

Stream: new members

[Edward Ayers]

Suppose I make

inductive foo |A |B |C |D |E

How can I show thatfoo is decidably equal with minimal faff?

[Floris van Doorn]

@[derive decidable_eq] inductive foo |A |B |C |D |E

[Edward Ayers]

win for Lean

[Edward Ayers]

What else can I @[derive ...]?

[Floris van Doorn]

Not sure. In mathlib, if I search for derive, I only find derive decidable_eq and derive has_reflect.

[Edward Ayers]

I found has_sizeof in the wild

[Scott Morrison]

I would love to write some "functorial" derive handlers, for automatically showing constructions are functorial with respect to either morphisms in their arguments, or isomorphisms in their arguments. This would be part of a bigger program to do transport of structure.

[Patrick Massot]

Today Cyril worked quite a lot on transport stuff.

[Scott Morrison]

Ah, okay, what approach are they taking?

[Patrick Massot]

parametricity for free, or something like that

[Patrick Massot]

https://hal.inria.fr/hal-01559073

[Scott Morrison]

I would really like some feedback on my iso_induction approach sketched in the comments of https://github.com/leanprover/mathlib/issues/408, and the very initial branch at https://github.com/leanprover-community/mathlib/commit/fc31a8c81040f2a7e087df890f1c848ff6d34eff.

It needs more examples of definitions shown to be functorial in their arguments (hopefully automatically) before you can really see how it would work.