spacing

.github/workflows/check-prelude.yml

@@ -1,26 +0,0 @@
-name: Check for modules that should use `prelude`
-
-on: [pull_request]
-
-jobs:
-  check-prelude:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v4
-        with:
-          # the default is to use a virtual merge commit between the PR and master: just use the PR
-          ref: ${{ github.event.pull_request.head.sha }}
-          sparse-checkout: src/Lean
-      - name: Check Prelude
-        run: |
-          failed_files=""
-          while IFS= read -r -d '' file; do
-            if ! grep -q "^prelude$" "$file"; then
-              failed_files="$failed_files$file\n"
-            fi
-          done < <(find src/Lean -name '*.lean' -print0)
-          if [ -n "$failed_files" ]; then
-            echo -e "The following files should use 'prelude':\n$failed_files"
-            exit 1
-          fi

.github/workflows/ci.yml

@@ -410,8 +410,7 @@ jobs:
         run: |
           cd build
           ulimit -c unlimited # coredumps
-          # clean rebuild in case of Makefile changes
-          make update-stage0 && rm -rf ./stage* && make -j4
+          make update-stage0 && make -j4
         if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false'
       - name: CCache stats
         run: ccache -s

RELEASES.md

@@ -18,10 +18,6 @@ v4.7.0 (development in progress)
 
 * `pp.proofs.withType` is now set to false by default to reduce noise in the info view.
 
