doc: add simproc release notes

Motivation: `simp?`

RELEASES.md

@@ -11,6 +11,61 @@ of each version.
 v4.6.0 (development in progress)
 ---------
 
+* Add custom simplification procedures (aka `simproc`s) to `simp`. Simprocs can be triggered by the simplifier on a specified term-pattern. Here is an small example:
+```lean
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+
+def foo (x : Nat) : Nat :=
+  x + 10
+
+/--
+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!
+    /-
+    The `Step` type has two constructors: `.done` and `.visit`.
+    * 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.
+
+    If the result holds definitionally as in this example, the field `proof?` can be omitted.
+    -/
+    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.
+Simprocs can be scoped, manually added to `simp` commands, and suppressed using `-`. They are also supported by `simp?`. `simp only` does not execute any `simproc`. Here are some examples for the `simproc` defined above.
+```lean
+example : x + foo 2 = 12 + x := by
+  set_option simprocs false in
+    /- This `simp` command does make progress since `simproc`s are disabled. -/
+    fail_if_success simp
+  simp_arith
+
+example : x + foo 2 = 12 + x := by
+  /- `simp only` must not use the default simproc set. -/
+  fail_if_success simp only
+  simp_arith
+
+example : x + foo 2 = 12 + x := by
+  /-
+  `simp only` does not use the default simproc set,
+  but we can provide simprocs as arguments. -/
+  simp only [reduceFoo]
+  simp_arith
+
+example : x + foo 2 = 12 + x := by
+  /- We can use `-` to disable `simproc`s. -/
+  fail_if_success simp [-reduceFoo]
+  simp_arith
+```
+
+
 v4.5.0
 ---------
 
@@ -50,7 +105,7 @@ v4.5.0
   - `Widget.UserWidgetDefinition` is deprecated in favour of `Widget.Module`. The annotation `@[widget]` is deprecated in favour of `@[widget_module]`. To migrate a definition of type `UserWidgetDefinition`, remove the `name` field and replace the type with `Widget.Module`. Removing the `name` results in a title bar no longer being drawn above your panel widget. To add it back, draw it as part of the component using `<details open=true><summary class='mv2 pointer'>{name}</summary>{rest_of_widget}</details>`. See an example migration [here](https://github.com/leanprover/std4/pull/475/files#diff-857376079661a0c28a53b7ff84701afabbdf529836a6944d106c5294f0e68109R43-R83).
   - The new command `show_panel_widgets` allows displaying always-on and locally-on panel widgets.
   - `RpcEncodable` widget props can now be stored in the infotree.
-  - See [RFC 2963](https://github.com/leanprover/lean4/issues/2963) for more details and motivation. 
+  - See [RFC 2963](https://github.com/leanprover/lean4/issues/2963) for more details and motivation.
 
 * If no usable lexicographic order can be found automatically for a termination proof, explain why.
   See [feat: GuessLex: if no measure is found, explain why](https://github.com/leanprover/lean4/pull/2960).
@@ -71,7 +126,7 @@ v4.5.0
 * Tactics with `withLocation *` [no longer fail](https://github.com/leanprover/lean4/pull/2917) if they close the main goal.
 
 * Implementation of a `test_extern` command for writing tests for `@[extern]` and `@[implemented_by]` functions.
-  Usage is 
+  Usage is
   ```
   import Lean.Util.TestExtern
 
@@ -79,8 +134,8 @@ v4.5.0
   ```
   The head symbol must be the constant with the `@[extern]` or `@[implemented_by]` attribute. The return type must have a `DecidableEq` instance.
 
-Bug fixes for 
-[#2853](https://github.com/leanprover/lean4/issues/2853), [#2953](https://github.com/leanprover/lean4/issues/2953), [#2966](https://github.com/leanprover/lean4/issues/2966), 
+Bug fixes for
+[#2853](https://github.com/leanprover/lean4/issues/2853), [#2953](https://github.com/leanprover/lean4/issues/2953), [#2966](https://github.com/leanprover/lean4/issues/2966),
 [#2971](https://github.com/leanprover/lean4/issues/2971), [#2990](https://github.com/leanprover/lean4/issues/2990), [#3094](https://github.com/leanprover/lean4/issues/3094).
 
 Bug fix for [eager evaluation of default value](https://github.com/leanprover/lean4/pull/3043) in `Option.getD`.
@@ -93,19 +148,19 @@ v4.4.0
 ---------
 
 * Lake and the language server now support per-package server options using the `moreServerOptions` config field, as well as options that apply to both the language server and `lean` using the `leanOptions` config field. Setting either of these fields instead of `moreServerArgs` ensures that viewing files from a dependency uses the options for that dependency. Additionally, `moreServerArgs` is being deprecated in favor of the `moreGlobalServerArgs` field. See PR [#2858](https://github.com/leanprover/lean4/pull/2858).
-  
+
   A Lakefile with the following deprecated package declaration:
   ```lean
   def moreServerArgs := #[
     "-Dpp.unicode.fun=true"
   ]
   def moreLeanArgs := moreServerArgs
-  
+
   package SomePackage where
     moreServerArgs := moreServerArgs
     moreLeanArgs := moreLeanArgs
   ```
-  
+
   ... can be updated to the following package declaration to use per-package options:
   ```lean
   package SomePackage where

src/Init.lean

@@ -23,4 +23,5 @@ import Init.NotationExtra
 import Init.SimpLemmas
 import Init.Hints
 import Init.Conv
+import Init.Simproc
 import Init.SizeOfLemmas

src/Init/Data/Fin/Basic.lean

@@ -100,7 +100,7 @@ instance : ShiftLeft (Fin n) where
 instance : ShiftRight (Fin n) where
   shiftRight := Fin.shiftRight
 
-instance : OfNat (Fin (no_index (n+1))) i where
+instance instOfNat : OfNat (Fin (no_index (n+1))) i where
   ofNat := Fin.ofNat i
 
 instance : Inhabited (Fin (no_index (n+1))) where

src/Init/Data/Int/Basic.lean

@@ -49,7 +49,7 @@ attribute [extern "lean_int_neg_succ_of_nat"] Int.negSucc
 
 instance : Coe Nat Int := ⟨Int.ofNat⟩
 
-instance : OfNat Int n where
+instance instOfNat : OfNat Int n where
   ofNat := Int.ofNat n
 
 namespace Int

src/Init/Data/List/Basic.lean

@@ -124,7 +124,8 @@ def appendTR (as bs : List α) : List α :=
   induction as with
   | nil  => rfl
   | cons a as ih =>
-    simp [reverseAux, List.append, ih, reverseAux_reverseAux]
+    rw [reverseAux, reverseAux_reverseAux]
+    simp [List.append, ih, reverseAux]
 
 instance : Append (List α) := ⟨List.append⟩
 

src/Init/Data/UInt/Basic.lean

@@ -39,7 +39,7 @@ def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.val >>> (modn b 8).val⟩
 def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
 def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
 
-instance : OfNat UInt8 n   := ⟨UInt8.ofNat n⟩
+instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
 instance : Add UInt8       := ⟨UInt8.add⟩
 instance : Sub UInt8       := ⟨UInt8.sub⟩
 instance : Mul UInt8       := ⟨UInt8.mul⟩
@@ -110,8 +110,7 @@ def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.val >>> (modn b 16).val⟩
 def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
 def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
 
-
-instance : OfNat UInt16 n   := ⟨UInt16.ofNat n⟩
+instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
 instance : Add UInt16       := ⟨UInt16.add⟩
 instance : Sub UInt16       := ⟨UInt16.sub⟩
 instance : Mul UInt16       := ⟨UInt16.mul⟩
@@ -184,7 +183,7 @@ def UInt8.toUInt32 (a : UInt8) : UInt32 := a.toNat.toUInt32
 @[extern "lean_uint16_to_uint32"]
 def UInt16.toUInt32 (a : UInt16) : UInt32 := a.toNat.toUInt32
 
-instance : OfNat UInt32 n   := ⟨UInt32.ofNat n⟩
+instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
 instance : Mul UInt32       := ⟨UInt32.mul⟩
@@ -244,7 +243,7 @@ def UInt16.toUInt64 (a : UInt16) : UInt64 := a.toNat.toUInt64
 @[extern "lean_uint32_to_uint64"]
 def UInt32.toUInt64 (a : UInt32) : UInt64 := a.toNat.toUInt64
 
-instance : OfNat UInt64 n   := ⟨UInt64.ofNat n⟩
+instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
 instance : Add UInt64       := ⟨UInt64.add⟩
 instance : Sub UInt64       := ⟨UInt64.sub⟩
 instance : Mul UInt64       := ⟨UInt64.mul⟩
@@ -322,7 +321,7 @@ def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
 def USize.lt (a b : USize) : Prop := a.val < b.val
 def USize.le (a b : USize) : Prop := a.val ≤ b.val
 
-instance : OfNat USize n   := ⟨USize.ofNat n⟩
+instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
 instance : Add USize       := ⟨USize.add⟩
 instance : Sub USize       := ⟨USize.sub⟩
 instance : Mul USize       := ⟨USize.mul⟩

src/Init/SimpLemmas.lean

@@ -10,6 +10,7 @@ import Init.Core
 set_option linter.missingDocs true -- keep it documented
 
 theorem of_eq_true (h : p = True) : p := h ▸ trivial
+theorem of_eq_false (h : p = False) : ¬ p := fun hp => False.elim (h.mp hp)
 
 theorem eq_true (h : p) : p = True :=
   propext ⟨fun _ => trivial, fun _ => h⟩
