chore: improve grind case-split trace

src/Init/Grind/Util.lean

@@ -59,4 +59,11 @@ def eqMatchUnexpander : PrettyPrinter.Unexpander := fun stx => do
   | `($_ $lhs:term $rhs:term) => `($lhs = $rhs)
   | _ => throw ()
 
+@[app_unexpander offset]
+def offsetUnexpander : PrettyPrinter.Unexpander := fun stx => do
+  match stx with
+  | `($_ $lhs:term $rhs:term) => `($lhs + $rhs)
+  | _ => throw ()
+
+
 end Lean.Grind

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

@@ -293,17 +293,25 @@ partial def ppPattern (pattern : Expr) : MessageData := Id.run do
   if let some e := groundPattern? pattern then
     return m!"`[{e}]"
   else if isPatternDontCare pattern then
-    return m!"?"
+    return m!"_"
   else match pattern with
     | .bvar idx => return m!"#{idx}"
     | _ =>
-      let mut r := m!"{pattern.getAppFn}"
-      for arg in pattern.getAppArgs do
-        let mut argFmt ← ppPattern arg
-        if !isAtomicPattern arg then
-          argFmt := MessageData.paren argFmt
-        r := r ++ " " ++ argFmt
-      return r
+      if pattern.isAppOfArity ``Grind.offset 2 then
+        let lhs := ppArg <| pattern.getArg! 0
+        let rhs := ppPattern <| pattern.getArg! 1
+        return m!"{lhs} + {rhs}"
+      else
+        let mut r := m!"{pattern.getAppFn}"
+        for arg in pattern.getAppArgs do
+          r := r ++ " " ++ ppArg arg
+        return r
+where
+  ppArg (arg : Expr) : MessageData :=
+    if isAtomicPattern arg then
+      ppPattern arg
+    else
+      .paren (ppPattern arg)
 
 namespace NormalizePattern
 

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

@@ -146,8 +146,8 @@ 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}" #[]
+    for { expr, i , num } in goal.casesTrace.reverse do
+      msgs := msgs.push <| .trace { cls := `cases } m!"[{i+1}/{num}]: {expr}" #[]
     pushMsg <| .trace { cls := `cases } "Case analyses" msgs
 
 def goalToMessageData (goal : Goal) (config : Grind.Config) : MetaM MessageData := goal.mvarId.withContext do

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

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

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

@@ -434,6 +434,13 @@ structure Canon.State where
   proofCanon : PHashMap Expr Expr := {}
   deriving Inhabited
 
+/-- Trace information for a case split. -/
+structure CaseTrace where
+  expr : Expr
+  i    : Nat
+  num  : Nat
+  deriving Inhabited
+
 structure Goal where
   mvarId       : MVarId
   canon        : Canon.State := {}
@@ -494,7 +501,7 @@ structure Goal where
   Remark: `casesTrace.length ≥ numSplits` because we don't increase the counter for `cases`
   applications that generated only 1 subgoal.
   -/
-  casesTrace : List (Expr × Nat) := []
+  casesTrace : List CaseTrace := []
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=

tests/lean/grind_guide.lean.expected.out

