From 62dc8d64fa12e112827e4a29c3433e6d784bfbea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 9 Jul 2025 20:18:44 -0700
Subject: [PATCH] perf: use custom `reduceCtorEq` simproc in `grind` (#9293)

This PR replaces the `reduceCtorEq` simproc used in `grind` by a much
more efficient one. The default one use in `simp` is just overhead
because the `grind` normalizer is already normalizing arithmetic.
In a separate PR, we will push performance improvements to the default
`reduceCtorEq`.
---
 src/Init/Grind/Norm.lean                 |  2 +-
 src/Lean/Meta/Tactic/Grind/SimpUtil.lean | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean
index 04baf9608b..85a85b993f 100644
--- a/src/Init/Grind/Norm.lean
+++ b/src/Init/Grind/Norm.lean
@@ -154,7 +154,7 @@ init_grind_norm
   -- And
   and_true true_and and_false false_and and_assoc
   -- ite
-  ite_true ite_false ite_true_false ite_false_true
+  ite_true_false ite_false_true
   -- Bool cond
   cond_eq_ite
   -- Bool or
diff --git a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
index f3d96f1d49..8f89c19ad3 100644
--- a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
+++ b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
@@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.ForallProp
 import Lean.Meta.Tactic.Grind.Arith.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
 
 namespace Lean.Meta.Grind
 
@@ -125,6 +126,14 @@ builtin_simproc_decl simpOr (Or _ _) := fun e => do
   | False => return .visit { expr := p, proof? := some <| mkApp (mkConst ``or_false) p }
   | _ => return .continue
 
+builtin_simproc_decl reduceCtorEqCheap (_ = _) := fun e => do
+  let_expr Eq _ lhs rhs ← e | return .continue
+  let some (c₁, _) ← constructorApp? lhs | return .continue
+  let some (c₂, _) ← constructorApp? rhs | return .continue
+  unless c₁.name != c₂.name do return .continue
+  withLocalDeclD `h e fun h =>
+    return .done { expr := mkConst ``False, proof? := (← withDefault <| mkEqFalse' (← mkLambdaFVars #[h] (← mkNoConfusion (mkConst ``False) h))) }
+
 /-- Returns the array of simprocs used by `grind`. -/
 protected def getSimprocs : MetaM (Array Simprocs) := do
   let s ← Simp.getSEvalSimprocs
@@ -142,6 +151,8 @@ protected def getSimprocs : MetaM (Array Simprocs) := do
   We don't want it to be simplified to `[] = []`.
   -/
   let s := s.erase ``List.reduceReplicate
+  let s := s.erase ``reduceCtorEq
+  let s ← s.add ``reduceCtorEqCheap (post := true)
   let s ← addSimpMatchDiscrsOnly s
   let s ← addPreMatchCondSimproc s
   let s ← Arith.addSimproc s