feat: dsimp tactic

src/Init/Meta.lean

@@ -994,6 +994,21 @@ inductive TransparencyMode where
   | all | default | reducible | instances
   deriving Inhabited, BEq, Repr
 
+namespace DSimp
+
+structure Config where
+  zeta              : Bool := true
+  beta              : Bool := true
+  eta               : Bool := true
+  etaStruct         : Bool := true
+  iota              : Bool := true
+  proj              : Bool := true
+  decide            : Bool := true
+  autoUnfold        : Bool := false
+  deriving Inhabited, BEq, Repr
+
+end DSimp
+
 namespace Simp
 
 def defaultMaxSteps := 100000

src/Init/Notation.lean

@@ -450,6 +450,12 @@ Only non-dependent propositional hypotheses are considered.
 -/
 syntax (name := simpAll) "simp_all " (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic
 
+/--
+The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but only applies theorems that hold by
+reflexivity. Thus, the result is guaranteed to be definitionally equal to the input.
+-/
+syntax (name := dsimp) "dsimp " (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
+
 /--
   Delta expand the given definition.
   This is a low-level tactic, it will expose how recursive definitions have been compiled by Lean. -/

src/Lean/Elab/Tactic/Simp.lean

@@ -16,6 +16,13 @@ open Meta
 
 declare_config_elab elabSimpConfigCore    Meta.Simp.Config
 declare_config_elab elabSimpConfigCtxCore Meta.Simp.ConfigCtx
+declare_config_elab elabDSimpConfigCore   Meta.DSimp.Config
+
+inductive SimpKind where
+  | simp
+  | simpAll
+  | dsimp
+  deriving Inhabited, BEq
 
 /--
   Implement a `simp` discharge function using the given tactic syntax code.
@@ -72,12 +79,12 @@ private def mkDischargeWrapper (optDischargeSyntax : Syntax) : TacticM Simp.Disc
 
 /-
   `optConfig` is of the form `("(" "config" ":=" term ")")?`
-  If `ctx == false`, the argument is assumed to have type `Meta.Simp.Config`, and `Meta.Simp.ConfigCtx` otherwise. -/
-def elabSimpConfig (optConfig : Syntax) (ctx : Bool) : TermElabM Meta.Simp.Config := do
-  if ctx then
-    return (← elabSimpConfigCtxCore optConfig).toConfig
-  else
-    elabSimpConfigCore optConfig
+-/
+def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TermElabM Meta.Simp.Config := do
+  match kind with
+  | .simp    => elabSimpConfigCore optConfig
+  | .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig
+  | .dsimp   => return { (← elabDSimpConfigCore optConfig) with }
 
 private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (e : Expr) (post : Bool) (inv : Bool) : MetaM Meta.SimpTheorems := do
   if e.isConst then
@@ -189,11 +196,17 @@ structure MkSimpContextResult where
   fvarIdToLemmaId  : FVarIdToLemmaId
 
 /--
-  If `ctx == false`, the config argument is assumed to have type `Meta.Simp.Config`, and `Meta.Simp.ConfigCtx` otherwise.
-  If `ctx == false`, the `discharge` option must be none -/
-def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ignoreStarArg : Bool := false) : TacticM MkSimpContextResult := do
-  if ctx && !stx[2].isNone then
-    throwError "'simp_all' tactic does not support 'discharger' option"
+   Create the `Simp.Context` for the `simp`, `dsimp`, and `simp_all` tactics.
+   If `kind != SimpKind.simp`, the `discharge` option must be `none`
+
+   TODO: generate error message if non `rfl` theorems are provided as arguments to `dsimp`.
+-/
+def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ignoreStarArg : Bool := false) : TacticM MkSimpContextResult := do
+  if !stx[2].isNone then
+    if kind == SimpKind.simpAll then
+      throwError "'simp_all' tactic does not support 'discharger' option"
+    if kind == SimpKind.dsimp then
+      throwError "'dsimp' tactic does not support 'discharger' option"
   let dischargeWrapper ← mkDischargeWrapper stx[2]
   let simpOnly := !stx[3].isNone
   let simpTheorems ←
@@ -203,7 +216,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ignoreStarA
       getSimpTheorems
   let congrTheorems ← getSimpCongrTheorems
   let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) {
-    config      := (← elabSimpConfig stx[1] (ctx := ctx))
+    config      := (← elabSimpConfig stx[1] (kind := kind))
     simpTheorems := #[simpTheorems], congrTheorems
   }
   if !r.starArg || ignoreStarArg then
