feat: add grind +locals to include local definitions (#11946)

This PR adds a `+locals` configuration option to the `grind` tactic that
automatically adds all definitions from the current file as e-match
theorems. This provides a convenient alternative to manually adding
`[local grind]` attributes to each definition. In the form `grind?
+locals`, it is also helpful for discovering which local declarations it
may be useful to add `[local grind]` attributes to.

Example usage:
```lean
def foo (n : Nat) : Nat := n + 1

-- Without +locals, grind doesn't know about foo
example (n : Nat) : foo n = n + 1 := by grind  -- fails

-- With +locals, grind can use the equation
example (n : Nat) : foo n = n + 1 := by grind +locals  -- succeeds
```

Instance definitions and internal details are filtered out.

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

Co-authored-by: Claude <noreply@anthropic.com>

src/Init/Grind/Config.lean

@@ -21,6 +21,8 @@ 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 `locals` is `true`, `grind` will add all definitions from the current file. -/
+  locals : 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

@@ -182,6 +182,7 @@ open LibrarySuggestions in
 def elabGrindSuggestions
     (params : Grind.Params) (suggestions : Array Suggestion := #[]) : MetaM Grind.Params := do
   let mut params := params
+  let mut added : Array Name := #[]
   for p in suggestions do
     let attr ← match p.flag with
     | some flag => parseModifier flag
@@ -190,6 +191,7 @@ def elabGrindSuggestions
     | .ematch kind =>
       try
         params ← addEMatchTheorem params (mkIdent p.name) p.name kind false (warn := false)
+        added := added.push p.name
       catch _ => pure () -- Don't worry if library suggestions gave bad theorems.
     | _ =>
       -- We could actually support arbitrary grind modifiers,
@@ -197,26 +199,40 @@ def elabGrindSuggestions
       -- but this would require a larger refactor.
       -- Let's only do this if there is a prospect of a library suggestion engine supporting this.
       throwError "unexpected modifier {p.flag}"
+  unless added.isEmpty do
+    trace[grind.debug.suggestions] "{added}"
   return params
 
-open LibrarySuggestions in
-def elabGrindParamsAndSuggestions
-    (params : Grind.Params)
-    (ps : TSyntaxArray ``Parser.Tactic.grindParam)
-    (suggestions : Array Suggestion := #[])
-    (only : Bool) (lax : Bool := false) : TermElabM Grind.Params := do
-  let params ← elabGrindParams params ps (lax := lax) (only := only)
-  elabGrindSuggestions params suggestions
+/-- Add all definitions from the current file. -/
+def elabGrindLocals (params : Grind.Params) : MetaM Grind.Params := do
+  let env ← getEnv
+  let mut params := params
+  let mut added : Array Name := #[]
+  for (name, ci) in env.constants.map₂.toList do
+    -- Filter similar to LibrarySuggestions.isDeniedPremise (but inlined to avoid dependency)
+    -- Skip internal details, but allow private names (which are accessible from current module)
+    if name.isInternalDetail && !isPrivateName name then continue
+    if (← Meta.isInstance name) then continue
+    match ci with
+    | .defnInfo _ =>
+      try
+        params ← addEMatchTheorem params (mkIdent name) name (.default false) false (warn := false)
+        added := added.push name
+      catch _ => pure ()
+    | _ => continue
+  unless added.isEmpty do
+    trace[grind.debug.locals] "{added}"
+  return params
 
 def mkGrindParams
     (config : Grind.Config) (only : Bool) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (mvarId : MVarId) :
     TermElabM Grind.Params := do
   let params ← if only then Grind.mkOnlyParams config else Grind.mkDefaultParams config
-  let suggestions ← if config.suggestions then
-    LibrarySuggestions.select mvarId { caller := some "grind" }
-  else
-    pure #[]
-  let mut params ← elabGrindParamsAndSuggestions params ps suggestions (only := only) (lax := config.lax)
+  let mut params ← elabGrindParams params ps (lax := config.lax) (only := only)
+  if config.suggestions then
+    params ← elabGrindSuggestions params (← LibrarySuggestions.select mvarId { caller := some "grind" })
+  if config.locals then
+    params ← elabGrindLocals params
   trace[grind.debug.inj] "{params.extensions[0]!.inj.getOrigins.map (·.pp)}"
   if params.anchorRefs?.isSome then
     /-
@@ -289,17 +305,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 -/
-def filterSuggestionsFromGrindConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) :
+/-- Filter out `+suggestions` and `+locals` from the config syntax -/
+def filterSuggestionsAndLocalsFromGrindConfig (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 +locals
     -- 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 == `locals))
         | none => true
       | none => true
     | none => true
@@ -345,7 +363,7 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
       let finish ← Grind.Action.mkFinish
       let goal :: _ ← Grind.getGoals
         | -- Goal was closed during initialization
-          let configStx' := filterSuggestionsFromGrindConfig configStx
+          let configStx' := filterSuggestionsAndLocalsFromGrindConfig configStx
           if termParamStxs.isEmpty then
             let tac ← `(tactic| grind $configStx':optConfig only)
             return #[tac]
@@ -357,7 +375,7 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
         -- let saved ← saveState
         match (← finish.run goal) with
         | .closed seq =>
-          let configStx' := filterSuggestionsFromGrindConfig configStx
+          let configStx' := filterSuggestionsAndLocalsFromGrindConfig configStx
           let tacs ← Grind.mkGrindOnlyTactics configStx' seq termParamStxs
           let seq := Grind.Action.mkGrindSeq seq
           let tac ← `(tactic| grind $configStx':optConfig => $seq:grindSeq)

src/Lean/Meta/Tactic/Grind.lean

@@ -101,5 +101,7 @@ builtin_initialize registerTraceClass `grind.debug.proveEq
 builtin_initialize registerTraceClass `grind.debug.pushNewFact
 builtin_initialize registerTraceClass `grind.debug.appMap
 builtin_initialize registerTraceClass `grind.debug.ext
+builtin_initialize registerTraceClass `grind.debug.suggestions
+builtin_initialize registerTraceClass `grind.debug.locals
 
 end Lean

tests/lean/run/grind_ite.lean

@@ -145,14 +145,15 @@ def normalize (assign : Std.HashMap Nat Bool) : IfExpr → IfExpr
     | some b => normalize assign (ite (lit b) t e)
   termination_by e => e.normSize
 
--- We tell `grind` to unfold our definitions above.
-attribute [local grind] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars eval List.disjoint
+-- We could tell `grind` to unfold our definitions above.
+-- attribute [local grind] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars eval List.disjoint
+-- Instead we just rely on `grind +locals`, which tells `grind` it is allowed to unfold definitions in the current file.
 
 theorem normalize_spec (assign : Std.HashMap Nat Bool) (e : IfExpr) :
     (normalize assign e).normalized
     ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → ¬ v ∈ assign := by
-  fun_induction normalize with grind
+  fun_induction normalize with grind +locals
 
 -- We can also prove other variations, where we spell "`v` is not in `assign`"
 -- different ways, and `grind` doesn't mind.
@@ -161,13 +162,13 @@ example (assign : Std.HashMap Nat Bool) (e : IfExpr) :
     (normalize assign e).normalized
     ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign.contains v = false := by
-  fun_induction normalize with grind
+  fun_induction normalize with grind +locals
 
 example (assign : Std.HashMap Nat Bool) (e : IfExpr) :
     (normalize assign e).normalized
     ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign[v]? = none := by
-  fun_induction normalize with grind
+  fun_induction normalize with grind +locals
 
 /--
 We recall the statement of the if-normalization problem.
@@ -203,18 +204,18 @@ theorem normalize'_spec (assign : Std.TreeMap Nat Bool) (e : IfExpr) :
     (normalize' assign e).normalized
     ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → ¬ v ∈ assign := by
-  fun_induction normalize' with grind
+  fun_induction normalize' with grind +locals
 
 example (assign : Std.TreeMap Nat Bool) (e : IfExpr) :
     (normalize' assign e).normalized
     ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → assign.contains v = false := by
-  fun_induction normalize' with grind
+  fun_induction normalize' with grind +locals
 
 example (assign : Std.TreeMap Nat Bool) (e : IfExpr) :
     (normalize' assign e).normalized
     ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → assign[v]? = none := by
-  fun_induction normalize' with grind
+  fun_induction normalize' with grind +locals
 
 end IfExpr

tests/lean/run/grind_locals.lean

@@ -0,0 +1,51 @@
+/-!
+# Test for `grind +locals` flag
+
+This tests that `grind +locals` adds local definitions from the current file.
+-/
+
+-- A simple definition that provides an equation grind can use
+def foo (n : Nat) : Nat := n + 1
+
+-- Without +locals, grind shouldn't know about foo
+-- (This test verifies +locals is actually doing something)
+/--
+error: `grind` failed
+case grind
+n : Nat
+h : ¬foo n = n + 1
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] ¬foo n = n + 1
+  [eqc] False propositions
+    [prop] foo n = n + 1
+  [cutsat] Assignment satisfying linear constraints
+    [assign] n := 0
+    [assign] foo n := 2
+-/
+#guard_msgs in
+example (n : Nat) : foo n = n + 1 := by grind
+
+-- Test that grind +locals can use the equation `foo n = n + 1`
+example (n : Nat) : foo n = n + 1 := by grind +locals
+
+-- An irrelevant definition that should NOT appear in grind? suggestions
+def bar (n : Nat) : Nat := n * 2
+
+-- Test that grind? +locals suggests only the relevant definition (foo), not bar
+/--
+info: Try these:
+  [apply] grind only [foo]
+  [apply] grind => instantiate only [foo]
+-/
+#guard_msgs in
+example (n : Nat) : foo n = n + 1 := by grind? +locals
+
+-- Test with a definition that has multiple equations via pattern matching
+def isZero : Nat → Bool
+  | 0 => true
+  | _ + 1 => false
+
+example : isZero 0 = true := by grind +locals
+example (n : Nat) : isZero (n + 1) = false := by grind +locals

tests/lean/run/grind_locals_module.lean

@@ -0,0 +1,56 @@
+
+module
+/-!
+# Test for `grind +locals` flag (using the module system)
+
+This tests that `grind +locals` adds local definitions from the current file.
+
+We have a separate test here as the current semantics for `isImplementationDetail` are poorly specified,
+and we've had to work around it in deciding which declarations should be included via `+locals`.
+-/
+
+-- A simple definition that provides an equation grind can use
+def foo (n : Nat) : Nat := n + 1
+
+-- Without +locals, grind shouldn't know about foo
+-- (This test verifies +locals is actually doing something)
+/--
+error: `grind` failed
+case grind
+n : Nat
+h : ¬foo n = n + 1
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] ¬foo n = n + 1
+  [eqc] False propositions
+    [prop] foo n = n + 1
+  [cutsat] Assignment satisfying linear constraints
+    [assign] n := 0
+    [assign] foo n := 2
+-/
+#guard_msgs in
+example (n : Nat) : foo n = n + 1 := by grind
+
+-- Test that grind +locals can use the equation `foo n = n + 1`
+example (n : Nat) : foo n = n + 1 := by grind +locals
+
+-- An irrelevant definition that should NOT appear in grind? suggestions
+def bar (n : Nat) : Nat := n * 2
+
+-- Test that grind? +locals suggests only the relevant definition (foo), not bar
+/--
+info: Try these:
+  [apply] grind only [foo]
+  [apply] grind => instantiate only [foo]
+-/
+#guard_msgs in
+example (n : Nat) : foo n = n + 1 := by grind? +locals
+
+-- Test with a definition that has multiple equations via pattern matching
+def isZero : Nat → Bool
+  | 0 => true
+  | _ + 1 => false
+
+example : isZero 0 = true := by grind +locals
+example (n : Nat) : isZero (n + 1) = false := by grind +locals