-* The pretty printer for applications now handles the case of over-application itself when applying app unexpanders.
-  In particular, the ``| `($_ $a $b $xs*) => `(($a + $b) $xs*)`` case of an `app_unexpander` is no longer necessary.
-  [#3495](https://github.com/leanprover/lean4/pull/3495).
-
 * New `simp` (and `dsimp`) configuration option: `zetaDelta`. It is `false` by default.
   The `zeta` option is still `true` by default, but their meaning has changed.
   - When `zeta := true`, `simp` and `dsimp` reduce terms of the form
@@ -30,7 +26,7 @@ v4.7.0 (development in progress)
     the context. For example, suppose the context contains `x := val`. Then,
     any occurrence of `x` is replaced with `val`.
 
-  See [issue #2682](https://github.com/leanprover/lean4/pull/2682) for additional details. Here are some examples:
+  See issue [#2682](https://github.com/leanprover/lean4/pull/2682) for additional details. Here are some examples:
   ```
   example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
     intro x
@@ -71,7 +67,7 @@ v4.7.0 (development in progress)
   ```
 
 * When adding new local theorems to `simp`, the system assumes that the function application arguments
-  have been annotated with `no_index`. This modification, which addresses [issue #2670](https://github.com/leanprover/lean4/issues/2670),
+  have been annotated with `no_index`. This modification, which addresses issue [#2670](https://github.com/leanprover/lean4/issues/2670),
   restores the Lean 3 behavior that users expect. With this modification, the following examples are now operational:
   ```
   example {α β : Type} {f : α × β → β → β} (h : ∀ p : α × β, f p p.2 = p.2)
@@ -85,30 +81,6 @@ v4.7.0 (development in progress)
   In both cases, `h` is applicable because `simp` does not index f-arguments anymore when adding `h` to the `simp`-set.
   It's important to note, however, that global theorems continue to be indexed in the usual manner.
 
-* Improved the error messages produced by the `decide` tactic. [#3422](https://github.com/leanprover/lean4/pull/3422)
-
-* Improved auto-completion performance. [#3460](https://github.com/leanprover/lean4/pull/3460)
-
-* Improved initial language server startup performance. [#3552](https://github.com/leanprover/lean4/pull/3552)
-
-* Changed call hierarchy to sort entries and strip private header from names displayed in the call hierarchy. [#3482](https://github.com/leanprover/lean4/pull/3482)
-
-* There is now a low-level error recovery combinator in the parsing framework, primarily intended for DSLs. [#3413](https://github.com/leanprover/lean4/pull/3413)
-* The Library search `exact?` and `apply?` tactics that were originally in
-* The library search tactics `exact?` and `apply?` that were originally in
-  Mathlib are now available in Lean itself.  These use the implementation using
-  lazy discrimination trees from `Std`, and thus do not require a disk cache but
-  have a slightly longer startup time.  The order used for selection lemmas has
-  changed as well to favor goals purely based on how many terms in the head
-  pattern match the current goal.
-
-* The `solve_by_elim` tactic has been ported from `Std` to Lean so that library
-  search can use it.
-
-* New `#check_tactic` and `#check_simp` commands have been added.  These are
-  useful for checking tactics (particularly `simp`) behave as expected in test
-  suites.
-
 Breaking changes:
 * `Lean.withTraceNode` and variants got a stronger `MonadAlwaysExcept` assumption to
   fix trace trees not being built on elaboration runtime exceptions. Instances for most elaboration
@@ -118,67 +90,67 @@ v4.6.0
 ---------
 
 * 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
+```lean
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
-  def foo (x : Nat) : Nat :=
-    x + 10
+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 Step -/
-    fun e => do
-      /-
-      The `Step` type has three constructors: `.done`, `.visit`, `.continue`.
-      * The constructor `.done` instructs `simp` that the result does
-        not need to be simplied further.
-      * The constructor `.visit` instructs `simp` to visit the resulting expression.
-      * The constructor `.continue` instructs `simp` to try other simplification procedures.
-
-      All three constructors take a `Result`. The `.continue` contructor may also take `none`.
-      `Result` has two fields `expr` (the new expression), and `proof?` (an optional proof).
-       If the new expression is definitionally equal to the input one, then `proof?` can be omitted or set to `none`.
-      -/
-      /- `simp` uses matching modulo reducibility. So, we ensure the term is a `foo`-application. -/
-      unless e.isAppOfArity ``foo 1 do
-        return .continue
-      /- `Nat.fromExpr?` tries to convert an expression into a `Nat` value -/
-      let some n ← Nat.fromExpr? e.appArg!
-        | return .continue
-      return .done { expr := Lean.mkNatLit (n+10) }
-  ```
-  We disable simprocs support by using the command `set_option simprocs false`. This command is particularly useful when porting files to v4.6.0.
-  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 not 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
+/--
+The `simproc` `reduceFoo` is invoked on terms that match the pattern `foo _`.
+-/
+simproc reduceFoo (foo _) :=
+  /- A term of type `Expr → SimpM Step -/
+  fun e => do
     /-
-    `simp only` does not use the default simproc set,
-    but we can provide simprocs as arguments. -/
-    simp only [reduceFoo]
-    simp_arith
+    The `Step` type has three constructors: `.done`, `.visit`, `.continue`.
+    * The constructor `.done` instructs `simp` that the result does
+      not need to be simplied further.
+    * The constructor `.visit` instructs `simp` to visit the resulting expression.
+    * The constructor `.continue` instructs `simp` to try other simplification procedures.
 
-  example : x + foo 2 = 12 + x := by
-    /- We can use `-` to disable `simproc`s. -/
-    fail_if_success simp [-reduceFoo]
-    simp_arith
-  ```
-  The command `register_simp_attr <id>` now creates a `simp` **and** a `simproc` set with the name `<id>`. The following command instructs Lean to insert the `reduceFoo` simplification procedure into the set `my_simp`. If no set is specified, Lean uses the default `simp` set.
-  ```lean
-  simproc [my_simp] reduceFoo (foo _) := ...
-  ```
+    All three constructors take a `Result`. The `.continue` contructor may also take `none`.
+    `Result` has two fields `expr` (the new expression), and `proof?` (an optional proof).
+     If the new expression is definitionally equal to the input one, then `proof?` can be omitted or set to `none`.
+    -/
+    /- `simp` uses matching modulo reducibility. So, we ensure the term is a `foo`-application. -/
+    unless e.isAppOfArity ``foo 1 do
+      return .continue
+    /- `Nat.fromExpr?` tries to convert an expression into a `Nat` value -/
+    let some n ← Nat.fromExpr? e.appArg!
+      | return .continue
+    return .done { expr := Lean.mkNatLit (n+10) }
+```
+We disable simprocs support by using the command `set_option simprocs false`. This command is particularly useful when porting files to v4.6.0.
+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 not 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
+```
+The command `register_simp_attr <id>` now creates a `simp` **and** a `simproc` set with the name `<id>`. The following command instructs Lean to insert the `reduceFoo` simplification procedure into the set `my_simp`. If no set is specified, Lean uses the default `simp` set.
+```lean
+simproc [my_simp] reduceFoo (foo _) := ...
+```
 
 * The syntax of the `termination_by` and `decreasing_by` termination hints is overhauled:
 
@@ -317,7 +289,7 @@ v4.6.0
   and hence greatly reduces the reliance on costly structure eta reduction. This has a large impact on mathlib,
   reducing total CPU instructions by 3% and enabling impactful refactors like leanprover-community/mathlib4#8386
   which reduces the build time by almost 20%.
-  See [PR #2478](https://github.com/leanprover/lean4/pull/2478) and [RFC #2451](https://github.com/leanprover/lean4/issues/2451).
+  See PR [#2478](https://github.com/leanprover/lean4/pull/2478) and RFC [#2451](https://github.com/leanprover/lean4/issues/2451).
 
 * Add pretty printer settings to omit deeply nested terms (`pp.deepTerms false` and `pp.deepTerms.threshold`) ([PR #3201](https://github.com/leanprover/lean4/pull/3201))
 
@@ -336,7 +308,7 @@ Other improvements:
 * produce simpler proof terms in `rw` [#3121](https://github.com/leanprover/lean4/pull/3121)
 * fuse nested `mkCongrArg` calls in proofs generated by `simp` [#3203](https://github.com/leanprover/lean4/pull/3203)
 * `induction using` followed by a general term [#3188](https://github.com/leanprover/lean4/pull/3188)
-* allow generalization in `let` [#3060](https://github.com/leanprover/lean4/pull/3060), fixing [#3065](https://github.com/leanprover/lean4/issues/3065)
+* allow generalization in `let` [#3060](https://github.com/leanprover/lean4/pull/3060, fixing [#3065](https://github.com/leanprover/lean4/issues/3065)
 * reducing out-of-bounds `swap!` should return `a`, not `default`` [#3197](https://github.com/leanprover/lean4/pull/3197), fixing [#3196](https://github.com/leanprover/lean4/issues/3196)
 * derive `BEq` on structure with `Prop`-fields [#3191](https://github.com/leanprover/lean4/pull/3191), fixing [#3140](https://github.com/leanprover/lean4/issues/3140)
 * refine through more `casesOnApp`/`matcherApp` [#3176](https://github.com/leanprover/lean4/pull/3176), fixing [#3175](https://github.com/leanprover/lean4/pull/3175)

script/prepare-llvm-linux.sh

@@ -25,8 +25,6 @@ cp -L llvm/bin/llvm-ar stage1/bin/
 # dependencies of the above
 $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/
 $CP $ZLIB/lib/libz.so* stage1/lib/
-# general clang++ dependency, breaks cross-library C++ exceptions if linked statically
-$CP $GCC_LIB/lib/libgcc_s.so* stage1/lib/
 # bundle libatomic (referenced by LLVM >= 15, and required by the lean executable to run)
 $CP $GCC_LIB/lib/libatomic.so* stage1/lib/
 
@@ -62,7 +60,7 @@ fi
 # use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
 # but do not change sysroot so users can still link against system libs
 echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
 # when not using the above flags, link GMP dynamically/as usual
 echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests

src/CMakeLists.txt

@@ -501,18 +501,24 @@ string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
 # (also looks nicer in the build log)
 file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
-# set up libInit_shared only on Windows; see also stdlib.make.in
-if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
+if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
+  string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a")
+else()
+  string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive")
+  if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+    string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
+  endif()
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
-elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
 else()
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive")
+  if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+    string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
+  endif()
 endif()
+string(APPEND LEANSHARED_LINKER_FLAGS " -lInit_shared")
 
 if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   # We do not use dynamic linking via leanshared for Emscripten to keep things

src/Init/Coe.lean

@@ -321,7 +321,7 @@ Helper definition used by the elaborator. It is not meant to be used directly by
 This is used for coercions between monads, in the case where we want to apply
 a monad lift and a coercion on the result type at the same time.
 -/
-@[coe_decl] abbrev Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u}
+@[inline, coe_decl] def Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u}
     [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
   let a ← liftM x
   pure (CoeT.coe a)
@@ -331,7 +331,7 @@ Helper definition used by the elaborator. It is not meant to be used directly by
 
 This is used for coercing the result type under a monad.
 -/
-@[coe_decl] abbrev Lean.Internal.coeM {m : Type u → Type v} {α β : Type u}
+@[inline, coe_decl] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u}
     [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
   let a ← x
   pure (CoeT.coe a)

src/Init/Data/Array/Lemmas.lean

@@ -185,84 +185,3 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
 
 theorem mem_def (a : α) (as : Array α) : a ∈ as ↔ a ∈ as.data :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
-
-/-- # get -/
-@[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
-
-theorem getElem?_lt
-    (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some (a[i]) := dif_pos h
-
-theorem getElem?_ge
-    (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
-
-@[simp] theorem get?_eq_getElem? (a : Array α) (i : Nat) : a.get? i = a[i]? := rfl
-
-theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = none := by
-  simp [getElem?_ge, h]
-
-theorem getD_get? (a : Array α) (i : Nat) (d : α) :
-  Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
-  if h : i < a.size then
-    simp [setD, h, getElem?]
-  else
-    have p : i ≥ a.size := Nat.le_of_not_gt h
-    simp [setD, getElem?_len_le _ p, h]
-
-@[simp] theorem getD_eq_get? (a : Array α) (n d) : a.getD n d = (a[n]?).getD d := by
-  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_get?, *]
-
-theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
-
-@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by
-  by_cases p : i < a.size <;> simp [getD_get?, get!_eq_getD, p]
-
-/-- # set -/
-
-@[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
-      (eq : i.val = j) (p : j < (a.set i v).size) :
-    (a.set i v)[j]'p = v := by
-  simp [set, getElem_eq_data_get, ←eq]
-
-@[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
-    (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
-  simp only [set, getElem_eq_data_get, List.get_set_ne _ h]
-
-theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
-    (h : j < (a.set i v).size) :
-    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v ▸ h) := by
-  by_cases p : i.1 = j <;> simp [p]
-
-@[simp] theorem getElem?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1]? = v := by simp [getElem?_lt, i.2]
-
-@[simp] theorem getElem?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
-    (ne : i.val ≠ j) : (a.set i v)[j]? = a[j]? := by
-  by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
-
-/- # setD -/
-
-@[simp] theorem set!_is_setD : @set! = @setD := rfl
-
-@[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) :
-  (Array.setD a index val).size = a.size := by
-  if h : index < a.size  then
-    simp [setD, h]
-  else
-    simp [setD, h]
-
-@[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
-  (setD a i v)[i]'h = v := by
-  simp at h
-  simp only [setD, h, dite_true, getElem_set, ite_true]
-
-@[simp]
-theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setD i v)[i]? = some v := by
-  simp [getElem?_lt, p]
-
-/-- Simplifies a normal form from `get!` -/
-@[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) :
-  Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
-  by_cases h : i < a.size <;>
-    simp [setD, Nat.not_lt_of_le, h,  getD_get?]
-
-end Array

src/Init/Data/Array/Mem.lean

@@ -8,6 +8,16 @@ import Init.Data.Array.Basic
 import Init.Data.Nat.Linear
 import Init.Data.List.BasicAux
 
+theorem List.sizeOf_get_lt [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
+  match as, i with
+  | [],    i      => apply Fin.elim0 i
+  | a::as, ⟨0, _⟩ => simp_arith [get]
+  | a::as, ⟨i+1, h⟩ =>
+    simp [get]
+    have h : i < as.length := Nat.lt_of_succ_lt_succ h
+    have ih := sizeOf_get_lt as ⟨i, h⟩
+    exact Nat.lt_of_lt_of_le ih (Nat.le_add_left ..)
+
 namespace Array
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
@@ -19,6 +29,10 @@ structure Mem (a : α) (as : Array α) : Prop where
 instance : Membership α (Array α) where
   mem a as := Mem a as
 
+theorem sizeOf_get_lt [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
+  cases as with | _ as =>
+  exact Nat.lt_trans (List.sizeOf_get_lt as i) (by simp_arith)
+
 theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as := by
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)

src/Init/Data/BitVec/Basic.lean

@@ -8,6 +8,8 @@ import Init.Data.Fin.Basic
 import Init.Data.Nat.Bitwise.Lemmas
 import Init.Data.Nat.Power2
 
+namespace Std
+
 /-!
 We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
 (Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
@@ -33,8 +35,6 @@ structure BitVec (w : Nat) where
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
 
-@[deprecated] abbrev Std.BitVec := _root_.BitVec
-
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
 -- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
@@ -124,20 +124,13 @@ section Int
 
 /-- Interpret the bitvector as an integer stored in two's complement form. -/
 protected def toInt (a : BitVec n) : Int :=
-  if 2 * a.toNat < 2^n then
-    a.toNat
-  else
-    (a.toNat : Int) - (2^n : Nat)
+  if a.msb then Int.ofNat a.toNat - Int.ofNat (2^n) else a.toNat
 
 /-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`.  -/
-protected def ofInt (n : Nat) (i : Int) : BitVec n := .ofNatLt (i % (Int.ofNat (2^n))).toNat (by
-  apply (Int.toNat_lt _).mpr
-  · apply Int.emod_lt_of_pos
-    exact Int.ofNat_pos.mpr (Nat.two_pow_pos _)
-  · apply Int.emod_nonneg
-    intro eq
-    apply Nat.ne_of_gt (Nat.two_pow_pos n)
-    exact Int.ofNat_inj.mp eq)
+protected def ofInt (n : Nat) (i : Int) : BitVec n :=
+  match i with
+  | Int.ofNat x => .ofNat n x
+  | Int.negSucc x => BitVec.ofNatLt (2^n - x % 2^n - 1) (by omega)
 
 instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩
 
@@ -173,7 +166,7 @@ protected def toHex {n : Nat} (x : BitVec n) : String :=
   let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
   t ++ s
 
-instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
+instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Format) ++ "#" ++ repr n
 instance : ToString (BitVec n) where toString a := toString (repr a)
 
 end repr_toString
@@ -613,5 +606,3 @@ section normalization_eqs
 @[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
 @[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
 end normalization_eqs
-
-end BitVec

src/Init/Data/BitVec/Bitblast.lean

@@ -45,7 +45,7 @@ end Bool
 
 /-! ### Preliminaries -/
 
-namespace BitVec
+namespace Std.BitVec
 
 private theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
     testBit x i = decide (x ≥ 2^i) := by
@@ -91,7 +91,7 @@ private theorem mod_two_pow_succ (x i : Nat) :
 
 private theorem mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ
      (x y i : Nat) (c : Bool) : x % 2^i + (y % 2^i + c.toNat) < 2^(i+1) := by
-  have : c.toNat ≤ 1 := Bool.toNat_le c
+  have : c.toNat ≤ 1 := Bool.toNat_le_one c
   rw [Nat.pow_succ]
   omega
 
@@ -173,5 +173,3 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
 /-- Subtracting `x` from the all ones bitvector is equivalent to taking its complement -/
 theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
   rw [← add_not_self x, BitVec.add_comm, add_sub_cancel]
-
-end BitVec

src/Init/Data/BitVec/Folds.lean

@@ -8,7 +8,7 @@ import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Fin.Iterate
 
-namespace BitVec
+namespace Std.BitVec
 
 /--
 iunfoldr is an iterative operation that applies a function `f` repeatedly.
@@ -57,5 +57,3 @@ theorem iunfoldr_replace
     (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
     iunfoldr f a = (state w, value) := by
   simp [iunfoldr.eq_test state value a init step]
-
-end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -9,7 +9,7 @@ import Init.Data.BitVec.Basic
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
 
-namespace BitVec
+namespace Std.BitVec
 
 /--
 This normalized a bitvec using `ofFin` to `ofNat`.
@@ -133,35 +133,21 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
   · simp [BitVec.eq_nil x]
   · simp
 
-@[bv_toNat] theorem getLsb_last (x : BitVec w) :
-    x.getLsb (w-1) = decide (2 ^ (w-1) ≤ x.toNat) := by
-  rcases w with rfl | w
-  · simp
-  · simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
+@[bv_toNat] theorem getLsb_last (x : BitVec (w + 1)) :
+    x.getLsb w = decide (2 ^ w ≤ x.toNat) := by
+  simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
     Nat.sub_zero, Nat.and_one_is_mod, Bool.true_and, Nat.shiftRight_eq_div_pow]
-    rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
-    · simp [Nat.div_eq_of_lt h, h]
-    · simp only [h]
-      rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
-      · decide
-      · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
-        omega
+  rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
+  · simp [Nat.div_eq_of_lt h, h]
+  · simp only [h]
+    rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
+    · decide
+    · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
+      omega
 
-@[bv_toNat] theorem getLsb_succ_last (x : BitVec (w + 1)) :
-    x.getLsb w = decide (2 ^ w ≤ x.toNat) := getLsb_last x
-
-@[bv_toNat] theorem msb_eq_decide (x : BitVec w) : BitVec.msb x = decide (2 ^ (w-1) ≤ x.toNat) := by
+@[bv_toNat] theorem msb_eq_decide (x : BitVec (w + 1)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by
   simp [msb_eq_getLsb_last, getLsb_last]
 
-theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat ≥ 2^(n-1) := by
-  match n with
-  | 0 =>
-    simp [BitVec.msb, BitVec.getMsb] at p
-  | n + 1 =>
-    simp [BitVec.msb_eq_decide] at p
-    simp only [Nat.add_sub_cancel]
-    exact p
-
 /-! ### cast -/
 
 @[simp, bv_toNat] theorem toNat_cast (h : w = v) (x : BitVec w) : (cast h x).toNat = x.toNat := rfl
@@ -177,53 +163,6 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
 @[simp] theorem msb_cast (h : w = v) (x : BitVec w) : (cast h x).msb = x.msb := by
   simp [BitVec.msb]
 
-/-! ### toInt/ofInt -/
-
-/-- Prove equality of bitvectors in terms of nat operations. -/
-theorem toInt_eq_toNat_cond (i : BitVec n) :
-    i.toInt =
-      if 2*i.toNat < 2^n then
-        (i.toNat : Int)
-      else
-        (i.toNat : Int) - (2^n : Nat) := by
-  unfold BitVec.toInt
-  split <;> omega
-
-theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by
-  simp only [toInt_eq_toNat_cond]
-  split
-  case inl g =>
-    rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
-    omega
-  case inr g =>
-    rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
-    omega
-
-/-- Prove equality of bitvectors in terms of nat operations. -/
-theorem eq_of_toInt_eq {i j : BitVec n} : i.toInt = j.toInt → i = j := by
-  intro eq
-  simp [toInt_eq_toNat_cond] at eq
-  apply eq_of_toNat_eq
-  revert eq
-  have _ilt := i.isLt
-  have _jlt := j.isLt
-  split <;> split <;> omega
-
-@[simp] theorem toNat_ofInt {n : Nat} (i : Int) :
-  (BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat := by
-  unfold BitVec.ofInt
-  simp
-
-theorem toInt_ofNat {n : Nat} (x : Nat) :
-  (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by
-  simp [toInt_eq_toNat_bmod]
-
-@[simp] theorem toInt_ofInt {n : Nat} (i : Int) :
-  (BitVec.ofInt n i).toInt = i.bmod (2^n) := by
-  have _ := Nat.two_pow_pos n
-  have p : 0 ≤ i % (2^n : Nat) := by omega
-  simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p]
-
 /-! ### zeroExtend and truncate -/
 
 @[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
@@ -259,24 +198,6 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
   apply eq_of_toNat_eq
   simp
 
-/-- Moves one-sided left toNat equality to BitVec equality. -/
-theorem toNat_eq_nat (x : BitVec w) (y : Nat)
-  : (x.toNat = y) ↔ (y < 2^w ∧ (x = y#w)) := by
-  apply Iff.intro
-  · intro eq
-    simp at eq
-    have lt := x.isLt
-    simp [eq] at lt
-    simp [←eq, lt, x.isLt]
-  · intro eq
-    simp [Nat.mod_eq_of_lt, eq]
-
-/-- Moves one-sided right toNat equality to BitVec equality. -/
-theorem nat_eq_toNat (x : BitVec w) (y : Nat)
-  : (y = x.toNat) ↔ (y < 2^w ∧ (x = y#w)) := by
-  rw [@eq_comm _ _ x.toNat]
-  apply toNat_eq_nat
-
 @[simp] theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend' ge x) i = getLsb x i := by
   simp [getLsb, toNat_zeroExtend']
@@ -524,15 +445,6 @@ theorem truncate_succ (x : BitVec w) :
 
 /-! ### concat -/
 
-@[simp] theorem toNat_concat (x : BitVec w) (b : Bool) :
-    (concat x b).toNat = x.toNat * 2 + b.toNat := by
-  apply Nat.eq_of_testBit_eq
-  simp only [concat, toNat_append, Nat.shiftLeft_eq, Nat.pow_one, toNat_ofBool, Nat.testBit_or]
-  cases b
-  · simp
-  · rintro (_ | i)
-    <;> simp [Nat.add_mod, Nat.add_comm, Nat.add_mul_div_right]
-
 theorem getLsb_concat (x : BitVec w) (b : Bool) (i : Nat) :
     (concat x b).getLsb i = if i = 0 then b else x.getLsb (i - 1) := by
   simp only [concat, getLsb, toNat_append, toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq]
@@ -677,19 +589,3 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   let ⟨y, lt⟩ := y
   simp
   exact Nat.lt_of_le_of_ne
-
-/- ! ### intMax -/
-
-/-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
-def intMax (w : Nat) : BitVec w  := (2^w - 1)#w
-
-theorem getLsb_intMax_eq (w : Nat) : (intMax w).getLsb i = decide (i < w) := by
-  simp [intMax, getLsb]
-
-theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by
-  have h : 2^w - 1 < 2^w := by
-    have pos : 2^w > 0 := Nat.pow_pos (by decide)
-    omega
-  simp [intMax, Nat.shiftLeft_eq, Nat.one_mul, natCast_eq_ofNat, toNat_ofNat, Nat.mod_eq_of_lt h]
-
-end BitVec

src/Init/Data/Bool.lean

@@ -217,13 +217,11 @@ def toNat (b:Bool) : Nat := cond b 1 0
 
 @[simp] theorem toNat_true : true.toNat = 1 := rfl
 
-theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by
+theorem toNat_le_one (c:Bool) : c.toNat ≤ 1 := by
   cases c <;> trivial
 
-@[deprecated toNat_le] abbrev toNat_le_one := toNat_le
-
 theorem toNat_lt (b : Bool) : b.toNat < 2 :=
-  Nat.lt_succ_of_le (toNat_le _)
+  Nat.lt_succ_of_le (toNat_le_one _)
 
 @[simp] theorem toNat_eq_zero (b : Bool) : b.toNat = 0 ↔ b = false := by
   cases b <;> simp

src/Init/Data/Int/DivMod.lean

@@ -158,44 +158,4 @@ instance : Div Int where
 instance : Mod Int where
   mod := Int.emod
 
-/-!
-# `bmod` ("balanced" mod)
-
-Balanced mod (and balanced div) are a division and modulus pair such
-that `b * (Int.bdiv a b) + Int.bmod a b = a` and `b/2 ≤ Int.bmod a b <
-b/2` for all `a : Int` and `b > 0`.
-
-This is used in Omega as well as signed bitvectors.
--/
-
-/--
-Balanced modulus.  This version of Integer modulus uses the
-balanced rounding convention, which guarantees that
-`m/2 ≤ bmod x m < m/2` for `m ≠ 0` and `bmod x m` is congruent
-to `x` modulo `m`.
-
-If `m = 0`, then `bmod x m = x`.
--/
-def bmod (x : Int) (m : Nat) : Int :=
-  let r := x % m
-  if r < (m + 1) / 2 then
-    r
-  else
-    r - m
-
-/--
-Balanced division.  This returns the unique integer so that
-`b * (Int.bdiv a b) + Int.bmod a b = a`.
--/
-def bdiv (x : Int) (m : Nat) : Int :=
-  if m = 0 then
-    0
-  else
-    let q := x / m
-    let r := x % m
-    if r < (m + 1) / 2 then
-      q
-    else
-      q + 1
-
 end Int

src/Init/Data/Int/DivModLemmas.lean

@@ -325,78 +325,23 @@ theorem sub_ediv_of_dvd (a : Int) {b c : Int}
   rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_ediv_of_dvd_right (Int.dvd_neg.2 hcb)]
   congr; exact Int.neg_ediv_of_dvd hcb
 
-@[simp] theorem ediv_one : ∀ a : Int, a / 1 = a
-  | (_:Nat) => congrArg Nat.cast (Nat.div_one _)
-  | -[_+1]  => congrArg negSucc (Nat.div_one _)
+/-!
+# `bmod` ("balanced" mod)
 
-@[simp] theorem emod_one (a : Int) : a % 1 = 0 := by
-  simp [emod_def, Int.one_mul, Int.sub_self]
+We use balanced mod in the omega algorithm,
+to make ±1 coefficients appear in equations without them.
+-/
 
-@[simp] protected theorem ediv_self {a : Int} (H : a ≠ 0) : a / a = 1 := by
-  have := Int.mul_ediv_cancel 1 H; rwa [Int.one_mul] at this
-
-@[simp]
-theorem Int.emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
-  if h : y = 0 then
-    simp [h]
+/--
+Balanced mod, taking values in the range [- m/2, (m - 1)/2].
+-/
+def bmod (x : Int) (m : Nat) : Int :=
+  let r := x % m
+  if r < (m + 1) / 2 then
+    r
   else
-    simp only [Int.emod_def, Int.sub_ediv_of_dvd, Int.dvd_refl, Int.ediv_self h, Int.mul_sub]
-    simp [Int.mul_one, Int.sub_sub, Int.add_comm y]
-
-/-! bmod -/
+    r - m
 
 @[simp] theorem bmod_emod : bmod x m % m = x % m := by
   dsimp [bmod]
   split <;> simp [Int.sub_emod]
-
-@[simp]
-theorem emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n) n = Int.bmod x n := by
-  simp [bmod, Int.emod_emod]
-
-theorem bmod_def (x : Int) (m : Nat) : bmod x m =
-  if (x % m) < (m + 1) / 2 then
-    x % m
-  else
-    (x % m) - m :=
-  rfl
-
-theorem bmod_pos (x : Int) (m : Nat) (p : x % m < (m + 1) / 2) : bmod x m = x % m := by
-  simp [bmod_def, p]
-
-theorem bmod_neg (x : Int) (m : Nat) (p : x % m ≥ (m + 1) / 2) : bmod x m = (x % m) - m := by
-  simp [bmod_def, Int.not_lt.mpr p]
-
-@[simp]
-theorem bmod_one_is_zero (x : Int) : Int.bmod x 1 = 0 := by
-  simp [Int.bmod]
-
-@[simp]
-theorem bmod_add_cancel (x : Int) (n : Nat) : Int.bmod (x + n) n = Int.bmod x n := by
-  simp [bmod_def]
-
-@[simp]
-theorem bmod_add_mul_cancel (x : Int) (n : Nat) (k : Int) : Int.bmod (x + n * k) n = Int.bmod x n := by
-  simp [bmod_def]
-
-@[simp]
-theorem bmod_sub_cancel (x : Int) (n : Nat) : Int.bmod (x - n) n = Int.bmod x n := by
-  simp [bmod_def]
-
-@[simp]
-theorem emod_add_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n + y) n = Int.bmod (x + y) n := by
-  simp [Int.emod_def, Int.sub_eq_add_neg]
-  rw [←Int.mul_neg, Int.add_right_comm,  Int.bmod_add_mul_cancel]
-
-@[simp]
-theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n := by
-  rw [bmod_def x n]
-  split
-  case inl p =>
-    simp
-  case inr p =>
-    rw [Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg]
-    simp
-
-@[simp]
-theorem add_bmod_bmod : Int.bmod (x + Int.bmod y n) n = Int.bmod (x + y) n := by
-  rw [Int.add_comm x, Int.bmod_add_bmod_congr, Int.add_comm y]

src/Init/Data/Int/Lemmas.lean

@@ -321,27 +321,6 @@ theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by
   · exact (Nat.add_sub_cancel_left ..).symm
   · dsimp; rw [Nat.add_assoc, Nat.sub_eq_zero_of_le (Nat.le_add_right ..)]; rfl
 
-/- ## add/sub injectivity -/
-
-@[simp]
-protected theorem add_right_inj (i j k : Int) : (i + k = j + k) ↔ i = j := by
-  apply Iff.intro
-  · intro p
-    rw [←Int.add_sub_cancel i k, ←Int.add_sub_cancel j k, p]
-  · exact congrArg (· + k)
-
-@[simp]
-protected theorem add_left_inj (i j k : Int) : (k + i = k + j) ↔ i = j := by
-  simp [Int.add_comm k]
-
-@[simp]
-protected theorem sub_left_inj (i j k : Int) : (k - i = k - j) ↔ i = j := by
-  simp [Int.sub_eq_add_neg, Int.neg_inj]
-
-@[simp]
-protected theorem sub_right_inj (i j k : Int) : (i - k = j - k) ↔ i = j := by
-  simp [Int.sub_eq_add_neg]
-
 /- ## Ring properties -/
 
 @[simp] theorem ofNat_mul_negSucc (m n : Nat) : (m : Int) * -[n+1] = -↑(m * succ n) := rfl
@@ -499,33 +478,10 @@ theorem eq_one_of_mul_eq_self_left {a b : Int} (Hpos : a ≠ 0) (H : b * a = a)
 theorem eq_one_of_mul_eq_self_right {a b : Int} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 :=
   Int.eq_of_mul_eq_mul_left Hpos <| by rw [Int.mul_one, H]
 
-/-! # pow -/
-
-protected theorem pow_zero (b : Int) : b^0 = 1 := rfl
-
 protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
 protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
   rw [Int.mul_comm, Int.pow_succ]
 
-theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
-  | 0      => Nat.le_refl _
-  | succ i => Nat.mul_le_mul (pow_le_pow_of_le_left h i) h
-
-theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
-  | 0,      h =>
-    have : i = 0 := eq_zero_of_le_zero h
-    this.symm ▸ Nat.le_refl _
-  | succ j, h =>
-    match le_or_eq_of_le_succ h with
-    | Or.inl h => show n^i ≤ n^j * n from
-      have : n^i * 1 ≤ n^j * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) hx
-      Nat.mul_one (n^i) ▸ this
-    | Or.inr h =>
-      h.symm ▸ Nat.le_refl _
-
-theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
-  pow_le_pow_of_le_right h (Nat.zero_le _)
-
 /-! NatCast lemmas -/
 
 /-!
@@ -545,10 +501,4 @@ theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl
 @[simp] theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by
   simp
 
-theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
-  match n with
-  | 0 => rfl
-  | n + 1 =>
-    simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]
-
 end Int

src/Init/Data/Int/Order.lean

@@ -192,11 +192,6 @@ protected theorem min_le_right (a b : Int) : min a b ≤ b := by rw [Int.min_def
 
 protected theorem min_le_left (a b : Int) : min a b ≤ a := Int.min_comm .. ▸ Int.min_le_right ..
 
-protected theorem min_eq_left {a b : Int} (h : a ≤ b) : min a b = a := by simp [Int.min_def, h]
-
-protected theorem min_eq_right {a b : Int} (h : b ≤ a) : min a b = b := by
-  rw [Int.min_comm a b]; exact Int.min_eq_left h
-
 protected theorem le_min {a b c : Int} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c :=
   ⟨fun h => ⟨Int.le_trans h (Int.min_le_left ..), Int.le_trans h (Int.min_le_right ..)⟩,
    fun ⟨h₁, h₂⟩ => by rw [Int.min_def]; split <;> assumption⟩
@@ -215,12 +210,6 @@ protected theorem max_le {a b c : Int} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c :
   ⟨fun h => ⟨Int.le_trans (Int.le_max_left ..) h, Int.le_trans (Int.le_max_right ..) h⟩,
    fun ⟨h₁, h₂⟩ => by rw [Int.max_def]; split <;> assumption⟩
 
-protected theorem max_eq_right {a b : Int} (h : a ≤ b) : max a b = b := by
-  simp [Int.max_def, h, Int.not_lt.2 h]
-
-protected theorem max_eq_left {a b : Int} (h : b ≤ a) : max a b = a := by
-  rw [← Int.max_comm b a]; exact Int.max_eq_right h
-
 theorem eq_natAbs_of_zero_le {a : Int} (h : 0 ≤ a) : a = natAbs a := by
   let ⟨n, e⟩ := eq_ofNat_of_zero_le h
   rw [e]; rfl
@@ -447,54 +436,3 @@ theorem natAbs_of_nonneg {a : Int} (H : 0 ≤ a) : (natAbs a : Int) = a :=
 
 theorem ofNat_natAbs_of_nonpos {a : Int} (H : a ≤ 0) : (natAbs a : Int) = -a := by
   rw [← natAbs_neg, natAbs_of_nonneg (Int.neg_nonneg_of_nonpos H)]
-
-/-! ### toNat -/
-
-theorem toNat_eq_max : ∀ a : Int, (toNat a : Int) = max a 0
-  | (n : Nat) => (Int.max_eq_left (ofNat_zero_le n)).symm
-  | -[n+1] => (Int.max_eq_right (Int.le_of_lt (negSucc_lt_zero n))).symm
-
-@[simp] theorem toNat_zero : (0 : Int).toNat = 0 := rfl
-
-@[simp] theorem toNat_one : (1 : Int).toNat = 1 := rfl
-
-@[simp] theorem toNat_of_nonneg {a : Int} (h : 0 ≤ a) : (toNat a : Int) = a := by
-  rw [toNat_eq_max, Int.max_eq_left h]
-
-@[simp] theorem toNat_ofNat (n : Nat) : toNat ↑n = n := rfl
-
-@[simp] theorem toNat_ofNat_add_one {n : Nat} : ((n : Int) + 1).toNat = n + 1 := rfl
-
-theorem self_le_toNat (a : Int) : a ≤ toNat a := by rw [toNat_eq_max]; apply Int.le_max_left
-
-@[simp] theorem le_toNat {n : Nat} {z : Int} (h : 0 ≤ z) : n ≤ z.toNat ↔ (n : Int) ≤ z := by
-  rw [← Int.ofNat_le, Int.toNat_of_nonneg h]
-
-@[simp] theorem toNat_lt {n : Nat} {z : Int} (h : 0 ≤ z) : z.toNat < n ↔ z < (n : Int) := by
-  rw [← Int.not_le, ← Nat.not_le, Int.le_toNat h]
-
-theorem toNat_add {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a + b).toNat = a.toNat + b.toNat :=
-  match a, b, eq_ofNat_of_zero_le ha, eq_ofNat_of_zero_le hb with
-  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => rfl
-
-theorem toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + n).toNat = a.toNat + n :=
-  match a, eq_ofNat_of_zero_le ha with | _, ⟨_, rfl⟩ => rfl
-
-@[simp] theorem pred_toNat : ∀ i : Int, (i - 1).toNat = i.toNat - 1
-  | 0 => rfl
-  | (n+1:Nat) => by simp [ofNat_add]
-  | -[n+1] => rfl
-
-@[simp] theorem toNat_sub_toNat_neg : ∀ n : Int, ↑n.toNat - ↑(-n).toNat = n
-  | 0 => rfl
-  | (_+1:Nat) => Int.sub_zero _
-  | -[_+1] => Int.zero_sub _
-
-@[simp] theorem toNat_add_toNat_neg_eq_natAbs : ∀ n : Int, n.toNat + (-n).toNat = n.natAbs
-  | 0 => rfl
-  | (_+1:Nat) => Nat.add_zero _
-  | -[_+1] => Nat.zero_add _
-
-@[simp] theorem toNat_neg_nat : ∀ n : Nat, (-(n : Int)).toNat = 0
-  | 0 => rfl
-  | _+1 => rfl

src/Init/Data/List/Basic.lean

@@ -727,9 +727,9 @@ inductive lt [LT α] : List α → List α → Prop where
 instance [LT α] : LT (List α) := ⟨List.lt⟩
 
 instance hasDecidableLt [LT α] [h : DecidableRel (α:=α) (·<·)] : (l₁ l₂ : List α) → Decidable (l₁ < l₂)
-  | [],    []    => isFalse nofun
+  | [],    []    => isFalse (fun h => nomatch h)
   | [],    _::_  => isTrue (List.lt.nil _ _)
-  | _::_, []     => isFalse nofun
+  | _::_, []     => isFalse (fun h => nomatch h)
   | a::as, b::bs =>
     match h a b with
     | isTrue h₁  => isTrue (List.lt.head _ _ h₁)

src/Init/Data/List/BasicAux.lean

@@ -227,23 +227,4 @@ where
     else
       go xs acc₁ (acc₂.push x)
 
-/--
-Given a function `f : α → β ⊕ γ`, `partitionMap f l` maps the list by `f`
-whilst partitioning the result it into a pair of lists, `List β × List γ`,
-partitioning the `.inl _` into the left list, and the `.inr _` into the right List.
-```
-partitionMap (id : Nat ⊕ Nat → Nat ⊕ Nat) [inl 0, inr 1, inl 2] = ([0, 2], [1])
-```
--/
-@[inline] def partitionMap (f : α → β ⊕ γ) (l : List α) : List β × List γ := go l #[] #[] where
-  /-- Auxiliary for `partitionMap`:
-  `partitionMap.go f l acc₁ acc₂ = (acc₁.toList ++ left, acc₂.toList ++ right)`
-  if `partitionMap f l = (left, right)`. -/
-  @[specialize] go : List α → Array β → Array γ → List β × List γ
-  | [], acc₁, acc₂ => (acc₁.toList, acc₂.toList)
-  | x :: xs, acc₁, acc₂ =>
-    match f x with
-    | .inl a => go xs (acc₁.push a) acc₂
-    | .inr b => go xs acc₁ (acc₂.push b)
-
 end List

src/Init/Data/List/Lemmas.lean

@@ -665,44 +665,3 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·
     exact congrArg some <| anti.1
       ((le_minimum?_iff le_min_iff (xs := x::xs) rfl _).1 (le_refl _) _ h₁)
       (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl))
-
-@[simp] theorem get_cons_succ {as : List α} {h : i + 1 < (a :: as).length} :
-  (a :: as).get ⟨i+1, h⟩ = as.get ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl
-
-@[simp] theorem get_cons_succ' {as : List α} {i : Fin as.length} :
-  (a :: as).get i.succ = as.get i := rfl
-
-@[simp] theorem set_nil (n : Nat) (a : α) : [].set n a = [] := rfl
-
-@[simp] theorem set_zero (x : α) (xs : List α) (a : α) :
-  (x :: xs).set 0 a = a :: xs := rfl
-
-@[simp] theorem set_succ (x : α) (xs : List α) (n : Nat) (a : α) :
-  (x :: xs).set n.succ a = x :: xs.set n a := rfl
-
-@[simp] theorem get_set_eq (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) :
-    (l.set i a).get ⟨i, h⟩ = a :=
-  match l, i with
-  | [], _ => by
-    simp at h
-    contradiction
-  | _ :: _, 0 => by
-    simp
-  | _ :: l, i + 1 => by
-    simp [get_set_eq l]
-
-@[simp] theorem get_set_ne (l : List α) {i j : Nat} (h : i ≠ j) (a : α)
-    (hj : j < (l.set i a).length) :
-    (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ :=
-  match l, i, j with
-  | [], _, _ => by
-    simp
-  | _ :: _, 0, 0 => by
-    contradiction
-  | _ :: _, 0, _ + 1 => by
-    simp
-  | _ :: _, _ + 1, 0 => by
-    simp
-  | _ :: l, i + 1, j + 1 => by
-    have g : i ≠ j := h ∘ congrArg (· + 1)
-    simp [get_set_ne l g]

src/Init/Data/Nat/Basic.lean

@@ -189,7 +189,7 @@ protected theorem mul_comm : ∀ (n m : Nat), n * m = m * n
   Nat.mul_comm n 1 ▸ Nat.mul_one n
 
 protected theorem left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := by
-  induction n with
+  induction n generalizing m k with
   | zero      => repeat rw [Nat.zero_mul]
   | succ n ih => simp [succ_mul, ih]; rw [Nat.add_assoc, Nat.add_assoc (n*m)]; apply congrArg; apply Nat.add_left_comm
 
@@ -503,10 +503,10 @@ theorem eq_of_mul_eq_mul_right {n m k : Nat} (hm : 0 < m) (h : n * m = k * m) :
 
 /-! # power -/
 
-protected theorem pow_succ (n m : Nat) : n^(succ m) = n^m * n :=
+theorem pow_succ (n m : Nat) : n^(succ m) = n^m * n :=
   rfl
 
-protected theorem pow_zero (n : Nat) : n^0 = 1 := rfl
+theorem pow_zero (n : Nat) : n^0 = 1 := rfl
 
 theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
   | 0      => Nat.le_refl _

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -239,7 +239,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
     rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
     exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
   | d+1 =>
-    simp [Nat.pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
+    simp [pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
 
 @[simp] theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
@@ -287,7 +287,7 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
     simp only [testBit_succ]
     match n with
     | 0 =>
-      simp only [Nat.pow_zero, succ_sub_succ_eq_sub, Nat.zero_sub, Nat.zero_div, zero_testBit]
+      simp only [pow_zero, succ_sub_succ_eq_sub, Nat.zero_sub, Nat.zero_div, zero_testBit]
       rw [decide_eq_false] <;> simp
     | n+1 =>
       rw [Nat.two_pow_succ_sub_succ_div_two, ih]
@@ -352,7 +352,7 @@ private theorem eq_0_of_lt (x : Nat) : x < 2^ 0 ↔ x = 0 := eq_0_of_lt_one x
 private theorem zero_lt_pow (n : Nat) : 0 < 2^n := by
   induction n
   case zero => simp [eq_0_of_lt]
-  case succ n hyp => simpa [Nat.pow_succ]
+  case succ n hyp => simpa [pow_succ]
 
 private theorem div_two_le_of_lt_two {m n : Nat} (p : m < 2 ^ succ n) : m / 2 < 2^n := by
   simp [div_lt_iff_lt_mul Nat.zero_lt_two]
@@ -377,7 +377,7 @@ theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x
       simp only [x_zero, y_zero, if_neg]
       have hyp1 := hyp (div_two_le_of_lt_two left) (div_two_le_of_lt_two right)
       by_cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true <;>
-        simp [p, Nat.pow_succ, mul_succ, Nat.add_assoc]
+        simp [p, pow_succ, mul_succ, Nat.add_assoc]
       case pos =>
         apply lt_of_succ_le
         simp only [← Nat.succ_add]

src/Init/Data/Nat/Lemmas.lean

@@ -742,7 +742,7 @@ theorem shiftLeft_eq (a b : Nat) : a <<< b = a * 2 ^ b :=
   match b with
   | 0 => (Nat.mul_one _).symm
   | b+1 => (shiftLeft_eq _ b).trans <| by
-    simp [Nat.pow_succ, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]
+    simp [pow_succ, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]
 
 theorem one_shiftLeft (n : Nat) : 1 <<< n = 2 ^ n := by rw [shiftLeft_eq, Nat.one_mul]
 

src/Init/Meta.lean

@@ -1362,19 +1362,6 @@ structure OmegaConfig where
 
 end Omega
 
-namespace CheckTactic
-
-/--
-Type used to lift an arbitrary value into a type parameter so it can
-appear in a proof goal.
-
-It is used by the #check_tactic command.
--/
-inductive CheckGoalType {α : Sort u} : (val : α) → Prop where
-| intro : (val : α) → CheckGoalType val
-
-end CheckTactic
-
 end Meta
 
 namespace Parser

src/Init/Notation.lean

@@ -503,25 +503,6 @@ applications of this function as `↑` when printing expressions.
 -/
 syntax (name := Attr.coe) "coe" : attr
 
-/--
-This attribute marks a code action, which is used to suggest new tactics or replace existing ones.
-
-* `@[command_code_action kind]`: This is a code action which applies to applications of the command
-  `kind` (a command syntax kind), which can replace the command or insert things before or after it.
-
-* `@[command_code_action kind₁ kind₂]`: shorthand for
-  `@[command_code_action kind₁, command_code_action kind₂]`.
-
-* `@[command_code_action]`: This is a command code action that applies to all commands.
-  Use sparingly.
--/
-syntax (name := command_code_action) "command_code_action" (ppSpace ident)* : attr
-
-/--
-Builtin command code action. See `command_code_action`.
--/
-syntax (name := builtin_command_code_action) "builtin_command_code_action" (ppSpace ident)* : attr
-
 /--
 When `parent_dir` contains the current Lean file, `include_str "path" / "to" / "file"` becomes
 a string literal with the contents of the file at `"parent_dir" / "path" / "to" / "file"`. If this
@@ -551,92 +532,3 @@ except that it doesn't print an empty diagnostic.
 (This is effectively a synonym for `run_elab`.)
 -/
 syntax (name := runMeta) "run_meta " doSeq : command
-
-/-- Element that can be part of a `#guard_msgs` specification. -/
-syntax guardMsgsSpecElt := &"drop"? (&"info" <|> &"warning" <|> &"error" <|> &"all")
-
-/-- Specification for `#guard_msgs` command. -/
-syntax guardMsgsSpec := "(" guardMsgsSpecElt,* ")"
-
-/--
-`#guard_msgs` captures the messages generated by another command and checks that they
-match the contents of the docstring attached to the `#guard_msgs` command.
-
-Basic example:
-```lean
-/--
-error: unknown identifier 'x'
--/
-#guard_msgs in
-example : α := x
-```
-This checks that there is such an error and then consumes the message entirely.
-
-By default, the command intercepts all messages, but there is a way to specify which types
-of messages to consider. For example, we can select only warnings:
-```lean
-/--
-warning: declaration uses 'sorry'
--/
-#guard_msgs(warning) in
-example : α := sorry
-```
-or only errors
-```lean
-#guard_msgs(error) in
-example : α := sorry
-```
-In this last example, since the message is not intercepted there is a warning on `sorry`.
-We can drop the warning completely with
-```lean
-#guard_msgs(error, drop warning) in
-example : α := sorry
-```
-
-Syntax description:
-```
-#guard_msgs (drop? info|warning|error|all,*)? in cmd
-```
-
-If there is no specification, `#guard_msgs` intercepts all messages.
-Otherwise, if there is one, the specification is considered in left-to-right order, and the first
-that applies chooses the outcome of the message:
-- `info`, `warning`, `error`: intercept a message with the given severity level.
-- `all`: intercept any message (so `#guard_msgs in cmd` and `#guard_msgs (all) in cmd`
-  are equivalent).
-- `drop info`, `drop warning`, `drop error`: intercept a message with the given severity
-  level and then drop it. These messages are not checked.
-- `drop all`: intercept a message and drop it.
-
-For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and then drop
-everything else.
--/
-syntax (name := guardMsgsCmd)
-  (docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
-
-namespace Parser
-
-/--
-`#check_tactic t ~> r by commands` runs the tactic sequence `commands`
-on a goal with `t` and sees if the resulting expression has reduced it
-to `r`.
--/
-syntax (name := checkTactic) "#check_tactic " term "~>" term "by" tactic : command
-
-/--
-`#check_tactic_failure t by tac` runs the tactic `tac`
-on a goal with `t` and verifies it fails.
--/
-syntax  (name := checkTacticFailure) "#check_tactic_failure " term "by" tactic : command
-
-/--
-`#check_simp t ~> r` checks `simp` reduces `t` to `r`.
--/
-syntax (name := checkSimp) "#check_simp " term "~>" term : command
-
-/--
-`#check_simp t !~>` checks `simp` fails on reducing `t`.
--/
-syntax (name := checkSimpFailure) "#check_simp " term "!~>" : command
-
-end Parser

src/Init/NotationExtra.lean

@@ -170,6 +170,19 @@ See [Theorem Proving in Lean 4][tpil4] for more information.
 -/
 syntax (name := calcTactic) "calc" calcSteps : tactic
 
+/--
+Denotes a term that was omitted by the pretty printer.
+This is only used for pretty printing, and it cannot be elaborated.
+The presence of `⋯` is controlled by the `pp.deepTerms` and `pp.proofs` options.
+-/
+syntax "⋯" : term
+
+macro_rules | `(⋯) => Macro.throwError "\
+  Error: The '⋯' token is used by the pretty printer to indicate omitted terms, \
+  and it cannot be elaborated.\
+  \n\nIts presence in pretty printing output is controlled by the 'pp.deepTerms' and `pp.proofs` options. \
+  These options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`."
+
 @[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
 
@@ -453,19 +466,3 @@ syntax "{" term,+ "}" : term
 macro_rules
   | `({$x:term}) => `(singleton $x)
   | `({$x:term, $xs:term,*}) => `(insert $x {$xs:term,*})
-
-namespace Lean
-
-/-- Unexpander for the `{ x }` notation. -/
-@[app_unexpander singleton]
-def singletonUnexpander : Lean.PrettyPrinter.Unexpander
-  | `($_ $a) => `({ $a:term })
-  | _ => throw ()
-
-/-- Unexpander for the `{ x, y, ... }` notation. -/
-@[app_unexpander insert]
-def insertUnexpander : Lean.PrettyPrinter.Unexpander
-  | `($_ $a { $ts:term,* }) => `({$a:term, $ts,*})
-  | _ => throw ()
-
-end Lean

src/Init/Omega/Coeffs.lean

@@ -20,7 +20,7 @@ There is an equivalent file setting up `Coeffs` as a type synonym for `AssocList
 currently in a private branch.
 Not all the theorems about the algebraic operations on that representation have been proved yet.
 When they are ready, we can replace the implementation in `omega` simply by importing
-`Init.Omega.IntDict` instead of `Init.Omega.IntList`.
+`Std.Tactic.Omega.Coeffs.IntDict` instead of `Std.Tactic.Omega.Coeffs.IntList`.
 
 For small problems, the sparse representation is actually slightly slower,
 so it is not urgent to make this replacement.

src/Init/Omega/Int.lean

@@ -12,7 +12,7 @@ import Init.Data.Nat.Lemmas
 # Lemmas about `Nat`, `Int`, and `Fin` needed internally by `omega`.
 
 These statements are useful for constructing proof expressions,
-but unlikely to be widely useful, so are inside the `Lean.Omega` namespace.
+but unlikely to be widely useful, so are inside the `Std.Tactic.Omega` namespace.
 
 If you do find a use for them, please move them into the appropriate file and namespace!
 -/

src/Init/Omega/Logic.lean

@@ -9,7 +9,7 @@ import Init.PropLemmas
 # Specializations of basic logic lemmas
 
 These are useful for `omega` while constructing proofs, but not considered generally useful
-so are hidden in the `Lean.Omega` namespace.
+so are hidden in the `Std.Tactic.Omega` namespace.
 
 If you find yourself needing them elsewhere, please move them first to another file.
 -/

src/Init/Prelude.lean

@@ -947,8 +947,7 @@ return `t` or `e` depending on whether `c` is true or false. The explicit argume
 determines how to evaluate `c` to true or false. Write `if h : c then t else e`
 instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
 that `c` is true/false.
--/
-/-
+
 Because Lean uses a strict (call-by-value) evaluation strategy, the signature of this
 function is problematic in that it would require `t` and `e` to be evaluated before
 calling the `ite` function, which would cause both sides of the `if` to be evaluated.
@@ -1635,8 +1634,8 @@ instance : LT Nat where
   lt := Nat.lt
 
 theorem Nat.not_succ_le_zero : ∀ (n : Nat), LE.le (succ n) 0 → False
-  | 0      => nofun
-  | succ _ => nofun
+  | 0,      h => nomatch h
+  | succ _, h => nomatch h
 
 theorem Nat.not_lt_zero (n : Nat) : Not (LT.lt n 0) :=
   not_succ_le_zero n

src/Init/Tactics.lean

@@ -1287,45 +1287,6 @@ a lemma from the list until it gets stuck.
 syntax (name := applyRules) "apply_rules" (config)? (&" only")? (args)? (using_)? : tactic
 end SolveByElim
 
-/--
-Searches environment for definitions or theorems that can solve the goal using `exact`
-with conditions resolved by `solve_by_elim`.
-
-The optional `using` clause provides identifiers in the local context that must be
-used by `exact?` when closing the goal.  This is most useful if there are multiple
-ways to resolve the goal, and one wants to guide which lemma is used.
--/
-syntax (name := exact?) "exact?" (" using " (colGt ident),+)? : tactic
-
-/--
-Searches environment for definitions or theorems that can refine the goal using `apply`
-with conditions resolved when possible with `solve_by_elim`.
-
-The optional `using` clause provides identifiers in the local context that must be
-used when closing the goal.
--/
-syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
-
-/--
-`show_term tac` runs `tac`, then prints the generated term in the form
-"exact X Y Z" or "refine X ?_ Z" if there are remaining subgoals.
-
-(For some tactics, the printed term will not be human readable.)
--/
-syntax (name := showTerm) "show_term " tacticSeq : tactic
-
-/--
-`show_term e` elaborates `e`, then prints the generated term.
--/
-macro (name := showTermElab) tk:"show_term " t:term : term =>
-  `(term| no_implicit_lambda% (show_term_elab%$tk $t))
-
-/--
-The command `by?` will print a suggestion for replacing the proof block with a proof term
-using `show_term`.
--/
-macro (name := by?) tk:"by?" t:tacticSeq : term => `(show_term%$tk by%$tk $t)
-
 end Tactic
 
 namespace Attr
@@ -1445,14 +1406,13 @@ macro_rules | `(‹$type›) => `((by assumption : $type))
 by the notation `arr[i]` to prove any side conditions that arise when
 constructing the term (e.g. the index is in bounds of the array).
 The default behavior is to just try `trivial` (which handles the case
-where `i < arr.size` is in the context) and `simp_arith` and `omega`
+where `i < arr.size` is in the context) and `simp_arith`
 (for doing linear arithmetic in the index).
 -/
 syntax "get_elem_tactic_trivial" : tactic
 
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
+macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
 
 /--
 `get_elem_tactic` is the tactic automatically called by the notation `arr[i]`
@@ -1463,24 +1423,6 @@ users are encouraged to extend `get_elem_tactic_trivial` instead of this tactic.
 -/
 macro "get_elem_tactic" : tactic =>
   `(tactic| first
-      /-
-      Recall that `macro_rules` are tried in reverse order.
-      We want `assumption` to be tried first.
-      This is important for theorems such as
-      ```
-      [simp] theorem getElem_pop (a : Array α) (i : Nat) (hi : i < a.pop.size) :
-      a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop ▸ hi) (Nat.sub_le _ _)) :=
-      ```
-      There is a proof embedded in the right-hand-side, and we want it to be just `hi`.
-      If `omega` is used to "fill" this proof, we will have a more complex proof term that
-      cannot be inferred by unification.
-      We hardcoded `assumption` here to ensure users cannot accidentaly break this IF
-      they add new `macro_rules` for `get_elem_tactic_trivial`.
-
-      TODO: Implement priorities for `macro_rules`.
-      TODO: Ensure we have a **high-priority** macro_rules for `get_elem_tactic_trivial` which is just `assumption`.
-      -/
-    | assumption
     | get_elem_tactic_trivial
     | fail "failed to prove index is valid, possible solutions:
   - Use `have`-expressions to prove the index is valid
@@ -1496,9 +1438,3 @@ macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
 @[inherit_doc getElem]
 syntax term noWs "[" withoutPosition(term) "]'" term:max : term
 macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
-
-/--
-Searches environment for definitions or theorems that can be substituted in
-for `exact?% to solve the goal.
- -/
-syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term

src/Init/WFTactics.lean

@@ -22,8 +22,7 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)
 -/
 syntax "decreasing_trivial" : tactic
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })); done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ProjFns
-import Lean.Meta.CtorRecognizer
 import Lean.Compiler.BorrowedAnnotation
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.Bind
@@ -620,7 +619,7 @@ where
       let rhs ← liftMetaM do Meta.whnf args[inductVal.numParams + inductVal.numIndices + 2]!
       let lhs := lhs.toCtorIfLit
       let rhs := rhs.toCtorIfLit
-      match (← liftMetaM <| Meta.isConstructorApp? lhs), (← liftMetaM <| Meta.isConstructorApp? rhs) with
+      match lhs.isConstructorApp? (← getEnv), rhs.isConstructorApp? (← getEnv) with
       | some lhsCtorVal, some rhsCtorVal =>
         if lhsCtorVal.name == rhsCtorVal.name then
           etaIfUnderApplied e (arity+1) do

src/Lean/Data/Json/Basic.lean

@@ -8,7 +8,6 @@ prelude
 import Init.Data.List.Control
 import Init.Data.Range
 import Init.Data.OfScientific
-import Init.Data.Hashable
 import Lean.Data.RBMap
 namespace Lean
 
@@ -16,7 +15,7 @@ namespace Lean
 structure JsonNumber where
   mantissa : Int
   exponent : Nat
-  deriving DecidableEq, Hashable
+  deriving DecidableEq
 
 namespace JsonNumber
 
@@ -206,19 +205,6 @@ private partial def beq' : Json → Json → Bool
 instance : BEq Json where
   beq := beq'
 
-private partial def hash' : Json → UInt64
-  | null   => 11
-  | bool b => mixHash 13 <| hash b
-  | num n  => mixHash 17 <| hash n
-  | str s  => mixHash 19 <| hash s
-  | arr elems =>
-    mixHash 23 <| elems.foldl (init := 7) fun r a => mixHash r (hash' a)
-  | obj kvPairs =>
-    mixHash 29 <| kvPairs.fold (init := 7) fun r k v => mixHash r <| mixHash (hash k) (hash' v)
-
-instance : Hashable Json where
-  hash := hash'
-
 -- HACK(Marc): temporary ugliness until we can use RBMap for JSON objects
 def mkObj (o : List (String × Json)) : Json :=
   obj <| Id.run do

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -47,19 +47,19 @@ structure CompletionItem where
   documentation? : Option MarkupContent := none
   kind?          : Option CompletionItemKind := none
   textEdit?      : Option InsertReplaceEdit := none
-  sortText?      : Option String := none
-  data?          : Option Json := none
   /-
   tags? : CompletionItemTag[]
   deprecated? : boolean
   preselect? : boolean
+  sortText? : string
   filterText? : string
   insertText? : string
   insertTextFormat? : InsertTextFormat
   insertTextMode? : InsertTextMode
   additionalTextEdits? : TextEdit[]
   commitCharacters? : string[]
-  command? : Command -/
+  command? : Command
+  data? : any -/
   deriving FromJson, ToJson, Inhabited
 
 structure CompletionList where
@@ -274,7 +274,7 @@ structure CallHierarchyItem where
   uri            : DocumentUri
   range          : Range
   selectionRange : Range
-  data?          : Option Json := none
+  -- data? : Option unknown
   deriving FromJson, ToJson, BEq, Hashable, Inhabited
 
 structure CallHierarchyIncomingCallsParams where

src/Lean/Data/Lsp/Utf16.lean

@@ -86,10 +86,6 @@ def leanPosToLspPos (text : FileMap) : Lean.Position → Lsp.Position
 def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
   text.leanPosToLspPos (text.toPosition pos)
 
-/-- Gets the LSP range from a `String.Range`. -/
-def utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
-  { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
-
 end FileMap
 end Lean
 

src/Lean/Data/PersistentHashMap.lean

@@ -84,14 +84,14 @@ partial def insertAtCollisionNodeAux [BEq α] : CollisionNode α β → Nat →
       else insertAtCollisionNodeAux n (i+1) k v
     else
       ⟨Node.collision (keys.push k) (vals.push v) (size_push heq k v), IsCollisionNode.mk _ _ _⟩
-  | ⟨Node.entries _, h⟩, _, _, _ => nomatch h
+  | ⟨Node.entries _, h⟩, _, _, _ => False.elim (nomatch h)
 
 def insertAtCollisionNode [BEq α] : CollisionNode α β → α → β → CollisionNode α β :=
   fun n k v => insertAtCollisionNodeAux n 0 k v
 
 def getCollisionNodeSize : CollisionNode α β → Nat
   | ⟨Node.collision keys _ _, _⟩ => keys.size
-  | ⟨Node.entries _, h⟩          => nomatch h
+  | ⟨Node.entries _, h⟩          => False.elim (nomatch h)
 
 def mkCollisionNode (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) : Node α β :=
   let ks : Array α := Array.mkEmpty maxCollisions
@@ -105,7 +105,7 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize
     let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v
     if depth >= maxDepth || getCollisionNodeSize newNode < maxCollisions then newNode.val
     else match newNode with
-      | ⟨Node.entries _, h⟩ => nomatch h
+      | ⟨Node.entries _, h⟩ => False.elim (nomatch h)
       | ⟨Node.collision keys vals heq, _⟩ =>
         let rec traverse (i : Nat) (entries : Node α β) : Node α β :=
           if h : i < keys.size then

src/Lean/Elab.lean

@@ -47,6 +47,3 @@ import Lean.Elab.Eval
 import Lean.Elab.Calc
 import Lean.Elab.InheritDoc
 import Lean.Elab.ParseImportsFast
-import Lean.Elab.GuardMsgs
-import Lean.Elab.CheckTactic
-import Lean.Elab.MatchExpr

src/Lean/Elab/BuiltinCommand.lean

@@ -534,10 +534,10 @@ open Meta
 def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
   | `(#check%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_check do
     -- show signature for `#check id`/`#check @id`
-    if let `($id:ident) := term then
+    if let `($_:ident) := term then
       try
         for c in (← resolveGlobalConstWithInfos term) do
-          addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
+          addCompletionInfo <| .id term c (danglingDot := false) {} none
           logInfoAt tk <| .ofPPFormat { pp := fun
             | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
             | none     => return f!"{c}"  -- should never happen

src/Lean/Elab/BuiltinTerm.lean

@@ -99,14 +99,6 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
         else
           throwError "synthetic hole has already been defined with an incompatible local context"
 
-@[builtin_term_elab Lean.Parser.Term.omission] def elabOmission : TermElab := fun stx expectedType? => do
-  logWarning m!"\
-    The '⋯' token is used by the pretty printer to indicate omitted terms, and it should not be used directly. \
-    It logs this warning and then elaborates like `_`.\
-    \n\nThe presence of `⋯` in pretty printing output is controlled by the 'pp.deepTerms' and `pp.proofs` options. \
-    These options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`."
-  elabHole stx expectedType?
-
 @[builtin_term_elab «letMVar»] def elabLetMVar : TermElab := fun stx expectedType? => do
   match stx with
   | `(let_mvar% ? $n := $e; $b) =>
@@ -166,10 +158,7 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
 @[builtin_term_elab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
   elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
 
-@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun stx expectedType? => do
-  if stx[0].getAtomVal == "." then
-    -- Users may input bad cdots because they are trying to auto-complete them using the expected type
-    addCompletionInfo <| CompletionInfo.dotId stx .anonymous (← getLCtx) expectedType?
+@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun _ _ =>
   throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)"
 
 @[builtin_term_elab str] def elabStrLit : TermElab := fun stx _ => do

src/Lean/Elab/CheckTactic.lean

@@ -1,95 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joe Hendrix
--/
-prelude
-import Lean.Elab.Tactic.ElabTerm
-import Lean.Elab.Command
-import Lean.Elab.Tactic.Meta
-
-/-!
-Commands to validate tactic results.
--/
-
-namespace Lean.Elab.CheckTactic
-
-open Lean.Meta CheckTactic
-open Lean.Elab.Tactic
-open Lean.Elab.Command
-
-private def matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level) := do
-  let u ← mkFreshLevelMVar
-  let type ← mkFreshExprMVar (some (.sort u))
-  let val  ← mkFreshExprMVar (some type)
-  let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val]
-  if !(← isDefEq goalType extType) then
-    throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}"
-  pure (val, type, u)
-
-@[builtin_command_elab Lean.Parser.checkTactic]
-def elabCheckTactic : CommandElab := fun stx => do
-  let `(#check_tactic $t ~> $result by $tac) := stx | throwUnsupportedSyntax
-  withoutModifyingEnv $ do
-    runTermElabM $ fun _vars => do
-      let u ← Lean.Elab.Term.elabTerm t none
-      let type ← inferType u
-      let lvl ← mkFreshLevelMVar
-      let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type u
-      let mvar ← mkFreshExprMVar (.some checkGoalType)
-      let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
-      let expTerm ← Lean.Elab.Term.elabTerm result (.some type)
-      match goals with
-      | [] =>
-        throwErrorAt stx
-          m!"{tac} closed goal, but is expected to reduce to {indentExpr expTerm}."
-      | [next] => do
-        let (val, _, _) ← matchCheckGoalType stx (←next.getType)
-        if !(← Meta.withReducible <| isDefEq val expTerm) then
-          throwErrorAt stx
-            m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
-      | _ => do
-        throwErrorAt stx
-          m!"{tac} produced multiple goals, but is expected to reduce to {indentExpr expTerm}."
-      pure ()
-
-@[builtin_command_elab Lean.Parser.checkTacticFailure]
-def elabCheckTacticFailure : CommandElab := fun stx => do
-  let `(#check_tactic_failure $t by $tactic) := stx | throwUnsupportedSyntax
-  withoutModifyingEnv $ do
-    runTermElabM $ fun _vars => do
-      let val ← Lean.Elab.Term.elabTerm t none
-      let type ← inferType val
-      let lvl ← mkFreshLevelMVar
-      let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type val
-      let mvar ← mkFreshExprMVar (.some checkGoalType)
-      let act := Lean.Elab.runTactic mvar.mvarId! tactic.raw
-      match ← try (Term.withoutErrToSorry (some <$> act)) catch _ => pure none with
-        | none =>
-          pure ()
-        | some (gls, _) =>
-          let ppGoal (g : MVarId) := do
-                let (val, _type, _u) ← matchCheckGoalType stx (← g.getType)
-                pure m!"{indentExpr val}"
-          let msg ←
-            match gls with
-              | [] => pure m!"{tactic} expected to fail on {val}, but closed goal."
-              | [g] =>
-                pure <| m!"{tactic} expected to fail on {val}, but returned: {←ppGoal g}"
-              | gls =>
-                let app m g := do pure <| m ++ (←ppGoal g)
-                let init := m!"{tactic} expected to fail on {val}, but returned goals:"
-                gls.foldlM (init := init) app
-          throwErrorAt stx msg
-
-@[builtin_macro Lean.Parser.checkSimp]
-def expandCheckSimp : Macro := fun stx => do
-  let `(#check_simp $t ~> $exp) := stx | Macro.throwUnsupported
-  `(command|#check_tactic $t ~> $exp by simp)
-
-@[builtin_macro Lean.Parser.checkSimpFailure]
-def expandCheckSimpFailure : Macro := fun stx => do
-  let `(#check_simp $t !~>) := stx | Macro.throwUnsupported
-  `(command|#check_tactic_failure $t by simp)
-
-end Lean.Elab.CheckTactic

src/Lean/Elab/Declaration.lean

@@ -347,21 +347,7 @@ def elabMutual : CommandElab := fun stx => do
   let attrs ← elabAttrs attrInsts
   let idents := stx[4].getArgs
   for ident in idents do withRef ident <| liftTermElabM do
-    /-
-    HACK to allow `attribute` command to disable builtin simprocs.
-    TODO: find a better solution. Example: have some "fake" declaration
-    for builtin simprocs.
-    -/
-    let declNames ←
-       try
-         resolveGlobalConst ident
-       catch _ =>
-         let name := ident.getId.eraseMacroScopes
-         if (← Simp.isBuiltinSimproc name) then
-           pure [name]
-         else
-           throwUnknownConstant name
-    let declName ← ensureNonAmbiguous ident declNames
+    let declName ← resolveGlobalConstNoOverloadWithInfo ident
     Term.applyAttributes declName attrs
     for attrName in toErase do
       Attribute.erase declName attrName

src/Lean/Elab/Do.lean

@@ -131,31 +131,12 @@ abbrev Var := Syntax  -- TODO: should be `Ident`
 
 /-- A `doMatch` alternative. `vars` is the array of variables declared by `patterns`. -/
 structure Alt (σ : Type) where
-  ref      : Syntax
-  vars     : Array Var
+  ref : Syntax
+  vars : Array Var
   patterns : Syntax
-  rhs      : σ
+  rhs : σ
   deriving Inhabited
 
-/-- A `doMatchExpr` alternative. -/
-structure AltExpr (σ : Type) where
-  ref     : Syntax
-  var?    : Option Var
-  funName : Syntax
-  pvars   : Array Syntax
-  rhs     : σ
-  deriving Inhabited
-
-def AltExpr.vars (alt : AltExpr σ) : Array Var := Id.run do
-  let mut vars := #[]
-  if let some var := alt.var? then
-    vars := vars.push var
-  for pvar in alt.pvars do
-    match pvar with
-    | `(_) => pure ()
-    | _ => vars := vars.push pvar
-  return vars
-
 /--
   Auxiliary datastructure for representing a `do` code block, and compiling "reassignments" (e.g., `x := x + 1`).
   We convert `Code` into a `Syntax` term representing the:
@@ -217,7 +198,6 @@ inductive Code where
   /-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/
   | ite          (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code)
   | match        (ref : Syntax) (gen : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt Code))
-  | matchExpr    (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (AltExpr Code)) (elseBranch : Code)
   | jmp          (ref : Syntax) (jpName : Name) (args : Array Syntax)
   deriving Inhabited
 
@@ -232,7 +212,6 @@ def Code.getRef? : Code → Option Syntax
   | .return ref _        => ref
   | .ite ref ..          => ref
   | .match ref ..        => ref
-  | .matchExpr ref ..    => ref
   | .jmp ref ..          => ref
 
 abbrev VarSet := RBMap Name Syntax Name.cmp
@@ -264,28 +243,19 @@ partial def CodeBlocl.toMessageData (codeBlock : CodeBlock) : MessageData :=
     | .match _ _ ds _ alts   =>
       m!"match {ds} with"
       ++ alts.foldl (init := m!"") fun acc alt => acc ++ m!"\n| {alt.patterns} => {loop alt.rhs}"
-    | .matchExpr _ meta d alts elseCode =>
-      let r := m!"match_expr {if meta then "" else "(meta := false)"} {d} with"
-      let r := r ++ alts.foldl (init := m!"") fun acc alt =>
-            let acc := acc ++ m!"\n| {if let some var := alt.var? then m!"{var}@" else ""}"
-            let acc := acc ++ m!"{alt.funName}"
-            let acc := acc ++ alt.pvars.foldl (init := m!"") fun acc pvar => acc ++ m!" {pvar}"
-            acc ++ m!" => {loop alt.rhs}"
-      r ++ m!"| _ => {loop elseCode}"
   loop codeBlock.code
 
 /-- Return true if the give code contains an exit point that satisfies `p` -/
 partial def hasExitPointPred (c : Code) (p : Code → Bool) : Bool :=
   let rec loop : Code → Bool
-    | .decl _ _ k             => loop k
-    | .reassign _ _ k         => loop k
-    | .joinpoint _ _ b k      => loop b || loop k
-    | .seq _ k                => loop k
-    | .ite _ _ _ _ t e        => loop t || loop e
-    | .match _ _ _ _ alts     => alts.any (loop ·.rhs)
-    | .matchExpr _ _ _ alts e => alts.any (loop ·.rhs) || loop e
-    | .jmp ..                 => false
-    | c                       => p c
+    | .decl _ _ k         => loop k
+    | .reassign _ _ k     => loop k
+    | .joinpoint _ _ b k  => loop b || loop k
+    | .seq _ k            => loop k
+    | .ite _ _ _ _ t e    => loop t || loop e
+    | .match _ _ _ _ alts => alts.any (loop ·.rhs)
+    | .jmp ..             => false
+    | c                   => p c
   loop c
 
 def hasExitPoint (c : Code) : Bool :=
@@ -330,18 +300,13 @@ partial def convertTerminalActionIntoJmp (code : Code) (jp : Name) (xs : Array V
     | .joinpoint n ps b k    => return .joinpoint n ps (← loop b) (← loop k)
     | .seq e k               => return .seq e (← loop k)
     | .ite ref x? h c t e    => return .ite ref x? h c (← loop t) (← loop e)
+    | .match ref g ds t alts => return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
     | .action e              => mkAuxDeclFor e fun y =>
       let ref := e
       -- We jump to `jp` with xs **and** y
       let jmpArgs := xs.push y
       return Code.jmp ref jp jmpArgs
-    | .match ref g ds t alts =>
-      return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
-    | .matchExpr ref meta d alts e => do
-      let alts ← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) }
-      let e ← loop e
-      return .matchExpr ref meta d alts e
-    | c => return c
+    | c                            => return c
   loop code
 
 structure JPDecl where
@@ -407,13 +372,14 @@ def mkJmp (ref : Syntax) (rs : VarSet) (val : Syntax) (mkJPBody : Syntax → Mac
   return Code.jmp ref jp args
 
 /-- `pullExitPointsAux rs c` auxiliary method for `pullExitPoints`, `rs` is the set of update variable in the current path.  -/
-partial def pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT (Array JPDecl) TermElabM Code := do
+partial def pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT (Array JPDecl) TermElabM Code :=
   match c with
   | .decl xs stx k         => return .decl xs stx (← pullExitPointsAux (eraseVars rs xs) k)
   | .reassign xs stx k     => return .reassign xs stx (← pullExitPointsAux (insertVars rs xs) k)
   | .joinpoint j ps b k    => return .joinpoint j ps (← pullExitPointsAux rs b) (← pullExitPointsAux rs k)
   | .seq e k               => return .seq e (← pullExitPointsAux rs k)
   | .ite ref x? o c t e    => return .ite ref x? o c (← pullExitPointsAux (eraseOptVar rs x?) t) (← pullExitPointsAux (eraseOptVar rs x?) e)
+  | .match ref g ds t alts => return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) })
   | .jmp ..                => return  c
   | .break ref             => mkSimpleJmp ref rs (.break ref)
   | .continue ref          => mkSimpleJmp ref rs (.continue ref)
@@ -423,13 +389,6 @@ partial def pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT (Array JPDecl
     mkAuxDeclFor e fun y =>
       let ref := e
       mkJmp ref rs y (fun yFresh => return .action (← ``(Pure.pure $yFresh)))
-  | .match ref g ds t alts =>
-    let alts ← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) }
-    return .match ref g ds t alts
-  | .matchExpr ref meta d alts e =>
-    let alts ← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) }
-    let e ← pullExitPointsAux rs e
-    return .matchExpr ref meta d alts e
 
 /--
 Auxiliary operation for adding new variables to the collection of updated variables in a CodeBlock.
@@ -498,14 +457,6 @@ partial def extendUpdatedVarsAux (c : Code) (ws : VarSet) : TermElabM Code :=
         pullExitPoints c
       else
         return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) })
-    | .matchExpr ref meta d alts e =>
-      if alts.any fun alt => alt.vars.any fun x => ws.contains x.getId then
-        -- If a pattern variable is shadowing a variable in ws, we `pullExitPoints`
-        pullExitPoints c
-      else
-        let alts ← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) }
-        let e ← update e
-        return .matchExpr ref meta d alts e
     | .ite ref none o c t e => return .ite ref none o c (← update t) (← update e)
     | .ite ref (some h) o cond t e =>
       if ws.contains h.getId then
@@ -619,16 +570,6 @@ def mkMatch (ref : Syntax) (genParam : Syntax) (discrs : Syntax) (optMotive : Sy
     return { ref := alt.ref, vars := alt.vars, patterns := alt.patterns, rhs := rhs.code : Alt Code }
   return { code := .match ref genParam discrs optMotive alts, uvars := ws }
 
-def mkMatchExpr (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (AltExpr CodeBlock)) (elseBranch : CodeBlock) : TermElabM CodeBlock := do
-  -- nary version of homogenize
-  let ws := alts.foldl (union · ·.rhs.uvars) {}
-  let ws := union ws elseBranch.uvars
-  let alts ← alts.mapM fun alt => do
-    let rhs ← extendUpdatedVars alt.rhs ws
-    return { alt with rhs := rhs.code : AltExpr Code }
-  let elseBranch ← extendUpdatedVars elseBranch ws
-  return { code := .matchExpr ref meta discr alts elseBranch.code, uvars := ws }
-
 /-- Return a code block that executes `terminal` and then `k` with the value produced by `terminal`.
    This method assumes `terminal` is a terminal -/
 def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Var) (k : CodeBlock) : TermElabM CodeBlock := do
@@ -765,19 +706,6 @@ private def expandDoIf? (stx : Syntax) : MacroM (Option Syntax) := match stx wit
     return some e
   | _ => pure none
 
-/--
-  If the given syntax is a `doLetExpr` or `doLetMetaExpr`, return an equivalent `doIf` that has an `else` but no `else if`s or `if let`s.  -/
-private def expandDoLetExpr? (stx : Syntax) (doElems : List Syntax) : MacroM (Option Syntax) := match stx with
-  | `(doElem| let_expr $pat:matchExprPat := $discr:term | $elseBranch:doSeq) =>
-    return some (← `(doElem| match_expr (meta := false) $discr:term with
-                             | $pat:matchExprPat => $(mkDoSeq doElems.toArray)
-                             | _ => $elseBranch))
-  | `(doElem| let_expr $pat:matchExprPat ← $discr:term | $elseBranch:doSeq) =>
-    return some (← `(doElem| match_expr $discr:term with
-                             | $pat:matchExprPat => $(mkDoSeq doElems.toArray)
-                             | _ => $elseBranch))
-  | _ => return none
-
 structure DoIfView where
   ref        : Syntax
   optIdent   : Syntax
@@ -1149,26 +1077,10 @@ where
       let mut termAlts := #[]
       for alt in alts do
         let rhs ← toTerm alt.rhs
-        let termAlt := mkNode ``Parser.Term.matchAlt #[mkAtomFrom alt.ref "|", mkNullNode #[alt.patterns], mkAtomFrom alt.ref "=>", rhs]
+        let termAlt := mkNode `Lean.Parser.Term.matchAlt #[mkAtomFrom alt.ref "|", mkNullNode #[alt.patterns], mkAtomFrom alt.ref "=>", rhs]
         termAlts := termAlts.push termAlt
-      let termMatchAlts := mkNode ``Parser.Term.matchAlts #[mkNullNode termAlts]
-      return mkNode ``Parser.Term.«match» #[mkAtomFrom ref "match", genParam, optMotive, discrs, mkAtomFrom ref "with", termMatchAlts]
-    | .matchExpr ref meta d alts elseBranch => withFreshMacroScope do
-      let d' ← `(discr)
-      let mut termAlts := #[]
-      for alt in alts do
-        let rhs ← `(($(← toTerm alt.rhs) : $((← read).m) _))
-        let optVar := if let some var := alt.var? then mkNullNode #[var, mkAtomFrom var "@"] else mkNullNode #[]
-        let pat := mkNode ``Parser.Term.matchExprPat #[optVar, alt.funName, mkNullNode alt.pvars]
-        let termAlt := mkNode ``Parser.Term.matchExprAlt #[mkAtomFrom alt.ref "|", pat, mkAtomFrom alt.ref "=>", rhs]
-        termAlts := termAlts.push termAlt
-      let elseBranch := mkNode ``Parser.Term.matchExprElseAlt #[mkAtomFrom ref "|", mkHole ref, mkAtomFrom ref "=>", (← toTerm elseBranch)]
-      let termMatchExprAlts := mkNode ``Parser.Term.matchExprAlts #[mkNullNode termAlts, elseBranch]
-      let body := mkNode ``Parser.Term.matchExpr #[mkAtomFrom ref "match_expr", d', mkAtomFrom ref "with", termMatchExprAlts]
-      if meta then
-        `(Bind.bind (instantiateMVarsIfMVarApp $d) fun discr => $body)
-      else
-        `(let discr := $d; $body)
+      let termMatchAlts := mkNode `Lean.Parser.Term.matchAlts #[mkNullNode termAlts]
+      return mkNode `Lean.Parser.Term.«match» #[mkAtomFrom ref "match", genParam, optMotive, discrs, mkAtomFrom ref "with", termMatchAlts]
 
 def run (code : Code) (m : Syntax) (returnType : Syntax) (uvars : Array Var := #[]) (kind := Kind.regular) : MacroM Syntax :=
   toTerm code { m, returnType, kind, uvars }
@@ -1621,24 +1533,6 @@ mutual
     let matchCode ← mkMatch ref genParam discrs optMotive alts
     concatWith matchCode doElems
 
-  /-- Generate `CodeBlock` for `doMatchExpr; doElems` -/
-  partial def doMatchExprToCode (doMatchExpr : Syntax) (doElems: List Syntax) : M CodeBlock := do
-    let ref       := doMatchExpr
-    let meta      := doMatchExpr[1].isNone
-    let discr     := doMatchExpr[2]
-    let alts      := doMatchExpr[4][0].getArgs -- Array of `doMatchExprAlt`
-    let alts ← alts.mapM fun alt => do
-      let pat      := alt[1]
-      let var?     := if pat[0].isNone then none else some pat[0][0]
-      let funName  := pat[1]
-      let pvars    := pat[2].getArgs
-      let rhs      := alt[3]
-      let rhs ← doSeqToCode (getDoSeqElems rhs)
-      pure { ref, var?, funName, pvars, rhs }
-    let elseBranch ← doSeqToCode (getDoSeqElems doMatchExpr[4][1][3])
-    let matchCode ← mkMatchExpr ref meta discr alts elseBranch
-    concatWith matchCode doElems
-
   /--
     Generate `CodeBlock` for `doTry; doElems`
     ```
@@ -1708,9 +1602,6 @@ mutual
       | none =>
       match (← liftMacroM <| expandDoIf? doElem) with
       | some doElem => doSeqToCode (doElem::doElems)
-      | none =>
-      match (← liftMacroM <| expandDoLetExpr? doElem doElems) with
-      | some doElem => doSeqToCode [doElem]
       | none =>
         let (liftedDoElems, doElem) ← expandLiftMethod doElem
         if !liftedDoElems.isEmpty then
@@ -1749,8 +1640,6 @@ mutual
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then
             doMatchToCode doElem doElems
-          else if k == ``Parser.Term.doMatchExpr then
-            doMatchExprToCode doElem doElems
           else if k == ``Parser.Term.doTry then
             doTryToCode doElem doElems
           else if k == ``Parser.Term.doBreak then

src/Lean/Elab/GuardMsgs.lean

@@ -1,136 +0,0 @@
-/-
-Copyright (c) 2023 Kyle Miller. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kyle Miller
--/
-prelude
-import Lean.Server.CodeActions.Attr
-
-/-! `#guard_msgs` command for testing commands
-
-This module defines a command to test that another command produces the expected messages.
-See the docstring on the `#guard_msgs` command.
--/
-
-open Lean Parser.Tactic Elab Command
-
-namespace Lean.Elab.Tactic.GuardMsgs
-
-/-- Gives a string representation of a message without source position information.
-Ensures the message ends with a '\n'. -/
-private def messageToStringWithoutPos (msg : Message) : IO String := do
-  let mut str ← msg.data.toString
-  unless msg.caption == "" do
-    str := msg.caption ++ ":\n" ++ str
-  if !("\n".isPrefixOf str) then str := " " ++ str
-  match msg.severity with
-  | MessageSeverity.information => str := "info:" ++ str
-  | MessageSeverity.warning     => str := "warning:" ++ str
-  | MessageSeverity.error       => str := "error:" ++ str
-  if str.isEmpty || str.back != '\n' then
-    str := str ++ "\n"
-  return str
-
-/-- The decision made by a specification for a message. -/
-inductive SpecResult
-  /-- Capture the message and check it matches the docstring. -/
-  | check
-  /-- Drop the message and delete it. -/
-  | drop
-  /-- Do not capture the message. -/
-  | passthrough
-
-/-- Parses a `guardMsgsSpec`.
-- No specification: check everything.
-- With a specification: interpret the spec, and if nothing applies pass it through. -/
-def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) :
-    CommandElabM (Message → SpecResult) := do
-  if let some spec := spec? then
-    match spec with
-    | `(guardMsgsSpec| ($[$elts:guardMsgsSpecElt],*)) => do
-      let mut p : Message → SpecResult := fun _ => .passthrough
-      let pushP (s : MessageSeverity) (drop : Bool) (p : Message → SpecResult)
-          (msg : Message) : SpecResult :=
-        if msg.severity == s then if drop then .drop else .check
-        else p msg
-      for elt in elts.reverse do
-        match elt with
-        | `(guardMsgsSpecElt| $[drop%$drop?]? info)    => p := pushP .information drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? warning) => p := pushP .warning drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? error)   => p := pushP .error drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? all) =>
-          p := fun _ => if drop?.isSome then .drop else .check
-        | _ => throwErrorAt elt "Invalid #guard_msgs specification element"
-      return p
-    | _ => throwErrorAt spec "Invalid #guard_msgs specification"
-  else
-    return fun _ => .check
-
-/-- An info tree node corresponding to a failed `#guard_msgs` invocation,
-used for code action support. -/
-structure GuardMsgFailure where
-  /-- The result of the nested command -/
-  res : String
-deriving TypeName
-
-@[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab
-  | `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do
-    let expected : String := (← dc?.mapM (getDocStringText ·)).getD "" |>.trim
-    let specFn ← parseGuardMsgsSpec spec?
-    let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
-    elabCommandTopLevel cmd
-    let msgs := (← get).messages
-    let mut toCheck : MessageLog := .empty
-    let mut toPassthrough : MessageLog := .empty
-    for msg in msgs.toList do
-      match specFn msg with
-      | .check       => toCheck := toCheck.add msg
-      | .drop        => pure ()
-      | .passthrough => toPassthrough := toPassthrough.add msg
-    let res := "---\n".intercalate (← toCheck.toList.mapM (messageToStringWithoutPos ·)) |>.trim
-    -- We do some whitespace normalization here to allow users to break long lines.
-    if expected.replace "\n" " " == res.replace "\n" " " then
-      -- Passed. Only put toPassthrough messages back on the message log
-      modify fun st => { st with messages := initMsgs ++ toPassthrough }
-    else
-      -- Failed. Put all the messages back on the message log and add an error
-      modify fun st => { st with messages := initMsgs ++ msgs }
-      logErrorAt tk m!"❌ Docstring on `#guard_msgs` does not match generated message:\n\n{res}"
-      pushInfoLeaf (.ofCustomInfo { stx := ← getRef, value := Dynamic.mk (GuardMsgFailure.mk res) })
-  | _ => throwUnsupportedSyntax
-
-open CodeAction Server RequestM in
-/-- A code action which will update the doc comment on a `#guard_msgs` invocation. -/
-@[builtin_command_code_action guardMsgsCmd]
-def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
-  let .node _ ts := node | return #[]
-  let res := ts.findSome? fun
-    | .node (.ofCustomInfo { stx, value }) _ => return (stx, (← value.get? GuardMsgFailure).res)
-    | _ => none
-  let some (stx, res) := res | return #[]
-  let doc ← readDoc
-  let eager := {
-    title := "Update #guard_msgs with tactic output"
-    kind? := "quickfix"
-    isPreferred? := true
-  }
-  pure #[{
-    eager
-    lazy? := some do
-      let some start := stx.getPos? true | return eager
-      let some tail := stx.setArg 0 mkNullNode |>.getPos? true | return eager
-      let newText := if res.isEmpty then
-        ""
-      else if res.length ≤ 100-7 && !res.contains '\n' then -- TODO: configurable line length?
-        s!"/-- {res} -/\n"
-      else
-        s!"/--\n{res}\n-/\n"
-      pure { eager with
-        edit? := some <|.ofTextEdit doc.versionedIdentifier {
-          range := doc.meta.text.utf8RangeToLspRange ⟨start, tail⟩
-          newText
-        }
-      }
-  }]
-
-end Lean.Elab.Tactic.GuardMsgs

src/Lean/Elab/InfoTree/Main.lean

@@ -49,25 +49,14 @@ def PartialContextInfo.mergeIntoOuter?
     some { outer with parentDecl? := innerParentDecl }
 
 def CompletionInfo.stx : CompletionInfo → Syntax
-  | dot i ..          => i.stx
-  | id stx ..         => stx
-  | dotId stx ..      => stx
-  | fieldId stx ..    => stx
-  | namespaceId stx   => stx
-  | option stx        => stx
+  | dot i .. => i.stx
+  | id stx .. => stx
+  | dotId stx .. => stx
+  | fieldId stx .. => stx
+  | namespaceId stx => stx
+  | option stx => stx
   | endSection stx .. => stx
-  | tactic stx ..     => stx
-
-/--
-Obtains the `LocalContext` from this `CompletionInfo` if available and yields an empty context
-otherwise.
--/
-def CompletionInfo.lctx : CompletionInfo → LocalContext
-  | dot i ..            => i.lctx
-  | id _ _ _ lctx ..    => lctx
-  | dotId _ _ lctx ..   => lctx
-  | fieldId _ _ lctx .. => lctx
-  | _                   => .empty
+  | tactic stx .. => stx
 
 def CustomInfo.format : CustomInfo → Format
   | i => f!"CustomInfo({i.value.typeName})"

src/Lean/Elab/Match.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 prelude
 import Lean.Util.ForEachExprWhere
-import Lean.Meta.CtorRecognizer
 import Lean.Meta.Match.Match
 import Lean.Meta.GeneralizeVars
 import Lean.Meta.ForEachExpr
@@ -443,7 +442,7 @@ private def applyRefMap (e : Expr) (map : ExprMap Expr) : Expr :=
 -/
 private def whnfPreservingPatternRef (e : Expr) : MetaM Expr := do
   let eNew ← whnf e
-  if (← isConstructorApp eNew) then
+  if eNew.isConstructorApp (← getEnv) then
     return eNew
   else
     return applyRefMap eNew (mkPatternRefMap e)
@@ -474,7 +473,7 @@ partial def normalize (e : Expr) : M Expr := do
         let p ← normalize p
         addVar h
         return mkApp4 e.getAppFn (e.getArg! 0) x p h
-      else if (← isMatchValue e) then
+      else if isMatchValue e then
         return e
       else if e.isFVar then
         if (← isExplicitPatternVar e) then
@@ -572,8 +571,8 @@ private partial def toPattern (e : Expr) : MetaM Pattern := do
         match e.getArg! 1, e.getArg! 3 with
         | Expr.fvar x, Expr.fvar h => return Pattern.as x p h
         | _,           _           => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
-      else if (← isMatchValue e) then
-        return Pattern.val (← normLitValue e)
+      else if isMatchValue e then
+        return Pattern.val e
       else if e.isFVar then
         return Pattern.var e.fvarId!
       else

src/Lean/Elab/MatchExpr.lean

@@ -1,217 +0,0 @@
-/-
-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
--/
-prelude
-import Lean.Elab.Term
-
-namespace Lean.Elab.Term
-namespace MatchExpr
-/--
-`match_expr` alternative. Recall that it has the following structure.
-```
-| (ident "@")? ident bindeIdent* => rhs
-```
-
-Example:
-```
-| c@Eq _ a b => f c a b
-```
--/
-structure Alt where
-  /--
-  `some c` if there is a variable binding to the function symbol being matched.
-  `c` is the variable name.
-  -/
-  var?    : Option Ident
-  /-- Function being matched. -/
-  funName : Ident
-  /-- Pattern variables. The list uses `none` for representing `_`, and `some a` for pattern variable `a`. -/
-  pvars   : List (Option Ident)
-  /-- right-hand-side for the alternative. -/
-  rhs     : Syntax
-  /-- Store the auxliary continuation function for each right-hand-side. -/
-  k       : Ident := ⟨.missing⟩
-  /-- Actual value to be passed as an argument. -/
-  actuals : List Term := []
-
-/--
-`match_expr` else-alternative. Recall that it has the following structure.
-```
-| _ => rhs
-```
--/
-structure ElseAlt where
-  rhs : Syntax
-
-open Parser Term
-
-/--
-Converts syntax representing a `match_expr` else-alternative into an `ElseAlt`.
--/
-def toElseAlt? (stx : Syntax) : Option ElseAlt :=
-  if !stx.isOfKind ``matchExprElseAlt then none else
-  some { rhs := stx[3] }
-
-/--
-Converts syntax representing a `match_expr` alternative into an `Alt`.
--/
-def toAlt? (stx : Syntax) : Option Alt :=
-  if !stx.isOfKind ``matchExprAlt then none else
-  match stx[1] with
-  | `(matchExprPat| $[$var? @]? $funName:ident $pvars*) =>
-    let pvars := pvars.toList.reverse.map fun arg =>
-      match arg.raw with
-      | `(_) => none
-      | _ => some ⟨arg⟩
-    let rhs := stx[3]
-    some { var?, funName, pvars, rhs }
-  | _ => none
-
-/--
-Returns the function names of alternatives that do not have any pattern variable left.
--/
-def getFunNamesToMatch (alts : List Alt) : List Ident := Id.run do
-  let mut funNames := #[]
-  for alt in alts do
-    if alt.pvars.isEmpty then
-      if Option.isNone <| funNames.find? fun funName => funName.getId == alt.funName.getId then
-        funNames := funNames.push alt.funName
-  return funNames.toList
-
-/--
-Returns `true` if there is at least one alternative whose next pattern variable is not a `_`.
--/
-def shouldSaveActual (alts : List Alt) : Bool :=
-  alts.any fun alt => alt.pvars matches some _ :: _
-
-/--
-Returns the first alternative whose function name is `funName` **and**
-does not have pattern variables left to match.
--/
-def getAltFor? (alts : List Alt) (funName : Ident) : Option Alt :=
-  alts.find? fun alt => alt.funName.getId == funName.getId && alt.pvars.isEmpty
-
-/--
-Removes alternatives that do not have any pattern variable left to be matched.
-For the ones that still have pattern variables, remove the first one, and
-save `actual` if the removed pattern variable is not a `_`.
--/
-def next (alts : List Alt) (actual : Term) : List Alt :=
-  alts.filterMap fun alt =>
-    if let some _ :: pvars := alt.pvars then
-      some { alt with pvars, actuals := actual :: alt.actuals }
-    else if let none :: pvars := alt.pvars then
-      some { alt with pvars }
-    else
-      none
-
-/--
-Creates a fresh identifier for representing the continuation function used to
-execute the RHS of the given alternative, and stores it in the field `k`.
--/
-def initK (alt : Alt) : MacroM Alt := withFreshMacroScope do
-  -- Remark: the compiler frontend implemented in C++ currently detects jointpoints created by
-  -- the "do" notation by testing the name. See hack at method `visit_let` at `lcnf.cpp`
-  -- We will remove this hack when we re-implement the compiler frontend in Lean.
-  let k : Ident ← `(__do_jp)
-  return { alt with k }
-
-/--
-Generates parameters for the continuation function used to execute
-the RHS of the given alternative.
--/
-def getParams (alt : Alt) : MacroM (Array (TSyntax ``bracketedBinder)) := do
-  let mut params := #[]
-  if let some var := alt.var? then
-    params := params.push (← `(bracketedBinderF| ($var : Expr)))
-  params := params ++ (← alt.pvars.toArray.reverse.filterMapM fun
-    | none => return none
-    | some arg => return some (← `(bracketedBinderF| ($arg : Expr))))
-  if params.isEmpty then
-    return #[(← `(bracketedBinderF| (_ : Unit)))]
-  return params
-
-/--
-Generates the actual arguments for invoking the auxiliary continuation function
-associated with the given alternative. The arguments are the actuals stored in `alt`.
-`discr` is also an argument if `alt.var?` is not none.
--/
-def getActuals (discr : Term) (alt : Alt) : MacroM (Array Term) := do
-  let mut actuals := #[]
-  if alt.var?.isSome then
-    actuals := actuals.push discr
-  actuals := actuals ++ alt.actuals.toArray
-  if actuals.isEmpty then
-    return #[← `(())]
-  return actuals
-
-def toDoubleQuotedName (ident : Ident) : Term :=
-  ⟨mkNode ``Parser.Term.doubleQuotedName #[mkAtom "`", mkAtom "`", ident]⟩
-
-/--
-Generates an `if-then-else` tree for implementing a `match_expr` with discriminant `discr`,
-alternatives `alts`, and else-alternative `elseAlt`.
--/
-partial def generate (discr : Term) (alts : List Alt) (elseAlt : ElseAlt) : MacroM Syntax := do
-  let alts ← alts.mapM initK
-  let discr' ← `(__discr)
-  -- Remark: the compiler frontend implemented in C++ currently detects jointpoints created by
-  -- the "do" notation by testing the name. See hack at method `visit_let` at `lcnf.cpp`
-  -- We will remove this hack when we re-implement the compiler frontend in Lean.
-  let kElse ← `(__do_jp)
-  let rec loop (discr : Term) (alts : List Alt) : MacroM Term := withFreshMacroScope do
-    let funNamesToMatch := getFunNamesToMatch alts
-    let saveActual := shouldSaveActual alts
-    let actual ← if saveActual then `(a) else `(_)
-    let altsNext := next alts actual
-    let body ← if altsNext.isEmpty then
-      `($kElse ())
-    else
-      let discr' ← `(__discr)
-      let body ← loop discr' altsNext
-      if saveActual then
-        `(if h : ($discr).isApp then let a := Expr.appArg $discr h; let __discr := Expr.appFnCleanup $discr h; $body else $kElse ())
-      else
-        `(if h : ($discr).isApp then let __discr := Expr.appFnCleanup $discr h; $body else $kElse ())
-    let mut result := body
-    for funName in funNamesToMatch do
-      if let some alt := getAltFor? alts funName then
-        let actuals ← getActuals discr alt
-        result ← `(if ($discr).isConstOf $(toDoubleQuotedName funName) then $alt.k $actuals* else $result)
-    return result
-  let body ← loop discr' alts
-  let mut result ← `(let_delayed __do_jp (_ : Unit) := $(⟨elseAlt.rhs⟩):term; let __discr := Expr.cleanupAnnotations $discr:term; $body:term)
-  for alt in alts do
-    let params ← getParams alt
-    result ← `(let_delayed $alt.k:ident $params:bracketedBinder* := $(⟨alt.rhs⟩):term; $result:term)
-  return result
-
-def main (discr : Term) (alts : Array Syntax) (elseAlt : Syntax) : MacroM Syntax := do
-  let alts ← alts.toList.mapM fun alt =>
-    if let some alt := toAlt? alt then
-      pure alt
-    else
-      Macro.throwErrorAt alt "unexpected `match_expr` alternative"
-  let some elseAlt := toElseAlt? elseAlt
-    | Macro.throwErrorAt elseAlt "unexpected `match_expr` else-alternative"
-  generate discr alts elseAlt
-
-end MatchExpr
-
-@[builtin_macro Lean.Parser.Term.matchExpr] def expandMatchExpr : Macro := fun stx =>
-  match stx with
-  | `(match_expr $discr:term with $alts) =>
-    MatchExpr.main discr alts.raw[0].getArgs alts.raw[1]
-  | _ => Macro.throwUnsupported
-
-@[builtin_macro Lean.Parser.Term.letExpr] def expandLetExpr : Macro := fun stx =>
-  match stx with
-  | `(let_expr $pat:matchExprPat := $discr:term | $elseBranch:term; $body:term) =>
-    `(match_expr $discr with
-      | $pat:matchExprPat => $body
-      | _ => $elseBranch)
-  | _ => Macro.throwUnsupported
-
-end Lean.Elab.Term

src/Lean/Elab/Notation.lean

@@ -107,10 +107,22 @@ def mkUnexpander (attrKind : TSyntax ``attrKind) (pat qrhs : Term) : OptionT Mac
   -- The reference is attached to the syntactic representation of the called function itself, not the entire function application
   let lhs ← `($$f:ident)
   let lhs := Syntax.mkApp lhs (.mk args)
+  -- allow over-application, avoiding nested `app` nodes
+  let lhsWithMoreArgs := flattenApp (← `($lhs $$moreArgs*))
+  let patWithMoreArgs := flattenApp (← `($pat $$moreArgs*))
   `(@[$attrKind app_unexpander $(mkIdent c)]
     aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
       | `($lhs)             => withRef f `($pat)
+      -- must be a separate case as the LHS and RHS above might not be `app` nodes
+      | `($lhsWithMoreArgs) => withRef f `($patWithMoreArgs)
       | _                   => throw ())
+where
+  -- NOTE: we consider only one nesting level here
+  flattenApp : Term → Term
+    | stx@`($f $xs*) => match f with
+      | `($f' $xs'*) => Syntax.mkApp f' (xs' ++ xs)
+      | _            => stx
+    | stx            => stx
 
 private def expandNotationAux (ref : Syntax) (currNamespace : Name)
     (doc? : Option (TSyntax ``docComment))

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Eqns
-import Lean.Meta.CtorRecognizer
 import Lean.Util.CollectFVars
 import Lean.Util.ForEachExprWhere
 import Lean.Meta.Tactic.Split
@@ -219,14 +218,13 @@ where
 -/
 private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
   let env ← getEnv
-  let find (root : Expr) : ExceptT Unit MetaM Unit :=
-    root.forEach fun e => do
-      if let some info := isMatcherAppCore? env e then
-        let args := e.getAppArgs
-        for discr in args[info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
-          if (← Meta.isConstructorApp discr) then
-            throwThe Unit ()
-  return (← (find e).run) matches .error _
+  return Option.isSome <| e.find? fun e => Id.run do
+    if let some info := isMatcherAppCore? env e then
+      let args := e.getAppArgs
+      for discr in args[info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
+        if discr.isConstructorApp env then
+          return true
+    return false
 
 partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
   let (_, eqnTypes) ← go mvarId |>.run { declNames } |>.run #[]

src/Lean/Elab/PreDefinition/Main.lean

@@ -121,7 +121,8 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       preDefs.forM (·.termination.ensureNone "partial")
     else
       try
-        let hasHints := preDefs.any fun preDef => preDef.termination.isNotNone
+        let hasHints := preDefs.any  fun preDef =>
+          preDef.termination.decreasing_by?.isSome || preDef.termination.termination_by?.isSome
         if hasHints then
           wfRecursion preDefs
         else

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

@@ -8,7 +8,6 @@ import Lean.Util.HasConstCache
 import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Refl
-import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Quotation
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
@@ -703,19 +702,17 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
   -- Collect all recursive calls and extract their context
   let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
   let recCalls := filterSubsumed recCalls
-  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) ·)
+  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasing_by?)) ·)
   let callMatrix := rcs.map (inspectCall ·)
 
   match ← liftMetaM <| solve measures callMatrix with
   | .some solution => do
     let wf ← buildTermWF originalVarNamess varNamess solution
 
-    let wf' := trimTermWF extraParamss wf
-    for preDef in preDefs, term in wf' do
-      if showInferredTerminationBy.get (← getOptions) then
-        logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}"
-      if let some ref := preDef.termination.terminationBy?? then
-        Tactic.TryThis.addSuggestion ref (← term.unexpand)
+    if showInferredTerminationBy.get (← getOptions) then
+      let wf' := trimTermWF extraParamss wf
+      for preDef in preDefs, term in wf' do
+        logInfoAt preDef.ref m!"Inferred termination argument: {← term.unexpand}"
 
     return wf
   | .none =>

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

@@ -94,12 +94,12 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
     return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
 
   let wf ← do
-    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.terminationBy?.isSome)
+    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.termination_by?.isSome)
     if preDefsWith.isEmpty then
       -- No termination_by anywhere, so guess one
       guessLex preDefs unaryPreDef fixedPrefixSize
     else if preDefsWithout.isEmpty then
-      pure <| preDefsWith.map (·.termination.terminationBy?.get!)
+      pure <| preDefsWith.map (·.termination.termination_by?.get!)
     else
       -- Some have, some do not, so report errors
       preDefsWithout.forM fun preDef => do
@@ -114,7 +114,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
-        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasingBy?))
+        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasing_by?))
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value

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

