fix

This PR fixes a bug in the pattern selection in the `grind`.

doc/dev/ffi.md

@@ -49,8 +49,9 @@ 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 `α`.
-* `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`).
+  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`).
 * 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,16 +37,32 @@ 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:
-    - [lean4checker](https://github.com/leanprover/lean4checker)
-      - No dependencies
-      - Toolchain bump PR
-      - Create and push the tag
-      - Merge the tag into `stable`
     - [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)
+      - No dependencies
+      - Toolchain bump PR
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
     - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
       - Dependencies: `Batteries`
       - Note on versions and branches:
@@ -61,17 +77,6 @@ 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,6 +27,13 @@ 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,6 +150,10 @@ 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.
@@ -167,6 +171,9 @@ 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,8 +244,7 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
 def range (n : Nat) : Array Nat :=
   ofFn fun (i : Fin n) => i
 
-def singleton (v : α) : Array α :=
-  mkArray 1 v
+@[inline] protected def singleton (v : α) : Array α := #[v]
 
 def back! [Inhabited α] (a : Array α) : α :=
   a[a.size - 1]!

src/Init/Data/Array/Lemmas.lean

@@ -1506,9 +1506,99 @@ theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array
 
 /-! 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 singleton_def (v : α) : singleton v = #[v] := 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
+
 
 -- This is a duplicate of `List.toArray_toList`.
 -- It's confusing to guess which namespace this theorem should live in,
@@ -2122,74 +2212,6 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
 
-/-! ### append -/
-
-@[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 α)} :

src/Init/Data/BitVec/Lemmas.lean

@@ -9,7 +9,9 @@ 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
 
@@ -98,6 +100,12 @@ 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 :=
@@ -442,6 +450,10 @@ 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]
 
@@ -454,6 +466,9 @@ 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]
@@ -2300,6 +2315,12 @@ 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]
@@ -2586,13 +2607,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
-  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)
+  rfl
 
 @[simp]
 theorem zero_udiv {x : BitVec w} : (0#w) / x = 0#w := by
@@ -2628,6 +2649,45 @@ 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} :
@@ -2640,6 +2700,10 @@ 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]
@@ -2667,6 +2731,55 @@ 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
@@ -2823,7 +2936,12 @@ theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by
 
 /-! # Rotate Left -/
 
-/-- rotateLeft is invariant under `mod` by the bitwidth. -/
+/--`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. -/
 @[simp]
 theorem rotateLeft_mod_eq_rotateLeft {x : BitVec w} {r : Nat} :
     x.rotateLeft (r % w) = x.rotateLeft r := by
@@ -2967,8 +3085,18 @@ 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)`.
@@ -3104,6 +3232,11 @@ 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/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 = singleton a := rfl
+@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = Array.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,4 +49,17 @@ 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,6 +159,8 @@ 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⟩
@@ -169,6 +171,8 @@ 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/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
--- @[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
---  by_cases p <;> by_cases q <;> simp [*]
+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

@@ -7,7 +7,7 @@ prelude
 import Init.Core
 import Init.Omega
 
-namespace Lean.Grind
+namespace Lean.Grind.Offset
 
 abbrev Var := Nat
 abbrev Context := Lean.RArray Nat
@@ -22,7 +22,7 @@ structure Cnstr where
   y : Var
   k : Nat  := 0
   l : Bool := true
-  deriving Repr, BEq, Inhabited
+  deriving Repr, DecidableEq, Inhabited
 
 def Cnstr.denote (c : Cnstr) (ctx : Context) : Prop :=
   if c.l then
@@ -82,51 +82,84 @@ 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 Certificate := List Cnstr
+def Cnstrs := List Cnstr
 
-def Certificate.denote' (ctx : Context) (c₁ : Cnstr) (c₂ : Certificate) : Prop :=
+def Cnstrs.denoteAnd' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : Prop :=
   match c₂ with
   | [] => c₁.denote ctx
-  | c::cs => c₁.denote ctx ∧ Certificate.denote' ctx c cs
+  | c::cs => c₁.denote ctx ∧ Cnstrs.denoteAnd' ctx c cs
 
-theorem Certificate.denote'_trans (ctx : Context) (c₁ c : Cnstr) (cs : Certificate) : c₁.denote ctx → denote' ctx c cs → denote' ctx (c₁.trans c) cs := by
+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 [denote', *]; apply Cnstr.denote_trans
-  next c cs ih => simp [denote']; intros; simp [*]
+  next => simp [denoteAnd', *]; apply Cnstr.denote_trans
+  next c cs ih => simp [denoteAnd']; intros; simp [*]
 
-def Certificate.trans' (c₁ : Cnstr) (c₂ : Certificate) : Cnstr :=
+def Cnstrs.trans' (c₁ : Cnstr) (c₂ : Cnstrs) : Cnstr :=
   match c₂ with
   | [] => c₁
   | c::c₂ => trans' (c₁.trans c) c₂
 
-@[simp] theorem Certificate.denote'_trans' (ctx : Context) (c₁ : Cnstr) (c₂ : Certificate) : denote' ctx c₁ c₂ → (trans' c₁ c₂).denote ctx := by
+@[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', denote']
-  next c cs ih => simp [denote']; intros; simp [trans']; apply ih; apply denote'_trans <;> assumption
+  next => intros; simp_all [trans', denoteAnd']
+  next c cs ih => simp [denoteAnd']; intros; simp [trans']; apply ih; apply denote'_trans <;> assumption
 
-def Certificate.denote (ctx : Context) (c : Certificate) : Prop :=
+def Cnstrs.denoteAnd (ctx : Context) (c : Cnstrs) : Prop :=
   match c with
   | [] => True
-  | c::cs => denote' ctx c cs
+  | c::cs => denoteAnd' ctx c cs
 
-def Certificate.trans (c : Certificate) : Cnstr :=
+def Cnstrs.trans (c : Cnstrs) : Cnstr :=
   match c with
   | []    => trivialCnstr
   | c::cs => trans' c cs
 
-theorem Certificate.denote_trans {ctx : Context} {c : Certificate} : c.denote ctx → c.trans.denote ctx := by
-  cases c <;> simp [*, trans, Certificate.denote] <;> intros <;> simp [*]
+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 Certificate.isFalse (c : Certificate) : Bool :=
+def Cnstrs.isFalse (c : Cnstrs) : Bool :=
   c.trans.isFalse
 
-theorem Certificate.unsat (ctx : Context) (c : Certificate) : c.isFalse = true → ¬ c.denote ctx := by
+theorem Cnstrs.unsat' (ctx : Context) (c : Cnstrs) : c.isFalse = true → ¬ c.denoteAnd ctx := by
   simp [isFalse]; intro h₁ h₂
-  have := Certificate.denote_trans h₂
+  have := of_denoteAnd_trans h₂
   have := Cnstr.of_isFalse ctx h₁
   contradiction
 
-theorem Certificate.imp (ctx : Context) (c : Certificate) : c.denote ctx → c.trans.denote ctx := by
-  apply denote_trans
+/-- `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
 
