feat: warn grind redundant parameters

This PR produces a warning for redundant `grind` arguments.

src/Lean/Elab/Tactic/Grind.lean

@@ -125,6 +125,8 @@ where
     let info ← getAsyncConstInfo declName
     match info.kind with
     | .thm | .axiom | .ctor =>
+      if params.ematch.containsWithSameKind (.decl declName) kind then
+        logWarning m!"this parameter is redundant, environment already contains `@{kind.toAttribute} {declName}`"
       match kind with
       | .eqBoth gen =>
         let params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios) }

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -342,7 +342,7 @@ def EMatchTheoremKind.isDefault : EMatchTheoremKind → Bool
   | .default _ => true
   | _ => false
 
-private def EMatchTheoremKind.toAttribute : EMatchTheoremKind → String
+def EMatchTheoremKind.toAttribute : EMatchTheoremKind → String
   | .eqLhs true     => "[grind = gen]"
   | .eqLhs false    => "[grind =]"
   | .eqRhs true     => "[grind =_ gen]"
@@ -433,14 +433,26 @@ def EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchThe
 def EMatchTheorems.contains (s : EMatchTheorems) (origin : Origin) : Bool :=
   s.origins.contains origin
 
-/-- Mark the theorem with the given origin as `erased` -/
+/-- Marks the theorem with the given origin as `erased` -/
 def EMatchTheorems.erase (s : EMatchTheorems) (origin : Origin) : EMatchTheorems :=
   { s with erased := s.erased.insert origin, origins := s.origins.erase origin }
 
-/-- Returns true if the theorem has been marked as erased. -/
+/-- Returns `true` if the theorem has been marked as erased. -/
 def EMatchTheorems.isErased (s : EMatchTheorems) (origin : Origin) : Bool :=
   s.erased.contains origin
 
+/-- Returns `true` if there is a theorem with exactly the same kind is already in `s` -/
+def EMatchTheorems.containsWithSameKind (s : EMatchTheorems) (origin : Origin) (kind : EMatchTheoremKind) : Bool :=
+  match kind with
+  | .eqBoth gen => go (.eqLhs gen) && go (.eqRhs gen)
+  | _ => go kind
+where
+  go (kind : EMatchTheoremKind) : Bool :=
+    if let some thms := s.omap.find? origin then
+      thms.any fun thm => thm.kind == kind
+    else
+      false
+
 /--
 Retrieves theorems from `s` associated with the given symbol. See `EMatchTheorem.insert`.
 The theorems are removed from `s`.

tests/lean/run/grind_warn_param.lean

@@ -0,0 +1,51 @@
+reset_grind_attrs%
+set_option warn.sorry false
+
+attribute [grind =] Array.size_set
+
+opaque P : Nat → Prop
+opaque Q : Nat → Prop
+opaque f : Nat → Nat → Nat
+
+@[grind→] theorem pqf : Q x → P (f x x) := sorry
+
+opaque h : Nat → Nat
+opaque g : Nat → Nat → Nat
+
+@[grind _=_]
+theorem hg : h x = g x (g x x) := sorry
+
+/--
+warning: this parameter is redundant, environment already contains `@[grind =] Array.size_set`
+-/
+#guard_msgs (warning) in
+example : True := by grind [= Array.size_set]
+
+/-- warning: this parameter is redundant, environment already contains `@[grind →] pqf` -/
+#guard_msgs (warning) in
+example : True := by grind [→ pqf]
+
+/--
+warning: this parameter is redundant, environment already contains `@[grind →] pqf`
+---
+warning: this parameter is redundant, environment already contains `@[grind =] Array.size_set`
+-/
+#guard_msgs (warning) in
+example : True := by grind [→ pqf, = Array.size_set]
+
+/-- warning: this parameter is redundant, environment already contains `@[grind _=_] hg` -/
+#guard_msgs (warning) in
+example : True := by grind [_=_ hg]
+
+/-- warning: this parameter is redundant, environment already contains `@[grind =_] hg` -/
+#guard_msgs (warning) in
+example : True := by grind [=_ hg]
+
+#guard_msgs (warning) in
+example : True := by grind [Array.size_set]
+
+#guard_msgs (warning) in
+example : True := by grind [pqf]
+
+#guard_msgs (warning) in
+example : True := by grind [hg]