From 0961561d4e8e589406654708f681e1bdb4151cef Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 19 Sep 2022 20:00:05 -0400
Subject: [PATCH] feat: track simp lemmas through the core tactics

---
 .../Elab/PreDefinition/Structural/Eqns.lean   |   2 +-
 src/Lean/Elab/PreDefinition/WF/Eqns.lean      |   4 +-
 src/Lean/Elab/Tactic/Conv/Pattern.lean        |   2 +-
 src/Lean/Elab/Tactic/Conv/Simp.lean           |   2 +-
 src/Lean/Elab/Tactic/Simp.lean                |  13 ++-
 src/Lean/Meta/Tactic/AC/Main.lean             |   2 +-
 src/Lean/Meta/Tactic/Acyclic.lean             |   2 +-
 src/Lean/Meta/Tactic/Simp/Main.lean           | 103 +++++++++++-------
 src/Lean/Meta/Tactic/Simp/Rewrite.lean        |   1 +
 src/Lean/Meta/Tactic/Simp/SimpAll.lean        |  22 ++--
 src/Lean/Meta/Tactic/Simp/Types.lean          |  10 +-
 src/Lean/Meta/Tactic/Split.lean               |   4 +-
 src/Lean/Meta/Tactic/SplitIf.lean             |   4 +-
 src/Lean/Meta/Tactic/Unfold.lean              |   2 +-
 tests/lean/1079.lean.expected.out             |   2 +-
 tests/lean/run/simp1.lean                     |   2 +-
 16 files changed, 105 insertions(+), 72 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index 707814cbe8..6eb2de8a50 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -42,7 +42,7 @@ where
       go mvarId
     else if let some mvarId ← whnfReducibleLHS? mvarId then
       go mvarId
-    else match (← simpTargetStar mvarId {}) with
+    else match (← simpTargetStar mvarId {}).1 with
       | TacticResultCNM.closed => return ()
       | TacticResultCNM.modified mvarId => go mvarId
       | TacticResultCNM.noChange =>
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index c29d49fbf7..df87a094b3 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -105,7 +105,7 @@ where
 def simpMatchWF? (info : EqnInfo) (us : List Level) (fixedPrefix : Array Expr) (mvarId : MVarId) : MetaM (Option MVarId) :=
   mvarId.withContext do
     let target ← instantiateMVars (← mvarId.getType)
-    let targetNew ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre })
+    let (targetNew, _) ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre })
     let mvarIdNew ← applySimpResultToTarget mvarId target targetNew
     if mvarId != mvarIdNew then return some mvarIdNew else return none
 where
@@ -169,7 +169,7 @@ private partial def mkProof (declName : Name) (info : EqnInfo) (type : Expr) : M
         go mvarId
       else if let some mvarId ← whnfReducibleLHS? mvarId then
         go mvarId
-      else match (← simpTargetStar mvarId { config.dsimp := false }) with
+      else match (← simpTargetStar mvarId { config.dsimp := false }).1 with
         | TacticResultCNM.closed => return ()
         | TacticResultCNM.modified mvarId => go mvarId
         | TacticResultCNM.noChange =>
diff --git a/src/Lean/Elab/Tactic/Conv/Pattern.lean b/src/Lean/Elab/Tactic/Conv/Pattern.lean
index 54c909de6d..e32d8cfc3f 100644
--- a/src/Lean/Elab/Tactic/Conv/Pattern.lean
+++ b/src/Lean/Elab/Tactic/Conv/Pattern.lean
@@ -48,7 +48,7 @@ private def pre (pattern : AbstractMVarsResult) (found? : IO.Ref (Option Expr))
 
 private def findPattern? (pattern : AbstractMVarsResult) (e : Expr) : MetaM (Option (MVarId × Simp.Result)) := do
   let found? ← IO.mkRef none
-  let result ← Simp.main e (← getContext) (methods := { pre := pre pattern found? })
+  let (result, _) ← Simp.main e (← getContext) (methods := { pre := pre pattern found? })
   if let some newGoal ← found?.get then
     return some (newGoal.mvarId!, result)
   else
