From 75df4c0b5233e8b68c2f90a3b649f436ca698bf1 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 28 Feb 2025 16:15:58 +0100 Subject: [PATCH] fix: statement of a `UIntX` conversion lemma (#7273) This PR fixes the statement of a `UIntX` conversion lemma. --- src/Init/Data/UInt/Lemmas.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean index 9d235cc707..64aebaf5e4 100644 --- a/src/Init/Data/UInt/Lemmas.lean +++ b/src/Init/Data/UInt/Lemmas.lean @@ -287,6 +287,8 @@ theorem UInt32.size_le_usizeSize : UInt32.size ≤ USize.size := by 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 USize.size_le_uint64Size : USize.size ≤ UInt64.size := by + cases USize.size_eq <;> simp_all +decide 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) @@ -373,7 +375,7 @@ theorem USize.size_dvd_uInt64Size : USize.size ∣ UInt64.size := by cases USize @[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 USize.toFin_toUInt64 (n : USize) : n.toUInt64.toFin = n.toFin.castLE size_le_uint64Size := 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