feat: finish? and grind? infrastructure (#10747)

This PR implements infrastructure for `finish?` and `grind?` tactics.

Author: leodemoura

src/Init/Meta.lean

@@ -6,14 +6,11 @@ Authors: Leonardo de Moura and Sebastian Ullrich
 Additional goodies for writing macros
 -/
 module
-
 prelude
 public import Init.Meta.Defs
 public meta import Init.Meta.Defs
 public import Init.Tactics
-
 public section
-
 namespace Lean
 
 macro_rules

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

@@ -34,9 +34,10 @@ builtin_initialize registerTraceClass `grind.debug.ac.eq
 builtin_initialize
   acExt.setMethods
     (internalize := AC.internalize)
-    (newEq := AC.processNewEq)
-    (newDiseq := AC.processNewDiseq)
-    (check := AC.check)
-    (checkInv := AC.checkInvariants)
+    (newEq       := AC.processNewEq)
+    (newDiseq    := AC.processNewDiseq)
+    (check       := AC.check)
+    (checkInv    := AC.checkInvariants)
+    (mkTactic?   := return some (← `(grind| ac)))
 
 end Lean.Meta.Grind.AC

src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean

@@ -55,5 +55,6 @@ builtin_initialize
     (newDiseq    := CommRing.processNewDiseq)
     (check       := CommRing.check)
     (checkInv    := CommRing.checkInvariants)
+    (mkTactic?   := return some (← `(grind| ring)))
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean

@@ -52,5 +52,6 @@ builtin_initialize
     (check       := Cutsat.check)
     (checkInv    := Cutsat.checkInvariants)
     (mbtc        := Cutsat.mbtc)
+    (mkTactic?   := return some (← `(grind| lia)))
 
 end Lean.Meta.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Linear.lean

@@ -50,5 +50,6 @@ builtin_initialize
     (check       := Linear.check)
     (checkInv    := Linear.checkInvariants)
     (mbtc        := Linear.mbtc)
