feat: cdot tactic in grind iteractive mode

Author: leodemoura

src/Init/Grind/Interactive.lean

@@ -162,6 +162,12 @@ inaccessible names to the given names.
 -/
 syntax (name := next) "next " binderIdent* " => " grindSeq : grind
 
+/--
+`· grindSeq` focuses on the main `grind` goal and tries to solve it using the given
+sequence of `grind` tactics.
+-/
+macro dot:patternIgnore("· " <|> ". ") s:grindSeq : grind => `(grind| next%$dot =>%$dot $s:grindSeq )
+
 /--
 `any_goals tac` applies the tactic `tac` to every goal,
 concatenating the resulting goals for successful tactic applications.

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

@@ -159,17 +159,16 @@ def mkGrindSeq (s : List TGrind) : TSyntax ``Parser.Tactic.Grind.grindSeq :=
 /--
 Given `[t₁, ..., tₙ]`, returns
 ```
-next =>
-  t₁
+· t₁
   ...
   tₙ
 ```
-If the list is empty, it returns `next => done`.
+If the list is empty, it returns `· done`.
 -/
 def mkGrindNext (s : List TGrind) : CoreM TGrind := do
   let s ← if s == [] then pure [← `(grind| done)] else pure s
   let s := mkGrindSeq s
-  `(grind| next => $s:grindSeq)
+  `(grind| · $s:grindSeq)
 
 /--
 Given `[t₁, ..., tₙ]`, returns
@@ -189,8 +188,7 @@ private def mkGrindParen (s : List TGrind) : CoreM TGrind := do
 If tracing is enabled and continuation produced `.closed [t₁, ..., tₙ]`,
 returns the singleton sequence `[t]` where `t` is
 ```
-next =>
-  t₁
+· t₁
   ...
   tₙ
 ```
@@ -205,7 +203,7 @@ def group : Action := fun goal _ kp => do
     return r
 
 /--
-If tracing is enabled and continuation produced `.closed [(next => t₁; ...; tₙ)]`,
+If tracing is enabled and continuation produced `.closed [(next => t₁; ...; tₙ)]` or its variant using `·`
 returns `.close [t₁, ... tₙ]`
 -/
 def ungroup : Action := fun goal _ kp => do
@@ -214,7 +212,9 @@ def ungroup : Action := fun goal _ kp => do
     match r with
     | .closed [tac] =>
       match tac with
-      | `(grind| next => $seq;*) => return .closed <| seq.getElems.toList.map TGrindStep.getTactic
+      | `(grind| next => $seq;*)
+      | `(grind| · $seq;*) =>
+        return .closed <| seq.getElems.toList.map TGrindStep.getTactic
       | _ => return r
     | _ => return r
   else

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

@@ -322,6 +322,7 @@ where
 private def isCompressibleSeq (seq : List (TSyntax `grind)) : Bool :=
   seq.all fun tac => match tac with
     | `(grind| next $_* => $_:grindSeq) => false
+    | `(grind| · $_:grindSeq) => false
     | _ => true
 
 /--

tests/lean/run/grind_finish_trace.lean

@@ -17,8 +17,8 @@ example {α : Type} [CommRing α] (a b c d e : α) :
 info: Try this:
   [apply] ⏎
     cases #b0f4
-    next => cases #50fc
-    next => cases #50fc <;> lia
+    · cases #50fc
+    · cases #50fc <;> lia
 -/
 #guard_msgs in
 example (p : Nat → Prop) (x y z w : Int) :
@@ -65,14 +65,12 @@ set_option warn.sorry false
 info: Try this:
   [apply] ⏎
     cases #c4b6
-    next =>
-      cases #8c9f
-      next => ring
-      next => sorry
-    next =>
-      cases #8c9f
-      next => ring
-      next => sorry
+    · cases #8c9f
+      · ring
+      · sorry
+    · cases #8c9f
+      · ring
+      · sorry
 -/
 #guard_msgs in
 example {α : Type} [CommRing α] (a b c d e : α) :
@@ -86,8 +84,8 @@ info: Try this:
   [apply] ⏎
     instantiate only [= Nat.min_def]
     cases #7640
-    next => sorry
-    next => lia
+    · sorry
+    · lia
 -/
 #guard_msgs in
 example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)

tests/lean/run/grind_indexmap_trace.lean

@@ -149,25 +149,18 @@ info: Try this:
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
     cases #4ed2
-    next =>
-      cases #ffdf
-      next => instantiate only
-      next =>
-        instantiate only
+    · cases #ffdf
+      · instantiate only
+      · instantiate only
         instantiate only [= HashMap.contains_insert]
-    next =>
-      cases #95a0
-      next =>
-        cases #2688
-        next => instantiate only
-        next =>
-          instantiate only
+    · cases #95a0
+      · cases #2688
+        · instantiate only
+        · instantiate only
           instantiate only [= HashMap.contains_insert]
-      next =>
-        cases #ffdf
-        next => instantiate only
-        next =>
-          instantiate only
+      · cases #ffdf
+        · instantiate only
+        · instantiate only
           instantiate only [= HashMap.contains_insert]
 -/
 #guard_msgs in
@@ -181,25 +174,18 @@ info: Try this:
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
     cases #4ed2
-    next =>
-      cases #ffdf
-      next => instantiate only
-      next =>
-        instantiate only
+    · cases #ffdf
+      · instantiate only
+      · instantiate only
         instantiate only [= HashMap.contains_insert]
-    next =>
-      cases #95a0
-      next =>
-        cases #2688
-        next => instantiate only
-        next =>
-          instantiate only
+    · cases #95a0
+      · cases #2688
+        · instantiate only
+        · instantiate only
           instantiate only [= HashMap.contains_insert]
-      next =>
-        cases #ffdf
-        next => instantiate only
-        next =>
-          instantiate only
+      · cases #ffdf
+        · instantiate only
+        · instantiate only
           instantiate only [= HashMap.contains_insert]
 -/
 #guard_msgs in
@@ -240,25 +226,19 @@ info: Try this:
     instantiate only [= mem_indices_of_mem, insert, = getElem_def]
     instantiate only [= getElem?_neg, = getElem?_pos]
     cases #f590
-    next =>
-      cases #ffdf
-      next =>
-        instantiate only
+    · cases #ffdf
+      · instantiate only
         instantiate only [= Array.getElem_set]
-      next =>
-        instantiate only
+      · instantiate only
         instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
-    next =>
-      instantiate only [= mem_indices_of_mem, = getElem_def]
+    · instantiate only [= mem_indices_of_mem, = getElem_def]
       instantiate only [usr getElem_indices_lt]
       instantiate only [size]
       cases #ffdf
-      next =>
-        instantiate only [=_ WF]
+      · instantiate only [=_ WF]
         instantiate only [= getElem?_neg, = getElem?_pos, = Array.getElem_set]
         instantiate only [WF']
-      next =>
-        instantiate only
+      · instantiate only
         instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
 -/
 #guard_msgs in
@@ -300,9 +280,8 @@ info: Try this:
     instantiate only [findIdx, insert, = mem_indices_of_mem]
     instantiate only [= getElem?_neg, = getElem?_pos]
     cases #1bba
-    next => instantiate only [findIdx]
-    next =>
-      instantiate only
+    · instantiate only [findIdx]
+    · instantiate only
       instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
 -/
 #guard_msgs in