feat: USize.size inequalities (#6203)

This PR adds the theorems `le_usize_size` and `usize_size_le`, which
make proving inequalities about `USize.size` easier.

It also deprecates `usize_size_gt_zero` in favor of `usize_size_pos` (as
that seems more consistent with our naming covention) and adds
`USize.toNat_ofNat_of_lt_32` for dealing with small USize literals.

It also moves `USize.ofNat32` and `USize.toUInt64` to
`Init.Data.UInt.Basic` as neither are used in `Init.Prelude` anymore.

---------

Co-authored-by: Kim Morrison <kim@tqft.net>

src/Init/Data/UInt/Basic.lean

@@ -246,6 +246,12 @@ instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
 instance : Max UInt64 := maxOfLe
 instance : Min UInt64 := minOfLe
 
+theorem usize_size_le : USize.size ≤ 18446744073709551616 := by
+  cases usize_size_eq <;> next h => rw [h]; decide
+
+theorem le_usize_size : 4294967296 ≤ USize.size := by
+  cases usize_size_eq <;> next h => rw [h]; decide
+
 @[extern "lean_usize_mul"]
 def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_usize_div"]
@@ -264,13 +270,29 @@ def USize.xor (a b : USize) : USize := ⟨a.toBitVec ^^^ b.toBitVec⟩
 def USize.shiftLeft (a b : USize) : USize := ⟨a.toBitVec <<< (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
 @[extern "lean_usize_shift_right"]
 def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
+/--
+Upcast a `Nat` less than `2^32` to a `USize`.
+This is lossless because `USize.size` is either `2^32` or `2^64`.
+This function is overridden with a native implementation.
+-/
+@[extern "lean_usize_of_nat"]
+def USize.ofNat32 (n : @& Nat) (h : n < 4294967296) : USize :=
+  USize.ofNatCore n (Nat.lt_of_lt_of_le h le_usize_size)
 @[extern "lean_uint32_to_usize"]
 def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.toBitVec.toNat a.toBitVec.isLt
 @[extern "lean_usize_to_uint32"]
 def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
 /-- Converts a `UInt64` to a `USize` by reducing modulo `USize.size`. -/
 @[extern "lean_uint64_to_usize"]
 def UInt64.toUSize (a : UInt64) : USize := a.toNat.toUSize
+/--
+Upcast a `USize` to a `UInt64`.
+This is lossless because `USize.size` is either `2^32` or `2^64`.
+This function is overridden with a native implementation.
+-/
+@[extern "lean_usize_to_uint64"]
+def USize.toUInt64 (a : USize) : UInt64 :=
+  UInt64.ofNatCore a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt usize_size_le)
 
 instance : Mul USize       := ⟨USize.mul⟩
 instance : Mod USize       := ⟨USize.mod⟩

src/Init/Data/UInt/BasicAux.lean

@@ -94,10 +94,8 @@ def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBit
 
 instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
 
-theorem usize_size_gt_zero : USize.size > 0 := by
-  cases usize_size_eq with
-  | inl h => rw [h]; decide
-  | inr h => rw [h]; decide
+@[deprecated usize_size_pos (since := "2024-11-24")] theorem usize_size_gt_zero : USize.size > 0 :=
+  usize_size_pos
 
 def USize.val (x : USize) : Fin USize.size := x.toBitVec.toFin
 @[extern "lean_usize_of_nat"]

src/Init/Data/UInt/Lemmas.lean

@@ -133,6 +133,9 @@ declare_uint_theorems UInt32
 declare_uint_theorems UInt64
 declare_uint_theorems USize
 
+theorem USize.toNat_ofNat_of_lt_32 {n : Nat} (h : n < 4294967296) : toNat (ofNat n) = n :=
+  toNat_ofNat_of_lt (Nat.lt_of_lt_of_le h le_usize_size)
+
 theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := by
   simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
 

src/Init/Prelude.lean

@@ -2116,6 +2116,11 @@ theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073
   | _, Or.inl rfl => Or.inl (of_decide_eq_true rfl)
   | _, Or.inr rfl => Or.inr (of_decide_eq_true rfl)
 
+theorem usize_size_pos : LT.lt 0 USize.size :=
+  match USize.size, usize_size_eq with
+  | _, Or.inl rfl => of_decide_eq_true rfl
+  | _, Or.inr rfl => of_decide_eq_true rfl
+
 /--
 A `USize` is an unsigned integer with the size of a word
 for the platform's architecture.
@@ -2155,24 +2160,7 @@ def USize.decEq (a b : USize) : Decidable (Eq a b) :=
 instance : DecidableEq USize := USize.decEq
 
 instance : Inhabited USize where
-  default := USize.ofNatCore 0 (match USize.size, usize_size_eq with
-    | _, Or.inl rfl => of_decide_eq_true rfl
-    | _, Or.inr rfl => of_decide_eq_true rfl)
-
-/--
-Upcast a `Nat` less than `2^32` to a `USize`.
-This is lossless because `USize.size` is either `2^32` or `2^64`.
-This function is overridden with a native implementation.
--/
-@[extern "lean_usize_of_nat"]
-def USize.ofNat32 (n : @& Nat) (h : LT.lt n 4294967296) : USize where
-  toBitVec :=
-    BitVec.ofNatLt n (
-      match System.Platform.numBits, System.Platform.numBits_eq with
-      | _, Or.inl rfl => h
-      | _, Or.inr rfl => Nat.lt_trans h (of_decide_eq_true rfl)
-    )
-
+  default := USize.ofNatCore 0 usize_size_pos
 /--
 A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and
 it is also not a "surrogate" character (the range `0xd800` to `0xdfff` inclusive).
@@ -3432,21 +3420,6 @@ class Hashable (α : Sort u) where
 
 export Hashable (hash)
 
-/--
-Upcast a `USize` to a `UInt64`.
-This is lossless because `USize.size` is either `2^32` or `2^64`.
-This function is overridden with a native implementation.
--/
-@[extern "lean_usize_to_uint64"]
-def USize.toUInt64 (u : USize) : UInt64 where
-  toBitVec := BitVec.ofNatLt u.toBitVec.toNat (
-        let ⟨⟨n, h⟩⟩ := u
-        show LT.lt n _ from
-        match System.Platform.numBits, System.Platform.numBits_eq, h with
-        | _, Or.inl rfl, h => Nat.lt_trans h (of_decide_eq_true rfl)
-        | _, Or.inr rfl, h => h
-      )
-
 /-- An opaque hash mixing operation, used to implement hashing for tuples. -/
 @[extern "lean_uint64_mix_hash"]
 opaque mixHash (u₁ u₂ : UInt64) : UInt64

src/Init/ShareCommon.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 prelude
 import Init.Util
+import Init.Data.UInt.Basic
 
 namespace ShareCommon
 /-