simpNF lint with hyps

Stream: mathlib4

[Jovan Gerbscheid]

For linter claims that LHS doesn't simplify, but it does, it seems that the simpNF linter runs simp instead of simp [*], which is why simpNF can't simplify the LHS. Should this be changed?

[Johan Commelin]

That sounds good to me

[Johan Commelin]

Would a patch like this make sense?

diff --git a/Batteries/Tactic/Lint/Simp.lean b/Batteries/Tactic/Lint/Simp.lean
index 3e83431d..ce585f5d 100644
--- a/Batteries/Tactic/Lint/Simp.lean
+++ b/Batteries/Tactic/Lint/Simp.lean
@@ -109,12 +109,18 @@ https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20for
   test := fun declName => do
     unless ← isSimpTheorem declName do return none
     let ctx ← Simp.Context.mkDefault
-    checkAllSimpTheoremInfos (← getConstInfo declName).type fun {lhs, rhs, isConditional, ..} => do
+    checkAllSimpTheoremInfos (← getConstInfo declName).type
+      fun {lhs, rhs, isConditional, hyps, ..} => do
+      -- add the local hypotheses to the simp context
+      let mut simpTheorems := ctx.simpTheorems
+      for h in hyps do
+        simpTheorems ← simpTheorems.addTheorem (.fvar h.fvarId!) h
+      let ctxHyps := ctx.setSimpTheorems simpTheorems
       let isRfl ← isRflTheorem declName
       let ({ expr := lhs', proof? := prf1, .. }, prf1Stats) ←
         decorateError "simplify fails on left-hand side:" <|
           if !isRfl then
-            simp lhs ctx
+            simp lhs ctx <|> simp lhs ctxHyps
           else do
             let (e, s) ← dsimp lhs ctx
             return (Simp.Result.mk e .none .true, s)

[Notification Bot]

3 messages were moved here from #mathlib4 > Technical Debt Counters by Johan Commelin.

[Jovan Gerbscheid]

Why wouldn't we just overwrite ctx with the extended context?

[Johan Commelin]

Maybe there is value in checking if something can be simped unconditionally?

[Johan Commelin]

But maybe we actually don't care.

[Jovan Gerbscheid]

You might want to add an isProp check (to the free variable type) before simpTheorems.addTheorem. hyps contains all of the free variables. (I think you'll get an error otherwise)

[Johan Commelin]

https://github.com/leanprover-community/batteries/pull/1214 contains my attempt.

[Johan Commelin]

Jovan Gerbscheid said:

You might want to add an isProp check (to the free variable type) before simpTheorems.addTheorem. hyps contains all of the free variables. (I think you'll get an error otherwise)

Good idea. Pushed that to the PR.

[Johan Commelin]

I'm removing 3 @[simp] attributes that are now flagged by the linter.

I tested, and indeed, these lemmas do not fire on their own LHS, even with simp [*].

https://github.com/leanprover-community/batteries/pull/1214/commits/8e47a2ac82ea7d0ccaaa2dbb5eaf1c516c491999

[Johan Commelin]

@Jovan Gerbscheid I've tested this out on mathlib, and we get 184 new linter warnings.
For example:

/-- The product of `f` over `insert a s` is the same as
the product over `s`, as long as `f a = 1`. -/
@[to_additive (attr := simp) "The sum of `f` over `insert a s` is the same as
the sum over `s`, as long as `f a = 0`."]
theorem prod_insert_one [DecidableEq ι] (h : f a = 1) : ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x :=
  prod_insert_of_eq_one_if_not_mem fun _ => h

-- Indeed, this lemma can be proven using `simp [*]` but not by `simp`.

theorem prod_insert_one' [DecidableEq ι] (h : f a = 1) : ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x := by
  simp [*]

[Johan Commelin]

So, I guess a general question for people to chime in on: do we want lemmas like prod_insert_one in our simp set, if simp [*] can already prove them...

[Jovan Gerbscheid]

Isn't this lemma overshadowed by docs#Finset.prod_insert_of_eq_one_if_not_mem ? I seems like it should clearly not have a @[simp] tag.

[Johan Commelin]

Indeed, that is exactly what the linter now reports:

././././Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean:51:1: error: @Finset.prod_insert_one simp can prove this:
  by simp only [implies_true, @Finset.prod_insert_of_eq_one_if_not_mem]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].

[Johan Commelin]

For the record, here is the full linter output: https://github.com/leanprover-community/mathlib4/actions/runs/14712661498/job/41288687885#step:25:21

[Jovan Gerbscheid]

I think many of the new warnings are valid warnings, however it mistakenly chokes on docs#Equiv.Perm.support_subtype_perm, because it has a hypothesis h : ∀ (x : α), x ∈ s ↔ f x ∈ s). And then simp [h] loops forever.

[Jovan Gerbscheid]

I think simp should have an option that determines whether local simp theorems that are equalities (or iff) are turned into rewriting simp theorem, or just theorems that simplify a statement into true. Then we can use it in simpNF to avoid these kinds of looping rewrites with hypotheses that weren't meant for rewriting.

[Johan Commelin]

I've pushed a whole bunch of fixes to branch#batteries-pr-testing-1214

[Johan Commelin]

Many of those can be backported to master indep of this linter change.

[Jovan Gerbscheid]

It seems that any "higher order" simp theorem gets flagged by the new linter, e.g.

lemma monovaryOn_inv_left₀ (hf : ∀ i ∈ s, 0 < f i) : MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s

which has a hypothesis that has a hypothesis. It seems like this simp lemma should be able to apply to itself, but the problem is that contextual is set to false by default. This means that when simplifying 0 < f i, the discharger doesn't have access to the i ∈ s hypothesis that is needed to apply hf. It does get solved by simp +contextual [*].

[Johan Commelin]

So... should the linter also try +contextual?
Or should we just not have such higher order simp lemmas in the default set?

[Jovan Gerbscheid]

We could put the @[simp] tag on a simpler version of the theorem without the i ∈ s hypothesis. On the other hand, the extra hypothesis doesn't do any harm, and is beneficial if we have +contextual.

[Jovan Gerbscheid]

Johan Commelin said:

So... should the linter also try +contextual?

I think that would be a reasonable workaround.

[Jovan Gerbscheid]

Interestingly, if we have a "higher higher order" simp theorem (having a hypothesis in a hypothesis in a hypothesis), then the linter will complain due to maxDischargeDepth := 2 :)

[Johan Commelin]

Clearly we should draw a line somewhere. :grinning:

[Johan Commelin]

@Jovan Gerbscheid btw, please feel free to push to the batteries PR if you have some ideas

[Jovan Gerbscheid]

I don't have write access for batteries. But the change I wanted to make is replacing

    let ctx ← Simp.Context.mkDefault

with

    let ctx ← Simp.mkContext (config := { contextual := true })
      (simpTheorems := #[(← getSimpTheorems)]) (congrTheorems := (← getSimpCongrTheorems))

[Johan Commelin]

Thanks, I pushed that change.

[Kim Morrison]

It looks like there are some further linting failures on branch#batteries-pr-testing-1214.

[Kim Morrison]

Ping me when when you'd like this merged.

[Jovan Gerbscheid]

The awkward thing about setting contextual to true, is that a lemma like not_imp_self : ¬a → a ↔ a now gets solved by simpNF (because it introduces ¬a to its context, thus simplifying a to False).

As a workaround, we could only set contextual to true if we detect that the lemma is higher order.

[Jovan Gerbscheid]

I made a pr where I only use +contextual in simpNF when it might need it: https://github.com/leanprover-community/batteries/pull/1220

But it seems the automatically generated mathlib branch isn't compatible.

[Johan Commelin]

Thanks, that's a lot more sophisticated (-;

[Johan Commelin]

Jovan Gerbscheid said:

But it seems the automatically generated mathlib branch isn't compatible.

I fear that it is caught in limbo between the 4.19 and 4.20-rc{1,2} releases.

[Johan Commelin]

@Jovan Gerbscheid I pushed an update to branch#batteries-pr-testing-1220 that moves to v4.20-rc2

[Johan Commelin]

Only 10 linter errors! https://github.com/leanprover-community/mathlib4/actions/runs/14807683945

[Johan Commelin]

I got confused by Github. It's actually 165 errors :expressionless:

[Johan Commelin]

There are still quite a few of the form

Mathlib/Topology/VectorBundle/Constructions.lean:83:1: error: Trivialization.coordChangeL_prod
Left-hand side does not simplify, when using the simp lemma on itself.

[Jovan Gerbscheid]

In that lemma, it looks like the hypothesis is not in simp normal form. So we should either remove the @[simp] tag, or change the hypothesis to be in normal form.

[Johan Commelin]

Aah, good catch. Maybe the linter should now warn about that possibility?

[Jovan Gerbscheid]

Good idea, I made a change so that the linter now tells you explicitly when a hypothesis is not in simp normal form.

[Johan Commelin]

@Jovan Gerbscheid What do you think of a case like this:

@[simp]
theorem support_subtype_perm [DecidableEq α] {s : Finset α} (f : Perm α) (h) :
    (f.subtypePerm h : Perm s).support = ({x | f x ≠ x} : Finset s) := by
  ext; simp [Subtype.ext_iff]

https://github.com/leanprover-community/mathlib4/blob/95eff173b853f2ce190e3c085d7bdcf349be71f6/Mathlib/GroupTheory/Perm/Support.lean#L655

Here h is

h : ∀ (x : α), x ∈ s ↔ f x ∈ s

This causes a loop when feeding h to simp.
(Arguably subtypePerm should not take h in that form, but swap the two sides.)

But more importantly: I think that in this case the linter should not run simp [h] but should run just simp, because it will still apply the lemma, with h determined by unification.

[Jovan Gerbscheid]

Ideally, we could run simp [h] in a way where the lemma added to the simp context is saying that for any x, (x ∈ s ↔ f x ∈ s) = True, instead of interpreting it as rewrite lemma. This would avoid the blowup in rewriting, but would still allow the linter to work in general. But this would require a change in core.

Even better would be if simp could detect when lemmas cause a blowup, and then swap the direction of the rewrite automatically. This would be useful in e.g. aesop which makes calls to simp_all.

[Johan Commelin]

@Jovan Gerbscheid But do you think we could instead detect that h can be determined by unification?

[Johan Commelin]

Or should the linter just try simp before attempting simp [h]?

[Johan Commelin]

(Aside: #24833 fixes the order of the argument to subtypePerm.)

[Jovan Gerbscheid]

The lemma that initiated this discussion, docs#LinearMap.linearProjOfIsCompl_of_proj, has a type where it looks like the hypothesis may be possible to infer from unification, but it actually can't . So if we were to try that approach, then this one would need to keep its nolint simpNF tag.

[Johan Commelin]

When you say "try that approach", which of the two that I mentioned are you referring to?

[Jovan Gerbscheid]

I meant to use simp instead of simp [h] for hypotheses h that appear on the LHS

[Johan Commelin]

Aha, but what about the second approach: where the linter tries simp, and if that fails, simp [h].

[Jovan Gerbscheid]

Yes, that would work in this case. But what about encouraging people to always write their equalities/iff in an order that works well with simp? Just like what you're doing in #24833.

[Johan Commelin]

Maybe that's good enough...

[Johan Commelin]

I'm confused by

-- Mathlib.CategoryTheory.Idempotents.Karoubi
#check @CategoryTheory.Idempotents.Karoubi.Hom.mk.injEq /- LINTER FAILED:
simplify fails on left-hand side:
tactic 'simp' failed, nested error:
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information -/

This is an autogenerated lemma... and I don't see where it ends up in the simp set...

[Aaron Liu]

I think these are automatically put in the simp set

[Johan Commelin]

Hmmmzz... so maybe we shouldn't do that?

[Jovan Gerbscheid]

Or we swap the sides of docs#CategoryTheory.Idempotents.Karoubi.Hom.comm :)

[Johan Commelin]

Can you explain why that would help? Is that something the linter could detect and suggest?

[Jovan Gerbscheid]

The problematic simp lemma has a hypothesis comm : f = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f Q.p), which causes the blowup, so that would be fixed. And similar to #24833, it seems generally more useful to state an equality in the direction that can be used by simp.

[Johan Commelin]

Thanks! #24848 should fix Karoubi.

[Johan Commelin]

#24851 patches a bunch of proofs that can be simp [*], and removes the @[simp] attribute from those lemmas.

[Johan Commelin]

#24926 is another such batch

[Johan Commelin]

Also, if there are further comment on #24833, please let me know. It's also on the roadmap to this improved simpNF linter.

[Michael Rothgang]

I have a question from the peanut gallery: could un-marking lemmas as simp potentially break any proofs? Sure, replacing simp by simp [*] should "always" fix this work (perhaps unless local hypotheses are contradictory)... is there a saving grace I'm not yet aware of?

[Johan Commelin]

I don't think it should break anything. If some proof X in the pastsimp used some conditional lemma foo, it would have had to fill in the hypothesis of foo. But if foo can be proved by simp [*], using some lower level conditional lemmas, then those hypotheses should now also be provable by simp in the proof of X.

[Johan Commelin]

There are 80 linter errors left on branch#batteries-pr-testing-1220
See https://github.com/leanprover-community/mathlib4/actions/runs/15039232241/job/42266873368

[Yaël Dillies]

It should break only long chains of conditional lemmas, as those might be pushed over the depth limit of simp

[Johan Commelin]

#24961 is another batch

[Johan Commelin]

#25024 puts a bunch of hypotheses in simp normal form (and other minor improvements to the simp set)

[Johan Commelin]

@Jovan Gerbscheid What do you think of

@[simp]
lemma Adj.right_mem (h : G.Adj x y) : y ∈ V(G) :=
  h.symm.left_mem

https://github.com/leanprover-community/mathlib4/blob/d6c3a2d285e461d43a0bed7d7a2aa51fce4de3d9/Mathlib/Combinatorics/Graph/Basic.lean#L293
which errors with

Error: /home/lean/actions-runner/_work/mathlib4/mathlib4/Mathlib/Combinatorics/Graph/Basic.lean:293:1: error: @Graph.Adj.right_mem Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.

[Johan Commelin]

Can we provide a more precise reason why this is a bad simp-lemma?

[Jovan Gerbscheid]

Yes, because arguments x cannot be determined. I think I could make the linter warn explicitly about this kind of situation.

[Johan Commelin]

Ooh, thanks for pointing it out! Yes, if you can automate that warning message, it would be really great.

[Johan Commelin]

This could possibly even run as an online-linter, right? As soon as the @[simp] attribute is added, we can run those checks.

[Jovan Gerbscheid]

Arguably, we can have a linter which checks if simp only [my_lemma] solves the lemma. This can run immediately. And then we also keep the linter that uses the global simp set. This runs at the end.

[Johan Commelin]

simp only [my_lemma, my, hyps], but yes, I think we should have both those linters.

[Michael Rothgang]

If you make this a syntax linter, I'm happy to review the "syntax"-y aspects of it.

[Jovan Gerbscheid]

The implementation will be the same as the current linter, just replacing the whole simp set by just the lemma. So not a syntax linter.

[Jovan Gerbscheid]

Johan Commelin said:

Yes, if you can automate that warning message, it would be really great.

I've pushed a change that should do this.

[Jovan Gerbscheid]

I think adding the online simp linter can go in a later PR.

[François G. Dorais]

Sorry, just coming back after many weeks of busy IRL work: tldr... What is the current status for batteries#1220?

[Jovan Gerbscheid]

@Johan Commelin has fixed a bunch of simp lemmas on the master branch of mathlib to satisfy the new linter. There are now 25 errors left to fix before we can merge batteries#1220.

[Johan Commelin]

Why is this a bad simp lemma?
https://github.com/leanprover-community/mathlib4/blob/401dce0e8e36a1011330773466b2c6c1b3683a29/Mathlib/NumberTheory/ArithmeticFunction.lean#L547

@[simp]
theorem map_mul_of_coprime {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {m n : ℕ}
    (h : m.Coprime n) : f (m * n) = f m * f n :=
  hf.2 h
/-
-- Mathlib.NumberTheory.ArithmeticFunction
Error: /home/lean/actions-runner/_work/mathlib4/mathlib4/Mathlib/NumberTheory/ArithmeticFunction.lean:546:1:
error: @ArithmeticFunction.IsMultiplicative.map_mul_of_coprime Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.
-/

[Johan Commelin]

There are now 15 cases left: https://github.com/leanprover-community/mathlib4/actions/runs/15434053802/job/43436958608

All of them are of the form

Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.

[Kevin Buzzard]

Random comment: I've seen that error plenty of times before and it turns out that sometimes it's a lie, in the sense that the simp lemma seems to fire just fine. I've nolinted this warning away in the past

[Johan Commelin]

I wonder whether we should just nolint these 15, and merge the improved linter.
Then we can investigate the existing 38 + 15 nolints after that.

[Johan Commelin]

• #25419 chore(Topology): remove @[simp] when simp can prove

Mathlib/Topology/FiberBundle/Trivialization.lean | 6 +++---
Mathlib/Topology/VectorBundle/Basic.lean | 9 +++++----
Mathlib/Topology/VectorBundle/Constructions.lean | 2 +-
3 files changed, 9 insertions(+), 8 deletions(-)

[Johan Commelin]

• #25420 chore(Data/List/EditDistance): put fields in simp-normal form

1 file changed, 13 insertions(+), 13 deletions(-)

[Jovan Gerbscheid]

The problem is in Coprime:

abbrev Coprime (m n : Nat) := Nat.gcd m n = 1

@[simp] theorem coprime (m n : Nat) : Coprime m n := sorry

example (m n : Nat) : Coprime m n := by
  simp -- simp made no progress

[Kenny Lau]

and it works when I replace abbrev with def

[Jovan Gerbscheid]

For the remaining lemmas:

• closure_sdiff_eq_closure causes a recursive blowup, because the lemma applies to its own hypothesis
• Finset.prod_image, Finset.fold_image and List.toFinset_filterMap have hypotheses that are too strong to be useful simp lemmas
• List.Vector.mapAccumr₂_unused_input_right and friends have a hypothesis that f doesn't depend on one of its arguments. I think instead of

theorem mapAccumr₂_unused_input_right [Inhabited β] (f : α → β → σ → σ × γ)
    (h : ∀ a b s, f a default s = f a b s)

it should state

theorem mapAccumr₂_unused_input_right (f : α → β → σ → σ × γ) {f' : α → σ → σ × γ}
    (h : ∀ a b s, f a b s = f' a s)

simp should be able to figure out the value of f' exactly in the case that f doesn't depend on its second argument. And then we can also use f' in the conclusion of the statement.

[Jovan Gerbscheid]

For Coprime, I think we need to inline the definition of Coprime, so that the hypothesis becomes m.gcd n = 1

[Jovan Gerbscheid]

Out of the existing nolint simpNF, 19 are labelled with a comment like

-- It seems the side condition `hf` is not applied by `simpNF`.

These should hopefully all correctly pass the new simpNF linter. (the labels were added in #23201 by @Anne Baanen)

[Johan Commelin]

@Jovan Gerbscheid Thanks for those investigations! I pushed a commit that fixes them.

[Jovan Gerbscheid]

Actually, fold_image and prod_image could probably remain a simp lemma if they used Set.injOn, instead of writing out the injectivity

[Johan Commelin]

Looks like we should do something like that, in order to keep the build working: https://github.com/leanprover-community/mathlib4/actions/runs/15442001546/job/43461831048#step:25:20

[Jovan Gerbscheid]

I added a simp lemma for simplifying Set.InjOn that should hopefully fix the places where proofs broke.

[Johan Commelin]

But some of the proofs that broke weren't using simp but eg rw. Those still need to be fixed by hand, right?

[Johan Commelin]

I'm working on that now.

[Jovan Gerbscheid]

The simp lemma that I added fixes the proof of Units.mk0_prod, without needing to pass Set.InjOn to simp. Feel free to remove it though.

[Jovan Gerbscheid]

But in that case I think it's clearer to unsimp prod_image, and pass it manually to simp as well.

[Johan Commelin]

I think your lemma is fine

[Johan Commelin]

My local build is at ~ 6000/6700

[Johan Commelin]

Local build is done. Running local lint now

[Johan Commelin]

Linting passed locally!

[Johan Commelin]

I'm trying to remove existing nolints on branch#jmc-nolint-simpnf

[Johan Commelin]

@Kim Morrison @François G. Dorais @Mario Carneiro

feat: simpNF to check lemmas with conditions batteries#1220

is now ready for review, and a testing branch of mathlib builds against this PR

[Johan Commelin]

$ rg -il "nolint simpnf" Mathlib
Mathlib/Topology/Specialization.lean
Mathlib/Data/NNRat/Defs.lean
Mathlib/Data/WSeq/Relation.lean
Mathlib/Data/Seq/Computation.lean
Mathlib/Data/Seq/Seq.lean
Mathlib/Computability/TMToPartrec.lean
Mathlib/CategoryTheory/WithTerminal/Basic.lean

[Johan Commelin]

The remaining ones all have to do with either LHS not being in simp normal form, or with auto-generated match lemmas that can be proven by simp.

[Jovan Gerbscheid]

When working on #25515, I discovered a small bug in the simpNF linter. I've make a fix at batteries#1266

[Johan Commelin]

Jovan asks a good question here: https://github.com/leanprover-community/mathlib4/pull/25515#discussion_r2151910631
In a situation where we have

@[reassoc (attr := simp), elementwise (attr := simp)]
lemma foo

the lemma foo gets tagged with simp twice. This doesn't seem to be too problematic, because it is an idempotent effect. But is this idiomatic, or should this be done differently?

[Jovan Gerbscheid]

What about a syntax (attr only := simp), to only add the attribute to the generated declaration and not the original?