1	import Base
2	import ../../lib/nat.bend as N
3	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
4	import ../../lib/lemmas/proofs/word_value.bend as WV
5	import ../../lib/u32div.bend as UD
6	import ./cyc.bend as CY
7	
8	# Offsets around a ring of n buckets (n > 0):
9	#   pos(n, h, t)  == (h + t) mod n   the bucket t steps after h
10	#   dist(n, h, j) == (j + n - h) mod n   the steps from h to j
11	# and they are inverse.
12	
13	def pos(+n: Nat, +h: Nat, +t: Nat) -> Nat:
14	  Nat.mod(Nat.add(h, t), n)
15	
16	def dist(+n: Nat, +h: Nat, +j: Nat) -> Nat:
17	  Nat.mod(Nat.add(j, Nat.sub(n, h)), n)
18	
19	def dm_e2(+bp: Nat, +v: Nat, g: WV.go_equation(bp, v, bp, 0n, 0n)) -> {v == Nat.add(Nat.mul(Nat.div(v, 1n+bp), 1n+bp), Nat.mod(v, 1n+bp)) : Nat}:
20	  (e, l) = g
21	  e
22	
23	def dm_l2(+bp: Nat, +v: Nat, g: WV.go_equation(bp, v, bp, 0n, 0n)) -> {Nat.is_lt(Nat.mod(v, 1n+bp), 1n+bp) == True{} : Bool}:
24	  (e, l) = g
25	  N.le_lt_succ(Nat.mod(v, 1n+bp), bp, l)
26	
27	# v == (v / n) n + v mod n, and v mod n < n
28	def dm_eq(+bp: Nat, +v: Nat) -> {v == Nat.add(Nat.mul(Nat.div(v, 1n+bp), 1n+bp), Nat.mod(v, 1n+bp)) : Nat}:
29	  dm_e2(bp, v, WV.go(bp, v, bp, 0n, 0n, N.add_zero(bp)))
30	
31	def dm_lt(+bp: Nat, +v: Nat) -> {Nat.is_lt(Nat.mod(v, 1n+bp), 1n+bp) == True{} : Bool}:
32	  dm_l2(bp, v, WV.go(bp, v, bp, 0n, 0n, N.add_zero(bp)))
33	
34	# (q n + r) mod n == r mod n
35	def absorb(+bp: Nat, +q: Nat, +r: Nat) -> {Nat.mod(Nat.add(Nat.mul(q, 1n+bp), r), 1n+bp) == Nat.mod(r, 1n+bp) : Nat}:
36	  +n = {1n+bp : Nat}
37	  +qr = Nat.div(r, n)
38	  +m = Nat.mod(r, n)
39	  +e = Equal.trans(Nat, Nat.add(Nat.mul(q, n), r), Nat.add(Nat.mul(q, n), Nat.add(Nat.mul(qr, n), m)), Nat.add(Nat.mul(Nat.add(q, qr), n), m),
40	    Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(q, n), z), r, Nat.add(Nat.mul(qr, n), m), dm_eq(bp, r)),
41	    Equal.trans(Nat, Nat.add(Nat.mul(q, n), Nat.add(Nat.mul(qr, n), m)), Nat.add(Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), m), Nat.add(Nat.mul(Nat.add(q, qr), n), m),
42	      Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), m), Nat.add(Nat.mul(q, n), Nat.add(Nat.mul(qr, n), m)), N.add_assoc(Nat.mul(q, n), Nat.mul(qr, n), m)),
43	      Equal.cong(Nat, Nat, z => Nat.add(z, m), Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), Nat.mul(Nat.add(q, qr), n), Equal.sym(Nat, Nat.mul(Nat.add(q, qr), n), Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), NA.mul_add_right(q, qr, n)))))
44	  Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(q, n), r), n), Nat.mod(Nat.add(Nat.mul(Nat.add(q, qr), n), m), n), m, Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(Nat.mul(q, n), r), Nat.add(Nat.mul(Nat.add(q, qr), n), m), e), UD.mod_identify(Nat.add(q, qr), n, m, dm_lt(bp, r)))
45	
46	# x + (y mod n) and x + y agree mod n
47	def mod_inner(+bp: Nat, +x: Nat, +y: Nat) -> {Nat.mod(Nat.add(x, Nat.mod(y, 1n+bp)), 1n+bp) == Nat.mod(Nat.add(x, y), 1n+bp) : Nat}:
48	  +n = {1n+bp : Nat}
49	  +qy = Nat.div(y, n)
50	  +my = Nat.mod(y, n)
51	  +e = Equal.trans(Nat, Nat.add(x, y), Nat.add(x, Nat.add(Nat.mul(qy, n), my)), Nat.add(Nat.mul(qy, n), Nat.add(x, my)),
52	    Equal.cong(Nat, Nat, z => Nat.add(x, z), y, Nat.add(Nat.mul(qy, n), my), dm_eq(bp, y)),
53	    NA.add_swap(x, Nat.mul(qy, n), my))
54	  Equal.sym(Nat, Nat.mod(Nat.add(x, y), n), Nat.mod(Nat.add(x, my), n), Equal.trans(Nat, Nat.mod(Nat.add(x, y), n), Nat.mod(Nat.add(Nat.mul(qy, n), Nat.add(x, my)), n), Nat.mod(Nat.add(x, my), n), Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(x, y), Nat.add(Nat.mul(qy, n), Nat.add(x, my)), e), absorb(bp, qy, Nat.add(x, my))))
55	
56	def pos_lt(+bp: Nat, +h: Nat, +t: Nat) -> {Nat.is_lt(pos(1n+bp, h, t), 1n+bp) == True{} : Bool}:
57	  dm_lt(bp, Nat.add(h, t))
58	
59	def dist_lt(+bp: Nat, +h: Nat, +j: Nat) -> {Nat.is_lt(dist(1n+bp, h, j), 1n+bp) == True{} : Bool}:
60	  dm_lt(bp, Nat.add(j, Nat.sub(1n+bp, h)))
61	
62	# walking dist(h, j) steps from h reaches j
63	def pos_dist(+bp: Nat, +h: Nat, +j: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}) -> {pos(1n+bp, h, dist(1n+bp, h, j)) == j : Nat}:
64	  +n = {1n+bp : Nat}
65	  +s = Nat.add(j, Nat.sub(n, h))
66	  +e = Equal.trans(Nat, Nat.add(h, s), Nat.add(j, Nat.add(h, Nat.sub(n, h))), Nat.add(n, j), NA.add_swap(h, j, Nat.sub(n, h)),
67	    Equal.trans(Nat, Nat.add(j, Nat.add(h, Nat.sub(n, h))), Nat.add(j, n), Nat.add(n, j), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(h, Nat.sub(n, h)), n, N.sub_add(n, h, N.lt_le(h, n, hh))), N.add_comm(j, n)))
68	  Equal.trans(Nat, Nat.mod(Nat.add(h, Nat.mod(s, n)), n), Nat.mod(Nat.add(h, s), n), j, mod_inner(bp, h, s),
69	    Equal.trans(Nat, Nat.mod(Nat.add(h, s), n), Nat.mod(Nat.add(n, j), n), j, Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(h, s), Nat.add(n, j), e), CY.mod_plus(n, j, hj)))
70	
71	# the distance from h to the bucket t < n steps after h is t
72	def dist_pos(+bp: Nat, +h: Nat, +t: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +ht: {Nat.is_lt(t, 1n+bp) == True{} : Bool}) -> {dist(1n+bp, h, pos(1n+bp, h, t)) == t : Nat}:
73	  +n = {1n+bp : Nat}
74	  +d = Nat.sub(n, h)
75	  +x = Nat.mod(Nat.add(h, t), n)
76	  +e1 = Equal.trans(Nat, Nat.mod(Nat.add(x, d), n), Nat.mod(Nat.add(d, x), n), Nat.mod(Nat.add(d, Nat.add(h, t)), n), Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(x, d), Nat.add(d, x), N.add_comm(x, d)), mod_inner(bp, d, Nat.add(h, t)))
77	  +e2 = Equal.trans(Nat, Nat.add(d, Nat.add(h, t)), Nat.add(Nat.add(d, h), t), Nat.add(n, t), Equal.sym(Nat, Nat.add(Nat.add(d, h), t), Nat.add(d, Nat.add(h, t)), N.add_assoc(d, h, t)),
78	    Equal.cong(Nat, Nat, z => Nat.add(z, t), Nat.add(d, h), n, Equal.trans(Nat, Nat.add(d, h), Nat.add(h, d), n, N.add_comm(d, h), N.sub_add(n, h, N.lt_le(h, n, hh)))))
79	  Equal.trans(Nat, Nat.mod(Nat.add(x, d), n), Nat.mod(Nat.add(d, Nat.add(h, t)), n), t, e1, Equal.trans(Nat, Nat.mod(Nat.add(d, Nat.add(h, t)), n), Nat.mod(Nat.add(n, t), n), t, Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(d, Nat.add(h, t)), Nat.add(n, t), e2), CY.mod_plus(n, t, ht)))
80	
81	# the bucket after pos(h, t) is pos(h, t + 1)
82	def pos_next(+bp: Nat, +h: Nat, +t: Nat) -> {Nat.mod(1n+pos(1n+bp, h, t), 1n+bp) == pos(1n+bp, h, 1n+t) : Nat}:
83	  +n = {1n+bp : Nat}
84	  Equal.trans(Nat, Nat.mod(Nat.add(1n, Nat.mod(Nat.add(h, t), n)), n), Nat.mod(Nat.add(1n, Nat.add(h, t)), n), Nat.mod(Nat.add(h, 1n+t), n), mod_inner(bp, 1n, Nat.add(h, t)), Equal.cong(Nat, Nat, z => Nat.mod(z, n), 1n+Nat.add(h, t), Nat.add(h, 1n+t), Equal.sym(Nat, Nat.add(h, 1n+t), 1n+Nat.add(h, t), N.add_succ(h, t))))