1 files changed, 16 insertions, 6 deletions
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index eacfe72b..7ae5a832 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -658,6 +658,12 @@ example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by
   rename_i x y z
   exists x + y + z
 
+/- Initialize a context for the `simp` function.
+
+   The initialization of the context is adapted from `Tactic.elabSimpArgs`.
+   Something very annoying is that there is no function which allows to
+   initialize a simp context without doing an elaboration - as a consequence
+   we write our own here. -/
 def mkSimpCtx (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
   Tactic.TacticM Simp.Context := do
   -- Initialize either with the builtin simp theorems or with all the simp theorems
@@ -689,7 +695,6 @@ def mkSimpCtx (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (
   let congrTheorems ← getSimpCongrTheorems
   pure { simpTheorems := #[simpThms], congrTheorems }
 
-
 inductive Location where
   /-- Apply the tactic everywhere. Same as `Tactic.Location.wildcard` -/
   | wildcard
@@ -725,11 +730,7 @@ where
     | some (_, mvarId) => replaceMainGoal [mvarId]
     return usedSimps
 
-/- Call the simp tactic.
-   The initialization of the context is adapted from Tactic.elabSimpArgs.
-   Something very annoying is that there is no function which allows to
-   initialize a simp context without doing an elaboration - as a consequence
-   we write our own here. -/
+/- Call the simp tactic. -/
 def simpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
   (loc : Location) :
   Tactic.TacticM Unit := do
@@ -738,6 +739,15 @@ def simpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hyp
   -- Apply the simplifier
   let _ ← customSimpLocation ctx (discharge? := .none) loc
 
+/- Call the dsimp tactic. -/
+def dsimpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
+  (loc : Tactic.Location) :
+  Tactic.TacticM Unit := do
+  -- Initialize the simp context
+  let ctx ← mkSimpCtx simpOnly declsToUnfold thms hypsToUse
+  -- Apply the simplifier
+  dsimpLocation ctx loc
+
 -- Call the simpAll tactic
 def simpAll (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
   Tactic.TacticM Unit := do