Hello ! I am trying to get how the universe declarations work when using the Template Monad to create new inductives.
My problem is the following: suppose that I want to add an inductive declaration in the global environment. I start from the inductive, say
list, and I want to replace the reified parameter of
list of type
tSort ... with the same one but of type
tSort fresh_universe . Then, the field
ind_universes of the record corresponding to the new modified inductive should be updated in some way, in order to take into account the new fresh universe. Using simply
fresh_level seems to be unsufficient, as I get the error
Undeclared universe: minimial_example.356 (maybe a bugged tactic).. How can I update the field
Hey Louise :) Can you first share what version of MetaCoq you are using? (opam package / direct installation from which branch / which commit)
Unfortunately this is an old version, as other tools that I use need Coq 8.13:
coq-metacoq 1.0~beta2+8.13 A meta-programming framework for Coq coq-metacoq-erasure 1.0~beta2+8.13 Implementation and verification of an erasure procedure for Coq coq-metacoq-pcuic 1.0~beta2+8.13 A type system equivalent to Coq's and its metatheory coq-metacoq-safechecker 1.0~beta2+8.13 Implementation and verification of safe conversion and typechecking algorithms for Coq coq-metacoq-template 1.0~beta2+8.13 A quoting and unquoting library for Coq in Coq coq-metacoq-translations 1.0~beta2+8.13 Translations built on top of MetaCoq
This will make things hard :/ The 8.14 branch of MetaCoq has features to infer universes properly. Are you tied to this particular MetaCoq version or do you think that you could update to a newer MetaCoq version (while keeping Coq at 8.13)?
Of course updating everything to 8.14 would be best, but probably not realistic
I am not tied to a particular MetaCoq version, however I am a bit surprised that it is possible to compile MetaCoq 8.14 with the 8.13 version of Coq. What are the features available in the 8.14 branch?
I guess Yannick means backporting the changes of 8.14 to 8.13?
Sorry, I was doing 2 steps in my head and only mentioned one. If it is not possible to you to move to 8.14, it might be possible for us to backport universe inference to 8.1... Yes, exactly what Théo says :)
It's not trivial though, because 8.14 and 8.13 differ quite a bit, and the fix affected several files
Thank you, I managed to use MetaCoq 8.14. So how it is possible to infer universes properly and solve my problem in this version?
tmMkInductive operation takes as first argument a
bool. If this is set to
true, universes for the inductive will be inferred when unquoting it
fresh_level should be treated properly
(I haven't used this myself, and I think nobody has apart from a couple of test cases. @Matthieu Sozeau please correct what I said if my description was not accurate)
Your description is accurate. In 8.13, it might also be possible to declare a fresh level by yourself, giving it a name like “myfreshlevel” and adding it to the ind_universes monomorphic context (I am not sure we tested that though). The general idea with universes is that they have to be declared in some context before they can be used.
I think @Marcel Ullrich has tested about every possible combination of things to do on 8.13 to get the right universe context for a non-trivial generated inductive, and in the end our conclusion was that inference of universes is the only way to go
So if I understand well, you recommend using
tmMkInductive rather than
tmMkInductive' in order to let the unquote mechanism infer the universes.
Suppose that my new inductive takes as parameter a term of type
T is a constant and was not present in the environment of the previous inductive. How can I add it in the new environment in order to generate the new inductive ?
Another rather unrelated question is that is encountered several times the term "template polymorphic" and I do not know its meaning
If I understand you correctly, you can just do
T before doing
tmMkInductive in order to have the constant in the environment
Template polymorphism is explained a bit here in the Coq refman: https://coq.inria.fr/refman/language/core/inductive.html#template-polymorphism
The formalisation of MetaCoq does not cover template polymorphism. But, if you just use the template monad and no proofs, this will likely not affect you :) (
tmMkInductive should produce a template polymorphic inductive, but ideally it works so well you don't even notice / you don't even have to know what template polymorphism is)
Thank you Yannick !
This is not exactly what I meant, I'll try to clarify my point. First, I have a term
T defined in my global environment. Then, I use the template monad, starting from an inductive
I does not depend on
T. I construct a new inductive
T occurs in
I'. When I try to generate
I', I have the error that
T does not appear in the environment.
This is not true as the constant
T is already present in the environment, but I guess as the initial inductive does not depend on it, I still get an error message because the recursively quoted term only mentions the dependencies. I can indeed use
tmDefinition to create a copy of
T and use it in my definition of
I' but I would prefer to use
T and not its copy
That sounds like a bug. If you unquote using
tmMkInductive the global context is not mentioned anywhere. So the unquoting should work exactly if and only if a constant with the right name is present in Coq's environment at the time of unquoting
It was not a real bug, there was some mistakes in my construction of
I'. However, the error message was a bit misleading as it mentioned the fact that
T was not in the environment. Not it is fixed and I managed to do what I wanted with the
tmMkInductive of 8.14. Thank you very much !
Last updated: Aug 11 2022 at 03:02 UTC