Universes

Stream: lean4

[Calvin Lee]

Can I use a type with two different universes in the same declaration?
e.g. if I have def foo {m : Type u -> Type v} can I use m with two different universes in the same formula?

[Kyle Miller]

If they're different m's, then yes. You can even be explicit with universes if needed. Here's setting u=0 and v=1: foo.{0, 1}. This notation works with universe variables, too.

[Floris van Doorn]

In the definition of foo you cannot use m with a different universe level: you only have one m that has type Type u -> Type v, and u and v are fixed in the definition of foo.
After you have declared foo you can use it with u and v instantiated however you want.

[Calvin Lee]

Is there any way to make a tuple of items in two different universes? e.g. could I have def foo {m : Type u -> Type v} {a : Type u} ... : Option (m a, a) because I'm trying to do something like this and getting some type errors

[Kyle Miller]

(deleted)

[Mario Carneiro]

I think you want Option (m a × a)

[Mario Carneiro]

and this should work even if m a and a are in different universes

[Floris van Doorn]

If you have a pair, you can just take a product.
If you need a sequence with n elements, this gets inconvenient, but it is possible with Ulift.

[Kind Bubble]

I want my definition of category to depend on a choice of universe or something like that. Here's what I've got going right now:

notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
notation "Σ" "(" X ":" A ")" ":" F => Σ' (X : A), F
notation "Π" "(" X ":" A ")" ":" F => forall (X : A), F
notation "*" => Unit.unit
notation "⊛" => Unit
notation x "==" y => Σ(_:x=y):⊛

def Cat :=
Σ(Obj:Type 1):
Σ(Hom:Π(_:Obj):Π(_:Obj):(Type 1)):
Σ(Id:Π(X:Obj):(Hom X X)):
Σ(Comp:Π(X:Obj):Π(Y:Obj):Π(Z:Obj):Π(_:Hom X Y):Π(_:Hom Y Z):(Hom X Z)):
Σ(_:Π(X:Obj):Π(Y:Obj):Π(f:Hom X Y):(Comp X Y Y) f (Id Y) == f):
Σ(_:Π(X:Obj):Π(Y:Obj):Π(f:Hom X Y):(Comp X X Y) (Id X) f == f):
Σ(_:Π(W:Obj):Π(X:Obj):Π(Y:Obj):Π(Z:Obj):Π(f:Hom W X):Π(g:Hom X Y):Π(h:Hom Y Z):(Comp W X Z) f (Comp X Y Z g h) == Comp W Y Z (Comp W X Y f g) h):
⊛

As you can see, Cat is a 7-tuple. I hope my notation isn't too purist.

But I would like to switch Type 1 for something more general. How would I make it depend on a universe?

[Adam Topaz]

What happens if you replace the 1s with _? Or with universe parameters?

[Adam Topaz]

Also, what's the reason for introducing these notations?

[Kind Bubble]

Adam Topaz said:

What happens if you replace the 1s with _? Or with universe parameters?

I don't know about this yet. How does that work? And what is the most general option?

[Adam Topaz]

An underscore will be an unspecified universe parameter, making your definition universe polymorphic.

[Kind Bubble]

Adam Topaz said:

An underscore will be an unspecified universe parameter, making your definition universe polymorphic.

ok this is good.

[Kind Bubble]

Kind Bubble said:

Adam Topaz said:

An underscore will be an unspecified universe parameter, making your definition universe polymorphic.

ok this is good.

And this will work for any universe now? Is the underscore the most general option?

[Adam Topaz]

An underscore will be (essentially) equivalent to introducing arbitrary universe variables and replacing the 1s with those variables.

[Adam Topaz]

If you want to specify the universe parameters in a certain order, which can be useful sometimes (particularly in category theory!!) then you should introduce and use those variables explicitly

[Kind Bubble]

Adam Topaz said:

An underscore will be (essentially) equivalent to introducing arbitrary universe variables and replacing the 1s with those variables.

Ok thanks for your help. This is good.

[James Gallicchio]

You can also explicitly introduce universes with the def Cat.{u,v} := ... syntax, using u and v as levels like Type u and Type v. The main advantage of doing so is that the _ might be filled in with concrete universe levels (if something constrains them to a concrete level), whereas the explicit universes will raise a type error if accidentally constrained somehow.