diff --git a/src/Lean/Elab/Tactic/Conv/Simp.lean b/src/Lean/Elab/Tactic/Conv/Simp.lean
index a3fdedbb96..34f479de08 100644
--- a/src/Lean/Elab/Tactic/Conv/Simp.lean
+++ b/src/Lean/Elab/Tactic/Conv/Simp.lean
@@ -19,7 +19,7 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
 @[builtinTactic Lean.Parser.Tactic.Conv.simp] def evalSimp : Tactic := fun stx => withMainContext do
   let { ctx, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
   let lhs ← getLhs
-  let result ← dischargeWrapper.with fun d? => simp lhs ctx (discharge? := d?)
+  let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (discharge? := d?)
   applySimpResult result
 
 @[builtinTactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun _ => withMainContext do
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 3cecb29d76..f27063c717 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -265,7 +265,7 @@ For many tactics other than the simplifier,
 one should use the `withLocation` tactic combinator
 when working with a `location`.
 -/
-def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (fvarIdToLemmaId : FVarIdToLemmaId := {}) (loc : Location) : TacticM Unit := do
+def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (fvarIdToLemmaId : FVarIdToLemmaId := {}) (loc : Location) : TacticM NameSet := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -275,24 +275,25 @@ def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := non
     withMainContext do
       go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true) fvarIdToLemmaId
 where
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToLemmaId : Lean.Meta.FVarIdToLemmaId) : TacticM Unit := do
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToLemmaId : Lean.Meta.FVarIdToLemmaId) : TacticM NameSet := do
     let mvarId ← getMainGoal
-    let result? ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp) (fvarIdToLemmaId := fvarIdToLemmaId)
+    let (result?, usedSimps) ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp) (fvarIdToLemmaId := fvarIdToLemmaId)
     match result? with
     | none => replaceMainGoal []
     | some (_, mvarId) => replaceMainGoal [mvarId]
+    return usedSimps
 
 /-
   "simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)?
 -/
 @[builtinTactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
   let { ctx, fvarIdToLemmaId, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
-  dischargeWrapper.with fun discharge? =>
+  discard <| dischargeWrapper.with fun discharge? =>
     simpLocation ctx discharge? fvarIdToLemmaId (expandOptLocation stx[5])
 
 @[builtinTactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => do
   let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
-  match (← simpAll (← getMainGoal) ctx) with
+  match (← simpAll (← getMainGoal) ctx).1 with
   | none => replaceMainGoal []
   | some mvarId => replaceMainGoal [mvarId]
 
@@ -308,7 +309,7 @@ def dsimpLocation (ctx : Simp.Context) (loc : Location) : TacticM Unit := do
 where
   go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := do
     let mvarId ← getMainGoal
-    let result? ← dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
+    let (result?, _) ← dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean
index cddd710178..d9e8e08b56 100644
--- a/src/Lean/Meta/Tactic/AC/Main.lean
+++ b/src/Lean/Meta/Tactic/AC/Main.lean
@@ -145,7 +145,7 @@ def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do
       config        := Simp.neutralConfig
     }
   let tgt ← instantiateMVars (← mvarId.getType)
-  let res ← Simp.main tgt simpCtx (methods := { post })
+  let (res, _) ← Simp.main tgt simpCtx (methods := { post })
   let newGoal ← applySimpResultToTarget mvarId tgt res
   newGoal.refl
 where
diff --git a/src/Lean/Meta/Tactic/Acyclic.lean b/src/Lean/Meta/Tactic/Acyclic.lean
index 58de1b70ce..2d6c581507 100644
--- a/src/Lean/Meta/Tactic/Acyclic.lean
+++ b/src/Lean/Meta/Tactic/Acyclic.lean
@@ -37,7 +37,7 @@ where
       let sizeOfEq ← mkLT sizeOf_lhs sizeOf_rhs
       let hlt ← mkFreshExprSyntheticOpaqueMVar sizeOfEq
       -- TODO: we only need the `sizeOf` simp theorems
-      match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] }) with
+      match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] }).1 with
       | some _ => return false
       | none   =>
         let heq ← mkCongrArg sizeOf_lhs.appFn! (← mkEqSymm h)
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 0e2d459ee3..47feb16eb7 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -165,7 +165,9 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
     | some e => return (← reduce e)
     | none   => pure ()
   match (← unfold? e) with
-  | some e => reduce e
+  | some e' =>
+    recordSimpTheorem e.getAppFn.constName!
+    reduce e'
   | none => return e
 
 private partial def dsimp (e : Expr) : M Expr := do
