fix: case-splitting in grind (#8410)

This PR fixes a case-splitting heuristic in `grind` and simplifies the
proof for test `grind_palindrome2.lean`.

Author: leodemoura

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

@@ -102,10 +102,12 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
       if (← isProp d) then
         addSplitCandidate (.imp e (h ▸ rfl))
     else if Arith.isRelevantPred d then
+      -- TODO: should we keep lookahead after we implement non-chronological backtracking?
       if (← getConfig).lookahead then
         addLookaheadCandidate (.imp e (h ▸ rfl))
-      else
-        addSplitCandidate (.imp e (h ▸ rfl))
+      -- We used to add the `split` only if `lookahead := false`, but it was counterintuitive
+      -- to make `grind` "stronger" by disabling a feature.
+      addSplitCandidate (.imp e (h ▸ rfl))
   | _ => pure ()
 
 /--

tests/lean/run/grind_palindrome2.lean

@@ -21,24 +21,17 @@ example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j
 theorem checkPalin1_correct' : checkPalin1 xs = true ↔ IsPalindrome xs := by
   unfold checkPalin1
   suffices ∀ i, checkPalin1.go xs i = true ↔ ∀ j, i ≤ j → (_ : j < xs.size / 2) → xs[j] = xs[xs.size - 1 - j] by
-    rw [this, IsPalindrome]
-    constructor
-    · intro w
-      ext i hi₁ hi₂
-      · grind
-      · by_cases h : i < xs.size / 2 <;> grind
-    · intro w
-      intro j hj hj'
-      grind
+    -- We need array extensionality. TODO: easy way to enable array extensionality, `extAll` enables all [ext] theorems
+    -- TODO: `IsPalindrome` (without `.eq_1`) produces bad error message.
+    grind +extAll [IsPalindrome.eq_1]
   intro i
   fun_induction checkPalin1.go
   case case1 j h₁ h₂ ih =>
-    constructor
-    · intro w j'
-      by_cases j' = j <;> grind
-    · grind
+    -- TODO: make sure we don't need `constructor` here. This is a normalization issue.
+    constructor <;> grind
   case case2 j h₁ h₂ =>
+    -- TODO: fix normalization
     simp only [Bool.false_eq_true, false_iff, Classical.not_forall]
-    refine ⟨j, by grind⟩
+    grind
   case case3 x h =>
     grind