fix: tolerate missing simp and simproc sets

When we declare a `simp` set using `register_simp_attr`, we
automatically create `simproc` set. However, users may create `simp`
sets programmatically, and the associated `simproc` set may be missing
and vice-versa.

RELEASES.md

@@ -22,20 +22,25 @@ def foo (x : Nat) : Nat :=
 The `simproc` `reduceFoo` is invoked on terms that match the pattern `foo _`.
 -/
 simproc reduceFoo (foo _) :=
-  /- A term of type `Expr → SimpM (Option Step) -/
-  fun e => OptionT.run do
-    /- `simp` uses matching modulo reducibility. So, we ensure the term is a `foo`-application. -/
-    guard (e.isAppOfArity ``foo 1)
-    /- `Nat.fromExpr?` tries to convert an expression into a `Nat` value -/
-    let n ← Nat.fromExpr? e.appArg!
+  /- A term of type `Expr → SimpM Step -/
+  fun e => do
     /-
-    The `Step` type has two constructors: `.done` and `.visit`.
+    The `Step` type has three constructors: `.done`, `.visit`, `.continue`.
     * The constructor `.done` instructs `simp` that the result does
       not need to be simplied further.
     * The constructor `.visit` instructs `simp` to visit the resulting expression.
+    * The constructor `.continue` instructs `simp` to try other simplification procedures.
 
-    If the result holds definitionally as in this example, the field `proof?` can be omitted.
+    All three constructors take a `Result`. The `.continue` contructor may also take `none`.
+    `Result` has two fields `expr` (the new expression), and `proof?` (an optional proof).
+     If the new expression is definitionally equal to the input one, then `proof?` can be omitted or set to `none`.
     -/
+    /- `simp` uses matching modulo reducibility. So, we ensure the term is a `foo`-application. -/
+    unless e.isAppOfArity ``foo 1 do
+      return .continue
+    /- `Nat.fromExpr?` tries to convert an expression into a `Nat` value -/
+    let some n ← Nat.fromExpr? e.appArg!
+      | return .continue
     return .done { expr := Lean.mkNatLit (n+10) }
 ```
 We disable simprocs support by using the command `set_option simprocs false`. This command is particularly useful when porting files to v4.6.0.
@@ -64,6 +69,10 @@ example : x + foo 2 = 12 + x := by
   fail_if_success simp [-reduceFoo]
   simp_arith
 ```
+The command `register_simp_attr <id>` now creates a `simp` **and** a `simproc` set with the name `<id>`. The following command instructs Lean to insert the `reduceFoo` simplification procedure into the set `my_simp`. If no set is specified, Lean uses the default `simp` set.
+```lean
+simproc [my_simp] reduceFoo (foo _) := ...
+```
 
 * The syntax of the `termination_by` and `decreasing_by` termination hints is overhauled:
 

src/Init/Simproc.lean

@@ -29,7 +29,7 @@ simproc ↓ reduce_add (_ + _) := fun e => ...
 ```
 Simplification procedures can be also scoped or local.
 -/
-syntax (docComment)? attrKind "simproc " (Tactic.simpPre <|> Tactic.simpPost)? ident " (" term ")" " := " term : command
+syntax (docComment)? attrKind "simproc " (Tactic.simpPre <|> Tactic.simpPost)? ("[" ident,* "]")? ident " (" term ")" " := " term : command
 
 /--
 A user-defined simplification procedure declaration. To activate this procedure in `simp` tactic,
@@ -40,7 +40,7 @@ syntax (docComment)? "simproc_decl " ident " (" term ")" " := " term : command
 /--
 A builtin simplification procedure.
 -/
-syntax (docComment)? attrKind "builtin_simproc " (Tactic.simpPre <|> Tactic.simpPost)? ident " (" term ")" " := " term : command
+syntax (docComment)? attrKind "builtin_simproc " (Tactic.simpPre <|> Tactic.simpPost)? ("[" ident,* "]")? ident " (" term ")" " := " term : command
 
 /--
 A builtin simplification procedure declaration.
@@ -63,10 +63,21 @@ Auxiliary attribute for simplification procedures.
 -/
 syntax (name := simprocAttr) "simproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
 
+/--
+Auxiliary attribute for symbolic evaluation procedures.
+-/
+syntax (name := sevalprocAttr) "sevalproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+
 /--
 Auxiliary attribute for builtin simplification procedures.
 -/
 syntax (name := simprocBuiltinAttr) "builtin_simproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+
+/--
+Auxiliary attribute for builtin symbolic evaluation procedures.
+-/
+syntax (name := sevalprocBuiltinAttr) "builtin_sevalproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+
 end Attr
 
 macro_rules
@@ -82,13 +93,37 @@ macro_rules
       builtin_simproc_pattern% $pattern => $n)
 
 macro_rules
-  | `($[$doc?:docComment]? $kind:attrKind simproc $[$pre?]? $n:ident ($pattern:term) := $body) => do
-    `(simproc_decl $n ($pattern) := $body
-      attribute [$kind simproc $[$pre?]?] $n)
+  | `($[$doc?:docComment]? $kind:attrKind simproc $[$pre?]? $[ [ $ids?:ident,* ] ]? $n:ident ($pattern:term) := $body) => do
+     let mut cmds := #[(← `(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
 
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind builtin_simproc $[$pre?]? $n:ident ($pattern:term) := $body) => do
     `(builtin_simproc_decl $n ($pattern) := $body
       attribute [$kind builtin_simproc $[$pre?]?] $n)
+  | `($[$doc?:docComment]? $kind:attrKind builtin_simproc $[$pre?]? [seval] $n:ident ($pattern:term) := $body) => do
+    `(builtin_simproc_decl $n ($pattern) := $body
+      attribute [$kind builtin_sevalproc $[$pre?]?] $n)
+  | `($[$doc?:docComment]? $kind:attrKind builtin_simproc $[$pre?]? [simp, seval] $n:ident ($pattern:term) := $body) => do
+    `(builtin_simproc_decl $n ($pattern) := $body
+      attribute [$kind builtin_simproc $[$pre?]?] $n
+      attribute [$kind builtin_sevalproc $[$pre?]?] $n)
 
 end Lean.Parser

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -44,19 +44,17 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
 def simpMatchWF? (mvarId : MVarId) : MetaM (Option MVarId) :=
   mvarId.withContext do
     let target ← instantiateMVars (← mvarId.getType)
-    let (targetNew, _) ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre })
+    let (targetNew, _) ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre, discharge? := SplitIf.discharge? })
     let mvarIdNew ← applySimpResultToTarget mvarId target targetNew
     if mvarId != mvarIdNew then return some mvarIdNew else return none
 where
   pre (e : Expr) : SimpM Simp.Step := do
-    let some app ← matchMatcherApp? e | return Simp.Step.visit { expr := e }
+    let some app ← matchMatcherApp? e
+      | return Simp.Step.continue
     -- First try to reduce matcher
     match (← reduceRecMatcher? e) with
     | some e' => return Simp.Step.done { expr := e' }
-    | none    =>
-      match (← Simp.simpMatchCore? app.matcherName e SplitIf.discharge?) with
-      | some r => return r
-      | none => return Simp.Step.visit { expr := e }
+    | none    => Simp.simpMatchCore app.matcherName e
 
 /--
   Given a goal of the form `|- f.{us} a_1 ... a_n b_1 ... b_m = ...`, return `(us, #[a_1, ..., a_n])`

src/Lean/Elab/Tactic/Conv/Pattern.lean

@@ -82,7 +82,7 @@ end PatternMatchState
 
 private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchState) (e : Expr) : SimpM Simp.Step := do
   if (← state.get).isDone then
-    return Simp.Step.visit { expr := e }
+    return Simp.Step.done { expr := e }
   else if let some (e, extraArgs) ← matchPattern? pattern e then
     if (← state.get).isReady then
       let (rhs, newGoal) ← mkConvGoalFor e
@@ -97,9 +97,9 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat
       -- it is possible for skipping an earlier match to affect what later matches
       -- refer to. For example, matching `f _` in `f (f a) = f b` with occs `[1, 2]`
       -- yields `[f (f a), f b]`, but `[2, 3]` yields `[f a, f b]`, and `[1, 3]` is an error.
-      return Simp.Step.visit { expr := e }
+      return Simp.Step.continue
   else
-    return Simp.Step.visit { expr := e }
+    return Simp.Step.continue
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.pattern] def evalPattern : Tactic := fun stx => withMainContext do
   match stx with

src/Lean/Elab/Tactic/Simp.lean

@@ -130,21 +130,28 @@ private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (p
 
 structure ElabSimpArgsResult where
   ctx      : Simp.Context
-  simprocs : Simprocs
+  simprocs : Simp.SimprocsArray
   starArg  : Bool := false
 
 inductive ResolveSimpIdResult where
   | none
   | expr (e : Expr)
   | simproc (declName : Name)
-  | ext  (ext : SimpExtension)
+  /--
+  Recall that when we declare a `simp` attribute using `register_simp_attr`, we automatically
+  create a `simproc` attribute. However, if the user creates `simp` and `simproc` attributes
+  programmatically, then one of them may be missing. Moreover, when we write `simp [seval]`,
+  we want to retrieve both the simp and simproc sets. We want to hide from users that
+  `simp` and `simproc` sets are stored in different data-structures.
+  -/
+  | ext  (ext₁? : Option SimpExtension) (ext₂? : Option Simp.SimprocExtension) (h : ext₁?.isSome || ext₂?.isSome)
 
 /--
   Elaborate extra simp theorems provided to `simp`. `stx` is of the form `"[" simpTheorem,* "]"`
   If `eraseLocal == true`, then we consider local declarations when resolving names for erased theorems (`- id`),
   this option only makes sense for `simp_all` or `*` is used.
 -/
-def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simprocs) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
+def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
   if stx.isNone then
     return { ctx, simprocs }
   else
@@ -188,8 +195,13 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simprocs) (eras
             thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
           | .simproc declName =>
             simprocs ← simprocs.add declName post
-          | .ext ext =>
-            thmsArray := thmsArray.push (← ext.getTheorems)
+          | .ext (some ext₁) (some ext₂) _ =>
+            thmsArray := thmsArray.push (← ext₁.getTheorems)
+            simprocs  := simprocs.push (← ext₂.getSimprocs)
+          | .ext (some ext₁) none _ =>
+            thmsArray := thmsArray.push (← ext₁.getTheorems)
+          | .ext none (some ext₂) _ =>
+            simprocs  := simprocs.push (← ext₂.getSimprocs)
           | .none    =>
             let name ← mkFreshId
             thms ← addSimpTheorem thms (.stx name arg) term post inv
@@ -206,8 +218,10 @@ where
 
   resolveSimpIdTheorem? (simpArgTerm : Term) : TacticM ResolveSimpIdResult := do
     let resolveExt (n : Name) : TacticM ResolveSimpIdResult := do
-      if let some ext ← getSimpExtension? n then
-        return .ext ext
+      let ext₁? ← getSimpExtension? n
+      let ext₂? ← Simp.getSimprocExtension? n
+      if h : ext₁?.isSome || ext₂?.isSome then
+        return .ext ext₁? ext₂? h
       else
         return .none
     match simpArgTerm with
@@ -236,7 +250,7 @@ where
 
 structure MkSimpContextResult where
   ctx              : Simp.Context
-  simprocs         : Simprocs
+  simprocs         : Simp.SimprocsArray
   dischargeWrapper : Simp.DischargeWrapper
 
 /--
@@ -259,7 +273,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
     getSimpTheorems
   let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← getSimpCongrTheorems
-  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := simprocs) {
+  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) {
     config      := (← elabSimpConfig stx[1] (kind := kind))
     simpTheorems := #[simpTheorems], congrTheorems
   }