@@ -687,18 +689,20 @@ where
       modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
     return r
 
-def main (e : Expr) (ctx : Context) (methods : Methods := {}) : MetaM Result := do
+def main (e : Expr) (ctx : Context) (usedSimps : NameSet := {}) (methods : Methods := {}) : MetaM (Result × NameSet) := do
   let ctx := { ctx with config := (← ctx.config.updateArith) }
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
     try
-      simp e methods ctx |>.run' {}
+      let (r, s) ← simp e methods ctx |>.run { usedTheorems := usedSimps }
+      pure (r, s.usedTheorems)
     catch ex =>
       if ex.isMaxHeartbeat then throwNestedTacticEx `simp ex else throw ex
 
-def dsimpMain (e : Expr) (ctx : Context) (methods : Methods := {}) : MetaM Expr := do
+def dsimpMain (e : Expr) (ctx : Context) (usedSimps : NameSet := {}) (methods : Methods := {}) : MetaM (Expr × NameSet) := do
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
     try
-      dsimp e methods ctx |>.run' {}
+      let (r, s) ← dsimp e methods ctx |>.run { usedTheorems := usedSimps }
+      pure (r, s.usedTheorems)
     catch ex =>
       if ex.isMaxHeartbeat then throwNestedTacticEx `dsimp ex else throw ex
 
@@ -806,13 +810,15 @@ end DefaultMethods
 
 end Simp
 
-def simp (e : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM Simp.Result := do profileitM Exception "simp" (← getOptions) do
+def simp (e : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
+    (usedSimps : NameSet := {}) : MetaM (Simp.Result × NameSet) := do profileitM Exception "simp" (← getOptions) do
   match discharge? with
-  | none   => Simp.main e ctx (methods := Simp.DefaultMethods.methods)
-  | some d => Simp.main e ctx (methods := { pre := (Simp.preDefault · d), post := (Simp.postDefault · d), discharge? := d })
+  | none   => Simp.main e ctx usedSimps (methods := Simp.DefaultMethods.methods)
+  | some d => Simp.main e ctx usedSimps (methods := { pre := (Simp.preDefault · d), post := (Simp.postDefault · d), discharge? := d })
 
-def dsimp (e : Expr) (ctx : Simp.Context) : MetaM Expr := do profileitM Exception "dsimp" (← getOptions) do
-  Simp.dsimpMain e ctx (methods := Simp.DefaultMethods.methods)
+def dsimp (e : Expr) (ctx : Simp.Context)
+    (usedSimps : NameSet := {}) : MetaM (Expr × NameSet) := do profileitM Exception "dsimp" (← getOptions) do
+  Simp.dsimpMain e ctx usedSimps (methods := Simp.DefaultMethods.methods)
 
 /--
   Auxiliary method.
@@ -828,24 +834,26 @@ def applySimpResultToTarget (mvarId : MVarId) (target : Expr) (r : Simp.Result)
       return mvarId
 
 /-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
-def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option MVarId) := do
+def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
+    (mayCloseGoal := true) (usedSimps : NameSet := {}) : MetaM (Option MVarId × NameSet) := do
   let target ← instantiateMVars (← mvarId.getType)
-  let r ← simp target ctx discharge?
+  let (r, usedSimps) ← simp target ctx discharge? usedSimps
   if mayCloseGoal && r.expr.isConstOf ``True then
     match r.proof? with
     | some proof => mvarId.assign (← mkOfEqTrue proof)
     | none => mvarId.assign (mkConst ``True.intro)
-    return none
+    return (none, usedSimps)
   else
-    applySimpResultToTarget mvarId target r
+    return (← applySimpResultToTarget mvarId target r, usedSimps)
 
 /--
   Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise,
   where `mvarId'` is the simplified new goal. -/
-def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option MVarId) :=
+def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
+    (mayCloseGoal := true) (usedSimps : NameSet := {}) : MetaM (Option MVarId × NameSet) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
-    simpTargetCore mvarId ctx discharge? mayCloseGoal
+    simpTargetCore mvarId ctx discharge? mayCloseGoal usedSimps
 
 /--
   Apply the result `r` for `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
@@ -876,9 +884,10 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
   otherwise, where `proof' : prop'` and `prop'` is the simplified `prop`.
 
   This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
