feat: add grind configuration options to control case-splitting (#6581)

This PR adds the following configuration options to `Grind.Config`:
`splitIte`, `splitMatch`, and `splitIndPred`.

src/Init/Grind/Tactics.lean

@@ -37,6 +37,14 @@ structure Config where
   instances : Nat := 1000
   /-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
   matchEqs : Bool := true
+  /-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search. -/
+  splitMatch : Bool := true
+  /-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search. -/
+  splitIte : Bool := true
+  /--
+  If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
+  Otherwise, it performs case-splitting only on types marked with `[grind_split]` attribute. -/
+  splitIndPred : Bool := true
   deriving Inhabited, BEq
 
 end Lean.Grind

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

@@ -56,22 +56,25 @@ private def forbiddenSplitTypes := [``Eq, ``HEq, ``True, ``False]
 /-- Inserts `e` into the list of case-split candidates if applicable. -/
 private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
   unless e.isApp do return ()
-  if e.isIte || e.isDIte then
+  if (← getConfig).splitIte && (e.isIte || e.isDIte) then
     addSplitCandidate e
-  else if (← isMatcherApp e) then
-    if let .reduced _ ← reduceMatcher? e then
-      -- When instantiating `match`-equations, we add `match`-applications that can be reduced,
-      -- and consequently don't need to be splitted.
-      return ()
-    else
-      addSplitCandidate e
-  else
-    let .const declName _  := e.getAppFn | return ()
+    return ()
+  if (← getConfig).splitMatch then
+    if (← isMatcherApp e) then
+      if let .reduced _ ← reduceMatcher? e then
+        -- When instantiating `match`-equations, we add `match`-applications that can be reduced,
+        -- and consequently don't need to be splitted.
+        return ()
+      else
+        addSplitCandidate e
+        return ()
+  let .const declName _  := e.getAppFn | return ()
     if forbiddenSplitTypes.contains declName then return ()
     -- We should have a mechanism for letting users to select types to case-split.
     -- Right now, we just consider inductive predicates that are not in the forbidden list
-    if (← isInductivePredicate declName) then
-      addSplitCandidate e
+    if (← getConfig).splitIndPred then
+      if (← isInductivePredicate declName) then
+        addSplitCandidate e
 
 /--
 If `e` is a `cast`-like term (e.g., `cast h a`), add `HEq e a` to the to-do list.

tests/lean/run/grind_match2.lean

@@ -26,3 +26,8 @@ set_option trace.grind true in
 example : h as ≠ 0 := by
   unfold h
   grind
+
+example : h as ≠ 0 := by
+  unfold h
+  fail_if_success grind (splitMatch := false)
+  sorry

tests/lean/run/grind_split.lean

@@ -28,6 +28,10 @@ set_option trace.grind true in
 example (p : Prop) [Decidable p] (a b c : Nat) : (if p then a else b) = c → R a → R b → R c := by
   grind
 
+example (p : Prop) [Decidable p] (a b c : Nat) : (if p then a else b) = c → R a → R b → R c := by
+  fail_if_success grind (splitIte := false)
+  sorry
+
 namespace grind_test_induct_pred
 
 inductive Expr where
@@ -52,4 +56,8 @@ set_option trace.grind true
 theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
   grind
 
+theorem HasType.det' (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
+  fail_if_success grind (splitIndPred := false)
+  sorry
+
 end grind_test_induct_pred