chore: update stage0

Simplification procedures that produce definitionally equal results.

WIP

src/Init/Simproc.lean

@@ -31,22 +31,43 @@ Simplification procedures can be also scoped or local.
 -/
 syntax (docComment)? attrKind "simproc " (Tactic.simpPre <|> Tactic.simpPost)? ("[" ident,* "]")? ident " (" term ")" " := " term : command
 
+/--
+Similar to `simproc`, but resulting expression must be definitionally equal to the input one.
+-/
+syntax (docComment)? attrKind "dsimproc " (Tactic.simpPre <|> Tactic.simpPost)? ("[" ident,* "]")? ident " (" term ")" " := " term : command
+
 /--
 A user-defined simplification procedure declaration. To activate this procedure in `simp` tactic,
 we must provide it as an argument, or use the command `attribute` to set its `[simproc]` attribute.
 -/
 syntax (docComment)? "simproc_decl " ident " (" term ")" " := " term : command
 
+/--
+A user-defined defeq simplification procedure declaration. To activate this procedure in `simp` tactic,
+we must provide it as an argument, or use the command `attribute` to set its `[simproc]` attribute.
+-/
+syntax (docComment)? "dsimproc_decl " ident " (" term ")" " := " term : command
+
 /--
 A builtin simplification procedure.
 -/
 syntax (docComment)? attrKind "builtin_simproc " (Tactic.simpPre <|> Tactic.simpPost)? ("[" ident,* "]")? ident " (" term ")" " := " term : command
 
+/--
+A builtin defeq simplification procedure.
+-/
+syntax (docComment)? attrKind "builtin_dsimproc " (Tactic.simpPre <|> Tactic.simpPost)? ("[" ident,* "]")? ident " (" term ")" " := " term : command
+
 /--
 A builtin simplification procedure declaration.
 -/
 syntax (docComment)? "builtin_simproc_decl " ident " (" term ")" " := " term : command
 
+/--
+A builtin defeq simplification procedure declaration.
+-/
+syntax (docComment)? "builtin_dsimproc_decl " ident " (" term ")" " := " term : command
+
 /--
 Auxiliary command for associating a pattern with a simplification procedure.
 -/
@@ -86,33 +107,60 @@ macro_rules
     `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
       simproc_pattern% $pattern => $n)
 
+macro_rules
+  | `($[$doc?:docComment]? dsimproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Simp.DSimproc
+    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+      simproc_pattern% $pattern => $n)
+
 macro_rules
   | `($[$doc?:docComment]? builtin_simproc_decl $n:ident ($pattern:term) := $body) => do
     let simprocType := `Lean.Meta.Simp.Simproc
     `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
       builtin_simproc_pattern% $pattern => $n)
 
+macro_rules
+  | `($[$doc?:docComment]? builtin_dsimproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Simp.DSimproc
+    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+      builtin_simproc_pattern% $pattern => $n)
+
+private def mkAttributeCmds
+    (kind : TSyntax `Lean.Parser.Term.attrKind)
+    (pre? : Option (TSyntax [`Lean.Parser.Tactic.simpPre, `Lean.Parser.Tactic.simpPost]))
+    (ids? : Option (Syntax.TSepArray `ident ","))
+    (n : Ident) : MacroM (Array Syntax) := do
+  let mut cmds := #[]
+  let pushDefault (cmds : Array (TSyntax `command)) : MacroM (Array (TSyntax `command)) := do
+    return cmds.push (← `(attribute [$kind simproc $[$pre?]?] $n))
+  if let some ids := ids? then
+    for id in ids.getElems do
+      let idName := id.getId
+      let (attrName, attrKey) :=
+        if idName == `simp then
+          (`simprocAttr, "simproc")
+        else if idName == `seval then
+          (`sevalprocAttr, "sevalproc")
+        else
+          let idName := idName.appendAfter "_proc"
+          (`Parser.Attr ++ idName, idName.toString)
+      let attrStx : TSyntax `attr := ⟨mkNode attrName #[mkAtom attrKey, mkOptionalNode pre?]⟩
+      cmds := cmds.push (← `(attribute [$kind $attrStx] $n))
+  else
+    cmds ← pushDefault cmds
+  return cmds
+
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind simproc $[$pre?]? $[ [ $ids?:ident,* ] ]? $n:ident ($pattern:term) := $body) => do
-     let mut cmds := #[(← `($[$doc?:docComment]? simproc_decl $n ($pattern) := $body))]
-     let pushDefault (cmds : Array (TSyntax `command)) : MacroM (Array (TSyntax `command)) := do
-       return cmds.push (← `(attribute [$kind simproc $[$pre?]?] $n))
-     if let some ids := ids? then
-       for id in ids.getElems do
-         let idName := id.getId
-         let (attrName, attrKey) :=
-           if idName == `simp then
-             (`simprocAttr, "simproc")
-           else if idName == `seval then
-             (`sevalprocAttr, "sevalproc")
-           else
-             let idName := idName.appendAfter "_proc"
-             (`Parser.Attr ++ idName, idName.toString)
-         let attrStx : TSyntax `attr := ⟨mkNode attrName #[mkAtom attrKey, mkOptionalNode pre?]⟩
-         cmds := cmds.push (← `(attribute [$kind $attrStx] $n))
-     else
-       cmds ← pushDefault cmds
-     return mkNullNode cmds
+     return mkNullNode <|
+       #[(← `($[$doc?:docComment]? simproc_decl $n ($pattern) := $body))]
+       ++ (← mkAttributeCmds kind pre? ids? n)
+
+macro_rules
+  | `($[$doc?:docComment]? $kind:attrKind dsimproc $[$pre?]? $[ [ $ids?:ident,* ] ]? $n:ident ($pattern:term) := $body) => do
+     return mkNullNode <|
+       #[(← `($[$doc?:docComment]? dsimproc_decl $n ($pattern) := $body))]
+       ++ (← mkAttributeCmds kind pre? ids? n)
 
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind builtin_simproc $[$pre?]? $n:ident ($pattern:term) := $body) => do
@@ -126,4 +174,16 @@ macro_rules
       attribute [$kind builtin_simproc $[$pre?]?] $n
       attribute [$kind builtin_sevalproc $[$pre?]?] $n)
 
+macro_rules
+  | `($[$doc?:docComment]? $kind:attrKind builtin_dsimproc $[$pre?]? $n:ident ($pattern:term) := $body) => do
+    `($[$doc?:docComment]? builtin_dsimproc_decl $n ($pattern) := $body
+      attribute [$kind builtin_simproc $[$pre?]?] $n)
+  | `($[$doc?:docComment]? $kind:attrKind builtin_dsimproc $[$pre?]? [seval] $n:ident ($pattern:term) := $body) => do
+    `($[$doc?:docComment]? builtin_dsimproc_decl $n ($pattern) := $body
+      attribute [$kind builtin_sevalproc $[$pre?]?] $n)
+  | `($[$doc?:docComment]? $kind:attrKind builtin_dsimproc $[$pre?]? [simp, seval] $n:ident ($pattern:term) := $body) => do
+    `($[$doc?:docComment]? builtin_dsimproc_decl $n ($pattern) := $body
+      attribute [$kind builtin_simproc $[$pre?]?] $n
+      attribute [$kind builtin_sevalproc $[$pre?]?] $n)
+
 end Lean.Parser

src/Lean/Elab/Tactic/Simp.lean

@@ -434,7 +434,7 @@ where
   if tactic.simp.trace.get (← getOptions) then
     traceSimpCall stx usedSimps
 
