Stream: MetaCoq

Topic: Adding constraints to Record based on Parameters and Fields

view this post on Zulip Angelo Taranto (Nov 30 2023 at 19:10):

Hi all, I am struggling with a constraints problem. I am creating a Record (or Inductive, to be specific) via MetaCoq from a given Record, which may have fields of type Type and input parameters of type Type. This is the case for an example I am working with. When creating the new record from the old, if I don't modify the ind_universes field of the new mutual_inductive_body (i.e. I don't feed it the old ind_universes), I run into errors. Attempting to, for the moment, hand-code in new constraints (Usually to quell errors of needing a constraint Type <= Type), I run into errors like Undeclared universe: Var(1) (maybe a bugged tactic) when referencing the level of one of the type Types in the original record. I get the levels by printing the mutual inductive body and seeing what types the parameters and constructor has.

My question: is there a more automatic way to do this? If I had to do it all by hand, I'd have to write a function which perused the constructors (the members of a tProd in the mutual inductive body's ind_bodies.(ind_ctors)) and if one were of type Type (not sure how to even do that part), I would add the term to a dictionary along with its level, then access that dictionary to add constraints like ind_universes := Polymorphic_ctx (AUContext.inter (AUContext.make [nAnon] (ConstraintSet.singleton (UnivConstraint.make (Var 1) (ConstraintType.Le 0) (Var 0)))) (AUContext.make [nAnon] (constraints_of_udecl mind.(ind_universes))) ) ; where the Var _s come from that dictionary. But when I create a Record in vanilla Coq, all of these constraints are handled automatically. Is there some internal function in Coq or MetaCoq which can dispatch constraints given the fields I want in a Record?

Last updated: Jul 23 2024 at 21:01 UTC