feat: rename show_splits and show_thms

src/Init/Grind/Interactive.lean

@@ -50,46 +50,48 @@ syntax thm := anchor <|> grindLemma <|> grindLemmaMin
 /-- Instantiates theorems using E-matching. -/
 syntax (name := instantiate) "instantiate" (colGt thm),* : grind
 
-declare_syntax_cat show_filter (behavior := both)
+declare_syntax_cat grind_filter (behavior := both)
 
-syntax:max ident : show_filter
-syntax:max &"gen" " < "  num  : show_filter
-syntax:max &"gen" " = "  num  : show_filter
-syntax:max &"gen" " != " num  : show_filter
-syntax:max &"gen" " ≤ "  num  : show_filter
-syntax:max &"gen" " <= " num  : show_filter
-syntax:max &"gen" " > "  num  : show_filter
-syntax:max &"gen" " ≥ "  num  : show_filter
-syntax:max &"gen" " >= " num  : show_filter
-syntax:max "(" show_filter ")" : show_filter
-syntax:35 show_filter:35 " && " show_filter:36 : show_filter
-syntax:35 show_filter:35 " || " show_filter:36 : show_filter
-syntax:max "!" show_filter:40 : show_filter
+syntax:max ident : grind_filter
+syntax:max &"gen" " < "  num  : grind_filter
+syntax:max &"gen" " = "  num  : grind_filter
+syntax:max &"gen" " != " num  : grind_filter
+syntax:max &"gen" " ≤ "  num  : grind_filter
+syntax:max &"gen" " <= " num  : grind_filter
+syntax:max &"gen" " > "  num  : grind_filter
+syntax:max &"gen" " ≥ "  num  : grind_filter
+syntax:max &"gen" " >= " num  : grind_filter
+syntax:max "(" grind_filter ")" : grind_filter
+syntax:35 grind_filter:35 " && " grind_filter:36 : grind_filter
+syntax:35 grind_filter:35 " || " grind_filter:36 : grind_filter
+syntax:max "!" grind_filter:40 : grind_filter
 
-syntax showFilter := (colGt show_filter)?
+syntax grindFilter := (colGt grind_filter)?
 
 -- **Note**: Should we rename the following tactics to `trace_`?
 /-- Shows asserted facts. -/
-syntax (name := showAsserted) "show_asserted" ppSpace showFilter : grind
+syntax (name := showAsserted) "show_asserted" ppSpace grindFilter : grind
 /-- Shows propositions known to be `True`. -/
-syntax (name := showTrue) "show_true" ppSpace showFilter : grind
+syntax (name := showTrue) "show_true" ppSpace grindFilter : grind
 /-- Shows propositions known to be `False`. -/
-syntax (name := showFalse) "show_false" ppSpace showFilter : grind
+syntax (name := showFalse) "show_false" ppSpace grindFilter : grind
 /-- Shows equivalence classes of terms. -/
-syntax (name := showEqcs) "show_eqcs" ppSpace showFilter : grind
+syntax (name := showEqcs) "show_eqcs" ppSpace grindFilter : grind
 /-- Show case-split candidates. -/
-syntax (name := showSplits) "show_splits" ppSpace showFilter : grind
+syntax (name := showCases) "show_cases" ppSpace grindFilter : grind
 /-- Show `grind` state. -/
-syntax (name := «showState») "show_state" ppSpace showFilter : grind
+syntax (name := «showState») "show_state" ppSpace grindFilter : grind
 /-- Show active local theorems and their anchors for heuristic instantiation. -/
-syntax (name := showThms) "show_thms" : grind
+syntax (name := showLocalThms) "show_local_thms" : grind
 
 declare_syntax_cat grind_ref (behavior := both)
 
 syntax:max anchor : grind_ref
 syntax term : grind_ref
 
-syntax (name := cases) "cases " grind_ref (" with " (colGt ident)+)? : grind
+syntax (name := cases) "cases " grind_ref : grind
+
+syntax (name := casesTrace) "cases?" grindFilter : grind
 
 /-- `done` succeeds iff there are no remaining goals. -/
 syntax (name := done) "done" : grind

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
+import Lean.Meta.Tactic.TryThis
 import Lean.Meta.Tactic.Grind.Solve
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Search
 import Lean.Meta.Tactic.Grind.Arith.Linear.Search
@@ -22,6 +23,7 @@ import Lean.Meta.Tactic.Grind.AC.PP
 import Lean.Meta.Tactic.ExposeNames
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.RenameInaccessibles
+import Lean.Elab.Tactic.Grind.Filter
 namespace Lean.Elab.Tactic.Grind
 
 def evalSepTactics (stx : Syntax) : GrindTacticM Unit := do
