chore: update stage0

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

RELEASES.md

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

src/CMakeLists.txt

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

src/Init/Coe.lean

@@ -321,7 +321,7 @@ Helper definition used by the elaborator. It is not meant to be used directly by
 This is used for coercions between monads, in the case where we want to apply
 a monad lift and a coercion on the result type at the same time.
 -/
-@[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/BitVec/Basic.lean

@@ -124,13 +124,20 @@ section Int
 
 /-- Interpret the bitvector as an integer stored in two's complement form. -/
 protected def toInt (a : BitVec n) : Int :=
-  if a.msb then Int.ofNat a.toNat - Int.ofNat (2^n) else a.toNat
+  if 2 * a.toNat < 2^n then
+    a.toNat
+  else
+    (a.toNat : Int) - (2^n : Nat)
 
 /-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`.  -/
-protected def ofInt (n : Nat) (i : Int) : BitVec n :=
-  match i with
-  | Int.ofNat x => .ofNat n x
-  | Int.negSucc x => BitVec.ofNatLt (2^n - x % 2^n - 1) (by omega)
+protected def ofInt (n : Nat) (i : Int) : BitVec n := .ofNatLt (i % (Int.ofNat (2^n))).toNat (by
+  apply (Int.toNat_lt _).mpr
+  · apply Int.emod_lt_of_pos
+    exact Int.ofNat_pos.mpr (Nat.two_pow_pos _)
+  · apply Int.emod_nonneg
+    intro eq
+    apply Nat.ne_of_gt (Nat.two_pow_pos n)
+    exact Int.ofNat_inj.mp eq)
 
 instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩
 

src/Init/Data/BitVec/Lemmas.lean

@@ -133,21 +133,35 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
   · simp [BitVec.eq_nil x]
   · simp
 
-@[bv_toNat] theorem getLsb_last (x : BitVec (w + 1)) :
-    x.getLsb w = decide (2 ^ w ≤ x.toNat) := by
-  simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
+@[bv_toNat] theorem getLsb_last (x : BitVec w) :
+    x.getLsb (w-1) = decide (2 ^ (w-1) ≤ x.toNat) := by
+  rcases w with rfl | w
+  · simp
+  · simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
     Nat.sub_zero, Nat.and_one_is_mod, Bool.true_and, Nat.shiftRight_eq_div_pow]
-  rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
-  · simp [Nat.div_eq_of_lt h, h]
-  · simp only [h]
-    rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
-    · decide
-    · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
-      omega
+    rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
+    · simp [Nat.div_eq_of_lt h, h]
+    · simp only [h]
+      rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
+      · decide
+      · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
+        omega
 
-@[bv_toNat] theorem msb_eq_decide (x : BitVec (w + 1)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by
+@[bv_toNat] theorem getLsb_succ_last (x : BitVec (w + 1)) :
+    x.getLsb w = decide (2 ^ w ≤ x.toNat) := getLsb_last x
+
+@[bv_toNat] theorem msb_eq_decide (x : BitVec w) : BitVec.msb x = decide (2 ^ (w-1) ≤ x.toNat) := by
   simp [msb_eq_getLsb_last, getLsb_last]
 
+theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat ≥ 2^(n-1) := by
+  match n with
+  | 0 =>
+    simp [BitVec.msb, BitVec.getMsb] at p
+  | n + 1 =>
+    simp [BitVec.msb_eq_decide] at p
+    simp only [Nat.add_sub_cancel]
+    exact p
+
 /-! ### cast -/
 
 @[simp, bv_toNat] theorem toNat_cast (h : w = v) (x : BitVec w) : (cast h x).toNat = x.toNat := rfl
@@ -163,6 +177,53 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
 @[simp] theorem msb_cast (h : w = v) (x : BitVec w) : (cast h x).msb = x.msb := by
   simp [BitVec.msb]
 
+/-! ### toInt/ofInt -/
+
+/-- Prove equality of bitvectors in terms of nat operations. -/
+theorem toInt_eq_toNat_cond (i : BitVec n) :
+    i.toInt =
+      if 2*i.toNat < 2^n then
+        (i.toNat : Int)
+      else
+        (i.toNat : Int) - (2^n : Nat) := by
+  unfold BitVec.toInt
+  split <;> omega
+
+theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by
+  simp only [toInt_eq_toNat_cond]
+  split
+  case inl g =>
+    rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
+    omega
+  case inr g =>
+    rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
+    omega
+
+/-- Prove equality of bitvectors in terms of nat operations. -/
+theorem eq_of_toInt_eq {i j : BitVec n} : i.toInt = j.toInt → i = j := by
+  intro eq
+  simp [toInt_eq_toNat_cond] at eq
+  apply eq_of_toNat_eq
+  revert eq
+  have _ilt := i.isLt
+  have _jlt := j.isLt
+  split <;> split <;> omega
+
+@[simp] theorem toNat_ofInt {n : Nat} (i : Int) :
+  (BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat := by
+  unfold BitVec.ofInt
+  simp
+
+theorem toInt_ofNat {n : Nat} (x : Nat) :
+  (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by
+  simp [toInt_eq_toNat_bmod]
+
+@[simp] theorem toInt_ofInt {n : Nat} (i : Int) :
+  (BitVec.ofInt n i).toInt = i.bmod (2^n) := by
+  have _ := Nat.two_pow_pos n
+  have p : 0 ≤ i % (2^n : Nat) := by omega
+  simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p]
+
 /-! ### zeroExtend and truncate -/
 
 @[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
@@ -198,6 +259,24 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
   apply eq_of_toNat_eq
   simp
 
+/-- Moves one-sided left toNat equality to BitVec equality. -/
+theorem toNat_eq_nat (x : BitVec w) (y : Nat)
+  : (x.toNat = y) ↔ (y < 2^w ∧ (x = y#w)) := by
+  apply Iff.intro
+  · intro eq
+    simp at eq
+    have lt := x.isLt
+    simp [eq] at lt
+    simp [←eq, lt, x.isLt]
+  · intro eq
+    simp [Nat.mod_eq_of_lt, eq]
+
+/-- Moves one-sided right toNat equality to BitVec equality. -/
+theorem nat_eq_toNat (x : BitVec w) (y : Nat)
+  : (y = x.toNat) ↔ (y < 2^w ∧ (x = y#w)) := by
+  rw [@eq_comm _ _ x.toNat]
+  apply toNat_eq_nat
+
 @[simp] theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend' ge x) i = getLsb x i := by
   simp [getLsb, toNat_zeroExtend']
@@ -599,4 +678,18 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   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/Int/DivMod.lean

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

src/Init/Data/Int/DivModLemmas.lean

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

src/Init/Data/Int/Lemmas.lean

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

src/Init/Data/Int/Order.lean

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

src/Init/Data/List/BasicAux.lean

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

src/Init/Data/List/Lemmas.lean

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

src/Init/Data/Nat/Basic.lean

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

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

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

src/Init/Data/Nat/Lemmas.lean

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

src/Init/Meta.lean

@@ -1362,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

@@ -613,3 +613,30 @@ 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
   | `($(_)) => `(())
 

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

@@ -1306,6 +1306,26 @@ used when closing the goal.
 -/
 syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
 
+/--
+`show_term tac` runs `tac`, then prints the generated term in the form
+"exact X Y Z" or "refine X ?_ Z" if there are remaining subgoals.
+
+(For some tactics, the printed term will not be human readable.)
+-/
+syntax (name := showTerm) "show_term " tacticSeq : tactic
+
+/--
+`show_term e` elaborates `e`, then prints the generated term.
+-/
+macro (name := showTermElab) tk:"show_term " t:term : term =>
+  `(term| no_implicit_lambda% (show_term_elab%$tk $t))
+
+/--
+The command `by?` will print a suggestion for replacing the proof block with a proof term
+using `show_term`.
+-/
+macro (name := by?) tk:"by?" t:tacticSeq : term => `(show_term%$tk by%$tk $t)
+
 end Tactic
 
 namespace Attr
@@ -1425,13 +1445,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| omega)
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
+macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
 
 /--
 `get_elem_tactic` is the tactic automatically called by the notation `arr[i]`
@@ -1442,6 +1463,24 @@ users are encouraged to extend `get_elem_tactic_trivial` instead of this tactic.
 -/
 macro "get_elem_tactic" : tactic =>
   `(tactic| first
+      /-
+      Recall that `macro_rules` are tried in reverse order.
+      We want `assumption` to be tried first.
+      This is important for theorems such as
+      ```
+      [simp] theorem getElem_pop (a : Array α) (i : Nat) (hi : i < a.pop.size) :
+      a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop ▸ hi) (Nat.sub_le _ _)) :=
+      ```
+      There is a proof embedded in the right-hand-side, and we want it to be just `hi`.
+      If `omega` is used to "fill" this proof, we will have a more complex proof term that
+      cannot be inferred by unification.
+      We hardcoded `assumption` here to ensure users cannot accidentaly break this IF
+      they add new `macro_rules` for `get_elem_tactic_trivial`.
+
+      TODO: Implement priorities for `macro_rules`.
+      TODO: Ensure we have a **high-priority** macro_rules for `get_elem_tactic_trivial` which is just `assumption`.
+      -/
+    | assumption
     | get_elem_tactic_trivial
     | fail "failed to prove index is valid, possible solutions:
   - Use `have`-expressions to prove the index is valid

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

@@ -48,3 +48,5 @@ import Lean.Elab.Calc
 import Lean.Elab.InheritDoc
 import Lean.Elab.ParseImportsFast
 import Lean.Elab.GuardMsgs
+import Lean.Elab.CheckTactic
+import Lean.Elab.MatchExpr

src/Lean/Elab/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) =>

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

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

src/Lean/Elab/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)

