fix: dsimp zeta issue

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -173,6 +173,7 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
   | none => return e
 
 private partial def dsimp (e : Expr) : M Expr := do
+  let cfg ← getConfig
   let pre (e : Expr) : M TransformStep := do
     if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
       if r.expr != e then
@@ -182,9 +183,11 @@ private partial def dsimp (e : Expr) : M Expr := do
     if let Step.visit r ← rewritePost e (fun _ => pure none) (rflOnly := true) then
       if r.expr != e then
         return .visit r.expr
-    let eNew ← reduce e
+    let mut eNew ← reduce e
+    if cfg.zeta && eNew.isFVar then
+      eNew ← reduceFVar cfg eNew
     if eNew != e then return .visit eNew else return .done e
-  transform e (pre := pre) (post := post)
+  transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
 instance : Inhabited (M α) where
   default := fun _ _ _ => default

tests/lean/dsimpZetaIssue.lean

@@ -0,0 +1,19 @@
+example : let x := 0; x + 5 = 5 := by
+  dsimp (config := { zeta := false })
+  trace_state
+  simp
+
+example : let x := 0; x + 5 = 5 := by
+  dsimp
+
+example : let x := 0; x + y = y := by
+  dsimp
+  trace_state
+  rw [Nat.zero_add]
+
+example : let x := 0; x + y = y := by
+  dsimp (config := { zeta := false })
+  trace_state
+  conv => zeta
+  trace_state
+  rw [Nat.zero_add]

tests/lean/dsimpZetaIssue.lean.expected.out

@@ -0,0 +1,9 @@
+⊢ let x := 0;
+  x + 5 = 5
+y : Nat
+⊢ 0 + y = y
+y : Nat
+⊢ let x := 0;
+  x + y = y
+y : Nat
+⊢ 0 + y = y