feat: configuration options for the grind tactic (#6490)

This PR adds basic configuration options for the `grind` tactic.

Author: leodemoura

src/Init/Grind/Tactics.lean

@@ -12,11 +12,22 @@ The configuration for `grind`.
 Passed to `grind` using, for example, the `grind (config := { eager := true })` syntax.
 -/
 structure Config where
+  /-- When `eager` is true (default: `false`), `grind` eagerly splits `if-then-else` and `match` expressions during internalization. -/
+  eager : Bool := false
+  /-- Maximum number of branches (i.e., case-splits) in the proof search tree. -/
+  splits : Nat := 100
   /--
-  When `eager` is true (default: `false`), `grind` eagerly splits `if-then-else` and `match`
-  expressions.
+  Maximum number of E-matching (aka heuristic theorem instantiation)
+  in a proof search tree branch.
   -/
-  eager : Bool := false
+  ematch : Nat := 5
+  /--
+  Maximum term generation.
+  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 := 5
+  /-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
+  instances : Nat := 1000
   deriving Inhabited, BEq
 
 end Lean.Grind
@@ -27,7 +38,7 @@ namespace Lean.Parser.Tactic
 `grind` tactic and related tactics.
 -/
 
--- TODO: configuration option, parameters
-syntax (name := grind) "grind" : tactic
+-- TODO: parameters
+syntax (name := grind) "grind" optConfig : tactic
 
 end Lean.Parser.Tactic

src/Lean/Elab/Tactic/Grind.lean

@@ -8,10 +8,13 @@ import Init.Grind.Tactics
 import Lean.Meta.Tactic.Grind
 import Lean.Elab.Command
 import Lean.Elab.Tactic.Basic
+import Lean.Elab.Tactic.Config
 
 namespace Lean.Elab.Tactic
 open Meta
 
+declare_config_elab elabGrindConfig Grind.Config
+
 open Command Term in
 @[builtin_command_elab Lean.Parser.Command.grindPattern]
 def elabGrindPattern : CommandElab := fun stx => do
@@ -29,17 +32,18 @@ def elabGrindPattern : CommandElab := fun stx => do
         Grind.addEMatchTheorem declName xs.size patterns.toList
   | _ => throwUnsupportedSyntax
 
-def grind (mvarId : MVarId) (mainDeclName : Name) : MetaM Unit := do
-  let mvarIds ← Grind.main mvarId mainDeclName
+def grind (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) : MetaM Unit := do
+  let mvarIds ← Grind.main mvarId config mainDeclName
   unless mvarIds.isEmpty do
     throwError "`grind` failed\n{goalsToMessageData mvarIds}"
 
 @[builtin_tactic Lean.Parser.Tactic.grind] def evalApplyRfl : Tactic := fun stx => do
   match stx with
-  | `(tactic| grind) =>
+  | `(tactic| grind $config:optConfig) =>
     logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
     let declName := (← Term.getDeclName?).getD `_grind
-    withMainContext do liftMetaFinishingTactic (grind · declName)
+    let config ← elabGrindConfig config
+    withMainContext do liftMetaFinishingTactic (grind · config declName)
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -181,6 +181,7 @@ where
     if (← isInconsistent) then
       resetNewEqs
       return ()
+    checkSystem "grind"
     let some { lhs, rhs, proof, isHEq } := (← popNextEq?) | return ()
     addEqStep lhs rhs proof isHEq
     processTodo

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -167,6 +167,7 @@ private def addNewInstance (origin : Origin) (proof : Expr) (generation : Nat) :
   let prop ← inferType proof
   trace[grind.ematch.instance] "{← origin.pp}: {prop}"
   modify fun s => { s with newInstances := s.newInstances.push { proof, prop, generation } }
+  modifyThe Goal fun s => { s with numInstances := s.numInstances + 1 }
 
 /--
 After processing a (multi-)pattern, use the choice assignment to instantiate the proof.
@@ -231,6 +232,8 @@ where
 /-- Process choice stack until we don't have more choices to be processed. -/
 private partial def processChoices : M Unit := do
   unless (← get).choiceStack.isEmpty do
+    checkSystem "ematch"
+    if (← checkMaxInstancesExceeded) then return ()
     let c ← modifyGet fun s : State => (s.choiceStack.head!, { s with choiceStack := s.choiceStack.tail! })
     match c.cnstrs with
     | [] => instantiateTheorem c
@@ -246,6 +249,7 @@ private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
   let useMT      := (← read).useMT
   let gmt        := (← getThe Goal).gmt
   for app in apps do
+    if (← checkMaxInstancesExceeded) then return ()
     let n ← getENode app
     if (n.heqProofs || isSameExpr n.cgRoot app) &&
        (!useMT || n.mt == gmt) then
@@ -254,6 +258,7 @@ private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
         processChoices
 
 def ematchTheorem (thm : EMatchTheorem) : M Unit := do
+  if (← checkMaxInstancesExceeded) then return ()
   withReader (fun ctx => { ctx with thm }) do
     let ps := thm.patterns
     match ps, (← read).useMT with
@@ -298,7 +303,6 @@ def ematch : GoalM (Array EMatchTheoremInstance) := do
       thms         := s.thms ++ s.newThms
       newThms      := {}
       gmt          := s.gmt + 1
-      numInstances := s.numInstances + insts.size
     }
     return insts
 

src/Lean/Meta/Tactic/Grind/Preprocessor.lean

@@ -162,16 +162,16 @@ open Preprocessor
 
 def preprocessAndProbe (mvarId : MVarId) (mainDeclName : Name) (p : GoalM Unit) : MetaM Unit :=
   withoutModifyingMCtx do
-    Preprocessor.preprocessAndProbe mvarId p |>.run |>.run mainDeclName
+    Preprocessor.preprocessAndProbe mvarId p |>.run |>.run mainDeclName {}
 
-def preprocess (mvarId : MVarId) (mainDeclName : Name) : MetaM Preprocessor.State :=
-  Preprocessor.preprocess mvarId |>.run |>.run mainDeclName
+def preprocess (mvarId : MVarId) (mainDeclName : Name) (config : Grind.Config) : MetaM Preprocessor.State :=
+  Preprocessor.preprocess mvarId |>.run |>.run mainDeclName config
 
-def main (mvarId : MVarId) (mainDeclName : Name) : MetaM (List MVarId) := do
+def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) : MetaM (List MVarId) := do
   let go : GrindM (List MVarId) := do
     let s ← Preprocessor.preprocess mvarId |>.run
     let goals := s.goals.toList.filter fun goal => !goal.inconsistent
     return goals.map (·.mvarId)
-  go.run mainDeclName
+  go.run mainDeclName config
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Run.lean

@@ -25,7 +25,7 @@ def mkMethods : CoreM Methods := do
        prop e
   }
 
-def GrindM.run (x : GrindM α) (mainDeclName : Name) : MetaM α := do
+def GrindM.run (x : GrindM α) (mainDeclName : Name) (config : Grind.Config) : MetaM α := do
   let scState := ShareCommon.State.mk _
   let (falseExpr, scState) := ShareCommon.State.shareCommon scState (mkConst ``False)
   let (trueExpr, scState)  := ShareCommon.State.shareCommon scState (mkConst ``True)
@@ -35,7 +35,7 @@ def GrindM.run (x : GrindM α) (mainDeclName : Name) : MetaM α := do
     (config := { arith := true })
     (simpTheorems := #[thms])
     (congrTheorems := (← getSimpCongrTheorems))
-  x (← mkMethods).toMethodsRef { mainDeclName, simprocs, simp } |>.run' { scState, trueExpr, falseExpr }
+  x (← mkMethods).toMethodsRef { mainDeclName, config, simprocs, simp } |>.run' { scState, trueExpr, falseExpr }
 
 @[inline] def GoalM.run (goal : Goal) (x : GoalM α) : GrindM (α × Goal) :=
   goal.mvarId.withContext do StateRefT'.run x goal

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Grind.Tactics
 import Lean.Util.ShareCommon
 import Lean.HeadIndex
 import Lean.Meta.Basic
@@ -47,9 +48,10 @@ register_builtin_option grind.debug.proofs : Bool := {
 
 /-- Context for `GrindM` monad. -/
 structure Context where
-  simp     : Simp.Context
-  simprocs : Array Simp.Simprocs
+  simp         : Simp.Context
+  simprocs     : Array Simp.Simprocs
   mainDeclName : Name
+  config       : Grind.Config
 
 /-- Key for the congruence theorem cache. -/
 structure CongrTheoremCacheKey where
@@ -87,6 +89,10 @@ instance : Nonempty MethodsRef := MethodsRefPointed.property
 
 abbrev GrindM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 
+/-- Returns the user-defined configuration options -/
+def getConfig : GrindM Grind.Config :=
+  return (← readThe Context).config
+
 /-- Returns the internalized `True` constant.  -/
 def getTrueExpr : GrindM Expr := do
   return (← get).trueExpr
@@ -101,10 +107,9 @@ def getMainDeclName : GrindM Name :=
 @[inline] def getMethodsRef : GrindM MethodsRef :=
   read
 
-/--
-Returns maximum term generation that is considered during ematching. -/
+/-- Returns maximum term generation that is considered during ematching. -/
 def getMaxGeneration : GrindM Nat := do
-  return 10000 -- TODO
+  return (← getConfig).gen
 
 /--
 Abtracts nested proofs in `e`. This is a preprocessing step performed before internalization.
@@ -355,7 +360,7 @@ def markTheorenInstance (proof : Expr) (assignment : Array Expr) : GoalM Bool :=
 
 /-- Returns `true` if the maximum number of instances has been reached. -/
 def checkMaxInstancesExceeded : GoalM Bool := do
-  return false -- TODO
+  return (← get).numInstances >= (← getConfig).instances
 
 /-- Returns `true` if `e` is the internalized `True` expression.  -/
 def isTrueExpr (e : Expr) : GrindM Bool :=

tests/lean/run/grind_ematch1.lean

@@ -51,3 +51,12 @@ info: [grind.ematch.instance] Rtrans: R c d → R d e → R c e
 example : R a b → R b c → R c d → R d e → R d n → False := by
   fail_if_success grind
   sorry
+
+/--
+info: [grind.ematch.instance] Rtrans: R c d → R d e → R c e
+[grind.ematch.instance] Rtrans: R c d → R d n → R c n
+-/
+#guard_msgs (info) in
+example : R a b → R b c → R c d → R d e → R d n → False := by
+  fail_if_success grind (instances := 2)
+  sorry