chore: cleanup grind palindrome test (#8428)

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/grind/grind_palindrome.lean

@@ -0,0 +1,37 @@
+set_option grind.warning false
+
+def IsPalindrome (xs : Array Nat) : Prop := xs.reverse = xs
+
+def checkPalin1 (xs : Array Nat) : Bool :=
+  go 0
+where
+  go  (i : Nat) :=
+    if h : i < xs.size / 2 then
+      if xs[i] = xs[xs.size - 1 - i] then
+        go (i + 1)
+      else
+        false
+    else
+      true
+
+-- This give the more natural proof that we'd like to give in `tests/run/grind_palindrome2.lean`,
+-- but in which `grind` currently fails.
+
+theorem checkPalin1_correct' : checkPalin1 xs = true ↔ IsPalindrome xs := by
+  unfold checkPalin1
+  suffices ∀ i, checkPalin1.go xs i = true ↔ ∀ j, i ≤ j → (_ : j < xs.size - i) → xs[j] = xs[xs.size - 1 - j] by
+    grind [IsPalindrome]
+  intro i
+  fun_induction checkPalin1.go
+  · grind (splits := 14)
+    -- fails, but it would be nice to succeed! The key observations are:
+    -- [eqc] True propositions ▼
+    --   [prop] ∀ (a : Nat) (b : a + 1 ≤ xs.toList.length - x), a + 1 ≤ x ∨ xs[a] = xs[xs.toList.length - (a + 1)]
+    -- [eqc] False propositions ▼
+    --   [prop] xs[x] = xs[xs.toList.length - (x + 1)]
+    -- Instantiating the `∀` with `a := x`, we can then easily prove `a + 1 ≤ xs.toList.length - x` and
+    -- prove that it's not the case that `a + 1 ≤ x`, so we get `xs[x] = xs[xs.toList.length - (x + 1)]`,
+    -- which is false.
+  · grind
+    -- The same argument should apply here.
+  · grind

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