chore: protect Std.BitVec

This adds @digama0 to the CODEOWNERS files for the tactics files which
have recently been upstreamed from Std.

.github/workflows/pr-release.yml

@@ -149,6 +149,7 @@ jobs:
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
             git -C lean4.git log -10 origin/master
 
+            git -C lean4.git fetch origin nightly-with-mathlib 
             NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "nightly-with-mathlib")"
             MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
           fi

CMakeLists.txt

@@ -78,6 +78,10 @@ add_custom_target(update-stage0
   COMMAND $(MAKE) -C stage1 update-stage0
   DEPENDS stage1)
 
+add_custom_target(update-stage0-commit
+  COMMAND $(MAKE) -C stage1 update-stage0-commit
+  DEPENDS stage1)
+
 add_custom_target(test
   COMMAND $(MAKE) -C stage1 test
   DEPENDS stage1)

CODEOWNERS

@@ -21,3 +21,21 @@
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
 /src/runtime/io.cpp @joehendrix
+/src/Lean/Elab/Tactic/RCases.lean @digama0
+/src/Init/RCases.lean @digama0
+/src/Lean/Elab/Tactic/Ext.lean @digama0
+/src/Init/Ext.lean @digama0
+/src/Lean/Elab/Tactic/Simpa.lean @digama0
+/src/Lean/Elab/Tactic/NormCast.lean @digama0
+/src/Lean/Meta/Tactic/NormCast.lean @digama0
+/src/Lean/Meta/Tactic/TryThis.lean @digama0
+/src/Lean/Elab/Tactic/SimpTrace.lean @digama0
+/src/Lean/Elab/Tactic/NoMatch.lean @digama0
+/src/Lean/Elab/Tactic/ShowTerm.lean @digama0
+/src/Lean/Elab/Tactic/Repeat.lean @digama0
+/src/Lean/Meta/Tactic/Repeat.lean @digama0
+/src/Lean/Meta/CoeAttr.lean @digama0
+/src/Lean/Elab/GuardMsgs.lean @digama0
+/src/Lean/Elab/Tactic/Guard.lean @digama0
+/src/Init/Guard.lean @digama0
+/src/Lean/Server/CodeActions/ @digama0

RELEASES.md

@@ -69,6 +69,12 @@ v4.8.0 (development in progress)
   to enable pretty printing function applications using generalized field notation (defaults to true).
   Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
 
+* Added options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
+  When `pp.mvars` is false, metavariables pretty print as `?_`,
+  and when `pp.mvars.withType` is true, metavariables pretty print with a type ascription.
+  These can be set when using `#guard_msgs` to make tests not rely on the unique ids assigned to anonymous metavariables.
+  [#3798](https://github.com/leanprover/lean4/pull/3798).
+
 * Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
   for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
   Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`

doc/dev/bootstrap.md

@@ -81,20 +81,8 @@ or using Github CLI with
 gh workflow run update-stage0.yml
 ```
 
-Leaving stage0 updates to the CI automation is preferrable, but should you need
-to do it locally, you can use `make update-stage0` in `build/release`, to
-update `stage0` from `stage1`, `make -C stageN update-stage0` to update from
-another stage, or `nix run .#update-stage0-commit` to update using nix.
-
-Updates to `stage0` should be their own commits in the Git history. So should
-you have to include the stage0 update in your PR (rather than using above
-automation after merging changes), commit your work before running `make
-update-stage0`, commit the updated `stage0` compiler code with the commit
-message:
-```
-chore: update stage0
-```
-and coordinate with the admins to not squash your PR.
+Leaving stage0 updates to the CI automation is preferable, but should you need to do it locally, you can use `make update-stage0-commit` in `build/release` to update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to update from another stage.
+This command will automatically stage the updated files and introduce a commit, so make sure to commit your work before that. Then coordinate with the admins to not squash your PR so that stage 0 updates are preserved as separate commits.
 
 ## Further Bootstrapping Complications
 

src/CMakeLists.txt

@@ -588,6 +588,10 @@ if(PREV_STAGE)
     COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/update-stage0'
     DEPENDS make_stdlib
     WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")
+
+  add_custom_target(update-stage0-commit
+    COMMAND git commit -m "chore: update stage0"
+    DEPENDS update-stage0)
 endif()
 
 # use Bash version for building, use Lean version in bin/ for tests & distribution

src/Init/Core.lean

@@ -1308,7 +1308,6 @@ gen_injective_theorems% Fin
 gen_injective_theorems% Array
 gen_injective_theorems% Sum
 gen_injective_theorems% PSum
-gen_injective_theorems% Nat
 gen_injective_theorems% Option
 gen_injective_theorems% List
 gen_injective_theorems% Except
@@ -1316,6 +1315,12 @@ gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
 
+theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
+  fun x => Nat.noConfusion x id
+
+theorem Nat.succ.injEq (u v : Nat) : (u.succ = v.succ) = (u = v) :=
+  Eq.propIntro Nat.succ.inj (congrArg Nat.succ)
+
 @[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] (a b : α) : a == b ↔ a = b :=
   ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩
 

src/Init/Data/BitVec/Basic.lean

@@ -34,7 +34,7 @@ structure BitVec (w : Nat) where
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
 
-@[deprecated] abbrev Std.BitVec := _root_.BitVec
+@[deprecated] protected abbrev Std.BitVec := _root_.BitVec
 
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we

src/Init/Data/BitVec/Lemmas.lean

@@ -728,8 +728,7 @@ theorem toNat_cons' {x : BitVec w} :
   rw [← BitVec.msb, msb_cons]
 
 @[simp] theorem getMsb_cons_succ : (cons a x).getMsb (i + 1) = x.getMsb i := by
-  simp [cons, cond_eq_if]
-  omega
+  simp [cons, Nat.le_add_left 1 i]
 
 theorem truncate_succ (x : BitVec w) :
     truncate (i+1) x = cons (getLsb x i) (truncate i x) := by

src/Init/Data/Bool.lean

@@ -220,6 +220,12 @@ due to `beq_iff_eq`.
 
 /-! ### coercision related normal forms -/
 
+theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
+    (a == b) = decide (a = b) := by
+  cases h : a == b
+  · simp [ne_of_beq_false h]
+  · simp [eq_of_beq h]
+
 @[simp] theorem not_eq_not : ∀ {a b : Bool}, ¬a = !b ↔ a = b := by decide
 
 @[simp] theorem not_not_eq : ∀ {a b : Bool}, ¬(!a) = b ↔ a = b := by decide
@@ -230,6 +236,11 @@ due to `beq_iff_eq`.
 @[simp] theorem coe_false_iff_true  : ∀(a b : Bool), (a = false ↔ b) ↔ (!a) = b := by decide
 @[simp] theorem coe_false_iff_false : ∀(a b : Bool), (a = false ↔ b = false) ↔ (!a) = (!b) := by decide
 
+/-! ### beq properties -/
+
+theorem beq_comm {α} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = (b == a) :=
+  (Bool.coe_iff_coe (a == b) (b == a)).mp (by simp [@eq_comm α])
+
 /-! ### xor -/
 
 theorem false_xor : ∀ (x : Bool), xor false x = x := false_bne

src/Init/Data/Fin/Lemmas.lean

@@ -541,7 +541,7 @@ theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w
     ∀ {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b
   | ⟨0, _⟩, _, ha, _ => by simp only [mk_zero, ne_eq, not_true] at ha
   | ⟨i + 1, _⟩, ⟨0, _⟩, _, hb => by simp only [mk_zero, ne_eq, not_true] at hb
-  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [ext_iff]
+  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [ext_iff, Nat.succ.injEq]
 
 @[simp] theorem pred_one {n : Nat} :
     Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt one_pos)) = 0 := rfl
@@ -683,6 +683,7 @@ and `cast` defines the inductive step using `motive i.succ`, inducting downwards
 termination_by n + 1 - i
 decreasing_by decreasing_with
   -- FIXME: we put the proof down here to avoid getting a dummy `have` in the definition
+  try simp only [Nat.succ_sub_succ_eq_sub]
   exact Nat.add_sub_add_right .. ▸ Nat.sub_lt_sub_left i.2 (Nat.lt_succ_self i)
 
 @[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :

src/Init/Data/List/Lemmas.lean

@@ -249,12 +249,14 @@ theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a
 theorem get?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n →
   (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)
 | [], _, n, _ => rfl
-| a :: l, _, n+1, h₁ => by rw [cons_append]; simp [get?_append_right (Nat.lt_succ.1 h₁)]
+| a :: l, _, n+1, h₁ => by
+  rw [cons_append]
+  simp [Nat.succ_sub_succ_eq_sub, get?_append_right (Nat.lt_succ.1 h₁)]
 
 theorem get?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
     get? l.reverse i = get? l j
   | [], _, _, _ => rfl
-  | a::l, i, 0, h => by simp at h; simp [h, get?_append_right]
+  | a::l, i, 0, h => by simp [Nat.succ.injEq] at h; simp [h, get?_append_right, Nat.succ.injEq]
   | a::l, i, j+1, h => by
     have := Nat.succ.inj h; simp at this ⊢
     rw [get?_append, get?_reverse' _ j this]

src/Init/Data/Nat.lean

@@ -19,3 +19,4 @@ import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Mod
 import Init.Data.Nat.Lcm
 import Init.Data.Nat.Compare
+import Init.Data.Nat.Simproc

src/Init/Data/Nat/Basic.lean

@@ -174,7 +174,7 @@ protected theorem add_right_comm (n m k : Nat) : (n + m) + k = (n + k) + m := by
 protected theorem add_left_cancel {n m k : Nat} : n + m = n + k → m = k := by
   induction n with
   | zero => simp
-  | succ n ih => simp [succ_add]; intro h; apply ih h
+  | succ n ih => simp [succ_add, succ.injEq]; intro h; apply ih h
 
 protected theorem add_right_cancel {n m k : Nat} (h : n + m = k + m) : n = k := by
   rw [Nat.add_comm n m, Nat.add_comm k m] at h
@@ -248,7 +248,7 @@ theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
 
 @[simp] protected theorem sub_zero (n : Nat) : n - 0 = n := rfl
 
-@[simp] theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
+theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   induction m with
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
@@ -574,7 +574,7 @@ theorem eq_zero_or_eq_succ_pred : ∀ n, n = 0 ∨ n = succ (pred n)
   | 0 => .inl rfl
   | _+1 => .inr rfl
 
-theorem succ_inj' : succ a = succ b ↔ a = b := ⟨succ.inj, congrArg _⟩
+theorem succ_inj' : succ a = succ b ↔ a = b := (Nat.succ.injEq a b).to_iff
 
 theorem succ_le_succ_iff : succ a ≤ succ b ↔ a ≤ b := ⟨le_of_succ_le_succ, succ_le_succ⟩
 
@@ -802,7 +802,7 @@ theorem add_sub_of_le {a b : Nat} (h : a ≤ b) : a + (b - a) = b := by
 protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m := by
   induction k with
   | zero => simp
-  | succ k ih => simp [← Nat.add_assoc, ih]
+  | succ k ih => simp [← Nat.add_assoc, succ_sub_succ_eq_sub, ih]
 
 protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m := by
   rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right]

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

@@ -9,6 +9,7 @@ import Init.Data.Bool
 import Init.Data.Int.Pow
 import Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Lemmas
+import Init.Data.Nat.Simproc
 import Init.TacticsExtra
 import Init.Omega
 
@@ -271,7 +272,7 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
   induction i generalizing n x with
   | zero =>
     match n with
-    | 0 => simp
+    | 0 => simp [succ_sub_succ_eq_sub]
     | n+1 =>
       simp [not_decide_mod_two_eq_one]
       omega
@@ -279,7 +280,7 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
     simp only [testBit_succ]
     match n with
     | 0 =>
-      simp [decide_eq_false]
+      simp [decide_eq_false, succ_sub_succ_eq_sub]
     | n+1 =>
       rw [Nat.two_pow_succ_sub_succ_div_two, ih]
       · simp [Nat.succ_lt_succ_iff]

src/Init/Data/Nat/Lemmas.lean

@@ -88,7 +88,7 @@ protected theorem add_pos_right (m) (h : 0 < n) : 0 < m + n :=
   Nat.lt_of_lt_of_le h (Nat.le_add_left ..)
 
 protected theorem add_self_ne_one : ∀ n, n + n ≠ 1
-  | n+1, h => by rw [Nat.succ_add, Nat.succ_inj'] at h; contradiction
+  | n+1, h => by rw [Nat.succ_add, Nat.succ.injEq] at h; contradiction
 
 /-! ## sub -/
 

src/Init/Data/Nat/Linear.lean

@@ -580,7 +580,7 @@ attribute [-simp] Nat.right_distrib Nat.left_distrib
 
 theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul (k+1)).denote ctx = c.denote ctx := by
   cases c; rename_i eq lhs rhs
-  have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp
+  have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp [Nat.succ.injEq]
   have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
   have : ¬ ((k + 1 == 0) = true)  := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
   have : (1 == (0 : Nat)) = false := rfl

src/Init/Data/Nat/Simproc.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2023 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Init.Data.Bool
+import Init.Data.Nat.Basic
+import Init.Data.Nat.Lemmas
+
+/-!
+This contains lemmas used by the Nat simprocs for simplifying arithmetic
+addition offsets.
+-/
+namespace Nat.Simproc
+
+/- Sub proofs -/
+
+theorem sub_add_eq_comm (a b c : Nat) : a - (b + c) = a - c - b := by
+  rw [Nat.add_comm b c]
+  exact Nat.sub_add_eq a c b
+
+theorem add_sub_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : a + b - (c + d) = a - (c + (d-b)) := by
+  induction b generalizing a c d with
+  | zero =>
+    simp
+  | succ b ind =>
+    match d with
+    | 0 =>
+      contradiction
+    | d + 1 =>
+      have g := Nat.le_of_succ_le_succ h
+      rw [Nat.add_succ a, Nat.add_succ c, Nat.succ_sub_succ, Nat.succ_sub_succ,
+          ind _ _ g]
+
+theorem add_sub_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : a + b - (c + d) = a + (b - d) - c := by
+  rw [Nat.add_comm c d, Nat.sub_add_eq, Nat.add_sub_assoc h a]
+
+theorem add_sub_le (a : Nat) {b c : Nat} (h : b ≤ c) : a + b - c = a - (c - b) := by
+  have p := add_sub_add_le a 0 h
+  simp only [Nat.zero_add] at p
+  exact p
+
+/- Eq proofs -/
+
+theorem add_eq_gt (a : Nat) {b c : Nat} (h : b > c) : (a + b = c) = False :=
+  eq_false (Nat.ne_of_gt (Nat.lt_of_lt_of_le h (le_add_left b a)))
+
+theorem eq_add_gt (a : Nat) {b c : Nat} (h : c > a) : (a = b + c) = False := by
+  rw [@Eq.comm Nat a (b + c)]
+  exact add_eq_gt b h
+
+theorem add_eq_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b = c + d) = (a = c + (d - b)) := by
+  have g : b ≤ c + d := Nat.le_trans h (le_add_left d c)
+  rw [← Nat.add_sub_assoc h, @Eq.comm _ a, Nat.sub_eq_iff_eq_add g, @Eq.comm _ (a + b)]
+
+theorem add_eq_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b = c + d) = (a + (b - d) = c) := by
+  rw [@Eq.comm _ (a + b) _, add_eq_add_le c a h, @Eq.comm _ _ c]
+
+theorem add_eq_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b = c) = (a = c - b) := by
+  have r := add_eq_add_le a 0 h
+  simp only [Nat.zero_add] at r
+  exact r
+
+theorem eq_add_le {a : Nat} (b : Nat) {c : Nat} (h : c ≤ a) : (a = b + c) = (b = a - c) := by
+  rw [@Eq.comm Nat a (b + c)]
+  exact add_eq_le b h
+
+/- Lemmas for lifting Eq proofs to beq -/
+
+theorem beqEqOfEqEq {a b c d : Nat} (p : (a = b) = (c = d)) : (a == b) = (c == d) := by
+  simp only [Bool.beq_eq_decide_eq, p]
+
+theorem beqFalseOfEqFalse {a b : Nat} (p : (a = b) = False) : (a == b) = false := by
+  simp [Bool.beq_eq_decide_eq, p]
+
+theorem bneEqOfEqEq {a b c d : Nat} (p : (a = b) = (c = d)) : (a != b) = (c != d) := by
+  simp only [bne, beqEqOfEqEq p]
+
+theorem bneTrueOfEqFalse {a b : Nat} (p : (a = b) = False) : (a != b) = true := by
+  simp [bne, beqFalseOfEqFalse p]
+
+/- le proofs -/
+
+theorem add_le_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b ≤ c + d) = (a ≤ c + (d - b)) := by
+  rw [← Nat.add_sub_assoc h, Nat.le_sub_iff_add_le]
+  exact Nat.le_trans h (le_add_left d c)
+
+theorem add_le_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b ≤ c + d) = (a + (b - d) ≤ c) := by
+  rw [← Nat.add_sub_assoc h, Nat.sub_le_iff_le_add]
+
+theorem add_le_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b ≤ c) = (a ≤ c - b) := by
+  have r := add_le_add_le a 0 h
+  simp only [Nat.zero_add] at r
+  exact r
+
+theorem add_le_gt (a : Nat) {b c : Nat} (h : b > c) : (a + b ≤ c) = False :=
+  eq_false (Nat.not_le_of_gt (Nat.lt_of_lt_of_le h (le_add_left b a)))
+
+theorem le_add_le (a : Nat) {b c : Nat} (h : a ≤ c) : (a ≤ b + c) = True :=
+  eq_true (Nat.le_trans h (le_add_left c b))
+
+theorem le_add_ge (a : Nat) {b c : Nat} (h : a ≥ c) : (a ≤ b + c) = (a - c ≤ b) := by
+  have r := add_le_add_ge 0 b h
+  simp only [Nat.zero_add] at r
+  exact r
+
+end Nat.Simproc

