The Coq mailing list

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

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> 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