!4#2104 simpNF error in other files

Stream: mathlib4

[Jon Eugster]

In !4#2104 there were simpNF linting errors in files that seem unrelated to the one that has been ported. One such case boils down to the following MWE:

import Mathlib.Algebra.Module.Basic -- just an import to get the linter

-- File one

variable (x y : PUnit)

instance : Mul PUnit where
  mul _ _ := PUnit.unit

@[simp]
theorem lemma₁ : x * y = unit :=
  rfl

#lint -- succeeds: lemma₁ is in simpNF.


-- File two
class BooleanRing (α) extends Mul α where
  mul_self : ∀ a : α, a * a = a

@[simp]
theorem lemma₂ [BooleanRing α] (a : α) : a * a = a :=
  BooleanRing.mul_self _

instance : BooleanRing PUnit :=
  ⟨fun _ => Subsingleton.elim _ _⟩

#lint only simpNF -- fail: lemma₁ is *not* in simpNF anymore.

i.e. after the instance BooleanRing PUnit is imported, previous simp lemmas simplify further than they did when they were proven.

What's the point of action here? Removing @[simp] from either lemma seems not ideal, but the simpNF-linter is also kinda right when looking at the entire mathlib...

[Eric Wieser]

I think the argument goes that rfl lemmas are always worth keeping, so just no-lint the rfl lemma

[Jon Eugster]

I have to check tomorrow, but there were a lot of files and lemmas affected. I hope I don't have to nolint all of them.

[Yaël Dillies]

Yeah, simpNF really should be taught about the difference between simp and dsimp lemmas.

[Jon Eugster]

Hmm, would that just amount to a check in
https://github.com/leanprover/std4/blob/6006307d2ceb8743fea7e00ba0036af8654d0347/Std/Tactic/Lint/Simp.lean#L113-L129
that lhs and rhs are defEq or something?

[Yaël Dillies]

That would work, although you can hopefully just fetch the data of whether it's a dsimp lemma or not.

[Eric Wieser]

That's not enough; lemmas which can be proved by rfl don't count as dsimp lemmas unless they're actually proved by rfl

[Jon Eugster]

I see. And the simpNF linter should never check/report any dsimp lemma? or what would be the right condition?

[Yaël Dillies]

It shouldn't report that a simp lemma simplifies the LHS of a dsimp lemma. It's fine if it checks that a dsimp lemma doesn't simplify the LHS of a dsimp lemma (which rarely ever occurs, to be quite fair. The only example I can think of is the pairs coe_bundled_function : ⇑f = g and bundled_function_apply : ⇑f a = g a).