src/Lean/Elab/MatchExpr.lean

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

src/Lean/Elab/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

@@ -37,3 +37,4 @@ import Lean.Elab.Tactic.NormCast
 import Lean.Elab.Tactic.Symm
 import Lean.Elab.Tactic.SolveByElim
 import Lean.Elab.Tactic.LibrarySearch
+import Lean.Elab.Tactic.ShowTerm

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -372,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/Omega/Frontend.lean

@@ -68,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))

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

@@ -51,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)
@@ -76,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
@@ -243,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/ShowTerm.lean

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

src/Lean/Elab/Tactic/Simp.lean

@@ -353,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

@@ -25,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/Exception.lean

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

src/Lean/Expr.lean

@@ -801,7 +801,7 @@ def isType0 : Expr → Bool
 
 /-- Return `true` if the given expression is `.sort .zero` -/
 def isProp : Expr → Bool
-  | sort (.zero ..) => true
+  | sort .zero => true
   | _ => false
 
 /-- Return `true` if the given expression is a bound variable. -/
@@ -904,6 +904,14 @@ def appArg!' : Expr → Expr
   | app _ a   => a
   | _         => panic! "application expected"
 
+def appArg (e : Expr) (h : e.isApp) : Expr :=
+  match e, h with
+  | .app _ a, _ => a
+
+def appFn (e : Expr) (h : e.isApp) : Expr :=
+  match e, h with
+  | .app f _, _ => f
+
 def sortLevel! : Expr → Level
   | sort u => u
   | _      => panic! "sort expected"
