Assistance Getting Rid of Superfluous Universe levels?

Using Coq
1

Dear Coq Discourse,

I have a question about instantiating Polymorphic universes, in particular how discharge/remove one universe from a definition and set it to a universe level that depends on the others. question is as follows:

Question

Suppose I have a lemma of the form:

MyLemma@{a b c} : Mysort {a b c |= a < c b <= c}

where the universe c comes from some definitions that are made due to the internals of the theory that I am writing. For the type I want to instantiate, c’s universe level does not matter, and I need it gone for it to be correct w.r.t. to a module type’s definitions for the module which MyLemma will instantiate a Parameter of.

My first naive attempt at a solution is the following, to make a dummy lemma that gets rid of y as follows:
MyLemma'@{a b} :=MyLemma@{a b max(a+1,b)}

If this was allowed my problem is solved immediately. However, I get the following error Syntax error: [univ_level_or_quality] or '|' or '}' expected (in [univ_annot])., so it seems that this way of specifying universes is not allowed in Coq.

I have also tried a tricksy way of solving this problem by loading the required universe into dummy arguments, i.e. doing something like the following to pull in the correct universe:

Definition y@{a b c}:=(fun (A:Type@{a}) (B:Type@{b}) (C:Type@{c}) => Type@{c}).
Definition g@{a b} := (fun (A:Type@{a}) (B:Type@{b}) (C:Type@{max(a+1,b)}) => (y@{a b _} A B C) ).

However in this instance I get an (expected) universe unbound error. I tried finagling it a little to get it to work but could not.

Lastly I have tried looking into the docs on this issue but didn’t really get all that in the way of understanding all that was said there. I did look and see that there is some thing called Private Polymorphic Universes which looked at least in the same ball park as what I’m trying to achive - though I couldn’t figure out how to use it or if I want to opaque the lemmas in the first place.

Does Coq have any mechanism to solve the problem I am experiencing, otherwise it means I will have to bake lots of nonsensical random universe levels into my module types in a way that is ultimately brittle and unnecessary?

2

There is ongoing work to allow instantiating polymorphic universes with arbitrary expressions but it is not finished Algebraic universes everywhere and new constraint algorithm by mattam82 · Pull Request #19537 · coq/coq · GitHub

Private Polymorphic Universes s automatic but only works with Qed lemmas

When the universe you want to instantiate is an upper bound of everything it may work to do

Monomorphic Universe Ubig_for_lemma.
Definition lemma'@{a b} := lemma@{a b Ubig_for_lemma}.
1 Like
3

Thanks for the quick response, this approach seems to partially help, but not quite one-shot the problem, explanation following:

Lets say I do something like this as you propose:

Section S.
Monomorphic Universe Ubig_for_lemma.
Definition lemma'@{a b} := lemma@{a b Ubig_for_lemma}.
End S.

this changes my polymorphic binders to @{a b |= a < Ubig_for_lemma, b <= Ubig_for_lemma}, which partially solves the problem. But then means one has a constant universe that bounds everything which I firstly don’t want for my theory and secondly also still does not satisfy the universe constraints I want for my module type which is @{a b |= }. I presume this is what you meant when you said

When the universe you want to instantiate is an upper bound of everything it may work:

I don’t have a general universe that will always act as an upper limit. This is part of the reason why I want to literally instantiate the universe c away. I’m possibly going to see if I can rewrite an explicit version of the lemma which gets rid of c, but doing that at scale is extremely brittle and requires a lot of code-duplication.

I presume when the ongoing work / feature finishes, (if my understanding of the phrase allow instantiating polymorphic universes with arbitrary expressions is correct), I can just write MyLemma'@{a b} :=MyLemma@{a b max(a+1,b)} as originally planned? If so I’m fine to just polyfill some lemmas or more easily temporally add some dummy universes to my module type and remove them later.

Perchance do you know of a rough timescale of when that feature should become part of mainline coq? If I want to keep up with being notified of the development of this feature is it sufficient to follow the linked git-issue?

Best,

4

I would generally not expect module subtyping and universe polymorphism to work well together.

if my understanding of the phrase allow instantiating polymorphic universes with arbitrary expressions is correct), I can just write MyLemma’@{a b} :=MyLemma@{a b max(a+1,b)} as originally planned?

yes

Perchance do you know of a rough timescale of when that feature should become part of mainline coq?

I am not 100% convinced that the performance issues can be solved so there is a risk that it will never be merged.

1 Like
5

Thanks for that info, I’ll proceed with that in mind