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

---
 src/Lean/Meta/Tactic/Simp/Main.lean      | 24 ++++++++++++++++++------
 tests/lean/unfoldDefEq.lean              | 10 +++++++++-
 tests/lean/unfoldDefEq.lean.expected.out | 11 ++++++++++-
 3 files changed, 37 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 765f8ec9dd..5c739616bd 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -734,22 +734,34 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
   withMVarContext mvarId do
     checkNotAssigned mvarId `simp
     let mut mvarId := mvarId
-    let mut toAssert : Array Hypothesis := #[]
+    let mut toAssert := #[]
+    let mut replaced := #[]
     for fvarId in fvarIdsToSimp do
       let localDecl ← getLocalDecl fvarId
       let type ← instantiateMVars localDecl.type
       let ctx ← match fvarIdToLemmaId.find? localDecl.fvarId with
         | none => pure ctx
         | some thmId => pure { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem thmId }
-      match (← simpStep mvarId (mkFVar fvarId) type ctx discharge?) with
-      | none => return none
-      | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
-    if simplifyTarget then
+      let r ← simp type ctx discharge?
+      match r.proof? with
+      | some proof => match (← applySimpResultToProp mvarId (mkFVar fvarId) type r) with
+        | none => return none
+        | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
+      | none =>
+        if r.expr.isConstOf ``False then
+          assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkFVar fvarId))
+          return none
+        -- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...`
+        -- Reason: it introduces a `mkExpectedTypeHint`
+        mvarId ← replaceLocalDeclDefEq mvarId fvarId r.expr
+        replaced := replaced.push fvarId
+     if simplifyTarget then
       match (← simpTarget mvarId ctx discharge?) with
       | none => return none
       | some mvarIdNew => mvarId := mvarIdNew
     let (fvarIdsNew, mvarIdNew) ← assertHypotheses mvarId toAssert
-    let mvarIdNew ← tryClearMany mvarIdNew fvarIdsToSimp
+    let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId
+    let mvarIdNew ← tryClearMany mvarIdNew toClear
     return (fvarIdsNew, mvarIdNew)
 
 def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM TacticResultCNM := withMVarContext mvarId do
diff --git a/tests/lean/unfoldDefEq.lean b/tests/lean/unfoldDefEq.lean
index af1e637eec..f03ebafebe 100644
--- a/tests/lean/unfoldDefEq.lean
+++ b/tests/lean/unfoldDefEq.lean
@@ -6,4 +6,12 @@ def some_property {n} (x : Fin n) : Prop :=
 
 example (x : (Wrapper n).1) (h : some_property x) : True := by
   unfold Wrapper at x
-  done
+  trace_state
+  simp at x
+  trace_state
+  sorry
+
+example (x : (Wrapper n).1) (h : some_property x) : True := by
+  simp [Wrapper] at x
+  trace_state
+  sorry
diff --git a/tests/lean/unfoldDefEq.lean.expected.out b/tests/lean/unfoldDefEq.lean.expected.out
index 427137db30..0c6f02fa4e 100644
--- a/tests/lean/unfoldDefEq.lean.expected.out
+++ b/tests/lean/unfoldDefEq.lean.expected.out
@@ -1,5 +1,14 @@
-unfoldDefEq.lean:9:2-9:6: error: unsolved goals
+unfoldDefEq.lean:12:2-12:7: warning: declaration uses 'sorry'
 n : Nat
 x : (Fin n, Fin n).fst
 h : some_property x
 ⊢ True
+n : Nat
+x : Fin n
+h : some_property x
+⊢ True
+unfoldDefEq.lean:17:2-17:7: warning: declaration uses 'sorry'
+n : Nat
+x : Fin n
+h : some_property x
+⊢ True