simpNF linter not triggered

Stream: mathlib4

[Jireh Loreaux]

In #31563 a simp lemma was removed. The reason is that it could already by proven by simp! And I checked, that is correct. Why didn't the simpNF linter trigger here?

[Kevin Buzzard]

Stab in the dark: can it still be proved by simp after import Mathlib? Not even sure if this is relevant.

[Jireh Loreaux]

yes

[Yaël Dillies]

I checked that this isn't what's happening here, but here's my reminder that the correct criterion is not whether the statement of the simp lemma can be simplified, but rather if its LHS can

[Jireh Loreaux]

I think the way you worded that is confusing me. You agree that in this particular situation, the LHS can be simplified, right?

[Jovan Gerbscheid]

We have the lemmas coe_innerSL_apply and innerSL_apply_apply, and innerSL_apply_apply can be proved by simp using coe_innerSL_apply.

But when simpNF called simp, it used innerSL_apply_apply instead of coe_innerSL_apply. So the simpNF linter didn't notice that coe_innerSL_apply could be used instead.

[Jovan Gerbscheid]

A solution could be to run simp with that particular simp lemma disabled. But this would lead to false positives, due to

library_note2 «specialised high priority simp lemma» /--
It sometimes happens that a `@[simp]` lemma declared early in the library can be proved by `simp`
using later, more general simp lemmas. In that case, the following reasons might be arguments for
the early lemma to be tagged `@[simp high]` (rather than `@[simp, nolint simpNF]` or
un``@[simp]``ed):
1. There is a significant portion of the library which needs the early lemma to be available via
  `simp` and which doesn't have access to the more general lemmas.
2. The more general lemmas have more complicated typeclass assumptions, causing rewrites with them
  to be slower.
-/

[Jireh Loreaux]

When simp does it's discrimination tree matching, does it pick the longest matching subexpression when there are two possible matches? This could explain why it is always choosing innerSL_apply_apply over coe_innerSL_apply when the former is applicable.

[Jovan Gerbscheid]

Yes, the matches of different length correspond to different discrimination tree searches, which are done in order from long to short.

[Jireh Loreaux]

okay, thanks for this. I think I am satisfied. The point is that simpNF won't trigger when we're making a simp lemma whose left-hand side contains an existing simp lemma as an initial segment of the expression.