Simplification of imax 1 u

Stream: lean4

[Parth Shastri]

Currently, the first example typechecks while the second does not.

example (α : Sort u) : Sort u := True → α
example (α : Sort u) : Sort u := Unit → α

This is because Sort (imax 1 u) is currently not being reduced to Sort u, despite them being equivalent:

example : ∀ u, Nat.imax 1 u = u
  | 0 => rfl
  | 1 => rfl
  | _ + 2 => rfl

I modified src/Lean/Level.lean and src/kernel/level.cpp to perform this simplification, basing it off of the initial code that simplifies imax 0 u to u. The result successfully handles both examples, as well as a more complicated situation where I first ran into this issue. Is there a reason this simplification is not already implemented? Does adding this cause breakage elsewhere?

[Siddhartha Gadgil]

Parth Shastri said:

Currently, the first example typechecks while the second does not.

example (α : Sort u) : Sort u := True → α
example (α : Sort u) : Sort u := Unit → α

This is because Sort (imax 1 u) is currently not being reduced to Sort u, despite them being equivalent:

example : ∀ u, Nat.imax 1 u = u
  | 0 => rfl
  | 1 => rfl
  | _ + 2 => rfl

I modified src/Lean/Level.lean and src/kernel/level.cpp to perform this simplification, basing it off of the initial code that simplifies imax 0 u to u. The result successfully handles both examples, as well as a more complicated situation where I first ran into this issue. Is there a reason this simplification is not already implemented? Does adding this cause breakage elsewhere?

Isn't the simplification false when u is Prop?

[Marcus Rossel]

@Siddhartha Gadgil, in #tpil4 they say:

imax i j is the maximum of i and j if j is not 0, and 0 otherwise.

So imax 1 0 = 0.

Also, Lean's implementation of Nat.imax is:

def Nat.imax (n m : Nat) : Nat :=
  if m = 0 then 0 else Nat.max n m

[Siddhartha Gadgil]

Marcus Rossel said:

Siddhartha Gadgil, in #tpil4 they say:

imax i j is the maximum of i and j if j is not 0, and 0 otherwise.

So imax 1 0 = 0.

Also, Lean's implementation of Nat.imax is:

def Nat.imax (n m : Nat) : Nat :=
  if m = 0 then 0 else Nat.max n m

Thanks.

[Mario Carneiro]

Note that #leantt validates the use of this rule, since it uses a more elaborate decision procedure that is complete for level arithmetic. AFAIK Lean's simplification-based universe checker is necessarily incomplete, so there will always be examples like this. The "correct" solution is to do case splitting on imax subexpressions, but this can have poor performance in some edge cases (which wouldn't check at all in lean's implementation). This is what the trepplein external typechecker implements

[James Gallicchio]

would it be possible to have an option for toggling a complete decision procedure on? or is there a workaround other than duplicating universe polymorphic definitions specialized to u = 0 and u > 0?

[Ghilain Bergeron]

Just got bitten by this issue as well.
Is there any reason why the typechecker does not already implement this simplification? Or is there a way to work around this issue somehow?

[Kyle Miller]

I would suggest creating a Lean 4 issue with examples you've run into. The example (α : Sort u) : Sort u := Unit → α example would be good to include.

[Arthur Adjedj]

(deleted)

[Robin Arnez]

Mario Carneiro schrieb:

Note that #leantt validates the use of this rule, since it uses a more elaborate decision procedure that is complete for level arithmetic. AFAIK Lean's simplification-based universe checker is necessarily incomplete, so there will always be examples like this. The "correct" solution is to do case splitting on imax subexpressions, but this can have poor performance in some edge cases (which wouldn't check at all in lean's implementation). This is what the trepplein external typechecker implements

I would argue that at least the kernel should support case splitting here or some other way of ensuring that universe defeq is exactly correct, perhaps if the normal defeq procedure failed. Otherwise this makes it impossible to create certain definitions, even if they are technically correct. And then perhaps the defeq procedure in Lean.Meta should also do case splitting on failure if no meta-variables are involved to support this.