From 005f6ae7cd9be5fe9c99be43531509429ee9a5cc Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 26 Feb 2026 16:37:52 -0800
Subject: [PATCH] fix: let `Meta.zetaReduce` zeta reduce `have` expressions
 (#12695)

This PR fixes a bug in `Meta.zetaReduce` where `have` expressions were
not being zeta reduced. It also adds a feature where applications of
local functions are beta reduced, and another where zeta-delta reduction
can be disabled. These are all controllable by flags:
- `zetaDelta` (default: true) enables unfolding local definitions
- `zetaHave` (default: true) enables zeta reducing `have` expressions
- `beta` (default: true) enables beta reducing applications of local
definitions

Closes #10850
---
 src/Lean/Meta/Transform.lean | 34 +++++++++----
 tests/lean/run/10850.lean    | 95 ++++++++++++++++++++++++++++++++++++
 2 files changed, 119 insertions(+), 10 deletions(-)
 create mode 100644 tests/lean/run/10850.lean

diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean
index 2723651acf..411c5b50cd 100644
--- a/src/Lean/Meta/Transform.lean
+++ b/src/Lean/Meta/Transform.lean
@@ -185,17 +185,31 @@ def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
   return e
 
 /--
-Replaces all free variables in `e` that have let-values with their values.
-The substitution is applied recursively to the values themselves.
+Zeta-reduces `let`/`have` expressions in `e`, and also zeta-delta reduces let-bound variables.
+Removes unused `let`/`have` expressions.
+
+Options:
+- If `zetaDelta` is true (default: true), then zeta-delta reduces (unfolds) let-bound variables.
+- If `zetaHave` is false (default: true), then does not zeta reduce `have` expressions.
+- If `beta` is true (default: true), then beta reduce applications of substituted values
 -/
--- TODO: add options to distinguish zeta and zetaDelta reduction
-def zetaReduce (e : Expr) : MetaM Expr := do
-  let pre (e : Expr) : MetaM TransformStep := do
-    let .fvar fvarId := e | return .continue
-    let some localDecl := (← getLCtx).find? fvarId | return .done e
-    let some value := localDecl.value? | return .done e
-    return .visit (← instantiateMVars value)
-  transform e (pre := pre) (usedLetOnly := true)
+def zetaReduce (e : Expr) (zetaDelta := true) (zetaHave := true) (beta := true) : MetaM Expr := do
+  let n := (← getLCtx).numIndices
+  let unfold? (fvarId : FVarId) : MetaM (Option Expr) := do
+    let some decl ← fvarId.findDecl? | return none
+    if !zetaDelta && decl.index < n then return none
+    -- Values for nondep ldecls created by `transform` are valid.
+    return decl.value? (allowNondep := zetaHave && decl.index ≥ n)
+  if beta then
+    transform e (usedLetOnly := true) (pre := fun e => do
+      let .fvar fvarId := e.getAppFn | return .continue
+      let some value ← unfold? fvarId | return .continue
+      return .visit <| (← instantiateMVars value).beta e.getAppArgs)
+  else
+    transform e (usedLetOnly := true) (pre := fun e => do
+      let .fvar fvarId := e | return .continue
+      let some value ← unfold? fvarId | return .done e
+      return .visit (← instantiateMVars value))
 
 /--
 Zeta-reduces only the specified free variables, applying beta reduction after substitution.
diff --git a/tests/lean/run/10850.lean b/tests/lean/run/10850.lean
new file mode 100644
index 0000000000..c3932bdd7c
--- /dev/null
+++ b/tests/lean/run/10850.lean
@@ -0,0 +1,95 @@
+module
+public meta import Lean
+/-!
+# Testing `Lean.Meta.zetaReduce`
+
+It needs to be able to reduce both `let` and `have` expressions.
+Previously it was relying on the fact that `let` creates local definitions,
+then zeta-delta reducing.
+-/
+
+open Lean Elab Term Meta Tactic
+
+elab "zetaReduce " zd?:"zetaDelta"? zh?:"zetaHave"? beta?:"beta"? ":" t:term : tactic => withMainContext do
+  let e ← elabTermAndSynthesize t none
+  let e' ← zetaReduce e (zetaDelta := zd?.isSome) (zetaHave := zh?.isSome) (beta := beta?.isSome)
+  logInfo m!"Before reduction:{indentExpr e}\nAfter reduction:{indentExpr e'}"
+
+/--
+info: Before reduction:
+  (have m := 0 + 1;
+    m - 1) =
+    0
+After reduction:
+  (have m := 0 + 1;
+    m - 1) =
+    0
+---
+info: Before reduction:
+  (have m := 0 + 1;
+    m - 1) =
+    0
+After reduction:
+  0 + 1 - 1 = 0
+---
+info: Before reduction:
+  v
+After reduction:
+  v
+---
+info: Before reduction:
+  v
+After reduction:
+  2
+---
+info: Before reduction:
+  f v
+After reduction:
+  f v
+---
+info: Before reduction:
+  f v
+After reduction:
+  (fun n =>
+      have m := n;
+      m + 1)
+    2
+---
+info: Before reduction:
+  f v
+After reduction:
+  have m := 2;
+  m + 1
+---
+info: Before reduction:
+  f v
+After reduction:
+  (fun n => n + 1) 2
+---
+info: Before reduction:
+  f v
+After reduction:
+  2 + 1
+---
+error: unsolved goals
+v : Nat := 2
+f : Nat → Nat :=
+  fun n =>
+    have m := n;
+    let m' := m;
+    m' + 1
+⊢ True
+-/
+#guard_msgs in
+example : True := by
+  let v := 2
+  let f n := have m := n; let m' := m; m' + 1
+  zetaReduce : (have m := 0 + 1; m - 1) = 0
+  zetaReduce zetaHave : (have m := 0 + 1; m - 1) = 0
+  zetaReduce : v
+  zetaReduce zetaDelta : v
+  zetaReduce : f v
+  zetaReduce zetaDelta : f v
+  zetaReduce zetaDelta beta : f v
+  zetaReduce zetaDelta zetaHave : f v
+  zetaReduce zetaDelta zetaHave beta : f v