From 11ddd0a572287d24e2aa1619ac0340dcb905c294 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 29 Aug 2026 12:51:16 +0000
Subject: [PATCH] fix: kernel error from `simp` results cached with a proof
 that has free variables

This PR fixes `simp` producing a proof with free variables, rejected by the kernel with "declaration has free variables", when the same `match` application occurs in two branches of a `dite`. This also affected the equation lemmas generated for well-founded definitions containing such a term.

`simp` caches results by expression, so the proof of a cached result must not mention local hypotheses that `simp` introduced itself while descending into the term (see `Methods.wellBehavedDischarge`). `dischargeEqnThmHypothesis?` violated this: proving a match-equation side condition substitutes a discriminant, and `subst` reverts every hypothesis depending on it, pulling e.g. the `dite` hypothesis into the proof. It now clears those hypotheses from the goal first; `tryClearMany` keeps the ones the side condition itself depends on.

Closes #14961.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Nk92q7cJwjqGyg8kep2Gyi
---
 src/Lean/Meta/Tactic/Simp/Rewrite.lean | 24 +++++++++++++++++++++---
 tests/elab/14961.lean                  | 14 ++++++++++++++
 2 files changed, 35 insertions(+), 3 deletions(-)
 create mode 100644 tests/elab/14961.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 8512275eee6f..164b629fe8eb 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -591,12 +591,15 @@ private def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
 /--
   Tries to solve `e` using `unifyEq?`.
   It assumes that `isEqnThmHypothesis e` is `true`.
+
+  The local declarations in `toClear` are removed from the goal before proving it, so that they
+  cannot occur in the resulting proof. `tryClearMany` keeps the ones `e` depends on.
 -/
-partial def dischargeEqnThmHypothesis? (e : Expr) : MetaM (Option Expr) := do
+partial def dischargeEqnThmHypothesis? (e : Expr) (toClear : Array FVarId := #[]) : MetaM (Option Expr) := do
   assert! isEqnThmHypothesis e
   let mvar ← mkFreshExprSyntheticOpaqueMVar e
   withCanUnfoldAtMatcherPred do
-    if let .none ← go? mvar.mvarId! then
+    if let .none ← go? (← mvar.mvarId!.tryClearMany toClear) then
       instantiateMVars mvar
     else
       return none
@@ -634,11 +637,26 @@ def dischargeRfl (e : Expr) : SimpM (Option Expr) := do
     return .none
 
 
+/--
+The local declarations that `simp` itself introduced, e.g. when descending into the branches of an
+`ite`. A discharger must not use them unless `contextual := true`, because its proof ends up in a
+`simp` result that is cached under a key that does not mention them.
+See the comment at `Methods.wellBehavedDischarge`.
+-/
+private def newLocalDecls : SimpM (Array FVarId) := do
+  if (← getConfig).contextual then return #[]
+  let lctxInitIndices := (← readThe Simp.Context).lctxInitIndices
+  let mut toClear := #[]
+  for localDecl in (← getLCtx) do
+    if localDecl.index >= lctxInitIndices then
+      toClear := toClear.push localDecl.fvarId
+  return toClear
+
 def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
   let e := e.cleanupAnnotations
   if isEqnThmHypothesis e then
     if let some r ← dischargeUsingAssumption? e then return some r
-    if let some r ← dischargeEqnThmHypothesis? e then return some r
+    if let some r ← dischargeEqnThmHypothesis? e (← newLocalDecls) then return some r
   let r ← simp e
   if let some p ← dischargeRfl r.expr then
     return some (mkApp4 (mkConst ``Eq.mpr [Level.zero]) e r.expr (← r.getProof) p)
diff --git a/tests/elab/14961.lean b/tests/elab/14961.lean
new file mode 100644
index 000000000000..d73bb585b690
--- /dev/null
+++ b/tests/elab/14961.lean
@@ -0,0 +1,14 @@
+/-!
+Tests that `simp` does not reuse a cached result whose proof mentions a hypothesis that `simp`
+introduced itself while descending into a term (here the `h` of the `dite`). Reusing such a result
+in a sibling branch produced a proof with free variables, which the kernel rejects.
+-/
+
+def f (n : Nat) : Nat :=
+  if _h : n = 0 then 0 else (let s := n; match s, true with | 2, false => 1 | _, _ => 0) + f 0
+  termination_by n
+
+example (n : Nat) :
+    (if _h : n = 0 then (let s := n; match s, true with | 2, false => 1 | _, _ => 0)
+     else (let s := n; match s, true with | 2, false => 1 | _, _ => 0)) = 0 := by
+  simp