New problems with the simpNF linter

Stream: batteries

[Kim Morrison]

After lean#4481, we are getting new false positives (about 10 cases across Mathlib) with the simpNF linter.

Here is a #mwe:

import Batteries

universe u v

class One (α : Type u) where
  one : α

instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1
instance (priority := 200) One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
  one := 1

variable {I : Type u} {i : I}
variable {f : I → Type v}

instance instOne [∀ i, One <| f i] : One (∀ i : I, f i) :=
  ⟨fun _ => 1⟩

@[simp]
theorem one_apply [∀ i, One <| f i] : (1 : ∀ i, f i) i = 1 :=
  rfl

example [∀ i, One <| f i] : (1 : ∀ i, f i) i = 1 := by simp only [one_apply]

#lint

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
#check @one_apply /- Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.
 -/

[Kim Morrison]

I have added nolint simpNF and an adaptation note linking to lean#4481, but hopefully I can pass the remainder of this problem off to someone else. :-)

[Damiano Testa]

Is there a similar example that fails on Mathlib?

[Kim Morrison]

That's usually the opposite of the question people ask. :-)

[Kim Morrison]

Yes, it occurred in the wild many times at https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/.2313981.20adaptations.20for.20nightly-2024-06-19

[Damiano Testa]

The reason for the question is that

• I have a working version of Mathlib;
• on Mathlib, I have the "local" simpNF linter with which I have been playing.

[Damiano Testa]

Anyway, thanks for the examples! I'll see if I spot anything suspicious in the simpNF linter.