@@ -1616,6 +1624,14 @@ partial def cleanupAnnotations (e : Expr) : Expr :=
   let e' := e.consumeMData.consumeTypeAnnotations
   if e' == e then e else cleanupAnnotations e'
 
+/--
+Similar to `appFn`, but also applies `cleanupAnnotations` to resulting function.
+This function is used compile the `match_expr` term.
+-/
+def appFnCleanup (e : Expr) (h : e.isApp) : Expr :=
+  match e, h with
+  | .app f _, _ => f.cleanupAnnotations
+
 def isFalse (e : Expr) : Bool :=
   e.cleanupAnnotations.isConstOf ``False
 

src/Lean/Meta/Basic.lean

@@ -254,7 +254,7 @@ structure PostponedEntry where
   ref  : Syntax
   lhs  : Level
   rhs  : Level
-  /-- Context for the surrounding `isDefEq` call when entry was created. -/
+  /-- Context for the surrounding `isDefEq` call when the entry was created. -/
   ctx? : Option DefEqContext
   deriving Inhabited
 
@@ -264,7 +264,7 @@ structure PostponedEntry where
 structure State where
   mctx             : MetavarContext := {}
   cache            : Cache := {}
-  /-- When `trackZetaDelta == true`, then any let-decl free variable that is zetaDelta expansion performed by `MetaM` is stored in `zetaDeltaFVarIds`. -/
+  /-- When `trackZetaDelta == true`, then any let-decl free variable that is zetaDelta-expanded by `MetaM` is stored in `zetaDeltaFVarIds`. -/
   zetaDeltaFVarIds : FVarIdSet := {}
   /-- Array of postponed universe level constraints -/
   postponed        : PersistentArray PostponedEntry := {}
@@ -1737,6 +1737,15 @@ def isDefEqNoConstantApprox (t s : Expr) : MetaM Bool :=
 def etaExpand (e : Expr) : MetaM Expr :=
   withDefault do forallTelescopeReducing (← inferType e) fun xs _ => mkLambdaFVars xs (mkAppN e xs)
 
+/--
+If `e` is of the form `?m ...` instantiate metavars
+-/
+def instantiateMVarsIfMVarApp (e : Expr) : MetaM Expr := do
+  if e.getAppFn.isMVar then
+    instantiateMVars e
+  else
+    return e
+
 end Meta
 
 builtin_initialize

src/Lean/Meta/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/Eqns.lean

@@ -131,8 +131,8 @@ def registerGetUnfoldEqnFn (f : GetUnfoldEqnFn) : IO Unit := do
   getUnfoldEqnFnsRef.modify (f :: ·)
 
 /--
-  Return a "unfold" theorem for the given declaration.
-  By default, we not create unfold theorems for nonrecursive definitions.
+  Return an "unfold" theorem for the given declaration.
+  By default, we do not create unfold theorems for nonrecursive definitions.
   You can use `nonRec := true` to override this behavior.
 -/
 def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) := withLCtx {} {} do

src/Lean/Meta/ExprLens.lean

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

src/Lean/Meta/LitValues.lean

@@ -78,7 +78,6 @@ def getBitVecValue? (e : Expr) : MetaM (Option ((n : Nat) × BitVec n)) := Optio
     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⟩
 
@@ -103,7 +102,7 @@ def getUInt64Value? (e : Expr) : MetaM (Option UInt64) := OptionT.run do
   return UInt64.ofNat n
 
 /--