@@ -361,7 +375,7 @@ For many tactics other than the simplifier,
 one should use the `withLocation` tactic combinator
 when working with a `location`.
 -/
-def simpLocation (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
+def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do

src/Lean/Elab/Tactic/Simproc.lean

@@ -52,34 +52,4 @@ namespace Command
 
 end Command
 
-builtin_initialize
-  registerBuiltinAttribute {
-    ref             := by exact decl_name%
-    name            := `simprocAttr
-    descr           := "Simplification procedure"
-    erase           := eraseSimprocAttr
-    add             := fun declName stx attrKind => do
-      let go : MetaM Unit := do
-        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-        addSimprocAttr declName attrKind post
-      go.run' {}
-    applicationTime := AttributeApplicationTime.afterCompilation
-  }
-
-builtin_initialize
-  registerBuiltinAttribute {
-    ref             := by exact decl_name%
-    name            := `simprocBuiltinAttr
-    descr           := "Builtin simplification procedure"
-    erase           := eraseSimprocAttr
-    add             := fun declName stx _ => 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 ``addSimprocBuiltinAttr) #[toExpr declName, toExpr post, mkConst declName]
-        let initDeclName ← mkFreshUserName (declName ++ `declare)
-        declareBuiltin initDeclName val
-      go.run' {}
-    applicationTime := AttributeApplicationTime.afterCompilation
-  }
-
 end Lean.Elab

src/Lean/Linter/MissingDocs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Mario Carneiro
 -/
-import Lean.Meta.Tactic.Simp.SimpTheorems
+import Lean.Meta.Tactic.Simp.RegisterCommand
 import Lean.Elab.Command
 import Lean.Elab.SetOption
 import Lean.Linter.Util

src/Lean/Meta/AppBuilder.lean

@@ -123,6 +123,17 @@ def mkEqTrans (h₁ h₂ : Expr) : MetaM Expr := do
     | none, _ => throwAppBuilderException ``Eq.trans ("equality proof expected" ++ hasTypeMsg h₁ hType₁)
     | _, none => throwAppBuilderException ``Eq.trans ("equality proof expected" ++ hasTypeMsg h₂ hType₂)
 
+/--
+Similar to `mkEqTrans`, but arguments can be `none`.
+`none` is treated as a reflexivity proof.
+-/
+def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
+  match h₁?, h₂? with
+  | none, none       => return none
+  | none, some h     => return h
+  | some h, none     => return h
+  | some h₁, some h₂ => mkEqTrans h₁ h₂
+
 /-- Given `h : HEq a b`, returns a proof of `HEq b a`.  -/
 def mkHEqSymm (h : Expr) : MetaM Expr := do
   if h.isAppOf ``HEq.refl then

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

@@ -8,7 +8,7 @@ import Lean.Meta.Tactic.LinearArith.Nat.Simp
 
 namespace Lean.Meta.Linear
 
-private def parentIsTarget (parent? : Option Expr) : Bool :=
+def parentIsTarget (parent? : Option Expr) : Bool :=
   match parent? with
   | none => false
   | some parent => isLinearTerm parent || isLinearCnstr parent

src/Lean/Meta/Tactic/Simp.lean

@@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Simp.Rewrite
 import Lean.Meta.Tactic.Simp.SimpAll
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs
+import Lean.Meta.Tactic.Simp.RegisterCommand
 
 namespace Lean
 

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

@@ -7,8 +7,8 @@ import Lean.Meta.Tactic.Simp.Simproc
 
 open Lean Meta Simp
 
-builtin_simproc ↓ reduceIte (ite _ _ _) := fun e => OptionT.run do
-  guard (e.isAppOfArity ``ite 5)
+builtin_simproc ↓ [simp, seval] reduceIte (ite _ _ _) := fun e => do
+  unless e.isAppOfArity ``ite 5 do return .continue
   let c := e.getArg! 1
   let r ← simp c
   if r.expr.isConstOf ``True then
@@ -19,10 +19,10 @@ builtin_simproc ↓ reduceIte (ite _ _ _) := fun e => OptionT.run do
     let eNew  := e.getArg! 4
     let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
     return .visit { expr := eNew, proof? := pr }
-  failure
+  return .continue
 
-builtin_simproc ↓ reduceDite (dite _ _ _) := fun e => OptionT.run do
-  guard (e.isAppOfArity ``dite 5)
+builtin_simproc ↓ [simp, seval] reduceDite (dite _ _ _) := fun e => do
+  unless e.isAppOfArity ``dite 5 do return .continue
   let c := e.getArg! 1
   let r ← simp c
   if r.expr.isConstOf ``True then
@@ -37,4 +37,4 @@ builtin_simproc ↓ reduceDite (dite _ _ _) := fun e => OptionT.run do
     let eNew  := mkApp (e.getArg! 4) h |>.headBeta
     let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) pr
     return .visit { expr := eNew, proof? := prNew }
-  failure
+  return .continue

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

@@ -14,7 +14,7 @@ structure Value where
   size      : Nat
   value     : Nat
 
-def fromExpr? (e : Expr) : OptionT SimpM Value := do
+def fromExpr? (e : Expr) : SimpM (Option Value) := OptionT.run do
   guard (e.isAppOfArity ``OfNat.ofNat 3)
   let type ← whnf e.appFn!.appFn!.appArg!
   guard (type.isAppOfArity ``Fin 1)
@@ -28,18 +28,18 @@ def Value.toExpr (v : Value) : Expr :=
   let vExpr := mkRawNatLit v.value
   mkApp2 v.ofNatFn vExpr (mkApp2 (mkConst ``Fin.instOfNat) (Lean.toExpr (v.size - 1)) vExpr)
 
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : OptionT SimpM Step := do
-  guard (e.isAppOfArity declName arity)
-  let v₁ ← fromExpr? e.appFn!.appArg!
-  let v₂ ← fromExpr? e.appArg!
-  guard (v₁.size == v₂.size)
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (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
+  unless v₁.size == v₂.size do return .continue
   let v := { v₁ with value := op v₁.value v₂.value % v₁.size }
   return .done { expr := v.toExpr }
 
-@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : OptionT SimpM Step := do
-  guard (e.isAppOfArity declName arity)
-  let v₁ ← fromExpr? e.appFn!.appArg!
-  let v₂ ← fromExpr? e.appArg!
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → 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
   let d ← mkDecide e
   if op v₁.value v₂.value then
     return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
@@ -51,20 +51,20 @@ The following code assumes users did not override the `Fin n` instances for the
 If they do, they must disable the following `simprocs`.
 -/
 
-builtin_simproc reduceAdd ((_ + _ : Fin _)) := reduceBin ``HAdd.hAdd 6 (· + ·)
-builtin_simproc reduceMul ((_ * _ : Fin _)) := reduceBin ``HMul.hMul 6 (· * ·)
-builtin_simproc reduceSub ((_ - _ : Fin _)) := reduceBin ``HSub.hSub 6 (· - ·)
-builtin_simproc reduceDiv ((_ / _ : Fin _)) := reduceBin ``HDiv.hDiv 6 (· / ·)
-builtin_simproc reduceMod ((_ % _ : Fin _)) := reduceBin ``HMod.hMod 6 (· % ·)
+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_simproc reduceLT  (( _ : Fin _) < _)  := reduceBinPred ``LT.lt 4 (. < .)
-builtin_simproc reduceLE  (( _ : Fin _) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
-builtin_simproc reduceGT  (( _ : Fin _) > _)  := reduceBinPred ``GT.gt 4 (. > .)
-builtin_simproc reduceGE  (( _ : Fin _) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+builtin_simproc [simp, seval] reduceLT  (( _ : Fin _) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc [simp, seval] reduceLE  (( _ : Fin _) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc [simp, seval] reduceGT  (( _ : Fin _) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc [simp, seval] reduceGE  (( _ : Fin _) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
 
-/-- Return `.done` for Fin values. We don't want to unfold them when `ground := true`. -/
-builtin_simproc isValue ((OfNat.ofNat _ : Fin _)) := fun e => OptionT.run do
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
+/-- Return `.done` for Fin values. We don't want to unfold in the symbolic evaluator. -/
+builtin_simproc [seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
+  unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue
   return .done { expr := e }
 
 end Fin

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

@@ -9,7 +9,7 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 namespace Int
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : OptionT SimpM Int := do
+def fromExpr? (e : Expr) : SimpM (Option Int) := OptionT.run do
   let mut e := e
   let mut isNeg := false
   if e.isAppOfArity ``Neg.neg 3 then
@@ -32,21 +32,21 @@ def toExpr (v : Int) : Expr :=
   else
     e
 
-@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Int → Int) (e : Expr) : OptionT SimpM Step := do
-  guard (e.isAppOfArity declName arity)
-  let n ← fromExpr? e.appArg!
+@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Int → Int) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some n ← fromExpr? e.appArg! | return .continue
   return .done { expr := toExpr (op n) }
 
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Int → Int → Int) (e : Expr) : OptionT SimpM Step := do
-  guard (e.isAppOfArity declName arity)
-  let v₁ ← fromExpr? e.appFn!.appArg!
-  let v₂ ← fromExpr? e.appArg!
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Int → Int → Int) (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
   return .done { expr := toExpr (op v₁ v₂) }
 
-@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Int → Int → Bool) (e : Expr) : OptionT SimpM Step := OptionT.run do
-  guard (e.isAppOfArity declName arity)
-  let v₁ ← fromExpr? e.appFn!.appArg!
-  let v₂ ← fromExpr? e.appArg!
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Int → Int → 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
   let d ← mkDecide e
   if op v₁ v₂ then
     return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
@@ -58,45 +58,44 @@ The following code assumes users did not override the `Int` instances for the ar
 If they do, they must disable the following `simprocs`.
 -/
 
-builtin_simproc reduceNeg ((- _ : Int)) := fun e => OptionT.run do
-  guard (e.isAppOfArity ``Neg.neg 3)
+builtin_simproc [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`.
-    guard (← getContext).unfoldGround
     return .done { expr := e }
   else
-    let v ← fromExpr? arg
+    let some v ← fromExpr? arg | return .continue
     if v < 0 then
       return .done { expr := toExpr (- v) }
     else
       return .done { expr := toExpr v }
 
-/-- Return `.done` for positive Int values. We don't want to unfold them when `ground := true`. -/
-builtin_simproc isPosValue ((OfNat.ofNat _ : Int)) := fun e => OptionT.run do
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
+/-- 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
+  unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue
   return .done { expr := e }
 
-builtin_simproc reduceAdd ((_ + _ : Int)) := reduceBin ``HAdd.hAdd 6 (· + ·)
-builtin_simproc reduceMul ((_ * _ : Int)) := reduceBin ``HMul.hMul 6 (· * ·)
-builtin_simproc reduceSub ((_ - _ : Int)) := reduceBin ``HSub.hSub 6 (· - ·)
-builtin_simproc reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv 6 (· / ·)
-builtin_simproc reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
+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_simproc reducePow ((_ : Int) ^ (_ : Nat)) := fun e => OptionT.run do
-  guard (e.isAppOfArity ``HPow.hPow 6)
-  let v₁ ← fromExpr? e.appFn!.appArg!
-  let v₂ ← Nat.fromExpr? e.appArg!
+builtin_simproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
+  unless e.isAppOfArity ``HPow.hPow 6 do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← Nat.fromExpr? e.appArg! | return .continue
   return .done { expr := toExpr (v₁ ^ v₂) }
 
-builtin_simproc reduceAbs (natAbs _) := fun e => OptionT.run do
-  guard (e.isAppOfArity ``natAbs 1)
-  let v ← fromExpr? e.appArg!
+builtin_simproc [simp, seval] reduceAbs (natAbs _) := fun e => do
+  unless e.isAppOfArity ``natAbs 1 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
   return .done { expr := mkNatLit (natAbs v) }
 
-builtin_simproc reduceLT  (( _ : Int) < _)  := reduceBinPred ``LT.lt 4 (. < .)
-builtin_simproc reduceLE  (( _ : Int) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
-builtin_simproc reduceGT  (( _ : Int) > _)  := reduceBinPred ``GT.gt 4 (. > .)
-builtin_simproc reduceGE  (( _ : Int) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+builtin_simproc [simp, seval] reduceLT  (( _ : Int) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc [simp, seval] reduceLE  (( _ : Int) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc [simp, seval] reduceGT  (( _ : Int) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc [simp, seval] reduceGE  (( _ : Int) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
 
 end Int

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

@@ -13,51 +13,50 @@ def fromExpr? (e : Expr) : SimpM (Option Nat) := do
   let some n ← evalNat e |>.run | return none
   return n
 
-@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : OptionT SimpM Step := do
-  guard (e.isAppOfArity declName arity)
-  let n ← fromExpr? e.appArg!
+@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some n ← fromExpr? e.appArg! | return .continue
   return .done { expr := mkNatLit (op n) }
 
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : OptionT SimpM Step := do
-  guard (e.isAppOfArity declName arity)
-  let n ← fromExpr? e.appFn!.appArg!
-  let m ← fromExpr? e.appArg!
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM Step := 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 := mkNatLit (op n m) }
 
-@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : OptionT SimpM Step := do
-  guard (e.isAppOfArity declName arity)
-  let n ← fromExpr? e.appFn!.appArg!
-  let m ← fromExpr? e.appArg!
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := 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
   let d ← mkDecide e
   if op n m then
     return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
   else
     return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
 
-builtin_simproc reduceSucc (Nat.succ _) := reduceUnary ``Nat.succ 1 (· + 1)
+builtin_simproc [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 reduceAdd ((_ + _ : Nat)) := reduceBin ``HAdd.hAdd 6 (· + ·)
-builtin_simproc reduceMul ((_ * _ : Nat)) := reduceBin ``HMul.hMul 6 (· * ·)
-builtin_simproc reduceSub ((_ - _ : Nat)) := reduceBin ``HSub.hSub 6 (· - ·)
-builtin_simproc reduceDiv ((_ / _ : Nat)) := reduceBin ``HDiv.hDiv 6 (· / ·)
-builtin_simproc reduceMod ((_ % _ : Nat)) := reduceBin ``HMod.hMod 6 (· % ·)
-builtin_simproc reducePow ((_ ^ _ : Nat)) := reduceBin ``HPow.hPow 6 (· ^ ·)
-builtin_simproc reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd
+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_simproc reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)
-builtin_simproc reduceLE  (( _ : Nat) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
-builtin_simproc reduceGT  (( _ : Nat) > _)  := reduceBinPred ``GT.gt 4 (. > .)
-builtin_simproc reduceGE  (( _ : Nat) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+builtin_simproc [simp, seval] reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc [simp, seval] reduceLE  (( _ : Nat) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc [simp, seval] reduceGT  (( _ : Nat) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc [simp, seval] reduceGE  (( _ : Nat) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
 
-/-- Return `.done` for Nat values. We don't want to unfold them when `ground := true`. -/
-builtin_simproc isValue ((OfNat.ofNat _ : Nat)) := fun e => OptionT.run do
-  guard (← getContext).unfoldGround
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
+/-- 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
+  unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue
   return .done { expr := e }
 
 end Nat

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

@@ -30,38 +30,37 @@ def $toExpr (v : Value) : Expr :=
   let vExpr := mkRawNatLit v.value.val
   mkApp2 v.ofNatFn vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
 
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : OptionT SimpM Step := do
-  guard (e.isAppOfArity declName arity)
-  let n ← ($fromExpr e.appFn!.appArg!)
-  let m ← ($fromExpr e.appArg!)
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : SimpM Step := 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
   let r := { n with value := op n.value m.value }
   return .done { expr := $toExpr r }
 
-@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : OptionT SimpM Step := do
-  guard (e.isAppOfArity declName arity)
-  let n ← ($fromExpr e.appFn!.appArg!)
-  let m ← ($fromExpr e.appArg!)
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := 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
   let d ← mkDecide e
   if op n.value m.value then
     return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
   else
     return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
 
-builtin_simproc $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
-builtin_simproc $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)
-builtin_simproc $(mkIdent `reduceSub):ident ((_ - _ : $typeName)) := reduceBin ``HSub.hSub 6 (· - ·)
-builtin_simproc $(mkIdent `reduceDiv):ident ((_ / _ : $typeName)) := reduceBin ``HDiv.hDiv 6 (· / ·)
-builtin_simproc $(mkIdent `reduceMod):ident ((_ % _ : $typeName)) := reduceBin ``HMod.hMod 6 (· % ·)
+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_simproc $(mkIdent `reduceLT):ident  (( _ : $typeName) < _)  := reduceBinPred ``LT.lt 4 (. < .)
-builtin_simproc $(mkIdent `reduceLE):ident  (( _ : $typeName) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
-builtin_simproc $(mkIdent `reduceGT):ident  (( _ : $typeName) > _)  := reduceBinPred ``GT.gt 4 (. > .)
-builtin_simproc $(mkIdent `reduceGE):ident  (( _ : $typeName) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+builtin_simproc [simp, seval] $(mkIdent `reduceLT):ident  (( _ : $typeName) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc [simp, seval] $(mkIdent `reduceLE):ident  (( _ : $typeName) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc [simp, seval] $(mkIdent `reduceGT):ident  (( _ : $typeName) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc [simp, seval] $(mkIdent `reduceGE):ident  (( _ : $typeName) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
 
-/-- Return `.done` for UInt values. We don't want to unfold them when `ground := true`. -/
-builtin_simproc isValue ((OfNat.ofNat _ : $typeName)) := fun e => OptionT.run do
-  guard (← getContext).unfoldGround
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
+/-- 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
+  unless (e.isAppOfArity ``OfNat.ofNat 3) do return .continue
   return .done { expr := e }
 
 end $typeName

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

@@ -34,11 +34,6 @@ def Config.updateArith (c : Config) : CoreM Config := do
 def isOfNatNatLit (e : Expr) : Bool :=
   e.isAppOfArity ``OfNat.ofNat 3 && e.appFn!.appArg!.isNatLit
 
-private def reduceProj (e : Expr) : MetaM Expr := do
-  match (← reduceProj? e) with
-  | some e => return e
-  | _      => return e
-
 private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
   matchConst e.getAppFn (fun _ => pure none) fun cinfo _ => do
     match (← getProjectionFnInfo? cinfo.name) with
@@ -403,12 +398,12 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   unless cfg.dsimp do
     return e
   let pre (e : Expr) : SimpM TransformStep := do
-    if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
+    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 some r ← rewritePost? e (fun _ => pure none) (rflOnly := true) then
+    if let Step.visit r ← rewritePost (rflOnly := true) e then
       if r.expr != e then
         return .visit r.expr
     let mut eNew ← reduce e
@@ -433,7 +428,7 @@ def visitFn (e : Expr) : SimpM Result := do
 
 def congrDefault (e : Expr) : SimpM Result := do
   if let some result ← tryAutoCongrTheorem? e then
-    mkEqTrans result (← visitFn result.expr)
+    result.mkEqTrans (← visitFn result.expr)
   else
     withParent e <| e.withApp fun f args => do
       congrArgs (← simp f) args
@@ -504,7 +499,7 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul
     unless modified do
       trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified"
       return none
-    unless (← synthesizeArgs (.decl c.theoremName) xs bis discharge?) do
+    unless (← synthesizeArgs (.decl c.theoremName) xs bis) do
       trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed"
       return none
     let eNew ← instantiateMVars rhs
@@ -533,14 +528,11 @@ def congr (e : Expr) : SimpM Result := do
     congrDefault e
 
 def simpApp (e : Expr) : SimpM Result := do
-  let e' ← reduceStep e
-  if e' != e then
-    simp e'
-  else if isOfNatNatLit e' then
+  if isOfNatNatLit e then
     -- Recall that we expand "orphan" kernel nat literals `n` into `ofNat n`
-    return { expr := e' }
+    return { expr := e }
   else
-    congr e'
+    congr e
 
 def simpStep (e : Expr) : SimpM Result := do
   match e with
@@ -558,54 +550,54 @@ def simpStep (e : Expr) : SimpM Result := do
   | .fvar ..     => return { expr := (← reduceFVar (← getConfig) (← getSimpTheorems) e) }
 
 def cacheResult (e : Expr) (cfg : Config) (r : Result) : SimpM Result := do
-  if cfg.memoize then
+  if cfg.memoize && r.cache then
     let ctx ← readThe Simp.Context
     let dischargeDepth := ctx.dischargeDepth
-    if ctx.unfoldGround then
-      modify fun s => { s with cacheGround := s.cacheGround.insert e { r with dischargeDepth } }
-    else
-      modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
+    modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
   return r
 
-partial def simpLoop (e : Expr) (r : Result) : SimpM Result := do
+partial def simpLoop (e : Expr) : SimpM Result := do
   let cfg ← getConfig
   if (← get).numSteps > cfg.maxSteps then
     throwError "simp failed, maximum number of steps exceeded"
   else
-    let init := r.expr
     modify fun s => { s with numSteps := s.numSteps + 1 }
-    match (← pre r.expr) with
-    | Step.done r'  => cacheResult e cfg (← mkEqTrans r r')
-    | Step.visit r' =>
-      let r ← mkEqTrans r r'
-      let r ← mkEqTrans r (← simpStep r.expr)
-      match (← post r.expr) with
-      | Step.done r'  => cacheResult e cfg (← mkEqTrans r r')
-      | Step.visit r' =>
-        let r ← mkEqTrans r r'
-        if cfg.singlePass || init == r.expr then
-          cacheResult e cfg r
-        else
-          simpLoop e r
+    match (← pre e) with
+    | .done r  => cacheResult e cfg r
+    | .visit r => cacheResult e cfg (← r.mkEqTrans (← simpLoop r.expr))
+    | .continue none => visitPreContinue cfg { expr := e }
+    | .continue (some r) => visitPreContinue cfg r
+where
+  visitPreContinue (cfg : Config) (r : Result) : SimpM Result := do
+    let eNew ← reduceStep r.expr
+    if eNew != r.expr then
+      let r := { r with expr := eNew }
+      cacheResult e cfg (← r.mkEqTrans (← simpLoop r.expr))
+    else
+      let r ← r.mkEqTrans (← simpStep r.expr)
+      visitPost cfg r
+  visitPost (cfg : Config) (r : Result) : SimpM Result := do
+    match (← post r.expr) with
+    | .done r' => cacheResult e cfg (← r.mkEqTrans r')
+    | .continue none => visitPostContinue cfg r
+    | .visit r' | .continue (some r') => visitPostContinue cfg (← r.mkEqTrans r')
+  visitPostContinue (cfg : Config) (r : Result) : SimpM Result := do
+    let mut r := r
+    unless cfg.singlePass || e == r.expr do
+      r ← r.mkEqTrans (← simpLoop r.expr)
+    cacheResult e cfg r
 
 @[export lean_simp]
 def simpImpl (e : Expr) : SimpM Result := withIncRecDepth do
   checkSystem "simp"
   if (← isProof e) then
     return { expr := e }
-  let ctx ← getContext
-  trace[Meta.debug] "visit [{ctx.unfoldGround}]: {e}"
-  if ctx.unfoldGround then
-    if (← isType e) then
-    unless (← isProp e) do
-      -- Recall that we set `unfoldGround := false` if `e` is a type that is not a proposition.
-      return (← withTheReader Context (fun ctx => { ctx with unfoldGround := false }) go)
   go
 where
   go : SimpM Result := do
     let cfg ← getConfig
     if cfg.memoize then
-      let cache ← if (← getContext).unfoldGround then pure ((← get).cacheGround) else pure ((← get).cache)
+      let cache := (← get).cache
       if let some result := cache.find? e then
         /-
           If the result was cached at a dischargeDepth > the current one, it may not be valid.
@@ -614,7 +606,7 @@ where
         if result.dischargeDepth ≤ (← readThe Simp.Context).dischargeDepth then
           return result
     trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
-    simpLoop e { expr := e }
+    simpLoop e
 
 @[inline] def withSimpConfig (ctx : Context) (x : MetaM α) : MetaM α :=
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
@@ -640,9 +632,9 @@ def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods
       if ex.isRuntime then throwNestedTacticEx `dsimp ex else throw ex
 
 end Simp
-open Simp (UsedSimps Simprocs)
+open Simp (UsedSimps SimprocsArray)
 
-def simp (e : Expr) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (usedSimps : UsedSimps := {}) : MetaM (Simp.Result × UsedSimps) := do profileitM Exception "simp" (← getOptions) do
   match discharge? with
   | none   => Simp.main e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs)
@@ -653,7 +645,7 @@ def dsimp (e : Expr) (ctx : Simp.Context)
   Simp.dsimpMain e ctx usedSimps (methods := Simp.mkDefaultMethodsCore {})
 
 /-- 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 : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   let target ← instantiateMVars (← mvarId.getType)
   let (r, usedSimps) ← simp target ctx simprocs discharge? usedSimps
@@ -668,7 +660,7 @@ def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs :
 /--
   Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise,
   where `mvarId'` is the simplified new goal. -/
-def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
@@ -703,7 +695,7 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
   otherwise, where `proof' : prop'` and `prop'` is the simplified `prop`.
 
   This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
-def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (Expr × Expr) × UsedSimps) := do
   let (r, usedSimps) ← simp prop ctx simprocs discharge? usedSimps
   return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
@@ -736,7 +728,7 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
   else
     applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
 
-def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (FVarId × MVarId) × UsedSimps) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
@@ -744,7 +736,7 @@ def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simp
     let (r, usedSimps) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal usedSimps
     return (← applySimpResultToLocalDeclCore mvarId fvarId r, usedSimps)
 
-def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do
   mvarId.withContext do
@@ -783,7 +775,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {})
       throwError "simp made no progress"
     return (some (fvarIdsNew, mvarIdNew), usedSimps)
 
-def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do
   let mut ctx := ctx
   for h in (← getPropHyps) do

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

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Simp.SimpTheorems
+import Lean.Meta.Tactic.Simp.Simproc
+
+namespace Lean.Meta.Simp
+
+macro (name := _root_.Lean.Parser.Command.registerSimpAttr) doc:(docComment)?
+  "register_simp_attr" id:ident : command => do
+  let str := id.getId.toString
+  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
+  let descr := quote (removeLeadingSpaces (doc.map (·.getDocString) |>.getD s!"simp set for {id.getId.toString}"))
+  let procId := mkIdentFrom id (simpAttrNameToSimprocAttrName id.getId)
+  let procStr := procId.getId.toString
+  let procIdParser := mkIdentFrom procId (`Parser.Attr ++ procId.getId)
+  let procDescr := quote s!"simproc set for {procId.getId.toString}"
+  -- TODO: better docDomment for simprocs
+  `($[$doc:docComment]? initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr $(quote id.getId)
+    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? (prio)? : attr
+    /-- Simplification procedure -/
+    initialize extProc : SimprocExtension ← registerSimprocAttr $(quote procId.getId) $procDescr none $(quote procId.getId)
+    /-- Simplification procedure -/
+    syntax (name := $procIdParser:ident) $(quote procStr):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? : attr)
+
+end Lean.Meta.Simp

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

@@ -14,14 +14,7 @@ import Lean.Meta.Tactic.Simp.Simproc
 
 namespace Lean.Meta.Simp
 
-def mkEqTrans (r₁ r₂ : Result) : MetaM Result := do
-  match r₁.proof? with
-  | none => return r₂
-  | some p₁ => match r₂.proof? with
-    | none    => return { r₂ with proof? := r₁.proof? }
-    | some p₂ => return { r₂ with proof? := (← Meta.mkEqTrans p₁ p₂) }
-
-def synthesizeArgs (thmId : Origin) (xs : Array Expr) (bis : Array BinderInfo) (discharge? : Expr → SimpM (Option Expr)) : SimpM Bool := do
+def synthesizeArgs (thmId : Origin) (xs : Array Expr) (bis : Array BinderInfo) : SimpM Bool := do
   for x in xs, bi in bis do
     let type ← inferType x
     -- Note that the binderInfo may be misleading here:
@@ -66,10 +59,10 @@ where
       trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to synthesize instance{indentExpr type}"
       return false
 
-private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Result) := do
+private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
   let rec go (e : Expr) : SimpM (Option Result) := do
     if (← isDefEq lhs e) then
-      unless (← synthesizeArgs thm.origin xs bis discharge?) do
+      unless (← synthesizeArgs thm.origin xs bis) do
         return none
       let proof? ← if thm.rfl then
         pure none
@@ -116,36 +109,36 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
       return none
     r.addExtraArgs extraArgs
 
-def tryTheoremWithExtraArgs? (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Result) :=
+def tryTheoremWithExtraArgs? (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) :=
   withNewMCtxDepth do
     let val  ← thm.getValue
     let type ← inferType val
     let (xs, bis, type) ← forallMetaTelescopeReducing type
     let type ← whnf (← instantiateMVars type)
     let lhs := type.appFn!.appArg!
-    tryTheoremCore lhs xs bis val type e thm numExtraArgs discharge?
+    tryTheoremCore lhs xs bis val type e thm numExtraArgs
 
-def tryTheorem? (e : Expr) (thm : SimpTheorem) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Result) := do
+def tryTheorem? (e : Expr) (thm : SimpTheorem) : SimpM (Option Result) := do
   withNewMCtxDepth do
     let val  ← thm.getValue
     let type ← inferType val
     let (xs, bis, type) ← forallMetaTelescopeReducing type
     let type ← whnf (← instantiateMVars type)
     let lhs := type.appFn!.appArg!
-    match (← tryTheoremCore lhs xs bis val type e thm 0 discharge?) with
+    match (← tryTheoremCore lhs xs bis val type e thm 0) with
     | some result => return some result
     | none =>
       let lhsNumArgs := lhs.getAppNumArgs
       let eNumArgs   := e.getAppNumArgs
       if eNumArgs > lhsNumArgs then
-        tryTheoremCore lhs xs bis val type e thm (eNumArgs - lhsNumArgs) discharge?
+        tryTheoremCore lhs xs bis val type e thm (eNumArgs - lhsNumArgs)
       else
         return none
 
 /--
 Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
 -/
-def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
+def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
   let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
   if candidates.isEmpty then
     trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
@@ -154,7 +147,7 @@ def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (discha
     let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
     for (thm, numExtraArgs) in candidates do
       unless inErasedSet thm || (rflOnly && !thm.rfl) do
-        if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs discharge? then
+        if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
           trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
           return some result
     return none
@@ -162,71 +155,63 @@ where
   inErasedSet (thm : SimpTheorem) : Bool :=
     erased.contains thm.origin
 
-@[inline] def andThen' (s : Step) (f? : Expr → SimpM Step) : SimpM Step := do
-  match s with
-  | Step.done _  => return s
-  | Step.visit r =>
-    let s' ← f? r.expr
-    return s'.updateResult (← mkEqTrans r s'.result)
+-- TODO: workaround for `Expr.constructorApp?` limitations. We should handle `OfNat.ofNat` there
+private def reduceOfNatNat (e : Expr) : MetaM Expr := do
+  unless e.isAppOfArity ``OfNat.ofNat 3 do
+    return e
+  unless (← whnfD (e.getArg! 0)).isConstOf ``Nat do
+    return e
+  return e.getArg! 1
 
-@[inline] def andThen (s : Step) (f? : Expr → SimpM (Option Step)) : SimpM Step := do
-  match s with
-  | Step.done _  => return s
-  | Step.visit r =>
-    if let some s' ← f? r.expr then
-      return s'.updateResult (← mkEqTrans r s'.result)
-    else
-      return s
-
-def rewriteCtorEq? (e : Expr) : MetaM (Option Result) := withReducibleAndInstances do
+def simpCtorEq : Simproc := fun e => withReducibleAndInstances do
   match e.eq? with
-  | none => return none
+  | none => return .continue
   | some (_, lhs, rhs) =>
-    let lhs ← whnf lhs
-    let rhs ← whnf rhs
+    let lhs ← reduceOfNatNat (← whnf lhs)
+    let rhs ← reduceOfNatNat (← whnf rhs)
     let env ← getEnv
     match lhs.constructorApp? env, rhs.constructorApp? env with
     | some (c₁, _), some (c₂, _) =>
       if c₁.name != c₂.name then
         withLocalDeclD `h e fun h =>
-          return some { expr := mkConst ``False, proof? := (← mkEqFalse' (← mkLambdaFVars #[h] (← mkNoConfusion (mkConst ``False) h))) }
+          return .done { expr := mkConst ``False, proof? := (← withDefault <| mkEqFalse' (← mkLambdaFVars #[h] (← mkNoConfusion (mkConst ``False) h))) }
       else
-        return none
-    | _, _ => return none
+        return .continue
+    | _, _ => return .continue
 
-@[inline] def tryRewriteCtorEq? (e : Expr) : SimpM (Option Step) := do
-  match (← rewriteCtorEq? e) with
-  | some r => return Step.done r
-  | none  => return none
-
-def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndInstances do
+@[inline] def simpUsingDecide : Simproc := fun e => do
+  unless (← getConfig).decide do
+    return .continue
   if e.hasFVar || e.hasMVar || e.consumeMData.isConstOf ``True || e.consumeMData.isConstOf ``False then
-    return none
-  else
-    try
-      let d ← mkDecide e
-      let r ← withDefault <| whnf d
-      if r.isConstOf ``true then
-        return some { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
-      else if r.isConstOf ``false then
-        return some { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
-      else
-        return none
-    catch _ =>
-      return none
+    return .continue
+  try
+    let d ← mkDecide e
+    let r ← withDefault <| whnf d
+    if r.isConstOf ``true then
+      return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
+    else if r.isConstOf ``false then
+      return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+    else
+      return .continue
+  catch _ =>
+    return .continue
 
-@[inline] def tryRewriteUsingDecide? (e : Expr) : SimpM (Option Step) := do
-  if (← getConfig).decide then
-    match (← rewriteUsingDecide? e) with
-    | some r => return Step.done r
-    | none => return none
+def simpArith (e : Expr) : SimpM Step := do
+  unless (← getConfig).arith do
+    return .continue
+  if Linear.isLinearCnstr e then
+    let some (e', h) ← Linear.Nat.simpCnstr? e
+      | return .continue
+    return .visit { expr := e', proof? := h }
+  else if Linear.isLinearTerm e then
+    if Linear.parentIsTarget (← getContext).parent? then
+      -- We mark `cache := false` to ensure we do not miss simplifications.
+      return .continue (some { expr := e, cache := false })
+    let some (e', h) ← Linear.Nat.simpExpr? e
+      | return .continue
+    return .visit { expr := e', proof? := h }
   else
-    return none
-
-def simpArith? (e : Expr) : SimpM (Option Step) := do
-  if !(← getConfig).arith then return none
-  let some (e', h) ← Linear.simp? e (← getContext).parent? | return none
-  return Step.visit { expr := e', proof? := h }
+    return .continue
 
 /--
 Given a match-application `e` with `MatcherInfo` `info`, return `some result`
@@ -264,122 +249,162 @@ def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) :=
     r ← mkCongrFun r arg
   return some r
 
-def simpMatchCore? (matcherName : Name) (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Step) := do
+def simpMatchCore (matcherName : Name) (e : Expr) : SimpM Step := do
   for matchEq in (← Match.getEquationsFor matcherName).eqnNames do
     -- Try lemma
-    match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq) } discharge?) with
+    match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq) }) with
     | none   => pure ()
-    | some r => return some (Simp.Step.done r)
-  return none
+    | some r => return .visit r
+  return .continue
 
-def simpMatch? (discharge? : Expr → SimpM (Option Expr)) (e : Expr) : SimpM (Option Step) := do
-  if (← getConfig).iota then
-    if let some e ← reduceRecMatcher? e then
-      return some (.visit { expr := e })
-    let .const declName _ := e.getAppFn
-      | return none
-    if let some info ← getMatcherInfo? declName then
-      if let some r ← simpMatchDiscrs? info e then
-        return some (.visit r)
-      simpMatchCore? declName e discharge?
-    else
+def simpMatch : Simproc := fun e => do
+  unless (← getConfig).iota do
+    return .continue
+  if let some e ← reduceRecMatcher? e then
+    return .visit { expr := e }
+  let .const declName _ := e.getAppFn
+    | return .continue
+  let some info ← getMatcherInfo? declName
+    | return .continue
+  if let some r ← simpMatchDiscrs? info e then
+    return .visit r
+  simpMatchCore declName e
+
+def rewritePre (rflOnly := false) : Simproc := fun e => do
+  for thms in (← getContext).simpTheorems do
+    if let some r ← rewrite? e thms.pre thms.erased (tag := "pre") (rflOnly := rflOnly) then
+      return .visit r
+  return .continue
+
+def rewritePost (rflOnly := false) : Simproc := fun e => do
+  for thms in (← getContext).simpTheorems do
+    if let some r ← rewrite? e thms.post thms.erased (tag := "post") (rflOnly := rflOnly) then
+      return .visit r
+  return .continue
+
+/--
+Discharge procedure for the ground/symbolic evaluator.
+-/
+def dischargeGround (e : Expr) : SimpM (Option Expr) := do
+  trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
+  let r ← simp e
+  if r.expr.consumeMData.isConstOf ``True then
+    try
+      return some (← mkOfEqTrue (← r.getProof))
+    catch _ =>
       return none
   else
     return none
 
-def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM Step := do
-  for thms in (← getContext).simpTheorems do
-    if let some r ← rewrite? e thms.pre thms.erased discharge? (tag := "pre") (rflOnly := rflOnly) then
-      return Step.visit r
-  return Step.visit { expr := e }
-
-partial def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
-  let s ← rewritePre e discharge?
-  let s ← andThen s (simpMatch? discharge?)
-  let s ← andThen s preSimproc?
-  let s ← andThen s tryRewriteUsingDecide?
-  if s.result.expr == e then
-    return s
-  else
-    andThen s (preDefault · discharge?)
-
-def rewritePost? (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM (Option Result) := do
-  for thms in (← getContext).simpTheorems do
-    if let some r ← rewrite? e thms.post thms.erased discharge? (tag := "post") (rflOnly := rflOnly) then
-      return r
-  return none
-
 /--
-Try to unfold ground term when `Context.unfoldGround := true`.
+Try to unfold ground term in the ground/symbolic evaluator.
 -/
-def unfoldGround? (discharge? : Expr → SimpM (Option Expr)) (e : Expr) : SimpM (Option Step) := do
-  -- Ground term unfolding is disabled.
-  unless (← getContext).unfoldGround do return none
+def sevalGround : Simproc := fun e => do
   -- `e` is not a ground term.
-  unless !e.hasExprMVar && !e.hasFVar do return none
-  trace[Meta.debug] "unfoldGround? {e}"
+  unless !e.hasExprMVar && !e.hasFVar do return .continue
   -- Check whether `e` is a constant application
   let f := e.getAppFn
-  let .const declName lvls := f | return none
+  let .const declName lvls := f | return .continue
   -- If declaration has been marked to not be unfolded, return none.
   let ctx ← getContext
-  if ctx.simpTheorems.isErased (.decl declName) then return none
+  if ctx.simpTheorems.isErased (.decl declName) then return .continue
   -- Matcher applications should have been reduced before we get here.
-  if (← isMatcher declName) then return none
+  if (← isMatcher declName) then return .continue
   if let some eqns ← withDefault <| getEqnsFor? declName then
     -- `declName` has equation theorems associated with it.
     for eqn in eqns do
       -- TODO: cache SimpTheorem to avoid calls to `isRflTheorem`
-      if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rfl := (← isRflTheorem eqn) } discharge? then
+      if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rfl := (← isRflTheorem eqn) } then
         trace[Meta.Tactic.simp.ground] "unfolded, {e} => {result.expr}"
-        return some (.visit result)
-    return none
+        return .visit result
+    return .continue
   -- `declName` does not have equation theorems associated with it.
   if e.isConst then
     -- We don't unfold constants that take arguments
     if let .forallE .. ← whnfD (← inferType e) then
-      return none
+      return .continue
   let info ← getConstInfo declName
-  unless info.hasValue && info.levelParams.length == lvls.length do return none
+  unless info.hasValue && info.levelParams.length == lvls.length do return .continue
   let fBody ← instantiateValueLevelParams info lvls
   let eNew := fBody.betaRev e.getAppRevArgs (useZeta := true)
   trace[Meta.Tactic.simp.ground] "delta, {e} => {eNew}"
-  return some (.visit { expr := eNew })
+  return .visit { expr := eNew }
 
-def postDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
-  /-
-  Remark 1:
-  `rewritePost?` used to return a `Step`, and we would try other methods even if it succeeded in rewriting the term.
-  This behavior was problematic, especially when `ground := true`, because we have rewriting rules such as
-  `List.append as bs = as ++ bs`, which are rules for folding polymorphic functions.
-  This type of rule can trigger nontermination in the context of `ground := true`.
-  For example, the method `unfoldGround?` would reduce `[] ++ [1]` to `List.append [] [1]`, and
-  `rewritePost` would refold it back to `[] ++ [1]`, leading to an endless loop.
+partial def preSEval (s : SimprocsArray) : Simproc :=
+  rewritePre >>
+  simpMatch >>
+  userPreSimprocs s
 
-  Initially, we considered always reducing ground terms first. However, this approach would
-  prevent us from adding auxiliary lemmas that could short-circuit the evaluation.
-  Ultimately, we settled on the following compromise: if a `rewritePost?` succeeds and produces a result `r`,
-  we return with `.visit r`. This allows pre-methods to be applied again along with other rewriting rules.
-  This strategy helps avoid non-termination, as we have `[simp]` theorems specifically for reducing `List.append`
-  ```lean
-  @[simp] theorem nil_append (as : List α) : [] ++ as = as := ...
-  @[simp] theorem cons_append (a : α) (as bs : List α) : (a::as) ++ bs = a::(as ++ bs) := ...
-  ```
+def postSEval (s : SimprocsArray) : Simproc :=
+  rewritePost >>
+  userPostSimprocs s >>
+  sevalGround >>
+  simpCtorEq
 
-  Remark 2:
-  In the simplifier, the ground value for some inductive types is *not* a constructor application.
-  Examples: `Nat`, `Int`, `Fin _`, `UInt?`. These types are represented using `OfNat.ofNat`.
-  To ensure `unfoldGround?` does not unfold `OfNat.ofNat` applications for these types, we
-  have `simproc` that return `.done ..` for these ground values. Thus, `unfoldGround?` is not
-  even tried. Alternative design: we could add an extensible ground value predicate.
-  -/
-  if let some r ← rewritePost? e discharge? then
-    return .visit r
-  let s ← andThen (.visit { expr := e }) postSimproc?
-  let s ← andThen s (unfoldGround? discharge?)
-  let s ← andThen s simpArith?
-  let s ← andThen s tryRewriteUsingDecide?
-  andThen s tryRewriteCtorEq?
+def mkSEvalMethods : CoreM Methods := do
+  let s ← getSEvalSimprocs
+  return {
+    pre        := preSEval #[s]
+    post       := postSEval #[s]
+    discharge? := dischargeGround
+  }
+
+def mkSEvalContext : CoreM Context := do
+  let s ← getSEvalTheorems
+  let c ← Meta.getSimpCongrTheorems
+  return { simpTheorems := #[s], congrTheorems := c, config := { ground := true } }
+
+/--
+Invoke ground/symbolic evaluator from `simp`.
+It uses the `seval` theorems and simprocs.
+-/
+def seval (e : Expr) : SimpM Result := do
+  let m ← mkSEvalMethods
+  let ctx ← mkSEvalContext
+  let cacheSaved := (← get).cache
+  let usedTheoremsSaved := (← get).usedTheorems
+  try
+    withReader (fun _ => m.toMethodsRef) do
+    withTheReader Simp.Context (fun _ => ctx) do
+    modify fun s => { s with cache := {}, usedTheorems := {} }
+    simp e
+  finally
+    modify fun s => { s with cache := cacheSaved, usedTheorems := usedTheoremsSaved }
+
+/--
+Try to unfold ground term in the ground/symbolic evaluator.
+-/
+def simpGround : Simproc := fun e => do
+  -- Ground term unfolding is disabled.
+  unless (← getConfig).ground do return .continue
+  -- `e` is not a ground term.
+  unless !e.hasExprMVar && !e.hasFVar do return .continue
+  -- Check whether `e` is a constant application
+  let f := e.getAppFn
+  let .const declName _ := f | return .continue
+  -- If declaration has been marked to not be unfolded, return none.
+  let ctx ← getContext
+  if ctx.simpTheorems.isErased (.decl declName) then return .continue
+  -- Matcher applications should have been reduced before we get here.
+  if (← isMatcher declName) then return .continue
+  trace[Meta.Tactic.Simp.ground] "seval: {e}"
+  let r ← seval e
+  trace[Meta.Tactic.Simp.ground] "seval result: {e} => {r.expr}"
+  return .done r
+
+def preDefault (s : SimprocsArray) : Simproc :=
+  rewritePre >>
+  simpMatch >>
+  userPreSimprocs s >>
+  simpUsingDecide
+
+def postDefault (s : SimprocsArray) : Simproc :=
+  rewritePost >>
+  userPostSimprocs s >>
+  simpGround >>
+  simpArith >>
+  simpCtorEq >>
+  simpUsingDecide
 
 /--
   Return true if `e` is of the form `(x : α) → ... → s = t → ... → False`
@@ -469,19 +494,18 @@ def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
 
 abbrev Discharge := Expr → SimpM (Option Expr)
 
-def mkMethods (simprocs : Simprocs) (discharge? : Discharge) : Methods := {
-  pre        := (preDefault · discharge?)
-  post       := (postDefault · discharge?)
+def mkMethods (s : SimprocsArray) (discharge? : Discharge) : Methods := {
+  pre        := preDefault s
+  post       := postDefault s
   discharge? := discharge?
-  simprocs   := simprocs
 }
 
-def mkDefaultMethodsCore (simprocs : Simprocs) : Methods :=
+def mkDefaultMethodsCore (simprocs : SimprocsArray) : Methods :=
   mkMethods simprocs dischargeDefault?
 
 def mkDefaultMethods : CoreM Methods := do
   if simprocs.get (← getOptions) then
-    return mkDefaultMethodsCore (← getSimprocs)
+    return mkDefaultMethodsCore #[(← getSimprocs)]
   else
     return mkDefaultMethodsCore {}
 

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

@@ -9,7 +9,7 @@ import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 
-open Simp (UsedSimps)
+open Simp (UsedSimps SimprocsArray)
 
 namespace SimpAll
 
@@ -27,7 +27,7 @@ structure State where
   mvarId    : MVarId
   entries   : Array Entry := #[]
   ctx       : Simp.Context
-  simprocs  : Simprocs
+  simprocs  : SimprocsArray
   usedSimps : UsedSimps := {}
 
 abbrev M := StateRefT State MetaM
@@ -142,7 +142,7 @@ def main : M (Option MVarId) := do
 
 end SimpAll
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   mvarId.withContext do
     let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps, simprocs }
     if let .some mvarIdNew := r then

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

@@ -117,7 +117,7 @@ builtin_initialize
       discard <| addSimpCongrTheorem declName attrKind prio |>.run {} {}
   }
 
-def getSimpCongrTheorems : MetaM SimpCongrTheorems :=
+def getSimpCongrTheorems : CoreM SimpCongrTheorems :=
   return congrExtension.getState (← getEnv)
 
 end Lean.Meta

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

@@ -417,12 +417,17 @@ def registerSimpAttr (attrName : Name) (attrDescr : String)
 
 builtin_initialize simpExtension : SimpExtension ← registerSimpAttr `simp "simplification theorem"
 
+builtin_initialize sevalSimpExtension : SimpExtension ← registerSimpAttr `seval "symbolic evaluator theorem"
+
 def getSimpExtension? (attrName : Name) : IO (Option SimpExtension) :=
   return (← simpExtensionMapRef.get).find? attrName
 
 def getSimpTheorems : CoreM SimpTheorems :=
   simpExtension.getTheorems
 
+def getSEvalTheorems : CoreM SimpTheorems :=
+  sevalSimpExtension.getTheorems
+
 /-- Auxiliary method for adding a global declaration to a `SimpTheorems` datastructure. -/
 def SimpTheorems.addConst (s : SimpTheorems) (declName : Name) (post := true) (inv := false) (prio : Nat := eval_prio default) : MetaM SimpTheorems := do
   let s := { s with erased := s.erased.erase (.decl declName post inv) }
@@ -491,14 +496,4 @@ def SimpTheoremsArray.isDeclToUnfold (thmsArray : SimpTheoremsArray) (declName :
 def SimpTheoremsArray.isLetDeclToUnfold (thmsArray : SimpTheoremsArray) (fvarId : FVarId) : Bool :=
 thmsArray.any fun thms => thms.isLetDeclToUnfold fvarId
 
-macro (name := _root_.Lean.Parser.Command.registerSimpAttr) doc:(docComment)?
-  "register_simp_attr" id:ident : command => do
-  let str := id.getId.toString
-  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
-  let descr := quote (removeLeadingSpaces (doc.map (·.getDocString) |>.getD s!"simp set for {id.getId.toString}"))
-  `($[$doc:docComment]? initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr $(quote id.getId)
-    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? (prio)? : attr)
-
-end Meta
-
-end Lean
+end Lean.Meta

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

@@ -4,16 +4,30 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.ScopedEnvExtension
+import Lean.Compiler.InitAttr
 import Lean.Meta.DiscrTree
 import Lean.Meta.Tactic.Simp.Types
 
 namespace Lean.Meta.Simp
 
+/--
+Builtin simproc declaration extension state.
+
+It contains:
+- The discrimination tree keys for each simproc (including symbolic evaluation procedures) name.
+- The actual procedure associated with a name.
+-/
 structure BuiltinSimprocs where
   keys  : HashMap Name (Array SimpTheoremKey) := {}
   procs : HashMap Name Simproc := {}
   deriving Inhabited
 
+/--
+This global reference is populated using the command `builtin_simproc_pattern%`.
+
+This reference is then used to process the attributes `builtin_simproc` and `builtin_sevalproc`.
+Both attributes need the keys and the actual procedure registered using the command `builtin_simproc_pattern%`.
+-/
 builtin_initialize builtinSimprocDeclsRef : IO.Ref BuiltinSimprocs ← IO.mkRef {}
 
 structure SimprocDecl where
@@ -59,6 +73,11 @@ def isBuiltinSimproc (declName : Name) : CoreM Bool := do
 def isSimproc (declName : Name) : CoreM Bool :=
   return (← getSimprocDeclKeys? declName).isSome
 
+/--
+Given a declaration name `declName`, store the discrimination tree keys and the actual procedure.
+
+This method is invoked by the command `builtin_simproc_pattern%` elaborator.
+-/
 def registerBuiltinSimproc (declName : Name) (key : Array SimpTheoremKey) (proc : Simproc) : IO Unit := do
   unless (← initializing) do
     throw (IO.userError s!"invalid builtin simproc declaration, it can only be registered during initialization")
@@ -84,8 +103,12 @@ instance : ToFormat SimprocEntry where
 def Simprocs.erase (s : Simprocs) (declName : Name) : Simprocs :=
   { s with erased := s.erased.insert declName, simprocNames := s.simprocNames.erase declName }
 
+/-- Builtin simprocs. -/
 builtin_initialize builtinSimprocsRef : IO.Ref Simprocs ← IO.mkRef {}
 
+/-- Builtin symbolic evaluation procedures. -/
+builtin_initialize builtinSEvalprocsRef : IO.Ref Simprocs ← IO.mkRef {}
+
 abbrev SimprocExtension := ScopedEnvExtension SimprocOLeanEntry SimprocEntry Simprocs
 
 unsafe def getSimprocFromDeclImpl (declName : Name) : ImportM Simproc := do
@@ -100,41 +123,34 @@ opaque getSimprocFromDecl (declName: Name) : ImportM Simproc
 def toSimprocEntry (e : SimprocOLeanEntry) : ImportM SimprocEntry := do
   return { toSimprocOLeanEntry := e, proc := (← getSimprocFromDecl e.declName) }
 
-builtin_initialize simprocExtension : SimprocExtension ←
-  registerScopedEnvExtension {
-    name          := `simproc
-    mkInitial     := builtinSimprocsRef.get
-    ofOLeanEntry  := fun _ => toSimprocEntry
-    toOLeanEntry  := fun e => e.toSimprocOLeanEntry
-    addEntry      := fun s e =>
-      if e.post then
-        { s with post := s.post.insertCore e.keys e }
-      else
-        { s with pre := s.pre.insertCore e.keys e }
-  }
-
-def eraseSimprocAttr (declName : Name) : AttrM Unit := do
-  let s := simprocExtension.getState (← getEnv)
+def eraseSimprocAttr (ext : SimprocExtension) (declName : Name) : AttrM Unit := do
+  let s := ext.getState (← getEnv)
   unless s.simprocNames.contains declName do
     throwError "'{declName}' does not have [simproc] attribute"
-  modifyEnv fun env => simprocExtension.modifyState env fun s => s.erase declName
+  modifyEnv fun env => ext.modifyState env fun s => s.erase declName
 
-def addSimprocAttr (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do
+def addSimprocAttr (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do
   let proc ← getSimprocFromDecl declName
   let some keys ← getSimprocDeclKeys? declName |
     throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
-  simprocExtension.add { declName, post, keys, proc } kind
+  ext.add { declName, post, keys, proc } kind
 
-def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO Unit := do
+/--
+Implements attributes `builtin_simproc` and `builtin_sevalproc`.
+-/
+def addSimprocBuiltinAttrCore (ref : IO.Ref Simprocs) (declName : Name) (post : Bool) (proc : Simproc) : IO Unit := do
   let some keys := (← builtinSimprocDeclsRef.get).keys.find? declName |
     throw (IO.userError "invalid [builtin_simproc] attribute, '{declName}' is not a builtin simproc")
   if post then
-    builtinSimprocsRef.modify fun s => { s with post := s.post.insertCore keys { declName, keys, post, proc } }
+    ref.modify fun s => { s with post := s.post.insertCore keys { declName, keys, post, proc } }
   else
-    builtinSimprocsRef.modify fun s => { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
+    ref.modify fun s => { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
 
-def getSimprocs : CoreM Simprocs :=
-  return simprocExtension.getState (← getEnv)
+def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO Unit :=
+  addSimprocBuiltinAttrCore builtinSimprocsRef declName post proc
+
+def addSEvalprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO Unit :=
+  addSimprocBuiltinAttrCore builtinSEvalprocsRef declName post proc
 
 def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs := do
   let proc ←
@@ -154,45 +170,202 @@ def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs
   else
     return { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
 
-def SimprocEntry.try? (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM (Option Step) := do
+def SimprocEntry.try (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM Step := 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 e) with
-  | none => return none
-  | some step => return some (← step.addExtraArgs extraArgs)
+  let s ← s.proc e
+  s.addExtraArgs extraArgs
 
-def simproc? (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM (Option Step) := do
+def simprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM Step := 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 none
+    return .continue
   else
+    let mut e  := e
+    let mut proof? : Option Expr := none
+    let mut found := false
+    let mut cache := true
     for (simprocEntry, numExtraArgs) in candidates do
       unless erased.contains simprocEntry.declName do
-        if let some step ← simprocEntry.try? numExtraArgs e then
-          trace[Debug.Meta.Tactic.simp] "simproc result {e} => {step.result.expr}"
+        let s ← simprocEntry.try numExtraArgs e
+        match s with
+        | .visit r =>
+          trace[Debug.Meta.Tactic.simp] "simproc result {e} => {r.expr}"
           recordSimpTheorem (.decl simprocEntry.declName post)
-          return some step
-    return none
+          return .visit (← mkEqTransOptProofResult proof? cache r)
+        | .done r =>
+          trace[Debug.Meta.Tactic.simp] "simproc result {e} => {r.expr}"
+          recordSimpTheorem (.decl simprocEntry.declName post)
+          return .done (← mkEqTransOptProofResult proof? cache r)
+        | .continue (some r) =>
+          trace[Debug.Meta.Tactic.simp] "simproc result {e} => {r.expr}"
+          recordSimpTheorem (.decl simprocEntry.declName post)
+          e := r.expr
+          proof? ← mkEqTrans? proof? r.proof?
+          cache := cache && r.cache
+          found := true
+        | .continue none =>
+          pure ()
+    if found then
+      return .continue (some { expr := e, proof?, cache })
+    else
+      return .continue
+
+abbrev SimprocsArray := Array Simprocs
+
+def SimprocsArray.add (ss : SimprocsArray) (declName : Name) (post : Bool) : CoreM SimprocsArray :=
+  if ss.isEmpty then
+    let s : Simprocs := {}
+    return #[ (← s.add declName post) ]
+  else
+    ss.modifyM 0 fun s => s.add declName post
+
+def SimprocsArray.erase (ss : SimprocsArray) (declName : Name) : SimprocsArray :=
+  ss.map fun s => s.erase declName
+
+def SimprocsArray.isErased (ss : SimprocsArray) (declName : Name) : Bool :=
+  ss.any fun s => s.erased.contains declName
+
+def simprocArrayCore (post : Bool) (ss : SimprocsArray) (e : Expr) : SimpM Step := do
+  let mut found := false
+  let mut e  := e
+  let mut proof? : Option Expr := none
+  let mut cache := true
+  for s in ss do
+    match (← simprocCore (post := post) (if post then s.post else s.pre) s.erased e) with
+    | .visit r => return .visit (← mkEqTransOptProofResult proof? cache r)
+    | .done r =>  return .done (← mkEqTransOptProofResult proof? cache r)
+    | .continue none => pure ()
+    | .continue (some r) =>
+      e := r.expr
+      proof? ← mkEqTrans? proof? r.proof?
+      cache := cache && r.cache
+      found := true
+  if found then
+    return .continue (some { expr := e, proof? })
+  else
+    return .continue
 
 register_builtin_option simprocs : Bool := {
   defValue := true
   descr    := "Enable/disable `simproc`s (simplification procedures)."
 }
 
-def preSimproc? (e : Expr) : SimpM (Option Step) := do
-  unless simprocs.get (← getOptions) do return none
-  let s := (← getMethods).simprocs
-  simproc? (post := false) s.pre s.erased e
+def userPreSimprocs (s : SimprocsArray) : Simproc := fun e => do
+  unless simprocs.get (← getOptions) do return .continue
+  simprocArrayCore (post := false) s e
 
-def postSimproc? (e : Expr) : SimpM (Option Step) := do
-  unless simprocs.get (← getOptions) do return none
-  let s := (← getMethods).simprocs
-  simproc? (post := true) s.post s.erased e
+def userPostSimprocs (s : SimprocsArray) : Simproc := fun e => do
+  unless simprocs.get (← getOptions) do return .continue
+  simprocArrayCore (post := true) s e
+
+def mkSimprocExt (name : Name := by exact decl_name%) (ref? : Option (IO.Ref Simprocs)) : IO SimprocExtension :=
+  registerScopedEnvExtension {
+    name          := name
+    mkInitial     :=
+      if let some ref := ref? then
+        ref.get
+      else
+        return {}
+    ofOLeanEntry  := fun _ => toSimprocEntry
+    toOLeanEntry  := fun e => e.toSimprocOLeanEntry
+    addEntry      := fun s e =>
+      if e.post then
+        { s with post := s.post.insertCore e.keys e }
+      else
+        { s with pre := s.pre.insertCore e.keys e }
+  }
+
+def mkSimprocAttr (attrName : Name) (attrDescr : String) (ext : SimprocExtension) (name : Name) : IO Unit := do
+  registerBuiltinAttribute {
+    ref   := name
+    name  := attrName
+    descr := attrDescr
+    applicationTime := AttributeApplicationTime.afterCompilation
+    add   := fun declName stx attrKind =>
+      let go : MetaM Unit := do
+        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
+        addSimprocAttr ext declName attrKind post
+      discard <| go.run {} {}
+    erase := eraseSimprocAttr ext
+  }
+
+abbrev SimprocExtensionMap := HashMap Name SimprocExtension
+
+builtin_initialize simprocExtensionMapRef : IO.Ref SimprocExtensionMap ← IO.mkRef {}
+
+def registerSimprocAttr (attrName : Name) (attrDescr : String) (ref? : Option (IO.Ref Simprocs))
+    (name : Name := by exact decl_name%) : IO SimprocExtension := do
+  let ext ← mkSimprocExt name ref?
+  mkSimprocAttr attrName attrDescr ext name
+  simprocExtensionMapRef.modify fun map => map.insert attrName ext
+  return ext
+
+builtin_initialize simprocExtension : SimprocExtension ← registerSimprocAttr `simprocAttr "Simplification procedure" (some builtinSimprocsRef)
+
+builtin_initialize simprocSEvalExtension : SimprocExtension ← registerSimprocAttr `sevalprocAttr "Symbolic evaluator procedure" (some builtinSEvalprocsRef)
+
+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 initDeclName ← mkFreshUserName (declName ++ `declare)
+    declareBuiltin initDeclName val
+  go.run' {}
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `simprocBuiltinAttr
+    descr           := "Builtin simplification procedure"
+    applicationTime := AttributeApplicationTime.afterCompilation
+    erase           := fun _ => throwError "Not implemented yet, [-builtin_simproc]"
+    add             := fun declName stx _ => addBuiltin declName stx ``addSimprocBuiltinAttr
+  }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `sevalprocBuiltinAttr
+    descr           := "Builtin symbolic evaluation procedure"
+    applicationTime := AttributeApplicationTime.afterCompilation
+    erase           := fun _ => throwError "Not implemented yet, [-builtin_sevalproc]"
+    add             := fun declName stx _ => addBuiltin declName stx ``addSEvalprocBuiltinAttr
+  }
+
+def getSimprocs : CoreM Simprocs :=
+  return simprocExtension.getState (← getEnv)
+
+def getSEvalSimprocs : CoreM Simprocs :=
+  return simprocSEvalExtension.getState (← getEnv)
+
+def getSimprocExtensionCore? (attrName : Name) : IO (Option SimprocExtension) :=
+  return (← simprocExtensionMapRef.get).find? attrName
+
+def simpAttrNameToSimprocAttrName (attrName : Name) : Name :=
+  if attrName == `simp then `simprocAttr
+  else if attrName == `seval then `sevalprocAttr
+  else attrName.appendAfter "_proc"
+
+/--
+Try to retrieve the simproc set using the `simp` or `simproc` attribute names.
+Recall that when we declare a `simp` set using `register_simp_attr`, an associated
+`simproc` set is automatically created. We use the function `simpAttrNameToSimprocAttrName` to
+find the `simproc` associated with the `simp` attribute.
+-/
+def getSimprocExtension? (simprocAttrNameOrsimpAttrName : Name)
+    : IO (Option SimprocExtension) := do
+  let some ext ← getSimprocExtensionCore? simprocAttrNameOrsimpAttrName
+    | getSimprocExtensionCore? (simpAttrNameToSimprocAttrName simprocAttrNameOrsimpAttrName)
+  return some ext
+
+def SimprocExtension.getSimprocs (ext : SimprocExtension) : CoreM Simprocs :=
+  return ext.getState (← getEnv)
 
 end Lean.Meta.Simp

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

@@ -17,29 +17,62 @@ structure Result where
   proof?         : Option Expr := none -- If none, proof is assumed to be `refl`
   /-- Save the field `dischargeDepth` at `Simp.Context` because it impacts the simplifier result. -/
   dischargeDepth : UInt32 := 0
+  /-- If `cache := true` the result is cached. -/
+  cache          : Bool := true
   deriving Inhabited
 
+def mkEqTransOptProofResult (h? : Option Expr) (cache : Bool) (r : Result) : MetaM Result :=
+  match h?, cache with
+  | none, true  => return r
+  | none, false => return { r with cache := false }
+  | some p₁, cache => match r.proof? with
+    | none    => return { r with proof? := some p₁, cache := cache && r.cache }
+    | some p₂ => return { r with proof? := (← Meta.mkEqTrans p₁ p₂), cache := cache && r.cache }
+
+def Result.mkEqTrans (r₁ r₂ : Result) : MetaM Result :=
+  mkEqTransOptProofResult r₁.proof? r₁.cache r₂
+
 abbrev Cache := ExprMap Result
 
 abbrev CongrCache := ExprMap (Option CongrTheorem)
 
 structure Context where
   config           : Config := {}
-  /--
-  We initialize this field using `config.ground`.
-  Here is how we use this flag.
-  - When `unfoldGround := false` for a term `t`, it will remain false for every `t`-subterm.
-  - When term is a proof, this flag has no effect since `simp` does not try to simplify proofs.
-  - When `unfoldGround := true` and visited term is type but not a proposition, we set `unfoldGround := false`.
-  - When `unfoldGround := true` and term is not ground, we set `unfoldGround := false` when visiting instance implicit
-    arguments. Reason: We don't want to unfold instance implicit arguments of non-ground applications.
-  - When `unfoldGround := true` and term is ground, we try to unfold it during post-visit.
-  -/
-  unfoldGround      : Bool := config.ground
   /-- `maxDischargeDepth` from `config` as an `UInt32`. -/
   maxDischargeDepth : UInt32 := UInt32.ofNatTruncate config.maxDischargeDepth
   simpTheorems      : SimpTheoremsArray := {}
   congrTheorems     : SimpCongrTheorems := {}
+  /--
+  Stores the "parent" term for the term being simplified.
+  If a simplification procedure result depends on this value,
+  then it is its reponsability to set `Result.cache := false`.
+
+  Motivation for this field:
+  Suppose we have a simplication procedure for normalizing arithmetic terms.
+  Then, given a term such as `t_1 + ... + t_n`, we don't want to apply the procedure
+  to every subterm `t_1 + ... + t_i` for `i < n` for performance issues. The procedure
+  can accomplish this by checking whether the parent term is also an arithmetical expression
+  and do nothing if it is. However, it should set `Result.cache := false` to ensure
+  we don't miss simplification opportunities. For example, consider the following:
+  ```
+  example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by
+    simp_arith only
+    ...
+  ```
+  If we don't set `Result.cache := false` for the first `x + x`, then we get
+  the resulting state:
+  ```
+  ... |- id (2*x + y) = id (x + x)
+  ```
+  instead of
+  ```
+  ... |- id (2*x + y) = id (2*x)
+  ```
+  as expected.
+
+  Remark: given an application `f a b c` the "parent" term for `f`, `a`, `b`, and `c`
+  is `f a b c`.
+  -/
   parent?           : Option Expr := none
   dischargeDepth    : UInt32 := 0
   deriving Inhabited
@@ -54,8 +87,6 @@ abbrev UsedSimps := HashMap Origin Nat
 
 structure State where
   cache        : Cache := {}
-  /-- Cache for `unfoldGround := true` -/
-  cacheGround  : Cache := {}
   congrCache   : CongrCache := {}
   usedTheorems : UsedSimps := {}
   numSteps     : Nat := 0
@@ -74,24 +105,62 @@ opaque simp (e : Expr) : SimpM Result
 @[extern "lean_dsimp"]
 opaque dsimp (e : Expr) : SimpM Expr
 
-@[always_inline]
-def withoutUnfoldGround (x : SimpM α) : SimpM α :=
-  withTheReader Context (fun ctx => { ctx with unfoldGround := false }) x
-
+/--
+Result type for a simplification procedure. We have `pre` and `post` simplication procedures.
+-/
 inductive Step where
-  | visit : Result → Step
-  | done  : Result → Step
+  /--
+  For `pre` procedures, it returns the result without visiting any subexpressions.
+
+  For `post` procedures, it returns the result.
+  -/
+  | done (r : Result)
+  /--
+  For `pre` procedures, the resulting expression is passed to `pre` again.
+
+  For `post` procedures, the resulting expression is passed to `pre` again IF
+  `Simp.Config.singlePass := false` and resulting expression is not equal to initial expression.
+  -/
+  | visit (e : Result)
+  /--
+  For `pre` procedures, continue transformation by visiting subexpressions, and then
+  executing `post` procedures.
+
+  For `post` procedures, this is equivalent to returning `visit`.
+  -/
+  | continue (e? : Option Result := none)
   deriving Inhabited
 
-def Step.result : Step → Result
-  | Step.visit r => r
-  | Step.done r => r
+/--
+A simplification procedure. Recall that we have `pre` and `post` procedures.
+See `Step`.
+-/
+abbrev Simproc := Expr → SimpM Step
 
-def Step.updateResult : Step → Result → Step
-  | Step.visit _, r => Step.visit r
-  | Step.done _, r  => Step.done r
+def mkEqTransResultStep (r : Result) (s : Step) : MetaM Step :=
+  match s with
+  | .done r'            => return .done (← mkEqTransOptProofResult r.proof? r.cache r')
+  | .visit r'           => return .visit (← mkEqTransOptProofResult r.proof? r.cache r')
+  | .continue none      => return .continue r
+  | .continue (some r') => return .continue (some (← mkEqTransOptProofResult r.proof? r.cache r'))
 
-abbrev Simproc := Expr → SimpM (Option Step)
+/--
+"Compose" the two given simplification procedures. We use the following semantics.
+- If `f` produces `done` or `visit`, then return `f`'s result.
+- If `f` produces `continue`, then apply `g` to new expression returned by `f`.
+
+See `Simp.Step` type.
+-/
+@[always_inline]
+def andThen (f g : Simproc) : Simproc := fun e => do
+  match (← f e) with
+  | .done r            => return .done r
+  | .continue none     => g e
+  | .continue (some r) => mkEqTransResultStep r (← g r.expr)
+  | .visit r           => return .visit r
+
+instance : AndThen Simproc where
+  andThen s₁ s₂ := andThen s₁ (s₂ ())
 
 /--
 `Simproc` .olean entry.
@@ -123,10 +192,9 @@ structure Simprocs where
   deriving Inhabited
 
 structure Methods where
-  pre        : Expr → SimpM Step          := fun e => return Step.visit { expr := e }
-  post       : Expr → SimpM Step          := fun e => return Step.done { expr := e }
+  pre        : Simproc                    := fun _ => return .continue
+  post       : Simproc                    := fun e => return .done { expr := e }
   discharge? : Expr → SimpM (Option Expr) := fun _ => return none
-  simprocs   : Simprocs                   := {}
   deriving Inhabited
 
 unsafe def Methods.toMethodsRefImpl (m : Methods) : MethodsRef :=
@@ -168,13 +236,16 @@ def getSimpTheorems : SimpM SimpTheoremsArray :=
 def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
   return (← readThe Context).congrTheorems
 
-@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : SimpM α) : SimpM α := do
+@[inline] def savingCache (x : SimpM α) : SimpM α := do
   let cacheSaved := (← get).cache
   modify fun s => { s with cache := {} }
-  try
-    withTheReader Context (fun ctx => { ctx with simpTheorems := s }) x
-  finally
-    modify fun s => { s with cache := cacheSaved }
+  try x finally modify fun s => { s with cache := cacheSaved }
+
+@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : SimpM α) : SimpM α := do
+  savingCache <| withTheReader Context (fun ctx => { ctx with simpTheorems := s }) x
+
+@[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
+  savingCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit :=
   modify fun s => if s.usedTheorems.contains thmId then s else
@@ -246,33 +317,32 @@ where
 /--
 Given a simplified function result `r` and arguments `args`, simplify arguments using `simp` and `dsimp`.
 The resulting proof is built using `congr` and `congrFun` theorems.
-
-Recall that, if the term is not ground and `Context.unfoldGround := true`, then we set `Context.unfoldGround := false`
-for instance implicit arguments.
 -/
 def congrArgs (r : Result) (args : Array Expr) : SimpM Result := do
   if args.isEmpty then
     return r
   else
-    let ctx ← getContext
+    let cfg ← getConfig
     let infos := (← getFunInfoNArgs r.expr args.size).paramInfo
     let mut r := r
     let mut i := 0
     for arg in args do
-      trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i]!.hasFwdDeps}"
       if h : i < infos.size then
+        trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}"
         let info := infos[i]