+    (mkTactic?   := return some (← `(grind| linarith)))
 
 end Lean.Meta.Grind.Arith.Linear

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

@@ -5,13 +5,13 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Util
-public import Lean.Meta.Basic
-public import Lean.Meta.FunInfo
-public import Lean.Util.FVarSubset
-public import Lean.Util.PtrSet
-public import Lean.Util.FVarSubset
 public import Lean.Meta.Tactic.Grind.Types
+import Init.Grind.Util
+import Lean.Meta.Basic
+import Lean.Meta.FunInfo
+import Lean.Util.FVarSubset
+import Lean.Util.PtrSet
+import Lean.Util.FVarSubset
 import Lean.Meta.IntInstTesters
 import Lean.Meta.NatInstTesters
 public section

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

@@ -9,17 +9,33 @@ public import Lean.Meta.Tactic.Grind.Types
 import Lean.Util.ForEachExpr
 public section
 namespace Lean.Meta.Grind
+
+/-- Helper type for implementing `finish?` and `grind?` -/
+inductive ProofStep where
+  | solver (id : Nat)
+  | lookahead | mbtc
+  | instantiate (thms : List EMatchTheorem) (usedThms : List EMatchTheorem)
+  deriving Inhabited
+
+/-- Helper type for implementing `finish?` and `grind?` -/
+inductive ProofTrace where
+  | done
+  | sep (s : ProofStep) (k : ProofTrace)
+  | cases (info : SplitInfo) (alts : List ProofTrace)
+  deriving Inhabited
+
 /--
 A `choice` (aka backtracking) point in the search tree.
 -/
 structure Choice where
+  info?       : Option SplitInfo
   /--
   Goal where the case-split was performed.
-  Invariant: `goalOld.mvarId` is not assigned.
+  Invariant: `goalPending.mvarId` is not assigned.
   -/
   goalPending : Goal
   /--
-  Expression to be assigned to `goalOld.mvarId` if it is not possible to perform
+  Expression to be assigned to `goalPending.mvarId` if it is not possible to perform
   non-chronological backtracking.
   `proof` is often a `casesOn` application containing meta-variables.
   -/
@@ -28,11 +44,14 @@ structure Choice where
   Subgoals that still need to be processed.
   -/
   todo       : List Goal
+  traces     : Array ProofTrace := #[]
   generation : Nat
   deriving Inhabited
 
 structure SearchM.State where
-  goal : Goal
+  goal        : Goal
+  steps       : Array ProofStep := #[]
+  trace?      : Option ProofTrace := none
   choiceStack : List Choice := []
 
 abbrev SearchM := StateRefT SearchM.State GrindM
@@ -66,7 +85,7 @@ update current goal using `s`.
 - If there are more than one `s :: ss`, we create a choice point using the current
 goal as the pending goal, and update the current goal with `s`.
 -/
-def mkChoice (proof : Expr) (subgoals : List Goal) (generation : Nat) : SearchM Unit := do
+def mkChoice (proof : Expr) (subgoals : List Goal) (generation : Nat) (info? : Option SplitInfo := none) : SearchM Unit := do
   assert! !(← isInconsistent)
   match subgoals with
   | [] =>
@@ -79,7 +98,7 @@ def mkChoice (proof : Expr) (subgoals : List Goal) (generation : Nat) : SearchM
     let goalPending ← getGoal
     modify fun s => { s with
       goal := subgoal
-      choiceStack := { goalPending, proof, generation, todo := subgoals } :: s.choiceStack
+      choiceStack := { info?, goalPending, proof, generation, todo := subgoals } :: s.choiceStack
     }
 
 /--
@@ -94,6 +113,9 @@ def mkAuxMVarForCurrGoal : SearchM MVarId := withCurrGoalContext do
   let mvarNew ← mkFreshExprSyntheticOpaqueMVar type tag
   return mvarNew.mvarId!
 
+/--
+Returns the maximum free variable id occurring in `e`
+-/
 private def findMaxFVarIdx? (e : Expr) : MetaM (Option Nat) := do
   let go (e : Expr) : StateT (Option Nat) MetaM Bool := do
     unless e.hasFVar do return false
@@ -187,14 +209,14 @@ def nextGoal? : SearchM (Option Nat) := do
     let mvarDecl ← choice.goalPending.mvarId.getDecl
     let numIndices := mvarDecl.lctx.numIndices
     if maxFVarIdx < numIndices then
-      -- `falseProof` can close `choice.goalOld` since all its free-variables are in scope.
+      -- `falseProof` can close `choice.goalPending` since all its free-variables are in scope.
       choice.goalPending.mvarId.assignFalseProof falseProof
       -- keep looking at next choice point
       -- Remark: we may be able to find other choice points using falseProof.
       choices := choices'
     else match choice.todo with
       | [] =>
-        -- All subgoals have been solved. We can finally assign `choice.proof` to `goalOld.mvarId`.
+        -- All subgoals have been solved. We can finally assign `choice.proof` to `goalPending.mvarId`.
         let proof ← instantiateMVars choice.proof
         choice.goalPending.mvarId.assign proof
         if (← isTargetFalse choice.goalPending.mvarId) then

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

@@ -13,6 +13,36 @@ import Lean.Meta.Tactic.Grind.Lookahead
 import Lean.Meta.Tactic.Grind.Intro
 public section
 namespace Lean.Meta.Grind
+
+def checkSolvers : SearchM Bool := do
+  if (← getConfig).trace then
+    let some solverIds ← Solvers.check? | return false
+    modify fun s => { s with steps := s.steps ++ solverIds.map (.solver ·) }
+    return true
+  else
+    Solvers.check
+
+def ematchStep : SearchM Bool := do
+  if (← getConfig).trace then
+    let .true ← ematch | return false
+    -- TODO: Collect instances
+    modify fun s => { s with steps := s.steps.push <| .instantiate [] [] }
+    return true
+  else
+    ematch
+
+def mbtcStep : SearchM Bool := do
+  let .true ← Solvers.mbtc | return false
+  if (← getConfig).trace then
+    modify fun s => { s with steps := s.steps.push .mbtc }
+  return true
+
+def lookaheadStep : SearchM Bool := do
+  let .true ← lookahead | return false
+  if (← getConfig).trace then
+    modify fun s => { s with steps := s.steps.push .lookahead }
+  return true
+
 /--
 Try to solve/close the given goal.
 Returns `some goal` if this subgoal failed to be closed,
@@ -39,8 +69,8 @@ where
           intros gen
         else
           break
-      if (← assertAll <||> Solvers.check <||> ematch <||> lookahead <||> splitNext
-           <||> Solvers.mbtc) then
+      if (← assertAll <||> checkSolvers <||> ematchStep <||> lookaheadStep <||> splitNext
+           <||> mbtcStep) then
         continue
       return some (← getGoal) -- failed
     return none -- solved

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

@@ -275,11 +275,11 @@ Selects a case-split from the list of candidates, and adds new choice point
 (aka backtracking point). Returns true if successful.
 -/
 def splitNext : SearchM Bool := withCurrGoalContext do
-  let .some c numCases isRec _ ← selectNextSplit?
+  let .some info numCases isRec _ ← selectNextSplit?
     | return false
   let mvarId ← mkAuxMVarForCurrGoal
-  let (goals, genNew) ← splitCore mvarId c numCases isRec
-  mkChoice (mkMVar mvarId) goals genNew
+  let (goals, genNew) ← splitCore mvarId info numCases isRec
+  mkChoice (mkMVar mvarId) goals genNew (info? := some info)
   intros genNew
   return true
 

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

@@ -1461,6 +1461,7 @@ structure SolverExtension (σ : Type) where private mk ::
   mbtc        : GoalM Bool
   check       : GoalM Bool
   checkInv    : GoalM Unit
+  mkTactic?   : CoreM (Option (TSyntax `grind))
   deriving Inhabited
 
 private builtin_initialize solverExtensionsRef : IO.Ref (Array (SolverExtension SolverExtensionState)) ← IO.mkRef #[]
