From fb64a4ccc06a75b92dbef2c6af629cb2c353ae91 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Apr 2022 07:17:05 -0700
Subject: [PATCH] fix: `unfold` should not create an auxiliary declaration when
 result is definitionally equal

This commit fixes an issue reported on Zulip
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unfolding.20the.20type.20of.20a.20variable.20creates.20a.20new.20variable
---
 src/Lean/Meta/Tactic/Simp/Main.lean      | 17 +++++++++++++----
 src/Lean/Meta/Tactic/Unfold.lean         |  2 +-
 tests/lean/unfoldDefEq.lean              |  9 +++++++++
 tests/lean/unfoldDefEq.lean.expected.out |  5 +++++
 4 files changed, 28 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/unfoldDefEq.lean
 create mode 100644 tests/lean/unfoldDefEq.lean.expected.out

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 4600383bb0..765f8ec9dd 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -680,9 +680,9 @@ def applySimpResultToProp (mvarId : MVarId) (proof : Expr) (prop : Expr) (r : Si
       else
         return some (proof, r.expr)
 
-def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) : MetaM (Option (Expr × Expr)) := do
+def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (Expr × Expr)) := do
   let localDecl ← getLocalDecl fvarId
-  applySimpResultToProp mvarId (mkFVar fvarId) localDecl.type r
+  applySimpResultToProp mvarId (mkFVar fvarId) localDecl.type r mayCloseGoal
 
 /--
   Simplify `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
@@ -709,8 +709,17 @@ def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Opti
 /--
   Simplify `simp` result to the given local declaration. Return `none` if the goal was closed.
   This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
-def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) : MetaM (Option (FVarId × MVarId)) := do
-  applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r)
+def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (FVarId × MVarId)) := do
+  if r.proof?.isNone then
+    -- New result is definitionally equal to input. Thus, we can avoid creating a new variable if there are dependencies
+    let mvarId ← replaceLocalDeclDefEq mvarId fvarId r.expr
+    if mayCloseGoal && r.expr.isConstOf ``False then
+      assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkFVar fvarId))
+      return none
+    else
+      return some (fvarId, mvarId)
+  else
+    applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
 
 def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option (FVarId × MVarId)) := do
   withMVarContext mvarId do
diff --git a/src/Lean/Meta/Tactic/Unfold.lean b/src/Lean/Meta/Tactic/Unfold.lean
index 3a7b91d06f..89b1dbc569 100644
--- a/src/Lean/Meta/Tactic/Unfold.lean
+++ b/src/Lean/Meta/Tactic/Unfold.lean
@@ -36,7 +36,7 @@ def unfoldTarget (mvarId : MVarId) (declName : Name) : MetaM MVarId := withMVarC
 def unfoldLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declName : Name) : MetaM MVarId := withMVarContext mvarId do
   let localDecl ← getLocalDecl fvarId
   let r ← unfold (← instantiateMVars localDecl.type) declName
-  let some (_, mvarId) ← applySimpResultToLocalDecl mvarId fvarId r | unreachable!
+  let some (_, mvarId) ← applySimpResultToLocalDecl mvarId fvarId r (mayCloseGoal := false) | unreachable!
   return mvarId
 
 end Lean.Meta
diff --git a/tests/lean/unfoldDefEq.lean b/tests/lean/unfoldDefEq.lean
new file mode 100644
index 0000000000..af1e637eec
--- /dev/null
+++ b/tests/lean/unfoldDefEq.lean
@@ -0,0 +1,9 @@
+def Wrapper (n : Nat) : Type × Type :=
+  (Fin n, Fin n)
+
+def some_property {n} (x : Fin n) : Prop :=
+  True
+
+example (x : (Wrapper n).1) (h : some_property x) : True := by
+  unfold Wrapper at x
+  done
diff --git a/tests/lean/unfoldDefEq.lean.expected.out b/tests/lean/unfoldDefEq.lean.expected.out
new file mode 100644
index 0000000000..427137db30
--- /dev/null
+++ b/tests/lean/unfoldDefEq.lean.expected.out
@@ -0,0 +1,5 @@
+unfoldDefEq.lean:9:2-9:6: error: unsolved goals
+n : Nat
+x : (Fin n, Fin n).fst
+h : some_property x
+⊢ True