From caa0eacea8a23a10fafbb42e8ce9b8fd1879ff3f Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 12 Sep 2025 09:52:45 +0200 Subject: [PATCH] feat: ranges in `UInt*` (#10303) This PR adds range support to`BitVec` and the `UInt*` types. This means that it is now possible to write, for example, `for i in (1 : UInt8)...5 do`, in order to loop over the values 1, 2, 3 and 4 of type `UInt8`. --- src/Init/Data/Range/Polymorphic.lean | 2 + src/Init/Data/Range/Polymorphic/BitVec.lean | 88 ++++ src/Init/Data/Range/Polymorphic/Int.lean | 11 +- src/Init/Data/Range/Polymorphic/Nat.lean | 9 +- src/Init/Data/Range/Polymorphic/UInt.lean | 382 ++++++++++++++++++ .../Range/Polymorphic/UpwardEnumerable.lean | 6 +- src/Init/Data/UInt/Lemmas.lean | 7 + tests/lean/run/rangePolymorphic.lean | 32 +- 8 files changed, 525 insertions(+), 12 deletions(-) create mode 100644 src/Init/Data/Range/Polymorphic/BitVec.lean create mode 100644 src/Init/Data/Range/Polymorphic/UInt.lean diff --git a/src/Init/Data/Range/Polymorphic.lean b/src/Init/Data/Range/Polymorphic.lean index c90630d9e9..975dea87b2 100644 --- a/src/Init/Data/Range/Polymorphic.lean +++ b/src/Init/Data/Range/Polymorphic.lean @@ -12,6 +12,8 @@ public import Init.Data.Range.Polymorphic.Stream public import Init.Data.Range.Polymorphic.Lemmas public import Init.Data.Range.Polymorphic.Nat public import Init.Data.Range.Polymorphic.Int +public import Init.Data.Range.Polymorphic.BitVec +public import Init.Data.Range.Polymorphic.UInt public import Init.Data.Range.Polymorphic.NatLemmas public import Init.Data.Range.Polymorphic.GetElemTactic diff --git a/src/Init/Data/Range/Polymorphic/BitVec.lean b/src/Init/Data/Range/Polymorphic/BitVec.lean new file mode 100644 index 0000000000..34e42bb0d9 --- /dev/null +++ b/src/Init/Data/Range/Polymorphic/BitVec.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Init.Data.Range.Polymorphic.Instances +public import Init.Data.Order.Lemmas +public import Init.Data.UInt +import Init.Omega + +public section + +open Std Std.PRange + +namespace BitVec + +variable {n : Nat} + +instance : UpwardEnumerable (BitVec n) where + succ? i := if i + 1 = 0 then none else some (i + 1) + succMany? m i := if h : i.toNat + m < 2 ^ n then some (.ofNatLT _ h) else none + +instance : LawfulUpwardEnumerable (BitVec n) where + ne_of_lt := by + simp +contextual [UpwardEnumerable.LT, ← BitVec.toNat_inj, succMany?] at ⊢ + omega + succMany?_zero := by simp [UpwardEnumerable.succMany?, BitVec.toNat_lt_twoPow_of_le] + succMany?_succ? a b := by + simp +contextual [← BitVec.toNat_inj, succMany?, succ?] + split <;> split + · rename_i h + simp [← BitVec.toNat_inj, Nat.mod_eq_of_lt (a := b.toNat + a + 1) ‹_›] + all_goals omega + · omega + · have : b.toNat + a + 1 = 2 ^ n := by omega + simp [this] + · simp + +instance : LawfulUpwardEnumerableLE (BitVec n) where + le_iff x y := by + simp [UpwardEnumerable.LE, UpwardEnumerable.succMany?, BitVec.le_def] + apply Iff.intro + · intro hle + refine ⟨y.toNat - x.toNat, ?_⟩ + apply Exists.intro <;> simp [Nat.add_sub_cancel' hle, BitVec.toNat_lt_twoPow_of_le] + · rintro ⟨n, hn, rfl⟩ + simp [BitVec.ofNatLT] + +instance : LawfulOrderLT (BitVec n) := inferInstance +instance : LawfulUpwardEnumerableLT (BitVec n) := inferInstance +instance : LawfulUpwardEnumerableLT (BitVec n) := inferInstance +instance : LawfulUpwardEnumerableLowerBound .closed (BitVec n) := inferInstance +instance : LawfulUpwardEnumerableUpperBound .closed (BitVec n) := inferInstance +instance : LawfulUpwardEnumerableLowerBound .open (BitVec n) := inferInstance +instance : LawfulUpwardEnumerableUpperBound .open (BitVec n) := inferInstance + +instance : RangeSize .closed (BitVec n) where + size bound a := bound.toNat + 1 - a.toNat + +instance : RangeSize .open (BitVec n) := RangeSize.openOfClosed + +instance : LawfulRangeSize .closed (BitVec n) where + size_eq_zero_of_not_isSatisfied bound x := by + simp [SupportsUpperBound.IsSatisfied, BitVec.not_le, RangeSize.size, BitVec.lt_def] + omega + size_eq_one_of_succ?_eq_none bound x := by + have := BitVec.toNat_lt_twoPow_of_le (Nat.le_refl _) (x := bound) + have (h : (x.toNat + 1) % 2 ^ n = 0) : x.toNat = 2 ^ n - 1 := by + apply Classical.not_not.mp + intro _ + simp [Nat.mod_eq_of_lt (a := x.toNat + 1) (b := 2 ^ n) (by omega)] at h + simp [RangeSize.size, BitVec.le_def, ← BitVec.toNat_inj, succ?] + omega + size_eq_succ_of_succ?_eq_some bound init x := by + have (h : ¬ (init.toNat + 1) % 2 ^ n = 0) : ¬ (init.toNat + 1 ≥ 2 ^ n) := by + intro _ + have : init.toNat + 1 = 2 ^ n := by omega + simp_all + simp_all +contextual [RangeSize.size, BitVec.le_def, ← BitVec.toNat_inj, + Nat.mod_eq_of_lt (a := init.toNat + 1) (b := 2 ^ n), succ?] + omega + +instance : LawfulRangeSize .open (BitVec n) := inferInstance + +end BitVec diff --git a/src/Init/Data/Range/Polymorphic/Int.lean b/src/Init/Data/Range/Polymorphic/Int.lean index 849e1418f4..d79aed472c 100644 --- a/src/Init/Data/Range/Polymorphic/Int.lean +++ b/src/Init/Data/Range/Polymorphic/Int.lean @@ -8,6 +8,7 @@ module prelude public import Init.Data.Range.Polymorphic.Instances public import Init.Data.Order.Classes +public import Init.Data.Int.Order import Init.Omega public section @@ -23,7 +24,7 @@ instance : LawfulUpwardEnumerable Int where simp only [UpwardEnumerable.LT, UpwardEnumerable.succMany?, Option.some.injEq] omega succMany?_zero := by simp [UpwardEnumerable.succMany?] - succMany?_succ := by + succMany?_succ? := by simp only [UpwardEnumerable.succMany?, UpwardEnumerable.succ?, Option.bind_some, Option.some.injEq] omega @@ -36,6 +37,14 @@ instance : LawfulUpwardEnumerableLE Int where simp [UpwardEnumerable.LE, UpwardEnumerable.succMany?, Int.le_def, Int.nonneg_def, Int.sub_eq_iff_eq_add', eq_comm (a := y)] +instance : LawfulOrderLT Int := inferInstance +instance : LawfulUpwardEnumerableLT Int := inferInstance +instance : LawfulUpwardEnumerableLT Int := inferInstance +instance : LawfulUpwardEnumerableLowerBound .closed Int := inferInstance +instance : LawfulUpwardEnumerableUpperBound .closed Int := inferInstance +instance : LawfulUpwardEnumerableLowerBound .open Int := inferInstance +instance : LawfulUpwardEnumerableUpperBound .open Int := inferInstance + instance : RangeSize .closed Int where size bound a := (bound + 1 - a).toNat diff --git a/src/Init/Data/Range/Polymorphic/Nat.lean b/src/Init/Data/Range/Polymorphic/Nat.lean index 5e48fa3e60..adaab7d13a 100644 --- a/src/Init/Data/Range/Polymorphic/Nat.lean +++ b/src/Init/Data/Range/Polymorphic/Nat.lean @@ -10,10 +10,12 @@ import Init.Data.Nat.Lemmas public import Init.Data.Nat.Order public import Init.Data.Range.Polymorphic.Instances public import Init.Data.Order.Classes -import Init.Data.Order.Lemmas +public import Init.Data.Order.Lemmas public section +open Std PRange + namespace Std.PRange instance : UpwardEnumerable Nat where @@ -39,7 +41,7 @@ instance : LawfulUpwardEnumerableLE Nat where instance : LawfulUpwardEnumerable Nat where succMany?_zero := by simp [UpwardEnumerable.succMany?] - succMany?_succ := by simp [UpwardEnumerable.succMany?, UpwardEnumerable.succ?, Nat.add_assoc] + succMany?_succ? := by simp [UpwardEnumerable.succMany?, UpwardEnumerable.succ?, Nat.add_assoc] ne_of_lt a b hlt := by have hn := hlt.choose_spec simp only [UpwardEnumerable.succMany?, Option.some.injEq] at hn @@ -76,8 +78,7 @@ instance : LawfulRangeSize .closed Nat where instance : LawfulRangeSize .open Nat := inferInstance instance : HasFiniteRanges .closed Nat := inferInstance instance : HasFiniteRanges .open Nat := inferInstance -instance : LinearlyUpwardEnumerable Nat := by - exact instLinearlyUpwardEnumerableOfTotalLeOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLE +instance : LinearlyUpwardEnumerable Nat := inferInstance /-! The following instances are used for the implementation of array slices a.k.a. `Subarray`. diff --git a/src/Init/Data/Range/Polymorphic/UInt.lean b/src/Init/Data/Range/Polymorphic/UInt.lean new file mode 100644 index 0000000000..23b3c7b8b9 --- /dev/null +++ b/src/Init/Data/Range/Polymorphic/UInt.lean @@ -0,0 +1,382 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Init.Data.Range.Polymorphic.Instances +public import Init.Data.Order.Lemmas +public import Init.Data.UInt +import Init.Omega +public import Init.Data.Range.Polymorphic.BitVec + +public section + +open Std Std.PRange + +namespace UInt8 + +instance : UpwardEnumerable UInt8 where + succ? i := if i + 1 = 0 then none else some (i + 1) + succMany? n i := if h : i.toNat + n < UInt8.size then some (.ofNatLT _ h) else none + +theorem succ?_ofBitVec {x : BitVec 8} : + UpwardEnumerable.succ? (UInt8.ofBitVec x) = UInt8.ofBitVec <$> UpwardEnumerable.succ? x := by + simp only [succ?, BitVec.ofNat_eq_ofNat, Option.map_eq_map, ← UInt8.toBitVec_inj] + split <;> simp_all + +theorem succMany?_ofBitVec {k : Nat} {x : BitVec 8} : + UpwardEnumerable.succMany? k (UInt8.ofBitVec x) = UInt8.ofBitVec <$> UpwardEnumerable.succMany? k x := by + simp [succMany?] + +theorem upwardEnumerableLE_ofBitVec {x y : BitVec 8} : + UpwardEnumerable.LE (UInt8.ofBitVec x) (UInt8.ofBitVec y) ↔ UpwardEnumerable.LE x y := by + simp [UpwardEnumerable.LE, succMany?_ofBitVec] + +theorem upwardEnumerableLT_ofBitVec {x y : BitVec 8} : + UpwardEnumerable.LT (UInt8.ofBitVec x) (UInt8.ofBitVec y) ↔ UpwardEnumerable.LT x y := by + simp [UpwardEnumerable.LT, succMany?_ofBitVec] + +instance : LawfulUpwardEnumerable UInt8 where + ne_of_lt x y := by + cases x; cases y + simpa [upwardEnumerableLT_ofBitVec] using LawfulUpwardEnumerable.ne_of_lt _ _ + succMany?_zero x := by + cases x + simpa [succMany?_ofBitVec] using succMany?_zero + succMany?_succ? n x := by + cases x + simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def, + succ?_ofBitVec] + +instance : LawfulUpwardEnumerableLE UInt8 where + le_iff x y := by + cases x; cases y + simpa [upwardEnumerableLE_ofBitVec, UInt8.le_iff_toBitVec_le] using + LawfulUpwardEnumerableLE.le_iff _ _ + +instance : LawfulOrderLT UInt8 := inferInstance +instance : LawfulUpwardEnumerableLT UInt8 := inferInstance +instance : LawfulUpwardEnumerableLT UInt8 := inferInstance +instance : LawfulUpwardEnumerableLowerBound .closed UInt8 := inferInstance +instance : LawfulUpwardEnumerableUpperBound .closed UInt8 := inferInstance +instance : LawfulUpwardEnumerableLowerBound .open UInt8 := inferInstance +instance : LawfulUpwardEnumerableUpperBound .open UInt8 := inferInstance + +instance : RangeSize .closed UInt8 where + size bound a := bound.toNat + 1 - a.toNat + +theorem rangeSizeSize_eq_toBitVec {bound : Bound .closed UInt8} {x : BitVec 8} : + RangeSize.size bound (UInt8.ofBitVec x) = RangeSize.size (shape := .closed) bound.toBitVec x := by + simp [RangeSize.size] + +instance : LawfulRangeSize .closed UInt8 where + size_eq_zero_of_not_isSatisfied bound x := by + simpa [rangeSizeSize_eq_toBitVec, UInt8.lt_iff_toBitVec_lt] using + LawfulRangeSize.size_eq_zero_of_not_isSatisfied (su := .closed) (α := BitVec 8) _ _ + size_eq_one_of_succ?_eq_none bound x := by + cases x + simpa [rangeSizeSize_eq_toBitVec, UInt8.le_iff_toBitVec_le, succ?_ofBitVec] using + LawfulRangeSize.size_eq_one_of_succ?_eq_none (su := .closed) (α := BitVec 8) _ _ + size_eq_succ_of_succ?_eq_some bound init x := by + simpa [rangeSizeSize_eq_toBitVec, UInt8.le_iff_toBitVec_le, ← UInt8.toBitVec_inj, succ?] using + LawfulRangeSize.size_eq_succ_of_succ?_eq_some (su := .closed) (α := BitVec 8) _ _ _ + +instance : RangeSize .open UInt8 := RangeSize.openOfClosed +instance : LawfulRangeSize .open UInt8 := inferInstance + +end UInt8 + +namespace UInt16 + +instance : UpwardEnumerable UInt16 where + succ? i := if i + 1 = 0 then none else some (i + 1) + succMany? n i := if h : i.toNat + n < UInt16.size then some (.ofNatLT _ h) else none + +theorem succ?_ofBitVec {x : BitVec 16} : + UpwardEnumerable.succ? (UInt16.ofBitVec x) = UInt16.ofBitVec <$> UpwardEnumerable.succ? x := by + simp only [succ?, BitVec.ofNat_eq_ofNat, Option.map_eq_map, ← UInt16.toBitVec_inj] + split <;> simp_all + +theorem succMany?_ofBitVec {k : Nat} {x : BitVec 16} : + UpwardEnumerable.succMany? k (UInt16.ofBitVec x) = UInt16.ofBitVec <$> UpwardEnumerable.succMany? k x := by + simp [succMany?] + +theorem upwardEnumerableLE_ofBitVec {x y : BitVec 16} : + UpwardEnumerable.LE (UInt16.ofBitVec x) (UInt16.ofBitVec y) ↔ UpwardEnumerable.LE x y := by + simp [UpwardEnumerable.LE, succMany?_ofBitVec] + +theorem upwardEnumerableLT_ofBitVec {x y : BitVec 16} : + UpwardEnumerable.LT (UInt16.ofBitVec x) (UInt16.ofBitVec y) ↔ UpwardEnumerable.LT x y := by + simp [UpwardEnumerable.LT, succMany?_ofBitVec] + +instance : LawfulUpwardEnumerable UInt16 where + ne_of_lt x y := by + cases x; cases y + simpa [upwardEnumerableLT_ofBitVec] using LawfulUpwardEnumerable.ne_of_lt _ _ + succMany?_zero x := by + cases x + simpa [succMany?_ofBitVec] using succMany?_zero + succMany?_succ? n x := by + cases x + simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def, + succ?_ofBitVec] + +instance : LawfulUpwardEnumerableLE UInt16 where + le_iff x y := by + cases x; cases y + simpa [upwardEnumerableLE_ofBitVec, UInt16.le_iff_toBitVec_le] using + LawfulUpwardEnumerableLE.le_iff _ _ + +instance : LawfulOrderLT UInt16 := inferInstance +instance : LawfulUpwardEnumerableLT UInt16 := inferInstance +instance : LawfulUpwardEnumerableLT UInt16 := inferInstance +instance : LawfulUpwardEnumerableLowerBound .closed UInt16 := inferInstance +instance : LawfulUpwardEnumerableUpperBound .closed UInt16 := inferInstance +instance : LawfulUpwardEnumerableLowerBound .open UInt16 := inferInstance +instance : LawfulUpwardEnumerableUpperBound .open UInt16 := inferInstance + +instance : RangeSize .closed UInt16 where + size bound a := bound.toNat + 1 - a.toNat + +theorem rangeSizeSize_eq_toBitVec {bound : Bound .closed UInt16} {x : BitVec 16} : + RangeSize.size bound (UInt16.ofBitVec x) = RangeSize.size (shape := .closed) bound.toBitVec x := by + simp [RangeSize.size] + +instance : LawfulRangeSize .closed UInt16 where + size_eq_zero_of_not_isSatisfied bound x := by + simpa [rangeSizeSize_eq_toBitVec, UInt16.lt_iff_toBitVec_lt] using + LawfulRangeSize.size_eq_zero_of_not_isSatisfied (su := .closed) (α := BitVec 16) _ _ + size_eq_one_of_succ?_eq_none bound x := by + cases x + simpa [rangeSizeSize_eq_toBitVec, UInt16.le_iff_toBitVec_le, succ?_ofBitVec] using + LawfulRangeSize.size_eq_one_of_succ?_eq_none (su := .closed) (α := BitVec 16) _ _ + size_eq_succ_of_succ?_eq_some bound init x := by + simpa [rangeSizeSize_eq_toBitVec, UInt16.le_iff_toBitVec_le, ← UInt16.toBitVec_inj, succ?] using + LawfulRangeSize.size_eq_succ_of_succ?_eq_some (su := .closed) (α := BitVec 16) _ _ _ + +instance : RangeSize .open UInt16 := RangeSize.openOfClosed +instance : LawfulRangeSize .open UInt16 := inferInstance + +end UInt16 + +namespace UInt32 + +instance : UpwardEnumerable UInt32 where + succ? i := if i + 1 = 0 then none else some (i + 1) + succMany? n i := if h : i.toNat + n < UInt32.size then some (.ofNatLT _ h) else none + +theorem succ?_ofBitVec {x : BitVec 32} : + UpwardEnumerable.succ? (UInt32.ofBitVec x) = UInt32.ofBitVec <$> UpwardEnumerable.succ? x := by + simp only [succ?, BitVec.ofNat_eq_ofNat, Option.map_eq_map, ← UInt32.toBitVec_inj] + split <;> simp_all + +theorem succMany?_ofBitVec {k : Nat} {x : BitVec 32} : + UpwardEnumerable.succMany? k (UInt32.ofBitVec x) = UInt32.ofBitVec <$> UpwardEnumerable.succMany? k x := by + simp [succMany?] + +theorem upwardEnumerableLE_ofBitVec {x y : BitVec 32} : + UpwardEnumerable.LE (UInt32.ofBitVec x) (UInt32.ofBitVec y) ↔ UpwardEnumerable.LE x y := by + simp [UpwardEnumerable.LE, succMany?_ofBitVec] + +theorem upwardEnumerableLT_ofBitVec {x y : BitVec 32} : + UpwardEnumerable.LT (UInt32.ofBitVec x) (UInt32.ofBitVec y) ↔ UpwardEnumerable.LT x y := by + simp [UpwardEnumerable.LT, succMany?_ofBitVec] + +instance : LawfulUpwardEnumerable UInt32 where + ne_of_lt x y := by + cases x; cases y + simpa [upwardEnumerableLT_ofBitVec] using LawfulUpwardEnumerable.ne_of_lt _ _ + succMany?_zero x := by + cases x + simpa [succMany?_ofBitVec] using succMany?_zero + succMany?_succ? n x := by + cases x + simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def, + succ?_ofBitVec] + +instance : LawfulUpwardEnumerableLE UInt32 where + le_iff x y := by + cases x; cases y + simpa [upwardEnumerableLE_ofBitVec, UInt32.le_iff_toBitVec_le] using + LawfulUpwardEnumerableLE.le_iff _ _ + +instance : LawfulOrderLT UInt32 := inferInstance +instance : LawfulUpwardEnumerableLT UInt32 := inferInstance +instance : LawfulUpwardEnumerableLT UInt32 := inferInstance +instance : LawfulUpwardEnumerableLowerBound .closed UInt32 := inferInstance +instance : LawfulUpwardEnumerableUpperBound .closed UInt32 := inferInstance +instance : LawfulUpwardEnumerableLowerBound .open UInt32 := inferInstance +instance : LawfulUpwardEnumerableUpperBound .open UInt32 := inferInstance + +instance : RangeSize .closed UInt32 where + size bound a := bound.toNat + 1 - a.toNat + +theorem rangeSizeSize_eq_toBitVec {bound : Bound .closed UInt32} {x : BitVec 32} : + RangeSize.size bound (UInt32.ofBitVec x) = RangeSize.size (shape := .closed) bound.toBitVec x := by + simp [RangeSize.size] + +instance : LawfulRangeSize .closed UInt32 where + size_eq_zero_of_not_isSatisfied bound x := by + simpa [rangeSizeSize_eq_toBitVec, UInt32.lt_iff_toBitVec_lt] using + LawfulRangeSize.size_eq_zero_of_not_isSatisfied (su := .closed) (α := BitVec 32) _ _ + size_eq_one_of_succ?_eq_none bound x := by + cases x + simpa [rangeSizeSize_eq_toBitVec, UInt32.le_iff_toBitVec_le, succ?_ofBitVec] using + LawfulRangeSize.size_eq_one_of_succ?_eq_none (su := .closed) (α := BitVec 32) _ _ + size_eq_succ_of_succ?_eq_some bound init x := by + simpa [rangeSizeSize_eq_toBitVec, UInt32.le_iff_toBitVec_le, ← UInt32.toBitVec_inj, succ?] using + LawfulRangeSize.size_eq_succ_of_succ?_eq_some (su := .closed) (α := BitVec 32) _ _ _ + +instance : RangeSize .open UInt32 := RangeSize.openOfClosed +instance : LawfulRangeSize .open UInt32 := inferInstance + +end UInt32 + +namespace UInt64 + +instance : UpwardEnumerable UInt64 where + succ? i := if i + 1 = 0 then none else some (i + 1) + succMany? n i := if h : i.toNat + n < UInt64.size then some (.ofNatLT _ h) else none + +theorem succ?_ofBitVec {x : BitVec 64} : + UpwardEnumerable.succ? (UInt64.ofBitVec x) = UInt64.ofBitVec <$> UpwardEnumerable.succ? x := by + simp only [succ?, BitVec.ofNat_eq_ofNat, Option.map_eq_map, ← UInt64.toBitVec_inj] + split <;> simp_all + +theorem succMany?_ofBitVec {k : Nat} {x : BitVec 64} : + UpwardEnumerable.succMany? k (UInt64.ofBitVec x) = UInt64.ofBitVec <$> UpwardEnumerable.succMany? k x := by + simp [succMany?] + +theorem upwardEnumerableLE_ofBitVec {x y : BitVec 64} : + UpwardEnumerable.LE (UInt64.ofBitVec x) (UInt64.ofBitVec y) ↔ UpwardEnumerable.LE x y := by + simp [UpwardEnumerable.LE, succMany?_ofBitVec] + +theorem upwardEnumerableLT_ofBitVec {x y : BitVec 64} : + UpwardEnumerable.LT (UInt64.ofBitVec x) (UInt64.ofBitVec y) ↔ UpwardEnumerable.LT x y := by + simp [UpwardEnumerable.LT, succMany?_ofBitVec] + +instance : LawfulUpwardEnumerable UInt64 where + ne_of_lt x y := by + cases x; cases y + simpa [upwardEnumerableLT_ofBitVec] using LawfulUpwardEnumerable.ne_of_lt _ _ + succMany?_zero x := by + cases x + simpa [succMany?_ofBitVec] using succMany?_zero + succMany?_succ? n x := by + cases x + simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def, + succ?_ofBitVec] + +instance : LawfulUpwardEnumerableLE UInt64 where + le_iff x y := by + cases x; cases y + simpa [upwardEnumerableLE_ofBitVec, UInt64.le_iff_toBitVec_le] using + LawfulUpwardEnumerableLE.le_iff _ _ + +instance : LawfulOrderLT UInt64 := inferInstance +instance : LawfulUpwardEnumerableLT UInt64 := inferInstance +instance : LawfulUpwardEnumerableLT UInt64 := inferInstance +instance : LawfulUpwardEnumerableLowerBound .closed UInt64 := inferInstance +instance : LawfulUpwardEnumerableUpperBound .closed UInt64 := inferInstance +instance : LawfulUpwardEnumerableLowerBound .open UInt64 := inferInstance +instance : LawfulUpwardEnumerableUpperBound .open UInt64 := inferInstance + +instance : RangeSize .closed UInt64 where + size bound a := bound.toNat + 1 - a.toNat + +theorem rangeSizeSize_eq_toBitVec {bound : Bound .closed UInt64} {x : BitVec 64} : + RangeSize.size bound (UInt64.ofBitVec x) = RangeSize.size (shape := .closed) bound.toBitVec x := by + simp [RangeSize.size] + +instance : LawfulRangeSize .closed UInt64 where + size_eq_zero_of_not_isSatisfied bound x := by + simpa [rangeSizeSize_eq_toBitVec, UInt64.lt_iff_toBitVec_lt] using + LawfulRangeSize.size_eq_zero_of_not_isSatisfied (su := .closed) (α := BitVec 64) _ _ + size_eq_one_of_succ?_eq_none bound x := by + cases x + simpa [rangeSizeSize_eq_toBitVec, UInt64.le_iff_toBitVec_le, succ?_ofBitVec] using + LawfulRangeSize.size_eq_one_of_succ?_eq_none (su := .closed) (α := BitVec 64) _ _ + size_eq_succ_of_succ?_eq_some bound init x := by + simpa [rangeSizeSize_eq_toBitVec, UInt64.le_iff_toBitVec_le, ← UInt64.toBitVec_inj, succ?] using + LawfulRangeSize.size_eq_succ_of_succ?_eq_some (su := .closed) (α := BitVec 64) _ _ _ + +instance : RangeSize .open UInt64 := RangeSize.openOfClosed +instance : LawfulRangeSize .open UInt64 := inferInstance + +end UInt64 + +namespace USize + +instance : UpwardEnumerable USize where + succ? i := if i + 1 = 0 then none else some (i + 1) + succMany? n i := if h : i.toNat + n < USize.size then some (.ofNatLT _ h) else none + +theorem succ?_ofBitVec {x : BitVec System.Platform.numBits} : + UpwardEnumerable.succ? (USize.ofBitVec x) = USize.ofBitVec <$> UpwardEnumerable.succ? x := by + simp only [succ?, BitVec.ofNat_eq_ofNat, Option.map_eq_map, ← USize.toBitVec_inj] + split <;> simp_all + +theorem succMany?_ofBitVec {k : Nat} {x : BitVec System.Platform.numBits} : + UpwardEnumerable.succMany? k (USize.ofBitVec x) = USize.ofBitVec <$> UpwardEnumerable.succMany? k x := by + simp [succMany?] + +theorem upwardEnumerableLE_ofBitVec {x y : BitVec System.Platform.numBits} : + UpwardEnumerable.LE (USize.ofBitVec x) (USize.ofBitVec y) ↔ UpwardEnumerable.LE x y := by + simp [UpwardEnumerable.LE, succMany?_ofBitVec] + +theorem upwardEnumerableLT_ofBitVec {x y : BitVec System.Platform.numBits} : + UpwardEnumerable.LT (USize.ofBitVec x) (USize.ofBitVec y) ↔ UpwardEnumerable.LT x y := by + simp [UpwardEnumerable.LT, succMany?_ofBitVec] + +instance : LawfulUpwardEnumerable USize where + ne_of_lt x y := by + cases x; cases y + simpa [upwardEnumerableLT_ofBitVec] using LawfulUpwardEnumerable.ne_of_lt _ _ + succMany?_zero x := by + cases x + simpa [succMany?_ofBitVec] using succMany?_zero + succMany?_succ? n x := by + cases x + simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def, + succ?_ofBitVec] + +instance : LawfulUpwardEnumerableLE USize where + le_iff x y := by + cases x; cases y + simpa [upwardEnumerableLE_ofBitVec, USize.le_iff_toBitVec_le] using + LawfulUpwardEnumerableLE.le_iff _ _ + +instance : LawfulOrderLT USize := inferInstance +instance : LawfulUpwardEnumerableLT USize := inferInstance +instance : LawfulUpwardEnumerableLT USize := inferInstance +instance : LawfulUpwardEnumerableLowerBound .closed USize := inferInstance +instance : LawfulUpwardEnumerableUpperBound .closed USize := inferInstance +instance : LawfulUpwardEnumerableLowerBound .open USize := inferInstance +instance : LawfulUpwardEnumerableUpperBound .open USize := inferInstance + +instance : RangeSize .closed USize where + size bound a := bound.toNat + 1 - a.toNat + +theorem rangeSizeSize_eq_toBitVec {bound : Bound .closed USize} {x : BitVec System.Platform.numBits} : + RangeSize.size bound (USize.ofBitVec x) = RangeSize.size (shape := .closed) bound.toBitVec x := by + simp [RangeSize.size] + +instance : LawfulRangeSize .closed USize where + size_eq_zero_of_not_isSatisfied bound x := by + simpa [rangeSizeSize_eq_toBitVec, USize.lt_iff_toBitVec_lt] using + LawfulRangeSize.size_eq_zero_of_not_isSatisfied (su := .closed) (α := BitVec System.Platform.numBits) _ _ + size_eq_one_of_succ?_eq_none bound x := by + cases x + simpa [rangeSizeSize_eq_toBitVec, USize.le_iff_toBitVec_le, succ?_ofBitVec] using + LawfulRangeSize.size_eq_one_of_succ?_eq_none (su := .closed) (α := BitVec System.Platform.numBits) _ _ + size_eq_succ_of_succ?_eq_some bound init x := by + simpa [rangeSizeSize_eq_toBitVec, USize.le_iff_toBitVec_le, ← USize.toBitVec_inj, succ?] using + LawfulRangeSize.size_eq_succ_of_succ?_eq_some (su := .closed) (α := BitVec System.Platform.numBits) _ _ _ + +instance : RangeSize .open USize := RangeSize.openOfClosed +instance : LawfulRangeSize .open USize := inferInstance + +end USize diff --git a/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean b/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean index 3d4a337d87..d19a160845 100644 --- a/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean +++ b/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean @@ -40,7 +40,6 @@ class UpwardEnumerable (α : Type u) where -/ succMany? (n : Nat) (a : α) : Option α := Nat.repeat (· >>= succ?) n (some a) -attribute [simp] UpwardEnumerable.succ? UpwardEnumerable.succMany? export UpwardEnumerable (succ? succMany?) /-- @@ -80,7 +79,6 @@ class Least? (α : Type u) where -/ least? : Option α -attribute [simp] Least?.least? export Least? (least?) /-- @@ -95,7 +93,7 @@ class LawfulUpwardEnumerable (α : Type u) [UpwardEnumerable α] where The `n + 1`-th successor of `a` is the successor of the `n`-th successor, given that said successors actually exist. -/ - succMany?_succ (n : Nat) (a : α) : + succMany?_succ? (n : Nat) (a : α) : succMany? (n + 1) a = (succMany? n a).bind succ? theorem UpwardEnumerable.succMany?_zero [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a : α} : @@ -105,7 +103,7 @@ theorem UpwardEnumerable.succMany?_zero [UpwardEnumerable α] [LawfulUpwardEnume theorem UpwardEnumerable.succMany?_succ? [UpwardEnumerable α] [LawfulUpwardEnumerable α] {n : Nat} {a : α} : succMany? (n + 1) a = (succMany? n a).bind succ? := - LawfulUpwardEnumerable.succMany?_succ n a + LawfulUpwardEnumerable.succMany?_succ? n a @[deprecated succMany?_succ? (since := "2025-09-03")] theorem UpwardEnumerable.succMany?_succ [UpwardEnumerable α] [LawfulUpwardEnumerable α] diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean index cbecdc5288..7f58667f95 100644 --- a/src/Init/Data/UInt/Lemmas.lean +++ b/src/Init/Data/UInt/Lemmas.lean @@ -311,6 +311,13 @@ theorem UInt64.ofNat_mod_size : ofNat (x % 2 ^ 64) = ofNat x := by theorem USize.ofNat_mod_size : ofNat (x % 2 ^ System.Platform.numBits) = ofNat x := by simp [ofNat, BitVec.ofNat, Fin.ofNat] +theorem UInt8.ofNat_size : ofNat size = 0 := by decide +theorem UInt16.ofNat_size : ofNat size = 0 := by decide +theorem UInt32.ofNat_size : ofNat size = 0 := by decide +theorem UInt64.ofNat_size : ofNat size = 0 := by decide +theorem USize.ofNat_size : ofNat size = 0 := by + simp [ofNat, BitVec.ofNat, USize.eq_iff_toBitVec_eq] + theorem UInt8.lt_ofNat_iff {n : UInt8} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m := by rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h] theorem UInt8.ofNat_lt_iff {n : UInt8} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat := by diff --git a/tests/lean/run/rangePolymorphic.lean b/tests/lean/run/rangePolymorphic.lean index b1a7ea23d2..032f8a6748 100644 --- a/tests/lean/run/rangePolymorphic.lean +++ b/tests/lean/run/rangePolymorphic.lean @@ -92,7 +92,33 @@ section Int example : ((-2)...3).toList = [-2, -1, 0, 1, 2] := by native_decide example : ((-2)...=3).toList = [-2, -1, 0, 1, 2, 3] := by native_decide -example : Std.PRange.LawfulRangeSize .closed Int := inferInstance -example : Std.PRange.LawfulRangeSize .open Int := inferInstance - end Int + +section UInt + +example : ((1 : UInt8)...3).toList = [1, 2] := by native_decide +example : ((-1 : UInt8)...3).toList = [] := by native_decide -- 255 ≤ x < 3 is impossible +example : ((1 : UInt8)...=3).toList = [1, 2, 3] := by native_decide +example : ((250 : UInt8)...-1).toList = [250, 251, 252, 253, 254] := by native_decide + +example : ((1 : UInt16)...3).toList = [1, 2] := by native_decide +example : ((-1 : UInt16)...3).toList = [] := by native_decide +example : ((1 : UInt16)...=3).toList = [1, 2, 3] := by native_decide +example : ((-4 : UInt16)...-1).toList = [-4, -3, -2] := by native_decide + +example : ((1 : UInt32)...3).toList = [1, 2] := by native_decide +example : ((-1 : UInt32)...3).toList = [] := by native_decide +example : ((1 : UInt32)...=3).toList = [1, 2, 3] := by native_decide +example : ((-4 : UInt32)...-1).toList = [-4, -3, -2] := by native_decide + +example : ((1 : UInt64)...3).toList = [1, 2] := by native_decide +example : ((-1 : UInt64)...3).toList = [] := by native_decide +example : ((1 : UInt64)...=3).toList = [1, 2, 3] := by native_decide +example : ((-4 : UInt64)...-1).toList = [-4, -3, -2] := by native_decide + +example : ((1 : USize)...3).toList = [1, 2] := by native_decide +example : ((-1 : USize)...3).toList = [] := by native_decide +example : ((1 : USize)...=3).toList = [1, 2, 3] := by native_decide +example : ((-4 : USize)...-1).toList = [-4, -3, -2] := by native_decide + +end UInt