chore: add empty test out

Else the `case` will now allow introducing all necessary variables.

Induction principles with `let` in the types of the cases will be more
common with #3432.

This implementation no longer reduces the type as it goes, but really
only counts
manifest foralls and lets. I find this more sensible and predictable: If
you have
```
theorem induction₂_symm {P : EReal → EReal → Prop} (symm : Symmetric P) …
```
then previously, writing
```
case symm => 
```
would actually bring a fresh `x` and `y` and variable `h : P x y` into
scope and produce a
goal of `P y x`, because `Symmetric P` happens to be
```
def Symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x
```

After this change, after `case symm =>` will leave `Symmetric P` as the
goal.

This gives more control to the author of the induction hypothesis about
the actual
goal of the cases. This shows up in mathlib in two places; fixes in
https://github.com/leanprover-community/mathlib4/pull/11023.
I consider these improvements.

.github/workflows/check-prelude.yml

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

RELEASES.md

@@ -81,6 +81,8 @@ 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)
+
 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

script/prepare-llvm-linux.sh

@@ -25,6 +25,8 @@ 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/
 
@@ -60,7 +62,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 -static-libgcc -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 -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/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.
 -/
-@[inline, coe_decl] def Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u}
+@[coe_decl] abbrev 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.
 -/
-@[inline, coe_decl] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u}
+@[coe_decl] abbrev 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,3 +185,84 @@ 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,16 +8,6 @@ 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`. -/
@@ -29,10 +19,6 @@ 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,8 +8,6 @@ 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
@@ -35,6 +33,8 @@ 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`.
@@ -166,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 : Format) ++ "#" ++ repr n
+instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
 instance : ToString (BitVec n) where toString a := toString (repr a)
 
 end repr_toString
@@ -606,3 +606,5 @@ 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 Std.BitVec
+namespace 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_one c
+  have : c.toNat ≤ 1 := Bool.toNat_le c
   rw [Nat.pow_succ]
   omega
 
@@ -173,3 +173,5 @@ 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 Std.BitVec
+namespace BitVec
 
 /--
 iunfoldr is an iterative operation that applies a function `f` repeatedly.
@@ -57,3 +57,5 @@ 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 Std.BitVec
+namespace BitVec
 
 /--
 This normalized a bitvec using `ofFin` to `ofNat`.
@@ -445,6 +445,15 @@ 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]
@@ -589,3 +598,19 @@ 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,11 +217,13 @@ def toNat (b:Bool) : Nat := cond b 1 0
 
 @[simp] theorem toNat_true : true.toNat = 1 := rfl
 
-theorem toNat_le_one (c:Bool) : c.toNat ≤ 1 := by
+theorem toNat_le (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_one _)
+  Nat.lt_succ_of_le (toNat_le _)
 
 @[simp] theorem toNat_eq_zero (b : Bool) : b.toNat = 0 ↔ b = false := by
   cases b <;> simp

src/Init/Data/List/Lemmas.lean

@@ -665,3 +665,47 @@ 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))
+
+#print get
+#print set
+
+@[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/Meta.lean

@@ -1362,6 +1362,19 @@ 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,6 +503,25 @@ 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
@@ -532,3 +551,92 @@ 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,19 +170,6 @@ 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
   | `($(_)) => `(())
 
@@ -466,3 +453,19 @@ 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
-`Std.Tactic.Omega.Coeffs.IntDict` instead of `Std.Tactic.Omega.Coeffs.IntList`.
+`Init.Omega.IntDict` instead of `Init.Omega.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 `Std.Tactic.Omega` namespace.
+but unlikely to be widely useful, so are inside the `Lean.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 `Std.Tactic.Omega` namespace.
+so are hidden in the `Lean.Omega` namespace.
 
 If you find yourself needing them elsewhere, please move them first to another file.
 -/

src/Init/Prelude.lean

@@ -947,7 +947,8 @@ 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.

src/Init/Tactics.lean

@@ -1287,6 +1287,25 @@ 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
+
 end Tactic
 
 namespace Attr
@@ -1406,13 +1425,14 @@ 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`
+where `i < arr.size` is in the context) and `simp_arith` and `omega`
 (for doing linear arithmetic in the index).
 -/
 syntax "get_elem_tactic_trivial" : tactic
 
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
+macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)
 
 /--
 `get_elem_tactic` is the tactic automatically called by the notation `arr[i]`
@@ -1438,3 +1458,9 @@ 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,7 +22,8 @@ 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| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
 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,6 +5,7 @@ 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
@@ -619,7 +620,7 @@ where
       let rhs ← liftMetaM do Meta.whnf args[inductVal.numParams + inductVal.numIndices + 2]!
       let lhs := lhs.toCtorIfLit
       let rhs := rhs.toCtorIfLit
-      match lhs.isConstructorApp? (← getEnv), rhs.isConstructorApp? (← getEnv) with
+      match (← liftMetaM <| Meta.isConstructorApp? lhs), (← liftMetaM <| Meta.isConstructorApp? rhs) with
       | some lhsCtorVal, some rhsCtorVal =>
         if lhsCtorVal.name == rhsCtorVal.name then
           etaIfUnderApplied e (arity+1) do

src/Lean/Data/Json/Basic.lean

@@ -8,6 +8,7 @@ prelude
 import Init.Data.List.Control
 import Init.Data.Range
 import Init.Data.OfScientific
+import Init.Data.Hashable
 import Lean.Data.RBMap
 namespace Lean
 
@@ -15,7 +16,7 @@ namespace Lean
 structure JsonNumber where
   mantissa : Int
   exponent : Nat
-  deriving DecidableEq
+  deriving DecidableEq, Hashable
 
 namespace JsonNumber
 
@@ -205,6 +206,19 @@ 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
-  data? : any -/
+  command? : Command -/
   deriving FromJson, ToJson, Inhabited
 
 structure CompletionList where
@@ -274,7 +274,7 @@ structure CallHierarchyItem where
   uri            : DocumentUri
   range          : Range
   selectionRange : Range
-  -- data? : Option unknown
+  data?          : Option Json := none
   deriving FromJson, ToJson, BEq, Hashable, Inhabited
 
 structure CallHierarchyIncomingCallsParams where

src/Lean/Data/Lsp/Utf16.lean

@@ -86,6 +86,10 @@ 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/Elab.lean

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

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 `($_:ident) := term then
+    if let `($id:ident) := term then
       try
         for c in (← resolveGlobalConstWithInfos term) do
-          addCompletionInfo <| .id term c (danglingDot := false) {} none
+          addCompletionInfo <| .id term id.getId (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,6 +99,14 @@ 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) =>
@@ -158,7 +166,10 @@ 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 _ _ =>
+@[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?
   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

@@ -0,0 +1,95 @@
+/-
+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,7 +347,21 @@ def elabMutual : CommandElab := fun stx => do
   let attrs ← elabAttrs attrInsts
   let idents := stx[4].getArgs
   for ident in idents do withRef ident <| liftTermElabM do
-    let declName ← resolveGlobalConstNoOverloadWithInfo ident
+    /-
+    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
     Term.applyAttributes declName attrs
     for attrName in toErase do
       Attribute.erase declName attrName

src/Lean/Elab/GuardMsgs.lean

@@ -0,0 +1,136 @@
+/-
+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,14 +49,25 @@ 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
+  | 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
 
 def CustomInfo.format : CustomInfo → Format
   | i => f!"CustomInfo({i.value.typeName})"

src/Lean/Elab/Match.lean

@@ -5,6 +5,7 @@ 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
@@ -442,7 +443,7 @@ private def applyRefMap (e : Expr) (map : ExprMap Expr) : Expr :=
 -/
 private def whnfPreservingPatternRef (e : Expr) : MetaM Expr := do
   let eNew ← whnf e
-  if eNew.isConstructorApp (← getEnv) then
+  if (← isConstructorApp eNew) then
     return eNew
   else
     return applyRefMap eNew (mkPatternRefMap e)
@@ -473,7 +474,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
@@ -571,8 +572,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 e
+      else if (← isMatchValue e) then
+        return Pattern.val (← normLitValue e)
       else if e.isFVar then
         return Pattern.var e.fvarId!
       else

src/Lean/Elab/Notation.lean

@@ -107,22 +107,10 @@ 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,6 +5,7 @@ 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
@@ -218,13 +219,14 @@ where
 -/
 private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
   let env ← getEnv
-  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
+  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 _
 
 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,8 +121,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       preDefs.forM (·.termination.ensureNone "partial")
     else
       try
-        let hasHints := preDefs.any  fun preDef =>
-          preDef.termination.decreasing_by?.isSome || preDef.termination.termination_by?.isSome
+        let hasHints := preDefs.any fun preDef => preDef.termination.isNotNone
         if hasHints then
           wfRecursion preDefs
         else

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

@@ -8,6 +8,7 @@ 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
@@ -702,17 +703,19 @@ 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.decreasing_by?)) ·)
+  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) ·)
   let callMatrix := rcs.map (inspectCall ·)
 
   match ← liftMetaM <| solve measures callMatrix with
   | .some solution => do
     let wf ← buildTermWF originalVarNamess varNamess solution
 
-    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}"
+    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)
 
     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.termination_by?.isSome)
+    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.terminationBy?.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.termination_by?.get!)
+      pure <| preDefsWith.map (·.termination.terminationBy?.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.decreasing_by?))
+        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasingBy?))
         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 Syntax := do
+def TerminationBy.unexpand (wf : TerminationBy) : MetaM (TSyntax ``terminationBy) := 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,8 +50,9 @@ is what `Term.runTactic` expects.
  -/
 structure TerminationHints where
   ref : Syntax
-  termination_by? : Option TerminationBy
-  decreasing_by?  : Option DecreasingBy
+  terminationBy?? : Option Syntax
+  terminationBy? : Option TerminationBy
+  decreasingBy?  : Option DecreasingBy
   /-- Here we record the number of parameters past the `:`. It is set by
   `TerminationHints.rememberExtraParams` and used as folows:
 
@@ -63,19 +64,27 @@ structure TerminationHints where
   extraParams : Nat
   deriving Inhabited
 
-def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, 0⟩
+def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, 0⟩
 
 /-- Logs warnings when the `TerminationHints` are present.  -/
 def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): CoreM Unit := do
-  match hints.termination_by?, hints.decreasing_by? with
-  | .none, .none => pure ()
-  | .none, .some dec_by =>
+  match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy? with
+  | .none, .none, .none => pure ()
+  | .none, .none, .some dec_by =>
     logErrorAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
-  | .some term_by, .none =>
+  | .some term_by?, .none, .none =>
+    logErrorAt term_by? m!"unused `termination_by?`, function is {reason}"
+  | .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`).
@@ -111,19 +120,23 @@ 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?: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}
+  | `(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
       | _ => throwErrorAt t "unexpected `termination_by` syntax"
-    let decreasing_by? ← d?.mapM fun d => match d with
+      else pure none
+    let decreasingBy? ← d?.mapM fun d => match d with
       | `(decreasingBy|decreasing_by $tactic) => pure {ref := d, tactic}
       | _ => throwErrorAt d "unexpected `decreasing_by` syntax"
-    return { ref := stx, termination_by?, decreasing_by?, extraParams := 0 }
+    return { ref := stx, terminationBy??, terminationBy?, decreasingBy?, extraParams := 0 }
   | _ => throwErrorAt stx s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}"
 
 end Lean.Elab.WF

src/Lean/Elab/Tactic.lean

