From dae150a9764992ff97ffc8d5a489142b3d93da09 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Fri, 13 Feb 2026 14:21:13 +0000
Subject: [PATCH] fix: handle `AppBuilderException` in `cbv` tactic if the
 projection function is dependent (#12460)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes an `AppBuilder` exception in the `cbv` tactic when
simplifying projections whose projection function is dependent (closes
#12457).

Previously, `handleProj` unconditionally used `mkCongrArg` to prove `e.i
= e'.i` from `e = e'`, but `mkCongrArg` requires a non-dependent
function. For dependent projections (e.g., `fun x => x.2 : (x :
String.Slice) → x.1.Pos`), this would fail.

Now, `handleProj` first checks whether the projection function type is
non-dependent (a simple arrow). If so, it proceeds with `mkCongrArg` as
before. Otherwise, it falls back to:
1. Attempting to reduce the projection directly.
2. If reduction fails, using a heterogeneous congruence lemma
(`mkHCongr`) converted to an equality via `mkEqOfHEq`, provided the
original and rewritten struct are definitionally equal.
---
 src/Lean/Meta/Tactic/Cbv/Main.lean | 27 +++++++++++++++++++++++----
 tests/lean/run/12457.lean          |  1 +
 2 files changed, 24 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/12457.lean

diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean
index e80da0abe9..2f29915fa7 100644
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Main.lean
@@ -120,10 +120,29 @@ def handleProj : Simproc := fun e => do
   | .step e' proof _ =>
     let type ← Sym.inferType e'
     let congrArgFun := Lean.mkLambda `x .default type <| .proj typeName idx <| .bvar 0
-
-    -- TODO: Create an efficient symbolic version of `mkCongrArg`
-    let newProof ← mkCongrArg congrArgFun proof
-    return .step (← Lean.Expr.updateProjS! e e') newProof
+    let congrArgFunType ← inferType congrArgFun
+    -- If the type of a projection function is non-dependent, we can safely prove `e.i = e'.i` from `e = e'`
+    if (congrArgFunType.isArrow) then
+      let newProof ← mkCongrArg congrArgFun proof
+      return .step (← Lean.Expr.updateProjS! e e') newProof
+    else
+      -- If the type of the projection function is dependent, we first try to reduce the projection
+      let reduced ← reduceProj? e
+      match reduced with
+      | .some reduced =>
+        let reduced ← Sym.share reduced
+        return .step reduced (← Sym.mkEqRefl reduced)
+      | .none =>
+       -- If we failed to reduce it, we turn to a last resort; we try use heterogenous congruence lemma that we then try to turn into an equality.
+        unless (← isDefEq struct e') do
+          -- If we rewrote the projection body using something that holds up to propositional equality, then there is nothing we can do.
+          -- TODO: Check if there is a need to report this to a user, or shall we fail silently.
+          return .rfl
+        let hcongr ← mkHCongr congrArgFun
+        let newProof := mkApp3 (hcongr.proof) struct e' proof
+        -- We have already checked if `struct` and `e'` are defEq, so we can skip the check.
+        let newProof ← mkEqOfHEq newProof (check := false)
+        return .step (← Lean.Expr.updateProjS! e e') newProof
 
 def simplifyAppFn : Simproc := fun e => do
     unless e.isApp do return .rfl
diff --git a/tests/lean/run/12457.lean b/tests/lean/run/12457.lean
new file mode 100644
index 0000000000..5bb7652430
--- /dev/null
+++ b/tests/lean/run/12457.lean
@@ -0,0 +1 @@
+example : ("abc".pos ⟨1⟩ (by decide_cbv)).get (by decide_cbv) = 'b' := by decide_cbv