feat: add missing UInt bitwise toNat theorems

leanprover · Nov 23, 2024 · 85366f3 · 85366f3
1 parent 4600bb1
commit 85366f3
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 9 deletions.
diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean
@@ -246,6 +246,9 @@ instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
 instance : Max UInt64 := maxOfLe
 instance : Min UInt64 := minOfLe
 
+theorem System.Platform.numBits_lt_usize : numBits < USize.size := by
+  cases numBits_eq <;> simp_all [USize.size]
+
 @[extern "lean_usize_mul"]
 def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_usize_div"]
@@ -261,9 +264,9 @@ def USize.lor (a b : USize) : USize := ⟨a.toBitVec ||| b.toBitVec⟩
 @[extern "lean_usize_xor"]
 def USize.xor (a b : USize) : USize := ⟨a.toBitVec ^^^ b.toBitVec⟩
 @[extern "lean_usize_shift_left"]
-def USize.shiftLeft (a b : USize) : USize := ⟨a.toBitVec <<< (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
+def USize.shiftLeft (a b : USize) : USize := ⟨a.toBitVec <<< (mod b (USize.ofNatCore System.Platform.numBits System.Platform.numBits_lt_usize)).toBitVec⟩
 @[extern "lean_usize_shift_right"]
-def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
+def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (mod b (USize.ofNatCore System.Platform.numBits System.Platform.numBits_lt_usize)).toBitVec⟩
 @[extern "lean_uint32_to_usize"]
 def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.toBitVec.toNat a.toBitVec.isLt
 @[extern "lean_usize_to_uint32"]

diff --git a/src/Init/Data/UInt/Bitwise.lean b/src/Init/Data/UInt/Bitwise.lean
@@ -9,17 +9,24 @@ import Init.Data.Fin.Bitwise
 import Init.Data.BitVec.Lemmas
 
 set_option hygiene false in
-macro "declare_bitwise_uint_theorems" typeName:ident : command =>
+macro "declare_bitwise_uint_theorems" typeName:ident bits:term:arg : command =>
+let toNat_and := Lean.mkIdentFrom typeName (typeName.getId.modifyBase (·.str "toNat_and"))
 `(
 namespace $typeName
 
-@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
+@[simp] protected theorem toNat_and (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
+@[simp] protected theorem toNat_or (a b : $typeName) : (a ||| b).toNat = a.toNat ||| b.toNat := BitVec.toNat_or ..
+@[simp] protected theorem toNat_xor (a b : $typeName) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := BitVec.toNat_xor ..
+@[simp] protected theorem toNat_shiftLeft (a b : $typeName) : (a <<< b).toNat = a.toNat <<< (b.toNat % $bits) % 2 ^ $bits := BitVec.toNat_shiftLeft
+@[simp] protected theorem toNat_shiftRight (a b : $typeName) : (a >>> b).toNat = a.toNat >>> (b.toNat % $bits) := BitVec.toNat_ushiftRight ..
+
+@[deprecated $toNat_and (since := "2024-11-23")] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
 
 end $typeName
 )
 
-declare_bitwise_uint_theorems UInt8
-declare_bitwise_uint_theorems UInt16
-declare_bitwise_uint_theorems UInt32
-declare_bitwise_uint_theorems UInt64
-declare_bitwise_uint_theorems USize
+declare_bitwise_uint_theorems UInt8 8
+declare_bitwise_uint_theorems UInt16 16
+declare_bitwise_uint_theorems UInt32 32
+declare_bitwise_uint_theorems UInt64 64
+declare_bitwise_uint_theorems USize System.Platform.numBits