@@ -36,3 +36,4 @@ 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

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -372,10 +372,24 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let d ← instantiateMVars d
-    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`
+    -- 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 rflPrf ← mkEqRefl (toExpr true)
     return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
 

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -0,0 +1,81 @@
+/-
+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,6 +3,7 @@ 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,6 +3,7 @@ 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,6 +3,8 @@ 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,6 +3,7 @@ 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
@@ -23,22 +24,6 @@ Allow elaboration of `OmegaConfig` arguments to tactics.
 -/
 declare_config_elab elabOmegaConfig Lean.Meta.Omega.OmegaConfig
 
-/--
-The current `ToExpr` instance for `Int` is bad,
-so we roll our own here.
--/
-def mkInt (i : Int) : Expr :=
-  if 0 ≤ i then
-    mkNat i.toNat
-  else
-    mkApp3 (.const ``Neg.neg [0]) (.const ``Int []) (mkNat (-i).toNat)
-      (.const ``Int.instNegInt [])
-where
-  mkNat (n : Nat) : Expr :=
-    let r := mkRawNatLit n
-    mkApp3 (.const ``OfNat.ofNat [0]) (.const ``Int []) r
-        (.app (.const ``instOfNat []) r)
-
 /-- Match on the two defeq expressions for successor: `n+1`, `n.succ`. -/
 def succ? (e : Expr) : Option Expr :=
   match e.getAppFnArgs with
@@ -83,7 +68,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 := (← getThe State).atoms
+    let atoms ← 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))
@@ -202,16 +187,16 @@ partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr ×
   | (``HMod.hMod, #[_, _, _, _, n, k]) =>
     match groundNat? k with
     | some k' => do
-      let k' := mkInt k'
+      let k' := toExpr (k' : Int)
       rewrite (← mkAppM ``HMod.hMod #[n, k']) (mkApp2 (.const ``Int.emod_def []) n k')
     | none => mkAtomLinearCombo e
   | (``HDiv.hDiv, #[_, _, _, _, x, z]) =>
     match groundInt? z with
     | some 0 => rewrite e (mkApp (.const ``Int.ediv_zero []) x)
     | some i => do
-      let e' ← mkAppM ``HDiv.hDiv #[x, mkInt i]
+      let e' ← mkAppM ``HDiv.hDiv #[x, toExpr i]
       if i < 0 then
-        rewrite e' (mkApp2 (.const ``Int.ediv_neg []) x (mkInt (-i)))
+        rewrite e' (mkApp2 (.const ``Int.ediv_neg []) x (toExpr (-i)))
       else
         mkAtomLinearCombo e'
     | _ => mkAtomLinearCombo e
@@ -613,7 +598,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 Std.Tactic.Omega.omegaDefault)`. -/
+the tactic call `aesop (add 50% tactic Lean.Omega.omegaDefault)`. -/
 def omegaDefault : TacticM Unit := omegaTactic {}
 
 @[builtin_tactic Lean.Parser.Tactic.omega]

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

@@ -3,6 +3,10 @@ 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,6 +3,11 @@ 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
 
 /-!
@@ -46,7 +51,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 : Array Expr := #[]
+  atoms : HashMap Expr Nat := {}
 
 /-- An intermediate layer in the `OmegaM` monad. -/
 abbrev OmegaM' := StateRefT State (ReaderT Context MetaM)
@@ -71,10 +76,11 @@ def OmegaM.run (m : OmegaM α) (cfg : OmegaConfig) : MetaM α :=
 def cfg : OmegaM OmegaConfig := do pure (← read).cfg
 
 /-- Retrieve the list of atoms. -/
-def atoms : OmegaM (List Expr) := return (← getThe State).atoms.toList
+def atoms : OmegaM (Array Expr) := do
+  return (← getThe State).atoms.toArray.qsort (·.2 < ·.2) |>.map (·.1)
 
 /-- Return the `Expr` representing the list of atoms. -/
-def atomsList : OmegaM Expr := do mkListLit (.const ``Int []) (← atoms)
+def atomsList : OmegaM Expr := do mkListLit (.const ``Int []) (← atoms).toList
 
 /-- Return the `Expr` representing the list of atoms as a `Coeffs`. -/
 def atomsCoeffs : OmegaM Expr := do
@@ -169,8 +175,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)
-      | _, (`Std.BitVec.toNat, #[n, x]) =>
-        r := r.insert (mkApp2 (.const `Std.BitVec.toNat_lt []) n x)
+      | _, (``BitVec.toNat, #[n, x]) =>
+        r := r.insert (mkApp2 (.const ``BitVec.toNat_lt []) n x)
       | _, _ => pure ()
     return r
   | (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with
@@ -238,15 +244,16 @@ 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
-  for h : i in [:c.atoms.size] do
-    if ← isDefEq e c.atoms[i] then
-      return (i, none)
+  match c.atoms.find? e with
+  | some i => return (i, none)
+  | 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.push e })
+  let i ← modifyGetThe State fun c =>
+    (c.atoms.size, { c with atoms := c.atoms.insert e c.atoms.size })
   return (i, some facts)
 
 end Omega

src/Lean/Elab/Tactic/Simp.lean

@@ -353,14 +353,13 @@ 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
-      -- `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
+    | .fvar fvarId =>
+      -- local hypotheses in the context
       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,6 +3,7 @@ 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
@@ -24,13 +25,12 @@ 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)?) => do
+      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext 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 } ←
-      withMainContext <| mkSimpContext stx (eraseLocal := false)
+    let { ctx, simprocs, dischargeWrapper } ← 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,6 +3,7 @@ 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/Expr.lean

@@ -912,7 +912,7 @@ def litValue! : Expr → Literal
   | lit v => v
   | _     => panic! "literal expected"
 
-def isNatLit : Expr → Bool
+def isRawNatLit : Expr → Bool
   | lit (Literal.natVal _) => true
   | _                      => false
 
@@ -925,7 +925,7 @@ def isStringLit : Expr → Bool
   | _                      => false
 
 def isCharLit : Expr → Bool
-  | app (const c _) a => c == ``Char.ofNat && a.isNatLit
+  | app (const c _) a => c == ``Char.ofNat && a.isRawNatLit
   | _                 => false
 
 def constName! : Expr → Name
@@ -1037,6 +1037,14 @@ 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
@@ -1207,10 +1215,21 @@ 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₀

src/Lean/Meta.lean

@@ -45,3 +45,5 @@ 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

@@ -1067,6 +1067,23 @@ 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
 

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,11 +29,21 @@ 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 :=
-  declName.isInternal && !isPrivateName declName
+  isInternalNameModuloPrivate declName
   || isAuxRecursor env declName
   || isNoConfusion env declName
   || isRecCore env declName

src/Lean/Meta/CtorRecognizer.lean

@@ -0,0 +1,74 @@
+/-
+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.isNatLit then true
+  if e.isRawNatLit then true
   else
     let f := e.getAppFn
     if !f.isConst then false

src/Lean/Meta/LazyDiscrTree.lean

@@ -0,0 +1,831 @@
+/-
+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

@@ -0,0 +1,151 @@
+/-
+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 e := e.consumeMData
+  guard <| e.isAppOfArity' ``OfNat.ofNat 3
+  let type ← whnfD (e.getArg!' 0)
+  guard <| type.getAppFn.isConstOf typeDeclName
+  let .lit (.natVal n) := (e.getArg!' 1).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
+  if e.isAppOfArity' ``Neg.neg 3 then
+    let some (n, _) ← getOfNatValue? (e.getArg!' 2) ``Int | return none
+    return some (-n)
+  return none
+
+/-- Return `some c` if `e` is a `Char.ofNat`-application encoding character `c`. -/
+def getCharValue? (e : Expr) : MetaM (Option Char) := OptionT.run do
+  guard <| e.isAppOfArity' ``Char.ofNat 1
+  let n ← getNatValue? (e.getArg!' 0)
+  return 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
+  IO.println v
+  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) (foldPatValue value)
+    let xEqValue ← mkEq (mkFVar fvarId) (← normLitValue 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,8 +4,10 @@ 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
@@ -94,10 +96,17 @@ private def hasValPattern (p : Problem) : Bool :=
     | .val _ :: _ => true
     | _           => false
 
-private def hasNatValPattern (p : Problem) : Bool :=
-  p.alts.any fun alt => match alt.patterns with
-    | .val v :: _ => v.isNatLit
-    | _           => 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 hasVarPattern (p : Problem) : Bool :=
   p.alts.any fun alt => match alt.patterns with
@@ -130,6 +139,15 @@ private def isValueTransition (p : Problem) : Bool :=
      | .var _ :: _ => true
      | _           => false
 
+private def isFinValueTransition (p : Problem) : 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 :: _   => return (← getFinValue? v).isSome
+     | .ctor .. :: _ => return true
+     | _             => return false
+
 private def isArrayLitTransition (p : Problem) : Bool :=
   hasArrayLitPattern p && hasVarPattern p
   && p.alts.all fun alt => match alt.patterns with
@@ -137,13 +155,32 @@ private def isArrayLitTransition (p : Problem) : Bool :=
      | .var _ :: _       => true
      | _                 => false
 
-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 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 processSkipInaccessible (p : Problem) : Problem := Id.run do
   let x :: xs := p.vars | unreachable!
@@ -373,14 +410,13 @@ 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 e.constructorApp? env with
+      match (← constructorApp? e) with
       | some (ctorVal, ctorArgs) =>
         if ctorVal.name == ctorName then
           let fields := ctorArgs.extract ctorVal.numParams ctorArgs.size
@@ -461,12 +497,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 :: _ => return (← whnfD e).isConstructorApp (← getEnv)
+    | .inaccessible e :: _ => isConstructorApp e
     | _ => return false
 
 private def processNonVariable (p : Problem) : MetaM Problem := withGoalOf p do
   let x :: xs := p.vars | unreachable!
-  if let some (ctorVal, xArgs) := (← whnfD x).constructorApp? (← getEnv) then
+  if let some (ctorVal, xArgs) ← withTransparency .default <| constructorApp'? x then
     if (← altsAreCtorLike p) then
       let alts ← p.alts.filterMapM fun alt => do
         match alt.patterns with
@@ -584,12 +620,43 @@ 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) : 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 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
+    match alt.patterns with
+    | .val n :: ps =>
+      match (← getFinValue? n) with
+      | some ⟨n, v⟩ =>
+        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 alt
+    | _ => return alt
+  return { p with alts := alts }
 
 private def traceStep (msg : String) : StateRefT State MetaM Unit := do
   trace[Meta.Match.match] "{msg} step"
@@ -634,9 +701,15 @@ 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)
+    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 !isNextVar p then
     traceStep ("non variable")
     let p ← processNonVariable p
@@ -654,11 +727,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,6 +4,7 @@ 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
@@ -15,6 +16,35 @@ 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`. -/
@@ -221,7 +251,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 lhs.isConstructorApp? (← getEnv), rhs.isConstructorApp? (← getEnv) with
+          match (← isConstructorApp? lhs), (← isConstructorApp? rhs) 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
@@ -349,14 +379,14 @@ private def injectionAnyCandidate? (type : Expr) : MetaM (Option (Expr × Expr))
       return some (lhs, rhs)
   return none
 
-private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult :=
+private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult := do
   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.isNatLit && rhs.isNatLit do
+          unless lhs.isRawNatLit && rhs.isRawNatLit do
             try
               match (← injection mvarId localDecl.fvarId) with
               | InjectionResult.solved  => return InjectionAnyResult.solved
@@ -567,6 +597,8 @@ 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,45 +4,24 @@ 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) : Bool :=
-  e.isNatLit || e.isCharLit || e.isStringLit || isFinPatLit e || isUIntPatLit e
+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
 
 end Lean.Meta

src/Lean/Meta/MatchUtil.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Util.Recognizers
 import Lean.Meta.Basic
+import Lean.Meta.CtorRecognizer
 
 namespace Lean.Meta
 
@@ -62,8 +63,6 @@ def matchNe? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
       return none
 
 def matchConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
-  let env ← getEnv
-  matchHelper? e fun e =>
-    return e.isConstructorApp? env
+  matchHelper? e isConstructorApp?
 
 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]!.isNatLit then
+          if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isRawNatLit 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
-    return (← whnf rhs).isConstructorApp (← getEnv)
+    isConstructorApp' rhs
 
 /--
   Close the given goal if `h` is a proof for an equality such as `as = a :: as`.

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -37,6 +37,15 @@ 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}"
@@ -64,8 +73,7 @@ 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) ← forallTelescopeReducing xDecl.type fun args concl =>
-            pure (args.size, concl.getAppFn == motive)
+          let (numFields, provesMotive) := altArity motive 0 xDecl.type
           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
-        let env ← getEnv
-        match a.isConstructorApp? env, b.isConstructorApp? env with
+        match (← isConstructorApp'? a), (← isConstructorApp'? b) with
         | some aCtor, some bCtor =>
-          let val ← mkNoConfusion target prf
+          -- We use the default transparency because `a` and `b` may be builtin literals.
+          let val ← withTransparency .default <| mkNoConfusion target prf
           if aCtor.name != bCtor.name then
             mvarId.assign val
             return InjectionResultCore.solved
           else
             let valType ← inferType val