@@ -1470,7 +1471,7 @@ Registers a new solver extension for `grind`.
 Solver extensions can only be registered during initialization.
 Reason: We do not use any synchronization primitive to access `solverExtensionsRef`.
 -/
-def registerSolverExtension {σ : Type} (mkInitial   : IO σ) : IO (SolverExtension σ) := do
+def registerSolverExtension {σ : Type} (mkInitial : IO σ) : IO (SolverExtension σ) := do
   unless (← initializing) do
     throw (IO.userError "failed to register `grind` solver, extensions can only be registered during initialization")
   let exts ← solverExtensionsRef.get
@@ -1483,6 +1484,7 @@ def registerSolverExtension {σ : Type} (mkInitial   : IO σ) : IO (SolverExtens
     check := fun _ _ => return false
     checkInv := fun _ _ => return ()
     mbtc := fun _ _ => return false
+    mkTactic? := return none
   }
   solverExtensionsRef.modify fun exts => exts.push (unsafe unsafeCast ext)
   return ext
@@ -1498,13 +1500,15 @@ def SolverExtension.setMethods (ext : SolverExtension σ)
     (newDiseq    : Expr → Expr → GoalM Unit := fun _ _ => return ())
     (mbtc        : GoalM Bool := return false)
     (check       : GoalM Bool := return false)
-    (checkInv    : GoalM Unit := return ()) : IO Unit := do
+    (checkInv    : GoalM Unit := return ())
+    (mkTactic?   : CoreM (Option (TSyntax `grind)) := return none)
+    : IO Unit := do
   unless (← initializing) do
     throw (IO.userError "failed to register `grind` solver, extensions can only be registered during initialization")
   unless ext.id < (← solverExtensionsRef.get).size do
     throw (IO.userError "failed to register `grind` solver methods, invalid solver id")
   solverExtensionsRef.modify fun exts => exts.modify ext.id fun s => { s with
-    internalize, newEq, newDiseq, mbtc, check, checkInv
+    internalize, newEq, newDiseq, mbtc, check, checkInv, mkTactic?
   }
 
 /-- Returns initial state for registered solvers. -/
@@ -1540,17 +1544,25 @@ def Solvers.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
 def Solvers.checkInvariants : GoalM Unit := do
   (← solverExtensionsRef.get).forM fun ext => ext.checkInv
 
-/-- Performs (expensive) satisfiability checks in all registered solvers. -/
-def Solvers.check : GoalM Bool := do
-  let mut result := false
+/--
+Performs (expensive) satisfiability checks in all registered solvers,
+and returns the solver ids that made progress.
+-/
+def Solvers.check? : GoalM (Option (Array Nat)) := do
+  let mut result := #[]
   for ext in (← solverExtensionsRef.get) do
     if (← isInconsistent) then
-      return true
+      return some result
     if (← ext.check) then
-      result := true
-  if result then
+      result := result.push ext.id
+  if !result.isEmpty then
     processNewFacts
-  return result
+    return some result
+  else
+    return none
+
+def Solvers.check : GoalM Bool := do
+  return !(← check?).isNone
 
 /-- Invokes model-based theory combination extensions in all registered solvers. -/
 def Solvers.mbtc : GoalM Bool := do