-def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option (Expr × Expr)) := do
-  let r ← simp prop ctx discharge?
-  applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal)
+def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
+    (mayCloseGoal := true) (usedSimps : NameSet := {}) : MetaM (Option (Expr × Expr) × NameSet) := do
+  let (r, usedSimps) ← simp prop ctx discharge? usedSimps
+  return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
 
 def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId)) := do
   match r with
@@ -908,87 +917,99 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
   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
+def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
+    (mayCloseGoal := true) (usedSimps : NameSet := {}) : MetaM (Option (FVarId × MVarId) × NameSet) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let type ← instantiateMVars (← fvarId.getType)
-    applySimpResultToLocalDeclCore mvarId fvarId (← simpStep mvarId (mkFVar fvarId) type ctx discharge? mayCloseGoal)
+    let (r, usedSimps) ← simpStep mvarId (mkFVar fvarId) type ctx discharge? mayCloseGoal usedSimps
+    return (← applySimpResultToLocalDeclCore mvarId fvarId r, usedSimps)
 
 abbrev FVarIdToLemmaId := FVarIdMap 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
+def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
+    (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (fvarIdToLemmaId : FVarIdToLemmaId := {})
+    (usedSimps : NameSet := {}) : MetaM (Option (Array FVarId × MVarId) × NameSet) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let mut mvarId := mvarId
     let mut toAssert := #[]
     let mut replaced := #[]
+    let mut usedSimps := usedSimps
     for fvarId in fvarIdsToSimp do
       let localDecl ← fvarId.getDecl
       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 }
-      let r ← simp type ctx discharge?
+      let (r, usedSimps') ← simp type ctx discharge? usedSimps
+      usedSimps := usedSimps'
       match r.proof? with
       | some _ => match (← applySimpResultToProp mvarId (mkFVar fvarId) type r) with
-        | none => return none
+        | none => return (none, usedSimps)
         | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
       | none =>
         if r.expr.isConstOf ``False then
           mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId))
-          return none
+          return (none, usedSimps)
         -- 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 ← mvarId.replaceLocalDeclDefEq fvarId r.expr
         replaced := replaced.push fvarId
     if simplifyTarget then
       match (← simpTarget mvarId ctx discharge?) with
-      | none => return none
-      | some mvarIdNew => mvarId := mvarIdNew
+      | (none, usedSimps') => return (none, usedSimps')
+      | (some mvarIdNew, usedSimps') => mvarId := mvarIdNew; usedSimps := usedSimps'
     let (fvarIdsNew, mvarIdNew) ← mvarId.assertHypotheses toAssert
     let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId
     let mvarIdNew ← mvarIdNew.tryClearMany toClear
-    return (fvarIdsNew, mvarIdNew)
+    return (some (fvarIdsNew, mvarIdNew), usedSimps)
 
-def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM TacticResultCNM := mvarId.withContext do
+def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
+    (usedSimps : NameSet := {}) : MetaM (TacticResultCNM × NameSet) := mvarId.withContext do
   let mut ctx := ctx
   for h in (← getPropHyps) do
     let localDecl ← h.getDecl
     let proof  := localDecl.toExpr
     let simpTheorems ← ctx.simpTheorems.addTheorem localDecl.fvarId.name proof
     ctx := { ctx with simpTheorems }
-  match (← simpTarget mvarId ctx discharge?) with
-  | none => return TacticResultCNM.closed
-  | some mvarId' =>
+  match (← simpTarget mvarId ctx discharge? (usedSimps := usedSimps)) with
+  | (none, usedSimps) => return (TacticResultCNM.closed, usedSimps)
+  | (some mvarId', usedSimps') =>
     if (← mvarId.getType) == (← mvarId'.getType) then
-      return TacticResultCNM.noChange
+      return (TacticResultCNM.noChange, usedSimps)
     else
-      return TacticResultCNM.modified mvarId'
+      return (TacticResultCNM.modified mvarId', usedSimps')
 
-def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) : MetaM (Option MVarId) := do
+def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
+    (usedSimps : NameSet := {}) : MetaM (Option MVarId × NameSet) := do
    mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let mut mvarId := mvarId
+    let mut usedSimps : NameSet := usedSimps
     for fvarId in fvarIdsToSimp do
       let type ← instantiateMVars (← fvarId.getType)
-      let typeNew ← dsimp type ctx
+      let (typeNew, usedSimps') ← dsimp type ctx
+      usedSimps := usedSimps'
       if typeNew.isConstOf ``False then
         mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId))
