Stream: MetaCoq

Topic: Theorems about inductive type descriptions


view this post on Zulip Josh Cohen (Sep 13 2023 at 03:49):

I have not used MetaCoq, just looked at a few of the papers, so I apologize if this is a silly question. I am wondering about the semantics defined in MetaCoq for structures like inductive types, and to what extent it is possible to prove theorems about them without unquoting specific instances into Coq. For example, can I prove that, given a MetaCoq description of an inductive datatype, that the MetaCoq descriptions of the constructors are disjoint (and/or that different constructors, no matter the arguments applied, will unquote to non-equal Coq terms)? Thanks

view this post on Zulip Théo Winterhalter (Sep 13 2023 at 06:23):

We don't prove anything about the unquoted terms, but semantically we can prove injectivity of constructors yes.

view this post on Zulip Josh Cohen (Sep 13 2023 at 15:19):

Thank you. Are these theorems provable about generic inductive types, or only for particular instances (i.e. something like forall i: inductive, constr_disjoint(i) vs constr_disjoint(tree))? And separately, could one prove an induction theorem about the inductive type descriptions?

view this post on Zulip Théo Winterhalter (Sep 13 2023 at 15:22):

I mean, I think it is practically baked in the specification of definitional equality. So I would say yes this should be provable generically.

I'm not sure I understand what you mean for the second one? Do you mean a generic function that would compute an eliminator? Then if so, I would think the answer is yes, but I don't think we've done it, and it's probably a pain for mutually nested inductive types.

view this post on Zulip Josh Cohen (Sep 13 2023 at 15:39):

Yes, I think that a generic function to compute an eliminator is what I mean. Thank you, this was helpful.

view this post on Zulip Yannick Forster (Sep 13 2023 at 16:17):

We have!

view this post on Zulip Yannick Forster (Sep 13 2023 at 16:17):

Even for nested mutual inductives

view this post on Zulip Yannick Forster (Sep 13 2023 at 16:17):

Modulo universe bugs

view this post on Zulip Yannick Forster (Sep 13 2023 at 16:17):

If somebody wants to pick that up, I'd be happy to discuss

view this post on Zulip Yannick Forster (Sep 13 2023 at 16:18):

Pointer 1: https://github.com/NeuralCoder3/nested_induction_v2

view this post on Zulip Yannick Forster (Sep 13 2023 at 16:19):

Pointer 2: https://www.ps.uni-saarland.de/~ullrich/bachelor.php


Last updated: Jul 23 2024 at 20:01 UTC