improve conversion lemma signatures

src/Init/Data/Range/Polymorphic.lean

@@ -12,6 +12,8 @@ public import Init.Data.Range.Polymorphic.Stream
 public import Init.Data.Range.Polymorphic.Lemmas
 public import Init.Data.Range.Polymorphic.Nat
 public import Init.Data.Range.Polymorphic.Int
+public import Init.Data.Range.Polymorphic.BitVec
+public import Init.Data.Range.Polymorphic.UInt
 public import Init.Data.Range.Polymorphic.NatLemmas
 public import Init.Data.Range.Polymorphic.GetElemTactic
 

src/Init/Data/Range/Polymorphic/BitVec.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Range.Polymorphic.Instances
+public import Init.Data.Order.Lemmas
+public import Init.Data.UInt
+import Init.Omega
+
+public section
+
+open Std Std.PRange
+
+namespace BitVec
+
+variable {n : Nat}
+
+instance : UpwardEnumerable (BitVec n) where
+  succ? i := if i + 1 = 0 then none else some (i + 1)
+  succMany? m i := if h : i.toNat + m < 2 ^ n then some (.ofNatLT _ h) else none
+
+instance : LawfulUpwardEnumerable (BitVec n) where
+  ne_of_lt := by
+    simp +contextual [UpwardEnumerable.LT, ← BitVec.toNat_inj, succMany?] at ⊢
+    omega
+  succMany?_zero := by simp [UpwardEnumerable.succMany?, BitVec.toNat_lt_twoPow_of_le]
+  succMany?_succ? a b := by
+    simp +contextual [← BitVec.toNat_inj, succMany?, succ?]
+    split <;> split
+    · rename_i h
+      simp [← BitVec.toNat_inj, Nat.mod_eq_of_lt (a := b.toNat + a + 1) ‹_›]
+      all_goals omega
+    · omega
+    · have : b.toNat + a + 1 = 2 ^ n := by omega
+      simp [this]
+    · simp
+
+instance : LawfulUpwardEnumerableLE (BitVec n) where
+  le_iff x y := by
+    simp [UpwardEnumerable.LE, UpwardEnumerable.succMany?, BitVec.le_def]
+    apply Iff.intro
+    · intro hle
+      refine ⟨y.toNat - x.toNat, ?_⟩
+      apply Exists.intro <;> simp [Nat.add_sub_cancel' hle, BitVec.toNat_lt_twoPow_of_le]
+    · rintro ⟨n, hn, rfl⟩
+      simp [BitVec.ofNatLT]
+
+instance : LawfulOrderLT (BitVec n) := inferInstance
+instance : LawfulUpwardEnumerableLT (BitVec n) := inferInstance
+instance : LawfulUpwardEnumerableLT (BitVec n) := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .closed (BitVec n) := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .closed (BitVec n) := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .open (BitVec n) := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .open (BitVec n) := inferInstance
+
+instance : RangeSize .closed (BitVec n) where
+  size bound a := bound.toNat + 1 - a.toNat
+
+instance : RangeSize .open (BitVec n) := RangeSize.openOfClosed
+
+instance : LawfulRangeSize .closed (BitVec n) where
+  size_eq_zero_of_not_isSatisfied bound x := by
+    simp [SupportsUpperBound.IsSatisfied, BitVec.not_le, RangeSize.size, BitVec.lt_def]
+    omega
+  size_eq_one_of_succ?_eq_none bound x := by
+    have := BitVec.toNat_lt_twoPow_of_le (Nat.le_refl _) (x := bound)
+    have (h : (x.toNat + 1) % 2 ^ n = 0) : x.toNat = 2 ^ n - 1 := by
+      apply Classical.not_not.mp
+      intro _
+      simp [Nat.mod_eq_of_lt (a := x.toNat + 1) (b := 2 ^ n) (by omega)] at h
+    simp [RangeSize.size, BitVec.le_def, ← BitVec.toNat_inj, succ?]
+    omega
+  size_eq_succ_of_succ?_eq_some bound init x := by
+    have (h : ¬ (init.toNat + 1) % 2 ^ n = 0) : ¬ (init.toNat + 1 ≥ 2 ^ n) := by
+      intro _
+      have : init.toNat + 1 = 2 ^ n := by omega
+      simp_all
+    simp_all +contextual [RangeSize.size, BitVec.le_def, ← BitVec.toNat_inj,
+      Nat.mod_eq_of_lt (a := init.toNat + 1) (b := 2 ^ n), succ?]
+    omega
+
+instance : LawfulRangeSize .open (BitVec n) := inferInstance
+
+end BitVec

src/Init/Data/Range/Polymorphic/Int.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Range.Polymorphic.Instances
 public import Init.Data.Order.Classes
+public import Init.Data.Int.Order
 import Init.Omega
 
 public section
@@ -23,7 +24,7 @@ instance : LawfulUpwardEnumerable Int where
     simp only [UpwardEnumerable.LT, UpwardEnumerable.succMany?, Option.some.injEq]
     omega
   succMany?_zero := by simp [UpwardEnumerable.succMany?]
-  succMany?_succ := by
+  succMany?_succ? := by
     simp only [UpwardEnumerable.succMany?, UpwardEnumerable.succ?,
       Option.bind_some, Option.some.injEq]
     omega
@@ -36,6 +37,14 @@ instance : LawfulUpwardEnumerableLE Int where
     simp [UpwardEnumerable.LE, UpwardEnumerable.succMany?, Int.le_def, Int.nonneg_def,
       Int.sub_eq_iff_eq_add', eq_comm (a := y)]
 
+instance : LawfulOrderLT Int := inferInstance
+instance : LawfulUpwardEnumerableLT Int := inferInstance
+instance : LawfulUpwardEnumerableLT Int := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .closed Int := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .closed Int := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .open Int := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .open Int := inferInstance
+
 instance : RangeSize .closed Int where
   size bound a := (bound + 1 - a).toNat
 

src/Init/Data/Range/Polymorphic/Nat.lean

@@ -10,10 +10,12 @@ import Init.Data.Nat.Lemmas
 public import Init.Data.Nat.Order
 public import Init.Data.Range.Polymorphic.Instances
 public import Init.Data.Order.Classes
-import Init.Data.Order.Lemmas
+public import Init.Data.Order.Lemmas
 
 public section
 
+open Std PRange
+
 namespace Std.PRange
 
 instance : UpwardEnumerable Nat where
@@ -39,7 +41,7 @@ instance : LawfulUpwardEnumerableLE Nat where
 
 instance : LawfulUpwardEnumerable Nat where
   succMany?_zero := by simp [UpwardEnumerable.succMany?]
-  succMany?_succ := by simp [UpwardEnumerable.succMany?, UpwardEnumerable.succ?, Nat.add_assoc]
+  succMany?_succ? := by simp [UpwardEnumerable.succMany?, UpwardEnumerable.succ?, Nat.add_assoc]
   ne_of_lt a b hlt := by
     have hn := hlt.choose_spec
     simp only [UpwardEnumerable.succMany?, Option.some.injEq] at hn
@@ -76,8 +78,7 @@ instance : LawfulRangeSize .closed Nat where
 instance : LawfulRangeSize .open Nat := inferInstance
 instance : HasFiniteRanges .closed Nat := inferInstance
 instance : HasFiniteRanges .open Nat := inferInstance
-instance : LinearlyUpwardEnumerable Nat := by
-  exact instLinearlyUpwardEnumerableOfTotalLeOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLE
+instance : LinearlyUpwardEnumerable Nat := inferInstance
 
 /-!
 The following instances are used for the implementation of array slices a.k.a. `Subarray`.

src/Init/Data/Range/Polymorphic/UInt.lean

@@ -0,0 +1,382 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Range.Polymorphic.Instances
+public import Init.Data.Order.Lemmas
+public import Init.Data.UInt
+import Init.Omega
+public import Init.Data.Range.Polymorphic.BitVec
+
+public section
+
+open Std Std.PRange
+
+namespace UInt8
+
+instance : UpwardEnumerable UInt8 where
+  succ? i := if i + 1 = 0 then none else some (i + 1)
+  succMany? n i := if h : i.toNat + n < UInt8.size then some (.ofNatLT _ h) else none
+
+theorem succ?_ofBitVec {x : BitVec 8} :
+    UpwardEnumerable.succ? (UInt8.ofBitVec x) = UInt8.ofBitVec <$> UpwardEnumerable.succ? x := by
+  simp only [succ?, BitVec.ofNat_eq_ofNat, Option.map_eq_map, ← UInt8.toBitVec_inj]
+  split <;> simp_all
+
+theorem succMany?_ofBitVec {k : Nat} {x : BitVec 8} :
+    UpwardEnumerable.succMany? k (UInt8.ofBitVec x) = UInt8.ofBitVec <$> UpwardEnumerable.succMany? k x := by
+  simp [succMany?]
+
+theorem upwardEnumerableLE_ofBitVec {x y : BitVec 8} :
+    UpwardEnumerable.LE (UInt8.ofBitVec x) (UInt8.ofBitVec y) ↔ UpwardEnumerable.LE x y := by
+  simp [UpwardEnumerable.LE, succMany?_ofBitVec]
+
+theorem upwardEnumerableLT_ofBitVec {x y : BitVec 8} :
+    UpwardEnumerable.LT (UInt8.ofBitVec x) (UInt8.ofBitVec y) ↔ UpwardEnumerable.LT x y := by
+  simp [UpwardEnumerable.LT, succMany?_ofBitVec]
+
+instance : LawfulUpwardEnumerable UInt8 where
+  ne_of_lt x y := by
+    cases x; cases y
+    simpa [upwardEnumerableLT_ofBitVec] using LawfulUpwardEnumerable.ne_of_lt _ _
+  succMany?_zero x := by
+    cases x
+    simpa [succMany?_ofBitVec] using succMany?_zero
+  succMany?_succ? n x := by
+    cases x
+    simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def,
+      succ?_ofBitVec]
+
+instance : LawfulUpwardEnumerableLE UInt8 where
+  le_iff x y := by
+    cases x; cases y
+    simpa [upwardEnumerableLE_ofBitVec, UInt8.le_iff_toBitVec_le] using
+      LawfulUpwardEnumerableLE.le_iff _ _
+
+instance : LawfulOrderLT UInt8 := inferInstance
+instance : LawfulUpwardEnumerableLT UInt8 := inferInstance
+instance : LawfulUpwardEnumerableLT UInt8 := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .closed UInt8 := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .closed UInt8 := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .open UInt8 := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .open UInt8 := inferInstance
+
+instance : RangeSize .closed UInt8 where
+  size bound a := bound.toNat + 1 - a.toNat
+
+theorem rangeSizeSize_eq_toBitVec {bound : Bound .closed UInt8} {x : BitVec 8} :
+    RangeSize.size bound (UInt8.ofBitVec x) = RangeSize.size (shape := .closed) bound.toBitVec x := by
+  simp [RangeSize.size]
+
+instance : LawfulRangeSize .closed UInt8 where
+  size_eq_zero_of_not_isSatisfied bound x := by
+    simpa [rangeSizeSize_eq_toBitVec, UInt8.lt_iff_toBitVec_lt] using
+      LawfulRangeSize.size_eq_zero_of_not_isSatisfied (su := .closed) (α := BitVec 8) _ _
+  size_eq_one_of_succ?_eq_none bound x := by
+    cases x
+    simpa [rangeSizeSize_eq_toBitVec, UInt8.le_iff_toBitVec_le, succ?_ofBitVec] using
+      LawfulRangeSize.size_eq_one_of_succ?_eq_none (su := .closed) (α := BitVec 8) _ _
+  size_eq_succ_of_succ?_eq_some bound init x := by
+    simpa [rangeSizeSize_eq_toBitVec, UInt8.le_iff_toBitVec_le, ← UInt8.toBitVec_inj, succ?] using
+      LawfulRangeSize.size_eq_succ_of_succ?_eq_some (su := .closed) (α := BitVec 8) _ _ _
+
+instance : RangeSize .open UInt8 := RangeSize.openOfClosed
+instance : LawfulRangeSize .open UInt8 := inferInstance
+
+end UInt8
+
+namespace UInt16
+
+instance : UpwardEnumerable UInt16 where
+  succ? i := if i + 1 = 0 then none else some (i + 1)
+  succMany? n i := if h : i.toNat + n < UInt16.size then some (.ofNatLT _ h) else none
+
+theorem succ?_ofBitVec {x : BitVec 16} :
+    UpwardEnumerable.succ? (UInt16.ofBitVec x) = UInt16.ofBitVec <$> UpwardEnumerable.succ? x := by
+  simp only [succ?, BitVec.ofNat_eq_ofNat, Option.map_eq_map, ← UInt16.toBitVec_inj]
+  split <;> simp_all
+
+theorem succMany?_ofBitVec {k : Nat} {x : BitVec 16} :
+    UpwardEnumerable.succMany? k (UInt16.ofBitVec x) = UInt16.ofBitVec <$> UpwardEnumerable.succMany? k x := by
+  simp [succMany?]
+
+theorem upwardEnumerableLE_ofBitVec {x y : BitVec 16} :
+    UpwardEnumerable.LE (UInt16.ofBitVec x) (UInt16.ofBitVec y) ↔ UpwardEnumerable.LE x y := by
+  simp [UpwardEnumerable.LE, succMany?_ofBitVec]
+
+theorem upwardEnumerableLT_ofBitVec {x y : BitVec 16} :
+    UpwardEnumerable.LT (UInt16.ofBitVec x) (UInt16.ofBitVec y) ↔ UpwardEnumerable.LT x y := by
+  simp [UpwardEnumerable.LT, succMany?_ofBitVec]
+
+instance : LawfulUpwardEnumerable UInt16 where
+  ne_of_lt x y := by
+    cases x; cases y
+    simpa [upwardEnumerableLT_ofBitVec] using LawfulUpwardEnumerable.ne_of_lt _ _
+  succMany?_zero x := by
+    cases x
+    simpa [succMany?_ofBitVec] using succMany?_zero
+  succMany?_succ? n x := by
+    cases x
+    simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def,
+      succ?_ofBitVec]
+
+instance : LawfulUpwardEnumerableLE UInt16 where
+  le_iff x y := by
+    cases x; cases y
+    simpa [upwardEnumerableLE_ofBitVec, UInt16.le_iff_toBitVec_le] using
+      LawfulUpwardEnumerableLE.le_iff _ _
+
+instance : LawfulOrderLT UInt16 := inferInstance
+instance : LawfulUpwardEnumerableLT UInt16 := inferInstance
+instance : LawfulUpwardEnumerableLT UInt16 := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .closed UInt16 := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .closed UInt16 := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .open UInt16 := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .open UInt16 := inferInstance
+
+instance : RangeSize .closed UInt16 where
+  size bound a := bound.toNat + 1 - a.toNat
+
+theorem rangeSizeSize_eq_toBitVec {bound : Bound .closed UInt16} {x : BitVec 16} :
+    RangeSize.size bound (UInt16.ofBitVec x) = RangeSize.size (shape := .closed) bound.toBitVec x := by
+  simp [RangeSize.size]
+
+instance : LawfulRangeSize .closed UInt16 where
+  size_eq_zero_of_not_isSatisfied bound x := by
+    simpa [rangeSizeSize_eq_toBitVec, UInt16.lt_iff_toBitVec_lt] using
+      LawfulRangeSize.size_eq_zero_of_not_isSatisfied (su := .closed) (α := BitVec 16) _ _
+  size_eq_one_of_succ?_eq_none bound x := by
+    cases x
+    simpa [rangeSizeSize_eq_toBitVec, UInt16.le_iff_toBitVec_le, succ?_ofBitVec] using
+      LawfulRangeSize.size_eq_one_of_succ?_eq_none (su := .closed) (α := BitVec 16) _ _
+  size_eq_succ_of_succ?_eq_some bound init x := by
+    simpa [rangeSizeSize_eq_toBitVec, UInt16.le_iff_toBitVec_le, ← UInt16.toBitVec_inj, succ?] using
+      LawfulRangeSize.size_eq_succ_of_succ?_eq_some (su := .closed) (α := BitVec 16) _ _ _
+
+instance : RangeSize .open UInt16 := RangeSize.openOfClosed
+instance : LawfulRangeSize .open UInt16 := inferInstance
+
+end UInt16
+
+namespace UInt32
+
+instance : UpwardEnumerable UInt32 where
+  succ? i := if i + 1 = 0 then none else some (i + 1)
+  succMany? n i := if h : i.toNat + n < UInt32.size then some (.ofNatLT _ h) else none
+
+theorem succ?_ofBitVec {x : BitVec 32} :
+    UpwardEnumerable.succ? (UInt32.ofBitVec x) = UInt32.ofBitVec <$> UpwardEnumerable.succ? x := by
+  simp only [succ?, BitVec.ofNat_eq_ofNat, Option.map_eq_map, ← UInt32.toBitVec_inj]
+  split <;> simp_all
+
+theorem succMany?_ofBitVec {k : Nat} {x : BitVec 32} :
+    UpwardEnumerable.succMany? k (UInt32.ofBitVec x) = UInt32.ofBitVec <$> UpwardEnumerable.succMany? k x := by
+  simp [succMany?]
+
+theorem upwardEnumerableLE_ofBitVec {x y : BitVec 32} :
+    UpwardEnumerable.LE (UInt32.ofBitVec x) (UInt32.ofBitVec y) ↔ UpwardEnumerable.LE x y := by
+  simp [UpwardEnumerable.LE, succMany?_ofBitVec]
+
+theorem upwardEnumerableLT_ofBitVec {x y : BitVec 32} :
+    UpwardEnumerable.LT (UInt32.ofBitVec x) (UInt32.ofBitVec y) ↔ UpwardEnumerable.LT x y := by
+  simp [UpwardEnumerable.LT, succMany?_ofBitVec]
+
+instance : LawfulUpwardEnumerable UInt32 where
+  ne_of_lt x y := by
+    cases x; cases y
+    simpa [upwardEnumerableLT_ofBitVec] using LawfulUpwardEnumerable.ne_of_lt _ _
+  succMany?_zero x := by
+    cases x
+    simpa [succMany?_ofBitVec] using succMany?_zero
+  succMany?_succ? n x := by
+    cases x
+    simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def,
+      succ?_ofBitVec]
+
+instance : LawfulUpwardEnumerableLE UInt32 where
+  le_iff x y := by
+    cases x; cases y
+    simpa [upwardEnumerableLE_ofBitVec, UInt32.le_iff_toBitVec_le] using
+      LawfulUpwardEnumerableLE.le_iff _ _
+
+instance : LawfulOrderLT UInt32 := inferInstance
+instance : LawfulUpwardEnumerableLT UInt32 := inferInstance
+instance : LawfulUpwardEnumerableLT UInt32 := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .closed UInt32 := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .closed UInt32 := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .open UInt32 := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .open UInt32 := inferInstance
+
+instance : RangeSize .closed UInt32 where
+  size bound a := bound.toNat + 1 - a.toNat
+
+theorem rangeSizeSize_eq_toBitVec {bound : Bound .closed UInt32} {x : BitVec 32} :
+    RangeSize.size bound (UInt32.ofBitVec x) = RangeSize.size (shape := .closed) bound.toBitVec x := by
+  simp [RangeSize.size]
+
+instance : LawfulRangeSize .closed UInt32 where
+  size_eq_zero_of_not_isSatisfied bound x := by
+    simpa [rangeSizeSize_eq_toBitVec, UInt32.lt_iff_toBitVec_lt] using
+      LawfulRangeSize.size_eq_zero_of_not_isSatisfied (su := .closed) (α := BitVec 32) _ _
+  size_eq_one_of_succ?_eq_none bound x := by
+    cases x
+    simpa [rangeSizeSize_eq_toBitVec, UInt32.le_iff_toBitVec_le, succ?_ofBitVec] using
+      LawfulRangeSize.size_eq_one_of_succ?_eq_none (su := .closed) (α := BitVec 32) _ _
+  size_eq_succ_of_succ?_eq_some bound init x := by
+    simpa [rangeSizeSize_eq_toBitVec, UInt32.le_iff_toBitVec_le, ← UInt32.toBitVec_inj, succ?] using
+      LawfulRangeSize.size_eq_succ_of_succ?_eq_some (su := .closed) (α := BitVec 32) _ _ _
+
+instance : RangeSize .open UInt32 := RangeSize.openOfClosed
+instance : LawfulRangeSize .open UInt32 := inferInstance
+
+end UInt32
+
+namespace UInt64
+
+instance : UpwardEnumerable UInt64 where
+  succ? i := if i + 1 = 0 then none else some (i + 1)
+  succMany? n i := if h : i.toNat + n < UInt64.size then some (.ofNatLT _ h) else none
+
+theorem succ?_ofBitVec {x : BitVec 64} :
+    UpwardEnumerable.succ? (UInt64.ofBitVec x) = UInt64.ofBitVec <$> UpwardEnumerable.succ? x := by
+  simp only [succ?, BitVec.ofNat_eq_ofNat, Option.map_eq_map, ← UInt64.toBitVec_inj]
+  split <;> simp_all
+
+theorem succMany?_ofBitVec {k : Nat} {x : BitVec 64} :
+    UpwardEnumerable.succMany? k (UInt64.ofBitVec x) = UInt64.ofBitVec <$> UpwardEnumerable.succMany? k x := by
+  simp [succMany?]
+
+theorem upwardEnumerableLE_ofBitVec {x y : BitVec 64} :
+    UpwardEnumerable.LE (UInt64.ofBitVec x) (UInt64.ofBitVec y) ↔ UpwardEnumerable.LE x y := by
+  simp [UpwardEnumerable.LE, succMany?_ofBitVec]
+
+theorem upwardEnumerableLT_ofBitVec {x y : BitVec 64} :
+    UpwardEnumerable.LT (UInt64.ofBitVec x) (UInt64.ofBitVec y) ↔ UpwardEnumerable.LT x y := by
+  simp [UpwardEnumerable.LT, succMany?_ofBitVec]
+
+instance : LawfulUpwardEnumerable UInt64 where
+  ne_of_lt x y := by
+    cases x; cases y
+    simpa [upwardEnumerableLT_ofBitVec] using LawfulUpwardEnumerable.ne_of_lt _ _
+  succMany?_zero x := by
+    cases x
+    simpa [succMany?_ofBitVec] using succMany?_zero
+  succMany?_succ? n x := by
+    cases x
+    simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def,
+      succ?_ofBitVec]
+
+instance : LawfulUpwardEnumerableLE UInt64 where
+  le_iff x y := by
+    cases x; cases y
+    simpa [upwardEnumerableLE_ofBitVec, UInt64.le_iff_toBitVec_le] using
+      LawfulUpwardEnumerableLE.le_iff _ _
+
+instance : LawfulOrderLT UInt64 := inferInstance
+instance : LawfulUpwardEnumerableLT UInt64 := inferInstance
+instance : LawfulUpwardEnumerableLT UInt64 := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .closed UInt64 := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .closed UInt64 := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .open UInt64 := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .open UInt64 := inferInstance
+
+instance : RangeSize .closed UInt64 where
+  size bound a := bound.toNat + 1 - a.toNat
+
+theorem rangeSizeSize_eq_toBitVec {bound : Bound .closed UInt64} {x : BitVec 64} :
+    RangeSize.size bound (UInt64.ofBitVec x) = RangeSize.size (shape := .closed) bound.toBitVec x := by
+  simp [RangeSize.size]
+
+instance : LawfulRangeSize .closed UInt64 where
+  size_eq_zero_of_not_isSatisfied bound x := by
+    simpa [rangeSizeSize_eq_toBitVec, UInt64.lt_iff_toBitVec_lt] using
+      LawfulRangeSize.size_eq_zero_of_not_isSatisfied (su := .closed) (α := BitVec 64) _ _
+  size_eq_one_of_succ?_eq_none bound x := by
+    cases x
+    simpa [rangeSizeSize_eq_toBitVec, UInt64.le_iff_toBitVec_le, succ?_ofBitVec] using
+      LawfulRangeSize.size_eq_one_of_succ?_eq_none (su := .closed) (α := BitVec 64) _ _
+  size_eq_succ_of_succ?_eq_some bound init x := by
+    simpa [rangeSizeSize_eq_toBitVec, UInt64.le_iff_toBitVec_le, ← UInt64.toBitVec_inj, succ?] using
+      LawfulRangeSize.size_eq_succ_of_succ?_eq_some (su := .closed) (α := BitVec 64) _ _ _
+
+instance : RangeSize .open UInt64 := RangeSize.openOfClosed
+instance : LawfulRangeSize .open UInt64 := inferInstance
+
+end UInt64
+
+namespace USize
+
+instance : UpwardEnumerable USize where
+  succ? i := if i + 1 = 0 then none else some (i + 1)
+  succMany? n i := if h : i.toNat + n < USize.size then some (.ofNatLT _ h) else none
+
+theorem succ?_ofBitVec {x : BitVec System.Platform.numBits} :
+    UpwardEnumerable.succ? (USize.ofBitVec x) = USize.ofBitVec <$> UpwardEnumerable.succ? x := by
+  simp only [succ?, BitVec.ofNat_eq_ofNat, Option.map_eq_map, ← USize.toBitVec_inj]
+  split <;> simp_all
+
+theorem succMany?_ofBitVec {k : Nat} {x : BitVec System.Platform.numBits} :
+    UpwardEnumerable.succMany? k (USize.ofBitVec x) = USize.ofBitVec <$> UpwardEnumerable.succMany? k x := by
+  simp [succMany?]
+
+theorem upwardEnumerableLE_ofBitVec {x y : BitVec System.Platform.numBits} :
+    UpwardEnumerable.LE (USize.ofBitVec x) (USize.ofBitVec y) ↔ UpwardEnumerable.LE x y := by
+  simp [UpwardEnumerable.LE, succMany?_ofBitVec]
+
+theorem upwardEnumerableLT_ofBitVec {x y : BitVec System.Platform.numBits} :
+    UpwardEnumerable.LT (USize.ofBitVec x) (USize.ofBitVec y) ↔ UpwardEnumerable.LT x y := by
+  simp [UpwardEnumerable.LT, succMany?_ofBitVec]
+
+instance : LawfulUpwardEnumerable USize where
+  ne_of_lt x y := by
+    cases x; cases y
+    simpa [upwardEnumerableLT_ofBitVec] using LawfulUpwardEnumerable.ne_of_lt _ _
+  succMany?_zero x := by
+    cases x
+    simpa [succMany?_ofBitVec] using succMany?_zero
+  succMany?_succ? n x := by
+    cases x
+    simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def,
+      succ?_ofBitVec]
+
+instance : LawfulUpwardEnumerableLE USize where
+  le_iff x y := by
+    cases x; cases y
+    simpa [upwardEnumerableLE_ofBitVec, USize.le_iff_toBitVec_le] using
+      LawfulUpwardEnumerableLE.le_iff _ _
+
+instance : LawfulOrderLT USize := inferInstance
+instance : LawfulUpwardEnumerableLT USize := inferInstance
+instance : LawfulUpwardEnumerableLT USize := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .closed USize := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .closed USize := inferInstance
+instance : LawfulUpwardEnumerableLowerBound .open USize := inferInstance
+instance : LawfulUpwardEnumerableUpperBound .open USize := inferInstance
+
+instance : RangeSize .closed USize where
+  size bound a := bound.toNat + 1 - a.toNat
+
+theorem rangeSizeSize_eq_toBitVec {bound : Bound .closed USize} {x : BitVec System.Platform.numBits} :
+    RangeSize.size bound (USize.ofBitVec x) = RangeSize.size (shape := .closed) bound.toBitVec x := by
+  simp [RangeSize.size]
+
+instance : LawfulRangeSize .closed USize where
+  size_eq_zero_of_not_isSatisfied bound x := by
+    simpa [rangeSizeSize_eq_toBitVec, USize.lt_iff_toBitVec_lt] using
+      LawfulRangeSize.size_eq_zero_of_not_isSatisfied (su := .closed) (α := BitVec System.Platform.numBits) _ _
+  size_eq_one_of_succ?_eq_none bound x := by
+    cases x
+    simpa [rangeSizeSize_eq_toBitVec, USize.le_iff_toBitVec_le, succ?_ofBitVec] using
+      LawfulRangeSize.size_eq_one_of_succ?_eq_none (su := .closed) (α := BitVec System.Platform.numBits) _ _
+  size_eq_succ_of_succ?_eq_some bound init x := by
+    simpa [rangeSizeSize_eq_toBitVec, USize.le_iff_toBitVec_le, ← USize.toBitVec_inj, succ?] using
+      LawfulRangeSize.size_eq_succ_of_succ?_eq_some (su := .closed) (α := BitVec System.Platform.numBits) _ _ _
+
+instance : RangeSize .open USize := RangeSize.openOfClosed
+instance : LawfulRangeSize .open USize := inferInstance
+
+end USize

