Type max

Stream: lean4

[Patrick Massot]

I just noticed that Lean 4 displays Type (max (max (max (max u_1 u_3) u_4) u_6) 0) where Lean 3 displayed Type (max u_1 u_3 u_4 u_6). Is this simply a missing delaborator? The max with zero looks suspicious. Was is already there in Lean 3 but not displayed?

[Mario Carneiro]

no, the normalization changed

[Mario Carneiro]

which is to say, it doesn't normalize as eagerly as it used to

[Mario Carneiro]

you can see that it still uses the same display for right associative max, but it doesn't actually right associate unsolicited:

universe a b c d
#check Type max (max a b) (max c d)
-- Type (max (max a b) c d) : Type ((max (max a b) c d) + 1)

[Mario Carneiro]

the universe inference mechanism is more likely to generate left associated max expressions too, so you get those towers of maxes

[Patrick Massot]

Ok thanks. Unfortunately none of this directly explain why Lean 4 can't understand universes in the sphere eversion project.

[Mario Carneiro]

no, it's probably just obfuscating things a bit

[Patrick Massot]

I have

#check HtpyFormalSol (RelMfld.localize p.φ p.ψ R) -- Type (max (max u₁ u₄) 0)

def RelLoc.HtpyFormalSol.unloc : HtpyFormalSol (RelMfld.localize p.φ p.ψ R) :=
  sorry

and the def complains about

stuck at solving universe constraint
  max (max (max u₁ u₃) u₄) u₆ =?= max ?u.114816 ?u.114817
while trying to unify
  Set : Type (max (max (max u₆ u₄) u₃) u₁) → Type (max (max (max u₆ u₄) u₃) u₁)
with
  Set.{max ?u.114816 ?u.114817} : Type (max ?u.114816 ?u.114817) → Type (max ?u.114816 ?u.114817)

[Patrick Massot]

It seems crazy that the check understands universe but not the def.

[Patrick Massot]

I know this isn't the first message on Zulip about Lean being stuck at a problem such as max (max (max u₁ u₃) u₄) u₆ =?= max ?u.114816 ?u.114817, but are we getting anywhere closer to a solution?

[Patrick Massot]

Of course I could replace all Type* in the project with Type without loosing any application, but somehow I've been trained not to do this.

[Mario Carneiro]

There is no Set in the example?

[Patrick Massot]

@[reducible]
def RelMfld := Set (OneJetBundle I M I' M')

[Mario Carneiro]

What do the variables look like?

[Patrick Massot]

The variables look like we are in the differential geometry corner of Mathlib:

variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type _} [TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) (M : Type _) [TopologicalSpace M] [ChartedSpace H M]
  [SmoothManifoldWithCorners I M] {E' : Type _} [NormedAddCommGroup E'] [NormedSpace ℝ E']
  {H' : Type _} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') (M' : Type _)
  [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] {F : Type _}
  [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type _} [TopologicalSpace G]
  (J : ModelWithCorners ℝ F G) (N : Type _) [TopologicalSpace N] [ChartedSpace G N]
  [SmoothManifoldWithCorners J N] {F' : Type _} [NormedAddCommGroup F'] [NormedSpace ℝ F']
  {G' : Type _} [TopologicalSpace G'] (J' : ModelWithCorners ℝ F' G') (N' : Type _)
  [TopologicalSpace N'] [ChartedSpace G' N'] [SmoothManifoldWithCorners J' N'] {EP : Type _}
  [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type _} [TopologicalSpace HP]
  (IP : ModelWithCorners ℝ EP HP) (P : Type _) [TopologicalSpace P] [ChartedSpace HP P]
  [SmoothManifoldWithCorners IP P] {EX : Type _} [NormedAddCommGroup EX] [NormedSpace ℝ EX]
  {HX : Type _} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX}
  {R : RelMfld I M I' M'}

[Mario Carneiro]

what is the type of HtpyFormalSol?

[Mario Carneiro]

wow that's a lot

[Patrick Massot]

Sorry, I copy-pasted from the wrong file

[Patrick Massot]

variable {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E]
  {H : Type u₂} [TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) (M : Type u₃) [TopologicalSpace M] [ChartedSpace H M]
  [SmoothManifoldWithCorners I M]
  {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E']
  {H' : Type u₅} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H')
  (M' : Type u₆) [MetricSpace M']
  [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] {R : RelMfld I M I' M'}

[Patrick Massot]

I added explicit universe variables in a desperate attempt to please the universe checker.

[Patrick Massot]

Mario Carneiro said:

wow that's a lot

That's a typical variable command in the sphere eversion end-game.

[Mario Carneiro]

that's not where you need the universes, you need them in HtpyFormalSol, hence the question

[Patrick Massot]

HtpyFormalSol.{u_1, u_2, u_3, u_4, u_5, u_6} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [SmoothManifoldWithCorners I M] {E' : Type u_4}
  [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5}
  [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'}
  {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M']
  [SmoothManifoldWithCorners I' M'] (R : RelMfld I M I' M') :
Type (max (max (max (max u_1 u_3) u_4) u_6) 0)

[Patrick Massot]

Sorry about all the edits, I tried to get it to fit on a Zulip code block.

[Mario Carneiro]

Does it help if you make RelMfld a def?

[Patrick Massot]

It is already a def.

[Mario Carneiro]

not reducible

[Patrick Massot]

It wasn't reducible in Lean 3, but I had to make it reducible to please Lean 4 which is more strict with defeq abuse.

[Mario Carneiro]

or maybe make RelMFld' which is a def wrapper around RelMfld and make HtpyFormalSol take it as an argument

[Mario Carneiro]

to minimize other breakage

[Mario Carneiro]

is OneJetBundle also reducible?

[Patrick Massot]

Maybe I should say that

abbrev HtpyFormalSol (R : RelMfld I M I' M') :=
  FamilyFormalSol 𝓘(ℝ, ℝ) ℝ R

where FamilyFormalSol is a serious definition in the sense that it is parametrized by 9 universe levels.

[Patrick Massot]

And yes, OneJetBundle is also reducible:

@[reducible]
def OneJetBundle :=
  TotalSpace (E →L[𝕜] E') (OneJetSpace I I' : M × M' → Type _)

[Mario Carneiro]

oh no

[Mario Carneiro]

how many of these definitions did you make reducible?

[Mario Carneiro]

Surely this file is intolerable to compile

[Patrick Massot]

Many. At some point during the ongoing port it seemed to be the solution to all issues.

[Patrick Massot]

Mario Carneiro said:

Surely this file is intolerable to compile

No, it isn't particularly slow.

[Patrick Massot]

Actually in that folder there are only three reducible definitions and two abbreviations.

[Mario Carneiro]

I think what is happening is that RelMfld I M I' M' =?= RelMfld ?I ?M ?I' ?M' doesn't actually imply I =?= ?I, M =?= ?M etc because one of these reducible definitions doesn't actually use the variable

[Mario Carneiro]

which then makes it useless as a way of inferring the implicit arguments

[Mario Carneiro]

Try passing in these variables explicitly, what is the type of RelMfld.localize p.φ p.ψ R?

[Patrick Massot]

RelMfld.localize p.φ p.ψ R : RelMfld 𝓘(ℝ, E) E 𝓘(ℝ, E') E'

[Mario Carneiro]

so maybe

def RelLoc.HtpyFormalSol.unloc : HtpyFormalSol (I := 𝓘(ℝ, E)) (M := E) (I' := 𝓘(ℝ, E')) (M' := E') (RelMfld.localize p.φ p.ψ R) :=

[Patrick Massot]

That doesn't help. I think you would waste less time by checking out the lean4 branch of https://github.com/leanprover-community/sphere-eversion

[Mario Carneiro]

I think I would waste quite a bit more time doing that :D

[Mario Carneiro]

it's a lean 3 project?

[Mario Carneiro]

oh the branch is just called lean4

[Patrick Massot]

The master branch is on Lean 3.

[Mario Carneiro]

Oh!

def RelLoc.HtpyFormalSol.unloc := sorry

is already giving the universe constraint error

[Patrick Massot]

What?

[Mario Carneiro]

which means the issue is in the variable declarations

[Patrick Massot]

But why do the #check work then?

[Mario Carneiro]

there is a red squiggle on the R on L154

[Mario Carneiro]

because #check doesn't require all pending universe problems to be solved, it shows things with metavariables

[Patrick Massot]

If you #exit before the def then there is no squiggle.

[Mario Carneiro]

that's because variable elaboration is borked

[Patrick Massot]

Actually Lean seems confused by the fact that HtpyFormalSol exist in two different namespaces (with different meaning).

[Mario Carneiro]

oh wait, def foo := sorry doesn't work period

[Patrick Massot]

You can get rid of the variable line error by replacing it by variable (F : _root_.HtpyFormalSol R)

[Patrick Massot]

This is wild.

[Mario Carneiro]

Aha, it's an ambiguous reference which was waiting for type information, and this is screwing up the rest of the inference

[Patrick Massot]

What do you call "the rest of the inference" in def foo := sorry?

[Patrick Massot]

Ok, def foo : Nat := sorry does work

[Mario Carneiro]

def foo := sorry just doesn't work at all, that was a false alarm

[Mario Carneiro]

it complains because it doesn't know what universe the definition lives in or something

[Patrick Massot]

Oh I see, def foo := sorry doesn't work in an empty Lean file.

[Mario Carneiro]

I think it should be made to work, but whatever

[Patrick Massot]

But putting _root_.HtpyFormalSol everywhere seems to work.

[Mario Carneiro]

Oh I see, this is even more wild than I thought: the HtpyFormalSol on the variable line is not ambiguous, but in the context of nonrec def RelLoc.HtpyFormalSol.unloc because this def is in the RelLoc namespace now it considers the other definition as in scope

[Mario Carneiro]

that's what hygiene was supposed to save us from

[Patrick Massot]

By the way, the nonrec is irrelevant, it's an habit I got when facing the weirdest errors in Lean 4: try addiing a nonrec in front of def, just in case Lean gets confused by names.

[Mario Carneiro]

sadly it wasn't enough to save us from this issue :(

[Patrick Massot]

Exactly, but it was in the right direction somehow.

[Patrick Massot]

Thank you very much Mario. I'll try to minimize this and open a Lean 4 issue.

[Patrick Massot]

Well, minimizing wasn't hard:

def Foo.Bar : Nat → Nat := id

def Bar : Nat := 3

def Foo.Baz : Nat := Bar + 2

[Patrick Massot]

failed to synthesize instance
  HAdd (Nat → Nat) Nat Nat

[Patrick Massot]

I opened lean4#2844.

[Mario Carneiro]

that one is expected, as I just wrote on the issue

[Kevin Buzzard]

Yeah this is normal, and it's a great feature once you've got over being bitten by it several times

[Patrick Massot]

I put a new example in the Lean 4 issue.