chore: fix mistakes in test cases

Motivation: `simp?`

.github/workflows/pr-release.yml

@@ -6,6 +6,10 @@
 # Instead we use `workflow_run`, which essentially allows us to escalate privileges
 # (but only runs the CI as described in the `master` branch, not in the PR branch).
 
+# The main specification/documentation for this workflow is at
+# https://leanprover-community.github.io/contribute/tags_and_branches.html
+# Keep that in sync!
+
 name: PR release
 
 on:
@@ -69,6 +73,20 @@ jobs:
           # The token used here must have `workflow` privileges.
           GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
 
+      - name: Report release status
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: actions/github-script@v6
+        with:
+          script: |
+            await github.rest.repos.createCommitStatus({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}",
+              state: "success",
+              context: "PR toolchain",
+              description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}",
+            });
+
       - name: Add label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: actions/github-script@v7
@@ -100,13 +118,13 @@ jobs:
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: ready
         run: |
-          echo "Most recent nightly in your branch: $MOST_RECENT_NIGHTLY"
+          echo "Most recent nightly release in your branch: $MOST_RECENT_NIGHTLY"
           NIGHTLY_SHA=$(git -C lean4.git rev-parse "nightly-$MOST_RECENT_NIGHTLY^{commit}")
-          echo "SHA of most recent nightly: $NIGHTLY_SHA"
+          echo "SHA of most recent nightly release: $NIGHTLY_SHA"
           MERGE_BASE_SHA=$(git -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}")
           echo "SHA of merge-base: $MERGE_BASE_SHA"
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
-            echo "Most recent nightly tag agrees with the merge base."
+            echo "The merge base of this PR coincides with the nightly release"
 
             REMOTE_BRANCHES=$(git ls-remote -h https://github.com/leanprover-community/mathlib4.git nightly-testing-$MOST_RECENT_NIGHTLY)
 
@@ -115,7 +133,7 @@ jobs:
               MESSAGE=""
             else
               echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' branch."
-              MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-$MOST_RECENT_NIGHTLY' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow."
+              MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-$MOST_RECENT_NIGHTLY' branch does not exist there yet. We will retry when you push more commits. If you rebase your branch onto `nightly-with-mathlib`, Mathlib CI should run now."
             fi
 
           else
@@ -123,7 +141,7 @@ jobs:
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
             git -C lean4.git log -10 origin/master
 
-            MESSAGE="- ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch."
+            MESSAGE="- ❗ Mathlib CI will not be attempted unless your PR branches off the 'nightly-with-mathlib' branch."
           fi
 
           if [[ -n "$MESSAGE" ]]; then
@@ -146,13 +164,14 @@ jobs:
               # Append new result to the existing comment or post a new comment
               # It's essential we use the MATHLIB4_BOT token here, so that Mathlib CI can subsequently edit the comment.
               if [ -z "$existing_comment_id" ]; then
+                INTRO="Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)):"
                 # Post new comment with a bullet point
                 echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X POST \
                   -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
                   -H "Accept: application/vnd.github.v3+json" \
-                  -d "$(jq --null-input --arg val "$MESSAGE" '{"body": $val}')" \
+                  -d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body": $intro + "\n" + $val}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
               else
                 # Append new result to the existing comment
@@ -172,6 +191,25 @@ jobs:
             echo "mathlib_ready=true" >> $GITHUB_OUTPUT
           fi
 
+      - name: Report mathlib base
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} && steps.ready.outputs.mathlib_ready == 'true'
+        uses: actions/github-script@v6
+        with:
+          script: |
+            const description =
+              process.env.MOST_RECENT_NIGHTLY ?
+              "nightly-" + process.env.MOST_RECENT_NIGHTLY :
+              "not branched off nightly";
+            await github.rest.repos.createCommitStatus({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}",
+              state: "success",
+              context: "PR branched off:",
+              description: description,
+            });
+
+
       # We next automatically create a Mathlib branch using this toolchain.
       # Mathlib CI will be responsible for reporting back success or failure
       # to the PR comments asynchronously.

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/Float.lean

@@ -26,6 +26,7 @@ opaque floatSpec : FloatSpec := {
   decLe := fun _ _ => inferInstanceAs (Decidable True)
 }
 
+/-- Native floating point type, corresponding to 64-bit `double` in C. -/
 structure Float where
   val : floatSpec.float
 

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/Range.lean

@@ -76,10 +76,12 @@ macro_rules
 end Range
 end Std
 
-theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop := by
-  simp [Membership.mem] at h
-  exact h.2
+theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop := h.2
 
-theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i := by
-  simp [Membership.mem] at h
-  exact h.1
+theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i := h.1
+
+theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) :
+    i < n := h₂ ▸ h₁.2
+
+macro_rules
+  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Membership.get_elem_helper; assumption; rfl)

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/Data/Array.lean

@@ -28,8 +28,8 @@ def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool ×
   let mut numRemoved := 0
   for h1 : i in [:a.size] do for h2 : j in [i+1:a.size] do
     unless removed[i]! || removed[j]! do
-      let xi := a[i]'h1.2
-      let xj := a[j]'h2.2
+      let xi := a[i]
+      let xj := a[j]
       let (keepi, keepj) ← f xi xj
       unless keepi do
         numRemoved := numRemoved + 1
@@ -40,7 +40,7 @@ def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool ×
   let mut a' := Array.mkEmpty numRemoved
   for h : i in [:a.size] do
     unless removed[i]! do
