feat: warning based on patterns for grind (#9883)

This PR refines the warning message for redundant `grind` arguments. It
is not based on the actual inferred pattern instead provided kind.

src/Lean/Elab/Tactic/Grind.lean

@@ -68,6 +68,17 @@ def elabInitGrindNorm : CommandElab := fun stx =>
         Grind.registerNormTheorems pre post
   | _ => throwUnsupportedSyntax
 
+private def warnRedundantEMatchArg (s : Grind.EMatchTheorems) (declName : Name) : MetaM Unit := do
+  let kinds ← match s.getKindsFor (.decl declName) with
+    | [] => return ()
+    | [k] => pure m!"@{k.toAttribute}"
+    | [.eqLhs gen, .eqRhs _]
+    | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute}"
+    | ks =>
+      let ks := ks.map fun k => m!"@{k.toAttribute}"
+      pure m!"{ks}"
+  logWarning m!"this parameter is redundant, environment already contains `{declName}` annotated with `{kinds}`"
+
 def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) (only : Bool) : MetaM Grind.Params := do
   let mut params := params
   for p in ps do
@@ -125,14 +136,19 @@ 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) }
-        return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios) }
+        let thm₁ ← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios
+        let thm₂ ← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios
+        if params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
+           params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then
+          warnRedundantEMatchArg params.ematch declName
+        return { params with extra := params.extra.push thm₁ |>.push thm₂ }
       | _ =>
-        return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind params.symPrios) }
+        let thm ← Grind.mkEMatchTheoremForDecl declName kind params.symPrios
+        if params.ematch.containsWithSamePatterns thm.origin thm.patterns then
+          warnRedundantEMatchArg params.ematch declName
+        return { params with extra := params.extra.push thm }
     | .defn =>
       if (← isReducible declName) then
         throwError "`{declName}` is a reducible definition, `grind` automatically unfolds them"
@@ -203,7 +219,7 @@ def evalGrindCore
   let only := only.isSome
   let params := if let some params := params then params.getElems else #[]
   if Grind.grind.warning.get (← getOptions) then
-    logWarningAt ref "The `grind` tactic is new and its behaviour may change in the future. This project has used `set_option grind.warning true` to discourage its use."
+    logWarningAt ref "The `grind` tactic is new and its behavior may change in the future. This project has used `set_option grind.warning true` to discourage its use."
   withMainContext do
     let result ← grind (← getMainGoal) config only params fallback
     replaceMainGoal []

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

@@ -441,17 +441,18 @@ def EMatchTheorems.erase (s : EMatchTheorems) (origin : Origin) : EMatchTheorems
 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
+/-- Returns `true` if there is a theorem with exactly the same pattern is already in `s` -/
+def EMatchTheorems.containsWithSamePatterns (s : EMatchTheorems) (origin : Origin) (patterns : List Expr) : Bool :=
+  if let some thms := s.omap.find? origin then
+    thms.any fun thm => thm.patterns == patterns
+  else
+    false
+
+def EMatchTheorems.getKindsFor (s : EMatchTheorems) (origin : Origin) : List EMatchTheoremKind :=
+  if let some thms := s.omap.find? origin then
+    thms.map (·.kind)
+  else
+    []
 
 /--
 Retrieves theorems from `s` associated with the given symbol. See `EMatchTheorem.insert`.

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -948,7 +948,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
     next k_ne_i =>
       have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i
       specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k
-      grind [Fin.getElem_fin]
+      grind
   · by_cases li.2 = true
     next li_eq_true =>
       have i_ne_k2 : ⟨i.1, i_in_bounds⟩ ≠ k2 := by

tests/lean/run/grind_warn_param.lean

@@ -16,36 +16,69 @@ opaque g : Nat → Nat → Nat
 theorem hg : h x = g x (g x x) := sorry
 
 /--
-warning: this parameter is redundant, environment already contains `@[grind =] Array.size_set`
+warning: this parameter is redundant, environment already contains `Array.size_set` annotated with `@[grind =]`
 -/
 #guard_msgs (warning) in
 example : True := by grind [= Array.size_set]
 
-/-- warning: this parameter is redundant, environment already contains `@[grind →] pqf` -/
+/--
+warning: this parameter is redundant, environment already contains `pqf` annotated with `@[grind →]`
+-/
 #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 `pqf` annotated with `@[grind →]`
 ---
-warning: this parameter is redundant, environment already contains `@[grind =] Array.size_set`
+warning: this parameter is redundant, environment already contains `Array.size_set` annotated with `@[grind =]`
 -/
 #guard_msgs (warning) in
 example : True := by grind [→ pqf, = Array.size_set]
 
-/-- warning: this parameter is redundant, environment already contains `@[grind _=_] hg` -/
+/--
+warning: this parameter is redundant, environment already contains `Array.size_set` annotated with `@[grind =]`
+-/
+#guard_msgs (warning) in
+example : True := by grind [Array.size_set]
+
+/--
+warning: this parameter is redundant, environment already contains `hg` annotated with `@[grind _=_]`
+-/
 #guard_msgs (warning) in
 example : True := by grind [_=_ hg]
 
-/-- warning: this parameter is redundant, environment already contains `@[grind =_] hg` -/
+/--
+warning: this parameter is redundant, environment already contains `hg` annotated with `@[grind _=_]`
+-/
 #guard_msgs (warning) in
 example : True := by grind [=_ hg]
 
+/--
+warning: this parameter is redundant, environment already contains `Array.size_set` annotated with `@[grind =]`
+-/
 #guard_msgs (warning) in
 example : True := by grind [Array.size_set]
 
 #guard_msgs (warning) in
 example : True := by grind [pqf]
 
+/--
+warning: this parameter is redundant, environment already contains `hg` annotated with `@[grind _=_]`
+-/
 #guard_msgs (warning) in
 example : True := by grind [hg]
+
+@[grind =] theorem mem_range : m ∈ List.range n ↔ m < n :=
+  sorry
+
+/--
+warning: this parameter is redundant, environment already contains `mem_range` annotated with `@[grind =]`
+-/
+#guard_msgs (warning) in
+example : True := by grind [mem_range]
+
+/--
+warning: this parameter is redundant, environment already contains `mem_range` annotated with `@[grind =]`
+-/
+#guard_msgs (warning) in
+example : True := by grind [= mem_range]