[Antoine Chambert-Loir]

I know you've read here that universes don't matter, but I would like to implement the type of trees that gives (would give) rise to Russell's paradox, as explained in Thorsten Altenkirch's notes.

Here, a tree is just a note followed by a collection of true. Here is a possible definition, where the collection is a member of Type 0:

inductive TATree : Type 1
  | node : (Σ (I : Type 0), I → TATree) → TATree

This gives TATree : Type 1, but I would like to allow more general collections, say, I : Type u, for some universe u, and I didn't manage the provide a definition that the compiler would accept.

[Notification Bot]

A message was moved here from #lean4 > IO.Process.spawn doesn't work on Windows by Antoine Chambert-Loir.

[Antoine Chambert-Loir]

The error message in

inductive TBTree : Type v -- doesn't work
  | node : (Σ (I : Type u), I → TBTree) → TBTree

suggests to me that the result (in Type v) should be at max (u + 2) (v + 1), so that any universe v such that u + 1 ≤ vshould work.
But

inductive TCTree : Type (u + 1)
  | node : (Σ (I : Type u), I → TCTree) → TCTree

gives an even more cryptic error message.

[Robin Arnez]

inductive TCTree : Type (u + 1)
  | node : (I : Type u) → (I → TCTree) → TCTree

works but oh god what the hell is that error message

[Sébastien Gouëzel]

There' s something fishy going on:

inductive TCTree : Sort 1
  | node : (Σ (I : Sort 0), I → TCTree) → TCTree