@@ -126,17 +128,15 @@ def elabAnchor (anchor : TSyntax `hexnum) : CoreM (Nat × UInt64) := do
   return (numDigits, val)
 
 @[builtin_grind_tactic instantiate] def evalInstantiate : GrindTactic := fun stx => withMainContext do
-  match stx with
-  | `(grind| instantiate $[$thmRefs:thm],*) =>
-    let mut thms := #[]
-    for thmRef in thmRefs do
-      match thmRef with
-      | `(Parser.Tactic.Grind.thm| #$anchor:hexnum) => thms := thms ++ (← withRef thmRef <| elabLocalEMatchTheorem anchor)
-      | `(Parser.Tactic.Grind.thm| $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id false)
-      | `(Parser.Tactic.Grind.thm| ! $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id true)
-      | _ => throwErrorAt thmRef "unexpected theorem reference"
-    ematchThms thms
-  | _ => throwUnsupportedSyntax
+  let `(grind| instantiate $[$thmRefs:thm],*) := stx | throwUnsupportedSyntax
+  let mut thms := #[]
+  for thmRef in thmRefs do
+    match thmRef with
+    | `(Parser.Tactic.Grind.thm| #$anchor:hexnum) => thms := thms ++ (← withRef thmRef <| elabLocalEMatchTheorem anchor)
+    | `(Parser.Tactic.Grind.thm| $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id false)
+    | `(Parser.Tactic.Grind.thm| ! $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id true)
+    | _ => throwErrorAt thmRef "unexpected theorem reference"
+  ematchThms thms
 where
   collectThms (numDigits : Nat) (anchorPrefix : UInt64) (thms : PArray EMatchTheorem) : StateT (Array EMatchTheorem) GrindTacticM Unit := do
     let mut found : Std.HashSet Expr := {}
@@ -248,31 +248,47 @@ def logAnchor (numDigits : Nat) (anchorPrefix : UInt64) (e : Expr) : TermElabM U
        m!"#{anchorToString numDigits anchorPrefix} := {e}"
 
 @[builtin_grind_tactic cases] def evalCases : GrindTactic := fun stx => do
-  match stx with
-  | `(grind| cases #$anchor:hexnum) =>
-    let (numDigits, val) ← elabAnchor anchor
-    let goal ← getMainGoal
-    let candidates := goal.split.candidates
-    let (e, goals, genNew) ← liftSearchM do
-      for c in candidates do
-        let e := c.getExpr
-        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 (e, result)
-      throwError "`cases` tactic failed, invalid anchor"
-    goal.withContext <| withRef anchor <| logAnchor numDigits val e
-    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
+  let `(grind| cases #$anchor:hexnum) := stx | throwUnsupportedSyntax
+  let (numDigits, val) ← elabAnchor anchor
+  let goal ← getMainGoal
+  let candidates := goal.split.candidates
+  let (e, goals, genNew) ← liftSearchM do
+    for c in candidates do
+      let e := c.getExpr
+      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 (e, result)
+    throwError "`cases` tactic failed, invalid anchor"
+  goal.withContext <| withRef anchor <| logAnchor numDigits val e
+  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
+
+def mkCasesSuggestions (candidates : Array SplitCandidateWithAnchor) (numDigits : Nat) : MetaM (Array Tactic.TryThis.Suggestion) := do
+  candidates.mapM fun { anchor, e, .. } => do
+    let anchorStx ← mkAnchorSyntax numDigits anchor
+    let tac ← `(grind| cases $anchorStx:anchor)
+    let msg ← addMessageContext m!"{tac} for{indentExpr e}"
+    return {
+      suggestion   := .tsyntax tac
+      messageData? := some msg
+    }
+
+@[builtin_grind_tactic casesTrace] def evalCasesTrace : GrindTactic := fun stx => withMainContext do
+  let `(grind| cases? $[$filter?]?) := stx | throwUnsupportedSyntax
+  let filter ← elabFilter filter?
+  let { candidates, numDigits } ← liftGoalM <| getSplitCandidateAnchors filter.eval
+  let suggestions ← mkCasesSuggestions candidates numDigits
+  Tactic.TryThis.addSuggestions stx suggestions
+  return ()
 
 @[builtin_grind_tactic Parser.Tactic.Grind.focus] def evalFocus : GrindTactic := fun stx => do
   let mkInfo ← mkInitialTacticInfo stx[0]
@@ -335,28 +351,24 @@ public def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIden
   return mvarId
 
 @[builtin_grind_tactic «next»] def evalNext : GrindTactic := fun stx => do
-  match stx with
-  | `(grind| next%$nextTk $hs* =>%$arr $seq:grindSeq) => do
-    let goal :: goals ← getUnsolvedGoals | throwNoGoalsToBeSolved
-    let mvarId ← renameInaccessibles goal.mvarId hs
-    let goal := { goal with mvarId }
-    setGoals [goal]
-    goal.mvarId.setTag Name.anonymous
-    withCaseRef arr seq <| closeUsingOrAdmit <| withTacticInfoContext (mkNullNode #[nextTk, arr]) <|
-      evalGrindTactic stx[3]
-    setGoals goals
-  | _ => throwUnsupportedSyntax
+  let `(grind| next%$nextTk $hs* =>%$arr $seq:grindSeq) := stx | throwUnsupportedSyntax
+  let goal :: goals ← getUnsolvedGoals | throwNoGoalsToBeSolved
+  let mvarId ← renameInaccessibles goal.mvarId hs
+  let goal := { goal with mvarId }
+  setGoals [goal]
+  goal.mvarId.setTag Name.anonymous
+  withCaseRef arr seq <| closeUsingOrAdmit <| withTacticInfoContext (mkNullNode #[nextTk, arr]) <|
+    evalGrindTactic stx[3]
+  setGoals goals
 
 @[builtin_grind_tactic nestedTacticCore] def evalNestedTactic : GrindTactic := fun stx => do
-  match stx with
-  | `(grind| tactic%$tacticTk =>%$arr $seq:tacticSeq) => do
-    let goal ← getMainGoal
-    let recover := (← read).recover
-    discard <| Tactic.run goal.mvarId <| withCaseRef arr seq <| Tactic.closeUsingOrAdmit
-      <| Tactic.withTacticInfoContext (mkNullNode #[tacticTk, arr])
-      <| Tactic.withRecover recover <| evalTactic seq
-    replaceMainGoal []
-  | _ => throwUnsupportedSyntax
+  let `(grind| tactic%$tacticTk =>%$arr $seq:tacticSeq) := stx | throwUnsupportedSyntax
+  let goal ← getMainGoal
+  let recover := (← read).recover
+  discard <| Tactic.run goal.mvarId <| withCaseRef arr seq <| Tactic.closeUsingOrAdmit
+    <| Tactic.withTacticInfoContext (mkNullNode #[tacticTk, arr])
+    <| Tactic.withRecover recover <| evalTactic seq
+  replaceMainGoal []
 
 @[builtin_grind_tactic «first»] partial def evalFirst : GrindTactic := fun stx => do
   let tacs := stx[1].getArgs
@@ -383,12 +395,11 @@ where
   | `(grind| fail $msg:str) => throwError "{msg.getString}\n{goalsMsg}"
   | _ => throwUnsupportedSyntax
 
-@[builtin_grind_tactic «renameI»] def evalRenameInaccessibles : GrindTactic
-  | `(grind| rename_i $hs*) => do
-    let goal ← getMainGoal
-    let mvarId ← renameInaccessibles goal.mvarId hs
-    replaceMainGoal [{ goal with mvarId }]
-  | _ => throwUnsupportedSyntax
+@[builtin_grind_tactic «renameI»] def evalRenameInaccessibles : GrindTactic := fun stx => do
+  let `(grind| rename_i $hs*) := stx | throwUnsupportedSyntax
+  let goal ← getMainGoal
+  let mvarId ← renameInaccessibles goal.mvarId hs
+  replaceMainGoal [{ goal with mvarId }]
 
 @[builtin_grind_tactic exposeNames] def evalExposeNames : GrindTactic := fun _ => do
   let goal ← getMainGoal

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

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Elab.Tactic.Grind.Basic
+import Init.Grind.Interactive
+namespace Lean.Elab.Tactic.Grind
+open Meta
+
+public inductive Filter where
+  | true
+  | const (declName : Name)
+  | fvar (fvarId : FVarId)
+  | gen (pred : Nat → Bool)
+  | or (a b : Filter)
+  | and (a b : Filter)
+  | not (a : Filter)
+
+public partial def elabFilter (filter? : Option (TSyntax `grind_filter)) : GrindTacticM Filter := do
+  let some filter := filter? | return .true
+  go filter
+where
+  go (filter : TSyntax `grind_filter) : GrindTacticM Filter := do
+    match filter with
+    | `(grind_filter| $id:ident) =>
+      match (← Term.resolveId? id) with
+      | some (.const declName _) => return .const declName
+      | some (.fvar fvarId) => return .fvar fvarId
+      | _ => throwErrorAt id "invalid identifier"
+    | `(grind_filter| $a:grind_filter && $b:grind_filter) => return .and (← go a) (← go b)
+    | `(grind_filter| $a:grind_filter || $b:grind_filter) => return .or (← go a) (← go b)
+    | `(grind_filter| ! $a:grind_filter) => return .not (← go a)
+    | `(grind_filter| ($a:grind_filter)) => go a
+    | `(grind_filter| gen = $n:num)  => let n := n.getNat; return .gen fun x => x == n
+    | `(grind_filter| gen > $n:num)  => let n := n.getNat; return .gen fun x => x > n
+    | `(grind_filter| gen ≥ $n:num)  => let n := n.getNat; return .gen fun x => x ≥ n
+    | `(grind_filter| gen >= $n:num) => let n := n.getNat; return .gen fun x => x ≥ n
+    | `(grind_filter| gen ≤ $n:num)  => let n := n.getNat; return .gen fun x => x ≤ n
+    | `(grind_filter| gen <= $n:num) => let n := n.getNat; return .gen fun x => x ≤ n
+    | `(grind_filter| gen < $n:num)  => let n := n.getNat; return .gen fun x => x < n
+    | `(grind_filter| gen != $n:num) => let n := n.getNat; return .gen fun x => x != n
+    | _ => throwUnsupportedSyntax
+
+open Meta.Grind
+
+-- **Note**: facts may not have been internalized if they are equalities.
+def getGen (e : Expr) : GoalM Nat := do
+  if (← alreadyInternalized e) then
+    getGeneration e
+  else match_expr e with
+   | Eq _ lhs rhs => return max (← getGeneration lhs) (← getGeneration rhs)
+   | _ => return 0
+
+public def Filter.eval (filter : Filter) (e : Expr) : GoalM Bool := do
+  go filter
+where
+  go (filter : Filter) : GoalM Bool := do
+  match filter with
+  | .true => return .true
+  | .and a b => go a <&&> go b
+  | .or a b => go a <||> go b
+  | .not a => return !(← go a)
+  | .const declName => return Option.isSome <| e.find? fun e => e.isConstOf declName
+  | .fvar fvarId => return Option.isSome <| e.find? fun e => e.isFVar && e.fvarId! == fvarId
+  | .gen pred => let gen ← getGen e; return pred gen
+
+end Lean.Elab.Tactic.Grind

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

@@ -6,69 +6,14 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
+import Lean.Elab.Tactic.Grind.Filter
 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
-
-inductive Filter where
-  | true
-  | const (declName : Name)
-  | fvar (fvarId : FVarId)
-  | gen (pred : Nat → Bool)
-  | or (a b : Filter)
-  | and (a b : Filter)
-  | not (a : Filter)
-
-partial def elabFilter (filter? : Option (TSyntax `show_filter)) : GrindTacticM Filter := do
-  let some filter := filter? | return .true
-  go filter
-where
-  go (filter : TSyntax `show_filter) : GrindTacticM Filter := do
-    match filter with
-    | `(show_filter| $id:ident) =>
-      match (← Term.resolveId? id) with
-      | some (.const declName _) => return .const declName
-      | some (.fvar fvarId) => return .fvar fvarId
-      | _ => throwErrorAt id "invalid identifier"
-    | `(show_filter| $a:show_filter && $b:show_filter) => return .and (← go a) (← go b)
-    | `(show_filter| $a:show_filter || $b:show_filter) => return .or (← go a) (← go b)
-    | `(show_filter| ! $a:show_filter) => return .not (← go a)
-    | `(show_filter| ($a:show_filter)) => go a
-    | `(show_filter| gen = $n:num)  => let n := n.getNat; return .gen fun x => x == n
-    | `(show_filter| gen > $n:num)  => let n := n.getNat; return .gen fun x => x > n
-    | `(show_filter| gen ≥ $n:num)  => let n := n.getNat; return .gen fun x => x ≥ n
-    | `(show_filter| gen >= $n:num) => let n := n.getNat; return .gen fun x => x ≥ n
-    | `(show_filter| gen ≤ $n:num)  => let n := n.getNat; return .gen fun x => x ≤ n
-    | `(show_filter| gen <= $n:num) => let n := n.getNat; return .gen fun x => x ≤ n
-    | `(show_filter| gen < $n:num)  => let n := n.getNat; return .gen fun x => x < n
-    | `(show_filter| gen != $n:num) => let n := n.getNat; return .gen fun x => x != n
-    | _ => throwUnsupportedSyntax
-
 open Meta.Grind
 
--- **Note**: facts may not have been internalized if they are equalities.
-def getGen (e : Expr) : GoalM Nat := do
-  if (← alreadyInternalized e) then
-    getGeneration e
-  else match_expr e with
-   | Eq _ lhs rhs => return max (← getGeneration lhs) (← getGeneration rhs)
-   | _ => return 0
-
-def Filter.eval (filter : Filter) (e : Expr) : GoalM Bool := do
-  go filter
-where
-  go (filter : Filter) : GoalM Bool := do
-  match filter with
-  | .true => return .true
-  | .and a b => go a <&&> go b
-  | .or a b => go a <||> go b
-  | .not a => return !(← go a)
-  | .const declName => return Option.isSome <| e.find? fun e => e.isConstOf declName
-  | .fvar fvarId => return Option.isSome <| e.find? fun e => e.isFVar && e.fvarId! == fvarId
-  | .gen pred => let gen ← getGen e; return pred gen
-
 def ppAsserted? (filter : Filter) (collapsed := false) : GrindTacticM (Option MessageData) := do
     let facts ← liftGoalM do (← get).facts.toArray.filterM fun e => filter.eval e
     if facts.isEmpty then
@@ -76,12 +21,10 @@ def ppAsserted? (filter : Filter) (collapsed := false) : GrindTacticM (Option Me
     return some <| Grind.ppExprArray `facts "Asserted facts" facts (collapsed := collapsed)
 
 @[builtin_grind_tactic showAsserted] def evalShowAsserted : GrindTactic := fun stx => withMainContext do
-  match stx with
-  | `(grind| show_asserted $[$filter?]?) =>
-    let filter ← elabFilter filter?
-    let some msg ← ppAsserted? filter | throwError "no facts"
-    logInfo msg
-  | _ => throwUnsupportedSyntax
+  let `(grind| show_asserted $[$filter?]?) := stx | throwUnsupportedSyntax
+  let filter ← elabFilter filter?
+  let some msg ← ppAsserted? filter | throwError "no facts"
+  logInfo msg
 
 def ppProps? (filter : Filter) (isTrue : Bool) (collapsed := false) : GrindTacticM (Option MessageData) := do
   let props ← liftGoalM do
@@ -91,21 +34,19 @@ def ppProps? (filter : Filter) (isTrue : Bool) (collapsed := false) : GrindTacti
     return none
   return some <| Grind.ppExprArray `props s!"{if isTrue then "True" else "False"} propositions" props (collapsed := collapsed)
 
-def showProps (filter? : Option (TSyntax `show_filter)) (isTrue : Bool) : GrindTacticM Unit := withMainContext do
+def showProps (filter? : Option (TSyntax `grind_filter)) (isTrue : Bool) : GrindTacticM Unit := withMainContext do
   let filter ← elabFilter filter?
   let some msg ← ppProps? filter isTrue
     | throwError s!"no {if isTrue then "true" else "false"} propositions"
   logInfo msg
 
 @[builtin_grind_tactic showTrue] def evalShowTrue : GrindTactic := fun stx => do
-  match stx with
-  | `(grind| show_true $[$filter?]?) => showProps filter? true
-  | _ => throwUnsupportedSyntax
+  let `(grind| show_true $[$filter?]?) := stx | throwUnsupportedSyntax
+  showProps filter? true
 
 @[builtin_grind_tactic showFalse] def evalShowFalse : GrindTactic := fun stx => do
-  match stx with
-  | `(grind| show_false $[$filter?]?) => showProps filter? false
-  | _ => throwUnsupportedSyntax
+  let `(grind| show_false $[$filter?]?) := stx | throwUnsupportedSyntax
+  showProps filter? false
 
 def ppEqcs? (filter : Filter) (collapsed := false) : GrindTacticM (Option MessageData) := liftGoalM do
   let mut regularEqcs : Array MessageData := #[]
@@ -143,55 +84,49 @@ def ppEqcs? (filter : Filter) (collapsed := false) : GrindTacticM (Option Messag
     return MessageData.trace { cls := `eqc, collapsed } "Equivalence classes" regularEqcs
 
 @[builtin_grind_tactic showEqcs] def evalShowEqcs : GrindTactic := fun stx => withMainContext do
-  match stx with
-  | `(grind| show_eqcs $[$filter?]?) =>
-    let filter ← elabFilter filter?
-    let some msg ← ppEqcs? filter | throwError "no equivalence classes"
-    logInfo msg
-  | _ => throwUnsupportedSyntax
+  let `(grind| show_eqcs $[$filter?]?) := stx | throwUnsupportedSyntax
+  let filter ← elabFilter filter?
+  let some msg ← ppEqcs? filter | throwError "no equivalence classes"
+  logInfo msg
 
 def pushIfSome (msgs : Array MessageData) (msg? : Option MessageData) : Array MessageData :=
   if let some msg := msg? then msgs.push msg else msgs
 
 @[builtin_grind_tactic showState] def evalShowState : GrindTactic := fun stx => withMainContext do
-  match stx with
-  | `(grind| show_state $[$filter?]?) =>
-    let filter ← elabFilter filter?
-    let msgs := #[]
-    let msgs := pushIfSome msgs (← ppAsserted? filter (collapsed := true))
-    let msgs := pushIfSome msgs (← ppProps? filter true (collapsed := false))
-    let msgs := pushIfSome msgs (← ppProps? filter false (collapsed := false))
-    let msgs := pushIfSome msgs (← ppEqcs? filter (collapsed := false))
-    logInfo <| MessageData.trace { cls := `grind, collapsed := false } "Grind state" msgs
-  | _ => throwUnsupportedSyntax
+  let `(grind| show_state $[$filter?]?) := stx | throwUnsupportedSyntax
+  let filter ← elabFilter filter?
+  let msgs := #[]
+  let msgs := pushIfSome msgs (← ppAsserted? filter (collapsed := true))
+  let msgs := pushIfSome msgs (← ppProps? filter true (collapsed := false))
+  let msgs := pushIfSome msgs (← ppProps? filter false (collapsed := false))
+  let msgs := pushIfSome msgs (← ppEqcs? filter (collapsed := false))
+  logInfo <| MessageData.trace { cls := `grind, collapsed := false } "Grind state" msgs
 
-@[builtin_grind_tactic showSplits] def evalShowSplits : GrindTactic := fun stx => withMainContext do
-  match stx with
-  | `(grind| show_splits $[$filter?]?) =>
-    let filter ← elabFilter filter?
-    let { candidates, numDigits } ← liftGoalM <| getSplitCandidateAnchors filter.eval
-    if candidates.isEmpty then
-      throwError "no case splits"
-    let msgs := candidates.map fun (a, e) =>
-      .trace { cls := `split } m!"#{anchorToString numDigits a} := {e}" #[]
-    let msg := MessageData.trace { cls := `splits, collapsed := false } "Case split candidates" msgs
-    logInfo msg
-  | _ => throwUnsupportedSyntax
+@[builtin_grind_tactic showCases] def evalShowCases : GrindTactic := fun stx => withMainContext do
+  let `(grind| show_cases $[$filter?]?) := stx | throwUnsupportedSyntax
+  let filter ← elabFilter filter?
+  let { candidates, numDigits } ← liftGoalM <| getSplitCandidateAnchors filter.eval
+  if candidates.isEmpty then
+    throwError "no case splits"
+  let msgs := candidates.map fun { anchor,  e, .. } =>
+    .trace { cls := `split } m!"#{anchorToString numDigits anchor} := {e}" #[]
+  let msg := MessageData.trace { cls := `splits, collapsed := false } "Case split candidates" msgs
+  logInfo msg
 
-@[builtin_grind_tactic showThms] def evalShowThms : GrindTactic := fun _ => withMainContext do
+@[builtin_grind_tactic showLocalThms] def evalShowLocalThms : GrindTactic := fun _ => withMainContext do
   let goal ← getMainGoal
   let entries ← liftGrindM do
     let (found, entries) ← go {} {} goal.ematch.thms
     let (_, entries) ← go found entries goal.ematch.newThms
     pure entries
-  let (entries, numDigits) := truncateAnchors entries
-  let msgs := entries.map fun (a, e) =>
-    .trace { cls := `thm } m!"#{anchorToString numDigits a} := {e}" #[]
+  let numDigits := getNumDigitsForAnchors entries
+  let msgs := entries.map fun { anchor, e } =>
+    .trace { cls := `thm } m!"#{anchorToString numDigits anchor} := {e}" #[]
   let msg := MessageData.trace { cls := `thms, collapsed := false } "Local theorems" msgs
   logInfo msg
 where
-  go (found : Std.HashSet Grind.Origin) (result : Array (UInt64 × Expr)) (thms : PArray EMatchTheorem)
-      : GrindM (Std.HashSet Grind.Origin × Array (UInt64 × Expr)) := do
+  go (found : Std.HashSet Grind.Origin) (result : Array ExprWithAnchor) (thms : PArray EMatchTheorem)
+      : GrindM (Std.HashSet Grind.Origin × Array ExprWithAnchor) := do
     let mut found := found
     let mut result := result
     for thm in thms do
@@ -202,7 +137,7 @@ where
         let type ← inferType thm.proof
         -- **Note**: Evaluate how stable these anchors are.
         let anchor ← getAnchor type
-        result := result.push (anchor, type)
+        result := result.push { anchor, e := type }
         pure ()
     return (found, result)
 

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

@@ -87,24 +87,44 @@ public def isAnchorPrefix (numHexDigits : Nat) (anchorPrefix : UInt64) (anchor :
   let shift := 64 - numHexDigits.toUInt64*4
   anchorPrefix == anchor >>> shift
 
-public def truncateAnchors (es : Array (UInt64 × α)) : Array (UInt64 × α) × Nat :=
+public class HasAnchor (α : Type u) where
+  getAnchor : α → UInt64
+
+/--
+Returns the number of digits needed to distinguish the anchors in `es`
+-/
+public def getNumDigitsForAnchors [HasAnchor α] (es : Array α) : Nat :=
   go 4
 where
-  go (numDigits : Nat) : Array (UInt64 × α) × Nat := Id.run do
+  go (numDigits : Nat) : Nat := Id.run do
     if 4*numDigits  < 64 then
       let shift := 64 - 4*numDigits
       let mut found : Std.HashSet UInt64 := {}
-      let mut result := #[]
-      for (a, e) in es do
+      for e in es do
+        let a := HasAnchor.getAnchor e
         let a' := a >>> shift.toUInt64
         if found.contains a' then
           return (← go (numDigits+1))
         else
           found  := found.insert a'
-          result := result.push (a', e)
-      return (result, numDigits)
+      return numDigits
     else
-      return (es, numDigits)
+      return numDigits
   termination_by 64 - 4*numDigits
 
+public structure ExprWithAnchor where
+  e      : Expr
+  anchor : UInt64
+
+public instance : HasAnchor ExprWithAnchor where
+  getAnchor e := e.anchor
+
+public def mkAnchorSyntaxFromPrefix (numDigits : Nat) (anchorPrefix : UInt64) : CoreM (TSyntax ``Parser.Tactic.Grind.anchor) := do
+  let hexnum := mkNode `hexnum #[mkAtom (anchorPrefixToString numDigits anchorPrefix)]
+  `(Parser.Tactic.Grind.anchor| #$hexnum)
+
+public def mkAnchorSyntax (numDigits : Nat) (anchor : UInt64) : CoreM (TSyntax ``Parser.Tactic.Grind.anchor) := do
+  let anchorPrefix := anchor >>> (64 - 4*numDigits.toUInt64)
+  mkAnchorSyntaxFromPrefix numDigits anchorPrefix
+
 end Lean.Meta.Grind

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

@@ -7,11 +7,11 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.SearchM
 public import Lean.Meta.Tactic.Grind.Action
+public import Lean.Meta.Tactic.Grind.Anchor
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.CasesMatch
 import Lean.Meta.Tactic.Grind.Internalize
-import Lean.Meta.Tactic.Grind.Anchor
 public section
 namespace Lean.Meta.Grind
 
@@ -242,9 +242,19 @@ private def casesWithTrace (mvarId : MVarId) (major : Expr) : GoalM (List MVarId
       saveCases declName false
   cases mvarId major
 
+structure SplitCandidateWithAnchor where
+  c        : SplitInfo
+  numCases : Nat
+  isRec    : Bool
+  e        : Expr
+  anchor   : UInt64
+
+instance : HasAnchor SplitCandidateWithAnchor where
+  getAnchor e := e.anchor
+
 structure SplitCandidateAnchors where
   /-- Pairs `(anchor, split)` -/
-  candidates : Array (UInt64 × Expr)
+  candidates : Array SplitCandidateWithAnchor
   /-- Number of digits (≥ 4) sufficient for distinguishing anchors. We usually display only the first `numDigits`. -/
   numDigits  : Nat
 
@@ -254,20 +264,22 @@ Applies additional `filter` if provided.
 -/
 def getSplitCandidateAnchors (filter : Expr → GoalM Bool := fun _ => return true) : GoalM SplitCandidateAnchors := do
   let candidates := (← get).split.candidates
-  let candidates ← candidates.toArray.mapM fun c => do
+  let candidates ← candidates.toArray.filterMapM fun c => do
     let e := c.getExpr
     let anchor ← getAnchor e
     let status ← checkSplitStatus c
-    return (e, status, anchor)
-  let candidates ← 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 e
+    match status with
+    | .resolved | .notReady => return none
+    | .ready numCases isRec _ =>
+      if (← filter e) then
+        return some { e, c, numCases, isRec, anchor }
+      else
+        return none
   -- **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) => (anchor, e)
-  let (candidates, numDigits) := truncateAnchors candidates
+  let numDigits := getNumDigitsForAnchors candidates
   return { candidates, numDigits }
 
 namespace Action
@@ -350,7 +362,7 @@ private def mkCasesResultSeq (cases : TSyntax `grind) (alts : Array (List (TSynt
 Performs a case-split using `c`.
 Remark: `numCases` and `isRec` are computed using `checkSplitStatus`.
 -/
-private def splitCore (c : SplitInfo) (numCases : Nat) (isRec : Bool)
+def splitCore (c : SplitInfo) (numCases : Nat) (isRec : Bool)
     (stopAtFirstFailure : Bool)
     (compress : Bool) : Action := fun goal _ kp => do
   let traceEnabled := (← getConfig).trace
@@ -402,9 +414,7 @@ private def splitCore (c : SplitInfo) (numCases : Nat) (isRec : Bool)
   if stuckNew.isEmpty then
     if traceEnabled then
       let anchor ← goal.withContext <| getAnchor cExpr
-      let anchorPrefix := anchor >>> (64 - 4*numDigits.toUInt64)
-      let hexnum := mkNode `hexnum #[mkAtom (anchorToString numDigits anchorPrefix)]
-      let cases ← `(grind| cases #$hexnum)
+      let cases ← `(grind| cases $(← mkAnchorSyntax numDigits anchor):anchor)
       return .closed (← mkCasesResultSeq cases seqNew compress)
     else
       return .closed []

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

@@ -1734,11 +1734,14 @@ where
       forEachDiseq parentSet (propagateDiseqOf solverId)
       go rest
 
-def anchorToString (numDigits : Nat) (anchor : UInt64) : String :=
-  let cs := Nat.toDigits 16 anchor.toNat
+def anchorPrefixToString (numDigits : Nat) (anchorPrefix : UInt64) : String :=
+  let cs := Nat.toDigits 16 anchorPrefix.toNat
   let n := cs.length
   let zs := List.replicate (numDigits - n) '0'
   let cs := zs ++ cs
   cs.asString
 
+def anchorToString (numDigits : Nat) (anchor : UInt64) : String :=
+  anchorPrefixToString numDigits (anchor >>> (64 - 4*numDigits.toUInt64))
+
 end Lean.Meta.Grind

tests/lean/run/grind_interactive.lean

@@ -179,7 +179,7 @@ trace: [splits] Case split candidates
 #guard_msgs (trace) in
 example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → False := by
   grind =>
-    show_splits
+    show_cases
     sorry
 
 /--
@@ -189,7 +189,7 @@ trace: [splits] Case split candidates
 -/
 example (r p q p₁ p₂ : Prop) : (p₁ → q) → p ∨ (q ∧ r) → p ∨ (p₁ ↔ p₂) → False := by
   grind =>
-    show_splits
+    show_cases
     sorry
 
 def h (as : List Nat) :=
@@ -213,13 +213,13 @@ trace: [splits] Case split candidates
 example : h bs = 1 → h as ≠ 0 := by
   grind [h.eq_def] =>
     instantiate
-    show_splits
+    show_cases
     sorry
 
 example : h bs = 1 → h as ≠ 0 := by
   grind [h.eq_def] =>
     instantiate
-    show_splits
+    show_cases
     cases #ec88
     instantiate
     focus instantiate
@@ -249,6 +249,40 @@ example : h bs = 1 → h as ≠ 0 := by
     cases #ec88
     all_goals instantiate
 
+/--
+info: Try these:
+  [apply] cases #7a08 for
+    ¬p ∨ ¬q
+  [apply] cases #8212 for
+    ¬p ∨ q
+  [apply] cases #fc16 for
+    p ∨ ¬q
+  [apply] cases #4283 for
+    p ∨ q
+  [apply] cases #0457 for
+    p ∨ r
+-/
+#guard_msgs in
+example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → False := by
+  grind =>
+    cases?
+    sorry
+
+/--
+info: Try these:
+  [apply] cases #7a08 for
+    ¬p ∨ ¬q
+  [apply] cases #8212 for
+    ¬p ∨ q
+  [apply] cases #fc16 for
+    p ∨ ¬q
+-/
+#guard_msgs in
+example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → False := by
+  grind =>
+    cases? p && Not
+    sorry
+
 example : h bs = 1 → h as ≠ 0 := by
   grind [h.eq_def] =>
     instantiate
@@ -411,12 +445,12 @@ trace: [thms] Local theorems
 #guard_msgs in
 example : (∀ x, q x) → (∀ x, p x → p (f x)) → p x → p (f (f x)) := by
   grind =>
-    show_thms
+    show_local_thms
     instantiate #bfb8
 
 example : (∀ x, q x) → (∀ x, p x → p (f x)) → p x → p (f (f x)) := by
   grind =>
-    show_thms
+    show_local_thms
     instantiate #bfb8
 
 /-- error: no local theorems -/
@@ -461,9 +495,9 @@ example : (a : Point Nat) → p a → x ≠ y → False := by
   grind =>
     cases #6ccb
     instantiate pax
-    show_splits
+    show_cases
     rename_i y w _ -- Must reset cached anchors
-    show_splits
+    show_cases
     cases #e2a6
     all_goals sorry
 
@@ -472,9 +506,9 @@ example : (a : Point Nat) → p a → x ≠ y → False := by
   grind =>
     cases #6ccb
     instantiate pax
-    show_splits
+    show_cases
     next y w _ =>
-    show_splits
+    show_cases
     cases #e2a6
     all_goals sorry