Stream: Elpi users & devs

Topic: coq.elaborate-skeleton generates fresh universes

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.

Enrico Tassi (Nov 09 2022 at 17:08):

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

Enrico Tassi (Nov 09 2022 at 17:09):

or coq.typecheck

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.

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»)

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

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:

• my code doing substitutions with copy will syntactically match terms correctly (if universe instances don't match it does not work);
• when giving the final term to coq.env.add-const it will not add extra binders to the universe instance.

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?

Enzo Crance (Nov 10 2022 at 15:12):

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

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

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

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: Apr 19 2024 at 04:02 UTC