src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean

@@ -40,7 +40,6 @@ class UpwardEnumerable (α : Type u) where
   -/
   succMany? (n : Nat) (a : α) : Option α := Nat.repeat (· >>= succ?) n (some a)
 
-attribute [simp] UpwardEnumerable.succ? UpwardEnumerable.succMany?
 export UpwardEnumerable (succ? succMany?)
 
 /--
@@ -80,7 +79,6 @@ class Least? (α : Type u) where
   -/
   least? : Option α
 
-attribute [simp] Least?.least?
 export Least? (least?)
 
 /--
@@ -95,7 +93,7 @@ class LawfulUpwardEnumerable (α : Type u) [UpwardEnumerable α] where
   The `n + 1`-th successor of `a` is the successor of the `n`-th successor, given that said
   successors actually exist.
   -/
-  succMany?_succ (n : Nat) (a : α) :
+  succMany?_succ? (n : Nat) (a : α) :
     succMany? (n + 1) a = (succMany? n a).bind succ?
 
 theorem UpwardEnumerable.succMany?_zero [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a : α} :
@@ -105,7 +103,7 @@ theorem UpwardEnumerable.succMany?_zero [UpwardEnumerable α] [LawfulUpwardEnume
 theorem UpwardEnumerable.succMany?_succ? [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     {n : Nat} {a : α} :
     succMany? (n + 1) a = (succMany? n a).bind succ? :=
-  LawfulUpwardEnumerable.succMany?_succ n a
+  LawfulUpwardEnumerable.succMany?_succ? n a
 
 @[deprecated succMany?_succ? (since := "2025-09-03")]
 theorem UpwardEnumerable.succMany?_succ [UpwardEnumerable α] [LawfulUpwardEnumerable α]

src/Init/Data/UInt/Lemmas.lean

@@ -311,6 +311,13 @@ theorem UInt64.ofNat_mod_size : ofNat (x % 2 ^ 64) = ofNat x := by
 theorem USize.ofNat_mod_size : ofNat (x % 2 ^ System.Platform.numBits) = ofNat x := by
   simp [ofNat, BitVec.ofNat, Fin.ofNat]
 
+theorem UInt8.ofNat_size : ofNat size = 0 := by decide
+theorem UInt16.ofNat_size : ofNat size = 0 := by decide
+theorem UInt32.ofNat_size : ofNat size = 0 := by decide
+theorem UInt64.ofNat_size : ofNat size = 0 := by decide
+theorem USize.ofNat_size : ofNat size = 0 := by
+  simp [ofNat, BitVec.ofNat, USize.eq_iff_toBitVec_eq]
+
 theorem UInt8.lt_ofNat_iff {n : UInt8} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m := by
   rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h]
 theorem UInt8.ofNat_lt_iff {n : UInt8} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat := by

tests/lean/run/rangePolymorphic.lean

@@ -92,7 +92,33 @@ section Int
 example : ((-2)...3).toList = [-2, -1, 0, 1, 2] := by native_decide
 example : ((-2)...=3).toList = [-2, -1, 0, 1, 2, 3] := by native_decide
 
-example : Std.PRange.LawfulRangeSize .closed Int := inferInstance
-example : Std.PRange.LawfulRangeSize .open Int := inferInstance
-
 end Int
+
+section UInt
+
+example : ((1 : UInt8)...3).toList = [1, 2] := by native_decide
+example : ((-1 : UInt8)...3).toList = [] := by native_decide -- 255 ≤ x < 3 is impossible
+example : ((1 : UInt8)...=3).toList = [1, 2, 3] := by native_decide
+example : ((250 : UInt8)...-1).toList = [250, 251, 252, 253, 254] := by native_decide
+
+example : ((1 : UInt16)...3).toList = [1, 2] := by native_decide
+example : ((-1 : UInt16)...3).toList = [] := by native_decide
+example : ((1 : UInt16)...=3).toList = [1, 2, 3] := by native_decide
+example : ((-4 : UInt16)...-1).toList = [-4, -3, -2] := by native_decide
+
+example : ((1 : UInt32)...3).toList = [1, 2] := by native_decide
+example : ((-1 : UInt32)...3).toList = [] := by native_decide
+example : ((1 : UInt32)...=3).toList = [1, 2, 3] := by native_decide
+example : ((-4 : UInt32)...-1).toList = [-4, -3, -2] := by native_decide
+
+example : ((1 : UInt64)...3).toList = [1, 2] := by native_decide
+example : ((-1 : UInt64)...3).toList = [] := by native_decide
+example : ((1 : UInt64)...=3).toList = [1, 2, 3] := by native_decide
+example : ((-4 : UInt64)...-1).toList = [-4, -3, -2] := by native_decide
+
+example : ((1 : USize)...3).toList = [1, 2] := by native_decide
+example : ((-1 : USize)...3).toList = [] := by native_decide
+example : ((1 : USize)...=3).toList = [1, 2, 3] := by native_decide
+example : ((-4 : USize)...-1).toList = [-4, -3, -2] := by native_decide
+
+end UInt