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?

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?

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

In particular, `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`

, 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

If I understand you correctly, you can just do `tmDefinition`

with `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,`

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

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: Oct 08 2024 at 16:02 UTC