feat: track set of added case-splits

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

@@ -50,11 +50,6 @@ private def updateAppMap (e : Expr) : GoalM Unit := do
       s.appMap.insert key [e]
   }
 
-/-- Inserts `e` into the list of case-split candidates. -/
-private def addSplitCandidate (e : Expr) : GoalM Unit := do
-  trace_goal[grind.split.candidate] "{e}"
-  modify fun s => { s with split.candidates := e :: s.split.candidates }
-
 private def forbiddenSplitTypes := [``Eq, ``HEq, ``True, ``False]
 
 /-- Returns `true` if `e` is of the form `@Eq Prop a b` -/

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

@@ -44,6 +44,8 @@ private def mkCandidateKey (a b : Expr) : Expr × Expr :=
 /-- Model-based theory combination. -/
 def mbtc (ctx : MBTC.Context) : GoalM Bool := do
   unless (← getConfig).mbtc do return false
+  -- It is pointless to run `mbtc` if maximum number of splits has been reached.
+  if (← checkMaxCaseSplit) then return false
   let mut map : Map := {}
   let mut candidates : Candidates := {}
   for ({ expr := e }, _) in (← get).enodes do
@@ -77,13 +79,19 @@ def mbtc (ctx : MBTC.Context) : GoalM Bool := do
       b₁.lt b₂
     else
       a₁.lt a₂
-  let eqs ← result.mapM fun (a, b) => do
+  let eqs ← result.filterMapM fun (a, b) => do
     let eq ← mkEq a b
     trace[grind.mbtc] "{eq}"
     let eq ← shareCommon (← canon eq)
-    internalize eq (Nat.max (← getGeneration a) (← getGeneration b))
-    return eq
-  modify fun s => { s with split.candidates := s.split.candidates ++ eqs.toList }
+    if (← isKnownCaseSplit eq) then
+      return none
+    else
+      internalize eq (Nat.max (← getGeneration a) (← getGeneration b))
+      return some eq
+  if eqs.isEmpty then
+    return false
+  for eq in eqs do
+    addSplitCandidate eq
   return true
 
 def mbtcTac (ctx : MBTC.Context) : GrindTactic := fun goal => do

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

@@ -480,6 +480,8 @@ structure Split.State where
   candidates : List Expr := []
   /-- Number of splits performed to get to this goal. -/
   num        : Nat := 0
+  /-- Case-splits that have been inserted at `candidates` at some point. -/
+  added      : PHashSet ENodeKey := {}
   /-- Case-splits that have already been performed, or that do not have to be performed anymore. -/
   resolved   : PHashSet ENodeKey := {}
   /--
@@ -1160,6 +1162,14 @@ partial def Goal.getEqcs (goal : Goal) : List (List Expr) := Id.run do
 def getEqcs : GoalM (List (List Expr)) :=
   return (← get).getEqcs
 
+/--
+Returns `true` if `e` has been already added to the case-split list at one point.
+Remark: this function returns `true` even if the split has already been resolved
+and is not in the list anymore.
+-/
+def isKnownCaseSplit (e : Expr) : GoalM Bool :=
+  return (← get).split.added.contains { expr := e }
+
 /-- Returns `true` if `e` is a case-split that does not need to be performed anymore. -/
 def isResolvedCaseSplit (e : Expr) : GoalM Bool :=
   return (← get).split.resolved.contains { expr := e }
@@ -1174,6 +1184,15 @@ def markCaseSplitAsResolved (e : Expr) : GoalM Unit := do
     trace_goal[grind.split.resolved] "{e}"
     modify fun s => { s with split.resolved := s.split.resolved.insert { expr := e } }
 
+/-- Inserts `e` into the list of case-split candidates if it was not inserted before. -/
+def addSplitCandidate (e : Expr) : GoalM Unit := do
+  unless (← isKnownCaseSplit e) do
+    trace_goal[grind.split.candidate] "{e}"
+    modify fun s => { s with
+      split.added := s.split.added.insert { expr := e }
+      split.candidates := e :: s.split.candidates
+    }
+
 /--
 Returns extensionality theorems for the given type if available.
 If `Config.ext` is `false`, the result is `#[]`.