-        return none
+        return (none, usedSimps)
       if typeNew != type then
         mvarId ← mvarId.replaceLocalDeclDefEq fvarId typeNew
     if simplifyTarget then
       let target ← mvarId.getType
-      let targetNew ← dsimp target ctx
+      let (targetNew, usedSimps') ← dsimp target ctx usedSimps
+      usedSimps := usedSimps'
       if targetNew.isConstOf ``True then
         mvarId.assign (mkConst ``True.intro)
-        return none
+        return (none, usedSimps)
       if let some (_, lhs, rhs) := targetNew.eq? then
         if (← withReducible <| isDefEq lhs rhs) then
           mvarId.assign (← mkEqRefl lhs)
-          return none
+          return (none, usedSimps)
       if target != targetNew then
         mvarId ← mvarId.replaceTargetDefEq targetNew
-    return some mvarId
+      pure () -- FIXME: bug in do notation if this is removed?
+    return (some mvarId, usedSimps)
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 0bcb72430a..6604bba622 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -73,6 +73,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
           trace[Meta.Tactic.simp.rewrite] "{thm}, perm rejected {e} ==> {rhs}"
           return none
       trace[Meta.Tactic.simp.rewrite] "{thm}, {e} ==> {rhs}"
+      recordSimpTheorem thm.name
       return some { expr := rhs, proof? }
     else
       unless lhs.isMVar do
diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
index b0d1b7043c..a696fba065 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
@@ -20,10 +20,11 @@ structure Entry where
   deriving Inhabited
 
 structure State where
-  modified : Bool := false
-  mvarId   : MVarId
-  entries  : Array Entry := #[]
-  ctx      : Simp.Context
+  modified  : Bool := false
+  mvarId    : MVarId
+  entries   : Array Entry := #[]
+  ctx       : Simp.Context
+  usedSimps : NameSet := {}
 
 abbrev M := StateRefT State MetaM
 
@@ -56,7 +57,9 @@ private partial def loop : M Bool := do
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
     let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
-    match (← simpStep (← get).mvarId entry.proof entry.type ctx) with
+    let (r, usedSimps) ← simpStep (← get).mvarId entry.proof entry.type ctx (usedSimps := (← get).usedSimps)
+    modify fun s => { s with usedSimps }
+    match r with
     | none => return true -- closed the goal
     | some (proofNew, typeNew) =>
       unless typeNew == entry.type do
@@ -94,7 +97,9 @@ private partial def loop : M Bool := do
         }
   -- simplify target
   let mvarId := (← get).mvarId
-  match (← simpTarget mvarId (← get).ctx) with
+  let (r, usedSimps) ← simpTarget mvarId (← get).ctx (usedSimps := (← get).usedSimps)
+  modify fun s => { s with usedSimps }
+  match r with
   | none => return true
   | some mvarIdNew =>
     unless mvarId == mvarIdNew do
@@ -121,8 +126,9 @@ def main : M (Option MVarId) := do
 
 end SimpAll
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) : MetaM (Option MVarId) := do
+def simpAll (mvarId : MVarId) (ctx : Simp.Context) (usedSimps : NameSet := {}) : MetaM (Option MVarId × NameSet) := do
   mvarId.withContext do
-    SimpAll.main.run' { mvarId := mvarId, ctx := ctx }
+    let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps }
+    return (r, s.usedSimps)
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index ee10264a05..ae20933539 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -37,9 +37,10 @@ def Context.mkDefault : MetaM Context :=
   return { config := {}, simpTheorems := #[(← getSimpTheorems)], congrTheorems := (← getSimpCongrTheorems) }
 
 structure State where
-  cache      : Cache := {}
-  congrCache : CongrCache := {}
-  numSteps   : Nat := 0
+  cache        : Cache := {}
+  congrCache   : CongrCache := {}
+  usedTheorems : NameSet := {}
+  numSteps     : Nat := 0
 
 abbrev SimpM := ReaderT Context $ StateRefT State MetaM
 
@@ -98,6 +99,9 @@ def getSimpCongrTheorems : M SimpCongrTheorems :=
   finally
     modify fun s => { s with cache := cacheSaved }
 
+def recordSimpTheorem (n : Name) : SimpM Unit :=
+  modify fun s => { s with usedTheorems := s.usedTheorems.insert n }
+
 end Simp
 
 export Simp (SimpM)
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index 0bb9af1238..e6e2ddd7b9 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -17,7 +17,7 @@ def getSimpMatchContext : MetaM Simp.Context :=
    }
 
 def simpMatch (e : Expr) : MetaM Simp.Result := do
