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.