-If `e` is literal value, ensure it is encoded using the standard representation.
+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
@@ -120,4 +119,32 @@ def normLitValue (e : Expr) : MetaM Expr := do
   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/Match.lean

@@ -7,6 +7,7 @@ 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
@@ -138,15 +139,21 @@ private def isValueTransition (p : Problem) : Bool :=
      | .var _ :: _ => true
      | _           => false
 
-private def isFinValueTransition (p : Problem) : MetaM Bool := do
+private def isValueOnlyTransitionCore (p : Problem) (isValue : Expr → MetaM Bool) : MetaM Bool := do
   if hasVarPattern p then return false
   if !hasValPattern p then return false
   p.alts.allM fun alt => do
      match alt.patterns with
-     | .val v :: _   => return (← getFinValue? v).isSome
+     | .val v :: _   => isValue v
      | .ctor .. :: _ => return true
      | _             => return false
 
+private def isFinValueTransition (p : Problem) : MetaM Bool :=
+  isValueOnlyTransitionCore p fun e => return (← getFinValue? e).isSome
+
+private def isBitVecValueTransition (p : Problem) : MetaM Bool :=
+  isValueOnlyTransitionCore p fun e => return (← getBitVecValue? e).isSome
+
 private def isArrayLitTransition (p : Problem) : Bool :=
   hasArrayLitPattern p && hasVarPattern p
   && p.alts.all fun alt => match alt.patterns with
@@ -409,14 +416,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
@@ -497,12 +503,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
@@ -647,15 +653,18 @@ private def expandIntValuePattern (p : Problem) : MetaM Problem := do
 
 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
+    let .val n :: ps := alt.patterns | return alt
+    let some ⟨n, v⟩ ← getFinValue? n | return alt
+    let p ← mkLt (toExpr v.val) (toExpr n)
+    let h ← mkDecideProof p
+    return { alt with patterns := .ctor ``Fin.mk [] [toExpr n] [.val (toExpr v.val), .inaccessible h] :: ps }
+  return { p with alts := alts }
+
+private def expandBitVecValuePattern (p : Problem) : MetaM Problem := do
+  let alts ← p.alts.mapM fun alt => do
+    let .val n :: ps := alt.patterns | return alt
+    let some ⟨_, v⟩ ← getBitVecValue? n | return alt
+    return { alt with patterns := .ctor ``BitVec.ofFin [] [] [.val (toExpr v.toFin)] :: ps }
   return { p with alts := alts }
 
 private def traceStep (msg : String) : StateRefT State MetaM Unit := do
@@ -710,6 +719,9 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
   else if (← isFinValueTransition p) then
     traceStep ("fin value to constructor")
     process (← expandFinValuePattern p)
+  else if (← isBitVecValueTransition p) then
+    traceStep ("bitvec value to constructor")
+    process (← expandBitVecValuePattern p)
   else if !isNextVar p then
     traceStep ("non variable")
     let p ← processNonVariable 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
@@ -250,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
@@ -378,7 +379,7 @@ 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

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/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

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -57,9 +57,6 @@ inductive DeclMod
   | /-- 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.
@@ -285,6 +282,26 @@ def mkLibrarySearchLemma (lem : Name) (mod : DeclMod) : MetaM Expr := do
   | .mp => mapForallTelescope (fun e => mkAppM ``Iff.mp #[e]) lem
   | .mpr => mapForallTelescope (fun e => mkAppM ``Iff.mpr #[e]) lem
 
+private def isVar (e : Expr) : Bool :=
+  match e with
+  | .bvar _ => true
+  | .fvar _ => true
+  | .mvar _ => true
+  | _ => false
+
+private def isNonspecific (type : Expr) : MetaM Bool := do
+  forallTelescope type fun _ tp =>
+    match tp.getAppFn with
+    | .bvar _ => pure true
+    | .fvar _ => pure true
+    | .mvar _ => pure true
+    | .const nm _ =>
+      if nm = ``Eq then
+        pure (tp.getAppArgsN 3 |>.all isVar)
+      else
+        pure false
+    | _ => pure false
+
 /--
 Tries to apply the given lemma (with symmetry modifier) to the goal,
 then tries to close subsequent goals using `solveByElim`.
@@ -294,9 +311,14 @@ 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
+  let ppMod (mod : DeclMod) : MessageData :=
+        match mod with | .none => "" | .mp => " with mp" | .mpr => " with mpr"
+  withTraceNode `Tactic.librarySearch (return m!"{emoji ·} trying {name}{ppMod mod} ") do
     setMCtx mctx
     let lem ← mkLibrarySearchLemma name mod
+    let lemType ← instantiateMVars (← inferType lem)
+    if ← isNonspecific lemType then
+      failure
     let newGoals ← goal.apply lem cfg
     try
       act newGoals

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
@@ -52,7 +53,8 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           let u1 ← getLevel α
           let u2 ← getLevel eType
           let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq
-          postprocessAppMVars `rewrite mvarId newMVars binderInfos (synthAssignedInstances := false)
+          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/Main.lean

@@ -69,7 +69,7 @@ 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
@@ -476,7 +476,7 @@ def processCongrHypothesis (h : Expr) : SimpM Bool := do
 def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do
   trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
   let thm ← mkConstWithFreshMVarLevels c.theoremName
-  let (xs, _, type) ← forallMetaTelescopeReducing (← inferType thm)
+  let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm)
   if c.hypothesesPos.any (· ≥ xs.size) then
     return none
   let isIff := type.isAppOf ``Iff
@@ -504,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) 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/Rewrite.lean

