feat: aligning List/Array/Vector lemmas for map

doc/dev/ffi.md

@@ -49,9 +49,8 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   is represented by the representation of that parameter's type.
 
   For example, `{ x : α // p }`, the `Subtype` structure of a value of type `α` and an irrelevant proof, is represented by the representation of `α`.
-  Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
-* `Nat` and `Int` are represented by `lean_object *`.
-  Their runtime values is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number or integer (`lean_box`/`lean_unbox`).
+* `Nat` is represented by `lean_object *`.
+  Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
 * A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
 * Any other type is represented by `lean_object *`.
   Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.

doc/dev/release_checklist.md

@@ -37,32 +37,16 @@ We'll use `v4.6.0` as the intended release version as a running example.
     - Create the tag `v4.6.0` from `master`/`main` and push it.
     - Merge the tag `v4.6.0` into the `stable` branch and push it.
   - We do this for the repositories:
-    - [Batteries](https://github.com/leanprover-community/batteries)
-      - No dependencies
-      - Toolchain bump PR
-      - Create and push the tag
-      - Merge the tag into `stable`
     - [lean4checker](https://github.com/leanprover/lean4checker)
       - No dependencies
       - Toolchain bump PR
       - Create and push the tag
       - Merge the tag into `stable`
-    - [doc-gen4](https://github.com/leanprover/doc-gen4)
-      - Dependencies: exist, but they're not part of the release workflow
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
-    - [Verso](https://github.com/leanprover/verso)
-      - Dependencies: exist, but they're not part of the release workflow
-      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
-    - [Cli](https://github.com/leanprover/lean4-cli)
+    - [Batteries](https://github.com/leanprover-community/batteries)
       - No dependencies
       - Toolchain bump PR
       - Create and push the tag
-      - There is no `stable` branch; skip this step
+      - Merge the tag into `stable`
     - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
       - Dependencies: `Batteries`
       - Note on versions and branches:
@@ -77,6 +61,17 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - Merge the tag into `stable`
+    - [doc-gen4](https://github.com/leanprover/doc-gen4)
+      - Dependencies: exist, but they're not part of the release workflow
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
+    - [Verso](https://github.com/leanprover/verso)
+      - Dependencies: exist, but they're not part of the release workflow
+      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
     - [import-graph](https://github.com/leanprover-community/import-graph)
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag

script/release_repos.yml

@@ -27,13 +27,6 @@ repositories:
     branch: main
     dependencies: []
 
-  - name: Cli
-    url: https://github.com/leanprover/lean4-cli
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: []
-
   - name: ProofWidgets4
     url: https://github.com/leanprover-community/ProofWidgets4
     toolchain-tag: false

src/Init/Conv.lean

@@ -150,10 +150,6 @@ See the `simp` tactic for more information. -/
 syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? : conv
 
-/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
-that would be sufficient to close the goal. See the `simp?` tactic for more information. -/
-syntax (name := simpTrace) "simp?" optConfig (discharger)? (&" only")? (simpArgs)? : conv
-
 /--
 `dsimp` is the definitional simplifier in `conv`-mode. It differs from `simp` in that it only
 applies theorems that hold by reflexivity.
@@ -171,9 +167,6 @@ example (a : Nat): (0 + 0) = a - a := by
 syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : conv
 
-@[inherit_doc simpTrace]
-syntax (name := dsimpTrace) "dsimp?" optConfig (&" only")? (dsimpArgs)? : conv
-
 /-- `simp_match` simplifies match expressions. For example,
 ```
 match [a, b] with

src/Init/Data/Array/Basic.lean

@@ -244,7 +244,8 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
 def range (n : Nat) : Array Nat :=
   ofFn fun (i : Fin n) => i
 
-@[inline] protected def singleton (v : α) : Array α := #[v]
+def singleton (v : α) : Array α :=
+  mkArray 1 v
 
 def back! [Inhabited α] (a : Array α) : α :=
   a[a.size - 1]!

src/Init/Data/Array/Lemmas.lean

@@ -124,8 +124,6 @@ theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a
   · rintro ⟨rfl, rfl⟩
     rfl
 
-theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
-
 theorem exists_push_of_ne_empty {xs : Array α} (h : xs ≠ #[]) :
     ∃ (ys : Array α) (a : α), xs = ys.push a := by
   rcases xs with ⟨xs⟩
@@ -1189,416 +1187,11 @@ theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
     rfl
 termination_by as.size - i
 
-/-! ### filter -/
-
-@[congr]
-theorem filter_congr {as bs : Array α} (h : as = bs)
-    {f : α → Bool} {g : α → Bool} (h' : f = g) {start stop start' stop' : Nat}
-    (h₁ : start = start') (h₂ : stop = stop') :
-    filter f as start stop = filter g bs start' stop' := by
-  congr
-
-@[simp] theorem toList_filter' (p : α → Bool) (l : Array α) (h : stop = l.size) :
-    (l.filter p 0 stop).toList = l.toList.filter p := by
-  subst h
-  dsimp only [filter]
-  rw [← foldl_toList]
-  generalize l.toList = l
-  suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
-      a.toList ++ List.filter p l by
-    simpa using this #[]
-  induction l with simp
-  | cons => split <;> simp [*]
-
-theorem toList_filter (p : α → Bool) (l : Array α) :
-    (l.filter p).toList = l.toList.filter p := by
-  simp
-
-@[simp] theorem _root_.List.filter_toArray' (p : α → Bool) (l : List α) (h : stop = l.length) :
-    l.toArray.filter p 0 stop = (l.filter p).toArray := by
-  apply ext'
-  simp [h]
-
-theorem _root_.List.filter_toArray (p : α → Bool) (l : List α) :
-    l.toArray.filter p = (l.filter p).toArray := by
-  simp
-
-@[simp] theorem filter_push_of_pos {p : α → Bool} {a : α} {l : Array α}
-    (h : p a) (w : stop = l.size + 1):
-    (l.push a).filter p 0 stop = (l.filter p).push a := by
-  subst w
-  rcases l with ⟨l⟩
-  simp [h]
-
-@[simp] theorem filter_push_of_neg {p : α → Bool} {a : α} {l : Array α}
-    (h : ¬p a) (w : stop = l.size + 1) :
-    (l.push a).filter p 0 stop = l.filter p := by
-  subst w
-  rcases l with ⟨l⟩
-  simp [h]
-
-theorem filter_push {p : α → Bool} {a : α} {l : Array α} :
-    (l.push a).filter p = if p a then (l.filter p).push a else l.filter p := by
-  split <;> simp [*]
-
-theorem size_filter_le (p : α → Bool) (l : Array α) :
-    (l.filter p).size ≤ l.size := by
-  rcases l with ⟨l⟩
-  simpa using List.length_filter_le p l
-
-@[simp] theorem filter_eq_self {p : α → Bool} {l : Array α} :
-    filter p l = l ↔ ∀ a ∈ l, p a := by
-  rcases l with ⟨l⟩
-  simp
-
-@[simp] theorem filter_size_eq_size {p : α → Bool} {l : Array α} :
-    (filter p l).size = l.size ↔ ∀ a ∈ l, p a := by
-  rcases l with ⟨l⟩
-  simp
-
-@[simp] theorem mem_filter {p : α → Bool} {l : Array α} {a : α} :
-    a ∈ filter p l ↔ a ∈ l ∧ p a := by
-  rcases l with ⟨l⟩
-  simp
-
-@[simp] theorem filter_eq_empty_iff {p : α → Bool} {l : Array α} :
-    filter p l = #[] ↔ ∀ a, a ∈ l → ¬p a := by
-  rcases l with ⟨l⟩
-  simp
-
-theorem forall_mem_filter {p : α → Bool} {l : Array α} {P : α → Prop} :
-    (∀ (i) (_ : i ∈ l.filter p), P i) ↔ ∀ (j) (_ : j ∈ l), p j → P j := by
-  simp
-
-@[simp] theorem filter_filter (q) (l : Array α) :
-    filter p (filter q l) = filter (fun a => p a && q a) l := by
-  apply ext'
-  simp only [toList_filter, List.filter_filter]
-
-theorem foldl_filter (p : α → Bool) (f : β → α → β) (l : Array α) (init : β) :
-    (l.filter p).foldl f init = l.foldl (fun x y => if p y then f x y else x) init := by
-  rcases l with ⟨l⟩
-  rw [List.filter_toArray]
-  simp [List.foldl_filter]
-
-theorem foldr_filter (p : α → Bool) (f : α → β → β) (l : Array α) (init : β) :
-    (l.filter p).foldr f init = l.foldr (fun x y => if p x then f x y else y) init := by
-  rcases l with ⟨l⟩
-  rw [List.filter_toArray]
-  simp [List.foldr_filter]
-
-theorem filter_map (f : β → α) (l : Array β) : filter p (map f l) = map f (filter (p ∘ f) l) := by
-  rcases l with ⟨l⟩
-  simp [List.filter_map]
-
-theorem map_filter_eq_foldl (f : α → β) (p : α → Bool) (l : Array α) :
-    map f (filter p l) = foldl (fun y x => bif p x then y.push (f x) else y) #[] l := by
-  rcases l with ⟨l⟩
-  apply ext'
-  simp only [size_toArray, List.filter_toArray', List.map_toArray, List.foldl_toArray']
-  rw [← List.reverse_reverse l]
-  generalize l.reverse = l
-  simp only [List.filter_reverse, List.map_reverse, List.foldl_reverse]
-  induction l with
-  | nil => rfl
-  | cons x l ih =>
-    simp only [List.filter_cons, List.foldr_cons]
-    split <;> simp_all
-
-@[simp] theorem filter_append {p : α → Bool} (l₁ l₂ : Array α) :
-    filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂ := by
-  rcases l₁ with ⟨l₁⟩
-  rcases l₂ with ⟨l₂⟩
-  simp [List.filter_append]
-
-theorem filter_eq_append_iff {p : α → Bool} :
-    filter p l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂ := by
-  rcases l with ⟨l⟩
-  rcases L₁ with ⟨L₁⟩
-  rcases L₂ with ⟨L₂⟩
-  simp only [size_toArray, List.filter_toArray', List.append_toArray, mk.injEq,
-    List.filter_eq_append_iff]
-  constructor
-  · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
-    refine ⟨l₁.toArray, l₂.toArray, by simp⟩
-  · rintro ⟨⟨l₁⟩, ⟨l₂⟩, h₁, h₂, h₃⟩
-    refine ⟨l₁, l₂, by simp_all⟩
-
-theorem filter_eq_push_iff {p : α → Bool} {l l' : Array α} {a : α} :
-    filter p l = l'.push a ↔
-      ∃ l₁ l₂, l = l₁.push a ++ l₂ ∧ filter p l₁ = l' ∧ p a ∧ (∀ x, x ∈ l₂ → ¬p x) := by
-  rcases l with ⟨l⟩
-  rcases l' with ⟨l'⟩
-  simp only [size_toArray, List.filter_toArray', List.push_toArray, mk.injEq, Bool.not_eq_true]
-  rw [← List.reverse_inj]
-  simp only [← List.filter_reverse]
-  simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
-    List.singleton_append]
-  rw [List.filter_eq_cons_iff]
-  constructor
-  · rintro ⟨l₁, l₂, h₁, h₂, h₃, h₄⟩
-    refine ⟨l₂.reverse.toArray, l₁.reverse.toArray, by simp_all⟩
-  · rintro ⟨⟨l₁⟩, ⟨l₂⟩, h₁, h₂, h₃, h₄⟩
-    refine ⟨l₂.reverse, l₁.reverse, by simp_all⟩
-
-@[deprecated filter_map (since := "2024-06-15")] abbrev map_filter := @filter_map
-
-theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
-  (mem_filter.mp h).1
-
-/-! ### filterMap -/
-
-@[congr]
-theorem filterMap_congr {as bs : Array α} (h : as = bs)
-    {f : α → Option β} {g : α → Option β} (h' : f = g) {start stop start' stop' : Nat}
-    (h₁ : start = start') (h₂ : stop = stop') :
-    filterMap f as start stop = filterMap g bs start' stop' := by
-  congr
-
-@[simp] theorem toList_filterMap' (f : α → Option β) (l : Array α) (w : stop = l.size) :
-    (l.filterMap f 0 stop).toList = l.toList.filterMap f := by
-  subst w
-  dsimp only [filterMap, filterMapM]
-  rw [← foldlM_toList]
-  generalize l.toList = l
-  have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
-    a.toList ++ List.filterMap f l := ?_
-  exact this #[]
-  induction l
-  · simp_all [Id.run]
-  · simp_all [Id.run, List.filterMap_cons]
-    split <;> simp_all
-
-theorem toList_filterMap (f : α → Option β) (l : Array α) :
-    (l.filterMap f).toList = l.toList.filterMap f := by
-  simp [toList_filterMap']
-
-
-@[simp] theorem _root_.List.filterMap_toArray' (f : α → Option β) (l : List α) (h : stop = l.length) :
-    l.toArray.filterMap f 0 stop = (l.filterMap f).toArray := by
-  apply ext'
-  simp [h]
-
-theorem _root_.List.filterMap_toArray (f : α → Option β) (l : List α) :
-    l.toArray.filterMap f = (l.filterMap f).toArray := by
-  simp
-
-@[simp] theorem filterMap_push_none {f : α → Option β} {a : α} {l : Array α}
-    (h : f a = none) (w : stop = l.size + 1) :
-    filterMap f (l.push a) 0 stop = filterMap f l := by
-  subst w
-  rcases l with ⟨l⟩
-  simp [h]
-
-@[simp] theorem filterMap_push_some {f : α → Option β} {a : α} {l : Array α} {b : β}
-    (h : f a = some b) (w : stop = l.size + 1) :
-    filterMap f (l.push a) 0 stop = (filterMap f l).push b := by
-  subst w
-  rcases l with ⟨l⟩
-  simp [h]
-
-@[simp] theorem filterMap_eq_map (f : α → β) : filterMap (some ∘ f) = map f := by
-  funext l
-  cases l
-  simp
-
-theorem filterMap_some_fun : filterMap (some : α → Option α) = id := by
-  funext l
-  cases l
-  simp
-
-@[simp] theorem filterMap_some (l : Array α) : filterMap some l = l := by
-  cases l
-  simp
-
-theorem map_filterMap_some_eq_filterMap_isSome (f : α → Option β) (l : Array α) :
-    (l.filterMap f).map some = (l.map f).filter fun b => b.isSome := by
-  cases l
-  simp [List.map_filterMap_some_eq_filter_map_isSome]
-
-theorem size_filterMap_le (f : α → Option β) (l : Array α) :
-    (filterMap f l).size ≤ l.size := by
-  cases l
-  simp [List.length_filterMap_le]
-
-@[simp] theorem filterMap_size_eq_size {l} :
-    (filterMap f l).size = l.size ↔ ∀ a, a ∈ l → (f a).isSome := by
-  cases l
-  simp [List.filterMap_length_eq_length]
-
-@[simp]
-theorem filterMap_eq_filter (p : α → Bool) :
-    filterMap (Option.guard (p ·)) = filter p := by
-  funext l
-  cases l
-  simp
-
-theorem filterMap_filterMap (f : α → Option β) (g : β → Option γ) (l : Array α) :
-    filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l := by
-  cases l
-  simp [List.filterMap_filterMap]
-
-theorem map_filterMap (f : α → Option β) (g : β → γ) (l : Array α) :
-    map g (filterMap f l) = filterMap (fun x => (f x).map g) l := by
-  cases l
-  simp [List.map_filterMap]
-
-@[simp] theorem filterMap_map (f : α → β) (g : β → Option γ) (l : Array α) :
-    filterMap g (map f l) = filterMap (g ∘ f) l := by
-  cases l
-  simp [List.filterMap_map]
-
-theorem filter_filterMap (f : α → Option β) (p : β → Bool) (l : Array α) :
-    filter p (filterMap f l) = filterMap (fun x => (f x).filter p) l := by
-  cases l
-  simp [List.filter_filterMap]
-
-theorem filterMap_filter (p : α → Bool) (f : α → Option β) (l : Array α) :
-    filterMap f (filter p l) = filterMap (fun x => if p x then f x else none) l := by
-  cases l
-  simp [List.filterMap_filter]
-
-@[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]
-
-theorem forall_mem_filterMap {f : α → Option β} {l : Array α} {P : β → Prop} :
-    (∀ (i) (_ : i ∈ filterMap f l), P i) ↔ ∀ (j) (_ : j ∈ l) (b), f j = some b → P b := by
-  simp only [mem_filterMap, forall_exists_index, and_imp]
-  rw [forall_comm]
-  apply forall_congr'
-  intro a
-  rw [forall_comm]
-
-@[simp] theorem filterMap_append {α β : Type _} (l l' : Array α) (f : α → Option β) :
-    filterMap f (l ++ l') = filterMap f l ++ filterMap f l' := by
-  cases l
-  cases l'
-  simp
-
-theorem map_filterMap_of_inv (f : α → Option β) (g : β → α) (H : ∀ x : α, (f x).map g = some x)
-    (l : Array α) : map g (filterMap f l) = l := by simp only [map_filterMap, H, filterMap_some, id]
-
-theorem forall_none_of_filterMap_eq_empty (h : filterMap f xs = #[]) : ∀ x ∈ xs, f x = none := by
-  cases xs
-  simpa using h
-
-@[simp] theorem filterMap_eq_nil_iff {l} : filterMap f l = #[] ↔ ∀ a, a ∈ l → f a = none := by
-  cases l
-  simp
-
-theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array β} {b : β} :
-    filterMap f l = l'.push b ↔ ∃ l₁ a l₂,
-      l = l₁.push a ++ l₂ ∧ filterMap f l₁ = l' ∧ f a = some b ∧ (∀ x, x ∈ l₂ → f x = none) := by
-  rcases l with ⟨l⟩
-  rcases l' with ⟨l'⟩
-  simp only [size_toArray, List.filterMap_toArray', List.push_toArray, mk.injEq]
-  rw [← List.reverse_inj]
-  simp only [← List.filterMap_reverse]
-  simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
-    List.singleton_append]
-  rw [List.filterMap_eq_cons_iff]
-  constructor
-  · rintro ⟨l₁, a, l₂, h₁, h₂, h₃, h₄⟩
-    refine ⟨l₂.reverse.toArray, a, l₁.reverse.toArray, by simp_all⟩
-  · rintro ⟨⟨l₁⟩, a, ⟨l₂⟩, h₁, h₂, h₃, h₄⟩
-    refine ⟨l₂.reverse, a, l₁.reverse, by simp_all⟩
-
 /-! Content below this point has not yet been aligned with `List`. -/
 
-/-! ### singleton -/
-
-@[simp] theorem singleton_def (v : α) : Array.singleton v = #[v] := rfl
-
-/-! ### append -/
-
-@[simp] theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} :
-    xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList := by
-  cases as
-  cases bs
-  simp
-
-@[simp] theorem append_eq_toArray_iff {as bs : Array α} {xs : List α} :
-    as ++ bs = xs.toArray ↔ as.toList ++ bs.toList = xs := by
-  cases as
-  cases bs
-  simp
-
 theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
 
-@[simp] theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
-  funext ⟨l⟩
-  simp
-
-@[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
-  simp only [mem_def, toList_append, List.mem_append]
-
-theorem mem_append_left {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂ :=
-  mem_append.2 (Or.inl h)
-
-theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂ :=
-  mem_append.2 (Or.inr h)
-
-@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
-  simp only [size, toList_append, List.length_append]
-
-theorem empty_append (as : Array α) : #[] ++ as = as := by simp
-
-theorem append_empty (as : Array α) : as ++ #[] = as := by simp
-
-theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
-    (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
-  cases as; cases bs
-  simp [List.getElem_append]
-
-theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
-    (as ++ bs)[i] = as[i] := by
-  simp only [← getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
-  conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
-  apply List.get_of_eq; rw [toList_append]
-
-theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i) :
-    (as ++ bs)[i] = bs[i - as.size]'(Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) := by
-  simp only [← getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
-  conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
-  apply List.get_of_eq; rw [toList_append]
-
-theorem getElem?_append_left {as bs : Array α} {i : Nat} (hn : i < as.size) :
-    (as ++ bs)[i]? = as[i]? := by
-  have hn' : i < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
-    size_append .. ▸ Nat.le_add_right ..
-  simp_all [getElem?_eq_getElem, getElem_append]
-
-theorem getElem?_append_right {as bs : Array α} {i : Nat} (h : as.size ≤ i) :
-    (as ++ bs)[i]? = bs[i - as.size]? := by
-  cases as
-  cases bs
-  simp at h
-  simp [List.getElem?_append_right, h]
-
-theorem getElem?_append {as bs : Array α} {i : Nat} :
-    (as ++ bs)[i]? = if i < as.size then as[i]? else bs[i - as.size]? := by
-  split <;> rename_i h
-  · exact getElem?_append_left h
-  · exact getElem?_append_right (by simpa using h)
-
-/-- Variant of `getElem_append_left` useful for rewriting from the small array to the big array. -/
-theorem getElem_append_left' (l₂ : Array α) {l₁ : Array α} {i : Nat} (hi : i < l₁.size) :
-    l₁[i] = (l₁ ++ l₂)[i]'(by simpa using Nat.lt_add_right l₂.size hi) := by
-  rw [getElem_append_left] <;> simp
-
-/-- Variant of `getElem_append_right` useful for rewriting from the small array to the big array. -/
-theorem getElem_append_right' (l₁ : Array α) {l₂ : Array α} {i : Nat} (hi : i < l₂.size) :
-    l₂[i] = (l₁ ++ l₂)[i + l₁.size]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hi _) := by
-  rw [getElem_append_right] <;> simp [*, Nat.le_add_left]
-
-theorem getElem_of_append {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂) (h : l₁.size = i) :
-    l[i]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
-  rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h]
-  simp
-
+@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
 -- This is a duplicate of `List.toArray_toList`.
 -- It's confusing to guess which namespace this theorem should live in,
@@ -2208,10 +1801,137 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
   simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
   split <;> split <;> rfl
 
+/-! ### filter -/
+
+@[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
+    (l.filter p).toList = l.toList.filter p := by
+  dsimp only [filter]
+  rw [← foldl_toList]
+  generalize l.toList = l
+  suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
+      a.toList ++ List.filter p l by
+    simpa using this #[]
+  induction l with simp
+  | cons => split <;> simp [*]
+
+@[simp] theorem filter_filter (q) (l : Array α) :
+    filter p (filter q l) = filter (fun a => p a && q a) l := by
+  apply ext'
+  simp only [toList_filter, List.filter_filter]
+
+@[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
+  simp only [mem_def, toList_filter, List.mem_filter]
+
+theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
+  (mem_filter.mp h).1
+
+@[congr]
+theorem filter_congr {as bs : Array α} (h : as = bs)
+    {f : α → Bool} {g : α → Bool} (h' : f = g) {start stop start' stop' : Nat}
+    (h₁ : start = start') (h₂ : stop = stop') :
+    filter f as start stop = filter g bs start' stop' := by
+  congr
+
+/-! ### filterMap -/
+
+@[simp] theorem toList_filterMap (f : α → Option β) (l : Array α) :
+    (l.filterMap f).toList = l.toList.filterMap f := by
+  dsimp only [filterMap, filterMapM]
+  rw [← foldlM_toList]
+  generalize l.toList = l
+  have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
+    a.toList ++ List.filterMap f l := ?_
+  exact this #[]
+  induction l
+  · simp_all [Id.run]
+  · simp_all [Id.run, List.filterMap_cons]
+    split <;> simp_all
+
+@[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]
+
+@[congr]
+theorem filterMap_congr {as bs : Array α} (h : as = bs)
+    {f : α → Option β} {g : α → Option β} (h' : f = g) {start stop start' stop' : Nat}
+    (h₁ : start = start') (h₂ : stop = stop') :
+    filterMap f as start stop = filterMap g bs start' stop' := by
+  congr
+
 /-! ### empty -/
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
 
+/-! ### append -/
+
+theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
+
+@[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
+  simp only [mem_def, toList_append, List.mem_append]
+
+theorem mem_append_left {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂ :=
+  mem_append.2 (Or.inl h)
+
+theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂ :=
+  mem_append.2 (Or.inr h)
+
+@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
+  simp only [size, toList_append, List.length_append]
+
+theorem empty_append (as : Array α) : #[] ++ as = as := by simp
+
+theorem append_empty (as : Array α) : as ++ #[] = as := by simp
+
+theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
+    (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
+  cases as; cases bs
+  simp [List.getElem_append]
+
+theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
+    (as ++ bs)[i] = as[i] := by
+  simp only [← getElem_toList]
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
+  conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
+  apply List.get_of_eq; rw [toList_append]
+
+theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i) :
+    (as ++ bs)[i] = bs[i - as.size]'(Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) := by
+  simp only [← getElem_toList]
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
+  conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
+  apply List.get_of_eq; rw [toList_append]
+
+theorem getElem?_append_left {as bs : Array α} {i : Nat} (hn : i < as.size) :
+    (as ++ bs)[i]? = as[i]? := by
+  have hn' : i < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
+    size_append .. ▸ Nat.le_add_right ..
+  simp_all [getElem?_eq_getElem, getElem_append]
+
+theorem getElem?_append_right {as bs : Array α} {i : Nat} (h : as.size ≤ i) :
+    (as ++ bs)[i]? = bs[i - as.size]? := by
+  cases as
+  cases bs
+  simp at h
+  simp [List.getElem?_append_right, h]
+
+theorem getElem?_append {as bs : Array α} {i : Nat} :
+    (as ++ bs)[i]? = if i < as.size then as[i]? else bs[i - as.size]? := by
+  split <;> rename_i h
+  · exact getElem?_append_left h
+  · exact getElem?_append_right (by simpa using h)
+
+@[simp] theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} :
+    xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList := by
+  cases as
+  cases bs
+  simp
+
+@[simp] theorem append_eq_toArray_iff {as bs : Array α} {xs : List α} :
+    as ++ bs = xs.toArray ↔ as.toList ++ bs.toList = xs := by
+  cases as
+  cases bs
+  simp
+
 /-! ### flatten -/
 
 @[simp] theorem toList_flatten {l : Array (Array α)} :
@@ -2547,6 +2267,26 @@ theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray
   apply ext'
   simp
 
+@[simp] theorem filter_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.filter p 0 stop = (l.filter p).toArray := by
+  subst h
+  apply ext'
+  rw [toList_filter]
+
+@[simp] theorem filterMap_toArray' (f : α → Option β) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.filterMap f 0 stop = (l.filterMap f).toArray := by
+  subst h
+  apply ext'
+  rw [toList_filterMap]
+
+theorem filter_toArray (p : α → Bool) (l : List α) :
+    l.toArray.filter p = (l.filter p).toArray := by
+  simp
+
+theorem filterMap_toArray (f : α → Option β) (l : List α) :
+    l.toArray.filterMap f = (l.filterMap f).toArray := by
+  simp
+
 @[simp] theorem flatten_toArray (l : List (List α)) :
     (l.toArray.map List.toArray).flatten = l.flatten.toArray := by
   apply ext'

src/Init/Data/BitVec/Lemmas.lean

@@ -9,9 +9,7 @@ import Init.Data.Bool
 import Init.Data.BitVec.Basic
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Div.Lemmas
 import Init.Data.Nat.Mod
-import Init.Data.Nat.Div.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
 import Init.Data.Int.Pow
 
@@ -100,12 +98,6 @@ theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
 theorem eq_of_toNat_eq {n} : ∀ {x y : BitVec n}, x.toNat = y.toNat → x = y
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
-/-- Prove nonequality of bitvectors in terms of nat operations. -/
-theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by
-  constructor
-  · rintro h rfl; apply h rfl
-  · intro h h_eq; apply h <| eq_of_toNat_eq h_eq
-
 @[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
 
 @[bv_toNat] theorem toNat_eq {x y : BitVec n} : x = y ↔ x.toNat = y.toNat :=
@@ -450,10 +442,6 @@ theorem toInt_eq_toNat_cond (x : BitVec n) :
         (x.toNat : Int) - (2^n : Nat) :=
   rfl
 
-theorem toInt_eq_toNat_of_lt {x : BitVec n} (h : 2 * x.toNat < 2^n) :
-    x.toInt = x.toNat := by
-  simp [toInt_eq_toNat_cond, h]
-
 theorem msb_eq_false_iff_two_mul_lt {x : BitVec w} : x.msb = false ↔ 2 * x.toNat < 2^w := by
   cases w <;> simp [Nat.pow_succ, Nat.mul_comm _ 2, msb_eq_decide, toNat_of_zero_length]
 
@@ -466,9 +454,6 @@ theorem toInt_eq_msb_cond (x : BitVec w) :
   simp only [BitVec.toInt, ← msb_eq_false_iff_two_mul_lt]
   cases x.msb <;> rfl
 
-theorem toInt_eq_toNat_of_msb {x : BitVec w} (h : x.msb = false) :
-    x.toInt = x.toNat := by
-  simp [toInt_eq_msb_cond, h]
 
 theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by
   simp only [toInt_eq_toNat_cond]
@@ -2315,12 +2300,6 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 @[simp, bv_toNat] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
   simp [Neg.neg, BitVec.neg]
 
-theorem toNat_neg_of_pos {x : BitVec n} (h : 0#n < x) :
-    (- x).toNat = 2^n - x.toNat := by
-  change 0 < x.toNat at h
-  rw [toNat_neg, Nat.mod_eq_of_lt]
-  omega
-
 theorem toInt_neg {x : BitVec w} :
     (-x).toInt = (-x.toInt).bmod (2 ^ w) := by
   rw [← BitVec.zero_sub, toInt_sub]
@@ -2607,13 +2586,13 @@ theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat) :
   rw [← udiv_eq]
   simp [udiv, bv_toNat, h, Nat.mod_eq_of_lt]
 
-@[simp]
-theorem toFin_udiv {x y : BitVec n} : (x / y).toFin = x.toFin / y.toFin := by
-  rfl
-
 @[simp, bv_toNat]
 theorem toNat_udiv {x y : BitVec n} : (x / y).toNat = x.toNat / y.toNat := by
-  rfl
+  rw [udiv_def]
+  by_cases h : y = 0
+  · simp [h]
+  · rw [toNat_ofNat, Nat.mod_eq_of_lt]
+    exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)
 
 @[simp]
 theorem zero_udiv {x : BitVec w} : (0#w) / x = 0#w := by
@@ -2649,45 +2628,6 @@ theorem udiv_self {x : BitVec w} :
       ↓reduceIte, toNat_udiv]
     rw [Nat.div_self (by omega), Nat.mod_eq_of_lt (by omega)]
 
-theorem msb_udiv (x y : BitVec w) :
-    (x / y).msb = (x.msb && y == 1#w) := by
-  cases msb_x : x.msb
-  · suffices x.toNat / y.toNat < 2 ^ (w - 1) by simpa [msb_eq_decide]
-    calc
-      x.toNat / y.toNat ≤ x.toNat     := by apply Nat.div_le_self
-                      _ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x
-  . rcases w with _|w
-    · contradiction
-    · have : (y == 1#_) = decide (y.toNat = 1) := by
-        simp [(· == ·), toNat_eq]
-      simp only [this, Bool.true_and]
-      match hy : y.toNat with
-      | 0 =>
-        obtain rfl : y = 0#_ := eq_of_toNat_eq hy
-        simp
-      | 1 =>
-        obtain rfl : y = 1#_ := eq_of_toNat_eq (by simp [hy])
-        simpa using msb_x
-      | y + 2 =>
-        suffices x.toNat / (y + 2) < 2 ^ w by
-          simp_all [msb_eq_decide, hy]
-        calc
-          x.toNat / (y + 2)
-            ≤ x.toNat / 2 := by apply Nat.div_add_le_right (by omega)
-          _ < 2 ^ w       := by omega
-
-theorem msb_udiv_eq_false_of {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
-    (x / y).msb = false := by
-  simp [msb_udiv, h]
-
-/--
-If `x` is nonnegative (i.e., does not have its msb set),
-then `x / y` is nonnegative, thus `toInt` and `toNat` coincide.
--/
-theorem toInt_udiv_of_msb {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
-    (x / y).toInt = x.toNat / y.toNat := by
-  simp [toInt_eq_msb_cond, msb_udiv_eq_false_of h]
-
 /-! ### umod -/
 
 theorem umod_def {x y : BitVec n} :
@@ -2700,10 +2640,6 @@ theorem umod_def {x y : BitVec n} :
 theorem toNat_umod {x y : BitVec n} :
     (x % y).toNat = x.toNat % y.toNat := rfl
 
-@[simp]
-theorem toFin_umod {x y : BitVec w} :
-    (x % y).toFin = x.toFin % y.toFin := rfl
-
 @[simp]
 theorem umod_zero {x : BitVec n} : x % 0#n = x := by
   simp [umod_def]
@@ -2731,55 +2667,6 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
     rcases hy with rfl | rfl <;>
       rfl
 
-theorem umod_eq_of_lt {x y : BitVec w} (h : x < y) :
-    x % y = x := by
-  apply eq_of_toNat_eq
-  simp [Nat.mod_eq_of_lt h]
-
-@[simp]
-theorem msb_umod {x y : BitVec w} :
-    (x % y).msb = (x.msb && (x < y || y == 0#w)) := by
-  rw [msb_eq_decide, toNat_umod]
-  cases msb_x : x.msb
-  · suffices x.toNat % y.toNat < 2 ^ (w - 1) by simpa
-    calc
-      x.toNat % y.toNat ≤ x.toNat     := by apply Nat.mod_le
-                      _ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x
-  . by_cases hy : y = 0
-    · simp_all [msb_eq_decide]
-    · suffices 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y by simp_all
-      by_cases x_lt_y : x < y
-      . simp_all [Nat.mod_eq_of_lt x_lt_y, msb_eq_decide]
-      · suffices x.toNat % y.toNat < 2 ^ (w - 1) by
-          simpa [x_lt_y]
-        have y_le_x : y.toNat ≤ x.toNat := by
-          simpa using x_lt_y
-        replace hy : y.toNat ≠ 0 :=
-          toNat_ne_iff_ne.mpr hy
-        by_cases msb_y : y.toNat < 2 ^ (w - 1)
-        · have : x.toNat % y.toNat < y.toNat := Nat.mod_lt _ (by omega)
-          omega
-        · rcases w with _|w
-          · contradiction
-          simp only [Nat.add_one_sub_one]
-          replace msb_y : 2 ^ w ≤ y.toNat := by
-            simpa using msb_y
-          have : y.toNat ≤ y.toNat * (x.toNat / y.toNat) := by
-              apply Nat.le_mul_of_pos_right
-              apply Nat.div_pos y_le_x
-              omega
-          have : x.toNat % y.toNat ≤ x.toNat - y.toNat := by
-            rw [Nat.mod_eq_sub]; omega
-          omega
-
-theorem toInt_umod {x y : BitVec w} :
-    (x % y).toInt = (x.toNat % y.toNat : Int).bmod (2 ^ w) := by
-  simp [toInt_eq_toNat_bmod]
-
-theorem toInt_umod_of_msb {x y : BitVec w} (h : x.msb = false) :
-    (x % y).toInt = x.toInt % y.toNat := by
-  simp [toInt_eq_msb_cond, h]
-
 /-! ### smtUDiv -/
 
 theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
@@ -2936,12 +2823,7 @@ theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by
 
 /-! # Rotate Left -/
 
-/--`rotateLeft` is defined in terms of left and right shifts. -/
-theorem rotateLeft_def {x : BitVec w} {r : Nat} :
-    x.rotateLeft r = (x <<< (r % w)) ||| (x >>> (w - r % w)) := by
-  simp only [rotateLeft, rotateLeftAux]
-
-/-- `rotateLeft` is invariant under `mod` by the bitwidth. -/
+/-- rotateLeft is invariant under `mod` by the bitwidth. -/
 @[simp]
 theorem rotateLeft_mod_eq_rotateLeft {x : BitVec w} {r : Nat} :
     x.rotateLeft (r % w) = x.rotateLeft r := by
@@ -3085,18 +2967,8 @@ theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
   · simp
     omega
 
-@[simp]
-theorem toNat_rotateLeft {x : BitVec w} {r : Nat} :
-    (x.rotateLeft r).toNat = (x.toNat <<< (r % w)) % (2^w) ||| x.toNat >>> (w - r % w) := by
-  simp only [rotateLeft_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
-
 /-! ## Rotate Right -/
 
-/-- `rotateRight` is defined in terms of left and right shifts. -/
-theorem rotateRight_def {x : BitVec w} {r : Nat} :
-    x.rotateRight r = (x >>> (r % w)) ||| (x <<< (w - r % w)) := by
-  simp only [rotateRight, rotateRightAux]
-
 /--
 Accessing bits in `x.rotateRight r` the range `[0, w-r)` is equal to
 accessing bits `x` in the range `[r, w)`.
@@ -3232,11 +3104,6 @@ theorem msb_rotateRight {r w : Nat} {x : BitVec w} :
     simp [h₁]
   · simp [show w = 0 by omega]
 
-@[simp]
-theorem toNat_rotateRight {x : BitVec w} {r : Nat} :
-    (x.rotateRight r).toNat = (x.toNat >>> (r % w)) ||| x.toNat <<< (w - r % w) % (2^w) := by
-  simp only [rotateRight_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
-
 /- ## twoPow -/
 
 theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by

src/Init/Data/List/Lemmas.lean

@@ -1285,7 +1285,7 @@ theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
 @[simp] theorem filter_append {p : α → Bool} :
     ∀ (l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
   | [], _ => rfl
-  | a :: l₁, l₂ => by simp only [cons_append, filter]; split <;> simp [filter_append l₁]
+  | a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
 
 theorem filter_eq_cons_iff {l} {a} {as} :
     filter p l = a :: as ↔

src/Init/Data/List/ToArray.lean

@@ -46,7 +46,7 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr
 @[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
   cases l <;> simp [Array.isEmpty]
 
-@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = Array.singleton a := rfl
+@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
 
 @[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
   simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]

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

@@ -49,17 +49,4 @@ theorem lt_div_mul_self (h : 0 < k) (w : k ≤ x) : x - k < x / k * k := by
   have : x % k < k := mod_lt x h
   omega
 
-theorem div_pos (hba : b ≤ a) (hb : 0 < b) : 0 < a / b := by
-  cases b
-  · contradiction
-  · simp [Nat.pos_iff_ne_zero, div_eq_zero_iff_lt, hba]
-
-theorem div_le_div_left (hcb : c ≤ b) (hc : 0 < c) : a / b ≤ a / c :=
-  (Nat.le_div_iff_mul_le hc).2 <|
-    Nat.le_trans (Nat.mul_le_mul_left _ hcb) (Nat.div_mul_le_self a b)
-
-theorem div_add_le_right {z : Nat} (h : 0 < z) (x y : Nat) :
-    x / (y + z) ≤ x / z :=
-  div_le_div_left (Nat.le_add_left z y) h
-
 end Nat

src/Init/Data/UInt/Basic.lean

@@ -159,8 +159,6 @@ def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩
 def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.toBitVec <<< (mod b 32).toBitVec⟩
 @[extern "lean_uint32_shift_right"]
 def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (mod b 32).toBitVec⟩
-def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
-def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
 
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
@@ -171,8 +169,6 @@ set_option linter.deprecated false in
 instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩
 
 instance : Div UInt32       := ⟨UInt32.div⟩
-instance : LT UInt32        := ⟨UInt32.lt⟩
-instance : LE UInt32        := ⟨UInt32.le⟩
 
 @[extern "lean_uint32_complement"]
 def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩

src/Init/Grind.lean

@@ -10,4 +10,3 @@ import Init.Grind.Lemmas
 import Init.Grind.Cases
 import Init.Grind.Propagator
 import Init.Grind.Util
-import Init.Grind.Offset

src/Init/Grind/Norm.lean

@@ -43,8 +43,8 @@ attribute [grind_norm] not_false_eq_true
 
 -- Remark: we disabled the following normalization rule because we want this information when implementing splitting heuristics
 -- Implication as a clause
-theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
-  by_cases p <;> by_cases q <;> simp [*]
+-- @[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
+--  by_cases p <;> by_cases q <;> simp [*]
 
 -- And
 @[grind_norm↓] theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by

src/Init/Grind/Offset.lean

@@ -1,165 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Core
-import Init.Omega
-
-namespace Lean.Grind.Offset
-
-abbrev Var := Nat
-abbrev Context := Lean.RArray Nat
-
-def fixedVar := 100000000 -- Any big number should work here
-
-def Var.denote (ctx : Context) (v : Var) : Nat :=
-  bif v == fixedVar then 1 else ctx.get v
-
-structure Cnstr where
-  x : Var
-  y : Var
-  k : Nat  := 0
-  l : Bool := true
-  deriving Repr, DecidableEq, Inhabited
-
-def Cnstr.denote (c : Cnstr) (ctx : Context) : Prop :=
-  if c.l then
-    c.x.denote ctx + c.k ≤ c.y.denote ctx
-  else
-    c.x.denote ctx ≤ c.y.denote ctx + c.k
-
-def trivialCnstr : Cnstr := { x := 0, y := 0, k := 0, l := true }
-
-@[simp] theorem denote_trivial (ctx : Context) : trivialCnstr.denote ctx := by
-  simp [Cnstr.denote, trivialCnstr]
-
-def Cnstr.trans (c₁ c₂ : Cnstr) : Cnstr :=
-  if c₁.y = c₂.x then
-    let { x, k := k₁, l := l₁, .. } := c₁
-    let { y, k := k₂, l := l₂, .. } := c₂
-    match l₁, l₂ with
-    | false, false =>
-      { x, y, k := k₁ + k₂, l := false }
-    | false, true =>
-      if k₁ < k₂ then
-        { x, y, k := k₂ - k₁, l := true }
-      else
-        { x, y, k := k₁ - k₂, l := false }
-    | true, false =>
-      if k₁ < k₂ then
-        { x, y, k := k₂ - k₁, l := false }
-      else
-        { x, y, k := k₁ - k₂, l := true }
-    | true, true =>
-      { x, y, k := k₁ + k₂, l := true }
-  else
-    trivialCnstr
-
-@[simp] theorem Cnstr.denote_trans_easy (ctx : Context) (c₁ c₂ : Cnstr) (h : c₁.y ≠ c₂.x) : (c₁.trans c₂).denote ctx := by
-  simp [*, Cnstr.trans]
-
-@[simp] theorem Cnstr.denote_trans (ctx : Context) (c₁ c₂ : Cnstr) : c₁.denote ctx → c₂.denote ctx → (c₁.trans c₂).denote ctx := by
-  by_cases c₁.y = c₂.x
-  case neg => simp [*]
-  simp [trans, *]
-  let { x, k := k₁, l := l₁, .. } := c₁
-  let { y, k := k₂, l := l₂, .. } := c₂
-  simp_all; split
-  · simp [denote]; omega
-  · split <;> simp [denote] <;> omega
-  · split <;> simp [denote] <;> omega
-  · simp [denote]; omega
-
-def Cnstr.isTrivial (c : Cnstr) : Bool := c.x == c.y && c.k == 0
-
-theorem Cnstr.of_isTrivial (ctx : Context) (c : Cnstr) : c.isTrivial = true → c.denote ctx := by
-  cases c; simp [isTrivial]; intros; simp [*, denote]
-
-def Cnstr.isFalse (c : Cnstr) : Bool := c.x == c.y && c.k != 0 && c.l == true
-
-theorem Cnstr.of_isFalse (ctx : Context) {c : Cnstr} : c.isFalse = true → ¬c.denote ctx := by
-  cases c; simp [isFalse]; intros; simp [*, denote]; omega
-
-def Cnstrs := List Cnstr
-
-def Cnstrs.denoteAnd' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : Prop :=
-  match c₂ with
-  | [] => c₁.denote ctx
-  | c::cs => c₁.denote ctx ∧ Cnstrs.denoteAnd' ctx c cs
-
-theorem Cnstrs.denote'_trans (ctx : Context) (c₁ c : Cnstr) (cs : Cnstrs) : c₁.denote ctx → denoteAnd' ctx c cs → denoteAnd' ctx (c₁.trans c) cs := by
-  induction cs
-  next => simp [denoteAnd', *]; apply Cnstr.denote_trans
-  next c cs ih => simp [denoteAnd']; intros; simp [*]
-
-def Cnstrs.trans' (c₁ : Cnstr) (c₂ : Cnstrs) : Cnstr :=
-  match c₂ with
-  | [] => c₁
-  | c::c₂ => trans' (c₁.trans c) c₂
-
-@[simp] theorem Cnstrs.denote'_trans' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : denoteAnd' ctx c₁ c₂ → (trans' c₁ c₂).denote ctx := by
-  induction c₂ generalizing c₁
-  next => intros; simp_all [trans', denoteAnd']
-  next c cs ih => simp [denoteAnd']; intros; simp [trans']; apply ih; apply denote'_trans <;> assumption
-
-def Cnstrs.denoteAnd (ctx : Context) (c : Cnstrs) : Prop :=
-  match c with
-  | [] => True
-  | c::cs => denoteAnd' ctx c cs
-
-def Cnstrs.trans (c : Cnstrs) : Cnstr :=
-  match c with
-  | []    => trivialCnstr
-  | c::cs => trans' c cs
-
-theorem Cnstrs.of_denoteAnd_trans {ctx : Context} {c : Cnstrs} : c.denoteAnd ctx → c.trans.denote ctx := by
-  cases c <;> simp [*, trans, denoteAnd] <;> intros <;> simp [*]
-
-def Cnstrs.isFalse (c : Cnstrs) : Bool :=
-  c.trans.isFalse
-
-theorem Cnstrs.unsat' (ctx : Context) (c : Cnstrs) : c.isFalse = true → ¬ c.denoteAnd ctx := by
-  simp [isFalse]; intro h₁ h₂
-  have := of_denoteAnd_trans h₂
-  have := Cnstr.of_isFalse ctx h₁
-  contradiction
-
-/-- `denote ctx [c_1, ..., c_n] C` is `c_1.denote ctx → ... → c_n.denote ctx → C` -/
-def Cnstrs.denote (ctx : Context) (cs : Cnstrs) (C : Prop) : Prop :=
-  match cs with
-  | [] => C
-  | c::cs => c.denote ctx → denote ctx cs C
-
-theorem Cnstrs.not_denoteAnd'_eq (ctx : Context) (c : Cnstr) (cs : Cnstrs) (C : Prop) : (denoteAnd' ctx c cs → C) = denote ctx (c::cs) C := by
-  simp [denote]
-  induction cs generalizing c
-  next => simp [denoteAnd', denote]
-  next c' cs ih =>
-    simp [denoteAnd', denote, *]
-
-theorem Cnstrs.not_denoteAnd_eq (ctx : Context) (cs : Cnstrs) (C : Prop) : (denoteAnd ctx cs → C) = denote ctx cs C := by
-  cases cs
-  next => simp [denoteAnd, denote]
-  next c cs => apply not_denoteAnd'_eq
-
-def Cnstr.isImpliedBy (cs : Cnstrs) (c : Cnstr) : Bool :=
-  cs.trans == c
-
-/-! Main theorems used by `grind`. -/
-
-/-- Auxiliary theorem used by `grind` to prove that a system of offset inequalities is unsatisfiable. -/
-theorem Cnstrs.unsat (ctx : Context) (cs : Cnstrs) : cs.isFalse = true → cs.denote ctx False := by
-  intro h
-  rw [← not_denoteAnd_eq]
-  apply unsat'
-  assumption
-
-/-- Auxiliary theorem used by `grind` to prove an implied offset inequality. -/
-theorem Cnstrs.imp (ctx : Context) (cs : Cnstrs) (c : Cnstr) (h : c.isImpliedBy cs = true)  : cs.denote ctx (c.denote ctx) := by
-  rw [← eq_of_beq h]
-  rw [← not_denoteAnd_eq]
-  apply of_denoteAnd_trans
-
-end Lean.Grind.Offset

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

@@ -7,10 +7,9 @@ prelude
 import Lean.Elab.Tactic.Simp
 import Lean.Elab.Tactic.Split
 import Lean.Elab.Tactic.Conv.Basic
-import Lean.Elab.Tactic.SimpTrace
 
 namespace Lean.Elab.Tactic.Conv
-open Meta Tactic TryThis
+open Meta
 
 def applySimpResult (result : Simp.Result) : TacticM Unit := do
   if result.proof?.isNone then
@@ -24,19 +23,6 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
   let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (simprocs := simprocs) (discharge? := d?)
   applySimpResult result
 
-@[builtin_tactic Lean.Parser.Tactic.Conv.simpTrace] def evalSimpTrace : Tactic := fun stx => withMainContext do
-  match stx with
-  | `(conv| simp?%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) => do
-    let stx ← `(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? $[[$args,*]]?)
-    let { ctx, simprocs, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
-    let lhs ← getLhs
-    let (result, stats) ← dischargeWrapper.with fun d? =>
-      simp lhs ctx (simprocs := simprocs) (discharge? := d?)
-    applySimpResult result
-    let stx ← mkSimpCallStx stx stats.usedTheorems
-    addSuggestion tk stx (origSpan? := ← getRef)
-  | _ => throwUnsupportedSyntax
-
 @[builtin_tactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun _ => withMainContext do
   applySimpResult (← Split.simpMatch (← getLhs))
 
@@ -44,15 +30,4 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
   let { ctx, .. } ← mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
   changeLhs (← Lean.Meta.dsimp (← getLhs) ctx).1
 
-@[builtin_tactic Lean.Parser.Tactic.Conv.dsimpTrace] def evalDSimpTrace : Tactic := fun stx => withMainContext do
-  match stx with
-  | `(conv| dsimp?%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]?) =>
-    let stx ← `(tactic| dsimp%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]?)
-    let { ctx, .. } ← mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
-    let (result, stats) ← Lean.Meta.dsimp (← getLhs) ctx
-    changeLhs result
-    let stx ← mkSimpCallStx stx stats.usedTheorems
-    addSuggestion tk stx (origSpan? := ← getRef)
-  | _ => throwUnsupportedSyntax
-
 end Lean.Elab.Tactic.Conv

src/Lean/Meta/Tactic/Grind.lean

@@ -53,5 +53,5 @@ builtin_initialize registerTraceClass `grind.debug.parent
 builtin_initialize registerTraceClass `grind.debug.final
 builtin_initialize registerTraceClass `grind.debug.forallPropagator
 builtin_initialize registerTraceClass `grind.debug.split
-builtin_initialize registerTraceClass `grind.debug.canon
+
 end Lean

src/Lean/Meta/Tactic/Grind/Canon.lean

@@ -46,35 +46,15 @@ structure State where
   proofCanon : PHashMap Expr Expr := {}
   deriving Inhabited
 
-inductive CanonElemKind where
-  | /--
-    Type class instances are canonicalized using `TransparencyMode.instances`.
-    -/
-    instance
-  | /--
-    Types and Type formers are canonicalized using `TransparencyMode.default`.
-    Remark: propositions are just visited. We do not invoke `canonElemCore` for them.
-    -/
-    type
-  | /--
-    Implicit arguments that are not types, type formers, or instances, are canonicalized
-    using `TransparencyMode.reducible`
-    -/
-    implicit
-  deriving BEq
-
-def CanonElemKind.explain : CanonElemKind → String
-  | .instance => "type class instances"
-  | .type => "types (or type formers)"
-  | .implicit => "implicit arguments (which are not type class instances or types)"
-
 /--
 Helper function for canonicalizing `e` occurring as the `i`th argument of an `f`-application.
+`isInst` is true if `e` is an type class instance.
 
-Thus, if diagnostics are enabled, we also re-check them using `TransparencyMode.default`. If the result is different
+Recall that we use `TransparencyMode.instances` for checking whether two instances are definitionally equal or not.
+Thus, if diagnostics are enabled, we also check them using `TransparencyMode.default`. If the result is different
 we report to the user.
 -/
-def canonElemCore (f : Expr) (i : Nat) (e : Expr) (kind : CanonElemKind) : StateT State MetaM Expr := do
+def canonElemCore (f : Expr) (i : Nat) (e : Expr) (isInst : Bool) : StateT State MetaM Expr := do
   let s ← get
   if let some c := s.canon.find? e then
     return c
@@ -86,19 +66,16 @@ def canonElemCore (f : Expr) (i : Nat) (e : Expr) (kind : CanonElemKind) : State
       -- in general safe to replace `e` with `c` if `c` has more free variables than `e`.
       -- However, we don't revert previously canonicalized elements in the `grind` tactic.
       modify fun s => { s with canon := s.canon.insert e c }
-      trace[grind.debug.canon] "found {e} ===> {c}"
       return c
-    if kind != .type then
-      if (← isTracingEnabledFor `grind.issues <&&> (withDefault <| isDefEq e c)) then
+    if isInst then
+      if (← isDiagnosticsEnabled <&&> pure (c.fvarsSubset e) <&&> (withDefault <| isDefEq e c)) then
         -- TODO: consider storing this information in some structure that can be browsed later.
-        trace[grind.issues] "the following {kind.explain} are definitionally equal with `default` transparency but not with a more restrictive transparency{indentExpr e}\nand{indentExpr c}"
-  trace[grind.debug.canon] "({f}, {i}) ↦ {e}"
+        trace[grind.issues] "the following `grind` static elements are definitionally equal with `default` transparency, but not with `instances` transparency{indentExpr e}\nand{indentExpr c}"
   modify fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key (e::cs) }
   return e
 
-abbrev canonType (f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore f i e .type
-abbrev canonInst (f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore f i e .instance
-abbrev canonImplicit (f : Expr) (i : Nat) (e : Expr) := withReducible <| canonElemCore f i e .implicit
+abbrev canonType (f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore f i e false
+abbrev canonInst (f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore f i e true
 
 /--
 Return type for the `shouldCanon` function.
@@ -108,8 +85,6 @@ private inductive ShouldCanonResult where
     canonType
   | /- Nested instances are canonicalized. -/
     canonInst
-  | /- Implicit argument that is not an instance nor a type. -/
-    canonImplicit
   | /-
     Term is not a proof, type (former), nor an instance.
     Thus, it must be recursively visited by the canonizer.
@@ -117,13 +92,6 @@ private inductive ShouldCanonResult where
     visit
   deriving Inhabited
 
-instance : Repr ShouldCanonResult where
-  reprPrec r _ := match r with
-    | .canonType => "canonType"
-    | .canonInst => "canonInst"
-    | .canonImplicit => "canonImplicit"
-    | .visit => "visit"
-
 /--
 See comments at `ShouldCanonResult`.
 -/
@@ -134,14 +102,7 @@ def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Should
       return .canonInst
     else if pinfo.isProp then
       return .visit
-    else if pinfo.isImplicit then
-      if (← isTypeFormer arg) then
-        return .canonType
-      else
-        return .canonImplicit
-  if (← isProp arg) then
-    return .visit
-  else if (← isTypeFormer arg) then
+  if (← isTypeFormer arg) then
     return .canonType
   else
     return .visit
@@ -171,11 +132,9 @@ where
           let mut args := args.toVector
           for h : i in [:args.size] do
             let arg := args[i]
-            trace[grind.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
             let arg' ← match (← shouldCanon pinfos i arg) with
             | .canonType  => canonType f i arg
             | .canonInst  => canonInst f i arg
-            | .canonImplicit => canonImplicit f i (← visit arg)
             | .visit      => visit arg
             unless ptrEq arg arg' do
               args := args.set i arg'
@@ -192,8 +151,7 @@ where
     return e'
 
 /-- Canonicalizes nested types, type formers, and instances in `e`. -/
-def canon (e : Expr) : StateT State MetaM Expr := do
-  trace[grind.debug.canon] "{e}"
+def canon (e : Expr) : StateT State MetaM Expr :=
   unsafe canonImpl e
 
 end Canon

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -499,7 +499,7 @@ def addEMatchEqTheorem (declName : Name) : MetaM Unit := do
 def getEMatchTheorems : CoreM EMatchTheorems :=
   return ematchTheoremsExt.getState (← getEnv)
 
-inductive TheoremKind where
+private inductive TheoremKind where
   | eqLhs | eqRhs | eqBoth | fwd | bwd | default
   deriving Inhabited, BEq
 

src/Lean/Meta/Tactic/Grind/ForallProp.lean

@@ -51,13 +51,6 @@ private def isEqTrueHyp? (proof : Expr) : Option FVarId := Id.run do
   let .fvar fvarId := p | return none
   return some fvarId
 
-/-- Similar to `mkEMatchTheoremWithKind?`, but swallow any exceptions. -/
-private def mkEMatchTheoremWithKind'? (origin : Origin) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
-  try
-    mkEMatchTheoremWithKind? origin #[] proof kind
-  catch _ =>
-    return none
-
 private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
   let proof ← mkEqTrueProof e
   let origin ← if let some fvarId := isEqTrueHyp? proof then
@@ -69,12 +62,12 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
   let size := (← get).newThms.size
   let gen ← getGeneration e
   -- TODO: we should have a flag for collecting all unary patterns in a local theorem
-  if let some thm ← mkEMatchTheoremWithKind'? origin proof .fwd then
+  if let some thm ← mkEMatchTheoremWithKind? origin #[] proof .fwd then
     activateTheorem thm gen
-  if let some thm ← mkEMatchTheoremWithKind'? origin proof .bwd then
+  if let some thm ← mkEMatchTheoremWithKind? origin #[] proof .bwd then
     activateTheorem thm gen
   if (← get).newThms.size == size then
-    if let some thm ← mkEMatchTheoremWithKind'? origin proof .default then
+    if let some thm ← mkEMatchTheoremWithKind? origin #[] proof .default then
       activateTheorem thm gen
   if (← get).newThms.size == size then
     trace[grind.issues] "failed to create E-match local theorem for{indentExpr e}"

src/Std.lean

@@ -10,4 +10,3 @@ import Std.Sync
 import Std.Time
 import Std.Tactic
 import Std.Internal
-import Std.Net

src/Std/Net.lean

@@ -1,7 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Std.Net.Addr

src/Std/Net/Addr.lean

@@ -1,197 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Init.Data.Vector.Basic
-
-/-!
-This module contains Lean representations of IP and socket addresses:
-- `IPv4Addr`: Representing IPv4 addresses.
-- `SocketAddressV4`: Representing a pair of IPv4 address and port.
-- `IPv6Addr`: Representing IPv6 addresses.
-- `SocketAddressV6`: Representing a pair of IPv6 address and port.
-- `IPAddr`: Can either be an `IPv4Addr` or an `IPv6Addr`.
-- `SocketAddress`: Can either be a `SocketAddressV4` or `SocketAddressV6`.
--/
-
-namespace Std
-namespace Net
-
-/--
-Representation of an IPv4 address.
--/
-structure IPv4Addr where
-  /--
-  This structure represents the address: `octets[0].octets[1].octets[2].octets[3]`.
-  -/
-  octets : Vector UInt8 4
-  deriving Inhabited, DecidableEq
-
-/--
-A pair of an `IPv4Addr` and a port.
--/
-structure SocketAddressV4 where
-  addr : IPv4Addr
-  port : UInt16
-  deriving Inhabited, DecidableEq
-
-/--
-Representation of an IPv6 address.
--/
-structure IPv6Addr where
-  /--
-  This structure represents the address: `segments[0]:segments[1]:...`.
-  -/
-  segments : Vector UInt16 8
-  deriving Inhabited, DecidableEq
-
-/--
-A pair of an `IPv6Addr` and a port.
--/
-structure SocketAddressV6 where
-  addr : IPv6Addr
-  port : UInt16
-  deriving Inhabited, DecidableEq
-
-/--
-An IP address, either IPv4 or IPv6.
--/
-inductive IPAddr where
-  | v4 (addr : IPv4Addr)
-  | v6 (addr : IPv6Addr)
-  deriving Inhabited, DecidableEq
-
-/--
-Either a `SocketAddressV4` or `SocketAddressV6`.
--/
-inductive SocketAddress where
-  | v4 (addr : SocketAddressV4)
-  | v6 (addr : SocketAddressV6)
-  deriving Inhabited, DecidableEq
-
-/--
-The kinds of address families supported by Lean, currently only IP variants.
--/
-inductive AddressFamily where
-  | ipv4
-  | ipv6
-  deriving Inhabited, DecidableEq
-
-namespace IPv4Addr
-
-/--
-Build the IPv4 address `a.b.c.d`.
--/
-def ofParts (a b c d : UInt8) : IPv4Addr :=
-  { octets := #v[a, b, c, d] }
-
-/--
-Try to parse `s` as an IPv4 address, returning `none` on failure.
--/
-@[extern "lean_uv_pton_v4"]
-opaque ofString (s : @&String) : Option IPv4Addr
-
-/--
-Turn `addr` into a `String` in the usual IPv4 format.
--/
-@[extern "lean_uv_ntop_v4"]
-opaque toString (addr : @&IPv4Addr) : String
-
-instance : ToString IPv4Addr where
-  toString := toString
-
-instance : Coe IPv4Addr IPAddr where
-  coe addr := .v4 addr
-
-end IPv4Addr
-
-namespace SocketAddressV4
-
-instance : Coe SocketAddressV4 SocketAddress where
-  coe addr := .v4 addr
-
-end SocketAddressV4
-
-namespace IPv6Addr
-
-/--
-Build the IPv6 address `a:b:c:d:e:f:g:h`.
--/
-def ofParts (a b c d e f g h : UInt16) : IPv6Addr :=
-  { segments := #v[a, b, c, d, e, f, g, h] }
-
-/--
-Try to parse `s` as an IPv6 address according to
-[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373), returning `none` on failure.
--/
-@[extern "lean_uv_pton_v6"]
-opaque ofString (s : @&String) : Option IPv6Addr
-
-/--
-Turn `addr` into a `String` in the IPv6 format described in
-[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373).
--/
-@[extern "lean_uv_ntop_v6"]
-opaque toString (addr : @&IPv6Addr) : String
-
-instance : ToString IPv6Addr where
-  toString := toString
-
-instance : Coe IPv6Addr IPAddr where
-  coe addr := .v6 addr
-
-end IPv6Addr
-
-namespace SocketAddressV6
-
-instance : Coe SocketAddressV6 SocketAddress where
-  coe addr := .v6 addr
-
-end SocketAddressV6
-
-namespace IPAddr
-
-/--
-Obtain the `AddressFamily` associated with an `IPAddr`.
--/
-def family : IPAddr → AddressFamily
-  | .v4 .. => .ipv4
-  | .v6 .. => .ipv6
-
-def toString : IPAddr → String
-  | .v4 addr => addr.toString
-  | .v6 addr => addr.toString
-
-instance : ToString IPAddr where
-  toString := toString
-
-end IPAddr
-
-namespace SocketAddress
-
-/--
-Obtain the `AddressFamily` associated with a `SocketAddress`.
--/
-def family : SocketAddress → AddressFamily
-  | .v4 .. => .ipv4
-  | .v6 .. => .ipv6
-
-/--
-Obtain the `IPAddr` contained in a `SocketAddress`.
--/
-def ipAddr : SocketAddress → IPAddr
-  | .v4 sa  => .v4 sa.addr
-  | .v6 sa  => .v6 sa.addr
-
-/--
-Obtain the port contained in a `SocketAddress`.
--/
-def port : SocketAddress → UInt16
-  | .v4 sa | .v6 sa => sa.port
-
-end SocketAddress
-
-end Net
-end Std

src/Std/Time/Date/Unit/Month.lean

@@ -39,12 +39,6 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 def Offset : Type := Int
   deriving Repr, BEq, Inhabited, Add, Sub, Mul, Div, Neg, ToString, LT, LE, DecidableEq
 
-instance {x y : Offset} : Decidable (x ≤ y) :=
-  Int.decLe x y
-
-instance {x y : Offset} : Decidable (x < y) :=
-  Int.decLt x y
-
 instance : OfNat Offset n :=
   ⟨Int.ofNat n⟩
 

src/Std/Time/Date/Unit/Week.lean

@@ -39,12 +39,6 @@ instance : Inhabited Ordinal where
 def Offset : Type := UnitVal (86400 * 7)
   deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
-instance {x y : Offset} : Decidable (x ≤ y) :=
-  inferInstanceAs (Decidable (x.val ≤ y.val))
-
-instance {x y : Offset} : Decidable (x < y) :=
-  inferInstanceAs (Decidable (x.val < y.val))
-
 instance : OfNat Offset n := ⟨UnitVal.ofNat n⟩
 
 namespace Ordinal

src/Std/Time/Time/Unit/Hour.lean

@@ -40,13 +40,7 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 or differences in hours.
 -/
 def Offset : Type := UnitVal 3600
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
-
-instance { x y : Offset } : Decidable (x ≤ y) :=
-  inferInstanceAs (Decidable (x.val ≤ y.val))
-
-instance { x y : Offset } : Decidable (x < y) :=
-  inferInstanceAs (Decidable (x.val < y.val))
+  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩

src/Std/Time/Time/Unit/Millisecond.lean

@@ -40,12 +40,6 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 def Offset : Type := UnitVal (1 / 1000)
   deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
-instance { x y : Offset } : Decidable (x ≤ y) :=
-  inferInstanceAs (Decidable (x.val ≤ y.val))
-
-instance { x y : Offset } : Decidable (x < y) :=
-  inferInstanceAs (Decidable (x.val < y.val))
-
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 

src/Std/Time/Time/Unit/Minute.lean

@@ -38,13 +38,7 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 `Offset` represents a duration offset in minutes.
 -/
 def Offset : Type := UnitVal 60
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
-
-instance { x y : Offset } : Decidable (x ≤ y) :=
-  inferInstanceAs (Decidable (x.val ≤ y.val))
-
-instance { x y : Offset } : Decidable (x < y) :=
-  inferInstanceAs (Decidable (x.val < y.val))
+  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofInt <| Int.ofNat n⟩

src/Std/Time/Time/Unit/Nanosecond.lean

@@ -42,9 +42,6 @@ def Offset : Type := UnitVal (1 / 1000000000)
 instance { x y : Offset } : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
-instance { x y : Offset } : Decidable (x < y) :=
-  inferInstanceAs (Decidable (x.val < y.val))
-
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 

src/Std/Time/Time/Unit/Second.lean

@@ -51,12 +51,6 @@ instance {x y : Ordinal l} : Decidable (x < y) :=
 def Offset : Type := UnitVal 1
   deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
-instance { x y : Offset } : Decidable (x ≤ y) :=
-  inferInstanceAs (Decidable (x.val ≤ y.val))
-
-instance { x y : Offset } : Decidable (x < y) :=
-  inferInstanceAs (Decidable (x.val < y.val))
-
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 

src/runtime/CMakeLists.txt

@@ -2,7 +2,7 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
 object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
 stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
-process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp)
+process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp)
 add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
 set_target_properties(leanrt_initial-exec PROPERTIES
   ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})

src/runtime/uv/net_addr.cpp

@@ -1,131 +0,0 @@
-/*
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Henrik Böving
-*/
-
-#include "runtime/uv/net_addr.h"
-#include <cstring>
-
-namespace lean {
-
-#ifndef LEAN_EMSCRIPTEN
-
-void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, in_addr* out) {
-    out->s_addr = 0;
-    for (int i = 0; i < 4; i++) {
-        uint32_t octet = (uint32_t)(uint8_t)lean_unbox(array_uget(ipv4_addr, i));
-        out->s_addr |= octet << (3 - i) * 8;
-    }
-    out->s_addr = htonl(out->s_addr);
-}
-
-void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, in6_addr* out) {
-    for (int i = 0; i < 8; i++) {
-        uint16_t segment = htons((uint16_t)lean_unbox(array_uget(ipv6_addr, i)));
-        out->s6_addr[2 * i] = (uint8_t)segment;
-        out->s6_addr[2 * i + 1] = (uint8_t)(segment >> 8);
-    }
-}
-
-lean_obj_res lean_in_addr_to_ipv4_addr(const in_addr* ipv4_addr) {
-    obj_res ret = alloc_array(0, 4);
-    uint32_t hostaddr = ntohl(ipv4_addr->s_addr);
-
-    for (int i = 0; i < 4; i++) {
-        uint8_t octet = (uint8_t)(hostaddr >> (3 - i) * 8);
-        array_push(ret, lean_box(octet));
-    }
-
-    lean_assert(array_size(ret) == 4);
-    return ret;
-}
-
-lean_obj_res lean_in6_addr_to_ipv6_addr(const in6_addr* ipv6_addr) {
-    obj_res ret = alloc_array(0, 8);
-
-    for (int i = 0; i < 16; i += 2) {
-        uint16_t part1 = (uint16_t)ipv6_addr->s6_addr[i];
-        uint16_t part2 = (uint16_t)ipv6_addr->s6_addr[i + 1];
-        uint16_t segment = ntohs((part2 << 8) | part1);
-        array_push(ret, lean_box(segment));
-    }
-
-    lean_assert(array_size(ret) == 8);
-    return ret;
-}
-
-/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) {
-    const char* str = string_cstr(str_obj);
-    in_addr internal;
-    if (uv_inet_pton(AF_INET, str, &internal) == 0) {
-        return mk_option_some(lean_in_addr_to_ipv4_addr(&internal));
-    } else {
-        return mk_option_none();
-    }
-}
-
-/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) {
-    in_addr internal;
-    lean_ipv4_addr_to_in_addr(ipv4_addr, &internal);
-    char dst[INET_ADDRSTRLEN];
-    int ret = uv_inet_ntop(AF_INET, &internal, dst, sizeof(dst));
-    lean_always_assert(ret == 0);
-    return lean_mk_string(dst);
-}
-
-/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) {
-    const char* str = string_cstr(str_obj);
-    in6_addr internal;
-    if (uv_inet_pton(AF_INET6, str, &internal) == 0) {
-        return mk_option_some(lean_in6_addr_to_ipv6_addr(&internal));
-    } else {
-        return mk_option_none();
-    }
-}
-
-/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
-    in6_addr internal;
-    lean_ipv6_addr_to_in6_addr(ipv6_addr, &internal);
-    char dst[INET6_ADDRSTRLEN];
-    int ret = uv_inet_ntop(AF_INET6, &internal, dst, sizeof(dst));
-    lean_always_assert(ret == 0);
-    return lean_mk_string(dst);
-}
-
-#else
-
-/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) {
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with libuv to invoke this.")
-    );
-}
-
-/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) {
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with libuv to invoke this.")
-    );
-}
-
-/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) {
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with libuv to invoke this.")
-    );
-}
-
-/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with libuv to invoke this.")
-    );
-}
-
-#endif
-}

src/runtime/uv/net_addr.h

@@ -1,28 +0,0 @@
-/*
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Henrik Böving
-*/
-#pragma once
-#include <lean/lean.h>
-#include "runtime/object.h"
-
-
-namespace lean {
-
-#ifndef LEAN_EMSCRIPTEN
-#include <uv.h>
-
-void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, struct in_addr* out);
-void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, struct in6_addr* out);
-lean_obj_res lean_in_addr_to_ipv4_addr(const struct in_addr* ipv4_addr);
-lean_obj_res lean_in6_addr_to_ipv6_addr(const struct in6_addr* ipv6_addr);
-
-#endif
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr);
-
-}