Skip to content

Commit 73b1991

Browse files
datokratdatokrat
committed
Rxi.HasSize
1 parent 167265f commit 73b1991

File tree

2 files changed

+131
-13
lines changed

2 files changed

+131
-13
lines changed

‎src/Init/Data/Range/Polymorphic/BitVec.lean‎

Lines changed: 46 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,37 @@ instance : UpwardEnumerable (BitVec n) where
2323
succ? i := if i + 1 = 0 then none else some (i + 1)
2424
succMany? m i := if h : i.toNat + m < 2 ^ n then some (.ofNatLT _ h) else none
2525

26+
theorem succ?_eq_none {x : BitVec n} :
27+
UpwardEnumerable.succ? x = none ↔ x.toNat = 2 ^ n - 1 := by
28+
simp [succ?, ← BitVec.toNat_inj]
29+
apply Iff.intro
30+
· refine fun h => Classical.not_not.mp fun _ => ?_
31+
simp [Nat.mod_eq_of_lt (a := x.toNat + 1) (b := 2 ^ n) (by omega)] at h
32+
· have := Nat.two_pow_pos n
33+
simp +contextual [show 2 ^ n - 1 + 1 = 2 ^ n by omega]
34+
35+
theorem succ?_eq_some {x y : BitVec n} :
36+
succ? x = some y ↔ x.toNat < 2 ^ n - 1 ∧ y.toNat = x.toNat + 1 := by
37+
match h : succ? x with
38+
| none => simp_all [succ?_eq_none]
39+
| some y' =>
40+
simp only [Option.some.injEq]
41+
apply Iff.intro
42+
· rintro rfl
43+
have : ¬ succ? x = none := fun _ => by simp_all
44+
simp only [succ?_eq_none] at this
45+
simp only [succ?, ofNat_eq_ofNat, Option.ite_none_left_eq_some, Option.some.injEq] at h
46+
apply And.intro
47+
· omega
48+
· simp only [← toNat_inj, toNat_add, toNat_ofNat, Nat.add_mod_mod, Nat.zero_mod] at h
49+
rw [Nat.mod_eq_of_lt (by omega)] at h
50+
exact h.2.symm
51+
· simp only [succ?, ofNat_eq_ofNat, ← toNat_inj, toNat_add, toNat_ofNat, Nat.add_mod_mod,
52+
Nat.zero_mod, Option.ite_none_left_eq_some, Option.some.injEq] at h
53+
intro h'
54+
rw [Nat.mod_eq_of_lt (by omega)] at h
55+
simp [← BitVec.toNat_inj, *]
56+
2657
instance : LawfulUpwardEnumerable (BitVec n) where
2758
ne_of_lt := by
2859
simp +contextual [UpwardEnumerable.LT, ← BitVec.toNat_inj, succMany?] at ⊢
@@ -58,23 +89,14 @@ instance : Rxc.HasSize (BitVec n) where
5889

5990
instance : Rxc.LawfulHasSize (BitVec n) where
6091
size_eq_zero_of_not_le bound x := by
61-
simp [BitVec.not_le, Rxc.HasSize.size, BitVec.lt_def]
92+
simp only [BitVec.not_le, Rxc.HasSize.size, BitVec.lt_def]
6293
omega
6394
size_eq_one_of_succ?_eq_none lo hi := by
6495
have := BitVec.toNat_lt_twoPow_of_le (Nat.le_refl _) (x := hi)
65-
have (h : (lo.toNat + 1) % 2 ^ n = 0) : lo.toNat = 2 ^ n - 1 := by
66-
apply Classical.not_not.mp
67-
intro _
68-
simp [Nat.mod_eq_of_lt (a := lo.toNat + 1) (b := 2 ^ n) (by omega)] at h
69-
simp [Rxc.HasSize.size, BitVec.le_def, ← BitVec.toNat_inj, succ?]
96+
simp only [succ?_eq_none, Rxc.HasSize.size, BitVec.le_def]
7097
omega
7198
size_eq_succ_of_succ?_eq_some lo hi x := by
72-
have (h : ¬ (lo.toNat + 1) % 2 ^ n = 0) : ¬ (lo.toNat + 1 ≥ 2 ^ n) := by
73-
intro _
74-
have : lo.toNat + 1 = 2 ^ n := by omega
75-
simp_all
76-
simp_all +contextual [Rxc.HasSize.size, BitVec.le_def, ← BitVec.toNat_inj,
77-
Nat.mod_eq_of_lt (a := lo.toNat + 1) (b := 2 ^ n), succ?]
99+
simp only [succ?_eq_some, Rxc.HasSize.size, BitVec.le_def]
78100
omega
79101

