Zulip Chat Archive

Stream: new members

Topic: proving simple inductive types are decidably equal


view this post on Zulip 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?

view this post on Zulip Floris van Doorn (Nov 06 2018 at 15:10):

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

view this post on Zulip Edward Ayers (Nov 06 2018 at 15:10):

win for Lean

view this post on Zulip Edward Ayers (Nov 06 2018 at 15:10):

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

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Nov 06 2018 at 15:12):

I found has_sizeof in the wild

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Nov 06 2018 at 21:31):

Today Cyril worked quite a lot on transport stuff.

view this post on Zulip Scott Morrison (Nov 06 2018 at 21:52):

Ah, okay, what approach are they taking?

view this post on Zulip Patrick Massot (Nov 06 2018 at 21:53):

parametricity for free, or something like that

view this post on Zulip Patrick Massot (Nov 06 2018 at 21:53):

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

view this post on Zulip 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