From 60ea92fdb0594065072ed843724d98cd15b76fba Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 12 May 2025 16:33:38 +1000
Subject: [PATCH] chore: add failing grind tests (#8289)

---
 tests/lean/grind/grind_congrArg.lean          | 21 +++++++++++
 .../grind/qsort_ematch_local_theorem.lean     | 35 +++++++++++++++++++
 2 files changed, 56 insertions(+)
 create mode 100644 tests/lean/grind/grind_congrArg.lean
 create mode 100644 tests/lean/grind/qsort_ematch_local_theorem.lean

diff --git a/tests/lean/grind/grind_congrArg.lean b/tests/lean/grind/grind_congrArg.lean
new file mode 100644
index 0000000000..d777ad2845
--- /dev/null
+++ b/tests/lean/grind/grind_congrArg.lean
@@ -0,0 +1,21 @@
+set_option grind.warning false
+
+namespace Array
+
+private theorem getElem_qpartition_snd_of_hi_lt {n} (lt : α → α → Bool) (as : Vector α n) (lo hi : Nat)
+    (hlo : lo < n) (hhi : hi < n) (w : lo ≤ hi)
+    (k : Nat) (h : hi < k) (h' : k < n) : (qpartition as lt lo hi hlo hhi).2[k] = as[k] := sorry
+
+@[local grind] private theorem getElem_qsort_sort_of_hi_lt
+    {n} (lt : α → α → Bool) (as : Vector α n) (lo hi : Nat)
+    (hlo : lo < n) (hhi : hi < n) (w : lo ≤ hi)
+    (i : Nat) (h : hi < i) (h' : i < n) : (qsort.sort lt as lo hi hlo hhi)[i] = as[i] := by
+  fun_induction qsort.sort
+  case case1 a b =>
+    unfold qsort.sort
+    -- `grind` fails unless we uncomment the following two lines. I would hope it manages both!
+    -- have := congrArg (·.2) a
+    -- simp only [dif_pos, *]
+    grind [getElem_qpartition_snd_of_hi_lt]
+  case case2 a b ih1 ih2 ih3 => sorry
+  case case3 => sorry
diff --git a/tests/lean/grind/qsort_ematch_local_theorem.lean b/tests/lean/grind/qsort_ematch_local_theorem.lean
new file mode 100644
index 0000000000..030e06af2f
--- /dev/null
+++ b/tests/lean/grind/qsort_ematch_local_theorem.lean
@@ -0,0 +1,35 @@
+set_option grind.warning false
+
+namespace Array
+
+private theorem getElem_qpartition_snd_of_lt_lo {n} (lt : α → α → Bool) (as : Vector α n) (lo hi : Nat)
+    (hlo : lo < n) (hhi : hi < n) (w : lo ≤ hi)
+    (k : Nat) (h : k < lo) : (qpartition as lt lo hi hlo hhi).2[k] = as[k] := sorry
+
+-- First version, works fine:
+private theorem getElem_qsort_sort_of_lt_lo
+    {n} (lt : α → α → Bool) (as : Vector α n) (lo hi : Nat)
+    (hlo : lo < n) (hhi : hi < n) (w : lo ≤ hi)
+    (i : Nat) (h : i < lo) : (qsort.sort lt as lo hi hlo hhi)[i] = as[i] := by
+  fun_induction qsort.sort
+  case case1 a b => sorry
+  case case2 a b ih1 ih2 ih3 =>
+    unfold qsort.sort
+    grind [getElem_qpartition_snd_of_lt_lo]
+  case case3 => sorry
+
+-- But this version fails:
+private theorem getElem_qsort_sort_of_lt_lo'
+    {n} (lt : α → α → Bool) (as : Vector α n) (lo hi : Nat)
+    (hlo : lo < n) (hhi : hi < n) (w : lo ≤ hi)
+    (i : Nat) (h : i < lo) : (qsort.sort lt as lo hi hlo hhi)[i] = as[i] := by
+  fun_induction qsort.sort
+  case case1 a b => sorry
+  case case2 a b ih1 ih2 ih3 =>
+    unfold qsort.sort
+    -- Grind can finish from here if we comment out the `simp only`.
+    -- But if we do a manual step, then `grind` fails and
+    -- we get "failed to create E-match local theorem" issues
+    simp only [↓reduceDIte, *]
+    grind [getElem_qpartition_snd_of_lt_lo]
+  case case3 => sorry