Louise Dubois de Prisque (May 04 2022 at 09:56): Louise Dubois de Prisque (May 04 2022 at 09:56):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 ind_universe properly?
Yannick Forster (May 04 2022 at 10:06):Hey Louise :) Can you first share what version of MetaCoq you are using? (opam package / direct installation from which branch / which commit)
Louise Dubois de Prisque (May 04 2022 at 10:18):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)?
Yannick Forster (May 04 2022 at 10:34):Of course updating everything to 8.14 would be best, but probably not realistic
Louise Dubois de Prisque (May 04 2022 at 15:17):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?
Théo Winterhalter (May 04 2022 at 15:18):I guess Yannick means backporting the changes of 8.14 to 8.13?
Yannick Forster (May 04 2022 at 15:18):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 :)
Yannick Forster (May 04 2022 at 15:19):It's not trivial though, because 8.14 and 8.13 differ quite a bit, and the fix affected several files
Louise Dubois de Prisque (May 05 2022 at 13:40):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?
Yannick Forster (May 06 2022 at 08:25):The tmMkInductive operation takes as first argument a bool. If this is set to true, universes for the inductive will be inferred when unquoting it
Yannick Forster (May 06 2022 at 08:25):In particular, fresh_level should be treated properly
Yannick Forster (May 06 2022 at 08:26):(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)
Matthieu Sozeau (May 06 2022 at 08:34):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.
Yannick Forster (May 06 2022 at 08:35):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
Louise Dubois de Prisque (May 06 2022 at 13:56):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, where 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
Yannick Forster (May 06 2022 at 14:05):If I understand you correctly, you can just do tmDefinition with T before doing tmMkInductive in order to have the constant in the environment
Yannick Forster (May 06 2022 at 14:06):Template polymorphism is explained a bit here in the Coq refman: https://coq.inria.fr/refman/language/core/inductive.html#template-polymorphism
Yannick Forster (May 06 2022 at 14:09):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)
Louise Dubois de Prisque (May 06 2022 at 14:34):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, and I does not depend on T. I construct a new inductive I' from I, but 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
Yannick Forster (May 06 2022 at 14:46):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
Louise Dubois de Prisque (May 06 2022 at 17:30):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: Oct 08 2024 at 16:02 UTC