Zulip Chat Archive

Stream: general

Topic: universe parameters of instances


view this post on Zulip Reid Barton (Jun 03 2018 at 16:33):

Is this a known issue?

class {u v} cat (α : Type u) :=
(β : Type v)
(x : β)

section
universe u
-- OK
example {α : Type u} [cat α] : cat.x α = cat.x α := rfl
end

section
universe u
variables {α : Type u} [cat α]
-- Fails: "invalid reference to undefined universe level parameter 'u_1'"
example : cat.x α = cat.x α := rfl
end

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:34):

It is known in the sense that it is a design that's hard to work with.

view this post on Zulip Reid Barton (Jun 03 2018 at 16:34):

It seems that the elaborator fails to gather the second universe variable of cat

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:35):

If you absolutely need to use it, you need to specify the universes as cat.{u v} α

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:35):

It makes it unpleasant to use though

view this post on Zulip Reid Barton (Jun 03 2018 at 16:35):

That makes no difference (except the error message complains about v now)

view this post on Zulip Reid Barton (Jun 03 2018 at 16:35):

I think this one is just a bug

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:36):

I don't think so. Can you try cat.{v u} α instead?

view this post on Zulip Reid Barton (Jun 03 2018 at 16:36):

why {v u}?

view this post on Zulip Reid Barton (Jun 03 2018 at 16:37):

section
universes u v
variables {α : Type u} [cat.{u v} α]
-- Fails: "invalid reference to undefined universe level parameter 'v'"
example : cat.x α = cat.x α := rfl
end

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:37):

Sometimes, the order of the universes is weird

view this post on Zulip Reid Barton (Jun 03 2018 at 16:37):

{v u} gives many worse errors

view this post on Zulip Reid Barton (Jun 03 2018 at 16:37):

I think if we could just, like, include the universe parameter v, then this would work

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:37):

Is the error on the equality?

view this post on Zulip Reid Barton (Jun 03 2018 at 16:37):

The error is located on the word example

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:38):

You may need cat.x.{u v} α = cat.x.{u v} α

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:39):

This here works for me:

section
universes u v
variables {α : Type u} [cat.{u v} α]
example : cat.x.{u v} α = cat.x α := rfl
end

view this post on Zulip Reid Barton (Jun 03 2018 at 16:40):

That does work

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:41):

Can you show me an example where using two universes is necessary? Maybe I can show you a way around it

view this post on Zulip Reid Barton (Jun 03 2018 at 16:41):

But, this also works

view this post on Zulip Reid Barton (Jun 03 2018 at 16:41):

section
universes u v
variables {α : Type u} [cat.{u v} α]
-- OK
example : cat.x α = cat.x α  nonempty (punit.{v}) := rfl, ⟨⟨⟩⟩⟩
end

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:43):

That makes sense. Every definition and theorem has an implicit list of free universe variables. The type of example did not mention v which meant that the instance of cat it needed was not necessarily parameterized by v

view this post on Zulip Reid Barton (Jun 03 2018 at 16:43):

So it really seems that the elaborator just does not understand that it ought to bind the universe variable v

view this post on Zulip Reid Barton (Jun 03 2018 at 16:44):

The type of example does mention v though

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:44):

I don't think I would say that it ought to.

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:45):

Only the versions that work

view this post on Zulip Reid Barton (Jun 03 2018 at 16:45):

No, all of them

view this post on Zulip Reid Barton (Jun 03 2018 at 16:45):

since they are really ∀ {α : Type u} [_inst_1 : cat.{u v} α], ...

view this post on Zulip Reid Barton (Jun 03 2018 at 16:46):

Consider the other original working version, which did not use variables

view this post on Zulip Reid Barton (Jun 03 2018 at 16:47):

Its full inferred type is ok.{u_1 u_2} : ∀ {α : Type u_1} [_inst_1 : cat.{u_1 u_2} α], cat.x.{u_1 u_2} α = cat.x.{u_1 u_2} α

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:47):

v does not appear in it either. It is inferred

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:48):

Since it's not specified, it's found through unification. v starts off as a universe meta variable and cat and cat.x start off with different universe variables, we do instance resolution and then unification and then they are forced to be the same.

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:49):

The the example with variable, the cat instance already has a universe so it's not inferred during elaboration

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:50):

Universe polymorphism is a pretty nasty can of worms. Keep it to a minimum. ulift can help you with that.

