feat: linter.simp.loopProtection #8688

nomeata · 2025-06-08T19:38:53Z

This PR adds the linter.simp.loopProtection option (on by default) which makes simp detect and warn about some obviously looping rewrite rules, implementing the ideas in #5111.

This check is not complete (will not detect all possible loops) and not conservative (will warn about theorems that could be looping, even if they are not looping in the simp application at hand, e.g. because of the concrete terms some other rewrite rule breaks the loop). Nevertheless is should, in practice, alert the user about likely unintended actions.

The warning triggers when a rewrite rule applies to its own (abstract) right-hand side, a pair of rewrite rules applies to each other’s right-hand side (or a larger cycle), and one of these rewrite rules is about to be actually applied by simp. It ignores local hypotheses and simp theorems that are marked as permuting.

For now it only checks explicit simp arguments, but not lemmas added to the simp set via @[simp]`, on the assumption that ad-hoc simp theorems are most likely the cause of loops.

The check can be disabled with set_option linter.simp.loopProtection false, as usual.

The mathlib adaption branch simply sets that option globally for mathlib for an easy transition. Partial fixes to make mathlib clean wrt to this setting can be found in leanprover-community/mathlib4#26032, if they are useful to anyone.

Here are some patterns of working simp calls found in mathlib that will trigger this:

Injectivity lemmas applied in reverse:
```
@[simp]
lemma contract_contract (M : Matroid α) (C₁ C₂ : Set α) : M ／ C₁ ／ C₂ = M ／ (C₁ ∪ C₂) := by
  simp [← dual_inj]
```
where dual_inj shows M₁✶ = M₂✶ ↔ M₁ = M₂. Clearly its inverse is not terminating. It works here because some other lemmas kick in for concrete M₁✶ before it can add another start. This can be made more explicit by writing instead
```
  rw [← dual_inj]; simp
