chore: move usize theorem to Batteries.Data.UInt (#1673)

Author: cmlsharp

Batteries/Data/Array/Basic.lean

@@ -5,6 +5,7 @@ Authors: Arthur Paulino, Floris van Doorn, Jannis Limperg
 -/
 module
 import Batteries.Tactic.Alias
+import Batteries.Data.UInt
 
 @[expose] public section
 
@@ -130,12 +131,6 @@ May be asserted to be true in an unsafe context via `Array.unsafe_sizeFitsUsize`
 -/
 private abbrev SizeFitsUSize (a : Array α) : Prop := a.size < USize.size
 
-@[grind .]
-private theorem SizeFitsUSize.toNat_ofNat_eq {n : Nat} {a : Array α}
-    (h : a.SizeFitsUSize) (hn : n ≤ a.size) :
-    (USize.ofNat n).toNat = n :=
-  USize.toNat_ofNat_of_lt' (Nat.lt_of_le_of_lt ‹_› ‹_›)
-
 /-
 This is guaranteed by the Array docs but it is unprovable.
 Can be used in unsafe functions to write more efficient implementations
@@ -214,13 +209,13 @@ private theorem scanlM_loop_eq_scanlMFast_loop [Monad m]
     {h_stop : stop ≤ as.size} {acc : Array β} :
     scanlM.loop f init as start stop h_stop acc
       = scanlMFast.loop f init as (USize.ofNat start) (USize.ofNat stop)
-      (by rw [USize.toNat_ofNat_of_lt' (Nat.lt_of_le_of_lt h_stop h_size)]; exact h_stop) acc := by
+      (by rw [USize.toNat_ofNat_of_le_of_lt h_size h_stop]; exact h_stop) acc := by
   generalize h_n : stop - start = n
   induction n using Nat.strongRecOn generalizing start acc init
   rename_i n ih
   rw [scanlM.loop, scanlMFast.loop]
-  have h_stop_usize := h_size.toNat_ofNat_eq h_stop
-  have h_start_usize := h_size.toNat_ofNat_eq h_start
+  have h_stop_usize := USize.toNat_ofNat_of_le_of_lt h_size h_stop
+  have h_start_usize := USize.toNat_ofNat_of_le_of_lt h_size h_start
   split
   case isTrue h_lt =>
     simp_all only [USize.toNat_ofNat', ↓reduceDIte, uget,
@@ -229,7 +224,7 @@ private theorem scanlM_loop_eq_scanlMFast_loop [Monad m]
     intro next
     have h_start_succ : USize.ofNat start + 1 = USize.ofNat (start + 1) := by
       simp_all only [← USize.toNat_inj, USize.toNat_add]
-      grind only [USize.size_eq, SizeFitsUSize.toNat_ofNat_eq]
+      grind only [USize.size_eq, USize.toNat_ofNat_of_le_of_lt]
     rw [h_start_succ]
     apply ih (stop - (start + 1)) <;> omega
   case isFalse h_nlt => grind [USize.lt_iff_toNat_lt]
@@ -255,7 +250,7 @@ private def scanrMFast [Monad m] (f : α → β → m β) (init : β) (as : Arra
     (start := USize.ofNat start) (stop := USize.ofNat stop)
     (h_start := by grind only [USize.size_eq, USize.ofNat_eq_iff_mod_eq_toNat, = Nat.min_def])
     (acc := Array.replicate (start - stop + 1) init)
-    (by grind only [!Array.size_replicate, = Nat.min_def, SizeFitsUSize.toNat_ofNat_eq])
+    (by grind only [!Array.size_replicate, = Nat.min_def, USize.toNat_ofNat_of_le_of_lt])
 where
   @[specialize]
   loop (f : α → β → m β) (init : β) (as : Array α)

Batteries/Data/UInt.lean

@@ -209,3 +209,16 @@ theorem UInt32.toUSize_toNat (x : UInt32) : x.toUSize.toNat = x.toNat := by simp
 instance : Std.LawfulOrd USize :=
   Std.LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm
     (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt USize.le_antisymm
+
+theorem USize.toNat_ofNat_of_le_of_lt (h : n < USize.size) (hn : i ≤ n) :
+    (USize.ofNat i).toNat = i :=
+  USize.toNat_ofNat_of_lt' (Nat.lt_of_le_of_lt ‹_› ‹_›)
+
+theorem USize.pred_toNat {i : USize} (h_gt : 0 < i) :
+    (i - 1).toNat = i.toNat - 1 := by
+  have h_gt_nat := USize.lt_iff_toNat_lt.mp h_gt
+  have h_bound := i.toNat_lt_size
+  cases System.Platform.numBits_eq
+  all_goals
+    simp_all only [USize.size, USize.toNat_sub, USize.reduceToNat]
+    omega