@@ -8,6 +8,7 @@ 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
@@ -16,9 +17,54 @@ import Lean.Meta.Tactic.Simp.Attr
 
 namespace Lean.Meta.Simp
 
-def synthesizeArgs (thmId : Origin) (xs : Array Expr) : SimpM Bool := do
-  for x in xs 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
+    -- We use the flag `tactic.skipAssignedInstances` for backward compatibility.
+    -- See comment below.
+    if !skipAssignedInstances && bi.isInstImplicit then
+      unless (← synthesizeInstance x type) do
+        return false
     /-
     We used to invoke `synthesizeInstance` for every instance implicit argument,
     to ensure the synthesized instance was definitionally equal to the one in
@@ -45,18 +91,7 @@ def synthesizeArgs (thmId : Origin) (xs : Array Expr) : SimpM Bool := do
         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
@@ -72,10 +107,10 @@ where
       trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to synthesize instance{indentExpr type}"
       return false
 
-private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
+private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
   let rec go (e : Expr) : SimpM (Option Result) := do
     if (← isDefEq lhs e) then
-      unless (← synthesizeArgs thm.origin xs) do
+      unless (← synthesizeArgs thm.origin bis xs) do
         return none
       let proof? ← if thm.rfl then
         pure none
@@ -126,25 +161,25 @@ def tryTheoremWithExtraArgs? (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat)
   withNewMCtxDepth do
     let val  ← thm.getValue
     let type ← inferType val
-    let (xs, _, type) ← forallMetaTelescopeReducing type
+    let (xs, bis, type) ← forallMetaTelescopeReducing type
     let type ← whnf (← instantiateMVars type)
     let lhs := type.appFn!.appArg!
-    tryTheoremCore lhs xs val type e thm numExtraArgs
+    tryTheoremCore lhs xs bis val type e thm numExtraArgs
 
 def tryTheorem? (e : Expr) (thm : SimpTheorem) : SimpM (Option Result) := do
   withNewMCtxDepth do
     let val  ← thm.getValue
     let type ← inferType val
-    let (xs, _, type) ← forallMetaTelescopeReducing type
+    let (xs, bis, type) ← forallMetaTelescopeReducing type
     let type ← whnf (← instantiateMVars type)
     let lhs := type.appFn!.appArg!
-    match (← tryTheoremCore lhs xs val type e thm 0) with
+    match (← tryTheoremCore lhs xs bis val type e thm 0) with
     | some result => return some result
     | none =>
       let lhsNumArgs := lhs.getAppNumArgs
       let eNumArgs   := e.getAppNumArgs
       if eNumArgs > lhsNumArgs then
-        tryTheoremCore lhs xs val type e thm (eNumArgs - lhsNumArgs)
+        tryTheoremCore lhs xs bis val type e thm (eNumArgs - lhsNumArgs)
       else
         return none
 
@@ -168,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 =>
@@ -299,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
@@ -491,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/Simproc.lean

@@ -256,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)."
 }
 

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
@@ -754,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/Parser/Do.lean

@@ -50,7 +50,7 @@ def notFollowedByRedefinedTermToken :=
   -- but we include them in the following list to fix the ambiguity where
   -- an "open" command follows the `do`-block.
   -- If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
-  notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "let" <|> "have" <|>
+  notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "match_expr" <|> "let" <|> "let_expr" <|> "have" <|>
       "do" <|> "dbg_trace" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
     "token at 'do' element"
 
@@ -60,6 +60,14 @@ def notFollowedByRedefinedTermToken :=
   "let " >> optional "mut " >> termParser >> " := " >> termParser >>
   checkColGt >> " | " >> doSeq
 
+@[builtin_doElem_parser] def doLetExpr  := leading_parser
+  "let_expr " >> matchExprPat >> " := " >> termParser >>
+  checkColGt >> " | " >> doSeq
+
+@[builtin_doElem_parser] def doLetMetaExpr  := leading_parser
+  "let_expr " >> matchExprPat >> " ← " >> termParser >>
+  checkColGt >> " | " >> doSeq
+
 @[builtin_doElem_parser] def doLetRec   := leading_parser
   group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
 def doIdDecl   := leading_parser
