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

@@ -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. -/

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`.