The Coq mailing list

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

And another question I have is: are there some principles on when to name a 
universe? If I am designing a library, what are the things I should consider 
for when I should name a universe and when I should not?

Best,
Yao

> On Apr 10, 2020, at 11:09 AM, Yao Li 
> <liyao AT seas.upenn.edu>
>  wrote:
> 
> 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
>>>>> 
>