refactor: simplify tactics

Author: leodemoura

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

@@ -474,7 +474,7 @@ end EMatch
 open EMatch
 
 /-- Performs one round of E-matching, and returns new instances. -/
-def ematch : GoalM Unit := do
+private def ematchCore : GoalM Unit := do
   let go (thms newThms : PArray EMatchTheorem) : EMatch.M Unit := do
     withReader (fun ctx => { ctx with useMT := true }) <| ematchTheorems thms
     withReader (fun ctx => { ctx with useMT := false }) <| ematchTheorems newThms
@@ -489,12 +489,13 @@ def ematch : GoalM Unit := do
       ematch.num       := s.ematch.num + 1
     }
 
-/-- Performs one round of E-matching, and assert new instances. -/
-def ematchAndAssert : GrindTactic := fun goal => do
+/-- Performs one round of E-matching. -/
+def ematch : GrindTactic := fun goal => do
   let numInstances := goal.ematch.numInstances
-  let goal ← GoalM.run' goal ematch
+  let goal ← GoalM.run' goal ematchCore
   if goal.ematch.numInstances == numInstances then
     return none
-  assertAll goal
+  else
+    return [goal]
 
 end Lean.Meta.Grind

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

@@ -263,7 +263,10 @@ def assertNext : GrindTactic := fun goal => do
   assertAt fact.proof fact.prop fact.generation { goal with newRawFacts }
 
 /-- Asserts all facts in the `goal` fact queue. -/
-partial def assertAll : GrindTactic :=
-  assertNext.iterate
+partial def assertAll : GrindTactic := fun goal =>
+  if goal.newRawFacts.isEmpty then
+    return none
+  else
+    assertNext.iterate goal
 
 end Lean.Meta.Grind

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

@@ -24,13 +24,13 @@ where
   loop (goal : Goal) : GrindM Bool := withIncRecDepth do
     if goal.inconsistent then
       return true
-    else if let some goals ← assertNext goal then
+    else if let some goals ← assertAll goal then
       cont goals
     else if let some goals ← Arith.check goal then
       cont goals
     else if let some goals ← splitNext goal then
       cont goals
-    else if let some goals ← ematchAndAssert goal then
+    else if let some goals ← ematch goal then
       cont goals
     else
       return false

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

@@ -52,18 +52,24 @@ def applyTac (x : GrindTactic) (goal : Goal) : M Bool := do
     return true
   stepGuard go goal
 
-def tryAssertNext : Goal → M Bool := applyTac assertNext
+-- TODO: it should be assertAll. It may produce multiple goals because of eager splitting.
+def tryAssertAll : Goal → M Bool := applyTac assertAll
 
-def tryEmatch : Goal → M Bool := applyTac ematchAndAssert
-
-def trySplit : Goal → M Bool := applyTac splitNext
+-- TODO: it doesn't need to invoke assertAll
+def tryEmatch : Goal → M Bool := applyTac ematch
 
+-- Can only fail or produce a new updated goal
 def tryArith : Goal → M Bool := applyTac Arith.check
 
+-- Can only fail or produce a new updated goal
 def tryLookahead : Goal → M Bool := applyTac lookahead
 
+-- Can only fail or produce a new updated goal
 def tryMBTC : Goal → M Bool := applyTac Arith.Cutsat.mbtcTac
 
+-- May fail or produce multiple new goals
+def trySplit : Goal → M Bool := applyTac splitNext
+
 partial def main (fallback : Fallback) : M Unit := do
   repeat do
     if (← get).failure?.isSome then
@@ -72,7 +78,7 @@ partial def main (fallback : Fallback) : M Unit := do
       return ()
     if goal.inconsistent then
       continue
-    if (← tryAssertNext goal) then
+    if (← tryAssertAll goal) then
       continue
     if (← tryArith goal) then
       continue