Skip to content

Commit d8cbef1

Browse files
datokratdatokrat
committed
wip (slow progress)
1 parent 2c5f922 commit d8cbef1

File tree

3 files changed

+256
-15
lines changed

3 files changed

+256
-15
lines changed

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

Lines changed: 105 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -119,16 +119,67 @@ instance : Rxi.IsAlwaysFinite (BitVec n) := inferInstance
119119

120120
namespace Signed
121121

122+
def irredMin n : BitVec n := ↑(2 ^ (n - 1) : Nat)
123+
theorem irredMin_def : irredMin n = ↑(2 ^ (n - 1) : Nat) := (rfl)
124+
seal irredMin
125+
126+
def irredMax n : BitVec n := ↑(2 ^ (n - 1) - 1 : Nat)
127+
theorem irredMax_def : irredMax n = ↑(2 ^ (n - 1) - 1 : Nat) := (rfl)
128+
seal irredMax
129+
122130
@[expose]
123-
def rotate (x : BitVec n) : BitVec n := x + ↑(2 ^ (n - 1) : Nat)
131+
def rotate (x : BitVec n) : BitVec n := x + irredMin n
132+
133+
theorem irredMax_eq_irredMin_add :
134+
irredMax n = irredMin n + ↑(2 ^ n - 1 : Nat) := by
135+
match n with
136+
| 0 => simp [eq_nil (irredMax 0), eq_nil (irredMin 0)]
137+
| n + 1 =>
138+
simp only [irredMax_def, Nat.add_one_sub_one, natCast_eq_ofNat, irredMin_def, ← ofNat_add,
139+
← toNat_inj, toNat_ofNat, Nat.mod_eq_mod_iff]
140+
exact ⟨1, 0, by omega⟩
141+
142+
theorem irredMin_add_irredMin :
143+
irredMin n + irredMin n = 0 := by
144+
match n with
145+
| 0 => simp [eq_nil (irredMin 0)]
146+
| n + 1 =>
147+
simp [irredMin_def, ← BitVec.ofNat_add, show 2 ^ n + 2 ^ n = 2 ^ (n + 1) by omega,
148+
← BitVec.toNat_inj]
149+
150+
theorem rotate_neg_eq_irredMin_sub {x : BitVec n} :
151+
rotate (-x) = irredMin n - x := by
152+
simp only [rotate, irredMin_def, natCast_eq_ofNat]
153+
rw [eq_sub_iff_add_eq, BitVec.add_comm, ← BitVec.add_assoc, BitVec.add_neg_eq_sub,
154+
BitVec.sub_self, BitVec.zero_add]
155+
156+
theorem rotate_eq_sub_irredMin {x : BitVec n} :
157+
rotate x = x - irredMin n := by
158+
simp [rotate, eq_sub_iff_add_eq, BitVec.add_assoc, irredMin_add_irredMin]
159+
160+
theorem rotate_add {x y : BitVec n} :
161+
rotate (x + y) = rotate x + y := by
162+
simp [rotate, BitVec.add_assoc, BitVec.add_comm y]
163+
164+
theorem rotate_sub {x y : BitVec n} :
165+
rotate (x - y) = rotate x - y := by
166+
simp [BitVec.sub_eq_add_neg, rotate_add]
167+
168+
theorem rotate_irredMin :
169+
rotate (irredMin n) = ↑(0 : Nat) := by
170+
simp [rotate, irredMin_add_irredMin]
171+
172+
theorem rotate_irredMax :
173+
rotate (irredMax n) = ↑(2 ^ n - 1 : Nat) := by
174+
simp [irredMax_eq_irredMin_add, rotate_add, rotate_irredMin]
124175

125176
theorem rotate_rotate {x : BitVec n} :
126177
rotate (rotate x) = x := by
127178
match n with
128-
| 0 => simp [eq_nil x, rotate]
179+
| 0 => simp [eq_nil x, rotate, irredMin_def]
129180
| n + 1 =>
130181
simp only [rotate, BitVec.add_assoc]
131-
simp [← BitVec.toNat_inj, ← Nat.two_mul, show 2 * 2 ^ n = 2 ^ (n + 1) by omega]
182+
simp [← BitVec.toNat_inj, ← Nat.two_mul, irredMin_def, show 2 * 2 ^ n = 2 ^ (n + 1) by omega]
132183

