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

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

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?

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.

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

We have!

Even for nested mutual inductives

Modulo universe bugs

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

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

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

Last updated: Jul 23 2024 at 20:01 UTC