feat: add linter for simp arguments triggering TC synthesis at every subterm - #14677
Open
sgraf812 wants to merge 1 commit into
Open
feat: add linter for simp arguments triggering TC synthesis at every subterm#14677sgraf812 wants to merge 1 commit into
sgraf812 wants to merge 1 commit into
Conversation
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
sgraf812
force-pushed
the
blanket-simp-args
branch
from
August 4, 2026 17:12
1eb4e3e to
33ac19b
Compare
1 task
sgraf812
changed the title
sgraf812
force-pushed
the
blanket-simp-args
branch
5 times, most recently
from
August 5, 2026 08:39
4afad45 to
e9d6b09
Compare
sgraf812
changed the title
sgraf812
changed the title
sgraf812
force-pushed
the
blanket-simp-args
branch
from
August 5, 2026 09:49
e9d6b09 to
ae5ae9a
Compare
sgraf812
changed the title
sgraf812
changed the title
This PR adds the `linter.blanketSimpArgs` linter, which warns about a `simp` argument whose left-hand side is a variable, such as `eq_zero {α} [Zero α] [Subsingleton α] (a : α) : a = 0`. Such an argument is tried at every subterm and synthesizes its instances at each match, which can dominate the elaboration time of a proof; the warning suggests determining those instances at the use site instead, by fixing the implicit arguments or applying the theorem to a term.
The check runs where `simp` arguments are elaborated.
sgraf812
force-pushed
the
blanket-simp-args
branch
from
August 5, 2026 09:54
ae5ae9a to
c2dcaeb
Compare
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
Contributor
Author
|
!bench |
|
Benchmark results for c2dcaeb against 945e78b are in. No significant results found. @sgraf812
Small changes (2✅, 3🟥)
|
sgraf812
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 5, 2026
Pin `Unique.eq_default` to the type being collapsed at the eight sites that `linter.blanketSimpArgs` reports. Its left-hand side is a variable of variable type, so `simp` matched it at every subterm and synthesized `Unique` at each match.
mathlib-lean-pr-testing
Bot
added
builds-mathlib
Contributor
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@657fe2a against leanprover-community/mathlib4-nightly-testing@3e9b868 are in. No significant results found. @sgraf812
Small changes (1✅)
|
sgraf812
marked this pull request as ready for review
August 5, 2026 13:57
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
3 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 adds the
linter.blanketSimpArgslinter, which warns about asimpargument whose left-hand side is a variable, such aseq_zero {α} [OfNat α 0] [Subsingleton α] (a : α) : a = 0. Such an argument is tried at every subterm and synthesizes its instances at each match, which can dominate the elaboration time of a proof; the warning suggests determining those instances at the use site instead, by fixing the implicit arguments or applying the theorem to a term.The check runs where
simparguments are elaborated. See also leanprover-community/mathlib4#42056, where this linter was first proposed and rejected because of its overhead. Hooking directly into the elaborator is much more efficient, by contrast.