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?