@@ -27,7 +27,7 @@ structure TerminationBy where
   deriving Inhabited
 
 open Parser.Termination in
-def TerminationBy.unexpand (wf : TerminationBy) : MetaM (TSyntax ``terminationBy) := do
+def TerminationBy.unexpand (wf : TerminationBy) : MetaM Syntax := do
   -- TODO: Why can I not just use $wf.vars in the quotation below?
   let vars : TSyntaxArray `ident := wf.vars.map (⟨·.raw⟩)
   if vars.isEmpty then
@@ -50,9 +50,8 @@ is what `Term.runTactic` expects.
  -/
 structure TerminationHints where
   ref : Syntax
-  terminationBy?? : Option Syntax
-  terminationBy? : Option TerminationBy
-  decreasingBy?  : Option DecreasingBy
+  termination_by? : Option TerminationBy
+  decreasing_by?  : Option DecreasingBy
   /-- Here we record the number of parameters past the `:`. It is set by
   `TerminationHints.rememberExtraParams` and used as folows:
 
@@ -64,27 +63,19 @@ structure TerminationHints where
   extraParams : Nat
   deriving Inhabited
 
-def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, 0⟩
+def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, 0⟩
 
 /-- Logs warnings when the `TerminationHints` are present.  -/
 def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): CoreM Unit := do
-  match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy? with
-  | .none, .none, .none => pure ()
-  | .none, .none, .some dec_by =>
+  match hints.termination_by?, hints.decreasing_by? with
+  | .none, .none => pure ()
+  | .none, .some dec_by =>
     logErrorAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
-  | .some term_by?, .none, .none =>
-    logErrorAt term_by? m!"unused `termination_by?`, function is {reason}"
-  | .none, .some term_by, .none =>
+  | .some term_by, .none =>
     logErrorAt term_by.ref m!"unused `termination_by`, function is {reason}"
-  | _, _, _ =>
+  | .some _, .some _ =>
     logErrorAt hints.ref m!"unused termination hints, function is {reason}"
 
-/-- True if any form of termination hint is present. -/
-def TerminationHints.isNotNone (hints : TerminationHints) : Bool :=
-  hints.terminationBy??.isSome ||
-  hints.terminationBy?.isSome ||
-  hints.decreasingBy?.isSome
-
 /--
 Remembers `extraParams` for later use. Needs to happen early enough where we still know
 how many parameters came from the function header (`headerParams`).
@@ -120,23 +111,19 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) :
   if let .missing := stx.raw then
     return { TerminationHints.none with ref := stx }
   match stx with
-  | `(suffix| $[$t?]? $[$d?:decreasingBy]? ) => do
-    let terminationBy?? : Option Syntax ← if let some t := t? then match t with
-      | `(terminationBy?|termination_by?) => pure (some t)
-      | _ => pure none
-      else pure none
-    let terminationBy? : Option TerminationBy ← if let some t := t? then match t with
-      | `(terminationBy|termination_by => $_body) =>
-        throwErrorAt t "no extra parameters bounds, please omit the `=>`"
-      | `(terminationBy|termination_by $vars* => $body) => pure (some {ref := t, vars, body})
-      | `(terminationBy|termination_by $body:term) => pure (some {ref := t, vars := #[], body})
-      | `(terminationBy?|termination_by?) => pure none
+  | `(suffix| $[$t?:terminationBy]? $[$d?:decreasingBy]? ) => do
+    let termination_by? ← t?.mapM fun t => match t with
+      | `(terminationBy|termination_by $vars* => $body) =>
+        if vars.isEmpty then
+          throwErrorAt t "no extra parameters bounds, please omit the `=>`"
+        else
+          pure {ref := t, vars, body}
+      | `(terminationBy|termination_by $body:term) => pure {ref := t, vars := #[], body}
       | _ => throwErrorAt t "unexpected `termination_by` syntax"
-      else pure none
-    let decreasingBy? ← d?.mapM fun d => match d with
+    let decreasing_by? ← d?.mapM fun d => match d with
       | `(decreasingBy|decreasing_by $tactic) => pure {ref := d, tactic}
       | _ => throwErrorAt d "unexpected `decreasing_by` syntax"
-    return { ref := stx, terminationBy??, terminationBy?, decreasingBy?, extraParams := 0 }
+    return { ref := stx, termination_by?, decreasing_by?, extraParams := 0 }
   | _ => throwErrorAt stx s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}"
 
 end Lean.Elab.WF

src/Lean/Elab/StructInst.lean

@@ -802,8 +802,10 @@ partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Ex
         let arg ← mkFreshExprMVar d
         mkDefaultValueAux? struct (b.instantiate1 arg)
   | e =>
-    let_expr id _ a := e | return some e
-    return some a
+    if e.isAppOfArity ``id 2 then
+      return some e.appArg!
+    else
+      return some e
 
 def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
   withRef struct.ref do

src/Lean/Elab/Tactic.lean

@@ -36,5 +36,3 @@ import Lean.Elab.Tactic.Simpa
 import Lean.Elab.Tactic.NormCast
 import Lean.Elab.Tactic.Symm
 import Lean.Elab.Tactic.SolveByElim
-import Lean.Elab.Tactic.LibrarySearch
-import Lean.Elab.Tactic.ShowTerm

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -372,24 +372,10 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let d ← instantiateMVars d
-    -- Get instance from `d`
-    let s := d.appArg!
-    -- Reduce the instance rather than `d` itself, since that gives a nicer error message on failure.
-    let r ← withDefault <| whnf s
-    if r.isAppOf ``isFalse then
-      throwError "\
-        tactic 'decide' proved that the proposition\
-        {indentExpr expectedType}\n\
-        is false"
-    unless r.isAppOf ``isTrue do
-      throwError "\
-        tactic 'decide' failed for proposition\
-        {indentExpr expectedType}\n\
-        since its 'Decidable' instance reduced to\
-        {indentExpr r}\n\
-        rather than to the 'isTrue' constructor."
-    -- While we have a proof from reduction, we do not embed it in the proof term,
-    -- but rather we let the kernel recompute it during type checking from a more efficient term.
+    let r ← withDefault <| whnf d
+    unless r.isConstOf ``true do
+      throwError "failed to reduce to 'true'{indentExpr r}"
+    let s := d.appArg! -- get instance from `d`
     let rflPrf ← mkEqRefl (toExpr true)
     return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
 

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -1,81 +0,0 @@
-/-
-Copyright (c) 2021-2024 Gabriel Ebner and Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Joe Hendrix, Scott Morrison
--/
-prelude
-import Lean.Meta.Tactic.LibrarySearch
-import Lean.Meta.Tactic.TryThis
-import Lean.Elab.Tactic.ElabTerm
-
-namespace Lean.Elab.LibrarySearch
-
-open Lean Meta LibrarySearch
-open Elab Tactic Term TryThis
-
-/--
-Implementation of the `exact?` tactic.
-
-* `ref` contains the input syntax and is used for locations in error reporting.
-* `required` contains an optional list of terms that should be used in closing the goal.
-* `requireClose` indicates if the goal must be closed.
-  It is `true` for `exact?` and `false` for `apply?`.
--/
-def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) :
-    TacticM Unit := do
-  let mvar ← getMainGoal
-  let (_, goal) ← (← getMainGoal).intros
-  goal.withContext do
-    let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
-    let tactic := fun exfalso =>
-          solveByElim required (exfalso := exfalso) (maxDepth := 6)
-    let allowFailure := fun g => do
-      let g ← g.withContext (instantiateMVars (.mvar g))
-      return required.all fun e => e.occurs g
-    match ← librarySearch goal tactic allowFailure with
-    -- Found goal that closed problem
-    | none =>
-      addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta
-    -- Found suggestions
-    | some suggestions =>
-      if requireClose then throwError
-        "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
-      reportOutOfHeartbeats `library_search ref
-      for (_, suggestionMCtx) in suggestions do
-        withMCtx suggestionMCtx do
-          addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)
-      if suggestions.isEmpty then logError "apply? didn't find any relevant lemmas"
-      admitGoal goal
-
-@[builtin_tactic Lean.Parser.Tactic.exact?]
-def evalExact : Tactic := fun stx => do
-  let `(tactic| exact? $[using $[$required],*]?) := stx
-        | throwUnsupportedSyntax
-  exact? (← getRef) required true
-
-
-@[builtin_tactic Lean.Parser.Tactic.apply?]
-def evalApply : Tactic := fun stx => do
-  let `(tactic| apply? $[using $[$required],*]?) := stx
-        | throwUnsupportedSyntax
-  exact? (← getRef) required false
-
-@[builtin_term_elab Lean.Parser.Syntax.exact?]
-def elabExact?Term : TermElab := fun stx expectedType? => do
-  let `(exact?%) := stx | throwUnsupportedSyntax
-  withExpectedType expectedType? fun expectedType => do
-    let goal ← mkFreshExprMVar expectedType
-    let (_, introdGoal) ← goal.mvarId!.intros
-    introdGoal.withContext do
-      if let some suggestions ← librarySearch introdGoal then
-        reportOutOfHeartbeats `library_search stx
-        for suggestion in suggestions do
-          withMCtx suggestion.2 do
-            addTermSuggestion stx (← instantiateMVars goal).headBeta
-        if suggestions.isEmpty then logError "exact?# didn't find any relevant lemmas"
-        mkSorry expectedType (synthetic := true)
-      else
-        addTermSuggestion stx (← instantiateMVars goal).headBeta
-        instantiateMVars goal
-
-end Lean.Elab.LibrarySearch

src/Lean/Elab/Tactic/NormCast.lean

@@ -3,7 +3,6 @@ Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
 -/
-prelude
 import Lean.Meta.Tactic.NormCast
 import Lean.Elab.Tactic.Conv.Simp
 import Lean.Elab.ElabRules

src/Lean/Elab/Tactic/Omega.lean

@@ -3,7 +3,6 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-prelude
 import Lean.Elab.Tactic.Omega.Frontend
 
 /-!

src/Lean/Elab/Tactic/Omega/Core.lean

@@ -3,8 +3,6 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-prelude
-import Init.Omega.Constraint
 import Lean.Elab.Tactic.Omega.OmegaM
 import Lean.Elab.Tactic.Omega.MinNatAbs
 

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -3,7 +3,6 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-prelude
 import Lean.Elab.Tactic.Omega.Core
 import Lean.Elab.Tactic.FalseOrByContra
 import Lean.Meta.Tactic.Cases
@@ -68,7 +67,7 @@ def mkEvalRflProof (e : Expr) (lc : LinearCombo) : OmegaM Expr := do
 `e = (coordinate n).eval atoms`. -/
 def mkCoordinateEvalAtomsEq (e : Expr) (n : Nat) : OmegaM Expr := do
   if n < 10 then
-    let atoms ← atoms
+    let atoms := (← getThe State).atoms
     let tail ← mkListLit (.const ``Int []) atoms[n+1:].toArray.toList
     let lem := .str ``LinearCombo s!"coordinate_eval_{n}"
     mkEqSymm (mkAppN (.const lem []) (atoms[:n+1].toArray.push tail))
@@ -598,7 +597,7 @@ def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
 
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This
 `TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via
-the tactic call `aesop (add 50% tactic Lean.Omega.omegaDefault)`. -/
+the tactic call `aesop (add 50% tactic Std.Tactic.Omega.omegaDefault)`. -/
 def omegaDefault : TacticM Unit := omegaTactic {}
 
 @[builtin_tactic Lean.Parser.Tactic.omega]

src/Lean/Elab/Tactic/Omega/MinNatAbs.lean

@@ -3,10 +3,6 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-prelude
-import Init.BinderPredicates
-import Init.Data.List
-import Init.Data.Option
 
 /-!
 # `List.nonzeroMinimum`, `List.minNatAbs`, `List.maxNatAbs`

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -3,11 +3,6 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-prelude
-import Init.Omega.LinearCombo
-import Init.Omega.Int
-import Init.Omega.Logic
-import Init.Data.BitVec
 import Lean.Meta.AppBuilder
 
 /-!
@@ -51,7 +46,7 @@ structure Context where
 /-- The internal state for the `OmegaM` monad, recording previously encountered atoms. -/
 structure State where
   /-- The atoms up-to-defeq encountered so far. -/
-  atoms : HashMap Expr Nat := {}
+  atoms : Array Expr := #[]
 
 /-- An intermediate layer in the `OmegaM` monad. -/
 abbrev OmegaM' := StateRefT State (ReaderT Context MetaM)
@@ -76,11 +71,10 @@ def OmegaM.run (m : OmegaM α) (cfg : OmegaConfig) : MetaM α :=
 def cfg : OmegaM OmegaConfig := do pure (← read).cfg
 
 /-- Retrieve the list of atoms. -/
-def atoms : OmegaM (Array Expr) := do
-  return (← getThe State).atoms.toArray.qsort (·.2 < ·.2) |>.map (·.1)
+def atoms : OmegaM (List Expr) := return (← getThe State).atoms.toList
 
 /-- Return the `Expr` representing the list of atoms. -/
-def atomsList : OmegaM Expr := do mkListLit (.const ``Int []) (← atoms).toList
+def atomsList : OmegaM Expr := do mkListLit (.const ``Int []) (← atoms)
 
 /-- Return the `Expr` representing the list of atoms as a `Coeffs`. -/
 def atomsCoeffs : OmegaM Expr := do
@@ -175,8 +169,8 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
         r := r.insert (mkApp (.const ``Int.neg_le_natAbs []) x)
       | _, (``Fin.val, #[n, i]) =>
         r := r.insert (mkApp2 (.const ``Fin.isLt []) n i)
-      | _, (``BitVec.toNat, #[n, x]) =>
-        r := r.insert (mkApp2 (.const ``BitVec.toNat_lt []) n x)
+      | _, (`Std.BitVec.toNat, #[n, x]) =>
+        r := r.insert (mkApp2 (.const `Std.BitVec.toNat_lt []) n x)
       | _, _ => pure ()
     return r
   | (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with
@@ -244,16 +238,15 @@ Return its index, and, if it is new, a collection of interesting facts about the
 -/
 def lookup (e : Expr) : OmegaM (Nat × Option (HashSet Expr)) := do
   let c ← getThe State
-  match c.atoms.find? e with
-  | some i => return (i, none)
-  | none =>
+  for h : i in [:c.atoms.size] do
+    if ← isDefEq e c.atoms[i] then
+      return (i, none)
   trace[omega] "New atom: {e}"
   let facts ← analyzeAtom e
   if ← isTracingEnabledFor `omega then
     unless facts.isEmpty do
       trace[omega] "New facts: {← facts.toList.mapM fun e => inferType e}"
-  let i ← modifyGetThe State fun c =>
-    (c.atoms.size, { c with atoms := c.atoms.insert e c.atoms.size })
+  let i ← modifyGetThe State fun c => (c.atoms.size, { c with atoms := c.atoms.push e })
   return (i, some facts)
 
 end Omega

src/Lean/Elab/Tactic/ShowTerm.lean

@@ -1,28 +0,0 @@
-/-
-Copyright (c) 2021 Scott Morrison. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison, Mario Carneiro
--/
-prelude
-import Lean.Elab.ElabRules
-import Lean.Meta.Tactic.TryThis
-
-namespace Std.Tactic
-open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
-
-@[builtin_tactic showTerm] def evalShowTerm : Tactic := fun stx =>
-  match stx with
-  | `(tactic| show_term%$tk $t) => withMainContext do
-    let g ← getMainGoal
-    evalTactic t
-    addExactSuggestion tk (← instantiateMVars (mkMVar g)).headBeta (origSpan? := ← getRef)
-  | _ => throwUnsupportedSyntax
-
-/-- Implementation of `show_term` term elaborator. -/
-@[builtin_term_elab showTermElabImpl] def elabShowTerm : TermElab
-  | `(show_term_elab%$tk $t), ty => do
-    let e ← Term.elabTermEnsuringType t ty
-    Term.synthesizeSyntheticMVarsNoPostponing
-    addTermSuggestion tk (← instantiateMVars e).headBeta (origSpan? := ← getRef)
-    pure e
-  | _, _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/Simp.lean

@@ -353,13 +353,14 @@ def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
           | true  => `(Parser.Tactic.simpLemma| $decl:term)
           | false => `(Parser.Tactic.simpLemma| ↓ $decl:term)
         args := args.push arg
-    | .fvar fvarId =>
-      -- local hypotheses in the context
+    | .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
+      -- be redundant. It would also be confusing since it suggests that only
+      -- `h` is used.
+      if isSimpAll then
+        continue
       if let some ldecl := lctx.find? fvarId then
-        -- `simp_all` always uses all propositional hypotheses.
-        -- So `simp_all only [x]`, only makes sense if `ldecl` is a let-variable.
-        if isSimpAll && !ldecl.hasValue then
-          continue
         localsOrStar := localsOrStar.bind fun locals =>
           if !ldecl.userName.isInaccessibleUserName && !ldecl.userName.hasMacroScopes &&
               (lctx.findFromUserName? ldecl.userName).get!.fvarId == ldecl.fvarId then

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -3,7 +3,6 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-prelude
 import Lean.Elab.ElabRules
 import Lean.Elab.Tactic.Simp
 import Lean.Meta.Tactic.TryThis
@@ -25,12 +24,13 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
 @[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
   match stx with
   | `(tactic|
-      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do
+      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => do
     let stx ← if bang.isSome then
       `(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
       `(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
-    let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
+    let { ctx, simprocs, dischargeWrapper } ←
+      withMainContext <| mkSimpContext stx (eraseLocal := false)
     let usedSimps ← dischargeWrapper.with fun discharge? =>
       simpLocation ctx (simprocs := simprocs) discharge? <|
         (loc.map expandLocation).getD (.targets #[] true)

src/Lean/Elab/Tactic/Simpa.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Gabriel Ebner, Mario Carneiro
 -/
-prelude
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Tactic.Simp

src/Lean/Exception.lean

@@ -69,7 +69,7 @@ protected def throwError [Monad m] [MonadError m] (msg : MessageData) : m α :=
   let (ref, msg) ← AddErrorMessageContext.add ref msg
   throw <| Exception.error ref msg
 
-/-- Throw an unknown constant error message. -/
+/-- Thrown an unknown constant error message. -/
 def throwUnknownConstant [Monad m] [MonadError m] (constName : Name) : m α :=
   Lean.throwError m!"unknown constant '{mkConst constName}'"
 

src/Lean/Expr.lean

@@ -801,7 +801,7 @@ def isType0 : Expr → Bool
 
 /-- Return `true` if the given expression is `.sort .zero` -/
 def isProp : Expr → Bool
-  | sort .zero => true
+  | sort (.zero ..) => true
   | _ => false
 
 /-- Return `true` if the given expression is a bound variable. -/
@@ -904,14 +904,6 @@ def appArg!' : Expr → Expr
   | app _ a   => a
   | _         => panic! "application expected"
 
-def appArg (e : Expr) (h : e.isApp) : Expr :=
-  match e, h with
-  | .app _ a, _ => a
-
-def appFn (e : Expr) (h : e.isApp) : Expr :=
-  match e, h with
-  | .app f _, _ => f
-
 def sortLevel! : Expr → Level
   | sort u => u
   | _      => panic! "sort expected"
@@ -920,7 +912,7 @@ def litValue! : Expr → Literal
   | lit v => v
   | _     => panic! "literal expected"
 
-def isRawNatLit : Expr → Bool
+def isNatLit : Expr → Bool
   | lit (Literal.natVal _) => true
   | _                      => false
 
@@ -933,7 +925,7 @@ def isStringLit : Expr → Bool
   | _                      => false
 
 def isCharLit : Expr → Bool
-  | app (const c _) a => c == ``Char.ofNat && a.isRawNatLit
+  | app (const c _) a => c == ``Char.ofNat && a.isNatLit
   | _                 => false
 
 def constName! : Expr → Name
@@ -1045,14 +1037,6 @@ def getAppFn : Expr → Expr
   | app f _ => getAppFn f
   | e         => e
 
-/--
-Similar to `getAppFn`, but skips `mdata`
--/
-def getAppFn' : Expr → Expr
-  | app f _   => getAppFn' f
-  | mdata _ a => getAppFn' a
-  | e         => e
-
 /-- Given `f a₀ a₁ ... aₙ`, returns true if `f` is a constant with name `n`. -/
 def isAppOf (e : Expr) (n : Name) : Bool :=
   match e.getAppFn with
@@ -1075,6 +1059,33 @@ def isAppOfArity' : Expr → Name → Nat → Bool
   | app f _,    n, a+1 => isAppOfArity' f n a
   | _,          _,  _   => false
 
+/--
+Checks if an expression is a "natural number numeral in normal form",
+i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n`
+where `n` matches `.lit (.natVal n)` for some literal natural number `n`.
+and if so returns `n`.
+-/
+-- Note that `Expr.lit (.natVal n)` is not considered in normal form!
+def nat? (e : Expr) : Option Nat := do
+  guard <| e.isAppOfArity ``OfNat.ofNat 3
+  let lit (.natVal n) := e.appFn!.appArg! | none
+  n
+
+/--
+Checks if an expression is an "integer numeral in normal form",
+i.e. of type `Nat` or `Int`, and either a natural number numeral in normal form (as specified by `nat?`),
+or the negation of a positive natural number numberal in normal form,
+and if so returns the integer.
+-/
+def int? (e : Expr) : Option Int :=
+  if e.isAppOfArity ``Neg.neg 3 then
+    match e.appArg!.nat? with
+    | none => none
+    | some 0 => none
+    | some n => some (-n)
+  else
+    e.nat?
+
 private def getAppNumArgsAux : Expr → Nat → Nat
   | app f _, n => getAppNumArgsAux f (n+1)
   | _,       n => n
@@ -1196,21 +1207,10 @@ def getRevArg! : Expr → Nat → Expr
   | app f _, i+1 => getRevArg! f i
   | _,       _   => panic! "invalid index"
 
-/-- Similar to `getRevArg!` but skips `mdata` -/
-def getRevArg!' : Expr → Nat → Expr
-  | mdata _ a, i => getRevArg!' a i
-  | app _ a, 0   => a
-  | app f _, i+1 => getRevArg!' f i
-  | _,       _   => panic! "invalid index"
-
 /-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or panics if out of bounds. -/
 @[inline] def getArg! (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
   getRevArg! e (n - i - 1)
 
-/-- Similar to `getArg!`, but skips mdata -/
-@[inline] def getArg!' (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
-  getRevArg!' e (n - i - 1)
-
 /-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or returns `v₀` if out of bounds. -/
 @[inline] def getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n := e.getAppNumArgs) : Expr :=
   getRevArgD e (n - i - 1) v₀
@@ -1597,45 +1597,12 @@ partial def cleanupAnnotations (e : Expr) : Expr :=
   let e' := e.consumeMData.consumeTypeAnnotations
   if e' == e then e else cleanupAnnotations e'
 
-/--
-Similar to `appFn`, but also applies `cleanupAnnotations` to resulting function.
-This function is used compile the `match_expr` term.
--/
-def appFnCleanup (e : Expr) (h : e.isApp) : Expr :=
-  match e, h with
-  | .app f _, _ => f.cleanupAnnotations
-
 def isFalse (e : Expr) : Bool :=
   e.cleanupAnnotations.isConstOf ``False
 
 def isTrue (e : Expr) : Bool :=
   e.cleanupAnnotations.isConstOf ``True
 
-/--
-Checks if an expression is a "natural number numeral in normal form",
-i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n`
-where `n` matches `.lit (.natVal n)` for some literal natural number `n`.
-and if so returns `n`.
--/
--- Note that `Expr.lit (.natVal n)` is not considered in normal form!
-def nat? (e : Expr) : Option Nat := do
-  let_expr OfNat.ofNat _ n _ := e | failure
-  let lit (.natVal n) := n | failure
-  n
-
-/--
-Checks if an expression is an "integer numeral in normal form",
-i.e. of type `Nat` or `Int`, and either a natural number numeral in normal form (as specified by `nat?`),
-or the negation of a positive natural number numberal in normal form,
-and if so returns the integer.
--/
-def int? (e : Expr) : Option Int :=
-  let_expr Neg.neg _ _ a := e | e.nat?
-  match a.nat? with
-  | none => none
-  | some 0 => none
-  | some n => some (-n)
-
 /-- Return true iff `e` contains a free variable which satisfies `p`. -/
 @[inline] def hasAnyFVar (e : Expr) (p : FVarId → Bool) : Bool :=
   let rec @[specialize] visit (e : Expr) := if !e.hasFVar then false else

src/Lean/Meta.lean

@@ -45,5 +45,3 @@ import Lean.Meta.ExprTraverse
 import Lean.Meta.Eval
 import Lean.Meta.CoeAttr
 import Lean.Meta.Iterator
-import Lean.Meta.LazyDiscrTree
-import Lean.Meta.LitValues

src/Lean/Meta/Basic.lean

@@ -254,7 +254,7 @@ structure PostponedEntry where
   ref  : Syntax
   lhs  : Level
   rhs  : Level
-  /-- Context for the surrounding `isDefEq` call when the entry was created. -/
+  /-- Context for the surrounding `isDefEq` call when entry was created. -/
   ctx? : Option DefEqContext
   deriving Inhabited
 
@@ -264,7 +264,7 @@ structure PostponedEntry where
 structure State where
   mctx             : MetavarContext := {}
   cache            : Cache := {}
-  /-- When `trackZetaDelta == true`, then any let-decl free variable that is zetaDelta-expanded by `MetaM` is stored in `zetaDeltaFVarIds`. -/
+  /-- When `trackZetaDelta == true`, then any let-decl free variable that is zetaDelta expansion performed by `MetaM` is stored in `zetaDeltaFVarIds`. -/
   zetaDeltaFVarIds : FVarIdSet := {}
   /-- Array of postponed universe level constraints -/
   postponed        : PersistentArray PostponedEntry := {}
@@ -1067,23 +1067,6 @@ partial def withNewLocalInstances (fvars : Array Expr) (j : Nat) : n α → n α
 def forallTelescope (type : Expr) (k : Array Expr → Expr → n α) : n α :=
   map2MetaM (fun k => forallTelescopeImp type k) k
 
-/--
-Given a monadic function `f` that takes a type and a term of that type and produces a new term,
-lifts this to the monadic function that opens a `∀` telescope, applies `f` to the body,
-and then builds the lambda telescope term for the new term.
--/
-def mapForallTelescope' (f : Expr → Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
-  forallTelescope (← inferType forallTerm) fun xs ty => do
-    mkLambdaFVars xs (← f ty (mkAppN forallTerm xs))
-
-/--
-Given a monadic function `f` that takes a term and produces a new term,
-lifts this to the monadic function that opens a `∀` telescope, applies `f` to the body,
-and then builds the lambda telescope term for the new term.
--/
-def mapForallTelescope (f : Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
-  mapForallTelescope' (fun _ e => f e) forallTerm
-
 private def forallTelescopeReducingImp (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
   forallTelescopeReducingAux type (maxFVars? := none) k
 
@@ -1737,15 +1720,6 @@ def isDefEqNoConstantApprox (t s : Expr) : MetaM Bool :=
 def etaExpand (e : Expr) : MetaM Expr :=
   withDefault do forallTelescopeReducing (← inferType e) fun xs _ => mkLambdaFVars xs (mkAppN e xs)
 
-/--
-If `e` is of the form `?m ...` instantiate metavars
--/
-def instantiateMVarsIfMVarApp (e : Expr) : MetaM Expr := do
-  if e.getAppFn.isMVar then
-    instantiateMVars e
-  else
-    return e
-
 end Meta
 
 builtin_initialize

src/Lean/Meta/CompletionName.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-prelude
+
 import Lean.Meta.Basic
 import Lean.Meta.Match.MatcherInfo
 
@@ -29,21 +29,11 @@ builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDec
 def addToCompletionBlackList (env : Environment) (declName : Name) : Environment :=
   completionBlackListExt.tag env declName
 
-/--
-Checks whether a given name is internal due to something other than `_private`.
-Correctly deals with names like `_private.<SomeNamespace>.0.<SomeType>._sizeOf_1` in a private type
-`SomeType`, which `n.isInternal && !isPrivateName n` does not.
--/
-private def isInternalNameModuloPrivate : Name → Bool
-  | n@(.str p s) => s.get 0 == '_' && n != privateHeader || isInternalNameModuloPrivate p
-  | .num p _ => isInternalNameModuloPrivate p
-  | _       => false
-
 /--
 Return true if name is blacklisted for completion purposes.
 -/
 private def isBlacklisted (env : Environment) (declName : Name) : Bool :=
-  isInternalNameModuloPrivate declName
+  declName.isInternal && !isPrivateName declName
   || isAuxRecursor env declName
   || isNoConfusion env declName
   || isRecCore env declName

src/Lean/Meta/CtorRecognizer.lean

@@ -1,74 +0,0 @@
-/-
-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
--/
-prelude
-import Lean.Meta.LitValues
-
-namespace Lean.Meta
-
-private def getConstructorVal? (env : Environment) (ctorName : Name) : Option ConstructorVal :=
-  match env.find? ctorName with
-  | some (.ctorInfo v) => v
-  | _                  => none
-
-
-/--
-If `e` is a constructor application or a builtin literal defeq to a constructor application,
-then return the corresponding `ConstructorVal`.
--/
-def isConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
-  let e ← litToCtor e
-  let .const n _ := e.getAppFn | return none
-  let some v := getConstructorVal? (← getEnv) n | return none
-  if v.numParams + v.numFields == e.getAppNumArgs then
-    return some v
-  else
-    return none
-
-/--
-Similar to `isConstructorApp?`, but uses `whnf`.
--/
-def isConstructorApp'? (e : Expr) : MetaM (Option ConstructorVal) := do
-  if let some r ← isConstructorApp? e then
-    return r
-  isConstructorApp? (← whnf e)
-
-/--
-Returns `true`, if `e` is constructor application of builtin literal defeq to
-a constructor application.
--/
-def isConstructorApp (e : Expr) : MetaM Bool :=
-  return (← isConstructorApp? e).isSome
-
-/--
-Returns `true` if `isConstructorApp e` or `isConstructorApp (← whnf e)`
--/
-def isConstructorApp' (e : Expr) : MetaM Bool := do
-  if (← isConstructorApp e) then return true
-  return (← isConstructorApp (← whnf e))
-
-/--
-If `e` is a constructor application, return a pair containing the corresponding `ConstructorVal` and the constructor
-application arguments.
--/
-def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) := do
-  let e ← litToCtor e
-  let .const declName _ := e.getAppFn | return none
-  let some v := getConstructorVal? (← getEnv) declName | return none
-  if v.numParams + v.numFields == e.getAppNumArgs then
-    return some (v, e.getAppArgs)
-  else
-    return none
-
-/--
-Similar to `constructorApp?`, but on failure it puts `e` in WHNF and tries again.
--/
-def constructorApp'? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) := do
-  if let some r ← constructorApp? e then
-    return some r
-  else
-    constructorApp? (← whnf e)
-
-end Lean.Meta

src/Lean/Meta/DiscrTree.lean

@@ -172,7 +172,7 @@ private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Arr
   - `Nat.succ x` where `isNumeral x`
   - `OfNat.ofNat _ x _` where `isNumeral x` -/
 private partial def isNumeral (e : Expr) : Bool :=
-  if e.isRawNatLit then true
+  if e.isNatLit then true
   else
     let f := e.getAppFn
     if !f.isConst then false

src/Lean/Meta/Eqns.lean

@@ -51,8 +51,7 @@ private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
     return false
 
 structure EqnsExtState where
-  map    : PHashMap Name (Array Name) := {}
-  mapInv : PHashMap Name Name := {}
+  map : PHashMap Name (Array Name) := {}
   deriving Inhabited
 
 /- We generate the equations on demand, and do not save them on .olean files. -/
@@ -78,22 +77,7 @@ private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
     return none
 
 /--
-Returns `some declName` if `thmName` is an equational theorem for `declName`.
--/
-def isEqnThm? (thmName : Name) : CoreM (Option Name) := do
-  return eqnsExt.getState (← getEnv) |>.mapInv.find? thmName
-
-/--
-Stores in the `eqnsExt` environment extension that `eqThms` are the equational theorems for `declName`
--/
-private def registerEqnThms (declName : Name) (eqThms : Array Name) : CoreM Unit := do
-  modifyEnv fun env => eqnsExt.modifyState env fun s => { s with
-    map := s.map.insert declName eqThms
-    mapInv := eqThms.foldl (init := s.mapInv) fun mapInv eqThm => mapInv.insert eqThm declName
-  }
-
-/--
-  Returns equation theorems for the given declaration.
+  Return equation theorems for the given declaration.
   By default, we do not create equation theorems for nonrecursive definitions.
   You can use `nonRec := true` to override this behavior, a dummy `rfl` proof is created on the fly.
 -/
@@ -103,12 +87,12 @@ def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)
   else if (← shouldGenerateEqnThms declName) then
     for f in (← getEqnsFnsRef.get) do
       if let some r ← f declName then
-        registerEqnThms declName r
+        modifyEnv fun env => eqnsExt.modifyState env fun s => { s with map := s.map.insert declName r }
         return some r
     if nonRec then
       let some eqThm ← mkSimpleEqThm declName | return none
       let r := #[eqThm]
-      registerEqnThms declName r
+      modifyEnv fun env => eqnsExt.modifyState env fun s => { s with map := s.map.insert declName r }
       return some r
   return none
 
@@ -147,8 +131,8 @@ def registerGetUnfoldEqnFn (f : GetUnfoldEqnFn) : IO Unit := do
   getUnfoldEqnFnsRef.modify (f :: ·)
 
 /--
-  Return an "unfold" theorem for the given declaration.
-  By default, we do not create unfold theorems for nonrecursive definitions.
+  Return a "unfold" theorem for the given declaration.
+  By default, we not create unfold theorems for nonrecursive definitions.
   You can use `nonRec := true` to override this behavior.
 -/
 def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) := withLCtx {} {} do

src/Lean/Meta/ExprLens.lean

@@ -138,11 +138,11 @@ private def viewCoordRaw: Expr → Nat → M Expr
   | e                     , c => throwError "Bad coordinate {c} for {e}"
 
 
-/-- Given a valid `SubExpr`, return the raw current expression without performing any instantiation.
-If the given `SubExpr` has a type subexpression coordinate, then throw an error.
+/-- Given a valid SubExpr, will return the raw current expression without performing any instantiation.
+If the SubExpr has a type subexpression coordinate then will error.
 
 This is a cheaper version of `Lean.Meta.viewSubexpr` and can be used to quickly view the
-subexpression at a position. Note that because the resulting expression may contain
+subexpression at a position. Note that because the resulting expression will contain
 loose bound variables it can't be used in any `MetaM` methods. -/
 def viewSubexpr (p : Pos) (root : Expr) : M Expr :=
   p.foldlM viewCoordRaw root
@@ -172,3 +172,5 @@ def numBinders (p : Pos) (e : Expr) : M Nat :=
 end ViewRaw
 
 end Lean.Core
+
+

src/Lean/Meta/Injective.lean

@@ -26,8 +26,10 @@ private def mkAnd? (args : Array Expr) : Option Expr := Id.run do
 
 def elimOptParam (type : Expr) : CoreM Expr := do
   Core.transform type fun e =>
-    let_expr optParam _ a := e | return .continue
-    return TransformStep.visit a
+    if e.isAppOfArity  ``optParam 2 then
+      return TransformStep.visit (e.getArg! 0)
+    else
+      return .continue
 
 private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
   let us := ctorVal.levelParams.map mkLevelParam

src/Lean/Meta/LazyDiscrTree.lean

@@ -1,831 +0,0 @@
-/-
-Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joe Hendrix, Scott Morrison
--/
-prelude
-import Lean.Meta.CompletionName
-import Lean.Meta.DiscrTree
-
-/-!
-# Lazy Discrimination Tree
-
-This file defines a new type of discrimination tree optimized for rapid
-population of imported modules for use in tactics.  It uses a lazy
-initialization strategy.
-
-The discrimination tree can be created through
-`createImportedEnvironment`. This creates a discrimination tree from all
-imported modules in an environment using a callback that provides the
-entries as `InitEntry` values.
-
-The function `getMatch` can be used to get the values that match the
-expression as well as an updated lazy discrimination tree that has
-elaborated additional parts of the tree.
--/
-namespace Lean.Meta.LazyDiscrTree
-
--- This namespace contains definitions copied from Lean.Meta.DiscrTree.
-namespace MatchClone
-
-/--
-Discrimination tree key.
--/
-private inductive Key where
-  | const : Name → Nat → Key
-  | fvar  : FVarId → Nat → Key
-  | lit   : Literal → Key
-  | star  : Key
-  | other : Key
-  | arrow : Key
-  | proj  : Name → Nat → Nat → Key
-  deriving Inhabited, BEq, Repr
-
-namespace Key
-
-/-- Hash function -/
-protected def hash : Key → UInt64
-  | .const n a   => mixHash 5237 $ mixHash n.hash (hash a)
-  | .fvar n a    => mixHash 3541 $ mixHash (hash n) (hash a)
-  | .lit v       => mixHash 1879 $ hash v
-  | .star        => 7883
-  | .other       => 2411
-  | .arrow       => 17
-  | .proj s i a  =>  mixHash (hash a) $ mixHash (hash s) (hash i)
-
-instance : Hashable Key := ⟨Key.hash⟩
-
-end Key
-
-private def tmpMVarId : MVarId := { name := `_discr_tree_tmp }
-private def tmpStar := mkMVar tmpMVarId
-
-/--
-  Returns true iff the argument should be treated as a "wildcard" by the
-  discrimination tree.
-
-  This includes proofs, instance implicit arguments, implicit arguments,
-  and terms of the form `noIndexing t`
-
-  This is a clone of `Lean.Meta.DiscrTree.ignoreArg` and mainly added to
-  avoid coupling between `DiscrTree` and `LazyDiscrTree` while both are
-  potentially subject to independent changes.
--/
-private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool := do
-  if h : i < infos.size then
-    let info := infos.get ⟨i, h⟩
-    if info.isInstImplicit then
-      return true
-    else if info.isImplicit || info.isStrictImplicit then
-      return not (← isType a)
-    else
-      isProof a
-  else
-    isProof a
-
-private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Array Expr → MetaM (Array Expr)
-  | i, .app f a, todo => do
-    if (← ignoreArg a i infos) then
-      pushArgsAux infos (i-1) f (todo.push tmpStar)
-    else
-      pushArgsAux infos (i-1) f (todo.push a)
-  | _, _, todo => return todo
-
-/--
-  Returns `true` if `e` is one of the following
-  - A nat literal (numeral)
-  - `Nat.zero`
-  - `Nat.succ x` where `isNumeral x`
-  - `OfNat.ofNat _ x _` where `isNumeral x` -/
-private partial def isNumeral (e : Expr) : Bool :=
-  if e.isRawNatLit then true
-  else
-    let f := e.getAppFn
-    if !f.isConst then false
-    else
-      let fName := f.constName!
-      if fName == ``Nat.succ && e.getAppNumArgs == 1 then isNumeral e.appArg!
-      else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then isNumeral (e.getArg! 1)
-      else if fName == ``Nat.zero && e.getAppNumArgs == 0 then true
-      else false
-
-private partial def toNatLit? (e : Expr) : Option Literal :=
-  if isNumeral e then
-    if let some n := loop e then
-      some (.natVal n)
-    else
-      none
-  else
-    none
-where
-  loop (e : Expr) : OptionT Id Nat := do
-    let f := e.getAppFn
-    match f with
-    | .lit (.natVal n) => return n
-    | .const fName .. =>
-      if fName == ``Nat.succ && e.getAppNumArgs == 1 then
-        let r ← loop e.appArg!
-        return r+1
-      else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then
-        loop (e.getArg! 1)
-      else if fName == ``Nat.zero && e.getAppNumArgs == 0 then
-        return 0
-      else
-        failure
-    | _ => failure
-
-private def isNatType (e : Expr) : MetaM Bool :=
-  return (← whnf e).isConstOf ``Nat
-
-/--
-  Returns `true` if `e` is one of the following
-  - `Nat.add _ k` where `isNumeral k`
-  - `Add.add Nat _ _ k` where `isNumeral k`
-  - `HAdd.hAdd _ Nat _ _ k` where `isNumeral k`
-  - `Nat.succ _`
-  This function assumes `e.isAppOf fName`
--/
-private def isNatOffset (fName : Name) (e : Expr) : MetaM Bool := do
-  if fName == ``Nat.add && e.getAppNumArgs == 2 then
-    return isNumeral e.appArg!
-  else if fName == ``Add.add && e.getAppNumArgs == 4 then
-    if (← isNatType (e.getArg! 0)) then return isNumeral e.appArg! else return false
-  else if fName == ``HAdd.hAdd && e.getAppNumArgs == 6 then
-    if (← isNatType (e.getArg! 1)) then return isNumeral e.appArg! else return false
-  else
-    return fName == ``Nat.succ && e.getAppNumArgs == 1
-
-/-
-This is a hook to determine if we should add an expression as a wildcard pattern.
-
-Clone of `Lean.Meta.DiscrTree.shouldAddAsStar`.  See it for more discussion.
--/
-private def shouldAddAsStar (fName : Name) (e : Expr) : MetaM Bool := do
-  isNatOffset fName e
-
-/--
-Eliminate loose bound variables via beta-reduction.
-
-This is primarily used to reduce pi-terms `∀(x : P), T` into
-non-dependend functions `P → T`.  The latter has a more specific
-discrimination tree key `.arrow..` and this improves the accuracy of the
-discrimination tree.
-
-Clone of `Lean.Meta.DiscrTree.elimLooseBVarsByBeta`.  See it for more
-discussion.
--/
-private def elimLooseBVarsByBeta (e : Expr) : CoreM Expr :=
-  Core.transform e
-    (pre := fun e => do
-      if !e.hasLooseBVars then
-        return .done e
-      else if e.isHeadBetaTarget then
-        return .visit e.headBeta
-      else
-        return .continue)
-
-private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) :
-    MetaM (Key × Array Expr) := do
-  let e ← DiscrTree.reduceDT e root config
-  unless root do
-    -- See pushArgs
-    if let some v := toNatLit? e then
-      return (.lit v, #[])
-  match e.getAppFn with
-  | .lit v         => return (.lit v, #[])
-  | .const c _     =>
-    if (← getConfig).isDefEqStuckEx && e.hasExprMVar then
-      if (← isReducible c) then
-        /- `e` is a term `c ...` s.t. `c` is reducible and `e` has metavariables, but it was not
-            unfolded.  This can happen if the metavariables in `e` are "blocking" smart unfolding.
-           If `isDefEqStuckEx` is enabled, then we must throw the `isDefEqStuck` exception to
-           postpone TC resolution.
-        -/
-        Meta.throwIsDefEqStuck
-      else if let some matcherInfo := isMatcherAppCore? (← getEnv) e then
-        -- A matcher application is stuck if one of the discriminants has a metavariable
-        let args := e.getAppArgs
-        let start := matcherInfo.getFirstDiscrPos
-        for arg in args[ start : start + matcherInfo.numDiscrs ] do
-          if arg.hasExprMVar then
-            Meta.throwIsDefEqStuck
-      else if (← isRec c) then
-        /- Similar to the previous case, but for `match` and recursor applications. It may be stuck
-           (i.e., did not reduce) because of metavariables. -/
-        Meta.throwIsDefEqStuck
-    let nargs := e.getAppNumArgs
-    return (.const c nargs, e.getAppRevArgs)
-  | .fvar fvarId   =>
-    let nargs := e.getAppNumArgs
-    return (.fvar fvarId nargs, e.getAppRevArgs)
-  | .mvar mvarId   =>
-    if isMatch then
-      return (.other, #[])
-    else do
-      let ctx ← read
-      if ctx.config.isDefEqStuckEx then
-        /-
-          When the configuration flag `isDefEqStuckEx` is set to true,
-          we want `isDefEq` to throw an exception whenever it tries to assign
-          a read-only metavariable.
-          This feature is useful for type class resolution where
-          we may want to notify the caller that the TC problem may be solvable
-          later after it assigns `?m`.
-          The method `DiscrTree.getUnify e` returns candidates `c` that may "unify" with `e`.
-          That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (Add ?m)`
-          where `?m` is a read-only metavariable, and the discrimination tree contains the keys
-          `HadAdd Nat` and `Add Int`. If `isDefEqStuckEx` is set to true, we must treat `?m` as
-          a regular metavariable here, otherwise we return the empty set of candidates.
-          This is incorrect because it is equivalent to saying that there is no solution even if
-          the caller assigns `?m` and try again. -/
-        return (.star, #[])
-      else if (← mvarId.isReadOnlyOrSyntheticOpaque) then
-        return (.other, #[])
-      else
-        return (.star, #[])
-  | .proj s i a .. =>
-    let nargs := e.getAppNumArgs
-    return (.proj s i nargs, #[a] ++ e.getAppRevArgs)
-  | .forallE _ d b _ =>
-    -- See comment at elimLooseBVarsByBeta
-    let b ← if b.hasLooseBVars then elimLooseBVarsByBeta b else pure b
-    if b.hasLooseBVars then
-      return (.other, #[])
-    else
-      return (.arrow, #[d, b])
-  | .bvar _ | .letE _ _ _ _ _ | .lam _ _ _ _ | .mdata _ _ | .app _ _ | .sort _ =>
-    return (.other, #[])
-
-/-
-Given an expression we are looking for patterns that match, return the key and sub-expressions.
--/
-private abbrev getMatchKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) :
-    MetaM (Key × Array Expr) :=
-  getKeyArgs e (isMatch := true) (root := root) (config := config)
-
-end MatchClone
-
-export MatchClone (Key Key.const)
-
-/--
-An unprocessed entry in the lazy discrimination tree.
--/
-private abbrev LazyEntry α := Array Expr × ((LocalContext × LocalInstances) × α)
-
-/--
-Index identifying trie in a discrimination tree.
--/
-@[reducible]
-private def TrieIndex := Nat
-
-/--
-Discrimination tree trie. See `LazyDiscrTree`.
--/
-private structure Trie (α : Type) where
-  node ::
-    /-- Values for matches ending at this trie. -/
-    values : Array α
-    /-- Index of trie matching star. -/
-    star : TrieIndex
-    /-- Following matches based on key of trie. -/
-    children : HashMap Key TrieIndex
-    /-- Lazy entries at this trie that are not processed. -/
-    pending : Array (LazyEntry α)
-  deriving Inhabited
-
-instance : EmptyCollection (Trie α) := ⟨.node #[] 0 {} #[]⟩
-
-/-- Push lazy entry to trie. -/
-private def Trie.pushPending : Trie α → LazyEntry α → Trie α
-| .node vs star cs p, e => .node vs star cs (p.push e)
-
-end LazyDiscrTree
-
-/--
-`LazyDiscrTree` is a variant of the discriminator tree datatype
-`DiscrTree` in Lean core that is designed to be efficiently
-initializable with a large number of patterns.  This is useful
-in contexts such as searching an entire Lean environment for
-expressions that match a pattern.
-
-Lazy discriminator trees achieve good performance by minimizing
-the amount of work that is done up front to build the discriminator
-tree.  When first adding patterns to the tree, only the root
-discriminator key is computed and processing the remaining
-terms is deferred until demanded by a match.
--/
-structure LazyDiscrTree (α : Type) where
-  /-- Configuration for normalization. -/
-  config : Lean.Meta.WhnfCoreConfig := {}
-  /-- Backing array of trie entries.  Should be owned by this trie. -/
-  tries : Array (LazyDiscrTree.Trie α) := #[default]
-  /-- Map from discriminator trie roots to the index. -/
-  roots : Lean.HashMap LazyDiscrTree.Key LazyDiscrTree.TrieIndex := {}
-
-namespace LazyDiscrTree
-
-open Lean Elab Meta
-
-instance : Inhabited (LazyDiscrTree α) where
-  default := {}
-
-open Lean.Meta.DiscrTree (mkNoindexAnnotation hasNoindexAnnotation reduceDT)
-
-/--
-Specialization of Lean.Meta.DiscrTree.pushArgs
--/
-private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : WhnfCoreConfig) :
-    MetaM (Key × Array Expr) := do
-  if hasNoindexAnnotation e then
-    return (.star, todo)
-  else
-    let e ← reduceDT e root config
-    let fn := e.getAppFn
-    let push (k : Key) (nargs : Nat) (todo : Array Expr) : MetaM (Key × Array Expr) := do
-      let info ← getFunInfoNArgs fn nargs
-      let todo ← MatchClone.pushArgsAux info.paramInfo (nargs-1) e todo
-      return (k, todo)
-    match fn with
-    | .lit v     =>
-      return (.lit v, todo)
-    | .const c _ =>
-      unless root do
-        if let some v := MatchClone.toNatLit? e then
-          return (.lit v, todo)
-        if (← MatchClone.shouldAddAsStar c e) then
-          return (.star, todo)
-      let nargs := e.getAppNumArgs
-      push (.const c nargs) nargs todo
-    | .proj s i a =>
-      /-
-      If `s` is a class, then `a` is an instance. Thus, we annotate `a` with `no_index` since we do
-      not index instances. This should only happen if users mark a class projection function as
-      `[reducible]`.
-
-      TODO: add better support for projections that are functions
-      -/
-      let a := if isClass (← getEnv) s then mkNoindexAnnotation a else a
-      let nargs := e.getAppNumArgs
-      push (.proj s i nargs) nargs (todo.push a)
-    | .fvar _fvarId   =>
-      return (.star, todo)
-    | .mvar mvarId   =>
-      if mvarId == MatchClone.tmpMVarId then
-        -- We use `tmp to mark implicit arguments and proofs
-        return (.star, todo)
-      else
-        failure
-    | .forallE _ d b _ =>
-      -- See comment at elimLooseBVarsByBeta
-      let b ← if b.hasLooseBVars then MatchClone.elimLooseBVarsByBeta b else pure b
-      if b.hasLooseBVars then
-        return (.other, todo)
-      else
-        return (.arrow, (todo.push d).push b)
-    | _ =>
-      return (.other, todo)
-
-/-- Initial capacity for key and todo vector. -/
-private def initCapacity := 8
-
-/--
-Get the root key and rest of terms of an expression using the specified config.
--/
-private def rootKey (cfg: WhnfCoreConfig) (e : Expr) : MetaM (Key × Array Expr) :=
-  pushArgs true (Array.mkEmpty initCapacity) e cfg
-
-private partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key)
-    (config : WhnfCoreConfig) : MetaM (Array Key) := do
-  if todo.isEmpty then
-    return keys
-  else
-    let e    := todo.back
-    let todo := todo.pop
-    let (k, todo) ← pushArgs root todo e config
-    mkPathAux false todo (keys.push k) config
-
-/--
-Create a path from an expression.
-
-This differs from Lean.Meta.DiscrTree.mkPath in that the expression
-should uses free variables rather than meta-variables for holes.
--/
-private def mkPath (e : Expr) (config : WhnfCoreConfig) : MetaM (Array Key) := do
-  let todo : Array Expr := .mkEmpty initCapacity
-  let keys : Array Key := .mkEmpty initCapacity
-  mkPathAux (root := true) (todo.push e) keys config
-
-/- Monad for finding matches while resolving deferred patterns. -/
-@[reducible]
-private def MatchM α := ReaderT WhnfCoreConfig (StateRefT (Array (Trie α)) MetaM)
-
-private def runMatch (d : LazyDiscrTree α) (m : MatchM α β)  : MetaM (β × LazyDiscrTree α) := do
-  let { config := c, tries := a, roots := r } := d
-  let (result, a) ← withReducible $ (m.run c).run a
-  pure (result, { config := c, tries := a, roots := r})
-
-private def setTrie (i : TrieIndex) (v : Trie α) : MatchM α Unit :=
-  modify (·.set! i v)
-
-/-- Create a new trie with the given lazy entry. -/
-private def newTrie [Monad m] [MonadState (Array (Trie α)) m] (e : LazyEntry α) : m TrieIndex := do
-  modifyGet fun a => let sz := a.size; (sz, a.push (.node #[] 0 {} #[e]))
-
-/-- Add a lazy entry to an existing trie. -/
-private def addLazyEntryToTrie (i:TrieIndex) (e : LazyEntry α) : MatchM α Unit :=
-  modify (·.modify i (·.pushPending e))
-
-/--
-This evaluates all lazy entries in a trie and updates `values`, `starIdx`, and `children`
-accordingly.
--/
-private partial def evalLazyEntries (config : WhnfCoreConfig)
-    (values : Array α) (starIdx : TrieIndex) (children : HashMap Key TrieIndex)
-    (entries : Array (LazyEntry α)) :
-    MatchM α (Array α × TrieIndex × HashMap Key TrieIndex) := do
-  let rec iter values starIdx children (i : Nat) : MatchM α _ := do
-        if p : i < entries.size then
-          let (todo, lctx, v) := entries[i]
-          if todo.isEmpty then
-            let values := values.push v
-            iter values starIdx children (i+1)
-          else
-            let e    := todo.back
-            let todo := todo.pop
-            let (k, todo) ← withLCtx lctx.1 lctx.2 $ pushArgs false todo e config
-            if k == .star then
-              if starIdx = 0 then
-                let starIdx ← newTrie (todo, lctx, v)
-                iter values starIdx children (i+1)
-              else
-                addLazyEntryToTrie starIdx (todo, lctx, v)
-                iter values starIdx children (i+1)
-            else
-              match children.find? k with
-              | none =>
-                let children := children.insert k (← newTrie (todo, lctx, v))
-                iter values starIdx children (i+1)
-              | some idx =>
-                addLazyEntryToTrie idx (todo, lctx, v)
-                iter values starIdx children (i+1)
-        else
-          pure (values, starIdx, children)
-  iter values starIdx children 0
-
-private def evalNode (c : TrieIndex) :
-    MatchM α (Array α × TrieIndex × HashMap Key TrieIndex) := do
-  let .node vs star cs pending := (←get).get! c
-  if pending.size = 0 then
-    pure (vs, star, cs)
-  else
-    let config ← read
-    setTrie c default
-    let (vs, star, cs) ← evalLazyEntries config vs star cs pending
-    setTrie c <| .node vs star cs #[]
-    pure (vs, star, cs)
-
-/--
-Return the information about the trie at the given idnex.
-
-Used for internal debugging purposes.
--/
-private def getTrie (d : LazyDiscrTree α) (idx : TrieIndex) :
-    MetaM ((Array α × TrieIndex × HashMap Key TrieIndex) × LazyDiscrTree α) :=
-  runMatch d (evalNode idx)
-
-/--
-A match result contains the terms formed from matching a term against
-patterns in the discrimination tree.
-
--/
-private structure MatchResult (α : Type) where
-  /--
-  The elements in the match result.
-
-  The top-level array represents an array from `score` values to the
-  results with that score. A `score` is the number of non-star matches
-  in a pattern against the term, and thus bounded by the size of the
-  term being matched against.  The elements of this array are themselves
-  arrays of non-empty arrays so that we can defer concatenating results until
-  needed.
-  -/
-  elts : Array (Array (Array α)) := #[]
-
-private def MatchResult.push (r : MatchResult α) (score : Nat) (e : Array α) : MatchResult α :=
-  if e.isEmpty then
-    r
-  else if score < r.elts.size then
-    { elts := r.elts.modify score (·.push e) }
-  else
-    let rec loop (a : Array (Array (Array α))) :=
-        if a.size < score then
-          loop (a.push #[])
-        else
-          { elts := a.push #[e] }
-    termination_by score - a.size
-    loop r.elts
-
-private partial def MatchResult.toArray (mr : MatchResult α) : Array α :=
-    loop (Array.mkEmpty n) mr.elts
-  where n := mr.elts.foldl (fun i a => a.foldl (fun n a => n + a.size) i) 0
-        loop (r : Array α) (a : Array (Array (Array α))) :=
-          if a.isEmpty then
-            r
-          else
-            loop (a.back.foldl (init := r) (fun r a => r ++ a)) a.pop
-
-private partial def getMatchLoop (todo : Array Expr) (score : Nat) (c : TrieIndex)
-    (result : MatchResult α) : MatchM α (MatchResult α) := do
-  let (vs, star, cs) ← evalNode c
-  if todo.isEmpty then
-    return result.push score vs
-  else if star == 0 && cs.isEmpty then
-    return result
-  else
-    let e     := todo.back
-    let todo  := todo.pop
-    /- We must always visit `Key.star` edges since they are wildcards.
-        Thus, `todo` is not used linearly when there is `Key.star` edge
-        and there is an edge for `k` and `k != Key.star`. -/
-    let visitStar (result : MatchResult α) : MatchM α (MatchResult α) :=
-      if star != 0 then
-        getMatchLoop todo score star result
-      else
-        return result
-    let visitNonStar (k : Key) (args : Array Expr) (result : MatchResult α) :=
-      match cs.find? k with
-      | none   => return result
-      | some c => getMatchLoop (todo ++ args) (score + 1) c result
-    let result ← visitStar result
-    let (k, args) ← MatchClone.getMatchKeyArgs e (root := false) (←read)
-    match k with
-    | .star  => return result
-    /-
-      Note: dep-arrow vs arrow
-      Recall that dependent arrows are `(Key.other, #[])`, and non-dependent arrows are
-      `(Key.arrow, #[a, b])`.
-      A non-dependent arrow may be an instance of a dependent arrow (stored at `DiscrTree`).
-      Thus, we also visit the `Key.other` child.
-    -/
-    | .arrow => visitNonStar .other #[] (← visitNonStar k args result)
-    | _      => visitNonStar k args result
-
-private def getStarResult (root : Lean.HashMap Key TrieIndex) : MatchM α (MatchResult α) :=
-  match root.find? .star with
-  | none =>
-    pure <| {}
-  | some idx => do
-    let (vs, _) ← evalNode idx
-    pure <| ({} : MatchResult α).push 0 vs
-
-private def getMatchRoot (r : Lean.HashMap Key TrieIndex) (k : Key) (args : Array Expr)
-    (result : MatchResult α) : MatchM α (MatchResult α) :=
-  match r.find? k with
-  | none => pure result
-  | some c => getMatchLoop args 1 c result
-
-/--
-  Find values that match `e` in `root`.
--/
-private def getMatchCore (root : Lean.HashMap Key TrieIndex) (e : Expr) :
-    MatchM α (MatchResult α) := do
-  let result ← getStarResult root
-  let (k, args) ← MatchClone.getMatchKeyArgs e (root := true) (←read)
-  match k with
-  | .star  => return result
-  /- See note about "dep-arrow vs arrow" at `getMatchLoop` -/
-  | .arrow =>
-    getMatchRoot root k args (←getMatchRoot root .other #[] result)
-  | _ =>
-    getMatchRoot root k args result
-
-/--
-  Find values that match `e` in `d`.
-
-  The results are ordered so that the longest matches in terms of number of
-  non-star keys are first with ties going to earlier operators first.
--/
-def getMatch (d : LazyDiscrTree α) (e : Expr) : MetaM (Array α × LazyDiscrTree α) :=
-  withReducible <| runMatch d <| (·.toArray) <$> getMatchCore d.roots e
-
-/--
-Structure for quickly initializing a lazy discrimination tree with a large number
-of elements using concurrent functions for generating entries.
--/
-private structure PreDiscrTree (α : Type) where
-  /-- Maps keys to index in tries array. -/
-  roots : HashMap Key Nat := {}
-  /-- Lazy entries for root of trie. -/
-  tries : Array (Array (LazyEntry α)) := #[]
-  deriving Inhabited
-
-namespace PreDiscrTree
-
-private def modifyAt (d : PreDiscrTree α) (k : Key)
-    (f : Array (LazyEntry α) → Array (LazyEntry α)) : PreDiscrTree α :=
-  let { roots, tries } := d
-  match roots.find? k with
-  | .none =>
-    let roots := roots.insert k tries.size
-    { roots, tries := tries.push (f #[]) }
-  | .some i =>
-    { roots, tries := tries.modify i f }
-
-/-- Add an entry to the pre-discrimination tree.-/
-private def push (d : PreDiscrTree α) (k : Key) (e : LazyEntry α) : PreDiscrTree α :=
-  d.modifyAt k (·.push e)
-
-/-- Convert a pre-discrimination tree to a lazy discrimination tree. -/
-private def toLazy (d : PreDiscrTree α) (config : WhnfCoreConfig := {}) : LazyDiscrTree α :=
-  let { roots, tries } := d
-  { config, roots, tries := tries.map (.node {} 0 {}) }
-
-/-- Merge two discrimination trees. -/
-protected def append (x y : PreDiscrTree α) : PreDiscrTree α :=
-  let (x, y, f) :=
-        if x.roots.size ≥ y.roots.size then
-          (x, y, fun y x => x ++ y)
-        else
-          (y, x, fun x y => x ++ y)
-  let { roots := yk, tries := ya } := y
-  yk.fold (init := x) fun d k yi => d.modifyAt k (f ya[yi]!)
-
-instance : Append (PreDiscrTree α) where
-  append := PreDiscrTree.append
-
-end PreDiscrTree
-
-/-- Initial entry in lazy discrimination tree -/
-@[reducible]
-structure InitEntry (α : Type) where
-  /-- Return root key for an entry. -/
-  key : Key
-  /-- Returns rest of entry for later insertion. -/
-  entry : LazyEntry α
-
-namespace InitEntry
-
-/--
-Constructs an initial entry from an expression and value.
--/
-def fromExpr (expr : Expr) (value : α) (config : WhnfCoreConfig := {}) : MetaM (InitEntry α) := do
-  let lctx ← getLCtx
-  let linst ← getLocalInstances
-  let lctx := (lctx, linst)
-  let (key, todo) ← LazyDiscrTree.rootKey config expr
-  pure <| { key, entry := (todo, lctx, value) }
-
-/--
-Creates an entry for a subterm of an initial entry.
-
-This is slightly more efficient than using `fromExpr` on subterms since it avoids a redundant call
-to `whnf`.
--/
-def mkSubEntry (e : InitEntry α) (idx : Nat) (value : α) (config : WhnfCoreConfig := {}) :
-    MetaM (InitEntry α) := do
-  let (todo, lctx, _) := e.entry
-  let (key, todo) ← LazyDiscrTree.rootKey config todo[idx]!
-  pure <| { key, entry := (todo, lctx, value) }
-
-end InitEntry
-
-/-- Information about a failed import. -/
-private structure ImportFailure where
-  /-- Module with constant that import failed on. -/
-  module  : Name
-  /-- Constant that import failed on. -/
-  const   : Name
-  /-- Exception that triggers error. -/
-  exception : Exception
-
-/-- Information generation from imported modules. -/
-private structure ImportData where
-  cache : IO.Ref (Lean.Meta.Cache)
-  errors : IO.Ref (Array ImportFailure)
-
-private def ImportData.new : BaseIO ImportData := do
-  let cache ← IO.mkRef {}
-  let errors ← IO.mkRef #[]
-  pure { cache, errors }
-
-private def addConstImportData
-    (env : Environment)
-    (modName : Name)
-    (d : ImportData)
-    (tree : PreDiscrTree α)
-    (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
-    (name : Name) (constInfo : ConstantInfo) : BaseIO (PreDiscrTree α) := do
-  if constInfo.isUnsafe then return tree
-  if !allowCompletion env name then return tree
-  let mstate : Meta.State := { cache := ←d.cache.get }
-  d.cache.set {}
-  let ctx : Meta.Context := { config := { transparency := .reducible } }
-  let cm := (act name constInfo).run ctx mstate
-  let cctx : Core.Context := {
-    fileName := default,
-    fileMap := default
-  }
-  let cstate : Core.State := {env}
-  match ←(cm.run cctx cstate).toBaseIO with
-  | .ok ((a, ms), _) =>
-    d.cache.set ms.cache
-    pure <| a.foldl (fun t e => t.push e.key e.entry) tree
-  | .error e =>
-    let i : ImportFailure := {
-      module := modName,
-      const := name,
-      exception := e
-    }
-    d.errors.modify (·.push i)
-    pure tree
-
-/--
-Contains the pre discrimination tree and any errors occuring during initialization of
-the library search tree.
--/
-private structure InitResults (α : Type) where
-  tree  : PreDiscrTree α := {}
-  errors : Array ImportFailure := #[]
-
-instance : Inhabited (InitResults α) where
-  default := {}
-
-namespace InitResults
-
-/-- Combine two initial results. -/
-protected def append (x y : InitResults α) : InitResults α :=
-  let { tree := xv, errors := xe } := x
-  let { tree := yv, errors := ye } := y
-  { tree := xv ++ yv, errors := xe ++ ye }
-
-instance : Append (InitResults α) where
-  append := InitResults.append
-
-end InitResults
-
-private def toFlat (d : ImportData) (tree : PreDiscrTree α) :
-    BaseIO (InitResults α) := do
-  let de ← d.errors.swap #[]
-  pure ⟨tree, de⟩
-
-private partial def loadImportedModule (env : Environment)
-    (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
-    (d : ImportData)
-    (tree : PreDiscrTree α)
-    (mname : Name)
-    (mdata : ModuleData)
-    (i : Nat := 0) : BaseIO (PreDiscrTree α) := do
-  if h : i < mdata.constNames.size then
-    let name := mdata.constNames[i]
-    let constInfo  := mdata.constants[i]!
-    let tree ← addConstImportData env mname d tree act name constInfo
-    loadImportedModule env act d tree mname mdata (i+1)
-  else
-    pure tree
-
-private def createImportedEnvironmentSeq (env : Environment)
-    (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
-    (start stop : Nat) : BaseIO (InitResults α) :=
-      do go (← ImportData.new) {} start stop
-    where go d (tree : PreDiscrTree α) (start stop : Nat) : BaseIO _ := do
-            if start < stop then
-              let mname := env.header.moduleNames[start]!
-              let mdata := env.header.moduleData[start]!
-              let tree ← loadImportedModule env act d tree mname mdata
-              go d tree (start+1) stop
-            else
-              toFlat d tree
-    termination_by stop - start
-
-/-- Get the results of each task and merge using combining function -/
-private def combineGet [Append α] (z : α) (tasks : Array (Task α)) : α :=
-  tasks.foldl (fun x t => x ++ t.get) (init := z)
-
-/-- Create an imported environment for tree. -/
-def createImportedEnvironment (env : Environment)
-    (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
-    (constantsPerTask : Nat := 1000) :
-    EIO Exception (LazyDiscrTree α) := do
-  let n := env.header.moduleData.size
-  let rec
-    /-- Allocate constants to tasks according to `constantsPerTask`. -/
-    go tasks start cnt idx := do
-      if h : idx < env.header.moduleData.size then
-        let mdata := env.header.moduleData[idx]
-        let cnt := cnt + mdata.constants.size
-        if cnt > constantsPerTask then
-          let t ← createImportedEnvironmentSeq env act start (idx+1) |>.asTask
-          go (tasks.push t) (idx+1) 0 (idx+1)
-        else
-          go tasks start cnt (idx+1)
-      else
-        if start < n then
-          tasks.push <$> (createImportedEnvironmentSeq env act start n).asTask
-        else
-          pure tasks
-    termination_by env.header.moduleData.size - idx
-  let tasks ← go #[] 0 0 0
-  let r := combineGet default tasks
-  if p : r.errors.size > 0 then
-    throw r.errors[0].exception
-  pure <| r.tree.toLazy

src/Lean/Meta/LitValues.lean

@@ -1,148 +0,0 @@
-/-
-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
--/
-prelude
-import Lean.Meta.Basic
-
-namespace Lean.Meta
-
-/-!
-Helper functions for recognizing builtin literal values.
-This module focus on recognizing the standard representation used in Lean for these literals.
-It also provides support for the following exceptional cases.
-- Raw natural numbers (i.e., natural numbers which are not encoded using `OfNat.ofNat`).
-- Bit-vectors encoded using `OfNat.ofNat` and `BitVec.ofNat`.
-- Negative integers encoded using raw natural numbers.
-- Characters encoded `Char.ofNat n` where `n` can be a raw natural number or an `OfNat.ofNat`.
-- Nested `Expr.mdata`.
--/
-
-/-- Returns `some n` if `e` is a raw natural number, i.e., it is of the form `.lit (.natVal n)`. -/
-def getRawNatValue? (e : Expr) : Option Nat :=
-  match e.consumeMData with
-  | .lit (.natVal n) => some n
-  | _ => none
-
-/-- Return `some (n, type)` if `e` is an `OfNat.ofNat`-application encoding `n` for a type with name `typeDeclName`. -/
-def getOfNatValue? (e : Expr) (typeDeclName : Name) : MetaM (Option (Nat × Expr)) := OptionT.run do
-  let_expr OfNat.ofNat type n _ ← e | failure
-  let type ← whnfD type
-  guard <| type.getAppFn.isConstOf typeDeclName
-  let .lit (.natVal n) := n.consumeMData | failure
-  return (n, type)
-
-/-- Return `some n` if `e` is a raw natural number or an `OfNat.ofNat`-application encoding `n`. -/
-def getNatValue? (e : Expr) : MetaM (Option Nat) := do
-  let e := e.consumeMData
-  if let some n := getRawNatValue? e then
-    return some n
-  let some (n, _) ← getOfNatValue? e ``Nat | return none
-  return some n
-
-/-- Return `some i` if `e` `OfNat.ofNat`-application encoding an integer, or `Neg.neg`-application of one. -/
-def getIntValue? (e : Expr) : MetaM (Option Int) := do
-  if let some (n, _) ← getOfNatValue? e ``Int then
-    return some n
-  let_expr Neg.neg _ _ a ← e | return none
-  let some (n, _) ← getOfNatValue? a ``Int | return none
-  return some (-↑n)
-
-/-- Return `some c` if `e` is a `Char.ofNat`-application encoding character `c`. -/
-def getCharValue? (e : Expr) : MetaM (Option Char) := do
-  let_expr Char.ofNat n ← e | return none
-  let some n ← getNatValue? n | return none
-  return some (Char.ofNat n)
-
-/-- Return `some s` if `e` is of the form `.lit (.strVal s)`. -/
-def getStringValue? (e : Expr) : (Option String) :=
-  match e with
-  | .lit (.strVal s) => some s
-  | _ => none
-
-/-- Return `some ⟨n, v⟩` if `e` is af `OfNat.ofNat` application encoding a `Fin n` with value `v` -/
-def getFinValue? (e : Expr) : MetaM (Option ((n : Nat) × Fin n)) := OptionT.run do
-  let (v, type) ← getOfNatValue? e ``Fin
-  let n ← getNatValue? (← whnfD type.appArg!)
-  match n with
-  | 0 => failure
-  | m+1 => return ⟨m+1, Fin.ofNat v⟩
-
-/-- Return `some ⟨n, v⟩` if `e` is af `OfNat.ofNat` application encoding a `BitVec n` with value `v` -/
-def getBitVecValue? (e : Expr) : MetaM (Option ((n : Nat) × BitVec n)) := OptionT.run do
-  if e.isAppOfArity' ``BitVec.ofNat 2 then
-    let n ← getNatValue? (e.getArg!' 0)
-    let v ← getNatValue? (e.getArg!' 1)
-    return ⟨n, BitVec.ofNat n v⟩
-  let (v, type) ← getOfNatValue? e ``BitVec
-  let n ← getNatValue? (← whnfD type.appArg!)
-  return ⟨n, BitVec.ofNat n v⟩
-
-/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt8` with value `n`. -/
-def getUInt8Value? (e : Expr) : MetaM (Option UInt8) := OptionT.run do
-  let (n, _) ← getOfNatValue? e ``UInt8
-  return UInt8.ofNat n
-
-/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt16` with value `n`. -/
-def getUInt16Value? (e : Expr) : MetaM (Option UInt16) := OptionT.run do
-  let (n, _) ← getOfNatValue? e ``UInt16
-  return UInt16.ofNat n
-
-/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt32` with value `n`. -/
-def getUInt32Value? (e : Expr) : MetaM (Option UInt32) := OptionT.run do
-  let (n, _) ← getOfNatValue? e ``UInt32
-  return UInt32.ofNat n
-
-/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt64` with value `n`. -/
-def getUInt64Value? (e : Expr) : MetaM (Option UInt64) := OptionT.run do
-  let (n, _) ← getOfNatValue? e ``UInt64
-  return UInt64.ofNat n
-
-/--
-If `e` is a literal value, ensure it is encoded using the standard representation.
-Otherwise, just return `e`.
--/
-def normLitValue (e : Expr) : MetaM Expr := do
-  let e ← instantiateMVars e
-  if let some n ← getNatValue? e then return toExpr n
-  if let some n ← getIntValue? e then return toExpr n
-  if let some ⟨_, n⟩ ← getFinValue? e then return toExpr n
-  if let some ⟨_, n⟩ ← getBitVecValue? e then return toExpr n
-  if let some s := getStringValue? e then return toExpr s
-  if let some c ← getCharValue? e then return toExpr c
-  if let some n ← getUInt8Value? e then return toExpr n
-  if let some n ← getUInt16Value? e then return toExpr n
-  if let some n ← getUInt32Value? e then return toExpr n
-  if let some n ← getUInt64Value? e then return toExpr n
-  return e
-
-/--
-If `e` is a `Nat`, `Int`, or `Fin` literal value, converts it into a constructor application.
-Otherwise, just return `e`.
--/
--- TODO: support other builtin literals if needed
-def litToCtor (e : Expr) : MetaM Expr := do
-  let e ← instantiateMVars e
-  if let some n ← getNatValue? e then
-    if n = 0 then
-      return mkConst ``Nat.zero
-    else
-      return .app (mkConst ``Nat.succ) (toExpr (n-1))
-  if let some n ← getIntValue? e then
-    if n < 0 then
-      return .app (mkConst ``Int.negSucc) (toExpr (- (n+1)).toNat)
-    else
-      return .app (mkConst ``Int.ofNat) (toExpr n.toNat)
-  if let some ⟨n, v⟩ ← getFinValue? e then
-    let i := toExpr v.val
-    let n := toExpr n
-    -- Remark: we construct the proof manually here to avoid a cyclic dependency.
-    let p := mkApp4 (mkConst ``LT.lt [0]) (mkConst ``Nat) (mkConst ``instLTNat) i n
-    let h := mkApp3 (mkConst ``of_decide_eq_true) p
-      (mkApp2 (mkConst ``Nat.decLt) i n)
-      (mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Bool) (mkConst ``true))
-    return mkApp3 (mkConst ``Fin.mk) n i h
-  return e
-
-end Lean.Meta

src/Lean/Meta/Match/Basic.lean

@@ -343,7 +343,7 @@ partial def toPattern (e : Expr) : MetaM Pattern := do
         match e.getArg! 1, e.getArg! 3 with
         | Expr.fvar x, Expr.fvar h => return Pattern.as x p h
         | _,           _   => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
-      else if (← isMatchValue e) then
+      else if isMatchValue e then
         return Pattern.val e
       else if e.isFVar then
         return Pattern.var e.fvarId!

src/Lean/Meta/Match/CaseValues.lean

@@ -30,7 +30,7 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa
     let tag ← mvarId.getTag
     mvarId.checkNotAssigned `caseValue
     let target ← mvarId.getType
-    let xEqValue ← mkEq (mkFVar fvarId) (← normLitValue value)
+    let xEqValue ← mkEq (mkFVar fvarId) (foldPatValue value)
     let xNeqValue := mkApp (mkConst `Not) xEqValue
     let thenTarget := Lean.mkForall hName BinderInfo.default xEqValue  target
     let elseTarget := Lean.mkForall hName BinderInfo.default xNeqValue target

src/Lean/Meta/Match/Match.lean

@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.LitValues
 import Lean.Meta.Check
 import Lean.Meta.Closure
-import Lean.Meta.CtorRecognizer
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.GeneralizeTelescope
@@ -96,17 +94,10 @@ private def hasValPattern (p : Problem) : Bool :=
     | .val _ :: _ => true
     | _           => false
 
-private def hasNatValPattern (p : Problem) : MetaM Bool :=
-  p.alts.anyM fun alt => do
-    match alt.patterns with
-    | .val v :: _ => return (← getNatValue? v).isSome
-    | _           => return false
-
-private def hasIntValPattern (p : Problem) : MetaM Bool :=
-  p.alts.anyM fun alt => do
-    match alt.patterns with
-    | .val v :: _ => return (← getIntValue? v).isSome
-    | _           => return false
+private def hasNatValPattern (p : Problem) : Bool :=
+  p.alts.any fun alt => match alt.patterns with
+    | .val v :: _ => v.isNatLit
+    | _           => false
 
 private def hasVarPattern (p : Problem) : Bool :=
   p.alts.any fun alt => match alt.patterns with
@@ -139,21 +130,6 @@ private def isValueTransition (p : Problem) : Bool :=
      | .var _ :: _ => true
      | _           => false
 
-private def isValueOnlyTransitionCore (p : Problem) (isValue : Expr → MetaM Bool) : MetaM Bool := do
-  if hasVarPattern p then return false
-  if !hasValPattern p then return false
-  p.alts.allM fun alt => do
-     match alt.patterns with
-     | .val v :: _   => isValue v
-     | .ctor .. :: _ => return true
-     | _             => return false
-
-private def isFinValueTransition (p : Problem) : MetaM Bool :=
-  isValueOnlyTransitionCore p fun e => return (← getFinValue? e).isSome
-
-private def isBitVecValueTransition (p : Problem) : MetaM Bool :=
-  isValueOnlyTransitionCore p fun e => return (← getBitVecValue? e).isSome
-
 private def isArrayLitTransition (p : Problem) : Bool :=
   hasArrayLitPattern p && hasVarPattern p
   && p.alts.all fun alt => match alt.patterns with
@@ -161,32 +137,13 @@ private def isArrayLitTransition (p : Problem) : Bool :=
      | .var _ :: _       => true
      | _                 => false
 
-private def hasCtorOrInaccessible (p : Problem) : Bool :=
-  !isNextVar p ||
-    p.alts.any fun alt => match alt.patterns with
-    | .ctor .. :: _        => true
-    | .inaccessible _ :: _ => true
-    | _                    => false
-
-private def isNatValueTransition (p : Problem) : MetaM Bool := do
-  unless (← hasNatValPattern p) do return false
-  return hasCtorOrInaccessible p
-
-/--
-Predicate for testing whether we need to expand `Int` value patterns into constructors.
-There are two cases:
-- We have constructor or inaccessible patterns. Example:
-```
-| 0, ...
-| Int.toVal p, ...
-...
-```
-- We don't have the `else`-case (i.e., variable pattern). This can happen
-when the non-value cases are unreachable.
--/
-private def isIntValueTransition (p : Problem) : MetaM Bool := do
-  unless (← hasIntValPattern p) do return false
-  return hasCtorOrInaccessible p || !hasVarPattern p
+private def isNatValueTransition (p : Problem) : Bool :=
+  hasNatValPattern p
+  && (!isNextVar p ||
+      p.alts.any fun alt => match alt.patterns with
+      | .ctor .. :: _        => true
+      | .inaccessible _ :: _ => true
+      | _                    => false)
 
 private def processSkipInaccessible (p : Problem) : Problem := Id.run do
   let x :: xs := p.vars | unreachable!
@@ -416,13 +373,14 @@ private def hasRecursiveType (x : Expr) : MetaM Bool := do
    update the next patterns with the fields of the constructor.
    Otherwise, return none. -/
 def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM (Option Alt) := do
+  let env ← getEnv
   match alt.patterns with
   | p@(.inaccessible e) :: ps =>
     trace[Meta.Match.match] "inaccessible in ctor step {e}"
     withExistingLocalDecls alt.fvarDecls do
       -- Try to push inaccessible annotations.
       let e ← whnfD e
-      match (← constructorApp? e) with
+      match e.constructorApp? env with
       | some (ctorVal, ctorArgs) =>
         if ctorVal.name == ctorName then
           let fields := ctorArgs.extract ctorVal.numParams ctorArgs.size
@@ -503,12 +461,12 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
 private def altsAreCtorLike (p : Problem) : MetaM Bool := withGoalOf p do
   p.alts.allM fun alt => do match alt.patterns with
     | .ctor .. :: _ => return true
-    | .inaccessible e :: _ => isConstructorApp e
+    | .inaccessible e :: _ => return (← whnfD e).isConstructorApp (← getEnv)
     | _ => return false
 
 private def processNonVariable (p : Problem) : MetaM Problem := withGoalOf p do
   let x :: xs := p.vars | unreachable!
-  if let some (ctorVal, xArgs) ← withTransparency .default <| constructorApp'? x then
+  if let some (ctorVal, xArgs) := (← whnfD x).constructorApp? (← getEnv) then
     if (← altsAreCtorLike p) then
       let alts ← p.alts.filterMapM fun alt => do
         match alt.patterns with
@@ -626,46 +584,12 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
       let newAlts := p.alts.filter isFirstPatternVar
       return { p with mvarId := subgoal.mvarId, alts := newAlts, vars := x::xs }
 
-private def expandNatValuePattern (p : Problem) : MetaM Problem := do
-  let alts ← p.alts.mapM fun alt => do
-    match alt.patterns with
-    | .val n :: ps =>
-      match (← getNatValue? n) with
-      | some 0     => return { alt with patterns := .ctor ``Nat.zero [] [] [] :: ps }
-      | some (n+1) => return { alt with patterns := .ctor ``Nat.succ [] [] [.val (toExpr n)] :: ps }
-      | _ => return alt
-    | _ => return alt
-  return { p with alts := alts }
-
-private def expandIntValuePattern (p : Problem) : MetaM Problem := do
-  let alts ← p.alts.mapM fun alt => do
-    match alt.patterns with
-    | .val n :: ps =>
-      match (← getIntValue? n) with
-      | some i =>
-        if i >= 0 then
-        return { alt with patterns := .ctor ``Int.ofNat [] [] [.val (toExpr i.toNat)] :: ps }
-        else
-        return { alt with patterns := .ctor ``Int.negSucc [] [] [.val (toExpr (-(i + 1)).toNat)] :: ps }
-      | _ => return alt
-    | _ => return alt
-  return { p with alts := alts }
-
-private def expandFinValuePattern (p : Problem) : MetaM Problem := do
-  let alts ← p.alts.mapM fun alt => do
-    let .val n :: ps := alt.patterns | return alt
-    let some ⟨n, v⟩ ← getFinValue? n | return alt
-    let p ← mkLt (toExpr v.val) (toExpr n)
-    let h ← mkDecideProof p
-    return { alt with patterns := .ctor ``Fin.mk [] [toExpr n] [.val (toExpr v.val), .inaccessible h] :: ps }
-  return { p with alts := alts }
-
-private def expandBitVecValuePattern (p : Problem) : MetaM Problem := do
-  let alts ← p.alts.mapM fun alt => do
-    let .val n :: ps := alt.patterns | return alt
-    let some ⟨_, v⟩ ← getBitVecValue? n | return alt
-    return { alt with patterns := .ctor ``BitVec.ofFin [] [] [.val (toExpr v.toFin)] :: ps }
-  return { p with alts := alts }
+private def expandNatValuePattern (p : Problem) : Problem :=
+  let alts := p.alts.map fun alt => match alt.patterns with
+    | .val (.lit (.natVal 0)) :: ps     => { alt with patterns := .ctor ``Nat.zero [] [] [] :: ps }
+    | .val (.lit (.natVal (n+1))) :: ps => { alt with patterns := .ctor ``Nat.succ [] [] [.val (mkRawNatLit n)] :: ps }
+    | _                                 => alt
+  { p with alts := alts }
 
 private def traceStep (msg : String) : StateRefT State MetaM Unit := do
   trace[Meta.Match.match] "{msg} step"
@@ -710,18 +634,9 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
     traceStep ("as-pattern")
     let p ← processAsPattern p
     process p
-  else if (← isNatValueTransition p) then
+  else if isNatValueTransition p then
     traceStep ("nat value to constructor")
-    process (← expandNatValuePattern p)
-  else if (← isIntValueTransition p) then
-    traceStep ("int value to constructor")
-    process (← expandIntValuePattern p)
-  else if (← isFinValueTransition p) then
-    traceStep ("fin value to constructor")
-    process (← expandFinValuePattern p)
-  else if (← isBitVecValueTransition p) then
-    traceStep ("bitvec value to constructor")
-    process (← expandBitVecValuePattern p)
+    process (expandNatValuePattern p)
   else if !isNextVar p then
     traceStep ("non variable")
     let p ← processNonVariable p
@@ -739,11 +654,11 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
   else if isArrayLitTransition p then
     let ps ← processArrayLit p
     ps.forM process
-  else if (← hasNatValPattern p) then
+  else if hasNatValPattern p then
     -- This branch is reachable when `p`, for example, is just values without an else-alternative.
     -- We added it just to get better error messages.
     traceStep ("nat value to constructor")
-    process (← expandNatValuePattern p)
+    process (expandNatValuePattern p)
   else
     checkNextPatternTypes p
     throwNonSupported p

src/Lean/Meta/Match/MatchEqs.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.CtorRecognizer
 import Lean.Meta.Match.Match
 import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.Tactic.Apply
@@ -16,35 +15,6 @@ import Lean.Meta.Tactic.Contradiction
 
 namespace Lean.Meta
 
-/--
-A custom, approximated, and quick `contradiction` tactic.
-It only finds contradictions of the form `(h₁ : p)` and `(h₂ : ¬ p)` where
-`p`s are structurally equal. The procedure is not quadratic like `contradiction`.
-
-We use it to improve the performance of `proveSubgoalLoop` at `mkSplitterProof`.
-We will eventually have to write more efficient proof automation for this module.
-The new proof automation should exploit the structure of the generated goals and avoid general purpose tactics
-such as `contradiction`.
--/
-private def _root_.Lean.MVarId.contradictionQuick (mvarId : MVarId) : MetaM Bool := do
-  mvarId.withContext do
-    let mut posMap : HashMap Expr FVarId := {}
-    let mut negMap : HashMap Expr FVarId := {}
-    for localDecl in (← getLCtx) do
-      unless localDecl.isImplementationDetail do
-        if let some p ← matchNot? localDecl.type then
-          if let some pFVarId := posMap.find? p then
-            mvarId.assign (← mkAbsurd (← mvarId.getType) (mkFVar pFVarId) localDecl.toExpr)
-            return true
-          negMap := negMap.insert p localDecl.fvarId
-        if (← isProp localDecl.type) then
-          if let some nFVarId := negMap.find? localDecl.type then
-            mvarId.assign (← mkAbsurd (← mvarId.getType) localDecl.toExpr (mkFVar nFVarId))
-            return true
-          posMap := posMap.insert localDecl.type localDecl.fvarId
-      pure ()
-    return false
-
 /--
   Helper method for `proveCondEqThm`. Given a goal of the form `C.rec ... xMajor = rhs`,
   apply `cases xMajor`. -/
@@ -251,7 +221,7 @@ private def processNextEq : M Bool := do
           return true
         -- If it is not possible, we try to show the hypothesis is redundant by substituting even variables that are not at `s.xs`, and then use contradiction.
         else
-          match (← isConstructorApp? lhs), (← isConstructorApp? rhs) with
+          match lhs.isConstructorApp? (← getEnv), rhs.isConstructorApp? (← getEnv) with
           | some lhsCtor, some rhsCtor =>
             if lhsCtor.name != rhsCtor.name then
               return false -- If the constructors are different, we can discard the hypothesis even if it a heterogeneous equality
@@ -379,14 +349,14 @@ private def injectionAnyCandidate? (type : Expr) : MetaM (Option (Expr × Expr))
       return some (lhs, rhs)
   return none
 
-private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult := do
+private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult :=
   mvarId.withContext do
     for localDecl in (← getLCtx) do
       if let some (lhs, rhs) ← injectionAnyCandidate? localDecl.type then
         unless (← isDefEq lhs rhs) do
           let lhs ← whnf lhs
           let rhs ← whnf rhs
-          unless lhs.isRawNatLit && rhs.isRawNatLit do
+          unless lhs.isNatLit && rhs.isNatLit do
             try
               match (← injection mvarId localDecl.fvarId) with
               | InjectionResult.solved  => return InjectionAnyResult.solved
@@ -597,8 +567,6 @@ where
 
   proveSubgoalLoop (mvarId : MVarId) : MetaM Unit := do
     trace[Meta.Match.matchEqs] "proveSubgoalLoop\n{mvarId}"
-    if (← mvarId.contradictionQuick) then
-      return ()
     match (← injectionAny mvarId) with
     | InjectionAnyResult.solved => return ()
     | InjectionAnyResult.failed =>

src/Lean/Meta/Match/Value.lean

@@ -4,24 +4,45 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.LitValues
 import Lean.Expr
 
 namespace Lean.Meta
 
+-- TODO: move?
+private def UIntTypeNames : Array Name :=
+  #[``UInt8, ``UInt16, ``UInt32, ``UInt64, ``USize]
+
+private def isUIntTypeName (n : Name) : Bool :=
+  UIntTypeNames.contains n
+
+def isFinPatLit (e : Expr) : Bool :=
+  e.isAppOfArity `Fin.ofNat 2 && e.appArg!.isNatLit
+
+/-- Return `some (typeName, numLit)` if `v` is of the form `UInt*.mk (Fin.ofNat _ numLit)` -/
+def isUIntPatLit? (v : Expr) : Option (Name × Expr) :=
+  match v with
+  | Expr.app (Expr.const (Name.str typeName "mk" ..) ..) val .. =>
+    if isUIntTypeName typeName && isFinPatLit val then
+      some (typeName, val.appArg!)
+    else
+      none
+  | _ => none
+
+def isUIntPatLit (v : Expr) : Bool :=
+  isUIntPatLit? v |>.isSome
+
+/--
+  The frontend expands uint numerals occurring in patterns into `UInt*.mk ..` constructor applications.
+  This method convert them back into `UInt*.ofNat ..` applications.
+-/
+def foldPatValue (v : Expr) : Expr :=
+  match isUIntPatLit? v with
+  | some (typeName, numLit) => mkApp (mkConst (Name.mkStr typeName "ofNat")) numLit
+  | _ => v
+
+
 /-- Return true is `e` is a term that should be processed by the `match`-compiler using `casesValues` -/
-def isMatchValue (e : Expr) : MetaM Bool := do
-  let e ← instantiateMVars e
-  if (← getNatValue? e).isSome then return true
-  if (← getIntValue? e).isSome then return true
-  if (← getFinValue? e).isSome then return true
-  if (← getBitVecValue? e).isSome then return true
-  if (getStringValue? e).isSome then return true
-  if (← getCharValue? e).isSome then return true
-  if (← getUInt8Value? e).isSome then return true
-  if (← getUInt16Value? e).isSome then return true
-  if (← getUInt32Value? e).isSome then return true
-  if (← getUInt64Value? e).isSome then return true
-  return false
+def isMatchValue (e : Expr) : Bool :=
+  e.isNatLit || e.isCharLit || e.isStringLit || isFinPatLit e || isUIntPatLit e
 
 end Lean.Meta

src/Lean/Meta/MatchUtil.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Util.Recognizers
 import Lean.Meta.Basic
-import Lean.Meta.CtorRecognizer
 
 namespace Lean.Meta
 
@@ -63,6 +62,8 @@ def matchNe? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
       return none
 
 def matchConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
-  matchHelper? e isConstructorApp?
+  let env ← getEnv
+  matchHelper? e fun e =>
+    return e.isConstructorApp? env
 
 end Lean.Meta

src/Lean/Meta/Reduce.lean

@@ -32,7 +32,7 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta
                 args ← args.modifyM i visit
             else
               args ← args.modifyM i visit
-          if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isRawNatLit then
+          if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isNatLit then
             return mkRawNatLit (args[0]!.natLit?.get! + 1)
           else
             return mkAppN f args

src/Lean/Meta/Tactic/Acyclic.lean

@@ -14,7 +14,7 @@ private def isTarget (lhs rhs : Expr) : MetaM Bool := do
   if !lhs.isFVar || !lhs.occurs rhs then
     return false
   else
-    isConstructorApp' rhs
+    return (← whnf rhs).isConstructorApp (← getEnv)
 
 /--
   Close the given goal if `h` is a proof for an equality such as `as = a :: as`.

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -37,15 +37,6 @@ structure ElimInfo where
   altsInfo   : Array ElimAltInfo := #[]
   deriving Repr, Inhabited
 
-
-/-- Given the type `t` of an alternative, determines the number of parameters
-(.forall and .let)-bound, and whether the conclusion is a `motive`-application.  -/
-def altArity (motive : Expr) (n : Nat) : Expr → Nat × Bool
-  | .forallE _ _ b _ => altArity motive (n+1) b
-  | .letE _ _ _ b _ => altArity motive (n+1) b
-  | conclusion => (n, conclusion.getAppFn == motive)
-
-
 def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do
   let elimType ← inferType elimExpr
   trace[Elab.induction] "eliminator {indentExpr elimExpr}\nhas type{indentExpr elimType}"
@@ -73,7 +64,8 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
       if x != motive && !targets.contains x then
         let xDecl ← x.fvarId!.getDecl
         if xDecl.binderInfo.isExplicit then
-          let (numFields, provesMotive) := altArity motive 0 xDecl.type
+          let (numFields, provesMotive) ← forallTelescopeReducing xDecl.type fun args concl =>
+            pure (args.size, concl.getAppFn == motive)
           let name := xDecl.userName
           let declName? := do
             let base ← baseDeclName?

src/Lean/Meta/Tactic/Injection.lean

@@ -34,19 +34,19 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor
       match type.eq? with
       | none           => throwTacticEx `injection mvarId "equality expected"
       | some (_, a, b) =>
+        let a ← whnf a
+        let b ← whnf b
         let target ← mvarId.getType
-        match (← isConstructorApp'? a), (← isConstructorApp'? b) with
+        let env ← getEnv
+        match a.isConstructorApp? env, b.isConstructorApp? env with
         | some aCtor, some bCtor =>
-          -- We use the default transparency because `a` and `b` may be builtin literals.
-          let val ← withTransparency .default <| mkNoConfusion target prf
+          let val ← mkNoConfusion target prf
           if aCtor.name != bCtor.name then
             mvarId.assign val
             return InjectionResultCore.solved
           else
             let valType ← inferType val
-            -- We use the default transparency setting here because `a` and `b` may be builtin literals
-            -- that need to expanded into constructors.
-            let valType ← whnfD valType
+            let valType ← whnf valType
             match valType with
             | Expr.forallE _ newTarget _ _ =>
               let newTarget := newTarget.headBeta
@@ -111,7 +111,7 @@ where
       if let some (_, lhs, rhs) ← matchEqHEq? (← fvarId.getType) then
         let lhs ← whnf lhs
         let rhs ← whnf rhs
-        if lhs.isRawNatLit && rhs.isRawNatLit then cont
+        if lhs.isNatLit && rhs.isNatLit then cont
         else
           try
             match (← injection mvarId fvarId newNames) with

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -1,421 +0,0 @@
-/-
-Copyright (c) 2021-2023 Gabriel Ebner and Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Joe Hendrix, Scott Morrison
--/
-prelude
-import Init.Data.Nat.MinMax
-import Lean.Meta.LazyDiscrTree
-import Lean.Meta.Tactic.SolveByElim
-import Lean.Util.Heartbeats
-
-/-!
-# Library search
-
-This file defines tactics `exact?` and `apply?`,
-(formerly known as `library_search`)
-and a term elaborator `exact?%`
-that tries to find a lemma
-solving the current goal
-(subgoals are solved using `solveByElim`).
-
-```
-example : x < x + 1 := exact?%
-example : Nat := by exact?
-```
--/
-
-
-namespace Lean.Meta.LibrarySearch
-
-open SolveByElim
-
-/--
-Wrapper for calling `Lean.Meta.SolveByElim.solveByElim with
-appropriate arguments for library search.
--/
-def solveByElim (required : List Expr) (exfalso : Bool) (goals : List MVarId) (maxDepth : Nat) := do
-  let cfg : SolveByElimConfig :=
-    { maxDepth, exfalso := exfalso, symm := true, commitIndependentGoals := true,
-      transparency := ← getTransparency,
-      -- `constructor` has been observed to significantly slow down `exact?` in Mathlib.
-      constructor := false }
-  let ⟨lemmas, ctx⟩ ← SolveByElim.mkAssumptionSet false false [] [] #[]
-  let cfg := if !required.isEmpty then cfg.requireUsingAll required else cfg
-  SolveByElim.solveByElim cfg lemmas ctx goals
-
-/--
-A "modifier" for a declaration.
-* `none` indicates the original declaration,
-* `mp` indicates that (possibly after binders) the declaration is an `↔`,
-  and we want to consider the forward direction,
-* `mpr` similarly, but for the backward direction.
--/
-inductive DeclMod
-  | /-- the original declaration -/ none
-  | /-- the forward direction of an `iff` -/ mp
-  | /-- the backward direction of an `iff` -/ mpr
-deriving DecidableEq, Inhabited, Ord
-
-/--
-LibrarySearch has an extension mechanism for replacing the function used
-to find candidate lemmas.
--/
-@[reducible]
-def CandidateFinder := Expr → MetaM (Array (Name × DeclMod))
-
-namespace DiscrTreeFinder
-
-/-- Adds a path to a discrimination tree. -/
-private def addPath [BEq α] (config : WhnfCoreConfig) (tree : DiscrTree α) (tp : Expr) (v : α) :
-    MetaM (DiscrTree α) := do
-  let k ← DiscrTree.mkPath tp config
-  pure <| tree.insertCore k v
-
-/-- Adds a constant with given name to tree. -/
-private def updateTree (config : WhnfCoreConfig) (tree : DiscrTree (Name × DeclMod))
-    (name : Name) (constInfo : ConstantInfo) : MetaM (DiscrTree (Name × DeclMod)) := do
-  if constInfo.isUnsafe then return tree
-  if !allowCompletion (←getEnv) name then return tree
-  withReducible do
-    let (_, _, type) ← forallMetaTelescope constInfo.type
-    let tree ← addPath config tree type (name, DeclMod.none)
-    match type.getAppFnArgs with
-    | (``Iff, #[lhs, rhs]) => do
-      let tree ← addPath config tree rhs (name, DeclMod.mp)
-      let tree ← addPath config tree lhs (name, DeclMod.mpr)
-      return tree
-    | _ =>
-      return tree
-
-/--
-Constructs an discrimination tree from the current environment.
--/
-def buildImportCache (config : WhnfCoreConfig) : MetaM (DiscrTree (Name × DeclMod)) := do
-  let profilingName := "apply?: init cache"
-  -- Sort so lemmas with longest names come first.
-  let post (A : Array (Name × DeclMod)) :=
-        A.map (fun (n, m) => (n.toString.length, n, m)) |>.qsort (fun p q => p.1 > q.1) |>.map (·.2)
-  profileitM Exception profilingName (← getOptions) do
-    (·.mapArrays post) <$> (← getEnv).constants.map₁.foldM (init := {}) (updateTree config)
-
-/--
-Returns matches from local constants.
--/
-/-
-N.B. The efficiency of this could likely be considerably improved by caching in environment
-extension.
--/
-def localMatches (config : WhnfCoreConfig) (ty : Expr) : MetaM (Array (Name × DeclMod)) := do
-  let locals ← (← getEnv).constants.map₂.foldlM (init := {}) (DiscrTreeFinder.updateTree config)
-  pure <| (← locals.getMatch  ty config).reverse
-
-/--
-Candidate-finding function that uses a strict discrimination tree for resolution.
--/
-def mkImportFinder (config : WhnfCoreConfig) (importTree : DiscrTree (Name × DeclMod))
-    (ty : Expr) : MetaM (Array (Name × DeclMod)) := do
-  pure <| (← importTree.getMatch ty config).reverse
-
-end DiscrTreeFinder
-
-namespace IncDiscrTreeFinder
-
-open LazyDiscrTree (InitEntry createImportedEnvironment)
-
-/--
-The maximum number of constants an individual task may perform.
-
-The value was picked because it roughly correponded to 50ms of work on the machine this was
-developed on.  Smaller numbers did not seem to improve performance when importing Std and larger
-numbers (<10k) seemed to degrade initialization performance.
--/
-private def constantsPerTask : Nat := 6500
-
-private def addImport (name : Name) (constInfo : ConstantInfo) :
-    MetaM (Array (InitEntry (Name × DeclMod))) :=
-  forallTelescope constInfo.type fun _ type => do
-    let e ← InitEntry.fromExpr type (name, DeclMod.none)
-    let a := #[e]
-    if e.key == .const ``Iff 2 then
-      let a := a.push (←e.mkSubEntry 0 (name, DeclMod.mp))
-      let a := a.push (←e.mkSubEntry 1 (name, DeclMod.mpr))
-      pure a
-    else
-      pure a
-
-/--
-Candidate-finding function that uses a strict discrimination tree for resolution.
--/
-def mkImportFinder : IO CandidateFinder := do
-  let ref ← IO.mkRef none
-  pure fun ty => do
-    let importTree ← (←ref.get).getDM $ do
-      profileitM Exception  "librarySearch launch" (←getOptions) $
-        createImportedEnvironment (←getEnv) (constantsPerTask := constantsPerTask) addImport
-    let (imports, importTree) ← importTree.getMatch ty
-    ref.set importTree
-    pure imports
-
-end IncDiscrTreeFinder
-
-initialize registerTraceClass `Tactic.librarySearch
-initialize registerTraceClass `Tactic.librarySearch.lemmas
-
-/-- State for resolving imports -/
-private def LibSearchState := IO.Ref (Option CandidateFinder)
-
-private initialize LibSearchState.default : IO.Ref (Option CandidateFinder) ← do
-  IO.mkRef .none
-
-private instance : Inhabited LibSearchState where
-  default := LibSearchState.default
-
-private initialize ext : EnvExtension LibSearchState ←
-  registerEnvExtension (IO.mkRef .none)
-
-/--
-The preferred candidate finding function.
--/
-initialize defaultCandidateFinder : IO.Ref CandidateFinder ← unsafe do
-  IO.mkRef (←IncDiscrTreeFinder.mkImportFinder)
-
-/--
-Update the candidate finder used by library search.
--/
-def setDefaultCandidateFinder (cf : CandidateFinder) : IO Unit :=
-  defaultCandidateFinder.set cf
-
-/--
-Return an action that returns true when  the remaining heartbeats is less
-than the currently remaining heartbeats * leavePercent / 100.
--/
-def mkHeartbeatCheck (leavePercent : Nat) : MetaM (MetaM Bool) := do
-  let maxHB ← getMaxHeartbeats
-  let hbThreshold := (← getRemainingHeartbeats) * leavePercent / 100
-  -- Return true if we should stop
-  pure $
-    if maxHB = 0 then
-      pure false
-    else do
-      return (← getRemainingHeartbeats) < hbThreshold
-
-private def librarySearchEmoji : Except ε (Option α) → String
-| .error _ => bombEmoji
-| .ok (some _) => crossEmoji
-| .ok none => checkEmoji
-
-/--
-Interleave x y interleaves the elements of x and y until one is empty and then returns
-final elements in other list.
--/
-def interleaveWith {α β γ} (f : α → γ) (x : Array α) (g : β → γ) (y : Array β) : Array γ :=
-    Id.run do
-  let mut res := Array.mkEmpty (x.size + y.size)
-  let n := min x.size y.size
-  for h : i in [0:n] do
-    have p : i < min x.size y.size := h.2
-    have q : i < x.size := Nat.le_trans p (Nat.min_le_left ..)
-    have r : i < y.size := Nat.le_trans p (Nat.min_le_right ..)
-    res := res.push (f x[i])
-    res := res.push (g y[i])
-  let last :=
-        if x.size > n then
-          (x.extract n x.size).map f
-        else
-          (y.extract n y.size).map g
-  pure $ res ++ last
-
-
-/--
-An exception ID that indicates further speculation on candidate lemmas should stop
-and current results should be returned.
--/
-private initialize abortSpeculationId : InternalExceptionId ←
-  registerInternalExceptionId `Std.Tactic.LibrarySearch.abortSpeculation
-
-/--
-Called to abort speculative execution in library search.
--/
-def abortSpeculation [MonadExcept Exception m] : m α :=
-  throw (Exception.internal abortSpeculationId {})
-
-/-- Returns true if this is an abort speculation exception. -/
-def isAbortSpeculation : Exception → Bool
-| .internal id _ => id == abortSpeculationId
-| _ => false
-
-section LibrarySearch
-
-/--
-A library search candidate using symmetry includes the goal to solve, the metavar
-context for that goal, and the name and orientation of a rule to try using with goal.
--/
-@[reducible]
-def Candidate :=  (MVarId × MetavarContext) × (Name × DeclMod)
-
-/--
-Run `searchFn` on both the goal and `symm` applied to the goal.
--/
-def librarySearchSymm (searchFn : CandidateFinder) (goal : MVarId) : MetaM (Array Candidate) := do
-  let tgt ← goal.getType
-  let l1 ← searchFn tgt
-  let coreMCtx ← getMCtx
-  let coreGoalCtx := (goal, coreMCtx)
-  if let some symmGoal ← observing? goal.applySymm then
-    let newType ← instantiateMVars  (← symmGoal.getType)
-    let l2 ← searchFn newType
-    let symmMCtx ← getMCtx
-    let symmGoalCtx := (symmGoal, symmMCtx)
-    setMCtx coreMCtx
-    pure $ interleaveWith (coreGoalCtx, ·) l1 (symmGoalCtx, ·) l2
-  else
-    pure $ l1.map (coreGoalCtx, ·)
-
-private def emoji (e : Except ε α) := if e.toBool then checkEmoji else crossEmoji
-
-/-- Create lemma from name and mod. -/
-def mkLibrarySearchLemma (lem : Name) (mod : DeclMod) : MetaM Expr := do
-  let lem ← mkConstWithFreshMVarLevels lem
-  match mod with
-  | .none => pure lem
-  | .mp => mapForallTelescope (fun e => mkAppM ``Iff.mp #[e]) lem
-  | .mpr => mapForallTelescope (fun e => mkAppM ``Iff.mpr #[e]) lem
-
-private def isVar (e : Expr) : Bool :=
-  match e with
-  | .bvar _ => true
-  | .fvar _ => true
-  | .mvar _ => true
-  | _ => false
-
-private def isNonspecific (type : Expr) : MetaM Bool := do
-  forallTelescope type fun _ tp =>
-    match tp.getAppFn with
-    | .bvar _ => pure true
-    | .fvar _ => pure true
-    | .mvar _ => pure true
-    | .const nm _ =>
-      if nm = ``Eq then
-        pure (tp.getAppArgsN 3 |>.all isVar)
-      else
-        pure false
-    | _ => pure false
-
-/--
-Tries to apply the given lemma (with symmetry modifier) to the goal,
-then tries to close subsequent goals using `solveByElim`.
-If `solveByElim` succeeds, `[]` is returned as the list of new subgoals,
-otherwise the full list of subgoals is returned.
--/
-private def librarySearchLemma (cfg : ApplyConfig) (act : List MVarId → MetaM (List MVarId))
-    (allowFailure : MVarId → MetaM Bool) (cand : Candidate)  : MetaM (List MVarId) := do
-  let ((goal, mctx), (name, mod)) := cand
-  let ppMod (mod : DeclMod) : MessageData :=
-        match mod with | .none => "" | .mp => " with mp" | .mpr => " with mpr"
-  withTraceNode `Tactic.librarySearch (return m!"{emoji ·} trying {name}{ppMod mod} ") do
-    setMCtx mctx
-    let lem ← mkLibrarySearchLemma name mod
-    let lemType ← instantiateMVars (← inferType lem)
-    if ← isNonspecific lemType then
-      failure
-    let newGoals ← goal.apply lem cfg
-    try
-      act newGoals
-    catch _ =>
-      if ← allowFailure goal then
-        pure newGoals
-      else
-        failure
-
-/--
-Sequentially invokes a tactic `act` on each value in candidates on the current state.
-
-The tactic `act` should return a list of meta-variables that still need to be resolved.
-If this list is empty, then no variables remain to be solved, and `tryOnEach` returns
-`none` with the environment set so each goal is resolved.
-
-If the action throws an internal exception with the `abortSpeculationId` id then
-further computation is stopped and intermediate results returned. If any other
-exception is thrown, then it is silently discarded.
--/
-def tryOnEach
-    (act : Candidate → MetaM (List MVarId))
-    (candidates : Array Candidate) :
-    MetaM (Option (Array (List MVarId × MetavarContext))) := do
-  let mut a := #[]
-  let s ← saveState
-  for c in candidates do
-    match ← (tryCatch (Except.ok <$> act c) (pure ∘ Except.error)) with
-    | .error e =>
-      restoreState s
-      if isAbortSpeculation e then
-        break
-    | .ok remaining =>
-      if remaining.isEmpty then
-        return none
-      let ctx ← getMCtx
-      restoreState s
-      a := a.push (remaining, ctx)
-  return (.some a)
-
-private def librarySearch' (goal : MVarId)
-    (tactic : List MVarId → MetaM (List MVarId))
-    (allowFailure : MVarId → MetaM Bool)
-    (leavePercentHeartbeats : Nat) :
-    MetaM (Option (Array (List MVarId × MetavarContext))) := do
-  withTraceNode `Tactic.librarySearch (return m!"{librarySearchEmoji ·} {← goal.getType}") do
-  profileitM Exception "librarySearch" (← getOptions) do
-  let importFinder ← do
-        let r := ext.getState (←getEnv)
-        match ←r.get with
-        | .some f => pure f
-        | .none =>
-          let f ← defaultCandidateFinder.get
-          r.set (.some f)
-          pure f
-  let searchFn (ty : Expr) := do
-      let localMap ← (← getEnv).constants.map₂.foldlM (init := {}) (DiscrTreeFinder.updateTree {})
-      let locals := (← localMap.getMatch  ty {}).reverse
-      pure <| locals ++ (← importFinder ty)
-  -- Create predicate that returns true when running low on heartbeats.
-  let shouldAbort ← mkHeartbeatCheck leavePercentHeartbeats
-  let candidates ← librarySearchSymm searchFn goal
-  let cfg : ApplyConfig := { allowSynthFailures := true }
-  let act := fun cand => do
-      if ←shouldAbort then
-        abortSpeculation
-      librarySearchLemma cfg tactic allowFailure cand
-  tryOnEach act candidates
-
-/--
-Tries to solve the goal either by:
-* calling `tactic true`
-* or applying a library lemma then calling `tactic false` on the resulting goals.
-
-Typically here `tactic` is `solveByElim`,
-with the `Bool` flag indicating whether it may retry with `exfalso`.
-
-If it successfully closes the goal, returns `none`.
-Otherwise, it returns `some a`, where `a : Array (List MVarId × MetavarContext)`,
-with an entry for each library lemma which was successfully applied,
-containing a list of the subsidiary goals, and the metavariable context after the application.
-
-(Always succeeds, and the metavariable context stored in the monad is reverted,
-unless the goal was completely solved.)
-
-(Note that if `solveByElim` solves some but not all subsidiary goals,
-this is not currently tracked.)
--/
-def librarySearch (goal : MVarId)
-    (tactic : Bool → List MVarId → MetaM (List MVarId) :=
-      fun initial g => solveByElim [] (maxDepth := 6) (exfalso := initial) g)
-    (allowFailure : MVarId → MetaM Bool := fun _ => pure true)
-    (leavePercentHeartbeats : Nat := 10) :
-    MetaM (Option (Array (List MVarId × MetavarContext))) := do
-  (tactic true [goal] *> pure none) <|>
-  librarySearch' goal (tactic false) allowFailure leavePercentHeartbeats
-
-end LibrarySearch
-
-end Lean.Meta.LibrarySearch

src/Lean/Meta/Tactic/NormCast.lean

@@ -3,9 +3,8 @@ Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
 -/
-prelude
 import Lean.Meta.CongrTheorems
-import Lean.Meta.Tactic.Simp.Attr
+import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.CoeAttr
 
 namespace Lean.Meta.NormCast

src/Lean/Meta/Tactic/Rewrite.lean

@@ -8,7 +8,6 @@ import Lean.Meta.AppBuilder
 import Lean.Meta.MatchUtil
 import Lean.Meta.KAbstract
 import Lean.Meta.Check
-import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Apply
 
 namespace Lean.Meta
@@ -54,7 +53,6 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           let u2 ← getLevel eType
           let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq
           postprocessAppMVars `rewrite mvarId newMVars binderInfos
-            (synthAssignedInstances := !tactic.skipAssignedInstances.get (← getOptions))
           let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
           let otherMVarIds ← getMVarsNoDelayed eqPrf
           let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)

src/Lean/Meta/Tactic/Simp.lean

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

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

@@ -1,74 +0,0 @@
-/-
-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
--/
-prelude
-import Lean.Meta.Tactic.Simp.Types
-import Lean.Meta.Tactic.Simp.SimpTheorems
-import Lean.Meta.Tactic.Simp.Simproc
-
-namespace Lean.Meta
-open Simp
-
-def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
-    (ref : Name := by exact decl_name%) : IO Unit :=
-  registerBuiltinAttribute {
-    ref   := ref
-    name  := attrName
-    descr := attrDescr
-    applicationTime := AttributeApplicationTime.afterCompilation
-    add   := fun declName stx attrKind => do
-      if (← isSimproc declName <||> isBuiltinSimproc declName) then
-        let simprocAttrName := simpAttrNameToSimprocAttrName attrName
-        Attribute.add declName simprocAttrName stx attrKind
-      else
-        let go : MetaM Unit := do
-          let info ← getConstInfo declName
-          let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-          let prio ← getAttrParamOptPrio stx[2]
-          if (← isProp info.type) then
-            addSimpTheorem ext declName post (inv := false) attrKind prio
-          else if info.hasValue then
-            if let some eqns ← getEqnsFor? declName then
-              for eqn in eqns do
-                addSimpTheorem ext eqn post (inv := false) attrKind prio
-              ext.add (SimpEntry.toUnfoldThms declName eqns) attrKind
-              if hasSmartUnfoldingDecl (← getEnv) declName then
-                ext.add (SimpEntry.toUnfold declName) attrKind
-            else
-              ext.add (SimpEntry.toUnfold declName) attrKind
-          else
-            throwError "invalid 'simp', it is not a proposition nor a definition (to unfold)"
-        discard <| go.run {} {}
-    erase := fun declName => do
-      if (← isSimproc declName <||> isBuiltinSimproc declName) then
-        let simprocAttrName := simpAttrNameToSimprocAttrName attrName
-        Attribute.erase declName simprocAttrName
-      else
-        let s := ext.getState (← getEnv)
-        let s ← s.erase (.decl declName)
-        modifyEnv fun env => ext.modifyState env fun _ => s
-  }
-
-def registerSimpAttr (attrName : Name) (attrDescr : String)
-    (ref : Name := by exact decl_name%) : IO SimpExtension := do
-  let ext ← mkSimpExt ref
-  mkSimpAttr attrName attrDescr ext ref -- Remark: it will fail if it is not performed during initialization
-  simpExtensionMapRef.modify fun map => map.insert attrName ext
-  return ext
-
-builtin_initialize simpExtension : SimpExtension ← registerSimpAttr `simp "simplification theorem"
-
-builtin_initialize sevalSimpExtension : SimpExtension ← registerSimpAttr `seval "symbolic evaluator theorem"
-
-def getSimpTheorems : CoreM SimpTheorems :=
-  simpExtension.getTheorems
-
-def getSEvalTheorems : CoreM SimpTheorems :=
-  sevalSimpExtension.getTheorems
-
-def Simp.Context.mkDefault : MetaM Context :=
-  return { config := {}, simpTheorems := #[(← Meta.getSimpTheorems)], congrTheorems := (← Meta.getSimpCongrTheorems) }
-
-end Lean.Meta

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

@@ -4,12 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Init.Data.BitVec.Basic
 
-namespace BitVec
+namespace Std.BitVec
 open Lean Meta Simp
 
 /-- A bit-vector literal -/
@@ -20,12 +19,38 @@ structure Literal where
   value : BitVec n
 
 /--
-Try to convert `OfNat.ofNat`/`BitVec.OfNat` application into a
+Try to convert an `OfNat.ofNat`-application into a bitvector literal.
+-/
+private def fromOfNatExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isAppOfArity ``BitVec 1)
+  let n ← Nat.fromExpr? type.appArg!
+  let v ← Nat.fromExpr? e.appFn!.appArg!
+  return { n, value := BitVec.ofNat n v }
+
+/--
+Try to convert an `Std.BitVec.ofNat`-application into a bitvector literal.
+-/
+private def fromBitVecExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  guard (e.isAppOfArity ``Std.BitVec.ofNat 2)
+  let n ← Nat.fromExpr? e.appFn!.appArg!
+  let v ← Nat.fromExpr? e.appArg!
+  return { n, value := BitVec.ofNat n v }
+
+/--
+Try to convert `OfNat.ofNat`/`Std.BitVec.OfNat` application into a
 bitvector literal.
 -/
-def fromExpr? (e : Expr) : SimpM (Option Literal) := do
-  let some ⟨n, value⟩ ← getBitVecValue? e | return none
-  return some { n, value }
+def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  fromBitVecExpr? e <|> fromOfNatExpr? e
+
+/--
+Convert a bitvector literal into an expression.
+-/
+-- Using `Std.BitVec.ofNat` because it is being used in `simp` theorems
+def Literal.toExpr (lit : Literal) : Expr :=
+  mkApp2 (mkConst ``Std.BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
 
 /--
 Helper function for reducing homogenous unary bitvector operators.
@@ -34,7 +59,8 @@ Helper function for reducing homogenous unary bitvector operators.
     (op : {n : Nat} → BitVec n → BitVec n) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op v.value) }
+  let v := { v with value := op v.value }
+  return .done { expr := v.toExpr }
 
 /--
 Helper function for reducing homogenous binary bitvector operators.
@@ -46,7 +72,8 @@ Helper function for reducing homogenous binary bitvector operators.
   let some v₂ ← fromExpr? e.appArg! | return .continue
   if h : v₁.n = v₂.n then
     trace[Meta.debug] "reduce [{declName}] {v₁.value}, {v₂.value}"
-    return .done { expr := toExpr (op v₁.value (h ▸ v₂.value)) }
+    let v := { v₁ with value := op v₁.value (h ▸ v₂.value) }
+    return .done { expr := v.toExpr }
   else
     return .continue
 
@@ -56,7 +83,8 @@ Helper function for reducing homogenous binary bitvector operators.
   unless e.isAppOfArity declName 3 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
   let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  return .done { expr := toExpr (op n v.value) }
+  let lit : Literal := { n, value := op n v.value }
+  return .done { expr := lit.toExpr }
 
 /--
 Helper function for reducing bitvector functions such as `getLsb` and `getMsb`.
@@ -77,7 +105,8 @@ Helper function for reducing bitvector functions such as `shiftLeft` and `rotate
   unless e.isAppOfArity declName arity do return .continue
   let some v ← fromExpr? e.appFn!.appArg! | return .continue
   let some i ← Nat.fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op v.value i) }
+  let v := { v with value := op v.value i }
+  return .done { expr := v.toExpr }
 
 /--
 Helper function for reducing bitvector predicates.
@@ -162,45 +191,48 @@ builtin_simproc [simp, seval] reduceRotateRight (BitVec.rotateRight _ _) :=
 
 /-- Simplification procedure for append on `BitVec`. -/
 builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : BitVec _)) := fun e => do
-  let_expr HAppend.hAppend _ _ _ _ a b ← e | return .continue
-  let some v₁ ← fromExpr? a | return .continue
-  let some v₂ ← fromExpr? b | return .continue
-  return .done { expr := toExpr (v₁.value ++ v₂.value) }
+  unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← fromExpr? e.appArg! | return .continue
+  let v : Literal := { n := v₁.n + v₂.n, value := v₁.value ++ v₂.value }
+  return .done { expr := v.toExpr }
 
 /-- Simplification procedure for casting `BitVec`s along an equality of the size. -/
 builtin_simproc [simp, seval] reduceCast (cast _ _) := fun e => do
-  let_expr cast _ m _ v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  let some m ← Nat.fromExpr? m | return .continue
-  return .done { expr := toExpr (BitVec.ofNat m v.value.toNat) }
+  unless e.isAppOfArity ``cast 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some m ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  let v : Literal := { n := m, value := BitVec.ofNat m v.value.toNat }
+  return .done { expr := v.toExpr }
 
 /-- Simplification procedure for `BitVec.toNat`. -/
 builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
-  let_expr BitVec.toNat _ v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
+  unless e.isAppOfArity ``BitVec.toNat 2 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
   return .done { expr := mkNatLit v.value.toNat }
 
 /-- Simplification procedure for `BitVec.toInt`. -/
 builtin_simproc [simp, seval] reduceToInt (BitVec.toInt _) := fun e => do
-  let_expr BitVec.toInt _ v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  return .done { expr := toExpr v.value.toInt }
+  unless e.isAppOfArity ``BitVec.toInt 2 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  return .done { expr := Int.toExpr v.value.toInt }
 
 /-- Simplification procedure for `BitVec.ofInt`. -/
 builtin_simproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
-  let_expr BitVec.ofInt n i ← e | return .continue
-  let some n ← Nat.fromExpr? n | return .continue
-  let some i ← Int.fromExpr? i | return .continue
-  return .done { expr := toExpr (BitVec.ofInt n i) }
+  unless e.isAppOfArity ``BitVec.ofInt 2 do return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let some i ← Int.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n, value := BitVec.ofInt n i }
+  return .done { expr := lit.toExpr }
 
 /-- Simplification procedure for ensuring `BitVec.ofNat` literals are normalized. -/
 builtin_simproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
-  let_expr BitVec.ofNat n v ← e | return .continue
-  let some n ← Nat.fromExpr? n | return .continue
-  let some v ← Nat.fromExpr? v | return .continue
+  unless e.isAppOfArity ``BitVec.ofNat 2 do return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let some v ← Nat.fromExpr? e.appArg! | return .continue
   let bv := BitVec.ofNat n v
   if bv.toNat == v then return .continue -- already normalized
-  return .done { expr := toExpr (BitVec.ofNat n v) }
+  return .done { expr := { n, value := BitVec.ofNat n v : Literal }.toExpr }
 
 /-- Simplification procedure for `<` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)
@@ -226,35 +258,39 @@ builtin_simproc [simp, seval] reduceSLE (BitVec.sle _ _) :=
 
 /-- Simplification procedure for `zeroExtend'` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
-  let_expr zeroExtend' _ w _ v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  let some w ← Nat.fromExpr? w | return .continue
+  unless e.isAppOfArity ``zeroExtend' 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some w ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
   if h : v.n ≤ w then
-    return .done { expr := toExpr (v.value.zeroExtend' h) }
+    let lit : Literal := { n := w, value := v.value.zeroExtend' h }
+    return .done { expr := lit.toExpr }
   else
     return .continue
 
 /-- Simplification procedure for `shiftLeftZeroExtend` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _ _) := fun e => do
-  let_expr shiftLeftZeroExtend _ v m ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  let some m ← Nat.fromExpr? m | return .continue
-  return .done { expr := toExpr (v.value.shiftLeftZeroExtend m) }
+  unless e.isAppOfArity ``shiftLeftZeroExtend 3 do return .continue
+  let some v ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← Nat.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n := v.n + m, value := v.value.shiftLeftZeroExtend m }
+  return .done { expr := lit.toExpr }
 
 /-- Simplification procedure for `extractLsb'` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => do
-  let_expr extractLsb' _ start len v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  let some start ← Nat.fromExpr? start | return .continue
-  let some len ← Nat.fromExpr? len | return .continue
-  return .done { expr := toExpr (v.value.extractLsb' start len) }
+  unless e.isAppOfArity ``extractLsb' 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some start ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  let some len ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let lit : Literal := { n := len, value := v.value.extractLsb' start len }
+  return .done { expr := lit.toExpr }
 
 /-- Simplification procedure for `replicate` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
-  let_expr replicate _ i v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  let some i ← Nat.fromExpr? i | return .continue
-  return .done { expr := toExpr (v.value.replicate i) }
+  unless e.isAppOfArity ``replicate 3 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some w ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let lit : Literal := { n := v.n * w, value := v.value.replicate w }
+  return .done { expr := lit.toExpr }
 
 /-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
@@ -264,8 +300,9 @@ builtin_simproc [simp, seval] reduceSignExtend (signExtend _ _) := reduceExtend
 
 /-- Simplification procedure for `allOnes` -/
 builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
-  let_expr allOnes n ← e | return .continue
-  let some n ← Nat.fromExpr? n | return .continue
-  return .done { expr := toExpr (allOnes n) }
+  unless e.isAppOfArity ``allOnes 1 do return .continue
+  let some n ← Nat.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n, value := allOnes n }
+  return .done { expr := lit.toExpr }
 
-end BitVec
+end Std.BitVec

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

@@ -3,16 +3,16 @@ 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
 -/
-prelude
 import Lean.ToExpr
-import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 
 namespace Char
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Char) :=
-  getCharValue? e
+def fromExpr? (e : Expr) : SimpM (Option Char) := OptionT.run do
+  guard (e.isAppOfArity ``Char.ofNat 1)
+  let value ← Nat.fromExpr? e.appArg!
+  return Char.ofNat value
 
 @[inline] def reduceUnary [ToExpr α] (declName : Name) (op : Char → α) (arity : Nat := 1) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -42,9 +42,9 @@ builtin_simproc [simp, seval] reduceIsDigit (Char.isDigit _) := reduceUnary ``Ch
 builtin_simproc [simp, seval] reduceIsAlphaNum (Char.isAlphanum _) := reduceUnary ``Char.isAlphanum Char.isAlphanum
 builtin_simproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnary ``toString toString 3
 builtin_simproc [simp, seval] reduceVal (Char.val _) := fun e => do
-  let_expr Char.val arg ← e | return .continue
-  let some c ← fromExpr? arg | return .continue
-  return .done { expr := toExpr c.val }
+  unless e.isAppOfArity ``Char.val 1 do return .continue
+  let some c ← fromExpr? e.appArg! | return .continue
+  return .done { expr := UInt32.toExprCore c.val }
 builtin_simproc [simp, seval] reduceEq  (( _ : Char) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Char) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
 builtin_simproc [simp, seval] reduceBEq  (( _ : Char) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
@@ -60,12 +60,12 @@ builtin_simproc ↓ [simp, seval] isValue (Char.ofNat _ ) := fun e => do
   return .done { expr := e }
 
 builtin_simproc [simp, seval] reduceOfNatAux (Char.ofNatAux _ _) := fun e => do
-  let_expr Char.ofNatAux n _ ← e | return .continue
-  let some n ← Nat.fromExpr? n | return .continue
+  unless e.isAppOfArity ``Char.ofNatAux 2 do return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
   return .done { expr := toExpr (Char.ofNat n) }
 
 builtin_simproc [simp, seval] reduceDefault ((default : Char)) := fun e => do
-  let_expr default _ _ ← e | return .continue
+  unless e.isAppOfArity ``default 2 do return .continue
   return .done { expr := toExpr (default : Char) }
 
 end Char

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

@@ -10,29 +10,33 @@ import Lean.Meta.Tactic.Simp.Simproc
 open Lean Meta Simp
 
 builtin_simproc ↓ [simp, seval] reduceIte (ite _ _ _) := fun e => do
-  let_expr f@ite α c i tb eb ← e | return .continue
+  unless e.isAppOfArity ``ite 5 do return .continue
+  let c := e.getArg! 1
   let r ← simp c
   if r.expr.isTrue then
-    let pr    := mkApp (mkApp5 (mkConst ``ite_cond_eq_true f.constLevels!) α c i tb eb) (← r.getProof)
-    return .visit { expr := tb, proof? := pr }
+    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.isFalse then
-    let pr    := mkApp (mkApp5 (mkConst ``ite_cond_eq_false f.constLevels!) α c i tb eb) (← r.getProof)
-    return .visit { expr := eb, proof? := pr }
+    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 }
   return .continue
 
 builtin_simproc ↓ [simp, seval] reduceDite (dite _ _ _) := fun e => do
-  let_expr f@dite α c i tb eb ← e | return .continue
+  unless e.isAppOfArity ``dite 5 do return .continue
+  let c := e.getArg! 1
   let r ← simp c
   if r.expr.isTrue then
     let pr    ← r.getProof
     let h     := mkApp2 (mkConst ``of_eq_true) c pr
-    let eNew  := mkApp tb h |>.headBeta
-    let prNew := mkApp (mkApp5 (mkConst ``dite_cond_eq_true f.constLevels!) α c i tb eb) 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.isFalse then
     let pr    ← r.getProof
     let h     := mkApp2 (mkConst ``of_eq_false) c pr
-    let eNew  := mkApp eb h |>.headBeta
-    let prNew := mkApp (mkApp5 (mkConst ``dite_cond_eq_false f.constLevels!) α c i tb eb) 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 }
   return .continue

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

@@ -5,29 +5,37 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ToExpr
-import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
 namespace Fin
 open Lean Meta Simp
 
 structure Value where
-  n     : Nat
-  value : Fin n
+  ofNatFn   : Expr
+  size      : Nat
+  value     : Nat
 
-def fromExpr? (e : Expr) : SimpM (Option Value) := do
-  let some ⟨n, value⟩ ← getFinValue? e | return none
-  return some { n, value }
+def fromExpr? (e : Expr) : SimpM (Option Value) := OptionT.run do
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isAppOfArity ``Fin 1)
+  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! }
 
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : {n : Nat} → Fin n → Fin n → Fin n) (e : Expr) : SimpM Step := do
+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) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  if h : v₁.n = v₂.n then
-    let v := op v₁.value (h ▸ v₂.value)
-    return .done { expr := toExpr v }
-  else
-    return .continue
+  unless v₁.size == v₂.size do return .continue
+  let v := { v₁ with value := op v₁.value v₂.value % v₁.size }
+  return .done { expr := v.toExpr }
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -63,12 +71,12 @@ builtin_simproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred
 
 /-- Simplification procedure for ensuring `Fin` literals are normalized. -/
 builtin_simproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
-  let some ⟨n, v⟩ ← getFinValue? e | return .continue
-  let some m ← getNatValue? e.appFn!.appArg! | return .continue
-  if n == m then
+  let some v ← fromExpr? e | return .continue
+  let v' ← Nat.fromExpr? e.appFn!.appArg!
+  if v.value == v' then
     -- Design decision: should we return `.continue` instead of `.done` when simplifying.
     -- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`
     return .done { expr := e }
-  return .done { expr := toExpr v }
+  return .done { expr := v.toExpr }
 
 end Fin

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

@@ -5,14 +5,33 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ToExpr
-import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
 namespace Int
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Int) :=
-  getIntValue? e
+def fromExpr? (e : Expr) : SimpM (Option Int) := OptionT.run do
+  let mut e := e
+  let mut isNeg := false
+  if e.isAppOfArity ``Neg.neg 3 then
+    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) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -57,7 +76,7 @@ builtin_simproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do
 
 /-- Return `.done` for positive Int values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do
-  let_expr OfNat.ofNat _ _ _ ← e | return .continue
+  unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue
   return .done { expr := e }
 
 builtin_simproc [simp, seval] reduceAdd ((_ + _ : Int)) := reduceBin ``HAdd.hAdd 6 (· + ·)
@@ -67,9 +86,9 @@ builtin_simproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv
 builtin_simproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
 
 builtin_simproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
-  let_expr HPow.hPow _ _ _ _ a b ← e | return .continue
-  let some v₁ ← fromExpr? a | return .continue
-  let some v₂ ← Nat.fromExpr? b | return .continue
+  unless e.isAppOfArity ``HPow.hPow 6 do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← Nat.fromExpr? e.appArg! | return .continue
   return .done { expr := toExpr (v₁ ^ v₂) }
 
 builtin_simproc [simp, seval] reduceLT  (( _ : Int) < _)  := reduceBinPred ``LT.lt 4 (. < .)

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

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Simproc
-import Lean.Meta.LitValues
 import Lean.Meta.Offset
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
@@ -13,19 +12,20 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
 namespace Nat
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Nat) :=
-  getNatValue? e
+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) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op n) }
+  return .done { expr := mkNatLit (op n) }
 
 @[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op n m) }
+  return .done { expr := mkNatLit (op n m) }
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -65,7 +65,7 @@ builtin_simproc [simp, seval] reduceBNe  (( _ : Nat) != _)  := reduceBoolPred ``
 
 /-- Return `.done` for Nat values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do
-  let_expr OfNat.ofNat _ _ _ ← e | return .continue
+  unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue
   return .done { expr := e }
 
 end Nat