universe parameters of instances

Stream: general

[Reid Barton]

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

[Simon Hudon]

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

[Reid Barton]

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

[Simon Hudon]

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

[Simon Hudon]

It makes it unpleasant to use though

[Reid Barton]

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

[Reid Barton]

I think this one is just a bug

[Simon Hudon]

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

[Reid Barton]

why {v u}?

[Reid Barton]

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

[Simon Hudon]

Sometimes, the order of the universes is weird

[Reid Barton]

{v u} gives many worse errors

[Reid Barton]

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

[Simon Hudon]

Is the error on the equality?

[Reid Barton]

The error is located on the word example

[Simon Hudon]

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

[Simon Hudon]

This here works for me:

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

[Reid Barton]

That does work

[Simon Hudon]

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

[Reid Barton]

But, this also works

[Reid Barton]

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

[Simon Hudon]

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

[Reid Barton]

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

[Reid Barton]

The type of example does mention v though

[Simon Hudon]

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

[Simon Hudon]

Only the versions that work

[Reid Barton]

No, all of them

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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} α

[Simon Hudon]

v does not appear in it either. It is inferred

[Simon Hudon]

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.

[Simon Hudon]

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

[Simon Hudon]

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

[Reid Barton]

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

[Reid Barton]

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

[Simon Hudon]

This is consistent with my explanation

[Simon Hudon]

Think of it as matching universe levels by name.

[Reid Barton]

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'

[Simon Hudon]

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

[Reid Barton]

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

[Simon Hudon]

Because its v is a local v to the class.

[Reid Barton]

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.

[Simon Hudon]

I just tried:

universes u v

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

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

[Simon Hudon]

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

[Reid Barton]

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

[Reid Barton]

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.

[Reid Barton]

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.

[Reid Barton]

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

[Reid Barton]

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.

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Reid Barton]

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.

[Scott Morrison]

I have to write:

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

[Scott Morrison]

quite often!

[Reid Barton]

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

[Scott Morrison]

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

[Reid Barton]

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

[Thang Nguyen]

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!

[Simon Hudon]

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?

[Patrick Massot]

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

[Patrick Massot]

And the disjunction at the end is unnecessary

[Patrick Massot]

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

[Thang Nguyen]

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

[Thang Nguyen]

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

so how to fix to p q consecutive

[Patrick Massot]

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

[Simon Hudon]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

and there is no prime number in between

[Thang Nguyen]

That is correct?

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

[Patrick Massot]

No, it's not

[Andrew Ashworth]

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

[Simon Hudon]

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

[Patrick Massot]

(23, 29)?

[Simon Hudon]

(31,37)

[Andrew Ashworth]

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?

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

@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".