From 4cfbe6030fc99a6d8481fe53f7b7899883571e5d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Aug 2021 13:40:41 -0700
Subject: [PATCH] feat: add `simpLocalDecl`

---
 src/Lean/Elab/Tactic/Simp.lean      |  2 +-
 src/Lean/Meta/Tactic/Simp/Main.lean | 46 ++++++++++++++++++-----------
 2 files changed, 30 insertions(+), 18 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index c8c3d983c9..f5c3b2e11b 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -181,7 +181,7 @@ private def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ign
 where
   go (ctx : Simp.Context) (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToLemmaId : FVarIdToLemmaId) : TacticM Unit := do
     liftMetaTactic1 fun mvarId =>
-      simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp) (fvarIdToLemmaId := fvarIdToLemmaId)
+      return (← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp) (fvarIdToLemmaId := fvarIdToLemmaId)).map (·.2)
 
 @[builtinTactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => do
   let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (ctx := true) (ignoreStarArg := true)
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index b298144c54..2caadf2490 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -414,26 +414,38 @@ def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context)
       else
         return some (proof, r.expr)
 
-abbrev FVarIdToLemmaId := NameMap Name
-
-def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (fvarIdToLemmaId : FVarIdToLemmaId := {}) : MetaM (Option MVarId) := do
-  let mut mvarId := mvarId
-  let mut toAssert : Array Hypothesis := #[]
-  for fvarId in fvarIdsToSimp do
+def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM (Option (FVarId × MVarId)) := do
+  withMVarContext mvarId do
     let localDecl ← getLocalDecl fvarId
     let type ← instantiateMVars localDecl.type
-    let ctx ← match fvarIdToLemmaId.find? localDecl.fvarId with
-      | none => pure ctx
-      | some lemmaId => pure { ctx with simpLemmas := (← ctx.simpLemmas.eraseCore lemmaId) }
     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
-    match (← simpTarget mvarId ctx discharge?) with
-    | none => return none
-    | some mvarIdNew => mvarId := mvarIdNew
-  let (_, mvarIdNew) ← assertHypotheses mvarId toAssert
-  let mvarIdNew ← tryClearMany mvarIdNew fvarIdsToSimp
-  return mvarIdNew
+    | some (value, type) =>
+      let mvarId ← assert mvarId localDecl.userName type value
+      let mvarId ← tryClear mvarId localDecl.fvarId
+      return some (fvarId, mvarId)
+
+abbrev FVarIdToLemmaId := NameMap Name
+
+def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (fvarIdToLemmaId : FVarIdToLemmaId := {}) : MetaM (Option (Array FVarId × MVarId)) := do
+  withMVarContext mvarId do
+    let mut mvarId := mvarId
+    let mut toAssert : Array Hypothesis := #[]
+    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 lemmaId => pure { ctx with simpLemmas := (← ctx.simpLemmas.eraseCore lemmaId) }
+      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
+      match (← simpTarget mvarId ctx discharge?) with
+      | none => return none
+      | some mvarIdNew => mvarId := mvarIdNew
+    let (fvarIdsNew, mvarIdNew) ← assertHypotheses mvarId toAssert
+    let mvarIdNew ← tryClearMany mvarIdNew fvarIdsToSimp
+    return (fvarIdsNew, mvarIdNew)
 
 end Lean.Meta