-        let go : SimpM Result := do
-          if !info.hasFwdDeps then
-            mkCongr r (← simp arg)
-          else if (← whnfD (← inferType r.expr)).isArrow then
-            mkCongr r (← simp arg)
-          else
-            mkCongrFun r (← dsimp arg)
-        if ctx.unfoldGround && info.isInstImplicit then
-          r ← withoutUnfoldGround go
+        if cfg.ground && info.isInstImplicit then
+          -- We don't visit instance implicit arguments when we are reducing ground terms.
+          -- Motivation: many instance implicit arguments are ground, and it does not make sense
+          -- to reduce them if the parent term is not ground.
+          -- TODO: consider using it as the default behavior.
+          -- We have considered it at https://github.com/leanprover/lean4/pull/3151
+          r ← mkCongrFun r arg
+        else if !info.hasFwdDeps then
+          r ← mkCongr r (← simp arg)
+        else if (← whnfD (← inferType r.expr)).isArrow then
+          r ← mkCongr r (← simp arg)
         else
-          r ← go
+          r ← mkCongrFun r (← dsimp arg)
       else if (← whnfD (← inferType r.expr)).isArrow then
         r ← mkCongr r (← simp arg)
       else
@@ -302,17 +372,6 @@ def mkCongrSimp? (f : Expr) : SimpM (Option CongrTheorem) := do
     modify fun s => { s with congrCache := s.congrCache.insert f thm? }
     return thm?
 
