feat: include Case analyses trace in the grind error message (#6881)

This PR improves the `grind` error message by including a trace of the
terms on which `grind` applied `cases`-like operations.

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

@@ -108,7 +108,7 @@ private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
   let m := m!"{← thm.origin.pp}: {thm.patterns.map ppPattern}"
   return .trace { cls := `thm } m #[]
 
-private def ppActiveTheorems : M Unit := do
+private def ppActiveTheoremPatterns : M Unit := do
   let goal ← read
   let m ← goal.thms.toArray.mapM fun thm => ppEMatchTheorem thm
   let m := m ++ (← goal.newThms.toArray.mapM fun thm => ppEMatchTheorem thm)
@@ -142,6 +142,14 @@ private def ppThresholds (c : Grind.Config) : M Unit := do
   unless msgs.isEmpty do
     pushMsg <| .trace { cls := `limits } "Thresholds reached" msgs
 
+private def ppCasesTrace : M Unit := do
+  let goal ← read
+  unless goal.casesTrace.isEmpty do
+    let mut msgs := #[]
+    for (e, num) in goal.casesTrace.reverse do
+      msgs := msgs.push <| .trace { cls := `cases } m!"[{num}]: {e}" #[]
+    pushMsg <| .trace { cls := `cases } "Case analyses" msgs
+
 def goalToMessageData (goal : Goal) (config : Grind.Config) : MetaM MessageData := goal.mvarId.withContext do
   let (_, m) ← go goal |>.run #[]
   let gm := MessageData.trace { cls := `grind, collapsed := false } "Diagnostics" m
@@ -151,7 +159,8 @@ where
   go : M Unit := do
     pushMsg <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop
     ppEqcs
-    ppActiveTheorems
+    ppCasesTrace
+    ppActiveTheoremPatterns
     ppOffset
     ppThresholds config
 

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

@@ -195,7 +195,8 @@ def splitNext : GrindTactic := fun goal => do
           saveCases declName false
       cases (← get).mvarId major
     let goal ← get
-    let goals := mvarIds.map fun mvarId => { goal with mvarId }
+    let numSubgoals := mvarIds.length
+    let goals := mvarIds.map fun mvarId => { goal with mvarId, casesTrace := (c, numSubgoals) :: goal.casesTrace }
     let goals ← introNewHyp goals [] genNew
     return some goals
   return goals?

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

@@ -480,6 +480,12 @@ structure Goal where
   facts      : PArray Expr := {}
   /-- Cached extensionality theorems for types. -/
   extThms    : PHashMap ENodeKey (Array Ext.ExtTheorem) := {}
+  /--
+  Sequence of cases steps that generated this goal. We only use this information for diagnostics.
+  Remark: `casesTrace.length ≥ numSplits` because we don't increase the counter for `cases`
+  applications that generated only 1 subgoal.
+  -/
+  casesTrace : List (Expr × Nat) := []
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=

tests/lean/run/grind_pre.lean

@@ -179,6 +179,9 @@ h : ¬r
     [prop] p
     [prop] q
     [prop] r
+  [cases] Case analyses
+    [cases] [1]: p = r
+    [cases] [2]: ¬r ∨ p
 [grind] Issues
   [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
 -/

tests/lean/run/grind_split_issue.lean

@@ -22,6 +22,8 @@ h : HEq ⋯ ⋯
     [prop] X c s
   [eqc] Equivalence classes
     [eqc] {s, 0}
+  [cases] Case analyses
+    [cases] [2]: X c 0
 [grind] Issues
   [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
 -/