inductive TCTree' : Sort 2
  | node : (Σ (I : Sort 1), I → TCTree') → TCTree'

inductive TCTree'' : Sort 3
  | node : (Σ (I : Sort 2), I → TCTree'') → TCTree''

The first two work, the last one fails...

[Aaron Liu]

I think it fails to generate the below and brec?

[Aaron Liu]

Sébastien Gouëzel said:

There' s something fishy going on:

inductive TCTree : Sort 1
  | node : (Σ (I : Sort 0), I → TCTree) → TCTree

inductive TCTree' : Sort 2
  | node : (Σ (I : Sort 1), I → TCTree') → TCTree'

inductive TCTree'' : Sort 3
  | node : (Σ (I : Sort 2), I → TCTree'') → TCTree''

The first two work, the last one fails...

Since imax 0 u and imax 1 u both reduce, but imax 2 u does not

[Antoine Chambert-Loir]

Do we agree that something like this should work? What does @Mario Carneiro think?

[Mario Carneiro]

this looks like a bit of a nightmare case TBH

[Mario Carneiro]

the details around which kinds of nested inductives are allowed are not very well defined

[Mario Carneiro]

right now the only thing we have is some code and whatever that code accepts is legal

[Antoine Chambert-Loir]

Thanks for the clarification.

[Mario Carneiro]

@Arthur Adjedj do you have any opinion here?

[Mario Carneiro]

It looks like the inductive itself is accepted but one of the generated functions fails

[Mario Carneiro]

ah yes, this is not a kernel issue at all

[Mario Carneiro]

you can #print TCTree immediately afterward and see that the declaration has been added to the environment even though it errored

[Arthur Adjedj]

As far as I can see, the sizeOf auxiliary definitions are where it's failing.

[Arthur Adjedj]

Ah nevermind, the order in which declarations appear withwhatsnew in is not too consistent.

[Arthur Adjedj]

TCTree''.belows and TCTree''.brecOns seem to be added as axioms instead of defs in the environment, I'm guessing it means the issue is happening there.

[Mario Carneiro]

are you sure? I see them as defs via print

inductive TCTree'' : Sort 3
  | node : (Σ (I : Sort 2), I → TCTree'') → TCTree''
#print TCTree''.brecOn
#print TCTree''.below

[Arthur Adjedj]

That's confusing, whatsnew shows me an axiom, but #check shows a def:

import Mathlib

whatsnew in
inductive TCTree'' : Sort 3
  | node : (Σ (I : Sort 2), I → TCTree'') → TCTree''
/-protected axiom TCTree''.below_1.{u} : {motive_1 : TCTree'' → Sort u} →
  {motive_2 : (I : Type 1) × (I → TCTree'') → Sort u} → (I : Type 1) × (I → TCTree'') → Sort (max 1 u)-/


#print TCTree''.below_1
/-@[reducible] protected def TCTree''.below_1.{u} : {motive_1 : TCTree'' → Sort u} →
  {motive_2 : (I : Type 1) × (I → TCTree'') → Sort u} → (I : Type 1) × (I → TCTree'') → Sort (max 1 u) :=
fun {motive_1} {motive_2} t =>
  TCTree''.rec_1 (fun a a_ih => motive_2 a ×' a_ih)
    (fun fst snd snd_ih => ((a : fst) → motive_1 (snd a)) ×' ((a : fst) → snd_ih a)) t-/

[Mario Carneiro]

maybe this has something to do with asynchronous environments

[Arthur Adjedj]

Are unrealized consts pretty-printed as axioms before they're realized ? would make sense.

[Mario Carneiro]

I don't think they should be, I just expect that whatsnew in hasn't been updated properly

[Arthur Adjedj]

Is there any chance #whatsnew also shows decls that have been added to the elab env before they've been validated in the kernel's env, leading false infos as to what really is available ?

[Arthur Adjedj]

Because otherwise, I don't see what's supposedly failing here, the diff doesn't show much difference.

[Aaron Liu]

It works if you don't import anything

prelude

@[pp_using_anonymous_constructor]
structure Sigma {α : Type u} (β : α → Type v) where
  mk ::
  fst : α
  snd : β fst
attribute [unbox] Sigma

inductive TCTree : Sort 3
  | node : (Sigma fun (I : Sort 2) => I → TCTree) → TCTree

[Aaron Liu]

The (kernel) application type mismatch errors are from the same constants that whatsnew in reports as axioms

[Mario Carneiro]

yes, the errors are in TCTree''.below, TCTree''.below_1, TCTree''.brecOn, TCTree''.brecOn_1 in that order

[Mario Carneiro]

the errors in brecOn seem to be because TCTree''.below doesn't unfold, so it was probably added as an axiom

[Mario Carneiro]

and it seems that TCTree''.below was added to the environment despite the type error:

example {motive_1 : TCTree'' → Sort u}
    {motive_2 : (I : Type 1) × (I → TCTree'') → Sort u}
    (t : TCTree'') : @Nat.TCTree''.below = sorry := by
  ext a b c
  delta TCTree''.below -- kernel error here
  sorry

[Mario Carneiro]

and the underlying issue is that #check Sort (max (max 1 (imax 2 u)) 2 u) = Sort (max 1 u) fails (correctly, these are not the same for u = 1)

[Mario Carneiro]

somehow the code has decided that TCTree''.below should live in Sort (max 1 u) but that universe is not big enough

[Arthur Adjedj]

indeed, bumping the universe for below to max 2 u seems to fix the issue:

@[reducible] protected def TCTree.below'.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Type 1) × (I → TCTree) → Sort u} → TCTree → Sort (max 2 u) :=
fun {motive_1} {motive_2} t =>
  TCTree.rec (fun a a_ih => motive_2 a ×' a_ih)
  (fun fst snd snd_ih => (a : fst) → motive_1 (snd a) ×' snd_ih a) t

[Joachim Breitner]

That code was recently touched by @Parth Shastri , maybe it got fixed along the way?
https://github.com/leanprover/lean4/pull/7639

---

No it didn't

[Parth Shastri]

My change in #7639 only affected reflexive inductive types. Even though TCTree should be considered reflexive (it contains I → TCTree), the way the kernel handles nested inductives makes it miss this case, and so the generated below/brecOn implementation uses the non-reflexive universe calculation, which is incorrect. I believe that with my previous change, the separate non-reflexive universe calculation is no longer needed, and I have opened #8937 to change the implementation to use the new universe calculation in all cases.

[Joachim Breitner]

Thanks! @Mario Carneiro, @Arthur Adjedj , since you have been looking at this here already, do you agree that this is a good fix?

[Arthur Adjedj]

LGTM. I think this also warrants some fix in the kernel to ensure the reflexive field is correctly set on such nested inductive types, but the field is not used in the kernel in practice, so this is not critical.