Josh Cohen (Sep 13 2023 at 03:49): 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.
Yannick Forster (Sep 13 2023 at 16:17):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:18):Pointer 1: https://github.com/NeuralCoder3/nested_induction_v2
Yannick Forster (Sep 13 2023 at 16:19):Pointer 2: https://www.ps.uni-saarland.de/~ullrich/bachelor.php
Last updated: Oct 13 2024 at 01:02 UTC