feat: add checkTactic action

Author: leodemoura

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

@@ -344,8 +344,7 @@ def liftSearchM (k : SearchM α) : GrindTacticM α := do
 def GrindTacticM.run (x : GrindTacticM α) (ctx : Context) (s : State) : TermElabM (α × State) :=
   x ctx |>.run s
 
-def mkEvalTactic (params : Params) : TacticM (Goal → TSyntax `grind → GrindM (List Goal)) := do
-  let elaborator := (← read).elaborator
+def mkEvalTactic' (elaborator : Name) (params : Params) : TermElabM (Goal → TSyntax `grind → GrindM (List Goal)) := do
   let termState ← getThe Term.State
   let termCtx ← readThe Term.Context
   let eval (goal : Goal) (stx : TSyntax `grind) : GrindM (List Goal) := do
@@ -364,6 +363,9 @@ def mkEvalTactic (params : Params) : TacticM (Goal → TSyntax `grind → GrindM
     return subgoals
   return eval
 
+def mkEvalTactic (params : Params) : TacticM (Goal → TSyntax `grind → GrindM (List Goal)) := do
+  mkEvalTactic' (← read).elaborator params
+
 def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM α) : TacticM (α × State) := do
   let evalTactic ← mkEvalTactic params
   let (methods, ctx, state) ← liftMetaM <| GrindM.runAtGoal mvarId params (evalTactic? := some evalTactic) fun goal => do

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

@@ -247,7 +247,7 @@ A terminal action which closes the goal or not.
 This kind of action may make progress, but we only include `mkTac` into the resulting tactic sequence
 if it closed the goal.
 -/
-public def terminalAction (check : GoalM Bool) (mkTac : GrindM (TSyntax `grind)) : Action := fun goal kna kp => do
+def terminalAction (check : GoalM Bool) (mkTac : GrindM (TSyntax `grind)) : Action := fun goal kna kp => do
   let (progress, goal') ← GoalM.run goal check
   if progress then
     if goal'.inconsistent then
@@ -257,6 +257,24 @@ public def terminalAction (check : GoalM Bool) (mkTac : GrindM (TSyntax `grind))
   else
     kna goal'
 
+/--
+Helper action that checks whether the resulting tactic script produced by its continuation
+can close the original goal.
+-/
+def checkTactic : Action := fun goal _ kp => do
+  let s ← saveState
+  let r ← kp goal
+  match r with
+  | .closed seq =>
+    let tac ← mkGrindNext seq
+    Lean.withoutModifyingState do
+      s.restore
+      let subgoals ← evalTactic goal tac
+      unless subgoals.isEmpty do
+        throwError "generated tactic cannot close the goal{indentD tac}\nInitial goal\n{goal.mvarId}\nPending subgoals\n{subgoals.map (·.mvarId)}"
+    return r
+  | _ => return r
+
 section
 /-!
 Some sanity check properties.