feat(Tactic/Linter): add blanketSimpArgs linter

[sgraf812]

The blanketSimpArgs linter flags simp arguments such as simp [Subsingleton.eq_zero] whose rewrite source is a bare variable and whose side conditions simp must discharge at every match. Such an argument is retrieved at every visited subterm (its discrimination tree key is *), and each attempted match triggers instance searches that miss the cache under binders; #42053 measured a single such argument dominating the elaboration time of a file. The linter suggests determining the side conditions at the use site, by applying the lemma to a term or by fixing its implicit arguments, as in Subsingleton.eq_zero (α := M).

The check is semantic, so it covers Subsingleton.eq_one, Unique.eq_default and any other lemma of the same shape. It walks the simpLemma argument nodes shared by the simp-like tactics, including the using clause of nontriviality, and the rewrite rules of simp_rw.

The first commit pins the remaining such simp arguments in Mathlib, all of them uses of Unique.eq_default, so that the library is clean under the new linter.

---

• depends on: [Merged by Bors] - perf: restrict Subsingleton.eq_zero/eq_one simp arguments to their intended type #42053

AI usage: the linter, its tests and the call-site fixes were written with Claude Code (Claude Fable 5) under my direction; I have reviewed all of it, and the tests and affected files were verified by building them locally.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for ded55c4 against 6c5a908 are in. There are significant results. @sgraf812

• 🟥 build//instructions: +588.0G (+0.41%)

Large changes (1🟥)

• 1 hidden

Medium changes (3✅)

• ✅ build/module/Mathlib.Algebra.Central.End//instructions: -6.6G (-43.34%)
• ✅ build/module/Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries//instructions: -6.7G (-33.56%)
• ✅ build/module/Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs//instructions: -7.5G (-32.49%)

Small changes (3✅)

• ✅ build/module/Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv//instructions: -3.4G (-4.50%)
• ✅ build/module/Mathlib.Combinatorics.Enumerative.Partition.GenFun//instructions: -2.2G (-12.24%)
• ✅ build/module/Mathlib.RepresentationTheory.Homological.TateCohomology.Basic//instructions: -2.4G (-10.37%)

[sgraf812]

t-meta
LLM-generated

[github-actions]

PR summary f2939c5ec4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 8243 files with changed transitive imports taking up over 359603 characters: this is too many to display!
You can run this locally from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

---

Declarations diff (regex)

+ blanketSimpArgsLinter
+ cache,
+ eq_nil_of_isEmpty
+ fallback
+ isBlanketRewrite
+ myId
+ rewriteSource?
+ simpRwKind

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit f2939c5).

• +2 new declarations
• −0 removed declarations

+Mathlib.Linter.BlanketSimpArgs.simpRwKind
+Mathlib.Linter.linter.blanketSimpArgs

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit f2939c5ec4
Reference commit 9fb10993c1

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[sgraf812]

Note to reviewers: I haven't reviewed the LLM-generated linter proposed here. If the reviewers find such a linter generally useful, then I would be willing to give it a closer look and polish before seriously submitting it for review. Hence I declare the initial round of review here, specifically this comment

# The `blanketSimpArgs` linter

The `blanketSimpArgs` linter flags simp arguments such as `simp [Subsingleton.eq_zero]`
whose rewrite source is a bare variable and whose remaining hypotheses `simp` must
discharge at every match.

## Example

```
example {M : Type} [Zero M] [Subsingleton M] (x : M) : x = 0 := by
  simp [Subsingleton.eq_zero]     -- linted against
```

## Why is this bad?

A lemma like `Subsingleton.eq_zero : ∀ {α} [Zero α] [Subsingleton α] (a : α), a = 0`
rewrites the bare variable `a`. Its discrimination tree key is `*`, so `simp` retrieves
and tries it at every visited subterm, and each attempted match triggers instance
searches for `Zero α` and `Subsingleton α`. Under binders these searches miss the
instance cache, so a single such simp argument can dominate the elaboration time of
a proof.

The fix is to determine the side conditions once, at elaboration time of the simp
argument: apply the lemma to a term, as in `simp [Subsingleton.eq_zero x]`, or fix
its implicit arguments, as in `simp [Subsingleton.eq_zero (α := M)]`.

as

easy

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 7c523de against 6c5a908 are in. There are significant results. @sgraf812

• 🟥 build//instructions: +565.1G (+0.39%)