80102
instance : Rxc.IsAlwaysFinite (BitVec n) := inferInstance
@@ -83,6 +105,17 @@ instance : Rxo.HasSize (BitVec n) := .ofClosed
83105
instance : Rxo.LawfulHasSize (BitVec n) := inferInstance
84106
instance : Rxo.IsAlwaysFinite (BitVec n) := inferInstance
85107

86-
-- TODO: Rxi.LawfulHasSize
108+
instance : Rxi.HasSize (BitVec n) where
109+
size lo := 2 ^ n - lo.toNat
110+
111+
instance : Rxi.LawfulHasSize (BitVec n) where
112+
size_eq_one_of_succ?_eq_none x := by
113+
simp only [succ?_eq_none, Rxi.HasSize.size]
114+
omega
115+
size_eq_succ_of_succ?_eq_some lo lo' := by
116+
simp only [succ?_eq_some, Rxi.HasSize.size]
117+
omega
118+
119+
instance : Rxi.IsAlwaysFinite (BitVec n) := inferInstance
87120

88121
end BitVec

‎src/Init/Data/Range/Polymorphic/UInt.lean‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,23 @@ instance : Rxo.HasSize UInt8 := .ofClosed
8888
instance : Rxo.LawfulHasSize UInt8 := inferInstance
8989
instance : Rxo.IsAlwaysFinite UInt8 := inferInstance
9090

91+
instance : Rxi.HasSize UInt8 where
92+
size lo := 2 ^ 8 - lo.toNat
93+
94+
theorem rxiHasSize_eq_toBitVec :
95+
Rxi.HasSize.size (UInt8.ofBitVec lo) = Rxi.HasSize.size lo := by
96+
simp [Rxi.HasSize.size]
97+
98+
instance : Rxi.LawfulHasSize UInt8 where
99+
size_eq_one_of_succ?_eq_none lo := by
100+
cases lo
101+
simpa [rxiHasSize_eq_toBitVec, succ?_ofBitVec] using
102+
Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none (α := BitVec 8) _
103+
size_eq_succ_of_succ?_eq_some lo lo' := by
104+
cases lo; cases lo'
105+
simpa [rxiHasSize_eq_toBitVec, succ?_ofBitVec] using
106+
Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some (α := BitVec 8) _ _
107+
91108
end UInt8
92109

93110
namespace UInt16
@@ -162,6 +179,23 @@ instance : Rxo.HasSize UInt16 := .ofClosed
162179
instance : Rxo.LawfulHasSize UInt16 := inferInstance
163180
instance : Rxo.IsAlwaysFinite UInt16 := inferInstance
164181

182+
instance : Rxi.HasSize UInt16 where
183+
size lo := 2 ^ 16 - lo.toNat
184+
185+
theorem rxiHasSize_eq_toBitVec :
186+
Rxi.HasSize.size (UInt16.ofBitVec lo) = Rxi.HasSize.size lo := by
187+
simp [Rxi.HasSize.size]
188+
189+
instance : Rxi.LawfulHasSize UInt16 where
190+
size_eq_one_of_succ?_eq_none lo := by
191+
cases lo
192+
simpa [rxiHasSize_eq_toBitVec, succ?_ofBitVec] using
193+
Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none (α := BitVec 16) _
194+
size_eq_succ_of_succ?_eq_some lo lo' := by
195+
cases lo; cases lo'
196+
simpa [rxiHasSize_eq_toBitVec, succ?_ofBitVec] using
197+
Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some (α := BitVec 16) _ _
198+
165199
end UInt16
166200