@@ -84,6 +85,13 @@ theorem dite_congr {_ : Decidable b} [Decidable c]
 @[simp] theorem ite_false (a b : α) : (if False then a else b) = b := rfl
 @[simp] theorem dite_true {α : Sort u} {t : True → α} {e : ¬ True → α} : (dite True t e) = t True.intro := rfl
 @[simp] theorem dite_false {α : Sort u} {t : False → α} {e : ¬ False → α} : (dite False t e) = e not_false := rfl
+section SimprocHelperLemmas
+set_option simprocs false
+theorem ite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = True) : (if c then a else b) = a := by simp [h]
+theorem ite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = False) : (if c then a else b) = b := by simp [h]
+theorem dite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = True) : (dite c t e) = t (of_eq_true h) := by simp [h]
+theorem dite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = False) : (dite c t e) = e (of_eq_false h) := by simp [h]
+end SimprocHelperLemmas
 @[simp] theorem ite_self {α : Sort u} {c : Prop} {d : Decidable c} (a : α) : ite c a a = a := by cases d <;> rfl
 @[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.1), fun h => ⟨h, h⟩⟩
 @[simp] theorem and_true (p : Prop) : (p ∧ True) = p := propext ⟨(·.1), (⟨·, trivial⟩)⟩

src/Init/Simproc.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2023 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
+-/
+prelude
+import Init.NotationExtra
+
+namespace Lean.Parser
+/--
+A user-defined simplification procedure used by the `simp` tactic, and its variants.
+Here is an example.
+```lean
+simproc reduce_add (_ + _) := fun e => do
+  unless (e.isAppOfArity ``HAdd.hAdd 6) do return none
+  let some n ← getNatValue? (e.getArg! 4) | return none
+  let some m ← getNatValue? (e.getArg! 5) | return none
+  return some (.done { expr := mkNatLit (n+m) })
+```
+The `simp` tactic invokes `reduce_add` whenever it finds a term of the form `_ + _`.
+The simplification procedures are stored in an (imperfect) discrimination tree.
+The procedure should **not** assume the term `e` perfectly matches the given pattern.
+The body of a simplification procedure must have type `Simproc`, which is an alias for
+`Expr → SimpM (Option Step)`.
+You can instruct the simplifier to apply the procedure before its sub-expressions
+have been simplified by using the modifier `↓` before the procedure name. Example.
+```lean
+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
+
+/--
+A user-defined simplification procedure declaration. To activate this procedure in `simp` tactic,
+we must provide it as an argument, or use the command `attribute` to set its `[simproc]` attribute.
+-/
+syntax (docComment)? "simproc_decl " ident " (" term ")" " := " term : command
+
+/--
+A builtin simplification procedure.
+-/
+syntax (docComment)? attrKind "builtin_simproc " (Tactic.simpPre <|> Tactic.simpPost)? ident " (" term ")" " := " term : command
+
+/--
+A builtin simplification procedure declaration.
+-/
+syntax (docComment)? "builtin_simproc_decl " ident " (" term ")" " := " term : command
+
+/--
+Auxiliary command for associating a pattern with a simplification procedure.
+-/
+syntax (name := simprocPattern) "simproc_pattern% " term " => " ident : command
+
+/--
+Auxiliary command for associating a pattern with a builtin simplification procedure.
+-/
+syntax (name := simprocPatternBuiltin) "builtin_simproc_pattern% " term " => " ident : command
+
+namespace Attr
+/--
+Auxiliary attribute for simplification procedures.
+-/
+syntax (name := simprocAttr) "simproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+
+/--
+Auxiliary attribute for builtin simplification procedures.
+-/
+syntax (name := simprocBuiltinAttr) "builtin_simproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+end Attr
+
+macro_rules
+  | `($[$doc?:docComment]? simproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Simp.Simproc
+    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+      simproc_pattern% $pattern => $n)
+
+macro_rules
+  | `($[$doc?:docComment]? builtin_simproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Simp.Simproc
+    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+      builtin_simproc_pattern% $pattern => $n)
+
+macro_rules
+  | `($[$doc?:docComment]? $kind:attrKind simproc $[$pre?]? $n:ident ($pattern:term) := $body) => do
+    `(simproc_decl $n ($pattern) := $body
+      attribute [$kind simproc $[$pre?]?] $n)
+
+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)
+
+end Lean.Parser

src/Init/Tactics.lean

@@ -753,7 +753,7 @@ end Tactic
 
 namespace Attr
 /--
-Theorems tagged with the `simp` attribute are by the simplifier
+Theorems tagged with the `simp` attribute are used by the simplifier
 (i.e., the `simp` tactic, and its variants) to simplify expressions occurring in your goals.
 We call theorems tagged with the `simp` attribute "simp theorems" or "simp lemmas".
 Lean maintains a database/index containing all active simp theorems.

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

@@ -42,7 +42,7 @@ where
       go mvarId
     else if let some mvarId ← whnfReducibleLHS? mvarId then
       go mvarId
-    else match (← simpTargetStar mvarId {}).1 with
+    else match (← simpTargetStar mvarId {} (simprocs := {})).1 with
       | TacticResultCNM.closed => return ()
       | TacticResultCNM.modified mvarId => go mvarId
       | TacticResultCNM.noChange =>

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

@@ -122,7 +122,7 @@ where
     match (← reduceRecMatcher? e) with
     | some e' => return Simp.Step.done { expr := e' }
     | none    =>
-      match (← Simp.simpMatchCore? app e SplitIf.discharge?) with
+      match (← Simp.simpMatchCore? app.matcherName e SplitIf.discharge?) with
       | some r => return r
       | none => return Simp.Step.visit { expr := e }
 
@@ -169,7 +169,7 @@ private partial def mkProof (declName : Name) (info : EqnInfo) (type : Expr) : M
         go mvarId
       else if let some mvarId ← whnfReducibleLHS? mvarId then
         go mvarId
-      else match (← simpTargetStar mvarId { config.dsimp := false }).1 with
+      else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
         | TacticResultCNM.closed => return ()
         | TacticResultCNM.modified mvarId => go mvarId
         | TacticResultCNM.noChange =>

src/Lean/Elab/Tactic.lean

@@ -13,6 +13,7 @@ import Lean.Elab.Tactic.Match
 import Lean.Elab.Tactic.Rewrite
 import Lean.Elab.Tactic.Location
 import Lean.Elab.Tactic.Simp
+import Lean.Elab.Tactic.Simproc
 import Lean.Elab.Tactic.BuiltinTactic
 import Lean.Elab.Tactic.Split
 import Lean.Elab.Tactic.Conv

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

@@ -17,9 +17,9 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
     updateLhs result.expr (← result.getProof)
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.simp] def evalSimp : Tactic := fun stx => withMainContext do
-  let { ctx, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
+  let { ctx, simprocs, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
   let lhs ← getLhs
-  let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (discharge? := d?)
+  let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (simprocs := simprocs) (discharge? := d?)
   applySimpResult result
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun _ => withMainContext do

src/Lean/Elab/Tactic/Simp.lean

@@ -88,7 +88,7 @@ def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TermElabM Meta.Simp.
   | .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig
   | .dsimp   => return { (← elabDSimpConfigCore optConfig) with }
 
-private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM Meta.SimpTheorems := do
+private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM SimpTheorems := do
   if e.isConst then
     let declName := e.constName!
     let info ← getConstInfo declName
@@ -115,7 +115,7 @@ private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (id : Origin) (e
   else
     thms.add id #[] e (post := post) (inv := inv)
 
-private def addSimpTheorem (thms : Meta.SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM Meta.SimpTheorems := do
+private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
   let (levelParams, proof) ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx <| Term.withoutErrToSorry do
     let e ← Term.elabTerm stx none
     Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
@@ -129,12 +129,14 @@ private def addSimpTheorem (thms : Meta.SimpTheorems) (id : Origin) (stx : Synta
   thms.add id levelParams proof (post := post) (inv := inv)
 
 structure ElabSimpArgsResult where
-  ctx     : Simp.Context
-  starArg : Bool := false
+  ctx      : Simp.Context
+  simprocs : Simprocs
+  starArg  : Bool := false
 
 inductive ResolveSimpIdResult where
   | none
   | expr (e : Expr)
+  | simproc (declName : Name)
   | ext  (ext : SimpExtension)
 
 /--
@@ -142,9 +144,9 @@ inductive ResolveSimpIdResult where
   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) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
+def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simprocs) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
   if stx.isNone then
-    return { ctx }
+    return { ctx, simprocs }
   else
     /-
     syntax simpPre := "↓"
@@ -156,6 +158,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind :
     withMainContext do
       let mut thmsArray := ctx.simpTheorems
       let mut thms      := thmsArray[0]!
+      let mut simprocs  := simprocs
       let mut starArg   := false
       for arg in stx[1].getSepArgs do
         if arg.getKind == ``Lean.Parser.Tactic.simpErase then
@@ -165,7 +168,9 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind :
             thms := thms.eraseCore (.fvar fvar.fvarId!)
           else
             let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
-            if ctx.config.autoUnfold then
+            if (← Simp.isSimproc declName) then
+              simprocs := simprocs.erase declName
+            else if ctx.config.autoUnfold then
               thms := thms.eraseCore (.decl declName)
             else
               thms ← thms.erase (.decl declName)
@@ -177,11 +182,12 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind :
               arg[0][0].getKind == ``Parser.Tactic.simpPost
           let inv  := !arg[1].isNone
           let term := arg[2]
-
           match (← resolveSimpIdTheorem? term) with
           | .expr e  =>
             let name ← mkFreshId
             thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
+          | .simproc declName =>
+            simprocs ← simprocs.add declName post
           | .ext ext =>
             thmsArray := thmsArray.push (← ext.getTheorems)
           | .none    =>
@@ -191,8 +197,13 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind :
           starArg := true
         else
           throwUnsupportedSyntax
-      return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, starArg }
+      return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
 where
+  isSimproc? (e : Expr) : MetaM (Option Name) := do
+    let .const declName _ := e | return none
+    unless (← Simp.isSimproc declName) do return none
+    return some declName
+
   resolveSimpIdTheorem? (simpArgTerm : Term) : TacticM ResolveSimpIdResult := do
     let resolveExt (n : Name) : TacticM ResolveSimpIdResult := do
       if let some ext ← getSimpExtension? n then
@@ -203,9 +214,16 @@ where
     | `($id:ident) =>
       try
         if let some e ← Term.resolveId? simpArgTerm (withInfo := true) then
