From 541902564ba2f9bfbdd62e599d71847ffdb7398a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 12 Jan 2025 07:40:36 -0800
Subject: [PATCH] feat: improve case split heuristic used in `grind` (#6613)

This PR improves the case split heuristic used in the `grind` tactic,
ensuring it now avoids unnecessary case-splits on `Iff`.
---
 src/Lean/Meta/Tactic/Grind/Split.lean | 79 ++++++++++++++++++---------
 tests/lean/run/grind_t1.lean          | 26 +++++++++
 2 files changed, 79 insertions(+), 26 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean
index b7c567f90224..3937644300a7 100644
--- a/src/Lean/Meta/Tactic/Grind/Split.lean
+++ b/src/Lean/Meta/Tactic/Grind/Split.lean
@@ -17,43 +17,70 @@ inductive CaseSplitStatus where
   | ready (numCases : Nat) (isRec := false)
   deriving Inhabited, BEq
 
-private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
-  match_expr e with
-  | Or a b =>
-    if (← isEqTrue e) then
-      if (← isEqTrue a <||> isEqTrue b) then
-        return .resolved
-      else
-        return .ready 2
-    else if (← isEqFalse e) then
+/-- Given `c`, the condition of an `if-then-else`, check whether we need to case-split on the `if-then-else` or not -/
+private def checkIteCondStatus (c : Expr) : GoalM CaseSplitStatus := do
+  if (← isEqTrue c <||> isEqFalse c) then
+    return .resolved
+  else
+    return .ready 2
+
+/--
+Given `e` of the form `a ∨ b`, check whether we are ready to case-split on `e`.
+That is, `e` is `True`, but neither `a` nor `b` is `True`."
+-/
+private def checkDisjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do
+  if (← isEqTrue e) then
+    if (← isEqTrue a <||> isEqTrue b) then
       return .resolved
     else
-      return .notReady
-  | And a b =>
-    if (← isEqTrue e) then
+      return .ready 2
+  else if (← isEqFalse e) then
+    return .resolved
+  else
+    return .notReady
+
+/--
+Given `e` of the form `a ∧ b`, check whether we are ready to case-split on `e`.
+That is, `e` is `False`, but neither `a` nor `b` is `False`.
+ -/
+private def checkConjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do
+  if (← isEqTrue e) then
+    return .resolved
+  else if (← isEqFalse e) then
+    if (← isEqFalse a <||> isEqFalse b) then
       return .resolved
-    else if (← isEqFalse e) then
-      if (← isEqFalse a <||> isEqFalse b) then
-        return .resolved
-      else
-        return .ready 2
     else
-      return .notReady
-  | Eq _ _ _ =>
-    if (← isEqTrue e <||> isEqFalse e) then
       return .ready 2
-    else
-      return .notReady
-  | ite _ c _ _ _ =>
-    if (← isEqTrue c <||> isEqFalse c) then
+  else
+    return .notReady
+
+/--
+Given `e` of the form `@Eq Prop a b`, check whether we are ready to case-split on `e`.
+There are two cases:
+1- `e` is `True`, but neither both `a` and `b` are `True`, nor both `a` and `b` are `False`.
+2- `e` is `False`, but neither `a` is `True` and `b` is `False`, nor `a` is `False` and `b` is `True`.
+-/
+private def checkIffStatus (e a b : Expr) : GoalM CaseSplitStatus := do
+  if (← isEqTrue e) then
+    if (← (isEqTrue a <&&> isEqTrue b) <||> (isEqFalse a <&&> isEqFalse b)) then
       return .resolved
     else
       return .ready 2
-  | dite _ c _ _ _ =>
-    if (← isEqTrue c <||> isEqFalse c) then
+  else if (← isEqFalse e) then
+    if (← (isEqTrue a <&&> isEqFalse b) <||> (isEqFalse a <&&> isEqTrue b)) then
       return .resolved
     else
       return .ready 2
+  else
+    return .notReady
+
+private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
+  match_expr e with
+  | Or a b => checkDisjunctStatus e a b
+  | And a b => checkConjunctStatus e a b
+  | Eq _ a b => checkIffStatus e a b
+  | ite _ c _ _ _ => checkIteCondStatus c
+  | dite _ c _ _ _ => checkIteCondStatus c
   | _ =>
     if (← isResolvedCaseSplit e) then
       trace[grind.debug.split] "split resolved: {e}"
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index 3df71a83c520..1752266b8e31 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -237,3 +237,29 @@ example {α} (a b c : α) [LE α] :
 
 example (x y : Bool) : ¬(x = true ↔ y = true) ↔ (¬(x = true) ↔ y = true) := by
   grind
+
+/--
+error: `grind` failed
+case grind
+p q : Prop
+a✝¹ : p = q
+a✝ : p
+⊢ False
+-/
+#guard_msgs (error) in
+set_option trace.grind.split true in
+example (p q : Prop) : (p ↔ q) → p → False := by
+  grind -- should not split on (p ↔ q)
+
+/--
+error: `grind` failed
+case grind
+p q : Prop
+a✝¹ : p = ¬q
+a✝ : p
+⊢ False
+-/
+#guard_msgs (error) in
+set_option trace.grind.split true in
+example (p q : Prop) : ¬(p ↔ q) → p → False := by
+  grind -- should not split on (p ↔ q)