-      a' := a'.push (a[i]'h.2)
+      a' := a'.push a[i]
   return a'
 
 end Array

src/Lean/Elab/Deriving/BEq.lean

@@ -91,9 +91,9 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
      $auxDefs:command*
     end)
 
-private def mkBEqInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "beq" declNames[0]!
-  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq declNames)
+private def mkBEqInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext "beq" declName
+  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq #[declName])
   trace[Elab.Deriving.beq] "\n{cmds}"
   return cmds
 
@@ -109,14 +109,18 @@ private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do
 
 open Command
 
+def mkBEqInstance (declName : Name) : CommandElabM Unit := do
+    let cmds ← liftTermElabM <|
+      if (← isEnumType declName) then
+        mkBEqEnumCmd declName
+      else
+         mkBEqInstanceCmds declName
+    cmds.forM elabCommand
+
 def mkBEqInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
-  if declNames.size == 1 && (← isEnumType declNames[0]!) then
-    let cmds ← liftTermElabM <| mkBEqEnumCmd declNames[0]!
-    cmds.forM elabCommand
-    return true
-  else if (← declNames.allM isInductive) && declNames.size > 0 then
-    let cmds ← liftTermElabM <| mkBEqInstanceCmds declNames
-    cmds.forM elabCommand
+  if (← declNames.allM isInductive) then
+    for declName in declNames do
+      mkBEqInstance declName
     return true
   else
     return false

src/Lean/Elab/Deriving/DecEq.lean

@@ -186,12 +186,15 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do
   trace[Elab.Deriving.decEq] "\n{cmd}"
   elabCommand cmd
 
-def mkDecEqInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
-  if (← isEnumType declNames[0]!) then
-    mkDecEqEnum declNames[0]!
+def mkDecEqInstance (declName : Name) : CommandElabM Bool := do
+  if (← isEnumType declName) then
+    mkDecEqEnum declName
     return true
   else
-    mkDecEq declNames[0]!
+    mkDecEq declName
+
+def mkDecEqInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
+  declNames.foldlM (fun b n => andM (pure b) (mkDecEqInstance n)) true
 
 builtin_initialize
   registerDerivingHandler `DecidableEq mkDecEqInstanceHandler

src/Lean/Elab/Deriving/FromToJson.lean

@@ -19,60 +19,58 @@ def mkJsonField (n : Name) : CoreM (Bool × Term) := do
   let s₁ := s.dropRightWhile (· == '?')
   return (s != s₁, Syntax.mkStrLit s₁)
 
-def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
-  if declNames.size == 1 then
-    if isStructure (← getEnv) declNames[0]! then
-      let cmds ← liftTermElabM do
-        let ctx ← mkContext "toJson" declNames[0]!
-        let header ← mkHeader ``ToJson 1 ctx.typeInfos[0]!
-        let fields := getStructureFieldsFlattened (← getEnv) declNames[0]! (includeSubobjectFields := false)
-        let fields ← fields.mapM fun field => do
-          let (isOptField, nm) ← mkJsonField field
-          let target := mkIdent header.targetNames[0]!
-          if isOptField then ``(opt $nm ($target).$(mkIdent field))
-          else ``([($nm, toJson ($target).$(mkIdent field))])
-        let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]!):ident $header.binders:bracketedBinder* : Json :=
-          mkObj <| List.join [$fields,*])
-        return #[cmd] ++ (← mkInstanceCmds ctx ``ToJson declNames)
-      cmds.forM elabCommand
-      return true
-    else
-      let indVal ← getConstInfoInduct declNames[0]!
-      let cmds ← liftTermElabM do
-        let ctx ← mkContext "toJson" declNames[0]!
-        let toJsonFuncId := mkIdent ctx.auxFunNames[0]!
-        -- Return syntax to JSONify `id`, either via `ToJson` or recursively
-        -- if `id`'s type is the type we're deriving for.
-        let mkToJson (id : Ident) (type : Expr) : TermElabM Term := do
-          if type.isAppOf indVal.name then `($toJsonFuncId:ident $id:ident)
-          else ``(toJson $id:ident)
-        let header ← mkHeader ``ToJson 1 ctx.typeInfos[0]!
-        let discrs ← mkDiscrs header indVal
-        let alts ← mkAlts indVal fun ctor args userNames => do
-          let ctorStr := ctor.name.eraseMacroScopes.getString!
-          match args, userNames with
-          | #[], _ => ``(toJson $(quote ctorStr))
-          | #[(x, t)], none => ``(mkObj [($(quote ctorStr), $(← mkToJson x t))])
-          | xs, none =>
-            let xs ← xs.mapM fun (x, t) => mkToJson x t
-            ``(mkObj [($(quote ctorStr), Json.arr #[$[$xs:term],*])])
-          | xs, some userNames =>
-            let xs ← xs.mapIdxM fun idx (x, t) => do
-              `(($(quote userNames[idx]!.eraseMacroScopes.getString!), $(← mkToJson x t)))
-            ``(mkObj [($(quote ctorStr), mkObj [$[$xs:term],*])])
-        let auxTerm ← `(match $[$discrs],* with $alts:matchAlt*)
-        let auxCmd ←
-          if ctx.usePartial then
-            let letDecls ← mkLocalInstanceLetDecls ctx ``ToJson header.argNames
-            let auxTerm ← mkLet letDecls auxTerm
-            `(private partial def $toJsonFuncId:ident $header.binders:bracketedBinder* : Json := $auxTerm)
-          else
-            `(private def $toJsonFuncId:ident $header.binders:bracketedBinder* : Json := $auxTerm)
-        return #[auxCmd] ++ (← mkInstanceCmds ctx ``ToJson declNames)
-      cmds.forM elabCommand
-      return true
+def mkToJsonInstance (declName : Name) : CommandElabM Bool := do
+  if isStructure (← getEnv) declName then
+    let cmds ← liftTermElabM do
+      let ctx ← mkContext "toJson" declName
+      let header ← mkHeader ``ToJson 1 ctx.typeInfos[0]!
+      let fields := getStructureFieldsFlattened (← getEnv) declName (includeSubobjectFields := false)
+      let fields ← fields.mapM fun field => do
+        let (isOptField, nm) ← mkJsonField field
+        let target := mkIdent header.targetNames[0]!
+        if isOptField then ``(opt $nm ($target).$(mkIdent field))
+        else ``([($nm, toJson ($target).$(mkIdent field))])
+      let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]!):ident $header.binders:bracketedBinder* : Json :=
+        mkObj <| List.join [$fields,*])
+      return #[cmd] ++ (← mkInstanceCmds ctx ``ToJson #[declName])
+    cmds.forM elabCommand
+    return true
   else
-    return false
+    let indVal ← getConstInfoInduct declName
+    let cmds ← liftTermElabM do
+      let ctx ← mkContext "toJson" declName
+      let toJsonFuncId := mkIdent ctx.auxFunNames[0]!
+      -- Return syntax to JSONify `id`, either via `ToJson` or recursively
+      -- if `id`'s type is the type we're deriving for.
+      let mkToJson (id : Ident) (type : Expr) : TermElabM Term := do
+        if type.isAppOf indVal.name then `($toJsonFuncId:ident $id:ident)
+        else ``(toJson $id:ident)
+      let header ← mkHeader ``ToJson 1 ctx.typeInfos[0]!
+      let discrs ← mkDiscrs header indVal
+      let alts ← mkAlts indVal fun ctor args userNames => do
+        let ctorStr := ctor.name.eraseMacroScopes.getString!
+        match args, userNames with
+        | #[], _ => ``(toJson $(quote ctorStr))
+        | #[(x, t)], none => ``(mkObj [($(quote ctorStr), $(← mkToJson x t))])
+        | xs, none =>
+          let xs ← xs.mapM fun (x, t) => mkToJson x t
+          ``(mkObj [($(quote ctorStr), Json.arr #[$[$xs:term],*])])
+        | xs, some userNames =>
+          let xs ← xs.mapIdxM fun idx (x, t) => do
+            `(($(quote userNames[idx]!.eraseMacroScopes.getString!), $(← mkToJson x t)))
+          ``(mkObj [($(quote ctorStr), mkObj [$[$xs:term],*])])
+      let auxTerm ← `(match $[$discrs],* with $alts:matchAlt*)
+      let auxCmd ←
+        if ctx.usePartial then
+          let letDecls ← mkLocalInstanceLetDecls ctx ``ToJson header.argNames
+          let auxTerm ← mkLet letDecls auxTerm
+          `(private partial def $toJsonFuncId:ident $header.binders:bracketedBinder* : Json := $auxTerm)
+        else
+          `(private def $toJsonFuncId:ident $header.binders:bracketedBinder* : Json := $auxTerm)
+      return #[auxCmd] ++ (← mkInstanceCmds ctx ``ToJson #[declName])
+    cmds.forM elabCommand
+    return true
+
 where
   mkAlts
     (indVal : InductiveVal)
@@ -103,54 +101,51 @@ where
       let rhs ← rhs ctorInfo binders (if userNames.size == binders.size then some userNames else none)
       `(matchAltExpr| | $[$patterns:term],* => $rhs:term)
 
