The Coq mailing list

[Yao Li <liyao AT seas.upenn.edu>]

I see. That makes sense.

However, I am getting Foo.2 from a library. Any way to bind it to a stable 
universe outside the library?

Another question is what are the cases that Coq >= 8.10 will automatically 
name universes? When the codebase is large, naming many universes manually 
would be painful...

Best,
Yao

> On Apr 10, 2020, at 10:57 AM, Gaëtan Gilbert 
> <gaetan.gilbert AT skyskimmer.net>
>  wrote:
> 
> The Foo.number universes are unstable (for instance the number changes if 
> you backtrack and rerun the command which generated the universe) so you 
> can't put them into a script.
> Instead you have to ensure they get a name when created (so eg if you have
> 
>    Definition foo := Type. (* produces Type@{Foo.123} *)
> 
> you can replace it by
> 
>    Universe foo_univ.
>    Definition foo := Type@{foo_univ}.
> 
> Coq >=8.10 will automatically name universes in some cases (for instance 
> the above example actually uses the name "foo.u0" not "Foo.123").
> 
> Gaëtan Gilbert
> 
> On 10/04/2020 17:42, Yao Li wrote:
>> Hi Christian,
>> Thanks for the pointers! They are helpful. In particular, I find your 
>> suggestion of using the “Constraint” command quite useful. I would like to 
>> reiterate that suggestion here:
>>> - once one has located the spot where needlessly strong constraints 
>>> (usually
>>> U = V for some U and V) are enforced, one can precede said 
>>> lemma/definition
>>> with a "Contraint" command ruling out the equality (e.g., Contraint U < 
>>> V) to
>>> force backtracking within the definition/lemma. Afterwards, the desired
>>> parallel structure can be reestablished.
>> However, I have universe variables whose names are in the form of “Foo.2”, 
>> which cannot be parsed by Coq, even under “Constraint” command (Coq would 
>> complain:"Error: Syntax Error: Lexer: Undefined token”). This prevents me 
>> from putting any constraints regarding “Foo.2”. Is this a bug or did I 
>> miss something?
>> Best,
>> Yao
>>> On Apr 10, 2020, at 3:30 AM, Christian Doczkal 
>>> <christian.doczkal AT inria.fr
>>>  
>>> <mailto:christian.doczkal AT inria.fr>>
>>>  wrote:
>>> 
>>> Hi,
>>> 
>>> the subject has been discussed on this list before, and I am not aware
>>> of any tooling advances made since then. The two treads I have been
>>> involved in are:
>>> 
>>> https://sympa.inria.fr/sympa/arc/coq-club/2018-09/msg00008.html
>>> https://sympa.inria.fr/sympa/arc/coq-club/2019-11/msg00087.html
>>> 
>>> I hope this helps!
>>> 
>>> Best,
>>> Christian
>>> 
>>> On 4/10/20 1:14 AM, Yao Li wrote:
>>>> Dear All,
>>>> 
>>>> I am having some recurring universe inconsistency problems lately and I 
>>>> would like to know if there are any commands/tools for helping me 
>>>> debugging what happened.
>>>> 
>>>> For example, a recurring pattern is that Coq complains to me that it 
>>>> cannot unify two universe levels (assuming they are u1 and u4) because 
>>>> “u1 <= u2 < u3 <= u4” or “u1 <= u2 < u3 = u4”. I would like to know 
>>>> where the constraints concerning u3 and u4 (and perhaps other relevant 
>>>> constraints as well) are generated—or better yet, why. However, I 
>>>> haven’t found a tool for doing that.
>>>> 
>>>> I have tried “Set Printing Universes”. Unfortunately, the constraints 
>>>> concerning u3 and u4 cannot be found at any relevant definitions. I have 
>>>> also tried “Print Universes”, but I cannot find what I’m looking for in 
>>>> the sea of constraints that Coq shows me.
>>>> 
>>>> Best,
>>>> Yao
>>>>