fix: handle numerals in non-tail positions of cutsat polynomials#13199
Closed
kim-em wants to merge 3 commits intoleanprover:masterfrom
Closed
fix: handle numerals in non-tail positions of cutsat polynomials#13199kim-em wants to merge 3 commits intoleanprover:masterfrom
kim-em wants to merge 3 commits intoleanprover:masterfrom
Conversation
After leanprover#13166, the canonicalizer normalizes Nat arithmetic in type positions (e.g. `n + 1 + 1` → `n + 2` in `Fin`) but leaves value-level expressions unchanged. When `toPoly` processes `↑n + 1 + 1` (in Int), the middle `1` appears as a numeral in a non-tail position and `addMonomial` would fall back to treating it as a variable. Fix: use `Poly.addConst` (which already exists in `Init.Data.Int.Linear`) to fold the numeral into the polynomial's constant term, regardless of position. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
kim-em
force-pushed
the
fix/lia-numeral-non-tail
branch
from
94c6d1b to
ad8ae7e
Compare
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
Collaborator
Author
|
Leo is going to solve this via a different approach. |
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 fixes a
liaregression introduced by #13166. After that PR, the canonicalizer normalizes Nat arithmetic in type positions (e.g.n + 1 + 1becomesn + 2inFin) but leaves value-level expressions unchanged. When cutsat'stoPolyprocesses↑n + 1 + 1(inInt), the middle1appears as a numeral in a non-tail position of the polynomial being built, andaddMonomialfalls back to treating it as a variable.The fix uses the existing
Poly.addConstto fold the numeral into the polynomial's constant term regardless of position, instead of the previous logic that only accepted numerals at the tail and reported an issue otherwise.🤖 Prepared with Claude Code