feat: add grind +simp mode

This PR adds `grind +simp`, which includes all `@[simp]` lemmas as E-matching theorems.

Patterns are generated dynamically at tactic execution time. If performance becomes an issue with large simp databases, the solution is to hook into the `@[simp]` attribute handler to pre-compute and cache patterns at registration time.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <[email protected]>

Author: kim-em

src/Init/Grind/Config.lean

@@ -21,6 +21,13 @@ structure Config where
   /-- If `suggestions` is `true`, `grind` will invoke the currently configured library suggestion engine on the current goal,
   and add attempt to use the resulting suggestions as additional parameters to the `grind` tactic. -/
   suggestions : Bool := false
+  /--
+  If `simp` is `true`, `grind` will use all `@[simp]` lemmas as E-matching theorems.
+  This generates grind patterns dynamically at tactic execution time, which may be slow
+  with large simp databases. If performance becomes an issue, the proper solution is to
+  hook into the `@[simp]` attribute handler to generate and cache patterns at registration time.
+  -/
+  simp : Bool := false
   /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
   splits : Nat := 9
   /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/

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

@@ -13,6 +13,7 @@ public import Lean.LibrarySuggestions.Basic
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.EMatchTheoremParam
+import Lean.Meta.Tactic.Simp.Attr
 import Lean.Elab.Tactic.Grind.Basic
 import Lean.Elab.Tactic.Grind.Param
 import Lean.Meta.Tactic.Grind.Action
@@ -198,6 +199,47 @@ def elabGrindSuggestions
       throwError "unexpected modifier {p.flag}"
   return params
 
+/--
+Check if the conclusion of a type (after stripping foralls) is an equality-like proposition
+(Eq, Iff, or HEq). Returns true if so.
+-/
+private def isEqLike (type : Expr) : Bool :=
+  let conclusion := type.getForallBody
+  conclusion.isAppOf ``Eq || conclusion.isAppOf ``Iff || conclusion.isAppOf ``HEq
+
+/--
+Add simp theorems as E-matching theorems for grind.
+
+**Performance note**: This function iterates over all simp lemmas and generates
+grind patterns dynamically at tactic execution time. This is potentially slow
+with large simp databases. If this becomes a bottleneck, the proper solution is
+to hook into the `@[simp]` attribute handler (in `Lean.Meta.Tactic.Simp.Attr`)
+to generate and cache grind patterns at attribute registration time, similar to
+how `@[grind]` works.
+-/
+def elabGrindSimpTheorems (params : Grind.Params) : MetaM Grind.Params := do
+  let simpTheorems ← getSimpTheorems
+  let symPrios ← Grind.getGlobalSymbolPriorities
+  let mut params := params
+  -- Iterate over all simp lemma origins (includes both fwd and inv directions)
+  for origin in simpTheorems.lemmaNames.toList do
+    match origin with
+    | .decl declName _ inv =>
+      try
+        let info ← getConstInfo declName
+        -- Use eqLhs/eqRhs for equality-like theorems (faster pattern extraction),
+        -- fall back to .default for other propositions like `P 37`
+        let kind : Grind.EMatchTheoremKind :=
+          if isEqLike info.type then
+            if inv then .eqRhs false else .eqLhs false
+          else
+            .default false
+        let thm ← Grind.mkEMatchTheoremForDecl declName kind symPrios
+        params := { params with ematch := params.ematch.insert thm }
+      catch _ => pure () -- Silently skip theorems that fail
+    | _ => pure () -- Skip non-declaration origins (fvars, etc.)
+  return params
+
 open LibrarySuggestions in
 def elabGrindParamsAndSuggestions
     (params : Grind.Params)
@@ -225,6 +267,8 @@ def mkGrindParams
   else
     pure #[]
   let mut params ← elabGrindParamsAndSuggestions params ps suggestions (only := only) (lax := config.lax)
+  if config.simp then
+    params ← elabGrindSimpTheorems params
   trace[grind.debug.inj] "{params.inj.getOrigins.map (·.pp)}"
   if params.anchorRefs?.isSome then
     /-
@@ -297,17 +341,19 @@ def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `ta
 def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
   stx.raw[grindParamsPos][1].getSepArgs
 
-/-- Filter out `+suggestions` from the config syntax -/
+/-- Filter out `+suggestions` and `+simp` from the config syntax for `grind?` suggestions. -/
 def filterSuggestionsFromGrindConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) :
     TSyntax ``Lean.Parser.Tactic.optConfig :=
   let configItems := config.raw.getArgs
   let filteredItems := configItems.filter fun item =>
-    -- Keep all items except +suggestions
+    -- Keep all items except +suggestions and +simp
     -- Structure: null node -> configItem -> posConfigItem -> ["+", ident]
     match item[0]? with
     | some configItem => match configItem[0]? with
       | some posConfigItem => match posConfigItem[1]? with
-        | some ident => !(posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && ident.getId == `suggestions)
+        | some ident =>
+          let id := ident.getId
+          !(posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && (id == `suggestions || id == `simp))
         | none => true
       | none => true
     | none => true

tests/lean/run/grind_simp.lean

@@ -0,0 +1,55 @@
+/-!
+# Tests for `grind +simp`
+
+This file tests the `grind +simp` feature, which allows grind to use all `@[simp]` lemmas
+as E-matching theorems.
+-/
+
+-- Test basic simp lemma usage
+def foo (n : Nat) : Nat := n + 1
+def bar (n : Nat) : Nat := 1 + n
+
+@[simp] theorem foo_eq_bar : foo n = bar n := by simp [foo, bar, Nat.add_comm]
+
+-- Verify plain grind fails but grind +simp succeeds
+example : foo 5 = bar 5 := by
+  fail_if_success grind
+  grind +simp
+
+-- Verify grind? +simp suggests the simp lemma
+/--
+info: Try these:
+  [apply] grind only [= foo_eq_bar]
+  [apply] grind => instantiate only [= foo_eq_bar]
+-/
+#guard_msgs in
+example : foo 5 = bar 5 := by grind? +simp
+
+-- Test that +simp can be combined with hypotheses
+def qux (n : Nat) : Nat := n
+
+@[simp] theorem qux_id : qux n = n := rfl
+
+example (h : a = b) : qux a = b := by
+  fail_if_success grind
+  grind +simp
+
+opaque P : Nat → Prop
+@[simp] axiom p : P 37
+
+example : P 37 := by
+  fail_if_success grind
+  grind +simp
+
+-- Test that grind +simp works with standard library simp lemmas
+-- String.length_append is currently @[simp] but not @[grind]
+-- (It's fine to delete this without replacement once we add `grind` annotations to String lemmas.)
+/--
+info: Try these:
+  [apply] grind only [= String.length_append]
+  [apply] grind => instantiate only [= String.length_append]
+-/
+#guard_msgs in
+example (s t : String) : (s ++ t).length = s.length + t.length := by
+  fail_if_success grind
+  grind? +simp