`simpNF` linter rejecting working simp lemma

[kbuzzard]

import Std.Tactic.Lint

def Set (α : Type u) := α → Prop

def unionᵢ (s : ι → Set β) : Set β := sorry
--  supᵢ s

def interᵢ (s : ι → Set β) : Set β := sorry

@[simp]
theorem unionᵢ_interᵢ_ge_nat_add (f : Nat → Set α) (k : Nat) :
    unionᵢ (λ n => interᵢ (λ i => interᵢ (λ (_h : i ≥ n) => f (i + k)))) =
    unionᵢ (λ n => interᵢ (λ i => interᵢ (λ (_h : i ≥ n) => f i))) := sorry

example (f : Nat → Set α) (k : Nat) :
    unionᵢ (λ n => interᵢ (λ i => interᵢ (λ (_h : i ≥ n) => f (i + k)))) =
    unionᵢ (λ n => interᵢ (λ i => interᵢ (λ (_h : i ≥ n) => f i))) := by simp -- works

#lint only simpNF
/- 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 @unionᵢ_interᵢ_ge_nat_add /- Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.
 -/

Is the linter misfiring? The simp lemma does seem to apply. Discussions here (about the corresponding lattice lemma) and here (about the lemma above). Note in particular Gabriel's comment. The lemma is usually written (⋃ n, ⋂ i ≥ n, f (i + k)) = ⋃ n, ⋂ i ≥ n, f i but I didn't want to use notation3 in the MWE. Note also that Gabriel suggests this shouldn't be a simp lemma anyway but I thought I'd record the issue anyway.

[kbuzzard]

Here's another example, coming from the port of Mathlib.Data.List.Basic:

import Std.Data.List.Lemmas
import Std.Tactic.Lint

namespace List

def pmap {p : α → Prop} (f : ∀ a, p a → β) : ∀ l : List α, (∀ a, a ∈ l → p a) → List β
  | [], _ => []
  | a :: l, H => f a (forall_mem_cons.1 H).1 :: pmap f l (forall_mem_cons.1 H).2

def attach (l : List α) : List { x // x ∈ l } :=
  pmap Subtype.mk l fun _ => id

@[simp]
theorem attach_map_coe' (l : List α) (f : α → β) :
    (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := sorry

--#lint only simpNF
/- 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 @attach_map_coe' /- Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.
 -/

example (l : List α) (f : α → β) :
    (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by simp? -- works
-- Try this: simp only [attach_map_coe']

[gebner]

The simpNF linter is ultimately correct that these shouldn't be simp lemmas (even though I didn't expect it to catch them). All of them require complicated higher-order matching, which Lean doesn't do (neither four nor three).

The only kind of higher-order matching supported by Lean are so called higher-order patterns. A higher-order pattern is one like ?P x where all arguments are variables. The simp lemmas here however match on ?P (x + 1) or ?P ↑x, which is unsupported.

• ∀ P : Nat → Prop, (∃ x, P x) ↔ False is a great simp lemma
• ∀ P : Nat → Prop, (∃ x, P (x+1)) ↔ False is a bad simp lemma and won't fire reliably. For example it won't fire on ∃ x, x+1 = y.

[eric-wieser]

Isn't a simp lemma that doesn't fire reliably still sometimes better than no simp lemma at all?