-end Lean.Grind
+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,9 +7,10 @@ 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
+open Meta Tactic TryThis
 
 def applySimpResult (result : Simp.Result) : TacticM Unit := do
   if result.proof?.isNone then
@@ -23,6 +24,19 @@ 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))
 
@@ -30,4 +44,15 @@ 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/Canon.lean

@@ -46,15 +46,35 @@ 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.
 
-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
+Thus, if diagnostics are enabled, we also re-check them using `TransparencyMode.default`. If the result is different
 we report to the user.
 -/
-def canonElemCore (f : Expr) (i : Nat) (e : Expr) (isInst : Bool) : StateT State MetaM Expr := do
+def canonElemCore (f : Expr) (i : Nat) (e : Expr) (kind : CanonElemKind) : StateT State MetaM Expr := do
   let s ← get
   if let some c := s.canon.find? e then
     return c
@@ -68,16 +88,17 @@ def canonElemCore (f : Expr) (i : Nat) (e : Expr) (isInst : Bool) : StateT State
       modify fun s => { s with canon := s.canon.insert e c }
       trace[grind.debug.canon] "found {e} ===> {c}"
       return c
-    if isInst then
-      if (← isDiagnosticsEnabled <&&> (withDefault <| isDefEq e c)) then
+    if kind != .type then
+      if (← isTracingEnabledFor `grind.issues <&&> (withDefault <| isDefEq e c)) then
         -- TODO: consider storing this information in some structure that can be browsed later.
-        trace[grind.issues] "the following `grind` static elements are definitionally equal with `default` transparency, but not with `instances` transparency{indentExpr e}\nand{indentExpr c}"
+        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}"
   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 false
-abbrev canonInst (f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore f i e true
+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
 
 /--
 Return type for the `shouldCanon` function.
@@ -87,6 +108,8 @@ 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.
@@ -98,6 +121,7 @@ instance : Repr ShouldCanonResult where
   reprPrec r _ := match r with
     | .canonType => "canonType"
     | .canonInst => "canonInst"
+    | .canonImplicit => "canonImplicit"
     | .visit => "visit"
 
 /--
@@ -110,6 +134,11 @@ 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
@@ -142,9 +171,11 @@ 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'

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)
 
-private inductive TheoremKind where
+inductive TheoremKind where
   | eqLhs | eqRhs | eqBoth | fwd | bwd | default
   deriving Inhabited, BEq
 

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

@@ -51,6 +51,13 @@ 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
@@ -62,12 +69,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,3 +10,4 @@ import Std.Sync
 import Std.Time
 import Std.Tactic
 import Std.Internal
+import Std.Net

src/Std/Net.lean

@@ -0,0 +1,7 @@
+/-
+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

@@ -0,0 +1,197 @@
+/-
+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,6 +39,12 @@ 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,6 +39,12 @@ 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,7 +40,13 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 or differences in hours.
 -/
 def Offset : Type := UnitVal 3600
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString
+  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))
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩

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

@@ -40,6 +40,12 @@ 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,7 +38,13 @@ 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
+  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))
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofInt <| Int.ofNat n⟩

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

@@ -42,6 +42,9 @@ 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,6 +51,12 @@ 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)
+process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.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

@@ -0,0 +1,131 @@
+/*
+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

@@ -0,0 +1,28 @@
+/*
+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);
+
+}