feat: add grind interactive mode tactics (#10731)

This PR adds the following tactics to the `grind` interactive mode:
- `focus <grind_tac_seq>`
- `next => <grind_tac_seq>`
- `any_goals <grind_tac_seq>`
- `all_goals <grind_tac_seq>`
- `grind_tac <;> grind_tac`
- `cases <anchor>`
- `tactic => <tac_seq>`

Example:
```lean
def g (as : List Nat) :=
  match as with
  | []      => 1
  | [_]     => 2
  | _::_::_ => 3

example : g bs = 1 → g as ≠ 0 := by
  grind [g.eq_def] =>
    instantiate
    cases #ec88
    next => instantiate
    next => finish
    tactic =>
      rw [h_2] at h_1
      simp [g] at h_1
```

src/Init/Grind/Interactive.lean

@@ -51,6 +51,7 @@ syntax:max "!" show_filter:40 : show_filter
 
 syntax showFilter := (colGt show_filter)?
 
+-- **Note**: Should we rename the following tactics to `trace_`?
 /-- Shows asserted facts. -/
 syntax (name := showAsserted) "show_asserted " showFilter : grind
 /-- Shows propositions known to be `True`. -/
@@ -66,7 +67,7 @@ syntax (name := «showState») "show_state " showFilter : grind
 
 declare_syntax_cat grind_ref (behavior := both)
 
-syntax:max "#" noWs num : grind_ref
+syntax:max "#" noWs hexnum : grind_ref
 syntax term : grind_ref
 
 syntax (name := cases) "cases " grind_ref (" with " (colGt ident)+)? : grind
@@ -82,4 +83,44 @@ syntax (name := «have») "have" letDecl : grind
 /-- Executes the given tactic block to close the current goal. -/
 syntax (name := nestedTacticCore) "tactic" " => " tacticSeq : grind
 
+/--
+`all_goals tac` runs `tac` on each goal, concatenating the resulting goals.
+If the tactic fails on any goal, the entire `all_goals` tactic fails.
+-/
+syntax (name := allGoals) "all_goals " grindSeq : grind
+
+/--
+`focus tac` focuses on the main goal, suppressing all other goals, and runs `tac` on it.
+Usually `· tac`, which enforces that the goal is closed by `tac`, should be preferred.
+-/
+syntax (name := focus) "focus " grindSeq : grind
+
+syntax (name := next) "next" " => " grindSeq : grind
+
+/--
+`any_goals tac` applies the tactic `tac` to every goal,
+concatenating the resulting goals for successful tactic applications.
+If the tactic fails on all of the goals, the entire `any_goals` tactic fails.
+
+This tactic is like `all_goals try tac` except that it fails if none of the applications of `tac` succeeds.
+-/
+syntax (name := anyGoals) "any_goals " grindSeq : grind
+
+/--
+`with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with
+the initial and final state of running tactic `t`.
+-/
+scoped syntax (name := withAnnotateState)
+  "with_annotate_state " rawStx ppSpace grind : grind
+
+/--
+`tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal,
+concatenating all goals produced by `tac'`.
+-/
+macro:1 x:grind tk:" <;> " y:grind:2 : grind => `(grind|
+  focus
+    $x:grind
+    with_annotate_state $tk skip
+    all_goals $y:grind)
+
 end Lean.Parser.Tactic.Grind

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

@@ -12,6 +12,9 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Search
 import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.Split
+import Lean.Meta.Tactic.Grind.Anchor
+import Lean.Elab.Tactic.Basic
 namespace Lean.Elab.Tactic.Grind
 
 def evalSepTactics (stx : Syntax) : GrindTacticM Unit := do
@@ -78,4 +81,108 @@ open Meta Grind
     getGoal
   replaceMainGoal [goal]
 
+@[builtin_grind_tactic cases] def evalCases : GrindTactic := fun stx => do
+  match stx with
+  | `(grind| cases #$anchor:hexnum) =>
+    let numDigits := anchor.getHexNumSize
+    let val := anchor.getHexNumVal
+    if val >= UInt64.size then
+      throwError "invalid anchor, value is too big"
+    let val := val.toUInt64
+    let goal ← getMainGoal
+    let candidates := goal.split.candidates
+    let (goals, genNew) ← liftSearchM do
+      for c in candidates do
+        let anchor ← getAnchor c.getExpr
+        if isAnchorPrefix numDigits val anchor then
+          let some result ← split? c
+            | throwError "`cases` tactic failed, case-split is not ready{indentExpr c.getExpr}"
+          return result
+      throwError "`cases` tactic failed, invalid anchor"
+    let goals ← goals.filterMapM fun goal => do
+      let (goal, _) ← liftGrindM <| SearchM.run goal do
+        intros genNew
+        getGoal
+      if goal.inconsistent then
+        return none
+      else
+        return some goal
+    replaceMainGoal goals
+  | _ => throwUnsupportedSyntax
+
+@[builtin_grind_tactic Parser.Tactic.Grind.focus] def evalFocus : GrindTactic := fun stx => do
+  let mkInfo ← mkInitialTacticInfo stx[0]
+  focus do
+    -- show focused state on `focus`
+    withInfoContext (pure ()) mkInfo
+    evalGrindTactic stx[1]
+
+@[builtin_grind_tactic allGoals] def evalAllGoals : GrindTactic := fun stx => do
+  let goals ← getGoals
+  let mut goalsNew := #[]
+  let mut abort := false
+  for goal in goals do
+    unless (← goal.mvarId.isAssigned) do
+      setGoals [goal]
+      let saved ← saveState
+      abort ← Grind.tryCatch
+        (do
+          evalGrindTactic stx[1]
+          pure abort)
+        (fun ex => do
+          if (← read).recover then
+            logException ex
+            let msgLog ← Core.getMessageLog
+            saved.restore
+            Core.setMessageLog msgLog
+            admitGoal goal.mvarId
+            pure true
+          else
+            throw ex)
+      goalsNew := goalsNew ++ (← getUnsolvedGoals)
+  if abort then
+    throwAbortTactic
+  setGoals goalsNew.toList
+
+@[builtin_grind_tactic withAnnotateState] def evalWithAnnotateState : GrindTactic := fun stx =>
+  withTacticInfoContext stx[1] do
+  evalGrindTactic stx[2]
+
+@[builtin_grind_tactic anyGoals] def evalAnyGoals : GrindTactic := fun stx => do
+  let goals ← getGoals
+  let mut goalsNew := #[]
+  let mut succeeded := false
+  for goal in goals do
+    unless (← goal.mvarId.isAssigned) do
+      setGoals [goal]
+      try
+        evalGrindTactic stx[1]
+        goalsNew := goalsNew ++ (← getUnsolvedGoals)
+        succeeded := true
+      catch _ =>
+        goalsNew := goalsNew.push goal
+  unless succeeded do
+    throwError "Tactic failed on all goals:{indentD stx[1]}"
+  setGoals goalsNew.toList
+
+@[builtin_grind_tactic «next»] def evalNext : GrindTactic := fun stx => do
+  match stx with
+  | `(grind| next%$nextTk =>%$arr $seq:grindSeq) => do
+    let goal :: goals ← getUnsolvedGoals | throwNoGoalsToBeSolved
+    setGoals [goal]
+    goal.mvarId.setTag Name.anonymous
+    withCaseRef arr seq <| closeUsingOrAdmit <| withTacticInfoContext (mkNullNode #[nextTk, arr]) <|
+      evalGrindTactic stx[2]
+    setGoals goals
+  | _ => throwUnsupportedSyntax
+
+@[builtin_grind_tactic nestedTacticCore] def evalNestedTactic : GrindTactic := fun stx => do
+  match stx with
+  | `(grind| tactic%$tacticTk =>%$arr $seq:tacticSeq) => do
+    let goal ← getMainGoal
+    discard <| Tactic.run goal.mvarId <| withCaseRef arr seq <| Tactic.closeUsingOrAdmit
+      <| Tactic.withTacticInfoContext (mkNullNode #[tacticTk, arr]) <| evalTactic seq
+    replaceMainGoal []
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.Grind

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

@@ -9,6 +9,7 @@ public import Lean.Elab.Tactic.Grind.Basic
 import Init.Grind.Interactive
 import Lean.Meta.Tactic.Grind.PP
 import Lean.Meta.Tactic.Grind.Anchor
+import Lean.Meta.Tactic.Grind.Split
 namespace Lean.Elab.Tactic.Grind
 open Meta
 
@@ -198,12 +199,20 @@ def anchorToString (numDigits : Nat) (anchor : UInt64) : String :=
     let filter ← elabFilter filter?
     let goal ← getMainGoal
     let candidates := goal.split.candidates
-    let candidates ← liftGrindM <| candidates.toArray.mapM fun c => do
+    let candidates ← liftGoalM <| candidates.toArray.mapM fun c => do
       let e := c.getExpr
       let anchor ← getAnchor e
-      return (e, anchor)
+      let status ← checkSplitStatus c
+      return (e, status, anchor)
+    let candidates ← liftGoalM <| candidates.filterM fun (e, status, _) => do
+      -- **Note**: we ignore case-splits that are not ready or have already been resolved.
+      -- We may consider adding an option for including "not-ready" splits in the future.
+      if status matches .resolved | .notReady then return false
+      filter.eval e
+    -- **TODO**: Add an option for including propositions that are only considered when using `+splitImp`
+    -- **TODO**: Add an option for including terms whose type is an inductive predicate or type
+    let candidates := candidates.map fun (e, _, anchor) => (e, anchor)
     let (candidates, numDigits) := truncateAnchors candidates
-    let candidates ← liftGoalM <| candidates.filterM fun (e, _) => filter.eval e
     if candidates.isEmpty then
       throwError "no case splits"
     let msgs := candidates.map fun (e, a) =>

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

@@ -243,19 +243,19 @@ private def casesWithTrace (mvarId : MVarId) (major : Expr) : GoalM (List MVarId
   cases mvarId major
 
 /--
-Selects a case-split from the list of candidates, and adds new choice point
-(aka backtracking point). Returns true if successful.
+Performs a case-split using `c`.
+Remarks:
+- `mvarId` is not necessarily `(← getGoal).mvarId`, `splitNext` creates an auxiliary meta-variable
+  to be able to implement non-chronological backtracking.
+- `numCases` and `isRec` are computed using `checkSplitStatus`.
 -/
-def splitNext : SearchM Bool := withCurrGoalContext do
-  let .some c numCases isRec _ ← selectNextSplit?
-    | return false
+private def splitCore (mvarId : MVarId) (c : SplitInfo) (numCases : Nat) (isRec : Bool) : SearchM (List Goal × Nat) := do
   let cExpr := c.getExpr
   let gen ← getGeneration cExpr
   let genNew := if numCases > 1 || isRec then gen+1 else gen
   saveSplitDiagInfo cExpr genNew numCases c.source
   markCaseSplitAsResolved cExpr
   trace_goal[grind.split] "{cExpr}, generation: {gen}"
-  let mvarId ← mkAuxMVarForCurrGoal
   let mvarIds ← if let .imp e h _ := c then
     casesWithTrace mvarId (mkGrindEM (e.forallDomain h))
   else if (← isMatcherApp cExpr) then
@@ -268,8 +268,28 @@ def splitNext : SearchM Bool := withCurrGoalContext do
     mvarId
     split.trace := { expr := cExpr, i, num := numSubgoals, source := c.source } :: goal.split.trace
   }
+  return (goals, genNew)
+
+/--
+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?
+    | return false
+  let mvarId ← mkAuxMVarForCurrGoal
+  let (goals, genNew) ← splitCore mvarId c numCases isRec
   mkChoice (mkMVar mvarId) goals genNew
   intros genNew
   return true
 
+/--
+Tries to perform a case-split using `c`. Returns `none` if `c` has already been resolved or
+is not ready.
+-/
+def split? (c : SplitInfo) : SearchM (Option (List Goal × Nat)) := do
+  let .ready numCases isRec ← checkSplitStatus c | return none
+  let mvarId := (← getGoal).mvarId
+  return some (← splitCore mvarId c numCases isRec)
+
 end Lean.Meta.Grind

tests/lean/run/grind_interactive.lean

@@ -181,6 +181,16 @@ example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p
     show_splits
     sorry
 
+/--
+trace: [splits] Case split candidates
+  [split] #65fc := p ∨ p₁ = p₂
+  [split] #1460 := p ∨ q ∧ r
+-/
+example (r p q p₁ p₂ : Prop) : (p₁ → q) → p ∨ (q ∧ r) → p ∨ (p₁ ↔ p₂) → False := by
+  grind =>
+    show_splits
+    sorry
+
 def h (as : List Nat) :=
   match as with
   | []      => 1
@@ -204,3 +214,62 @@ example : h bs = 1 → h as ≠ 0 := by
     instantiate
     show_splits
     sorry
+
+example : h bs = 1 → h as ≠ 0 := by
+  grind [h.eq_def] =>
+    instantiate
+    show_splits
+    cases #ec88
+    instantiate
+    focus instantiate
+    instantiate
+
+example : h bs = 1 → h as ≠ 0 := by
+  grind [h.eq_def] =>
+    instantiate
+    cases #ec88
+    all_goals instantiate
+
+example : h bs = 1 → h as ≠ 0 := by
+  grind [h.eq_def] =>
+    instantiate
+    cases #ec88 <;> instantiate
+
+example : h bs = 1 → h as ≠ 1 := by
+  grind [h.eq_def] =>
+    instantiate
+    cases #ec88
+    any_goals instantiate
+    sorry
+
+/--
+error: unsolved goals
+bs as : List Nat
+h : _root_.h bs = 1
+h_1 : _root_.h as = 0
+h_2 : as = []
+⊢ False
+-/
+#guard_msgs in
+example : h bs = 1 → h as ≠ 0 := by
+  grind [h.eq_def] =>
+    instantiate
+    cases #ec88
+    next => skip
+    all_goals sorry
+
+def g (as : List Nat) :=
+  match as with
+  | []      => 1
+  | [_]     => 2
+  | _::_::_ => 3
+
+example : g bs = 1 → g as ≠ 0 := by
+  grind [g.eq_def] =>
+    instantiate
+    cases #ec88
+    next => instantiate
+    next => finish
+    tactic =>
+      rw [h_2] at h_1
+      simp [g] at h_1