@@ -150,6 +158,12 @@ def doMatchAlts := ppDedent <| matchAlts (rhsParser := doSeq)
   "match " >> optional Term.generalizingParam >> optional Term.motive >>
   sepBy1 matchDiscr ", " >> " with" >> doMatchAlts
 
+def doMatchExprAlts := ppDedent <| matchExprAlts (rhsParser := doSeq)
+def optMetaFalse :=
+  optional ("(" >> nonReservedSymbol "meta" >>  " := " >> nonReservedSymbol "false" >> ") ")
+@[builtin_doElem_parser] def doMatchExpr := leading_parser:leadPrec
+  "match_expr " >> optMetaFalse >> termParser >> " with" >> doMatchExprAlts
+
 def doCatch      := leading_parser
   ppDedent ppLine >> atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
 def doCatchMatch := leading_parser

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
@@ -791,7 +802,6 @@ interpolated string literal) to stderr. It should only be used for debugging.
 @[builtin_term_parser] def assert := leading_parser:leadPrec
   withPosition ("assert! " >> termParser) >> optSemicolon termParser
 
-
 def macroArg       := termParser maxPrec
 def macroDollarArg := leading_parser "$" >> termParser 10
 def macroLastArg   := macroDollarArg <|> macroArg
@@ -806,6 +816,29 @@ def macroLastArg   := macroDollarArg <|> macroArg
 @[builtin_term_parser] def dotIdent := leading_parser
   "." >> checkNoWsBefore >> rawIdent
 
