From 3396ac91c5a43d840e2a66e58880aec36d2f88ca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 8 Jan 2025 12:00:46 -0800
Subject: [PATCH] feat: add `grind` configuration options to control
 case-splitting

This PR adds the following configuration options to `Grind.Config`:
`splitIte`, `splitMatch`, and `splitIndPred`.
---
 src/Init/Grind/Tactics.lean                 |  8 ++++++
 src/Lean/Meta/Tactic/Grind/Internalize.lean | 27 ++++++++++++---------
 tests/lean/run/grind_match2.lean            |  5 ++++
 tests/lean/run/grind_split.lean             |  8 ++++++
 4 files changed, 36 insertions(+), 12 deletions(-)

diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index f4678adfc68..951d3e2c0c7 100644
--- a/src/Init/Grind/Tactics.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index e6f76fe7d9d..980aca39772 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/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.
diff --git a/tests/lean/run/grind_match2.lean b/tests/lean/run/grind_match2.lean
index 24160dd1954..410e5c8819f 100644
--- a/tests/lean/run/grind_match2.lean
+++ b/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
diff --git a/tests/lean/run/grind_split.lean b/tests/lean/run/grind_split.lean
index 7acf78263d5..edf944cfae7 100644
--- a/tests/lean/run/grind_split.lean
+++ b/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