The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

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