@@ -266,9 +279,30 @@ where
     simpLocation ctx discharge? fvarIdToLemmaId (expandOptLocation stx[5])
 
 @[builtinTactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => do
-  let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (ctx := true) (ignoreStarArg := true)
+  let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
   match (← simpAll (← getMainGoal) ctx) with
   | none => replaceMainGoal []
   | some mvarId => replaceMainGoal [mvarId]
 
+def dsimpLocation (ctx : Simp.Context) (fvarIdToSimp : FVarIdToLemmaId := {}) (loc : Location) : TacticM Unit := do
+  match loc with
+  | Location.targets hyps simplifyTarget =>
+    withMainContext do
+      let fvarIds ← getFVarIds hyps
+      go fvarIds simplifyTarget fvarIdToSimp
+  | Location.wildcard =>
+    withMainContext do
+      go (← getNondepPropHyps (← getMainGoal)) (simplifyTarget := true) fvarIdToSimp
+where
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToSimp : Lean.Meta.FVarIdToLemmaId) : TacticM Unit := do
+    let mvarId ← getMainGoal
+    let result? ← dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
+    match result? with
+    | none => replaceMainGoal []
+    | some mvarId => replaceMainGoal [mvarId]
+
+@[builtinTactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do
+  let { ctx, fvarIdToLemmaId, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
+  dsimpLocation ctx fvarIdToLemmaId (expandOptLocation stx[5])
+
 end Lean.Elab.Tactic

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -688,6 +688,13 @@ def main (e : Expr) (ctx : Context) (methods : Methods := {}) : MetaM Result :=
     catch ex =>
       if ex.isMaxHeartbeat then throwNestedTacticEx `simp ex else throw ex
 
+def dsimpMain (e : Expr) (ctx : Context) (methods : Methods := {}) : MetaM Expr := do
+  withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
+    try
+      dsimp e methods ctx |>.run' {}
+    catch ex =>
+      if ex.isMaxHeartbeat then throwNestedTacticEx `dsimp ex else throw ex
+
 partial def isEqnThmHypothesis (e : Expr) : Bool :=
   e.isForall && go e
 where
@@ -750,6 +757,9 @@ def simp (e : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge :=
   | 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 })
 
+def dsimp (e : Expr) (ctx : Simp.Context) : MetaM Expr := do profileitM Exception "dsimp" (← getOptions) do
+  Simp.dsimpMain e ctx (methods := Simp.DefaultMethods.methods)
+
 /--
   Auxiliary method.
   Given the current `target` of `mvarId`, apply `r` which is a new target and proof that it is equaal to the current one.
@@ -878,7 +888,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
         -- Reason: it introduces a `mkExpectedTypeHint`
         mvarId ← replaceLocalDeclDefEq mvarId fvarId r.expr
         replaced := replaced.push fvarId
-     if simplifyTarget then
+    if simplifyTarget then
       match (← simpTarget mvarId ctx discharge?) with
       | none => return none
       | some mvarIdNew => mvarId := mvarIdNew
@@ -902,4 +912,31 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option S
     else
       return TacticResultCNM.modified mvarId'
 
+def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) : MetaM (Option MVarId) := do
+  withMVarContext mvarId do
+    checkNotAssigned mvarId `simp
+    let mut mvarId := mvarId
+    for fvarId in fvarIdsToSimp do
+      let localDecl ← getLocalDecl fvarId
+      let type ← instantiateMVars localDecl.type
+      let typeNew ← dsimp type ctx
+      if typeNew.isConstOf ``False then
+        assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkFVar fvarId))
+        return none
+      if typeNew != type then
+        mvarId ← replaceLocalDeclDefEq mvarId fvarId typeNew
+    if simplifyTarget then
+      let target ← getMVarType mvarId
+      let targetNew ← dsimp target ctx
+      if targetNew.isConstOf ``True then
+        assignExprMVar mvarId (mkConst ``True.intro)
+        return none
+      if let some (_, lhs, rhs) := targetNew.eq? then
+        if (← isDefEq lhs rhs) then
+          assignExprMVar mvarId (← mkEqRefl lhs)
+          return none
+      if target != targetNew then
+        mvarId ← replaceTargetDefEq mvarId targetNew
+    return some mvarId
+
 end Lean.Meta

tests/lean/run/dsimp1.lean

@@ -0,0 +1,18 @@
+def Nat.isZero (x : Nat) : Bool :=
+  match x with
+  | 0 => true
+  | x+1 => false
+
+example (x : Nat) : (1 + id x.succ.pred).isZero = false := by
+  dsimp
+  trace_state
+  simp [Nat.succ_add]
+  dsimp [Nat.isZero]
+
+@[simp] theorem isZero_succ (x : Nat) : (x + 1).isZero = false :=
+  rfl
+
+theorem ex1 (x : Nat) : (id x.succ.succ.pred).isZero = false := by
+  dsimp
+
+#print ex1