-/--
-Set `unfoldGround := false` when executing `x` IF `infos[i].isInstImplicit`.
--/
-@[always_inline]
-def withoutUnfoldGroundIfInstImplicit (infos : Array ParamInfo) (i : Nat) (x : SimpM α) : SimpM α := do
-  if (← getContext).unfoldGround then
-    if h : i < infos.size then
-      if infos[i].isInstImplicit then
-        return (← withoutUnfoldGround x)
-  x
-
 /--
 Try to use automatically generated congruence theorems. See `mkCongrSimp?`.
 -/
@@ -323,6 +382,7 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
   if cgrThm.argKinds.size != e.getAppNumArgs then return none
   let args := e.getAppArgs
   let infos := (← getFunInfoNArgs f args.size).paramInfo
+  let config ← getConfig
   let mut simplified := false
   let mut hasProof   := false
   let mut hasCast    := false
@@ -330,12 +390,19 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
   let mut argResults := #[]
   let mut i          := 0 -- index at args
   for arg in args, kind in cgrThm.argKinds do
+    if h : config.ground ∧ i < infos.size then
+      if (infos[i]'h.2).isInstImplicit then
+        -- Do not visit instance implict arguments when `ground := true`
+        -- See comment at `congrArgs`
+        argsNew := argsNew.push arg
+        i := i + 1
+        continue
     match kind with
-    | CongrArgKind.fixed => argsNew := argsNew.push (← withoutUnfoldGroundIfInstImplicit infos i (dsimp arg))
+    | CongrArgKind.fixed => argsNew := argsNew.push (← dsimp arg)
     | CongrArgKind.cast  => hasCast := true; argsNew := argsNew.push arg
     | CongrArgKind.subsingletonInst => argsNew := argsNew.push arg
     | CongrArgKind.eq =>
-      let argResult ← withoutUnfoldGroundIfInstImplicit infos i (simp arg)
+      let argResult ← simp arg
       argResults := argResults.push argResult
       argsNew    := argsNew.push argResult.expr
       if argResult.proof?.isSome then hasProof := true
@@ -433,6 +500,8 @@ def Step.addExtraArgs (s : Step) (extraArgs : Array Expr) : MetaM Step := do
   match s with
   | .visit r => return .visit (← r.addExtraArgs extraArgs)
   | .done r => return .done (← r.addExtraArgs extraArgs)
+  | .continue none => return .continue none
+  | .continue (some r) => return .continue (← r.addExtraArgs extraArgs)
 
 end Simp
 

src/Lean/Meta/Tactic/Split.lean

@@ -19,19 +19,16 @@ def getSimpMatchContext : MetaM Simp.Context :=
    }
 
 def simpMatch (e : Expr) : MetaM Simp.Result := do