@@ -30,7 +30,7 @@ x✝ :
         0}
   [ematch] E-matching patterns
     [thm] _example.match_1.eq_1: [_example.match_1 #2 `[0] #1 #0]
-    [thm] _example.match_1.eq_2: [_example.match_1 #3 (Lean.Grind.offset #2 (1)) #1 #0]
+    [thm] _example.match_1.eq_2: [_example.match_1 #3 (#2 + 1) #1 #0]
   [limits] Thresholds reached
     [limit] maximum number of case-splits has been reached, threshold: `(splits := 0)`
 grind_guide.lean:68:2-68:7: error: `grind` failed
@@ -73,12 +73,12 @@ h : x = 0
         1}
     [eqc] {x, 0}
   [cases] Case analyses
-    [cases] [2]: match x with
+    [cases] [1/2]: match x with
         | 0 => 1
         | n.succ => 2
   [ematch] E-matching patterns
     [thm] _example.match_1.eq_1: [_example.match_1 #2 `[0] #1 #0]
-    [thm] _example.match_1.eq_2: [_example.match_1 #3 (Lean.Grind.offset #2 (1)) #1 #0]
+    [thm] _example.match_1.eq_2: [_example.match_1 #3 (#2 + 1) #1 #0]
   [offset] Assignment satisfying offset contraints
     [assign] match x with
         | 0 => 1

tests/lean/run/grind_ctor_ematch.lean

@@ -36,7 +36,7 @@ x✝ : ¬Even 16
   [eqc] False propositions
     [prop] Even 16
   [ematch] E-matching patterns
-    [thm] Even.plus_two: [Even (Lean.Grind.offset #1 (2))]
+    [thm] Even.plus_two: [Even (#1 + 2)]
     [thm] Even.zero: [Even `[0]]
   [limits] Thresholds reached
     [limit] maximum number of E-matching rounds has been reached, threshold: `(ematch := 5)`

tests/lean/run/grind_ematch_patterns.lean

@@ -4,7 +4,7 @@ def replicate : (n : Nat) → (a : α) → List α
 
 /--
 info: [grind.ematch.pattern] replicate.eq_1: [@replicate #1 `[0] #0]
-[grind.ematch.pattern] replicate.eq_2: [@replicate #2 (Lean.Grind.offset #0 (1)) #1]
+[grind.ematch.pattern] replicate.eq_2: [@replicate #2 (#0 + 1) #1]
 -/
 #guard_msgs (info) in
 set_option trace.grind.ematch.pattern true in

tests/lean/run/grind_eq_pattern.lean

@@ -1,21 +1,19 @@
 %reset_grind_attrs
 
 /--
-info: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppend ? ? ? ? #2 #0]
+info: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppend _ _ _ _ #2 #0]
 -/
 #guard_msgs (info) in
 set_option trace.grind.ematch.pattern true in
 attribute [grind] List.append_ne_nil_of_left_ne_nil
 
 /--
-info: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend ? ? ? ? #1 #2]
+info: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend _ _ _ _ #1 #2]
 -/
 #guard_msgs (info) in
 set_option trace.grind.ematch.pattern true in
 attribute [grind] List.append_ne_nil_of_right_ne_nil
-/--
-info: [grind.ematch.pattern] List.getLast?_eq_some_iff: [@List.getLast? #2 #1, @some ? #0]
--/
+/-- info: [grind.ematch.pattern] List.getLast?_eq_some_iff: [@List.getLast? #2 #1, @some _ #0] -/
 #guard_msgs (info) in
 set_option trace.grind.ematch.pattern true in
 attribute [grind =] List.getLast?_eq_some_iff

tests/lean/run/grind_offset.lean

@@ -9,9 +9,7 @@ set_option trace.grind.ematch.pattern true
 set_option trace.grind.ematch.instance true
 set_option trace.grind.assert true
 
-/--
-info: [grind.ematch.pattern] f.eq_2: [f (Lean.Grind.offset #0 (1))]
--/
+/-- info: [grind.ematch.pattern] f.eq_2: [f (#0 + 1)] -/
 #guard_msgs in
 grind_pattern f.eq_2 => f (x + 1)
 
@@ -66,9 +64,7 @@ example : f (c + 2) = a → a = g (g (f c)) := by
   | 1 => 10
   | a+2 => g (foo a)
 
-/--
-info: [grind.ematch.pattern] foo.eq_3: [foo (Lean.Grind.offset #0 (2))]
--/
+/-- info: [grind.ematch.pattern] foo.eq_3: [foo (#0 + 2)] -/
 #guard_msgs in
 grind_pattern foo.eq_3 => foo (a_2 + 2)
 

tests/lean/run/grind_pattern1.lean

@@ -1,18 +1,20 @@
 set_option trace.grind.ematch.pattern true
 
 /--
-info: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem ? `[Nat] #4 ? ? (@Array.push ? #3 #2) #1 ?]
+info: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem _ `[Nat] #4 _ _ (@Array.push _ #3 #2) #1 _]
 -/
 #guard_msgs in
 grind_pattern Array.getElem_push_lt => (a.push x)[i]
 
 
-/-- info: [grind.ematch.pattern] List.getElem_attach: [@getElem ? `[Nat] ? ? ? (@List.attach #3 #2) #1 ?] -/
+/--
+info: [grind.ematch.pattern] List.getElem_attach: [@getElem _ `[Nat] _ _ _ (@List.attach #3 #2) #1 _]
+-/
 #guard_msgs in
 grind_pattern List.getElem_attach => xs.attach[i]
 
 /--
-info: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 ? ? (@HAppend.hAppend ? ? ? ? #1 (@List.cons ? #0 (@List.nil ?))) #0]
+info: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 _ _ (@HAppend.hAppend _ _ _ _ #1 (@List.cons _ #0 (@List.nil _))) #0]
 -/
 #guard_msgs in
 grind_pattern List.mem_concat_self => a ∈ xs ++ [a]
@@ -52,13 +54,13 @@ instance [Boo α β] : Boo (List α) (Array β) where
 
 theorem fEq [Foo α β] [Boo α β] (a : List α) : (f a).1 = a := rfl
 
-/-- info: [grind.ematch.pattern] fEq: [@f ? ? ? ? #0] -/
+/-- info: [grind.ematch.pattern] fEq: [@f _ _ _ _ #0] -/
 #guard_msgs in
 grind_pattern fEq => f a
 
 theorem fEq2 [Foo α β] [Boo α β] (a : List α) (_h : a.length > 5) : (f a).1 = a := rfl
 
-/-- info: [grind.ematch.pattern] fEq2: [@f ? ? ? ? #1] -/
+/-- info: [grind.ematch.pattern] fEq2: [@f _ _ _ _ #1] -/
 #guard_msgs in
 grind_pattern fEq2 => f a
 
@@ -69,12 +71,12 @@ theorem gEq [Boo α β] (a : List α) : (g (β := Array β) a).1 = a := rfl
 
 /--
 error: invalid pattern(s) for `gEq`
-  [@g ? ? ? #0]
+  [@g _ _ _ #0]
 the following theorem parameters cannot be instantiated:
   β : Type
   inst✝ : Boo α β
 ---
-info: [grind.ematch.pattern] gEq: [@g ? ? ? #0]
+info: [grind.ematch.pattern] gEq: [@g _ _ _ #0]
 -/
 #guard_msgs in
 grind_pattern gEq => g a

tests/lean/run/grind_pattern2.lean

@@ -16,9 +16,7 @@ grind_pattern contains_insert => contains (insertElem s a) a
 set_option trace.grind.ematch true
 set_option trace.grind.ematch.pattern true
 
-/--
-info: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem ? #2 #1 #0) #0]
--/
+/-- info: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] -/
 #guard_msgs (info) in
 example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
         s₂ = insertElem s₁ a₁ → a₁ = a₂ → contains s₂ a₂ := by
@@ -26,7 +24,7 @@ example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
 
 /--
 info: [grind.ematch] reinsert `contains_insert`
-[grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem ? #2 #1 #0) #0]
+[grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0]
 -/
 #guard_msgs (info) in
 example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
@@ -67,7 +65,7 @@ theorem arrEx [Add α] (as : Array α) (h₁ : i < as.size) (h₂ : i = j) : as[
 
 
 /--
-info: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 ? ? ? (@getElem ? `[Nat] ? ? ? #2 #5 ?) (@getElem ? `[Nat] ? ? ? #2 #4 ?)]
+info: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 _ _ _ (@getElem _ `[Nat] _ _ _ #2 #5 _) (@getElem _ `[Nat] _ _ _ #2 #4 _)]
 -/
 #guard_msgs in
 grind_pattern arrEx => as[i]+as[j]'(h₂▸h₁)

tests/lean/run/grind_pattern_proj.lean

@@ -35,13 +35,13 @@ structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.
 set_option trace.grind.ematch.pattern true
 
 /--
-info: [grind.ematch.pattern] Functor.map_id: [@Prefunctor.map #5 ? #3 ? (@Functor.toPrefunctor ? #4 ? #2 #1) #0 #0 (@CategoryStruct.id ? ? #0)]
+info: [grind.ematch.pattern] Functor.map_id: [@Prefunctor.map #5 _ #3 _ (@Functor.toPrefunctor _ #4 _ #2 #1) #0 #0 (@CategoryStruct.id _ _ #0)]
 -/
 #guard_msgs in
 grind_pattern Functor.map_id => self.map (𝟙 X)
 
 /--
-info: [grind.ematch.pattern] Functor.map_comp: [@Prefunctor.map #9 ? #7 ? (@Functor.toPrefunctor ? #8 ? #6 #5) #4 #2 (@CategoryStruct.comp ? ? #4 #3 #2 #1 #0)]
+info: [grind.ematch.pattern] Functor.map_comp: [@Prefunctor.map #9 _ #7 _ (@Functor.toPrefunctor _ #8 _ #6 #5) #4 #2 (@CategoryStruct.comp _ _ #4 #3 #2 #1 #0)]
 -/
 #guard_msgs in
 grind_pattern Functor.map_comp => self.map (f ≫ g)

tests/lean/run/grind_pre.lean

@@ -180,8 +180,8 @@ h : ¬r
     [prop] q
     [prop] r
   [cases] Case analyses
-    [cases] [1]: p = r
-    [cases] [2]: ¬r ∨ p
+    [cases] [1/1]: p = r
+    [cases] [1/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

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