-  Simp.main e (← getSimpMatchContext) (methods := { pre })
+  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre })
 where
   pre (e : Expr) : SimpM Simp.Step := do
     let some app ← matchMatcherApp? e | return Simp.Step.visit { expr := e }
@@ -35,7 +35,7 @@ def simpMatchTarget (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   applySimpResultToTarget mvarId target r
 
 private def simpMatchCore (matchDeclName : Name) (matchEqDeclName : Name) (e : Expr) : MetaM Simp.Result := do
-  Simp.main e (← getSimpMatchContext) (methods := { pre })
+  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre })
 where
   pre (e : Expr) : SimpM Simp.Step := do
     if e.isAppOf matchDeclName then
diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
index 7e655355af..0bba1d84d0 100644
--- a/src/Lean/Meta/Tactic/SplitIf.lean
+++ b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -82,14 +82,14 @@ open SplitIf
 
 def simpIfTarget (mvarId : MVarId) (useDecide := false) : MetaM MVarId := do
   let mut ctx ← getSimpContext
-  if let some mvarId' ← simpTarget mvarId ctx (discharge? useDecide) (mayCloseGoal := false) then
+  if let (some mvarId', _) ← simpTarget mvarId ctx (discharge? useDecide) (mayCloseGoal := false) then
     return mvarId'
   else
     unreachable!
 
 def simpIfLocalDecl (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do
   let mut ctx ← getSimpContext
-  if let some (_, mvarId') ← simpLocalDecl mvarId fvarId ctx discharge? (mayCloseGoal := false) then
+  if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx discharge? (mayCloseGoal := false) then
     return mvarId'
   else
     unreachable!
diff --git a/src/Lean/Meta/Tactic/Unfold.lean b/src/Lean/Meta/Tactic/Unfold.lean
index e95f4a3eac..b85a1a8e4d 100644
--- a/src/Lean/Meta/Tactic/Unfold.lean
+++ b/src/Lean/Meta/Tactic/Unfold.lean
@@ -17,7 +17,7 @@ private def getSimpUnfoldContext : MetaM Simp.Context :=
 
 def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
   if let some unfoldThm ← getUnfoldEqnFor? declName  then
-    Simp.main e (← getSimpUnfoldContext) (methods := { pre := pre unfoldThm })
+    (·.1) <$> Simp.main e (← getSimpUnfoldContext) (methods := { pre := pre unfoldThm })
   else
     return { expr  := (← deltaExpand e (· == declName)) }
 where
diff --git a/tests/lean/1079.lean.expected.out b/tests/lean/1079.lean.expected.out
index 36423069da..3db1085ef9 100644
--- a/tests/lean/1079.lean.expected.out
+++ b/tests/lean/1079.lean.expected.out
@@ -1,5 +1,5 @@
 1079.lean:3:2-6:12: error: alternative 'isFalse' has not been provided
-[Meta.Tactic.simp.rewrite] h:1000, m ==> n
+[Meta.Tactic.simp.rewrite] _uniq.82:1000, m ==> n
 [Meta.Tactic.simp.rewrite] eq_self:1000, n = n ==> True
 [Meta.Tactic.simp.unify] ite_self:1000, failed to unify
       if ?c then ?a else ?a
diff --git a/tests/lean/run/simp1.lean b/tests/lean/run/simp1.lean
index 559bf93981..c05ba2106d 100644
--- a/tests/lean/run/simp1.lean
+++ b/tests/lean/run/simp1.lean
@@ -46,7 +46,7 @@ def tst2 : MetaM Unit := do
       let s ← Meta.getSimpTheorems
       let m ← s.post.getMatch lhs
       trace[Meta.debug] "result: {m}"
-      assert! m.any fun s => s.name? == `ex2
+      assert! m.any fun s => s.name == `ex2
 
 
 set_option trace.Meta.debug true in