leanprover
fix: Level.geq is missing a case
It's not a false alarm this time, this came up during testing of lean4lean. Currently Level.geq differs from level::is_geq in the case of max u v >= imax u v: the lean function is overly pessimistic and yields false on this while the C++ function says true, because the lean function does return (u >= imax u v) || (v >= imax u v) while the C++ function does if ((u >= imax u v) || (v >= imax u v)) return true and continues to the rest of the function otherwise. This comes up concretely in the Trans class:
class Trans (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) where
trans : r a b → s b c → t a c
The type of this class is apparently Sort (max (max (max (max (max (max 1 u) u_1) u_2) u_3) v) w) (where u_1 u_2 u_3 are the levels of α β γ), but if you try writing that type explicitly then it fails, because if you leave the type off the elaborator takes the max of all the universe levels appearing and assumes it would succeed (and it does, in the kernel), while if you write the type then the elaborator checks the inequality (using the lean geq) and this fails.
PS: Level.normalize also differs from level::normalize: the lean function left associates max expressions and the C++ function right associates. I suspect this could also lead to different behaviors in edge cases, although I don't yet have an example. Is it worth making them agree here?
- ✅ Mathlib branch lean-pr-testing-2689 has successfully built against this PR. (2023-10-15 17:59:22) View Log
- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase e4daca8d6b02677115282abff8515a9afb6a2a29 --onto 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a. (2024-04-22 03:10:38) - 🟡 Mathlib branch lean-pr-testing-2689 build this PR didn't complete normally. (2024-11-19 20:32:28) View Log
Just noting there's a conflict here now.
Would it be possible to include the Trans example as a test?
Ping @leodemoura on this since apparently #2750 was missed so probably this long standing bug was too.
Mathlib CI status (docs):
- ✅ Mathlib branch lean-pr-testing-2689 has successfully built against this PR. (2024-11-19 21:30:36) View Log
