grind incorrectly redundant parameter

Stream: lean4

[Alex Meiburg]

This is the (ugly) MWE that I have, no imports required besides core:

theorem naughty_grind {α : Type u} (head x y a head_1 : α) (tail : List α)
  (hn :
    0 + 1 <
      ((List.zipWith Prod.mk ((head_1 :: tail ++ [a]).reverse ++ [y, x, head])
              (((head_1 :: tail ++ [a]).reverse ++ [y, x, head]).tail ++
                List.take 1 ((head_1 :: tail ++ [a]).reverse ++ [y, x, head]))).rotateLeft
          ((head_1 :: tail ++ [a]).length + 2)).length)
  (hn' : 0 + 1 < (head_1 :: tail ++ [a]).length + 3)
  (left : (tail.reverse ++ [head_1, y, x, head])[0] = (head_1 :: (tail ++ [head]))[tail.length])
  (right : (tail.reverse ++ [head_1, y, x, head])[1] = (y :: head_1 :: tail)[tail.length]) :
    (tail.reverse ++ [head_1, y, x, head, a])[0] = (head_1 :: (tail ++ [a]))[tail.length] := by
  grind [→ Array.eq_empty_of_size_eq_zero, List.getElem_append, → List.eq_nil_of_append_eq_nil, → List.eq_nil_of_length_eq_zero, cases Or]

Grind says

this parameter is redundant, environment already contains `List.getElem_append` annotated with `@[grind =]`

so that my "bare" List.getElem_append in the list gets a warning. But if I remove that, the proof fails.

[Alex Meiburg]

In particular I ran into this when porting code forward a few versions, and a grind command that was working before broke. Running grind? in the old repo gave a bare List.getElem_append, so I assume that was earlier annotated as @[grind] and now it's @[grind =].

[Alex Meiburg]

Ah, actually I think I see the "issue": it's being used here as ← List.getElem_append. But if I change the grind command to that, it still complains.

So it sees

grind [→ Array.eq_empty_of_size_eq_zero, ← List.getElem_append, → List.eq_nil_of_append_eq_nil, → List.eq_nil_of_length_eq_zero, cases Or]

and complains that I should drop List.getElem_append since it's already marked =, but if I do that the proof breaks.

[Alex Meiburg]

Maybe overlapping with #general > confusing grind redundant parameter warning @ 💬

[Kim Morrison]

Sorry to have not responded here. On v4.26.0-rc1, or current nightlies, simply removing the flagged theorems seems to work. Let me know if there's something else you'd like me to look at here!