From 2ce55ba460bcfca781dacd57242e37359ff5edc8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Thu, 19 Feb 2026 11:10:30 +0000
Subject: [PATCH] fix: catch exceptions in cbv rewrite simprocs to handle
 projections (#12562)

This PR fixes #12554 where the `cbv` tactic throws "unexpected kernel
projection term during structural definitional equality" when a rewrite
theorem's pattern contains a lambda and the expression being matched has
a `.proj` (kernel projection) at the corresponding position.

The `Sym` pattern matching infrastructure (`isDefEqMain` in
`Pattern.lean`) does not handle `.proj` expressions and can throw an
exception. Rather than presenting it as an error in `cbv`, we fail
quietly and let the `cbv` tactic try other fallback paths.

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/Lean/Meta/Sym/Simp/Simproc.lean  |  4 ++++
 src/Lean/Meta/Tactic/Cbv/Main.lean   |  8 ++++----
 tests/lean/run/cbv_proj_arg_bug.lean | 23 +++++++++++++++++++++++
 3 files changed, 31 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/cbv_proj_arg_bug.lean

diff --git a/src/Lean/Meta/Sym/Simp/Simproc.lean b/src/Lean/Meta/Sym/Simp/Simproc.lean
index c02be80a76..668048804b 100644
--- a/src/Lean/Meta/Sym/Simp/Simproc.lean
+++ b/src/Lean/Meta/Sym/Simp/Simproc.lean
@@ -27,4 +27,8 @@ public abbrev Simproc.orElse (f g : Simproc) : Simproc := fun e₁ => do
 public instance : OrElse Simproc where
   orElse f g := Simproc.orElse f (g ())
 
+/-- Wraps a simproc so that any exception is caught and treated as `.rfl` (no rewrite). -/
+public abbrev Simproc.tryCatch (f : Simproc) : Simproc := fun e => do
+  try f e catch _ => return .rfl
+
 end Lean.Meta.Sym.Simp
diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean
index fedec47fde..c67012a95d 100644
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Main.lean
@@ -29,14 +29,14 @@ def tryEquations : Simproc := fun e => do
     return .rfl
   let some appFn := e.getAppFn.constName? | return .rfl
   let thms ← getEqnTheorems appFn
-  thms.rewrite (d := dischargeNone) e
+  Simproc.tryCatch (thms.rewrite (d := dischargeNone)) e
 
 def tryUnfold : Simproc := fun e => do
   unless e.isApp do
     return .rfl
   let some appFn := e.getAppFn.constName? | return .rfl
   let some thm ← getUnfoldTheorem appFn | return .rfl
-  Theorem.rewrite thm e
+  Simproc.tryCatch (fun e => Theorem.rewrite thm e) e
 
 def handleConstApp : Simproc := fun e => do
   if (← isCbvOpaque e.getAppFn.constName!) then
@@ -53,7 +53,7 @@ def betaReduce : Simproc := fun e => do
 def tryCbvTheorems : Simproc := fun e => do
   let some fnName := e.getAppFn.constName? | return .rfl
   let some evalLemmas ← getCbvEvalLemmas fnName | return .rfl
-  Theorems.rewrite evalLemmas (d := dischargeNone) e
+  Simproc.tryCatch (Theorems.rewrite evalLemmas (d := dischargeNone)) e
 
 def handleApp : Simproc := fun e => do
   unless e.isApp do return .rfl
@@ -154,7 +154,7 @@ def handleConst : Simproc := fun e => do
     return .rfl
   -- TODO: Check if we need to look if we applied all the levels correctly
   let some thm ← getUnfoldTheorem n | return .rfl
-  Theorem.rewrite thm e
+  Simproc.tryCatch (fun e => Theorem.rewrite thm e) e
 
 def cbvPreStep : Simproc := fun e => do
   match e with
diff --git a/tests/lean/run/cbv_proj_arg_bug.lean b/tests/lean/run/cbv_proj_arg_bug.lean
new file mode 100644
index 0000000000..4df1d97e0d
--- /dev/null
+++ b/tests/lean/run/cbv_proj_arg_bug.lean
@@ -0,0 +1,23 @@
+-- Regression test for https://github.com/leanprover/lean4/issues/12554
+
+def applyFn (f : Nat → Nat) (x : Nat) : Nat := f x
+
+@[cbv_eval] theorem applyFn_id : applyFn (fun x => x) = fun x => x := by
+  funext x; rfl
+
+opaque fnPair : (Nat → Nat) × Nat
+
+-- The `.proj` in `fnPair.1` caused pattern matching against the lambda in
+-- `applyFn_id` to throw.
+example : applyFn fnPair.1 42 = fnPair.1 42 := by cbv
+
+opaque pair : Nat × Nat
+def myId (x : Nat) : Nat := x
+example : myId pair.1 = pair.1 := by cbv
+
+def isZero : Nat → Bool
+  | 0 => true
+  | _ + 1 => false
+
+example : isZero pair.1 = isZero pair.1 := by cbv
+example : applyFn (fun x => x) 42 = 42 := by cbv