chore: rename List.bind and Array.concatMap to flatMap

fix

src/Init/Core.lean

@@ -1385,7 +1385,6 @@ gen_injective_theorems% Except
 gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
-gen_injective_theorems% BitVec
 
 theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
   fun x => Nat.noConfusion x id
@@ -1865,8 +1864,7 @@ section
 variable {α : Type u}
 variable (r : α → α → Prop)
 
-instance Quotient.decidableEq {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)]
-    : DecidableEq (Quotient s) :=
+instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
   fun (q₁ q₂ : Quotient s) =>
     Quotient.recOnSubsingleton₂ q₁ q₂
       fun a₁ a₂ =>
@@ -1937,6 +1935,15 @@ instance : Subsingleton (Squash α) where
     apply Quot.sound
     trivial
 
+/-! # Relations -/
+
+/--
+`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
+-/
+class Antisymm {α : Sort u} (r : α → α → Prop) : Prop where
+  /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
+  antisymm {a b : α} : r a b → r b a → a = b
+
 namespace Lean
 /-! # Kernel reduction hints -/
 
@@ -2112,14 +2119,4 @@ instance : Commutative Or := ⟨fun _ _ => propext or_comm⟩
 instance : Commutative And := ⟨fun _ _ => propext and_comm⟩
 instance : Commutative Iff := ⟨fun _ _ => propext iff_comm⟩
 
-/--
-`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
--/
-class Antisymm (r : α → α → Prop) : Prop where
-  /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
-  antisymm {a b : α} : r a b → r b a → a = b
-
-@[deprecated Antisymm (since := "2024-10-16"), inherit_doc Antisymm]
-abbrev _root_.Antisymm (r : α → α → Prop) : Prop := Std.Antisymm r
-
 end Std

src/Init/Data/Array.lean

@@ -16,4 +16,3 @@ import Init.Data.Array.Lemmas
 import Init.Data.Array.TakeDrop
 import Init.Data.Array.Bootstrap
 import Init.Data.Array.GetLit
-import Init.Data.Array.MapIdx

src/Init/Data/Array/Basic.lean

@@ -7,7 +7,7 @@ prelude
 import Init.WFTactics
 import Init.Data.Nat.Basic
 import Init.Data.Fin.Basic
-import Init.Data.UInt.BasicAux
+import Init.Data.UInt.Basic
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
@@ -817,15 +817,9 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
 
 /-! ## Auxiliary functions used in metaprogramming.
 
-We do not currently intend to provide verification theorems for these functions.
+We do not intend to provide verification theorems for these functions.
 -/
 
-/- ### reduceOption -/
-
-/-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/
-@[inline] def reduceOption (as : Array (Option α)) : Array α :=
-  as.filterMap id
-
 /-! ### eraseReps -/
 
 /--

src/Init/Data/Array/Lemmas.lean

@@ -12,7 +12,9 @@ import Init.Data.Array.Mem
 import Init.TacticsExtra
 
 /-!
-## Theorems about `Array`.
+## Bootstrapping theorems about arrays
+
+This file contains some theorems about `Array` and `List` needed for `Init.Data.List.Impl`.
 -/
 
 namespace Array
@@ -43,6 +45,16 @@ theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[
   rw [getElem?_eq]
   split <;> simp_all
 
+@[deprecated getElem_eq_getElem_toList (since := "2024-09-25")]
+abbrev getElem_eq_toList_getElem := @getElem_eq_getElem_toList
+
+@[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
+abbrev getElem_eq_data_getElem := @getElem_eq_getElem_toList
+
+@[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
+theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
+  simp
+
 theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (a.push x)[i] = a[i] := by
@@ -65,10 +77,7 @@ namespace List
 
 open Array
 
-/-! ### Lemmas about `List.toArray`.
-
-We prefer to pull `List.toArray` outwards.
--/
+/-! ### Lemmas about `List.toArray`. -/
 
 @[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
@@ -76,11 +85,20 @@ We prefer to pull `List.toArray` outwards.
 
 @[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
 
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
 @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
     a.toArray[i] = a[i]'(by simpa using h) := rfl
 
 @[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
 
+@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
+theorem toArray_concat {as : List α} {x : α} :
+    (as ++ [x]).toArray = as.toArray.push x := by
+  apply ext'
+  simp
+
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
@@ -145,12 +163,20 @@ end List
 
 namespace Array
 
+attribute [simp] uset
+
 @[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
 @[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
 
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
 @[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
 
+@[deprecated length_toList (since := "2024-09-09")]
+abbrev data_length := @length_toList
+
 @[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
 
 @[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
@@ -199,6 +225,9 @@ where
     induction l generalizing arr <;> simp [*]
   simp [H]
 
+@[deprecated toList_map (since := "2024-09-09")]
+abbrev map_data := @toList_map
+
 @[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
   simp only [← length_toList]
   simp
@@ -219,10 +248,21 @@ theorem foldl_toList_eq_flatMap (l : List α) (acc : Array β)
     (l.foldl F acc).toList = acc.toList ++ l.flatMap G := by
   induction l generalizing acc <;> simp [*, List.flatMap]
 
+@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
+abbrev foldl_toList_eq_bind := @foldl_toList_eq_flatMap
+
+@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
+abbrev foldl_data_eq_bind := @foldl_toList_eq_flatMap
+
 theorem foldl_toList_eq_map (l : List α) (acc : Array β) (G : α → β) :
     (l.foldl (fun acc a => acc.push (G a)) acc).toList = acc.toList ++ l.map G := by
   induction l generalizing acc <;> simp [*]
 
+@[deprecated foldl_toList_eq_map (since := "2024-09-09")]
+abbrev foldl_data_eq_map := @foldl_toList_eq_map
+
+theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by simp
+
 theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
     anyM p as start stop = anyM.loop p as (min stop as.size) (Nat.min_le_right ..) start := by
   simp only [anyM, Nat.min_def]; split <;> rfl
@@ -237,12 +277,6 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
 @[simp] theorem not_mem_empty (a : α) : ¬(a ∈ #[]) := by
   simp [mem_def]
 
-/-! # uset -/
-
-attribute [simp] uset
-
-theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by simp
-
 /-! # get -/
 
 @[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
@@ -362,10 +396,6 @@ termination_by n - i
     (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
   getElem_ofFn_go _ _ _ (by simp) (by simp) nofun
 
-theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
-    (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by
-  simp [getElem?_def]
-
 /-- # mkArray -/
 
 @[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
@@ -373,17 +403,19 @@ theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
 
 @[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
 
+@[deprecated toList_mkArray (since := "2024-09-09")]
+abbrev mkArray_data := @toList_mkArray
+
 @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
     (mkArray n v)[i] = v := by simp [Array.getElem_eq_getElem_toList]
 
-theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
-    (mkArray n v)[i]? = if i < n then some v else none := by
-  simp [getElem?_def]
-
 /-- # mem -/
 
 theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
 
+@[deprecated mem_toList (since := "2024-09-09")]
+abbrev mem_data := @mem_toList
+
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
 
 theorem getElem_of_mem {a : α} {as : Array α} :
@@ -393,12 +425,6 @@ theorem getElem_of_mem {a : α} {as : Array α} :
   exists i
   exists hbound
 
-theorem getElem?_of_mem {a : α} {as : Array α} :
-    a ∈ as → ∃ (n : Nat), as[n]? = some a := by
-  intro ha
-  rcases List.getElem?_of_mem ha.val with ⟨i, hi⟩
-  exists i
-
 @[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Array α} :
     (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
   split <;> simp_all [mem_def]
@@ -421,11 +447,14 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
     idx < a.size :=
   hidx
 
-theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
+theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
   erw [Array.mem_def, getElem_eq_getElem_toList]
   apply List.get_mem
 
-theorem getElem_fin_eq_getElem_toList (a : Array α) (i : Fin a.size) : a[i] = a.toList[i] := rfl
+theorem getElem_fin_eq_toList_get (a : Array α) (i : Fin _) : a[i] = a.toList.get i := rfl
+
+@[deprecated getElem_fin_eq_toList_get (since := "2024-09-09")]
+abbrev getElem_fin_eq_data_get := @getElem_fin_eq_toList_get
 
 @[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
   a[i] = a[i.toNat] := rfl
@@ -436,8 +465,26 @@ theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none :
 theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
   simp only [getElem_eq_getElem_toList, List.getElem_mem]
 
-theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get? i := by
-  simp [getElem?_eq_getElem?_toList]
+@[deprecated getElem_mem_toList (since := "2024-09-09")]
+abbrev getElem_mem_data := @getElem_mem_toList
+
+theorem getElem?_eq_toList_getElem? (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg]
+
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
+theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
+
+set_option linter.deprecated false in
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
+abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
+
+set_option linter.deprecated false in
+theorem get?_eq_toList_get? (a : Array α) (i : Nat) : a.get? i = a.toList.get? i :=
+  getElem?_eq_toList_get? ..
+
+@[deprecated get?_eq_toList_get? (since := "2024-09-09")]
+abbrev get?_eq_data_get? := @get?_eq_toList_get?
 
 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
   simp [get!_eq_getD]
@@ -450,7 +497,7 @@ theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < a
   simp [back, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
-  simp [back?, getElem?_eq_getElem?_toList]
+  simp [back?, getElem?_eq_toList_getElem?]
 
 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
 
@@ -481,6 +528,9 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
 
 @[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
 
+@[deprecated toList_set (since := "2024-09-09")]
+abbrev data_set := @toList_set
+
 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
     (a.set i v)[i.1] = v := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
@@ -521,9 +571,12 @@ theorem swap_def (a : Array α) (i j : Fin a.size) :
 @[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
     (a.swap i j).toList = (a.toList.set i (a.get j)).set j (a.get i) := by simp [swap_def]
 
-theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
+@[deprecated toList_swap (since := "2024-09-09")]
+abbrev data_swap := @toList_swap
+
+theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
     if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
-  simp [swap_def, get?_set, ← getElem_fin_eq_getElem_toList]
+  simp [swap_def, get?_set, ← getElem_fin_eq_toList_get]
 
 @[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
     a.swapAt i v = (a[i.1], a.set i v) := rfl
@@ -541,6 +594,9 @@ theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
 
 @[simp] theorem toList_pop (a : Array α) : a.pop.toList = a.toList.dropLast := by simp [pop]
 
+@[deprecated toList_pop (since := "2024-09-09")]
+abbrev data_pop := @toList_pop
+
 @[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
 
 @[simp] theorem pop_push (a : Array α) : (a.push x).pop = a := by simp [pop]
@@ -573,6 +629,9 @@ theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
 
 theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rfl
 
+@[deprecated size_eq_length_toList (since := "2024-09-09")]
+abbrev size_eq_length_data := @size_eq_length_toList
+
 @[simp] theorem size_swap! (a : Array α) (i j) :
     (a.swap! i j).size = a.size := by unfold swap!; split <;> (try split) <;> simp [size_swap]
 
@@ -597,10 +656,14 @@ theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rf
 @[simp] theorem toList_range (n : Nat) : (range n).toList = List.range n := by
   induction n <;> simp_all [range, Nat.fold, flip, List.range_succ]
 
+@[deprecated toList_range (since := "2024-09-09")]
+abbrev data_range := @toList_range
+
 @[simp]
 theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
   simp [getElem_eq_getElem_toList]
 
+set_option linter.deprecated false in
 @[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
   let rec go (as : Array α) (i j hj)
       (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
@@ -613,9 +676,9 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
       · intro k
-        rw [← getElem?_eq_getElem?_toList, getElem?_swap]
+        rw [← getElem?_eq_toList_getElem?, get?_swap]
         simp only [H, getElem_eq_getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
-          getElem?_eq_getElem?_toList]
+          getElem?_eq_toList_getElem?]
         split <;> rename_i h₂
         · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
           exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
@@ -642,6 +705,9 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
         true_and, Nat.not_lt] at h
       rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
 
+@[deprecated toList_reverse (since := "2024-09-30")]
+abbrev reverse_toList := @toList_reverse
+
 /-! ### foldl / foldr -/
 
 @[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
@@ -670,7 +736,7 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
     foldrM f init #[] start stop = return init := by
   simp [foldrM]
 
--- This proof is the pure version of `Array.SatisfiesM_foldlM` in Batteries,
+-- This proof is the pure version of `Array.SatisfiesM_foldlM`,
 -- reproduced to avoid a dependency on `SatisfiesM`.
 theorem foldl_induction
     {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → β}
@@ -686,7 +752,7 @@ theorem foldl_induction
     · next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ H
   simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0
 
--- This proof is the pure version of `Array.SatisfiesM_foldrM` in Batteries,
+-- This proof is the pure version of `Array.SatisfiesM_foldrM`,
 -- reproduced to avoid a dependency on `SatisfiesM`.
 theorem foldr_induction
     {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive as.size init) {f : α → β → β}
@@ -732,6 +798,9 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : A
     toList <$> arr.mapM f = arr.toList.mapM f := by
   simp [mapM_eq_mapM_toList]
 
+@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
+abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
+
 theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
     mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
   unfold mapM.map
@@ -803,11 +872,56 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
   · simp only [getElem_map, get_push, size_map]
     split <;> rfl
 
-@[simp] theorem map_pop {f : α → β} {as : Array α} :
-    as.pop.map f = (as.map f).pop := by
-  ext
-  · simp
-  · simp only [getElem_map, getElem_pop, size_map]
+/-! ### mapIdx -/
+
+-- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
+theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
+    (motive : Nat → Prop) (h0 : motive 0)
+    (p : Fin as.size → β → Prop)
+    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
+    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := by
+  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
+    let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
+    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
+    induction i generalizing j bs with simp [mapIdxM.map]
+    | zero =>
+      have := (Nat.zero_add _).symm.trans h
+      exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
+    | succ i ih =>
+      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
+      · intro i i_lt h'
+        rw [get_push]
+        split
+        · apply h₂
+        · simp only [size_push] at h'
+          obtain rfl : i = j := by omega
+          apply (hs ⟨i, by omega⟩ hm).1
+      · exact (hs ⟨j, by omega⟩ hm).2
+  simp [mapIdx, mapIdxM]; exact go rfl nofun h0
+
+theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
+    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
+    ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
+  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
+
+@[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapIdx f).size = a.size :=
+  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
+
+@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
+  Array.size_mapIdx _ _
+
+@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
+    (h : i < (mapIdx a f).size) :
+    (a.mapIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
+  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
+
+@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
+    (a.mapIdx f)[i]? =
+      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
+  simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
+  split <;> simp_all
 
 /-! ### modify -/
 
@@ -831,6 +945,12 @@ theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
     (as.modify i f)[j] = as[j]'(by simpa using hj) := by
   simp [getElem_modify hj, h]
 
+@[deprecated getElem_modify (since := "2024-08-08")]
+theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
+    (arr.modify x f).get ⟨i, h⟩ =
+    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
+  simp [getElem_modify h]
+
 /-! ### filter -/
 
 @[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
@@ -844,6 +964,9 @@ theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
   induction l with simp
   | cons => split <;> simp [*]
 
+@[deprecated toList_filter (since := "2024-09-09")]
+abbrev filter_data := @toList_filter
+
 @[simp] theorem filter_filter (q) (l : Array α) :
     filter p (filter q l) = filter (fun a => p a && q a) l := by
   apply ext'
@@ -877,6 +1000,9 @@ theorem filter_congr {as bs : Array α} (h : as = bs)
   · simp_all [Id.run, List.filterMap_cons]
     split <;> simp_all
 
+@[deprecated toList_filterMap (since := "2024-09-09")]
+abbrev filterMap_data := @toList_filterMap
+
 @[simp] theorem mem_filterMap {f : α → Option β} {l : Array α} {b : β} :
     b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
   simp only [mem_def, toList_filterMap, List.mem_filterMap]
@@ -894,6 +1020,9 @@ theorem size_empty : (#[] : Array α).size = 0 := rfl
 
 theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
+@[deprecated toList_empty (since := "2024-09-09")]
+abbrev empty_data := @toList_empty
+
 /-! ### append -/
 
 theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
@@ -916,6 +1045,9 @@ theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt :
   conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
   apply List.get_of_eq; rw [toList_append]
 
+@[deprecated getElem_append_left (since := "2024-09-30")]
+abbrev get_append_left := @getElem_append_left
+
 theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
     (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
     (as ++ bs)[i] = bs[i - as.size] := by
@@ -924,6 +1056,9 @@ theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle :
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [toList_append]
 
+@[deprecated getElem_append_right (since := "2024-09-30")]
+abbrev get_append_right := @getElem_append_right
+
 @[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
   apply ext'; simp only [toList_append, toList_empty, List.append_nil]
 
@@ -1166,6 +1301,9 @@ theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
   exact ⟨fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩, fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩⟩
 
+@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
+abbrev any_def := @any_toList
+
 /-! ### all -/
 
 theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
@@ -1205,6 +1343,9 @@ theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all
     rw [← getElem_eq_getElem_toList]
     exact w ⟨r, h⟩
 
+@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
+abbrev all_def := @all_toList
+
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
   simp only [← all_toList, List.all_eq_true, mem_def]
 
@@ -1274,8 +1415,33 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
+@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
+abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
+@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
+abbrev get_extract_loop_lt := @getElem_extract_loop_lt
+@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
+abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
+@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
+abbrev get_extract_loop_ge := @getElem_extract_loop_ge
+@[deprecated getElem_extract_aux (since := "2024-09-30")]
+abbrev get_extract_aux := @getElem_extract_aux
+@[deprecated getElem_extract (since := "2024-09-30")]
+abbrev get_extract := @getElem_extract
+
+@[deprecated getElem_swap_right (since := "2024-09-30")]
+abbrev get_swap_right := @getElem_swap_right
+@[deprecated getElem_swap_left (since := "2024-09-30")]
+abbrev get_swap_left := @getElem_swap_left
+@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
+abbrev get_swap_of_ne := @getElem_swap_of_ne
+@[deprecated getElem_swap (since := "2024-09-30")]
+abbrev get_swap := @getElem_swap
+@[deprecated getElem_swap' (since := "2024-09-30")]
+abbrev get_swap' := @getElem_swap'
+
 end Array
 
+
 open Array
 
 namespace List
@@ -1420,158 +1586,3 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   simp
 
 end List
-
-/-! ### Deprecations -/
-
-namespace List
-
-@[deprecated toArray_toList (since := "2024-09-09")]
-abbrev toArray_data := @toArray_toList
-
-@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
-theorem toArray_concat {as : List α} {x : α} :
-    (as ++ [x]).toArray = as.toArray.push x := by
-  apply ext'
-  simp
-
-end List
-
-namespace Array
-
-@[deprecated getElem_eq_getElem_toList (since := "2024-09-25")]
-abbrev getElem_eq_toList_getElem := @getElem_eq_getElem_toList
-
-@[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
-abbrev getElem_eq_data_getElem := @getElem_eq_getElem_toList
-
-@[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
-theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
-  simp
-
-@[deprecated toArray_toList (since := "2024-09-09")]
-abbrev toArray_data := @toArray_toList
-
-@[deprecated length_toList (since := "2024-09-09")]
-abbrev data_length := @length_toList
-
-@[deprecated toList_map (since := "2024-09-09")]
-abbrev map_data := @toList_map
-
-@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
-abbrev foldl_toList_eq_bind := @foldl_toList_eq_flatMap
-
-@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
-abbrev foldl_data_eq_bind := @foldl_toList_eq_flatMap
-
-@[deprecated foldl_toList_eq_map (since := "2024-09-09")]
-abbrev foldl_data_eq_map := @foldl_toList_eq_map
-
-@[deprecated toList_mkArray (since := "2024-09-09")]
-abbrev mkArray_data := @toList_mkArray
-
-@[deprecated mem_toList (since := "2024-09-09")]
-abbrev mem_data := @mem_toList
-
-@[deprecated getElem_mem (since := "2024-10-17")]
-abbrev getElem?_mem := @getElem_mem
-
-@[deprecated getElem_fin_eq_getElem_toList (since := "2024-10-17")]
-abbrev getElem_fin_eq_toList_get := @getElem_fin_eq_getElem_toList
-
-@[deprecated getElem_fin_eq_getElem_toList (since := "2024-09-09")]
-abbrev getElem_fin_eq_data_get := @getElem_fin_eq_getElem_toList
-
-@[deprecated getElem_mem_toList (since := "2024-09-09")]
-abbrev getElem_mem_data := @getElem_mem_toList
-
-@[deprecated getElem?_eq_getElem?_toList (since := "2024-10-17")]
-abbrev getElem?_eq_toList_getElem? := @getElem?_eq_getElem?_toList
-
-@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
-theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
-
-set_option linter.deprecated false in
-@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
-abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
-
-@[deprecated get?_eq_get?_toList (since := "2024-10-17")]
-abbrev get?_eq_toList_get? := @get?_eq_get?_toList
-
-@[deprecated get?_eq_toList_get? (since := "2024-09-09")]
-abbrev get?_eq_data_get? := @get?_eq_get?_toList
-
-@[deprecated toList_set (since := "2024-09-09")]
-abbrev data_set := @toList_set
-
-@[deprecated toList_swap (since := "2024-09-09")]
-abbrev data_swap := @toList_swap
-
-@[deprecated getElem?_swap (since := "2024-10-17")] abbrev get?_swap := @getElem?_swap
-
-@[deprecated toList_pop (since := "2024-09-09")] abbrev data_pop := @toList_pop
-
-@[deprecated size_eq_length_toList (since := "2024-09-09")]
-abbrev size_eq_length_data := @size_eq_length_toList
-
-@[deprecated toList_range (since := "2024-09-09")]
-abbrev data_range := @toList_range
-
-@[deprecated toList_reverse (since := "2024-09-30")]
-abbrev reverse_toList := @toList_reverse
-
-@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
-abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
-
-@[deprecated getElem_modify (since := "2024-08-08")]
-theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
-    (arr.modify x f).get ⟨i, h⟩ =
-    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
-  simp [getElem_modify h]
-
-@[deprecated toList_filter (since := "2024-09-09")]
-abbrev filter_data := @toList_filter
-
-@[deprecated toList_filterMap (since := "2024-09-09")]
-abbrev filterMap_data := @toList_filterMap
-
-@[deprecated toList_empty (since := "2024-09-09")]
-abbrev empty_data := @toList_empty
-
-@[deprecated getElem_append_left (since := "2024-09-30")]
-abbrev get_append_left := @getElem_append_left
-
-@[deprecated getElem_append_right (since := "2024-09-30")]
-abbrev get_append_right := @getElem_append_right
-
-@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
-abbrev any_def := @any_toList
-
-@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
-abbrev all_def := @all_toList
-
-@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
-abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
-@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
-abbrev get_extract_loop_lt := @getElem_extract_loop_lt
-@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
-abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
-@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
-abbrev get_extract_loop_ge := @getElem_extract_loop_ge
-@[deprecated getElem_extract_aux (since := "2024-09-30")]
-abbrev get_extract_aux := @getElem_extract_aux
-@[deprecated getElem_extract (since := "2024-09-30")]
-abbrev get_extract := @getElem_extract
-
-@[deprecated getElem_swap_right (since := "2024-09-30")]
-abbrev get_swap_right := @getElem_swap_right
-@[deprecated getElem_swap_left (since := "2024-09-30")]
-abbrev get_swap_left := @getElem_swap_left
-@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
-abbrev get_swap_of_ne := @getElem_swap_of_ne
-@[deprecated getElem_swap (since := "2024-09-30")]
-abbrev get_swap := @getElem_swap
-@[deprecated getElem_swap' (since := "2024-09-30")]
-abbrev get_swap' := @getElem_swap'
-
-end Array

src/Init/Data/Array/MapIdx.lean

@@ -1,64 +0,0 @@
-/-
-Copyright (c) 2022 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Kim Morrison
--/
-prelude
-import Init.Data.Array.Lemmas
-import Init.Data.List.MapIdx
-
-namespace Array
-
-
-/-! ### mapIdx -/
-
--- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
-theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
-    (motive : Nat → Prop) (h0 : motive 0)
-    (p : Fin as.size → β → Prop)
-    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
-    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := by
-  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
-    let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
-    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
-    induction i generalizing j bs with simp [mapIdxM.map]
-    | zero =>
-      have := (Nat.zero_add _).symm.trans h
-      exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
-    | succ i ih =>
-      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
-      · intro i i_lt h'
-        rw [get_push]
-        split
-        · apply h₂
-        · simp only [size_push] at h'
-          obtain rfl : i = j := by omega
-          apply (hs ⟨i, by omega⟩ hm).1
-      · exact (hs ⟨j, by omega⟩ hm).2
-  simp [mapIdx, mapIdxM]; exact go rfl nofun h0
-
-theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
-    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
-    ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
-  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
-
-@[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapIdx f).size = a.size :=
-  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
-
-@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
-  Array.size_mapIdx _ _
-
-@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
-    (h : i < (mapIdx a f).size) :
-    (a.mapIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
-  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
-
-@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
-    (a.mapIdx f)[i]? =
-      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
-  simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
-  split <;> simp_all
-
-end Array

src/Init/Data/BitVec/Basic.lean

@@ -8,13 +8,12 @@ import Init.Data.Fin.Basic
 import Init.Data.Nat.Bitwise.Lemmas
 import Init.Data.Nat.Power2
 import Init.Data.Int.Bitwise
-import Init.Data.BitVec.BasicAux
 
 /-!
-We define the basic algebraic structure of bitvectors. We choose the `Fin` representation over
-others for its relative efficiency (Lean has special support for `Nat`),  and the fact that bitwise
-operations on `Fin` are already defined. Some other possible representations are `List Bool`,
-`{ l : List Bool // l.length = w }`, `Fin w → Bool`.
+We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
+(Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
+with `Fin`, and the fact that bitwise operations on `Fin` are already defined. Some other possible
+representations are `List Bool`, `{ l : List Bool // l.length = w }`, `Fin w → Bool`.
 
 We define many of the bitvector operations from the
 [`QF_BV` logic](https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV).
@@ -23,12 +22,60 @@ of SMT-LIBv2.
 
 set_option linter.missingDocs true
 
+/--
+A bitvector of the specified width.
+
+This is represented as the underlying `Nat` number in both the runtime
+and the kernel, inheriting all the special support for `Nat`.
+-/
+structure BitVec (w : Nat) where
+  /-- Construct a `BitVec w` from a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector. -/
+  ofFin ::
+  /-- Interpret a bitvector as a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector. -/
+  toFin : Fin (2^w)
+
+/--
+Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
+-/
+-- We manually derive the `DecidableEq` instances for `BitVec` because
+-- we want to have builtin support for bit-vector literals, and we
+-- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
+def BitVec.decEq (x y : BitVec n) : Decidable (x = y) :=
+  match x, y with
+  | ⟨n⟩, ⟨m⟩ =>
+    if h : n = m then
+      isTrue (h ▸ rfl)
+    else
+      isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h))
+
+instance : DecidableEq (BitVec n) := BitVec.decEq
+
 namespace BitVec
 
 section Nat
 
+/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
+@[match_pattern]
+protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2^n) : BitVec n where
+  toFin := ⟨i, p⟩
+
+/-- The `BitVec` with value `i mod 2^n`. -/
+@[match_pattern]
+protected def ofNat (n : Nat) (i : Nat) : BitVec n where
+  toFin := Fin.ofNat' (2^n) i
+
+instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
 instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
 
+/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
+(zero-cost) wrapper around a `Nat`. -/
+protected def toNat (x : BitVec n) : Nat := x.toFin.val
+
+/-- Return the bound in terms of toNat. -/
+theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
+
 @[deprecated isLt (since := "2024-03-12")]
 theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
 
@@ -191,6 +238,22 @@ end repr_toString
 
 section arithmetic
 
+/--
+Addition for bit vectors. This can be interpreted as either signed or unsigned addition
+modulo `2^n`.
+
+SMT-Lib name: `bvadd`.
+-/
+protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
+instance : Add (BitVec n) := ⟨BitVec.add⟩
+
+/--
+Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
+modulo `2^n`.
+-/
+protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)
+instance : Sub (BitVec n) := ⟨BitVec.sub⟩
+
 /--
 Negation for bit vectors. This can be interpreted as either signed or unsigned negation
 modulo `2^n`.
@@ -324,6 +387,10 @@ SMT-Lib name: `bvult`.
 -/
 protected def ult (x y : BitVec n) : Bool := x.toNat < y.toNat
 
+instance : LT (BitVec n) where lt := (·.toNat < ·.toNat)
+instance (x y : BitVec n) : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.toNat < y.toNat))
+
 /--
 Unsigned less-than-or-equal-to for bit vectors.
 
@@ -331,6 +398,10 @@ SMT-Lib name: `bvule`.
 -/
 protected def ule (x y : BitVec n) : Bool := x.toNat ≤ y.toNat
 
+instance : LE (BitVec n) where le := (·.toNat ≤ ·.toNat)
+instance (x y : BitVec n) : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.toNat ≤ y.toNat))
+
 /--
 Signed less-than for bit vectors.
 

src/Init/Data/BitVec/BasicAux.lean

@@ -1,52 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed
--/
-prelude
-import Init.Data.Fin.Basic
-
-set_option linter.missingDocs true
-
-/-!
-This module exists to provide the very basic `BitVec` definitions required for
-`Init.Data.UInt.BasicAux`.
--/
-
-namespace BitVec
-
-section Nat
-
-/-- The `BitVec` with value `i mod 2^n`. -/
-@[match_pattern]
-protected def ofNat (n : Nat) (i : Nat) : BitVec n where
-  toFin := Fin.ofNat' (2^n) i
-
-instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
-
-/-- Return the bound in terms of toNat. -/
-theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
-
-end Nat
-
-section arithmetic
-
-/--
-Addition for bit vectors. This can be interpreted as either signed or unsigned addition
-modulo `2^n`.
-
-SMT-Lib name: `bvadd`.
--/
-protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
-instance : Add (BitVec n) := ⟨BitVec.add⟩
-
-/--
-Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
-modulo `2^n`.
--/
-protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)
-instance : Sub (BitVec n) := ⟨BitVec.sub⟩
-
-end arithmetic
-
-end BitVec

src/Init/Data/BitVec/Bitblast.lean

@@ -267,21 +267,6 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
 
 /-! ### add -/
 
-theorem getMsbD_add {i : Nat} {i_lt : i < w} {x y : BitVec w} :
-    getMsbD (x + y) i =
-      Bool.xor (getMsbD x i) (Bool.xor (getMsbD y i) (carry (w - 1 - i) x y false)) := by
-  simp [getMsbD, getLsbD_add, i_lt, show w - 1 - i < w by omega]
-
-theorem msb_add {w : Nat} {x y: BitVec w} :
-    (x + y).msb =
-      Bool.xor x.msb (Bool.xor y.msb (carry (w - 1) x y false)) := by
-  simp only [BitVec.msb, BitVec.getMsbD]
-  by_cases h : w ≤ 0
-  · simp [h, show w = 0 by omega]
-  · rw [getLsbD_add (x := x)]
-    simp [show w > 0 by omega]
-    omega
-
 /-- Adding a bitvector to its own complement yields the all ones bitpattern -/
 @[simp] theorem add_not_self (x : BitVec w) : x + ~~~x = allOnes w := by
   rw [add_eq_adc, adc, iunfoldr_replace (fun _ => false) (allOnes w)]
@@ -307,26 +292,6 @@ theorem add_eq_or_of_and_eq_zero {w : Nat} (x y : BitVec w)
       simp_all [hx]
     · by_cases hx : x.getLsbD i <;> simp_all [hx]
 
-/-! ### Sub-/
-
-theorem getLsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
-    (x - y).getLsbD i
-      = (x.getLsbD i ^^ ((~~~y + 1#w).getLsbD i ^^ carry i x (~~~y + 1#w) false)) := by
-  rw [sub_toAdd, BitVec.neg_eq_not_add, getLsbD_add]
-  omega
-
-theorem getMsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
-    (x - y).getMsbD i =
-      (x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1) false)) := by
-  rw [sub_toAdd, neg_eq_not_add, getMsbD_add]
-  · rfl
-  · omega
-
-theorem msb_sub {x y: BitVec w} :
-    (x - y).msb
-      = (x.msb ^^ ((~~~y + 1#w).msb ^^ carry (w - 1 - 0) x (~~~y + 1#w) false)) := by
-  simp [sub_toAdd, BitVec.neg_eq_not_add, msb_add]
-
 /-! ### Negation -/
 
 theorem bit_not_testBit (x : BitVec w) (i : Fin w) :

src/Init/Data/BitVec/Lemmas.lean

@@ -286,19 +286,6 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 
 @[simp] theorem getMsbD_zero : (0#w).getMsbD i = false := by simp [getMsbD]
 
-@[simp] theorem getLsbD_one : (1#w).getLsbD i = (decide (0 < w) && decide (i = 0)) := by
-  simp only [getLsbD, toNat_ofNat, Nat.testBit_mod_two_pow]
-  by_cases h : i = 0
-    <;> simp [h, Nat.testBit_to_div_mod, Nat.div_eq_of_lt]
-
-@[simp] theorem getElem_one (h : i < w) : (1#w)[i] = decide (i = 0) := by
-  simp [← getLsbD_eq_getElem, getLsbD_one, h, show 0 < w by omega]
-
-/-- The msb at index `w-1` is the least significant bit, and is true when the width is nonzero. -/
-@[simp] theorem getMsbD_one : (1#w).getMsbD i = (decide (i = w - 1) && decide (0 < w)) := by
-  simp only [getMsbD]
-  by_cases h : 0 < w <;> by_cases h' : i = w - 1 <;> simp [h, h'] <;> omega
-
 @[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
   Nat.mod_eq_of_lt x.isLt
 
@@ -360,10 +347,6 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
 
-@[simp] theorem msb_one : (1#w).msb = decide (w = 1) := by
-  simp [BitVec.msb, getMsbD_one, ← Bool.decide_and]
-  omega
-
 theorem msb_eq_getLsbD_last (x : BitVec w) :
     x.msb = x.getLsbD (w - 1) := by
   simp only [BitVec.msb, getMsbD]
@@ -2090,11 +2073,6 @@ theorem sub_eq_xor {a b : BitVec 1} : a - b = a ^^^ b := by
   have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
   rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
 
-@[simp]
-theorem sub_eq_self {x : BitVec 1} : -x = x := by
-  have ha : x = 0 ∨ x = 1 := eq_zero_or_eq_one _
-  rcases ha with h | h <;> simp [h]
-
 theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
   rcases w with _ | w
   · apply Subsingleton.elim
@@ -2363,24 +2341,6 @@ theorem toNat_sdiv {x y : BitVec w} : (x.sdiv y).toNat =
   simp only [sdiv_eq, toNat_udiv]
   by_cases h : x.msb <;> by_cases h' : y.msb <;> simp [h, h']
 
-@[simp]
-theorem zero_sdiv {x : BitVec w} : (0#w).sdiv x = 0#w := by
-  simp only [sdiv_eq]
-  rcases x.msb with msb | msb <;> simp
-
-@[simp]
-theorem sdiv_zero {x : BitVec n} : x.sdiv 0#n = 0#n := by
-  simp only [sdiv_eq, msb_zero]
-  rcases x.msb with msb | msb <;> apply eq_of_toNat_eq <;> simp
-
-@[simp]
-theorem sdiv_one {x : BitVec w} : x.sdiv 1#w = x := by
-  simp only [sdiv_eq]
-  · by_cases h : w = 1
-    · subst h
-      rcases x.msb with msb | msb <;> simp
-    · rcases x.msb with msb | msb <;> simp [h]
-
 theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
   have hx : x = 0#1 ∨ x = 1#1 := by bv_omega
   have hy : y = 0#1 ∨ y = 1#1 := by bv_omega
@@ -2389,13 +2349,9 @@ theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
       rfl
 
 @[simp]
-theorem sdiv_self {x : BitVec w} :
-    x.sdiv x = if x == 0#w then 0#w else 1#w := by
-  simp [sdiv_eq]
-  · by_cases h : w = 1
-    · subst h
-      rcases x.msb with msb | msb <;> simp
-    · rcases x.msb with msb | msb <;> simp [h]
+theorem sdiv_zero {x : BitVec n} : x.sdiv 0#n = 0#n := by
+  simp only [sdiv_eq, msb_zero]
+  rcases x.msb with msb | msb <;> apply eq_of_toNat_eq <;> simp
 
 /-! ### smod -/
 
@@ -2697,6 +2653,14 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
   apply eq_of_toNat_eq
   simp
 
+@[simp]
+theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by
+  rw [← twoPow_zero, getLsbD_twoPow]
+
+@[simp]
+theorem getElem_one {w i : Nat} (h : i < w) : (1#w)[i] = decide (i = 0) := by
+  rw [← twoPow_zero, getElem_twoPow]
+
 theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
     x <<< n = x * (BitVec.twoPow w n) := by
   ext i
@@ -2716,6 +2680,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
 @[simp] theorem zero_concat_true : concat 0#w true = 1#(w + 1) := by
   ext
   simp [getLsbD_concat]
+  omega
 
 /- ### setWidth, setWidth, and bitwise operations -/
 
@@ -2756,7 +2721,7 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
   ext i
   simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_ofBool,
     Bool.true_and]
-  by_cases h : ((i : Nat) = 0) <;> simp [h] <;> omega
+  by_cases h : (0 = (i : Nat)) <;> simp [h] <;> omega
 
 @[simp]
 theorem replicate_zero_eq {x : BitVec w} : x.replicate 0 = 0#0 := by

src/Init/Data/Char/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import Init.Data.UInt.BasicAux
+import Init.Data.UInt.Basic
 
 /-- Determines if the given integer is a valid [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).
 
@@ -42,10 +42,8 @@ theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size := by
 
 theorem isValidChar_of_isValidCharNat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNat' n (isValidUInt32 n h)) :=
   match h with
-  | Or.inl h =>
-    Or.inl (UInt32.ofNat'_lt_of_lt _ (by decide) h)
-  | Or.inr ⟨h₁, h₂⟩ =>
-    Or.inr ⟨UInt32.lt_ofNat'_of_lt _ (by decide) h₁, UInt32.ofNat'_lt_of_lt _ (by decide) h₂⟩
+  | Or.inl h        => Or.inl h
+  | Or.inr ⟨h₁, h₂⟩ => Or.inr ⟨h₁, h₂⟩
 
 theorem isValidChar_zero : isValidChar 0 :=
   Or.inl (by decide)
@@ -59,7 +57,7 @@ theorem isValidChar_zero : isValidChar 0 :=
   c.val.toUInt8
 
 /-- The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other. -/
-def ofUInt8 (n : UInt8) : Char := ⟨n.toUInt32, .inl (Nat.lt_trans n.toBitVec.isLt (by decide))⟩
+def ofUInt8 (n : UInt8) : Char := ⟨n.toUInt32, .inl (Nat.lt_trans n.1.2 (by decide))⟩
 
 instance : Inhabited Char where
   default := 'A'

src/Init/Data/Hashable.lean

@@ -51,9 +51,6 @@ instance : Hashable USize where
 instance : Hashable (Fin n) where
   hash v := v.val.toUInt64
 
-instance : Hashable Char where
-  hash c := c.val.toUInt64
-
 instance : Hashable Int where
   hash
     | Int.ofNat n => UInt64.ofNat (2 * n)

src/Init/Data/List/Basic.lean

@@ -558,13 +558,10 @@ def flatten : List (List α) → List α
 
 @[deprecated flatten (since := "2024-10-14"), inherit_doc flatten] abbrev join := @flatten
 
-/-! ### singleton -/
+/-! ### pure -/
 
-/-- `singleton x = [x]`. -/
-@[inline] protected def singleton {α : Type u} (a : α) : List α := [a]
-
-set_option linter.missingDocs false in
-@[deprecated singleton (since := "2024-10-16")] protected abbrev pure := @singleton
+/-- `pure x = [x]` is the `pure` operation of the list monad. -/
+@[inline] protected def pure {α : Type u} (a : α) : List α := [a]
 
 /-! ### flatMap -/
 
@@ -1408,17 +1405,8 @@ def unzip : List (α × β) → List α × List β
 
 /-! ## Ranges and enumeration -/
 
-/-- Sum of a list.
-
-`List.sum [a, b, c] = a + (b + (c + 0))` -/
-def sum {α} [Add α] [Zero α] : List α → α :=
-  foldr (· + ·) 0
-
-@[simp] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
-@[simp] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
-
 /-- Sum of a list of natural numbers. -/
--- We intend to subsequently deprecate this in favor of `List.sum`.
+-- This is not in the `List` namespace as later `List.sum` will be defined polymorphically.
 protected def _root_.Nat.sum (l : List Nat) : Nat := l.foldr (·+·) 0
 
 @[simp] theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl

src/Init/Data/List/BasicAux.lean

@@ -232,8 +232,7 @@ theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.g
     apply Nat.lt_trans ih
     simp_arith
 
-theorem le_antisymm [LT α] [s : Std.Antisymm (¬ · < · : α → α → Prop)]
-    {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
+theorem le_antisymm [LT α] [s : Antisymm (¬ · < · : α → α → Prop)] {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
   match as, bs with
   | [],    []    => rfl
   | [],    _::_ => False.elim <| h₂ (List.lt.nil ..)
@@ -249,8 +248,7 @@ theorem le_antisymm [LT α] [s : Std.Antisymm (¬ · < · : α → α → Prop)]
         have : a = b := s.antisymm hab hba
         simp [this, ih]
 
-instance [LT α] [Std.Antisymm (¬ · < · : α → α → Prop)] :
-    Std.Antisymm (· ≤ · : List α → List α → Prop) where
+instance [LT α] [Antisymm (¬ · < · : α → α → Prop)] : Antisymm (· ≤ · : List α → List α → Prop) where
   antisymm h₁ h₂ := le_antisymm h₁ h₂
 
 end List

src/Init/Data/List/Count.lean

@@ -156,7 +156,7 @@ theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : List α)
   simp (config := { contextual := true }) [Option.getD_eq_iff, Option.isSome_eq_isSome]
 
 @[simp] theorem countP_flatten (l : List (List α)) :
-    countP p l.flatten = (l.map (countP p)).sum := by
+    countP p l.flatten = Nat.sum (l.map (countP p)) := by
   simp only [countP_eq_length_filter, filter_flatten]
   simp [countP_eq_length_filter']
 
@@ -232,7 +232,7 @@ theorem count_singleton (a b : α) : count a [b] = if b == a then 1 else 0 := by
 @[simp] theorem count_append (a : α) : ∀ l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
   countP_append _
 
-theorem count_flatten (a : α) (l : List (List α)) : count a l.flatten = (l.map (count a)).sum := by
+theorem count_flatten (a : α) (l : List (List α)) : count a l.flatten = Nat.sum (l.map (count a)) := by
   simp only [count_eq_countP, countP_flatten, count_eq_countP']
 
 @[deprecated count_flatten (since := "2024-10-14")] abbrev count_join := @count_flatten

src/Init/Data/List/Find.lean

@@ -793,7 +793,7 @@ theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
 theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
     l.flatten.findIdx? p =
       (l.findIdx? (·.any p)).map
-        fun i => ((l.take i).map List.length).sum +
+        fun i => Nat.sum ((l.take i).map List.length) +
           (l[i]?.map fun xs => xs.findIdx p).getD 0 := by
   induction l with
   | nil => simp

src/Init/Data/List/Lemmas.lean

@@ -2070,7 +2070,8 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = concat L b
 
 /-! ### flatten -/
 
-@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = (L.map length).sum := by
+
+@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = Nat.sum (L.map length) := by
   induction L with
   | nil => rfl
   | cons =>

src/Init/Data/List/MinMax.lean

@@ -75,7 +75,7 @@ theorem le_min?_iff [Min α] [LE α]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
 -- and `le_min_iff`.
-theorem min?_eq_some_iff [Min α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
+theorem min?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
     (le_refl : ∀ a : α, a ≤ a)
     (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b)
     (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} :
@@ -146,7 +146,7 @@ theorem max?_le_iff [Max α] [LE α]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`,
 -- and `le_min_iff`.
-theorem max?_eq_some_iff [Max α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
+theorem max?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
     (le_refl : ∀ a : α, a ≤ a)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
     (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :

src/Init/Data/List/Monadic.lean

@@ -99,14 +99,4 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
     funext b
     split <;> simp_all
 
-/-! ### foldlM and foldrM -/
-
-theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :
-    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
-  induction l generalizing g init <;> simp [*]
-
-theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : List β₁)
-    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
-  induction l generalizing g init <;> simp [*]
-
 end List

src/Init/Data/List/Range.lean

@@ -20,6 +20,7 @@ open Nat
 
 /-! ## Ranges and enumeration -/
 
+
 /-! ### range' -/
 
 theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step) n step := by

src/Init/Data/List/Sublist.lean

@@ -976,7 +976,7 @@ theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l :=
   drop_subset _ _ h
 
 theorem drop_suffix_drop_left (l : List α) {m n : Nat} (h : m ≤ n) : drop n l <:+ drop m l := by
-  rw [← Nat.sub_add_cancel h, Nat.add_comm, ← drop_drop]
+  rw [← Nat.sub_add_cancel h, ← drop_drop]
   apply drop_suffix
 
 -- See `Init.Data.List.Nat.TakeDrop` for `take_prefix_take_left`.

src/Init/Data/List/TakeDrop.lean

@@ -97,14 +97,14 @@ theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.
 
 theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := by simp
 
-@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (m + n) l
+@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l
   | m, [] => by simp
   | 0, l => by simp
   | m + 1, a :: l =>
     calc
       drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl
-      _ = drop (m + n) l := drop_drop n m l
-      _ = drop ((m + 1) + n) (a :: l) := by rw [Nat.add_right_comm]; rfl
+      _ = drop (n + m) l := drop_drop n m l
+      _ = drop (n + (m + 1)) (a :: l) := rfl
 
 theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
   | 0, _, _ => by simp
@@ -112,7 +112,7 @@ theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (t
   | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
 
 @[deprecated drop_drop (since := "2024-06-15")]
-theorem drop_add (m n) (l : List α) : drop (m + n) l = drop n (drop m l) := by
+theorem drop_add (m n) (l : List α) : drop (m + n) l = drop m (drop n l) := by
   simp [drop_drop]
 
 @[simp]
@@ -126,7 +126,7 @@ theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) :=
 
 @[simp]
 theorem drop_tail (l : List α) (n : Nat) : l.tail.drop n = l.drop (n + 1) := by
-  rw [Nat.add_comm, ← drop_drop, drop_one]
+  rw [← drop_drop, drop_one]
 
 @[simp]
 theorem drop_eq_nil_iff {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by

src/Init/Data/Nat/Basic.lean

@@ -131,7 +131,7 @@ theorem or_exists_add_one : p 0 ∨ (Exists fun n => p (n + 1)) ↔ Exists p :=
 @[simp] theorem blt_eq : (Nat.blt x y = true) = (x < y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
 
 instance : LawfulBEq Nat where
-  eq_of_beq h := by simpa using h
+  eq_of_beq h := Nat.eq_of_beq_eq_true h
   rfl := by simp [BEq.beq]
 
 theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := by simp
@@ -490,10 +490,10 @@ protected theorem le_antisymm_iff {a b : Nat} : a = b ↔ a ≤ b ∧ b ≤ a :=
             (fun ⟨hle, hge⟩ => Nat.le_antisymm hle hge)
 protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤ a := @Nat.le_antisymm_iff
 
-instance : Std.Antisymm ( . ≤ . : Nat → Nat → Prop) where
+instance : Antisymm ( . ≤ . : Nat → Nat → Prop) where
   antisymm h₁ h₂ := Nat.le_antisymm h₁ h₂
 
-instance : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
+instance : Antisymm (¬ . < . : Nat → Nat → Prop) where
   antisymm h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
 
 protected theorem add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m :=
@@ -796,8 +796,6 @@ theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
   | zero => cases h
   | succ n => simp [Nat.pow_succ]
 
-protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
-
 instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
   ⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pos_pow_of_pos m (pos_of_neZero _))⟩
 

src/Init/Data/Nat/Power2.lean

@@ -8,6 +8,8 @@ import Init.Data.Nat.Linear
 
 namespace Nat
 
+protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
+
 theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
   have : power * 2 = power + power := by simp_arith
   rw [this, Nat.sub_add_eq]

src/Init/Data/OfScientific.lean

@@ -10,10 +10,8 @@ import Init.Data.Nat.Log2
 
 /-- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`).
    Examples:
-   - `1.23` is syntax for `OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)`
-   - `121e100` is syntax for `OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)`
-
-   Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.
+   - `OfScientific.ofScientific 123 true 2`    represents `1.23`
+   - `OfScientific.ofScientific 121 false 100` represents `121e100`
 -/
 class OfScientific (α : Type u) where
   ofScientific (mantissa : Nat) (exponentSign : Bool) (decimalExponent : Nat) : α

src/Init/Data/Option/Attach.lean

@@ -44,7 +44,7 @@ theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
   simp
 
 theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x ∈ o₁, P x} :
-    o₁.attachWith P H = o₂.attachWith P fun _ h => H _ (w ▸ h) := by
+    o₁.attachWith P H = o₂.attachWith P fun x h => H _ (w ▸ h) := by
   subst w
   simp
 
@@ -128,12 +128,12 @@ theorem attach_map {o : Option α} (f : α → β) :
   cases o <;> simp
 
 theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ o.map f → P b} :
-    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
+    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases o <;> simp
 
 theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
-    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun _ h => h) := by
+    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun a h => h) := by
   cases o <;> simp
 
 theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}

src/Init/Data/Prod.lean

@@ -7,8 +7,6 @@ prelude
 import Init.SimpLemmas
 import Init.NotationExtra
 
-namespace Prod
-
 instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
   eq_of_beq {a b} (h : a.1 == b.1 && a.2 == b.2) := by
     cases a; cases b
@@ -16,65 +14,9 @@ instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β)
   rfl {a} := by cases a; simp [BEq.beq, LawfulBEq.rfl]
 
 @[simp]
-protected theorem «forall» {p : α × β → Prop} : (∀ x, p x) ↔ ∀ a b, p (a, b) :=
+protected theorem Prod.forall {p : α × β → Prop} : (∀ x, p x) ↔ ∀ a b, p (a, b) :=
   ⟨fun h a b ↦ h (a, b), fun h ⟨a, b⟩ ↦ h a b⟩
 
 @[simp]
-protected theorem «exists» {p : α × β → Prop} : (∃ x, p x) ↔ ∃ a b, p (a, b) :=
+protected theorem Prod.exists {p : α × β → Prop} : (∃ x, p x) ↔ ∃ a b, p (a, b) :=
   ⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩
-
-@[simp] theorem map_id : Prod.map (@id α) (@id β) = id := rfl
-
-@[simp] theorem map_id' : Prod.map (fun a : α => a) (fun b : β => b) = fun x ↦ x := rfl
-
-/--
-Composing a `Prod.map` with another `Prod.map` is equal to
-a single `Prod.map` of composed functions.
--/
-theorem map_comp_map (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) :
-    Prod.map g g' ∘ Prod.map f f' = Prod.map (g ∘ f) (g' ∘ f') :=
-  rfl
-
-/--
-Composing a `Prod.map` with another `Prod.map` is equal to
-a single `Prod.map` of composed functions, fully applied.
--/
-theorem map_map (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) (x : α × γ) :
-    Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x :=
-  rfl
-
-/-- Swap the factors of a product. `swap (a, b) = (b, a)` -/
-def swap : α × β → β × α := fun p => (p.2, p.1)
-
-@[simp]
-theorem swap_swap : ∀ x : α × β, swap (swap x) = x
-  | ⟨_, _⟩ => rfl
-
-@[simp]
-theorem fst_swap {p : α × β} : (swap p).1 = p.2 :=
-  rfl
-
-@[simp]
-theorem snd_swap {p : α × β} : (swap p).2 = p.1 :=
-  rfl
-
-@[simp]
-theorem swap_prod_mk {a : α} {b : β} : swap (a, b) = (b, a) :=
-  rfl
-
-@[simp]
-theorem swap_swap_eq : swap ∘ swap = @id (α × β) :=
-  funext swap_swap
-
-@[simp]
-theorem swap_inj {p q : α × β} : swap p = swap q ↔ p = q := by
-  cases p; cases q; simp [and_comm]
-
-/--
-For two functions `f` and `g`, the composition of `Prod.map f g` with `Prod.swap`
-is equal to the composition of `Prod.swap` with `Prod.map g f`.
--/
-theorem map_comp_swap (f : α → β) (g : γ → δ) :
-    Prod.map f g ∘ Prod.swap = Prod.swap ∘ Prod.map g f := rfl
-
-end Prod

src/Init/Data/Repr.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.Format.Basic
 import Init.Data.Int.Basic
 import Init.Data.Nat.Div
-import Init.Data.UInt.BasicAux
+import Init.Data.UInt.Basic
 import Init.Control.Id
 open Sum Subtype Nat
 

src/Init/Data/String/Basic.lean

@@ -317,9 +317,6 @@ theorem _root_.Char.utf8Size_le_four (c : Char) : c.utf8Size ≤ 4 := by
 
 @[simp] theorem pos_add_char (p : Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size := rfl
 
-protected theorem Pos.ne_zero_of_lt : {a b : Pos} → a < b → b ≠ 0
-  | _, _, hlt, rfl => Nat.not_lt_zero _ hlt
-
 theorem lt_next (s : String) (i : Pos) : i.1 < (s.next i).1 :=
   Nat.add_lt_add_left (Char.utf8Size_pos _) _
 
@@ -1024,66 +1021,6 @@ instance hasBeq : BEq Substring := ⟨beq⟩
 def sameAs (ss1 ss2 : Substring) : Bool :=
   ss1.startPos == ss2.startPos && ss1 == ss2
 
-/--
-Returns the longest common prefix of two substrings.
-The returned substring will use the same underlying string as `s`.
--/
-def commonPrefix (s t : Substring) : Substring :=
-  { s with stopPos := loop s.startPos t.startPos }
-where
-  /-- Returns the ending position of the common prefix, working up from `spos, tpos`. -/
-  loop spos tpos :=
-    if h : spos < s.stopPos ∧ tpos < t.stopPos then
-      if s.str.get spos == t.str.get tpos then
-        have := Nat.sub_lt_sub_left h.1 (s.str.lt_next spos)
-        loop (s.str.next spos) (t.str.next tpos)
-      else
-        spos
-    else
-      spos
-  termination_by s.stopPos.byteIdx - spos.byteIdx
-
-/--
-Returns the longest common suffix of two substrings.
-The returned substring will use the same underlying string as `s`.
--/
-def commonSuffix (s t : Substring) : Substring :=
-  { s with startPos := loop s.stopPos t.stopPos }
-where
-  /-- Returns the starting position of the common prefix, working down from `spos, tpos`. -/
-  loop spos tpos :=
-    if h : s.startPos < spos ∧ t.startPos < tpos then
-      let spos' := s.str.prev spos
-      let tpos' := t.str.prev tpos
-      if s.str.get spos' == t.str.get tpos' then
-        have : spos' < spos := s.str.prev_lt_of_pos spos (String.Pos.ne_zero_of_lt h.1)
-        loop spos' tpos'
-      else
-        spos
-    else
-      spos
-  termination_by spos.byteIdx
-
-/--
-If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
--/
-def dropPrefix? (s : Substring) (pre : Substring) : Option Substring :=
-  let t := s.commonPrefix pre
-  if t.bsize = pre.bsize then
-    some { s with startPos := t.stopPos }
-  else
-    none
-
-/--
-If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
--/
-def dropSuffix? (s : Substring) (suff : Substring) : Option Substring :=
-  let t := s.commonSuffix suff
-  if t.bsize = suff.bsize then
-    some { s with stopPos := t.startPos }
-  else
-    none
-
 end Substring
 
 namespace String
@@ -1145,28 +1082,6 @@ namespace String
 @[inline] def decapitalize (s : String) :=
   s.set 0 <| s.get 0 |>.toLower
 
-/--
-If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
--/
-def dropPrefix? (s : String) (pre : String) : Option Substring :=
-  s.toSubstring.dropPrefix? pre.toSubstring
-
-/--
-If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
--/
-def dropSuffix? (s : String) (suff : String) : Option Substring :=
-  s.toSubstring.dropSuffix? suff.toSubstring
-
-/-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
-or otherwise return `s`. -/
-def stripPrefix (s : String) (pre : String) : String :=
-  s.dropPrefix? pre |>.map Substring.toString |>.getD s
-
-/-- `s.stripSuffix suff` will remove `suff` from the end of `s` if it occurs there,
-or otherwise return `s`. -/
-def stripSuffix (s : String) (suff : String) : String :=
-  s.dropSuffix? suff |>.map Substring.toString |>.getD s
-
 end String
 
 namespace Char

src/Init/Data/String/Extra.lean

@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.ByteArray
-import Init.Data.UInt.Lemmas
 
 namespace String
 
@@ -21,14 +20,14 @@ def toNat! (s : String) : Nat :=
 def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
   let c ← a[i]?
   if c &&& 0x80 == 0 then
-    some ⟨c.toUInt32, .inl (Nat.lt_trans c.toBitVec.isLt (by decide))⟩
+    some ⟨c.toUInt32, .inl (Nat.lt_trans c.1.2 (by decide))⟩
   else if c &&& 0xe0 == 0xc0 then
     let c1 ← a[i+1]?
     guard (c1 &&& 0xc0 == 0x80)
     let r := ((c &&& 0x1f).toUInt32 <<< 6) ||| (c1 &&& 0x3f).toUInt32
     guard (0x80 ≤ r)
     -- TODO: Prove h from the definition of r once we have the necessary lemmas
-    if h : r < 0xd800 then some ⟨r, .inl (UInt32.toNat_lt_of_lt (by decide) h)⟩ else none
+    if h : r < 0xd800 then some ⟨r, .inl h⟩ else none
   else if c &&& 0xf0 == 0xe0 then
     let c1 ← a[i+1]?
     let c2 ← a[i+2]?
@@ -39,14 +38,7 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
       (c2 &&& 0x3f).toUInt32
     guard (0x800 ≤ r)
     -- TODO: Prove `r < 0x110000` from the definition of r once we have the necessary lemmas
-    if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then
-      have :=
-        match h with
-        | .inl h => Or.inl (UInt32.toNat_lt_of_lt (by decide) h)
-        | .inr h => Or.inr ⟨UInt32.lt_toNat_of_lt (by decide) h.left, UInt32.toNat_lt_of_lt (by decide) h.right⟩
-      some ⟨r, this⟩
-    else
-      none
+    if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then some ⟨r, h⟩ else none
   else if c &&& 0xf8 == 0xf0 then
     let c1 ← a[i+1]?
     let c2 ← a[i+2]?
@@ -58,7 +50,7 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
       ((c2 &&& 0x3f).toUInt32 <<< 6) |||
       (c3 &&& 0x3f).toUInt32
     if h : 0x10000 ≤ r ∧ r < 0x110000 then
-      some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) (UInt32.le_toNat_of_le (by decide) h.left), UInt32.toNat_lt_of_lt (by decide) h.right⟩⟩
+      some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) h.1, h.2⟩⟩
     else none
   else
     none

src/Init/Data/Sum.lean

@@ -4,5 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yury G. Kudryashov
 -/
 prelude
-import Init.Data.Sum.Basic
-import Init.Data.Sum.Lemmas
+import Init.Core
+
+namespace Sum
+
+deriving instance DecidableEq for Sum
+deriving instance BEq for Sum
+
+/-- Check if a sum is `inl` and if so, retrieve its contents. -/
+def getLeft? : α ⊕ β → Option α
+  | inl a => some a
+  | inr _ => none
+
+/-- Check if a sum is `inr` and if so, retrieve its contents. -/
+def getRight? : α ⊕ β → Option β
+  | inr b => some b
+  | inl _ => none
+
+end Sum

src/Init/Data/Sum/Basic.lean

@@ -1,178 +0,0 @@
-/-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Yury G. Kudryashov
--/
-prelude
-import Init.PropLemmas
-
-/-!
-# Disjoint union of types
-
-This file defines basic operations on the the sum type `α ⊕ β`.
-
-`α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.
-
-## Main declarations
-
-* `Sum.isLeft`: Returns whether `x : α ⊕ β` comes from the left component or not.
-* `Sum.isRight`: Returns whether `x : α ⊕ β` comes from the right component or not.
-* `Sum.getLeft`: Retrieves the left content of a `x : α ⊕ β` that is known to come from the left.
-* `Sum.getRight`: Retrieves the right content of `x : α ⊕ β` that is known to come from the right.
-* `Sum.getLeft?`: Retrieves the left content of `x : α ⊕ β` as an option type or returns `none`
-  if it's coming from the right.
-* `Sum.getRight?`: Retrieves the right content of `x : α ⊕ β` as an option type or returns `none`
-  if it's coming from the left.
-* `Sum.map`: Maps `α ⊕ β` to `γ ⊕ δ` component-wise.
-* `Sum.elim`: Nondependent eliminator/induction principle for `α ⊕ β`.
-* `Sum.swap`: Maps `α ⊕ β` to `β ⊕ α` by swapping components.
-* `Sum.LiftRel`: The disjoint union of two relations.
-* `Sum.Lex`: Lexicographic order on `α ⊕ β` induced by a relation on `α` and a relation on `β`.
-
-## Further material
-
-See `Batteries.Data.Sum.Lemmas` for theorems about these definitions.
-
-## Notes
-
-The definition of `Sum` takes values in `Type _`. This effectively forbids `Prop`- valued sum types.
-To this effect, we have `PSum`, which takes value in `Sort _` and carries a more complicated
-universe signature in consequence. The `Prop` version is `Or`.
--/
-
-namespace Sum
-
-deriving instance DecidableEq for Sum
-deriving instance BEq for Sum
-
-section get
-
-/-- Check if a sum is `inl`. -/
-def isLeft : α ⊕ β → Bool
-  | inl _ => true
-  | inr _ => false
-
-/-- Check if a sum is `inr`. -/
-def isRight : α ⊕ β → Bool
-  | inl _ => false
-  | inr _ => true
-
-/-- Retrieve the contents from a sum known to be `inl`.-/
-def getLeft : (ab : α ⊕ β) → ab.isLeft → α
-  | inl a, _ => a
-
-/-- Retrieve the contents from a sum known to be `inr`.-/
-def getRight : (ab : α ⊕ β) → ab.isRight → β
-  | inr b, _ => b
-
-/-- Check if a sum is `inl` and if so, retrieve its contents. -/
-def getLeft? : α ⊕ β → Option α
-  | inl a => some a
-  | inr _ => none
-
-/-- Check if a sum is `inr` and if so, retrieve its contents. -/
-def getRight? : α ⊕ β → Option β
-  | inr b => some b
-  | inl _ => none
-
-@[simp] theorem isLeft_inl : (inl x : α ⊕ β).isLeft = true := rfl
-@[simp] theorem isLeft_inr : (inr x : α ⊕ β).isLeft = false := rfl
-@[simp] theorem isRight_inl : (inl x : α ⊕ β).isRight = false := rfl
-@[simp] theorem isRight_inr : (inr x : α ⊕ β).isRight = true := rfl
-
-@[simp] theorem getLeft_inl (h : (inl x : α ⊕ β).isLeft) : (inl x).getLeft h = x := rfl
-@[simp] theorem getRight_inr (h : (inr x : α ⊕ β).isRight) : (inr x).getRight h = x := rfl
-
-@[simp] theorem getLeft?_inl : (inl x : α ⊕ β).getLeft? = some x := rfl
-@[simp] theorem getLeft?_inr : (inr x : α ⊕ β).getLeft? = none := rfl
-@[simp] theorem getRight?_inl : (inl x : α ⊕ β).getRight? = none := rfl
-@[simp] theorem getRight?_inr : (inr x : α ⊕ β).getRight? = some x := rfl
-
-end get
-
-/-- Define a function on `α ⊕ β` by giving separate definitions on `α` and `β`. -/
-protected def elim {α β γ} (f : α → γ) (g : β → γ) : α ⊕ β → γ :=
-  fun x => Sum.casesOn x f g
-
-@[simp] theorem elim_inl (f : α → γ) (g : β → γ) (x : α) :
-    Sum.elim f g (inl x) = f x := rfl
-
-@[simp] theorem elim_inr (f : α → γ) (g : β → γ) (x : β) :
-    Sum.elim f g (inr x) = g x := rfl
-
-/-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
-protected def map (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β' :=
-  Sum.elim (inl ∘ f) (inr ∘ g)
-
-@[simp] theorem map_inl (f : α → α') (g : β → β') (x : α) : (inl x).map f g = inl (f x) := rfl
-
-@[simp] theorem map_inr (f : α → α') (g : β → β') (x : β) : (inr x).map f g = inr (g x) := rfl
-
-/-- Swap the factors of a sum type -/
-def swap : α ⊕ β → β ⊕ α := Sum.elim inr inl
-
-@[simp] theorem swap_inl : swap (inl x : α ⊕ β) = inr x := rfl
-
-@[simp] theorem swap_inr : swap (inr x : α ⊕ β) = inl x := rfl
-
-section LiftRel
-
-/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
-`α ⊕ β` and `γ ⊕ δ`. -/
-inductive LiftRel (r : α → γ → Prop) (s : β → δ → Prop) : α ⊕ β → γ ⊕ δ → Prop
-  /-- `inl a` and `inl c` are related via `LiftRel r s` if `a` and `c` are related via `r`. -/
-  | protected inl {a c} : r a c → LiftRel r s (inl a) (inl c)
-  /-- `inr b` and `inr d` are related via `LiftRel r s` if `b` and `d` are related via `s`. -/
-  | protected inr {b d} : s b d → LiftRel r s (inr b) (inr d)
-
-@[simp] theorem liftRel_inl_inl : LiftRel r s (inl a) (inl c) ↔ r a c :=
-  ⟨fun h => by cases h; assumption, LiftRel.inl⟩
-
-@[simp] theorem not_liftRel_inl_inr : ¬LiftRel r s (inl a) (inr d) := nofun
-
-@[simp] theorem not_liftRel_inr_inl : ¬LiftRel r s (inr b) (inl c) := nofun
-
-@[simp] theorem liftRel_inr_inr : LiftRel r s (inr b) (inr d) ↔ s b d :=
-  ⟨fun h => by cases h; assumption, LiftRel.inr⟩
-
-instance {r : α → γ → Prop} {s : β → δ → Prop}
-    [∀ a c, Decidable (r a c)] [∀ b d, Decidable (s b d)] :
-    ∀ (ab : α ⊕ β) (cd : γ ⊕ δ), Decidable (LiftRel r s ab cd)
-  | inl _, inl _ => decidable_of_iff' _ liftRel_inl_inl
-  | inl _, inr _ => Decidable.isFalse not_liftRel_inl_inr
-  | inr _, inl _ => Decidable.isFalse not_liftRel_inr_inl
-  | inr _, inr _ => decidable_of_iff' _ liftRel_inr_inr
-
-end LiftRel
-
-section Lex
-
-/-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`, otherwise use the
-respective order on `α` or `β`. -/
-inductive Lex (r : α → α → Prop) (s : β → β → Prop) : α ⊕ β → α ⊕ β → Prop
-  /-- `inl a₁` and `inl a₂` are related via `Lex r s` if `a₁` and `a₂` are related via `r`. -/
-  | protected inl {a₁ a₂} (h : r a₁ a₂) : Lex r s (inl a₁) (inl a₂)
-  /-- `inr b₁` and `inr b₂` are related via `Lex r s` if `b₁` and `b₂` are related via `s`. -/
-  | protected inr {b₁ b₂} (h : s b₁ b₂) : Lex r s (inr b₁) (inr b₂)
-  /-- `inl a` and `inr b` are always related via `Lex r s`. -/
-  | sep (a b) : Lex r s (inl a) (inr b)
-
-attribute [simp] Lex.sep
-
-@[simp] theorem lex_inl_inl : Lex r s (inl a₁) (inl a₂) ↔ r a₁ a₂ :=
-  ⟨fun h => by cases h; assumption, Lex.inl⟩
-
-@[simp] theorem lex_inr_inr : Lex r s (inr b₁) (inr b₂) ↔ s b₁ b₂ :=
-  ⟨fun h => by cases h; assumption, Lex.inr⟩
-
-@[simp] theorem lex_inr_inl : ¬Lex r s (inr b) (inl a) := nofun
-
-instance instDecidableRelSumLex [DecidableRel r] [DecidableRel s] : DecidableRel (Lex r s)
-  | inl _, inl _ => decidable_of_iff' _ lex_inl_inl
-  | inl _, inr _ => Decidable.isTrue (Lex.sep _ _)
-  | inr _, inl _ => Decidable.isFalse lex_inr_inl
-  | inr _, inr _ => decidable_of_iff' _ lex_inr_inr
-
-end Lex
-
-end Sum

src/Init/Data/Sum/Lemmas.lean

@@ -1,251 +0,0 @@
-/-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Yury G. Kudryashov
--/
-prelude
-import Init.Data.Sum.Basic
-import Init.Ext
-
-/-!
-# Disjoint union of types
-
-Theorems about the definitions introduced in `Init.Data.Sum.Basic`.
--/
-
-open Function
-
-namespace Sum
-
-@[simp] protected theorem «forall» {p : α ⊕ β → Prop} :
-    (∀ x, p x) ↔ (∀ a, p (inl a)) ∧ ∀ b, p (inr b) :=
-  ⟨fun h => ⟨fun _ => h _, fun _ => h _⟩, fun ⟨h₁, h₂⟩ => Sum.rec h₁ h₂⟩
-
-@[simp] protected theorem «exists» {p : α ⊕ β → Prop} :
-    (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b) :=
-  ⟨ fun
-    | ⟨inl a, h⟩ => Or.inl ⟨a, h⟩
-    | ⟨inr b, h⟩ => Or.inr ⟨b, h⟩,
-    fun
-    | Or.inl ⟨a, h⟩ => ⟨inl a, h⟩
-    | Or.inr ⟨b, h⟩ => ⟨inr b, h⟩⟩
-
-theorem forall_sum {γ : α ⊕ β → Sort _} (p : (∀ ab, γ ab) → Prop) :
-    (∀ fab, p fab) ↔ (∀ fa fb, p (Sum.rec fa fb)) := by
-  refine ⟨fun h fa fb => h _, fun h fab => ?_⟩
-  have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by
-    apply funext
-    rintro (_ | _) <;> rfl
-  rw [h1]; exact h _ _
-
-section get
-
-@[simp] theorem inl_getLeft : ∀ (x : α ⊕ β) (h : x.isLeft), inl (x.getLeft h) = x
-  | inl _, _ => rfl
-@[simp] theorem inr_getRight : ∀ (x : α ⊕ β) (h : x.isRight), inr (x.getRight h) = x
-  | inr _, _ => rfl
-
-@[simp] theorem getLeft?_eq_none_iff {x : α ⊕ β} : x.getLeft? = none ↔ x.isRight := by
-  cases x <;> simp only [getLeft?, isRight, eq_self_iff_true, reduceCtorEq]
-
-@[simp] theorem getRight?_eq_none_iff {x : α ⊕ β} : x.getRight? = none ↔ x.isLeft := by
-  cases x <;> simp only [getRight?, isLeft, eq_self_iff_true, reduceCtorEq]
-
-theorem eq_left_getLeft_of_isLeft : ∀ {x : α ⊕ β} (h : x.isLeft), x = inl (x.getLeft h)
-  | inl _, _ => rfl
-
-@[simp] theorem getLeft_eq_iff (h : x.isLeft) : x.getLeft h = a ↔ x = inl a := by
-  cases x <;> simp at h ⊢
-
-theorem eq_right_getRight_of_isRight : ∀ {x : α ⊕ β} (h : x.isRight), x = inr (x.getRight h)
-  | inr _, _ => rfl
-
-@[simp] theorem getRight_eq_iff (h : x.isRight) : x.getRight h = b ↔ x = inr b := by
-  cases x <;> simp at h ⊢
-
-@[simp] theorem getLeft?_eq_some_iff : x.getLeft? = some a ↔ x = inl a := by
-  cases x <;> simp only [getLeft?, Option.some.injEq, inl.injEq, reduceCtorEq]
-
-@[simp] theorem getRight?_eq_some_iff : x.getRight? = some b ↔ x = inr b := by
-  cases x <;> simp only [getRight?, Option.some.injEq, inr.injEq, reduceCtorEq]
-
-@[simp] theorem bnot_isLeft (x : α ⊕ β) : !x.isLeft = x.isRight := by cases x <;> rfl
-
-@[simp] theorem isLeft_eq_false {x : α ⊕ β} : x.isLeft = false ↔ x.isRight := by cases x <;> simp
-
-theorem not_isLeft {x : α ⊕ β} : ¬x.isLeft ↔ x.isRight := by simp
-
-@[simp] theorem bnot_isRight (x : α ⊕ β) : !x.isRight = x.isLeft := by cases x <;> rfl
-
-@[simp] theorem isRight_eq_false {x : α ⊕ β} : x.isRight = false ↔ x.isLeft := by cases x <;> simp
-
-theorem not_isRight {x : α ⊕ β} : ¬x.isRight ↔ x.isLeft := by simp
-
-theorem isLeft_iff : x.isLeft ↔ ∃ y, x = Sum.inl y := by cases x <;> simp
-
-theorem isRight_iff : x.isRight ↔ ∃ y, x = Sum.inr y := by cases x <;> simp
-
-end get
-
-theorem inl.inj_iff : (inl a : α ⊕ β) = inl b ↔ a = b := ⟨inl.inj, congrArg _⟩
-
-theorem inr.inj_iff : (inr a : α ⊕ β) = inr b ↔ a = b := ⟨inr.inj, congrArg _⟩
-
-theorem inl_ne_inr : inl a ≠ inr b := nofun
-
-theorem inr_ne_inl : inr b ≠ inl a := nofun
-
-/-! ### `Sum.elim` -/
-
-@[simp] theorem elim_comp_inl (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inl = f :=
-  rfl
-
-@[simp] theorem elim_comp_inr (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inr = g :=
-  rfl
-
-@[simp] theorem elim_inl_inr : @Sum.elim α β _ inl inr = id :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-theorem comp_elim (f : γ → δ) (g : α → γ) (h : β → γ) :
-    f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h) :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-@[simp] theorem elim_comp_inl_inr (f : α ⊕ β → γ) :
-    Sum.elim (f ∘ inl) (f ∘ inr) = f :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-theorem elim_eq_iff {u u' : α → γ} {v v' : β → γ} :
-    Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v' := by
-  simp [funext_iff]
-
-/-! ### `Sum.map` -/
-
-@[simp] theorem map_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
-    ∀ x : Sum α β, (x.map f g).map f' g' = x.map (f' ∘ f) (g' ∘ g)
-  | inl _ => rfl
-  | inr _ => rfl
-
-@[simp] theorem map_comp_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
-    Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g) :=
-  funext <| map_map f' g' f g
-
-@[simp] theorem map_id_id : Sum.map (@id α) (@id β) = id :=
-  funext fun x => Sum.recOn x (fun _ => rfl) fun _ => rfl
-
-theorem elim_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} {x} :
-    Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x := by
-  cases x <;> rfl
-
-theorem elim_comp_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} :
-    Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) :=
-  funext fun _ => elim_map
-
-@[simp] theorem isLeft_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    isLeft (x.map f g) = isLeft x := by
-  cases x <;> rfl
-
-@[simp] theorem isRight_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    isRight (x.map f g) = isRight x := by
-  cases x <;> rfl
-
-@[simp] theorem getLeft?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    (x.map f g).getLeft? = x.getLeft?.map f := by
-  cases x <;> rfl
-
-@[simp] theorem getRight?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    (x.map f g).getRight? = x.getRight?.map g := by cases x <;> rfl
-
-/-! ### `Sum.swap` -/
-
-@[simp] theorem swap_swap (x : α ⊕ β) : swap (swap x) = x := by cases x <;> rfl
-
-@[simp] theorem swap_swap_eq : swap ∘ swap = @id (α ⊕ β) := funext <| swap_swap
-
-@[simp] theorem isLeft_swap (x : α ⊕ β) : x.swap.isLeft = x.isRight := by cases x <;> rfl
-
-@[simp] theorem isRight_swap (x : α ⊕ β) : x.swap.isRight = x.isLeft := by cases x <;> rfl
-
-@[simp] theorem getLeft?_swap (x : α ⊕ β) : x.swap.getLeft? = x.getRight? := by cases x <;> rfl
-
-@[simp] theorem getRight?_swap (x : α ⊕ β) : x.swap.getRight? = x.getLeft? := by cases x <;> rfl
-
-section LiftRel
-
-theorem LiftRel.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b)
-  (h : LiftRel r₁ s₁ x y) : LiftRel r₂ s₂ x y := by
-  cases h
-  · exact LiftRel.inl (hr _ _ ‹_›)
-  · exact LiftRel.inr (hs _ _ ‹_›)
-
-theorem LiftRel.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : LiftRel r₁ s x y) :
-    LiftRel r₂ s x y :=
-  (h.mono hr) fun _ _ => id
-
-theorem LiftRel.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : LiftRel r s₁ x y) :
-    LiftRel r s₂ x y :=
-  h.mono (fun _ _ => id) hs
-
-protected theorem LiftRel.swap (h : LiftRel r s x y) : LiftRel s r x.swap y.swap := by
-  cases h
-  · exact LiftRel.inr ‹_›
-  · exact LiftRel.inl ‹_›
-
-@[simp] theorem liftRel_swap_iff : LiftRel s r x.swap y.swap ↔ LiftRel r s x y :=
-  ⟨fun h => by rw [← swap_swap x, ← swap_swap y]; exact h.swap, LiftRel.swap⟩
-
-end LiftRel
-
-section Lex
-
-protected theorem LiftRel.lex {a b : α ⊕ β} (h : LiftRel r s a b) : Lex r s a b := by
-  cases h
-  · exact Lex.inl ‹_›
-  · exact Lex.inr ‹_›
-
-theorem liftRel_subrelation_lex : Subrelation (LiftRel r s) (Lex r s) := LiftRel.lex
-
-theorem Lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r₁ s₁ x y) :
-    Lex r₂ s₂ x y := by
-  cases h
-  · exact Lex.inl (hr _ _ ‹_›)
-  · exact Lex.inr (hs _ _ ‹_›)
-  · exact Lex.sep _ _
-
-theorem Lex.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : Lex r₁ s x y) : Lex r₂ s x y :=
-  (h.mono hr) fun _ _ => id
-
-theorem Lex.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r s₁ x y) : Lex r s₂ x y :=
-  h.mono (fun _ _ => id) hs
-
-theorem lex_acc_inl (aca : Acc r a) : Acc (Lex r s) (inl a) := by
-  induction aca with
-  | intro _ _ IH =>
-    constructor
-    intro y h
-    cases h with
-    | inl h' => exact IH _ h'
-
-theorem lex_acc_inr (aca : ∀ a, Acc (Lex r s) (inl a)) {b} (acb : Acc s b) :
-    Acc (Lex r s) (inr b) := by
-  induction acb with
-  | intro _ _ IH =>
-    constructor
-    intro y h
-    cases h with
-    | inr h' => exact IH _ h'
-    | sep => exact aca _
-
-theorem lex_wf (ha : WellFounded r) (hb : WellFounded s) : WellFounded (Lex r s) :=
-  have aca : ∀ a, Acc (Lex r s) (inl a) := fun a => lex_acc_inl (ha.apply a)
-  ⟨fun x => Sum.recOn x aca fun b => lex_acc_inr aca (hb.apply b)⟩
-
-end Lex
-
-theorem elim_const_const (c : γ) :
-    Sum.elim (const _ c : α → γ) (const _ c : β → γ) = const _ c := by
-  apply funext
-  rintro (_ | _) <;> rfl
-
-@[simp] theorem elim_lam_const_lam_const (c : γ) :
-    Sum.elim (fun _ : α => c) (fun _ : β => c) = fun _ => c :=
-  Sum.elim_const_const c

src/Init/Data/ToString/Basic.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.String.Basic
-import Init.Data.UInt.BasicAux
+import Init.Data.UInt.Basic
 import Init.Data.Nat.Div
 import Init.Data.Repr
 import Init.Data.Int.Basic

src/Init/Data/UInt.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Init.Data.UInt.BasicAux
 import Init.Data.UInt.Basic
 import Init.Data.UInt.Log2
 import Init.Data.UInt.Lemmas

src/Init/Data/UInt/Basic.lean

@@ -4,50 +4,52 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.UInt.BasicAux
-import Init.Data.BitVec.Basic
+import Init.Data.Fin.Basic
 
 open Nat
 
+@[extern "lean_uint8_of_nat"]
+def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨Fin.ofNat n⟩
+abbrev Nat.toUInt8 := UInt8.ofNat
+@[extern "lean_uint8_to_nat"]
+def UInt8.toNat (n : UInt8) : Nat := n.val.val
 @[extern "lean_uint8_add"]
-def UInt8.add (a b : UInt8) : UInt8 := ⟨a.toBitVec + b.toBitVec⟩
+def UInt8.add (a b : UInt8) : UInt8 := ⟨a.val + b.val⟩
 @[extern "lean_uint8_sub"]
-def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.toBitVec - b.toBitVec⟩
+def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.val - b.val⟩
 @[extern "lean_uint8_mul"]
-def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.toBitVec * b.toBitVec⟩
+def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.val * b.val⟩
 @[extern "lean_uint8_div"]
-def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
+def UInt8.div (a b : UInt8) : UInt8 := ⟨a.val / b.val⟩
 @[extern "lean_uint8_mod"]
-def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[extern "lean_uint8_modn", deprecated UInt8.mod (since := "2024-09-23")]
+def UInt8.mod (a b : UInt8) : UInt8 := ⟨a.val % b.val⟩
+@[extern "lean_uint8_modn"]
 def UInt8.modn (a : UInt8) (n : @& Nat) : UInt8 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint8_land"]
-def UInt8.land (a b : UInt8) : UInt8 := ⟨a.toBitVec &&& b.toBitVec⟩
+def UInt8.land (a b : UInt8) : UInt8 := ⟨Fin.land a.val b.val⟩
 @[extern "lean_uint8_lor"]
-def UInt8.lor (a b : UInt8) : UInt8 := ⟨a.toBitVec ||| b.toBitVec⟩
+def UInt8.lor (a b : UInt8) : UInt8 := ⟨Fin.lor a.val b.val⟩
 @[extern "lean_uint8_xor"]
-def UInt8.xor (a b : UInt8) : UInt8 := ⟨a.toBitVec ^^^ b.toBitVec⟩
+def UInt8.xor (a b : UInt8) : UInt8 := ⟨Fin.xor a.val b.val⟩
 @[extern "lean_uint8_shift_left"]
-def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.toBitVec <<< (mod b 8).toBitVec⟩
+def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.val <<< (modn b 8).val⟩
 @[extern "lean_uint8_shift_right"]
-def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.toBitVec >>> (mod b 8).toBitVec⟩
-def UInt8.lt (a b : UInt8) : Prop := a.toBitVec < b.toBitVec
-def UInt8.le (a b : UInt8) : Prop := a.toBitVec ≤ b.toBitVec
+def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.val >>> (modn b 8).val⟩
+def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
+def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
 
+instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
 instance : Add UInt8       := ⟨UInt8.add⟩
 instance : Sub UInt8       := ⟨UInt8.sub⟩
 instance : Mul UInt8       := ⟨UInt8.mul⟩
 instance : Mod UInt8       := ⟨UInt8.mod⟩
-
-set_option linter.deprecated false in
 instance : HMod UInt8 Nat UInt8 := ⟨UInt8.modn⟩
-
 instance : Div UInt8       := ⟨UInt8.div⟩
 instance : LT UInt8        := ⟨UInt8.lt⟩
 instance : LE UInt8        := ⟨UInt8.le⟩
 
 @[extern "lean_uint8_complement"]
-def UInt8.complement (a : UInt8) : UInt8 := ⟨~~~a.toBitVec⟩
+def UInt8.complement (a:UInt8) : UInt8 := 0-(a+1)
 
 instance : Complement UInt8 := ⟨UInt8.complement⟩
 instance : AndOp UInt8     := ⟨UInt8.land⟩
@@ -56,58 +58,69 @@ instance : Xor UInt8       := ⟨UInt8.xor⟩
 instance : ShiftLeft UInt8  := ⟨UInt8.shiftLeft⟩
 instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩
 
+set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint8_dec_lt"]
 def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
-  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
+set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint8_dec_le"]
 def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
-  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
 
 instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
 instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
 instance : Max UInt8 := maxOfLe
 instance : Min UInt8 := minOfLe
 
+@[extern "lean_uint16_of_nat"]
+def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨Fin.ofNat n⟩
+abbrev Nat.toUInt16 := UInt16.ofNat
+@[extern "lean_uint16_to_nat"]
+def UInt16.toNat (n : UInt16) : Nat := n.val.val
 @[extern "lean_uint16_add"]
-def UInt16.add (a b : UInt16) : UInt16 := ⟨a.toBitVec + b.toBitVec⟩
+def UInt16.add (a b : UInt16) : UInt16 := ⟨a.val + b.val⟩
 @[extern "lean_uint16_sub"]
-def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.toBitVec - b.toBitVec⟩
+def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.val - b.val⟩
 @[extern "lean_uint16_mul"]
-def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.toBitVec * b.toBitVec⟩
+def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.val * b.val⟩
 @[extern "lean_uint16_div"]
-def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
+def UInt16.div (a b : UInt16) : UInt16 := ⟨a.val / b.val⟩
 @[extern "lean_uint16_mod"]
-def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[extern "lean_uint16_modn", deprecated UInt16.mod (since := "2024-09-23")]
+def UInt16.mod (a b : UInt16) : UInt16 := ⟨a.val % b.val⟩
+@[extern "lean_uint16_modn"]
 def UInt16.modn (a : UInt16) (n : @& Nat) : UInt16 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint16_land"]
-def UInt16.land (a b : UInt16) : UInt16 := ⟨a.toBitVec &&& b.toBitVec⟩
+def UInt16.land (a b : UInt16) : UInt16 := ⟨Fin.land a.val b.val⟩
 @[extern "lean_uint16_lor"]
-def UInt16.lor (a b : UInt16) : UInt16 := ⟨a.toBitVec ||| b.toBitVec⟩
+def UInt16.lor (a b : UInt16) : UInt16 := ⟨Fin.lor a.val b.val⟩
 @[extern "lean_uint16_xor"]
-def UInt16.xor (a b : UInt16) : UInt16 := ⟨a.toBitVec ^^^ b.toBitVec⟩
+def UInt16.xor (a b : UInt16) : UInt16 := ⟨Fin.xor a.val b.val⟩
 @[extern "lean_uint16_shift_left"]
-def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.toBitVec <<< (mod b 16).toBitVec⟩
+def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.val <<< (modn b 16).val⟩
+@[extern "lean_uint16_to_uint8"]
+def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
+@[extern "lean_uint8_to_uint16"]
+def UInt8.toUInt16 (a : UInt8) : UInt16 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
 @[extern "lean_uint16_shift_right"]
-def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.toBitVec >>> (mod b 16).toBitVec⟩
-def UInt16.lt (a b : UInt16) : Prop := a.toBitVec < b.toBitVec
-def UInt16.le (a b : UInt16) : Prop := a.toBitVec ≤ b.toBitVec
+def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.val >>> (modn b 16).val⟩
+def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
+def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
 
+instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
 instance : Add UInt16       := ⟨UInt16.add⟩
 instance : Sub UInt16       := ⟨UInt16.sub⟩
 instance : Mul UInt16       := ⟨UInt16.mul⟩
 instance : Mod UInt16       := ⟨UInt16.mod⟩
-
-set_option linter.deprecated false in
 instance : HMod UInt16 Nat UInt16 := ⟨UInt16.modn⟩
-
 instance : Div UInt16       := ⟨UInt16.div⟩
 instance : LT UInt16        := ⟨UInt16.lt⟩
 instance : LE UInt16        := ⟨UInt16.le⟩
 
 @[extern "lean_uint16_complement"]
-def UInt16.complement (a : UInt16) : UInt16 := ⟨~~~a.toBitVec⟩
+def UInt16.complement (a:UInt16) : UInt16 := 0-(a+1)
 
 instance : Complement UInt16 := ⟨UInt16.complement⟩
 instance : AndOp UInt16     := ⟨UInt16.land⟩
@@ -119,53 +132,74 @@ instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint16_dec_lt"]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
-  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint16_dec_le"]
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
-  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
 
 instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
 instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
 instance : Max UInt16 := maxOfLe
 instance : Min UInt16 := minOfLe
 
+@[extern "lean_uint32_of_nat"]
+def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
+@[extern "lean_uint32_of_nat"]
+def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨⟨n, h⟩⟩
+/--
+Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
+-/
+def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
+  if h : n < UInt32.size then
+    UInt32.ofNat' n h
+  else
+    UInt32.ofNat' (UInt32.size - 1) (by decide)
+abbrev Nat.toUInt32 := UInt32.ofNat
 @[extern "lean_uint32_add"]
-def UInt32.add (a b : UInt32) : UInt32 := ⟨a.toBitVec + b.toBitVec⟩
+def UInt32.add (a b : UInt32) : UInt32 := ⟨a.val + b.val⟩
 @[extern "lean_uint32_sub"]
-def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.toBitVec - b.toBitVec⟩
+def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.val - b.val⟩
 @[extern "lean_uint32_mul"]
-def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.toBitVec * b.toBitVec⟩
+def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.val * b.val⟩
 @[extern "lean_uint32_div"]
-def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
+def UInt32.div (a b : UInt32) : UInt32 := ⟨a.val / b.val⟩
 @[extern "lean_uint32_mod"]
-def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[extern "lean_uint32_modn", deprecated UInt32.mod (since := "2024-09-23")]
+def UInt32.mod (a b : UInt32) : UInt32 := ⟨a.val % b.val⟩
+@[extern "lean_uint32_modn"]
 def UInt32.modn (a : UInt32) (n : @& Nat) : UInt32 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint32_land"]
-def UInt32.land (a b : UInt32) : UInt32 := ⟨a.toBitVec &&& b.toBitVec⟩
+def UInt32.land (a b : UInt32) : UInt32 := ⟨Fin.land a.val b.val⟩
 @[extern "lean_uint32_lor"]
-def UInt32.lor (a b : UInt32) : UInt32 := ⟨a.toBitVec ||| b.toBitVec⟩
+def UInt32.lor (a b : UInt32) : UInt32 := ⟨Fin.lor a.val b.val⟩
 @[extern "lean_uint32_xor"]
-def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩
+def UInt32.xor (a b : UInt32) : UInt32 := ⟨Fin.xor a.val b.val⟩
 @[extern "lean_uint32_shift_left"]
-def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.toBitVec <<< (mod b 32).toBitVec⟩
+def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.val <<< (modn b 32).val⟩
 @[extern "lean_uint32_shift_right"]
-def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (mod b 32).toBitVec⟩
+def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.val >>> (modn b 32).val⟩
+@[extern "lean_uint32_to_uint8"]
+def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
+@[extern "lean_uint32_to_uint16"]
+def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
+@[extern "lean_uint8_to_uint32"]
+def UInt8.toUInt32 (a : UInt8) : UInt32 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
+@[extern "lean_uint16_to_uint32"]
+def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
 
+instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
 instance : Mul UInt32       := ⟨UInt32.mul⟩
 instance : Mod UInt32       := ⟨UInt32.mod⟩
-
-set_option linter.deprecated false in
 instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩
-
 instance : Div UInt32       := ⟨UInt32.div⟩
 
 @[extern "lean_uint32_complement"]
-def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩
+def UInt32.complement (a:UInt32) : UInt32 := 0-(a+1)
 
 instance : Complement UInt32 := ⟨UInt32.complement⟩
 instance : AndOp UInt32     := ⟨UInt32.land⟩
@@ -174,45 +208,60 @@ instance : Xor UInt32       := ⟨UInt32.xor⟩
 instance : ShiftLeft UInt32  := ⟨UInt32.shiftLeft⟩
 instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
 
+@[extern "lean_uint64_of_nat"]
+def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨Fin.ofNat n⟩
+abbrev Nat.toUInt64 := UInt64.ofNat
+@[extern "lean_uint64_to_nat"]
+def UInt64.toNat (n : UInt64) : Nat := n.val.val
 @[extern "lean_uint64_add"]
-def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
+def UInt64.add (a b : UInt64) : UInt64 := ⟨a.val + b.val⟩
 @[extern "lean_uint64_sub"]
-def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.toBitVec - b.toBitVec⟩
+def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.val - b.val⟩
 @[extern "lean_uint64_mul"]
-def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.toBitVec * b.toBitVec⟩
+def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.val * b.val⟩
 @[extern "lean_uint64_div"]
-def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
+def UInt64.div (a b : UInt64) : UInt64 := ⟨a.val / b.val⟩
 @[extern "lean_uint64_mod"]
-def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[extern "lean_uint64_modn", deprecated UInt64.mod (since := "2024-09-23")]
+def UInt64.mod (a b : UInt64) : UInt64 := ⟨a.val % b.val⟩
+@[extern "lean_uint64_modn"]
 def UInt64.modn (a : UInt64) (n : @& Nat) : UInt64 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint64_land"]
-def UInt64.land (a b : UInt64) : UInt64 := ⟨a.toBitVec &&& b.toBitVec⟩
+def UInt64.land (a b : UInt64) : UInt64 := ⟨Fin.land a.val b.val⟩
 @[extern "lean_uint64_lor"]
-def UInt64.lor (a b : UInt64) : UInt64 := ⟨a.toBitVec ||| b.toBitVec⟩
+def UInt64.lor (a b : UInt64) : UInt64 := ⟨Fin.lor a.val b.val⟩
 @[extern "lean_uint64_xor"]
-def UInt64.xor (a b : UInt64) : UInt64 := ⟨a.toBitVec ^^^ b.toBitVec⟩
+def UInt64.xor (a b : UInt64) : UInt64 := ⟨Fin.xor a.val b.val⟩
 @[extern "lean_uint64_shift_left"]
-def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.toBitVec <<< (mod b 64).toBitVec⟩
+def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.val <<< (modn b 64).val⟩
 @[extern "lean_uint64_shift_right"]
-def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.toBitVec >>> (mod b 64).toBitVec⟩
-def UInt64.lt (a b : UInt64) : Prop := a.toBitVec < b.toBitVec
-def UInt64.le (a b : UInt64) : Prop := a.toBitVec ≤ b.toBitVec
+def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.val >>> (modn b 64).val⟩
+def UInt64.lt (a b : UInt64) : Prop := a.val < b.val
+def UInt64.le (a b : UInt64) : Prop := a.val ≤ b.val
+@[extern "lean_uint64_to_uint8"]
+def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
+@[extern "lean_uint64_to_uint16"]
+def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
+@[extern "lean_uint64_to_uint32"]
+def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
+@[extern "lean_uint8_to_uint64"]
+def UInt8.toUInt64 (a : UInt8) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
+@[extern "lean_uint16_to_uint64"]
+def UInt16.toUInt64 (a : UInt16) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
+@[extern "lean_uint32_to_uint64"]
+def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
 
+instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
 instance : Add UInt64       := ⟨UInt64.add⟩
 instance : Sub UInt64       := ⟨UInt64.sub⟩
 instance : Mul UInt64       := ⟨UInt64.mul⟩
 instance : Mod UInt64       := ⟨UInt64.mod⟩
-
-set_option linter.deprecated false in
 instance : HMod UInt64 Nat UInt64 := ⟨UInt64.modn⟩
-
 instance : Div UInt64       := ⟨UInt64.div⟩
 instance : LT UInt64        := ⟨UInt64.lt⟩
 instance : LE UInt64        := ⟨UInt64.le⟩
 
 @[extern "lean_uint64_complement"]
-def UInt64.complement (a : UInt64) : UInt64 := ⟨~~~a.toBitVec⟩
+def UInt64.complement (a:UInt64) : UInt64 := 0-(a+1)
 
 instance : Complement UInt64 := ⟨UInt64.complement⟩
 instance : AndOp UInt64     := ⟨UInt64.land⟩
@@ -224,52 +273,79 @@ instance : ShiftRight UInt64 := ⟨UInt64.shiftRight⟩
 @[extern "lean_bool_to_uint64"]
 def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0
 
+set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint64_dec_lt"]
 def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
-  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
+set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint64_dec_le"]
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
-  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
 
 instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
 instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
 instance : Max UInt64 := maxOfLe
 instance : Min UInt64 := minOfLe
 
+-- This instance would interfere with the global instance `NeZero (n + 1)`,
+-- so we only enable it locally.
+@[local instance]
+private def instNeZeroUSizeSize : NeZero USize.size := ⟨add_one_ne_zero _⟩
+
+@[deprecated (since := "2024-09-16")]
+theorem usize_size_gt_zero : USize.size > 0 :=
+  Nat.zero_lt_succ ..
+
+@[extern "lean_usize_of_nat"]
+def USize.ofNat (n : @& Nat) : USize := ⟨Fin.ofNat'  _ n⟩
+abbrev Nat.toUSize := USize.ofNat
+@[extern "lean_usize_to_nat"]
+def USize.toNat (n : USize) : Nat := n.val.val
+@[extern "lean_usize_add"]
+def USize.add (a b : USize) : USize := ⟨a.val + b.val⟩
+@[extern "lean_usize_sub"]
+def USize.sub (a b : USize) : USize := ⟨a.val - b.val⟩
 @[extern "lean_usize_mul"]
-def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
+def USize.mul (a b : USize) : USize := ⟨a.val * b.val⟩
 @[extern "lean_usize_div"]
-def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
+def USize.div (a b : USize) : USize := ⟨a.val / b.val⟩
 @[extern "lean_usize_mod"]
-def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩
-@[extern "lean_usize_modn", deprecated USize.mod (since := "2024-09-23")]
+def USize.mod (a b : USize) : USize := ⟨a.val % b.val⟩
+@[extern "lean_usize_modn"]
 def USize.modn (a : USize) (n : @& Nat) : USize := ⟨Fin.modn a.val n⟩
 @[extern "lean_usize_land"]
-def USize.land (a b : USize) : USize := ⟨a.toBitVec &&& b.toBitVec⟩
+def USize.land (a b : USize) : USize := ⟨Fin.land a.val b.val⟩
 @[extern "lean_usize_lor"]
-def USize.lor (a b : USize) : USize := ⟨a.toBitVec ||| b.toBitVec⟩
+def USize.lor (a b : USize) : USize := ⟨Fin.lor a.val b.val⟩
 @[extern "lean_usize_xor"]
-def USize.xor (a b : USize) : USize := ⟨a.toBitVec ^^^ b.toBitVec⟩
+def USize.xor (a b : USize) : USize := ⟨Fin.xor a.val b.val⟩
 @[extern "lean_usize_shift_left"]
-def USize.shiftLeft (a b : USize) : USize := ⟨a.toBitVec <<< (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
+def USize.shiftLeft (a b : USize) : USize := ⟨a.val <<< (modn b System.Platform.numBits).val⟩
 @[extern "lean_usize_shift_right"]
-def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
+def USize.shiftRight (a b : USize) : USize := ⟨a.val >>> (modn b System.Platform.numBits).val⟩
 @[extern "lean_uint32_to_usize"]
-def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.toBitVec.toNat a.toBitVec.isLt
+def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.val a.1.2
 @[extern "lean_usize_to_uint32"]
 def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
 
+def USize.lt (a b : USize) : Prop := a.val < b.val
+def USize.le (a b : USize) : Prop := a.val ≤ b.val
+
+instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
+instance : Add USize       := ⟨USize.add⟩
+instance : Sub USize       := ⟨USize.sub⟩
 instance : Mul USize       := ⟨USize.mul⟩
 instance : Mod USize       := ⟨USize.mod⟩
-
-set_option linter.deprecated false in
 instance : HMod USize Nat USize := ⟨USize.modn⟩
-
 instance : Div USize       := ⟨USize.div⟩
+instance : LT USize        := ⟨USize.lt⟩
+instance : LE USize        := ⟨USize.le⟩
 
 @[extern "lean_usize_complement"]
-def USize.complement (a : USize) : USize := ⟨~~~a.toBitVec⟩
+def USize.complement (a:USize) : USize := 0-(a+1)
 
 instance : Complement USize := ⟨USize.complement⟩
 instance : AndOp USize      := ⟨USize.land⟩
@@ -278,5 +354,19 @@ instance : Xor USize        := ⟨USize.xor⟩
 instance : ShiftLeft USize  := ⟨USize.shiftLeft⟩
 instance : ShiftRight USize := ⟨USize.shiftRight⟩
 
+set_option bootstrap.genMatcherCode false in
+@[extern "lean_usize_dec_lt"]
+def USize.decLt (a b : USize) : Decidable (a < b) :=
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
+
+set_option bootstrap.genMatcherCode false in
+@[extern "lean_usize_dec_le"]
+def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
+
+instance (a b : USize) : Decidable (a < b) := USize.decLt a b
+instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
 instance : Max USize := maxOfLe
 instance : Min USize := minOfLe

src/Init/Data/UInt/BasicAux.lean

@@ -1,132 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Data.Fin.Basic
-import Init.Data.BitVec.BasicAux
-
-/-!
-This module exists to provide the very basic `UInt8` etc. definitions required for
-`Init.Data.Char.Basic` and `Init.Data.Array.Basic`. These are very important as they are used in
-meta code that is then (transitively) used in `Init.Data.UInt.Basic` and `Init.Data.BitVec.Basic`.
-This file thus breaks the import cycle that would be created by this dependency.
--/
-
-open Nat
-
-def UInt8.val (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
-@[extern "lean_uint8_of_nat"]
-def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩
-abbrev Nat.toUInt8 := UInt8.ofNat
-@[extern "lean_uint8_to_nat"]
-def UInt8.toNat (n : UInt8) : Nat := n.toBitVec.toNat
-
-instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
-
-def UInt16.val (x : UInt16) : Fin UInt16.size := x.toBitVec.toFin
-@[extern "lean_uint16_of_nat"]
-def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨BitVec.ofNat 16 n⟩
-abbrev Nat.toUInt16 := UInt16.ofNat
-@[extern "lean_uint16_to_nat"]
-def UInt16.toNat (n : UInt16) : Nat := n.toBitVec.toNat
-@[extern "lean_uint16_to_uint8"]
-def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
-@[extern "lean_uint8_to_uint16"]
-def UInt8.toUInt16 (a : UInt8) : UInt16 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
-
-instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
-
-def UInt32.val (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin
-@[extern "lean_uint32_of_nat"]
-def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨BitVec.ofNat 32 n⟩
-@[extern "lean_uint32_of_nat"]
-def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨BitVec.ofNatLt n h⟩
-/--
-Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
--/
-def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
-  if h : n < UInt32.size then
-    UInt32.ofNat' n h
-  else
-    UInt32.ofNat' (UInt32.size - 1) (by decide)
-abbrev Nat.toUInt32 := UInt32.ofNat
-@[extern "lean_uint32_to_uint8"]
-def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
-@[extern "lean_uint32_to_uint16"]
-def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
-@[extern "lean_uint8_to_uint32"]
-def UInt8.toUInt32 (a : UInt8) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
-@[extern "lean_uint16_to_uint32"]
-def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
-
-instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
-
-theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
-     n < m → UInt32.ofNat' n h1 < UInt32.ofNat m := by
-  simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLt, ofNat, BitVec.ofNat, Fin.ofNat',
-    Nat.mod_eq_of_lt h2, imp_self]
-
-theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
-     m < n → UInt32.ofNat m < UInt32.ofNat' n h1  := by
-  simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLt, ofNat, BitVec.ofNat, Fin.ofNat',
-    Nat.mod_eq_of_lt h2, imp_self]
-
-def UInt64.val (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin
-@[extern "lean_uint64_of_nat"]
-def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨BitVec.ofNat 64 n⟩
-abbrev Nat.toUInt64 := UInt64.ofNat
-@[extern "lean_uint64_to_nat"]
-def UInt64.toNat (n : UInt64) : Nat := n.toBitVec.toNat
-@[extern "lean_uint64_to_uint8"]
-def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
-@[extern "lean_uint64_to_uint16"]
-def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
-@[extern "lean_uint64_to_uint32"]
-def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
-@[extern "lean_uint8_to_uint64"]
-def UInt8.toUInt64 (a : UInt8) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
-@[extern "lean_uint16_to_uint64"]
-def UInt16.toUInt64 (a : UInt16) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
-@[extern "lean_uint32_to_uint64"]
-def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
-
-instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
-
-theorem usize_size_gt_zero : USize.size > 0 := by
-  cases usize_size_eq with
-  | inl h => rw [h]; decide
-  | inr h => rw [h]; decide
-
-def USize.val (x : USize) : Fin USize.size := x.toBitVec.toFin
-@[extern "lean_usize_of_nat"]
-def USize.ofNat (n : @& Nat) : USize := ⟨BitVec.ofNat _ n⟩
-abbrev Nat.toUSize := USize.ofNat
-@[extern "lean_usize_to_nat"]
-def USize.toNat (n : USize) : Nat := n.toBitVec.toNat
-@[extern "lean_usize_add"]
-def USize.add (a b : USize) : USize := ⟨a.toBitVec + b.toBitVec⟩
-@[extern "lean_usize_sub"]
-def USize.sub (a b : USize) : USize := ⟨a.toBitVec - b.toBitVec⟩
-
-def USize.lt (a b : USize) : Prop := a.toBitVec < b.toBitVec
-def USize.le (a b : USize) : Prop := a.toBitVec ≤ b.toBitVec
-
-instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
-
-instance : Add USize       := ⟨USize.add⟩
-instance : Sub USize       := ⟨USize.sub⟩
-instance : LT USize        := ⟨USize.lt⟩
-instance : LE USize        := ⟨USize.le⟩
-
-@[extern "lean_usize_dec_lt"]
-def USize.decLt (a b : USize) : Decidable (a < b) :=
-  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
-
-@[extern "lean_usize_dec_le"]
-def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
-  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
-
-instance (a b : USize) : Decidable (a < b) := USize.decLt a b
-instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b

src/Init/Data/UInt/Bitwise.lean

@@ -6,14 +6,13 @@ Authors: Markus Himmel
 prelude
 import Init.Data.UInt.Basic
 import Init.Data.Fin.Bitwise
-import Init.Data.BitVec.Lemmas
 
 set_option hygiene false in
 macro "declare_bitwise_uint_theorems" typeName:ident : command =>
 `(
 namespace $typeName
 
-@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
+@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := Fin.and_val ..
 
 end $typeName
 )

src/Init/Data/UInt/Lemmas.lean

@@ -6,8 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.UInt.Basic
 import Init.Data.Fin.Lemmas
-import Init.Data.BitVec.Lemmas
-import Init.Data.BitVec.Bitblast
 
 set_option hygiene false in
 macro "declare_uint_theorems" typeName:ident : command =>
@@ -19,111 +17,50 @@ instance : Inhabited $typeName where
 
 theorem zero_def : (0 : $typeName) = ⟨0⟩ := rfl
 theorem one_def : (1 : $typeName) = ⟨1⟩ := rfl
-theorem sub_def (a b : $typeName) : a - b = ⟨a.toBitVec - b.toBitVec⟩ := rfl
-theorem mul_def (a b : $typeName) : a * b = ⟨a.toBitVec * b.toBitVec⟩ := rfl
-theorem mod_def (a b : $typeName) : a % b = ⟨a.toBitVec % b.toBitVec⟩ := rfl
-theorem add_def (a b : $typeName) : a + b = ⟨a.toBitVec + b.toBitVec⟩ := rfl
+theorem sub_def (a b : $typeName) : a - b = ⟨a.val - b.val⟩ := rfl
+theorem mul_def (a b : $typeName) : a * b = ⟨a.val * b.val⟩ := rfl
+theorem mod_def (a b : $typeName) : a % b = ⟨a.val % b.val⟩ := rfl
+theorem add_def (a b : $typeName) : a + b = ⟨a.val + b.val⟩ := rfl
 
-@[simp] theorem mk_toBitVec_eq : ∀ (a : $typeName), mk a.toBitVec = a
+@[simp] theorem mk_val_eq : ∀ (a : $typeName), mk a.val = a
   | ⟨_, _⟩ => rfl
-
-theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
+theorem val_eq_of_lt {a : Nat} : a < size → ((ofNat a).val : Nat) = a :=
   Nat.mod_eq_of_lt
-
 theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
-  rw [toNat, toBitVec_eq_of_lt h]
-
-theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
-
-theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
-
-@[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := by simp [le_def, lt_def]
-
-@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := by simp [le_def, lt_def]
+  rw [toNat, val_eq_of_lt h]
 
+theorem le_def {a b : $typeName} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
+theorem lt_def {a b : $typeName} : a < b ↔ a.1 < b.1 := .rfl
+theorem lt_iff_val_lt_val {a b : $typeName} : a < b ↔ a.val < b.val := .rfl
+@[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := Fin.not_le
+@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := Fin.not_lt
 @[simp] protected theorem le_refl (a : $typeName) : a ≤ a := by simp [le_def]
-
 @[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
-
-protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := BitVec.le_trans
-
-protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := BitVec.lt_trans
-
-protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := BitVec.le_total ..
-
-protected theorem lt_asymm {a b : $typeName} : a < b → ¬ b < a := BitVec.lt_asymm
-
-protected theorem toBitVec_eq_of_eq {a b : $typeName} (h : a = b) : a.toBitVec = b.toBitVec := h ▸ rfl
-
-protected theorem eq_of_toBitVec_eq {a b : $typeName} (h : a.toBitVec = b.toBitVec) : a = b := by
-  cases a; cases b; simp_all
-
-open $typeName (eq_of_toBitVec_eq) in
-protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by
-  rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [val]
-
-open $typeName (toBitVec_eq_of_eq) in
-protected theorem ne_of_toBitVec_ne {a b : $typeName} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b :=
-  fun h' => absurd (toBitVec_eq_of_eq h') h
-
-open $typeName (ne_of_toBitVec_ne) in
-protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := by
-  apply ne_of_toBitVec_ne
-  apply BitVec.ne_of_lt
-  simpa [lt_def] using h
+protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := Fin.le_trans
+protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := Fin.lt_trans
+protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := Fin.le_total a.1 b.1
+protected theorem lt_asymm {a b : $typeName} (h : a < b) : ¬ b < a := Fin.lt_asymm h
+protected theorem val_eq_of_eq {a b : $typeName} (h : a = b) : a.val = b.val := h ▸ rfl
+protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by cases a; cases b; simp at h; simp [h]
+open $typeName (val_eq_of_eq) in
+protected theorem ne_of_val_ne {a b : $typeName} (h : a.val ≠ b.val) : a ≠ b := fun h' => absurd (val_eq_of_eq h') h
+open $typeName (ne_of_val_ne) in
+protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := ne_of_val_ne (Fin.ne_of_lt h)
 
 @[simp] protected theorem toNat_zero : (0 : $typeName).toNat = 0 := Nat.zero_mod _
-
-@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := BitVec.toNat_umod ..
-
-@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := BitVec.toNat_udiv  ..
-
-@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := BitVec.toNat_sub_of_le
-
-protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.toBitVec.isLt
-
-open $typeName (toNat_mod toNat_lt_size) in
-protected theorem toNat_mod_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % ofNat m) < m := by
-  intro u h1
-  by_cases h2 : m < size
-  · rw [toNat_mod, toNat_ofNat_of_lt h2]
-    apply Nat.mod_lt _ h1
-  · apply Nat.lt_of_lt_of_le
-    · apply toNat_lt_size
-    · simpa using h2
-
-open $typeName (toNat_mod_lt) in
-set_option linter.deprecated false in
-@[deprecated toNat_mod_lt (since := "2024-09-24")]
-protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m := by
-  intro u
-  simp only [(· % ·)]
-  simp only [gt_iff_lt, toNat, modn, Fin.modn_val, BitVec.natCast_eq_ofNat, BitVec.toNat_ofNat,
-    Nat.reducePow]
-  rw [Nat.mod_eq_of_lt]
-  · apply Nat.mod_lt
-  · apply Nat.lt_of_le_of_lt
-    · apply Nat.mod_le
-    · apply Fin.is_lt
-
-protected theorem mod_lt (a : $typeName) {b : $typeName} : 0 < b → a % b < b := by
-  simp only [lt_def, mod_def]
-  apply BitVec.umod_lt
-
+@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := Fin.mod_val ..
+@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := Fin.div_val ..
+@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := Fin.sub_val_of_le
+@[simp] protected theorem toNat_modn (a : $typeName) (b : Nat) : (a.modn b).toNat = a.toNat % b := Fin.modn_val ..
+protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m
+  | ⟨u⟩, h => Fin.modn_lt u h
+open $typeName (modn_lt) in
+protected theorem mod_lt (a b : $typeName) (h : 0 < b) : a % b < b := modn_lt _ (by simp [lt_def] at h; exact h)
 protected theorem toNat.inj : ∀ {a b : $typeName}, a.toNat = b.toNat → a = b
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
-
+protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.1.2
 @[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
 
-@[simp]
-theorem val_ofNat (n : Nat) : val (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
-
-@[simp]
-theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
-
-@[simp]
-theorem mk_ofNat (n : Nat) : mk (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
-
 end $typeName
 )
 
@@ -133,34 +70,27 @@ declare_uint_theorems UInt32
 declare_uint_theorems UInt64
 declare_uint_theorems USize
 
-theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := by
-  simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
-
-theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat := by
-  simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
-
-theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m := by
-  simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
-
-theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by
-  simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
-
 @[deprecated (since := "2024-06-23")] protected abbrev UInt8.zero_toNat := @UInt8.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt8.div_toNat := @UInt8.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt8.mod_toNat := @UInt8.toNat_mod
+@[deprecated (since := "2024-06-23")] protected abbrev UInt8.modn_toNat := @UInt8.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev UInt16.zero_toNat := @UInt16.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt16.div_toNat := @UInt16.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt16.mod_toNat := @UInt16.toNat_mod
+@[deprecated (since := "2024-06-23")] protected abbrev UInt16.modn_toNat := @UInt16.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev UInt32.zero_toNat := @UInt32.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt32.div_toNat := @UInt32.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt32.mod_toNat := @UInt32.toNat_mod
+@[deprecated (since := "2024-06-23")] protected abbrev UInt32.modn_toNat := @UInt32.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev UInt64.zero_toNat := @UInt64.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt64.div_toNat := @UInt64.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt64.mod_toNat := @UInt64.toNat_mod
+@[deprecated (since := "2024-06-23")] protected abbrev UInt64.modn_toNat := @UInt64.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev USize.zero_toNat := @USize.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev USize.div_toNat := @USize.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev USize.mod_toNat := @USize.toNat_mod
+@[deprecated (since := "2024-06-23")] protected abbrev USize.modn_toNat := @USize.toNat_modn

src/Init/Data/UInt/Log2.lean

@@ -7,16 +7,16 @@ prelude
 import Init.Data.Fin.Log2
 
 @[extern "lean_uint8_log2"]
-def UInt8.log2 (a : UInt8) : UInt8 := ⟨⟨Fin.log2 a.val⟩⟩
+def UInt8.log2 (a : UInt8) : UInt8 := ⟨Fin.log2 a.val⟩
 
 @[extern "lean_uint16_log2"]
-def UInt16.log2 (a : UInt16) : UInt16 := ⟨⟨Fin.log2 a.val⟩⟩
+def UInt16.log2 (a : UInt16) : UInt16 := ⟨Fin.log2 a.val⟩
 
 @[extern "lean_uint32_log2"]
-def UInt32.log2 (a : UInt32) : UInt32 := ⟨⟨Fin.log2 a.val⟩⟩
+def UInt32.log2 (a : UInt32) : UInt32 := ⟨Fin.log2 a.val⟩
 
 @[extern "lean_uint64_log2"]
-def UInt64.log2 (a : UInt64) : UInt64 := ⟨⟨Fin.log2 a.val⟩⟩
+def UInt64.log2 (a : UInt64) : UInt64 := ⟨Fin.log2 a.val⟩
 
 @[extern "lean_usize_log2"]
-def USize.log2 (a : USize) : USize := ⟨⟨Fin.log2 a.val⟩⟩
+def USize.log2 (a : USize) : USize := ⟨Fin.log2 a.val⟩

src/Init/MetaTypes.lean

@@ -224,7 +224,11 @@ structure Config where
   -/
   index             : Bool := true
   /--
-  This option does not have any effect (yet).
+  When `true` (default: `true`), `simp` will **not** create a proof for a rewriting rule associated
+  with an `rfl`-theorem.
+  Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`.
+  If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp`
+  will **not** create a proof term which is an application of the annotated theorem.
   -/
   implicitDefEqProofs : Bool := true
   deriving Inhabited, BEq

src/Init/Prelude.lean

@@ -1592,6 +1592,9 @@ def Nat.beq : (@& Nat) → (@& Nat) → Bool
   | succ _, zero   => false
   | succ n, succ m => beq n m
 
+instance : BEq Nat where
+  beq := Nat.beq
+
 theorem Nat.eq_of_beq_eq_true : {n m : Nat} → Eq (beq n m) true → Eq n m
   | zero,   zero,   _ => rfl
   | zero,   succ _, h => Bool.noConfusion h
@@ -1866,52 +1869,6 @@ instance {n} : LE (Fin n) where
 instance Fin.decLt {n} (a b : Fin n) : Decidable (LT.lt a b) := Nat.decLt ..
 instance Fin.decLe {n} (a b : Fin n) : Decidable (LE.le a b) := Nat.decLe ..
 
-/--
-A bitvector of the specified width.
-
-This is represented as the underlying `Nat` number in both the runtime
-and the kernel, inheriting all the special support for `Nat`.
--/
-structure BitVec (w : Nat) where
-  /-- Construct a `BitVec w` from a number less than `2^w`.
-  O(1), because we use `Fin` as the internal representation of a bitvector. -/
-  ofFin ::
-  /-- Interpret a bitvector as a number less than `2^w`.
-  O(1), because we use `Fin` as the internal representation of a bitvector. -/
-  toFin : Fin (hPow 2 w)
-
-/--
-Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
--/
--- We manually derive the `DecidableEq` instances for `BitVec` because
--- we want to have builtin support for bit-vector literals, and we
--- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
-def BitVec.decEq (x y : BitVec n) : Decidable (Eq x y) :=
-  match x, y with
-  | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m)
-      (fun h => isTrue (h ▸ rfl))
-      (fun h => isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h)))
-
-instance : DecidableEq (BitVec n) := BitVec.decEq
-
-/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
-@[match_pattern]
-protected def BitVec.ofNatLt {n : Nat} (i : Nat) (p : LT.lt i (hPow 2 n)) : BitVec n where
-  toFin := ⟨i, p⟩
-
-/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
-(zero-cost) wrapper around a `Nat`. -/
-protected def BitVec.toNat (x : BitVec n) : Nat := x.toFin.val
-
-instance : LT (BitVec n) where lt := (LT.lt ·.toNat ·.toNat)
-instance (x y : BitVec n) : Decidable (LT.lt x y) :=
-  inferInstanceAs (Decidable (LT.lt x.toNat y.toNat))
-
-instance : LE (BitVec n) where le := (LE.le ·.toNat ·.toNat)
-instance (x y : BitVec n) : Decidable (LE.le x y) :=
-  inferInstanceAs (Decidable (LE.le x.toNat y.toNat))
-
 /-- The size of type `UInt8`, that is, `2^8 = 256`. -/
 abbrev UInt8.size : Nat := 256
 
@@ -1920,12 +1877,12 @@ The type of unsigned 8-bit integers. This type has special support in the
 compiler to make it actually 8 bits rather than wrapping a `Nat`.
 -/
 structure UInt8 where
-  /-- Unpack a `UInt8` as a `BitVec 8`.
+  /-- Unpack a `UInt8` as a `Nat` less than `2^8`.
   This function is overridden with a native implementation. -/
-  toBitVec : BitVec 8
+  val : Fin UInt8.size
 
 attribute [extern "lean_uint8_of_nat_mk"] UInt8.mk
-attribute [extern "lean_uint8_to_nat"] UInt8.toBitVec
+attribute [extern "lean_uint8_to_nat"] UInt8.val
 
 /--
 Pack a `Nat` less than `2^8` into a `UInt8`.
@@ -1933,7 +1890,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint8_of_nat"]
 def UInt8.ofNatCore (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
-  toBitVec := BitVec.ofNatLt n h
+  val := { val := n, isLt := h }
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -1944,9 +1901,7 @@ This function is overridden with a native implementation.
 def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m)
-      (fun h => isTrue (h ▸ rfl))
-      (fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq UInt8 := UInt8.decEq
 
@@ -1961,12 +1916,12 @@ The type of unsigned 16-bit integers. This type has special support in the
 compiler to make it actually 16 bits rather than wrapping a `Nat`.
 -/
 structure UInt16 where
-  /-- Unpack a `UInt16` as a `BitVec 16`.
+  /-- Unpack a `UInt16` as a `Nat` less than `2^16`.
   This function is overridden with a native implementation. -/
-  toBitVec : BitVec 16
+  val : Fin UInt16.size
 
 attribute [extern "lean_uint16_of_nat_mk"] UInt16.mk
-attribute [extern "lean_uint16_to_nat"] UInt16.toBitVec
+attribute [extern "lean_uint16_to_nat"] UInt16.val
 
 /--
 Pack a `Nat` less than `2^16` into a `UInt16`.
@@ -1974,7 +1929,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint16_of_nat"]
 def UInt16.ofNatCore (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where
-  toBitVec := BitVec.ofNatLt n h
+  val := { val := n, isLt := h }
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -1985,9 +1940,7 @@ This function is overridden with a native implementation.
 def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m)
-      (fun h => isTrue (h ▸ rfl))
-      (fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq UInt16 := UInt16.decEq
 
@@ -2002,12 +1955,12 @@ The type of unsigned 32-bit integers. This type has special support in the
 compiler to make it actually 32 bits rather than wrapping a `Nat`.
 -/
 structure UInt32 where
-  /-- Unpack a `UInt32` as a `BitVec 32.
+  /-- Unpack a `UInt32` as a `Nat` less than `2^32`.
   This function is overridden with a native implementation. -/
-  toBitVec : BitVec 32
+  val : Fin UInt32.size
 
 attribute [extern "lean_uint32_of_nat_mk"] UInt32.mk
-attribute [extern "lean_uint32_to_nat"] UInt32.toBitVec
+attribute [extern "lean_uint32_to_nat"] UInt32.val
 
 /--
 Pack a `Nat` less than `2^32` into a `UInt32`.
@@ -2015,14 +1968,14 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_of_nat"]
 def UInt32.ofNatCore (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 where
-  toBitVec := BitVec.ofNatLt n h
+  val := { val := n, isLt := h }
 
 /--
 Unpack a `UInt32` as a `Nat`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_to_nat"]
-def UInt32.toNat (n : UInt32) : Nat := n.toBitVec.toNat
+def UInt32.toNat (n : UInt32) : Nat := n.val.val
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -2041,26 +1994,30 @@ instance : Inhabited UInt32 where
   default := UInt32.ofNatCore 0 (by decide)
 
 instance : LT UInt32 where
-  lt a b := LT.lt a.toBitVec b.toBitVec
+  lt a b := LT.lt a.val b.val
 
 instance : LE UInt32 where
-  le a b := LE.le a.toBitVec b.toBitVec
+  le a b := LE.le a.val b.val
 
+set_option bootstrap.genMatcherCode false in
 /--
 Decides less-equal on `UInt32`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_dec_lt"]
 def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
-  inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LT.lt n m))
 
+set_option bootstrap.genMatcherCode false in
 /--
 Decides less-than on `UInt32`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_dec_le"]
 def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
-  inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LE.le n m))
 
 instance (a b : UInt32) : Decidable (LT.lt a b) := UInt32.decLt a b
 instance (a b : UInt32) : Decidable (LE.le a b) := UInt32.decLe a b
@@ -2074,12 +2031,12 @@ The type of unsigned 64-bit integers. This type has special support in the
 compiler to make it actually 64 bits rather than wrapping a `Nat`.
 -/
 structure UInt64 where
-  /-- Unpack a `UInt64` as a `BitVec 64`.
+  /-- Unpack a `UInt64` as a `Nat` less than `2^64`.
   This function is overridden with a native implementation. -/
-  toBitVec: BitVec 64
+  val : Fin UInt64.size
 
 attribute [extern "lean_uint64_of_nat_mk"] UInt64.mk
-attribute [extern "lean_uint64_to_nat"] UInt64.toBitVec
+attribute [extern "lean_uint64_to_nat"] UInt64.val
 
 /--
 Pack a `Nat` less than `2^64` into a `UInt64`.
@@ -2087,7 +2044,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint64_of_nat"]
 def UInt64.ofNatCore (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where
-  toBitVec := BitVec.ofNatLt n h
+  val := { val := n, isLt := h }
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -2098,20 +2055,36 @@ This function is overridden with a native implementation.
 def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m)
-      (fun h => isTrue (h ▸ rfl))
-      (fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq UInt64 := UInt64.decEq
 
 instance : Inhabited UInt64 where
   default := UInt64.ofNatCore 0 (by decide)
 
-/-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/
-abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
+/--
+The size of type `USize`, that is, `2^System.Platform.numBits`, which may
+be either `2^32` or `2^64` depending on the platform's architecture.
+
+Remark: we define `USize.size` using `(2^numBits - 1) + 1` to ensure the
+Lean unifier can solve constraints such as `?m + 1 = USize.size`. Recall that
+`numBits` does not reduce to a numeral in the Lean kernel since it is platform
+specific. Without this trick, the following definition would be rejected by the
+Lean type checker.
+```
+def one: Fin USize.size := 1
+```
+Because Lean would fail to synthesize instance `OfNat (Fin USize.size) 1`.
+Recall that the `OfNat` instance for `Fin` is
+```
+instance : OfNat (Fin (n+1)) i where
+  ofNat := Fin.ofNat i
+```
+-/
+abbrev USize.size : Nat := hAdd (hSub (hPow 2 System.Platform.numBits) 1) 1
 
 theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
-  show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
+  show Or (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 4294967296) (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 18446744073709551616) from
   match System.Platform.numBits, System.Platform.numBits_eq with
   | _, Or.inl rfl => Or.inl (by decide)
   | _, Or.inr rfl => Or.inr (by decide)
@@ -2124,20 +2097,21 @@ For example, if running on a 32-bit machine, USize is equivalent to UInt32.
 Or on a 64-bit machine, UInt64.
 -/
 structure USize where
-  /-- Unpack a `USize` as a `BitVec System.Platform.numBits`.
+  /-- Unpack a `USize` as a `Nat` less than `USize.size`.
   This function is overridden with a native implementation. -/
-  toBitVec : BitVec System.Platform.numBits
+  val : Fin USize.size
 
 attribute [extern "lean_usize_of_nat_mk"] USize.mk
-attribute [extern "lean_usize_to_nat"] USize.toBitVec
+attribute [extern "lean_usize_to_nat"] USize.val
 
 /--
 Pack a `Nat` less than `USize.size` into a `USize`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_of_nat"]
-def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize where
-  toBitVec := BitVec.ofNatLt n h
+def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize := {
+  val := { val := n, isLt := h }
+}
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -2148,9 +2122,7 @@ This function is overridden with a native implementation.
 def USize.decEq (a b : USize) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m)
-      (fun h => isTrue (h ▸ rfl))
-      (fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m) (fun h =>isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq USize := USize.decEq
 
@@ -2166,12 +2138,12 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_of_nat"]
 def USize.ofNat32 (n : @& Nat) (h : LT.lt n 4294967296) : USize where
-  toBitVec :=
-    BitVec.ofNatLt n (
-      match System.Platform.numBits, System.Platform.numBits_eq with
+  val := {
+    val  := n
+    isLt := match USize.size, usize_size_eq with
       | _, Or.inl rfl => h
       | _, Or.inr rfl => Nat.lt_trans h (by decide)
-    )
+  }
 
 /--
 A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and
@@ -2206,7 +2178,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_of_nat"]
 def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=
-  { val := ⟨BitVec.ofNatLt n (isValidChar_UInt32 h)⟩, valid := h }
+  { val := ⟨{ val := n, isLt := isValidChar_UInt32 h }⟩, valid := h }
 
 /--
 Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scalar value,
@@ -2216,7 +2188,7 @@ Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scal
 def Char.ofNat (n : Nat) : Char :=
   dite (n.isValidChar)
     (fun h => Char.ofNatAux n h)
-    (fun _ => { val := ⟨BitVec.ofNatLt 0 (by decide)⟩, valid := Or.inl (by decide) })
+    (fun _ => { val := ⟨{ val := 0, isLt := by decide }⟩, valid := Or.inl (by decide) })
 
 theorem Char.eq_of_val_eq : ∀ {c d : Char}, Eq c.val d.val → Eq c d
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
@@ -3476,13 +3448,15 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_to_uint64"]
 def USize.toUInt64 (u : USize) : UInt64 where
-  toBitVec := BitVec.ofNatLt u.toBitVec.toNat (
-        let ⟨⟨n, h⟩⟩ := u
-        show LT.lt n _ from
-        match System.Platform.numBits, System.Platform.numBits_eq, h with
-        | _, Or.inl rfl, h => Nat.lt_trans h (by decide)
-        | _, Or.inr rfl, h => h
-      )
+  val := {
+    val  := u.val.val
+    isLt :=
+      let ⟨n, h⟩ := u
+      show LT.lt n _ from
+      match USize.size, usize_size_eq, h with
+      | _, Or.inl rfl, h => Nat.lt_trans h (by decide)
+      | _, Or.inr rfl, h => h
+  }
 
 /-- An opaque hash mixing operation, used to implement hashing for tuples. -/
 @[extern "lean_uint64_mix_hash"]

src/Init/PropLemmas.lean

@@ -135,10 +135,6 @@ Both reduce to `b = false ∧ c = false` via `not_or`.
 
 theorem not_and_of_not_or_not (h : ¬a ∨ ¬b) : ¬(a ∧ b) := h.elim (mt (·.1)) (mt (·.2))
 
-/-! ## not equal -/
-
-theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} : f x ≠ f y → x ≠ y :=
-  mt <| congrArg _
 
 /-! ## Ite -/
 
@@ -388,17 +384,6 @@ theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' :
 
 end quantifiers
 
-/-! ## membership -/
-
-section Mem
-variable [Membership α β] {s t : β} {a b : α}
-
-theorem ne_of_mem_of_not_mem (h : a ∈ s) : b ∉ s → a ≠ b := mt fun e => e ▸ h
-
-theorem ne_of_mem_of_not_mem' (h : a ∈ s) : a ∉ t → s ≠ t := mt fun e => e ▸ h
-
-end Mem
-
 /-! ## Nonempty -/
 
 @[simp] theorem nonempty_prop {p : Prop} : Nonempty p ↔ p :=

src/Init/SizeOf.lean

@@ -67,7 +67,6 @@ deriving instance SizeOf for PLift
 deriving instance SizeOf for ULift
 deriving instance SizeOf for Decidable
 deriving instance SizeOf for Fin
-deriving instance SizeOf for BitVec
 deriving instance SizeOf for UInt8
 deriving instance SizeOf for UInt16
 deriving instance SizeOf for UInt32

src/Init/SizeOfLemmas.lean

@@ -11,25 +11,22 @@ import Init.Data.Nat.Linear
 @[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
   cases a; simp_arith
 
-@[simp] protected theorem BitVec.sizeOf (a : BitVec w) : sizeOf a = sizeOf a.toFin + 1 := by
-  cases a; simp_arith
+@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 2 := by
+  cases a; simp_arith [UInt8.toNat]
 
-@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 3 := by
-  cases a; simp_arith [UInt8.toNat, BitVec.toNat]
+@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 2 := by
+  cases a; simp_arith [UInt16.toNat]
 
-@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 3 := by
-  cases a; simp_arith [UInt16.toNat, BitVec.toNat]
+@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 2 := by
+  cases a; simp_arith [UInt32.toNat]
 
-@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 3 := by
-  cases a; simp_arith [UInt32.toNat, BitVec.toNat]
+@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 2 := by
+  cases a; simp_arith [UInt64.toNat]
 
-@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 3 := by
-  cases a; simp_arith [UInt64.toNat, BitVec.toNat]
+@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 2 := by
+  cases a; simp_arith [USize.toNat]
 
-@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 3 := by
-  cases a; simp_arith [USize.toNat, BitVec.toNat]
-
-@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 4 := by
+@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 3 := by
   cases a; simp_arith [Char.toNat]
 
 @[simp] protected theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by

src/Init/Tactics.lean

@@ -268,9 +268,9 @@ syntax (name := case') "case' " sepBy1(caseArg, " | ") " => " tacticSeq : tactic
 `next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
 inaccessible names to the given names.
 -/
-macro nextTk:"next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
+macro "next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
   -- Limit ref variability for incrementality; see Note [Incremental Macros]
-  withRef arrowTk `(tactic| case%$nextTk _ $args* =>%$arrowTk $tac)
+  withRef arrowTk `(tactic| case _ $args* =>%$arrowTk $tac)
 
 /-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
 syntax (name := allGoals) "all_goals " tacticSeq : tactic
@@ -910,15 +910,6 @@ macro_rules | `(tactic| trivial) => `(tactic| simp)
 -/
 syntax "trivial" : tactic
 
-/--
-`classical tacs` runs `tacs` in a scope where `Classical.propDecidable` is a low priority
-local instance.
-
-Note that `classical` is a scoping tactic: it adds the instance only within the
-scope of the tactic.
--/
-syntax (name := classical) "classical" ppDedent(tacticSeq) : tactic
-
 /--
 The `split` tactic is useful for breaking nested if-then-else and `match` expressions into separate cases.
 For a `match` expression with `n` cases, the `split` tactic generates at most `n` subgoals.

src/Lean.lean

@@ -29,6 +29,7 @@ import Lean.Server
 import Lean.ScopedEnvExtension
 import Lean.DocString
 import Lean.DeclarationRange
+import Lean.LazyInitExtension
 import Lean.LoadDynlib
 import Lean.Widget
 import Lean.Log

src/Lean/Data/HashMap.lean

@@ -46,7 +46,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property

src/Lean/Data/HashSet.lean

@@ -42,7 +42,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property

src/Lean/Data/Lsp/Capabilities.lean

@@ -54,7 +54,7 @@ structure WorkspaceEditClientCapabilities where
   deriving ToJson, FromJson
 
 structure WorkspaceClientCapabilities where
-  applyEdit? : Option Bool := none
+  applyEdit: Bool
   workspaceEdit? : Option WorkspaceEditClientCapabilities := none
   deriving ToJson, FromJson
 

src/Lean/Data/PersistentArray.lean

@@ -7,7 +7,6 @@ prelude
 import Init.Data.Array.Basic
 import Init.NotationExtra
 import Init.Data.ToString.Macro
-import Init.Data.UInt.Basic
 
 universe u v w
 

src/Lean/Data/PersistentHashMap.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.BasicAux
 import Init.Data.ToString.Macro
-import Init.Data.UInt.Basic
 
 namespace Lean
 universe u v w w'

src/Lean/Elab/BuiltinNotation.lean

@@ -135,21 +135,13 @@ open Meta
   | _                                                => Macro.throwUnsupported
 
 @[builtin_macro Lean.Parser.Term.suffices] def expandSuffices : Macro
-  | `(suffices%$tk $x:ident      : $type from $val; $body)   => `(have%$tk $x : $type := $body; $val)
-  | `(suffices%$tk _%$x          : $type from $val; $body)   => `(have%$tk _%$x : $type := $body; $val)
-  | `(suffices%$tk $hy:hygieneInfo $type from $val; $body)   => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
-  | `(suffices%$tk $x:ident      : $type $b:byTactic'; $body) =>
-    -- Pass on `SourceInfo` of `b` to `have`. This is necessary to display the goal state in the
-    -- trailing whitespace of `by` and sound since `byTactic` and `byTactic'` are identical.
-    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
-    `(have%$tk $x : $type := $body; $b:byTactic)
-  | `(suffices%$tk _%$x          : $type $b:byTactic'; $body) =>
-    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
-    `(have%$tk _%$x : $type := $body; $b:byTactic)
-  | `(suffices%$tk $hy:hygieneInfo $type $b:byTactic'; $body) =>
-    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
-    `(have%$tk $hy:hygieneInfo : $type := $body; $b:byTactic)
-  | _ => Macro.throwUnsupported
+  | `(suffices%$tk $x:ident      : $type from $val; $body)            => `(have%$tk $x : $type := $body; $val)
+  | `(suffices%$tk _%$x          : $type from $val; $body)            => `(have%$tk _%$x : $type := $body; $val)
+  | `(suffices%$tk $hy:hygieneInfo $type from $val; $body)            => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
+  | `(suffices%$tk $x:ident      : $type by%$b $tac:tacticSeq; $body) => `(have%$tk $x : $type := $body; by%$b $tac)
+  | `(suffices%$tk _%$x          : $type by%$b $tac:tacticSeq; $body) => `(have%$tk _%$x : $type := $body; by%$b $tac)
+  | `(suffices%$tk $hy:hygieneInfo $type by%$b $tac:tacticSeq; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; by%$b $tac)
+  | _                                                                 => Macro.throwUnsupported
 
 open Lean.Parser in
 private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do

src/Lean/Elab/Command.lean

@@ -532,12 +532,11 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     let mut msgs := (← get).messages
     for tree in (← getInfoTrees) do
       trace[Elab.info] (← tree.format)
-    if (← isTracingEnabledFor `Elab.snapshotTree) then
-      if let some snap := (← read).snap? then
-        -- We can assume that the root command snapshot is not involved in parallelism yet, so this
-        -- should be true iff the command supports incrementality
-        if (← IO.hasFinished snap.new.result) then
-          liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace
+    if let some snap := (← read).snap? then
+      -- We can assume that the root command snapshot is not involved in parallelism yet, so this
+      -- should be true iff the command supports incrementality
+      if (← IO.hasFinished snap.new.result) then
+        liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace
     modify fun st => { st with
       messages := initMsgs ++ msgs
       infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees }

src/Lean/Elab/LetRec.lean

@@ -90,7 +90,6 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
       for i in [0:view.binderIds.size] do
         addLocalVarInfo view.binderIds[i]! xs[i]!
       withDeclName view.declName do
-        withInfoContext' view.valStx (mkInfo := mkTermInfo `MutualDef.body view.valStx) do
          let value ← elabTermEnsuringType view.valStx type
          mkLambdaFVars xs value
 

src/Lean/Elab/MutualDef.lean

@@ -410,15 +410,11 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
           -- skip auto-bound prefix in `xs`
           addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]!
         let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do
-          -- Store instantiated body in info tree for the benefit of the unused variables linter
-          -- and other metaprograms that may want to inspect it without paying for the instantiation
-          -- again
-          withInfoContext' valStx (mkInfo := mkTermInfo `MutualDef.body valStx) do
-            -- synthesize mvars here to force the top-level tactic block (if any) to run
-            let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
-            -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
-            -- leads to more section variables being included than necessary
-            instantiateMVarsProfiling val
+          -- synthesize mvars here to force the top-level tactic block (if any) to run
+          elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
+        -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
+        -- leads to more section variables being included than necessary
+        let val ← instantiateMVarsProfiling val
         let val ← mkLambdaFVars xs val
         if linter.unusedSectionVars.get (← getOptions) && !header.type.hasSorry && !val.hasSorry then
           let unusedVars ← vars.filterMapM fun var => do

src/Lean/Elab/Tactic.lean

@@ -43,4 +43,3 @@ import Lean.Elab.Tactic.Rewrites
 import Lean.Elab.Tactic.DiscrTreeKey
 import Lean.Elab.Tactic.BVDecide
 import Lean.Elab.Tactic.BoolToPropSimps
-import Lean.Elab.Tactic.Classical

src/Lean/Elab/Tactic/Basic.lean

@@ -52,7 +52,6 @@ instance : Monad TacticM :=
 instance : Inhabited (TacticM α) where
   default := fun _ _ => default
 
-/-- Returns the list of goals. Goals may or may not already be assigned. -/
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals
 
@@ -301,22 +300,13 @@ instance : MonadBacktrack SavedState TacticM where
   saveState := Tactic.saveState
   restoreState b := b.restore
 
-/--
-Non-backtracking `try`/`catch`.
--/
 @[inline] protected def tryCatch {α} (x : TacticM α) (h : Exception → TacticM α) : TacticM α := do
-  try x catch ex => h ex
-
-/--
-Backtracking `try`/`catch`. This is used for the `MonadExcept` instance for `TacticM`.
--/
-@[inline] protected def tryCatchRestore {α} (x : TacticM α) (h : Exception → TacticM α) : TacticM α := do
   let b ← saveState
   try x catch ex => b.restore; h ex
 
 instance : MonadExcept Exception TacticM where
   throw    := throw
-  tryCatch := Tactic.tryCatchRestore
+  tryCatch := Tactic.tryCatch
 
 /-- Execute `x` with error recovery disabled -/
 def withoutRecover (x : TacticM α) : TacticM α :=
@@ -352,26 +342,12 @@ def adaptExpander (exp : Syntax → TacticM Syntax) : Tactic := fun stx => do
   let stx' ← exp stx
   withMacroExpansion stx stx' $ evalTactic stx'
 
-/-- Add the given goal to the front of the current list of goals. -/
-def pushGoal (mvarId : MVarId) : TacticM Unit :=
-  modify fun s => { s with goals := mvarId :: s.goals }
-
-/-- Add the given goals to the front of the current list of goals. -/
-def pushGoals (mvarIds : List MVarId) : TacticM Unit :=
-  modify fun s => { s with goals := mvarIds ++ s.goals }
-
-/-- Add the given goals at the end of the current list of goals. -/
+/-- Add the given goals at the end of the current goals collection. -/
 def appendGoals (mvarIds : List MVarId) : TacticM Unit :=
   modify fun s => { s with goals := s.goals ++ mvarIds }
 
-/--
-Discard the first goal and replace it by the given list of goals,
-keeping the other goals. This is used in conjunction with `getMainGoal`.
-
-Contract: between `getMainGoal` and `replaceMainGoal`, nothing manipulates the goal list.
-
-See also `Lean.Elab.Tactic.popMainGoal` and `Lean.Elab.Tactic.pushGoal`/`Lean.Elab.Tactic.pushGoal` for another interface.
--/
+/-- Discard the first goal and replace it by the given list of goals,
+keeping the other goals. -/
 def replaceMainGoal (mvarIds : List MVarId) : TacticM Unit := do
   let (_ :: mvarIds') ← getGoals | throwNoGoalsToBeSolved
   modify fun _ => { goals := mvarIds ++ mvarIds' }
@@ -389,16 +365,6 @@ where
         setGoals (mvarId :: mvarIds)
         return mvarId
 
-/--
-Return the first goal, and remove it from the goal list.
-
-See also: `Lean.Elab.Tactic.pushGoal` and `Lean.Elab.Tactic.pushGoals`.
--/
-def popMainGoal : TacticM MVarId := do
-  let mvarId ← getMainGoal
-  replaceMainGoal []
-  return mvarId
-
 /-- Return the main goal metavariable declaration. -/
 def getMainDecl : TacticM MetavarDecl := do
   (← getMainGoal).getDecl

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -520,7 +520,7 @@ where
 
 @[builtin_tactic «case», builtin_incremental]
 def evalCase : Tactic
-  | stx@`(tactic| case%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
+  | stx@`(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
     -- disable incrementality if body is run multiple times
     Term.withoutTacticIncrementality (tag.size > 1) do
       for tag in tag, hs in hs do
@@ -528,20 +528,20 @@ def evalCase : Tactic
         let g ← renameInaccessibles g hs
         setGoals [g]
         g.setTag Name.anonymous
-        withCaseRef arr tac <| closeUsingOrAdmit <| withTacticInfoContext (mkNullNode #[caseTk, arr]) <|
+        withCaseRef arr tac <| closeUsingOrAdmit <| withTacticInfoContext stx <|
           Term.withNarrowedArgTacticReuse (argIdx := 3) (evalTactic ·) stx
         setGoals gs
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic «case'»] def evalCase' : Tactic
-  | `(tactic| case'%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
+  | `(tactic| case' $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
     let mut acc := #[]
     for tag in tag, hs in hs do
       let (g, gs) ← getCaseGoals tag
       let g ← renameInaccessibles g hs
       let mvarTag ← g.getTag
       setGoals [g]
-      withCaseRef arr tac <| withTacticInfoContext (mkNullNode #[caseTk, arr]) <| evalTactic tac
+      withCaseRef arr tac (evalTactic tac)
       let gs' ← getUnsolvedGoals
       if let [g'] := gs' then
         g'.setTag mvarTag

src/Lean/Elab/Tactic/Calc.lean

@@ -14,9 +14,9 @@ open Meta
 @[builtin_tactic Lean.calcTactic]
 def evalCalc : Tactic := fun stx => withMainContext do
   let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
-  let target := (← getMainTarget).consumeMData
-  let tag ← getMainTag
-  let (val, mvarIds) ← withCollectingNewGoalsFrom (parentTag := tag) (tagSuffix := `calc) do
+  let (val, mvarIds) ← withCollectingNewGoalsFrom (tagSuffix := `calc) do
+    let target := (← getMainTarget).consumeMData
+    let tag ← getMainTag
     runTermElab do
     let mut val ← Term.elabCalcSteps steps
     let mut valType ← instantiateMVars (← inferType val)

src/Lean/Elab/Tactic/Classical.lean

@@ -1,34 +0,0 @@
-/-
-Copyright (c) 2021 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Kim Morrison
--/
-prelude
-import Lean.Elab.Tactic.Basic
-
-/-! # `classical` tactic -/
-
-namespace Lean.Elab.Tactic
-open Lean Meta Elab.Tactic
-
-/--
-`classical t` runs `t` in a scope where `Classical.propDecidable` is a low priority
-local instance.
--/
-def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t : m α) :
-    m α := do
-  modifyEnv Meta.instanceExtension.pushScope
-  Meta.addInstance ``Classical.propDecidable .local 10
-  try
-    t
-  finally
-    modifyEnv Meta.instanceExtension.popScope
-
-@[builtin_tactic Lean.Parser.Tactic.classical]
-def evalClassical : Tactic := fun stx => do
-  match stx with
-  | `(tactic| classical $tacs:tacticSeq) =>
-     classical <| Elab.Tactic.evalTactic tacs
-  | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -56,6 +56,11 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpo
       Term.throwTypeMismatchError none expectedType eType e
     return e
 
+/-- Try to close main goal using `x target`, where `target` is the type of the main goal.  -/
+def closeMainGoalUsing (tacName : Name) (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit :=
+  withMainContext do
+    closeMainGoal (tacName := tacName) (checkUnassigned := checkUnassigned) (← x (← getMainTarget))
+
 def logUnassignedAndAbort (mvarIds : Array MVarId) : TacticM Unit := do
    if (← Term.logUnassignedUsingErrorInfos mvarIds) then
      throwAbortTactic
@@ -64,37 +69,14 @@ def filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) : MetaM (Ar
   let mctx ← getMCtx
   return mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved
 
-/--
-Try to close main goal using `x target tag`, where `target` is the type of the main goal and `tag` is its user name.
-
-If `checkNewUnassigned` is true, then throws an error if the resulting value has metavariables that were created during the execution of `x`.
-If it is false, then it is the responsibility of `x` to add such metavariables to the goal list.
-
-During the execution of `x`:
-* The local context is that of the main goal.
-* The goal list has the main goal removed.
-* It is allowable to modify the goal list, for example with `Lean.Elab.Tactic.pushGoals`.
-
-On failure, the main goal remains at the front of the goal list.
--/
-def closeMainGoalUsing (tacName : Name) (x : Expr → Name → TacticM Expr) (checkNewUnassigned := true) : TacticM Unit := do
-  let mvarCounterSaved := (← getMCtx).mvarCounter
-  let mvarId ← popMainGoal
-  Tactic.tryCatch
-    (mvarId.withContext do
-      let val ← x (← mvarId.getType) (← mvarId.getTag)
-      if checkNewUnassigned then
-        let mvars ← filterOldMVars (← getMVars val) mvarCounterSaved
-        logUnassignedAndAbort mvars
-      unless (← mvarId.checkedAssign val) do
-        throwTacticEx tacName mvarId m!"attempting to close the goal using{indentExpr val}\nthis is often due occurs-check failure")
-    (fun ex => do
-      pushGoal mvarId
-      throw ex)
-
 @[builtin_tactic «exact»] def evalExact : Tactic := fun stx => do
   match stx with
-  | `(tactic| exact $e) => closeMainGoalUsing `exact fun type _ => elabTermEnsuringType e type
+  | `(tactic| exact $e) =>
+    closeMainGoalUsing `exact (checkUnassigned := false) fun type => do
+      let mvarCounterSaved := (← getMCtx).mvarCounter
+      let r ← elabTermEnsuringType e type
+      logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
+      return r
   | _ => throwUnsupportedSyntax
 
 def sortMVarIdArrayByIndex [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) : m (Array MVarId) := do
@@ -111,12 +93,9 @@ def sortMVarIdsByIndex [MonadMCtx m] [Monad m] (mvarIds : List MVarId) : m (List
   return (← sortMVarIdArrayByIndex mvarIds.toArray).toList
 
 /--
-Execute `k`, and collect new "holes" in the resulting expression.
-
-* `parentTag` and `tagSuffix` are used to tag untagged goals with `Lean.Elab.Tactic.tagUntaggedGoals`.
-* If `allowNaturalHoles` is true, then `_`'s are allowed and create new goals.
+  Execute `k`, and collect new "holes" in the resulting expression.
 -/
-def withCollectingNewGoalsFrom (k : TacticM Expr) (parentTag : Name) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) :=
+def withCollectingNewGoalsFrom (k : TacticM Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) :=
   /-
   When `allowNaturalHoles = true`, unassigned holes should become new metavariables, including `_`s.
   Thus, we set `holesAsSyntheticOpaque` to true if it is not already set to `true`.
@@ -165,7 +144,7 @@ where
     appear in the `.lean` file. We should tell users to prefer tagged goals.
     -/
     let newMVarIds ← sortMVarIdsByIndex newMVarIds.toList
-    tagUntaggedGoals parentTag tagSuffix newMVarIds
+    tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
     return (val, newMVarIds)
 
 /-- Elaborates `stx` and collects the `MVarId`s of any holes that were created during elaboration.
@@ -174,8 +153,8 @@ With `allowNaturalHoles := false` (the default), any new natural holes (`_`) whi
 be synthesized during elaboration cause `elabTermWithHoles` to fail. (Natural goals appearing in
 `stx` which were created prior to elaboration are permitted.)
 
-Unnamed `MVarId`s are renamed to share the tag `parentTag?` (or the main goal's tag if `parentTag?` is `none`).
-If multiple unnamed goals are encountered, `tagSuffix` is appended to this tag along with a numerical index.
+Unnamed `MVarId`s are renamed to share the main goal's tag. If multiple unnamed goals are
+encountered, `tagSuffix` is appended to the main goal's tag along with a numerical index.
 
 Note:
 * Previously-created `MVarId`s which appear in `stx` are not returned.
@@ -184,8 +163,8 @@ metavariables.
 * When `allowNaturalHoles := true`, `stx` is elaborated under `withAssignableSyntheticOpaque`,
 meaning that `.syntheticOpaque` metavariables might be assigned during elaboration. This is a
 consequence of the implementation. -/
-def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) (parentTag? : Option Name := none) : TacticM (Expr × List MVarId) := do
-  withCollectingNewGoalsFrom (elabTermEnsuringType stx expectedType?) (← parentTag?.getDM getMainTag) tagSuffix allowNaturalHoles
+def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
+  withCollectingNewGoalsFrom (elabTermEnsuringType stx expectedType?) tagSuffix allowNaturalHoles
 
 /-- If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables.
    Recall that "natutal" metavariables are created for explicit holes `_` and implicit arguments. They are meant to be
@@ -416,7 +395,7 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := wi
   return inst
 
 def evalDecideCore (tacticName : Name) (kernelOnly : Bool) : TacticM Unit :=
-  closeMainGoalUsing tacticName fun expectedType _ => do
+  closeMainGoalUsing tacticName fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType
     let pf ← mkDecideProof expectedType
     -- Get instance from `pf`
@@ -522,7 +501,7 @@ private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Na
   pure auxName
 
 @[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ =>
-  closeMainGoalUsing `nativeDecide fun expectedType _ => do
+  closeMainGoalUsing `nativeDecide fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d

src/Lean/Elab/Tactic/Induction.lean

@@ -27,10 +27,8 @@ open Meta
   syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq)
   ```
 -/
-private def getAltLhses (alt : Syntax) : Syntax :=
-  alt[0]
 private def getFirstAltLhs (alt : Syntax) : Syntax :=
-  (getAltLhses alt)[0]
+  alt[0][0]
 /-- Return `inductionAlt` name. It assumes `alt` does not have multiple `inductionAltLHS` -/
 private def getAltName (alt : Syntax) : Name :=
   let lhs := getFirstAltLhs alt
@@ -72,9 +70,7 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : Tactic
       let goals ← getGoals
       try
         setGoals [mvarId]
-        closeUsingOrAdmit <|
-          withTacticInfoContext (mkNullNode #[getAltLhses alt, getAltDArrow alt]) <|
-            (addInfo *> evalTactic rhs)
+        closeUsingOrAdmit (withTacticInfoContext alt (addInfo *> evalTactic rhs))
       finally
         setGoals goals
 

src/Lean/Expr.lean

@@ -1038,14 +1038,6 @@ def getForallBinderNames : Expr → List Name
   | forallE n _ b _ => n :: getForallBinderNames b
   | _ => []
 
-/--
-Returns the number of leading `∀` binders of an expression. Ignores metadata.
--/
-def getNumHeadForalls : Expr → Nat
-  | mdata _ b => getNumHeadForalls b
-  | forallE _ _ body _ => getNumHeadForalls body + 1
-  | _ => 0
-
 /--
 If the given expression is a sequence of
 function applications `f a₁ .. aₙ`, return `f`.
@@ -1093,16 +1085,6 @@ private def getAppNumArgsAux : Expr → Nat → Nat
 def getAppNumArgs (e : Expr) : Nat :=
   getAppNumArgsAux e 0
 
-/-- Like `getAppNumArgs` but ignores metadata. -/
-def getAppNumArgs' (e : Expr) : Nat :=
-  go e 0
-where
-  /-- Auxiliary definition for `getAppNumArgs'`. -/
-  go : Expr → Nat → Nat
-    | mdata _ b, n => go b n
-    | app f _  , n => go f (n + 1)
-    | _        , n => n
-
 /--
 Like `Lean.Expr.getAppFn` but assumes the application has up to `maxArgs` arguments.
 If there are any more arguments than this, then they are returned by `getAppFn` as part of the function.

src/Lean/Language/Basic.lean

@@ -243,16 +243,11 @@ instance : ToSnapshotTree SnapshotLeaf where
 structure DynamicSnapshot where
   /-- Concrete snapshot value as `Dynamic`. -/
   val  : Dynamic
-  /--
-  Snapshot tree retrieved from `val` before erasure. We do thunk even the first level as accessing
-  it too early can create some unnecessary tasks from `toSnapshotTree` that are otherwise avoided by
-  `(sync := true)` when accessing only after elaboration has finished. Early access can even lead to
-  deadlocks when later forcing these unnecessary tasks on a starved thread pool.
-  -/
-  tree : Thunk SnapshotTree
+  /-- Snapshot tree retrieved from `val` before erasure. -/
+  tree : SnapshotTree
 
 instance : ToSnapshotTree DynamicSnapshot where
-  toSnapshotTree s := s.tree.get
+  toSnapshotTree s := s.tree
 
 /-- Creates a `DynamicSnapshot` from a typed snapshot value. -/
 def DynamicSnapshot.ofTyped [TypeName α] [ToSnapshotTree α] (val : α) : DynamicSnapshot where

src/Lean/LazyInitExtension.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.MonadEnv
+
+namespace Lean
+
+structure LazyInitExtension (m : Type → Type) (α : Type) where
+  ext : EnvExtension (Option α)
+  fn  : m α
+
+instance [Monad m] [Inhabited α] : Inhabited (LazyInitExtension m α) where
+  default := {
+    ext := default
+    fn  := pure default
+  }
+
+/--
+  Register an environment extension for storing the result of `fn`.
+  We initialize the extension with `none`, and `fn` is executed the
+  first time `LazyInit.get` is executed.
+
+  This kind of extension is useful for avoiding work duplication in
+  scenarios where a thunk cannot be used because the computation depends
+  on state from the `m` monad. For example, we may want to "cache" a collection
+  of theorems as a `SimpLemmas` object.  -/
+def registerLazyInitExtension (fn : m α) : IO (LazyInitExtension m α) := do
+  let ext ← registerEnvExtension (pure none)
+  return { ext, fn }
+
+def LazyInitExtension.get [MonadEnv m] [Monad m] (init : LazyInitExtension m α) : m α := do
+  match init.ext.getState (← getEnv) with
+  | some a => return a
+  | none   =>
+    let a ← init.fn
+    modifyEnv fun env => init.ext.setState env (some a)
+    return a
+
+end Lean

src/Lean/Linter/ConstructorAsVariable.lean

@@ -37,7 +37,7 @@ def constructorNameAsVariable : Linter where
     let warnings : IO.Ref (Std.HashMap String.Range (Syntax × Name × Name)) ← IO.mkRef {}
 
     for tree in infoTrees do
-      tree.visitM' (postNode := fun ci info _ => do
+      tree.visitM' (preNode := fun ci info _ => do
         match info with
         | .ofTermInfo ti =>
           match ti.expr with

src/Lean/Linter/UnusedVariables.lean

@@ -10,55 +10,41 @@ set_option linter.missingDocs true -- keep it documented
 
 /-! # Unused variable Linter
 
-This file implements the unused variable linter, which runs automatically on all
-commands and reports any local variables that are never referred to, using
-information from the info tree.
+This file implements the unused variable linter, which runs automatically on all commands
+and reports any local variables that are never referred to, using information from the info tree.
 
-It is not immediately obvious but this is a surprisingly expensive check without
-some optimizations.  The main complication is that it can be difficult to
-determine what constitutes a "use" apart from direct references to a variable
-that we can easily find in the info tree.  For example, we would like this to be
-considered a use of `x`: 
+It is not immediately obvious but this is a surprisingly expensive check without some optimizations.
+The main complication is that it can be difficult to determine what constitutes a "use".
+For example, we would like this to be considered a use of `x`:
 ```
 def foo (x : Nat) : Nat := by assumption
 ```
 
-The final proof term is `fun x => x` so clearly `x` was used, but we can't make
-use of this because the final proof term is after we have abstracted over the
-original `fvar` for `x`. Instead, we make sure to store the proof term before
-abstraction but after instantiation of mvars in the info tree and retrieve it in
-the linter. Using the instantiated term is very important as redoing that step
-in the linter can be prohibitively expensive. The downside of special-casing the
-definition body in this way is that while it works for parameters, it does not
-work for local variables in the body, so we ignore them by default if any tactic
-infos are present (`linter.unusedVariables.analyzeTactics`).
+The final proof term is `fun x => x` so clearly `x` was used, but we can't make use of this because
+the final proof term is after we have abstracted over the original `fvar` for `x`. If we look
+further into the tactic state we can see the `fvar` show up in the instantiation to the original
+goal metavariable `?m : Nat := x`, but it is not always the case that we can follow metavariable
+instantiations to determine what happened after the fact, because tactics might skip the goal
+metavariable and instantiate some other metavariable created prior to it instead.
 
-If we do turn on this option and look further into the tactic state, we can see
-the `fvar` show up in the instantiation to the original goal metavariable
-`?m : Nat := x`, but it is not always the case that we can follow metavariable
-instantiations to determine what happened after the fact, because tactics might
-skip the goal metavariable and instantiate some other metavariable created prior
-to it instead.  Instead, we use a (much more expensive) overapproximation, which
-is just to look through the entire metavariable context looking for occurrences
-of `x`. We use caching to ensure that this is still linear in the size of the
-info tree, even though there are many metavariable contexts in all the
-intermediate stages of elaboration; these are highly similar and make use of
-`PersistentHashMap` so there is a lot of subterm sharing we can take advantage
-of.
+Instead, we use a (much more expensive) overapproximation, which is just to look through the entire
+metavariable context looking for occurrences of `x`. We use caching to ensure that this is still
+linear in the size of the info tree, even though there are many metavariable contexts in all the
+intermediate stages of elaboration; these are highly similar and make use of `PersistentHashMap`
+so there is a lot of subterm sharing we can take advantage of.
 
 ## The `@[unused_variables_ignore_fn]` attribute
 
-Some occurrences of variables are deliberately unused, or at least we don't want
-to lint on unused variables in these positions. For example:
+Some occurrences of variables are deliberately unused, or at least we don't want to lint on unused
+variables in these positions. For example:
 
 ```
 def foo (x : Nat) : (y : Nat) → Nat := fun _ => x
                   -- ^ don't lint this unused variable because it is public API
 ```
 
-They are generally a syntactic criterion, so we allow adding custom
-`IgnoreFunction`s so that external syntax can also opt in to lint suppression,
-like so:
+They are generally a syntactic criterion, so we allow adding custom `IgnoreFunction`s so that
+external syntax can also opt in to lint suppression, like so:
 
 ```
 macro (name := foobarKind) "foobar " name:ident : command => `(def foo ($name : Nat) := 0)
@@ -91,17 +77,6 @@ register_builtin_option linter.unusedVariables.patternVars : Bool := {
   defValue := true,
   descr := "enable the 'unused variables' linter to mark unused pattern variables"
 }
-/-- Enables linting variables defined in tactic blocks, may be expensive for complex proofs -/
-register_builtin_option linter.unusedVariables.analyzeTactics : Bool := {
-  defValue := false
-  descr := "enable analysis of local variables in presence of tactic proofs\
-          \n\
-          \nBy default, the linter will limit itself to linting a declaration's parameters \
-            whenever tactic proofs are present as these can be expensive to analyze. Enabling this \
-            option extends linting to local variables both inside and outside tactic proofs, \
-            though it can also lead to some false negatives as intermediate tactic states may \
-            reference some variables without the declaration ultimately depending on them."
-}
 
 /-- Gets the status of `linter.unusedVariables` -/
 def getLinterUnusedVariables (o : Options) : Bool :=
@@ -381,82 +356,55 @@ structure References where
 
 /-- Collect information from the `infoTrees` into `References`.
 See `References` for more information about the return value. -/
-partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
-    StateRefT References IO Unit := ReaderT.run (r := false) <| go infoTrees none
+def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
+    StateRefT References IO Unit := do
+  for tree in infoTrees do
+    tree.visitM' (preNode := fun ci info _ => do
+      match info with
+      | .ofTermInfo ti =>
+        match ti.expr with
+        | .const .. =>
+          if ti.isBinder then
+            let some range := info.range? | return
+            let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
+            modify fun s => { s with constDecls := s.constDecls.insert range }
+        | .fvar id .. =>
+          let some range := info.range? | return
+          let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
+          if ti.isBinder then
+            -- This is a local variable declaration.
+            let some ldecl := ti.lctx.find? id | return
+            -- Skip declarations which are outside the command syntax range, like `variable`s
+            -- (it would be confusing to lint these), or those which are macro-generated
+            if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return
+            let opts := ci.options
+            -- we have to check for the option again here because it can be set locally
+            if !getLinterUnusedVariables opts then return
+            let stx := skipDeclIdIfPresent info.stx
+            if let .str _ s := stx.getId then
+              -- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
+              -- This is the suggested way to silence the warning
+              if s.startsWith "_" then return
+            -- Record this either as a new `fvarDefs`, or an alias of an existing one
+            modify fun s =>
+              if let some ref := s.fvarDefs[range]? then
+                { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
+              else
+                { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
+          else
+            -- Found a direct use, keep track of it
+            modify fun s => { s with fvarUses := s.fvarUses.insert id }
+        | _ => pure ()
+      | .ofTacticInfo ti =>
+        -- Keep track of the `MetavarContext` after a tactic for later
+        modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
+      | .ofFVarAliasInfo i =>
+        -- record any aliases we find
+        modify fun s =>
+          let id := followAliases s.fvarAliases i.baseId
+          { s with fvarAliases := s.fvarAliases.insert i.id id }
+      | _ => pure ())
 where
-  go infoTrees ctx? := do
-    for tree in infoTrees do
-      tree.visitM' (ctx? := ctx?) (preNode := fun ci info children => do
-        -- set if `analyzeTactics` is unset, tactic infos are present, and we're inside the body
-        let ignored ← read
-        match info with
-        | .ofTermInfo ti =>
-          -- NOTE: we have to do this check *before* `ignored` because nested bodies (e.g. from
-          -- nested `let rec`s) do need to be included to find all `Expr` uses of the top-level
-          -- parameters
-          if ti.elaborator == `MutualDef.body &&
-              !linter.unusedVariables.analyzeTactics.get ci.options then
-            -- the body is the only `Expr` we will analyze in this case
-            -- NOTE: we include it even if no tactics are present as at least for parameters we want
-            -- to lint only truly unused binders
-            let (e, _) := instantiateMVarsCore ci.mctx ti.expr
-            modify fun s => { s with
-              assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
-            let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
-            withReader (· || tacticsPresent) do
-              go children.toArray ci
-            return false
-          if ignored then return true
-          match ti.expr with
-          | .const .. =>
-            if ti.isBinder then
-              let some range := info.range? | return true
-              let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
-              modify fun s => { s with constDecls := s.constDecls.insert range }
-          | .fvar id .. =>
-            let some range := info.range? | return true
-            let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
-            if ti.isBinder then
-              -- This is a local variable declaration.
-              if ignored then return true
-              let some ldecl := ti.lctx.find? id | return true
-              -- Skip declarations which are outside the command syntax range, like `variable`s
-              -- (it would be confusing to lint these), or those which are macro-generated
-              if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return true
-              let opts := ci.options
-              -- we have to check for the option again here because it can be set locally
-              if !getLinterUnusedVariables opts then return true
-              let stx := skipDeclIdIfPresent info.stx
-              if let .str _ s := stx.getId then
-                -- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
-                -- This is the suggested way to silence the warning
-                if s.startsWith "_" then return true
-              -- Record this either as a new `fvarDefs`, or an alias of an existing one
-              modify fun s =>
-                if let some ref := s.fvarDefs[range]? then
-                  { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
-                else
-                  { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
-            else
-              -- Found a direct use, keep track of it
-              modify fun s => { s with fvarUses := s.fvarUses.insert id }
-          | _ => pure ()
-          return true
-        | .ofTacticInfo ti =>
-          -- When ignoring new binders, no need to look at intermediate tactic states either as
-          -- references to binders outside the body will be covered by the body `Expr`
-          if ignored then return true
-          -- Keep track of the `MetavarContext` after a tactic for later
-          modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
-          return true
-        | .ofFVarAliasInfo i =>
-          if ignored then return true
-          -- record any aliases we find
-          modify fun s =>
-            let id := followAliases s.fvarAliases i.baseId
-            { s with fvarAliases := s.fvarAliases.insert i.id id }
-          return true
-        | _ => return true)
   /-- Since declarations attach the declaration info to the `declId`,
   we skip that to get to the `.ident` if possible. -/
   skipDeclIdIfPresent (stx : Syntax) : Syntax :=
@@ -545,7 +493,7 @@ def unusedVariables : Linter where
         -- collect additional `fvarUses` from tactic assignments
         visitAssignments (← IO.mkRef {}) fvarUsesRef s.assignments
         -- Resolve potential aliases again to preserve `fvarUsesRef` invariant
-        fvarUsesRef.modify fun fvarUses => fvarUses.toArray.map getCanonVar |> .insertMany {}
+        fvarUsesRef.modify fun fvarUses => fvarUses.fold (·.insert <| getCanonVar ·) {}
         initializedMVars := true
         let fvarUses ← fvarUsesRef.get
         -- Redo the initial check because `fvarUses` could be bigger now

src/Lean/Meta/DiscrTree.lean

@@ -76,7 +76,7 @@ def Key.format : Key → Format
   | .const k _       => Std.format k
   | .proj s i _      => Std.format s ++ "." ++ Std.format i
   | .fvar k _        => Std.format k.name
-  | .arrow           => "∀"
+  | .arrow           => "→"
 
 instance : ToFormat Key := ⟨Key.format⟩
 
@@ -113,8 +113,7 @@ where
       mkApp m!"{mkFVar fvarId}" (← goN nargs) parenIfNonAtomic
     | .proj _ i nargs =>
       mkApp m!"{← go}.{i+1}" (← goN nargs) parenIfNonAtomic
-    | .arrow =>
-      mkApp m!"∀ " (← goN 1) parenIfNonAtomic
+    | .arrow => return "<arrow>"
     | .star => return "_"
     | .other => return "<other>"
     | .lit (.natVal v) => return m!"{v}"
@@ -130,15 +129,21 @@ def Key.arity : Key → Nat
   | .const _ a  => a
   | .fvar _ a   => a
   /-
-  Remark: `.arrow` used to have arity 2, and was used to encode only **non**-dependent
-  arrows. However, this feature was a recurrent source of bugs. For example, a
-  theorem about a dependent arrow can be applied to a non-dependent one. The
-  reverse direction may also happen. See issue #2835. Therefore, `.arrow` was made
-  to have arity 0. But this throws away easy to use information, and makes it so
-  that ∀ and ∃ behave quite differently. So now `.arrow` at least indexes the
-  domain of the forall (whether dependent or non-dependent).
+  Remark: `.arrow` used to have arity 2, and was used to encode non-dependent arrows.
+  However, this feature was a recurrent source of bugs. For example, a theorem about
+  a dependent arrow can be applied to a non-dependent one. The reverse direction may
+  also happen. See issue #2835.
+  ```
+  -- A theorem about the non-dependent arrow `a → a`
+  theorem imp_self' {a : Prop} : (a → a) ↔ True := ⟨fun _ => trivial, fun _ => id⟩
+
+  -- can be applied to the dependent one `(h : P a) → P (f h)`.
+  example {α : Prop} {P : α → Prop} {f : ∀ {a}, P a → α} {a : α} : (h : P a) → P (f h) := by
+    simp only [imp_self']
+  ```
+  Thus, we now index dependent and non-dependent arrows using the key `.arrow` with arity 0.
   -/
-  | .arrow      => 1
+  | .arrow      => 0
   | .proj _ _ a => 1 + a
   | _           => 0
 
@@ -417,8 +422,7 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : Whnf
         return (.other, todo)
       else
         return (.star, todo)
-    | .forallE _n d _ _ =>
-      return (.arrow, todo.push d)
+    | .forallE .. => return (.arrow, todo)
     | _ => return (.other, todo)
 
 @[inherit_doc pushArgs]
@@ -577,7 +581,7 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
   | .proj s i a .. =>
     let nargs := e.getAppNumArgs
     return (.proj s i nargs, #[a] ++ e.getAppRevArgs)
-  | .forallE _ d _ _ => return (.arrow, #[d])
+  | .forallE .. => return (.arrow, #[])
   | _ => return (.other, #[])
 
 private abbrev getMatchKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) :=

src/Lean/Meta/RecursorInfo.lean

@@ -67,6 +67,29 @@ instance : ToString RecursorInfo := ⟨fun info =>
 
 end RecursorInfo
 
+private def mkRecursorInfoForKernelRec (declName : Name) (val : RecursorVal) : MetaM RecursorInfo := do
+  let ival ← getConstInfoInduct val.getInduct
+  let numLParams    := ival.levelParams.length
+  let univLevelPos  := (List.range numLParams).map RecursorUnivLevelPos.majorType
+  let univLevelPos  := if val.levelParams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos
+  let produceMotive := List.replicate val.numMinors true
+  let paramsPos     := (List.range val.numParams).map some
+  let indicesPos    := (List.range val.numIndices).map fun pos => val.numParams + pos
+  let numArgs       := val.numIndices + val.numParams + val.numMinors + val.numMotives + 1
+  pure {
+    recursorName  := declName,
+    typeName      := val.getInduct,
+    univLevelPos  := univLevelPos,
+    majorPos      := val.getMajorIdx,
+    depElim       := true,
+    recursive     := ival.isRec,
+    produceMotive := produceMotive,
+    paramsPos     := paramsPos,
+    indicesPos    := indicesPos,
+    numArgs       := numArgs
+  }
+
+
 private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat) : MetaM (Option Nat) :=
   if majorPos?.isSome then pure majorPos?
   else do
@@ -179,8 +202,8 @@ private def checkMotiveResultType (declName : Name) (motiveArgs : Array Expr) (m
   if !motiveResultType.isSort || motiveArgs.size != motiveTypeParams.size then
     throwError "invalid user defined recursor '{declName}', motive must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant"
 
-private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat) : MetaM RecursorInfo := do
-  let cinfo ← getConstInfo declName
+private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) : MetaM RecursorInfo := do
+  let declName := cinfo.name
   let majorPos? ← getMajorPosIfAuxRecursor? declName majorPos?
   forallTelescopeReducing cinfo.type fun xs type => type.withApp fun motive motiveArgs => do
     checkMotive declName motive motiveArgs
@@ -227,6 +250,12 @@ def Attribute.Recursor.getMajorPos (stx : Syntax) : AttrM Nat := do
   else
     throwErrorAt stx "unexpected attribute argument, numeral expected"
 
+private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
+  let cinfo ← getConstInfo declName
+  match cinfo with
+  | ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
+  | _                        => mkRecursorInfoAux cinfo majorPos?
+
 builtin_initialize recursorAttribute : ParametricAttribute Nat ←
   registerParametricAttribute {
     name := `recursor,
@@ -240,7 +269,11 @@ def getMajorPos? (env : Environment) (declName : Name) : Option Nat :=
   recursorAttribute.getParam? env declName
 
 def mkRecursorInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
-  let majorPos? := majorPos? <|> getMajorPos? (← getEnv) declName
-  mkRecursorInfoCore declName majorPos?
+  let cinfo ← getConstInfo declName
+  match cinfo with
+  | ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
+  | _                        => match majorPos? with
+    | none => do mkRecursorInfoAux cinfo (getMajorPos? (← getEnv) declName)
+    | _    => mkRecursorInfoAux cinfo majorPos?
 
 end Lean.Meta

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

@@ -86,63 +86,35 @@ def toACExpr (op l r : Expr) : MetaM (Array Expr × ACExpr) := do
     | PreExpr.op l r => Data.AC.Expr.op (toACExpr varMap l) (toACExpr varMap r)
     | PreExpr.var x => Data.AC.Expr.var (varMap x)
 
-/--
-In order to prevent the kernel trying to reduce the atoms of the expression, we abstract the proof
-over them. But `ac_rfl` proofs are not completely abstract in the value of the atoms – it recognizes
-neutral elements. So we have to abstract over these proofs as well.
--/
-def abstractAtoms (preContext : PreContext) (atoms : Array Expr)
-    (k : Array (Expr × Option Expr) → MetaM Expr) : MetaM Expr := do
-  let α ← inferType atoms[0]!
-  let u ← getLevel α
-  let rec go i (acc : Array (Expr × Option Expr)) (vars : Array Expr) (args : Array Expr) := do
-    if h : i < atoms.size then
-      withLocalDeclD `x α fun v => do
-        match (← getInstance ``LawfulIdentity #[preContext.op, atoms[i]]) with
-        | none =>
-          go (i+1) (acc.push (v, .none)) (vars.push v) (args.push atoms[i])
-        | some inst =>
-          withLocalDeclD `inst (mkApp3 (mkConst ``LawfulIdentity [u]) α preContext.op v) fun iv =>
-            go (i+1) (acc.push (v, .some iv)) (vars ++ #[v,iv]) (args ++ #[atoms[i], inst])
-    else
-      let proof ← k acc
-      let proof ← mkLambdaFVars vars proof
-      let proof := mkAppN proof args
-      return proof
-  go 0 #[] #[] #[]
-
 def buildNormProof (preContext : PreContext) (l r : Expr) : MetaM (Lean.Expr × Lean.Expr) := do
-  let (atoms, acExpr) ← toACExpr preContext.op l r
-  let proof ← abstractAtoms preContext atoms fun varsData => do
-    let α ← inferType atoms[0]!
-    let u ← getLevel α
-    let context ← mkContext α u varsData
-    let isNeutrals := varsData.map (·.2.isSome)
-    let vars := varsData.map (·.1)
-    let acExprNormed := Data.AC.evalList ACExpr preContext $ Data.AC.norm (preContext, isNeutrals) acExpr
-    let lhs := convert acExpr
-    let rhs := convert acExprNormed
-    let proof := mkAppN (mkConst ``Context.eq_of_norm [u]) #[α, context, lhs, rhs, ←mkEqRefl (mkConst ``Bool.true)]
-    let proofType ← mkEq (convertTarget vars acExpr) (convertTarget vars acExprNormed)
-    let proof ← mkExpectedTypeHint proof proofType
-    return proof
-  let some (_, _, tgt) := (← inferType proof).eq? | panic! "unexpected proof type"
+  let (vars, acExpr) ← toACExpr preContext.op l r
+
+  let α ← inferType vars[0]!
+  let u ← getLevel α
+  let (isNeutrals, context) ← mkContext α u vars
+  let acExprNormed := Data.AC.evalList ACExpr preContext $ Data.AC.norm (preContext, isNeutrals) acExpr
+  let tgt := convertTarget vars acExprNormed
+  let lhs := convert acExpr
+  let rhs := convert acExprNormed
+  let proof := mkAppN (mkConst ``Context.eq_of_norm [u]) #[α, context, lhs, rhs, ←mkEqRefl (mkConst ``Bool.true)]
   return (proof, tgt)
 where
-  mkContext (α : Expr) (u : Level) (vars : Array (Expr × Option Expr)) : MetaM Expr := do
-    let arbitrary := vars[0]!.1
+  mkContext (α : Expr) (u : Level) (vars : Array Expr) : MetaM (Array Bool × Expr) := do
+    let arbitrary := vars[0]!
     let plift := mkApp (mkConst ``PLift [.zero])
     let pliftUp := mkApp2 (mkConst ``PLift.up [.zero])
     let noneE tp   := mkApp  (mkConst ``Option.none [.zero]) (plift tp)
     let someE tp v := mkApp2 (mkConst ``Option.some [.zero]) (plift tp) (pliftUp tp v)
-    let vars ← vars.mapM fun ⟨x, inst?⟩ =>
+    let vars ← vars.mapM fun x => do
       let isNeutral :=
         let isNeutralClass := mkApp3 (mkConst ``LawfulIdentity [u]) α preContext.op x
-        match inst? with
-        | none => noneE isNeutralClass
-        | some isNeutral => someE isNeutralClass isNeutral
-      return mkApp4 (mkConst ``Variable.mk [u]) α preContext.op x isNeutral
+        match ←getInstance ``LawfulIdentity #[preContext.op, x] with
+        | none => (false, noneE isNeutralClass)
+        | some isNeutral => (true, someE isNeutralClass isNeutral)
 
+      return (isNeutral.1, mkApp4 (mkConst ``Variable.mk [u]) α preContext.op x isNeutral.2)
+
+    let (isNeutrals, vars) := vars.unzip
     let vars := vars.toList
     let vars ← mkListLit (mkApp2 (mkConst ``Variable [u]) α preContext.op) vars
 
@@ -158,7 +130,7 @@ where
       | none => noneE idemClass
       | some idem => someE idemClass idem
 
-    return mkApp7 (mkConst ``Lean.Data.AC.Context.mk [u]) α preContext.op preContext.assoc comm idem vars arbitrary
+    return (isNeutrals, mkApp7 (mkConst ``Lean.Data.AC.Context.mk [u]) α preContext.op preContext.assoc comm idem vars arbitrary)
 
   convert : ACExpr → Expr
     | .op l r => mkApp2 (mkConst ``Data.AC.Expr.op) (convert l) (convert r)

src/Lean/Meta/Tactic/Intro.lean

@@ -164,11 +164,7 @@ does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId true
 
-/--
-Calculate the number of new hypotheses that would be created by `intros`,
-i.e. the number of binders which can be introduced without unfolding definitions.
--/
-partial def getIntrosSize : Expr → Nat
+private partial def getIntrosSize : Expr → Nat
   | .forallE _ _ b _ => getIntrosSize b + 1
   | .letE _ _ _ b _  => getIntrosSize b + 1
   | .mdata _ b       => getIntrosSize b

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

@@ -8,43 +8,24 @@ import Lean.Meta.Tactic.LinearArith.Nat.Basic
 
 namespace Lean.Meta.Linear.Nat
 
-/-
-To prevent the kernel from accidentially reducing the atoms in the equation while typechecking,
-we abstract over them.
--/
-def withAbstractAtoms (atoms : Array Expr) (k : Array Expr → MetaM (Option (Expr × Expr))) :
-    MetaM (Option (Expr × Expr)) := do
-  let atoms := atoms
-  let decls : Array (Name × (Array Expr → MetaM Expr)) ← atoms.mapM fun _ => do
-    return ((← mkFreshUserName `x), fun _ => pure (mkConst ``Nat))
-  withLocalDeclsD decls fun ctxt => do
-    let some (r, p) ← k ctxt | return none
-    let r := (← mkLambdaFVars ctxt r).beta atoms
-    let p := mkAppN (← mkLambdaFVars ctxt p) atoms
-    return some (r, p)
-
 def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
-  let (some c, atoms) ← ToLinear.run (ToLinear.toLinearCnstr? e) | return none
-  withAbstractAtoms atoms fun ctx => do
-    let lhs ← c.toArith ctx
-    let c₁ := c.toPoly
-    let c₂ := c₁.norm
-    if c₂.isUnsat then
-      let r := mkConst ``False
-      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr ctx) (toExpr c) reflTrue
-      return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
-    else if c₂.isValid then
-      let r := mkConst ``True
-      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue
-      return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
+  let (some c, ctx) ← ToLinear.run (ToLinear.toLinearCnstr? e) | return none
+  let c₁ := c.toPoly
+  let c₂ := c₁.norm
+  if c₂.isUnsat then
+    let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr ctx) (toExpr c) reflTrue
+    return some (mkConst ``False, p)
+  else if c₂.isValid then
+    let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue
+    return some (mkConst ``True, p)
+  else
+    let c₂ : LinearCnstr := c₂.toExpr
+    let r ← c₂.toArith ctx
+    if r != e then
+      let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
+      return some (r, ← mkExpectedTypeHint p (← mkEq e r))
     else
-      let c₂ : LinearCnstr := c₂.toExpr
-      let r ← c₂.toArith ctx
-      if r != lhs then
-        let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
-        return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
-      else
-        return none
+      return none
 
 def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   if let some arg := e.not? then

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

@@ -62,12 +62,12 @@ builtin_simproc [simp, seval] reduceNe  (( _ : Fin _) ≠ _)  := reduceBinPred `
 builtin_dsimproc [simp, seval] reduceBEq  (( _ : Fin _) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
 builtin_dsimproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred ``bne 4 (. != .)
 
-/-- Simplification procedure for ensuring `Fin n` literals are normalized. -/
+/-- Simplification procedure for ensuring `Fin` literals are normalized. -/
 builtin_dsimproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
   let_expr OfNat.ofNat _ m _ ← e | return .continue
   let some ⟨n, v⟩ ← getFinValue? e | return .continue
   let some m ← getNatValue? m | return .continue
-  if m < n then
+  if n == m then
     -- Design decision: should we return `.continue` instead of `.done` when simplifying.
     -- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`
     return .done e

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

@@ -149,14 +149,11 @@ private def mkSubNat (x y : Expr) : Expr :=
 private def mkEqNat (x y : Expr) : Expr :=
   mkAppN (mkConst ``Eq [levelOne]) #[mkConst ``Nat, x, y]
 
-private def mkBEqNatInstance : Expr :=
-  mkAppN (mkConst ``instBEqOfDecidableEq [levelZero]) #[mkConst ``Nat, mkConst ``instDecidableEqNat []]
-
-private def mkBEqNat (x y : Expr) : Expr :=
-  mkAppN (mkConst ``BEq.beq [levelZero]) #[mkConst ``Nat, mkBEqNatInstance, 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, mkBEqNatInstance, x, y]
+  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]
@@ -253,7 +250,7 @@ builtin_simproc [simp, seval] reduceBeqDiff ((_ : Nat) == _) := fun e => do
     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 }
+    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

src/Lean/Meta/Tactic/SplitIf.lean

@@ -4,26 +4,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.LazyInitExtension
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 namespace SplitIf
 
+builtin_initialize ext : LazyInitExtension MetaM Simp.Context ←
+  registerLazyInitExtension do
+    let mut s : SimpTheorems := {}
+    s ← s.addConst ``if_pos
+    s ← s.addConst ``if_neg
+    s ← s.addConst ``dif_pos
+    s ← s.addConst ``dif_neg
+    return {
+      simpTheorems  := #[s]
+      congrTheorems := (← getSimpCongrTheorems)
+      config        := { Simp.neutralConfig with dsimp := false }
+    }
+
 /--
   Default `Simp.Context` for `simpIf` methods. It contains all congruence theorems, but
   just the rewriting rules for reducing `if` expressions. -/
-def getSimpContext : MetaM Simp.Context := do
-  let mut s : SimpTheorems := {}
-  s ← s.addConst ``if_pos
-  s ← s.addConst ``if_neg
-  s ← s.addConst ``dif_pos
-  s ← s.addConst ``dif_neg
-  return {
-    simpTheorems  := #[s]
-    congrTheorems := (← getSimpCongrTheorems)
-    config        := { Simp.neutralConfig with dsimp := false }
-  }
+def getSimpContext : MetaM Simp.Context :=
+  ext.get
 
 /--
   Default `discharge?` function for `simpIf` methods.

src/Lean/Server/InfoUtils.lean

@@ -40,34 +40,27 @@ structure InfoWithCtx where
   info : Elab.Info
   children : PersistentArray InfoTree
 
-/--
-Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones) and
-accumulating results on the way back up. If `preNode` returns `false`, the children of the current
-node are skipped and `postNode` is invoked with an empty list of results.
--/
+/-- Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones)
+and accumulating results on the way back up. -/
 partial def InfoTree.visitM [Monad m]
-    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Bool := fun _ _ _ => pure true)
+    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
     (postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → List (Option α) → m α)
-    (ctx? : Option ContextInfo := none) : InfoTree → m (Option α) :=
-  go ctx?
+    : InfoTree → m (Option α) :=
+  go none
 where go
   | ctx?, context ctx t => go (ctx.mergeIntoOuter? ctx?) t
   | some ctx, node i cs => do
-    let visitChildren ← preNode ctx i cs
-    if !visitChildren then
-      postNode ctx i cs []
-    else
-      let as ← cs.toList.mapM (go <| i.updateContext? ctx)
-      postNode ctx i cs as
+    preNode ctx i cs
+    let as ← cs.toList.mapM (go <| i.updateContext? ctx)
+    postNode ctx i cs as
   | none, node .. => panic! "unexpected context-free info tree node"
   | _, hole .. => pure none
 
 /-- `InfoTree.visitM` specialized to `Unit` return type -/
 def InfoTree.visitM' [Monad m]
-    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Bool := fun _ _ _ => pure true)
+    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
     (postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
-    (ctx? : Option ContextInfo := none) (t : InfoTree) : m Unit :=
-  t.visitM preNode (fun ci i cs _ => postNode ci i cs) ctx? |> discard
+    (t : InfoTree) : m Unit := t.visitM preNode (fun ci i cs _ => postNode ci i cs) |> discard
 
 /--
   Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves). -/
@@ -417,9 +410,6 @@ where go ci?
     match ci?, i with
     | some ci, .ofTermInfo ti
     | some ci, .ofOmissionInfo { toTermInfo := ti, .. } => do
-      -- NOTE: `instantiateMVars` can potentially be expensive but we rely on the elaborator
-      -- creating a fully instantiated `MutualDef.body` term info node which has the implicit effect
-      -- of making the `instantiateMVars` here a no-op and avoids further recursing into the body
       let expr ← ti.runMetaM ci (instantiateMVars ti.expr)
       return expr.hasSorry
       -- we assume that `cs` are subterms of `ti.expr` and

src/Lean/ToExpr.lean

@@ -59,35 +59,35 @@ instance : ToExpr (BitVec n) where
 instance : ToExpr UInt8 where
   toTypeExpr := mkConst ``UInt8
   toExpr a :=
-    let r := mkRawNatLit a.toNat
+    let r := mkRawNatLit a.val
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt8) r
       (.app (.const ``UInt8.instOfNat []) r)
 
 instance : ToExpr UInt16 where
   toTypeExpr := mkConst ``UInt16
   toExpr a :=
-    let r := mkRawNatLit a.toNat
+    let r := mkRawNatLit a.val
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt16) r
       (.app (.const ``UInt16.instOfNat []) r)
 
 instance : ToExpr UInt32 where
   toTypeExpr := mkConst ``UInt32
   toExpr a :=
-    let r := mkRawNatLit a.toNat
+    let r := mkRawNatLit a.val
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt32) r
       (.app (.const ``UInt32.instOfNat []) r)
 
 instance : ToExpr UInt64 where
   toTypeExpr := mkConst ``UInt64
   toExpr a :=
-    let r := mkRawNatLit a.toNat
+    let r := mkRawNatLit a.val
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt64) r
       (.app (.const ``UInt64.instOfNat []) r)
 
 instance : ToExpr USize where
   toTypeExpr := mkConst ``USize
   toExpr a :=
-    let r := mkRawNatLit a.toNat
+    let r := mkRawNatLit a.val
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``USize) r
       (.app (.const ``USize.instOfNat []) r)
 

src/Std/Data/DHashMap/Internal/Index.lean

@@ -54,9 +54,9 @@ cf. https://github.com/leanprover/lean4/issues/4157
         · exact Nat.one_pos
         · exact Nat.lt_of_le_of_lt h h'
       · exact h'
-      · rw [USize.le_def, BitVec.le_def]
+      · rw [USize.le_def, Fin.le_def]
         change _ ≤ (_ % _)
-        rw [Nat.mod_eq_of_lt h', USize.ofNat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt]
+        rw [Nat.mod_eq_of_lt h', USize.ofNat, Fin.val_ofNat', Nat.mod_eq_of_lt]
         · exact h
         · exact Nat.lt_of_le_of_lt h h'
     · exact Nat.lt_of_lt_of_le (USize.toNat_lt_size _) (Nat.le_of_not_lt h')⟩

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -1112,7 +1112,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
   let li := derivedLits_arr[i]
   have li_in_derivedLits : li ∈ derivedLits := by
     rw [Array.mem_toList, ← derivedLits_arr_def]
-    simp [li, Array.getElem_mem]
+    simp only [li, Array.getElem?_mem]
   have i_in_bounds : i.1 < derivedLits.length := by
     have i_property := i.2
     simp only [derivedLits_arr_def, Array.size_mk] at i_property

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean

@@ -570,7 +570,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
         rw [c_clause_rw] at pc1
         have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
           rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-          simp only [List.get_eq_getElem] at hidx
+          rw [← Array.getElem_fin_eq_toList_get] at hidx
           exact Exists.intro idx hidx
         rcases idx_exists with ⟨idx, hidx⟩
         specialize h1 idx idx.2
@@ -580,7 +580,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
         rw [c_clause_rw] at pc1
         have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
           rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-          simp only [List.get_eq_getElem] at hidx
+          rw [← Array.getElem_fin_eq_toList_get] at hidx
           exact Exists.intro idx hidx
         rcases idx_exists with ⟨idx, hidx⟩
         specialize h1 idx idx.2
@@ -595,7 +595,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
       rw [c_clause_rw] at pc1
       have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
         rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-        simp only [List.get_eq_getElem] at hidx
+        rw [← Array.getElem_fin_eq_toList_get] at hidx
         exact Exists.intro idx hidx
       rcases idx_exists with ⟨idx, hidx⟩
       apply Exists.intro idx ∘ And.intro idx.2
@@ -606,7 +606,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
       rw [c_clause_rw] at pc1
       have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
         rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-        simp only [List.get_eq_getElem] at hidx
+        rw [← Array.getElem_fin_eq_toList_get] at hidx
         exact Exists.intro idx hidx
       rcases idx_exists with ⟨idx, hidx⟩
       apply Exists.intro idx ∘ And.intro idx.2

src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean

@@ -81,7 +81,8 @@ attribute [bv_normalize] BitVec.testBit_toNat
 @[bv_normalize]
 theorem BitVec.lt_ult (x y : BitVec w) : (x < y) = (BitVec.ult x y = true) := by
   rw [BitVec.ult]
-  simp only [(· < ·)]
+  rw [LT.lt]
+  rw [BitVec.instLT]
   simp
 
 attribute [bv_normalize] BitVec.natCast_eq_ofNat

src/lake/Lake/CLI/Init.lean

@@ -126,8 +126,7 @@ package {repr pkgName} where
   version := v!\"0.1.0\"
   keywords := #[\"math\"]
   leanOptions := #[
-    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
-    ⟨`autoImplicit, false⟩
+    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
   ]
 
 require \"leanprover-community\" / \"mathlib\"
@@ -145,7 +144,6 @@ defaultTargets = [{repr libRoot}]
 
 [leanOptions]
 pp.unicode.fun = true # pretty-prints `fun a ↦ b`
-autoImplicit = false
 
 [[require]]
 name = \"mathlib\"

src/lake/Lake/Util/Compare.lean

@@ -64,7 +64,7 @@ instance : LawfulCmpEq Nat compare where
 
 instance : LawfulCmpEq UInt64 compare where
   eq_of_cmp h := eq_of_compareOfLessAndEq h
-  cmp_rfl := compareOfLessAndEq_rfl <| UInt64.lt_irrefl _
+  cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
 
 instance : LawfulCmpEq String compare where
   eq_of_cmp := eq_of_compareOfLessAndEq