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

@@ -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

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

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