feat: model-based theory combination tactic and action (#10950)

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/Elab/Tactic/Grind/Trace.lean

@@ -20,7 +20,8 @@ def withTracing (x : GrindTacticM α) : GrindTacticM α := do
 
 def mkFinish (maxIterations : Nat) : IO Action := do
   let solvers ← Solvers.mkAction
-  return Action.checkTactic >> (Action.done <|> solvers <|> Action.instantiate <|> Action.splitNext).loop maxIterations
+  let step : Action := Action.done <|> solvers <|> Action.instantiate <|> Action.splitNext <|> Action.mbtc
+  return Action.checkTactic (warnOnly := true) >> step.loop maxIterations
 
 def maxIterations := 1000 -- **TODO**: Add option
 

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
@@ -282,21 +282,26 @@ def checkSeqAt (s? : Option SavedState) (goal : Goal) (seq : List TGrind) : Grin
 /--
 Helper action that checks whether the resulting tactic script produced by its continuation
 can close the original goal.
+If `warnOnly = true`, just generates a warning message instead of an error
 -/
-def checkTactic : Action := fun goal _ kp => do
+def checkTactic (warnOnly : Bool) : Action := fun goal _ kp => do
   let s ← saveStateIfTracing
   let r ← kp goal
   match r with
   | .closed seq =>
     unless (← checkSeqAt s goal seq) do
-      throwError "generated tactic cannot close the goal{indentD (← mkGrindNext seq)}\nInitial goal\n{goal.mvarId}"
+      let m := m!"generated tactic cannot close the goal{indentD (← mkGrindNext seq)}\nInitial goal\n{goal.mvarId}"
+      if warnOnly then
+        logWarning m
+      else
+        throwError m
     return r
   | _ => return r
 
 /--
 Helper action for satellite solvers that use `CheckResult`.
 -/
-def solverAction (check : GoalM CheckResult) (mkTac : GrindM (TSyntax `grind)) : Action := fun goal kna kp => do
+def solverAction (check : GoalM CheckResult) (mkTac : GrindM TGrind) : Action := fun goal kna kp => do
   let saved? ← saveStateIfTracing
   let (result, goal') ← GoalM.run goal check
   match result with
@@ -327,6 +332,24 @@ def solverAction (check : GoalM CheckResult) (mkTac : GrindM (TSyntax `grind)) :
       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,31 @@ 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?
+
+example (f : Int → Int → Int) (x y : Int)
+    : 0 ≤ x → x ≠ 0 → x ≤ 1 → f x y = 2 → f 1 y = 2 := by
+  grind =>
+    -- We can use `have` to golf proofs using `mbtc` and `cases`
+    have : x = 1