From a639eb185cab63adac2616486c2239a796b7b066 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Jul 2022 06:42:09 -0700
Subject: [PATCH] fix: `dsimp` `zeta` issue

---
 src/Lean/Meta/Tactic/Simp/Main.lean         |  7 +++++--
 tests/lean/dsimpZetaIssue.lean              | 19 +++++++++++++++++++
 tests/lean/dsimpZetaIssue.lean.expected.out |  9 +++++++++
 3 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/dsimpZetaIssue.lean
 create mode 100644 tests/lean/dsimpZetaIssue.lean.expected.out

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 98c14323fff..3e98d59fac7 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/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
diff --git a/tests/lean/dsimpZetaIssue.lean b/tests/lean/dsimpZetaIssue.lean
new file mode 100644
index 00000000000..d7ab6a439e0
--- /dev/null
+++ b/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]
diff --git a/tests/lean/dsimpZetaIssue.lean.expected.out b/tests/lean/dsimpZetaIssue.lean.expected.out
new file mode 100644
index 00000000000..fde407474f5
--- /dev/null
+++ b/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