## Stream: MetaCoq

### Topic: Theorems about inductive type descriptions

#### 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

#### 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.

#### 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?

#### 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.

#### 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.

We have!

#### Yannick Forster (Sep 13 2023 at 16:17):

Even for nested mutual inductives

#### Yannick Forster (Sep 13 2023 at 16:17):

Modulo universe bugs

#### Yannick Forster (Sep 13 2023 at 16:17):

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

#### Yannick Forster (Sep 13 2023 at 16:19):

Last updated: Jul 23 2024 at 20:01 UTC