view this post on Zulip Reid Barton (Jun 03 2018 at 16:51):

I have to say I still don't really buy any of this!

view this post on Zulip Reid Barton (Jun 03 2018 at 16:52):

section
universes u v
variables {α : Type u} [cat.{u v} α] {γ : Type v} (y : γ)
-- OK
def foo : cat.x α = cat.x α  nonempty γ := rfl, y⟩⟩
end

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:52):

This is consistent with my explanation

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:53):

Think of it as matching universe levels by name.

view this post on Zulip Reid Barton (Jun 03 2018 at 16:55):

FWIW, this is the full error message with the failing version

kernel failed to type check declaration 'test' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
   {α : Type u} [_inst_1 : cat.{u v} α],
    @eq.{v+1} (@cat.β.{u v} α _inst_1) (@cat.x.{u v} α _inst_1) (@cat.x.{u v} α _inst_1)
elaborated value:
  λ {α : Type u} [_inst_1 : cat.{u v} α], @rfl.{v+1} (@cat.β.{u v} α _inst_1) (@cat.x.{u v} α _inst_1)
nested exception message:
invalid reference to undefined universe level parameter 'v'

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:56):

In cat.x we don't what the universes will be so they start off as meta variables. α brings in universe u and γ brings in v

view this post on Zulip Reid Barton (Jun 03 2018 at 16:56):

So why doesn't the instance resolution of cat.x bring in v?

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:57):

Because its v is a local v to the class.

view this post on Zulip Reid Barton (Jun 03 2018 at 16:58):

It's using this variable _inst_1 whose type mentions v, and when I make it use the variables γ and y then it understands that it should bring in v.

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:58):

I just tried:

universes u v

class cat (α : Type u) :=
(β : Type v)
(x : β)

and that doesn't work either. That's weird

view this post on Zulip Simon Hudon (Jun 03 2018 at 16:59):

Ok, I'm not sure now. Maybe @Sebastian Ullrich or @Gabriel Ebner can come clear this up

view this post on Zulip Reid Barton (Jun 03 2018 at 17:03):

I guess it cannot "see" the dependence on the variable which was used through instance resolution as easily as it can see a direct reference

view this post on Zulip Reid Barton (Jun 03 2018 at 17:08):

Or, here is another way to look at it. Intuitively, I expect variables <bindings> to prepend <bindings> to the parameters of every definition/lemma. Well that's not quite true, I only expect bindings that are used somehow to get prepended.

view this post on Zulip Reid Barton (Jun 03 2018 at 17:09):

Here lean obviously understands that it needs to include the cat instance, since otherwise there would be an error earlier about cat.x. But, if I just manually prepend both variables, as in the first example, then it works fine.

view this post on Zulip Reid Barton (Jun 03 2018 at 17:10):

aha, here is another workaround!

section
universes u v
variables {α : Type u} [inst : cat α]
include inst
-- OK
def ok : cat.x α = cat.x α := rfl
end

view this post on Zulip Reid Barton (Jun 03 2018 at 17:18):

not very surprising that that works, but certainly a palatable workaround. Actually, this could nicely solve my "upgrading" type class issue too. Just name both instances as variables and then include the one you want at any given time and hide it when done.

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:03):

Thanks for the interesting discussion here! I've absolutely run into this in my category theory library. Unfortunately, universe issues are a pain. Unavoidably, one needs to be able to discuss "small_category", where objects and morphisms live in the same universe, and "large_category", where objects live in a universe one higher than the morphisms.

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:04):

Rather than develop these in parallel (and deal with the combinatorial explosion of functors and natural transformations going between the worlds), I've settled on the somewhat ugly solution of having a single "category", with

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:04):

abbreviation large_category (C : Type (u+1)) : Type (u+1) := category.{u+1 u} C
abbreviation small_category (C : Type u)     : Type (u+1) := category.{u u} C

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:05):

If you're only dealing with small or large categories (or even one of each at the same time), everything works nicely, and typeclass inference remains your friend.

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:06):

If you're trying to write library code that covers both cases, it is slightly ugly, and we need to specify universes explicitly and do a certain amount of "including" typeclass instances.

view this post on Zulip Reid Barton (Jun 04 2018 at 00:06):

As you might have guessed, cat stands for your category class.
In my so far limited use, I haven't had any issues just using category directly where mathematically reasonable, aside from the issue discussed in this topic, which I now have a workaround for.

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:06):

I have to write:

variable {C : Type u₁}
variable [𝒞 : category.{u₁ v₁} C]
variable {D : Type u₂}
variable [𝒟 : category.{u₂ v₂} D]
include 𝒞 𝒟

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:06):

quite often!

view this post on Zulip Reid Barton (Jun 04 2018 at 00:06):

Aha, so you already discovered the include workaround I guess.

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:07):

(But that said, that's usually as ugly as it gets, and after those includes everything works pretty naturally.)

view this post on Zulip Reid Barton (Jun 04 2018 at 18:50):

Here's another, admittedly silly workaround for the issue here:

def {u v} Type₂ : Type (u+1) := Type u
variables {C : Type₂.{u v}} [category.{u v} C]

Now the type of C mentions v, so the elaborator correctly includes v

view this post on Zulip Thang Nguyen (Jun 08 2018 at 15:59):

Hi, I am new in lean programming. I am attending to Hanoi FABS summer school 2018 and really interested in doing.
My homework is formalizing the statement of Polignac Conjecture: For every even number 2n, there are infinitely many pairs of consecutive primes which differ by 2n.
I have formalized and wonder regarding that:

def Polignac :Prop :=  n, isEven n   m,  p q > m, isPrime p  isPrime q  ((p - q) = n  (q - p) =n)

I need your help!

view this post on Zulip Simon Hudon (Jun 08 2018 at 16:02):

Can you be a bit more specific? Why do you wonder about that definition? Or more precisely, what is giving you trouble about that definition?

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:02):

It would be easier to actually use n as in the informal statement (and write 2*n where you want 2n

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:02):

And the disjunction at the end is unnecessary

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:05):

Note also that your attempt says nothing about p and q being consecutive

view this post on Zulip Thang Nguyen (Jun 08 2018 at 16:08):

I need to define the statement of Polignac Conjecture. And I defined it and dont know that is okay.

view this post on Zulip Thang Nguyen (Jun 08 2018 at 16:09):

Note also that your attempt says nothing about p and q being consecutive

so how to fix to p q consecutive

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:10):

What you wrote is not the correct statement, even assuming isEven and isPrime are defined

view this post on Zulip Simon Hudon (Jun 08 2018 at 16:11):

You'd need to say every number between p and q is not prime. Using a different definition for that may be best

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:11):

You could add a condition that no natural number between p and q (p and q excluded) is prime

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:11):

And you don't need to have a notation for q

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:11):

You really want n, a prime p and asserting that p+2*n is also prime

view this post on Zulip Patrick Massot (Jun 08 2018 at 16:12):

and there is no prime number in between

view this post on Zulip Thang Nguyen (Jun 08 2018 at 16:20):

That is correct?

def Polignac :Prop :=  n m: nat,  p : nat, isPrime m  (m = p  m = (p + 2*n))

view this post on Zulip Patrick Massot (Jun 08 2018 at 17:07):

No, it's not

view this post on Zulip Andrew Ashworth (Jun 08 2018 at 18:03):

today I learned about https://en.wikipedia.org/wiki/Sexy_prime

view this post on Zulip Simon Hudon (Jun 08 2018 at 18:04):

I learned that when I got married: our age is 6 apart and both of our ages were prime numbers. It's probably partly responsible for my saying yes

view this post on Zulip Patrick Massot (Jun 08 2018 at 18:33):

(23, 29)?

view this post on Zulip Simon Hudon (Jun 08 2018 at 18:36):

(31,37)

view this post on Zulip Andrew Ashworth (Jun 08 2018 at 18:51):

Going back to his question, I feel like you would want to define a prime gap counting function, as in wikipedia (the number of prime gaps of size n below x). Then you take the limit as x goes to infinity. Is that a standard way to formalize it?

view this post on Zulip Johan Commelin (Jun 08 2018 at 18:52):

Given kthe size of the gaps, I would write: \forall n, \ex p, p > n \and is_prime_gap p k

view this post on Zulip Johan Commelin (Jun 08 2018 at 18:53):

And then you need to express that p and p+k have a prime gap of size k in is_prime_gap p k : Prop

view this post on Zulip Scott Morrison (Jun 11 2018 at 08:38):

@Thang Nguyen, just a suggestion --- in zulipchat you can set the "topic" name for a conversation, and it helps organise the conversation here a lot! For example, this one could have been "help with a statement about primes".


Last updated: May 10 2021 at 00:31 UTC