-def dsimpLocation (ctx : Simp.Context) (loc : Location) : TacticM Unit := do
+def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Location) : TacticM Unit := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -446,7 +446,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?, usedSimps) ← dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
+    let (result?, usedSimps) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
@@ -454,8 +454,8 @@ where
       mvarId.withContext <| traceSimpCall (← getRef) usedSimps
 
 @[builtin_tactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do
-  let { ctx, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
-  dsimpLocation ctx (expandOptLocation stx[5])
+  let { ctx, simprocs, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
+  dsimpLocation ctx simprocs (expandOptLocation stx[5])
 
 end Lean.Elab.Tactic
 

src/Lean/Elab/Tactic/Simproc.lean

@@ -26,10 +26,11 @@ def elabSimprocKeys (stx : Syntax) : MetaM (Array Meta.SimpTheoremKey) := do
   let pattern ← elabSimprocPattern stx
   DiscrTree.mkPath pattern simpDtConfig
 
-def checkSimprocType (declName : Name) : CoreM Unit := do
+def checkSimprocType (declName : Name) : CoreM Bool := do
   let decl ← getConstInfo declName
   match decl.type with
-  | .const ``Simproc _ => pure ()
+  | .const ``Simproc _ => pure false
+  | .const ``DSimproc _ => pure true
   | _ => throwError "unexpected type at '{declName}', 'Simproc' expected"
 
 namespace Command
@@ -38,7 +39,7 @@ namespace Command
   let `(simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
   let declName ← resolveGlobalConstNoOverload declName
   liftTermElabM do
-    checkSimprocType declName
+    discard <| checkSimprocType declName
     let keys ← elabSimprocKeys pattern
     registerSimproc declName keys
 
@@ -46,9 +47,10 @@ namespace Command
   let `(builtin_simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
   let declName ← resolveGlobalConstNoOverload declName
   liftTermElabM do
-    checkSimprocType declName
+    let dsimp ← checkSimprocType declName
     let keys ← elabSimprocKeys pattern
-    let val := mkAppN (mkConst ``registerBuiltinSimproc) #[toExpr declName, toExpr keys, mkConst declName]
+    let registerProcName := if dsimp then ``registerBuiltinDSimproc else ``registerBuiltinSimproc
+    let val := mkAppN (mkConst registerProcName) #[toExpr declName, toExpr keys, mkConst declName]
     let initDeclName ← mkFreshUserName (declName ++ `declare)
     declareBuiltin initDeclName val
 

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -31,176 +31,185 @@ def fromExpr? (e : Expr) : SimpM (Option Literal) := do
 Helper function for reducing homogenous unary bitvector operators.
 -/
 @[inline] def reduceUnary (declName : Name) (arity : Nat)
-    (op : {n : Nat} → BitVec n → BitVec n) (e : Expr) : SimpM Step := do
+    (op : {n : Nat} → BitVec n → BitVec n) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op v.value) }
+  return .done <| toExpr (op v.value)
 
 /--
 Helper function for reducing homogenous binary bitvector operators.
 -/
 @[inline] def reduceBin (declName : Name) (arity : Nat)
-    (op : {n : Nat} → BitVec n → BitVec n → BitVec n) (e : Expr) : SimpM Step := do
+    (op : {n : Nat} → BitVec n → BitVec n → BitVec n) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
   if h : v₁.n = v₂.n then
     trace[Meta.debug] "reduce [{declName}] {v₁.value}, {v₂.value}"
-    return .done { expr := toExpr (op v₁.value (h ▸ v₂.value)) }
+    return .done <| toExpr (op v₁.value (h ▸ v₂.value))
   else
     return .continue
 
 /-- Simplification procedure for `zeroExtend` and `signExtend` on `BitVec`s. -/
 @[inline] def reduceExtend (declName : Name)
-    (op : {n : Nat} → (m : Nat) → BitVec n → BitVec m) (e : Expr) : SimpM Step := do
+    (op : {n : Nat} → (m : Nat) → BitVec n → BitVec m) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName 3 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
   let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  return .done { expr := toExpr (op n v.value) }
+  return .done <| toExpr (op n v.value)
 
 /--
 Helper function for reducing bitvector functions such as `getLsb` and `getMsb`.
 -/
 @[inline] def reduceGetBit (declName : Name) (op : {n : Nat} → BitVec n → Nat → Bool) (e : Expr)
-    : SimpM Step := do
+    : SimpM DStep := do
   unless e.isAppOfArity declName 3 do return .continue
   let some v ← fromExpr? e.appFn!.appArg! | return .continue
   let some i ← Nat.fromExpr? e.appArg! | return .continue
   let b := op v.value i
-  return .done { expr := toExpr b }
+  return .done <| toExpr b
 
 /--
 Helper function for reducing bitvector functions such as `shiftLeft` and `rotateRight`.
 -/
 @[inline] def reduceShift (declName : Name) (arity : Nat)
-    (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Expr) : SimpM Step := do
+    (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some v ← fromExpr? e.appFn!.appArg! | return .continue
   let some i ← Nat.fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op v.value i) }
+  return .done <| toExpr (op v.value i)
 
 /--
 Helper function for reducing bitvector predicates.
 -/
 @[inline] def reduceBinPred (declName : Name) (arity : Nat)
-    (op : {n : Nat} → BitVec n → BitVec n → Bool) (e : Expr) (isProp := true) : SimpM Step := do
+    (op : {n : Nat} → BitVec n → BitVec n → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
   if h : v₁.n = v₂.n then
     let b := op v₁.value (h ▸ v₂.value)
-    if isProp then
-      evalPropStep e b
-    else
-      return .done { expr := toExpr b }
+    evalPropStep e b
   else
     return .continue
 
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat)
+    (op : {n : Nat} → BitVec n → BitVec n → Bool) (e : Expr) : SimpM DStep := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← fromExpr? e.appArg! | return .continue
+  if h : v₁.n = v₂.n then
+    let b := op v₁.value (h ▸ v₂.value)
+    return .done <| toExpr b
+  else
+    return .continue
+
+
 /-- Simplification procedure for negation of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceNeg ((- _ : BitVec _)) := reduceUnary ``Neg.neg 3 (- ·)
+builtin_dsimproc [simp, seval] reduceNeg ((- _ : BitVec _)) := reduceUnary ``Neg.neg 3 (- ·)
 /-- Simplification procedure for bitwise not of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceNot ((~~~ _ : BitVec _)) :=
+builtin_dsimproc [simp, seval] reduceNot ((~~~ _ : BitVec _)) :=
   reduceUnary ``Complement.complement 3 (~~~ ·)
 /-- Simplification procedure for absolute value of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceAbs (BitVec.abs _) := reduceUnary ``BitVec.abs 2 BitVec.abs
+builtin_dsimproc [simp, seval] reduceAbs (BitVec.abs _) := reduceUnary ``BitVec.abs 2 BitVec.abs
 /-- Simplification procedure for bitwise and of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceAnd ((_ &&& _ : BitVec _)) := reduceBin ``HAnd.hAnd 6 (· &&& ·)
+builtin_dsimproc [simp, seval] reduceAnd ((_ &&& _ : BitVec _)) := reduceBin ``HAnd.hAnd 6 (· &&& ·)
 /-- Simplification procedure for bitwise or of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceOr ((_ ||| _ : BitVec _)) := reduceBin ``HOr.hOr 6 (· ||| ·)
+builtin_dsimproc [simp, seval] reduceOr ((_ ||| _ : BitVec _)) := reduceBin ``HOr.hOr 6 (· ||| ·)
 /-- Simplification procedure for bitwise xor of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceXOr ((_ ^^^ _ : BitVec _)) := reduceBin ``HXor.hXor 6 (· ^^^ ·)
+builtin_dsimproc [simp, seval] reduceXOr ((_ ^^^ _ : BitVec _)) := reduceBin ``HXor.hXor 6 (· ^^^ ·)
 /-- Simplification procedure for addition of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceAdd ((_ + _ : BitVec _)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+builtin_dsimproc [simp, seval] reduceAdd ((_ + _ : BitVec _)) := reduceBin ``HAdd.hAdd 6 (· + ·)
 /-- Simplification procedure for multiplication of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceMul ((_ * _ : BitVec _)) := reduceBin ``HMul.hMul 6 (· * ·)
+builtin_dsimproc [simp, seval] reduceMul ((_ * _ : BitVec _)) := reduceBin ``HMul.hMul 6 (· * ·)
 /-- Simplification procedure for subtraction of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceSub ((_ - _ : BitVec _)) := reduceBin ``HSub.hSub 6 (· - ·)
+builtin_dsimproc [simp, seval] reduceSub ((_ - _ : BitVec _)) := reduceBin ``HSub.hSub 6 (· - ·)
 /-- Simplification procedure for division of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceDiv ((_ / _ : BitVec _)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : BitVec _)) := reduceBin ``HDiv.hDiv 6 (· / ·)
 /-- Simplification procedure for the modulo operation on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceMod ((_ % _ : BitVec _)) := reduceBin ``HMod.hMod 6 (· % ·)
+builtin_dsimproc [simp, seval] reduceMod ((_ % _ : BitVec _)) := reduceBin ``HMod.hMod 6 (· % ·)
 /-- Simplification procedure for for the unsigned modulo operation on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceUMod ((umod _ _ : BitVec _)) := reduceBin ``umod 3 umod
+builtin_dsimproc [simp, seval] reduceUMod ((umod _ _ : BitVec _)) := reduceBin ``umod 3 umod
 /-- Simplification procedure for unsigned division of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceUDiv ((udiv _ _ : BitVec _)) := reduceBin ``udiv 3 udiv
+builtin_dsimproc [simp, seval] reduceUDiv ((udiv _ _ : BitVec _)) := reduceBin ``udiv 3 udiv
 /-- Simplification procedure for division of `BitVec`s using the SMT-Lib conventions. -/
-builtin_simproc [simp, seval] reduceSMTUDiv ((smtUDiv _ _ : BitVec _)) := reduceBin ``smtUDiv 3 smtUDiv
+builtin_dsimproc [simp, seval] reduceSMTUDiv ((smtUDiv _ _ : BitVec _)) := reduceBin ``smtUDiv 3 smtUDiv
 /-- Simplification procedure for the signed modulo operation on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceSMod ((smod _ _ : BitVec _)) := reduceBin ``smod 3 smod
+builtin_dsimproc [simp, seval] reduceSMod ((smod _ _ : BitVec _)) := reduceBin ``smod 3 smod
 /-- Simplification procedure for signed remainder of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceSRem ((srem _ _ : BitVec _)) := reduceBin ``srem 3 srem
+builtin_dsimproc [simp, seval] reduceSRem ((srem _ _ : BitVec _)) := reduceBin ``srem 3 srem
 /-- Simplification procedure for signed t-division of `BitVec`s. -/
-builtin_simproc [simp, seval] reduceSDiv ((sdiv _ _ : BitVec _)) := reduceBin ``sdiv 3 sdiv
+builtin_dsimproc [simp, seval] reduceSDiv ((sdiv _ _ : BitVec _)) := reduceBin ``sdiv 3 sdiv
 /-- Simplification procedure for signed division of `BitVec`s using the SMT-Lib conventions. -/
-builtin_simproc [simp, seval] reduceSMTSDiv ((smtSDiv _ _ : BitVec _)) := reduceBin ``smtSDiv 3 smtSDiv
+builtin_dsimproc [simp, seval] reduceSMTSDiv ((smtSDiv _ _ : BitVec _)) := reduceBin ``smtSDiv 3 smtSDiv
 /-- Simplification procedure for `getLsb` (lowest significant bit) on `BitVec`. -/
-builtin_simproc [simp, seval] reduceGetLsb (getLsb _ _) := reduceGetBit ``getLsb getLsb
+builtin_dsimproc [simp, seval] reduceGetLsb (getLsb _ _) := reduceGetBit ``getLsb getLsb
 /-- Simplification procedure for `getMsb` (most significant bit) on `BitVec`. -/
-builtin_simproc [simp, seval] reduceGetMsb (getMsb _ _) := reduceGetBit ``getMsb getMsb
+builtin_dsimproc [simp, seval] reduceGetMsb (getMsb _ _) := reduceGetBit ``getMsb getMsb
 
 /-- Simplification procedure for shift left on `BitVec`. -/
-builtin_simproc [simp, seval] reduceShiftLeft (BitVec.shiftLeft _ _) :=
+builtin_dsimproc [simp, seval] reduceShiftLeft (BitVec.shiftLeft _ _) :=
   reduceShift ``BitVec.shiftLeft 3 BitVec.shiftLeft
 /-- Simplification procedure for unsigned shift right on `BitVec`. -/
-builtin_simproc [simp, seval] reduceUShiftRight (BitVec.ushiftRight _ _) :=
+builtin_dsimproc [simp, seval] reduceUShiftRight (BitVec.ushiftRight _ _) :=
   reduceShift ``BitVec.ushiftRight 3 BitVec.ushiftRight
 /-- Simplification procedure for signed shift right on `BitVec`. -/
-builtin_simproc [simp, seval] reduceSShiftRight (BitVec.sshiftRight _ _) :=
+builtin_dsimproc [simp, seval] reduceSShiftRight (BitVec.sshiftRight _ _) :=
   reduceShift ``BitVec.sshiftRight 3 BitVec.sshiftRight
 /-- Simplification procedure for shift left on `BitVec`. -/
-builtin_simproc [simp, seval] reduceHShiftLeft ((_ <<< _ : BitVec _)) :=
+builtin_dsimproc [simp, seval] reduceHShiftLeft ((_ <<< _ : BitVec _)) :=
   reduceShift ``HShiftLeft.hShiftLeft 6 (· <<< ·)
 /-- Simplification procedure for shift right on `BitVec`. -/
-builtin_simproc [simp, seval] reduceHShiftRight ((_ >>> _ : BitVec _)) :=
+builtin_dsimproc [simp, seval] reduceHShiftRight ((_ >>> _ : BitVec _)) :=
   reduceShift ``HShiftRight.hShiftRight 6 (· >>> ·)
 /-- Simplification procedure for rotate left on `BitVec`. -/
-builtin_simproc [simp, seval] reduceRotateLeft (BitVec.rotateLeft _ _) :=
+builtin_dsimproc [simp, seval] reduceRotateLeft (BitVec.rotateLeft _ _) :=
   reduceShift ``BitVec.rotateLeft 3 BitVec.rotateLeft
 /-- Simplification procedure for rotate right on `BitVec`. -/
-builtin_simproc [simp, seval] reduceRotateRight (BitVec.rotateRight _ _) :=
+builtin_dsimproc [simp, seval] reduceRotateRight (BitVec.rotateRight _ _) :=
   reduceShift ``BitVec.rotateRight 3 BitVec.rotateRight
 
 /-- Simplification procedure for append on `BitVec`. -/
-builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : BitVec _)) := fun e => do
+builtin_dsimproc [simp, seval] reduceAppend ((_ ++ _ : BitVec _)) := fun e => do
   let_expr HAppend.hAppend _ _ _ _ a b ← e | return .continue
   let some v₁ ← fromExpr? a | return .continue
   let some v₂ ← fromExpr? b | return .continue
-  return .done { expr := toExpr (v₁.value ++ v₂.value) }
+  return .done <| toExpr (v₁.value ++ v₂.value)
 
 /-- Simplification procedure for casting `BitVec`s along an equality of the size. -/
-builtin_simproc [simp, seval] reduceCast (cast _ _) := fun e => do
+builtin_dsimproc [simp, seval] reduceCast (cast _ _) := fun e => do
   let_expr cast _ m _ v ← e | return .continue
   let some v ← fromExpr? v | return .continue
   let some m ← Nat.fromExpr? m | return .continue
-  return .done { expr := toExpr (BitVec.ofNat m v.value.toNat) }
+  return .done <| toExpr (BitVec.ofNat m v.value.toNat)
 
 /-- Simplification procedure for `BitVec.toNat`. -/
-builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
+builtin_dsimproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
   let_expr BitVec.toNat _ v ← e | return .continue
   let some v ← fromExpr? v | return .continue
-  return .done { expr := mkNatLit v.value.toNat }
+  return .done <| mkNatLit v.value.toNat
 
 /-- Simplification procedure for `BitVec.toInt`. -/
-builtin_simproc [simp, seval] reduceToInt (BitVec.toInt _) := fun e => do
+builtin_dsimproc [simp, seval] reduceToInt (BitVec.toInt _) := fun e => do
   let_expr BitVec.toInt _ v ← e | return .continue
   let some v ← fromExpr? v | return .continue
-  return .done { expr := toExpr v.value.toInt }
+  return .done <| toExpr v.value.toInt
 
 /-- Simplification procedure for `BitVec.ofInt`. -/
-builtin_simproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
+builtin_dsimproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
   let_expr BitVec.ofInt n i ← e | return .continue
   let some n ← Nat.fromExpr? n | return .continue
   let some i ← Int.fromExpr? i | return .continue
-  return .done { expr := toExpr (BitVec.ofInt n i) }
+  return .done <| toExpr (BitVec.ofInt n i)
 
 /-- Simplification procedure for ensuring `BitVec.ofNat` literals are normalized. -/
-builtin_simproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
+builtin_dsimproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
   let_expr BitVec.ofNat n v ← e | return .continue
   let some n ← Nat.fromExpr? n | return .continue
   let some v ← Nat.fromExpr? v | return .continue
   let bv := BitVec.ofNat n v
   if bv.toNat == v then return .continue -- already normalized
-  return .done { expr := toExpr (BitVec.ofNat n v) }
+  return .done <| toExpr (BitVec.ofNat n v)
 
 /-- Simplification procedure for `<` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)
@@ -212,71 +221,71 @@ builtin_simproc [simp, seval] reduceGT (( _ : BitVec _) > _)  := reduceBinPred `
 builtin_simproc [simp, seval] reduceGE (( _ : BitVec _) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
 
 /-- Simplification procedure for unsigned less than `ult` on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceULT (BitVec.ult _ _) :=
-  reduceBinPred ``BitVec.ult 3 BitVec.ult (isProp := false)
+builtin_dsimproc [simp, seval] reduceULT (BitVec.ult _ _) :=
+  reduceBoolPred ``BitVec.ult 3 BitVec.ult
 /-- Simplification procedure for unsigned less than or equal `ule` on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceULE (BitVec.ule _ _) :=
-  reduceBinPred ``BitVec.ule 3 BitVec.ule (isProp := false)
+builtin_dsimproc [simp, seval] reduceULE (BitVec.ule _ _) :=
+  reduceBoolPred ``BitVec.ule 3 BitVec.ule
 /-- Simplification procedure for signed less than `slt` on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceSLT (BitVec.slt _ _) :=
-  reduceBinPred ``BitVec.slt 3 BitVec.slt (isProp := false)
+builtin_dsimproc [simp, seval] reduceSLT (BitVec.slt _ _) :=
+  reduceBoolPred ``BitVec.slt 3 BitVec.slt
 /-- Simplification procedure for signed less than or equal `sle` on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceSLE (BitVec.sle _ _) :=
-  reduceBinPred ``BitVec.sle 3 BitVec.sle (isProp := false)
+builtin_dsimproc [simp, seval] reduceSLE (BitVec.sle _ _) :=
+  reduceBoolPred ``BitVec.sle 3 BitVec.sle
 
 /-- Simplification procedure for `zeroExtend'` on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
+builtin_dsimproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
   let_expr zeroExtend' _ w _ v ← e | return .continue
   let some v ← fromExpr? v | return .continue
   let some w ← Nat.fromExpr? w | return .continue
   if h : v.n ≤ w then
-    return .done { expr := toExpr (v.value.zeroExtend' h) }
+    return .done <| toExpr (v.value.zeroExtend' h)
   else
     return .continue
 
 /-- Simplification procedure for `shiftLeftZeroExtend` on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _ _) := fun e => do
+builtin_dsimproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _ _) := fun e => do
   let_expr shiftLeftZeroExtend _ v m ← e | return .continue
   let some v ← fromExpr? v | return .continue
   let some m ← Nat.fromExpr? m | return .continue
-  return .done { expr := toExpr (v.value.shiftLeftZeroExtend m) }
+  return .done <| toExpr (v.value.shiftLeftZeroExtend m)
 
 /-- Simplification procedure for `extractLsb'` on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => do
+builtin_dsimproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => do
   let_expr extractLsb' _ start len v ← e | return .continue
   let some v ← fromExpr? v | return .continue
   let some start ← Nat.fromExpr? start | return .continue
   let some len ← Nat.fromExpr? len | return .continue
-  return .done { expr := toExpr (v.value.extractLsb' start len) }
+  return .done <| toExpr (v.value.extractLsb' start len)
 
 /-- Simplification procedure for `replicate` on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
+builtin_dsimproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
   let_expr replicate _ i v ← e | return .continue
   let some v ← fromExpr? v | return .continue
   let some i ← Nat.fromExpr? i | return .continue
-  return .done { expr := toExpr (v.value.replicate i) }
+  return .done <| toExpr (v.value.replicate i)
 
 /-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
+builtin_dsimproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
 
 /-- Simplification procedure for `signExtend` on `BitVec`s. -/
-builtin_simproc [simp, seval] reduceSignExtend (signExtend _ _) := reduceExtend ``signExtend signExtend
+builtin_dsimproc [simp, seval] reduceSignExtend (signExtend _ _) := reduceExtend ``signExtend signExtend
 
 /-- Simplification procedure for `allOnes` -/
-builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
+builtin_dsimproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
   let_expr allOnes n ← e | return .continue
   let some n ← Nat.fromExpr? n | return .continue
-  return .done { expr := toExpr (allOnes n) }
+  return .done <| toExpr (allOnes n)
 
-builtin_simproc [simp, seval] reduceBitVecOfFin (BitVec.ofFin _)  := fun e => do
+builtin_dsimproc [simp, seval] reduceBitVecOfFin (BitVec.ofFin _)  := fun e => do
   let_expr BitVec.ofFin w v ← e | return .continue
   let some w ← evalNat w |>.run | return .continue
   let some ⟨_, v⟩ ← getFinValue? v | return .continue
-  return .done { expr := toExpr (BitVec.ofNat w v.val) }
+  return .done <| toExpr (BitVec.ofNat w v.val)
 
-builtin_simproc [simp, seval] reduceBitVecToFin (BitVec.toFin _)  := fun e => do
+builtin_dsimproc [simp, seval] reduceBitVecToFin (BitVec.toFin _)  := fun e => do
   let_expr BitVec.toFin _ v ← e | return .continue
   let some ⟨_, v⟩ ← getBitVecValue? v | return .continue
-  return .done { expr := toExpr v.toFin }
+  return .done <| toExpr v.toFin
 
 end BitVec

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean

@@ -14,10 +14,10 @@ open Lean Meta Simp
 def fromExpr? (e : Expr) : SimpM (Option Char) :=
   getCharValue? e
 
-@[inline] def reduceUnary [ToExpr α] (declName : Name) (op : Char → α) (arity : Nat := 1) (e : Expr) : SimpM Step := do
+@[inline] def reduceUnary [ToExpr α] (declName : Name) (op : Char → α) (arity : Nat := 1) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some c ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op c) }
+  return .done <| toExpr (op c)
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Char → Char → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -25,47 +25,47 @@ def fromExpr? (e : Expr) : SimpM (Option Char) :=
   let some m ← fromExpr? e.appArg! | return .continue
   evalPropStep e (op n m)
 
-@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Char → Char → Bool) (e : Expr) : SimpM Step := do
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Char → Char → Bool) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op n m) }
+  return .done <| toExpr (op n m)
 
-builtin_simproc [simp, seval] reduceToLower (Char.toLower _) := reduceUnary ``Char.toLower Char.toLower
-builtin_simproc [simp, seval] reduceToUpper (Char.toUpper _) := reduceUnary ``Char.toUpper Char.toUpper
-builtin_simproc [simp, seval] reduceToNat (Char.toNat _) := reduceUnary ``Char.toNat Char.toNat
-builtin_simproc [simp, seval] reduceIsWhitespace (Char.isWhitespace _) := reduceUnary ``Char.isWhitespace Char.isWhitespace
-builtin_simproc [simp, seval] reduceIsUpper (Char.isUpper _) := reduceUnary ``Char.isUpper Char.isUpper
-builtin_simproc [simp, seval] reduceIsLower (Char.isLower _) := reduceUnary ``Char.isLower Char.isLower
-builtin_simproc [simp, seval] reduceIsAlpha (Char.isAlpha _) := reduceUnary ``Char.isAlpha Char.isAlpha
-builtin_simproc [simp, seval] reduceIsDigit (Char.isDigit _) := reduceUnary ``Char.isDigit Char.isDigit
-builtin_simproc [simp, seval] reduceIsAlphaNum (Char.isAlphanum _) := reduceUnary ``Char.isAlphanum Char.isAlphanum
-builtin_simproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnary ``toString toString 3
-builtin_simproc [simp, seval] reduceVal (Char.val _) := fun e => do
+builtin_dsimproc [simp, seval] reduceToLower (Char.toLower _) := reduceUnary ``Char.toLower Char.toLower
+builtin_dsimproc [simp, seval] reduceToUpper (Char.toUpper _) := reduceUnary ``Char.toUpper Char.toUpper
+builtin_dsimproc [simp, seval] reduceToNat (Char.toNat _) := reduceUnary ``Char.toNat Char.toNat
+builtin_dsimproc [simp, seval] reduceIsWhitespace (Char.isWhitespace _) := reduceUnary ``Char.isWhitespace Char.isWhitespace
+builtin_dsimproc [simp, seval] reduceIsUpper (Char.isUpper _) := reduceUnary ``Char.isUpper Char.isUpper
+builtin_dsimproc [simp, seval] reduceIsLower (Char.isLower _) := reduceUnary ``Char.isLower Char.isLower
+builtin_dsimproc [simp, seval] reduceIsAlpha (Char.isAlpha _) := reduceUnary ``Char.isAlpha Char.isAlpha
+builtin_dsimproc [simp, seval] reduceIsDigit (Char.isDigit _) := reduceUnary ``Char.isDigit Char.isDigit
+builtin_dsimproc [simp, seval] reduceIsAlphaNum (Char.isAlphanum _) := reduceUnary ``Char.isAlphanum Char.isAlphanum
+builtin_dsimproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnary ``toString toString 3
+builtin_dsimproc [simp, seval] reduceVal (Char.val _) := fun e => do
   let_expr Char.val arg ← e | return .continue
   let some c ← fromExpr? arg | return .continue
-  return .done { expr := toExpr c.val }
+  return .done <| toExpr c.val
 builtin_simproc [simp, seval] reduceEq  (( _ : Char) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Char) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
-builtin_simproc [simp, seval] reduceBEq  (( _ : Char) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
-builtin_simproc [simp, seval] reduceBNe  (( _ : Char) != _)  := reduceBoolPred ``bne 4 (. != .)
+builtin_dsimproc [simp, seval] reduceBEq  (( _ : Char) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_dsimproc [simp, seval] reduceBNe  (( _ : Char) != _)  := reduceBoolPred ``bne 4 (. != .)
 
 /--
 Return `.done` for Char values. We don't want to unfold in the symbolic evaluator.
 In regular `simp`, we want to prevent the nested raw literal from being converted into
 a `OfNat.ofNat` application. TODO: cleanup
 -/
-builtin_simproc ↓ [simp, seval] isValue (Char.ofNat _ ) := fun e => do
+builtin_dsimproc ↓ [simp, seval] isValue (Char.ofNat _ ) := fun e => do
   unless (← fromExpr? e).isSome do return .continue
-  return .done { expr := e }
+  return .done e
 
-builtin_simproc [simp, seval] reduceOfNatAux (Char.ofNatAux _ _) := fun e => do
+builtin_dsimproc [simp, seval] reduceOfNatAux (Char.ofNatAux _ _) := fun e => do
   let_expr Char.ofNatAux n _ ← e | return .continue
   let some n ← Nat.fromExpr? n | return .continue
-  return .done { expr := toExpr (Char.ofNat n) }
+  return .done <| toExpr (Char.ofNat n)
 
-builtin_simproc [simp, seval] reduceDefault ((default : Char)) := fun e => do
+builtin_dsimproc [simp, seval] reduceDefault ((default : Char)) := fun e => do
   let_expr default _ _ ← e | return .continue
-  return .done { expr := toExpr (default : Char) }
+  return .done <| toExpr (default : Char)
 
 end Char

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean

@@ -19,13 +19,13 @@ def fromExpr? (e : Expr) : SimpM (Option Value) := do
   let some ⟨n, value⟩ ← getFinValue? e | return none
   return some { n, value }
 
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : {n : Nat} → Fin n → Fin n → Fin n) (e : Expr) : SimpM Step := do
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : {n : Nat} → Fin n → Fin n → Fin n) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
   if h : v₁.n = v₂.n then
     let v := op v₁.value (h ▸ v₂.value)
-    return .done { expr := toExpr v }
+    return .done <| toExpr v
   else
     return .continue
 
@@ -35,22 +35,22 @@ def fromExpr? (e : Expr) : SimpM (Option Value) := do
   let some v₂ ← fromExpr? e.appArg! | return .continue
   evalPropStep e (op v₁.value v₂.value)
 
-@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  return .done { expr := Lean.toExpr (op v₁.value v₂.value) }
+  return .done <| toExpr (op v₁.value v₂.value)
 
 /-
 The following code assumes users did not override the `Fin n` instances for the arithmetic operators.
 If they do, they must disable the following `simprocs`.
 -/
 
-builtin_simproc [simp, seval] reduceAdd ((_ + _ : Fin _)) := reduceBin ``HAdd.hAdd 6 (· + ·)
-builtin_simproc [simp, seval] reduceMul ((_ * _ : Fin _)) := reduceBin ``HMul.hMul 6 (· * ·)
-builtin_simproc [simp, seval] reduceSub ((_ - _ : Fin _)) := reduceBin ``HSub.hSub 6 (· - ·)
-builtin_simproc [simp, seval] reduceDiv ((_ / _ : Fin _)) := reduceBin ``HDiv.hDiv 6 (· / ·)
-builtin_simproc [simp, seval] reduceMod ((_ % _ : Fin _)) := reduceBin ``HMod.hMod 6 (· % ·)
+builtin_dsimproc [simp, seval] reduceAdd ((_ + _ : Fin _)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+builtin_dsimproc [simp, seval] reduceMul ((_ * _ : Fin _)) := reduceBin ``HMul.hMul 6 (· * ·)
+builtin_dsimproc [simp, seval] reduceSub ((_ - _ : Fin _)) := reduceBin ``HSub.hSub 6 (· - ·)
+builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Fin _)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Fin _)) := reduceBin ``HMod.hMod 6 (· % ·)
 
 builtin_simproc [simp, seval] reduceLT  (( _ : Fin _) < _)  := reduceBinPred ``LT.lt 4 (. < .)
 builtin_simproc [simp, seval] reduceLE  (( _ : Fin _) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
@@ -58,25 +58,25 @@ builtin_simproc [simp, seval] reduceGT  (( _ : Fin _) > _)  := reduceBinPred ``G
 builtin_simproc [simp, seval] reduceGE  (( _ : Fin _) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
 builtin_simproc [simp, seval] reduceEq  (( _ : Fin _) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Fin _) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
-builtin_simproc [simp, seval] reduceBEq  (( _ : Fin _) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
-builtin_simproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred ``bne 4 (. != .)
+builtin_dsimproc [simp, seval] reduceBEq  (( _ : Fin _) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_dsimproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred ``bne 4 (. != .)
 
 /-- Simplification procedure for ensuring `Fin` literals are normalized. -/
-builtin_simproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
+builtin_dsimproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
   let some ⟨n, v⟩ ← getFinValue? e | return .continue
   let some m ← getNatValue? e.appFn!.appArg! | return .continue
   if n == m then
     -- Design decision: should we return `.continue` instead of `.done` when simplifying.
     -- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`
-    return .done { expr := e }
-  return .done { expr := toExpr v }
+    return .done e
+  return .done <| toExpr v
 
-builtin_simproc [simp, seval] reduceFinMk (Fin.mk _ _)  := fun e => do
+builtin_dsimproc [simp, seval] reduceFinMk (Fin.mk _ _)  := fun e => do
   let_expr Fin.mk n v _ ← e | return .continue
   let some n ← evalNat n |>.run | return .continue
   let some v ← getNatValue? v | return .continue
   if h : n > 0 then
-    return .done { expr := toExpr (Fin.ofNat' v h) }
+    return .done <| toExpr (Fin.ofNat' v h)
   else
     return .continue
 

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -14,16 +14,16 @@ open Lean Meta Simp
 def fromExpr? (e : Expr) : SimpM (Option Int) :=
   getIntValue? e
 
-@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Int → Int) (e : Expr) : SimpM Step := do
+@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Int → Int) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op n) }
+  return .done <| toExpr (op n)
 
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Int → Int → Int) (e : Expr) : SimpM Step := do
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Int → Int → Int) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op v₁ v₂) }
+  return .done <| toExpr (op v₁ v₂)
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Int → Int → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -31,46 +31,46 @@ def fromExpr? (e : Expr) : SimpM (Option Int) :=
   let some v₂ ← fromExpr? e.appArg! | return .continue
   evalPropStep e (op v₁ v₂)
 
-@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Int → Int → Bool) (e : Expr) : SimpM Step := do
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Int → Int → Bool) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
-  return .done { expr := Lean.toExpr (op n m) }
+  return .done <| toExpr (op n m)
 
 /-
 The following code assumes users did not override the `Int` instances for the arithmetic operators.
 If they do, they must disable the following `simprocs`.
 -/
 
-builtin_simproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do
+builtin_dsimproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do
   unless e.isAppOfArity ``Neg.neg 3 do return .continue
   let arg := e.appArg!
   if arg.isAppOfArity ``OfNat.ofNat 3 then
     -- We return .done to ensure `Neg.neg` is not unfolded even when `ground := true`.
-    return .done { expr := e }
+    return .done e
   else
     let some v ← fromExpr? arg | return .continue
     if v < 0 then
-      return .done { expr := toExpr (- v) }
+      return .done <| toExpr (- v)
     else
-      return .done { expr := toExpr v }
+      return .done <| toExpr v
 
 /-- Return `.done` for positive Int values. We don't want to unfold in the symbolic evaluator. -/
-builtin_simproc [seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do
+builtin_dsimproc [seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do
   let_expr OfNat.ofNat _ _ _ ← e | return .continue
-  return .done { expr := e }
+  return .done e
 
-builtin_simproc [simp, seval] reduceAdd ((_ + _ : Int)) := reduceBin ``HAdd.hAdd 6 (· + ·)
-builtin_simproc [simp, seval] reduceMul ((_ * _ : Int)) := reduceBin ``HMul.hMul 6 (· * ·)
-builtin_simproc [simp, seval] reduceSub ((_ - _ : Int)) := reduceBin ``HSub.hSub 6 (· - ·)
-builtin_simproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv 6 (· / ·)
-builtin_simproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
+builtin_dsimproc [simp, seval] reduceAdd ((_ + _ : Int)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+builtin_dsimproc [simp, seval] reduceMul ((_ * _ : Int)) := reduceBin ``HMul.hMul 6 (· * ·)
+builtin_dsimproc [simp, seval] reduceSub ((_ - _ : Int)) := reduceBin ``HSub.hSub 6 (· - ·)
+builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
 
-builtin_simproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
+builtin_dsimproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
   let_expr HPow.hPow _ _ _ _ a b ← e | return .continue
   let some v₁ ← fromExpr? a | return .continue
   let some v₂ ← Nat.fromExpr? b | return .continue
-  return .done { expr := toExpr (v₁ ^ v₂) }
+  return .done <| toExpr (v₁ ^ v₂)
 
 builtin_simproc [simp, seval] reduceLT  (( _ : Int) < _)  := reduceBinPred ``LT.lt 4 (. < .)
 builtin_simproc [simp, seval] reduceLE  (( _ : Int) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
@@ -78,25 +78,25 @@ builtin_simproc [simp, seval] reduceGT  (( _ : Int) > _)  := reduceBinPred ``GT.
 builtin_simproc [simp, seval] reduceGE  (( _ : Int) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
 builtin_simproc [simp, seval] reduceEq  (( _ : Int) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Int) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
-builtin_simproc [simp, seval] reduceBEq  (( _ : Int) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
-builtin_simproc [simp, seval] reduceBNe  (( _ : Int) != _)  := reduceBoolPred ``bne 4 (. != .)
+builtin_dsimproc [simp, seval] reduceBEq  (( _ : Int) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_dsimproc [simp, seval] reduceBNe  (( _ : Int) != _)  := reduceBoolPred ``bne 4 (. != .)
 
-@[inline] def reduceNatCore (declName : Name) (op : Int → Nat) (e : Expr) : SimpM Step := do
+@[inline] def reduceNatCore (declName : Name) (op : Int → Nat) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName 1 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
-  return .done { expr := mkNatLit (op v) }
+  return .done <| mkNatLit (op v)
 
-builtin_simproc [simp, seval] reduceAbs (natAbs _) := reduceNatCore ``natAbs natAbs
-builtin_simproc [simp, seval] reduceToNat (Int.toNat _) := reduceNatCore ``Int.toNat Int.toNat
+builtin_dsimproc [simp, seval] reduceAbs (natAbs _) := reduceNatCore ``natAbs natAbs
+builtin_dsimproc [simp, seval] reduceToNat (Int.toNat _) := reduceNatCore ``Int.toNat Int.toNat
 
-builtin_simproc [simp, seval] reduceNegSucc (Int.negSucc _) := fun e => do
+builtin_dsimproc [simp, seval] reduceNegSucc (Int.negSucc _) := fun e => do
   let_expr Int.negSucc a ← e | return .continue
   let some a ← getNatValue? a | return .continue
-  return .done { expr := toExpr (-(Int.ofNat a + 1)) }
+  return .done <| toExpr (-(Int.ofNat a + 1))
 
-builtin_simproc [simp, seval] reduceOfNat (Int.ofNat _) := fun e => do
+builtin_dsimproc [simp, seval] reduceOfNat (Int.ofNat _) := fun e => do
   let_expr Int.ofNat a ← e | return .continue
   let some a ← getNatValue? a | return .continue
-  return .done { expr := toExpr (Int.ofNat a) }
+  return .done <| toExpr (Int.ofNat a)
 
 end Int

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -16,16 +16,16 @@ open Lean Meta Simp
 def fromExpr? (e : Expr) : SimpM (Option Nat) :=
   getNatValue? e
 
-@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : SimpM Step := do
+@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op n) }
+  return .done <| toExpr (op n)
 
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM Step := do
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op n m) }
+  return .done <| toExpr (op n m)
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -33,26 +33,26 @@ def fromExpr? (e : Expr) : SimpM (Option Nat) :=
   let some m ← fromExpr? e.appArg! | return .continue
   evalPropStep e (op n m)
 
-@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op n m) }
+  return .done <| toExpr (op n m)
 
-builtin_simproc [simp, seval] reduceSucc (Nat.succ _) := reduceUnary ``Nat.succ 1 (· + 1)
+builtin_dsimproc [simp, seval] reduceSucc (Nat.succ _) := reduceUnary ``Nat.succ 1 (· + 1)
 
 /-
 The following code assumes users did not override the `Nat` instances for the arithmetic operators.
 If they do, they must disable the following `simprocs`.
 -/
 
-builtin_simproc [simp, seval] reduceAdd ((_ + _ : Nat)) := reduceBin ``HAdd.hAdd 6 (· + ·)
-builtin_simproc [simp, seval] reduceMul ((_ * _ : Nat)) := reduceBin ``HMul.hMul 6 (· * ·)
-builtin_simproc [simp, seval] reduceSub ((_ - _ : Nat)) := reduceBin ``HSub.hSub 6 (· - ·)
-builtin_simproc [simp, seval] reduceDiv ((_ / _ : Nat)) := reduceBin ``HDiv.hDiv 6 (· / ·)
-builtin_simproc [simp, seval] reduceMod ((_ % _ : Nat)) := reduceBin ``HMod.hMod 6 (· % ·)
-builtin_simproc [simp, seval] reducePow ((_ ^ _ : Nat)) := reduceBin ``HPow.hPow 6 (· ^ ·)
-builtin_simproc [simp, seval] reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd
+builtin_dsimproc [simp, seval] reduceAdd ((_ + _ : Nat)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+builtin_dsimproc [simp, seval] reduceMul ((_ * _ : Nat)) := reduceBin ``HMul.hMul 6 (· * ·)
+builtin_dsimproc [simp, seval] reduceSub ((_ - _ : Nat)) := reduceBin ``HSub.hSub 6 (· - ·)
+builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Nat)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Nat)) := reduceBin ``HMod.hMod 6 (· % ·)
+builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := reduceBin ``HPow.hPow 6 (· ^ ·)
+builtin_dsimproc [simp, seval] reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd
 
 builtin_simproc [simp, seval] reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)
 builtin_simproc [simp, seval] reduceLE  (( _ : Nat) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
@@ -60,12 +60,12 @@ builtin_simproc [simp, seval] reduceGT  (( _ : Nat) > _)  := reduceBinPred ``GT.
 builtin_simproc [simp, seval] reduceGE  (( _ : Nat) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
 builtin_simproc [simp, seval] reduceEq  (( _ : Nat) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Nat) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
-builtin_simproc [simp, seval] reduceBEq  (( _ : Nat) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
-builtin_simproc [simp, seval] reduceBNe  (( _ : Nat) != _)  := reduceBoolPred ``bne 4 (. != .)
+builtin_dsimproc [simp, seval] reduceBEq  (( _ : Nat) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_dsimproc [simp, seval] reduceBNe  (( _ : Nat) != _)  := reduceBoolPred ``bne 4 (. != .)
 
 /-- Return `.done` for Nat values. We don't want to unfold in the symbolic evaluator. -/
-builtin_simproc [seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do
+builtin_dsimproc [seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do
   let_expr OfNat.ofNat _ _ _ ← e | return .continue
-  return .done { expr := e }
+  return .done e
 
 end Nat

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -13,23 +13,23 @@ open Lean Meta Simp
 def fromExpr? (e : Expr) : SimpM (Option String) := do
   return getStringValue? e
 
-builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : String)) := fun e => do
+builtin_dsimproc [simp, seval] reduceAppend ((_ ++ _ : String)) := fun e => do
   unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue
   let some a ← fromExpr? e.appFn!.appArg! | return .continue
   let some b ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (a ++ b) }
+  return .done <| toExpr (a ++ b)
 
-private partial def reduceListChar (e : Expr) (s : String) : SimpM Step := do
+private partial def reduceListChar (e : Expr) (s : String) : SimpM DStep := do
   trace[Meta.debug] "reduceListChar {e}, {s}"
   if e.isAppOfArity ``List.nil 1 then
-    return .done { expr := toExpr s }
+    return .done <| toExpr s
   else if e.isAppOfArity ``List.cons 3 then
     let some c ← Char.fromExpr? e.appFn!.appArg! | return .continue
     reduceListChar e.appArg! (s.push c)
   else
     return .continue
 
-builtin_simproc [simp, seval] reduceMk (String.mk _) := fun e => do
+builtin_dsimproc [simp, seval] reduceMk (String.mk _) := fun e => do
   unless e.isAppOfArity ``String.mk 1 do return .continue
   reduceListChar e.appArg! ""
 

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean

@@ -21,11 +21,11 @@ def $fromExpr (e : Expr) : SimpM (Option $typeName) := do
   let some (n, _) ← getOfNatValue? e $(quote typeName.getId) | return none
   return $(mkIdent ofNat) n
 
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : SimpM Step := do
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  return .done { expr := toExpr (op n m) }
+  return .done <| toExpr (op n m)
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -33,17 +33,17 @@ def $fromExpr (e : Expr) : SimpM (Option $typeName) := do
   let some m ← ($fromExpr e.appArg!) | return .continue
   evalPropStep e (op n m)
 
-@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := do
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  return .done { expr := toExpr (op n m) }
+  return .done <| toExpr (op n m)
 
-builtin_simproc [simp, seval] $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
-builtin_simproc [simp, seval] $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)
-builtin_simproc [simp, seval] $(mkIdent `reduceSub):ident ((_ - _ : $typeName)) := reduceBin ``HSub.hSub 6 (· - ·)
-builtin_simproc [simp, seval] $(mkIdent `reduceDiv):ident ((_ / _ : $typeName)) := reduceBin ``HDiv.hDiv 6 (· / ·)
-builtin_simproc [simp, seval] $(mkIdent `reduceMod):ident ((_ % _ : $typeName)) := reduceBin ``HMod.hMod 6 (· % ·)
+builtin_dsimproc [simp, seval] $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+builtin_dsimproc [simp, seval] $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)
+builtin_dsimproc [simp, seval] $(mkIdent `reduceSub):ident ((_ - _ : $typeName)) := reduceBin ``HSub.hSub 6 (· - ·)
+builtin_dsimproc [simp, seval] $(mkIdent `reduceDiv):ident ((_ / _ : $typeName)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+builtin_dsimproc [simp, seval] $(mkIdent `reduceMod):ident ((_ % _ : $typeName)) := reduceBin ``HMod.hMod 6 (· % ·)
 
 builtin_simproc [simp, seval] $(mkIdent `reduceLT):ident  (( _ : $typeName) < _)  := reduceBinPred ``LT.lt 4 (. < .)
 builtin_simproc [simp, seval] $(mkIdent `reduceLE):ident  (( _ : $typeName) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
@@ -51,31 +51,31 @@ builtin_simproc [simp, seval] $(mkIdent `reduceGT):ident  (( _ : $typeName) > _)
 builtin_simproc [simp, seval] $(mkIdent `reduceGE):ident  (( _ : $typeName) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
 builtin_simproc [simp, seval] reduceEq  (( _ : $typeName) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : $typeName) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
-builtin_simproc [simp, seval] reduceBEq  (( _ : $typeName) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
-builtin_simproc [simp, seval] reduceBNe  (( _ : $typeName) != _)  := reduceBoolPred ``bne 4 (. != .)
+builtin_dsimproc [simp, seval] reduceBEq  (( _ : $typeName) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_dsimproc [simp, seval] reduceBNe  (( _ : $typeName) != _)  := reduceBoolPred ``bne 4 (. != .)
 
-builtin_simproc [simp, seval] $(mkIdent `reduceOfNatCore):ident ($ofNatCore _ _) := fun e => do
+builtin_dsimproc [simp, seval] $(mkIdent `reduceOfNatCore):ident ($ofNatCore _ _) := fun e => do
   unless e.isAppOfArity $(quote ofNatCore.getId) 2 do return .continue
   let some value ← Nat.fromExpr? e.appFn!.appArg! | return .continue
   let value := $(mkIdent ofNat) value
-  return .done { expr := toExpr value }
+  return .done <| toExpr value
 
-builtin_simproc [simp, seval] $(mkIdent `reduceOfNat):ident ($(mkIdent ofNat) _) := fun e => do
+builtin_dsimproc [simp, seval] $(mkIdent `reduceOfNat):ident ($(mkIdent ofNat) _) := fun e => do
   unless e.isAppOfArity $(quote ofNat) 1 do return .continue
   let some value ← Nat.fromExpr? e.appArg! | return .continue
   let value := $(mkIdent ofNat) value
-  return .done { expr := toExpr value }
+  return .done <| toExpr value
 
-builtin_simproc [simp, seval] $(mkIdent `reduceToNat):ident ($toNat _) := fun e => do
+builtin_dsimproc [simp, seval] $(mkIdent `reduceToNat):ident ($toNat _) := fun e => do
   unless e.isAppOfArity $(quote toNat.getId) 1 do return .continue
   let some v ← ($fromExpr e.appArg!) | return .continue
   let n := $toNat v
-  return .done { expr := toExpr n }
+  return .done <| toExpr n
 
 /-- Return `.done` for UInt values. We don't want to unfold in the symbolic evaluator. -/
-builtin_simproc [seval] isValue ((OfNat.ofNat _ : $typeName)) := fun e => do
+builtin_dsimproc [seval] isValue ((OfNat.ofNat _ : $typeName)) := fun e => do
   unless (e.isAppOfArity ``OfNat.ofNat 3) do return .continue
-  return .done { expr := e }
+  return .done e
 
 end $typeName
 )

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

@@ -400,24 +400,20 @@ def simpLet (e : Expr) : SimpM Result := do
           let h ← mkLambdaFVars #[x] h
           return { expr := e', proof? := some (← mkLetBodyCongr v' h) }
 
+private def dsimpReduce : DSimproc := fun e => do
+  let mut eNew ← reduce e
+  if eNew.isFVar then
+    eNew ← reduceFVar (← getConfig) (← getSimpTheorems) eNew
+  if eNew != e then return .visit eNew else return .done e
+
 @[export lean_dsimp]
 private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let cfg ← getConfig
   unless cfg.dsimp do
     return e
-  let pre (e : Expr) : SimpM TransformStep := do
-    if let Step.visit r ← rewritePre (rflOnly := true) e then
-      if r.expr != e then
-        return .visit r.expr
-    return .continue
-  let post (e : Expr) : SimpM TransformStep := do
-    if let Step.visit r ← rewritePost (rflOnly := true) e then
-      if r.expr != e then
-        return .visit r.expr
-    let mut eNew ← reduce e
-    if eNew.isFVar then
-      eNew ← reduceFVar cfg (← getSimpTheorems) eNew
-    if eNew != e then return .visit eNew else return .done e
+  let m ← getMethods
+  let pre := m.dpre
+  let post := m.dpost >> dsimpReduce
   transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
 def visitFn (e : Expr) : SimpM Result := do
@@ -649,9 +645,9 @@ def simp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (disc
   | none   => Simp.main e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs)
   | some d => Simp.main e ctx usedSimps (methods := Simp.mkMethods simprocs d)
 
-def dsimp (e : Expr) (ctx : Simp.Context)
+def dsimp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[])
     (usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" (← getOptions) do
-  Simp.dsimpMain e ctx usedSimps (methods := Simp.mkDefaultMethodsCore {})
+  Simp.dsimpMain e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs )
 
 /-- 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) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
@@ -800,7 +796,7 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsAr
     else
       return (TacticResultCNM.modified mvarId', usedSimps')
 
-def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
+def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
    mvarId.withContext do
     mvarId.checkNotAssigned `simp
@@ -808,7 +804,7 @@ def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := t
     let mut usedSimps : UsedSimps := usedSimps
     for fvarId in fvarIdsToSimp do
       let type ← instantiateMVars (← fvarId.getType)
-      let (typeNew, usedSimps') ← dsimp type ctx
+      let (typeNew, usedSimps') ← dsimp type ctx simprocs
       usedSimps := usedSimps'
       if typeNew.isFalse then
         mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
@@ -817,7 +813,7 @@ def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := t
         mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId typeNew
     if simplifyTarget then
       let target ← mvarIdNew.getType
-      let (targetNew, usedSimps') ← dsimp target ctx usedSimps
+      let (targetNew, usedSimps') ← dsimp target ctx simprocs usedSimps
       usedSimps := usedSimps'
       if targetNew.isTrue then
         mvarIdNew.assign (mkConst ``True.intro)

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

@@ -319,6 +319,26 @@ def rewritePost (rflOnly := false) : Simproc := fun e => do
       return .visit r
   return .continue
 
+def drewritePre : DSimproc := fun e => do
+  for thms in (← getContext).simpTheorems do
+    if let some r ← rewrite? e thms.pre thms.erased (tag := "pre") (rflOnly := true) then
+      return .visit r.expr
+  return .continue
+
+def drewritePost : DSimproc := fun e => do
+  for thms in (← getContext).simpTheorems do
+    if let some r ← rewrite? e thms.post thms.erased (tag := "post") (rflOnly := true) then
+      return .visit r.expr
+  return .continue
+
+def dpreDefault (s : SimprocsArray) : DSimproc :=
+  drewritePre >>
+  userPreDSimprocs s
+
+def dpostDefault (s : SimprocsArray) : DSimproc :=
+  drewritePost >>
+  userPostDSimprocs s
+
 /--
 Discharge procedure for the ground/symbolic evaluator.
 -/
@@ -382,6 +402,8 @@ def mkSEvalMethods : CoreM Methods := do
   return {
     pre        := preSEval #[s]
     post       := postSEval #[s]
+    dpre       := dpreDefault #[s]
+    dpost      := dpostDefault #[s]
     discharge? := dischargeGround
   }
 
@@ -525,6 +547,8 @@ abbrev Discharge := Expr → SimpM (Option Expr)
 def mkMethods (s : SimprocsArray) (discharge? : Discharge) : Methods := {
   pre        := preDefault s
   post       := postDefault s
+  dpre       := dpreDefault s
+  dpost      := dpostDefault s
   discharge? := discharge?
 }
 

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

@@ -20,7 +20,7 @@ It contains:
 -/
 structure BuiltinSimprocs where
   keys  : HashMap Name (Array SimpTheoremKey) := {}
-  procs : HashMap Name Simproc := {}
+  procs : HashMap Name (Sum Simproc DSimproc) := {}
   deriving Inhabited
 
 /--
@@ -79,7 +79,7 @@ Given a declaration name `declName`, store the discrimination tree keys and the
 
 This method is invoked by the command `builtin_simproc_pattern%` elaborator.
 -/
-def registerBuiltinSimproc (declName : Name) (key : Array SimpTheoremKey) (proc : Simproc) : IO Unit := do
+def registerBuiltinSimprocCore (declName : Name) (key : Array SimpTheoremKey) (proc : Sum Simproc DSimproc) : IO Unit := do
   unless (← initializing) do
     throw (IO.userError s!"invalid builtin simproc declaration, it can only be registered during initialization")
   if (← builtinSimprocDeclsRef.get).keys.contains declName then
@@ -87,6 +87,12 @@ def registerBuiltinSimproc (declName : Name) (key : Array SimpTheoremKey) (proc
   builtinSimprocDeclsRef.modify fun { keys, procs } =>
     { keys := keys.insert declName key, procs := procs.insert declName proc }
 
+def registerBuiltinSimproc (declName : Name) (key : Array SimpTheoremKey) (proc : Simproc) : IO Unit := do
+  registerBuiltinSimprocCore declName key (.inl proc)
+
+def registerBuiltinDSimproc (declName : Name) (key : Array SimpTheoremKey) (proc : DSimproc) : IO Unit := do
+  registerBuiltinSimprocCore declName key (.inr proc)
+
 def registerSimproc (declName : Name) (keys : Array SimpTheoremKey) : CoreM Unit := do
   let env ← getEnv
   unless (env.getModuleIdxFor? declName).isNone do
@@ -112,14 +118,21 @@ builtin_initialize builtinSEvalprocsRef : IO.Ref Simprocs ← IO.mkRef {}
 
 abbrev SimprocExtension := ScopedEnvExtension SimprocOLeanEntry SimprocEntry Simprocs
 
-unsafe def getSimprocFromDeclImpl (declName : Name) : ImportM Simproc := do
+unsafe def getSimprocFromDeclImpl (declName : Name) : ImportM (Sum Simproc DSimproc) := do
   let ctx ← read
-  match ctx.env.evalConstCheck Simproc ctx.opts ``Lean.Meta.Simp.Simproc declName with
-  | .ok proc  => return proc
-  | .error ex => throw (IO.userError ex)
+  match ctx.env.find? declName with
+  | none      => throw <| IO.userError ("unknown constant '" ++ toString declName ++ "'")
+  | some info =>
+    match info.type with
+    | .const ``Simproc _ =>
+      return .inl (← IO.ofExcept <| ctx.env.evalConst Simproc ctx.opts declName)
+    | .const ``DSimproc _ =>
+      return .inr (← IO.ofExcept <| ctx.env.evalConst DSimproc ctx.opts declName)
+    | _ => throw <| IO.userError "unexpected type at simproc"
+
 
 @[implemented_by getSimprocFromDeclImpl]
-opaque getSimprocFromDecl (declName: Name) : ImportM Simproc
+opaque getSimprocFromDecl (declName: Name) : ImportM (Sum Simproc DSimproc)
 
 def toSimprocEntry (e : SimprocOLeanEntry) : ImportM SimprocEntry := do
   return { toSimprocOLeanEntry := e, proc := (← getSimprocFromDecl e.declName) }
@@ -136,7 +149,7 @@ def addSimprocAttrCore (ext : SimprocExtension) (declName : Name) (kind : Attrib
     throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
   ext.add { declName, post, keys, proc } kind
 
-def Simprocs.addCore (s : Simprocs) (keys : Array SimpTheoremKey) (declName : Name) (post : Bool) (proc : Simproc) : Simprocs :=
+def Simprocs.addCore (s : Simprocs) (keys : Array SimpTheoremKey) (declName : Name) (post : Bool) (proc : Sum Simproc DSimproc) : Simprocs :=
   let s := { s with simprocNames := s.simprocNames.insert declName, erased := s.erased.erase declName }
   if post then
     { s with post := s.post.insertCore keys { declName, keys, post, proc } }
@@ -146,15 +159,15 @@ def Simprocs.addCore (s : Simprocs) (keys : Array SimpTheoremKey) (declName : Na
 /--
 Implements attributes `builtin_simproc` and `builtin_sevalproc`.
 -/
-def addSimprocBuiltinAttrCore (ref : IO.Ref Simprocs) (declName : Name) (post : Bool) (proc : Simproc) : IO Unit := do
+def addSimprocBuiltinAttrCore (ref : IO.Ref Simprocs) (declName : Name) (post : Bool) (proc : Sum Simproc DSimproc) : IO Unit := do
   let some keys := (← builtinSimprocDeclsRef.get).keys.find? declName |
     throw (IO.userError "invalid [builtin_simproc] attribute, '{declName}' is not a builtin simproc")
   ref.modify fun s => s.addCore keys declName post proc
 
-def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO Unit :=
+def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Sum Simproc DSimproc) : IO Unit :=
   addSimprocBuiltinAttrCore builtinSimprocsRef declName post proc
 
-def addSEvalprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO Unit :=
+def addSEvalprocBuiltinAttr (declName : Name) (post : Bool) (proc : Sum Simproc DSimproc) : IO Unit :=
   addSimprocBuiltinAttrCore builtinSEvalprocsRef declName post proc
 
 def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs := do
@@ -179,8 +192,25 @@ def SimprocEntry.try (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM
     extraArgs := extraArgs.push e.appArg!
     e := e.appFn!
   extraArgs := extraArgs.reverse
-  let s ← s.proc e
-  s.addExtraArgs extraArgs
+  match s.proc with
+  | .inl proc =>
+    let s ← proc e
+    s.addExtraArgs extraArgs
+  | .inr proc =>
+    let s ← proc e
+    s.toStep.addExtraArgs extraArgs
+
+/-- Similar to `try`, but only consider `DSimproc` case. That is, if `s.proc` is a `Simproc`, treat it as a `.continue`. -/
+def SimprocEntry.tryD (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM DStep := do
+  let mut extraArgs := #[]
+  let mut e := e
+  for _ in [:numExtraArgs] do
+    extraArgs := extraArgs.push e.appArg!
+    e := e.appFn!
+  extraArgs := extraArgs.reverse
+  match s.proc with
+  | .inl _ => return .continue
+  | .inr proc => return (← proc e).addExtraArgs extraArgs
 
 def simprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM Step := do
   let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
@@ -219,6 +249,39 @@ def simprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Ex
     else
       return .continue
 
+def dsimprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM DStep := do
+  let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+  if candidates.isEmpty then
+    let tag := if post then "post" else "pre"
+    trace[Debug.Meta.Tactic.simp] "no {tag}-simprocs found for {e}"
+    return .continue
+  else
+    let mut e  := e
+    let mut found := false
+    for (simprocEntry, numExtraArgs) in candidates do
+      unless erased.contains simprocEntry.declName do
+        let s ← simprocEntry.tryD numExtraArgs e
+        match s with
+        | .visit eNew =>
+          trace[Debug.Meta.Tactic.simp] "simproc result {e} => {eNew}"
+          recordSimpTheorem (.decl simprocEntry.declName post)
+          return .visit eNew
+        | .done eNew =>
+          trace[Debug.Meta.Tactic.simp] "simproc result {e} => {eNew}"
+          recordSimpTheorem (.decl simprocEntry.declName post)
+          return .done eNew
+        | .continue (some eNew) =>
+          trace[Debug.Meta.Tactic.simp] "simproc result {e} => {eNew}"
+          recordSimpTheorem (.decl simprocEntry.declName post)
+          e := eNew
+          found := true
+        | .continue none =>
+          pure ()
+    if found then
+      return .continue (some e)
+    else
+      return .continue
+
 abbrev SimprocsArray := Array Simprocs
 
 def SimprocsArray.add (ss : SimprocsArray) (declName : Name) (post : Bool) : CoreM SimprocsArray :=
@@ -254,6 +317,22 @@ def simprocArrayCore (post : Bool) (ss : SimprocsArray) (e : Expr) : SimpM Step
   else
     return .continue
 
+def dsimprocArrayCore (post : Bool) (ss : SimprocsArray) (e : Expr) : SimpM DStep := do
+  let mut found := false
+  let mut e  := e
+  for s in ss do
+    match (← dsimprocCore (post := post) (if post then s.post else s.pre) s.erased e) with
+    | .visit eNew => return .visit eNew
+    | .done eNew =>  return .done eNew
+    | .continue none => pure ()
+    | .continue (some eNew) =>
+      e := eNew
+      found := true
+  if found then
+    return .continue (some e)
+  else
+    return .continue
+
 register_builtin_option simprocs : Bool := {
   defValue := true
   group    := "backward compatibility"
@@ -268,6 +347,14 @@ def userPostSimprocs (s : SimprocsArray) : Simproc := fun e => do
   unless simprocs.get (← getOptions) do return .continue
   simprocArrayCore (post := true) s e
 
+def userPreDSimprocs (s : SimprocsArray) : DSimproc := fun e => do
+  unless simprocs.get (← getOptions) do return .continue
+  dsimprocArrayCore (post := false) s e
+
+def userPostDSimprocs (s : SimprocsArray) : DSimproc := fun e => do
+  unless simprocs.get (← getOptions) do return .continue
+  dsimprocArrayCore (post := true) s e
+
 def mkSimprocExt (name : Name := by exact decl_name%) (ref? : Option (IO.Ref Simprocs)) : IO SimprocExtension :=
   registerScopedEnvExtension {
     name          := name
@@ -315,7 +402,11 @@ builtin_initialize simprocSEvalExtension : SimprocExtension ← registerSimprocA
 private def addBuiltin (declName : Name) (stx : Syntax) (addDeclName : Name) : AttrM Unit := do
   let go : MetaM Unit := do
     let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-    let val := mkAppN (mkConst addDeclName) #[toExpr declName, toExpr post, mkConst declName]
+    let procExpr ← match (← getConstInfo declName).type with
+      | .const ``Simproc _  => pure <| mkApp3 (mkConst ``Sum.inl [0, 0]) (mkConst ``Simproc) (mkConst ``DSimproc) (mkConst declName)
+      | .const ``DSimproc _ => pure <| mkApp3 (mkConst ``Sum.inr [0, 0]) (mkConst ``Simproc) (mkConst ``DSimproc) (mkConst declName)
+      | _ => throwError "unexpected type at simproc"
+    let val := mkAppN (mkConst addDeclName) #[toExpr declName, toExpr post, procExpr]
     let initDeclName ← mkFreshUserName (declName ++ `declare)
     declareBuiltin initDeclName val
   go.run' {}

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

@@ -146,6 +146,20 @@ See `Step`.
 -/
 abbrev Simproc := Expr → SimpM Step
 
+abbrev DStep := TransformStep
+
+/--
+Similar to `Simproc`, but resulting expression should be definitionally equal to the input one.
+-/
+abbrev DSimproc := Expr → SimpM DStep
+
+def _root_.Lean.TransformStep.toStep (s : TransformStep) : Step :=
+  match s with
+  | .done e            => .done { expr := e }
+  | .visit e           => .visit { expr := e }
+  | .continue (some e) => .continue (some { expr := e })
+  | .continue none     => .continue none
+
 def mkEqTransResultStep (r : Result) (s : Step) : MetaM Step :=
   match s with
   | .done r'            => return .done (← mkEqTransOptProofResult r.proof? r.cache r')
@@ -171,6 +185,17 @@ def andThen (f g : Simproc) : Simproc := fun e => do
 instance : AndThen Simproc where
   andThen s₁ s₂ := andThen s₁ (s₂ ())
 
+@[always_inline]
+def dandThen (f g : DSimproc) : DSimproc := fun e => do
+  match (← f e) with
+  | .done eNew            => return .done eNew
+  | .continue none        => g e
+  | .continue (some eNew) => g eNew
+  | .visit eNew           => return .visit eNew
+
+instance : AndThen DSimproc where
+  andThen s₁ s₂ := dandThen s₁ (s₂ ())
+
 /--
 `Simproc` .olean entry.
 -/
@@ -189,7 +214,7 @@ structure SimprocEntry extends SimprocOLeanEntry where
   Recall that we cannot store `Simproc` into .olean files because it is a closure.
   Given `SimprocOLeanEntry.declName`, we convert it into a `Simproc` by using the unsafe function `evalConstCheck`.
   -/
-  proc : Simproc
+  proc : Sum Simproc DSimproc
 
 abbrev SimprocTree := DiscrTree SimprocEntry
 
@@ -203,6 +228,8 @@ structure Simprocs where
 structure Methods where
   pre        : Simproc                    := fun _ => return .continue
   post       : Simproc                    := fun e => return .done { expr := e }
+  dpre       : DSimproc                   := fun _ => return .continue
+  dpost      : DSimproc                   := fun e => return .done e
   discharge? : Expr → SimpM (Option Expr) := fun _ => return none
   deriving Inhabited
 
@@ -529,6 +556,13 @@ def Step.addExtraArgs (s : Step) (extraArgs : Array Expr) : MetaM Step := do
   | .continue none => return .continue none
   | .continue (some r) => return .continue (← r.addExtraArgs extraArgs)
 
+def DStep.addExtraArgs (s : DStep) (extraArgs : Array Expr) : DStep :=
+  match s with
+  | .visit eNew => .visit (mkAppN eNew extraArgs)
+  | .done eNew => .done (mkAppN eNew extraArgs)
+  | .continue none => .continue none
+  | .continue (some eNew) => .continue (mkAppN eNew extraArgs)
+
 end Simp
 
 export Simp (SimpM Simprocs)

src/Lean/Meta/Transform.lean

@@ -21,6 +21,7 @@ inductive TransformStep where
   For `pre`, this means visiting the children of the expression.
   For `post`, this is equivalent to returning `done`. -/
   | continue (e? : Option Expr := none)
+  deriving Inhabited
 
 namespace Core
 

tests/lean/run/dsimp_bv_simproc.lean

@@ -0,0 +1,30 @@
+open BitVec
+
+variable (write : (n : Nat) → BitVec 64 → BitVec (n * 8) → Type → Type)
+
+theorem write_simplify_test_0 (a x y : BitVec 64)
+  (h : ((8 * 8) + 8 * 8) = 2 * ((8 * 8) / 8) * 8) :
+  write (2 * ((8 * 8) / 8)) a (BitVec.cast h (zeroExtend (8 * 8) x ++ (zeroExtend (8 * 8) y))) s
+  =
+  write 16 a (x ++ y) s := by
+  simp only [zeroExtend_eq, BitVec.cast_eq]
+
+/--
+warning: declaration uses 'sorry'
+---
+info: write : (n : Nat) → BitVec 64 → BitVec (n * 8) → Type → Type
+s aux : Type
+a x y : BitVec 64
+h : 128 = 128
+⊢ write 16 a (x ++ y) s = aux
+-/
+#guard_msgs in
+example (a x y : BitVec 64)
+  (h : ((8 * 8) + 8 * 8) = 2 * ((8 * 8) / 8) * 8) :
+  write (2 * ((8 * 8) / 8)) a (BitVec.cast h (zeroExtend (8 * 8) x ++ (zeroExtend (8 * 8) y))) s
+  =
+  aux := by
+  simp
+  dsimp at h
+  trace_state
+  sorry

tests/lean/run/dsimproc.lean

@@ -0,0 +1,64 @@
+import Lean
+
+def foo (x : Nat) := x + 1
+
+open Lean Meta Simp
+dsimproc reduceFoo (foo _) := fun e => do
+  let_expr foo a ← e | return .continue
+  let some n ← getNatValue? a | return .continue
+  return .done (toExpr (n+1))
+
+example (h : 3 = x) : foo 2 = x := by
+  simp
+  guard_target =ₛ 3 = x
+  assumption
+
+example (h : 3 = x) : foo 2 = x := by
+  fail_if_success simp [-reduceFoo]
+  fail_if_success simp only
+  simp only [reduceFoo]
+  guard_target =ₛ 3 = x
+  assumption
+
+def bla (x : Nat) := 2*x
+
+dsimproc_decl reduceBla (bla _) := fun e => do
+  let_expr bla a ← e | return .continue
+  let some n ← getNatValue? a | return .continue
+  return .done (toExpr (2*n))
+
+example (h : 6 = x) : bla 3 = x := by
+  fail_if_success simp
+  fail_if_success simp only
+  simp [bla]
+  guard_target =ₛ 6 = x
+  assumption
+
+example (h : 6 = x) : bla 3 = x := by
+  fail_if_success simp
+  fail_if_success simp only
+  simp [bla]
+  guard_target =ₛ 6 = x
+  assumption
+
+example (h : 6 = x) : bla 3 = x := by
+  simp only [bla]
+  guard_target =ₛ 2*3 = x
+  assumption
+
+example (h : 6 = x) : bla 3 = x := by
+  simp only [bla, Nat.reduceMul]
+  guard_target =ₛ 6 = x
+  assumption
+
+attribute [simp] reduceBla
+
+example (h : 6 = x) : bla 3 = x := by
+  simp
+  guard_target =ₛ 6 = x
+  assumption
+
+example (h : 5 = x) : 2 + 3 = x := by
+  dsimp
+  guard_target =ₛ 5 = x
+  assumption