Conversation
digama0
changed the title
Lean/Level.lean\ and \kernel/level.cpp\ normalization rulesLean/Level.lean and kernel/level.cpp normalization rules
This PR aligns the `Level` normalization rules in `Lean/Level.lean` (stdlib) and `kernel/level.cpp` (kernel) so that both produce the same normalized `Level` for the same input. Specifically, `mk_max` in `src/kernel/level.cpp` gains the "one operand is explicit and the other's offset dominates" simplification (e.g. `max (succ u_1) 1 → succ u_1`, which the stdlib's `mkLevelMaxCore` already performed), and `mkLevelIMaxCore` in `src/Lean/Level.lean` gains the `imax 1 u = u` case that C++'s `mk_imax` already had (via `is_one(l1)`). Both simplifications are semantics-preserving; the goal is only to make the two implementations agree so that downstream expression hashes computed by different tools (elaborator, `#reduce`, `lean4lean`, other kernel reimplementations) match on a fixed input.
digama0
force-pushed
the
fix/level-normalize-parity
branch
from
July 10, 2026 15:09
af1ee70 to
8193825
Compare
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
The elaborator now normalizes imax 1 u to u when pretty-printing the kernel error, matching the kernel's existing behavior. The kernel mismatch this regression test guards is unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
leanprover-bot
added
the
builds-manual
3 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR aligns the
Levelnormalization rules inLean/Level.lean(stdlib) andkernel/level.cpp(kernel) so that both produce the same normalizedLevelfor the same input.Specifically,
mk_maxinsrc/kernel/level.cppgains the "one operand is explicit and the other's offset dominates" simplification (e.g.max (succ u_1) 1 → succ u_1, which the stdlib'smkLevelMaxCorealready performed), andmkLevelIMaxCoreinsrc/Lean/Level.leangains theimax 1 u = ucase that C++'smk_imaxalready had (viais_one(l1)). Both simplifications are semantics-preserving; the goal is only to make the two implementations agree so that downstream expression hashes computed by different tools (elaborator,#reduce,lean4lean, other kernel reimplementations) match on a fixed input.