-def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
-  if declNames.size == 1 then
-    let declName := declNames[0]!
-    if isStructure (← getEnv) declName then
-      let cmds ← liftTermElabM do
-        let ctx ← mkContext "fromJson" declName
-        let header ← mkHeader ``FromJson 0 ctx.typeInfos[0]!
-        let fields := getStructureFieldsFlattened (← getEnv) declName (includeSubobjectFields := false)
-        let getters ← fields.mapM (fun field => do
-          let getter ← `(getObjValAs? j _ $(Prod.snd <| ← mkJsonField field))
-          let getter ← `(doElem| Except.mapError (fun s => (toString $(quote declName)) ++ "." ++ (toString $(quote field)) ++ ": " ++ s) <| $getter)
-          return getter
-        )
-        let fields := fields.map mkIdent
-        let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]!):ident $header.binders:bracketedBinder* (j : Json)
-          : Except String $(← mkInductiveApp ctx.typeInfos[0]! header.argNames) := do
-          $[let $fields:ident ← $getters]*
-          return { $[$fields:ident := $(id fields)],* })
-        return #[cmd] ++ (← mkInstanceCmds ctx ``FromJson declNames)
-      cmds.forM elabCommand
-      return true
-    else
-      let indVal ← getConstInfoInduct declName
-      let cmds ← liftTermElabM do
-        let ctx ← mkContext "fromJson" declName
-        let header ← mkHeader ``FromJson 0 ctx.typeInfos[0]!
-        let fromJsonFuncId := mkIdent ctx.auxFunNames[0]!
-        let alts ← mkAlts indVal fromJsonFuncId
-        let mut auxTerm ← alts.foldrM (fun xs x => `(Except.orElseLazy $xs (fun _ => $x))) (← `(Except.error "no inductive constructor matched"))
-        if ctx.usePartial then
-          let letDecls ← mkLocalInstanceLetDecls ctx ``FromJson header.argNames
-          auxTerm ← mkLet letDecls auxTerm
-        -- FromJson is not structurally recursive even non-nested recursive inductives,
-        -- so we also use `partial` then.
-        let auxCmd ←
-          if ctx.usePartial || indVal.isRec then
-            `(private partial def $fromJsonFuncId:ident $header.binders:bracketedBinder* (json : Json)
-                  : Except String $(← mkInductiveApp ctx.typeInfos[0]! header.argNames) :=
-                $auxTerm)
-          else
-            `(private def $fromJsonFuncId:ident $header.binders:bracketedBinder* (json : Json)
-                  : Except String $(← mkInductiveApp ctx.typeInfos[0]! header.argNames) :=
-                $auxTerm)
-        return #[auxCmd] ++ (← mkInstanceCmds ctx ``FromJson declNames)
-      cmds.forM elabCommand
-      return true
+def mkFromJsonInstance (declName : Name) : CommandElabM Bool := do
+  if isStructure (← getEnv) declName then
+    let cmds ← liftTermElabM do
+      let ctx ← mkContext "fromJson" declName
+      let header ← mkHeader ``FromJson 0 ctx.typeInfos[0]!
+      let fields := getStructureFieldsFlattened (← getEnv) declName (includeSubobjectFields := false)
+      let getters ← fields.mapM (fun field => do
+        let getter ← `(getObjValAs? j _ $(Prod.snd <| ← mkJsonField field))
+        let getter ← `(doElem| Except.mapError (fun s => (toString $(quote declName)) ++ "." ++ (toString $(quote field)) ++ ": " ++ s) <| $getter)
+        return getter
+      )
+      let fields := fields.map mkIdent
+      let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]!):ident $header.binders:bracketedBinder* (j : Json)
+        : Except String $(← mkInductiveApp ctx.typeInfos[0]! header.argNames) := do
+        $[let $fields:ident ← $getters]*
+        return { $[$fields:ident := $(id fields)],* })
+      return #[cmd] ++ (← mkInstanceCmds ctx ``FromJson #[declName])
+    cmds.forM elabCommand
+    return true
   else
-    return false
+    let indVal ← getConstInfoInduct declName
+    let cmds ← liftTermElabM do
+      let ctx ← mkContext "fromJson" declName
+      let header ← mkHeader ``FromJson 0 ctx.typeInfos[0]!
+      let fromJsonFuncId := mkIdent ctx.auxFunNames[0]!
+      let alts ← mkAlts indVal fromJsonFuncId
+      let mut auxTerm ← alts.foldrM (fun xs x => `(Except.orElseLazy $xs (fun _ => $x))) (← `(Except.error "no inductive constructor matched"))
+      if ctx.usePartial then
+        let letDecls ← mkLocalInstanceLetDecls ctx ``FromJson header.argNames
+        auxTerm ← mkLet letDecls auxTerm
+      -- FromJson is not structurally recursive even non-nested recursive inductives,
+      -- so we also use `partial` then.
+      let auxCmd ←
+        if ctx.usePartial || indVal.isRec then
+          `(private partial def $fromJsonFuncId:ident $header.binders:bracketedBinder* (json : Json)
+                : Except String $(← mkInductiveApp ctx.typeInfos[0]! header.argNames) :=
+              $auxTerm)
+        else
+          `(private def $fromJsonFuncId:ident $header.binders:bracketedBinder* (json : Json)
+                : Except String $(← mkInductiveApp ctx.typeInfos[0]! header.argNames) :=
+              $auxTerm)
+      return #[auxCmd] ++ (← mkInstanceCmds ctx ``FromJson #[declName])
+    cmds.forM elabCommand
+    return true
+
 where
   mkAlts (indVal : InductiveVal) (fromJsonFuncId : Ident) : TermElabM (Array Term) := do
   let alts ←
@@ -188,6 +183,12 @@ where
   let alts := alts.qsort (fun (_, x) (_, y) => x < y)
   return alts.map Prod.fst
 
+def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
+  declNames.foldlM (fun b n => andM (pure b) (mkToJsonInstance n)) true
+
+def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
+  declNames.foldlM (fun b n => andM (pure b) (mkFromJsonInstance n)) true
+
 builtin_initialize
   registerDerivingHandler ``ToJson mkToJsonInstanceHandler
   registerDerivingHandler ``FromJson mkFromJsonInstanceHandler

src/Lean/Elab/Deriving/Hashable.lean

@@ -75,16 +75,17 @@ def mkHashFuncs (ctx : Context) : TermElabM Syntax := do
     auxDefs := auxDefs.push (← mkAuxFunction ctx i)
   `(mutual $auxDefs:command* end)
 
-private def mkHashableInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "hash" declNames[0]!
-  let cmds := #[← mkHashFuncs ctx] ++ (← mkInstanceCmds ctx `Hashable declNames)
+private def mkHashableInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext "hash" declName
+  let cmds := #[← mkHashFuncs ctx] ++ (← mkInstanceCmds ctx `Hashable #[declName])
   trace[Elab.Deriving.hashable] "\n{cmds}"
   return cmds
 
 def mkHashableHandler (declNames : Array Name) : CommandElabM Bool := do
