Stream: Coq users

Topic: Meaning of universe annotation

Julin S (Jan 09 2022 at 05:06):

I did

Set Printing Universes.

Check Type.

and got

Type@{universes.3}
     : Type@{universes.3+1}
(* {universes.3} |=  *)

as output.

Found in 'Explicit universes' section of coq reference manual (couldn't find a web version of that section. Is it not there?) that

universe_name := qualid | Set | Prop
univ_annot := @{universe_level}
universe_level := Set | Prop | Type

So I suppose the universes.3 part is the universe level?

Why does it start with 3 though (when run first)?

Why not 0 or 1?

Gaëtan Gilbert (Jan 09 2022 at 10:29):

it's a anonymous universe, they appear only in printing and not in the parsing grammar
the number starts at 1 but doesn't reset when backtracking

Julin S (Jan 10 2022 at 04:27):

So the numbering does start with 1? I tried running this snippet as the first thing in a buffer after coq started. But the minimum universe level (that's what it is, right) I could get was 3. Is it because something happens during the time coq gets started up?

Meven Lennon-Bertrand (Jan 10 2022 at 13:24):

What might happens is that calling the Check command triggers the elaboration, which itself generates universe levels (including universes.1 and universes.2). But regardless, theses are only names, but they do not refer to one universe being smaller or larger than another (similarly to how the auto-generated variable names H1 and H2 have a priori nothing in common), if that is what you meant by "the minimum universe level".

Meven Lennon-Bertrand (Jan 10 2022 at 13:26):

The trace of the universe hierarchy appears in the list of constraints that is printed after your command (here the (* {universes.3} |= *) tells you there is no such constraint, but if you do

Check Type : Type.

you should see two universe levels in you declaration, together with a constraint that one is strictly smaller than the other.

Gaëtan Gilbert (Jan 10 2022 at 14:33):

Julin S said:

So the numbering does start with 1? I tried running this snippet as the first thing in a buffer after coq started. But the minimum universe level (that's what it is, right) I could get was 3. Is it because something happens during the time coq gets started up?

I get

Type@{foo.1}
     : Type@{foo.1+1}
(* {foo.1} |=  *)

with

Set Printing Universes.
Check Type.

Maybe you have some universe-generating code in your ~/.coqrc?

Julin S (Jan 11 2022 at 06:43):

No my coqrc is empty (don't have one, actually). I was trying it in coqtail plugin of vim. Trying it on proof-general gave me universe level from 1 itself. Maybe I got some setting wrong. Thanks.

Gaëtan Gilbert (Jan 11 2022 at 09:40):

if you do

Set Printing Universes.
Check Type.
Check Type.

what numbers do you get?

Julin S (Jan 11 2022 at 10:33):

Got

Type@{tst1.3}
     : Type@{tst1.3+1}
(* {tst1.3} |=  *)

and

Type@{tst1.4}
     : Type@{tst1.4+1}
(* {tst1.4} |=  *)

Last updated: Oct 03 2023 at 04:02 UTC