133184
theorem rotate_map_eq_iff {x y : Option (BitVec n)} :
134185
rotate <$> x = y ↔ x = rotate <$> y := by
@@ -156,7 +207,8 @@ theorem sle_iff_rotate_le_rotate {x y : BitVec n} :
156207
match n with
157208
| 0 => simp [eq_nil x, eq_nil y]
158209
| n + 1 =>
159-
simp [BitVec.sle_iff_toInt_le, BitVec.toInt, Nat.pow_add, Nat.mul_comm _ 2, rotate, BitVec.le_def]
210+
simp [BitVec.sle_iff_toInt_le, BitVec.toInt, Nat.pow_add, Nat.mul_comm _ 2, rotate, BitVec.le_def,
211+
irredMin_def]
160212
split <;> split
161213
· simp only [Int.ofNat_le]
162214
rw [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega)]
@@ -200,12 +252,45 @@ theorem rotate_inj {x y : BitVec n} :
200252
· intro h
201253
exact congrArg rotate h
202254

255+
theorem rotate_eq_iff {x y : BitVec n} :
256+
rotate x = y ↔ x = rotate y := by
257+
rw [← rotate_rotate (x := y), rotate_inj, rotate_rotate]
258+
259+
theorem toInt_eq_ofNat_toNat_rotate_sub' {x : BitVec n} (h : n > 0) :
260+
x.toInt = (↑(rotate x).toNat : Int) - ↑(irredMin n).toNat := by
261+
match n with
262+
| 0 => omega
263+
| n + 1 =>
264+
simp [BitVec.toInt, rotate, irredMin_def]
265+
rw [Int.emod_eq_of_lt (a := 2 ^ n)]; rotate_left
266+
· exact Int.le_of_lt (Int.pow_pos (by omega))
267+
· rw [Int.pow_add, Int.pow_succ, Int.pow_zero, Int.one_mul, Int.mul_comm, Int.two_mul]
268+
exact Int.lt_add_of_pos_right _ (Int.pow_pos (by omega))
269+
have : (2 : Int) ^ n > 0 := Int.pow_pos (by omega)
270+
split <;> rename_i h
271+
· rw [Nat.pow_add, Nat.pow_one, Nat.mul_comm _ 2, Nat.mul_lt_mul_left (by omega),
272+
← Int.ofNat_lt, Int.natCast_pow, Int.cast_ofNat_Int] at h
273+
rw [Int.emod_eq_of_lt (by omega) (by omega)]
274+
omega
275+
· rw [Nat.pow_add, Nat.pow_one, Nat.mul_comm _ 2, Nat.mul_lt_mul_left (by omega),
276+
← Int.ofNat_lt, Int.natCast_pow, Int.cast_ofNat_Int] at h
277+
simp [Int.pow_add, Int.mul_comm _ 2, Int.two_mul, ← Int.sub_sub]
278+
rw [eq_comm, Int.emod_eq_iff (by omega)]
279+
refine ⟨by omega, ?_, ?_⟩
280+
· have := BitVec.toNat_lt_twoPow_of_le (x := x) (Nat.le_refl _)
281+
rw [Int.ofNat_natAbs_of_nonneg (by omega)]
282+
simp only [Nat.pow_add, Nat.pow_one, ← Int.ofNat_lt, Int.natCast_mul, Int.natCast_pow,
283+
Int.cast_ofNat_Int] at this
284+
omega
285+
· conv => rhs; rw [← Int.sub_sub, Int.sub_sub (b := 2 ^ n), Int.add_comm, ← Int.sub_sub]
286+
exact ⟨-1, by omega⟩
287+
203288
theorem toInt_eq_ofNat_toNat_rotate_sub {x : BitVec n} (h : n > 0) :
204289
x.toInt = (↑(rotate x).toNat : Int) - 2 ^ (n - 1) := by
205290
match n with
206291
| 0 => omega
207292
| n + 1 =>
208-
simp [BitVec.toInt, rotate]
293+
simp [BitVec.toInt, rotate, irredMin_def]
209294
have : (2 : Int) ^ n > 0 := Int.pow_pos (by omega)
210295
split <;> rename_i h
211296
· rw [Nat.pow_add, Nat.pow_one, Nat.mul_comm _ 2, Nat.mul_lt_mul_left (by omega),
@@ -225,6 +310,19 @@ theorem toInt_eq_ofNat_toNat_rotate_sub {x : BitVec n} (h : n > 0) :
225310
· conv => rhs; rw [← Int.sub_sub, Int.sub_sub (b := 2 ^ n), Int.add_comm, ← Int.sub_sub]
226311
exact ⟨-1, by omega⟩
227312

313+
theorem ofNat_eq_rotate_ofInt_sub {n k : Nat} :
314+
BitVec.ofNat n k = rotate (BitVec.ofInt n (↑k - ↑(irredMin n).toNat)) := by
315+
match n with
316+
| 0 => simp only [eq_nil (BitVec.ofNat _ _), eq_nil (rotate _)]
317+
| n + 1 =>
318+
simp [irredMin]
319+
rw [Int.emod_eq_of_lt]; rotate_left
320+
· exact Int.le_of_lt (Int.pow_pos (by omega))
321+
· exact Int.pow_lt_pow_of_lt (by omega) (by omega)
322+
simp [← BitVec.toInt_inj, toInt_ofNat', rotate, Int.bmod_eq_bmod_iff_bmod_sub_eq_zero]
323+
simp [Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc]
324+
simp [Int.add_neg_eq_sub, irredMin, toInt_ofNat']
325+
228326
scoped instance instLE : LE (BitVec n) where
229327
le x y := x.sle y
230328

@@ -308,7 +406,7 @@ scoped instance : Rxc.LawfulHasSize (BitVec n) where
308406
generalize rotate lo = lo
309407
simp only [LE.le]
310408
match n with
311-
| 0 => simp [eq_nil lo, eq_nil hi, succ?, rotate, Rxc.HasSize.size]
409+
| 0 => simp [eq_nil lo, eq_nil hi, succ?, rotate, Rxc.HasSize.size, irredMin_def]
312410
| n + 1 =>
313411
simp [BitVec.sle_iff_toInt_le, toInt_eq_ofNat_toNat_rotate_sub,
314412
Rxc.HasSize.size, rotate_rotate, succ?_rotate, Option.map_eq_map, Option.map_eq_none_iff,
@@ -319,7 +417,7 @@ scoped instance : Rxc.LawfulHasSize (BitVec n) where
319417
generalize rotate lo = lo
320418
simp only [LE.le]
321419
match n with
322-
| 0 => simp [eq_nil lo, eq_nil hi, succ?, rotate, Rxc.HasSize.size]
420+
| 0 => simp [eq_nil lo, eq_nil hi, succ?, rotate, Rxc.HasSize.size, irredMin_def]
323421
| n + 1 =>
324422
simp [BitVec.sle_iff_toInt_le, toInt_eq_ofNat_toNat_rotate_sub,
325423
Rxc.HasSize.size, rotate_rotate, succ?_rotate, succ?_eq_some]

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

Lines changed: 150 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,13 @@ Authors: Paul Reichert
66
module
77

88
prelude
9+
910
public import Init.Data.Range.Polymorphic.Instances
1011
public import Init.Data.Order.Lemmas
1112
public import Init.Data.SInt
1213
import Init.Omega
1314
public import Init.Data.Range.Polymorphic.BitVec
1415
import Init.Data.Range.Polymorphic.UInt
15-
1616
import all Init.Data.SInt.Basic
1717

1818
public section
@@ -23,7 +23,7 @@ namespace HasModel
2323

2424
open BitVec.Signed
2525

26-
variable {α : Type u} [LE α] [LT α] {β : Type u} [LE β] [LT β]
26+
variable {α : Type u} [LE α] [LT α] {β : Type v} [LE β] [LT β]
2727

2828
class _root_.HasModel (α : Type u) [LE α] [LT α] (β : outParam (Type v)) [LE β] [LT β]
2929
[UpwardEnumerable β] [LawfulUpwardEnumerable β] [LawfulUpwardEnumerableLE β]
@@ -257,11 +257,99 @@ open scoped HasModel
257257
attribute [-instance] BitVec.instUpwardEnumerable BitVec.instHasSize BitVec.instHasSize_1
258258
BitVec.instHasSize_2 BitVec.instLawfulUpwardEnumerable
259259

260+
@[inline]
261+
def irredMin := Int16.minValue
262+
theorem irredMin_def : irredMin = Int16.minValue := (rfl)
263+
seal irredMin
264+
265+
@[inline]
266+
def irredMax := Int16.maxValue
267+
theorem irredMax_def : irredMax = Int16.maxValue := (rfl)
268+
seal irredMax
269+
270+
theorem toBitVec_irredMin_eq_irredMin :
271+
irredMin.toBitVec = BitVec.Signed.irredMin 16 := by
272+
simp [irredMin_def, BitVec.Signed.irredMin_def]
273+
274+
theorem toBitVec_irredMax_eq_irredMax :
275+
irredMax.toBitVec = BitVec.Signed.irredMax 16 := by
276+
simp [irredMax_def, BitVec.Signed.irredMax_def]
277+
260278
instance : UpwardEnumerable Int16 where
261-
succ? i := if i + 1 = Int16.minValue then none else some (i + 1)
279+
succ? i := if i + 1 = irredMin then none else some (i + 1)
262280
succMany? n i :=
263281
have := i.minValue_le_toInt
264-
if h : i.toInt + n ≤ Int16.maxValue.toInt then some (.ofIntLE _ (by omega) h) else none
282+
if h : i.toInt + n ≤ irredMax.toInt then some (.ofIntLE _ (by omega) (irredMax_def ▸ h)) else none
283+
284+
instance : HasModel Int16 (BitVec 16) where
285+
encode x := x.toBitVec
286+
decode x := .ofBitVec x
287+
encode_decode := by simp
288+
decode_encode := by simp
289+
le_iff_encode_le := by simp [Int16.le_iff_toBitVec_sle, BitVec.Signed.instLE]
290+
lt_iff_encode_lt := by simp [Int16.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
291+
292+
private theorem ofBitVec_eq_iff {x : BitVec 16} {y : Int16} :
293+
Int16.ofBitVec x = y ↔ x = y.toBitVec := by
294+
rw [← toBitVec_ofBitVec x, toBitVec_inj, toBitVec_ofBitVec]
295+
296+
theorem general_succ? {α : Type u} [UpwardEnumerable α] [LE α] [LT α] [m : HasModel α (BitVec n)]
297+
{x : α}
298+
(h : ∀ y, succ? x = some y ↔ ¬ m.encode x + 1#n = BitVec.Signed.irredMin n ∧ m.encode x + 1#n = m.encode y) :
299+
succ? x = (haveI := HasModel.instUpwardEnumerable (α := α); succ? x) := by
300+
ext y
301+
simp only [UpwardEnumerable.succ?, h]
302+
rw [← Option.map_inj_right HasModel.eq_of_encode_eq, Option.map_map, Function.comp_def]
303+
simp [HasModel.encode_decode, ← BitVec.eq_sub_iff_add_eq, rotate_eq_iff,
304+
← rotate_neg_eq_irredMin_sub, rotate_sub, rotate_rotate]
305+
306+
theorem general_succMany? {α : Type u} [UpwardEnumerable α] [LE α] [LT α] [m : HasModel α (BitVec n)]
307+
{x : α} {k} :
308+
haveI := HasModel.instUpwardEnumerable (α := α)
309+
succMany? k x = if (m.encode x).toInt + ↑k ≤ (BitVec.Signed.irredMax n).toInt then some (m.decode (BitVec.ofInt n ((m.encode x).toInt + ↑k))) else none := by
310+
have h : ∀ a b c d : Int, a - b + c ≤ d - b ↔ a + c ≤ d := by omega
311+
simp [UpwardEnumerable.succMany?, BitVec.ofNatLT_eq_ofNat]
312+
simp [toInt_eq_ofNat_toNat_rotate_sub' sorry, rotate_irredMax, h]
313+
simp only [← Int.natCast_add]
314+
congr
315+
· rw [Nat.lt_iff_add_one_le, Int.ofNat_le, Nat.le_sub_iff_add_le]
316+
exact Nat.pow_pos (Nat.zero_lt_succ _)
317+
· generalize rotate (HasModel.encode x) = x
318+
simp only [ofNat_eq_rotate_ofInt_sub, rotate_rotate]
319+
congr; omega
320+
321+
theorem instUpwardEnumerable_eq :
322+
instUpwardEnumerable = HasModel.instUpwardEnumerable := by
323+
apply UpwardEnumerable.ext
324+
· apply funext; intro x
325+
apply general_succ?
326+
intro y
327+
simp [HasModel.encode, succ?, ← Int16.toBitVec_inj, toBitVec_irredMin_eq_irredMin]
328+
· apply funext; intro n; apply funext; intro x
329+
simp [general_succMany?, instUpwardEnumerable, HasModel.encode, HasModel.decode,
330+
← toInt_toBitVec, toBitVec_irredMax_eq_irredMax, ofIntLE_eq_ofInt]
331+
332+
open BitVec.Signed
333+
open scoped HasModel
334+
335+
attribute [-instance] BitVec.instUpwardEnumerable BitVec.instHasSize BitVec.instHasSize_1
336+
BitVec.instHasSize_2 BitVec.instLawfulUpwardEnumerable
337+
338+
@[inline]
339+
def irredMin := Int16.minValue
340+
theorem irredMin_def : irredMin = Int16.minValue := (rfl)
341+
seal irredMin
342+
343+
@[inline]
344+
def irredMax := Int16.maxValue
345+
theorem irredMax_def : irredMax = Int16.maxValue := (rfl)
346+
seal irredMax
347+
348+
instance : UpwardEnumerable Int16 where
349+
succ? i := if i + 1 = irredMin then none else some (i + 1)
350+
succMany? n i :=
351+
have := i.minValue_le_toInt
352+
if h : i.toInt + n ≤ irredMax.toInt then some (.ofIntLE _ (by omega) (irredMax_def ▸ h)) else none
265353

266354
instance : HasModel Int16 (BitVec 16) where
267355
encode x := x.toBitVec
@@ -271,6 +359,61 @@ instance : HasModel Int16 (BitVec 16) where
271359
le_iff_encode_le := by simp [Int16.le_iff_toBitVec_sle, BitVec.Signed.instLE]
272360
lt_iff_encode_lt := by simp [Int16.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
273361

362+
-- theorem bla {x : Int16} :
363+
-- (succ? x) = (if (x.toBitVec + 1 = - 2 ^ 15) then none else some (x.toBitVec + 1)).map .ofBitVec := by
364+
-- sorry
365+
366+
-- #print instUpwardEnumerable
367+
368+
-- axiom sry {α} : α
369+
370+
-- seal HasModel.instUpwardEnumerable
371+
372+
-- theorem ex :
373+
-- sry = (HasModel.instUpwardEnumerable : UpwardEnumerable Int16) := by
374+
-- apply UpwardEnumerable.ext
375+
-- · apply funext; intro x
376+
-- generalize h : @succ? Int16 sry x = g
377+
-- rw [bla] at h
378+
-- rw [bla]
379+
380+
theorem bla {x : Int16} :
381+
(succ? x) = (if (x.toBitVec + 1 = - 2 ^ 15) then none else some (x.toBitVec + 1)).map .ofBitVec := by
382+
simp only [← BitVec.eq_sub_iff_add_eq, succ?, ← toBitVec_inj,
383+
show minValue.toBitVec = - 2 ^ 15 by rfl, Int16.toBitVec_add, toBitVec_ofNat]
384+
split <;> simp
385+
386+
#print instUpwardEnumerable
387+
388+
--seal HasModel.instUpwardEnumerable
389+
--seal instUpwardEnumerable
390+
391+
theorem ex :
392+
instUpwardEnumerable = HasModel.instUpwardEnumerable := by
393+
apply UpwardEnumerable.ext
394+
· apply funext; intro x
395+
refine Eq.trans bla ?_
396+
397+
398+
simp only [instUpwardEnumerable, HasModel.instUpwardEnumerable, HasModel.encode,
399+
HasModel.decode]
400+
-- simp only [instUpwardEnumerable, HasModel.instUpwardEnumerable,
401+
-- HasModel.encode, HasModel.decode, UpwardEnumerable.succ?,
402+
-- UpwardEnumerable.succMany?]
403+
-- have : ∀ {s sm s' sm'}, sm = sm' → UpwardEnumerable.mk s sm = (UpwardEnumerable.mk s' sm' : UpwardEnumerable Int16) := by
404+
-- sorry
405+
406+
-- apply this
407+
-- · ext n x y
408+
-- simp only [← toInt_toBitVec, toInt_eq_ofNat_toNat_rotate_sub (show 16 > 0 by omega), rotate,
409+
-- BitVec.natCast_eq_ofNat, BitVec.toNat_add, BitVec.toNat_ofNat]
410+
-- simp only [ofIntLE_eq_ofInt]
411+
-- -- simp [h₁, h₂, ← Int16.toInt_toBitVec, toInt_eq_ofNat_toNat_rotate_sub (show 16 > 0 by omega),
412+
-- -- rotate, BitVec.ofNatLT_eq_ofNat, ofIntLE_eq_ofInt, Int16.ofInt_eq_ofNat,
413+
-- -- ofInt_eq_ofNat, Int16.add_assoc, Int16.add_comm (ofNat (2 ^ 15)), and_congr_left_iff,
414+
-- -- - Int.reducePow, - Nat.reducePow, - Int.natCast_pow, - Int.natCast_add, - Int.natCast_emod, ]
415+
-- omega
416+
274417
theorem instUpwardEnumerable_eq :
275418
instUpwardEnumerable = HasModel.instUpwardEnumerable := by
276419
simp only [instUpwardEnumerable, HasModel.instUpwardEnumerable,
@@ -280,11 +423,10 @@ theorem instUpwardEnumerable_eq :
280423
sorry
281424
apply this
282425
--congr 1
283-
· ext x y
284-
simp [← Int16.toBitVec_inj, ← BitVec.eq_sub_iff_add_eq, rotate, BitVec.sub_sub]
426+
· sorry
427+
-- ext x y
428+
-- simp [← Int16.toBitVec_inj, ← BitVec.eq_sub_iff_add_eq, rotate, BitVec.sub_sub]
285429
· ext n x y
286-
have h₁ : ∀ n, (2 : Int) ^ n = ↑((2 : Nat) ^ n) := by simp
287-
have h₂ : ∀ x : Int16, x - ofNat (2 ^ 15) = x + ofNat (2 ^ 15) := by simp
288430
simp only [← toInt_toBitVec, toInt_eq_ofNat_toNat_rotate_sub (show 16 > 0 by omega), rotate,
289431
BitVec.natCast_eq_ofNat, BitVec.toNat_add, BitVec.toNat_ofNat]
290432
simp only [ofIntLE_eq_ofInt]

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ These properties and the compatibility of `succ?` with `succMany?` are encoded i
2727
`LawfulUpwardEnumerable`, `LawfulUpwardEnumerableLE` and `LawfulUpwardEnumerableLT`.
2828
2929
-/
30+
@[ext]
3031
class UpwardEnumerable (α : Type u) where
3132
/-- Maps elements of `α` to their successor, or none if no successor exists. -/
3233
succ? : α → Option α

0 commit comments

Comments
 (0)