```

Reversing duplicate lemmas

@[simp]
theorem mem_affineSpan_singleton : p₁ ∈ affineSpan k ({p₂} : Set P) ↔ p₁ = p₂ := by
  simp [← mem_coe, - SetLike.mem_coe]

The mem_coe here is AffineSubspace.mem_coe. There is also SetLike.mem_coe in the simp set, so they will conflict now. This can be fixed by disabling the other

  simp [← mem_coe, - SetLike.mem_coe]

or writing

  simp [← SetLike.mem_coe]

Known deficiencies of the initial implementation:

It could also check at @[simp] attribution application time.
It could check the whole simp set at the end (via an environment linter). Maybe this is functionality that is better suited, thought, to be implemented like the simpNF linter in Batteries.
The warning could come with a clickable hint (removing a simp argument, or adding - foo for a simp theorem).
The warning does not mention when an unfolding is part of the loop (simp [f, g_eq_f])
The warning does no explain what f.eq_1 means.
When the linter is off, simp could suggest turnig it on in the “maximum recursion depth has been reached” message (e.g. to benefit mathlib)
It was suggestd that it would be nice to be able write simp -loopProtection … instead of set_option linter.simp.loopProtection false in simp …. This is plausible, but needs some preparation to allow good interaction between options and simp config flags.

digama0 · 2025-06-08T19:45:26Z

Does this need to be a flag? If it will definitely loop, then no simp call in the wild could be doing it because it would cause timeouts.

nomeata · 2025-06-08T19:54:26Z

This is still rather early WIP and I’m still in the process of figuring out if this should be a flag, or an option, or both.

Note that the check may be expensive (TBD), and that the check can have false positives if for the concrete values the lemma is instantiated with the RHS can be rewritten some other, terminating way. So an opt-out is likely needed.

leanprover-community-bot · 2025-06-08T20:04:39Z

Mathlib CI status (docs):

❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-08 20:04:39)
🟡 Mathlib branch lean-pr-testing-8688 build against this PR was cancelled. (2025-06-11 16:08:28) View Log
🟡 Mathlib branch lean-pr-testing-8688 build against this PR was cancelled. (2025-06-11 16:31:35) View Log
💥 Mathlib branch lean-pr-testing-8688 build failed against this PR. (2025-06-11 16:51:20) View Log
💥 Mathlib branch lean-pr-testing-8688 build failed against this PR. (2025-06-11 17:12:53) View Log
💥 Mathlib branch lean-pr-testing-8688 build failed against this PR. (2025-06-12 11:14:57) View Log
💥 Mathlib branch lean-pr-testing-8688 build failed against this PR. (2025-06-12 17:07:56) View Log
💥 Mathlib branch lean-pr-testing-8688 build failed against this PR. (2025-06-17 14:49:52) View Log
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-06-17 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-17 15:27:18)
💥 Mathlib branch lean-pr-testing-8688 build failed against this PR. (2025-06-17 15:28:24) View Log
💥 Mathlib branch lean-pr-testing-8688 build failed against this PR. (2025-06-17 16:42:02) View Log

nomeata · 2025-06-08T21:06:17Z

!bench

leanprover-bot · 2025-06-08T21:11:32Z

Here are the benchmark results for commit 94269c5.
The entire run failed.
Found no significant differences.

nomeata · 2025-06-11T14:10:41Z

!bench

leanprover-bot · 2025-06-11T14:48:40Z

Here are the benchmark results for commit 889fba0.
There were significant changes against commit 8904e5c:

  Benchmark                              Metric                    Change
  ==================================================================================
- Init.Data.BitVec.Lemmas                branches                    5.9%  (204.2 σ)
- Init.Data.BitVec.Lemmas                instructions                5.5%  (169.1 σ)
- Init.Data.BitVec.Lemmas re-elab        branches                    5.5%  (321.5 σ)
- Init.Data.BitVec.Lemmas re-elab        instructions                5.1%  (285.3 σ)
- Init.Data.List.Sublist async           branches                    4.5%  (111.6 σ)
- Init.Data.List.Sublist async           instructions                4.4%   (97.7 σ)
- Init.Data.List.Sublist re-elab -j4     branch-misses               2.8%   (47.1 σ)
- Init.Data.List.Sublist re-elab -j4     branches                    3.9%   (65.1 σ)
- Init.Data.List.Sublist re-elab -j4     instructions                3.9%   (77.7 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branch-misses               8.0%   (45.6 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branches                    9.3%  (712.3 σ)
- Std.Data.DHashMap.Internal.RawLemmas   instructions                9.5%  (647.7 σ)
- Std.Data.Internal.List.Associative     branches                    8.9% (1485.9 σ)
- Std.Data.Internal.List.Associative     instructions                8.9% (1226.1 σ)
+ bv_decide_realworld                    maxrss                     -4.0%  (-30.5 σ)
+ stdlib                                 attribute application      -1.2%  (-46.9 σ)
- stdlib                                 instructions                1.9%  (292.5 σ)
+ stdlib                                 process pre-definitions    -2.3%  (-42.2 σ)

…mp-loop-detection

nomeata · 2025-06-17T15:15:26Z

!bench

leanprover-bot · 2025-06-17T15:41:40Z

Here are the benchmark results for commit 34659c4.
There were significant changes against commit 3b2990b:

  Benchmark                              Metric                  Change
  ================================================================================
- Init.Data.BitVec.Lemmas                branch-misses             2.3%   (37.4 σ)
- Init.Data.BitVec.Lemmas                branches                  3.5%  (256.8 σ)
- Init.Data.BitVec.Lemmas                instructions              3.3%  (219.0 σ)
- Init.Data.BitVec.Lemmas re-elab        branches                  3.3%   (62.1 σ)
- Init.Data.BitVec.Lemmas re-elab        instructions              3.1%   (60.5 σ)
- Init.Data.BitVec.Lemmas re-elab        task-clock                2.5%   (36.7 σ)
- Init.Data.List.Sublist async           branches                  2.6%   (67.5 σ)
- Init.Data.List.Sublist async           instructions              2.5%   (58.4 σ)
- Init.Data.List.Sublist re-elab -j4     branches                  2.3%   (42.6 σ)
- Init.Data.List.Sublist re-elab -j4     instructions              2.2%   (47.6 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branches                 12.1% (1452.5 σ)
- Std.Data.DHashMap.Internal.RawLemmas   instructions             12.3% (1228.7 σ)
- Std.Data.Internal.List.Associative     branch-misses             8.8%   (32.7 σ)
- Std.Data.Internal.List.Associative     branches                 10.2%  (531.1 σ)
- Std.Data.Internal.List.Associative     instructions             10.2%  (465.2 σ)
- lake config elab                       instructions              2.7%  (205.3 σ)
- lake config import                     instructions              5.1%  (175.1 σ)
- lake config tree                       instructions              4.8%  (168.4 σ)
- lake env                               instructions              5.1%  (190.9 σ)
- stdlib                                 blocked (unaccounted)    11.6%   (28.9 σ)
- stdlib                                 instructions              3.1% (2285.9 σ)
- stdlib                                 tactic execution         63.5%   (37.7 σ)
- stdlib                                 task-clock                4.7%   (35.3 σ)
- stdlib                                 wall-clock                2.1%   (23.4 σ)

nomeata · 2025-06-17T15:59:21Z

Yuck, I was hoping by checking just the simp arguments these numbers would be much better :-(

nomeata · 2025-06-18T07:45:50Z

!bench

leanprover-bot · 2025-06-18T08:27:41Z

Here are the benchmark results for commit 13755a0.
There were significant changes against commit 3b2990b:

  Benchmark                              Metric                    Change
  ===================================================================================
- Init.Data.BitVec.Lemmas                branches                    3.5%   (165.0 σ)
- Init.Data.BitVec.Lemmas                instructions                3.3%   (144.5 σ)
- Init.Data.BitVec.Lemmas re-elab        branches                    3.3%    (60.0 σ)
- Init.Data.BitVec.Lemmas re-elab        instructions                3.1%    (60.7 σ)
- Init.Data.List.Sublist async           branches                    2.6%    (85.2 σ)
- Init.Data.List.Sublist async           instructions                2.5%    (75.2 σ)
- Init.Data.List.Sublist re-elab -j4     branches                    2.2%    (90.0 σ)
- Init.Data.List.Sublist re-elab -j4     instructions                2.2%    (95.5 σ)
- Init.Data.List.Sublist re-elab -j4     wall-clock                  2.5%   (121.4 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branch-misses               9.4%    (39.7 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branches                   12.1%   (741.1 σ)
- Std.Data.DHashMap.Internal.RawLemmas   instructions               12.3%   (651.7 σ)
- Std.Data.Internal.List.Associative     branch-misses               8.7%    (29.9 σ)
- Std.Data.Internal.List.Associative     branches                   10.2%   (751.5 σ)
- Std.Data.Internal.List.Associative     instructions               10.2%   (670.6 σ)
- bv_decide_large_aig.lean               task-clock                  7.9%    (38.5 σ)
- bv_decide_large_aig.lean               wall-clock                  7.7%    (42.3 σ)
- bv_decide_mod                          task-clock                  7.6%   (536.1 σ)
- bv_decide_mod                          wall-clock                  7.6%    (93.6 σ)
- lake config elab                       instructions                2.7%   (209.7 σ)
- lake config import                     instructions                5.1%   (126.7 σ)
- lake config tree                       instructions                4.8%   (156.1 σ)
- lake env                               instructions                5.1%   (197.6 σ)
- qsort                                  task-clock                 13.7%    (25.0 σ)
- qsort                                  wall-clock                 13.7%    (24.8 σ)
- stdlib                                 blocked                     8.8%   (488.3 σ)
+ stdlib                                 grind                      -2.6%  (-143.2 σ)
- stdlib                                 instructions                3.1% (11334.2 σ)
- stdlib                                 process pre-definitions     2.3%    (85.5 σ)
- stdlib                                 tactic execution           58.3%    (33.3 σ)
- stdlib                                 task-clock                  4.3%    (28.4 σ)
- tests/bench/ interpreted               task-clock                  5.8%    (47.4 σ)
+ workspaceSymbols                       task-clock                 -9.0%   (-91.5 σ)
+ workspaceSymbols                       wall-clock                 -9.1%   (-89.6 σ)

nomeata · 2025-06-21T17:57:38Z

I’ll pursue #8865 instead.

This PR refactors the way simp arguments are elaborated: Instead of changing the `SimpTheorems` structure as we go, this elaborates each argument to a more declarative description of what it does, and then apply those. This enables more interesting checks of simp arguments that need to happen in the context of the eventually constructed simp context (the checks in #8688), or after simp has run (unused argument linter #8901). The new data structure describing an elaborated simp argument isn’t the most elegant, but follows from the code. While I am at it, move handling of `[*]` into `elabSimpArgs`. Downstream adaption branches exist (but may not be fully up to date because of the permission changes). While I am at it, I cleaned up `SimpTheorems.lean` file a bit (sorting declarations, mild renaming) and added documentation.

This PR allows `simp` to recognize and warn about simp lemmas that are likely looping in the current simp set. It does so automatically whenever simplification fails with the dreaded “max recursion depth” error fails, but it can be made to do it always with `set_option linter.loopingSimpArgs true`. This check is not on by default because it is somewhat costly, and can warn about simp calls that still happen to work. This closes #5111. In the end, this implemented much simpler logic than described there (and tried in the abandoned #8688; see that PR description for more background information), but it didn’t work as well as I thought. The current logic is: “Simplify the RHS of the simp theorem, complain if that fails”. It is a reasonable policy for a Lean project to say that all simp invocation should be so that this linter does not complain. Often it is just a matter of explicitly disabling some simp theorems from the default simp set, to make it clear and robust that in this call, we do not want them to trigger. But given that often such simp call happen to work, it’s too pedantic to impose it on everyone.

This PR refactors the way simp arguments are elaborated: Instead of changing the `SimpTheorems` structure as we go, this elaborates each argument to a more declarative description of what it does, and then apply those. This enables more interesting checks of simp arguments that need to happen in the context of the eventually constructed simp context (the checks in leanprover#8688), or after simp has run (unused argument linter leanprover#8901). The new data structure describing an elaborated simp argument isn’t the most elegant, but follows from the code. While I am at it, move handling of `[*]` into `elabSimpArgs`. Downstream adaption branches exist (but may not be fully up to date because of the permission changes). While I am at it, I cleaned up `SimpTheorems.lean` file a bit (sorting declarations, mild renaming) and added documentation.

This PR allows `simp` to recognize and warn about simp lemmas that are likely looping in the current simp set. It does so automatically whenever simplification fails with the dreaded “max recursion depth” error fails, but it can be made to do it always with `set_option linter.loopingSimpArgs true`. This check is not on by default because it is somewhat costly, and can warn about simp calls that still happen to work. This closes leanprover#5111. In the end, this implemented much simpler logic than described there (and tried in the abandoned leanprover#8688; see that PR description for more background information), but it didn’t work as well as I thought. The current logic is: “Simplify the RHS of the simp theorem, complain if that fails”. It is a reasonable policy for a Lean project to say that all simp invocation should be so that this linter does not complain. Often it is just a matter of explicitly disabling some simp theorems from the default simp set, to make it clear and robust that in this call, we do not want them to trigger. But given that often such simp call happen to work, it’s too pedantic to impose it on everyone.

feat: simp +loopProtection

1816815

nomeata force-pushed the joachim/simp-loop-detection branch from f320905 to 1816815 Compare June 8, 2025 19:39

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jun 8, 2025

Experiment with enabling it by default

94269c5

Adapt init

c1129f7

nomeata added 2 commits June 8, 2025 23:37

More adjustments to init

bbc0cdc

Do not use perm rules during checking

606670f

github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Jun 8, 2025

nomeata added 4 commits June 11, 2025 10:20

Even more adjustments to init

d1f996e

Tricky test

789213c

Some refactoring

2df0ced

Update test

c97d911

nomeata force-pushed the joachim/simp-loop-detection branch from e85650a to c97d911 Compare June 11, 2025 08:46

github-actions bot removed the changes-stage0 Contains stage0 changes, merge manually using rebase label Jun 11, 2025

nomeata added 5 commits June 11, 2025 10:53

Compare whole SimpTheorem

11ccd5e

Boolean blindness

514ef77

Better loop protection during loop protection

715c469

Cleaner code structure, use state not exceptions

bb30b64

Adapt for bootstrapping

2d92fca

nomeata added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Jun 11, 2025

nomeata added 2 commits June 11, 2025 16:11

Merge ../lean4-stage2 into joachim/simp-loop-detection

889fba0

Undo toolchain change

141637b

Add hints to error message

4b9f107

nomeata added 2 commits June 17, 2025 12:10

stash

fb0bd52

Warn eagerly on simp arguments

84b23d9

nomeata mentioned this pull request Jun 17, 2025

refactor: simp arg elaboration #8815

Merged

nomeata added 2 commits June 17, 2025 15:36

Docstrings

ab7e3ac

Remove simp config, phrase as linter option

982293d

nomeata mentioned this pull request Jun 17, 2025

chore: adaptions for https://github.com/leanprover/lean4/pull/8688 leanprover-community/mathlib4#26032

Closed

nomeata changed the title ~~feat: simp +loopProtection~~ feat: linter.simp.loopProtection Jun 17, 2025

Fix tests

1a34047

nomeata changed the base branch from master to nightly-with-mathlib June 17, 2025 14:38

stage2 adaptions

1f076b1

nomeata force-pushed the joachim/simp-loop-detection branch from 0e3ae4d to 1f076b1 Compare June 17, 2025 14:42

Merge branch 'nightly' of github.com:leanprover/lean4 into joachim/si…

60b8fc4

…mp-loop-detection

nomeata changed the base branch from nightly-with-mathlib to nightly June 17, 2025 14:55

more stage2 adaptions

34659c4

nomeata mentioned this pull request Jun 17, 2025

refactor: SimpM.run #8843

Merged

Kick CI

13755a0

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 17, 2025

Update lean-toolchain for leanprover/lean4#8688

eaa67fd

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 17, 2025

Update lean-toolchain for leanprover/lean4#8688

1c05859

nomeata mentioned this pull request Jun 18, 2025

feat: linter.loopingSimpArgs #8865

Merged

nomeata closed this Jun 21, 2025

feat: linter.simp.loopProtection #8688

feat: linter.simp.loopProtection #8688

Uh oh!

Conversation

nomeata commented Jun 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

digama0 commented Jun 8, 2025

Uh oh!

nomeata commented Jun 8, 2025

Uh oh!

leanprover-community-bot commented Jun 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Jun 8, 2025

Uh oh!

leanprover-bot commented Jun 8, 2025

Uh oh!

nomeata commented Jun 11, 2025

Uh oh!

leanprover-bot commented Jun 11, 2025

Uh oh!

nomeata commented Jun 17, 2025

Uh oh!

leanprover-bot commented Jun 17, 2025

Uh oh!

nomeata commented Jun 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Jun 18, 2025

Uh oh!

leanprover-bot commented Jun 18, 2025

Uh oh!

nomeata commented Jun 21, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

nomeata commented Jun 8, 2025 •

edited

Loading

leanprover-community-bot commented Jun 8, 2025 •

edited

Loading

nomeata commented Jun 17, 2025 •

edited

Loading