confusing grind redundant parameter warning

Stream: general

[Chris Henson]

I find this warning behavior a little confusing, does anyone have an explanation?

import Mathlib

variable {α β : Type*} [DecidableEq α]

attribute [grind =] List.dlookup_isSome

-- fails
theorem foo (l : List (Σ _ : α, β)) (mem : b ∈ l.dlookup a) : a ∈ l.keys := by
  have := Option.isSome_of_mem mem
  grind

-- succeeds, but with a redundant parameter warning
theorem foo' (l : List (Σ _ : α, β)) (mem : b ∈ l.dlookup a) : a ∈ l.keys := by
  have := Option.isSome_of_mem mem
  grind [= List.dlookup_isSome]

-- succeeds
theorem foo'' (l : List (Σ _ : α, β)) (mem : b ∈ l.dlookup a) : a ∈ l.keys := by
  have := Option.isSome_of_mem mem
  grind [List.dlookup_isSome]

[Bhavik Mehta]

In the third case, the grind pattern used for the lemma is different to that given by grind =, which is the one used in the second (and the one you told it to use by default).

[Chris Henson]

Right, my confusion is that if you remove the pattern, it then fails (the first case).

[Bhavik Mehta]

Oops, I mis-numbered things, have edited. The pattern given by = is needed, and the (less restricted) pattern used in grind [List.dlookup_isSome] is (therefore) also enough, but it is different, so no warning is given.

[Chris Henson]

Yeah, the third makes sense, it highlights that the check is for the exact pattern. Together it suggests the linter doesn't check if removing the redundant patterns gives another valid proof, just what patterns are registered?

[Bhavik Mehta]

Yes, it checks which patterns it used, and warns if a pattern was explicitly included in a call that wasn't used. It doesn't check if there's still a proof if the pattern is removed.

[Chris Henson]

What I'm not understanding is why it fails without specifying the = pattern. Isn't that exactly what the attribute I placed above is supposed to be adding? The reason it is redundant is because it recognizes they are the same.

[Bhavik Mehta]

Ah! I misunderstood what you were confused about. This time I share your confusion!

[Alex Meiburg]

I had a similar but different issue: #lean4 > grind incorrectly redundant parameter

[Chris Henson]

Maybe worth opening an issue since multiple people have run into this? I can try making my example Mathlib independent too if that's helpful.