167201
namespace UInt32
@@ -236,6 +270,23 @@ instance : Rxo.HasSize UInt32 := .ofClosed
236270
instance : Rxo.LawfulHasSize UInt32 := inferInstance
237271
instance : Rxo.IsAlwaysFinite UInt32 := inferInstance
238272

273+
instance : Rxi.HasSize UInt32 where
274+
size lo := 2 ^ 32 - lo.toNat
275+
276+
theorem rxiHasSize_eq_toBitVec :
277+
Rxi.HasSize.size (UInt32.ofBitVec lo) = Rxi.HasSize.size lo := by
278+
simp [Rxi.HasSize.size]
279+
280+
instance : Rxi.LawfulHasSize UInt32 where
281+
size_eq_one_of_succ?_eq_none lo := by
282+
cases lo
283+
simpa [rxiHasSize_eq_toBitVec, succ?_ofBitVec] using
284+
Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none (α := BitVec 32) _
285+
size_eq_succ_of_succ?_eq_some lo lo' := by
286+
cases lo; cases lo'
287+
simpa [rxiHasSize_eq_toBitVec, succ?_ofBitVec] using
288+
Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some (α := BitVec 32) _ _
289+
239290
end UInt32
240291

241292
namespace UInt64
@@ -310,6 +361,23 @@ instance : Rxo.HasSize UInt64 := .ofClosed
310361
instance : Rxo.LawfulHasSize UInt64 := inferInstance
311362
instance : Rxo.IsAlwaysFinite UInt64 := inferInstance
312363

364+
instance : Rxi.HasSize UInt64 where
365+
size lo := 2 ^ 64 - lo.toNat
366+
367+
theorem rxiHasSize_eq_toBitVec :
368+
Rxi.HasSize.size (UInt64.ofBitVec lo) = Rxi.HasSize.size lo := by
369+
simp [Rxi.HasSize.size]
370+
371+
instance : Rxi.LawfulHasSize UInt64 where
372+
size_eq_one_of_succ?_eq_none lo := by
373+
cases lo
374+
simpa [rxiHasSize_eq_toBitVec, succ?_ofBitVec] using
375+
Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none (α := BitVec 64) _
376+
size_eq_succ_of_succ?_eq_some lo lo' := by
377+
cases lo; cases lo'
378+
simpa [rxiHasSize_eq_toBitVec, succ?_ofBitVec] using
379+
Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some (α := BitVec 64) _ _
380+
313381
end UInt64
314382

315383
namespace USize
@@ -384,4 +452,21 @@ instance : Rxo.HasSize USize := .ofClosed
384452
instance : Rxo.LawfulHasSize USize := inferInstance
385453
instance : Rxo.IsAlwaysFinite USize := inferInstance
386454

455+
instance : Rxi.HasSize USize where
456+
size lo := 2 ^ System.Platform.numBits - lo.toNat
457+
458+
theorem rxiHasSize_eq_toBitVec :
459+
Rxi.HasSize.size (USize.ofBitVec lo) = Rxi.HasSize.size lo := by
460+
simp [Rxi.HasSize.size]
461+
462+
instance : Rxi.LawfulHasSize USize where
463+
size_eq_one_of_succ?_eq_none lo := by
464+
cases lo
465+
simpa [rxiHasSize_eq_toBitVec, succ?_ofBitVec] using
466+
Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none (α := BitVec System.Platform.numBits) _
467+
size_eq_succ_of_succ?_eq_some lo lo' := by
468+
cases lo; cases lo'
469+
simpa [rxiHasSize_eq_toBitVec, succ?_ofBitVec] using
470+
Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some (α := BitVec System.Platform.numBits) _ _
471+
387472
end USize

0 commit comments

Comments
 (0)