feat: dsimp! tactic

RELEASES.md

@@ -1,6 +1,9 @@
 Unreleased
 ---------
 
+* Add `dsimp` and `dsimp!` tactics. They guarantee the result term is definitionally equal, and only apply
+  `rfl`-theorems.
+
 * Fix binder information for `match` patterns that use definitions tagged with `[matchPattern]` (e.g., `Nat.add`).
   We now have proper binder information for the variable `y` in the following example.
   ```lean

src/Init/Meta.lean

@@ -1062,12 +1062,17 @@ namespace Parser.Tactic
 macro "erw " s:rwRuleSeq loc:(location)? : tactic =>
   `(rw (config := { transparency := Lean.Meta.TransparencyMode.default }) $s:rwRuleSeq $[$loc:location]?)
 
-macro "declare_simp_like_tactic" opt:(("(" &"all " " := " &"true" ")")?) tacName:ident tacToken:str updateCfg:term : command => do
+syntax simpAllKind := atomic("(" &"all") " := " &"true" ")"
+syntax dsimpKind   := atomic("(" &"dsimp") " := " &"true" ")"
+
+macro "declare_simp_like_tactic" opt:((simpAllKind <|> dsimpKind)?) tacName:ident tacToken:str updateCfg:term : command => do
   let (kind, tkn, stx) ←
     if opt.isNone then
       pure (← `(``simp), ← `("simp "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
-    else
+    else if opt[0].getKind == ``simpAllKind then
       pure (← `(``simpAll), ← `("simp_all "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic))
+    else
+      pure (← `(``dsimp), ← `("dsimp "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
   `($stx:command
     @[macro $tacName:ident] def expandSimp : Macro := fun s => do
       let c ← match s[1][0] with
@@ -1086,6 +1091,8 @@ declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " fun (c : L
 declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true }
 declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true, autoUnfold := true }
 
+declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " fun (c : Lean.Meta.DSimp.Config) => { c with autoUnfold := true }
+
 end Parser.Tactic
 
 end Lean

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

@@ -932,7 +932,7 @@ def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := t
         assignExprMVar mvarId (mkConst ``True.intro)
         return none
       if let some (_, lhs, rhs) := targetNew.eq? then
-        if (← isDefEq lhs rhs) then
+        if (← withReducible <| isDefEq lhs rhs) then
           assignExprMVar mvarId (← mkEqRefl lhs)
           return none
       if target != targetNew then

tests/lean/run/dsimp1.lean

@@ -9,10 +9,16 @@ example (x : Nat) : (1 + id x.succ.pred).isZero = false := by
   simp [Nat.succ_add]
   dsimp [Nat.isZero]
 
+#check Nat.pred_succ
+
+example (x : Nat) : (id x.succ.succ).isZero = false := by
+  dsimp [Nat.isZero]
+
+example (x : Nat) : (id x.succ.succ).isZero = false := by
+  dsimp!
+
 @[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