-            let valType ← whnf valType
+            -- 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
             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.isNatLit && rhs.isNatLit then cont
+        if lhs.isRawNatLit && rhs.isRawNatLit then cont
         else
           try
             match (← injection mvarId fvarId newNames) with

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -0,0 +1,399 @@
+/-
+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
+
+instance : ToString DeclMod where
+  toString m := match m with | .none => "" | .mp => "mp" | .mpr => "mpr"
+
+/--
+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
+
+/--
+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
+  withTraceNode `Tactic.librarySearch (return m!"{emoji ·} trying {name} with {mod} ") do
+    setMCtx mctx
+    let lem ← mkLibrarySearchLemma name mod
+    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,8 +3,9 @@ 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.SimpTheorems
+import Lean.Meta.Tactic.Simp.Attr
 import Lean.Meta.CoeAttr
 
 namespace Lean.Meta.NormCast

src/Lean/Meta/Tactic/Rewrite.lean

@@ -8,6 +8,7 @@ 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
@@ -53,6 +54,7 @@ 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,6 +13,7 @@ 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

@@ -0,0 +1,74 @@
+/-
+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,11 +4,12 @@ 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 Std.BitVec
+namespace BitVec
 open Lean Meta Simp
 
 /-- A bit-vector literal -/
@@ -19,38 +20,12 @@ structure Literal where
   value : BitVec n
 
 /--
-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
+Try to convert `OfNat.ofNat`/`BitVec.OfNat` application into a
 bitvector literal.
 -/
-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)
+def fromExpr? (e : Expr) : SimpM (Option Literal) := do
+  let some ⟨n, value⟩ ← getBitVecValue? e | return none
+  return some { n, value }
 
 /--
 Helper function for reducing homogenous unary bitvector operators.
@@ -59,8 +34,7 @@ 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
-  let v := { v with value := op v.value }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr (op v.value) }
 
 /--
 Helper function for reducing homogenous binary bitvector operators.
@@ -72,8 +46,7 @@ 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}"
-    let v := { v₁ with value := op v₁.value (h ▸ v₂.value) }
-    return .done { expr := v.toExpr }
+    return .done { expr := toExpr (op v₁.value (h ▸ v₂.value)) }
   else
     return .continue
 
@@ -83,8 +56,7 @@ 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
-  let lit : Literal := { n, value := op n v.value }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (op n v.value) }
 
 /--
 Helper function for reducing bitvector functions such as `getLsb` and `getMsb`.
@@ -105,8 +77,7 @@ 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
-  let v := { v with value := op v.value i }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr (op v.value i) }
 
 /--
 Helper function for reducing bitvector predicates.
@@ -194,16 +165,14 @@ builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : BitVec _)) := fun e => do
   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 }
+  return .done { expr := toExpr (v₁.value ++ v₂.value) }
 
 /-- Simplification procedure for casting `BitVec`s along an equality of the size. -/
 builtin_simproc [simp, seval] reduceCast (cast _ _) := fun e => do
   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 }
+  return .done { expr := toExpr (BitVec.ofNat m v.value.toNat) }
 
 /-- Simplification procedure for `BitVec.toNat`. -/
 builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
@@ -215,15 +184,14 @@ builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
 builtin_simproc [simp, seval] reduceToInt (BitVec.toInt _) := fun e => do
   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 }
+  return .done { expr := toExpr v.value.toInt }
 
 /-- Simplification procedure for `BitVec.ofInt`. -/
 builtin_simproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
   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 }
+  return .done { expr := toExpr (BitVec.ofInt n i) }
 
 /-- Simplification procedure for ensuring `BitVec.ofNat` literals are normalized. -/
 builtin_simproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
@@ -232,7 +200,7 @@ builtin_simproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
   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 := { n, value := BitVec.ofNat n v : Literal }.toExpr }
+  return .done { expr := toExpr (BitVec.ofNat n v) }
 
 /-- Simplification procedure for `<` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)
@@ -262,8 +230,7 @@ builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
   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
-    let lit : Literal := { n := w, value := v.value.zeroExtend' h }
-    return .done { expr := lit.toExpr }
+    return .done { expr := toExpr (v.value.zeroExtend' h) }
   else
     return .continue
 
@@ -272,8 +239,7 @@ builtin_simproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _ _
   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 }
+  return .done { expr := toExpr (v.value.shiftLeftZeroExtend m) }
 
 /-- Simplification procedure for `extractLsb'` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => do
@@ -281,16 +247,14 @@ builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => d
   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 }
+  return .done { expr := toExpr (v.value.extractLsb' start len) }
 
 /-- Simplification procedure for `replicate` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
   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 }
+  return .done { expr := toExpr (v.value.replicate w) }
 
 /-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
@@ -302,7 +266,6 @@ builtin_simproc [simp, seval] reduceSignExtend (signExtend _ _) := reduceExtend
 builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
   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 }
+  return .done { expr := toExpr (allOnes n) }
 
-end Std.BitVec
+end 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) := OptionT.run do
-  guard (e.isAppOfArity ``Char.ofNat 1)
-  let value ← Nat.fromExpr? e.appArg!
-  return Char.ofNat value
+def fromExpr? (e : Expr) : SimpM (Option Char) :=
+  getCharValue? e
 
 @[inline] def reduceUnary [ToExpr α] (declName : Name) (op : Char → α) (arity : Nat := 1) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -44,7 +44,7 @@ builtin_simproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnar
 builtin_simproc [simp, seval] reduceVal (Char.val _) := fun e => do
   unless e.isAppOfArity ``Char.val 1 do return .continue
   let some c ← fromExpr? e.appArg! | return .continue
-  return .done { expr := UInt32.toExprCore c.val }
+  return .done { expr := toExpr c.val }
 builtin_simproc [simp, seval] reduceEq  (( _ : Char) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Char) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
 builtin_simproc [simp, seval] reduceBEq  (( _ : Char) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)

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

@@ -5,37 +5,29 @@ 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
-  ofNatFn   : Expr
-  size      : Nat
-  value     : Nat
+  n     : Nat
+  value : Fin n
 
-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! }
+def fromExpr? (e : Expr) : SimpM (Option Value) := do
+  let some ⟨n, value⟩ ← getFinValue? e | return none
+  return some { n, value }
 
