feat: model-based theory combination tactic and action

This PR adds the `mbtc` tactic to the `grind` interactive mode. It
implements model-based theory combination. It also ensures `finish?`
is capable of generating it.

Author: leodemoura

src/Init/Grind/Interactive.lean

@@ -225,5 +225,10 @@ Proves `<term>` using the current `grind` state and default search strategy.
 -/
 syntax (name := haveSilent) "have" (ppSpace ident)? ppSpace ": " term : grind
 
+/--
+Adds new case-splits using model-based theory combination.
+-/
+syntax (name := mbtc) "mbtc" : grind
+
 end Grind
 end Lean.Parser.Tactic

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

@@ -429,4 +429,13 @@ where
   let options ← Elab.elabSetOption stx[1] stx[3]
   withOptions (fun _ => options) do evalGrindTactic stx[5]
 
+@[builtin_grind_tactic mbtc] def elabMBTC : GrindTactic := fun _ => do
+  liftGoalM do
+    discard <| Solvers.check
+    if (← get).inconsistent then
+      return ()
+    let progress ← Solvers.mbtc
+    unless progress do
+      throwError "`mbtc` tactic failed to generate new candidate case-splits."
+
 end Lean.Elab.Tactic.Grind

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

@@ -225,7 +225,7 @@ Appends a new tactic syntax to a successful result.
 Used by leaf actions to record the tactic that produced progress.
 If `(← getConfig).trace` is `false`, it just returns `r`.
 -/
-def concatTactic (r : ActionResult) (mk : GrindM (TSyntax `grind)) : GrindM ActionResult := do
+def concatTactic (r : ActionResult) (mk : GrindM TGrind) : GrindM ActionResult := do
   if (← getConfig).trace then
     match r with
     | .closed seq =>
@@ -236,7 +236,7 @@ def concatTactic (r : ActionResult) (mk : GrindM (TSyntax `grind)) : GrindM Acti
     return r
 
 /-- Returns `.closed [← mk]` if tracing is enabled, and `.closed []` otherwise. -/
-def closeWith (mk : GrindM (TSyntax `grind)) : GrindM ActionResult := do
+def closeWith (mk : GrindM TGrind) : GrindM ActionResult := do
   if (← getConfig).trace then
     return .closed [(← mk)]
   else
@@ -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.
 -/
-def terminalAction (check : GoalM Bool) (mkTac : GrindM (TSyntax `grind)) : Action := fun goal kna kp => do
+def terminalAction (check : GoalM Bool) (mkTac : GrindM TGrind) : Action := fun goal kna kp => do
   let (progress, goal') ← GoalM.run goal check
   if progress then
     if goal'.inconsistent then
@@ -332,6 +332,24 @@ def solverAction (check : GoalM CheckResult) (mkTac : GrindM TGrind) : Action :=
       kp goal'
   | .closed     => closeWith mkTac
 
+def mbtc : Action := fun goal kna kp => do
+  let saved? ← saveStateIfTracing
+  let (progress, goal') ← GoalM.run goal Solvers.mbtc
+  if progress then
+    if (← getConfig).trace then
+      match (← kp goal') with
+      | .closed seq =>
+        if (← checkSeqAt saved? goal seq) then
+          return .closed seq
+        else
+          let tac ← `(grind| mbtc)
+          return .closed (tac :: seq)
+      | r => return r
+    else
+      kp goal'
+  else
+    kna goal'
+
 section
 /-!
 Some sanity check properties.

tests/lean/run/grind_finish_trace.lean

@@ -134,3 +134,25 @@ info: Try this:
 example (a : Array (BitVec 64)) (i : Nat) (v : BitVec 64)
     : (_ : i < a.size) → (_ : i + 1 < a.size) → (a.set i v)[i+1] + a[i+1] = 2*a[i+1] := by
   grind => finish?
+
+/--
+info: Try this:
+  [apply] ⏎
+    mbtc
+    cases #a6c8
+-/
+#guard_msgs in
+example (f : Nat → Nat) (x : Nat)
+    : x ≠ 0 → x ≤ 1 → f x = 2 → f 1 = 2 := by
+  grind => finish?
+
+/--
+info: Try this:
+  [apply] ⏎
+    mbtc
+    cases #beb4
+-/
+#guard_msgs in
+example (f : Int → Int → Int) (x y : Int)
+    : 0 ≤ x → x ≠ 0 → x ≤ 1 → f x y = 2 → f 1 y = 2 := by
+  grind => finish?