From d98f40cda2392d2f8ad58635067ed59c2dfeba89 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 10 May 2026 20:23:00 -0700
Subject: [PATCH] feat: add `genLocal` configuration option for `grind`
 (#13699)

This PR adds a new `grind` configuration option, `genLocal`, that
controls the
maximum term generation for local theorems (e.g., hypotheses). It
defaults to
`8`, same value as `gen` and applies whenever
`grind` instantiates a theorem whose origin is local rather than a
declaration
or user-provided term. Since users have little control over the patterns
used
for local theorems, a tighter generation bound is a reasonable default.

Internally, E-matching now selects the generation bound via a new
`getMaxGeneration` helper that dispatches on the theorem's `Origin`:
`.stx` and
`.decl` use `gen`, everything else uses `genLocal`.
---
 src/Init/Grind/Config.lean             | 5 +++++
 src/Lean/Meta/Tactic/Grind/EMatch.lean | 8 ++++++++
 2 files changed, 13 insertions(+)

diff --git a/src/Init/Grind/Config.lean b/src/Init/Grind/Config.lean
index 12e8ec2006..2df1e30dac 100644
--- a/src/Init/Grind/Config.lean
+++ b/src/Init/Grind/Config.lean
@@ -35,6 +35,11 @@ structure Config where
   The input goal terms have generation 0. When we instantiate a theorem using a term from generation `n`,
   the new terms have generation `n+1`. Thus, this parameter limits the length of an instantiation chain. -/
   gen : Nat := 8
+  /--
+  Maximum term generation for local theorems (e.g., hypotheses).
+  See `gen`.
+  -/
+  genLocal : Nat := 8
   /-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
   instances : Nat := 1000
   /-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index 917a2bfb32..ee75170c3c 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -272,6 +272,14 @@ private def assignGenInfo? (genInfo? : Option GenPatternInfo) (c : Choice) (x :
   let c ← saveSource c x
   genInfo.assign? c x
 
+/--
+Return the maximum generation allowed for the current theorem.
+-/
+private def getMaxGeneration : M Nat := do
+  match (← read).thm.origin with
+  | .stx .. | .decl _ => return (← getConfig).gen
+  | _ => return (← getConfig).genLocal
+
 /--
 Matches pattern `p` with term `e` with respect to choice `c`.
 We traverse the equivalence class of `e` looking for applications compatible with `p`.