-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
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : {n : Nat} → Fin n → Fin n → Fin n) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  unless v₁.size == v₂.size do return .continue
-  let v := { v₁ with value := op v₁.value v₂.value % v₁.size }
-  return .done { expr := v.toExpr }
+  if h : v₁.n = v₂.n then
+    let v := op v₁.value (h ▸ v₂.value)
+    return .done { expr := toExpr v }
+  else
+    return .continue
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -71,12 +63,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 v ← fromExpr? e | return .continue
-  let v' ← Nat.fromExpr? e.appFn!.appArg!
-  if v.value == v' then
+  let some ⟨n, v⟩ ← getFinValue? e | return .continue
+  let some m ← getNatValue? e.appFn!.appArg! | return .continue
+  if n == m then
     -- Design decision: should we return `.continue` instead of `.done` when simplifying.
     -- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`
     return .done { expr := e }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr v }
 
 end Fin

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

@@ -5,33 +5,14 @@ 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) := 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
+def fromExpr? (e : Expr) : SimpM (Option Int) :=
+  getIntValue? e
 
 @[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Int → Int) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue

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

@@ -5,6 +5,7 @@ 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
@@ -12,20 +13,19 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
 namespace Nat
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Nat) := do
-  let some n ← evalNat e |>.run | return none
-  return n
+def fromExpr? (e : Expr) : SimpM (Option Nat) :=
+  getNatValue? e
 
 @[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appArg! | return .continue
-  return .done { expr := mkNatLit (op n) }
+  return .done { expr := toExpr (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 := mkNatLit (op n m) }
+  return .done { expr := toExpr (op n m) }
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue

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

@@ -3,15 +3,15 @@ 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.Tactic.Simp.BuiltinSimprocs.Char
 
 namespace String
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option String) := OptionT.run do
-  let .lit (.strVal s) := e | failure
-  return s
+def fromExpr? (e : Expr) : SimpM (Option String) := do
+  return getStringValue? e
 
 builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : String)) := fun e => do
   unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue

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

@@ -4,6 +4,7 @@ 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
 
 open Lean Meta Simp
@@ -13,49 +14,30 @@ let ofNat := typeName.getId ++ `ofNat
 let ofNatCore := mkIdent (typeName.getId ++ `ofNatCore)
 let toNat := mkIdent (typeName.getId ++ `toNat)
 let fromExpr := mkIdent `fromExpr
-let toExprCore := mkIdent `toExprCore
-let toExpr := mkIdent `toExpr
 `(
 namespace $typeName
 
-structure Value where
-  ofNatFn : Expr
-  value   : $typeName
-
-def $fromExpr (e : Expr) : OptionT SimpM Value := do
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
-  let type ← whnf e.appFn!.appFn!.appArg!
-  guard (type.isConstOf $(quote typeName.getId))
-  let value ← Nat.fromExpr? e.appFn!.appArg!
-  let value := $(mkIdent ofNat) value
-  return { value, ofNatFn := e.appFn!.appFn! }
-
-def $toExprCore (v : $typeName) : Expr :=
-  let vExpr := mkRawNatLit v.val
-  mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst $(quote typeName.getId)) vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
-
-def $toExpr (v : Value) : Expr :=
-  let vExpr := mkRawNatLit v.value.val
-  mkApp2 v.ofNatFn vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
+def $fromExpr (e : Expr) : SimpM (Option $typeName) := do
+  let some (n, _) ← getOfNatValue? e $(quote typeName.getId) | return none
+  return $(mkIdent ofNat) n
 
 @[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  let r := { n with value := op n.value m.value }
-  return .done { expr := $toExpr r }
+  return .done { expr := toExpr (op n m) }
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  evalPropStep e (op n.value m.value)
+  evalPropStep e (op n m)
 
 @[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  return .done { expr := Lean.toExpr (op n.value m.value) }
+  return .done { expr := toExpr (op n m) }
 
 builtin_simproc [simp, seval] $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
 builtin_simproc [simp, seval] $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)
@@ -76,14 +58,13 @@ builtin_simproc [simp, seval] $(mkIdent `reduceOfNatCore):ident ($ofNatCore _ _)
   unless e.isAppOfArity $(quote ofNatCore.getId) 2 do return .continue
   let some value ← Nat.fromExpr? e.appFn!.appArg! | return .continue
   let value := $(mkIdent ofNat) value
-  let eNew := $toExprCore value
-  return .done { expr := eNew }
+  return .done { expr := toExpr value }
 
 builtin_simproc [simp, seval] $(mkIdent `reduceToNat):ident ($toNat _) := fun e => do
   unless e.isAppOfArity $(quote toNat.getId) 1 do return .continue
   let some v ← ($fromExpr e.appArg!) | return .continue
-  let n := $toNat v.value
-  return .done { expr := mkNatLit n }
+  let n := $toNat v
+  return .done { expr := toExpr n }
 
 /-- Return `.done` for UInt values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isValue ((OfNat.ofNat _ : $typeName)) := fun e => do
@@ -97,4 +78,8 @@ declare_uint_simprocs UInt8
 declare_uint_simprocs UInt16
 declare_uint_simprocs UInt32
 declare_uint_simprocs UInt64
-declare_uint_simprocs USize
+/-
+We disabled the simprocs for USize since the result of most operations depend on an opaque value: `System.Platform.numBits`.
+We could reduce some cases using the fact that this opaque value is `32` or `64`, but it is unclear whether it would be useful in practice.
+-/
+-- declare_uint_simprocs USize

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

@@ -33,7 +33,7 @@ def Config.updateArith (c : Config) : CoreM Config := do
 
 /-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal -/
 def isOfNatNatLit (e : Expr) : Bool :=
-  e.isAppOfArity ``OfNat.ofNat 3 && e.appFn!.appArg!.isNatLit
+  e.isAppOfArity ``OfNat.ofNat 3 && e.appFn!.appArg!.isRawNatLit
 
 private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
   matchConst e.getAppFn (fun _ => pure none) fun cinfo _ => do
@@ -69,16 +69,18 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
           unless e.getAppNumArgs > projInfo.numParams do
             return none
           let major := e.getArg! projInfo.numParams
-          unless major.isConstructorApp (← getEnv) do
+          unless (← isConstructorApp major) do
             return none
           reduceProjCont? (← withDefault <| unfoldDefinition? e)
       else
         -- `structure` projections
         reduceProjCont? (← unfoldDefinition? e)
 
-private def reduceFVar (cfg : Config) (thms : SimpTheoremsArray) (e : Expr) : MetaM Expr := do
+private def reduceFVar (cfg : Config) (thms : SimpTheoremsArray) (e : Expr) : SimpM Expr := do
   let localDecl ← getFVarLocalDecl e
   if cfg.zetaDelta || thms.isLetDeclToUnfold e.fvarId! || localDecl.isImplementationDetail then
+    if !cfg.zetaDelta && thms.isLetDeclToUnfold e.fvarId! then
+      recordSimpTheorem (.fvar localDecl.fvarId)
     let some v := localDecl.value? | return e
     return v
   else
@@ -502,7 +504,7 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul
     unless modified do
       trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified"
       return none
-    unless (← synthesizeArgs (.decl c.theoremName) xs bis) do
+    unless (← synthesizeArgs (.decl c.theoremName) bis xs) do
       trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed"
       return none
     let eNew ← instantiateMVars rhs

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Simp.Attr
 
 namespace Lean.Meta.Simp
 

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

@@ -8,24 +8,82 @@ import Lean.Meta.ACLt
 import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.AppBuilder
 import Lean.Meta.SynthInstance
+import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.LinearArith.Simp
 import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Simp.Attr
 
 namespace Lean.Meta.Simp
 
-def synthesizeArgs (thmId : Origin) (xs : Array Expr) (bis : Array BinderInfo) : SimpM Bool := do
+/--
+Helper type for implementing `discharge?'`
+-/
+inductive DischargeResult where
+  | proved
+  | notProved
+  | maxDepth
+  | failedAssign
+  deriving DecidableEq
+
+/--
+Wrapper for invoking `discharge?`. It checks for maximum discharge depth, create trace nodes, and ensure
+the generated proof was successfully assigned to `x`.
+-/
+def discharge?' (thmId : Origin) (x : Expr) (type : Expr) : SimpM Bool := do
+  let r : DischargeResult ← withTraceNode `Meta.Tactic.simp.discharge (fun
+      | .ok .proved       => return m!"{← ppOrigin thmId} discharge {checkEmoji}{indentExpr type}"
+      | .ok .notProved    => return m!"{← ppOrigin thmId} discharge {crossEmoji}{indentExpr type}"
+      | .ok .maxDepth     => return m!"{← ppOrigin thmId} discharge {crossEmoji} max depth{indentExpr type}"
+      | .ok .failedAssign => return m!"{← ppOrigin thmId} discharge {crossEmoji} failed to assign proof{indentExpr type}"
+      | .error err        => return m!"{← ppOrigin thmId} discharge {crossEmoji}{indentExpr type}{indentD err.toMessageData}") do
+    let ctx ← getContext
+    if ctx.dischargeDepth >= ctx.maxDischargeDepth then
+      return .maxDepth
+    else withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
+      -- We save the state, so that `UsedTheorems` does not accumulate
+      -- `simp` lemmas used during unsuccessful discharging.
+      let usedTheorems := (← get).usedTheorems
+      match (← discharge? type) with
+      | some proof =>
+        unless (← isDefEq x proof) do
+          modify fun s => { s with usedTheorems }
+          return .failedAssign
+        return .proved
+      | none =>
+        modify fun s => { s with usedTheorems }
+        return .notProved
+  return r = .proved
+
+def synthesizeArgs (thmId : Origin) (bis : Array BinderInfo) (xs : Array Expr) : SimpM Bool := do
+  let skipAssignedInstances := tactic.skipAssignedInstances.get (← getOptions)
   for x in xs, bi in bis do
     let type ← inferType x
-    -- Note that the binderInfo may be misleading here:
-    -- `simp [foo _]` uses `abstractMVars` to turn the elaborated term with
-    -- mvars into the lambda expression `fun α x inst => foo x`, and all
-    -- its bound variables have default binderInfo!
-    if bi.isInstImplicit then
+    -- We use the flag `tactic.skipAssignedInstances` for backward compatibility.
+    -- See comment below.
+    if !skipAssignedInstances && bi.isInstImplicit then
       unless (← synthesizeInstance x type) do
         return false
-    else if (← instantiateMVars x).isMVar then
+    /-
+    We used to invoke `synthesizeInstance` for every instance implicit argument,
+    to ensure the synthesized instance was definitionally equal to the one in
+    the term, but it turned out to be to inconvenient in practice. Here is an
+    example:
+    ```
+    theorem dec_and (p q : Prop) [Decidable (p ∧ q)] [Decidable p] [Decidable q] : decide (p ∧ q) = (p && q) := by
+      by_cases p <;> by_cases q <;> simp [*]
+
+    theorem dec_not (p : Prop) [Decidable (¬p)] [Decidable p] : decide (¬p) = !p := by
+      by_cases p <;> simp [*]
+
+    example [Decidable u] [Decidable v] : decide (u ∧ (v → False)) = (decide u && !decide v) := by
+      simp only [imp_false]
+      simp only [dec_and]
+      simp only [dec_not]
+    ```
+    -/
+    if (← instantiateMVars x).isMVar then
       -- A hypothesis can be both a type class instance as well as a proposition,
       -- in that case we try both TC synthesis and the discharger
       -- (because we don't know whether the argument was originally explicit or instance-implicit).
@@ -33,18 +91,7 @@ def synthesizeArgs (thmId : Origin) (xs : Array Expr) (bis : Array BinderInfo) :
         if (← synthesizeInstance x type) then
           continue
       if (← isProp type) then
-        -- We save the state, so that `UsedTheorems` does not accumulate
-        -- `simp` lemmas used during unsuccessful discharging.
-        let usedTheorems := (← get).usedTheorems
-        match (← discharge? type) with
-        | some proof =>
-          unless (← isDefEq x proof) do
-            trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign proof{indentExpr type}"
-            modify fun s => { s with usedTheorems }
-            return false
-        | none =>
-          trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to discharge hypotheses{indentExpr type}"
-          modify fun s => { s with usedTheorems }
+        unless (← discharge?' thmId x type) do
           return false
   return true
 where
@@ -63,7 +110,7 @@ where
 private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
   let rec go (e : Expr) : SimpM (Option Result) := do
     if (← isDefEq lhs e) then
-      unless (← synthesizeArgs thm.origin xs bis) do
+      unless (← synthesizeArgs thm.origin bis xs) do
         return none
       let proof? ← if thm.rfl then
         pure none
@@ -156,22 +203,11 @@ where
   inErasedSet (thm : SimpTheorem) : Bool :=
     erased.contains thm.origin
 
--- TODO: workaround for `Expr.constructorApp?` limitations. We should handle `OfNat.ofNat` there
-private def reduceOfNatNat (e : Expr) : MetaM Expr := do
-  unless e.isAppOfArity ``OfNat.ofNat 3 do
-    return e
-  unless (← whnfD (e.getArg! 0)).isConstOf ``Nat do
-    return e
-  return e.getArg! 1
-
 def simpCtorEq : Simproc := fun e => withReducibleAndInstances do
   match e.eq? with
   | none => return .continue
   | some (_, lhs, rhs) =>
-    let lhs ← reduceOfNatNat (← whnf lhs)
-    let rhs ← reduceOfNatNat (← whnf rhs)
-    let env ← getEnv
-    match lhs.constructorApp? env, rhs.constructorApp? env with
+    match (← constructorApp'? lhs), (← constructorApp'? rhs) with
     | some (c₁, _), some (c₂, _) =>
       if c₁.name != c₂.name then
         withLocalDeclD `h e fun h =>
@@ -287,7 +323,6 @@ def rewritePost (rflOnly := false) : Simproc := fun e => do
 Discharge procedure for the ground/symbolic evaluator.
 -/
 def dischargeGround (e : Expr) : SimpM (Option Expr) := do
-  trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
   let r ← simp e
   if r.expr.isTrue then
     try
@@ -479,21 +514,11 @@ def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
       return some r
     if let some r ← dischargeEqnThmHypothesis? e then
       return some r
-  let ctx ← getContext
-  trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
-  if ctx.dischargeDepth >= ctx.maxDischargeDepth then
-    trace[Meta.Tactic.simp.discharge] "maximum discharge depth has been reached"
-    return none
+  let r ← simp e
+  if r.expr.isTrue then
+    return some (← mkOfEqTrue (← r.getProof))
   else
-    withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
-      let r ← simp e
-      if r.expr.isTrue then
-        try
-          return some (← mkOfEqTrue (← r.getProof))
-        catch _ =>
-          return none
-      else
-        return none
+    return none
 
 abbrev Discharge := Expr → SimpM (Option Expr)
 

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

@@ -362,37 +362,6 @@ def addSimpTheorem (ext : SimpExtension) (declName : Name) (post : Bool) (inv :
   for simpThm in simpThms do
     ext.add (SimpEntry.thm simpThm) attrKind
 
-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 =>
-      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
-      let s := ext.getState (← getEnv)
-      let s ← s.erase (.decl declName)
-      modifyEnv fun env => ext.modifyState env fun _ => s
-  }
 
 def mkSimpExt (name : Name := by exact decl_name%) : IO SimpExtension :=
   registerSimpleScopedEnvExtension {
@@ -409,26 +378,9 @@ abbrev SimpExtensionMap := HashMap Name SimpExtension
 
 builtin_initialize simpExtensionMapRef : IO.Ref SimpExtensionMap ← IO.mkRef {}
 
-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 getSimpExtension? (attrName : Name) : IO (Option SimpExtension) :=
   return (← simpExtensionMapRef.get).find? attrName
 
-def getSimpTheorems : CoreM SimpTheorems :=
-  simpExtension.getTheorems
-
-def getSEvalTheorems : CoreM SimpTheorems :=
-  sevalSimpExtension.getTheorems
-
 /-- Auxiliary method for adding a global declaration to a `SimpTheorems` datastructure. -/
 def SimpTheorems.addConst (s : SimpTheorems) (declName : Name) (post := true) (inv := false) (prio : Nat := eval_prio default) : MetaM SimpTheorems := do
   let s := { s with erased := s.erased.erase (.decl declName post inv) }

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

@@ -127,25 +127,29 @@ def toSimprocEntry (e : SimprocOLeanEntry) : ImportM SimprocEntry := do
 def eraseSimprocAttr (ext : SimprocExtension) (declName : Name) : AttrM Unit := do
   let s := ext.getState (← getEnv)
   unless s.simprocNames.contains declName do
-    throwError "'{declName}' does not have [simproc] attribute"
+    throwError "'{declName}' does not have a simproc attribute"
   modifyEnv fun env => ext.modifyState env fun s => s.erase declName
 
-def addSimprocAttr (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do
+def addSimprocAttrCore (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do
   let proc ← getSimprocFromDecl declName
   let some keys ← getSimprocDeclKeys? declName |
     throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
   ext.add { declName, post, keys, proc } kind
 
+def Simprocs.addCore (s : Simprocs) (keys : Array SimpTheoremKey) (declName : Name) (post : Bool) (proc : Simproc) : Simprocs :=
+  let s := { s with simprocNames := s.simprocNames.insert declName, erased := s.erased.erase declName }
+  if post then
+    { s with post := s.post.insertCore keys { declName, keys, post, proc } }
+  else
+    { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
+
 /--
 Implements attributes `builtin_simproc` and `builtin_sevalproc`.
 -/
 def addSimprocBuiltinAttrCore (ref : IO.Ref Simprocs) (declName : Name) (post : Bool) (proc : Simproc) : IO Unit := do
   let some keys := (← builtinSimprocDeclsRef.get).keys.find? declName |
     throw (IO.userError "invalid [builtin_simproc] attribute, '{declName}' is not a builtin simproc")
-  if post then
-    ref.modify fun s => { s with post := s.post.insertCore keys { declName, keys, post, proc } }
-  else
-    ref.modify fun s => { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
+  ref.modify fun s => s.addCore keys declName post proc
 
 def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO Unit :=
   addSimprocBuiltinAttrCore builtinSimprocsRef declName post proc
@@ -166,10 +170,7 @@ def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs
         throw e
   let some keys ← getSimprocDeclKeys? declName |
     throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
-  if post then
-    return { s with post := s.post.insertCore keys { declName, keys, post, proc } }
-  else
-    return { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
+  return s.addCore keys declName post proc
 
 def SimprocEntry.try (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM Step := do
   let mut extraArgs := #[]
@@ -255,6 +256,7 @@ def simprocArrayCore (post : Bool) (ss : SimprocsArray) (e : Expr) : SimpM Step
 
 register_builtin_option simprocs : Bool := {
   defValue := true
+  group    := "backward compatibility"
   descr    := "Enable/disable `simproc`s (simplification procedures)."
 }
 
@@ -276,24 +278,22 @@ def mkSimprocExt (name : Name := by exact decl_name%) (ref? : Option (IO.Ref Sim
         return {}
     ofOLeanEntry  := fun _ => toSimprocEntry
     toOLeanEntry  := fun e => e.toSimprocOLeanEntry
-    addEntry      := fun s e =>
-      if e.post then
-        { s with post := s.post.insertCore e.keys e }
-      else
-        { s with pre := s.pre.insertCore e.keys e }
+    addEntry      := fun s e => s.addCore e.keys e.declName e.post e.proc
   }
 
+def addSimprocAttr (ext : SimprocExtension) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
+  let go : MetaM Unit := do
+    let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
+    addSimprocAttrCore ext declName attrKind post
+  discard <| go.run {} {}
+
 def mkSimprocAttr (attrName : Name) (attrDescr : String) (ext : SimprocExtension) (name : Name) : IO Unit := do
   registerBuiltinAttribute {
     ref   := name
     name  := attrName
     descr := attrDescr
     applicationTime := AttributeApplicationTime.afterCompilation
-    add   := fun declName stx attrKind =>
-      let go : MetaM Unit := do
-        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-        addSimprocAttr ext declName attrKind post
-      discard <| go.run {} {}
+    add   := addSimprocAttr ext
     erase := eraseSimprocAttr ext
   }
 

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

@@ -92,9 +92,6 @@ structure Context where
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
   ctx.simpTheorems.isDeclToUnfold declName
 
-def Context.mkDefault : MetaM Context :=
-  return { config := {}, simpTheorems := #[(← getSimpTheorems)], congrTheorems := (← getSimpCongrTheorems) }
-
 abbrev UsedSimps := HashMap Origin Nat
 
 structure State where

src/Lean/Meta/Tactic/TryThis.lean

@@ -7,11 +7,7 @@ prelude
 import Lean.Server.CodeActions
 import Lean.Widget.UserWidget
 import Lean.Data.Json.Elab
-
-/-- Gets the LSP range from a `String.Range`. -/
-def Lean.FileMap.utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
-  { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
-
+import Lean.Data.Lsp.Utf16
 
 /-!
 # "Try this" support

src/Lean/Meta/Tactic/UnifyEq.lean

@@ -70,8 +70,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
           else
             throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}"
         let rec injection (a b : Expr) := do
-          let env ← getEnv
-          if a.isConstructorApp env && b.isConstructorApp env then
+          if (← isConstructorApp a <&&> isConstructorApp b) then
             /- ctor_i ... = ctor_j ... -/
             match (← injectionCore mvarId eqFVarId) with
             | InjectionResultCore.solved                   => return none -- this alternative has been solved

src/Lean/Meta/Tactic/Util.lean

@@ -178,4 +178,10 @@ def _root_.Lean.MVarId.isSubsingleton (g : MVarId) : MetaM Bool := do
   catch _ =>
     return false
 
+register_builtin_option tactic.skipAssignedInstances : Bool := {
+  defValue := true
+  group    := "backward compatibility"
+  descr    := "in the `rw` and `simp` tactics, if an instance implicit argument is assigned, do not try to synthesize instance."
+}
+
 end Lean.Meta

src/Lean/Meta/WHNF.lean

@@ -8,6 +8,7 @@ import Lean.Structure
 import Lean.Util.Recognizers
 import Lean.Meta.GetUnfoldableConst
 import Lean.Meta.FunInfo
+import Lean.Meta.CtorRecognizer
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchPatternAttr
 
@@ -133,7 +134,7 @@ private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr
   let env ← getEnv
   if !isStructureLike env inductName then
     return major
-  else if let some _ := major.isConstructorApp? env then
+  else if let some _ ← isConstructorApp? major then
     return major
   else
     let majorType ← inferType major
@@ -450,6 +451,7 @@ def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
        || info.name == ``Char.ofNat   || info.name == ``Char.ofNatAux
        || info.name == ``String.decEq || info.name == ``List.hasDecEq
        || info.name == ``Fin.ofNat
+       || info.name == ``Fin.ofNat' -- It is used to define `BitVec` literals
        || info.name == ``UInt8.ofNat  || info.name == ``UInt8.decEq
        || info.name == ``UInt16.ofNat || info.name == ``UInt16.decEq
        || info.name == ``UInt32.ofNat || info.name == ``UInt32.decEq
@@ -753,7 +755,7 @@ mutual
                 let numArgs := e.getAppNumArgs
                 if recArgPos >= numArgs then return none
                 let recArg := e.getArg! recArgPos numArgs
-                if !(← whnfMatcher recArg).isConstructorApp (← getEnv) then return none
+                if !(← isConstructorApp (← whnfMatcher recArg)) then return none
                 return some r
             | _ =>
               if (← getMatcherInfo? fInfo.name).isSome then

src/Lean/Modifiers.lean

@@ -47,7 +47,7 @@ def isPrivateNameExport (n : Name) : Bool :=
 Return `true` if `n` is of the form `_private.<module_name>.0`
 See comment above.
 -/
-private def isPrivatePrefix (n : Name) : Bool :=
+def isPrivatePrefix (n : Name) : Bool :=
   match n with
   | .num p 0 => go p
   | _ => false

src/Lean/Parser/Tactic.lean

@@ -66,13 +66,60 @@ doing a pattern match. This is equivalent to `fun` with match arms in term mode.
 @[builtin_tactic_parser] def introMatch := leading_parser
   nonReservedSymbol "intro" >> matchAlts
 
-/-- `decide` will attempt to prove a goal of type `p` by synthesizing an instance
-of `Decidable p` and then evaluating it to `isTrue ..`. Because this uses kernel
-computation to evaluate the term, it may not work in the presence of definitions
-by well founded recursion, since this requires reducing proofs.
-```
+/--
+`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
+and then reducing that instance to evaluate the truth value of `p`.
+If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.
+
+Limitations:
+- The target is not allowed to contain local variables or metavariables.
+  If there are local variables, you can try first using the `revert` tactic with these local variables
+  to move them into the target, which may allow `decide` to succeed.
+- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined
+  by well-founded recursion might not work, because evaluating them requires reducing proofs.
+  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.
+  These can appear for instances defined using tactics (such as `rw` and `simp`).
+  To avoid this, use definitions such as `decidable_of_iff` instead.
+
+## Examples
+
+Proving inequalities:
+```lean
 example : 2 + 2 ≠ 5 := by decide
 ```
+
+Trying to prove a false proposition:
+```lean
+example : 1 ≠ 1 := by decide
+/-
+tactic 'decide' proved that the proposition
+  1 ≠ 1
+is false
+-/
+```
+
+Trying to prove a proposition whose `Decidable` instance fails to reduce
+```lean
+opaque unknownProp : Prop
+
+open scoped Classical in
+example : unknownProp := by decide
+/-
+tactic 'decide' failed for proposition
+  unknownProp
+since its 'Decidable' instance reduced to
+  Classical.choice ⋯
+rather than to the 'isTrue' constructor.
+-/
+```
+
+## Properties and relations
+
+For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
+```lean
+example : 1 + 1 = 2 := by decide
+example : 1 + 1 = 2 := by rfl
+```
 -/
 @[builtin_tactic_parser] def decide := leading_parser
   nonReservedSymbol "decide"

src/Lean/Parser/Term.lean

@@ -118,14 +118,18 @@ def example (a : Nat) : Nat → Nat → Nat :=
 termination_by b c => a - b
 ```
 
-If omitted, a termination argument will be inferred.
+If omitted, a termination argument will be inferred. If written as `termination_by?`,
+the inferrred termination argument will be suggested.
 -/
 def terminationBy := leading_parser
-  ppDedent ppLine >>
   "termination_by " >>
   optional (atomic (many (ppSpace >> (ident <|> "_")) >> " => ")) >>
   termParser
 
+@[inherit_doc terminationBy]
+def terminationBy? := leading_parser
+  "termination_by?"
+
 /--
 Manually prove that the termination argument (as specified with `termination_by` or inferred)
 decreases at each recursive call.
@@ -139,7 +143,7 @@ def decreasingBy := leading_parser
 Termination hints are `termination_by` and `decreasing_by`, in that order.
 -/
 def suffix := leading_parser
-  optional terminationBy >> optional decreasingBy
+  optional (ppDedent ppLine >> (terminationBy? <|> terminationBy)) >> optional decreasingBy
 
 end Termination
 
@@ -191,6 +195,13 @@ def optSemicolon (p : Parser) : Parser :=
 This syntax is used to construct named metavariables. -/
 @[builtin_term_parser] def syntheticHole := leading_parser
   "?" >> (ident <|> hole)
+/--
+Denotes a term that was omitted by the pretty printer.
+This is only meant to be used for pretty printing, however for copy/paste friendliness it elaborates like `_` while logging a warning.
+The presence of `⋯` in pretty printer output is controlled by the `pp.deepTerms` and `pp.proofs` options.
+-/
+@[builtin_term_parser] def omission := leading_parser
+  "⋯"
 def binderIdent : Parser  := ident <|> hole
 /-- A temporary placeholder for a missing proof or value. -/
 @[builtin_term_parser] def «sorry» := leading_parser

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -16,12 +16,22 @@ open Lean.Parser.Term
 open SubExpr
 open TSyntax.Compat
 
-def maybeAddBlockImplicit (ident : Syntax) : DelabM Syntax := do
-  if ← getPPOption getPPAnalysisBlockImplicit then `(@$ident:ident) else pure ident
+/--
+If `cond` is true, wraps the syntax produced by `d` in a type ascription.
+-/
+def withTypeAscription (d : Delab) (cond : Bool := true) : DelabM Term := do
+  let stx ← d
+  if cond then
+    let typeStx ← withType delab
+    `(($stx : $typeStx))
+  else
+    return stx
 
-def unfoldMDatas : Expr → Expr
-  | Expr.mdata _ e => unfoldMDatas e
-  | e              => e
+/--
+Wraps the identifier (or identifier with explicit universe levels) with `@` if `pp.analysis.blockImplicit` is set to true.
+-/
+def maybeAddBlockImplicit (identLike : Syntax) : DelabM Syntax := do
+  if ← getPPOption getPPAnalysisBlockImplicit then `(@$identLike) else pure identLike
 
 @[builtin_delab fvar]
 def delabFVar : Delab := do
@@ -59,8 +69,12 @@ def delabSort : Delab := do
     | some l' => `(Type $(Level.quote l' max_prec))
     | none    => `(Sort $(Level.quote l max_prec))
 
-
--- NOTE: not a registered delaborator, as `const` is never called (see [delab] description)
+/--
+Delaborator for `const` expressions.
+This is not registered as a delaborator, as `const` is not an expression kind
+(see [delab] description and `Lean.PrettyPrinter.Delaborator.getExprKind`).
+Rather, it is called through the `app` delaborator.
+-/
 def delabConst : Delab := do
   let Expr.const c₀ ls ← getExpr | unreachable!
   let c₀ := if (← getPPOption getPPPrivateNames) then c₀ else (privateToUserName? c₀).getD c₀
@@ -78,11 +92,11 @@ def delabConst : Delab := do
   else
     `($(mkIdent c).{$[$(ls.toArray.map quote)],*})
 
-  let mut stx ← maybeAddBlockImplicit stx
+  let stx ← maybeAddBlockImplicit stx
   if (← getPPOption getPPTagAppFns) then
-    stx ← annotateCurPos stx
-    addTermInfo (← getPos) stx (← getExpr)
-  return stx
+    annotateTermInfo stx
+  else
+    return stx
 
 def withMDataOptions [Inhabited α] (x : DelabM α) : DelabM α := do
   match ← getExpr with
@@ -99,12 +113,6 @@ def withMDataOptions [Inhabited α] (x : DelabM α) : DelabM α := do
 partial def withMDatasOptions [Inhabited α] (x : DelabM α) : DelabM α := do
   if (← getExpr).isMData then withMDataOptions (withMDatasOptions x) else x
 
-def delabAppFn : Delab := do
-  if (← getExpr).consumeMData.isConst then
-    withMDatasOptions delabConst
-  else
-    delab
-
 /--
 A structure that records details of a function parameter.
 -/
@@ -117,6 +125,7 @@ structure ParamKind where
   defVal      : Option Expr := none
   /-- Whether the parameter is an autoparam (i.e., whether it uses a tactic for the default value). -/
   isAutoParam : Bool := false
+  deriving Inhabited
 
 /--
 Returns true if the parameter is an explicit parameter that has neither a default value nor a tactic.
@@ -128,7 +137,7 @@ def ParamKind.isRegularExplicit (param : ParamKind) : Bool :=
 Given a function `f` supplied with arguments `args`, returns an array whose n-th element
 is set to the kind of the n-th argument's associated parameter.
 We do not assume the expression `mkAppN f args` is sensical,
-and this function captures errors (except for panics) and returns the empty array.
+and this function captures errors (except for panics) and returns the empty array in that case.
 
 The returned array might be longer than the number of arguments.
 It gives parameter kinds for the fully-applied function.
@@ -141,25 +150,24 @@ argument when its arguments are specialized to function types, like in `id id 2`
 -/
 def getParamKinds (f : Expr) (args : Array Expr) : MetaM (Array ParamKind) := do
   try
-    withTransparency TransparencyMode.all do
-      let mut result : Array ParamKind := Array.mkEmpty args.size
-      let mut fnType ← inferType f
-      let mut j := 0
-      for i in [0:args.size] do
-        unless fnType.isForall do
-          fnType ← whnf (fnType.instantiateRevRange j i args)
-          j := i
-        let .forallE n t b bi := fnType | failure
-        let defVal := t.getOptParamDefault? |>.map (·.instantiateRevRange j i args)
-        result := result.push { name := n, bInfo := bi, defVal, isAutoParam := t.isAutoParam }
-        fnType := b
-      fnType := fnType.instantiateRevRange j args.size args
-      -- We still want to consider parameters past the ones for the supplied arguments.
-      forallTelescopeReducing fnType fun xs _ => do
-        xs.foldlM (init := result) fun result x => do
-          let l ← x.fvarId!.getDecl
-          -- Warning: the defVal might refer to fvars that are only valid in this context
-          pure <| result.push { name := l.userName, bInfo := l.binderInfo, defVal := l.type.getOptParamDefault?, isAutoParam := l.type.isAutoParam }
+    let mut result : Array ParamKind := Array.mkEmpty args.size
+    let mut fnType ← inferType f
+    let mut j := 0
+    for i in [0:args.size] do
+      unless fnType.isForall do
+        fnType ← withTransparency .all <| whnf (fnType.instantiateRevRange j i args)
+        j := i
+      let .forallE n t b bi := fnType | failure
+      let defVal := t.getOptParamDefault? |>.map (·.instantiateRevRange j i args)
+      result := result.push { name := n, bInfo := bi, defVal, isAutoParam := t.isAutoParam }
+      fnType := b
+    fnType := fnType.instantiateRevRange j args.size args
+    -- We still want to consider parameters past the ones for the supplied arguments for analysis.
+    forallTelescopeReducing fnType fun xs _ => do
+      xs.foldlM (init := result) fun result x => do
+        let l ← x.fvarId!.getDecl
+        -- Warning: the defVal might refer to fvars that are only valid in this context
+        pure <| result.push { name := l.userName, bInfo := l.binderInfo, defVal := l.type.getOptParamDefault?, isAutoParam := l.type.isAutoParam }
   catch _ => pure #[] -- recall that expr may be nonsensical
 
 def shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool := do
@@ -167,46 +175,10 @@ def shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool := do
   <||> (pure (getPPMotivesPi opts) <&&> returnsPi motive)
   <||> (pure (getPPMotivesNonConst opts) <&&> isNonConstFun motive)
 
-/--
-Returns true if an application should use explicit mode when delaborating.
--/
-def useAppExplicit (paramKinds : Array ParamKind) : DelabM Bool := do
-  if ← getPPOption getPPExplicit then
-    if paramKinds.any (fun param => !param.isRegularExplicit) then return true
-
-  -- If the expression has an implicit function type, fall back to delabAppExplicit.
-  -- This is e.g. necessary for `@Eq`.
-  let isImplicitApp ← try
-      let ty ← whnf (← inferType (← getExpr))
-      pure <| ty.isForall && (ty.binderInfo matches .implicit | .instImplicit)
-    catch _ => pure false
-  if isImplicitApp then return true
-
-  return false
-
-/--
-Returns true if the application is a candidate for unexpanders.
--/
-def isRegularApp (maxArgs : Nat) : DelabM Bool := do
-  let e ← getExpr
-  if not (unfoldMDatas (e.getBoundedAppFn maxArgs)).isConst then return false
-  withBoundedAppFnArgs maxArgs
-    (not <$> withMDatasOptions (getPPOption getPPUniverses <||> getPPOption getPPAnalysisBlockImplicit))
-    (fun b => pure b <&&> not <$> getPPOption getPPAnalysisNamedArg)
-
-def unexpandRegularApp (stx : Syntax) : Delab := do
-  let Expr.const c .. := (unfoldMDatas (← getExpr).getAppFn) | unreachable!
-  let fs := appUnexpanderAttribute.getValues (← getEnv) c
-  let ref ← getRef
-  fs.firstM fun f =>
-    match f stx |>.run ref |>.run () with
-    | EStateM.Result.ok stx _ => pure stx
-    | _ => failure
-
 def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStructureInstances do
   let env ← getEnv
   let e ← getExpr
-  let some s ← pure $ e.isConstructorApp? env | failure
+  let some s ← isConstructorApp? e | failure
   guard $ isStructure env s.induct;
   /- If implicit arguments should be shown, and the structure has parameters, we should not
      pretty print using { ... }, because we will not be able to see the parameters. -/
@@ -228,96 +200,203 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct
   `({ $fields,* $[: $tyStx]? })
 
 /--
-Delaborates a function application in explicit mode, and ensures the resulting
-head syntax is wrapped with `@`.
+Given an application of `numArgs` arguments with the calculated `ParamKind`s,
+returns `true` if we should wrap the applied function with `@` when we are in explicit mode.
 -/
-def delabAppExplicitCore (maxArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) (tagAppFn : Bool) : Delab := do
-  let (fnStx, _, argStxs) ← withBoundedAppFnArgs maxArgs
+def needsExplicit (f : Expr) (numArgs : Nat) (paramKinds : Array ParamKind) : Bool :=
+  if paramKinds.size == 0 && 0 < numArgs && f matches .const _ [] then
+    -- Error calculating ParamKinds,
+    -- but we presume that the universe list has been intentionally erased, for example by LCNF.
+    -- The arguments in this case are *only* the explicit arguments, so we don't want to prefix with `@`.
+    false
+  else
+    -- Error calculating ParamKinds, so return `true` to be safe
+    paramKinds.size < numArgs
+    -- One of the supplied parameters isn't explicit
+    || paramKinds[:numArgs].any (fun param => !param.bInfo.isExplicit)
+    -- The next parameter is implicit or inst implicit
+    || (numArgs < paramKinds.size && paramKinds[numArgs]!.bInfo matches .implicit | .instImplicit)
+    -- One of the parameters after the supplied parameters is explicit but not regular explicit.
+    || paramKinds[numArgs:].any (fun param => param.bInfo.isExplicit && !param.isRegularExplicit)
+
+/--
+Delaborates a function application in explicit mode, and ensures the resulting
+head syntax is wrapped with `@` if needed.
+-/
+def delabAppExplicitCore (numArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) : Delab := do
+  let (fnStx, _, argStxs) ← withBoundedAppFnArgs numArgs
     (do
-      let stx ← withOptionAtCurrPos `pp.tagAppFns tagAppFn delabHead
-      let needsExplicit := stx.raw.getKind != ``Lean.Parser.Term.explicit
-      let stx ← if needsExplicit then `(@$stx) else pure stx
+      let stx ← delabHead
+      let insertExplicit := !stx.raw.isOfKind ``Lean.Parser.Term.explicit && needsExplicit (← getExpr) numArgs paramKinds
+      let stx ← if insertExplicit then `(@$stx) else pure stx
       pure (stx, paramKinds.toList, #[]))
     (fun ⟨fnStx, paramKinds, argStxs⟩ => do
-      let isInstImplicit := match paramKinds with
-                            | [] => false
-                            | param :: _ => param.bInfo == BinderInfo.instImplicit
+      let isInstImplicit := paramKinds.head? |>.map (·.bInfo == .instImplicit) |>.getD false
       let argStx ← if ← getPPOption getPPAnalysisHole then `(_)
                    else if isInstImplicit == true then
-                     let stx ← if ← getPPOption getPPInstances then delab else `(_)
-                     if ← getPPOption getPPInstanceTypes then
-                       let typeStx ← withType delab
-                       `(($stx : $typeStx))
-                     else pure stx
+                     withTypeAscription (cond := ← getPPOption getPPInstanceTypes) do
+                       if ← getPPOption getPPInstances then delab else `(_)
                    else delab
       pure (fnStx, paramKinds.tailD [], argStxs.push argStx))
   return Syntax.mkApp fnStx argStxs
 
 /--
 Delaborates a function application in the standard mode, where implicit arguments are generally not
-included.
--/
-def delabAppImplicitCore (maxArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) (tagAppFn : Bool) : Delab := do
-  -- TODO: always call the unexpanders, make them guard on the right # args?
-  let (fnStx, _, argStxs) ← withBoundedAppFnArgs maxArgs
-    (do
-      let stx ← withOptionAtCurrPos `pp.tagAppFns tagAppFn delabHead
-      return (stx, paramKinds.toList, #[]))
-    (fun (fnStx, paramKinds, argStxs) => do
-      let arg ← getExpr
-      let opts ← getOptions
-      let mkNamedArg (name : Name) (argStx : Syntax) : DelabM Syntax := do
-        `(Parser.Term.namedArgument| ($(mkIdent name) := $argStx))
-      let argStx? : Option Syntax ←
-        if ← getPPOption getPPAnalysisSkip then pure none
-        else if ← getPPOption getPPAnalysisHole then `(_)
-        else
-          match paramKinds with
-          | [] => delab
-          | param :: rest =>
-            if param.defVal.isSome && rest.isEmpty then
-              let v := param.defVal.get!
-              if !v.hasLooseBVars && v == arg then pure none else delab
-            else if !param.isRegularExplicit && param.defVal.isNone then
-              if ← getPPOption getPPAnalysisNamedArg <||> (pure (param.name == `motive) <&&> shouldShowMotive arg opts) then some <$> mkNamedArg param.name (← delab) else pure none
-            else delab
-      let argStxs := match argStx? with
-        | none => argStxs
-        | some stx => argStxs.push stx
-      pure (fnStx, paramKinds.tailD [], argStxs))
-  let stx := Syntax.mkApp fnStx argStxs
+included, unless `pp.analysis.namedArg` is set at that argument.
 
-  if ← isRegularApp maxArgs then
-    (guard (← getPPOption getPPNotation) *> unexpandRegularApp stx)
-    <|> (guard (← getPPOption getPPStructureInstances) *> unexpandStructureInstance stx)
-    <|> pure stx
-  else pure stx
+This delaborator is where `app_unexpander`s and the structure instance unexpander are applied.
+
+Assumes `numArgs ≤ paramKinds.size`.
+-/
+def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) : Delab := do
+  let (shouldUnexpand, fnStx, _, _, argStxs, argData) ←
+    withBoundedAppFnArgs numArgs
+      (do
+        let head ← getExpr
+        let shouldUnexpand ← pure (unexpand && head.consumeMData.isConst)
+          <&&> not <$> withMDatasOptions (getPPOption getPPUniverses <||> getPPOption getPPAnalysisBlockImplicit)
+        return (shouldUnexpand, ← delabHead, numArgs, paramKinds.toList, Array.mkEmpty numArgs, (Array.mkEmpty numArgs).push (shouldUnexpand, 0)))
+      (fun (shouldUnexpand, fnStx, remainingArgs, paramKinds, argStxs, argData) => do
+        /-
+        - `argStxs` is the accumulated array of arguments that should be pretty printed
+        - `argData` is a list of `Bool × Nat` used to figure out:
+          1. whether an unexpander could be used for the prefix up to this argument and
+          2. how many arguments we need to include after this one when annotating the result of unexpansion.
+          Argument `argStxs[i]` corresponds to `argData[i+1]`, with `argData[0]` being for the head itself.
+        -/
+        let (argUnexpandable, stx?) ← mkArgStx (remainingArgs - 1) paramKinds
+        let shouldUnexpand := shouldUnexpand && argUnexpandable
+        let (argStxs, argData) :=
+          match stx?, argData.back with
+          -- By default, a pretty-printed argument accounts for just itself.
+          | some stx, _ => (argStxs.push stx, argData.push (shouldUnexpand, 1))
+          -- A non-pretty-printed argument is accounted for by the previous pretty printed one.
+          | none, (_, argCount) => (argStxs, argData.pop.push (shouldUnexpand, argCount + 1))
+        return (shouldUnexpand, fnStx, remainingArgs - 1, paramKinds.tailD [], argStxs, argData))
+  if ← pure (argData.any Prod.fst) <&&> getPPOption getPPNotation then
+    -- Try using an app unexpander for a prefix of the arguments.
+    if let some stx ← (some <$> tryAppUnexpanders fnStx argStxs argData) <|> pure none then
+      return stx
+  let stx := Syntax.mkApp fnStx argStxs
+  if ← pure shouldUnexpand <&&> getPPOption getPPStructureInstances then
+    -- Try using the structure instance unexpander.
+    -- It only makes sense applying this to the entire application, since structure instances cannot themselves be applied.
+    if let some stx ← (some <$> unexpandStructureInstance stx) <|> pure none then
+      return stx
+  return stx
+where
+  mkNamedArg (name : Name) (argStx : Syntax) : DelabM (Bool × Option Syntax) :=
+    return (false, ← `(Parser.Term.namedArgument| ($(mkIdent name) := $argStx)))
+  /--
+  If the argument should be pretty printed then it returns the syntax for that argument.
+  The boolean is `false` if an unexpander should not be used for the application due to this argument.
+  The argumnet `remainingArgs` is the number of arguments in the application after this one.
+  -/
+  mkArgStx (remainingArgs : Nat) (paramKinds : List ParamKind) : DelabM (Bool × Option Syntax) := do
+    if ← getPPOption getPPAnalysisSkip then return (true, none)
+    else if ← getPPOption getPPAnalysisHole then return (true, ← `(_))
+    else
+      let arg ← getExpr
+      let param :: _ := paramKinds | unreachable!
+      if ← getPPOption getPPAnalysisNamedArg then
+        mkNamedArg param.name (← delab)
+      else if param.defVal.isSome && remainingArgs == 0 && param.defVal.get! == arg then
+        -- Assumption: `useAppExplicit` has already detected whether it is ok to omit this argument
+        return (true, none)
+      else if param.bInfo.isExplicit then
+        return (true, ← delab)
+      else if ← pure (param.name == `motive) <&&> shouldShowMotive arg (← getOptions) then
+        mkNamedArg param.name (← delab)
+      else
+        return (true, none)
+  /--
+  Runs the given unexpanders, returning the resulting syntax if any are applicable, and otherwise fails.
+  -/
+  tryUnexpand (fs : List Unexpander) (stx : Syntax) : DelabM Syntax := do
+    let ref ← getRef
+    fs.firstM fun f =>
+      match f stx |>.run ref |>.run () with
+      | EStateM.Result.ok stx _ => return stx
+      | _ => failure
+  /--
+  If the expression is a candidate for app unexpanders,
+  try applying an app unexpander using some prefix of the arguments, longest prefix first.
+  This function makes sure that the unexpanded syntax is annotated and given TermInfo so that it is hoverable in the InfoView.
+  -/
+  tryAppUnexpanders (fnStx : Term) (argStxs : Array Syntax) (argData : Array (Bool × Nat)) : Delab := do
+    let .const c _ := (← getExpr).getAppFn.consumeMData | unreachable!
+    let fs := appUnexpanderAttribute.getValues (← getEnv) c
+    if fs.isEmpty then failure
+    let rec go (prefixArgs : Nat) : DelabM Term := do
+      let (unexpand, argCount) := argData[prefixArgs]!
+      match prefixArgs with
+      | 0 =>
+        guard unexpand
+        let stx ← tryUnexpand fs fnStx
+        return Syntax.mkApp (← annotateTermInfo stx) argStxs
+      | prefixArgs' + 1 =>
+        (do guard unexpand
+            let stx ← tryUnexpand fs <| Syntax.mkApp fnStx (argStxs.extract 0 prefixArgs)
+            return Syntax.mkApp (← annotateTermInfo stx) (argStxs.extract prefixArgs argStxs.size))
+        <|> withBoundedAppFn argCount (go prefixArgs')
+    go argStxs.size
+
+/--
+Returns true if an application should use explicit mode when delaborating.
+-/
+def useAppExplicit (numArgs : Nat) (paramKinds : Array ParamKind) : DelabM Bool := do
+  -- If `pp.explicit` is set, then use explicit mode.
+  -- (Note that explicit mode can decide to omit `@` if the application has no implicit arguments.)
+  if ← getPPOption getPPExplicit then return true
+
+  -- If there was an error collecting ParamKinds, fall back to explicit mode.
+  if paramKinds.size < numArgs then return true
+
+  if numArgs < paramKinds.size then
+    let nextParam := paramKinds[numArgs]!
+
+    -- If the next parameter is implicit or inst implicit, fall back to explicit mode.
+    -- This is necessary for `@Eq` for example.
+    if nextParam.bInfo matches .implicit | .instImplicit then return true
+
+  -- If any of the next parameters is explicit but has an optional value or is an autoparam, fall back to explicit mode.
+  -- This is necessary since these are eagerly processed when elaborating.
+  if paramKinds[numArgs:].any fun param => param.bInfo.isExplicit && !param.isRegularExplicit then return true
+
+  return false
 
 /--
 Delaborates applications. Removes up to `maxArgs` arguments to form
 the "head" of the application and delaborates the head using `delabHead`.
-The remaining arguments are processed depending on whether heuristics indicate that the application
-should be delaborated using `@`.
+Then the application is then processed in explicit mode or implicit mode depending on which should be used.
 -/
-def delabAppCore (maxArgs : Nat) (delabHead : Delab) : Delab := do
-  let tagAppFn ← getPPOption getPPTagAppFns
+def delabAppCore (unexpand : Bool) (maxArgs : Nat) (delabHead : Delab) : Delab := do
   let e ← getExpr
-  let paramKinds ← getParamKinds (e.getBoundedAppFn maxArgs) (e.getBoundedAppArgs maxArgs)
+  let args := e.getBoundedAppArgs maxArgs
+  let paramKinds ← getParamKinds (e.getBoundedAppFn maxArgs) args
 
-  let useExplicit ← useAppExplicit paramKinds
+  let useExplicit ← useAppExplicit args.size paramKinds
 
   if useExplicit then
-    delabAppExplicitCore maxArgs delabHead paramKinds tagAppFn
+    delabAppExplicitCore args.size delabHead paramKinds
   else
-    delabAppImplicitCore maxArgs delabHead paramKinds tagAppFn
+    delabAppImplicitCore unexpand args.size delabHead paramKinds
 
 /--
 Default delaborator for applications.
 -/
 @[builtin_delab app]
 def delabApp : Delab := do
+  let tagAppFn ← getPPOption getPPTagAppFns
   let e ← getExpr
-  delabAppCore e.getAppNumArgs delabAppFn
+  delabAppCore true e.getAppNumArgs (delabAppFn tagAppFn)
+where
+  delabAppFn (tagAppFn : Bool) : Delab :=
+    withOptionAtCurrPos `pp.tagAppFns tagAppFn do
+      if (← getExpr).consumeMData.isConst then
+        withMDatasOptions delabConst
+      else
+        delab
 
 /--
 The `withOverApp` combinator allows delaborators to handle "over-application" by using the core
@@ -344,7 +423,7 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
   if n == arity then
     x
   else
-    delabAppCore (n - arity) (withAnnotateTermInfo x)
+    delabAppCore false (n - arity) (withAnnotateTermInfo x)
 
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where

src/Lean/PrettyPrinter/Delaborator/SubExpr.lean

@@ -65,6 +65,16 @@ def withBoundedAppFnArgs (maxArgs : Nat) (xf : m α) (xa : α → m α) : m α :
     withAppArg (xa acc)
   | _, _ => xf
 
+/--
+Runs `xf` in the context of `Lean.Expr.getBoundedAppFn maxArgs`.
+This is equivalent to `withBoundedAppFnArgs maxArgs xf pure`.
+-/
+def withBoundedAppFn (maxArgs : Nat) (xf : m α) : m α := do
+  let e ← getExpr
+  let numArgs := min maxArgs e.getAppNumArgs
+  let newPos := (← getPos).pushNaryFn numArgs
+  withTheReader SubExpr (fun cfg => { cfg with expr := e.getBoundedAppFn numArgs, pos := newPos }) xf
+
 def withBindingDomain (x : m α) : m α := do descend (← getExpr).bindingDomain! 0 x
 
 def withBindingBody (n : Name) (x : m α) : m α := do

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -6,6 +6,7 @@ Authors: Daniel Selsam
 prelude
 import Lean.Data.RBMap
 import Lean.Meta.SynthInstance
+import Lean.Meta.CtorRecognizer
 import Lean.Util.FindMVar
 import Lean.Util.FindLevelMVar
 import Lean.Util.CollectLevelParams
@@ -152,7 +153,7 @@ def isIdLike (arg : Expr) : Bool :=
   | _ => false
 
 def isStructureInstance (e : Expr) : MetaM Bool := do
-  match e.isConstructorApp? (← getEnv) with
+  match (← isConstructorApp? e) with
   | some s => return isStructure (← getEnv) s.induct
   | none   => return false
 
@@ -288,7 +289,7 @@ where
 partial def isTrivialBottomUp (e : Expr) : AnalyzeM Bool := do
   let opts ← getOptions
   return e.isFVar
-         || e.isConst || e.isMVar || e.isNatLit || e.isStringLit || e.isSort
+         || e.isConst || e.isMVar || e.isRawNatLit || e.isStringLit || e.isSort
          || (getPPAnalyzeTrustOfNat opts && e.isAppOfArity ``OfNat.ofNat 3)
          || (getPPAnalyzeTrustOfScientific opts && e.isAppOfArity ``OfScientific.ofScientific 5)
 

src/Lean/Server/CodeActions.lean

@@ -5,164 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: E.W.Ayers
 -/
 prelude
-import Lean.Server.FileWorker.RequestHandling
-import Lean.Server.InfoUtils
-
-namespace Lean.Server
-
-open Lsp
-open RequestM
-open Snapshots
-
-/-- A code action optionally supporting a lazy code action computation that is only run when the user clicks on
-the code action in the editor.
-
-If you want to use the lazy feature, make sure that the `edit?` field on the `eager` code action result is `none`.
- -/
-structure LazyCodeAction where
-  /-- This is the initial code action that is sent to the server, to implement -/
-  eager : CodeAction
-  lazy? : Option (IO CodeAction) := none
-
-/-- Passed as the `data?` field of `Lsp.CodeAction` to recover the context of the code action. -/
-structure CodeActionResolveData where
-  params : CodeActionParams
-  /-- Name of CodeActionProvider that produced this request. -/
-  providerName : Name
-  /-- Index in the list of code action that the given provider generated. -/
-  providerResultIndex : Nat
-  deriving ToJson, FromJson
-
-def CodeAction.getFileSource! (ca : CodeAction) : DocumentUri :=
-  let r : Except String DocumentUri := do
-    let some data := ca.data?
-      | throw s!"no data param on code action {ca.title}"
-    let data : CodeActionResolveData ← fromJson? data
-    return data.params.textDocument.uri
-  match r with
-  | Except.ok uri => uri
-  | Except.error e => panic! e
-
-instance : FileSource CodeAction where
-  fileSource x := CodeAction.getFileSource! x
-
-
-instance : Coe CodeAction LazyCodeAction where
-  coe c := { eager := c }
-
-/-- A code action provider is a function for providing LSP code actions for an editor.
-You can register them with the `@[code_action_provider]` attribute.
-
-This is a low-level interface for making LSP code actions.
-This interface can be used to implement the following applications:
-- refactoring code: adding underscores to unused variables,
-- suggesting imports
-- document-level refactoring: removing unused imports, sorting imports, formatting.
-- Helper suggestions for working with type holes (`_`)
-- Helper suggestions for tactics.
-
-When implementing your own `CodeActionProvider`, we assume that no long-running computations are allowed.
-If you need to create a code-action with a long-running computation, you can use the `lazy?` field on `LazyCodeAction`
-to perform the computation after the user has clicked on the code action in their editor.
--/
-def CodeActionProvider := CodeActionParams → Snapshot → RequestM (Array LazyCodeAction)
-deriving instance Inhabited for CodeActionProvider
-
-private builtin_initialize builtinCodeActionProviders : IO.Ref (NameMap CodeActionProvider) ←
-  IO.mkRef ∅
-
-def addBuiltinCodeActionProvider (decl : Name) (provider : CodeActionProvider) : IO Unit :=
-  builtinCodeActionProviders.modify (·.insert decl provider)
-
-builtin_initialize codeActionProviderExt : SimplePersistentEnvExtension Name NameSet ← registerSimplePersistentEnvExtension {
-  addImportedFn := fun nss => nss.foldl (fun acc ns => ns.foldl NameSet.insert acc) ∅
-  addEntryFn := fun s n => s.insert n
-  toArrayFn  := fun es => es.toArray.qsort Name.quickLt
-}
-
-builtin_initialize
-  let mkAttr (builtin : Bool) (name : Name) := registerBuiltinAttribute {
-    name
-    descr           := (if builtin then "(builtin) " else "") ++
-      "Use to decorate methods for suggesting code actions. This is a low-level interface for making code actions."
-    applicationTime := .afterCompilation
-    add             := fun decl stx kind => do
-      Attribute.Builtin.ensureNoArgs stx
-      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
-      unless (← getConstInfo decl).type.isConstOf ``CodeActionProvider do
-        throwError "invalid attribute '{name}', must be of type `Lean.Server.CodeActionProvider`"
-      let env ← getEnv
-      if builtin then
-        let h := mkConst decl
-        declareBuiltin decl <| mkApp2 (mkConst ``addBuiltinCodeActionProvider) (toExpr decl) h
-      else
-        setEnv <| codeActionProviderExt.addEntry env decl
-  }
-  mkAttr true `builtin_code_action_provider
-  mkAttr false `code_action_provider
-
-private unsafe def evalCodeActionProviderUnsafe [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider := do
-  evalConstCheck CodeActionProvider ``CodeActionProvider declName
-
-/-- Get a `CodeActionProvider` from a declaration name. -/
-@[implemented_by evalCodeActionProviderUnsafe]
-private opaque evalCodeActionProvider [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider
-
-/-- Handles a `textDocument/codeAction` request.
-
-This is implemented by calling all of the registered `CodeActionProvider` functions.
-
-[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_codeAction). -/
-def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array CodeAction)) := do
-  let doc ← readDoc
-  let pos := doc.meta.text.lspPosToUtf8Pos params.range.end
-  withWaitFindSnap doc (fun s => s.endPos ≥ pos)
-    (notFoundX := return #[])
-    fun snap => do
-      let caps ← RequestM.runCoreM snap do
-        let env ← getEnv
-        let names := codeActionProviderExt.getState env |>.toArray
-        let caps ← names.mapM evalCodeActionProvider
-        return (← builtinCodeActionProviders.get).toList.toArray ++ Array.zip names caps
-      caps.concatMapM fun (providerName, cap) => do
-        let cas ← cap params snap
-        cas.mapIdxM fun i lca => do
-          if lca.lazy?.isNone then return lca.eager
-          let data : CodeActionResolveData := {
-            params, providerName, providerResultIndex := i
-          }
-          let j : Json := toJson data
-          let ca := { lca.eager with data? := some j }
-          return ca
-
-builtin_initialize
-  registerLspRequestHandler "textDocument/codeAction" CodeActionParams (Array CodeAction) handleCodeAction
-
-/-- Handler for `"codeAction/resolve"`.
-
-[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#codeAction_resolve)
--/
-def handleCodeActionResolve (param : CodeAction) : RequestM (RequestTask CodeAction) := do
-  let doc ← readDoc
-  let some data := param.data?
-    | throw (RequestError.invalidParams "Expected a data field on CodeAction.")
-  let data : CodeActionResolveData ← liftExcept <| Except.mapError RequestError.invalidParams <| fromJson? data
-  let pos := doc.meta.text.lspPosToUtf8Pos data.params.range.end
-  withWaitFindSnap doc (fun s => s.endPos ≥ pos)
-    (notFoundX := throw <| RequestError.internalError "snapshot not found")
-    fun snap => do
-      let cap ← match (← builtinCodeActionProviders.get).find? data.providerName with
-        | some cap => pure cap
-        | none     => RequestM.runCoreM snap <| evalCodeActionProvider data.providerName
-      let cas ← cap data.params snap
-      let some ca := cas[data.providerResultIndex]?
-        | throw <| RequestError.internalError s!"Failed to resolve code action index {data.providerResultIndex}."
-      let some lazy := ca.lazy?
-        | throw <| RequestError.internalError s!"Can't resolve; nothing further to resolve."
-      let r ← liftM lazy
-      return r
-
-builtin_initialize
-  registerLspRequestHandler "codeAction/resolve" CodeAction CodeAction handleCodeActionResolve
-
-end Lean.Server
+import Lean.Server.CodeActions.Attr
+import Lean.Server.CodeActions.Basic
+import Lean.Server.CodeActions.Provider

src/Lean/Server/CodeActions/Attr.lean

@@ -0,0 +1,150 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+prelude
+import Lean.Server.CodeActions.Basic
+
+/-!
+# Initial setup for code action attributes
+
+* Attribute `@[hole_code_action]` collects code actions which will be called
+  on each occurrence of a hole (`_`, `?_` or `sorry`).
+
+* Attribute `@[tactic_code_action]` collects code actions which will be called
+  on each occurrence of a tactic.
+
+* Attribute `@[command_code_action]` collects code actions which will be called
+  on each occurrence of a command.
+-/
+namespace Lean.CodeAction
+
+open Lean Elab Server Lsp RequestM Snapshots
+
+/-- A hole code action extension. -/
+abbrev HoleCodeAction :=
+  CodeActionParams → Snapshot →
+  (ctx : ContextInfo) → (hole : TermInfo) → RequestM (Array LazyCodeAction)
+
+/-- Read a hole code action from a declaration of the right type. -/
+def mkHoleCodeAction (n : Name) : ImportM HoleCodeAction := do
+  let { env, opts, .. } ← read
+  IO.ofExcept <| unsafe env.evalConstCheck HoleCodeAction opts ``HoleCodeAction n
+
+/-- An extension which collects all the hole code actions. -/
+builtin_initialize holeCodeActionExt :
+    PersistentEnvExtension Name (Name × HoleCodeAction) (Array Name × Array HoleCodeAction) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure (#[], #[])
+    addImportedFn := fun as => return (#[], ← as.foldlM (init := #[]) fun m as =>
+      as.foldlM (init := m) fun m a => return m.push (← mkHoleCodeAction a))
+    addEntryFn := fun (s₁, s₂) (n₁, n₂) => (s₁.push n₁, s₂.push n₂)
+    exportEntriesFn := (·.1)
+  }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name := `hole_code_action
+    descr := "Declare a new hole code action, to appear in the code actions on ?_ and _"
+    applicationTime := .afterCompilation
+    add := fun decl stx kind => do
+      Attribute.Builtin.ensureNoArgs stx
+      unless kind == AttributeKind.global do
+        throwError "invalid attribute 'hole_code_action', must be global"
+      if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
+      modifyEnv (holeCodeActionExt.addEntry · (decl, ← mkHoleCodeAction decl))
+  }
+
+/-- A command code action extension. -/
+abbrev CommandCodeAction :=
+  CodeActionParams → Snapshot → (ctx : ContextInfo) → (node : InfoTree) →
+  RequestM (Array LazyCodeAction)
+
+/-- Read a command code action from a declaration of the right type. -/
+def mkCommandCodeAction (n : Name) : ImportM CommandCodeAction := do
+  let { env, opts, .. } ← read
+  IO.ofExcept <| unsafe env.evalConstCheck CommandCodeAction opts ``CommandCodeAction n
+
+/-- An entry in the command code actions extension, containing the attribute arguments. -/
+structure CommandCodeActionEntry where
+  /-- The declaration to tag -/
+  declName : Name
+  /-- The command kinds that this extension supports.
+  If empty it is called on all command kinds. -/
+  cmdKinds : Array Name
+  deriving Inhabited
+
+/-- The state of the command code actions extension. -/
+structure CommandCodeActions where
+  /-- The list of command code actions to apply on any command. -/
+  onAnyCmd : Array CommandCodeAction := {}
+  /-- The list of command code actions to apply when a particular command kind is highlighted. -/
+  onCmd : NameMap (Array CommandCodeAction) := {}
+  deriving Inhabited
+
+/-- Insert a command code action entry into the `CommandCodeActions` structure. -/
+def CommandCodeActions.insert (self : CommandCodeActions)
+    (tacticKinds : Array Name) (action : CommandCodeAction) : CommandCodeActions :=
+  if tacticKinds.isEmpty then
+    { self with onAnyCmd := self.onAnyCmd.push action }
+  else
+    { self with onCmd := tacticKinds.foldl (init := self.onCmd) fun m a =>
+        m.insert a ((m.findD a #[]).push action) }
+
+builtin_initialize builtinCmdCodeActions : IO.Ref CommandCodeActions ← IO.mkRef {}
+
+def insertBuiltin (args : Array Name) (proc : CommandCodeAction) : IO Unit := do
+  builtinCmdCodeActions.modify fun self => self.insert args proc
+
+/-- An extension which collects all the command code actions. -/
+builtin_initialize cmdCodeActionExt :
+    PersistentEnvExtension CommandCodeActionEntry (CommandCodeActionEntry × CommandCodeAction)
+      (Array CommandCodeActionEntry × CommandCodeActions) ←
+  registerPersistentEnvExtension {
+    mkInitial := return (#[], ← builtinCmdCodeActions.get)
+    addImportedFn := fun as => do
+      let init ← builtinCmdCodeActions.get
+      return (#[], ← as.foldlM (init := init) fun m as =>
+      as.foldlM (init := m) fun m ⟨name, kinds⟩ =>
+        return m.insert kinds (← mkCommandCodeAction name))
+    addEntryFn := fun (s₁, s₂) (e, n₂) => (s₁.push e, s₂.insert e.cmdKinds n₂)
+    exportEntriesFn := (·.1)
+  }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name := `command_code_action
+    descr := "Declare a new command code action, to appear in the code actions on commands"
+    applicationTime := .afterCompilation
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do
+        throwError "invalid attribute 'command_code_action', must be global"
+      let `(attr| command_code_action $args*) := stx | return
+      let args ← args.mapM resolveGlobalConstNoOverloadWithInfo
+      if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
+      modifyEnv (cmdCodeActionExt.addEntry · (⟨decl, args⟩, ← mkCommandCodeAction decl))
+  }
+
+private def addBuiltin (declName : Name) (args : Array Name) : AttrM Unit := do
+  let go : MetaM Unit := do
+    let val := mkAppN (mkConst ``insertBuiltin) #[toExpr args, mkConst declName]
+    let initDeclName ← mkFreshUserName (declName ++ `declare)
+    declareBuiltin initDeclName val
+  go.run' {}
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `builtin_command_code_action
+    descr           := "Declare a new builtin command code action, to appear in the code actions on commands"
+    applicationTime := .afterCompilation
+    add             := fun decl stx kind => do
+      unless kind == AttributeKind.global do
+        throwError "invalid attribute 'command_code_action', must be global"
+      let `(attr| builtin_command_code_action $args*) := stx |
+        throwError "unexpected 'command_code_action' attribute syntax"
+      let args ← args.mapM resolveGlobalConstNoOverloadWithInfo
+      if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
+      addBuiltin decl args
+  }