Stream: Coq devs & plugin devs

Topic: Universe levels and section discharge


view this post on Zulip Kenji Maillard (Dec 15 2021 at 15:53):

From working with polymorphic universe levels in sections, I have an experimental understanding that whenever a polymoprhic universe variable is "allocated" within a section, then all the following definitions will polymorphically bound this variable. This intuition is supported by the following code that make me a bit crazy:

Set Universe Polymorphism.
Set Printing Universes.

Cumulative Record F@{v} (X : Type@{v}) : Type@{v} := { R : Set }.

Definition foo0@{u} (A : Type@{u}) (FA : F@{u} A) (aa : R A FA) := tt.

Section Blah.
  Universe u.
  Context (A : Type@{u}) (FA : F@{u} A) (aa : R A FA).
  Definition foo1 := tt.
End Blah.
Print foo1.
(* No argument but one universe bound *)

Section Blah.
  Universe u.
  Context (A : Type@{u}) (FA : F@{u} A).
  Section Deeper.
    Context (aa : R A FA). (* A fresh universe is created here *)
    Definition foo2 := tt.
  End Deeper.
End Blah.
Print foo2.
(* No argument but two universes bound *)

The coq documentation only states that two definitions in the section sharing a common variable will both get parameterized by the universes produced by the variable declaration and does not specify which universe levels will not be bound at discharge time. This incomplete specification makes it a bit hard to work with universes explicitly...

Is there any hope for a discharge mechanism for polymorphic universe levels working similarly to usual arguments ?

view this post on Zulip Gaëtan Gilbert (Dec 15 2021 at 15:56):

the doc says "This means that the universe variables and their associated constraints are discharged polymorphically over definitions that use them" which is wrong, but later (at the end) it says "constants and inductives are abstracted by all the section's polymorphic universes and constraints" which is almost correct (it's only the universes declared before that constant)

view this post on Zulip Gaëtan Gilbert (Dec 15 2021 at 15:56):

Is there any hope for a discharge mechanism for polymorphic universe levels working similarly to usual arguments ?

it should be possible, I don't think anyone is working on it at this time

view this post on Zulip Kenji Maillard (Dec 15 2021 at 16:26):

So documentation should be fixed, and the discharge feature for universe level addeed to the wishlist for christmas ?

view this post on Zulip Gaëtan Gilbert (Dec 15 2021 at 16:27):

christmas next year maybe ;)


Last updated: Dec 06 2023 at 14:01 UTC