src/Init/Data/String/Basic.lean

@@ -245,12 +245,21 @@ termination_by s.endPos.1 - i.1
 @[specialize] def split (s : String) (p : Char → Bool) : List String :=
   splitAux s p 0 0 []
 
+/--
+Auxiliary for `splitOn`. Preconditions:
+* `sep` is not empty
+* `b <= i` are indexes into `s`
+* `j` is an index into `sep`, and not at the end
+
+It represents the state where we have currently parsed some split parts into `r` (in reverse order),
+`b` is the beginning of the string / the end of the previous match of `sep`, and the first `j` bytes
+of `sep` match the bytes `i-j .. i` of `s`.
+-/
 def splitOnAux (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String) : List String :=
-  if h : s.atEnd i then
+  if s.atEnd i then
     let r := (s.extract b i)::r
     r.reverse
   else
-    have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next s _)
     if s.get i == sep.get j then
       let i := s.next i
       let j := sep.next j
@@ -259,9 +268,42 @@ def splitOnAux (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String)
       else
         splitOnAux s sep b i j r
     else
-      splitOnAux s sep b (s.next i) 0 r
-termination_by s.endPos.1 - i.1
+      splitOnAux s sep b (s.next (i - j)) 0 r
+termination_by (s.endPos.1 - (i - j).1, sep.endPos.1 - j.1)
+decreasing_by
+  all_goals simp_wf
+  focus
+    rename_i h _ _
+    left; exact Nat.sub_lt_sub_left
+      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (Nat.gt_of_not_le (mt decide_eq_true h)))
+      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (lt_next s _))
+  focus
+    rename_i i₀ j₀ _ eq h'
+    rw [show (s.next i₀ - sep.next j₀).1 = (i₀ - j₀).1 by
+      show (_ + csize _) - (_ + csize _) = _
+      rw [(beq_iff_eq ..).1 eq, Nat.add_sub_add_right]; rfl]
+    right; exact Nat.sub_lt_sub_left
+      (Nat.lt_of_le_of_lt (Nat.le_add_right ..) (Nat.gt_of_not_le (mt decide_eq_true h')))
+      (lt_next sep _)
+  focus
+    rename_i h _
+    left; exact Nat.sub_lt_sub_left
+      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (Nat.gt_of_not_le (mt decide_eq_true h)))
+      (lt_next s _)
 
+/--
+Splits a string `s` on occurrences of the separator `sep`. When `sep` is empty, it returns `[s]`;
+when `sep` occurs in overlapping patterns, the first match is taken. There will always be exactly
+`n+1` elements in the returned list if there were `n` nonoverlapping matches of `sep` in the string.
+The default separator is `" "`. The separators are not included in the returned substrings.
+
+```
+"here is some text ".splitOn = ["here", "is", "some", "text", ""]
+"here is some text ".splitOn "some" = ["here is ", " text "]
+"here is some text ".splitOn "" = ["here is some text "]
+"ababacabac".splitOn "aba" = ["", "bac", "c"]
+```
+-/
 def splitOn (s : String) (sep : String := " ") : List String :=
   if sep == "" then [s] else splitOnAux s sep 0 0 0 []
 

src/Init/Omega/Int.lean

@@ -137,11 +137,13 @@ theorem add_le_iff_le_sub (a b c : Int) : a + b ≤ c ↔ a ≤ c - b := by
     lhs
     rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg,
       Int.add_le_add_iff_right]
+  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem le_add_iff_sub_le (a b c : Int) : a ≤ b + c ↔ a - c ≤ b := by
   conv =>
     lhs
     rw [← Int.neg_neg c, ← Int.sub_eq_add_neg, ← add_le_iff_le_sub]
+  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem add_le_zero_iff_le_neg (a b : Int) : a + b ≤ 0 ↔ a ≤ - b := by
   rw [add_le_iff_le_sub, Int.zero_sub]

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -147,7 +147,7 @@ def callLeanRefcountFn (builder : LLVM.Builder llvmctx)
     (delta : Option (LLVM.Value llvmctx) := Option.none) : M llvmctx Unit := do
   let fnName :=  s!"lean_{kind}{if checkRef? then "" else "_ref"}{if delta.isNone then "" else "_n"}"
   let retty ← LLVM.voidType llvmctx
-  let argtys := if delta.isNone then #[← LLVM.voidPtrType llvmctx] else #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
+  let argtys ← if delta.isNone then pure #[← LLVM.voidPtrType llvmctx] else pure #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   match delta with

src/Lean/Compiler/LCNF/LambdaLifting.lean

@@ -88,7 +88,7 @@ occurring in `decl`.
 -/
 def mkAuxDecl (closure : Array Param) (decl : FunDecl) : LiftM LetDecl := do
   let nameNew ← mkAuxDeclName
-  let inlineAttr? := if (← read).inheritInlineAttrs then (← read).mainDecl.inlineAttr? else none
+  let inlineAttr? ← if (← read).inheritInlineAttrs then pure (← read).mainDecl.inlineAttr? else pure none
   let auxDecl ← go nameNew (← read).mainDecl.safe inlineAttr? |>.run' {}
   let us := auxDecl.levelParams.map mkLevelParam
   let auxDeclName ← match (← cacheAuxDecl auxDecl) with

src/Lean/Data/PersistentHashMap.lean

@@ -325,6 +325,9 @@ def map {α : Type u} {β : Type v} {σ : Type u} {_ : BEq α} {_ : Hashable α}
 def toList {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : List (α × β) :=
   m.foldl (init := []) fun ps k v => (k, v) :: ps
 
+def toArray {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : Array (α × β) :=
+  m.foldl (init := #[]) fun ps k v => ps.push (k, v)
+
 structure Stats where
   numNodes      : Nat := 0
   numNull       : Nat := 0

src/Lean/DocString.lean

@@ -16,10 +16,12 @@ private builtin_initialize docStringExt : MapDeclarationExtension String ← mkM
 def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
   builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
 
-def addDocString [MonadEnv m] (declName : Name) (docString : String) : m Unit :=
+def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
+  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
+    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
   modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
 
-def addDocString' [Monad m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
+def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
   match docString? with
   | some docString => addDocString declName docString
   | none => return ()

src/Lean/Elab/App.lean

@@ -1199,8 +1199,8 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
   let rec loop : Expr → List LVal → TermElabM Expr
   | f, []          => elabAppArgs f namedArgs args expectedType? explicit ellipsis
   | f, lval::lvals => do
-    if let LVal.fieldName (ref := fieldStx) (targetStx := targetStx) .. := lval then
-      addDotCompletionInfo targetStx f expectedType? fieldStx
+    if let LVal.fieldName (fullRef := fullRef) .. := lval then
+      addDotCompletionInfo fullRef f expectedType?
     let hasArgs := !namedArgs.isEmpty || !args.isEmpty
     let (f, lvalRes) ← resolveLVal f lval hasArgs
     match lvalRes with
@@ -1340,7 +1340,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     let elabFieldName (e field : Syntax) := do
       let newLVals := field.identComponents.map fun comp =>
         -- We use `none` in `suffix?` since `field` can't be part of a composite name
-        LVal.fieldName comp comp.getId.getString! none e
+        LVal.fieldName comp comp.getId.getString! none f
       elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     let elabFieldIdx (e idxStx : Syntax) := do
       let some idx := idxStx.isFieldIdx? | throwError "invalid field index"

src/Lean/Elab/BuiltinCommand.lean

@@ -749,7 +749,7 @@ def elabRunMeta : CommandElab := fun stx =>
     pure ()
 
 @[builtin_command_elab «set_option»] def elabSetOption : CommandElab := fun stx => do
-  let options ← Elab.elabSetOption stx[1] stx[2]
+  let options ← Elab.elabSetOption stx[1] stx[3]
   modify fun s => { s with maxRecDepth := maxRecDepth.get options }
   modifyScope fun scope => { scope with opts := options }
 

src/Lean/Elab/BuiltinTerm.lean

@@ -232,7 +232,7 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
 
 @[builtin_term_elab Parser.Term.withDeclName] def elabWithDeclName : TermElab := fun stx expectedType? => do
   let id := stx[2].getId
-  let id := if stx[1].isNone then id else (← getCurrNamespace) ++ id
+  let id ← if stx[1].isNone then pure id else pure <| (← getCurrNamespace) ++ id
   let e := stx[3]
   withMacroExpansion stx e <| withDeclName id <| elabTerm e expectedType?
 
@@ -312,9 +312,9 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
     popScope
 
 @[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
-  let options ← Elab.elabSetOption stx[1] stx[2]
+  let options ← Elab.elabSetOption stx[1] stx[3]
   withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
-    elabTerm stx[4] expectedType?
+    elabTerm stx[5] expectedType?
 
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
   match stx with

src/Lean/Elab/Command.lean

@@ -535,9 +535,9 @@ first evaluates any local `set_option ... in ...` clauses and then invokes `cmd`
 partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
   if stx.getKind == ``Lean.Parser.Command.in &&
      stx[0].getKind == ``Lean.Parser.Command.set_option then
-      let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
+      let opts ← Elab.elabSetOption stx[0][1] stx[0][3]
       Command.withScope (fun scope => { scope with opts }) do
-        withSetOptionIn cmd stx[1]
+        withSetOptionIn cmd stx[2]
   else
     cmd stx
 

src/Lean/Elab/Deriving/DecEq.lean

@@ -27,8 +27,9 @@ where
       let rhs ← if isProof then
         `(have h : @$a = @$b := rfl; by subst h; exact $(← mkSameCtorRhs todo):term)
       else
+        let sameCtor ← mkSameCtorRhs todo
         `(if h : @$a = @$b then
-           by subst h; exact $(← mkSameCtorRhs todo):term
+           by subst h; exact $sameCtor:term
           else
            isFalse (by intro n; injection n; apply h _; assumption))
       if let some auxFunName := recField then

src/Lean/Elab/Do.lean

@@ -63,8 +63,9 @@ private def letDeclHasBinders (letDecl : Syntax) : Bool :=
 /-- Return true if we should generate an error message when lifting a method over this kind of syntax. -/
 private def liftMethodForbiddenBinder (stx : Syntax) : Bool :=
   let k := stx.getKind
+  -- TODO: make this extensible in the future.
   if k == ``Parser.Term.fun || k == ``Parser.Term.matchAlts ||
-     k == ``Parser.Term.doLetRec || k == ``Parser.Term.letrec  then
+     k == ``Parser.Term.doLetRec || k == ``Parser.Term.letrec then
      -- It is never ok to lift over this kind of binder
     true
   -- The following kinds of `let`-expressions require extra checks to decide whether they contain binders or not
@@ -77,12 +78,15 @@ private def liftMethodForbiddenBinder (stx : Syntax) : Bool :=
   else
     false
 
+-- TODO: we must track whether we are inside a quotation or not.
 private partial def hasLiftMethod : Syntax → Bool
   | Syntax.node _ k args =>
     if liftMethodDelimiter k then false
     -- NOTE: We don't check for lifts in quotations here, which doesn't break anything but merely makes this rare case a
     -- bit slower
     else if k == ``Parser.Term.liftMethod then true
+    -- For `pure` if-then-else, we only lift `(<- ...)` occurring in the condition.
+    else if k == ``termDepIfThenElse || k == ``termIfThenElse then args.size >= 2 && hasLiftMethod args[1]!
     else args.any hasLiftMethod
   | _ => false
 
@@ -1321,6 +1325,12 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt
       return .node i k (alts.map (·.1))
     else if liftMethodDelimiter k then
       return stx
+    -- For `pure` if-then-else, we only lift `(<- ...)` occurring in the condition.
+    else if args.size >= 2 && (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
+      let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
+      let arg1 ← expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]!
+      let args := args.set! 1 arg1
+      return Syntax.node i k args
     else if k == ``Parser.Term.liftMethod && !inQuot then withFreshMacroScope do
       if inBinder then
         throwErrorAt stx "cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`"

src/Lean/Elab/InfoTree/Types.lean

@@ -76,7 +76,7 @@ structure CommandInfo extends ElabInfo where
 /-- A completion is an item that appears in the [IntelliSense](https://code.visualstudio.com/docs/editor/intellisense)
 box that appears as you type. -/
 inductive CompletionInfo where
-  | dot (termInfo : TermInfo) (field? : Option Syntax) (expectedType? : Option Expr)
+  | dot (termInfo : TermInfo) (expectedType? : Option Expr)
   | id (stx : Syntax) (id : Name) (danglingDot : Bool) (lctx : LocalContext) (expectedType? : Option Expr)
   | dotId (stx : Syntax) (id : Name) (lctx : LocalContext) (expectedType? : Option Expr)
   | fieldId (stx : Syntax) (id : Name) (lctx : LocalContext) (structName : Name)

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

@@ -101,6 +101,7 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
         -/
         registerEqnsInfo preDef recArgPos
     addSmartUnfoldingDef preDef recArgPos
+    markAsRecursive preDef.declName
     applyAttributesOf #[preDefNonRec] AttributeApplicationTime.afterCompilation
 
 builtin_initialize

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

@@ -144,6 +144,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   let preDefs ← preDefs.mapM (abstractNestedProofs ·)
   registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
   for preDef in preDefs do
+    markAsRecursive preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
 builtin_initialize registerTraceClass `Elab.definition.wf

src/Lean/Elab/SetOption.lean

@@ -15,7 +15,7 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
   let ref ← getRef
   -- For completion purposes, we discard `val` and any later arguments.
   -- We include the first argument (the keyword) for position information in case `id` is `missing`.
-  addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[0:2]))
+  addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[0:3]))
   let optionName := id.getId.eraseMacroScopes
   let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error ref ex.toString) (getOptionDecl optionName)
   pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }

src/Lean/Elab/Structure.lean

@@ -704,6 +704,7 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
       if info.kind == StructFieldKind.fromParent then
         return none
       else
+        let env ← getEnv
         return some {
           fieldName  := info.name
           projFn     := info.declName
@@ -711,7 +712,7 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
           autoParam? := (← inferType info.fvar).getAutoParamTactic?
           subobject? :=
             if info.kind == StructFieldKind.subobject then
-              match (← getEnv).find? info.declName with
+              match env.find? info.declName with
               | some (ConstantInfo.defnInfo val) =>
                 match val.type.getForallBody.getAppFn with
                 | Expr.const parentName .. => some parentName

src/Lean/Elab/Syntax.lean

@@ -442,7 +442,4 @@ def strLitToPattern (stx: Syntax) : MacroM Syntax :=
   | some str => return mkAtomFrom stx str
   | none     => Macro.throwUnsupported
 
-builtin_initialize
-  registerTraceClass `Elab.syntax
-
 end Lean.Elab.Command

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -162,9 +162,9 @@ private def getOptRotation (stx : Syntax) : Nat :=
     popScope
 
 @[builtin_tactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
-  let options ← Elab.elabSetOption stx[1] stx[2]
+  let options ← Elab.elabSetOption stx[1] stx[3]
   withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
-    evalTactic stx[4]
+    evalTactic stx[5]
 
 @[builtin_tactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do
   let mvarIds ← getGoals

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

@@ -115,7 +115,7 @@ def evalSepByIndentConv (stx : Syntax) : TacticM Unit := do
     -- save state before/after entering focus on `{`
     withInfoContext (pure ()) initInfo
     evalSepByIndentConv stx[1]
-    evalTactic (← `(tactic| all_goals (try rfl)))
+    evalTactic (← `(tactic| all_goals (try with_reducible rfl)))
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.nestedConv] def evalNestedConv : Tactic := fun stx => do
   evalConvSeqBracketed stx[0]
@@ -163,7 +163,7 @@ private def convTarget (conv : Syntax) : TacticM Unit := withMainContext do
    let target ← getMainTarget
    let (targetNew, proof) ← convert target (withTacticInfoContext (← getRef) (evalTactic conv))
    liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
-   evalTactic (← `(tactic| try rfl))
+   evalTactic (← `(tactic| try with_reducible rfl))
 
 private def convLocalDecl (conv : Syntax) (hUserName : Name) : TacticM Unit := withMainContext do
    let localDecl ← getLocalDeclFromUserName hUserName

src/Lean/Elab/Tactic/Ext.lean

@@ -131,10 +131,10 @@ def withExtHyps (struct : Name) (flat : Term)
   withLocalDeclD `x (mkAppN structC params) fun x => do
   withLocalDeclD `y (mkAppN structC params) fun y => do
     let mut hyps := #[]
-    let fields := if flat then
-      getStructureFieldsFlattened (← getEnv) struct (includeSubobjectFields := false)
+    let fields ← if flat then
+      pure <| getStructureFieldsFlattened (← getEnv) struct (includeSubobjectFields := false)
     else
-      getStructureFields (← getEnv) struct
+      pure <| getStructureFields (← getEnv) struct
     for field in fields do
       let x_f ← mkProjection x field
       let y_f ← mkProjection y field

src/Lean/Elab/Tactic/FalseOrByContra.lean

@@ -36,7 +36,9 @@ partial def falseOrByContra (g : MVarId) (useClassical : Option Bool := none) :
   match ty with
   | .const ``False _ => pure g
   | .forallE _ _ _ _
-  | .app (.const ``Not _) _ => falseOrByContra (← g.intro1).2
+  | .app (.const ``Not _) _ =>
+    -- We set the transparency back to default; otherwise this breaks when run by a `simp` discharger.
+    falseOrByContra (← withTransparency default g.intro1P).2 useClassical
   | _ =>
     let gs ← if ← isProp ty then
       match useClassical with

src/Lean/Elab/Tactic/Induction.lean

@@ -59,7 +59,7 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) (remaini
   withCaseRef (getAltDArrow alt) rhs do
     if isHoleRHS rhs then
       addInfo
-      let gs' ← mvarId.withContext <| withRef rhs do
+      let gs' ← mvarId.withContext <| withTacticInfoContext rhs do
         let mvarDecl ← mvarId.getDecl
         let val ← elabTermEnsuringType rhs mvarDecl.type
         mvarId.assign val

src/Lean/Elab/Term.lean

@@ -354,8 +354,8 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl
 inductive LVal where
   | fieldIdx  (ref : Syntax) (i : Nat)
   /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierarchical/composite name.
-  `ref` is the syntax object representing the field. `targetStx` is the target object being accessed. -/
-  | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (targetStx : Syntax)
+  `ref` is the syntax object representing the field. `fullRef` includes the LHS. -/
+  | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (fullRef : Syntax)
 
 def LVal.getRef : LVal → Syntax
   | .fieldIdx ref _    => ref
@@ -1409,9 +1409,9 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
     trace[Elab.step.result] result
     pure result
 
-/-- Store in the `InfoTree` that `e` is a "dot"-completion target. -/
-def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr) (field? : Option Syntax := none) : TermElabM Unit := do
-  addCompletionInfo <| CompletionInfo.dot { expr := e, stx, lctx := (← getLCtx), elaborator := .anonymous, expectedType? } (field? := field?) (expectedType? := expectedType?)
+/-- Store in the `InfoTree` that `e` is a "dot"-completion target. `stx` should cover the entire term. -/
+def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr) : TermElabM Unit := do
+  addCompletionInfo <| CompletionInfo.dot { expr := e, stx, lctx := (← getLCtx), elaborator := .anonymous, expectedType? } (expectedType? := expectedType?)
 
 /--
   Main function for elaborating terms.

src/Lean/Expr.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Hashable
 import Lean.Data.KVMap
+import Lean.Data.SMap
 import Lean.Level
 
 namespace Lean
@@ -1389,6 +1390,8 @@ def mkDecIsFalse (pred proof : Expr) :=
 
 abbrev ExprMap (α : Type)  := HashMap Expr α
 abbrev PersistentExprMap (α : Type) := PHashMap Expr α
+abbrev SExprMap (α : Type)  := SMap Expr α
+
 abbrev ExprSet := HashSet Expr
 abbrev PersistentExprSet := PHashSet Expr
 abbrev PExprSet := PersistentExprSet
@@ -2019,17 +2022,46 @@ def mkEM (p : Expr) : Expr := mkApp (mkConst ``Classical.em) p
 /-- Return `p ↔ q` -/
 def mkIff (p q : Expr) : Expr := mkApp2 (mkConst ``Iff) p q
 
+/-! Constants for Nat typeclasses. -/
+namespace Nat
+
+def natType : Expr := mkConst ``Nat
+
+def instAdd : Expr := mkConst ``instAddNat
+def instHAdd : Expr := mkApp2 (mkConst ``instHAdd [levelZero]) natType instAdd
+
+def instSub : Expr := mkConst ``instSubNat
+def instHSub : Expr := mkApp2 (mkConst ``instHSub [levelZero]) natType instSub
+
+def instMul : Expr := mkConst ``instMulNat
+def instHMul : Expr := mkApp2 (mkConst ``instHMul [levelZero]) natType instMul
+
+def instDiv : Expr := mkConst ``Nat.instDivNat
+def instHDiv : Expr := mkApp2 (mkConst ``instHDiv [levelZero]) natType instDiv
+
+def instMod : Expr := mkConst ``Nat.instModNat
+def instHMod : Expr := mkApp2 (mkConst ``instHMod [levelZero]) natType instMod
+
+def instNatPow : Expr := mkConst ``instNatPowNat
+def instPow  : Expr := mkApp2 (mkConst ``instPowNat [levelZero]) natType instNatPow
+def instHPow : Expr := mkApp3 (mkConst ``instHPow [levelZero, levelZero]) natType natType instPow
+
+def instLT : Expr := mkConst ``instLTNat
+def instLE : Expr := mkConst ``instLENat
+
+end Nat
+
 private def natAddFn : Expr :=
   let nat := mkConst ``Nat
-  mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHAdd [0]) nat (mkConst ``instAddNat))
+  mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) nat nat nat Nat.instHAdd
 
 private def natSubFn : Expr :=
   let nat := mkConst ``Nat
-  mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHSub [0]) nat (mkConst ``instSubNat))
+  mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) nat nat nat Nat.instHSub
 
 private def natMulFn : Expr :=
   let nat := mkConst ``Nat
