feat: UIntX conversion lemmas (part 1/n) (#7174)
This PR adds the first batch of lemmas about iterated conversions between finite types starting with something of type `UIntX`.
This commit is contained in:
Markus Himmel
GitHub
parent
3ebce4e190
commit
36723d38b9
7 changed files with 216 additions and 29 deletions
|
|
@ -7,6 +7,7 @@ prelude
|
|||
import Init.Data.SInt.Basic
|
||||
import Init.Data.SInt.Float
|
||||
import Init.Data.SInt.Float32
|
||||
import Init.Data.SInt.Lemmas
|
||||
|
||||
/-!
|
||||
This module contains the definitions and basic theory about signed fixed width integer types.
|
||||
|
|
|
|||
13
src/Init/Data/SInt/Lemmas.lean
Normal file
13
src/Init/Data/SInt/Lemmas.lean
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Markus Himmel
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.SInt.Basic
|
||||
|
||||
@[simp] theorem UInt8.toBitVec_toInt8 (x : UInt8) : x.toInt8.toBitVec = x.toBitVec := rfl
|
||||
@[simp] theorem UInt16.toBitVec_toInt16 (x : UInt16) : x.toInt16.toBitVec = x.toBitVec := rfl
|
||||
@[simp] theorem UInt32.toBitVec_toInt32 (x : UInt32) : x.toInt32.toBitVec = x.toBitVec := rfl
|
||||
@[simp] theorem UInt64.toBitVec_toInt64 (x : UInt64) : x.toInt64.toBitVec = x.toBitVec := rfl
|
||||
@[simp] theorem USize.toBitVec_toISize (x : USize) : x.toISize.toBitVec = x.toBitVec := rfl
|
||||
|
|
@ -295,11 +295,16 @@ def USize.mk (bitVec : BitVec System.Platform.numBits) : USize :=
|
|||
def USize.ofNatCore (n : Nat) (h : n < USize.size) : USize :=
|
||||
USize.ofNatLT n h
|
||||
|
||||
theorem usize_size_le : USize.size ≤ 18446744073709551616 := by
|
||||
cases usize_size_eq <;> next h => rw [h]; decide
|
||||
@[simp] theorem USize.le_size : 2 ^ 32 ≤ USize.size := by cases USize.size_eq <;> simp_all
|
||||
@[simp] theorem USize.size_le : USize.size ≤ 2 ^ 64 := by cases USize.size_eq <;> simp_all
|
||||
|
||||
theorem le_usize_size : 4294967296 ≤ USize.size := by
|
||||
cases usize_size_eq <;> next h => rw [h]; decide
|
||||
@[deprecated USize.size_le (since := "2025-02-24")]
|
||||
theorem usize_size_le : USize.size ≤ 18446744073709551616 :=
|
||||
USize.size_le
|
||||
|
||||
@[deprecated USize.le_size (since := "2025-02-24")]
|
||||
theorem le_usize_size : 4294967296 ≤ USize.size :=
|
||||
USize.le_size
|
||||
|
||||
@[extern "lean_usize_mul"]
|
||||
def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
|
||||
|
|
@ -326,7 +331,7 @@ This function is overridden with a native implementation.
|
|||
-/
|
||||
@[extern "lean_usize_of_nat"]
|
||||
def USize.ofNat32 (n : @& Nat) (h : n < 4294967296) : USize :=
|
||||
USize.ofNatLT n (Nat.lt_of_lt_of_le h le_usize_size)
|
||||
USize.ofNatLT n (Nat.lt_of_lt_of_le h USize.le_size)
|
||||
@[extern "lean_uint8_to_usize"]
|
||||
def UInt8.toUSize (a : UInt8) : USize :=
|
||||
USize.ofNat32 a.toBitVec.toNat (Nat.lt_trans a.toBitVec.isLt (by decide))
|
||||
|
|
@ -351,7 +356,7 @@ This function is overridden with a native implementation.
|
|||
-/
|
||||
@[extern "lean_usize_to_uint64"]
|
||||
def USize.toUInt64 (a : USize) : UInt64 :=
|
||||
UInt64.ofNatLT a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt usize_size_le)
|
||||
UInt64.ofNatLT a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt USize.size_le)
|
||||
|
||||
instance : Mul USize := ⟨USize.mul⟩
|
||||
instance : Mod USize := ⟨USize.mod⟩
|
||||
|
|
|
|||
|
|
@ -138,8 +138,16 @@ def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBit
|
|||
|
||||
instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
|
||||
|
||||
@[deprecated usize_size_pos (since := "2024-11-24")] theorem usize_size_gt_zero : USize.size > 0 :=
|
||||
usize_size_pos
|
||||
@[deprecated USize.size_eq (since := "2025-02-24")]
|
||||
theorem usize_size_eq : USize.size = 4294967296 ∨ USize.size = 18446744073709551616 :=
|
||||
USize.size_eq
|
||||
|
||||
@[deprecated USize.size_pos (since := "2025-02-24")]
|
||||
theorem usize_size_pos : 0 < USize.size :=
|
||||
USize.size_pos
|
||||
|
||||
@[deprecated USize.size_pos (since := "2024-11-24")] theorem usize_size_gt_zero : USize.size > 0 :=
|
||||
USize.size_pos
|
||||
|
||||
/-- Converts a `USize` into the corresponding `Fin USize.size`. -/
|
||||
def USize.toFin (x : USize) : Fin USize.size := x.toBitVec.toFin
|
||||
|
|
@ -155,7 +163,7 @@ def USize.ofNatTruncate (n : Nat) : USize :=
|
|||
if h : n < USize.size then
|
||||
USize.ofNatLT n h
|
||||
else
|
||||
USize.ofNatLT (USize.size - 1) (Nat.pred_lt (Nat.ne_zero_of_lt usize_size_pos))
|
||||
USize.ofNatLT (USize.size - 1) (Nat.pred_lt (Nat.ne_zero_of_lt USize.size_pos))
|
||||
abbrev Nat.toUSize := USize.ofNat
|
||||
@[extern "lean_usize_to_nat"]
|
||||
def USize.toNat (n : USize) : Nat := n.toBitVec.toNat
|
||||
|
|
|
|||
|
|
@ -25,11 +25,11 @@ namespace $typeName
|
|||
@[simp, int_toBitVec] protected theorem toBitVec_shiftLeft (a b : $typeName) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % $bits) := rfl
|
||||
@[simp, int_toBitVec] protected theorem toBitVec_shiftRight (a b : $typeName) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % $bits) := rfl
|
||||
|
||||
@[simp] protected theorem toNat_and (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := by simp [toNat]
|
||||
@[simp] protected theorem toNat_or (a b : $typeName) : (a ||| b).toNat = a.toNat ||| b.toNat := by simp [toNat]
|
||||
@[simp] protected theorem toNat_xor (a b : $typeName) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := by simp [toNat]
|
||||
@[simp] protected theorem toNat_shiftLeft (a b : $typeName) : (a <<< b).toNat = a.toNat <<< (b.toNat % $bits) % 2 ^ $bits := by simp [toNat]
|
||||
@[simp] protected theorem toNat_shiftRight (a b : $typeName) : (a >>> b).toNat = a.toNat >>> (b.toNat % $bits) := by simp [toNat]
|
||||
@[simp] protected theorem toNat_and (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := by simp [toNat, -toNat_toBitVec]
|
||||
@[simp] protected theorem toNat_or (a b : $typeName) : (a ||| b).toNat = a.toNat ||| b.toNat := by simp [toNat, -toNat_toBitVec]
|
||||
@[simp] protected theorem toNat_xor (a b : $typeName) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := by simp [toNat, -toNat_toBitVec]
|
||||
@[simp] protected theorem toNat_shiftLeft (a b : $typeName) : (a <<< b).toNat = a.toNat <<< (b.toNat % $bits) % 2 ^ $bits := by simp [toNat, -toNat_toBitVec]
|
||||
@[simp] protected theorem toNat_shiftRight (a b : $typeName) : (a >>> b).toNat = a.toNat >>> (b.toNat % $bits) := by simp [toNat, -toNat_toBitVec]
|
||||
|
||||
open $typeName (toNat_and) in
|
||||
@[deprecated toNat_and (since := "2024-11-28")]
|
||||
|
|
@ -37,7 +37,6 @@ protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.
|
|||
|
||||
end $typeName
|
||||
)
|
||||
|
||||
declare_bitwise_uint_theorems UInt8 8
|
||||
declare_bitwise_uint_theorems UInt16 16
|
||||
declare_bitwise_uint_theorems UInt32 32
|
||||
|
|
|
|||
|
|
@ -34,15 +34,23 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
|
|||
@[deprecated toNat_ofNatLT (since := "2025-02-13")]
|
||||
theorem toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n := BitVec.toNat_ofNatLT ..
|
||||
|
||||
@[simp] theorem toFin_val_eq_toNat (x : $typeName) : x.toFin.val = x.toNat := rfl
|
||||
@[deprecated toFin_val_eq_toNat (since := "2025-02-12")]
|
||||
@[simp] theorem toFin_val (x : $typeName) : x.toFin.val = x.toNat := rfl
|
||||
@[deprecated toFin_val (since := "2025-02-12")]
|
||||
theorem val_val_eq_toNat (x : $typeName) : x.toFin.val = x.toNat := rfl
|
||||
|
||||
@[simp] theorem toNat_toBitVec (x : $typeName) : x.toBitVec.toNat = x.toNat := rfl
|
||||
@[simp] theorem toFin_toBitVec (x : $typeName) : x.toBitVec.toFin = x.toFin := rfl
|
||||
|
||||
@[deprecated toNat_toBitVec (since := "2025-02-21")]
|
||||
theorem toNat_toBitVec_eq_toNat (x : $typeName) : x.toBitVec.toNat = x.toNat := rfl
|
||||
|
||||
@[simp] theorem ofBitVec_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a
|
||||
@[simp] theorem ofBitVec_toBitVec : ∀ (a : $typeName), ofBitVec a.toBitVec = a
|
||||
| ⟨_, _⟩ => rfl
|
||||
|
||||
@[deprecated ofBitVec_toBitVec (since := "2025-02-21")]
|
||||
theorem ofBitVec_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a :=
|
||||
ofBitVec_toBitVec
|
||||
|
||||
@[deprecated ofBitVec_toBitVec_eq (since := "2025-02-12")]
|
||||
theorem mk_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a
|
||||
| ⟨_, _⟩ => rfl
|
||||
|
|
@ -241,21 +249,174 @@ declare_uint_theorems USize System.Platform.numBits
|
|||
|
||||
@[simp] theorem USize.toNat_ofNat32 {n : Nat} {h : n < 4294967296} : (ofNat32 n h).toNat = n := rfl
|
||||
|
||||
@[simp] theorem USize.toNat_toUInt32 (x : USize) : x.toUInt32.toNat = x.toNat % 2 ^ 32 := rfl
|
||||
|
||||
@[simp] theorem USize.toNat_toUInt8 (x : USize) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
|
||||
@[simp] theorem USize.toNat_toUInt16 (x : USize) : x.toUInt16.toNat = x.toNat % 2 ^ 16 := rfl
|
||||
@[simp] theorem USize.toNat_toUInt32 (x : USize) : x.toUInt32.toNat = x.toNat % 2 ^ 32 := rfl
|
||||
@[simp] theorem USize.toNat_toUInt64 (x : USize) : x.toUInt64.toNat = x.toNat := rfl
|
||||
|
||||
theorem USize.toNat_ofNat_of_lt_32 {n : Nat} (h : n < 4294967296) : toNat (ofNat n) = n :=
|
||||
toNat_ofNat_of_lt (Nat.lt_of_lt_of_le h le_usize_size)
|
||||
toNat_ofNat_of_lt (Nat.lt_of_lt_of_le h USize.le_size)
|
||||
|
||||
theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := by
|
||||
simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
simp [-toNat_toBitVec, lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
|
||||
theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat := by
|
||||
simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
simp [-toNat_toBitVec, lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
|
||||
theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m := by
|
||||
simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
simp [-toNat_toBitVec, le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
|
||||
theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by
|
||||
simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
simp [-toNat_toBitVec, le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
|
||||
@[simp] theorem UInt8.toNat_lt (n : UInt8) : n.toNat < 2 ^ 8 := n.toFin.isLt
|
||||
@[simp] theorem UInt16.toNat_lt (n : UInt16) : n.toNat < 2 ^ 16 := n.toFin.isLt
|
||||
@[simp] theorem UInt32.toNat_lt (n : UInt32) : n.toNat < 2 ^ 32 := n.toFin.isLt
|
||||
@[simp] theorem UInt64.toNat_lt (n : UInt64) : n.toNat < 2 ^ 64 := n.toFin.isLt
|
||||
|
||||
theorem UInt8.size_lt_usizeSize : UInt8.size < USize.size := by
|
||||
cases USize.size_eq <;> simp_all +decide
|
||||
theorem UInt8.size_le_usizeSize : UInt8.size ≤ USize.size :=
|
||||
Nat.le_of_lt UInt8.size_lt_usizeSize
|
||||
theorem UInt16.size_lt_usizeSize : UInt16.size < USize.size := by
|
||||
cases USize.size_eq <;> simp_all +decide
|
||||
theorem UInt16.size_le_usizeSize : UInt16.size ≤ USize.size :=
|
||||
Nat.le_of_lt UInt16.size_lt_usizeSize
|
||||
theorem UInt32.size_le_usizeSize : UInt32.size ≤ USize.size := by
|
||||
cases USize.size_eq <;> simp_all +decide
|
||||
theorem USize.size_eq_two_pow : USize.size = 2 ^ System.Platform.numBits := rfl
|
||||
theorem USize.toNat_lt_two_pow_numBits (n : USize) : n.toNat < 2 ^ System.Platform.numBits := n.toFin.isLt
|
||||
@[simp] theorem USize.toNat_lt (n : USize) : n.toNat < 2 ^ 64 := Nat.lt_of_lt_of_le n.toFin.isLt size_le
|
||||
|
||||
theorem UInt8.toNat_lt_usizeSize (n : UInt8) : n.toNat < USize.size :=
|
||||
Nat.lt_of_lt_of_le n.toNat_lt (by cases USize.size_eq <;> simp_all)
|
||||
theorem UInt16.toNat_lt_usizeSize (n : UInt16) : n.toNat < USize.size :=
|
||||
Nat.lt_of_lt_of_le n.toNat_lt (by cases USize.size_eq <;> simp_all)
|
||||
theorem UInt32.toNat_lt_usizeSize (n : UInt32) : n.toNat < USize.size :=
|
||||
Nat.lt_of_lt_of_le n.toNat_lt (by cases USize.size_eq <;> simp_all)
|
||||
|
||||
@[simp] theorem Fin.mk_uInt8ToNat (n : UInt8) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
|
||||
@[simp] theorem Fin.mk_uInt16ToNat (n : UInt16) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
|
||||
@[simp] theorem Fin.mk_uInt32ToNat (n : UInt32) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
|
||||
@[simp] theorem Fin.mk_uInt64ToNat (n : UInt64) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
|
||||
@[simp] theorem Fin.mk_uSizeToNat (n : USize) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
|
||||
|
||||
@[simp] theorem BitVec.ofNatLT_uInt8ToNat (n : UInt8) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
|
||||
@[simp] theorem BitVec.ofNatLT_uInt16ToNat (n : UInt16) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
|
||||
@[simp] theorem BitVec.ofNatLT_uInt32ToNat (n : UInt32) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
|
||||
@[simp] theorem BitVec.ofNatLT_uInt64ToNat (n : UInt64) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
|
||||
@[simp] theorem BitVec.ofNatLT_uSizeToNat (n : USize) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
|
||||
|
||||
@[simp] theorem BitVec.ofFin_uInt8ToFin (n : UInt8) : BitVec.ofFin n.toFin = n.toBitVec := rfl
|
||||
@[simp] theorem BitVec.ofFin_uInt16ToFin (n : UInt16) : BitVec.ofFin n.toFin = n.toBitVec := rfl
|
||||
@[simp] theorem BitVec.ofFin_uInt32ToFin (n : UInt32) : BitVec.ofFin n.toFin = n.toBitVec := rfl
|
||||
@[simp] theorem BitVec.ofFin_uInt64ToFin (n : UInt64) : BitVec.ofFin n.toFin = n.toBitVec := rfl
|
||||
@[simp] theorem BitVec.ofFin_uSizeToFin (n : USize) : BitVec.ofFin n.toFin = n.toBitVec := rfl
|
||||
|
||||
@[simp] theorem UInt8.toFin_toUInt16 (n : UInt8) : n.toUInt16.toFin = n.toFin.castLE (by decide) := rfl
|
||||
@[simp] theorem UInt8.toFin_toUInt32 (n : UInt8) : n.toUInt32.toFin = n.toFin.castLE (by decide) := rfl
|
||||
@[simp] theorem UInt8.toFin_toUInt64 (n : UInt8) : n.toUInt64.toFin = n.toFin.castLE (by decide) := rfl
|
||||
@[simp] theorem UInt8.toFin_toUSize (n : UInt8) :
|
||||
n.toUSize.toFin = n.toFin.castLE size_le_usizeSize := rfl
|
||||
|
||||
@[simp] theorem UInt16.toFin_toUInt32 (n : UInt16) : n.toUInt32.toFin = n.toFin.castLE (by decide) := rfl
|
||||
@[simp] theorem UInt16.toFin_toUInt64 (n : UInt16) : n.toUInt64.toFin = n.toFin.castLE (by decide) := rfl
|
||||
@[simp] theorem UInt16.toFin_toUSize (n : UInt16) :
|
||||
n.toUSize.toFin = n.toFin.castLE size_le_usizeSize := rfl
|
||||
|
||||
@[simp] theorem UInt32.toFin_toUInt64 (n : UInt32) : n.toUInt64.toFin = n.toFin.castLE (by decide) := rfl
|
||||
@[simp] theorem UInt32.toFin_toUSize (n : UInt32) :
|
||||
n.toUSize.toFin = n.toFin.castLE size_le_usizeSize := rfl
|
||||
|
||||
@[simp] theorem USize.toFin_toUInt64 (n : USize) : n.toUInt64.toFin = n.toFin.castLE size_le_usizeSize := rfl
|
||||
|
||||
@[simp] theorem UInt16.toBitVec_toUInt8 (n : UInt16) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := rfl
|
||||
@[simp] theorem UInt32.toBitVec_toUInt8 (n : UInt32) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := rfl
|
||||
@[simp] theorem UInt64.toBitVec_toUInt8 (n : UInt64) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := rfl
|
||||
@[simp] theorem USize.toBitVec_toUInt8 (n : USize) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := BitVec.eq_of_toNat_eq (by simp)
|
||||
|
||||
@[simp] theorem UInt8.toBitVec_toUInt16 (n : UInt8) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := rfl
|
||||
@[simp] theorem UInt32.toBitVec_toUInt16 (n : UInt32) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := rfl
|
||||
@[simp] theorem UInt64.toBitVec_toUInt16 (n : UInt64) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := rfl
|
||||
@[simp] theorem USize.toBitVec_toUInt16 (n : USize) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := BitVec.eq_of_toNat_eq (by simp)
|
||||
|
||||
@[simp] theorem UInt8.toBitVec_toUInt32 (n : UInt8) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := rfl
|
||||
@[simp] theorem UInt16.toBitVec_toUInt32 (n : UInt16) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := rfl
|
||||
@[simp] theorem UInt64.toBitVec_toUInt32 (n : UInt64) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := rfl
|
||||
@[simp] theorem USize.toBitVec_toUInt32 (n : USize) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := BitVec.eq_of_toNat_eq (by simp)
|
||||
|
||||
@[simp] theorem UInt8.toBitVec_toUInt64 (n : UInt8) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 := rfl
|
||||
@[simp] theorem UInt16.toBitVec_toUInt64 (n : UInt16) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 := rfl
|
||||
@[simp] theorem UInt32.toBitVec_toUInt64 (n : UInt32) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 := rfl
|
||||
@[simp] theorem USize.toBitVec_toUInt64 (n : USize) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 :=
|
||||
BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt (USize.toNat_lt _)])
|
||||
|
||||
@[simp] theorem UInt8.toBitVec_toUSize (n : UInt8) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
|
||||
BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
|
||||
@[simp] theorem UInt16.toBitVec_toUSize (n : UInt16) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
|
||||
BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
|
||||
@[simp] theorem UInt32.toBitVec_toUSize (n : UInt32) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
|
||||
BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
|
||||
@[simp] theorem UInt64.toBitVec_toUSize (n : UInt64) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
|
||||
BitVec.eq_of_toNat_eq (by simp)
|
||||
|
||||
@[simp] theorem UInt8.ofNatLT_toNat (n : UInt8) : UInt8.ofNatLT n.toNat n.toNat_lt = n := rfl
|
||||
@[simp] theorem UInt16.ofNatLT_uInt8ToNat (n : UInt8) : UInt16.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt16 := rfl
|
||||
@[simp] theorem UInt32.ofNatLT_uInt8ToNat (n : UInt8) : UInt32.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt32 := rfl
|
||||
@[simp] theorem UInt64.ofNatLT_uInt8ToNat (n : UInt8) : UInt64.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt64 := rfl
|
||||
@[simp] theorem USize.ofNatLT_uInt8ToNat (n : UInt8) : USize.ofNatLT n.toNat n.toNat_lt_usizeSize = n.toUSize := rfl
|
||||
|
||||
@[simp] theorem UInt16.ofNatLT_toNat (n : UInt16) : UInt16.ofNatLT n.toNat n.toNat_lt = n := rfl
|
||||
@[simp] theorem UInt32.ofNatLT_uInt16ToNat (n : UInt16) : UInt32.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt32 := rfl
|
||||
@[simp] theorem UInt64.ofNatLT_uInt16ToNat (n : UInt16) : UInt64.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt64 := rfl
|
||||
@[simp] theorem USize.ofNatLT_uInt16ToNat (n : UInt16) : USize.ofNatLT n.toNat n.toNat_lt_usizeSize = n.toUSize := rfl
|
||||
|
||||
@[simp] theorem UInt32.ofNatLT_toNat (n : UInt32) : UInt32.ofNatLT n.toNat n.toNat_lt = n := rfl
|
||||
@[simp] theorem UInt64.ofNatLT_uInt32ToNat (n : UInt32) : UInt64.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt64 := rfl
|
||||
@[simp] theorem USize.ofNatLT_uInt32ToNat (n : UInt32) : USize.ofNatLT n.toNat n.toNat_lt_usizeSize = n.toUSize := rfl
|
||||
|
||||
@[simp] theorem UInt64.ofNatLT_toNat (n : UInt64) : UInt64.ofNatLT n.toNat n.toNat_lt = n := rfl
|
||||
|
||||
@[simp] theorem USize.ofNatLT_toNat (n : USize) : USize.ofNatLT n.toNat n.toNat_lt_size = n := rfl
|
||||
@[simp] theorem UInt64.ofNatLT_uSizeToNat (n : USize) : UInt64.ofNatLT n.toNat n.toNat_lt = n.toUInt64 := rfl
|
||||
|
||||
-- We are not making these into `simp` lemmas because they lose the information stored in `h`. ·
|
||||
theorem UInt8.ofNatLT_uInt16ToNat (n : UInt16) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
|
||||
UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
|
||||
theorem UInt8.ofNatLT_uInt32ToNat (n : UInt32) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
|
||||
UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
|
||||
theorem UInt8.ofNatLT_uInt64ToNat (n : UInt64) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
|
||||
UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
|
||||
theorem UInt8.ofNatLT_uSizeToNat (n : USize) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
|
||||
UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
|
||||
theorem UInt16.ofNatLT_uInt32ToNat (n : UInt32) (h) : UInt16.ofNatLT n.toNat h = n.toUInt16 :=
|
||||
UInt16.toNat.inj (by simp [Nat.mod_eq_of_lt h])
|
||||
theorem UInt16.ofNatLT_uInt64ToNat (n : UInt64) (h) : UInt16.ofNatLT n.toNat h = n.toUInt16 :=
|
||||
UInt16.toNat.inj (by simp [Nat.mod_eq_of_lt h])
|
||||
theorem UInt16.ofNatLT_uSizeToNat (n : USize) (h) : UInt16.ofNatLT n.toNat h = n.toUInt16 :=
|
||||
UInt16.toNat.inj (by simp [Nat.mod_eq_of_lt h])
|
||||
theorem UInt32.ofNatLT_uInt64ToNat (n : UInt64) (h) : UInt32.ofNatLT n.toNat h = n.toUInt32 :=
|
||||
UInt32.toNat.inj (by simp [Nat.mod_eq_of_lt h])
|
||||
theorem UInt32.ofNatLT_uSizeToNat (n : USize) (h) : UInt32.ofNatLT n.toNat h = n.toUInt32 :=
|
||||
UInt32.toNat.inj (by simp [Nat.mod_eq_of_lt h])
|
||||
theorem USize.ofNatLT_uInt64ToNat (n : UInt64) (h) : USize.ofNatLT n.toNat h = n.toUSize :=
|
||||
USize.toNat.inj (by simp [Nat.mod_eq_of_lt h])
|
||||
|
||||
@[simp] theorem UInt8.ofFin_toFin (n : UInt8) : UInt8.ofFin n.toFin = n := rfl
|
||||
@[simp] theorem UInt16.ofFin_toFin (n : UInt16) : UInt16.ofFin n.toFin = n := rfl
|
||||
@[simp] theorem UInt32.ofFin_toFin (n : UInt32) : UInt32.ofFin n.toFin = n := rfl
|
||||
@[simp] theorem UInt64.ofFin_toFin (n : UInt64) : UInt64.ofFin n.toFin = n := rfl
|
||||
@[simp] theorem USize.ofFin_toFin (n : USize) : USize.ofFin n.toFin = n := rfl
|
||||
|
||||
@[simp] theorem UInt16.ofFin_uint8ToFin (n : UInt8) : UInt16.ofFin (n.toFin.castLE (by decide)) = n.toUInt16 := rfl
|
||||
|
||||
@[simp] theorem UInt32.ofFin_uint8ToFin (n : UInt8) : UInt32.ofFin (n.toFin.castLE (by decide)) = n.toUInt32 := rfl
|
||||
@[simp] theorem UInt32.ofFin_uint16ToFin (n : UInt16) : UInt32.ofFin (n.toFin.castLE (by decide)) = n.toUInt32 := rfl
|
||||
|
||||
@[simp] theorem UInt64.ofFin_uint8ToFin (n : UInt8) : UInt64.ofFin (n.toFin.castLE (by decide)) = n.toUInt64 := rfl
|
||||
@[simp] theorem UInt64.ofFin_uint16ToFin (n : UInt16) : UInt64.ofFin (n.toFin.castLE (by decide)) = n.toUInt64 := rfl
|
||||
@[simp] theorem UInt64.ofFin_uint32ToFin (n : UInt32) : UInt64.ofFin (n.toFin.castLE (by decide)) = n.toUInt64 := rfl
|
||||
|
||||
@[simp] theorem USize.ofFin_uint8ToFin (n : UInt8) : USize.ofFin (n.toFin.castLE UInt8.size_le_usizeSize) = n.toUSize := rfl
|
||||
@[simp] theorem USize.ofFin_uint16ToFin (n : UInt16) : USize.ofFin (n.toFin.castLE UInt16.size_le_usizeSize) = n.toUSize := rfl
|
||||
@[simp] theorem USize.ofFin_uint32ToFin (n : UInt32) : USize.ofFin (n.toFin.castLE UInt32.size_le_usizeSize) = n.toUSize := rfl
|
||||
|
|
|
|||
|
|
@ -2150,14 +2150,14 @@ instance : Inhabited UInt64 where
|
|||
/-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/
|
||||
abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
|
||||
|
||||
theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
|
||||
theorem USize.size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
|
||||
show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
|
||||
match System.Platform.numBits, System.Platform.numBits_eq with
|
||||
| _, Or.inl rfl => Or.inl (of_decide_eq_true rfl)
|
||||
| _, Or.inr rfl => Or.inr (of_decide_eq_true rfl)
|
||||
|
||||
theorem usize_size_pos : LT.lt 0 USize.size :=
|
||||
match USize.size, usize_size_eq with
|
||||
theorem USize.size_pos : LT.lt 0 USize.size :=
|
||||
match USize.size, USize.size_eq with
|
||||
| _, Or.inl rfl => of_decide_eq_true rfl
|
||||
| _, Or.inr rfl => of_decide_eq_true rfl
|
||||
|
||||
|
|
@ -2207,7 +2207,7 @@ def USize.decEq (a b : USize) : Decidable (Eq a b) :=
|
|||
instance : DecidableEq USize := USize.decEq
|
||||
|
||||
instance : Inhabited USize where
|
||||
default := USize.ofNatLT 0 usize_size_pos
|
||||
default := USize.ofNatLT 0 USize.size_pos
|
||||
|
||||
/--
|
||||
A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue