feat: UIntX.[val_ofNat, toBitVec_ofNat] (#5735)

src/Init/Data/UInt/Lemmas.lean

@@ -115,6 +115,15 @@ protected theorem toNat.inj : ∀ {a b : $typeName}, a.toNat = b.toNat → a = b
 
 @[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
 
+@[simp]
+theorem val_ofNat (n : Nat) : val (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+
+@[simp]
+theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
+
+@[simp]
+theorem mk_ofNat (n : Nat) : mk (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
+
 end $typeName
 )
 

src/Lean/Data/HashMap.lean

@@ -46,7 +46,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property

src/Lean/Data/HashSet.lean

@@ -42,7 +42,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property

tests/lean/run/trivial_uint.lean

@@ -0,0 +1,15 @@
+example : UInt8.val 42 = 42 := by simp
+example : UInt16.val 42 = 42 := by simp
+example : UInt32.val 42 = 42 := by simp
+example : UInt64.val 42 = 42 := by simp
+example : USize.val 42 = 42 := by simp
+example : UInt8.toBitVec 42 = 42 := by simp
+example : UInt16.toBitVec 42 = 42 := by simp
+example : UInt32.toBitVec 42 = 42 := by simp
+example : UInt64.toBitVec 42 = 42 := by simp
+example : USize.toBitVec 42 = 42 := by simp
+example : UInt8.mk 42 = 42 := by simp
+example : UInt16.mk 42 = 42 := by simp
+example : UInt32.mk 42 = 42 := by simp
+example : UInt64.mk 42 = 42 := by simp
+example : USize.mk 42 = 42 := by simp