-  mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHMul [0]) nat (mkConst ``instMulNat))
+  mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat Nat.instHMul
 
 /-- Given `a : Nat`, returns `Nat.succ a` -/
 def mkNatSucc (a : Expr) : Expr :=
@@ -2048,7 +2080,7 @@ def mkNatMul (a b : Expr) : Expr :=
   mkApp2 natMulFn a b
 
 private def natLEPred : Expr :=
-  mkApp2 (mkConst ``LE.le [0]) (mkConst ``Nat) (mkConst ``instLENat)
+  mkApp2 (mkConst ``LE.le [0]) (mkConst ``Nat) Nat.instLE
 
 /-- Given `a b : Nat`, return `a ≤ b` -/
 def mkNatLE (a b : Expr) : Expr :=

src/Lean/Linter/MissingDocs.lean

@@ -236,7 +236,7 @@ def checkRegisterSimpAttr : SimpleHandler := mkSimpleHandler "simp attr"
 @[builtin_missing_docs_handler «in»]
 def handleIn : Handler := fun _ stx => do
   if stx[0].getKind == ``«set_option» then
-    let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
+    let opts ← Elab.elabSetOption stx[0][1] stx[0][3]
     withScope (fun scope => { scope with opts }) do
       missingDocs.run stx[2]
   else

src/Lean/Meta/ACLt.lean

@@ -50,7 +50,7 @@ mutual
    - We ignore metadata.
    - We ignore universe parameterst at constants.
 -/
-unsafe def main (a b : Expr) (mode : ReduceMode := .none) : MetaM Bool :=
+partial def main (a b : Expr) (mode : ReduceMode := .none) : MetaM Bool := do
   lt a b
 where
   reduce (e : Expr) : MetaM Expr := do
@@ -66,7 +66,9 @@ where
       | .none => return e
 
   lt (a b : Expr) : MetaM Bool := do
-    if ptrAddrUnsafe a == ptrAddrUnsafe b then
+    if a == b then
+      -- We used to have an "optimization" using only pointer equality.
+      -- This was a bad idea, `==` is often much cheaper than `acLt`.
       return false
     -- We ignore metadata
     else if a.isMData then
@@ -84,6 +86,16 @@ where
     else
       lt a₂ b₂
 
+  getParamsInfo (f : Expr) (numArgs : Nat) : MetaM (Array ParamInfo) := do
+    -- Ensure `f` does not have loose bound variables. This may happen in
+    -- since we go inside binders without extending the local context.
+    -- See `lexSameCtor` and `allChildrenLt`
+    -- See issue #3705.
+    if f.hasLooseBVars then
+      return #[]
+    else
+      return (← getFunInfoNArgs f numArgs).paramInfo
+
   ltApp (a b : Expr) : MetaM Bool := do
     let aFn := a.getAppFn
     let bFn := b.getAppFn
@@ -99,7 +111,7 @@ where
       else if aArgs.size > bArgs.size then
         return false
       else
-        let infos := (← getFunInfoNArgs aFn aArgs.size).paramInfo
+        let infos ← getParamsInfo aFn aArgs.size
         for i in [:infos.size] do
           -- We ignore instance implicit arguments during comparison
           if !infos[i]!.isInstImplicit then
@@ -137,7 +149,7 @@ where
     | .proj _ _ e ..    => lt e b
     | .app ..           =>
       a.withApp fun f args => do
-        let infos := (← getFunInfoNArgs f args.size).paramInfo
+        let infos ← getParamsInfo f args.size
         for i in [:infos.size] do
           -- We ignore instance implicit arguments during comparison
           if !infos[i]!.isInstImplicit then
@@ -176,7 +188,8 @@ end
 
 end ACLt
 
-@[implemented_by ACLt.main, inherit_doc ACLt.main]
-opaque Expr.acLt : Expr → Expr → (mode : ACLt.ReduceMode := .none) → MetaM Bool
+@[inherit_doc ACLt.main]
+def acLt (a b : Expr) (mode : ACLt.ReduceMode := .none) : MetaM Bool :=
+  ACLt.main a b mode
 
 end Lean.Meta

src/Lean/Meta/AbstractMVars.lean

@@ -101,7 +101,10 @@ partial def abstractExprMVars (e : Expr) : M Expr := do
             let type   ← abstractExprMVars decl.type
             let fvarId ← mkFreshFVarId
             let fvar := mkFVar fvarId;