-          return .expr e
+          if let some simprocDeclName ← isSimproc? e then
+            return .simproc simprocDeclName
+          else
+            return .expr e
         else
-          resolveExt id.getId.eraseMacroScopes
+          let name := id.getId.eraseMacroScopes
+          if (← Simp.isBuiltinSimproc name) then
+            return .simproc name
+          else
+            resolveExt name
       catch _ =>
         resolveExt id.getId.eraseMacroScopes
     | _ =>
@@ -218,6 +236,7 @@ where
 
 structure MkSimpContextResult where
   ctx              : Simp.Context
+  simprocs         : Simprocs
   dischargeWrapper : Simp.DischargeWrapper
 
 /--
@@ -238,8 +257,9 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
     simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
   else
     getSimpTheorems
+  let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← getSimpCongrTheorems
-  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) {
+  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := simprocs) {
     config      := (← elabSimpConfig stx[1] (kind := kind))
     simpTheorems := #[simpTheorems], congrTheorems
   }
@@ -247,6 +267,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
     return { r with dischargeWrapper }
   else
     let ctx := r.ctx
+    let simprocs := r.simprocs
     let mut simpTheorems := ctx.simpTheorems
     /-
     When using `zeta := false`, we do not expand let-declarations when using `[*]`.
@@ -257,7 +278,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
       unless simpTheorems.isErased (.fvar h) do
         simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
     let ctx := { ctx with simpTheorems }
-    return { ctx, dischargeWrapper }
+    return { ctx, simprocs, dischargeWrapper }
 
 register_builtin_option tactic.simp.trace : Bool := {
   defValue := false
@@ -281,12 +302,21 @@ def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
   let env ← getEnv
   for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
     match thm with
-    | .decl declName inv => -- global definitions in the environment
+    | .decl declName post inv => -- global definitions in the environment
       if env.contains declName && (inv || !simpOnlyBuiltins.contains declName) then
-        args := args.push (if inv then
-          (← `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident))
-        else
-          (← `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident)))
+        let decl : Term ← `($(mkIdent (← unresolveNameGlobal declName)):ident)
+        let arg ← match post, inv with
+          | true,  true  => `(Parser.Tactic.simpLemma| ← $decl:term)
+          | true,  false => `(Parser.Tactic.simpLemma| $decl:term)
+          | false, true  => `(Parser.Tactic.simpLemma| ↓ ← $decl:term)
+          | false, false => `(Parser.Tactic.simpLemma| ↓ $decl:term)
+        args := args.push arg
+      else if (← Simp.isBuiltinSimproc declName) then
+        let decl := mkIdent declName
+        let arg ← match post with
+          | true  => `(Parser.Tactic.simpLemma| $decl:term)
+          | false => `(Parser.Tactic.simpLemma| ↓ $decl:term)
+        args := args.push arg
     | .fvar fvarId => -- local hypotheses in the context
       -- `simp_all` always uses all propositional hypotheses (and it can't use
       -- any others). So `simp_all only [h]`, where `h` is a hypothesis, would
@@ -331,7 +361,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) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
+def simpLocation (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -343,7 +373,7 @@ def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := non
 where
   go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM UsedSimps := do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
+    let (result?, usedSimps) ← simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some (_, mvarId) => replaceMainGoal [mvarId]
@@ -353,15 +383,15 @@ where
   "simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)?
 -/
 @[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do
-  let { ctx, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
+  let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
   let usedSimps ← dischargeWrapper.with fun discharge? =>
-    simpLocation ctx discharge? (expandOptLocation stx[5])
+    simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
   if tactic.simp.trace.get (← getOptions) then
     traceSimpCall stx usedSimps
 
 @[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do
-  let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
-  let (result?, usedSimps) ← simpAll (← getMainGoal) ctx
+  let { ctx, simprocs, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
+  let (result?, usedSimps) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
   match result? with
   | none => replaceMainGoal []
   | some mvarId => replaceMainGoal [mvarId]

src/Lean/Elab/Tactic/Simproc.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2023 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.Simproc
+import Lean.Elab.Binders
+import Lean.Elab.SyntheticMVars
+import Lean.Elab.Term
+import Lean.Elab.Command
+
+namespace Lean.Elab
+
+open Lean Meta Simp
+
+def elabSimprocPattern (stx : Syntax) : MetaM Expr := do
+  let go : TermElabM Expr := do
+    let pattern ← Term.elabTerm stx none
+    Term.synthesizeSyntheticMVars
+    return pattern
+  go.run'
+
+def elabSimprocKeys (stx : Syntax) : MetaM (Array Meta.SimpTheoremKey) := do
+  let pattern ← elabSimprocPattern stx
+  DiscrTree.mkPath pattern simpDtConfig
+
+def checkSimprocType (declName : Name) : CoreM Unit := do
+  let decl ← getConstInfo declName
+  match decl.type with
+  | .const ``Simproc _ => pure ()
+  | _ => throwError "unexpected type at '{declName}', 'Simproc' expected"
+
+namespace Command
+
+@[builtin_command_elab Lean.Parser.simprocPattern] def elabSimprocPattern : CommandElab := fun stx => do
+  let `(simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
+  let declName ← resolveGlobalConstNoOverload declName
+  liftTermElabM do
+    checkSimprocType declName
+    let keys ← elabSimprocKeys pattern
+    registerSimproc declName keys
+
+@[builtin_command_elab Lean.Parser.simprocPatternBuiltin] def elabSimprocPatternBuiltin : CommandElab := fun stx => do
+  let `(builtin_simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
+  let declName ← resolveGlobalConstNoOverload declName
+  liftTermElabM do
+    checkSimprocType declName
+    let keys ← elabSimprocKeys pattern
+    let val := mkAppN (mkConst ``registerBuiltinSimproc) #[toExpr declName, toExpr keys, mkConst declName]
+    let initDeclName ← mkFreshUserName (declName ++ `declare)
+    declareBuiltin initDeclName val
+
+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/Expr.lean

@@ -947,6 +947,37 @@ private def getAppRevArgsAux : Expr → Array Expr → Array Expr
   let nargs := e.getAppNumArgs
   withAppAux k e (mkArray nargs dummy) (nargs-1)
 
+/--
+Given `f a_1 ... a_n`, returns `#[a_1, ..., a_n]`.
+Note that `f` may be an application.
+The resulting array has size `n` even if `f.getAppNumArgs < n`.
+-/
+@[inline] def getAppArgsN (e : Expr) (n : Nat) : Array Expr :=
+  let dummy := mkSort levelZero
+  loop n e (mkArray n dummy)
+where
+  loop : Nat → Expr → Array Expr → Array Expr
+    | 0,   _,        as => as
+    | i+1, .app f a, as => loop i f (as.set! i a)
+    | _,   _,        _  => panic! "too few arguments at"
+
+/--
+Given `e` of the form `f a_1 ... a_n`, return `f`.
+If `n` is greater than the number of arguments, then return `e.getAppFn`.
+-/
+def stripArgsN (e : Expr) (n : Nat) : Expr :=
+  match n, e with
+  | 0,   _        => e
+  | n+1, .app f _ => stripArgsN f n
+  | _,   _        => e
+
+/--
+Given `e` of the form `f a_1 ... a_n ... a_m`, return `f a_1 ... a_n`.
+If `n` is greater than the arity, then return `e`.
+-/
+def getAppPrefix (e : Expr) (n : Nat) : Expr :=
+  e.stripArgsN (e.getAppNumArgs - n)
+
 /-- Given `e = fn a₁ ... aₙ`, runs `f` on `fn` and each of the arguments `aᵢ` and
 makes a new function application with the results. -/
 def traverseApp {M} [Monad M]

src/Lean/Meta/DiscrTreeTypes.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Expr
+import Lean.ToExpr
 
 namespace Lean.Meta
 
@@ -34,6 +35,17 @@ protected def Key.hash : Key → UInt64
 
 instance : Hashable Key := ⟨Key.hash⟩
 
+instance : ToExpr Key where
+  toTypeExpr := mkConst ``Key
+  toExpr k   := match k with
+   | .const n a => mkApp2 (mkConst ``Key.const) (toExpr n) (toExpr a)
+   | .fvar id a => mkApp2 (mkConst ``Key.fvar) (toExpr id) (toExpr a)
+   | .lit l => mkApp (mkConst ``Key.lit) (toExpr l)
+   | .star => mkConst ``Key.star
+   | .other => mkConst ``Key.other
+   | .arrow => mkConst ``Key.arrow
+   | .proj n i a => mkApp3 (mkConst ``Key.proj) (toExpr n) (toExpr i) (toExpr a)
+
 /--
 Discrimination tree trie. See `DiscrTree`.
 -/

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

@@ -150,7 +150,7 @@ def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do
   newGoal.refl
 where
   post (e : Expr) : SimpM Simp.Step := do
