chore: cleanup grind palindrome test

Author: kim-em

src/Init/Data/Array/Lemmas.lean

@@ -63,7 +63,7 @@ theorem toArray_eq : List.toArray as = xs ↔ as = xs.toList := by
 
 /-! ### size -/
 
-@[grind →] theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
+theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
   cases xs
   simp_all
 

src/Init/Data/Vector/Lemmas.lean

@@ -486,7 +486,7 @@ abbrev toArray_mkVector := @toArray_replicate
 `Vector.ext` is an extensionality theorem.
 Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
 -/
-@[ext]
+@[ext, grind ext]
 protected theorem ext {xs ys : Vector α n} (h : (i : Nat) → (_ : i < n) → xs[i] = ys[i]) : xs = ys := by
   apply Vector.toArray_inj.1
   apply Array.ext

src/Init/Ext.lean

@@ -82,6 +82,8 @@ end Lean
 attribute [ext] Prod PProd Sigma PSigma
 attribute [ext] funext propext Subtype.eq Array.ext
 
+attribute [grind ext] Array.ext
+
 @[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
 protected theorem Unit.ext (x y : Unit) : x = y := rfl
 

tests/lean/run/grind_palindrome2.lean

@@ -14,15 +14,12 @@ where
     else
       true
 
-example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j < xs.size / 2) :
-    xs[j] = xs[xs.size - 1 - j] := by
-  grind
-
-attribute [grind ext] Array.ext -- TODO: should we mark it by default?
-
-theorem checkPalin1_correct' : checkPalin1 xs = true ↔ IsPalindrome xs := by
+-- This works nicely, but there is some human assistance here:
+-- on the right hand side of the `suffices` we've asserted it's enough to check up to `j < xs.size / 2`
+-- while the "natural" statement would be all the way to `j < xs.size - i`.
+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
     grind [IsPalindrome]
   intro i
-  fun_induction checkPalin1.go <;> grind
+  fun_induction checkPalin1.go with grind