feat: add simps and toNat lemmas for UIntX types (#853)

leanprover-community · Jun 21, 2024 · 73c7f46 · 73c7f46
1 parent f343929
commit 73c7f46
Showing 1 changed file with 107 additions and 2 deletions.
diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean
@@ -14,6 +14,12 @@ theorem UInt8.ext_iff {x y : UInt8} : x = y ↔ x.toNat = y.toNat := ⟨congrArg
 
 @[simp] theorem UInt8.val_val_eq_toNat (x : UInt8) : x.val.val = x.toNat := rfl
 
+@[simp] theorem UInt8.val_ofNat (n) :
+    (no_index (OfNat.ofNat n) : UInt8).val = OfNat.ofNat n := rfl
+
+@[simp] theorem UInt8.toNat_ofNat (n) :
+    (no_index (OfNat.ofNat n) : UInt8).toNat = n % UInt8.size := rfl
+
 theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt
 
 @[simp] theorem UInt8.toUInt16_toNat (x : UInt8) : x.toUInt16.toNat = x.toNat := rfl
@@ -22,6 +28,21 @@ theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt
 
 @[simp] theorem UInt8.toUInt64_toNat (x : UInt8) : x.toUInt64.toNat = x.toNat := rfl
 
+theorem UInt8.toNat_zero : (0 : UInt8).toNat = 0 := rfl
+
+theorem UInt8.toNat_add (x y : UInt8) : (x + y).toNat = (x.toNat + y.toNat) % UInt8.size := rfl
+
+theorem UInt8.toNat_sub (x y : UInt8) :
+  (x - y).toNat = (x.toNat + (UInt8.size - y.toNat)) % UInt8.size := rfl
+
+theorem UInt8.toNat_mul (x y : UInt8) : (x * y).toNat = (x.toNat * y.toNat) % UInt8.size := rfl
+
+theorem UInt8.toNat_div (x y : UInt8) : (x / y).toNat = x.toNat / y.toNat := rfl
+
+theorem UInt8.toNat_mod (x y : UInt8) : (x % y).toNat = x.toNat % y.toNat := rfl
+
+theorem UInt8.toNat_modn (x : UInt8) (n) : (x.modn n).toNat = x.toNat % n := rfl
+
 theorem UInt8.le_antisymm_iff {x y : UInt8} : x = y ↔ x ≤ y ∧ y ≤ x :=
   UInt8.ext_iff.trans Nat.le_antisymm_iff
 
@@ -38,16 +59,37 @@ instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
 
 theorem UInt16.ext_iff {x y : UInt16} : x = y ↔ x.toNat = y.toNat := ⟨congrArg _, UInt16.ext⟩
 
-theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt
-
 @[simp] theorem UInt16.val_val_eq_toNat (x : UInt16) : x.val.val = x.toNat := rfl
 
+@[simp] theorem UInt16.val_ofNat (n) :
+    (no_index (OfNat.ofNat n) : UInt16).val = OfNat.ofNat n := rfl
+
+@[simp] theorem UInt16.toNat_ofNat (n) :
+    (no_index (OfNat.ofNat n) : UInt16).toNat = n % UInt16.size := rfl
+
+theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt
+
 @[simp] theorem UInt16.toUInt8_toNat (x : UInt16) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
 
 @[simp] theorem UInt16.toUInt32_toNat (x : UInt16) : x.toUInt32.toNat = x.toNat := rfl
 
 @[simp] theorem UInt16.toUInt64_toNat (x : UInt16) : x.toUInt64.toNat = x.toNat := rfl
 
+theorem UInt16.toNat_zero : (0 : UInt16).toNat = 0 := rfl
+
+theorem UInt16.toNat_add (x y : UInt16) : (x + y).toNat = (x.toNat + y.toNat) % UInt16.size := rfl
+
+theorem UInt16.toNat_sub (x y : UInt16) :
+  (x - y).toNat = (x.toNat + (UInt16.size - y.toNat)) % UInt16.size := rfl
+
+theorem UInt16.toNat_mul (x y : UInt16) : (x * y).toNat = (x.toNat * y.toNat) % UInt16.size := rfl
+
+theorem UInt16.toNat_div (x y : UInt16) : (x / y).toNat = x.toNat / y.toNat := rfl
+
+theorem UInt16.toNat_mod (x y : UInt16) : (x % y).toNat = x.toNat % y.toNat := rfl
+
+theorem UInt16.toNat_modn (x : UInt16) (n) : (x.modn n).toNat = x.toNat % n := rfl
+
 theorem UInt16.le_antisymm_iff {x y : UInt16} : x = y ↔ x ≤ y ∧ y ≤ x :=
   UInt16.ext_iff.trans Nat.le_antisymm_iff
 
@@ -66,6 +108,12 @@ theorem UInt32.ext_iff {x y : UInt32} : x = y ↔ x.toNat = y.toNat := ⟨congrA
 
 @[simp] theorem UInt32.val_val_eq_toNat (x : UInt32) : x.val.val = x.toNat := rfl
 
+@[simp] theorem UInt32.val_ofNat (n) :
+    (no_index (OfNat.ofNat n) : UInt32).val = OfNat.ofNat n := rfl
+
+@[simp] theorem UInt32.toNat_ofNat (n) :
+    (no_index (OfNat.ofNat n) : UInt32).toNat = n % UInt32.size := rfl
+
 theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt
 
 @[simp] theorem UInt32.toUInt8_toNat (x : UInt32) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
@@ -74,6 +122,21 @@ theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt
 
 @[simp] theorem UInt32.toUInt64_toNat (x : UInt32) : x.toUInt64.toNat = x.toNat := rfl
 
+theorem UInt32.toNat_zero : (0 : UInt32).toNat = 0 := rfl
+
+theorem UInt32.toNat_add (x y : UInt32) : (x + y).toNat = (x.toNat + y.toNat) % UInt32.size := rfl
+
+theorem UInt32.toNat_sub (x y : UInt32) :
+  (x - y).toNat = (x.toNat + (UInt32.size - y.toNat)) % UInt32.size := rfl
+
+theorem UInt32.toNat_mul (x y : UInt32) : (x * y).toNat = (x.toNat * y.toNat) % UInt32.size := rfl
+
+theorem UInt32.toNat_div (x y : UInt32) : (x / y).toNat = x.toNat / y.toNat := rfl
+
+theorem UInt32.toNat_mod (x y : UInt32) : (x % y).toNat = x.toNat % y.toNat := rfl
+
+theorem UInt32.toNat_modn (x : UInt32) (n) : (x.modn n).toNat = x.toNat % n := rfl
+
 theorem UInt32.le_antisymm_iff {x y : UInt32} : x = y ↔ x ≤ y ∧ y ≤ x :=
   UInt32.ext_iff.trans Nat.le_antisymm_iff
 
@@ -92,6 +155,12 @@ theorem UInt64.ext_iff {x y : UInt64} : x = y ↔ x.toNat = y.toNat := ⟨congrA
 
 @[simp] theorem UInt64.val_val_eq_toNat (x : UInt64) : x.val.val = x.toNat := rfl
 
+@[simp] theorem UInt64.val_ofNat (n) :
+    (no_index (OfNat.ofNat n) : UInt64).val = OfNat.ofNat n := rfl
+
+@[simp] theorem UInt64.toNat_ofNat (n) :
+    (no_index (OfNat.ofNat n) : UInt64).toNat = n % UInt64.size := rfl
+
 theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt
 
 @[simp] theorem UInt64.toUInt8_toNat (x : UInt64) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
@@ -100,6 +169,21 @@ theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt
 
 @[simp] theorem UInt64.toUInt32_toNat (x : UInt64) : x.toUInt32.toNat = x.toNat % 2 ^ 32 := rfl
 
+theorem UInt64.toNat_zero : (0 : UInt64).toNat = 0 := rfl
+
+theorem UInt64.toNat_add (x y : UInt64) : (x + y).toNat = (x.toNat + y.toNat) % UInt64.size := rfl
+
+theorem UInt64.toNat_sub (x y : UInt64) :
+  (x - y).toNat = (x.toNat + (UInt64.size - y.toNat)) % UInt64.size := rfl
+
+theorem UInt64.toNat_mul (x y : UInt64) : (x * y).toNat = (x.toNat * y.toNat) % UInt64.size := rfl
+
+theorem UInt64.toNat_div (x y : UInt64) : (x / y).toNat = x.toNat / y.toNat := rfl
+
+theorem UInt64.toNat_mod (x y : UInt64) : (x % y).toNat = x.toNat % y.toNat := rfl
+
+theorem UInt64.toNat_modn (x : UInt64) (n) : (x.modn n).toNat = x.toNat % n := rfl
+
 theorem UInt64.le_antisymm_iff {x y : UInt64} : x = y ↔ x ≤ y ∧ y ≤ x :=
   UInt64.ext_iff.trans Nat.le_antisymm_iff
 
@@ -118,6 +202,12 @@ theorem USize.ext_iff {x y : USize} : x = y ↔ x.toNat = y.toNat := ⟨congrArg
 
 @[simp] theorem USize.val_val_eq_toNat (x : USize) : x.val.val = x.toNat := rfl
 
+@[simp] theorem USize.val_ofNat (n) :
+    (no_index (OfNat.ofNat n) : USize).val = OfNat.ofNat n := rfl
+
+@[simp] theorem USize.toNat_ofNat (n) :
+    (no_index (OfNat.ofNat n) : USize).toNat = n % USize.size := rfl
+
 theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits := by
   have : 1 ≤ 2 ^ System.Platform.numBits := Nat.succ_le_of_lt (Nat.two_pow_pos _)
   rw [USize.size, Nat.sub_add_cancel this]
@@ -140,6 +230,21 @@ theorem USize.toNat_lt (x : USize) : x.toNat < 2 ^ System.Platform.numBits := by
 
 @[simp] theorem UInt32.toUSize_toNat (x : UInt32) : x.toUSize.toNat = x.toNat := rfl
 
+theorem USize.toNat_zero : (0 : USize).toNat = 0 := rfl
+
+theorem USize.toNat_add (x y : USize) : (x + y).toNat = (x.toNat + y.toNat) % USize.size := rfl
+
+theorem USize.toNat_sub (x y : USize) :
+  (x - y).toNat = (x.toNat + (USize.size - y.toNat)) % USize.size := rfl
+
+theorem USize.toNat_mul (x y : USize) : (x * y).toNat = (x.toNat * y.toNat) % USize.size := rfl
+
+theorem USize.toNat_div (x y : USize) : (x / y).toNat = x.toNat / y.toNat := rfl
+
+theorem USize.toNat_mod (x y : USize) : (x % y).toNat = x.toNat % y.toNat := rfl
+
+theorem USize.toNat_modn (x : USize) (n) : (x.modn n).toNat = x.toNat % n := rfl
+
 theorem USize.le_antisymm_iff {x y : USize} : x = y ↔ x ≤ y ∧ y ≤ x :=
   USize.ext_iff.trans Nat.le_antisymm_iff