-  if (← declNames.allM isInductive) && declNames.size > 0 then
-    let cmds ← liftTermElabM <| mkHashableInstanceCmds declNames
-    cmds.forM elabCommand
+  if (← declNames.allM isInductive)  then
+    for declName in declNames do
+      let cmds ← liftTermElabM <| mkHashableInstanceCmds declName
+      cmds.forM elabCommand
     return true
   else
     return false

src/Lean/Elab/Deriving/Ord.lean

@@ -86,18 +86,19 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
      $auxDefs:command*
     end)
 
-private def mkOrdInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "ord" declNames[0]!
-  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Ord declNames)
+private def mkOrdInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext "ord" declName
+  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Ord #[declName])
   trace[Elab.Deriving.ord] "\n{cmds}"
   return cmds
 
 open Command
 
 def mkOrdInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
-  if (← declNames.allM isInductive) && declNames.size > 0 then
-    let cmds ← liftTermElabM <| mkOrdInstanceCmds declNames
-    cmds.forM elabCommand
+  if (← declNames.allM isInductive) then
+    for declName in declNames do
+      let cmds ← liftTermElabM <| mkOrdInstanceCmds declName
+      cmds.forM elabCommand
     return true
   else
     return false

src/Lean/Elab/Deriving/Repr.lean

@@ -104,18 +104,19 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
      $auxDefs:command*
     end)
 
-private def mkReprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "repr" declNames[0]!
-  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr declNames)
+private def mkReprInstanceCmd (declName : Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext "repr" declName
+  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr #[declName])
   trace[Elab.Deriving.repr] "\n{cmds}"
   return cmds
 
 open Command
 
 def mkReprInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
-  if (← declNames.allM isInductive) && declNames.size > 0 then
-    let cmds ← liftTermElabM <| mkReprInstanceCmds declNames
-    cmds.forM elabCommand
+  if (← declNames.allM isInductive) then
+    for declName in declNames do
+      let cmds ← liftTermElabM <| mkReprInstanceCmd declName
+      cmds.forM elabCommand
     return true
   else
     return false

src/Lean/Elab/Deriving/SizeOf.lean

@@ -16,8 +16,9 @@ namespace Lean.Elab.Deriving.SizeOf
 open Command
 
 def mkSizeOfHandler (declNames : Array Name) : CommandElabM Bool := do
-  if (← declNames.allM isInductive) && declNames.size > 0 then
-    liftTermElabM <| Meta.mkSizeOfInstances declNames[0]!
+  if (← declNames.allM isInductive) then
+    for declName in declNames do
+      liftTermElabM <| Meta.mkSizeOfInstances declName
     return true
   else
     return false

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

@@ -36,73 +36,12 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   mvarId.assign (← mkEqTrans h mvarNew)
   return mvarNew.mvarId!
 
-private def hasWellFoundedFix (e : Expr) : Bool :=
-  Option.isSome <| e.find? (·.isConstOf ``WellFounded.fix)
-
-/--
-  Helper function for decoding the packed argument for a `WellFounded.fix` application.
-  Recall that we use `PSum` and `PSigma` for packing the arguments of mutually recursive nary functions.
--/
-private partial def decodePackedArg? (info : EqnInfo) (e : Expr) : Option (Name × Array Expr) := do
-  if info.declNames.size == 1 then
-    let args := decodePSigma e #[]
-    return (info.declNames[0]!, args)
-  else
-    decodePSum? e 0
-where
-  decodePSum? (e : Expr) (i : Nat) : Option (Name × Array Expr) := do
-    if e.isAppOfArity ``PSum.inl 3 then
-      decodePSum? e.appArg! i
-    else if e.isAppOfArity ``PSum.inr 3 then
-      decodePSum? e.appArg! (i+1)
-    else
-      guard (i < info.declNames.size)
-      return (info.declNames[i]!, decodePSigma e #[])
-
-  decodePSigma (e : Expr) (acc : Array Expr) : Array Expr :=
-    /- TODO: check arity of the given function. If it takes a PSigma as the last argument,
-       this function will produce incorrect results. -/
-    if e.isAppOfArity ``PSigma.mk 4 then
-       decodePSigma e.appArg! (acc.push e.appFn!.appArg!)
-    else
-       acc.push e
-
-/--
-  Try to fold `WellFounded.fix` applications that represent recursive applications of the functions in `info.declNames`.
-  We need that to make sure `simpMatchWF?` succeeds at goals such as
-  ```lean
-  ...
-  h : g x = 0
-  ...
-  |- (match (WellFounded.fix ...) with | ...) = ...
-  ```
-  where `WellFounded.fix ...` can be folded back to `g x`.
--/
-private def tryToFoldWellFoundedFix (info : EqnInfo) (us : List Level) (fixedPrefix : Array Expr) (e : Expr) : MetaM Expr := do
-  if hasWellFoundedFix e then
-    transform e (pre := pre)
-  else
-    return e
-where
-  pre (e : Expr) : MetaM TransformStep := do
-    let e' := e.headBeta
-    if e'.isAppOf ``WellFounded.fix && e'.getAppNumArgs >= 6 then
-      let args := e'.getAppArgs
-      let packedArg := args[5]!
-      let extraArgs := args[6:]
-      if let some (declName, args) := decodePackedArg? info packedArg then
-        let candidate := mkAppN (mkAppN (mkAppN (mkConst declName us) fixedPrefix) args) extraArgs
-        trace[Elab.definition.wf] "found nested WF at discr {candidate}"
-        if (← withDefault <| isDefEq candidate e) then
-          return .visit candidate
-    return .continue
-
 /--
   Simplify `match`-expressions when trying to prove equation theorems for a recursive declaration defined using well-founded recursion.
   It is similar to `simpMatch?`, but is also tries to fold `WellFounded.fix` applications occurring in discriminants.
   See comment at `tryToFoldWellFoundedFix`.
 -/
-def simpMatchWF? (info : EqnInfo) (us : List Level) (fixedPrefix : Array Expr) (mvarId : MVarId) : MetaM (Option MVarId) :=
+def simpMatchWF? (mvarId : MVarId) : MetaM (Option MVarId) :=
   mvarId.withContext do
     let target ← instantiateMVars (← mvarId.getType)
     let (targetNew, _) ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre })
@@ -111,32 +50,14 @@ def simpMatchWF? (info : EqnInfo) (us : List Level) (fixedPrefix : Array Expr) (
 where
   pre (e : Expr) : SimpM Simp.Step := do
     let some app ← matchMatcherApp? e | return Simp.Step.visit { expr := e }
-    if app.discrs.any hasWellFoundedFix then
-      let discrsNew ← app.discrs.mapM (tryToFoldWellFoundedFix info us fixedPrefix ·)
-      if discrsNew != app.discrs then
-        let app := { app with discrs := discrsNew }
-        let eNew := app.toExpr
-        trace[Elab.definition.wf] "folded discriminants {indentExpr eNew}"
-        return Simp.Step.visit { expr := app.toExpr }
     -- 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? app.matcherName e SplitIf.discharge?) with
       | some r => return r
       | none => return Simp.Step.visit { expr := e }
 
-private def tryToFoldLHS? (info : EqnInfo) (us : List Level) (fixedPrefix : Array Expr) (mvarId : MVarId) : MetaM (Option MVarId) :=
-  mvarId.withContext do
-    let target ← mvarId.getType'
-    let some (_, lhs, rhs) := target.eq? | unreachable!
-    let lhsNew ← tryToFoldWellFoundedFix info us fixedPrefix lhs
-    if lhs == lhsNew then return none
-    let targetNew ← mkEq lhsNew rhs
-    let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew
-    mvarId.assign mvarNew
-    return mvarNew.mvarId!
-
 /--
   Given a goal of the form `|- f.{us} a_1 ... a_n b_1 ... b_m = ...`, return `(us, #[a_1, ..., a_n])`
   where `f` is a constant named `declName`, and `n = info.fixedPrefixSize`.
@@ -151,25 +72,24 @@ private def getFixedPrefix (declName : Name) (info : EqnInfo) (mvarId : MVarId)
   trace[Elab.definition.wf.eqns] "fixedPrefix: {result}"
   return (lhs.getAppFn.constLevels!, result)
 
-private partial def mkProof (declName : Name) (info : EqnInfo) (type : Expr) : MetaM Expr := do
+private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
   trace[Elab.definition.wf.eqns] "proving: {type}"
   withNewMCtxDepth do
     let main ← mkFreshExprSyntheticOpaqueMVar type
     let (_, mvarId) ← main.mvarId!.intros
-    let (us, fixedPrefix) ← getFixedPrefix declName info mvarId
     let rec go (mvarId : MVarId) : MetaM Unit := do
       trace[Elab.definition.wf.eqns] "step\n{MessageData.ofGoal mvarId}"
       if (← tryURefl mvarId) then
         return ()
       else if (← tryContradiction mvarId) then
         return ()
-      else if let some mvarId ← simpMatchWF? info us fixedPrefix mvarId then
+      else if let some mvarId ← simpMatchWF? mvarId then
         go mvarId
       else if let some mvarId ← simpIf? mvarId then
         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 =>
@@ -177,9 +97,10 @@ private partial def mkProof (declName : Name) (info : EqnInfo) (type : Expr) : M
             mvarIds.forM go
           else if let some mvarIds ← splitTarget? mvarId then
             mvarIds.forM go
-          else if let some mvarId ← tryToFoldLHS? info us fixedPrefix mvarId then
-            go mvarId
           else
+            -- At some point in the past, we looked for occurences of Wf.fix to fold on the
+            -- LHS (introduced in 096e4eb), but it seems that code path was never used,
+            -- so #3133 removed it again (and can be recovered from there if this was premature).
             throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
     go (← rwFixEq (← deltaLHSUntilFix mvarId))
     instantiateMVars main