Large changes (1🟥)

• 1 hidden

Medium changes (3✅)

• ✅ build/module/Mathlib.Algebra.Central.End//instructions: -6.6G (-43.41%)
• ✅ build/module/Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries//instructions: -6.7G (-33.27%)
• ✅ build/module/Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs//instructions: -7.4G (-32.08%)

Small changes (3✅)

• ✅ build/module/Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv//instructions: -3.4G (-4.55%)
• ✅ build/module/Mathlib.Combinatorics.Enumerative.Partition.GenFun//instructions: -2.3G (-12.68%)
• ✅ build/module/Mathlib.RepresentationTheory.Homological.TateCohomology.Basic//instructions: -2.5G (-10.75%)

[grunweg]

Nice find; thanks for making this linter! I agree this is a potential performance footgun, so we should have such a linter.

I wonder, though: can the root cause

Under binders these searches miss the instance cache, so a single such simp argument can dominate the elaboration time of a proof.

be fixed in Lean core instead? That would be even nicer than papering over it with a linter :-)

[sgraf812]

I'll relay your question to Sebastian U, who is currently investigating type class caching :)

[sgraf812]

So the issue here might be partially fixed in Core, but certainly an equality like eq_zero [...] (lhs : α) : lhs = 0 will still trigger a type class search for every type that occurs in the term. That sounds pretty wasteful to me even if cached.

[grunweg]

Thanks for passing that on - and the answer sounds fair. We should probably have both the linter and a core fix if viable :-)

[sgraf812]

I guess the linter can be more targeted at the particular Eq ?α ?lhs ... conclusion. Eq Nat ?lhs ... would be OK.

[sgraf812]

Nevermind, that's exactly what the linter checks already. That, plus whether there are any instance or proposition parameters that need discharging. It's pretty reasonable, I'd say. Do you think you'd merge it if I polish? Shall I make it ready for review next week?

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - perf: restrict Subsingleton.eq_zero/eq_one simp arguments to their intended type #42053
  By Dependent Issues (🤖). Happy coding!

[grunweg]

Polishing this would be great. (Splitting out the other adaptations is also welcome.)

[joneugster]

I'm a bit confused about the radar result. From the description & discussion I would have expected to see much more of a positive effect. Does that mean the linting takes up more time/instructions than the issues fixed here?

Anyways, even if this was the case, I think this linter is really useful to have, as Michael already said above! (there is always the possibility to disable some linters by default and only run then periodicall if they were ever too slow)

I'll add

awaiting-author

for now to give you the time for clean-up and thelike.

[grunweg]

Regarding the benchmarking, this underscores that landing the adaptations separately would be really valuable. This way, we separate the performance side-effects (which we could also harvest by having a weekly linter) from the slow-down of the linter.

[grunweg]

I'll be happy to review the final adaptation PR, by the way.

[sgraf812]

Sorry, didn't manage to come back to it this week. Next week 🤞

[grunweg]

Sure, no worries!

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 042d20f against 9fb1099 are in. There are significant results. @sgraf812

• 🟥 build//instructions: +551.1G (+0.38%)

Large changes (1🟥)

• 1 hidden

Small changes (1✅)

• ✅ build/module/Mathlib.RepresentationTheory.Homological.TateCohomology.Basic//instructions: -2.5G (-10.68%)

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for f2939c5 against 9fb1099 are in. There are significant results. @sgraf812

• 🟥 build//instructions: +396.7G (+0.28%)

Large changes (1🟥)

• 1 hidden

Small changes (1✅)

• ✅ build/module/Mathlib.RepresentationTheory.Homological.TateCohomology.Basic//instructions: -2.5G (-10.66%)

[sgraf812]

Can't make it any faster. I think I'll suggest a simp linter upstream instead; see leanprover/lean4#14677. If that is rejected, you can deliberate whether you want to take the linter as is. I frankly don't see it carrying its weight.

[grunweg]

Thanks for trying! I agree that 0.3% overall slowdown is a mouthful, we certainly wouldn't want that as a linter enabled by default. (We could have it as a weekly linter, which is run once a week together with other diagnostic linters.) In any case, a core linter is even better - so fingers crossed!
And I'm interested in benchmarking just the mathlib adaptations to see if they are useful.

[sgraf812]

leanprover/lean4#14677 is awaiting review. The performance numbers look much better and it shows that it more than pays just for the remaining adaptations it found.