-    let ctx ← read
+    let ctx ← Simp.getContext
     match e, ctx.parent? with
     | bin op₁ l r, some (bin op₂ _ _) =>
       if ←isDefEq op₁ op₂ then

src/Lean/Meta/Tactic/Acyclic.lean

@@ -37,7 +37,7 @@ where
       let sizeOfEq ← mkLT sizeOf_lhs sizeOf_rhs
       let hlt ← mkFreshExprSyntheticOpaqueMVar sizeOfEq
       -- TODO: we only need the `sizeOf` simp theorems
-      match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] }).1 with
+      match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] } {}).1 with
       | some _ => return false
       | none   =>
         let heq ← mkCongrArg sizeOf_lhs.appFn! (← mkEqSymm h)

src/Lean/Meta/Tactic/Simp.lean

@@ -9,6 +9,8 @@ import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Simp.Rewrite
 import Lean.Meta.Tactic.Simp.SimpAll
+import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs
 
 namespace Lean
 

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

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2023 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.BuiltinSimprocs.Core
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int

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

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2023 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.Simproc
+
+open Lean Meta Simp
+
+builtin_simproc ↓ reduceIte (ite _ _ _) := fun e => OptionT.run do
+  guard (e.isAppOfArity ``ite 5)
+  let c := e.getArg! 1
+  let r ← simp c
+  if r.expr.isConstOf ``True then
+    let eNew  := e.getArg! 3
+    let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
+    return .visit { expr := eNew, proof? := pr }
+  if r.expr.isConstOf ``False then
+    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
+
+builtin_simproc ↓ reduceDite (dite _ _ _) := fun e => OptionT.run do
+  guard (e.isAppOfArity ``dite 5)
+  let c := e.getArg! 1
+  let r ← simp c
+  if r.expr.isConstOf ``True then
+    let pr    ← r.getProof
+    let h     := mkApp2 (mkConst ``of_eq_true) c pr
+    let eNew  := mkApp (e.getArg! 3) h |>.headBeta
+    let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) pr
+    return .visit { expr := eNew, proof? := prNew }
+  if r.expr.isConstOf ``False then
+    let pr    ← r.getProof
+    let h     := mkApp2 (mkConst ``of_eq_false) c pr
+    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

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

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2023 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.ToExpr
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+
+namespace Fin
+open Lean Meta Simp
+
+structure Value where
+  ofNatFn   : Expr
+  size      : Nat
+  value     : Nat
+
+def fromExpr? (e : Expr) : OptionT SimpM Value := do
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isAppOfArity ``Fin 1)
+  let size ← Nat.fromExpr? type.appArg!
+  guard (size > 0)
+  let value ← Nat.fromExpr? e.appFn!.appArg!
+  let value := value % size
+  return { size, value, ofNatFn := e.appFn!.appFn! }
+
+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)
+  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!
+  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))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+
+/-
+The following code assumes users did not override the `Fin n` instances for the arithmetic operators.
+If they do, they must disable the following `simprocs`.
+-/
+
+builtin_simproc 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 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 (. ≥ .)
+
+end Fin

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

@@ -0,0 +1,89 @@
+/-
+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.ToExpr
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+
+namespace Int
+open Lean Meta Simp
+
+def fromExpr? (e : Expr) : OptionT SimpM Int := do
+  let mut e := e
+  let mut isNeg := false
+  if e.isAppOfArity ``Neg.neg 3 then
+    e := e.appArg!
+    isNeg := true
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isConstOf ``Int)
+  let value ← Nat.fromExpr? e.appFn!.appArg!
+  let mut value : Int := value
+  if isNeg then value := - value
+  return value
+
+def toExpr (v : Int) : Expr :=
+  let n := v.natAbs
+  let r := mkRawNatLit n
+  let e := mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Int) r (mkApp (mkConst ``instOfNat) r)
+  if v < 0 then
+    mkAppN (mkConst ``Neg.neg [levelZero]) #[mkConst ``Int, mkConst ``instNegInt, e]
+  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!
+  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!
+  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!
+  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))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+
+/-
+The following code assumes users did not override the `Int` instances for the arithmetic operators.
+If they do, they must disable the following `simprocs`.
+-/
+
+builtin_simproc reduceNeg ((- _ : Int)) := fun e => OptionT.run do
+  guard (e.isAppOfArity ``Neg.neg 3)
+  let v ← fromExpr? e.appArg!
+  guard (v < 0)
+  return .done { expr := toExpr (- v) }
+
+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 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!
+  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!
+  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 (. ≥ .)
+
+end Int

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

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2023 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.Offset
+import Lean.Meta.Tactic.Simp.Simproc
+
+namespace Nat
+open Lean Meta Simp
+
+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!
+  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!
+  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!
+  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)
+
+/-
+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 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 (. ≥ .)
+
+end Nat

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

@@ -0,0 +1,68 @@
+/-
+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.BuiltinSimprocs.Nat
+
+open Lean Meta Simp
+
+macro "declare_uint_simprocs" typeName:ident : command =>
+let ofNat := typeName.getId ++ `ofNat
+let fromExpr := mkIdent `fromExpr
+let toExpr := mkIdent `toExpr
+`(
+namespace $typeName
+
+structure Value where
+  ofNatFn : Expr
+  value   : $typeName
+
+def $fromExpr (e : Expr) : OptionT SimpM Value := do
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isConstOf $(quote typeName.getId))
+  let value ← Nat.fromExpr? e.appFn!.appArg!
+  let value := $(mkIdent ofNat) value
+  return { value, ofNatFn := e.appFn!.appFn! }
+
+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!)
+  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!)
+  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 $(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 (. ≥ .)
+
+end $typeName
+)
+
+declare_uint_simprocs UInt8
+declare_uint_simprocs UInt16
+declare_uint_simprocs UInt32
+declare_uint_simprocs UInt64
+declare_uint_simprocs USize

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

@@ -7,8 +7,10 @@ import Lean.Meta.ACLt
 import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.AppBuilder
 import Lean.Meta.SynthInstance
+import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.LinearArith.Simp
+import Lean.Meta.Tactic.Simp.Simproc
 
 namespace Lean.Meta.Simp
 
@@ -108,19 +110,11 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
   extraArgs := extraArgs.reverse
   match (← go e) with
   | none => return none
-  | some { expr := eNew, proof? := none, .. } =>
-    if (← hasAssignableMVar eNew) then
+  | some r =>
+    if (← hasAssignableMVar r.expr) then
       trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, resulting expression has unassigned metavariables"
       return none
-    return some { expr := mkAppN eNew extraArgs }
-  | some { expr := eNew, proof? := some proof, .. } =>
-    let mut proof := proof
-    for extraArg in extraArgs do
-      proof ← Meta.mkCongrFun proof extraArg
-    if (← hasAssignableMVar eNew) then
-      trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, resulting expression has unassigned metavariables"
-      return none
-    return some { expr := mkAppN eNew extraArgs, proof? := some proof }
+    r.addExtraArgs extraArgs
 
 def tryTheoremWithExtraArgs? (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Result) :=
   withNewMCtxDepth do