+/--
+Implementation of the `show_term` term elaborator.
+-/
+@[builtin_term_parser] def showTermElabImpl :=
+  leading_parser:leadPrec "show_term_elab " >> termParser
+
+/-!
+`match_expr` support.
+-/
+
+def matchExprPat := leading_parser optional (atomic (ident >> "@")) >> ident >> many binderIdent
+def matchExprAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (matchExprPat >> " => " >> rhsParser)
+def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (hole >> " => " >> rhsParser)
+def matchExprAlts (rhsParser : Parser) :=
+  leading_parser withPosition $
+    many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser)
+    >> (ppLine >> checkColGe "irrelevant" >> matchExprElseAlt rhsParser)
+@[builtin_term_parser] def matchExpr := leading_parser:leadPrec
+  "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)
+
+@[builtin_term_parser] def letExpr := leading_parser:leadPrec
+  withPosition ("let_expr " >> matchExprPat >> " := " >> termParser >> checkColGt >> " | " >> termParser) >> optSemicolon termParser
+
 end Term
 
 @[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser
@@ -824,6 +857,7 @@ builtin_initialize
   register_parser_alias matchDiscr
   register_parser_alias bracketedBinder
   register_parser_alias attrKind
+  register_parser_alias optSemicolon
 
 end Parser
 end Lean

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -178,7 +178,7 @@ def shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool := do
 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. -/

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
 

src/Lean/Server/Watchdog.lean

@@ -901,23 +901,33 @@ def findWorkerPath : IO System.FilePath := do
     workerPath := System.FilePath.mk path
   return workerPath
 
-def loadReferences : IO References := do
-  let oleanSearchPath ← Lean.searchPathRef.get
-  let mut refs := References.empty
-  for path in ← oleanSearchPath.findAllWithExt "ilean" do
-    try
-      refs := refs.addIlean path (← Ilean.load path)
-    catch _ =>
-      -- could be a race with the build system, for example
-      -- ilean load errors should not be fatal, but we *should* log them
-      -- when we add logging to the server
-      pure ()
-  return refs
+/--
+Starts loading .ileans present in the search path asynchronously in an IO task.
+This ensures that server startup is not blocked by loading the .ileans.
+In return, while the .ileans are being loaded, users will only get incomplete
+results in requests that need references.
+-/
+def startLoadingReferences (references : IO.Ref References) : IO Unit := do
+  -- Discard the task; there isn't much we can do about this failing,
+  -- but we should try to continue server operations regardless
+  let _ ← IO.asTask do
+    let oleanSearchPath ← Lean.searchPathRef.get
+    for path in ← oleanSearchPath.findAllWithExt "ilean" do
+      try
+        let ilean ← Ilean.load path
+        references.modify fun refs =>
+          refs.addIlean path ilean
+      catch _ =>
+        -- could be a race with the build system, for example
+        -- ilean load errors should not be fatal, but we *should* log them
+        -- when we add logging to the server
+        pure ()
 
 def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
   let workerPath ← findWorkerPath
   let srcSearchPath ← initSrcSearchPath
-  let references ← IO.mkRef (← loadReferences)
+  let references ← IO.mkRef .empty
+  startLoadingReferences references
   let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
   let i ← maybeTee "wdIn.txt" false i
   let o ← maybeTee "wdOut.txt" true o

src/Lean/Util/Recognizers.lean

@@ -106,52 +106,4 @@ def arrayLit? (e : Expr) : Option (Expr × List Expr) :=
 def prod? (e : Expr) : Option (Expr × Expr) :=
   e.app2? ``Prod
 
-private def getConstructorVal? (env : Environment) (ctorName : Name) : Option ConstructorVal :=
-  match env.find? ctorName with
-  | some (ConstantInfo.ctorInfo v) => v
-  | _                              => none
-
-def isConstructorApp? (env : Environment) (e : Expr) : Option ConstructorVal :=
-  match e with
-  | Expr.lit (Literal.natVal n) => if n == 0 then getConstructorVal? env `Nat.zero else getConstructorVal? env `Nat.succ
-  | _ =>
-    match e.getAppFn with
-    | Expr.const n _ => match getConstructorVal? env n with
-      | some v => if v.numParams + v.numFields == e.getAppNumArgs then some v else none
-      | none   => none
-    | _ => none
-
-def isConstructorApp (env : Environment) (e : Expr) : Bool :=
-  e.isConstructorApp? env |>.isSome
-
-/--
-If `e` is a constructor application, return a pair containing the corresponding `ConstructorVal` and the constructor
-application arguments.
-This function treats numerals as constructors. For example, if `e` is the numeral `2`, the result pair
-is `ConstructorVal` for `Nat.succ`, and the array `#[1]`. The parameter `useRaw` controls how the resulting
-numeral is represented. If `useRaw := false`, then `mkNatLit` is used, otherwise `mkRawNatLit`.
-Recall that `mkNatLit` uses the `OfNat.ofNat` application which is the canonical way of representing numerals
-in the elaborator and tactic framework. We `useRaw := false` in the compiler (aka code generator).
-
-Remark: This function does not treat `(ofNat 0 : Nat)` applications as constructors.
--/
-def constructorApp? (env : Environment) (e : Expr) (useRaw := false) : Option (ConstructorVal × Array Expr) := do
-  match e with
-  | Expr.lit (Literal.natVal n) =>
-    if n == 0 then do
-      let v ← getConstructorVal? env `Nat.zero
-      pure (v, #[])
-    else do
-      let v ← getConstructorVal? env `Nat.succ
-      pure (v, #[if useRaw then mkRawNatLit (n-1) else mkNatLit (n-1)])
-  | _ =>
-    match e.getAppFn with
-    | Expr.const n _ => do
-      let v ← getConstructorVal? env n
-      if v.numParams + v.numFields == e.getAppNumArgs then
-        pure (v, e.getAppArgs)
-      else
-        none
-    | _ => none
-
 end Lean.Expr

src/lake/Lake/CLI/Init.lean

@@ -16,6 +16,9 @@ open Git System
 /-- The default module of an executable in `std` package. -/
 def defaultExeRoot : Name := `Main
 
+/-- `elan` toolchain file name -/
+def toolchainFileName : FilePath := "lean-toolchain"
+
 def gitignoreContents :=
 s!"/{defaultLakeDir}
 "

src/lake/Lake/Config/Defaults.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+namespace Lake
+open System (FilePath)
+
+/--
+The default directory to output Lake-related files
+(e.g., build artifacts, packages, caches, etc.).
+Currently not configurable.
+-/
+def defaultLakeDir : FilePath := ".lake"
+
+/-- The default setting for a `WorkspaceConfig`'s `packagesDir` option. -/
+def defaultPackagesDir : FilePath := "packages"
+
+/-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
+def defaultConfigFile : FilePath := "lakefile.lean"
+
+/-- The default name of the Lake manifest file (i.e., `lake-manifest.json`). -/
+def defaultManifestFile : FilePath := "lake-manifest.json"
+
+/-- The default build directory for packages (i.e., `.lake/build`). -/
+def defaultBuildDir : FilePath := defaultLakeDir / "build"
+
+/-- The default Lean library directory for packages. -/
+def defaultLeanLibDir : FilePath := "lib"
+
+/-- The default native library directory for packages. -/
+def defaultNativeLibDir : FilePath := "lib"
+
+/-- The default binary directory for packages. -/
+def defaultBinDir : FilePath := "bin"
+
+/-- The default IR directory for packages. -/
+def defaultIrDir : FilePath := "ir"

src/lake/Lake/Config/InstallPath.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Util.NativeLib
+import Lake.Config.Defaults
 
 open System
 namespace Lake
@@ -78,17 +79,17 @@ def LeanInstall.sharedLibPath (self : LeanInstall) : SearchPath :=
 def LeanInstall.leanCc? (self : LeanInstall) : Option String :=
   if self.customCc then self.cc.toString else none
 
-/-- Standard path of `lake` in a Lake installation. -/
-def lakeExe (buildHome : FilePath) :=
-  buildHome / "bin" / "lake" |>.addExtension FilePath.exeExtension
+/-- Lake executable file path. -/
+def lakeExe : FilePath :=
+  FilePath.mk "lake" |>.addExtension FilePath.exeExtension
 
 /-- Path information about the local Lake installation. -/
 structure LakeInstall where
   home : FilePath
   srcDir := home
-  binDir := home / "build" / "bin"
-  libDir := home / "build" / "lib"
-  lake := lakeExe <| home / "build"
+  binDir := home / defaultBuildDir / defaultBinDir
+  libDir := home / defaultBuildDir / defaultLeanLibDir
+  lake := binDir / lakeExe
   deriving Inhabited, Repr
 
 /-- Construct a Lake installation co-located with the specified Lean installation. -/
@@ -97,7 +98,7 @@ def LakeInstall.ofLean (lean : LeanInstall) : LakeInstall where
   srcDir := lean.srcDir / "lake"
   binDir := lean.binDir
   libDir := lean.leanLibDir
-  lake := lakeExe lean.sysroot
+  lake := lean.binDir / lakeExe
 
 /-! ## Detection Functions -/
 

src/lake/Lake/Config/Package.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Config.Opaque
+import Lake.Config.Defaults
 import Lake.Config.LeanLibConfig
 import Lake.Config.LeanExeConfig
 import Lake.Config.ExternLibConfig
@@ -26,25 +27,6 @@ Currently used for package and target names taken from the CLI.
 def stringToLegalOrSimpleName (s : String) : Name :=
   if s.toName.isAnonymous then Lean.Name.mkSimple s else s.toName
 
---------------------------------------------------------------------------------
-/-! # Defaults -/
---------------------------------------------------------------------------------
-
-/-- The default setting for a `PackageConfig`'s `buildDir` option. -/
-def defaultBuildDir : FilePath := "build"
-
-/-- The default setting for a `PackageConfig`'s `leanLibDir` option. -/
-def defaultLeanLibDir : FilePath := "lib"
-
-/-- The default setting for a `PackageConfig`'s `nativeLibDir` option. -/
-def defaultNativeLibDir : FilePath := "lib"
-
-/-- The default setting for a `PackageConfig`'s `binDir` option. -/
-def defaultBinDir : FilePath := "bin"
-
-/-- The default setting for a `PackageConfig`'s `irDir` option. -/
-def defaultIrDir : FilePath := "ir"
-
 --------------------------------------------------------------------------------
 /-! # PackageConfig -/
 --------------------------------------------------------------------------------
@@ -102,9 +84,9 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
 
   /--
   The directory to which Lake should output the package's build results.
-  Defaults to `defaultLakeDir / defaultBuildDir` (i.e., `.lake/build`).
+  Defaults to `defaultBuildDir` (i.e., `.lake/build`).
   -/
-  buildDir : FilePath := defaultLakeDir / defaultBuildDir
+  buildDir : FilePath := defaultBuildDir
 
   /--
   The build subdirectory to which Lake should output the package's

src/lake/Lake/Config/WorkspaceConfig.lean

@@ -3,20 +3,11 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.Config.Defaults
 
 open System
 namespace Lake
 
-/--
-The default directory to output Lake-related files
-(e.g., build artifacts, packages, caches, etc.).
-Currently not configurable.
--/
-def defaultLakeDir : FilePath := ".lake"
-
-/-- The default setting for a `WorkspaceConfig`'s `packagesDir` option. -/
-def defaultPackagesDir : FilePath := "packages"
-
 /-- A `Workspace`'s declarative configuration. -/
 structure WorkspaceConfig where
   /--

src/lake/Lake/Load/Config.lean

@@ -5,21 +5,13 @@ Authors: Mac Malone
 -/
 import Lean.Data.Name
 import Lean.Data.Options
+import Lake.Config.Defaults
 import Lake.Config.Env
 import Lake.Util.Log
 
 namespace Lake
 open System Lean
 
-/-- `elan` toolchain file name -/
-def toolchainFileName : FilePath := "lean-toolchain"
-
-/-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
-def defaultConfigFile : FilePath := "lakefile.lean"
-
-/-- The default name of the Lake manifest file (i.e., `lake-manifest.json`). -/
-def defaultManifestFile := "lake-manifest.json"
-
 /-- Context for loading a Lake configuration. -/
 structure LoadConfig where
   /-- The Lake environment of the load process. -/

src/stdlib.make.in

@@ -42,14 +42,22 @@ Init:
 Lean: Init
 	+"${LEAN_BIN}/leanmake" lib PKG=Lean $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING
 
+${LIB}/temp/empty.c:
+	touch $@
+
 # the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt
 
 # we specify the precise file names here to avoid rebuilds
-${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a
+${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c
+ifeq "${INIT_SHARED_LINKER_FLAGS}" ""
+  # create empty library on platforms without restrictive symbol limits; avoids costly indirections and troubles with cross-library exceptions
+	"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${LIB}/temp/empty.c ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
+else
 	@echo "[    ] Building $@"
 # on Windows, must remove file before writing a new one (since the old one may be in use)
 	@rm -f $@
 	"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${INIT_SHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
+endif
 
 Init_shared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}