@@ -198,7 +119,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
     trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}"
     let name := baseName ++ (`_eq).appendIndexAfter (i+1)
     thmNames := thmNames.push name
-    let value ← mkProof declName info type
+    let value ← mkProof declName type
     let (type, value) ← removeUnusedEqnHypotheses type value
     addDecl <| Declaration.thmDecl {
       name, type, value

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

@@ -89,7 +89,7 @@ def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array
     let xs := xs.extract fixedPrefixSize xs.size
     let mut ns : Array Name := #[]
     for h : i in [:xs.size] do
-      let n ← (xs[i]'h.2).fvarId!.getUserName
+      let n ← xs[i].fvarId!.getUserName
       let n := if n.hasMacroScopes then .mkSimple s!"x{i+1}" else n
       ns := ns.push (← freshen ns n)
     return ns
@@ -505,7 +505,7 @@ partial def solve {m} {α} [Monad m] (measures : Array α)
 
     -- Find the first measure that has at least one < and otherwise only = or <=
     for h : measureIdx in [:measures.size] do
-      let measure := measures[measureIdx]'h.2
+      let measure := measures[measureIdx]
       let mut has_lt := false
       let mut all_le := true
       let mut todo := #[]
@@ -542,10 +542,10 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
     (measures : Array MutualMeasure) : MetaM TerminationWF := do
   let mut termByElements := #[]
   for h : funIdx in [:varNamess.size] do
-    let vars := (varNamess[funIdx]'h.2).map mkIdent
+    let vars := varNamess[funIdx].map mkIdent
     let body ← mkTupleSyntax (← measures.mapM fun
       | .args varIdxs => do
-          let v := vars.get! (varIdxs[funIdx]!)
+          let v := vars.get! varIdxs[funIdx]!
           let sizeOfIdent := mkIdent (← unresolveNameGlobal ``sizeOf)
           `($sizeOfIdent $v)
       | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
@@ -567,14 +567,14 @@ Single space as column separator.
 -/
 def formatTable : Array (Array String) → String := fun xss => Id.run do
   let mut colWidths := xss[0]!.map (fun _ => 0)
-  for i in [:xss.size] do
-    for j in [:xss[i]!.size] do
-      if xss[i]![j]!.length > colWidths[j]! then
-        colWidths := colWidths.set! j xss[i]![j]!.length
+  for hi : i in [:xss.size] do
+    for hj : j in [:xss[i].size] do
+      if xss[i][j].length > colWidths[j]! then
+        colWidths := colWidths.set! j xss[i][j].length
   let mut str := ""
-  for i in [:xss.size] do
-    for j in [:xss[i]!.size] do
-      let s := xss[i]![j]!
+  for hi : i in [:xss.size] do
+    for hj : j in [:xss[i].size] do
+      let s := xss[i][j]
       if j > 0 then -- right-align
         for _ in [:colWidths[j]! - s.length] do
           str := str ++ " "
@@ -582,7 +582,7 @@ def formatTable : Array (Array String) → String := fun xss => Id.run do
       if j = 0 then -- left-align
         for _ in [:colWidths[j]! - s.length] do
           str := str ++ " "
-      if j + 1 < xss[i]!.size then
+      if j + 1 < xss[i].size then
         str := str ++ " "
     if i + 1 < xss.size then
       str := str ++ "\n"

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

@@ -35,7 +35,7 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
     if element.vars.size > varNames.size then
       throwErrorAt element.vars[varNames.size]! "too many variable names"
     for h : i in [:element.vars.size] do
-      let varStx := element.vars[i]'h.2
+      let varStx := element.vars[i]
       if let `($ident:ident) := varStx then
         varNames := varNames.set! (varNames.size - element.vars.size + i) ident.getId
     return varNames

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 =>
@@ -867,6 +872,11 @@ def reduceNat? (e : Expr) : MetaM (Option Expr) :=
     | ``Nat.gcd => reduceBinNatOp Nat.gcd a1 a2
     | ``Nat.beq => reduceBinNatPred Nat.beq a1 a2
     | ``Nat.ble => reduceBinNatPred Nat.ble a1 a2
+    | ``Nat.land => reduceBinNatOp Nat.land a1 a2
+    | ``Nat.lor  => reduceBinNatOp Nat.lor a1 a2
+    | ``Nat.xor  => reduceBinNatOp Nat.xor a1 a2
+    | ``Nat.shiftLeft  => reduceBinNatOp Nat.shiftLeft a1 a2
+    | ``Nat.shiftRight => reduceBinNatOp Nat.shiftRight a1 a2
     | _ => return none
   | _ =>
     return none

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

src/kernel/type_checker.cpp

@@ -35,6 +35,11 @@ static expr * g_nat_mod      = nullptr;
 static expr * g_nat_div      = nullptr;
 static expr * g_nat_beq      = nullptr;
 static expr * g_nat_ble      = nullptr;
+static expr * g_nat_land     = nullptr;
+static expr * g_nat_lor      = nullptr;
+static expr * g_nat_xor      = nullptr;
+static expr * g_nat_shiftLeft  = nullptr;
+static expr * g_nat_shiftRight = nullptr;
 
 type_checker::state::state(environment const & env):
     m_env(env), m_ngen(*g_kernel_fresh) {}
@@ -609,6 +614,11 @@ optional<expr> type_checker::reduce_nat(expr const & e) {
         if (f == *g_nat_div) return reduce_bin_nat_op(nat_div, e);
         if (f == *g_nat_beq) return reduce_bin_nat_pred(nat_eq, e);
         if (f == *g_nat_ble) return reduce_bin_nat_pred(nat_le, e);
+        if (f == *g_nat_land) return reduce_bin_nat_op(nat_land, e);
+        if (f == *g_nat_lor)  return reduce_bin_nat_op(nat_lor, e);
+        if (f == *g_nat_xor)  return reduce_bin_nat_op(nat_lxor, e);
+        if (f == *g_nat_shiftLeft) return reduce_bin_nat_op(lean_nat_shiftl, e);
+        if (f == *g_nat_shiftRight) return reduce_bin_nat_op(lean_nat_shiftr, e);
     }
     return none_expr();
 }
@@ -1006,7 +1016,7 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
     bool use_hash = true;
     lbool r = quick_is_def_eq(t, s, use_hash);
     if (r != l_undef) return r == l_true;
-    
+
     // Very basic support for proofs by reflection. If `t` has no free variables and `s` is `Bool.true`,
     // we fully reduce `t` and check whether result is `s`.
     // TODO: add metadata to control whether this optimization is used or not.
@@ -1135,46 +1145,44 @@ extern "C" LEAN_EXPORT lean_object * lean_kernel_whnf(lean_object * env, lean_ob
     });
 }
 
+inline static expr * new_persistent_expr_const(name const & n) {
+    expr * e = new expr(mk_const(n));
+    mark_persistent(e->raw());
+    return e;
+}
+
 void initialize_type_checker() {
-    g_dont_care    = new expr(mk_const("dontcare"));
-    mark_persistent(g_dont_care->raw());
     g_kernel_fresh = new name("_kernel_fresh");
     mark_persistent(g_kernel_fresh->raw());
     g_bool_true    = new name{"Bool", "true"};
-    g_nat_zero     = new expr(mk_constant(name{"Nat", "zero"}));
-    mark_persistent(g_nat_zero->raw());
-    g_nat_succ     = new expr(mk_constant(name{"Nat", "succ"}));
-    mark_persistent(g_nat_succ->raw());
-    g_nat_add      = new expr(mk_constant(name{"Nat", "add"}));
-    mark_persistent(g_nat_add->raw());
-    g_nat_sub      = new expr(mk_constant(name{"Nat", "sub"}));
-    mark_persistent(g_nat_sub->raw());
-    g_nat_mul      = new expr(mk_constant(name{"Nat", "mul"}));
-    mark_persistent(g_nat_mul->raw());
-    g_nat_pow      = new expr(mk_constant(name{"Nat", "pow"}));
-    mark_persistent(g_nat_pow->raw());
-    g_nat_gcd      = new expr(mk_constant(name{"Nat", "gcd"}));
-    mark_persistent(g_nat_gcd->raw());
-    g_nat_div      = new expr(mk_constant(name{"Nat", "div"}));
-    mark_persistent(g_nat_div->raw());
-    g_nat_mod      = new expr(mk_constant(name{"Nat", "mod"}));
-    mark_persistent(g_nat_mod->raw());
-    g_nat_beq      = new expr(mk_constant(name{"Nat", "beq"}));
-    mark_persistent(g_nat_beq->raw());
-    g_nat_ble      = new expr(mk_constant(name{"Nat", "ble"}));
-    mark_persistent(g_nat_ble->raw());
-    g_string_mk    = new expr(mk_constant(name{"String", "mk"}));
-    mark_persistent(g_string_mk->raw());
-    g_lean_reduce_bool = new expr(mk_constant(name{"Lean", "reduceBool"}));
-    mark_persistent(g_lean_reduce_bool->raw());
-    g_lean_reduce_nat  = new expr(mk_constant(name{"Lean", "reduceNat"}));
-    mark_persistent(g_lean_reduce_nat->raw());
+    mark_persistent(g_bool_true->raw());
+    g_dont_care    = new_persistent_expr_const("dontcare");
+    g_nat_zero     = new_persistent_expr_const({"Nat", "zero"});
+    g_nat_succ     = new_persistent_expr_const({"Nat", "succ"});
+    g_nat_add      = new_persistent_expr_const({"Nat", "add"});
+    g_nat_sub      = new_persistent_expr_const({"Nat", "sub"});
+    g_nat_mul      = new_persistent_expr_const({"Nat", "mul"});
+    g_nat_pow      = new_persistent_expr_const({"Nat", "pow"});
+    g_nat_gcd      = new_persistent_expr_const({"Nat", "gcd"});
+    g_nat_div      = new_persistent_expr_const({"Nat", "div"});
+    g_nat_mod      = new_persistent_expr_const({"Nat", "mod"});
+    g_nat_beq      = new_persistent_expr_const({"Nat", "beq"});
+    g_nat_ble      = new_persistent_expr_const({"Nat", "ble"});
+    g_nat_land     = new_persistent_expr_const({"Nat", "land"});
+    g_nat_lor      = new_persistent_expr_const({"Nat", "lor"});
+    g_nat_xor      = new_persistent_expr_const({"Nat", "xor"});
+    g_nat_shiftLeft  = new_persistent_expr_const({"Nat", "shiftLeft"});
+    g_nat_shiftRight = new_persistent_expr_const({"Nat", "shiftRight"});
+    g_string_mk    = new_persistent_expr_const({"String", "mk"});
+    g_lean_reduce_bool = new_persistent_expr_const({"Lean", "reduceBool"});
+    g_lean_reduce_nat  = new_persistent_expr_const({"Lean", "reduceNat"});
     register_name_generator_prefix(*g_kernel_fresh);
 }
 
 void finalize_type_checker() {
-    delete g_dont_care;
     delete g_kernel_fresh;
+    delete g_bool_true;
+    delete g_dont_care;
     delete g_nat_succ;
     delete g_nat_zero;
     delete g_nat_add;
@@ -1186,6 +1194,11 @@ void finalize_type_checker() {
     delete g_nat_mod;
     delete g_nat_beq;
     delete g_nat_ble;
+    delete g_nat_land;
+    delete g_nat_lor;
+    delete g_nat_xor;
+    delete g_nat_shiftLeft;
+    delete g_nat_shiftRight;
     delete g_string_mk;
     delete g_lean_reduce_bool;
     delete g_lean_reduce_nat;