The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 10/12/2015 13:51, Dominique Larchey-Wendling wrote:
> Thank you for your suggestion Guillaume.
> 
>> Print Sorted Universes "universes.txt".
> 
> Reading the generated file, I remark that there
> are two kinds of informations:
> 
> 1/ order constraints like Type.{n} < Type.{n+1}
> 2/ identity constraints like {path}.{number} = Type.{n}
> 
> I have some questions.
> 
> a/ what does the {number} mean ? An occurrence in the source code ?

Kind of. It is a fresh identifier for denoting a universe level. So it
will increase as you progress through you file. But tactics might have
to create fresh Type types, so the counter will increase faster than the
number of Type occurrences in your definitions.

> b/ if Type.2 is the greatest Type.{n} that occurs in the list of
>    constraints, can I deduce that all the loaded theorems can be
>    proved in a restriction of the CIC with a Type hierarchy equal
>    to
>            Prop < Type.0 < Type.1 < Type.2

Kind of. It depends on the typing rules of your formal system. For
instance, you might need an extra Type.* level to encompass all the
Type.i levels. But other than that, yes, the number you obtain is a good
indication of the number of levels you need to prove your theorems

> c/ After Cedric Auger's message, I am a bit confused. It seemed to
>    me that CIC was equal to the limit \bigcup_n CIC(n) where
>    CIC(n) is the restriction of the CIC where n bounds the highest
>    level in the Type hierarchy. It seems (but may be I did not
>    understand well) that Cedric suggests that CIC(n) might even
>    be inconsistent ? In which case, the questions I am asking
>    could be found odd.

Note sure what you mean there. As long as you don't get a typing
judgment Type.i : Type.i, there should be no consistency issue with
respect to universe levels.

Best regards,

Guillaume