-  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre })
+  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre, discharge? := SplitIf.discharge? })
 where
   pre (e : Expr) : SimpM Simp.Step := do
     unless (← isMatcherApp e) do
-      return Simp.Step.visit { expr := e }
+      return Simp.Step.continue
     let matcherDeclName := e.getAppFn.constName!
     -- First try to reduce matcher
     match (← reduceRecMatcher? e) with
     | some e' => return Simp.Step.done { expr := e' }
-    | none    =>
-      match (← Simp.simpMatchCore? matcherDeclName e SplitIf.discharge?) with
-      | some r => return r
-      | none => return Simp.Step.visit { expr := e }
+    | none    => Simp.simpMatchCore matcherDeclName e
 
 def simpMatchTarget (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   let target ← instantiateMVars (← mvarId.getType)
@@ -39,13 +36,13 @@ def simpMatchTarget (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   applySimpResultToTarget mvarId target r
 
 private def simpMatchCore (matchDeclName : Name) (matchEqDeclName : Name) (e : Expr) : MetaM Simp.Result := do
-  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre })
+  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre, discharge? := SplitIf.discharge? })
 where
   pre (e : Expr) : SimpM Simp.Step := do
     if e.isAppOf matchDeclName then
       -- First try to reduce matcher
       match (← reduceRecMatcher? e) with
