Stream: Elpi users & devs

Topic: coq.elaborate-skeleton generates fresh universes


view this post on Zulip Enzo Crance (Nov 09 2022 at 16:28):

Hello.

Consider the universe polymorphic version of the unit inductive:

Inductive unit@{i} : Type@{i} := tt : unit.

Why are L and L1 different in the following code?

  sort (typ S) = {{ Set }},
  coq.univ.variable S Uv,
  coq.univ-instance UI [Uv],
  coq.locate "unit" Unit,
  coq.elaborate-skeleton (pglobal Unit UI) (sort (typ L)) _ ok,
  coq.elaborate-skeleton (pglobal Unit UI) (sort (typ L1)) _ ok.

view this post on Zulip Enrico Tassi (Nov 09 2022 at 17:08):

It is in the spec of elaboration, try @keepunivs!

view this post on Zulip Enrico Tassi (Nov 09 2022 at 17:09):

or coq.typecheck

view this post on Zulip Enzo Crance (Nov 10 2022 at 12:32):

Thanks for the option suggestion. btw I think there was a reason why I started using elaborate-skeleton also for typechecking rather than typecheck, but cannot remember it.

view this post on Zulip Enzo Crance (Nov 10 2022 at 13:13):

The fresh variable generation goes on in the case of Type, even with the option:

@keepunivs! => coq.elaborate-skeleton (sort (typ T)) Ty _ ok,
@keepunivs! => coq.elaborate-skeleton (sort (typ T)) Ty2 _ ok
T = «Test.941»
Ty = sort (typ «Test.943»)
Ty2 = sort (typ «Test.946»)

With typecheck, I get the behaviour I expect (generating that +1) only if I give a variable as output:

coq.typecheck (sort (typ T)) (sort (typ L)) ok,
coq.typecheck (sort (typ T)) A ok
L = «Test.948»
A = sort (typ «Test.941+1»)

view this post on Zulip Enrico Tassi (Nov 10 2022 at 13:38):

keepunivs should change what you discard, try to print it.
About Ty and Ty2, they are variables you can force to be equal with the APIs

view this post on Zulip Enzo Crance (Nov 10 2022 at 15:08):

Is there any way to dodge the fresh universe creation with coq.univ.variable? I can make all my typechecks give always the same value with the example I gave with coq.typecheck and a variable as output, but coq.univ.variable will keep creating a fresh universe variable each time. I'd like to have that «Test.10+1» as a universe variable then as a universe instance, so that:

view this post on Zulip Enrico Tassi (Nov 10 2022 at 15:11):

I'd need more time to investigate, but I have the feeling it is the code to purge algebraics that bothers you. Would you try switching it off?

view this post on Zulip Enzo Crance (Nov 10 2022 at 15:12):

I think I did that already in my local version of Coq-Elpi

view this post on Zulip Enzo Crance (Nov 10 2022 at 15:14):

coq.univ.variable runs into this branch, which calls this auxiliary function. Then as the universe is not a named level but some algebraic stuff (something +1), it takes the None branch and new_univ_blahblahblah

view this post on Zulip Enrico Tassi (Nov 10 2022 at 15:24):

I guess we need to do a visio session next week, this way it will be faster

view this post on Zulip Enzo Crance (Nov 10 2022 at 15:24):

ok maybe I can use Sorts.super to model that +1 directly in the variable


Last updated: Feb 05 2023 at 15:03 UTC