@@ -148,18 +142,6 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) (discharge? : Expr → SimpM (Opt
       else
         return none
 
-/--
-Return a WHNF configuration for retrieving `[simp]` from the discrimination tree.
-If user has disabled `zeta` and/or `beta` reduction in the simplifier, we must also
-disable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281
--/
-def getDtConfig (cfg : Config) : WhnfCoreConfig :=
-  match cfg.beta, cfg.zeta with
-  | true, true => simpDtConfig
-  | true, false => { simpDtConfig with zeta := false }
-  | false, true => { simpDtConfig with beta := false }
-  | false, false => { simpDtConfig with beta := false, zeta := false }
-
 /--
 Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
 -/
@@ -180,6 +162,13 @@ 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)
+
 @[inline] def andThen (s : Step) (f? : Expr → SimpM (Option Step)) : SimpM Step := do
   match s with
   | Step.done _  => return s
@@ -227,7 +216,7 @@ def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndIn
       return none
 
 @[inline] def tryRewriteUsingDecide? (e : Expr) : SimpM (Option Step) := do
-  if (← read).config.decide then
+  if (← getConfig).decide then
     match (← rewriteUsingDecide? e) with
     | some r => return Step.done r
     | none => return none
@@ -235,12 +224,48 @@ def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndIn
     return none
 
 def simpArith? (e : Expr) : SimpM (Option Step) := do
-  if !(← read).config.arith then return none
-  let some (e', h) ← Linear.simp? e (← read).parent? | return none
+  if !(← getConfig).arith then return none
+  let some (e', h) ← Linear.simp? e (← getContext).parent? | return none
   return Step.visit { expr := e', proof? := h }
 
-def simpMatchCore? (app : MatcherApp) (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Step) := do
-  for matchEq in (← Match.getEquationsFor app.matcherName).eqnNames do
+/--
+Given a match-application `e` with `MatcherInfo` `info`, return `some result`
+if at least of one of the discriminants has been simplified.
+-/
+def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) := do
+  let numArgs := e.getAppNumArgs
+  if numArgs < info.arity then
+    return none
+  let prefixSize := info.numParams + 1 /- motive -/
+  let n     := numArgs - prefixSize
+  let f     := e.stripArgsN n
+  let infos := (← getFunInfoNArgs f n).paramInfo
+  let args  := e.getAppArgsN n
+  let mut r : Result := { expr := f }
+  let mut modified := false
+  for i in [0 : info.numDiscrs] do
+    let arg := args[i]!
+    if i < infos.size && !infos[i]!.hasFwdDeps then
+      let argNew ← simp arg
+      if argNew.expr != arg then modified := true
+      r ← mkCongr r argNew
+    else if (← whnfD (← inferType r.expr)).isArrow then
+      let argNew ← simp arg
+      if argNew.expr != arg then modified := true
+      r ← mkCongr r argNew
+    else
+      let argNew ← dsimp arg
+      if argNew != arg then modified := true
+      r ← mkCongrFun r argNew
+  unless modified do
+    return none
+  for i in [info.numDiscrs : args.size] do
+    let arg := args[i]!
+    r ← mkCongrFun r arg
+  return some r
+
+def simpMatchCore? (matcherName : Name) (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option 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
     | none   => pure ()
@@ -248,33 +273,151 @@ def simpMatchCore? (app : MatcherApp) (e : Expr) (discharge? : Expr → SimpM (O
   return none
 
 def simpMatch? (discharge? : Expr → SimpM (Option Expr)) (e : Expr) : SimpM (Option Step) := do
-  if (← read).config.iota then
-    let some app ← matchMatcherApp? e | return none
-    simpMatchCore? app e discharge?
+  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
+      return none
   else
     return none
 
 def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM Step := do
-  for thms in (← read).simpTheorems 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 }
 
 def rewritePost (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM Step := do
-  for thms in (← read).simpTheorems do
+  for thms in (← getContext).simpTheorems do
     if let some r ← rewrite? e thms.post thms.erased discharge? (tag := "post") (rflOnly := rflOnly) then
       return Step.visit r
   return Step.visit { expr := e }
 
-def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
+partial def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
   let s ← rewritePre e discharge?
-  andThen s tryRewriteUsingDecide?
+  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 postDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
   let s ← rewritePost e discharge?
-  let s ← andThen s (simpMatch? discharge?)
   let s ← andThen s simpArith?
+  let s ← andThen s postSimproc?
   let s ← andThen s tryRewriteUsingDecide?
   andThen s tryRewriteCtorEq?
 
+/--
+  Return true if `e` is of the form `(x : α) → ... → s = t → ... → False`
+
+  Recall that this kind of proposition is generated by Lean when creating equations for
+  functions and match-expressions with overlapping cases.
+  Example: the following `match`-expression has overlapping cases.
+  ```
+  def f (x y : Nat) :=
+    match x, y with
+    | Nat.succ n, Nat.succ m => ...
+    | _, _ => 0
+  ```
+  The second equation is of the form
+  ```
+  (x y : Nat) → ((n m : Nat) → x = Nat.succ n → y = Nat.succ m → False) → f x y = 0
+  ```
+  The hypothesis `(n m : Nat) → x = Nat.succ n → y = Nat.succ m → False` is essentially
+  saying the first case is not applicable.
+-/
+partial def isEqnThmHypothesis (e : Expr) : Bool :=
+  e.isForall && go e
+where
+  go (e : Expr) : Bool :=
+    match e with
+    | .forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && go b
+    | _ => e.consumeMData.isConstOf ``False
+
+def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
+  (← getLCtx).findDeclRevM? fun localDecl => do
+    if localDecl.isImplementationDetail then
+      return none
+    else if (← isDefEq e localDecl.type) then
+      return some localDecl.toExpr
+    else
+      return none
+
+/--
+  Tries to solve `e` using `unifyEq?`.
+  It assumes that `isEqnThmHypothesis e` is `true`.
+-/
+partial def dischargeEqnThmHypothesis? (e : Expr) : MetaM (Option Expr) := do
+  assert! isEqnThmHypothesis e
+  let mvar ← mkFreshExprSyntheticOpaqueMVar e
+  withReader (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher }) do
+    if let .none ← go? mvar.mvarId! then
+      instantiateMVars mvar
+    else
+      return none
+where
+  go? (mvarId : MVarId) : MetaM (Option MVarId) :=
+    try
+      let (fvarId, mvarId) ← mvarId.intro1
+      mvarId.withContext do
+        let localDecl ← fvarId.getDecl
+        if localDecl.type.isEq || localDecl.type.isHEq then
+          if let some { mvarId, .. } ← unifyEq? mvarId fvarId {} then
+            go? mvarId
+          else
+            return none
+        else
+          go? mvarId
+    catch _  =>
+      return some mvarId
+
+def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
+  if isEqnThmHypothesis e then
+    if let some r ← dischargeUsingAssumption? e then
+      return some r
+    if let some r ← dischargeEqnThmHypothesis? e then
+      return some r
+  let ctx ← getContext
+  trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
+  if ctx.dischargeDepth >= ctx.config.maxDischargeDepth then
+    trace[Meta.Tactic.simp.discharge] "maximum discharge depth has been reached"
+    return none
+  else
+    withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
+      let r ← simp e
+      if r.expr.consumeMData.isConstOf ``True then
+        try
+          return some (← mkOfEqTrue (← r.getProof))
+        catch _ =>
+          return none
+      else
+        return none
+
+abbrev Discharge := Expr → SimpM (Option Expr)
+
+def mkMethods (simprocs : Simprocs) (discharge? : Discharge) : Methods := {
+  pre        := (preDefault · discharge?)
+  post       := (postDefault · discharge?)
+  discharge? := discharge?
+  simprocs   := simprocs
+}
+
+def mkDefaultMethodsCore (simprocs : Simprocs) : Methods :=
+  mkMethods simprocs dischargeDefault?
+
+def mkDefaultMethods : CoreM Methods := do
+  if simprocs.get (← getOptions) then
+    return mkDefaultMethodsCore (← getSimprocs)
+  else
+    return mkDefaultMethodsCore {}
+
 end Lean.Meta.Simp

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

@@ -27,6 +27,7 @@ structure State where
   mvarId    : MVarId
   entries   : Array Entry := #[]
   ctx       : Simp.Context
+  simprocs  : Simprocs
   usedSimps : UsedSimps := {}
 
 abbrev M := StateRefT State MetaM
@@ -52,6 +53,7 @@ private abbrev getSimpTheorems : M SimpTheoremsArray :=
 
 private partial def loop : M Bool := do
   modify fun s => { s with modified := false }
+  let simprocs := (← get).simprocs
   -- simplify entries
   for i in [:(← get).entries.size] do
     let entry := (← get).entries[i]!
@@ -59,7 +61,7 @@ private partial def loop : M Bool := do
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
     let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
-    let (r, usedSimps) ← simpStep (← get).mvarId entry.proof entry.type ctx (usedSimps := (← get).usedSimps)
+    let (r, usedSimps) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (usedSimps := (← get).usedSimps)
     modify fun s => { s with usedSimps }
     match r with
     | none => return true -- closed the goal
@@ -99,7 +101,7 @@ private partial def loop : M Bool := do
         }
   -- simplify target
   let mvarId := (← get).mvarId
-  let (r, usedSimps) ← simpTarget mvarId (← get).ctx (usedSimps := (← get).usedSimps)
+  let (r, usedSimps) ← simpTarget mvarId (← get).ctx simprocs (usedSimps := (← get).usedSimps)
   modify fun s => { s with usedSimps }
   match r with
   | none => return true
@@ -140,9 +142,9 @@ def main : M (Option MVarId) := do
 
 end SimpAll
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   mvarId.withContext do
-    let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps }
+    let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps, simprocs }
     if let .some mvarIdNew := r then
       if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
         throwError "simp_all made no progress"

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

@@ -18,7 +18,7 @@ what action the user took which lead to this theorem existing in the simp set.
 -/
 inductive Origin where
   /-- A global declaration in the environment. -/
-  | decl (declName : Name) (inv := false)
+  | decl (declName : Name) (post := true) (inv := false)
   /--
   A local hypothesis.
   When `contextual := true` is enabled, this fvar may exist in an extension
@@ -42,7 +42,7 @@ inductive Origin where
 
 /-- A unique identifier corresponding to the origin. -/
 def Origin.key : Origin → Name
-  | .decl declName _ => declName
+  | .decl declName _ _ => declName
   | .fvar fvarId => fvarId.name
   | .stx id _ => id
   | .other name => name
@@ -137,7 +137,13 @@ instance : ToFormat SimpTheorem where
     name ++ prio ++ perm
 
 def ppOrigin [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData
-  | .decl n inv => do let r ← mkConstWithLevelParams n; if inv then return m!"← {r}" else return r
+  | .decl n post inv => do
+    let r ← mkConstWithLevelParams n;
+    match post, inv with
+    | true,  true  => return m!"← {r}"
+    | true,  false => return r
+    | false, true  => return m!"↓ ← {r}"
+    | false, false => return m!"↓ {r}"
   | .fvar n => return mkFVar n
   | .stx _ ref => return ref
   | .other n => return n
@@ -201,10 +207,11 @@ def SimpTheorems.registerDeclToUnfoldThms (d : SimpTheorems) (declName : Name) (
 
 partial def SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpTheorems :=
   let d := { d with erased := d.erased.insert thmId, lemmaNames := d.lemmaNames.erase thmId }
-  if let .decl declName := thmId then
+  if let .decl declName .. := thmId then
     let d := { d with toUnfold := d.toUnfold.erase declName }
     if let some thms := d.toUnfoldThms.find? declName then
-      thms.foldl (init := d) (eraseCore · <| .decl ·)
+      let dummy := true
+      thms.foldl (init := d) (eraseCore · <| .decl · dummy dummy)
     else
       d
   else
@@ -213,7 +220,7 @@ partial def SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpThe
 def SimpTheorems.erase [Monad m] [MonadError m] (d : SimpTheorems) (thmId : Origin) : m SimpTheorems := do
   unless d.isLemma thmId ||
     match thmId with
-    | .decl declName => d.isDeclToUnfold declName || d.toUnfoldThms.contains declName
+    | .decl declName .. => d.isDeclToUnfold declName || d.toUnfoldThms.contains declName
     | _ => false
   do
     throwError "'{thmId.key}' does not have [simp] attribute"
@@ -333,10 +340,10 @@ private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool)
       let mut r := #[]
       for (val, type) in (← preprocess val type inv (isGlobal := true)) do
         let auxName ← mkAuxLemma cinfo.levelParams type val
-        r := r.push <| (← mkSimpTheoremCore (.decl declName inv) (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio)
+        r := r.push <| (← mkSimpTheoremCore (.decl declName post inv) (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio)
       return r
     else
-      return #[← mkSimpTheoremCore (.decl declName) (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio]
+      return #[← mkSimpTheoremCore (.decl declName post inv) (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio]
 
 inductive SimpEntry where
   | thm      : SimpTheorem → SimpEntry
@@ -418,7 +425,7 @@ def getSimpTheorems : CoreM SimpTheorems :=
 
 /-- 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 inv) }
+  let s := { s with erased := s.erased.erase (.decl declName post inv) }
   let simpThms ← mkSimpTheoremsFromConst declName post inv prio
   return simpThms.foldl addSimpTheoremEntry s
 

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

@@ -0,0 +1,198 @@
+/-
+Copyright (c) 2023 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.ScopedEnvExtension
+import Lean.Meta.DiscrTree
+import Lean.Meta.Tactic.Simp.Types
+
+namespace Lean.Meta.Simp
+
+structure BuiltinSimprocs where
+  keys  : HashMap Name (Array SimpTheoremKey) := {}
+  procs : HashMap Name Simproc := {}
+  deriving Inhabited
+
+builtin_initialize builtinSimprocDeclsRef : IO.Ref BuiltinSimprocs ← IO.mkRef {}
+
+structure SimprocDecl where
+  declName : Name
+  keys     : Array SimpTheoremKey
+  deriving Inhabited
+
+structure SimprocDeclExtState where
+  builtin    : HashMap Name (Array SimpTheoremKey)
+  newEntries : PHashMap Name (Array SimpTheoremKey) := {}
+  deriving Inhabited
+
+def SimprocDecl.lt (decl₁ decl₂ : SimprocDecl) : Bool :=
+  Name.quickLt decl₁.declName decl₂.declName
+
+builtin_initialize simprocDeclExt : PersistentEnvExtension SimprocDecl SimprocDecl SimprocDeclExtState ←
+  registerPersistentEnvExtension {
+    mkInitial       := return { builtin := (← builtinSimprocDeclsRef.get).keys }
+    addImportedFn   := fun _ => return { builtin := (← builtinSimprocDeclsRef.get).keys }
+    addEntryFn      := fun s d => { s with newEntries := s.newEntries.insert d.declName d.keys }
+    exportEntriesFn := fun s =>
+      let result := s.newEntries.foldl (init := #[]) fun result declName keys => result.push { declName, keys }
+      result.qsort SimprocDecl.lt
+  }
+
+def getSimprocDeclKeys? (declName : Name) : CoreM (Option (Array SimpTheoremKey)) := do
+  let env ← getEnv
+  let keys? ← match env.getModuleIdxFor? declName with
+    | some modIdx => do
+      let some decl := (simprocDeclExt.getModuleEntries env modIdx).binSearch { declName, keys := #[] } SimprocDecl.lt
+        | pure none
+      pure (some decl.keys)
+    | none        => pure ((simprocDeclExt.getState env).newEntries.find? declName)
+  if let some keys := keys? then
+    return some keys
+  else
+    return (simprocDeclExt.getState env).builtin.find? declName
+
+def isBuiltinSimproc (declName : Name) : CoreM Bool := do
+  let s := simprocDeclExt.getState (← getEnv)
+  return s.builtin.contains declName
+
+def isSimproc (declName : Name) : CoreM Bool :=
+  return (← getSimprocDeclKeys? declName).isSome
+
+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")
+  if (← builtinSimprocDeclsRef.get).keys.contains declName then
+    throw (IO.userError s!"invalid builtin simproc declaration '{declName}', it has already been declared")
+  builtinSimprocDeclsRef.modify fun { keys, procs } =>
+    { keys := keys.insert declName key, procs := procs.insert declName proc }
+
+def registerSimproc (declName : Name) (keys : Array SimpTheoremKey) : CoreM Unit := do
+  let env ← getEnv
+  unless (env.getModuleIdxFor? declName).isNone do
+    throwError "invalid simproc declaration '{declName}', function declaration is in an imported module"
+  if (← isSimproc declName) then
+    throwError "invalid simproc declaration '{declName}', it has already been declared"
+  modifyEnv fun env => simprocDeclExt.modifyState env fun s => { s with newEntries := s.newEntries.insert declName keys }
+
+instance : BEq SimprocEntry where
+  beq e₁ e₂ := e₁.declName == e₂.declName
+
+instance : ToFormat SimprocEntry where
+  format e := format e.declName
+
+def Simprocs.erase (s : Simprocs) (declName : Name) : Simprocs :=
+  { s with erased := s.erased.insert declName, simprocNames := s.simprocNames.erase declName }
+
+builtin_initialize builtinSimprocsRef : IO.Ref Simprocs ← IO.mkRef {}
+
+abbrev SimprocExtension := ScopedEnvExtension SimprocOLeanEntry SimprocEntry Simprocs
+
+unsafe def getSimprocFromDeclImpl (declName : Name) : ImportM Simproc := do
+  let ctx ← read
+  match ctx.env.evalConstCheck Simproc ctx.opts ``Lean.Meta.Simp.Simproc declName with
+  | .ok proc  => return proc
+  | .error ex => throw (IO.userError ex)
+
+@[implemented_by getSimprocFromDeclImpl]
+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)
+  unless s.simprocNames.contains declName do
+    throwError "'{declName}' does not have [simproc] attribute"
+  modifyEnv fun env => simprocExtension.modifyState env fun s => s.erase declName
+
+def addSimprocAttr (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
+
+def addSimprocBuiltinAttr (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 } }
+  else
+    builtinSimprocsRef.modify fun s => { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
+
+def getSimprocs : CoreM Simprocs :=
+  return simprocExtension.getState (← getEnv)
+
+def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs := do
+  let proc ←
+    try
+      getSimprocFromDecl declName
+    catch e =>
+      if (← isBuiltinSimproc declName) then
+        let some proc := (← builtinSimprocDeclsRef.get).procs.find? declName
+          | throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
+        pure proc
+      else
+        throw e
+  let some keys ← getSimprocDeclKeys? declName |
+    throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
+  if post then
+    return { s with post := s.post.insertCore keys { declName, keys, post, proc } }
+  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
+  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)
+
+def simproc? (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM (Option 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
+  else
+    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}"
+          recordSimpTheorem (.decl simprocEntry.declName post)
+          return some step
+    return none
+
+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 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
+
+end Lean.Meta.Simp

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

@@ -44,7 +44,19 @@ structure State where
   usedTheorems : UsedSimps := {}
   numSteps     : Nat := 0
 
-abbrev SimpM := ReaderT Context $ StateRefT State MetaM
+private opaque MethodsRefPointed : NonemptyType.{0}
+
+private def MethodsRef : Type := MethodsRefPointed.type
+
+instance : Nonempty MethodsRef := MethodsRefPointed.property
+
+abbrev SimpM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
+
+@[extern "lean_simp"]
+opaque simp (e : Expr) : SimpM Result
+
+@[extern "lean_dsimp"]
+opaque dsimp (e : Expr) : SimpM Expr
 
 inductive Step where
   | visit : Result → Step
@@ -59,37 +71,84 @@ def Step.updateResult : Step → Result → Step
   | Step.visit _, r => Step.visit r
   | Step.done _, r  => Step.done r
 
+abbrev Simproc := Expr → SimpM (Option Step)
+
+/--
+`Simproc` .olean entry.
+-/
+structure SimprocOLeanEntry where
+  /-- Name of a declaration stored in the environment which has type `Simproc`. -/
+  declName : Name
+  post     : Bool := true
+  keys     : Array SimpTheoremKey := #[]
+  deriving Inhabited
+
+/--
+`Simproc` entry. It is the .olean entry plus the actual function.
+-/
+structure SimprocEntry extends SimprocOLeanEntry where
+  /--
+  Recall that we cannot store `Simproc` into .olean files because it is a closure.
+  Given `SimprocOLeanEntry.declName`, we convert it into a `Simproc` by using the unsafe function `evalConstCheck`.
+  -/
+  proc : Simproc
+
+abbrev SimprocTree := DiscrTree SimprocEntry
+
+structure Simprocs where
+  pre          : SimprocTree   := DiscrTree.empty
+  post         : SimprocTree   := DiscrTree.empty
+  simprocNames : PHashSet Name := {}
+  erased       : PHashSet Name := {}
+  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 }
   discharge? : Expr → SimpM (Option Expr) := fun _ => return none
+  simprocs   : Simprocs                   := {}
   deriving Inhabited
 
-/- Internal monad -/
-abbrev M := ReaderT Methods SimpM
+unsafe def Methods.toMethodsRefImpl (m : Methods) : MethodsRef :=
+  unsafeCast m
 
-def pre (e : Expr) : M Step := do
-  (← read).pre e
+@[implemented_by Methods.toMethodsRefImpl]
+opaque Methods.toMethodsRef (m : Methods) : MethodsRef
 
-def post (e : Expr) : M Step := do
-  (← read).post e
+unsafe def MethodsRef.toMethodsImpl (m : MethodsRef) : Methods :=
+  unsafeCast m
 
-def discharge? (e : Expr) : M (Option Expr) := do
-  (← read).discharge? e
+@[implemented_by MethodsRef.toMethodsImpl]
+opaque MethodsRef.toMethods (m : MethodsRef) : Methods
+
+def getMethods : SimpM Methods :=
+  return MethodsRef.toMethods (← read)
+
+def pre (e : Expr) : SimpM Step := do
+  (← getMethods).pre e
+
+def post (e : Expr) : SimpM Step := do
+  (← getMethods).post e
+
+def discharge? (e : Expr) : SimpM (Option Expr) := do
+  (← getMethods).discharge? e
+
+@[inline] def getContext : SimpM Context :=
+  readThe Context
 
 def getConfig : SimpM Config :=
-  return (← read).config
+  return (← getContext).config
 
-@[inline] def withParent (parent : Expr) (f : M α) : M α :=
+@[inline] def withParent (parent : Expr) (f : SimpM α) : SimpM α :=
   withTheReader Context (fun ctx => { ctx with parent? := parent }) f
 
-def getSimpTheorems : M SimpTheoremsArray :=
+def getSimpTheorems : SimpM SimpTheoremsArray :=
   return (← readThe Context).simpTheorems
 
-def getSimpCongrTheorems : M SimpCongrTheorems :=
+def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
   return (← readThe Context).congrTheorems
 
-@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : M α) : M α := do
+@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : SimpM α) : SimpM α := do
   let cacheSaved := (← get).cache
   modify fun s => { s with cache := {} }
   try
@@ -168,11 +227,7 @@ 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.
 -/
-@[specialize] def congrArgs
-    [Monad m] [MonadLiftT MetaM m] [MonadLiftT IO m] [MonadRef m] [MonadOptions m] [MonadTrace m] [AddMessageContext m]
-    (simp : Expr → m Result)
-    (dsimp : Expr → m Expr)
-    (r : Result) (args : Array Expr) : m Result := do
+def congrArgs (r : Result) (args : Array Expr) : SimpM Result := do
   if args.isEmpty then
     return r
   else
@@ -190,25 +245,13 @@ The resulting proof is built using `congr` and `congrFun` theorems.
       i := i + 1
     return r
 
-/--
-Helper class for generalizing `mkCongrSimp?`
--/
-class MonadCongrCache (m : Type → Type) where
-  find? : Expr → m (Option (Option CongrTheorem))
-  save  : Expr → (Option CongrTheorem) → m Unit
-
-instance : MonadCongrCache M where
-  find? f := return (← get).congrCache.find? f
-  save f thm? := modify fun s => { s with congrCache := s.congrCache.insert f thm? }
-
 /--
 Retrieve auto-generated congruence lemma for `f`.
 
 Remark: If all argument kinds are `fixed` or `eq`, it returns `none` because
 using simple congruence theorems `congr`, `congrArg`, and `congrFun` produces a more compact proof.
 -/
-def mkCongrSimp? [Monad m] [MonadLiftT MetaM m] [MonadEnv m] [MonadCongrCache m]
-  (f : Expr) : m (Option CongrTheorem) := do
+def mkCongrSimp? (f : Expr) : SimpM (Option CongrTheorem) := do
   if f.isConst then if (← isMatcher f.constName!) then
     -- We always use simple congruence theorems for auxiliary match applications
     return none
@@ -217,22 +260,17 @@ def mkCongrSimp? [Monad m] [MonadLiftT MetaM m] [MonadEnv m] [MonadCongrCache m]
   if kinds.all fun k => match k with | CongrArgKind.fixed => true | CongrArgKind.eq => true | _ => false then
     /- See remark above. -/
     return none
-  match (← MonadCongrCache.find? f) with
+  match (← get).congrCache.find? f with
   | some thm? => return thm?
   | none =>
     let thm? ← mkCongrSimpCore? f info kinds
-    MonadCongrCache.save f thm?
+    modify fun s => { s with congrCache := s.congrCache.insert f thm? }
     return thm?
 
 /--
 Try to use automatically generated congruence theorems. See `mkCongrSimp?`.
 -/
-@[specialize] def tryAutoCongrTheorem?
-    [Monad m] [MonadEnv m] [MonadCongrCache m] [MonadLiftT MetaM m]
-    [MonadLiftT IO m] [MonadRef m] [MonadOptions m] [MonadTrace m] [AddMessageContext m]
-    (simp : Expr → m Result)
-    (dsimp : Expr → m Expr)
-    (e : Expr) : m (Option Result) := do
+def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
   let f := e.getAppFn
   -- TODO: cache
   let some cgrThm ← mkCongrSimp? f | return none
@@ -321,9 +359,35 @@ Try to use automatically generated congruence theorems. See `mkCongrSimp?`.
     /- See comment above. This is reachable if `hasCast == true`. The `rhs` is not structurally equal to `mkAppN f argsNew` -/
     return some { expr := rhs }
 
+/--
+Return a WHNF configuration for retrieving `[simp]` from the discrimination tree.
+If user has disabled `zeta` and/or `beta` reduction in the simplifier, we must also
+disable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281
+-/
+def getDtConfig (cfg : Config) : WhnfCoreConfig :=
+  match cfg.beta, cfg.zeta with
+  | true, true => simpDtConfig
+  | true, false => { simpDtConfig with zeta := false }
+  | false, true => { simpDtConfig with beta := false }
+  | false, false => { simpDtConfig with beta := false, zeta := false }
+
+def Result.addExtraArgs (r : Result) (extraArgs : Array Expr) : MetaM Result := do
+  match r.proof? with
+  | none => return { expr := mkAppN r.expr extraArgs }
+  | some proof =>
+    let mut proof := proof
+    for extraArg in extraArgs do
+      proof ← Meta.mkCongrFun proof extraArg
+    return { expr := mkAppN r.expr extraArgs, proof? := some proof }
+
+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)
+
 end Simp
 
-export Simp (SimpM)
+export Simp (SimpM Simprocs)
 
 /--
   Auxiliary method.

src/Lean/Meta/Tactic/Split.lean

@@ -22,12 +22,14 @@ def simpMatch (e : Expr) : MetaM Simp.Result := do
   (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre })
 where
   pre (e : Expr) : SimpM Simp.Step := do
