feat: make grind +premises more robust to bad suggestions

Author: kim-em

src/Lean/Elab/Tactic/Grind/Main.lean

@@ -120,7 +120,9 @@ def elabGrindParams
     | none => pure <| .ematch (.default false)
     match attr with
     | .ematch kind =>
-      params ← addEMatchTheorem params (mkIdent p.name) p.name kind false
+      try
+        params ← addEMatchTheorem params (mkIdent p.name) p.name kind false (warn := false)
+      catch _ => pure () -- Don't worry if premise suggestion gave bad suggetions.
     | _ =>
       -- We could actually support arbitrary grind modifiers,
       -- and call `processParam` rather than `addEMatchTheorem`,

tests/lean/run/grind_premises.lean

@@ -38,3 +38,19 @@ set_premise_selector (fun _ _ => pure #[{ name := `p, score := 1.0 }])
 
 example : P 7 := by
   grind +premises
+
+set_premise_selector (fun _ _ => pure #[{ name := `List.append_assoc, score := 1.0 }])
+
+-- Make sure there is no warning about the redundant theorem.
+#guard_msgs in
+example (x y z : List Nat) : x ++ (y ++ z) = (x ++ y) ++ z := by
+  grind +premises
+
+theorem f : True := trivial
+
+set_premise_selector (fun _ _ => pure #[{ name := `f, score := 1.0 }])
+
+-- Make sure that bad suggestions (e.g. not patterns) from premise selection are dropped silently.
+#guard_msgs in
+example (x y z : List Nat) : x ++ (y ++ z) = (x ++ y) ++ z := by
+  grind +premises