-      | some e' => return Simp.Step.done { expr := e' }
+      | some e' => return .done { expr := e' }
       | none    =>
       -- Try lemma
       let simpTheorem := {
@@ -53,11 +50,11 @@ where
         proof := mkConst matchEqDeclName
         rfl := (← isRflTheorem matchEqDeclName)
       }
-      match (← withReducible <| Simp.tryTheorem? e simpTheorem SplitIf.discharge?) with
-      | none => return Simp.Step.visit { expr := e }
-      | some r => return Simp.Step.done r
+      match (← withReducible <| Simp.tryTheorem? e simpTheorem) with
+      | none => return .continue
+      | some r => return .done r
     else
-      return Simp.Step.visit { expr := e }
+      return .continue
 
 private def simpMatchTargetCore (mvarId : MVarId) (matchDeclName : Name) (matchEqDeclName : Name) : MetaM MVarId := do
   mvarId.withContext do

src/Lean/Meta/Tactic/Unfold.lean

@@ -22,12 +22,12 @@ def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
     return { expr  := (← deltaExpand e (· == declName)) }
 where
   pre (unfoldThm : Name) (e : Expr) : SimpM Simp.Step := do
-    match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rfl := (← isRflTheorem unfoldThm) } (fun _ => return none)) with
+    match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rfl := (← isRflTheorem unfoldThm) }) with
     | none   => pure ()
     | some r => match (← reduceMatcher? r.expr) with
-      | .reduced e' => return Simp.Step.done { r with expr := e' }
-      | _ => return Simp.Step.done r
-    return Simp.Step.visit { expr := e }
+      | .reduced e' => return .done { r with expr := e' }
+      | _ => return .done r
+    return .continue
 
 def unfoldTarget (mvarId : MVarId) (declName : Name) : MetaM MVarId := mvarId.withContext do
   let target ← instantiateMVars (← mvarId.getType)

src/Lean/Util/Recognizers.lean

@@ -131,6 +131,8 @@ is `ConstructorVal` for `Nat.succ`, and the array `#[1]`. The parameter `useRaw`
 numeral is represented. If `useRaw := false`, then `mkNatLit` is used, otherwise `mkRawNatLit`.
 Recall that `mkNatLit` uses the `OfNat.ofNat` application which is the canonical way of representing numerals
 in the elaborator and tactic framework. We `useRaw := false` in the compiler (aka code generator).
+
+Remark: This function does not treat `(ofNat 0 : Nat)` applications as constructors.
 -/
 def constructorApp? (env : Environment) (e : Expr) (useRaw := false) : Option (ConstructorVal × Array Expr) := do
   match e with