From dd7bc0e64376d12b5bcd77fa4766fb3668d85846 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 4 Jul 2025 22:13:49 -0700
Subject: [PATCH] perf: simproc for `grind` normalizations and decls to unfold
 (#9202)

This PR extends the `Eq` simproc used in `grind`. It covers more cases
now. It also adds 3 reducible declarations to the list of declarations
to unfold.
---
 src/Init/Data/Vector/Lemmas.lean         |  2 +-
 src/Lean/Meta/Tactic/Grind/SimpUtil.lean | 56 ++++++++++++++++--------
 stage0/src/stdlib_flags.h                |  1 +
 3 files changed, 40 insertions(+), 19 deletions(-)

diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 4fd9e0a03d..6cf7af13b9 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -284,7 +284,7 @@ set_option linter.indexVariables false in
     (xs.drop i).toArray = xs.toArray.extract i n := by
   simp [drop]
 
-@[simp, grind] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl
+@[simp, grind =] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl
 
 @[simp, grind] theorem toArray_emptyWithCapacity {cap} :
     (Vector.emptyWithCapacity (α := α) cap).toArray = Array.emptyWithCapacity cap := rfl
diff --git a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
index 767ae9b220..0d51f1afaf 100644
--- a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
+++ b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
@@ -33,20 +33,31 @@ private def isBoolEqTarget (declName : Name) : Bool :=
   declName == ``BEq.beq  ||
   declName == ``decide
 
-builtin_simproc_decl simpBoolEq (@Eq Bool _ _) := fun e => do
-  let_expr f@Eq bool lhs rhs ← e | return .continue
-  let .const rhsName _ := rhs.getAppFn | return .continue
-  if rhsName == ``true || rhsName == ``false then return .continue
-  let .const lhsName _ := lhs.getAppFn | return .continue
-  if lhsName == ``true || lhsName == ``false then
-    -- Just apply comm
-    let e' := mkApp3 f bool rhs lhs
-    return .visit { expr := e', proof? := mkApp2 (mkConst ``Grind.flip_bool_eq) lhs rhs }
-  if isBoolEqTarget lhsName || isBoolEqTarget rhsName then
-    -- Convert into `(lhs = true) = (rhs = true)`
-    let tr := mkConst ``true
-    let e' ← mkEq (mkApp3 f bool lhs tr) (mkApp3 f bool rhs tr)
-    return .visit { expr := e', proof? := mkApp2 (mkConst ``Grind.bool_eq_to_prop) lhs rhs }
+builtin_simproc_decl simpEq (@Eq _ _ _) := fun e => do
+  let_expr f@Eq α lhs rhs ← e | return .continue
+  match_expr α with
+  | Bool =>
+    let .const rhsName _ := rhs.getAppFn | return .continue
+    if rhsName == ``true || rhsName == ``false then return .continue
+    let .const lhsName _ := lhs.getAppFn | return .continue
+    if lhsName == ``true || lhsName == ``false then
+      -- Just apply comm
+      let e' := mkApp3 f α rhs lhs
+      return .visit { expr := e', proof? := mkApp2 (mkConst ``Grind.flip_bool_eq) lhs rhs }
+    if isBoolEqTarget lhsName || isBoolEqTarget rhsName then
+      -- Convert into `(lhs = true) = (rhs = true)`
+      let tr := mkConst ``true
+      let e' ← mkEq (mkApp3 f α lhs tr) (mkApp3 f α rhs tr)
+      return .visit { expr := e', proof? := mkApp2 (mkConst ``Grind.bool_eq_to_prop) lhs rhs }
+    return .continue
+  | _ =>
+    if (← isDefEq lhs rhs) then
+      let u := f.constLevels!
+      return .done { expr := mkConst ``True, proof? := mkApp2 (mkConst ``eq_self u) α lhs }
+    else if rhs == mkConst ``True then
+      return .done { expr := lhs, proof? := mkApp (mkConst ``Grind.eq_true_eq) lhs }
+    else if rhs == mkConst ``False then
+      return .visit { expr := mkNot lhs, proof? := mkApp (mkConst ``Grind.eq_false_eq) lhs }
   return .continue
 
 /-- Returns the array of simprocs used by `grind`. -/
@@ -70,14 +81,23 @@ protected def getSimprocs : MetaM (Array Simprocs) := do
   let s ← addPreMatchCondSimproc s
   let s ← Arith.addSimproc s
   let s ← addForallSimproc s
-  let s ← s.add ``simpBoolEq (post := false)
+  let s ← s.add ``simpEq (post := false)
   return #[s]
 
+private def addDeclToUnfold (s : SimpTheorems) (declName : Name) : MetaM SimpTheorems := do
+  if (← getEnv).contains declName then
+    s.addDeclToUnfold declName
+  else
+    return s
+
 /-- Returns the simplification context used by `grind`. -/
 protected def getSimpContext (config : Grind.Config) : MetaM Simp.Context := do
-  let thms ← normExt.getTheorems
-  let thms ← thms.addDeclToUnfold ``GE.ge
-  let thms ← thms.addDeclToUnfold ``GT.gt
+  let mut thms ← normExt.getTheorems
+  thms ← addDeclToUnfold thms ``GE.ge
+  thms ← addDeclToUnfold thms ``GT.gt
+  thms ← addDeclToUnfold thms ``Nat.cast
+  thms ← addDeclToUnfold thms ``Bool.xor
+  thms ← addDeclToUnfold thms ``Ne
   Simp.mkContext
     (config := { arith := true, zeta := config.zeta, zetaDelta := config.zetaDelta, catchRuntime := false })
     (simpTheorems := #[thms])
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..ad491b0de1 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {