fix: matcher splitter is code

It have to keep it as a private definition for now.
We currently only support duplicate theorems in different modules.
Splitters are generated on demand, and are also used to write code.

.github/workflows/pr-release.yml

@@ -149,7 +149,6 @@ 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,10 +78,6 @@ 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)

doc/dev/bootstrap.md

@@ -81,8 +81,20 @@ or using Github CLI with
 gh workflow run update-stage0.yml
 ```
 
-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.
+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.
 
 ## Further Bootstrapping Complications
 

src/CMakeLists.txt

@@ -588,10 +588,6 @@ 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,6 +1308,7 @@ 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
@@ -1315,12 +1316,6 @@ 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/Lemmas.lean

@@ -728,7 +728,8 @@ 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, Nat.le_add_left 1 i]
+  simp [cons, cond_eq_if]
+  omega
 
 theorem truncate_succ (x : BitVec w) :
     truncate (i+1) x = cons (getLsb x i) (truncate i x) := by

src/Init/Data/Bool.lean

@@ -220,12 +220,6 @@ 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
@@ -236,11 +230,6 @@ theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
 @[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, Nat.succ.injEq]
+  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [ext_iff]
 
 @[simp] theorem pred_one {n : Nat} :
     Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt one_pos)) = 0 := rfl
@@ -683,7 +683,6 @@ 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,14 +249,12 @@ 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 [Nat.succ_sub_succ_eq_sub, get?_append_right (Nat.lt_succ.1 h₁)]
+| a :: l, _, n+1, h₁ => by rw [cons_append]; simp [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 [Nat.succ.injEq] at h; simp [h, get?_append_right, Nat.succ.injEq]
+  | a::l, i, 0, h => by simp at h; simp [h, get?_append_right]
   | 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,4 +19,3 @@ 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, succ.injEq]; intro h; apply ih h
+  | succ n ih => simp [succ_add]; 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
 
-theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
+@[simp] 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 := (Nat.succ.injEq a b).to_iff
+theorem succ_inj' : succ a = succ b ↔ a = b := ⟨succ.inj, congrArg _⟩
 
 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, succ_sub_succ_eq_sub, ih]
+  | succ k ih => simp [← Nat.add_assoc, 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,7 +9,6 @@ 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
 
@@ -272,7 +271,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 [succ_sub_succ_eq_sub]
+    | 0 => simp
     | n+1 =>
       simp [not_decide_mod_two_eq_one]
       omega
@@ -280,7 +279,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, succ_sub_succ_eq_sub]
+      simp [decide_eq_false]
     | 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.injEq] at h; contradiction
+  | n+1, h => by rw [Nat.succ_add, Nat.succ_inj'] 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 [Nat.succ.injEq]
+  have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp
   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

@@ -1,108 +0,0 @@
-/-
-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,21 +245,12 @@ 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 s.atEnd i then
+  if h : 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
@@ -268,42 +259,9 @@ 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 - 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 _)
+      splitOnAux s sep b (s.next i) 0 r
+termination_by s.endPos.1 - i.1
 
-/--
-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/Prelude.lean

@@ -477,8 +477,6 @@ and `Prod.snd p` respectively. You can also write `p.fst` and `p.snd`.
 For more information: [Constructors with Arguments](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html?highlight=Prod#constructors-with-arguments)
 -/
 structure Prod (α : Type u) (β : Type v) where
-  /-- Constructs a pair from two terms. -/
-  mk ::
   /-- The first projection out of a pair. if `p : α × β` then `p.1 : α`. -/
   fst : α
   /-- The second projection out of a pair. if `p : α × β` then `p.2 : β`. -/

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 pure #[← LLVM.voidPtrType llvmctx] else pure #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
+  let argtys := if delta.isNone then #[← LLVM.voidPtrType llvmctx] else #[← 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 pure (← read).mainDecl.inlineAttr? else pure none
+  let inlineAttr? := if (← read).inheritInlineAttrs then (← read).mainDecl.inlineAttr? else 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,9 +325,6 @@ 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,12 +16,10 @@ private builtin_initialize docStringExt : MapDeclarationExtension String ← mkM
 def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
   builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
 
-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"
+def addDocString [MonadEnv m] (declName : Name) (docString : String) : m Unit :=
   modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
 
-def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
+def addDocString' [Monad 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 (fullRef := fullRef) .. := lval then
-      addDotCompletionInfo fullRef f expectedType?
+    if let LVal.fieldName (ref := fieldStx) (targetStx := targetStx) .. := lval then
+      addDotCompletionInfo targetStx f expectedType? fieldStx
     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 f
+        LVal.fieldName comp comp.getId.getString! none e
       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[3]
+  let options ← Elab.elabSetOption stx[1] stx[2]
   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 pure id else pure <| (← getCurrNamespace) ++ id
+  let id := if stx[1].isNone then id else (← 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[3]
+  let options ← Elab.elabSetOption stx[1] stx[2]
   withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
-    elabTerm stx[5] expectedType?
+    elabTerm stx[4] 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][3]
+      let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
       Command.withScope (fun scope => { scope with opts }) do
-        withSetOptionIn cmd stx[2]
+        withSetOptionIn cmd stx[1]
   else
     cmd stx
 

src/Lean/Elab/Deriving/DecEq.lean

@@ -27,9 +27,8 @@ 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 $sameCtor:term
+           by subst h; exact $(← mkSameCtorRhs todo):term
           else
            isFalse (by intro n; injection n; apply h _; assumption))
       if let some auxFunName := recField then

src/Lean/Elab/Do.lean

@@ -63,9 +63,8 @@ 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
@@ -78,15 +77,12 @@ 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
 
@@ -1325,12 +1321,6 @@ 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) (expectedType? : Option Expr)
+  | dot (termInfo : TermInfo) (field? : Option Syntax) (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/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:3]))
+  addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[0:2]))
   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,7 +704,6 @@ 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
@@ -712,7 +711,7 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
           autoParam? := (← inferType info.fvar).getAutoParamTactic?
           subobject? :=
             if info.kind == StructFieldKind.subobject then
-              match env.find? info.declName with
+              match (← getEnv).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,4 +442,7 @@ 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[3]
+  let options ← Elab.elabSetOption stx[1] stx[2]
   withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
-    evalTactic stx[5]
+    evalTactic stx[4]
 
 @[builtin_tactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do
   let mvarIds ← getGoals

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
-      pure <| getStructureFieldsFlattened (← getEnv) struct (includeSubobjectFields := false)
+    let fields := if flat then
+      getStructureFieldsFlattened (← getEnv) struct (includeSubobjectFields := false)
     else
-      pure <| getStructureFields (← getEnv) struct
+      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,9 +36,7 @@ partial def falseOrByContra (g : MVarId) (useClassical : Option Bool := none) :
   match ty with
   | .const ``False _ => pure g
   | .forallE _ _ _ _
-  | .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
+  | .app (.const ``Not _) _ => falseOrByContra (← g.intro1).2
   | _ =>
     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 <| withTacticInfoContext rhs do
+      let gs' ← mvarId.withContext <| withRef 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. `fullRef` includes the LHS. -/
-  | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (fullRef : Syntax)
+  `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)
 
 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. `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?)
+/-- 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?)
 
 /--
   Main function for elaborating terms.

src/Lean/Expr.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Hashable
 import Lean.Data.KVMap
-import Lean.Data.SMap
 import Lean.Level
 
 namespace Lean
@@ -1390,8 +1389,6 @@ 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
@@ -2022,46 +2019,17 @@ 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 Nat.instHAdd
+  mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHAdd [0]) nat (mkConst ``instAddNat))
 
 private def natSubFn : Expr :=
   let nat := mkConst ``Nat
-  mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) nat nat nat Nat.instHSub
+  mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHSub [0]) nat (mkConst ``instSubNat))
 
 private def natMulFn : Expr :=
   let nat := mkConst ``Nat
-  mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat Nat.instHMul
+  mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHMul [0]) nat (mkConst ``instMulNat))
 
 /-- Given `a : Nat`, returns `Nat.succ a` -/
 def mkNatSucc (a : Expr) : Expr :=
@@ -2080,7 +2048,7 @@ def mkNatMul (a b : Expr) : Expr :=
   mkApp2 natMulFn a b
 
 private def natLEPred : Expr :=
-  mkApp2 (mkConst ``LE.le [0]) (mkConst ``Nat) Nat.instLE
+  mkApp2 (mkConst ``LE.le [0]) (mkConst ``Nat) (mkConst ``instLENat)
 
 /-- 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][3]
+    let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
     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.
 -/
-partial def main (a b : Expr) (mode : ReduceMode := .none) : MetaM Bool := do
+unsafe def main (a b : Expr) (mode : ReduceMode := .none) : MetaM Bool :=
   lt a b
 where
   reduce (e : Expr) : MetaM Expr := do
@@ -66,9 +66,7 @@ where
       | .none => return e
 
   lt (a b : Expr) : MetaM Bool := do
-    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`.
+    if ptrAddrUnsafe a == ptrAddrUnsafe b then
       return false
     -- We ignore metadata
     else if a.isMData then
@@ -86,16 +84,6 @@ 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
@@ -111,7 +99,7 @@ where
       else if aArgs.size > bArgs.size then
         return false
       else
-        let infos ← getParamsInfo aFn aArgs.size
+        let infos := (← getFunInfoNArgs aFn aArgs.size).paramInfo
         for i in [:infos.size] do
           -- We ignore instance implicit arguments during comparison
           if !infos[i]!.isInstImplicit then
@@ -149,7 +137,7 @@ where
     | .proj _ _ e ..    => lt e b
     | .app ..           =>
       a.withApp fun f args => do
-        let infos ← getParamsInfo f args.size
+        let infos := (← getFunInfoNArgs f args.size).paramInfo
         for i in [:infos.size] do
           -- We ignore instance implicit arguments during comparison
           if !infos[i]!.isInstImplicit then
@@ -188,8 +176,7 @@ end
 
 end ACLt
 
-@[inherit_doc ACLt.main]
-def acLt (a b : Expr) (mode : ACLt.ReduceMode := .none) : MetaM Bool :=
-  ACLt.main a b mode
+@[implemented_by ACLt.main, inherit_doc ACLt.main]
+opaque Expr.acLt : Expr → Expr → (mode : ACLt.ReduceMode := .none) → MetaM Bool
 
 end Lean.Meta

