Documentation

Init.Data.UInt.Lemmas

Equations
  • One or more equations did not get rendered due to their size.
theorem UInt8.sub_def (a b : UInt8) :
a - b = { toBitVec := a.toBitVec - b.toBitVec }
@[simp]
theorem UInt8.not_le {a b : UInt8} :
¬a b b < a
theorem UInt8.toBitVec_eq_of_lt {a : Nat} :
a < UInt8.size(UInt8.ofNat a).toBitVec.toNat = a
@[simp]
theorem UInt8.lt_irrefl (a : UInt8) :
¬a < a
theorem UInt8.ne_of_lt {a b : UInt8} (h : a < b) :
a b
@[simp]
theorem UInt8.toBitVec_ofNat (n : Nat) :
(OfNat.ofNat n).toBitVec = BitVec.ofNat 8 n
theorem UInt8.add_def (a b : UInt8) :
a + b = { toBitVec := a.toBitVec + b.toBitVec }
theorem UInt8.toNat_mod_lt {m : Nat} (u : UInt8) :
m > 0(u % UInt8.ofNat m).toNat < m
theorem UInt8.lt_def {a b : UInt8} :
a < b a.toBitVec < b.toBitVec
theorem UInt8.zero_def :
0 = { toBitVec := 0 }
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.toNat_ofNat_of_lt {n : Nat} (h : n < UInt8.size) :
(UInt8.ofNat n).toNat = n
theorem UInt8.eq_of_toBitVec_eq {a b : UInt8} (h : a.toBitVec = b.toBitVec) :
a = b
@[simp]
theorem UInt8.mk_ofNat (n : Nat) :
{ toBitVec := BitVec.ofNat 8 n } = OfNat.ofNat n
theorem UInt8.lt_asymm {a b : UInt8} :
a < b¬b < a
@[simp]
theorem UInt8.mk_toBitVec_eq (a : UInt8) :
{ toBitVec := a.toBitVec } = a
@[simp]
theorem UInt8.toNat_div (a b : UInt8) :
(a / b).toNat = a.toNat / b.toNat
theorem UInt8.ne_of_toBitVec_ne {a b : UInt8} (h : a.toBitVec b.toBitVec) :
a b
@[simp]
theorem UInt8.val_ofNat (n : Nat) :
theorem UInt8.le_def {a b : UInt8} :
a b a.toBitVec b.toBitVec
@[simp]
theorem UInt8.not_lt {a b : UInt8} :
¬a < b b a
theorem UInt8.toBitVec_eq_of_eq {a b : UInt8} (h : a = b) :
a.toBitVec = b.toBitVec
@[simp]
@[simp]
theorem UInt8.le_refl (a : UInt8) :
a a
theorem UInt8.le_trans {a b c : UInt8} :
a bb ca c
@[simp]
theorem UInt8.mod_lt (a : UInt8) {b : UInt8} :
0 < ba % b < b
theorem UInt8.mul_def (a b : UInt8) :
a * b = { toBitVec := a.toBitVec * b.toBitVec }
theorem UInt8.one_def :
1 = { toBitVec := 1 }
theorem UInt8.lt_trans {a b c : UInt8} :
a < bb < ca < c
theorem UInt8.mod_def (a b : UInt8) :
a % b = { toBitVec := a.toBitVec % b.toBitVec }
@[simp]
theorem UInt8.toNat_sub_of_le (a b : UInt8) :
b a(a - b).toNat = a.toNat - b.toNat
@[deprecated UInt8.toNat_mod_lt]
theorem UInt8.modn_lt {m : Nat} (u : UInt8) :
m > 0(u % m).toNat < m
theorem UInt8.le_total (a b : UInt8) :
a b b a
theorem UInt8.eq_of_val_eq {a b : UInt8} (h : a.val = b.val) :
a = b
theorem UInt16.lt_asymm {a b : UInt16} :
a < b¬b < a
@[simp]
theorem UInt16.toNat_mod (a b : UInt16) :
(a % b).toNat = a.toNat % b.toNat
theorem UInt16.le_def {a b : UInt16} :
a b a.toBitVec b.toBitVec
@[simp]
theorem UInt16.toBitVec_ofNat (n : Nat) :
(OfNat.ofNat n).toBitVec = BitVec.ofNat 16 n
theorem UInt16.lt_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
theorem UInt16.le_total (a b : UInt16) :
a b b a
theorem UInt16.ne_of_lt {a b : UInt16} (h : a < b) :
a b
@[simp]
theorem UInt16.lt_irrefl (a : UInt16) :
¬a < a
theorem UInt16.one_def :
1 = { toBitVec := 1 }
theorem UInt16.toNat.inj {a b : UInt16} :
a.toNat = b.toNata = b
theorem UInt16.zero_def :
0 = { toBitVec := 0 }
theorem UInt16.lt_def {a b : UInt16} :
a < b a.toBitVec < b.toBitVec
theorem UInt16.mod_def (a b : UInt16) :
a % b = { toBitVec := a.toBitVec % b.toBitVec }
theorem UInt16.sub_def (a b : UInt16) :
a - b = { toBitVec := a.toBitVec - b.toBitVec }
theorem UInt16.mod_lt (a : UInt16) {b : UInt16} :
0 < ba % b < b
theorem UInt16.toBitVec_eq_of_lt {a : Nat} :
a < UInt16.size(UInt16.ofNat a).toBitVec.toNat = a
theorem UInt16.ne_of_toBitVec_ne {a b : UInt16} (h : a.toBitVec b.toBitVec) :
a b
@[simp]
theorem UInt16.mk_toBitVec_eq (a : UInt16) :
{ toBitVec := a.toBitVec } = a
@[simp]
theorem UInt16.val_ofNat (n : Nat) :
theorem UInt16.mul_def (a b : UInt16) :
a * b = { toBitVec := a.toBitVec * b.toBitVec }
@[simp]
theorem UInt16.mk_ofNat (n : Nat) :
{ toBitVec := BitVec.ofNat 16 n } = OfNat.ofNat n
theorem UInt16.eq_of_toBitVec_eq {a b : UInt16} (h : a.toBitVec = b.toBitVec) :
a = b
@[simp]
theorem UInt16.toNat_sub_of_le (a b : UInt16) :
b a(a - b).toNat = a.toNat - b.toNat
theorem UInt16.add_def (a b : UInt16) :
a + b = { toBitVec := a.toBitVec + b.toBitVec }
theorem UInt16.eq_of_val_eq {a b : UInt16} (h : a.val = b.val) :
a = b
@[simp]
theorem UInt16.toNat_div (a b : UInt16) :
(a / b).toNat = a.toNat / b.toNat
@[simp]
theorem UInt16.not_le {a b : UInt16} :
¬a b b < a
theorem UInt16.toNat_mod_lt {m : Nat} (u : UInt16) :
m > 0(u % UInt16.ofNat m).toNat < m
theorem UInt16.le_trans {a b c : UInt16} :
a bb ca c
@[simp]
theorem UInt16.le_refl (a : UInt16) :
a a
@[deprecated UInt16.toNat_mod_lt]
theorem UInt16.modn_lt {m : Nat} (u : UInt16) :
m > 0(u % m).toNat < m
@[simp]
theorem UInt16.not_lt {a b : UInt16} :
¬a < b b a
theorem UInt16.toNat_ofNat_of_lt {n : Nat} (h : n < UInt16.size) :
(UInt16.ofNat n).toNat = n
@[simp]
theorem UInt32.not_lt {a b : UInt32} :
¬a < b b a
theorem UInt32.sub_def (a b : UInt32) :
a - b = { toBitVec := a.toBitVec - b.toBitVec }
theorem UInt32.mul_def (a b : UInt32) :
a * b = { toBitVec := a.toBitVec * b.toBitVec }
theorem UInt32.mod_def (a b : UInt32) :
a % b = { toBitVec := a.toBitVec % b.toBitVec }
theorem UInt32.le_total (a b : UInt32) :
a b b a
@[simp]
theorem UInt32.lt_irrefl (a : UInt32) :
¬a < a
@[simp]
theorem UInt32.mk_ofNat (n : Nat) :
{ toBitVec := BitVec.ofNat 32 n } = OfNat.ofNat n
theorem UInt32.le_trans {a b c : UInt32} :
a bb ca c
theorem UInt32.eq_of_toBitVec_eq {a b : UInt32} (h : a.toBitVec = b.toBitVec) :
a = b
theorem UInt32.mod_lt (a : UInt32) {b : UInt32} :
0 < ba % b < b
theorem UInt32.one_def :
1 = { toBitVec := 1 }
theorem UInt32.ne_of_toBitVec_ne {a b : UInt32} (h : a.toBitVec b.toBitVec) :
a b
theorem UInt32.le_def {a b : UInt32} :
a b a.toBitVec b.toBitVec
theorem UInt32.add_def (a b : UInt32) :
a + b = { toBitVec := a.toBitVec + b.toBitVec }
theorem UInt32.toNat_ofNat_of_lt {n : Nat} (h : n < UInt32.size) :
(UInt32.ofNat n).toNat = n
theorem UInt32.eq_of_val_eq {a b : UInt32} (h : a.val = b.val) :
a = b
@[simp]
theorem UInt32.le_refl (a : UInt32) :
a a
theorem UInt32.toNat.inj {a b : UInt32} :
a.toNat = b.toNata = b
@[simp]
theorem UInt32.toNat_sub_of_le (a b : UInt32) :
b a(a - b).toNat = a.toNat - b.toNat
@[deprecated UInt32.toNat_mod_lt]
theorem UInt32.modn_lt {m : Nat} (u : UInt32) :
m > 0(u % m).toNat < m
theorem UInt32.toNat_mod_lt {m : Nat} (u : UInt32) :
m > 0(u % UInt32.ofNat m).toNat < m
@[simp]
theorem UInt32.val_ofNat (n : Nat) :
@[simp]
theorem UInt32.not_le {a b : UInt32} :
¬a b b < a
theorem UInt32.ne_of_lt {a b : UInt32} (h : a < b) :
a b
@[simp]
theorem UInt32.toBitVec_ofNat (n : Nat) :
(OfNat.ofNat n).toBitVec = BitVec.ofNat 32 n
theorem UInt32.lt_asymm {a b : UInt32} :
a < b¬b < a
theorem UInt32.toBitVec_eq_of_lt {a : Nat} :
a < UInt32.size(UInt32.ofNat a).toBitVec.toNat = a
theorem UInt32.toBitVec_eq_of_eq {a b : UInt32} (h : a = b) :
a.toBitVec = b.toBitVec
@[simp]
theorem UInt32.mk_toBitVec_eq (a : UInt32) :
{ toBitVec := a.toBitVec } = a
theorem UInt32.lt_def {a b : UInt32} :
a < b a.toBitVec < b.toBitVec
@[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.lt_trans {a b c : UInt32} :
a < bb < ca < c
theorem UInt32.zero_def :
0 = { toBitVec := 0 }
@[simp]
theorem UInt64.le_refl (a : UInt64) :
a a
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 }
theorem UInt64.add_def (a b : UInt64) :
a + b = { toBitVec := a.toBitVec + b.toBitVec }
@[simp]
theorem UInt64.lt_irrefl (a : UInt64) :
¬a < a
@[simp]
theorem UInt64.not_le {a b : UInt64} :
¬a b b < a
theorem UInt64.toNat_ofNat_of_lt {n : Nat} (h : n < UInt64.size) :
(UInt64.ofNat n).toNat = n
theorem UInt64.le_def {a b : UInt64} :
a b a.toBitVec b.toBitVec
theorem UInt64.eq_of_val_eq {a b : UInt64} (h : a.val = b.val) :
a = b
theorem UInt64.lt_def {a b : UInt64} :
a < b a.toBitVec < b.toBitVec
theorem UInt64.eq_of_toBitVec_eq {a b : UInt64} (h : a.toBitVec = b.toBitVec) :
a = b
@[simp]
theorem UInt64.toBitVec_ofNat (n : Nat) :
(OfNat.ofNat n).toBitVec = BitVec.ofNat 64 n
@[simp]
theorem UInt64.mk_ofNat (n : Nat) :
{ toBitVec := BitVec.ofNat 64 n } = OfNat.ofNat n
theorem UInt64.ne_of_lt {a b : UInt64} (h : a < b) :
a b
@[simp]
theorem UInt64.not_lt {a b : UInt64} :
¬a < b b a
theorem UInt64.toBitVec_eq_of_lt {a : Nat} :
a < UInt64.size(UInt64.ofNat a).toBitVec.toNat = a
@[simp]
theorem UInt64.toNat_mod (a b : UInt64) :
(a % b).toNat = a.toNat % b.toNat
theorem UInt64.mod_lt (a : UInt64) {b : UInt64} :
0 < ba % b < b
@[simp]
theorem UInt64.toNat_div (a b : UInt64) :
(a / b).toNat = a.toNat / b.toNat
@[simp]
theorem UInt64.mk_toBitVec_eq (a : UInt64) :
{ toBitVec := a.toBitVec } = a
theorem UInt64.lt_asymm {a b : UInt64} :
a < b¬b < a
theorem UInt64.mod_def (a b : UInt64) :
a % b = { toBitVec := a.toBitVec % b.toBitVec }
theorem UInt64.le_total (a b : UInt64) :
a b b a
theorem UInt64.toNat_mod_lt {m : Nat} (u : UInt64) :
m > 0(u % UInt64.ofNat m).toNat < m
theorem UInt64.lt_trans {a b c : UInt64} :
a < bb < ca < c
theorem UInt64.le_trans {a b c : UInt64} :
a bb ca c
@[deprecated UInt64.toNat_mod_lt]
theorem UInt64.modn_lt {m : Nat} (u : UInt64) :
m > 0(u % m).toNat < m
@[simp]
theorem UInt64.val_ofNat (n : Nat) :
theorem UInt64.mul_def (a b : UInt64) :
a * b = { toBitVec := a.toBitVec * b.toBitVec }
theorem UInt64.zero_def :
0 = { toBitVec := 0 }
theorem UInt64.one_def :
1 = { toBitVec := 1 }
theorem UInt64.ne_of_toBitVec_ne {a b : UInt64} (h : a.toBitVec b.toBitVec) :
a b
@[simp]
theorem UInt64.toNat_sub_of_le (a b : UInt64) :
b a(a - b).toNat = a.toNat - b.toNat
theorem UInt64.toBitVec_eq_of_eq {a b : UInt64} (h : a = b) :
a.toBitVec = b.toBitVec
theorem USize.toBitVec_eq_of_eq {a b : USize} (h : a = b) :
a.toBitVec = b.toBitVec
theorem USize.mod_lt (a : USize) {b : USize} :
0 < ba % b < b
theorem USize.one_def :
1 = { toBitVec := 1 }
theorem USize.mul_def (a b : USize) :
a * b = { toBitVec := a.toBitVec * b.toBitVec }
@[simp]
theorem USize.toNat_mod (a b : USize) :
(a % b).toNat = a.toNat % b.toNat
theorem USize.toBitVec_eq_of_lt {a : Nat} :
a < USize.size(USize.ofNat a).toBitVec.toNat = a
@[simp]
theorem USize.le_refl (a : USize) :
a a
theorem USize.le_def {a b : USize} :
a b a.toBitVec b.toBitVec
theorem USize.toNat_ofNat_of_lt {n : Nat} (h : n < USize.size) :
(USize.ofNat n).toNat = n
@[simp]
@[simp]
theorem USize.toNat_div (a b : USize) :
(a / b).toNat = a.toNat / b.toNat
theorem USize.le_total (a b : USize) :
a b b a
@[simp]
theorem USize.mk_toBitVec_eq (a : USize) :
{ toBitVec := a.toBitVec } = a
theorem USize.sub_def (a b : USize) :
a - b = { toBitVec := a.toBitVec - b.toBitVec }
@[simp]
theorem USize.lt_irrefl (a : USize) :
¬a < a
@[simp]
theorem USize.not_le {a b : USize} :
¬a b b < a
theorem USize.eq_of_val_eq {a b : USize} (h : a.val = b.val) :
a = b
theorem USize.add_def (a b : USize) :
a + b = { toBitVec := a.toBitVec + b.toBitVec }
theorem USize.eq_of_toBitVec_eq {a b : USize} (h : a.toBitVec = b.toBitVec) :
a = b
@[simp]
@[simp]
theorem USize.not_lt {a b : USize} :
¬a < b b a
theorem USize.lt_asymm {a b : USize} :
a < b¬b < a
theorem USize.le_trans {a b c : USize} :
a bb ca c
theorem USize.ne_of_toBitVec_ne {a b : USize} (h : a.toBitVec b.toBitVec) :
a b
@[deprecated USize.toNat_mod_lt]
theorem USize.modn_lt {m : Nat} (u : USize) :
m > 0(u % m).toNat < m
theorem USize.zero_def :
0 = { toBitVec := 0 }
@[simp]
theorem USize.toNat_mod_lt {m : Nat} (u : USize) :
m > 0(u % USize.ofNat m).toNat < m
theorem USize.lt_trans {a b c : USize} :
a < bb < ca < c
theorem USize.ne_of_lt {a b : USize} (h : a < b) :
a b
@[simp]
theorem USize.val_ofNat (n : Nat) :
theorem USize.mod_def (a b : USize) :
a % b = { toBitVec := a.toBitVec % b.toBitVec }
@[simp]
theorem USize.toNat_sub_of_le (a b : USize) :
b a(a - b).toNat = a.toNat - b.toNat
theorem USize.toNat.inj {a b : USize} :
a.toNat = b.toNata = b
theorem USize.lt_def {a b : USize} :
a < b a.toBitVec < b.toBitVec
theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < UInt32.size) :
n < UInt32.ofNat mn.toNat < m
theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < UInt32.size) :
UInt32.ofNat m < nm < n.toNat
theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < UInt32.size) :
n UInt32.ofNat mn.toNat m
theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < UInt32.size) :
UInt32.ofNat m nm n.toNat
@[reducible, inline, deprecated]
Equations
@[reducible, inline, deprecated]
abbrev UInt8.div_toNat (a b : UInt8) :
(a / b).toNat = a.toNat / b.toNat
Equations
@[reducible, inline, deprecated]
abbrev UInt8.mod_toNat (a b : UInt8) :
(a % b).toNat = a.toNat % b.toNat
Equations
@[reducible, inline, deprecated]
Equations
@[reducible, inline, deprecated]
abbrev UInt16.div_toNat (a b : UInt16) :
(a / b).toNat = a.toNat / b.toNat
Equations
@[reducible, inline, deprecated]
abbrev UInt16.mod_toNat (a b : UInt16) :
(a % b).toNat = a.toNat % b.toNat
Equations
@[reducible, inline, deprecated]
Equations
@[reducible, inline, deprecated]
abbrev UInt32.div_toNat (a b : UInt32) :
(a / b).toNat = a.toNat / b.toNat
Equations
@[reducible, inline, deprecated]
abbrev UInt32.mod_toNat (a b : UInt32) :
(a % b).toNat = a.toNat % b.toNat
Equations
@[reducible, inline, deprecated]
Equations
@[reducible, inline, deprecated]
abbrev UInt64.div_toNat (a b : UInt64) :
(a / b).toNat = a.toNat / b.toNat
Equations
@[reducible, inline, deprecated]
abbrev UInt64.mod_toNat (a b : UInt64) :
(a % b).toNat = a.toNat % b.toNat
Equations
@[reducible, inline, deprecated]
Equations
@[reducible, inline, deprecated]
abbrev USize.div_toNat (a b : USize) :
(a / b).toNat = a.toNat / b.toNat
Equations
@[reducible, inline, deprecated]
abbrev USize.mod_toNat (a b : USize) :
(a % b).toNat = a.toNat % b.toNat
Equations