Stream: new members

Topic: proving simple inductive types are decidably equal

Edward Ayers (Nov 06 2018 at 15:08):

Suppose I make

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


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

Floris van Doorn (Nov 06 2018 at 15:10):

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


win for Lean

Edward Ayers (Nov 06 2018 at 15:10):

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

Floris van Doorn (Nov 06 2018 at 15:12):

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

Edward Ayers (Nov 06 2018 at 15:12):

I found has_sizeof in the wild

Scott Morrison (Nov 06 2018 at 21:26):

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 (Nov 06 2018 at 21:31):

Today Cyril worked quite a lot on transport stuff.

Scott Morrison (Nov 06 2018 at 21:52):

Ah, okay, what approach are they taking?

Patrick Massot (Nov 06 2018 at 21:53):

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

Scott Morrison (Nov 06 2018 at 21:55):

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.

Last updated: May 13 2021 at 21:12 UTC