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₂ =>

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

src/Init/Data/Array/Lemmas.lean

@@ -45,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
@@ -67,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
@@ -78,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
@@ -147,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]
@@ -201,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
@@ -221,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
@@ -239,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
@@ -364,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 :=
@@ -375,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 α} :
@@ -395,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]
@@ -423,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
@@ -438,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]
@@ -452,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
 
@@ -483,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]
@@ -523,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
@@ -543,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]
@@ -575,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]
 
@@ -599,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)
@@ -615,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
@@ -644,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) :
@@ -672,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 : β → α → β}
@@ -688,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 : α → β → β}
@@ -734,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
@@ -805,12 +872,6 @@ 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.
@@ -884,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 α) :
@@ -897,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'
@@ -930,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]
@@ -947,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
@@ -969,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
@@ -977,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]
 
@@ -1219,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 α) :
@@ -1258,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]
 
@@ -1327,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
@@ -1473,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/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/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/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/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
@@ -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/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 : Substring) : Option Substring :=
-  s.toSubstring.dropPrefix? pre
-
-/--
-If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
--/
-def dropSuffix? (s : String) (suff : Substring) : Option Substring :=
-  s.toSubstring.dropSuffix? suff
-
-/-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
-or otherwise return `s`. -/
-def stripPrefix (s : String) (pre : Substring) : 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 : Substring) : 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/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/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/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

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