-            let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter (← get).fvars.size else decl.userName
+            let userName ← if decl.userName.isAnonymous then
+              pure <| (`x).appendIndexAfter (← get).fvars.size
+            else
+              pure decl.userName
             modify fun s => {
               s with
               emap  := s.emap.insert mvarId fvar,

src/Lean/Meta/Basic.lean

@@ -1444,6 +1444,12 @@ def whnfD (e : Expr) : MetaM Expr :=
 def whnfI (e : Expr) : MetaM Expr :=
   withTransparency TransparencyMode.instances <| whnf e
 
+/-- `whnf` with at most instances transparency. -/
+def whnfAtMostI (e : Expr) : MetaM Expr := do
+  match (← getTransparency) with
+  | .all | .default => withTransparency TransparencyMode.instances <| whnf e
+  | _ => whnf e
+
 /--
   Mark declaration `declName` with the attribute `[inline]`.
   This method does not check whether the given declaration is a definition.

src/Lean/Meta/Canonicalizer.lean

@@ -82,8 +82,10 @@ private partial def mkKey (e : Expr) : CanonM Key := do
     return key
   else
     let key ← match e with
-      | .sort .. | .fvar .. | .bvar .. | .const .. | .lit .. =>
+      | .sort .. | .fvar .. | .bvar .. | .lit .. =>
         pure { e := (← shareCommon e) }
+      | .const n _ =>
+        pure { e := (← shareCommon (.const n [])) }
       | .mvar .. =>
         -- We instantiate assigned metavariables because the
         -- pretty-printer also instantiates them.
@@ -92,7 +94,7 @@ private partial def mkKey (e : Expr) : CanonM Key := do
         else mkKey eNew
       | .mdata _ a => mkKey a
       | .app .. =>
-        let f := (← mkKey e.getAppFn).e
+        let f := e.getAppFn
         if f.isMVar then
           let eNew ← instantiateMVars e
           unless eNew == e do
@@ -107,7 +109,8 @@ private partial def mkKey (e : Expr) : CanonM Key := do
               pure (mkSort 0) -- some dummy value for erasing implicit
           else
             pure (← mkKey arg).e
-        pure { e := (← shareCommon (mkAppN f args)) }
+        let f' := (← mkKey f).e
+        pure { e := (← shareCommon (mkAppN f' args)) }
       | .lam n t b i =>
         pure { e := (← shareCommon (.lam n (← mkKey t).e (← mkKey b).e i)) }
       | .forallE n t b i =>

src/Lean/Meta/Eqns.lean

@@ -7,8 +7,28 @@ prelude
 import Lean.ReservedNameAction
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
+import Lean.Meta.Match.MatcherInfo
 
 namespace Lean.Meta
+/--
+Environment extension for storing which declarations are recursive.
+This information is populated by the `PreDefinition` module, but the simplifier
+uses when unfolding declarations.
+-/
+builtin_initialize recExt : TagDeclarationExtension ← mkTagDeclarationExtension `recExt
+
+/--
+Marks the given declaration as recursive.
+-/
+def markAsRecursive (declName : Name) : CoreM Unit :=
+  modifyEnv (recExt.tag · declName)
+
+/--
+Returns `true` if `declName` was defined using well-founded recursion, or structural recursion.
+-/
+def isRecursiveDefinition (declName : Name) : CoreM Bool :=
+  return recExt.isTagged (← getEnv) declName
+
 def eqnThmSuffixBase := "eq"
 def eqnThmSuffixBasePrefix := eqnThmSuffixBase ++ "_"
 def eqn1ThmSuffix := eqnThmSuffixBasePrefix ++ "1"
@@ -38,7 +58,13 @@ Ensures that `f.eq_def` and `f.eq_<idx>` are reserved names if `f` is a safe def
 -/
 builtin_initialize registerReservedNamePredicate fun env n =>
   match n with
-  | .str p s => (isEqnReservedNameSuffix s || isUnfoldReservedNameSuffix s) && env.isSafeDefinition p
+  | .str p s =>
+    (isEqnReservedNameSuffix s || isUnfoldReservedNameSuffix s)
+    && env.isSafeDefinition p
+    -- Remark: `f.match_<idx>.eq_<idx>` are private definitions and are not treated as reserved names
+    -- Reason: `f.match_<idx>.splitter is generated at the same time, and can eliminate into type.
+    -- Thus, it cannot be defined in different modules since it is not a theorem, and is used to generate code.
+    && !isMatcherCore env p
   | _ => false
 
 def GetEqnsFn := Name → MetaM (Option (Array Name))

src/Lean/Meta/ExprDefEq.lean

@@ -1690,9 +1690,9 @@ private def isDefEqOnFailure (t s : Expr) : MetaM Bool := do
     tryUnificationHints t s <||> tryUnificationHints s t
 
 private def isDefEqProj : Expr → Expr → MetaM Bool
-  | Expr.proj m i t, Expr.proj n j s => pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
-  | Expr.proj structName 0 s, v => isDefEqSingleton structName s v
-  | v, Expr.proj structName 0 s => isDefEqSingleton structName s v
+  | .proj m i t, .proj n j s => pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
+  | .proj structName 0 s, v  => isDefEqSingleton structName s v
+  | v, .proj structName 0 s  => isDefEqSingleton structName s v
   | _, _ => pure false
 where
   /-- If `structName` is a structure with a single field and `(?m ...).1 =?= v`, then solve constraint as `?m ... =?= ⟨v⟩` -/
@@ -1779,25 +1779,30 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
   whenUndefDo (isDefEqEta t s) do
   whenUndefDo (isDefEqEta s t) do
   if (← isDefEqProj t s) then return true
-  whenUndefDo (isDefEqNative t s) do
-  whenUndefDo (isDefEqNat t s) do
-  whenUndefDo (isDefEqOffset t s) do
-  whenUndefDo (isDefEqDelta t s) do
-  -- We try structure eta *after* lazy delta reduction;
-  -- otherwise we would end up applying it at every step of a reduction chain
-  -- as soon as one of the sides is a constructor application,
-  -- which is very costly because it requires us to unify the fields.
-  if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
-    return true
-  if t.isConst && s.isConst then
-    if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
-  else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
-    return true
+  let t' ← whnfCore t
+  let s' ← whnfCore s
+  if t != t' || s != s' then
+    Meta.isExprDefEqAux t' s'
   else
-    whenUndefDo (isDefEqProjInst t s) do
-    whenUndefDo (isDefEqStringLit t s) do
-    if (← isDefEqUnitLike t s) then return true else
-    isDefEqOnFailure t s
+    whenUndefDo (isDefEqNative t s) do
+    whenUndefDo (isDefEqNat t s) do
+    whenUndefDo (isDefEqOffset t s) do
+    whenUndefDo (isDefEqDelta t s) do
+    -- We try structure eta *after* lazy delta reduction;
+    -- otherwise we would end up applying it at every step of a reduction chain
+    -- as soon as one of the sides is a constructor application,
+    -- which is very costly because it requires us to unify the fields.
+    if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
+      return true
+    if t.isConst && s.isConst then
+      if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
+    else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
+      return true
+    else
+      whenUndefDo (isDefEqProjInst t s) do
+      whenUndefDo (isDefEqStringLit t s) do
+      if (← isDefEqUnitLike t s) then return true else
+      isDefEqOnFailure t s
 
 inductive DefEqCacheKind where
   | transient -- problem has mvars or is using nonstandard configuration, we should use transient cache
@@ -1863,14 +1868,41 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
   whenUndefDo (isDefEqProofIrrel t s) do
   /-
     We also reduce projections here to prevent expensive defeq checks when unifying TC operations.
-    When unifying e.g. `@Neg.neg α (@Field.toNeg α inst1) =?= @Neg.neg α (@Field.toNeg α inst2)`,
+    When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
     we only want to unify negation (and not all other field operations as well).
     Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
-    We used to *not* reduce projections here, to support unifying `(?a).1 =?= (x, y).1`.
-    NOTE: this still seems to work because we don't eagerly unfold projection definitions to primitive projections.
+
+    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
+    We added this refinement to address a performance issue in code such as
+    ```
+    let val : Test := bar c1 key
+    have : val.1 = (bar c1 key).1 := rfl
+    ```
+    where `bar` is a complex function that takes a long time to be reduced.
+
+    Note that the current solution times out at unification problems such as
+    `(f x).1 =?= (g x).1` where `f`, `g` are defined as
+    ```
+    structure Foo where
+      x : Nat
+      y : Nat
+
+    def f (x : Nat) : Foo :=
+      { x, y := ack 10 10 }
+
+    def g (x : Nat) : Foo :=
+      { x, y := ack 10 11 }
+    ```
+    and `ack` is ackermann. We claim this is an abuse of the unifier.
+    That being said, we could in principle address this issue by implementing
+    lazy-delta reduction at `isDefEqProj`.
+
+    The current solution should be sufficient. In the past, we have used
+    `whnfCore t (config := { proj := .yes })` which more conservative than `.yesWithDeltaI`,
+    and it only created performance issues when handling TC unification problems.
   -/
-  let t' ← whnfCore t
-  let s' ← whnfCore s
+  let t' ← whnfCore t (config := { proj := .yesWithDeltaI })
+  let s' ← whnfCore s (config := { proj := .yesWithDeltaI })
   if t != t' || s != s' then
     isExprDefEqAuxImpl t' s'
   else

src/Lean/Meta/LazyDiscrTree.lean

@@ -25,7 +25,6 @@ elaborated additional parts of the tree.
 -/
 namespace Lean.Meta.LazyDiscrTree
 
-
 /--
 Discrimination tree key.
 -/
@@ -580,41 +579,76 @@ partial def appendResults (mr : MatchResult α) (a : Array α) : Array α :=
 
 end MatchResult
 
-private partial def getMatchLoop (todo : Array Expr) (score : Nat) (c : TrieIndex)
-    (result : MatchResult α) : MatchM α (MatchResult α) := do
-  let (vs, star, cs) ← evalNode c
-  if todo.isEmpty then
-    return result.push score vs
-  else if star == 0 && cs.isEmpty then
-    return result
-  else
-    let e     := todo.back
-    let todo  := todo.pop
-    /- We must always visit `Key.star` edges since they are wildcards.
-        Thus, `todo` is not used linearly when there is `Key.star` edge
-        and there is an edge for `k` and `k != Key.star`. -/
-    let visitStar (result : MatchResult α) : MatchM α (MatchResult α) :=
-      if star != 0 then
-        getMatchLoop todo (score + 1) star result
-      else
-        return result
-    let visitNonStar (k : Key) (args : Array Expr) (result : MatchResult α) :=
-      match cs.find? k with
-      | none   => return result
-      | some c => getMatchLoop (todo ++ args) (score + 1) c result
-    let result ← visitStar result
-    let (k, args) ← MatchClone.getMatchKeyArgs e (root := false) (←read)
-    match k with
-    | .star  => return result
-    /-
-      Note: dep-arrow vs arrow
-      Recall that dependent arrows are `(Key.other, #[])`, and non-dependent arrows are
-      `(Key.arrow, #[a, b])`.
-      A non-dependent arrow may be an instance of a dependent arrow (stored at `DiscrTree`).
-      Thus, we also visit the `Key.other` child.
-    -/
-    | .arrow => visitNonStar .other #[] (← visitNonStar k args result)
-    | _      => visitNonStar k args result
+/-
+A partial match captures the intermediate state of a match
+execution.
+
+N.B. The discriminator tree in Lean has non-determinism due to
+star and function arrows, so matching loop maintains a stack of
+partial match results.
+-/
+structure PartialMatch where
+  -- Remaining terms to match
+  todo : Array Expr
+  -- Number of non-star matches so far.
+  score : Nat
+  -- Trie to match next
+  c : TrieIndex
+  deriving Inhabited
+
+/--
+Evaluate all partial matches and add resulting matches to `MatchResult`.
+
+The partial matches are stored in an array that is used as a stack. When adding
+multiple partial matches to explore next, to ensure the order of results matches
+user expectations, this code must add paths we want to prioritize and return
+results earlier are added last.
+-/
+private partial def getMatchLoop (cases : Array PartialMatch) (result : MatchResult α) : MatchM α (MatchResult α) := do
+  if cases.isEmpty then
+    pure result
+  else do
+    let ca := cases.back
+    let cases := cases.pop
+    let (vs, star, cs) ← evalNode ca.c
+    if ca.todo.isEmpty then
+      let result := result.push ca.score vs
+      getMatchLoop cases result
+    else if star == 0 && cs.isEmpty then
+      getMatchLoop cases result
+    else
+      let e     := ca.todo.back
+      let todo  := ca.todo.pop
+      /- We must always visit `Key.star` edges since they are wildcards.
+          Thus, `todo` is not used linearly when there is `Key.star` edge
+          and there is an edge for `k` and `k != Key.star`. -/
+      let pushStar (cases : Array PartialMatch) :=
+        if star = 0 then
+          cases
+        else
+          cases.push { todo, score := ca.score, c := star }
+      let pushNonStar (k : Key) (args : Array Expr) (cases : Array PartialMatch) :=
+        match cs.find? k with
+        | none   => cases
+        | some c => cases.push { todo := todo ++ args, score := ca.score + 1, c }
+      let cases := pushStar cases
+      let (k, args) ← MatchClone.getMatchKeyArgs e (root := false) (← read)
+      let cases :=
+        match k with
+        | .star  => cases
+        /-
+          Note: dep-arrow vs arrow
+          Recall that dependent arrows are `(Key.other, #[])`, and non-dependent arrows are
+          `(Key.arrow, #[a, b])`.
+          A non-dependent arrow may be an instance of a dependent arrow (stored at `DiscrTree`).
+          Thus, we also visit the `Key.other` child.
+        -/
+        | .arrow =>
+          cases |> pushNonStar .other #[]
+                |> pushNonStar k args
+        | _      =>
+          cases |> pushNonStar k args
+      getMatchLoop cases result
 
 private def getStarResult (root : Lean.HashMap Key TrieIndex) : MatchM α (MatchResult α) :=
   match root.find? .star with
@@ -624,11 +658,14 @@ private def getStarResult (root : Lean.HashMap Key TrieIndex) : MatchM α (Match
     let (vs, _) ← evalNode idx
     pure <| ({} : MatchResult α).push (score := 1) vs
 
-private def getMatchRoot (r : Lean.HashMap Key TrieIndex) (k : Key) (args : Array Expr)
-    (result : MatchResult α) : MatchM α (MatchResult α) :=
+/-
+Add partial match to cases if discriminator tree root map has potential matches.
+-/
+private def pushRootCase (r : Lean.HashMap Key TrieIndex) (k : Key) (args : Array Expr)
+    (cases : Array PartialMatch) : Array PartialMatch :=
   match r.find? k with
-  | none => pure result
-  | some c => getMatchLoop args (score := 1) c result
+  | none => cases
+  | some c => cases.push { todo := args, score := 1, c }
 
 /--
   Find values that match `e` in `root`.
@@ -637,13 +674,17 @@ private def getMatchCore (root : Lean.HashMap Key TrieIndex) (e : Expr) :
     MatchM α (MatchResult α) := do
   let result ← getStarResult root
   let (k, args) ← MatchClone.getMatchKeyArgs e (root := true) (← read)
-  match k with
-  | .star  => return result
-  /- See note about "dep-arrow vs arrow" at `getMatchLoop` -/
-  | .arrow =>
-    getMatchRoot root k args (← getMatchRoot root .other #[] result)
-  | _ =>
-    getMatchRoot root k args result
+  let cases :=
+    match k with
+    | .star  =>
+      #[]
+    /- See note about "dep-arrow vs arrow" at `getMatchLoop` -/
+    | .arrow =>
+      #[] |> pushRootCase root .other #[]
+          |> pushRootCase root k args
+    | _ =>
+      #[] |> pushRootCase root k args
+  getMatchLoop cases result
 
 /--
   Find values that match `e` in `d`.

src/Lean/Meta/Match/MatchEqs.lean

@@ -649,13 +649,18 @@ where
 private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns := withLCtx {} {} do
   trace[Meta.Match.matchEqs] "mkEquationsFor '{matchDeclName}'"
   withConfig (fun c => { c with etaStruct := .none }) do
-  let baseName := matchDeclName
+  /-
+  Remark: user have requested the `split` tactic to be available for writing code.
+  Thus, the `splitter` declaration must be a definition instead of a theorem.
+  Moreover, the `splitter` is generated on demand, and we currently
+  can't import the same definition from different modules. Thus, we must
+  keep `splitter` as a private declaration to prevent import failures.
+  -/
+  let baseName := mkPrivateName (← getEnv) matchDeclName
   let splitterName := baseName ++ `splitter
   let constInfo ← getConstInfo matchDeclName
   let us := constInfo.levelParams.map mkLevelParam
   let some matchInfo ← getMatcherInfo? matchDeclName | throwError "'{matchDeclName}' is not a matcher function"
-  -- `alreadyDeclared` is `true` if matcher equations were defined in an imported module
-  let alreadyDeclared := (← getEnv).contains splitterName
   let numDiscrEqs := getNumEqsFromDiscrInfos matchInfo.discrInfos
   forallTelescopeReducing constInfo.type fun xs matchResultType => do
     let mut eqnNames := #[]
@@ -690,59 +695,51 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
         for discr in discrs.toArray.reverse, pattern in patterns.reverse do
           notAlt ← mkArrow (← mkEqHEq discr pattern) notAlt
         notAlt ← mkForallFVars (discrs ++ ys) notAlt
-        if alreadyDeclared then
-          -- If the matcher equations and splitter have already been declared, the only
-          -- values we are `notAlt` and `splitterAltNumParam`. This code is a bit hackish.
-          return (notAlt, default, splitterAltNumParam, default)
-        else
-          /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant.
-             Thus, we need to create new `alts`. -/
-          withNewAlts numDiscrEqs discrs patterns alts fun alts => do
-            let alt := alts[i]!
-            let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
-            let rhs := mkAppN alt rhsArgs
-            let thmType ← mkEq lhs rhs
-            let thmType ← hs.foldrM (init := thmType) (mkArrow · ·)
-            let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType
-            let thmType ← unfoldNamedPattern thmType
-            let thmVal ← proveCondEqThm matchDeclName thmType
-            addDecl <| Declaration.thmDecl {
-              name        := thmName
-              levelParams := constInfo.levelParams
-              type        := thmType
-              value       := thmVal
-            }
-            return (notAlt, splitterAltType, splitterAltNumParam, argMask)
+        /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant.
+           Thus, we need to create new `alts`. -/
+        withNewAlts numDiscrEqs discrs patterns alts fun alts => do
+          let alt := alts[i]!
+          let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
+          let rhs := mkAppN alt rhsArgs
+          let thmType ← mkEq lhs rhs
+          let thmType ← hs.foldrM (init := thmType) (mkArrow · ·)
+          let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType
+          let thmType ← unfoldNamedPattern thmType
+          let thmVal ← proveCondEqThm matchDeclName thmType
+          addDecl <| Declaration.thmDecl {
+            name        := thmName
+            levelParams := constInfo.levelParams
+            type        := thmType
+            value       := thmVal
+          }
+          return (notAlt, splitterAltType, splitterAltNumParam, argMask)
       notAlts := notAlts.push notAlt
       splitterAltTypes := splitterAltTypes.push splitterAltType
       splitterAltNumParams := splitterAltNumParams.push splitterAltNumParam
       altArgMasks := altArgMasks.push argMask
       trace[Meta.Match.matchEqs] "splitterAltType: {splitterAltType}"
       idx := idx + 1
-    if alreadyDeclared then
-      return { eqnNames, splitterName, splitterAltNumParams }
-    else
-      -- Define splitter with conditional/refined alternatives
-      withSplitterAlts splitterAltTypes fun altsNew => do
-        let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
-        let splitterType ← mkForallFVars splitterParams matchResultType
-        trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
-        let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
-        let template ← deltaExpand template (· == constInfo.name)
-        let template := template.headBeta
-        let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks)
-        addAndCompile <| Declaration.defnDecl {
-          name        := splitterName
-          levelParams := constInfo.levelParams
-          type        := splitterType
-          value       := splitterVal
-          hints       := .abbrev
-          safety      := .safe
-        }
-        setInlineAttribute splitterName
-        let result := { eqnNames, splitterName, splitterAltNumParams }
-        registerMatchEqns matchDeclName result
-        return result
+    -- Define splitter with conditional/refined alternatives
+    withSplitterAlts splitterAltTypes fun altsNew => do
+      let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
+      let splitterType ← mkForallFVars splitterParams matchResultType
+      trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
+      let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
+      let template ← deltaExpand template (· == constInfo.name)
+      let template := template.headBeta
+      let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks)
+      addAndCompile <| Declaration.defnDecl {
+        name        := splitterName
+        levelParams := constInfo.levelParams
+        type        := splitterType
+        value       := splitterVal
+        hints       := .abbrev
+        safety      := .safe
+      }
+      setInlineAttribute splitterName
+      let result := { eqnNames, splitterName, splitterAltNumParams }
+      registerMatchEqns matchDeclName result
+      return result
 
 /- See header at `MatchEqsExt.lean` -/
 @[export lean_get_match_equations_for]
@@ -753,23 +750,4 @@ def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
 
 builtin_initialize registerTraceClass `Meta.Match.matchEqs
 
-private def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
-  unless (← isMatcher declName) do
-    return none
-  let result ← getEquationsForImpl declName
-  return some result.eqnNames
-
-builtin_initialize
-  registerGetEqnsFn getEqnsFor?
-
-/-
-We register `foo.match_<idx>.splitter` as a reserved name, but
-we do not install a realizer. The `splitter` will be generated by the
-`foo.match_<idx>.eq_<idx>` realizer.
--/
-builtin_initialize registerReservedNamePredicate fun env n =>
-  match n with
-  | .str p "splitter" => isMatcherCore env p
-  | _ => false
-
 end Lean.Meta.Match

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -24,8 +24,10 @@ private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNu
         let alt ← try instantiateLambda alt xs catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
         forallBoundedTelescope d (some 1) fun x _ => do
           let alt ← mkLambdaFVars x alt -- x is the new argument we are adding to the alternative
-          let refined := if refined then refined else
-            !(← isDefEq unrefinedArgType (← inferType x[0]!))
+          let refined ← if refined then
+            pure refined
+          else
+            pure <| !(← isDefEq unrefinedArgType (← inferType x[0]!))
           return (← mkLambdaFVars xs alt, refined)
       updateAlts unrefinedArgType (b.instantiate1 alt) (altNumParams.set! i (numParams+1)) (alts.set ⟨i, h⟩ alt) refined (i+1)
     | _ => throwError "unexpected type at MatcherApp.addArg"

src/Lean/Meta/Offset.lean

@@ -54,6 +54,16 @@ where
     | HPow.hPow _ _ _ i a b => guard (← isInstHPowNat i); return (← evalNat a) ^ (← evalNat b)
     | _ => failure
 
+/--
+Checks that expression `e` is definitional equal to `inst`.
+
+Uses `instances` transparency so that reducible terms and instances extended
+other instances are unfolded.
+-/
+def matchesInstance (e inst : Expr) : MetaM Bool :=
+  -- Note. We use withNewMCtxDepth to avoid assigning meta-variables in isDefEq checks
+  withNewMCtxDepth (withTransparency .instances (isDefEq e inst))
+
 mutual
 
 /--
@@ -65,7 +75,7 @@ private partial def getOffset (e : Expr) : MetaM (Expr × Nat) :=
   return (← isOffset? e).getD (e, 0)
 
 /--
-Similar to `getOffset` but returns `none` if the expression is not syntactically an offset.
+Similar to `getOffset` but returns `none` if the expression is not an offset.
 -/
 partial def isOffset? (e : Expr) : OptionT MetaM (Expr × Nat) := do
   let add (a b : Expr) := do
@@ -77,8 +87,8 @@ partial def isOffset? (e : Expr) : OptionT MetaM (Expr × Nat) := do
     let (s, k) ← getOffset a
     return (s, k+1)
   | Nat.add a b => add a b
-  | Add.add _ i a b => guard (← isInstAddNat i); add a b
-  | HAdd.hAdd _ _ _ i a b => guard (← isInstHAddNat i); add a b
+  | Add.add _ i a b => guard (← matchesInstance i Nat.instAdd); add a b
+  | HAdd.hAdd _ _ _ i a b => guard (← matchesInstance i Nat.instHAdd); add a b
   | _ => failure
 
 end

src/Lean/Meta/Tactic/Rewrites.lean

@@ -329,11 +329,11 @@ def findRewrites (hyps : Array (Expr × Bool × Nat))
     (leavePercentHeartbeats : Nat := 10) : MetaM (List RewriteResult) := do
   let mctx ← getMCtx
   let candidates ← rewriteCandidates hyps moduleRef target forbidden
-  let minHeartbeats : Nat :=
+  let minHeartbeats : Nat ←
         if (← getMaxHeartbeats) = 0 then
-          0
+          pure 0
         else
-          leavePercentHeartbeats * (← getRemainingHeartbeats) / 100
+          pure <| leavePercentHeartbeats * (← getRemainingHeartbeats) / 100
   let cfg : RewriteResultConfig :=
         { stopAtRfl, minHeartbeats, max, mctx, goal, target, side }
   return (← takeListAux cfg {} (Array.mkEmpty max) candidates.toList).toList

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Simproc
+import Init.Data.Nat.Simproc
 import Lean.Meta.LitValues
 import Lean.Meta.Offset
 import Lean.Meta.Tactic.Simp.Simproc
@@ -55,11 +56,7 @@ builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := reduceBin ``HPow.hPo
 builtin_dsimproc [simp, seval] reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd
 
 builtin_simproc [simp, seval] reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)
-builtin_simproc [simp, seval] reduceLE  (( _ : Nat) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
 builtin_simproc [simp, seval] reduceGT  (( _ : Nat) > _)  := reduceBinPred ``GT.gt 4 (. > .)
-builtin_simproc [simp, seval] reduceGE  (( _ : Nat) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
-builtin_simproc [simp, seval] reduceEq  (( _ : Nat) = _)  := reduceBinPred ``Eq 3 (. = .)
-builtin_simproc [simp, seval] reduceNe  (( _ : Nat) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
 builtin_dsimproc [simp, seval] reduceBEq  (( _ : Nat) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
 builtin_dsimproc [simp, seval] reduceBNe  (( _ : Nat) != _)  := reduceBoolPred ``bne 4 (. != .)
 
@@ -68,4 +65,263 @@ builtin_dsimproc [seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do
   let_expr OfNat.ofNat _ _ _ ← e | return .continue
   return .done e
 
+/-- A literal natural number or a base + offset expression. -/
+private inductive NatOffset where
+  /- denotes expression definition equal to `n` -/
+  | const (n : Nat)
+  /-- denotes `e + o` where `o` is expression definitionally equal to `n` -/
+  | offset (e o : Expr) (n : Nat)
+
+/- Attempt to parse a `NatOffset` from an expression-/
+private partial def NatOffset.asOffset (e : Expr) : Meta.SimpM (Option (Expr × Nat)) := do
+  if e.isAppOfArity ``HAdd.hAdd 6 then
+    let inst := e.appFn!.appFn!.appArg!
+    unless ← matchesInstance inst Nat.instHAdd do return none
+    let b := e.appFn!.appArg!
+    let o := e.appArg!
+    let some n ← Nat.fromExpr? o | return none
+    pure (some (b, n))
+  else if e.isAppOfArity ``Add.add 4 then
+    let inst := e.appFn!.appFn!.appArg!
+    unless ← matchesInstance inst Nat.instAdd do return none
+    let b := e.appFn!.appArg!
+    let some n ← Nat.fromExpr? e.appArg! | return none
+    pure (some (b, n))
+  else if e.isAppOfArity ``Nat.add 2 then
+    let b := e.appFn!.appArg!
+    let some n ← Nat.fromExpr? e.appArg! | return none
+    pure (some (b, n))
+  else if e.isAppOfArity ``Nat.succ 1 then
+    let b := e.appArg!
+    pure (some (b, 1))
+  else
+    pure none
+
+/- Attempt to parse a `NatOffset` from an expression-/
+private partial def NatOffset.fromExprAux (e : Expr) (inc : Nat) : Meta.SimpM (Option (Expr × Nat)) := do
+  let e := e.consumeMData
+  match ← asOffset e with
+  | some (b, o) =>
+    fromExprAux b (inc + o)
+  | none =>
+    return if inc != 0 then some (e, inc) else none
+
+/- Attempt to parse a `NatOffset` from an expression-/
+private def NatOffset.fromExpr? (e : Expr) (inc : Nat := 0) : Meta.SimpM (Option NatOffset) := do
+  match ← Nat.fromExpr? e with
+  | some n => pure (some (const (n + inc)))
+  | none =>
+    match ← fromExprAux e inc with
+    | none => pure none
+    | some (b, o) => pure (some (offset b (toExpr o) o))
+
+private def mkAddNat (x y : Expr) : Expr :=
+  let lz := levelZero
+  let nat := mkConst ``Nat
+  let instHAdd := mkAppN (mkConst ``instHAdd [lz]) #[nat, mkConst ``instAddNat]
+  mkAppN (mkConst ``HAdd.hAdd [lz, lz, lz]) #[nat, nat, nat, instHAdd, x, y]
+
+private def mkSubNat (x y : Expr) : Expr :=
+  let lz := levelZero
+  let nat := mkConst ``Nat
+  let instSub := mkConst ``instSubNat
+  let instHSub := mkAppN (mkConst ``instHSub [lz]) #[nat, instSub]
+  mkAppN (mkConst ``HSub.hSub [lz, lz, lz]) #[nat, nat, nat, instHSub, x, y]
+
+private def mkEqNat (x y : Expr) : Expr :=
+  mkAppN (mkConst ``Eq [levelOne]) #[mkConst ``Nat, x, y]
+
+private def mkBeqNat (x y : Expr) : Expr :=
+  mkAppN (mkConst ``BEq.beq [levelZero]) #[mkConst ``Nat, mkConst ``instBEqNat, x, y]
+
+private def mkBneNat (x y : Expr) : Expr :=
+  mkAppN (mkConst ``bne [levelZero]) #[mkConst ``Nat, mkConst ``instBEqNat, x, y]
+
+private def mkLENat (x y : Expr) : Expr :=
+  mkAppN (.const ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat, x, y]
+
+private def mkGENat (x y : Expr) : Expr := mkLENat y x
+
+private def mkLTNat (x y : Expr) : Expr :=
+  mkAppN (.const ``LT.lt [levelZero]) #[mkConst ``Nat, mkConst ``instLTNat, x, y]
+
+private def mkGTNat (x y : Expr) : Expr := mkLTNat y x
+
+private def mkOfDecideEqTrue (p : Expr) : MetaM Expr := do
+  let d ← Meta.mkDecide p
+  pure <| mkAppN (mkConst ``of_decide_eq_true) #[p, d.appArg!, (← Meta.mkEqRefl (mkConst ``true))]
+
+def applySimprocConst (expr : Expr) (nm : Name) (args : Array Expr) : SimpM Step := do
+  unless (← getEnv).contains nm do return .continue
+  let finProof := mkAppN (mkConst nm) args
+  return .visit { expr, proof? := finProof, cache := true }
+
+inductive EqResult where
+| decide (b : Bool) : EqResult
+| false (p : Expr) : EqResult
+| eq (x y : Expr) (p : Expr) : EqResult
+
+def applyEqLemma (e : Expr → EqResult) (lemmaName : Name) (args : Array Expr) : SimpM (Option EqResult) := do
+  unless (← getEnv).contains lemmaName do
+    return none
+  return .some (e (mkAppN (mkConst lemmaName) args))
+
+def reduceNatEqExpr (x y : Expr) : SimpM (Option EqResult):= do
+  let some xno ← NatOffset.fromExpr? x | return none
+  let some yno ← NatOffset.fromExpr? y | return none
+  match xno, yno with
+  | .const xn, .const yn =>
+    return some (.decide (xn = yn))
+  | .offset xb xo xn, .const yn => do
+    if xn ≤ yn then
+      let leProof ← mkOfDecideEqTrue (mkLENat xo y)
+      applyEqLemma (.eq xb (toExpr (yn - xn))) ``Nat.Simproc.add_eq_le #[xb, xo, y, leProof]
+    else
+      let gtProof ← mkOfDecideEqTrue (mkGTNat xo y)
+      applyEqLemma .false ``Nat.Simproc.add_eq_gt  #[xb, xo, y, gtProof]
+  | .const xn, .offset yb yo yn => do
+    if yn ≤ xn then
+      let leProof ← mkOfDecideEqTrue (mkLENat yo x)
+      applyEqLemma (.eq yb (toExpr (xn - yn))) ``Nat.Simproc.eq_add_le  #[x, yb, yo, leProof]
+    else
+      let gtProof ← mkOfDecideEqTrue (mkGTNat yo x)
+      applyEqLemma .false ``Nat.Simproc.eq_add_gt #[x, yb, yo, gtProof]
+  | .offset xb xo xn, .offset yb yo yn => do
+    if xn ≤ yn then
+      let zb := (if xn = yn then yb else mkAddNat yb (toExpr (yn - xn)))
+      let leProof ← mkOfDecideEqTrue (mkLENat xo yo)
+      applyEqLemma (.eq xb zb) ``Nat.Simproc.add_eq_add_le #[xb, yb, xo, yo, leProof]
+    else
+      let zb := mkAddNat xb (toExpr (xn - yn))
+      let geProof ← mkOfDecideEqTrue (mkGENat xo yo)
+      applyEqLemma (.eq zb yb) ``Nat.Simproc.add_eq_add_ge #[xb, yb, xo, yo, geProof]
+
+builtin_simproc [simp, seval] reduceEqDiff ((_ : Nat) = _) := fun e => do
+  unless e.isAppOfArity ``Eq 3 do
+    return .continue
+  let x := e.appFn!.appArg!
+  let y := e.appArg!
+  match ← reduceNatEqExpr x y with
+  | none =>
+    return .continue
+  | some (.decide true) =>
+    let d ← mkDecide e
+    let p := mkAppN (mkConst ``eq_true_of_decide)  #[e, d.appArg!, (← mkEqRefl (mkConst ``true))]
+    return .done  { expr := mkConst ``True,  proof? := some p, cache := true }
+  | some (.decide false) =>
+    let d ← mkDecide e
+    let p := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))]
+    return .done  { expr := mkConst ``False, proof? := some p, cache := true }
+  | some (.false p)  =>
+    return .done  { expr := mkConst ``False, proof? := some p, cache := true }
+  | some (.eq x y p) =>
+    return .visit { expr := mkEqNat x y,     proof? := some p, cache := true }
+
+builtin_simproc [simp, seval] reduceBeqDiff ((_ : Nat) == _) := fun e => do
+  unless e.isAppOfArity ``BEq.beq 4 do
+    return .continue
+  let x := e.appFn!.appArg!
+  let y := e.appArg!
+  match ← reduceNatEqExpr x y with
+  | none =>
+    return .continue
+  | some (.decide b) =>
+    return .done { expr := toExpr b }
+  | some (.false p) =>
+    let q := mkAppN (mkConst ``Nat.Simproc.beqFalseOfEqFalse) #[x, y, p]
+    return .done  { expr := mkConst ``false, proof? := some q, cache := true }
+  | some (.eq u v p) =>
+    let q := mkAppN (mkConst ``Nat.Simproc.beqEqOfEqEq) #[x, y, u, v, p]
+    return .visit { expr := mkBeqNat u v, proof? := some q, cache := true }
+
+builtin_simproc [simp, seval] reduceBneDiff ((_ : Nat) != _) := fun e => do
+  unless e.isAppOfArity ``bne 4 do
+    return .continue
+  let x := e.appFn!.appArg!
+  let y := e.appArg!
+  match ← reduceNatEqExpr x y with
+  | none =>
+    return .continue
+  | some (.decide b) =>
+    return .done { expr := toExpr (!b) }
+  | some (.false p) =>
+    let q := mkAppN (mkConst ``Nat.Simproc.bneTrueOfEqFalse) #[x, y, p]
+    return .done  { expr := mkConst ``true, proof? := some q, cache := true }
+  | some (.eq u v p) =>
+    let q := mkAppN (mkConst ``Nat.Simproc.bneEqOfEqEq) #[x, y, u, v, p]
+    return .visit { expr := mkBneNat u v, proof? := some q, cache := true }
+
+def reduceLTLE (nm : Name) (arity : Nat) (isLT : Bool) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity nm arity do
+    return .continue
+  let x := e.appFn!.appArg!
+  let y := e.appArg!
+  let some xno ← NatOffset.fromExpr? x (inc := cond isLT 1 0) | return .continue
+  let some yno ← NatOffset.fromExpr? y | return .continue
+  match xno, yno with
+  | .const xn, .const yn =>
+    Meta.Simp.evalPropStep e (xn ≤ yn)
+  | .offset xb xo xn, .const yn => do
+    if xn ≤ yn then
+      let finExpr := mkLENat xb (toExpr (yn - xn))
+      let leProof ← mkOfDecideEqTrue (mkLENat xo y)
+      applySimprocConst finExpr ``Nat.Simproc.add_le_le #[xb, xo, y, leProof]
+    else
+      let gtProof ← mkOfDecideEqTrue (mkGTNat xo y)
+      applySimprocConst (mkConst ``False) ``Nat.Simproc.add_le_gt #[xb, xo, y, gtProof]
+  | .const xn, .offset yb yo yn => do
+    if xn ≤ yn then
+      let leProof ← mkOfDecideEqTrue (mkLENat x yo)
+      applySimprocConst (mkConst ``True) ``Nat.Simproc.le_add_le #[x, yb, yo, leProof]
+    else
+      let finExpr := mkLENat (toExpr (xn - yn)) yb
+      let geProof ← mkOfDecideEqTrue (mkGENat yo x)
+      applySimprocConst finExpr ``Nat.Simproc.le_add_ge #[x, yb, yo, geProof]
+  | .offset xb xo xn, .offset yb yo yn => do
+    if xn ≤ yn then
+      let finExpr := mkLENat xb (if xn = yn then yb else mkAddNat yb (toExpr (yn - xn)))
+      let leProof ← mkOfDecideEqTrue (mkLENat xo yo)
+      applySimprocConst finExpr ``Nat.Simproc.add_le_add_le  #[xb, yb, xo, yo, leProof]
+    else
+      let finExpr := mkLENat (mkAddNat xb (toExpr (xn - yn))) yb
+      let geProof ← mkOfDecideEqTrue (mkGENat xo yo)
+      applySimprocConst finExpr ``Nat.Simproc.add_le_add_ge  #[xb, yb, xo, yo, geProof]
+
+builtin_simproc [simp, seval] reduceLeDiff ((_ : Nat) ≤ _) := reduceLTLE ``LE.le 4 false
+
+builtin_simproc [simp, seval] reduceSubDiff ((_ - _ : Nat)) := fun e => do
+  unless e.isAppOfArity ``HSub.hSub 6 do
+    return .continue
+  let p := e.appFn!.appArg!
+  let some pno ← NatOffset.fromExpr? p | return .continue
+  let q := e.appArg!
+  let some qno ← NatOffset.fromExpr? q | return .continue
+  match pno, qno with
+  | .const pn, .const qn =>
+    -- Generate rfl proof  showing (p - q) = pn - qn
+    let finExpr := toExpr (pn - qn)
+    let finProof ← Meta.mkEqRefl finExpr
+    return .done  { expr := finExpr, proof? := finProof, cache := true }
+  | .offset pb po pn, .const n => do
+    if pn ≤ n then
+      let finExpr := if pn = n then pb else mkSubNat pb (toExpr (n - pn))
+      let leProof ← mkOfDecideEqTrue (mkLENat po q)
+      applySimprocConst finExpr ``Nat.Simproc.add_sub_le  #[pb, po, q, leProof]
+    else
+      let finExpr := mkAddNat pb (toExpr (pn - n))
+      let geProof ← mkOfDecideEqTrue (mkGENat po q)
+      applySimprocConst finExpr ``Nat.add_sub_assoc #[po, q, geProof, pb]
+  | .const po, .offset nb no nn => do
+      let finExpr := mkSubNat (toExpr (po - nn)) nb
+      applySimprocConst finExpr ``Nat.Simproc.sub_add_eq_comm #[p, nb, no]
+  | .offset pb po pn, .offset nb no nn => do
+    if pn ≤ nn then
+      let finExpr := mkSubNat pb (if pn = nn then nb else mkAddNat nb (toExpr (nn - pn)))
+      let leProof ← mkOfDecideEqTrue (mkLENat po no)
+      applySimprocConst finExpr ``Nat.Simproc.add_sub_add_le #[pb, nb, po, no, leProof]
+    else
+      let finExpr := mkSubNat (mkAddNat pb (toExpr (pn - nn))) nb
+      let geProof ← mkOfDecideEqTrue (mkGENat po no)
+      applySimprocConst finExpr ``Nat.Simproc.add_sub_add_ge #[pb, nb, po, no, geProof]
+
 end Nat

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

@@ -54,6 +54,10 @@ def foldRawNatLit (e : Expr) : SimpM Expr := do
 def isOfScientificLit (e : Expr) : Bool :=
   e.isAppOfArity ``OfScientific.ofScientific 5 && (e.getArg! 4).isRawNatLit && (e.getArg! 2).isRawNatLit
 
+/-- Return true if `e` is of the form `Char.ofNat n` where `n` is a kernel Nat literals. -/
+def isCharLit (e : Expr) : Bool :=
+  e.isAppOfArity ``Char.ofNat 1 && e.appArg!.isRawNatLit
+
 private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
   matchConst e.getAppFn (fun _ => pure none) fun cinfo _ => do
     match (← getProjectionFnInfo? cinfo.name) with
@@ -436,13 +440,18 @@ Auliliary `dsimproc` for not visiting `OfScientific.ofScientific` application su
 -/
 private def doNotVisitOfScientific : DSimproc := doNotVisit isOfScientificLit ``OfScientific.ofScientific
 
+/--
+Auliliary `dsimproc` for not visiting `Char` literal subterms.
+-/
+private def doNotVisitCharLit : DSimproc := doNotVisit isCharLit ``Char.ofNat
+
 @[export lean_dsimp]
 private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let cfg ← getConfig
   unless cfg.dsimp do
     return e
   let m ← getMethods
-  let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific
+  let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit
   let post := m.dpost >> dsimpReduce
   transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
@@ -562,7 +571,7 @@ def congr (e : Expr) : SimpM Result := do
     congrDefault e
 
 def simpApp (e : Expr) : SimpM Result := do
-  if isOfNatNatLit e || isOfScientificLit e then
+  if isOfNatNatLit e || isOfScientificLit e || isCharLit e then
     -- Recall that we fold "orphan" kernel Nat literals `n` into `OfNat.ofNat n`
     return { expr := e }
   else
@@ -585,9 +594,7 @@ def simpStep (e : Expr) : SimpM Result := do
 
 def cacheResult (e : Expr) (cfg : Config) (r : Result) : SimpM Result := do
   if cfg.memoize && r.cache then
-    let ctx ← readThe Simp.Context
-    let dischargeDepth := ctx.dischargeDepth
-    modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
+    modify fun s => { s with cache := s.cache.insert e r }
   return r
 
 partial def simpLoop (e : Expr) : SimpM Result := withIncRecDepth do
@@ -634,12 +641,7 @@ where
     if cfg.memoize then
       let cache := (← get).cache
       if let some result := cache.find? e then
-        /-
-          If the result was cached at a dischargeDepth > the current one, it may not be valid.
-          See issue #1234
-        -/
-        if result.dischargeDepth ≤ (← readThe Simp.Context).dischargeDepth then
-          return result
+        return result
     trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
     simpLoop e
 

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

@@ -28,7 +28,7 @@ inductive DischargeResult where
   deriving DecidableEq
 
 /--
-Wrapper for invoking `discharge?`. It checks for maximum discharge depth, create trace nodes, and ensure
+Wrapper for invoking `discharge?` method. 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
@@ -44,8 +44,9 @@ def discharge?' (thmId : Origin) (x : Expr) (type : Expr) : SimpM Bool := do
     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.
+      -- We use `withPreservedCache` to ensure the cache is restored after `discharge?`
       let usedTheorems := (← get).usedTheorems
-      match (← discharge? type) with
+      match (← withPreservedCache <| (← getMethods).discharge? type) with
       | some proof =>
         unless (← isDefEq x proof) do
           modify fun s => { s with usedTheorems }
@@ -128,7 +129,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
         We use `.reduceSimpleOnly` because this is how we indexed the discrimination tree.
         See issue #1815
         -/
-        if !(← Expr.acLt rhs e .reduceSimpleOnly) then
+        if !(← acLt rhs e .reduceSimpleOnly) then
           trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, perm rejected {e} ==> {rhs}"
           return none
       trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, {e} ==> {rhs}"

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

@@ -422,7 +422,20 @@ def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM Si
     let mut d := d
     for eqn in eqns do
       d ← SimpTheorems.addConst d eqn
-    if hasSmartUnfoldingDecl (← getEnv) declName then
+    /-
+    Even if a function has equation theorems,
+    we also store it in the `toUnfold` set in the following two cases:
+    1- It was defined by structural recursion and has a smart-unfolding associated declaration.
+    2- It is non-recursive.
+
+    Reason: `unfoldPartialApp := true` or conditional equations may not apply.
+
+    Remark: In the future, we are planning to disable this
+    behavior unless `unfoldPartialApp := true`.
+    Moreover, users will have to use `f.eq_def` if they want to force the definition to be
+    unfolded.
+    -/
+    if hasSmartUnfoldingDecl (← getEnv) declName || !(← isRecursiveDefinition declName) then
       d := d.addDeclToUnfoldCore declName
     return d
   else

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

@@ -21,8 +21,6 @@ structure Result where
   /-- A proof that `$e = $expr`, where the simplified expression is on the RHS.
   If `none`, the proof is assumed to be `refl`. -/
   proof?         : Option Expr := none
-  /-- Save the field `dischargeDepth` at `Simp.Context` because it impacts the simplifier result. -/
-  dischargeDepth : UInt32 := 0
   /-- If `cache := true` the result is cached. -/
   cache          : Bool := true
   deriving Inhabited
@@ -44,7 +42,8 @@ def Result.mkEqSymm (e : Expr) (r : Simp.Result) : MetaM Simp.Result :=
   | none   => return { r with expr := e }
   | some p => return { r with expr := e, proof? := some (← Meta.mkEqSymm p) }
 
-abbrev Cache := ExprMap Result
+-- We use `SExprMap` because we want to discard cached results after a `discharge?`
+abbrev Cache := SExprMap Result
 
 abbrev CongrCache := ExprMap (Option CongrTheorem)
 
@@ -92,7 +91,8 @@ structure Context where
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
   ctx.simpTheorems.isDeclToUnfold declName
 
-abbrev UsedSimps := HashMap Origin Nat
+-- We should use `PHashMap` because we backtrack the contents of `UsedSimps`
+abbrev UsedSimps := PHashMap Origin Nat
 
 structure State where
   cache        : Cache := {}
@@ -254,9 +254,6 @@ def pre (e : Expr) : SimpM Step := do
 def post (e : Expr) : SimpM Step := do
   (← getMethods).post e
 
-def discharge? (e : Expr) : SimpM (Option Expr) := do
-  (← getMethods).discharge? e
-
 @[inline] def getContext : SimpM Context :=
   readThe Context
 
@@ -272,16 +269,26 @@ def getSimpTheorems : SimpM SimpTheoremsArray :=
 def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
   return (← readThe Context).congrTheorems
 
-@[inline] def savingCache (x : SimpM α) : SimpM α := do
+@[inline] def withPreservedCache (x : SimpM α) : SimpM α := do
+  -- Recall that `cache.map₁` should be used linearly but `cache.map₂` is great for copies.
+  let savedMap₂   := (← get).cache.map₂
+  let savedStage₁ := (← get).cache.stage₁
+  modify fun s => { s with cache := s.cache.switch }
+  try x finally modify fun s => { s with cache.map₂ := savedMap₂, cache.stage₁ := savedStage₁ }
+
+/--
+Save current cache, reset it, execute `x`, and then restore original cache.
+-/
+@[inline] def withFreshCache (x : SimpM α) : SimpM α := do
   let cacheSaved := (← get).cache
   modify fun s => { s with cache := {} }
   try x finally modify fun s => { s with cache := cacheSaved }
 
 @[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : SimpM α) : SimpM α := do
-  savingCache <| withTheReader Context (fun ctx => { ctx with simpTheorems := s }) x
+  withFreshCache <| withTheReader Context (fun ctx => { ctx with simpTheorems := s }) x
 
 @[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
-  savingCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
+  withFreshCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
   /-

src/Lean/Meta/WHNF.lean

@@ -342,6 +342,16 @@ inductive ProjReductionKind where
   Recall that `whnfCore` does not perform `delta` reduction (i.e., it will not unfold constant declarations), but `whnf` does.
   -/
   | yesWithDelta
+  /--
+  Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
+  Recall that `whnfAtMostII` is like `whnf` but uses transparency at most `instances`.
+  This option is stronger than `yes`, but weaker than `yesWithDelta`.
+  We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
+  When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
+  we only want to unify negation (and not all other field operations as well).
+  Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
+  -/
+  | yesWithDeltaI
   deriving DecidableEq, Inhabited, Repr
 
 /--
@@ -566,12 +576,6 @@ private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) :=
 /--
 Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
 expand let-expressions, expand assigned meta-variables.
-
-The parameter `deltaAtProj` controls how to reduce projections `s.i`. If `deltaAtProj == true`,
-then delta reduction is used to reduce `s` (i.e., `whnf` is used), otherwise `whnfCore`.
-
-If `simpleReduceOnly`, then `iota` and projection reduction are not performed.
-Note that the value of `deltaAtProj` is irrelevant if `simpleReduceOnly = true`.
 -/
 partial def whnfCore (e : Expr) (config : WhnfCoreConfig := {}): MetaM Expr :=
   go e
@@ -613,11 +617,16 @@ where
                   return e
               | _ => return e
       | .proj _ i c =>
-        if config.proj == .no then return e
-        let c ← if config.proj == .yesWithDelta then whnf c else go c
-        match (← projectCore? c i) with
-        | some e => go e
-        | none => return e
+        let k (c : Expr) := do
+          match (← projectCore? c i) with
+          | some e => go e
+          | none => return e
+        match config.proj with
+        | .no => return e
+        | .yes => k (← go c)
+        | .yesWithDelta => k (← whnf c)
+        -- Remark: If the current transparency setting is `reducible`, we should not increase it to `instances`
+        | .yesWithDeltaI => k (← whnfAtMostI c)
       | _ => unreachable!
 
 /--

src/Lean/Parser/Command.lean

@@ -44,7 +44,6 @@ match against a quotation in a command kind's elaborator). -/
 @[builtin_term_parser low] def quot := leading_parser
   "`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
 
-
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|
   "/-!" >> commentBody >> ppLine
@@ -203,17 +202,17 @@ def «structure»          := leading_parser
 @[builtin_command_parser] def «deriving»     := leading_parser
   "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover ident skip) ", "
 @[builtin_command_parser] def noncomputableSection := leading_parser
-  "noncomputable " >> "section" >> optional (ppSpace >> ident)
+  "noncomputable " >> "section" >> optional (ppSpace >> checkColGt >> ident)
 @[builtin_command_parser] def «section»      := leading_parser
-  "section" >> optional (ppSpace >> ident)
+  "section" >> optional (ppSpace >> checkColGt >> ident)
 @[builtin_command_parser] def «namespace»    := leading_parser
-  "namespace " >> ident
+  "namespace " >> checkColGt >> ident
 @[builtin_command_parser] def «end»          := leading_parser
-  "end" >> optional (ppSpace >> ident)
+  "end" >> optional (ppSpace >> checkColGt >> ident)
 @[builtin_command_parser] def «variable»     := leading_parser
-  "variable" >> many1 (ppSpace >> Term.bracketedBinder)
+  "variable" >> many1 (ppSpace >> checkColGt >> Term.bracketedBinder)
 @[builtin_command_parser] def «universe»     := leading_parser
-  "universe" >> many1 (ppSpace >> ident)
+  "universe" >> many1 (ppSpace >> checkColGt >> ident)
 @[builtin_command_parser] def check          := leading_parser
   "#check " >> termParser
 @[builtin_command_parser] def check_failure  := leading_parser
@@ -236,7 +235,7 @@ def «structure»          := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
 @[builtin_command_parser] def «set_option»   := leading_parser
-  "set_option " >> ident >> ppSpace >> optionValue
+  "set_option " >> identWithPartialTrailingDot >> ppSpace >> optionValue
 def eraseAttr := leading_parser
   "-" >> rawIdent
 @[builtin_command_parser] def «attribute»    := leading_parser
@@ -324,7 +323,7 @@ It makes the given namespaces available in the term `e`.
 It sets the option `opt` to the value `val` in the term `e`.
 -/
 @[builtin_term_parser] def «set_option» := leading_parser:leadPrec
-  "set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> termParser
+  "set_option " >> identWithPartialTrailingDot >> ppSpace >> Command.optionValue >> " in " >> termParser
 end Term
 
 namespace Tactic
@@ -336,7 +335,7 @@ but it opens a namespace only within the tactics `tacs`. -/
 /-- `set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,
 but it sets the option only within the tactics `tacs`. -/
 @[builtin_tactic_parser] def «set_option» := leading_parser:leadPrec
-  "set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> tacticSeq
+  "set_option " >> identWithPartialTrailingDot >> ppSpace >> Command.optionValue >> " in " >> tacticSeq
 end Tactic
 
 end Parser

src/Lean/Parser/Extra.lean

@@ -73,6 +73,13 @@ You can use `TSyntax.getId` to extract the name from the resulting syntax object
 @[run_builtin_parser_attribute_hooks] def ident : Parser :=
   withAntiquot (mkAntiquot "ident" identKind) identNoAntiquot
 
+-- `optional (checkNoWsBefore >> "." >> checkNoWsBefore >> ident)`
+-- can never fully succeed but ensures that the identifier
+-- produces a partial syntax that contains the dot.
+-- The partial syntax is sometimes useful for dot-auto-completion.
+@[run_builtin_parser_attribute_hooks] def identWithPartialTrailingDot :=
+  ident >> optional (checkNoWsBefore >> "." >> checkNoWsBefore >> ident)
+
 -- `ident` and `rawIdent` produce the same syntax tree, so we reuse the antiquotation kind name
 @[run_builtin_parser_attribute_hooks] def rawIdent : Parser :=
   withAntiquot (mkAntiquot "ident" identKind) rawIdentNoAntiquot

src/Lean/Parser/Module.lean

@@ -12,11 +12,7 @@ namespace Parser
 
 namespace Module
 def «prelude»  := leading_parser "prelude"
--- `optional (checkNoWsBefore >> "." >> checkNoWsBefore >> ident)`
--- can never fully succeed but ensures that `import (runtime)? <ident>.`
--- produces a partial syntax that contains the dot.
--- The partial syntax is useful for import dot-auto-completion.
-def «import»   := leading_parser "import " >> optional "runtime" >> ident >> optional (checkNoWsBefore >> "." >> checkNoWsBefore >> ident)
+def «import»   := leading_parser "import " >> optional "runtime" >> identWithPartialTrailingDot
 def header     := leading_parser optional («prelude» >> ppLine) >> many («import» >> ppLine) >> ppLine
 /--
   Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -178,35 +178,6 @@ def annotatePos (pos : Pos) (stx : Term) : Term :=
 def annotateCurPos (stx : Term) : Delab :=
   return annotatePos (← getPos) stx
 
-def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do
-  -- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
-  let suggestion := if suggestion.isAnonymous then `a else suggestion
-  -- We use this small hack to convert identifiers created using `mkAuxFunDiscr` to simple names
-  let suggestion := suggestion.eraseMacroScopes
-  let lctx ← getLCtx
-  if !lctx.usesUserName suggestion then
-    return suggestion
-  else if (← getPPOption getPPSafeShadowing) && !bodyUsesSuggestion lctx suggestion then
-    return suggestion
-  else
-    return lctx.getUnusedName suggestion
-where
-  bodyUsesSuggestion (lctx : LocalContext) (suggestion' : Name) : Bool :=
-    Option.isSome <| body.find? fun
-      | Expr.fvar fvarId =>
-        match lctx.find? fvarId with
-        | none      => false
-        | some decl => decl.userName == suggestion'
-      | _ => false
-
-def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
-  let n ← getUnusedName (← getExpr).bindingName! (← getExpr).bindingBody!
-  let stxN ← annotateCurPos (mkIdent n)
-  withBindingBody n $ d stxN
-
-@[inline] def liftMetaM {α} (x : MetaM α) : DelabM α :=
-  liftM x
-
 def addTermInfo (pos : Pos) (stx : Syntax) (e : Expr) (isBinder : Bool := false) : DelabM Unit := do
   let info := Info.ofTermInfo <| ← mkTermInfo stx e isBinder
   modify fun s => { s with infos := s.infos.insert pos info }
@@ -232,6 +203,62 @@ where
     stx := stx
   }
 
+/--
+Annotates the term with the current expression position and registers `TermInfo`
+to associate the term to the current expression.
+-/
+def annotateTermInfo (stx : Term) : Delab := do
+  let stx ← annotateCurPos stx
+  addTermInfo (← getPos) stx (← getExpr)
+  pure stx
+
+/--
+Modifies the delaborator so that it annotates the resulting term with the current expression
+position and registers `TermInfo` to associate the term to the current expression.
+-/
+def withAnnotateTermInfo (d : Delab) : Delab := do
+  let stx ← d
+  annotateTermInfo stx
+
+def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do
+  -- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
+  let suggestion := if suggestion.isAnonymous then `a else suggestion
+  -- We use this small hack to convert identifiers created using `mkAuxFunDiscr` to simple names
+  let suggestion := suggestion.eraseMacroScopes
+  let lctx ← getLCtx
+  if !lctx.usesUserName suggestion then
+    return suggestion
+  else if (← getPPOption getPPSafeShadowing) && !bodyUsesSuggestion lctx suggestion then
+    return suggestion
+  else
+    return lctx.getUnusedName suggestion
+where
+  bodyUsesSuggestion (lctx : LocalContext) (suggestion' : Name) : Bool :=
+    Option.isSome <| body.find? fun
+      | Expr.fvar fvarId =>
+        match lctx.find? fvarId with
+        | none      => false
+        | some decl => decl.userName == suggestion'
+      | _ => false
+
+/--
+Creates an identifier that is annotated with the term `e`, using a fresh position using the `HoleIterator`.
+-/
+def mkAnnotatedIdent (n : Name) (e : Expr) : DelabM Ident := do
+  let pos ← nextExtraPos
+  let stx : Syntax := annotatePos pos (mkIdent n)
+  addTermInfo pos stx e
+  return ⟨stx⟩
+
+/--
+Enters the body of the current expression, which must be a lambda or forall.
+The binding variable is passed to `d` as `Syntax`, and it is an identifier that has been annotated with the fvar expression
+for the variable.
+-/
+def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
+  let n ← getUnusedName (← getExpr).bindingName! (← getExpr).bindingBody!
+  withBindingBody' n (mkAnnotatedIdent n) (d ·)
+
 inductive OmissionReason
   | deep
   | proof
@@ -315,23 +342,6 @@ def shouldOmitProof (e : Expr) : DelabM Bool := do
 
   return !isShallowExpression (← getPPOption getPPProofsThreshold) e
 
-/--
-Annotates the term with the current expression position and registers `TermInfo`
-to associate the term to the current expression.
--/
-def annotateTermInfo (stx : Term) : Delab := do
-  let stx ← annotateCurPos stx
-  addTermInfo (← getPos) stx (← getExpr)
-  pure stx
-
-/--
-Modifies the delaborator so that it annotates the resulting term with the current expression
-position and registers `TermInfo` to associate the term to the current expression.
--/
-def withAnnotateTermInfo (d : Delab) : Delab := do
-  let stx ← d
-  annotateTermInfo stx
-
 /--
 Delaborates the current expression as `⋯` and attaches `Elab.OmissionInfo`, which influences how the
 subterm omitted by `⋯` is delaborated when hovered over.

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -54,12 +54,16 @@ def delabBVar : Delab := do
 @[builtin_delab mvar]
 def delabMVar : Delab := do
   let Expr.mvar n ← getExpr | unreachable!
-  let mvarDecl ← n.getDecl
-  let n :=
-    match mvarDecl.userName with
-    | Name.anonymous => n.name.replacePrefix `_uniq `m
-    | n => n
-  `(?$(mkIdent n))
+  withTypeAscription (cond := ← getPPOption getPPMVarsWithType) do
+    if ← getPPOption getPPMVars then
+      let mvarDecl ← n.getDecl
+      let n :=
+        match mvarDecl.userName with
+        | .anonymous => n.name.replacePrefix `_uniq `m
+        | n => n
+      `(?$(mkIdent n))
+    else
+      `(?_)
 
 @[builtin_delab sort]
 def delabSort : Delab := do
@@ -670,12 +674,12 @@ def delabLetFun : Delab := whenPPOption getPPNotation <| withOverApp 4 do
   let Expr.lam n _ b _ := e.appArg! | failure
   let n ← getUnusedName n b
   let stxV ← withAppFn <| withAppArg delab
-  let stxB ← withAppArg <| withBindingBody n delab
+  let (stxN, stxB) ← withAppArg <| withBindingBody' n (mkAnnotatedIdent n) fun stxN => return (stxN, ← delab)
   if ← getPPOption getPPLetVarTypes <||> getPPOption getPPAnalysisLetVarType then
     let stxT ← SubExpr.withNaryArg 0 delab
-    `(let_fun $(mkIdent n) : $stxT := $stxV; $stxB)
+    `(let_fun $stxN : $stxT := $stxV; $stxB)
   else
-    `(let_fun $(mkIdent n) := $stxV; $stxB)
+    `(let_fun $stxN := $stxV; $stxB)
 
 @[builtin_delab mdata]
 def delabMData : Delab := do
@@ -847,13 +851,13 @@ def delabLetE : Delab := do
   let Expr.letE n t v b _ ← getExpr | unreachable!
   let n ← getUnusedName n b
   let stxV ← descend v 1 delab
-  let stxB ← withLetDecl n t v fun fvar =>
+  let (stxN, stxB) ← withLetDecl n t v fun fvar => do
     let b := b.instantiate1 fvar
-    descend b 2 delab
+    return (← mkAnnotatedIdent n fvar, ← descend b 2 delab)
   if ← getPPOption getPPLetVarTypes <||> getPPOption getPPAnalysisLetVarType then
     let stxT ← descend t 0 delab
-    `(let $(mkIdent n) : $stxT := $stxV; $stxB)
-  else `(let $(mkIdent n) := $stxV; $stxB)
+    `(let $stxN : $stxT := $stxV; $stxB)
+  else `(let $stxN := $stxV; $stxB)
 
 @[builtin_delab app.Char.ofNat]
 def delabChar : Delab := do

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -79,6 +79,16 @@ register_builtin_option pp.instantiateMVars : Bool := {
   group    := "pp"
   descr    := "(pretty printer) instantiate mvars before delaborating"
 }
+register_builtin_option pp.mvars : Bool := {
+  defValue := true
+  group    := "pp"
+  descr    := "(pretty printer) display names of metavariables when true, and otherwise display them as '?_'"
+}
+register_builtin_option pp.mvars.withType : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) display metavariables with a type ascription"
+}
 register_builtin_option pp.beta : Bool := {
   defValue := false
   group    := "pp"
@@ -235,6 +245,8 @@ def getPPUniverses (o : Options) : Bool := o.get pp.universes.name (getPPAll o)
 def getPPFullNames (o : Options) : Bool := o.get pp.fullNames.name (getPPAll o)
 def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPAll o)
 def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.defValue
+def getPPMVars (o : Options) : Bool := o.get pp.mvars.name pp.mvars.defValue
+def getPPMVarsWithType (o : Options) : Bool := o.get pp.mvars.withType.name pp.mvars.withType.defValue
 def getPPBeta (o : Options) : Bool := o.get pp.beta.name pp.beta.defValue
 def getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue
 def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (pp.proofs.defValue || getPPAll o)

src/Lean/PrettyPrinter/Delaborator/SubExpr.lean

@@ -77,10 +77,24 @@ def withBoundedAppFn (maxArgs : Nat) (xf : m α) : m α := do
 
 def withBindingDomain (x : m α) : m α := do descend (← getExpr).bindingDomain! 0 x
 
-def withBindingBody (n : Name) (x : m α) : m α := do
+/--
+Assumes the `SubExpr` is a lambda or forall.
+1. Creates a local declaration for this binder using the name `n`.
+2. Evaluates `v` using the fvar for the local declaration.
+3. Enters the binding body, and evaluates `x` using this result.
+-/
+def withBindingBody' (n : Name) (v : Expr → m β) (x : β → m α) : m α := do
   let e ← getExpr
-  Meta.withLocalDecl n e.binderInfo e.bindingDomain! fun fvar =>
-    descend (e.bindingBody!.instantiate1 fvar) 1 x
+  Meta.withLocalDecl n e.binderInfo e.bindingDomain! fun fvar => do
+    let b ← v fvar
+    descend (e.bindingBody!.instantiate1 fvar) 1 (x b)
+
+/--
+Assumes the `SubExpr` is a lambda or forall.
+Creates a local declaration for this binder using the name `n`, enters the binding body, and evaluates `x`.
+-/
+def withBindingBody (n : Name) (x : m α) : m α :=
+  withBindingBody' n (fun _ => pure ()) (fun _ => x)
 
 def withProj (x : m α) : m α := do
   let Expr.proj _ _ e ← getExpr | unreachable!
@@ -138,7 +152,10 @@ def HoleIterator.next (iter : HoleIterator) : HoleIterator :=
 
 /-- The positioning scheme guarantees that there will be an infinite number of extra positions
 which are never used by `Expr`s. The `HoleIterator` always points at the next such "hole".
-We use these to attach additional `Elab.Info`. -/
+We use these to attach additional `Elab.Info`.
+
+Note: these positions are incompatible with `Lean.SubExpr.Pos.push` since the iterator
+will eventually yield every child of every returned position. -/
 def nextExtraPos : m Pos := do
   let iter ← getThe HoleIterator
   let pos := iter.toPos

src/Lean/Server/Completion.lean

@@ -659,10 +659,10 @@ private def tacticCompletion (params : CompletionParams) (ctx : ContextInfo) : I
     return some { items := sortCompletionItems items, isIncomplete := true }
 
 private def findCompletionInfoAt?
-  (fileMap  : FileMap)
-  (hoverPos : String.Pos)
-  (infoTree : InfoTree)
-  : Option (HoverInfo × ContextInfo × CompletionInfo) :=
+    (fileMap  : FileMap)
+    (hoverPos : String.Pos)
+    (infoTree : InfoTree)
+    : Option (HoverInfo × ContextInfo × CompletionInfo) :=
   let ⟨hoverLine, _⟩ := fileMap.toPosition hoverPos
   match infoTree.foldInfo (init := none) (choose hoverLine) with
   | some (hoverInfo, ctx, Info.ofCompletionInfo info) =>
@@ -677,7 +677,8 @@ where
       (info      : Info)
       (best?     : Option (HoverInfo × ContextInfo × Info))
       : Option (HoverInfo × ContextInfo × Info) :=
-    if !info.isCompletion then best?
+    if !info.isCompletion then
+      best?
     else if info.occursInside? hoverPos |>.isSome then
       let headPos          := info.pos?.get!
       let ⟨headPosLine, _⟩ := fileMap.toPosition headPos
@@ -695,15 +696,14 @@ where
     else if let some (HoverInfo.inside _, _, _) := best? then
       -- We assume the "inside matches" have precedence over "before ones".
       best?
-    else if let some d := info.occursBefore? hoverPos then
+    else if info.occursDirectlyBefore hoverPos then
       let pos := info.tailPos?.get!
       let ⟨line, _⟩ := fileMap.toPosition pos
       if line != hoverLine then best?
       else match best? with
         | none => (HoverInfo.after, ctx, info)
         | some (_, _, best) =>
-          let dBest := best.occursBefore? hoverPos |>.get!
-          if d < dBest || (d == dBest && info.isSmaller best) then
+          if info.isSmaller best then
             (HoverInfo.after, ctx, info)
           else
             best?

src/Lean/Server/InfoUtils.lean

@@ -166,10 +166,10 @@ def Info.isSmaller (i₁ i₂ : Info) : Bool :=
   | some _, none => true
   | _, _ => false
 
-def Info.occursBefore? (i : Info) (hoverPos : String.Pos) : Option String.Pos := do
-  let tailPos ← i.tailPos?
-  guard (tailPos ≤ hoverPos)
-  return hoverPos - tailPos
+def Info.occursDirectlyBefore (i : Info) (hoverPos : String.Pos) : Bool := Id.run do
+  let some tailPos := i.tailPos?
+    | return false
+  return tailPos == hoverPos
 
 def Info.occursInside? (i : Info) (hoverPos : String.Pos) : Option String.Pos := do
   let headPos ← i.pos?

src/Lean/Server/Watchdog.lean

@@ -1109,7 +1109,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
       capabilities := mkLeanServerCapabilities
       serverInfo?  := some {
         name     := "Lean 4 Server"
-        version? := "0.1.2"
+        version? := "0.2.0"
       }
       : InitializeResult
     }

src/Lean/Util/Profile.lean

@@ -12,7 +12,9 @@ namespace Lean
 register_builtin_option profiler : Bool := {
   defValue := false
   group    := "profiler"
-  descr    := "show execution times of various Lean components"
+  descr    := "show exclusive execution times of various Lean components
+  
+See also `trace.profiler` for an alternative profiling system with structured output."
 }
 
 register_builtin_option profiler.threshold : Nat := {

src/Lean/Widget/InteractiveCode.lean

@@ -81,6 +81,7 @@ def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos :=
     if explicit then
       withOptionAtCurrPos pp.tagAppFns.name true do
       withOptionAtCurrPos pp.explicit.name true do
+      withOptionAtCurrPos pp.mvars.name true do
         delabApp
     else
       withOptionAtCurrPos pp.proofs.name true do

src/kernel/type_checker.cpp

@@ -376,16 +376,8 @@ expr type_checker::whnf_fvar(expr const & e, bool cheap_rec, bool cheap_proj) {
     return e;
 }
 
-/* If `cheap == true`, then we don't perform delta-reduction when reducing major premise. */
-optional<expr> type_checker::reduce_proj(expr const & e, bool cheap_rec, bool cheap_proj) {
-    if (!proj_idx(e).is_small())
-        return none_expr();
-    unsigned idx = proj_idx(e).get_small_value();
-    expr c;
-    if (cheap_proj)
-        c = whnf_core(proj_expr(e), cheap_rec, cheap_proj);
-    else
-        c = whnf(proj_expr(e));
+/* Auxiliary method for `reduce_proj` */
+optional<expr> type_checker::reduce_proj_core(expr c, unsigned idx) {
     if (is_string_lit(c))
         c = string_lit_to_constructor(c);
     buffer<expr> args;
@@ -402,6 +394,19 @@ optional<expr> type_checker::reduce_proj(expr const & e, bool cheap_rec, bool ch
         return none_expr();
 }
 
+/* If `cheap == true`, then we don't perform delta-reduction when reducing major premise. */
+optional<expr> type_checker::reduce_proj(expr const & e, bool cheap_rec, bool cheap_proj) {
+    if (!proj_idx(e).is_small())
+        return none_expr();
+    unsigned idx = proj_idx(e).get_small_value();
+    expr c;
+    if (cheap_proj)
+        c = whnf_core(proj_expr(e), cheap_rec, cheap_proj);
+    else
+        c = whnf(proj_expr(e));
+    return reduce_proj_core(c, idx);
+}
+
 static bool is_let_fvar(local_ctx const & lctx, expr const & e) {
     lean_assert(is_fvar(e));
     if (optional<local_decl> decl = lctx.find_local_decl(e)) {
@@ -983,6 +988,33 @@ lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
     }
 }
 
+/*
+Auxiliary method for checking `t_n.idx =?= s_n.idx`.
+It lazily unfolds `t_n` and `s_n`.
+Recall that the simpler approach used at `Meta.ExprDefEq` cannot be used in the
+kernel since it does not have access to reducibility annotations.
+The approach used here is more complicated, but it is also more powerful.
+*/
+bool type_checker::lazy_delta_proj_reduction(expr & t_n, expr & s_n, nat const & idx) {
+    while (true) {
+        switch (lazy_delta_reduction_step(t_n, s_n)) {
+        case reduction_status::Continue:   break;
+        case reduction_status::DefEqual:   return true;
+        case reduction_status::DefUnknown:
+        case reduction_status::DefDiff:
+            if (idx.is_small()) {
+                unsigned i = idx.get_small_value();
+                if (auto t = reduce_proj_core(t_n, i)) {
+                if (auto s = reduce_proj_core(s_n, i)) {
+                    return is_def_eq_core(*t, *s);
+                }}
+            }
+            return is_def_eq_core(t_n, s_n);
+        }
+    }
+}
+
+
 static expr * g_string_mk = nullptr;
 
 lbool type_checker::try_string_lit_expansion_core(expr const & t, expr const & s) {
@@ -1054,8 +1086,12 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
     if (is_fvar(t_n) && is_fvar(s_n) && fvar_name(t_n) == fvar_name(s_n))
         return true;
 
-    if (is_proj(t_n) && is_proj(s_n) && proj_idx(t_n) == proj_idx(s_n) && is_def_eq(proj_expr(t_n), proj_expr(s_n)))
-        return true;
+    if (is_proj(t_n) && is_proj(s_n) && proj_idx(t_n) == proj_idx(s_n)) {
+        expr t_c = proj_expr(t_n);
+        expr s_c = proj_expr(s_n);
+        if (lazy_delta_proj_reduction(t_c, s_c, proj_idx(t_n)))
+            return true;
+    }
 
     // Invoke `whnf_core` again, but now using `whnf` to reduce projections.
     expr t_n_n = whnf_core(t_n);

src/kernel/type_checker.h

@@ -63,6 +63,7 @@ private:
 
     enum class reduction_status { Continue, DefUnknown, DefEqual, DefDiff };
     optional<expr> reduce_recursor(expr const & e, bool cheap_rec, bool cheap_proj);
+    optional<expr> reduce_proj_core(expr c, unsigned idx);
     optional<expr> reduce_proj(expr const & e, bool cheap_rec, bool cheap_proj);
     expr whnf_fvar(expr const & e, bool cheap_rec, bool cheap_proj);
     optional<constant_info> is_delta(expr const & e) const;
@@ -91,6 +92,7 @@ private:
     void cache_failure(expr const & t, expr const & s);
     reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n);
     lbool lazy_delta_reduction(expr & t_n, expr & s_n);
+    bool lazy_delta_proj_reduction(expr & t_n, expr & s_n, nat const & idx);
     bool is_def_eq_core(expr const & t, expr const & s);
     /** \brief Like \c check, but ignores undefined universes */
     expr check_ignore_undefined_universes(expr const & e);

src/lake/Lake/Build/Imports.lean

@@ -12,18 +12,6 @@ Definitions to support `lake setup-file` builds.
 open System
 namespace Lake
 
-/--
-Construct an `Array` of `Module`s for the workspace-local modules of
-a `List` of import strings.
--/
-def Workspace.processImportList
-(imports : List String) (self : Workspace) : Array Module := Id.run do
-  let mut localImports := #[]
-  for imp in imports do
-    if let some mod := self.findModule? imp.toName then
-      localImports := localImports.push mod
-  return localImports
-
 /--
 Recursively build a set of imported modules and return their build jobs,
 the build jobs of their precompiled modules and the build jobs of said modules'
@@ -45,14 +33,11 @@ def recBuildImports (imports : Array Module)
   return (modJobs, precompileJobs, externJobs)
 
 /--
-Builds the workspace-local modules of list of imports.
-Used by `lake setup-file` to build modules for the Lean server.
-Returns the set of module dynlibs built (so they can be loaded by the server).
-
-Builds only module `.olean` and `.ilean` files if the package is configured
-as "Lean-only". Otherwise, also builds `.c` files.
+Builds an `Array` of module imports. Used by `lake setup-file` to build modules
+for the Lean server and by `lake lean` to build the imports of a file.
+Returns the set of module dynlibs built (so they can be loaded by Lean).
 -/
-def buildImportsAndDeps (imports : List String) : BuildM (Array FilePath) := do
+def buildImportsAndDeps (imports : Array Module) : BuildM (Array FilePath) := do
   let ws ← getWorkspace
   if imports.isEmpty then
     -- build the package's (and its dependencies') `extraDepTarget`
@@ -60,9 +45,8 @@ def buildImportsAndDeps (imports : List String) : BuildM (Array FilePath) := do
     return #[]
   else
     -- build local imports from list
-    let mods := ws.processImportList imports
     let (modJobs, precompileJobs, externLibJobs) ←
-      recBuildImports mods |>.run.run
+      recBuildImports imports |>.run.run
     modJobs.forM (·.await)
     let modLibs ← precompileJobs.mapM (·.await <&> (·.path))
     let externLibs ← externLibJobs.mapM (·.await <&> (·.path))

src/lake/Lake/CLI/Actions.lean

@@ -26,3 +26,15 @@ def uploadRelease (pkg : Package) (tag : String) : LogIO Unit := do
   tar pkg.buildArchive pkg.buildDir pkg.buildArchiveFile
   logInfo s!"Uploading {tag}/{pkg.buildArchive}"
   proc {cmd := "gh", args}
+
+def Package.test (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := {}) : LakeT LogIO UInt32 := do
+  let pkgName := pkg.name.toString (escape := false)
+  if pkg.testRunner.isAnonymous then
+    error s!"{pkgName}: no test runner script or executable"
+  else if let some script := pkg.scripts.find? pkg.testRunner then
+    script.run args
+  else if let some exe := pkg.findLeanExe? pkg.testRunner then
+    let exeFile ← runBuild (exe.build >>= (·.await)) buildConfig
+    env exeFile.toString args.toArray
+  else
+    error s!"{pkgName}: invalid test runner: unknown script or executable `{pkg.testRunner}`"

src/lake/Lake/CLI/Help.lean

@@ -18,8 +18,10 @@ COMMANDS:
   init <name> <temp>    create a Lean package in the current directory
   build <targets>...    build targets
   exe <exe> <args>...   build an exe and run it in Lake's environment
+  test                  run the workspace's test script or executable
   clean                 remove build outputs
   env <cmd> <args>...   execute a command in Lake's environment
+  lean <file>           elaborate a Lean file in Lake's context
   update                update dependencies and save them to the manifest
   upload <tag>          upload build artifacts to a GitHub release
   script                manage and run workspace scripts
@@ -135,6 +137,15 @@ of the same package, the version materialized is undefined.
 
 A bare `lake update` will upgrade all dependencies."
 
+def helpTest :=
+"Run the workspace's test script or executable
+
+USAGE:
+  lake test [-- <args>...]
+
+Looks for a script or executable tagged `@[test_runner]` in the workspace's
+root package and executes it with `args`. "
+
 def helpUpload :=
 "Upload build artifacts to a GitHub release
 
@@ -248,6 +259,17 @@ learn how to specify targets), builds it if it is out of date, and then runs
 it with the given `args` in Lake's environment (see `lake help env` for how
 the environment is set up)."
 
+def helpLean :=
+"Elaborate a Lean file in the context of the Lake workspace
+
+USAGE:
+  lake lean <file> [-- <args>...]
+
+Build the imports of the the given file and then runs `lean` on it using
+the workspace's root package's additional Lean arguments and the given args
+(in that order). The `lean` process is executed in Lake's environment like
+`lake env lean` (see `lake help env` for how the environment is set up)."
+
 def helpTranslateConfig :=
 "Translate a Lake configuration file into a different language
 
@@ -275,6 +297,7 @@ def help : (cmd : String) → String
 | "build"               => helpBuild
 | "update" | "upgrade"  => helpUpdate
 | "upload"              => helpUpload
+| "test"                => helpTest
 | "clean"               => helpClean
 | "script"              => helpScriptCli
 | "scripts"             => helpScriptList
@@ -282,5 +305,6 @@ def help : (cmd : String) → String
 | "serve"               => helpServe
 | "env"                 => helpEnv
 | "exe" | "exec"        => helpExe
+| "lean"                => helpLean
 | "translate-config"    => helpTranslateConfig
 | _                     => usage

src/lake/Lake/CLI/Main.lean

@@ -335,6 +335,20 @@ protected def setupFile : CliM PUnit := do
   let imports ← takeArgs
   setupFile loadConfig filePath imports buildConfig opts.verbosity
 
+protected def test : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let config ← mkLoadConfig opts
+  let ws ← loadWorkspace config
+  noArgsRem do
+  let x := ws.root.test opts.subArgs (mkBuildConfig opts)
+  exit <| ← x.run (mkLakeContext ws) |>.run (MonadLog.io opts.verbosity)
+
+protected def checkTest : CliM PUnit := do
+  processOptions lakeOption
+  let ws ← loadWorkspace ( ← mkLoadConfig (← getThe LakeOptions))
+  noArgsRem do exit <| if ws.root.testRunner.isAnonymous then 1 else 0
+
 protected def clean : CliM PUnit := do
   processOptions lakeOption
   let config ← mkLoadConfig (← getThe LakeOptions)
@@ -391,6 +405,26 @@ protected def exe : CliM PUnit := do
   let exeFile ← ws.runBuild (exe.build >>= (·.await)) <| mkBuildConfig opts
   exit <| ← (env exeFile.toString args.toArray).run <| mkLakeContext ws
 
+protected def lean : CliM PUnit := do
+  processOptions lakeOption
+  let leanFile ← takeArg "Lean file"
+  let opts ← getThe LakeOptions
+  noArgsRem do
+  let ws ← loadWorkspace (← mkLoadConfig opts)
+  let imports ← Lean.parseImports' (← IO.FS.readFile leanFile) leanFile
+  let imports := imports.filterMap (ws.findModule? ·.module)
+  let dynlibs ← ws.runBuild (buildImportsAndDeps imports) (mkBuildConfig opts)
+  let spawnArgs := {
+    args :=
+      #[leanFile] ++ dynlibs.map (s!"--load-dynlib={·}") ++
+      ws.root.moreLeanArgs ++ opts.subArgs
+    cmd := ws.lakeEnv.lean.lean.toString
+    env := ws.augmentedEnvVars
+  }
+  logProcCmd spawnArgs logVerbose
+  let rc ← IO.Process.spawn spawnArgs >>= (·.wait)
+  exit rc
+
 protected def translateConfig : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
@@ -424,6 +458,8 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "resolve-deps"        => lake.resolveDeps
 | "upload"              => lake.upload
 | "setup-file"          => lake.setupFile
+| "test"                => lake.test
+| "check-test"          => lake.checkTest
 | "clean"               => lake.clean
 | "script"              => lake.script
 | "scripts"             => lake.script.list
@@ -431,6 +467,7 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "serve"               => lake.serve
 | "env"                 => lake.env
 | "exe" | "exec"        => lake.exe
+| "lean"                => lake.lean
 | "translate-config"    => lake.translateConfig
 | "self-check"          => lake.selfCheck
 | "help"                => lake.help

src/lake/Lake/CLI/Serve.lean

@@ -34,6 +34,8 @@ def setupFile (loadConfig : LoadConfig) (path : FilePath) (imports : List String
       IO.eprintln s!"Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file."
       exit 1
     let ws ← MainM.runLogIO (loadWorkspace loadConfig) verbosity
+    let imports := imports.foldl (init := #[]) fun imps imp =>
+    if let some mod := ws.findModule? imp.toName then imps.push mod else imps
     let dynlibs ← ws.runBuild (buildImportsAndDeps imports) buildConfig
       |>.run (MonadLog.eio verbosity)
     let paths : LeanPaths := {

src/lake/Lake/CLI/Translate/Lean.lean

@@ -130,10 +130,9 @@ protected def Glob.quote (glob : Glob) : Term := Unhygienic.run do
 
 local instance : Quote Glob := ⟨Glob.quote⟩
 
-@[inline] private def mkConfigAttrs? (defaultTarget : Bool) : Option Attributes :=
-  if defaultTarget then Unhygienic.run `(Term.attributes|@[default_target]) else none
-
-protected def LeanLibConfig.mkSyntax (cfg : LeanLibConfig) (defaultTarget := false) : LeanLibDecl := Unhygienic.run do
+protected def LeanLibConfig.mkSyntax
+  (cfg : LeanLibConfig) (defaultTarget := false)
+: LeanLibDecl := Unhygienic.run do
   let declVal? := mkDeclValWhere? <| Array.empty
     |> addDeclFieldD `srcDir cfg.srcDir "."
     |> addDeclFieldD `roots cfg.roots #[cfg.name]
@@ -142,20 +141,26 @@ protected def LeanLibConfig.mkSyntax (cfg : LeanLibConfig) (defaultTarget := fal
     |> addDeclFieldD `precompileModules cfg.precompileModules false
     |> addDeclFieldD `defaultFacets cfg.defaultFacets #[LeanLib.leanArtsFacet]
     |> cfg.toLeanConfig.addDeclFields
-  let attrs? := mkConfigAttrs? defaultTarget
+  let attrs? ← if defaultTarget then some <$> `(Term.attributes|@[default_target]) else pure none
   `(leanLibDecl|$[$attrs?:attributes]? lean_lib $(mkIdent cfg.name) $[$declVal?]?)
 
-protected def LeanExeConfig.mkSyntax (cfg : LeanExeConfig) (defaultTarget := false) : LeanExeDecl := Unhygienic.run do
+protected def LeanExeConfig.mkSyntax
+  (cfg : LeanExeConfig) (defaultTarget := false) (testRunner := false)
+: LeanExeDecl := Unhygienic.run do
   let declVal? := mkDeclValWhere? <| Array.empty
     |> addDeclFieldD `srcDir cfg.srcDir "."
     |> addDeclFieldD `root cfg.root cfg.name
     |> addDeclFieldD `exeName cfg.exeName (cfg.name.toStringWithSep "-" (escape := false))
     |> addDeclFieldD `supportInterpreter cfg.supportInterpreter false
     |> cfg.toLeanConfig.addDeclFields
-  let attrs? := mkConfigAttrs? defaultTarget
+  let attrs? ← id do
+    let mut attrs := #[]
+    if testRunner then attrs := attrs.push <| ← `(Term.attrInstance|test_runner)
+    if defaultTarget then attrs := attrs.push <| ← `(Term.attrInstance|default_target)
+    if attrs.isEmpty then pure none else some <$> `(Term.attributes|@[$attrs,*])
   `(leanExeDecl|$[$attrs?:attributes]? lean_exe $(mkIdent cfg.name) $[$declVal?]?)
 
-protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl:= Unhygienic.run do
+protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl := Unhygienic.run do
   let opts? := if cfg.opts.isEmpty then none else some <| Unhygienic.run do
     cfg.opts.foldM (init := mkCIdent ``NameMap.empty) fun stx opt val =>
       `($stx |>.insert $(quote opt) $(quote val))
@@ -170,13 +175,14 @@ protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl:= Unhygienic.
 
 /-- Create a Lean module that encodes the declarative configuration of the package. -/
 def Package.mkLeanConfig (pkg : Package) : TSyntax ``module := Unhygienic.run do
-  let pkgConfig := pkg.config.mkSyntax
+  let testRunner := pkg.testRunner
   let defaultTargets := pkg.defaultTargets.foldl NameSet.insert NameSet.empty
+  let pkgConfig := pkg.config.mkSyntax
   let requires := pkg.depConfigs.map (·.mkSyntax)
   let leanLibs := pkg.leanLibConfigs.toArray.map fun cfg =>
     cfg.mkSyntax (defaultTargets.contains cfg.name)
   let leanExes := pkg.leanExeConfigs.toArray.map fun cfg =>
-    cfg.mkSyntax (defaultTargets.contains cfg.name)
+    cfg.mkSyntax (defaultTargets.contains cfg.name) (cfg.name == testRunner)
   `(module|
   import $(mkIdent `Lake)
   open $(mkIdent `System) $(mkIdent `Lake) $(mkIdent `DSL)

src/lake/Lake/CLI/Translate/Toml.lean

@@ -122,6 +122,7 @@ instance : ToToml Dependency := ⟨(toToml ·.toToml)⟩
 /-- Create a TOML table that encodes the declarative configuration of the package. -/
 def Package.mkTomlConfig (pkg : Package) (t : Table := {}) : Table :=
   pkg.config.toToml t
+  |>.insertD `testRunner pkg.testRunner .anonymous
   |>.smartInsert `defaultTargets pkg.defaultTargets
   |>.smartInsert `require pkg.depConfigs
   |>.smartInsert `lean_lib pkg.leanLibConfigs.toArray

src/lake/Lake/Config/Package.lean

@@ -203,6 +203,8 @@ structure Package where
   defaultScripts : Array Script := #[]
   /-- Post-`lake update` hooks for the package. -/
   postUpdateHooks : Array (OpaquePostUpdateHook config.name) := #[]
+  /-- Name of the package's test runner script or executable (if any). -/
+  testRunner : Name := .anonymous
 
 instance : Nonempty Package :=
   have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance

src/lake/Lake/DSL/Attributes.lean

@@ -49,6 +49,15 @@ initialize defaultTargetAttr : OrderedTagAttribute ←
       unless valid do
         throwError "attribute `default_target` can only be used on a target (e.g., `lean_lib`, `lean_exe`)"
 
+initialize testRunnerAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `test_runner "mark a Lake script or executable as the package's test runner"
+    fun name => do
+      let valid ← getEnv <&> fun env =>
+        scriptAttr.hasTag env name ||
+        leanExeAttr.hasTag env name
+      unless valid do
+        throwError "attribute `test_runner` can only be used on a `script` or `lean_exe`"
+
 initialize moduleFacetAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `module_facet "mark a definition as a Lake module facet"
 

src/lake/Lake/Load/Elab.lean

@@ -133,6 +133,7 @@ where
     |>.insert ``externLibAttr
     |>.insert ``targetAttr
     |>.insert ``defaultTargetAttr
+    |>.insert ``testRunnerAttr
     |>.insert ``moduleFacetAttr
     |>.insert ``packageFacetAttr
     |>.insert ``libraryFacetAttr

src/lake/Lake/Load/Main.lean

@@ -160,14 +160,13 @@ def Workspace.updateAndMaterialize
             modifyThe (NameMap PackageEntry) (·.insert entry.name entry)
       if let some oldRelPkgsDir := manifest.packagesDir? then
         let oldPkgsDir := ws.dir / oldRelPkgsDir
-        if oldPkgsDir != ws.pkgsDir && (← oldPkgsDir.pathExists) then
+        if oldRelPkgsDir.normalize != ws.relPkgsDir.normalize && (← oldPkgsDir.pathExists) then
+          logInfo s!"workspace packages directory changed; renaming '{oldPkgsDir}' to '{ws.pkgsDir}'"
           let doRename : IO Unit := do
             createParentDirs ws.pkgsDir
             IO.FS.rename oldPkgsDir ws.pkgsDir
           if let .error e ← doRename.toBaseIO then
-            error <|
-              s!"{rootName}: could not rename packages directory " ++
-              s!"({oldPkgsDir} -> {ws.pkgsDir}): {e}"
+            error s!"could not rename workspace packages directory: {e}"
     | .error (.noFileOrDirectory ..) =>
       logInfo s!"{rootName}: no previous manifest, creating one from scratch"
     | .error e =>

src/lake/Lake/Load/Package.lean

@@ -109,6 +109,14 @@ def Package.loadFromEnv
     | .error e => error e
   let depConfigs ← IO.ofExcept <| packageDepAttr.getAllEntries env |>.mapM fun name =>
     evalConstCheck env opts Dependency ``Dependency name
+  let testRunners := testRunnerAttr.getAllEntries env
+  let testRunner ←
+    if testRunners.size > 1 then
+      error s!"{self.name}: only one script or executable can be tagged `@[test_runner]`"
+    else if h : testRunners.size > 0 then
+      pure (testRunners[0]'h)
+    else
+      pure .anonymous
 
   -- Deprecation warnings
   unless self.config.manifestFile.isNone do
@@ -119,7 +127,7 @@ def Package.loadFromEnv
   -- Fill in the Package
   return {self with
     depConfigs, leanLibConfigs, leanExeConfigs, externLibConfigs
-    opaqueTargetConfigs, defaultTargets, scripts, defaultScripts
+    opaqueTargetConfigs, defaultTargets, scripts, defaultScripts, testRunner
     postUpdateHooks
   }
 

src/lake/Lake/Load/Toml.lean

@@ -259,10 +259,12 @@ def loadTomlConfig (dir relDir relConfigFile : FilePath) : LogIO Package := do
       let leanLibConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_lib #[]
       let leanExeConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_exe #[]
       let defaultTargets ← table.tryDecodeD `defaultTargets #[]
+      let testRunner ← table.tryDecodeD `testRunner .anonymous
       let depConfigs ← table.tryDecodeD `require #[]
       return {
-        dir, relDir, relConfigFile,
-        config, depConfigs, leanLibConfigs, leanExeConfigs, defaultTargets
+        dir, relDir, relConfigFile
+        config, depConfigs, leanLibConfigs, leanExeConfigs
+        defaultTargets, testRunner
       }
     if errs.isEmpty then
       return pkg

src/lake/tests/lean/Lib.lean

@@ -0,0 +1,3 @@
+import Lib.Basic
+
+def libSrc := s!"the library {libName}"

src/lake/tests/lean/Lib/Basic.lean

@@ -0,0 +1 @@
+def libName := "foo"

src/lake/tests/lean/Test.lean

@@ -0,0 +1,6 @@
+import Lib
+
+def main (args : List String) : IO Unit :=
+  IO.println s!"Hello {", ".intercalate args}!"
+
+#eval IO.println s!"Hello from {libSrc}!"

src/lake/tests/lean/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json

src/lake/tests/lean/lakefile.lean

@@ -0,0 +1,7 @@
+import Lake
+open System Lake DSL
+
+package test
+
+lean_lib Lib where
+  precompileModules := true

src/lake/tests/lean/test.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+./clean.sh
+
+$LAKE lean Test.lean -v | grep --color "Hello from the library foo!"
+$LAKE lean Test.lean -- --run Bob | grep --color "Hello Bob!"
+test -f .lake/build/lib/Lib.olean

src/lake/tests/test/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json

src/lake/tests/test/exe.lean

@@ -0,0 +1,7 @@
+import Lake
+open System Lake DSL
+
+package test
+
+@[test_runner]
+lean_exe test

src/lake/tests/test/exe.toml

@@ -0,0 +1,5 @@
+name = "test"
+testRunner = "test"
+
+[[lean_exe]]
+name = "test"

src/lake/tests/test/none.lean

@@ -0,0 +1,4 @@
+import Lake
+open System Lake DSL
+
+package test

src/lake/tests/test/none.toml

@@ -0,0 +1 @@
+name = "test"

src/lake/tests/test/script.lean

@@ -0,0 +1,9 @@
+import Lake
+open System Lake DSL
+
+package test
+
+@[test_runner]
+script test args do
+  IO.println s!"script: {args}"
+  return 0