src/Lean/Meta/AbstractMVars.lean

@@ -101,10 +101,7 @@ 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
-              pure <| (`x).appendIndexAfter (← get).fvars.size
-            else
-              pure decl.userName
+            let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter (← get).fvars.size else decl.userName
             modify fun s => {
               s with
               emap  := s.emap.insert mvarId fvar,

src/Lean/Meta/Basic.lean

@@ -1444,12 +1444,6 @@ 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,10 +82,8 @@ private partial def mkKey (e : Expr) : CanonM Key := do
     return key
   else
     let key ← match e with
-      | .sort .. | .fvar .. | .bvar .. | .lit .. =>
+      | .sort .. | .fvar .. | .bvar .. | .const .. | .lit .. =>
         pure { e := (← shareCommon e) }
-      | .const n ls =>
-        pure { e := (← shareCommon (.const n (List.replicate ls.length levelZero))) }
       | .mvar .. =>
         -- We instantiate assigned metavariables because the
         -- pretty-printer also instantiates them.

src/Lean/Meta/ExprDefEq.lean

@@ -1872,7 +1872,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
     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
 
-    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
+    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfI` 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

src/Lean/Meta/LazyDiscrTree.lean

@@ -25,6 +25,7 @@ elaborated additional parts of the tree.
 -/
 namespace Lean.Meta.LazyDiscrTree
 
+
 /--
 Discrimination tree key.
 -/
@@ -579,76 +580,41 @@ partial def appendResults (mr : MatchResult α) (a : Array α) : Array α :=
 
 end MatchResult
 
-/-
-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 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
 
 private def getStarResult (root : Lean.HashMap Key TrieIndex) : MatchM α (MatchResult α) :=
   match root.find? .star with
@@ -658,14 +624,11 @@ private def getStarResult (root : Lean.HashMap Key TrieIndex) : MatchM α (Match
     let (vs, _) ← evalNode idx
     pure <| ({} : MatchResult α).push (score := 1) vs
 
-/-
-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 :=
+private def getMatchRoot (r : Lean.HashMap Key TrieIndex) (k : Key) (args : Array Expr)
+    (result : MatchResult α) : MatchM α (MatchResult α) :=
   match r.find? k with
-  | none => cases
-  | some c => cases.push { todo := args, score := 1, c }
+  | none => pure result
+  | some c => getMatchLoop args (score := 1) c result
 
 /--
   Find values that match `e` in `root`.
@@ -674,17 +637,13 @@ 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)
-  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
+  match k with
+  | .star  => return result
+  /- See note about "dep-arrow vs arrow" at `getMatchLoop` -/
+  | .arrow =>
+    getMatchRoot root k args (← getMatchRoot root .other #[] result)
+  | _ =>
+    getMatchRoot root k args result
 
 /--
   Find values that match `e` in `d`.

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

@@ -24,10 +24,8 @@ 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
-            pure refined
-          else
-            pure <| !(← isDefEq unrefinedArgType (← inferType x[0]!))
+          let refined := if refined then refined else
+            !(← 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,16 +54,6 @@ 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
 
 /--
@@ -75,7 +65,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 an offset.
+Similar to `getOffset` but returns `none` if the expression is not syntactically an offset.
 -/
 partial def isOffset? (e : Expr) : OptionT MetaM (Expr × Nat) := do
   let add (a b : Expr) := do
@@ -87,8 +77,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 (← matchesInstance i Nat.instAdd); add a b
-  | HAdd.hAdd _ _ _ i a b => guard (← matchesInstance i Nat.instHAdd); 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
   | _ => 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
-          pure 0
+          0
         else
-          pure <| leavePercentHeartbeats * (← getRemainingHeartbeats) / 100
+          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,7 +5,6 @@ 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
@@ -56,7 +55,11 @@ 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 (. != .)
 
@@ -65,263 +68,4 @@ 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,10 +54,6 @@ 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
@@ -440,18 +436,13 @@ 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 >> doNotVisitCharLit
+  let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific
   let post := m.dpost >> dsimpReduce
   transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
@@ -571,7 +562,7 @@ def congr (e : Expr) : SimpM Result := do
     congrDefault e
 
 def simpApp (e : Expr) : SimpM Result := do
-  if isOfNatNatLit e || isOfScientificLit e || isCharLit e then
+  if isOfNatNatLit e || isOfScientificLit e then
     -- Recall that we fold "orphan" kernel Nat literals `n` into `OfNat.ofNat n`
     return { expr := e }
   else
@@ -594,7 +585,9 @@ def simpStep (e : Expr) : SimpM Result := do
 
 def cacheResult (e : Expr) (cfg : Config) (r : Result) : SimpM Result := do
   if cfg.memoize && r.cache then
-    modify fun s => { s with cache := s.cache.insert e r }
+    let ctx ← readThe Simp.Context
+    let dischargeDepth := ctx.dischargeDepth
+    modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
   return r
 
 partial def simpLoop (e : Expr) : SimpM Result := withIncRecDepth do
@@ -641,7 +634,12 @@ where
     if cfg.memoize then
       let cache := (← get).cache
       if let some result := cache.find? e then
-        return result
+        /-
+          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
     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?` method. It checks for maximum discharge depth, create trace nodes, and ensure
+Wrapper for invoking `discharge?`. It checks for maximum discharge depth, create trace nodes, and ensure
 the generated proof was successfully assigned to `x`.
 -/
 def discharge?' (thmId : Origin) (x : Expr) (type : Expr) : SimpM Bool := do
@@ -44,9 +44,8 @@ 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 (← withPreservedCache <| (← getMethods).discharge? type) with
+      match (← discharge? type) with
       | some proof =>
         unless (← isDefEq x proof) do
           modify fun s => { s with usedTheorems }
@@ -129,7 +128,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 !(← acLt rhs e .reduceSimpleOnly) then
+        if !(← Expr.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/Types.lean

@@ -21,6 +21,8 @@ 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
@@ -42,8 +44,7 @@ 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) }
 
--- We use `SExprMap` because we want to discard cached results after a `discharge?`
-abbrev Cache := SExprMap Result
+abbrev Cache := ExprMap Result
 
 abbrev CongrCache := ExprMap (Option CongrTheorem)
 
@@ -91,8 +92,7 @@ structure Context where
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
   ctx.simpTheorems.isDeclToUnfold declName
 
--- We should use `PHashMap` because we backtrack the contents of `UsedSimps`
-abbrev UsedSimps := PHashMap Origin Nat
+abbrev UsedSimps := HashMap Origin Nat
 
 structure State where
   cache        : Cache := {}
@@ -254,6 +254,9 @@ 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
 
@@ -269,26 +272,16 @@ def getSimpTheorems : SimpM SimpTheoremsArray :=
 def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
   return (← readThe Context).congrTheorems
 
-@[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
+@[inline] def savingCache (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
-  withFreshCache <| withTheReader Context (fun ctx => { ctx with simpTheorems := s }) x
+  savingCache <| withTheReader Context (fun ctx => { ctx with simpTheorems := s }) x
 
 @[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
-  withFreshCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
+  savingCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
   /-

src/Lean/Meta/WHNF.lean

@@ -343,8 +343,8 @@ inductive ProjReductionKind where
   -/
   | 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`.
+  Projections `s.i` are reduced at `whnfCore`, and `whnfI` is used at `s` during the process.
+  Recall that `whnfI` is like `whnf` but uses transparency `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`,
@@ -625,8 +625,7 @@ where
         | .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)
+        | .yesWithDeltaI => k (← whnfI c)
       | _ => unreachable!
 
 /--

src/Lean/Parser/Command.lean

@@ -44,6 +44,7 @@ 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
@@ -235,7 +236,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 " >> identWithPartialTrailingDot >> ppSpace >> optionValue
+  "set_option " >> ident >> ppSpace >> optionValue
 def eraseAttr := leading_parser
   "-" >> rawIdent
 @[builtin_command_parser] def «attribute»    := leading_parser
@@ -323,7 +324,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 " >> identWithPartialTrailingDot >> ppSpace >> Command.optionValue >> " in " >> termParser
+  "set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> termParser
 end Term
 
 namespace Tactic
@@ -335,7 +336,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 " >> identWithPartialTrailingDot >> ppSpace >> Command.optionValue >> " in " >> tacticSeq
+  "set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> tacticSeq
 end Tactic
 
 end Parser

src/Lean/Parser/Extra.lean

@@ -73,13 +73,6 @@ 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,7 +12,11 @@ namespace Parser
 
 namespace Module
 def «prelude»  := leading_parser "prelude"
-def «import»   := leading_parser "import " >> optional "runtime" >> identWithPartialTrailingDot
+-- `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 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/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,8 +677,7 @@ 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
@@ -696,14 +695,15 @@ where
     else if let some (HoverInfo.inside _, _, _) := best? then
       -- We assume the "inside matches" have precedence over "before ones".
       best?
-    else if info.occursDirectlyBefore hoverPos then
+    else if let some d := info.occursBefore? 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) =>
-          if info.isSmaller best then
+          let dBest := best.occursBefore? hoverPos |>.get!
+          if d < dBest || (d == dBest && 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.occursDirectlyBefore (i : Info) (hoverPos : String.Pos) : Bool := Id.run do
-  let some tailPos := i.tailPos?
-    | return false
-  return tailPos == hoverPos
+def Info.occursBefore? (i : Info) (hoverPos : String.Pos) : Option String.Pos := do
+  let tailPos ← i.tailPos?
+  guard (tailPos ≤ hoverPos)
+  return hoverPos - tailPos
 
 def Info.occursInside? (i : Info) (hoverPos : String.Pos) : Option String.Pos := do
   let headPos ← i.pos?

src/Lean/Util/Profile.lean

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