-    let some app ← matchMatcherApp? e | return Simp.Step.visit { expr := e }
+    unless (← isMatcherApp e) do
+      return Simp.Step.visit { expr := e }
+    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? app e SplitIf.discharge?) with
+      match (← Simp.simpMatchCore? matcherDeclName e SplitIf.discharge?) with
       | some r => return r
       | none => return Simp.Step.visit { expr := e }
 

src/Lean/Meta/Tactic/SplitIf.lean

@@ -82,14 +82,14 @@ open SplitIf
 
 def simpIfTarget (mvarId : MVarId) (useDecide := false) : MetaM MVarId := do
   let mut ctx ← getSimpContext
-  if let (some mvarId', _) ← simpTarget mvarId ctx (discharge? useDecide) (mayCloseGoal := false) then
+  if let (some mvarId', _) ← simpTarget mvarId ctx {} (discharge? useDecide) (mayCloseGoal := false) then
     return mvarId'
   else
     unreachable!
 
 def simpIfLocalDecl (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do
   let mut ctx ← getSimpContext
-  if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx discharge? (mayCloseGoal := false) then
+  if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx {} discharge? (mayCloseGoal := false) then
     return mvarId'
   else
     unreachable!

src/Lean/Meta/WHNF.lean

@@ -827,12 +827,17 @@ def reduceNative? (e : Expr) : MetaM (Option Expr) :=
   | _ =>
     return none
 
-@[inline] def withNatValue {α} (a : Expr) (k : Nat → MetaM (Option α)) : MetaM (Option α) := do
+@[inline] def withNatValue (a : Expr) (k : Nat → MetaM (Option α)) : MetaM (Option α) := do
+  if !a.hasExprMVar && a.hasFVar then
+    return none
+  let a ← instantiateMVars a
+  if a.hasExprMVar || a.hasFVar then
+    return none
   let a ← whnf a
   match a with
-  | Expr.const `Nat.zero _      => k 0
-  | Expr.lit (Literal.natVal v) => k v
-  | _                           => return none
+  | .const ``Nat.zero _ => k 0
+  | .lit (.natVal v)    => k v
+  | _                   => return none
 
 def reduceUnaryNatOp (f : Nat → Nat) (a : Expr) : MetaM (Option Expr) :=
   withNatValue a fun a =>

src/Lean/ToExpr.lean

@@ -100,6 +100,16 @@ instance [ToExpr α] [ToExpr β] : ToExpr (α × β) :=
   { toExpr     := fun ⟨a, b⟩ => mkApp4 (mkConst ``Prod.mk [levelZero, levelZero]) αType βType (toExpr a) (toExpr b),
     toTypeExpr := mkApp2 (mkConst ``Prod [levelZero, levelZero]) αType βType }
 
+instance : ToExpr Literal where
+  toTypeExpr := mkConst ``Literal
+  toExpr l   := match l with
+   | .natVal _ => mkApp (mkConst ``Literal.natVal) (.lit l)
+   | .strVal _ => mkApp (mkConst ``Literal.strVal) (.lit l)
+
+instance : ToExpr FVarId where
+  toTypeExpr    := mkConst ``FVarId
+  toExpr fvarId := mkApp (mkConst ``FVarId.mk) (toExpr fvarId.name)
+
 def Expr.toCtorIfLit : Expr → Expr
   | .lit (.natVal v) =>
     if v == 0 then mkConst ``Nat.zero

tests/lean/1079.lean.expected.out

@@ -1,11 +1,6 @@
 1079.lean:3:2-6:12: error: alternative 'isFalse' has not been provided
 [Meta.Tactic.simp.rewrite] h:1000, m ==> n
 [Meta.Tactic.simp.rewrite] @eq_self:1000, n = n ==> True
-[Meta.Tactic.simp.unify] @ite_self:1000, failed to unify
-      if ?c then ?a else ?a
-    with
-      if True then Ordering.eq else Ordering.gt
-[Meta.Tactic.simp.rewrite] @ite_true:1000, if True then Ordering.eq else Ordering.gt ==> Ordering.eq
 [Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
       ?a = ?a
     with

tests/lean/2040.lean.expected.out

@@ -9,4 +9,4 @@
 has type
   a = @OfNat.ofNat Nat 2 (instOfNatNat 2) ^ n : Prop
 but is expected to have type
-  a = @OfNat.ofNat Int 2 instOfNatInt ^ n : Prop
+  a = @OfNat.ofNat Int 2 instOfNat ^ n : Prop

tests/lean/2220.lean.expected.out

@@ -1,18 +1,18 @@
-@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNatInt 3))
+@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
   (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNatInt 1))
-  (@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNatInt 3))
+@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1))
+  (@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
     (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNatInt 1))
-  (@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNatInt 3))
+@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1))
+  (@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
     (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
-@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNatInt 3))
+@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
   (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
 2220.lean:25:19-25:24: error: failed to synthesize instance
   HPow Nat Nat Int
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNatInt 1))
+@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
 2220.lean:26:12-26:17: error: failed to synthesize instance
   HPow Nat Nat Int
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNatInt 1))
+@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int

tests/lean/builtinSimprocTrace.lean

@@ -0,0 +1,6 @@
+def f (_ : Nat) := 10
+
+set_option tactic.simp.trace true
+example : f x = (if true then 8 + 2 else 0) := by
+ simp
+ rw [f]

tests/lean/builtinSimprocTrace.lean.expected.out

@@ -0,0 +1 @@
+Try this: simp only [↓reduceIte, Nat.reduceAdd]

tests/lean/matchOfNatIssue.lean.expected.out

@@ -1,3 +1,3 @@
 x : Int
 h : x = 2
-⊢ Int.ofNat (2 / 1) = x
+⊢ Int.ofNat 2 = x

tests/lean/run/simpIfPre.lean

@@ -0,0 +1,64 @@
+/-!
+Test support for `if-then-else` terms in the simplifier.
+The condition should be simplified before trying to apply congruence.
+We are currently accomplished that using pre-simp theorems.
+TODO: replace them with simprocs.
+In the following example, the term `g (a + <num>)` takes an
+exponential amount of time to be simplified without the pre-simp theorems.
+-/
+
+def myid (x : Nat) := 0 + x
+
+@[simp] theorem myid_eq : myid x = x := by simp [myid]
+
+namespace Ex1
+def f (x : Nat) (y z : Nat) : Nat :=
+  if myid x = 0 then y else z
+
+def g (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | a+1 => f x (g a + 1) (g a)
+
+theorem ex (h : a = 1) : g (a+32) = a := by
+  simp [g, f, h]
+end Ex1
+
+namespace Ex2
+def f (x : Nat) (y z : Nat) : Nat :=
+  if myid x > 0 then z else y
+
+def g (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | a+1 => f x (g a + 1) (g a)
+
+theorem ex (h : a = 1) : g (a+32) = a := by
+  simp [g, f, h]
+end Ex2
+
+namespace Ex3
+def f (x : Nat) (y z : Nat) : Nat :=
+  if _ : myid x = 0 then y else z
+
+def g (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | a+1 => f x (g a + 1) (g a)
+
+theorem ex (h : a = 1) : g (a+32) = a := by
+  simp [g, f, h]
+end Ex3
+
+namespace Ex4
+def f (x : Nat) (y z : Nat) : Nat :=
+  if _ : myid x > 0 then z else y
+
+def g (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | a+1 => f x (g a + 1) (g a)
+
+theorem ex (h : a = 1) : g (a+32) = a := by
+  simp [g, f, h]
+end Ex4

tests/lean/run/simpMatchDiscrIssue.lean

@@ -0,0 +1,24 @@
+/-!
+Test support for `match`-applications in the simplifier.
+The discriminants should be simplified before trying to apply congruence.
+In the following example, the term `g (a + <num>)` takes an
+exponential amount of time to be simplified the discriminants are not simplified,
+and the `match`-application reduced before visiting the alternatives.
+-/
+
+def myid (x : Nat) := 0 + x
+
+@[simp] theorem myid_eq : myid x = x := by simp [myid]
+
+def f (x : Nat) (y z : Nat) : Nat :=
+  match myid x with
+  | 0   => y
+  | _+1 => z
+
+def g (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | a+1 => f x (g a + 1) (g a)
+
+theorem ex (h : a = 1) : g (a+64) = a := by
+  simp [g, f, h]

tests/lean/run/simpPreIssue.lean

@@ -0,0 +1,37 @@
+/-!
+Test a simplifier issue. `simpApp` first tries to `reduce` the term. If the
+term is reduce, pre-simp rules should be tried again before trying to use
+congruence. In the following example, the term `g (a + <num>)` takes an
+exponential amount of time to be simplified when the pre-simp rules are not
+tried before applying congruence.
+-/
+
+def myid (x : Nat) := 0 + x
+
+@[simp] theorem myid_eq : myid x = x := by simp [myid]
+
+def myif (c : Prop) [Decidable c] (a b : α) : α :=
+  if c then a else b
+
+@[simp ↓] theorem myif_cond_true (c : Prop) {_ : Decidable c} (a b : α) (h : c) : (myif c a b) = a := by
+  simp [myif, h]
+
+@[simp ↓] theorem myif_cond_false (c : Prop) {_ : Decidable c} (a b : α) (h : Not c) : (myif c a b) = b := by
+  simp [myif, h]
+
+@[congr] theorem myif_congr {x y u v : α} {s : Decidable b} [Decidable c]
+    (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬ c → y = v) : myif b x y = myif c u v := by
+  unfold myif
+  apply @ite_congr <;> assumption
+
+def f (x : Nat) (y z : Nat) : Nat :=
+  myif (myid x = 0) y z
+
+def g (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | a+1 => f x (g a + 1) (g a)
+
+-- `simp` should not be exponential on `g (a + <num>)`
+theorem ex (h : a = 1) : g (a+32) = a := by
+  simp [g, f, h]

tests/lean/run/simproc1.lean

@@ -0,0 +1,32 @@
+import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Offset
+
+def foo (x : Nat) : Nat :=
+  x + 10
+
+simproc reduce_foo (foo _) := fun e => open Lean Meta in do
+  let some n ← evalNat e.appArg! |>.run | return none
+  return some (.done { expr := mkNatLit (n+10) })
+
+example : x + foo 2 = 12 + x := by
+  set_option simprocs false in
+    fail_if_success simp
+  simp
+  rw [Nat.add_comm]
+
+example : x + foo 2 = 12 + x := by
+  -- `simp only` must not use the default simproc set
+  fail_if_success simp only
+  simp
+  rw [Nat.add_comm]
+
+example : x + foo 2 = 12 + x := by
+  -- `simp only` does not use the default simproc set, but we can provide simprocs as arguments
+  simp only [reduce_foo]
+  rw [Nat.add_comm]
+
+example : x + foo 2 = 12 + x := by
+  -- We can use `-` to disable `simproc`s
+  fail_if_success simp [-reduce_foo]
+  simp
+  rw [Nat.add_comm]

tests/lean/run/simproc2.lean

@@ -0,0 +1,12 @@
+def foo (_ : Nat) : Nat := 10
+
+example : foo x = 8 + 2 := by
+  fail_if_success simp only
+  simp only [Nat.reduceAdd]
+  rw [foo]
+
+
+example : foo x = 8 + 2 := by
+  fail_if_success simp [-Nat.reduceAdd]
+  simp only [Nat.reduceAdd]
+  rw [foo]

tests/lean/run/simproc_panic.lean

@@ -0,0 +1,38 @@
+-- Extracted from Mathlib.Data.UnionFind.
+-- This file was failing in Mathlib during development of #3124.
+
+section Std.Data.Nat.Init.Lemmas
+
+protected theorem Nat.le_max_left (a b : Nat) : a ≤ max a b := sorry
+protected theorem Nat.le_max_right (a b : Nat) : b ≤ max a b := sorry
+
+end Std.Data.Nat.Init.Lemmas
+
+section Std.Data.Nat.Lemmas
+
+protected theorem Nat.lt_or_eq_of_le {n m : Nat} (h : n ≤ m) : n < m ∨ n = m := sorry
+
+end Std.Data.Nat.Lemmas
+
+section Mathlib.Data.UnionFind
+
+structure UFNode (α : Type _) where
+  parent : Nat
+  value : α
+  rank : Nat
+
+structure UnionFind (α) where
+  arr : Array (UFNode α)
+
+-- The `PANIC` can be avoided by turning `simprocs` off:
+-- set_option simprocs false
+
+def rankMaxAux (self : UnionFind α) : ∀ (i : Nat),
+    {k : Nat // ∀ j, j < i → ∀ h, (self.arr.get ⟨j, h⟩).rank ≤ k}
+  | 0 => ⟨0, fun j hj => nomatch hj⟩
+  | i+1 => by
+    let ⟨k, H⟩ := rankMaxAux self i
+    refine ⟨max k (if h : _ then (self.arr.get ⟨i, h⟩).rank else 0), fun j hj h ↦ ?_⟩
+    match j, Nat.lt_or_eq_of_le (Nat.le_of_lt_succ hj) with
+    | j, Or.inl hj => exact Nat.le_trans (H _ hj h) (Nat.le_max_left _ _)
+    | _, Or.inr rfl => simp [h, Nat.le_max_right]