Documentation

Init.Data.UInt.Lemmas

Equations
  • One or more equations did not get rendered due to their size.
theorem UInt8.toNat_ofNat_of_lt {n : Nat} (h : n < size) :
(ofNat n).toNat = n
theorem UInt8.add_def (a b : UInt8) :
a + b = { toBitVec := a.toBitVec + b.toBitVec }
theorem UInt8.eq_of_toBitVec_eq {a b : UInt8} (h : a.toBitVec = b.toBitVec) :
a = b
theorem UInt8.toNat_toBitVec_eq_toNat (x : UInt8) :
x.toBitVec.toNat = x.toNat
theorem UInt8.le_total (a b : UInt8) :
a b b a
@[simp]
theorem UInt8.toNat_sub_of_le (a b : UInt8) :
b a(a - b).toNat = a.toNat - b.toNat
@[simp]
theorem UInt8.toNat_mul (a b : UInt8) :
(a * b).toNat = a.toNat * b.toNat % 2 ^ 8
theorem UInt8.mod_lt (a : UInt8) {b : UInt8} :
0 < ba % b < b
theorem UInt8.le_iff_toNat_le {a b : UInt8} :
a b a.toNat b.toNat
@[simp]
theorem UInt8.val_ofNat (n : Nat) :
theorem UInt8.toNat_mod_lt {m : Nat} (u : UInt8) :
m > 0(u % ofNat m).toNat < m
@[simp]
theorem UInt8.not_le {a b : UInt8} :
¬a b b < a
theorem UInt8.toBitVec_inj {a b : UInt8} :
a.toBitVec = b.toBitVec a = b
theorem UInt8.le_antisymm {a b : UInt8} (h₁ : a b) (h₂ : b a) :
a = b
theorem UInt8.ne_of_toBitVec_ne {a b : UInt8} (h : a.toBitVec b.toBitVec) :
a b
theorem UInt8.val_inj {a b : UInt8} :
a.val = b.val a = b
@[simp]
theorem UInt8.ofNat_toNat {x : UInt8} :
ofNat x.toNat = x
theorem UInt8.lt_iff_toNat_lt {a b : UInt8} :
a < b a.toNat < b.toNat
theorem UInt8.one_def :
1 = { toBitVec := 1 }
@[simp]
theorem UInt8.toNat_toUInt64 (x : UInt8) :
x.toUInt64.toNat = x.toNat
@[simp]
theorem UInt8.toNat_zero :
toNat 0 = 0
theorem UInt8.lt_def {a b : UInt8} :
a < b a.toBitVec < b.toBitVec
theorem UInt8.toBitVec_eq_of_lt {a : Nat} :
a < size(ofNat a).toBitVec.toNat = a
theorem UInt8.zero_def :
0 = { toBitVec := 0 }
theorem UInt8.le_antisymm_iff {a b : UInt8} :
a = b a b b a
theorem UInt8.toNat.inj {a b : UInt8} :
a.toNat = b.toNata = b
@[simp]
theorem UInt8.toNat_mod (a b : UInt8) :
(a % b).toNat = a.toNat % b.toNat
theorem UInt8.lt_trans {a b c : UInt8} :
a < bb < ca < c
@[simp]
theorem UInt8.le_refl (a : UInt8) :
a a
theorem UInt8.mul_def (a b : UInt8) :
a * b = { toBitVec := a.toBitVec * b.toBitVec }
@[simp]
theorem UInt8.mk_ofNat (n : Nat) :
{ toBitVec := BitVec.ofNat 8 n } = OfNat.ofNat n
theorem UInt8.le_trans {a b c : UInt8} :
a bb ca c
theorem UInt8.lt_asymm {a b : UInt8} :
a < b¬b < a
@[simp]
theorem UInt8.toNat_add (a b : UInt8) :
(a + b).toNat = (a.toNat + b.toNat) % 2 ^ 8
@[simp]
theorem UInt8.toNat_ofNatCore {n : Nat} {h : n < size} :
(ofNatCore n h).toNat = n
@[simp]
theorem UInt8.mk_toBitVec_eq (a : UInt8) :
{ toBitVec := a.toBitVec } = a
@[deprecated UInt8.toNat_mod_lt (since := "2024-09-24")]
theorem UInt8.modn_lt {m : Nat} (u : UInt8) :
m > 0(u % m).toNat < m
@[simp]
theorem UInt8.toNat_div (a b : UInt8) :
(a / b).toNat = a.toNat / b.toNat
@[simp]
theorem UInt8.toNat_mk {a : BitVec 8} :
{ toBitVec := a }.toNat = a.toNat
theorem UInt8.eq_of_val_eq {a b : UInt8} (h : a.val = b.val) :
a = b
@[simp]
theorem UInt8.toNat_toUInt32 (x : UInt8) :
x.toUInt32.toNat = x.toNat
@[simp]
theorem UInt8.lt_irrefl (a : UInt8) :
¬a < a
theorem UInt8.sub_def (a b : UInt8) :
a - b = { toBitVec := a.toBitVec - b.toBitVec }
theorem UInt8.ne_of_lt {a b : UInt8} (h : a < b) :
a b
@[simp]
theorem UInt8.toNat_toUSize (x : UInt8) :
x.toUSize.toNat = x.toNat
theorem UInt8.le_def {a b : UInt8} :
a b a.toBitVec b.toBitVec
theorem UInt8.mod_def (a b : UInt8) :
a % b = { toBitVec := a.toBitVec % b.toBitVec }
@[simp]
theorem UInt8.toBitVec_ofNat (n : Nat) :
(OfNat.ofNat n).toBitVec = BitVec.ofNat 8 n
@[simp]
theorem UInt8.ofNat_one :
ofNat 1 = 1
theorem UInt8.toNat_sub (a b : UInt8) :
(a - b).toNat = (2 ^ 8 - b.toNat + a.toNat) % 2 ^ 8
@[simp]
theorem UInt8.toNat_ofNat {n : Nat} :
(ofNat n).toNat = n % 2 ^ 8
@[simp]
theorem UInt8.not_lt {a b : UInt8} :
¬a < b b a
theorem UInt8.toNat_lt_size (a : UInt8) :
a.toNat < size
theorem UInt8.toNat_inj {a b : UInt8} :
a.toNat = b.toNat a = b
@[simp]
theorem UInt8.val_val_eq_toNat (x : UInt8) :
x.val = x.toNat
theorem UInt8.toBitVec_eq_of_eq {a b : UInt8} (h : a = b) :
a.toBitVec = b.toBitVec
@[simp]
theorem UInt8.toNat_toUInt16 (x : UInt8) :
x.toUInt16.toNat = x.toNat
theorem UInt16.le_antisymm {a b : UInt16} (h₁ : a b) (h₂ : b a) :
a = b
theorem UInt16.lt_def {a b : UInt16} :
a < b a.toBitVec < b.toBitVec
@[simp]
theorem UInt16.toNat_toUInt32 (x : UInt16) :
x.toUInt32.toNat = x.toNat
theorem UInt16.val_inj {a b : UInt16} :
a.val = b.val a = b
@[simp]
theorem UInt16.toNat_toUInt8 (x : UInt16) :
x.toUInt8.toNat = x.toNat % 2 ^ 8
@[simp]
theorem UInt16.toNat_mod (a b : UInt16) :
(a % b).toNat = a.toNat % b.toNat
theorem UInt16.lt_trans {a b c : UInt16} :
a < bb < ca < c
theorem UInt16.sub_def (a b : UInt16) :
a - b = { toBitVec := a.toBitVec - b.toBitVec }
@[simp]
theorem UInt16.val_ofNat (n : Nat) :
theorem UInt16.le_iff_toNat_le {a b : UInt16} :
a b a.toNat b.toNat
@[simp]
theorem UInt16.toNat_mk {a : BitVec 16} :
{ toBitVec := a }.toNat = a.toNat
@[simp]
theorem UInt16.lt_irrefl (a : UInt16) :
¬a < a
theorem UInt16.le_antisymm_iff {a b : UInt16} :
a = b a b b a
@[simp]
theorem UInt16.toNat_mul (a b : UInt16) :
(a * b).toNat = a.toNat * b.toNat % 2 ^ 16
@[simp]
theorem UInt16.toNat_toUSize (x : UInt16) :
x.toUSize.toNat = x.toNat
@[simp]
theorem UInt16.toNat_add (a b : UInt16) :
(a + b).toNat = (a.toNat + b.toNat) % 2 ^ 16
@[simp]
theorem UInt16.mk_toBitVec_eq (a : UInt16) :
{ toBitVec := a.toBitVec } = a
theorem UInt16.le_def {a b : UInt16} :
a b a.toBitVec b.toBitVec
theorem UInt16.le_total (a b : UInt16) :
a b b a
theorem UInt16.le_trans {a b c : UInt16} :
a bb ca c
theorem UInt16.toBitVec_eq_of_eq {a b : UInt16} (h : a = b) :
a.toBitVec = b.toBitVec
@[simp]
theorem UInt16.le_refl (a : UInt16) :
a a
theorem UInt16.toNat_lt_size (a : UInt16) :
a.toNat < size
theorem UInt16.toNat_toBitVec_eq_toNat (x : UInt16) :
x.toBitVec.toNat = x.toNat
@[simp]
theorem UInt16.not_lt {a b : UInt16} :
¬a < b b a
theorem UInt16.lt_asymm {a b : UInt16} :
a < b¬b < a
theorem UInt16.toBitVec_inj {a b : UInt16} :
a.toBitVec = b.toBitVec a = b
@[simp]
theorem UInt16.mk_ofNat (n : Nat) :
{ toBitVec := BitVec.ofNat 16 n } = OfNat.ofNat n
theorem UInt16.lt_iff_toNat_lt {a b : UInt16} :
a < b a.toNat < b.toNat
theorem UInt16.toNat_inj {a b : UInt16} :
a.toNat = b.toNat a = b
theorem UInt16.mod_lt (a : UInt16) {b : UInt16} :
0 < ba % b < b
@[simp]
theorem UInt16.toNat_toUInt64 (x : UInt16) :
x.toUInt64.toNat = x.toNat
@[simp]
@[simp]
theorem UInt16.toNat_ofNat {n : Nat} :
(ofNat n).toNat = n % 2 ^ 16
theorem UInt16.eq_of_val_eq {a b : UInt16} (h : a.val = b.val) :
a = b
theorem UInt16.toBitVec_eq_of_lt {a : Nat} :
a < size(ofNat a).toBitVec.toNat = a
@[simp]
theorem UInt16.toNat_div (a b : UInt16) :
(a / b).toNat = a.toNat / b.toNat
theorem UInt16.ne_of_toBitVec_ne {a b : UInt16} (h : a.toBitVec b.toBitVec) :
a b
theorem UInt16.mod_def (a b : UInt16) :
a % b = { toBitVec := a.toBitVec % b.toBitVec }
@[deprecated UInt16.toNat_mod_lt (since := "2024-09-24")]
theorem UInt16.modn_lt {m : Nat} (u : UInt16) :
m > 0(u % m).toNat < m
theorem UInt16.ne_of_lt {a b : UInt16} (h : a < b) :
a b
@[simp]
theorem UInt16.ofNat_one :
ofNat 1 = 1
theorem UInt16.mul_def (a b : UInt16) :
a * b = { toBitVec := a.toBitVec * b.toBitVec }
theorem UInt16.one_def :
1 = { toBitVec := 1 }
@[simp]
theorem UInt16.ofNat_toNat {x : UInt16} :
ofNat x.toNat = x
@[simp]
theorem UInt16.toNat_ofNatCore {n : Nat} {h : n < size} :
(ofNatCore n h).toNat = n
theorem UInt16.toNat_mod_lt {m : Nat} (u : UInt16) :
m > 0(u % ofNat m).toNat < m
theorem UInt16.toNat.inj {a b : UInt16} :
a.toNat = b.toNata = b
theorem UInt16.toNat_ofNat_of_lt {n : Nat} (h : n < size) :
(ofNat n).toNat = n
theorem UInt16.eq_of_toBitVec_eq {a b : UInt16} (h : a.toBitVec = b.toBitVec) :
a = b
@[simp]
theorem UInt16.val_val_eq_toNat (x : UInt16) :
x.val = x.toNat
@[simp]
theorem UInt16.toNat_sub_of_le (a b : UInt16) :
b a(a - b).toNat = a.toNat - b.toNat
@[simp]
theorem UInt16.not_le {a b : UInt16} :
¬a b b < a
theorem UInt16.add_def (a b : UInt16) :
a + b = { toBitVec := a.toBitVec + b.toBitVec }
@[simp]
theorem UInt16.toBitVec_ofNat (n : Nat) :
(OfNat.ofNat n).toBitVec = BitVec.ofNat 16 n
theorem UInt16.toNat_sub (a b : UInt16) :
(a - b).toNat = (2 ^ 16 - b.toNat + a.toNat) % 2 ^ 16
theorem UInt16.zero_def :
0 = { toBitVec := 0 }
@[simp]
theorem UInt32.le_refl (a : UInt32) :
a a
@[simp]
theorem UInt32.toNat_sub (a b : UInt32) :
(a - b).toNat = (2 ^ 32 - b.toNat + a.toNat) % 2 ^ 32
theorem UInt32.toNat_lt_size (a : UInt32) :
a.toNat < size
theorem UInt32.add_def (a b : UInt32) :
a + b = { toBitVec := a.toBitVec + b.toBitVec }
theorem UInt32.eq_of_val_eq {a b : UInt32} (h : a.val = b.val) :
a = b
@[simp]
theorem UInt32.val_ofNat (n : Nat) :
theorem UInt32.toBitVec_eq_of_eq {a b : UInt32} (h : a = b) :
a.toBitVec = b.toBitVec
@[simp]
theorem UInt32.not_le {a b : UInt32} :
¬a b b < a
theorem UInt32.le_antisymm {a b : UInt32} (h₁ : a b) (h₂ : b a) :
a = b
theorem UInt32.lt_trans {a b c : UInt32} :
a < bb < ca < c
@[simp]
theorem UInt32.mk_toBitVec_eq (a : UInt32) :
{ toBitVec := a.toBitVec } = a
theorem UInt32.toNat_inj {a b : UInt32} :
a.toNat = b.toNat a = b
@[simp]
theorem UInt32.toNat_mk {a : BitVec 32} :
{ toBitVec := a }.toNat = a.toNat
theorem UInt32.le_total (a b : UInt32) :
a b b a
@[simp]
theorem UInt32.toNat_ofNatCore {n : Nat} {h : n < size} :
(ofNatCore n h).toNat = n
theorem UInt32.le_def {a b : UInt32} :
a b a.toBitVec b.toBitVec
theorem UInt32.le_iff_toNat_le {a b : UInt32} :
a b a.toNat b.toNat
theorem UInt32.lt_asymm {a b : UInt32} :
a < b¬b < a
@[simp]
theorem UInt32.toNat_mul (a b : UInt32) :
(a * b).toNat = a.toNat * b.toNat % 2 ^ 32
theorem UInt32.lt_iff_toNat_lt {a b : UInt32} :
a < b a.toNat < b.toNat
theorem UInt32.le_antisymm_iff {a b : UInt32} :
a = b a b b a
@[simp]
theorem UInt32.toNat_add (a b : UInt32) :
(a + b).toNat = (a.toNat + b.toNat) % 2 ^ 32
@[deprecated UInt32.toNat_mod_lt (since := "2024-09-24")]
theorem UInt32.modn_lt {m : Nat} (u : UInt32) :
m > 0(u % m).toNat < m
@[simp]
theorem UInt32.mk_ofNat (n : Nat) :
{ toBitVec := BitVec.ofNat 32 n } = OfNat.ofNat n
@[simp]
theorem UInt32.lt_irrefl (a : UInt32) :
¬a < a
theorem UInt32.ne_of_toBitVec_ne {a b : UInt32} (h : a.toBitVec b.toBitVec) :
a b
theorem UInt32.le_trans {a b c : UInt32} :
a bb ca c
@[simp]
theorem UInt32.not_lt {a b : UInt32} :
¬a < b b a
@[simp]
theorem UInt32.ofNat_toNat {x : UInt32} :
ofNat x.toNat = x
theorem UInt32.toNat_mod_lt {m : Nat} (u : UInt32) :
m > 0(u % ofNat m).toNat < m
theorem UInt32.sub_def (a b : UInt32) :
a - b = { toBitVec := a.toBitVec - b.toBitVec }
@[simp]
theorem UInt32.val_val_eq_toNat (x : UInt32) :
x.val = x.toNat
theorem UInt32.toBitVec_inj {a b : UInt32} :
a.toBitVec = b.toBitVec a = b
theorem UInt32.toNat_ofNat_of_lt {n : Nat} (h : n < size) :
(ofNat n).toNat = n
theorem UInt32.toNat_toBitVec_eq_toNat (x : UInt32) :
x.toBitVec.toNat = x.toNat
theorem UInt32.val_inj {a b : UInt32} :
a.val = b.val a = b
theorem UInt32.toBitVec_eq_of_lt {a : Nat} :
a < size(ofNat a).toBitVec.toNat = a
theorem UInt32.eq_of_toBitVec_eq {a b : UInt32} (h : a.toBitVec = b.toBitVec) :
a = b
@[simp]
theorem UInt32.toNat_toUSize (x : UInt32) :
x.toUSize.toNat = x.toNat
theorem UInt32.lt_def {a b : UInt32} :
a < b a.toBitVec < b.toBitVec
theorem UInt32.ne_of_lt {a b : UInt32} (h : a < b) :
a b
theorem UInt32.mod_lt (a : UInt32) {b : UInt32} :
0 < ba % b < b
@[simp]
theorem UInt32.toNat_div (a b : UInt32) :
(a / b).toNat = a.toNat / b.toNat
@[simp]
theorem UInt32.toNat_mod (a b : UInt32) :
(a % b).toNat = a.toNat % b.toNat
theorem UInt32.zero_def :
0 = { toBitVec := 0 }
theorem UInt32.one_def :
1 = { toBitVec := 1 }
theorem UInt32.mul_def (a b : UInt32) :
a * b = { toBitVec := a.toBitVec * b.toBitVec }
@[simp]
theorem UInt32.toNat_ofNat {n : Nat} :
(ofNat n).toNat = n % 2 ^ 32
@[simp]
theorem UInt32.ofNat_one :
ofNat 1 = 1
@[simp]
theorem UInt32.toBitVec_ofNat (n : Nat) :
(OfNat.ofNat n).toBitVec = BitVec.ofNat 32 n
theorem UInt32.mod_def (a b : UInt32) :
a % b = { toBitVec := a.toBitVec % b.toBitVec }
@[simp]
theorem UInt32.toNat_toUInt64 (x : UInt32) :
x.toUInt64.toNat = x.toNat
@[simp]
theorem UInt32.toNat_toUInt16 (x : UInt32) :
x.toUInt16.toNat = x.toNat % 2 ^ 16
theorem UInt32.toNat.inj {a b : UInt32} :
a.toNat = b.toNata = b
@[simp]
theorem UInt32.toNat_toUInt8 (x : UInt32) :
x.toUInt8.toNat = x.toNat % 2 ^ 8
@[simp]
theorem UInt32.toNat_sub_of_le (a b : UInt32) :
b a(a - b).toNat = a.toNat - b.toNat
@[simp]
theorem UInt64.toNat_sub_of_le (a b : UInt64) :
b a(a - b).toNat = a.toNat - b.toNat
theorem UInt64.toNat_lt_size (a : UInt64) :
a.toNat < size
theorem UInt64.mod_def (a b : UInt64) :
a % b = { toBitVec := a.toBitVec % b.toBitVec }
@[simp]
theorem UInt64.toNat_mod (a b : UInt64) :
(a % b).toNat = a.toNat % b.toNat
theorem UInt64.eq_of_val_eq {a b : UInt64} (h : a.val = b.val) :
a = b
@[simp]
theorem UInt64.toNat_mul (a b : UInt64) :
(a * b).toNat = a.toNat * b.toNat % 2 ^ 64
@[simp]
theorem UInt64.not_lt {a b : UInt64} :
¬a < b b a
@[simp]
theorem UInt64.ofNat_one :
ofNat 1 = 1
@[simp]
theorem UInt64.val_ofNat (n : Nat) :
@[simp]
theorem UInt64.toNat_ofNat {n : Nat} :
(ofNat n).toNat = n % 2 ^ 64
theorem UInt64.toNat.inj {a b : UInt64} :
a.toNat = b.toNata = b
theorem UInt64.sub_def (a b : UInt64) :
a - b = { toBitVec := a.toBitVec - b.toBitVec }
@[simp]
theorem UInt64.not_le {a b : UInt64} :
¬a b b < a
theorem UInt64.toNat_sub (a b : UInt64) :
(a - b).toNat = (2 ^ 64 - b.toNat + a.toNat) % 2 ^ 64
theorem UInt64.toNat_toBitVec_eq_toNat (x : UInt64) :
x.toBitVec.toNat = x.toNat
@[simp]
theorem UInt64.toBitVec_ofNat (n : Nat) :
(OfNat.ofNat n).toBitVec = BitVec.ofNat 64 n
@[simp]
theorem UInt64.toNat_toUInt8 (x : UInt64) :
x.toUInt8.toNat = x.toNat % 2 ^ 8
@[simp]
theorem UInt64.toNat_ofNatCore {n : Nat} {h : n < size} :
(ofNatCore n h).toNat = n
@[simp]
@[simp]
theorem UInt64.lt_irrefl (a : UInt64) :
¬a < a
theorem UInt64.lt_def {a b : UInt64} :
a < b a.toBitVec < b.toBitVec
theorem UInt64.toBitVec_eq_of_lt {a : Nat} :
a < size(ofNat a).toBitVec.toNat = a
theorem UInt64.eq_of_toBitVec_eq {a b : UInt64} (h : a.toBitVec = b.toBitVec) :
a = b
@[simp]
theorem UInt64.mk_toBitVec_eq (a : UInt64) :
{ toBitVec := a.toBitVec } = a
@[simp]
theorem UInt64.val_val_eq_toNat (x : UInt64) :
x.val = x.toNat
theorem UInt64.lt_iff_toNat_lt {a b : UInt64} :
a < b a.toNat < b.toNat
theorem UInt64.le_iff_toNat_le {a b : UInt64} :
a b a.toNat b.toNat
@[simp]
theorem UInt64.toNat_toUInt32 (x : UInt64) :
x.toUInt32.toNat = x.toNat % 2 ^ 32
theorem UInt64.toBitVec_inj {a b : UInt64} :
a.toBitVec = b.toBitVec a = b
theorem UInt64.val_inj {a b : UInt64} :
a.val = b.val a = b
@[simp]
theorem UInt64.mk_ofNat (n : Nat) :
{ toBitVec := BitVec.ofNat 64 n } = OfNat.ofNat n
@[simp]
theorem UInt64.le_refl (a : UInt64) :
a a
theorem UInt64.toBitVec_eq_of_eq {a b : UInt64} (h : a = b) :
a.toBitVec = b.toBitVec
theorem UInt64.toNat_mod_lt {m : Nat} (u : UInt64) :
m > 0(u % ofNat m).toNat < m
theorem UInt64.le_total (a b : UInt64) :
a b b a
@[simp]
theorem UInt64.toNat_add (a b : UInt64) :
(a + b).toNat = (a.toNat + b.toNat) % 2 ^ 64
theorem UInt64.ne_of_lt {a b : UInt64} (h : a < b) :
a b
theorem UInt64.le_trans {a b c : UInt64} :
a bb ca c
theorem UInt64.mul_def (a b : UInt64) :
a * b = { toBitVec := a.toBitVec * b.toBitVec }
theorem UInt64.toNat_ofNat_of_lt {n : Nat} (h : n < size) :
(ofNat n).toNat = n
theorem UInt64.le_antisymm {a b : UInt64} (h₁ : a b) (h₂ : b a) :
a = b
theorem UInt64.zero_def :
0 = { toBitVec := 0 }
@[deprecated UInt64.toNat_mod_lt (since := "2024-09-24")]
theorem UInt64.modn_lt {m : Nat} (u : UInt64) :
m > 0(u % m).toNat < m
theorem UInt64.lt_trans {a b c : UInt64} :
a < bb < ca < c
theorem UInt64.one_def :
1 = { toBitVec := 1 }
@[simp]
theorem UInt64.ofNat_toNat {x : UInt64} :
ofNat x.toNat = x
@[simp]
theorem UInt64.toNat_toUInt16 (x : UInt64) :
x.toUInt16.toNat = x.toNat % 2 ^ 16
@[simp]
theorem UInt64.toNat_mk {a : BitVec 64} :
{ toBitVec := a }.toNat = a.toNat
@[simp]
theorem UInt64.toNat_toUSize (x : UInt64) :
x.toUSize.toNat = x.toNat % 2 ^ System.Platform.numBits
theorem UInt64.lt_asymm {a b : UInt64} :
a < b¬b < a
theorem UInt64.le_antisymm_iff {a b : UInt64} :
a = b a b b a
theorem UInt64.mod_lt (a : UInt64) {b : UInt64} :
0 < ba % b < b
theorem UInt64.ne_of_toBitVec_ne {a b : UInt64} (h : a.toBitVec b.toBitVec) :
a b
theorem UInt64.le_def {a b : UInt64} :
a b a.toBitVec b.toBitVec
@[simp]
theorem UInt64.toNat_div (a b : UInt64) :
(a / b).toNat = a.toNat / b.toNat
theorem UInt64.toNat_inj {a b : UInt64} :
a.toNat = b.toNat a = b
theorem UInt64.add_def (a b : UInt64) :
a + b = { toBitVec := a.toBitVec + b.toBitVec }
@[simp]
theorem USize.not_lt {a b : USize} :
¬a < b b a
theorem USize.le_def {a b : USize} :
a b a.toBitVec b.toBitVec
theorem USize.eq_of_toBitVec_eq {a b : USize} (h : a.toBitVec = b.toBitVec) :
a = b
theorem USize.one_def :
1 = { toBitVec := 1 }
@[simp]
theorem USize.not_le {a b : USize} :
¬a b b < a
@[simp]
theorem USize.toNat_sub_of_le (a b : USize) :
b a(a - b).toNat = a.toNat - b.toNat
theorem USize.lt_asymm {a b : USize} :
a < b¬b < a
theorem USize.le_antisymm {a b : USize} (h₁ : a b) (h₂ : b a) :
a = b
theorem USize.toBitVec_eq_of_lt {a : Nat} :
a < size(ofNat a).toBitVec.toNat = a
theorem USize.lt_trans {a b c : USize} :
a < bb < ca < c
@[simp]
theorem USize.toNat_zero :
toNat 0 = 0
theorem USize.lt_def {a b : USize} :
a < b a.toBitVec < b.toBitVec
@[simp]
theorem USize.toNat_mk {a : BitVec System.Platform.numBits} :
{ toBitVec := a }.toNat = a.toNat
theorem USize.toNat_ofNat_of_lt {n : Nat} (h : n < size) :
(ofNat n).toNat = n
@[simp]
theorem USize.toNat_mul (a b : USize) :
(a * b).toNat = a.toNat * b.toNat % 2 ^ System.Platform.numBits
@[simp]
theorem USize.toNat_div (a b : USize) :
(a / b).toNat = a.toNat / b.toNat
@[simp]
theorem USize.ofNat_one :
ofNat 1 = 1
@[simp]
theorem USize.toNat_ofNat {n : Nat} :
theorem USize.mul_def (a b : USize) :
a * b = { toBitVec := a.toBitVec * b.toBitVec }
theorem USize.toNat_lt_size (a : USize) :
a.toNat < size
@[simp]
theorem USize.mk_toBitVec_eq (a : USize) :
{ toBitVec := a.toBitVec } = a
theorem USize.val_inj {a b : USize} :
a.val = b.val a = b
theorem USize.zero_def :
0 = { toBitVec := 0 }
theorem USize.le_trans {a b c : USize} :
a bb ca c
theorem USize.eq_of_val_eq {a b : USize} (h : a.val = b.val) :
a = b
theorem USize.ne_of_lt {a b : USize} (h : a < b) :
a b
theorem USize.mod_lt (a : USize) {b : USize} :
0 < ba % b < b
@[simp]
theorem USize.toNat_ofNatCore {n : Nat} {h : n < size} :
(ofNatCore n h).toNat = n
@[simp]
theorem USize.le_refl (a : USize) :
a a
theorem USize.toNat_mod_lt {m : Nat} (u : USize) :
m > 0(u % ofNat m).toNat < m
theorem USize.le_total (a b : USize) :
a b b a
theorem USize.add_def (a b : USize) :
a + b = { toBitVec := a.toBitVec + b.toBitVec }
theorem USize.mod_def (a b : USize) :
a % b = { toBitVec := a.toBitVec % b.toBitVec }
theorem USize.le_iff_toNat_le {a b : USize} :
a b a.toNat b.toNat
theorem USize.lt_iff_toNat_lt {a b : USize} :
a < b a.toNat < b.toNat
theorem USize.toBitVec_inj {a b : USize} :
a.toBitVec = b.toBitVec a = b
theorem USize.ne_of_toBitVec_ne {a b : USize} (h : a.toBitVec b.toBitVec) :
a b
theorem USize.le_antisymm_iff {a b : USize} :
a = b a b b a
@[simp]
theorem USize.toNat_add (a b : USize) :
(a + b).toNat = (a.toNat + b.toNat) % 2 ^ System.Platform.numBits
theorem USize.toBitVec_eq_of_eq {a b : USize} (h : a = b) :
a.toBitVec = b.toBitVec
theorem USize.sub_def (a b : USize) :
a - b = { toBitVec := a.toBitVec - b.toBitVec }
theorem USize.toNat.inj {a b : USize} :
a.toNat = b.toNata = b
theorem USize.toNat_toBitVec_eq_toNat (x : USize) :
x.toBitVec.toNat = x.toNat
theorem USize.toNat_inj {a b : USize} :
a.toNat = b.toNat a = b
@[simp]
theorem USize.toNat_sub (a b : USize) :
(a - b).toNat = (2 ^ System.Platform.numBits - b.toNat + a.toNat) % 2 ^ System.Platform.numBits
@[simp]
theorem USize.toNat_mod (a b : USize) :
(a % b).toNat = a.toNat % b.toNat
@[simp]
theorem USize.ofNat_toNat {x : USize} :
ofNat x.toNat = x
@[simp]
theorem USize.val_val_eq_toNat (x : USize) :
x.val = x.toNat
@[simp]
theorem USize.val_ofNat (n : Nat) :
@[simp]
theorem USize.lt_irrefl (a : USize) :
¬a < a
@[deprecated USize.toNat_mod_lt (since := "2024-09-24")]
theorem USize.modn_lt {m : Nat} (u : USize) :
m > 0(u % m).toNat < m
@[simp]
theorem USize.toNat_ofNat32 {n : Nat} {h : n < 4294967296} :
(ofNat32 n h).toNat = n
@[simp]
theorem USize.toNat_toUInt32 (x : USize) :
x.toUInt32.toNat = x.toNat % 2 ^ 32
@[simp]
theorem USize.toNat_toUInt64 (x : USize) :
x.toUInt64.toNat = x.toNat
theorem USize.toNat_ofNat_of_lt_32 {n : Nat} (h : n < 4294967296) :
(ofNat n).toNat = n
theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) :
n < ofNat mn.toNat < m
theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) :
ofNat m < nm < n.toNat
theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) :
n ofNat mn.toNat m
theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) :
ofNat m nm n.toNat
@[reducible, inline, deprecated UInt8.toNat_zero (since := "2024-06-23")]
Equations
@[reducible, inline, deprecated UInt8.toNat_div (since := "2024-06-23")]
abbrev UInt8.div_toNat (a b : UInt8) :
(a / b).toNat = a.toNat / b.toNat
Equations
@[reducible, inline, deprecated UInt8.toNat_mod (since := "2024-06-23")]
abbrev UInt8.mod_toNat (a b : UInt8) :
(a % b).toNat = a.toNat % b.toNat
Equations
@[reducible, inline, deprecated UInt16.toNat_zero (since := "2024-06-23")]
Equations
@[reducible, inline, deprecated UInt16.toNat_div (since := "2024-06-23")]
abbrev UInt16.div_toNat (a b : UInt16) :
(a / b).toNat = a.toNat / b.toNat
Equations
@[reducible, inline, deprecated UInt16.toNat_mod (since := "2024-06-23")]
abbrev UInt16.mod_toNat (a b : UInt16) :
(a % b).toNat = a.toNat % b.toNat
Equations
@[reducible, inline, deprecated UInt32.toNat_zero (since := "2024-06-23")]
Equations
@[reducible, inline, deprecated UInt32.toNat_div (since := "2024-06-23")]
abbrev UInt32.div_toNat (a b : UInt32) :
(a / b).toNat = a.toNat / b.toNat
Equations
@[reducible, inline, deprecated UInt32.toNat_mod (since := "2024-06-23")]
abbrev UInt32.mod_toNat (a b : UInt32) :
(a % b).toNat = a.toNat % b.toNat
Equations
@[reducible, inline, deprecated UInt64.toNat_zero (since := "2024-06-23")]
Equations
@[reducible, inline, deprecated UInt64.toNat_div (since := "2024-06-23")]
abbrev UInt64.div_toNat (a b : UInt64) :
(a / b).toNat = a.toNat / b.toNat
Equations
@[reducible, inline, deprecated UInt64.toNat_mod (since := "2024-06-23")]
abbrev UInt64.mod_toNat (a b : UInt64) :
(a % b).toNat = a.toNat % b.toNat
Equations
@[reducible, inline, deprecated USize.toNat_zero (since := "2024-06-23")]
Equations
@[reducible, inline, deprecated USize.toNat_div (since := "2024-06-23")]
abbrev USize.div_toNat (a b : USize) :
(a / b).toNat = a.toNat / b.toNat
Equations
@[reducible, inline, deprecated USize.toNat_mod (since := "2024-06-23")]
abbrev USize.mod_toNat (a b : USize) :
(a % b).toNat = a.toNat % b.toNat
Equations