From 5f2f010d6611d5f14fbfe1fc138e97ebad1f5f2f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 3 Apr 2025 15:57:49 -0700
Subject: [PATCH] fix: missing forall normalization rules in `grind` (#7808)

This PR adds missing forall normalization rules to `grind`.
---
 src/Init/Grind/Norm.lean            |  7 +++++--
 tests/lean/grind/list_problems.lean | 13 +++++--------
 tests/lean/run/grind_t1.lean        |  4 ++++
 3 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean
index 325f9248c6..9a83192c44 100644
--- a/src/Init/Grind/Norm.lean
+++ b/src/Init/Grind/Norm.lean
@@ -83,6 +83,9 @@ theorem Nat.pow_one (a : Nat) : a ^ 1 = a := by
 theorem Int.pow_one (a : Int) : a ^ 1 = a := by
   simp [Int.pow_succ]
 
+theorem forall_true (p : True → Prop) : (∀ h : True, p h) = p True.intro :=
+  propext <| Iff.intro (fun h => h True.intro) (fun h _ => h)
+
 init_grind_norm
   /- Pre theorems -/
   not_and not_or not_ite not_forall not_exists
@@ -108,7 +111,7 @@ init_grind_norm
   ite_true ite_false ite_true_false ite_false_true
   dite_eq_ite
   -- Forall
-  forall_and
+  forall_and forall_false forall_true
   -- Exists
   exists_const exists_or exists_prop exists_and_left exists_and_right
   -- Bool cond
@@ -131,7 +134,7 @@ init_grind_norm
   Nat.le_zero_eq Nat.lt_eq Nat.succ_eq_add_one
   Nat.add_eq Nat.sub_eq Nat.mul_eq Nat.zero_eq Nat.le_eq
   Nat.div_zero Nat.mod_zero Nat.div_one Nat.mod_one
-  Nat.sub_sub Nat.pow_zero Nat.pow_one
+  Nat.sub_sub Nat.pow_zero Nat.pow_one Nat.sub_self
   -- Int
   Int.lt_eq
   Int.emod_neg Int.ediv_neg
diff --git a/tests/lean/grind/list_problems.lean b/tests/lean/grind/list_problems.lean
index 4624d22d5d..b560abb6a1 100644
--- a/tests/lean/grind/list_problems.lean
+++ b/tests/lean/grind/list_problems.lean
@@ -2,18 +2,15 @@ theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.le
   induction l
   · grind
   · cases i
-    · -- Fails because of the issue:
-      --   [issue] failed to create E-match local theorem for
-      --     ∀ (x : 1 ≤ tail.length), ¬tail[0] = a
-      -- despite having asserted `1 ≤ tail.length `.
+    · -- Better support for implication and dependent implication.
+      -- We need inequality propagation (or case-splits)
       grind
     · -- Similarly
       grind
 
 attribute [grind] List.getElem_append_left List.getElem_append_right
+attribute [grind] List.length_cons List.length_nil
 
-@[simp] theorem getElem_concat_length {l : List α} {a : α} {i : Nat} (h : i = l.length) (w) :
+example {l : List α} {a : α} {i : Nat} (h : i = l.length) (w) :
     (l ++ [a])[i]'w = a := by
-  subst h; grind
--- [issue] failed to create E-match local theorem for
---   ∀ (h₁ : True), (l ++ [a])[l.length] = [a][l.length - l.length]
+  grind -- Similar to issue above.
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index bb7c1a9bf9..326b6436d3 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -420,3 +420,7 @@ example [BEq α] [LawfulBEq α] (a b : α) : a ≠ b → foo a b = 0 := by
 
 example [BEq α] [LawfulBEq α] (a b : α) : a ≠ b → foo a b = 0 := by
   grind (splits := 0) [foo]
+
+@[simp] theorem getElem_concat_length {l : List α} {a : α} {i : Nat} (h : i = l.length) (w) :
+    (l ++ [a])[i]'w = a := by
+  subst h; grind [List.getElem_append_left, List.getElem_append_right]