proofs/containers/hash_table/ring.bend
bend-collections-laws-containers@1.0.0.0 · 107 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/modn.bend as M
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/inv.bend as IV
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insm.bend as IM
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insert.bend as IS
11
12# Offsets around the ring of buckets, and rewriting two buckets of a list.
13
14
15def mod_n(+bp: Nat, +r: Nat) -> {Nat.mod(Nat.add(1n+bp, r), 1n+bp) == Nat.mod(r, 1n+bp) : Nat}:
16 Equal.trans(Nat, Nat.mod(Nat.add(1n+bp, r), 1n+bp), Nat.mod(Nat.add(Nat.mul(1n, 1n+bp), r), 1n+bp), Nat.mod(r, 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(z, r), 1n+bp), 1n+bp, Nat.mul(1n, 1n+bp), Equal.sym(Nat, Nat.mul(1n, 1n+bp), 1n+bp, Equal.trans(Nat, Nat.mul(1n, 1n+bp), Nat.mul(1n+bp, 1n), 1n+bp, NA.mul_comm(1n, 1n+bp), NA.mul_one(1n+bp)))), M.absorb(bp, 1n, r))
17
18# walking x then y steps is walking x + y steps
19def pos_add(+bp: Nat, +a: Nat, +x: Nat, +y: Nat) -> {M.pos(1n+bp, M.pos(1n+bp, a, x), y) == M.pos(1n+bp, a, Nat.add(x, y)) : Nat}:
20 +p = Nat.mod(Nat.add(a, x), 1n+bp)
21 Equal.trans(Nat, Nat.mod(Nat.add(p, y), 1n+bp), Nat.mod(Nat.add(y, p), 1n+bp), M.pos(1n+bp, a, Nat.add(x, y)), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(p, y), Nat.add(y, p), N.add_comm(p, y)),
22 Equal.trans(Nat, Nat.mod(Nat.add(y, p), 1n+bp), Nat.mod(Nat.add(y, Nat.add(a, x)), 1n+bp), M.pos(1n+bp, a, Nat.add(x, y)), M.mod_inner(bp, y, Nat.add(a, x)),
23 Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(y, Nat.add(a, x)), Nat.add(a, Nat.add(x, y)), Equal.trans(Nat, Nat.add(y, Nat.add(a, x)), Nat.add(a, Nat.add(y, x)), Nat.add(a, Nat.add(x, y)), NA.add_swap(y, a, x), Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(y, x), Nat.add(x, y), N.add_comm(y, x))))))
24
25# walking n more steps comes back
26def pos_wrap(+bp: Nat, +a: Nat, +t: Nat) -> {M.pos(1n+bp, a, Nat.add(1n+bp, t)) == M.pos(1n+bp, a, t) : Nat}:
27 Equal.trans(Nat, Nat.mod(Nat.add(a, Nat.add(1n+bp, t)), 1n+bp), Nat.mod(Nat.add(1n+bp, Nat.add(a, t)), 1n+bp), M.pos(1n+bp, a, t), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(a, Nat.add(1n+bp, t)), Nat.add(1n+bp, Nat.add(a, t)), NA.add_swap(a, 1n+bp, t)), mod_n(bp, Nat.add(a, t)))
28
29def dist_self(+bp: Nat, +a: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}) -> {M.dist(1n+bp, a, a) == 0n : Nat}:
30 L.subst(Nat, z => {M.dist(1n+bp, a, z) == 0n : Nat}, M.pos(1n+bp, a, 0n), a, IV.pos0(bp, a, ha), M.dist_pos(bp, a, 0n, ha, N.succ_le_lt(0n, 1n+bp, N.zero_le(bp))))
31
32def eq_of_dist0(+bp: Nat, +a: Nat, +j: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +h: {M.dist(1n+bp, a, j) == 0n : Nat}) -> {a == j : Nat}:
33 Equal.trans(Nat, a, M.pos(1n+bp, a, 0n), j, Equal.sym(Nat, M.pos(1n+bp, a, 0n), a, IV.pos0(bp, a, ha)), Equal.trans(Nat, M.pos(1n+bp, a, 0n), M.pos(1n+bp, a, M.dist(1n+bp, a, j)), j, Equal.cong(Nat, Nat, z => M.pos(1n+bp, a, z), 0n, M.dist(1n+bp, a, j), Equal.sym(Nat, M.dist(1n+bp, a, j), 0n, h)), M.pos_dist(bp, a, j, ha, hj)))
34
35def pn_c(+bp: Nat, +a: Nat, +t: Nat, +h: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}, +ht: {Nat.is_lt(t, 1n+bp) == True{} : Bool}, +hne: {Nat.is_eq(t, M.dist(1n+bp, a, h)) == False{} : Bool}, +c: Bool, +hc: {Nat.is_eq(M.pos(1n+bp, a, t), h) == c : Bool}) -> {c == False{} : Bool}:
36 match c:
37 case False{}:
38 {==}
39 case True{}:
40 +e = Equal.trans(Nat, t, M.dist(1n+bp, a, M.pos(1n+bp, a, t)), M.dist(1n+bp, a, h), Equal.sym(Nat, M.dist(1n+bp, a, M.pos(1n+bp, a, t)), t, M.dist_pos(bp, a, t, ha, ht)), Equal.cong(Nat, Nat, z => M.dist(1n+bp, a, z), M.pos(1n+bp, a, t), h, N.eq_from_is_eq(M.pos(1n+bp, a, t), h, hc)))
41 Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_eq(t, M.dist(1n+bp, a, h)), False{}, Equal.sym(Bool, Nat.is_eq(t, M.dist(1n+bp, a, h)), True{}, IS.eq_is_eq(t, M.dist(1n+bp, a, h), e)), hne)))
42
43# the step t < n of a path is at h only when t = dist(a, h)
44def pos_ne(+bp: Nat, +a: Nat, +t: Nat, +h: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}, +ht: {Nat.is_lt(t, 1n+bp) == True{} : Bool}, +hne: {Nat.is_eq(t, M.dist(1n+bp, a, h)) == False{} : Bool}) -> {Nat.is_eq(M.pos(1n+bp, a, t), h) == False{} : Bool}:
45 pn_c(bp, a, t, h, ha, ht, hne, Nat.is_eq(M.pos(1n+bp, a, t), h), {==})
46
47# x + z < x + y: z < y
48def zy_lt(+x: Nat, +y: Nat, +z: Nat, +h: {Nat.is_lt(Nat.add(x, z), Nat.add(x, y)) == True{} : Bool}) -> {Nat.is_lt(z, y) == True{} : Bool}:
49 match x:
50 case 0n:
51 h
52 case 1n+p:
53 zy_lt(p, y, z, h)
54
55def ds_c(+bp: Nat, +a: Nat, +h: Nat, +j: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +hle: {Nat.is_le(M.dist(1n+bp, h, j), M.dist(1n+bp, a, j)) == True{} : Bool}, +pj: {M.pos(1n+bp, a, Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j))) == j : Nat}, +c: Bool, +hc: {Nat.is_lt(Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)), 1n+bp) == c : Bool}) -> {Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)) == M.dist(1n+bp, a, j) : Nat}:
56 match c:
57 case True{}:
58 Equal.trans(Nat, Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)), M.dist(1n+bp, a, M.pos(1n+bp, a, Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)))), M.dist(1n+bp, a, j), Equal.sym(Nat, M.dist(1n+bp, a, M.pos(1n+bp, a, Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)))), Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)), M.dist_pos(bp, a, Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)), ha, hc)), Equal.cong(Nat, Nat, z => M.dist(1n+bp, a, z), M.pos(1n+bp, a, Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j))), j, pj))
59 case False{}:
60 +z = Nat.sub(Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)), 1n+bp)
61 +enz = N.sub_add(Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)), 1n+bp, N.not_lt_le(Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)), 1n+bp, hc))
62 +pz = Equal.trans(Nat, M.pos(1n+bp, a, z), M.pos(1n+bp, a, Nat.add(1n+bp, z)), j, Equal.sym(Nat, M.pos(1n+bp, a, Nat.add(1n+bp, z)), M.pos(1n+bp, a, z), pos_wrap(bp, a, z)), Equal.trans(Nat, M.pos(1n+bp, a, Nat.add(1n+bp, z)), M.pos(1n+bp, a, Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j))), j, Equal.cong(Nat, Nat, w => M.pos(1n+bp, a, w), Nat.add(1n+bp, z), Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)), enz), pj))
63 +hxz = L.subst(Nat, w => {Nat.is_lt(Nat.add(M.dist(1n+bp, a, h), z), w) == True{} : Bool}, Nat.add(1n+bp, z), Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)), enz, N.lt_add_r2(M.dist(1n+bp, a, h), 1n+bp, z, M.dist_lt(bp, a, h)))
64 +hzn = N.lt_trans(z, M.dist(1n+bp, h, j), 1n+bp, zy_lt(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j), z, hxz), M.dist_lt(bp, h, j))
65 +dz = Equal.trans(Nat, M.dist(1n+bp, a, j), M.dist(1n+bp, a, M.pos(1n+bp, a, z)), z, Equal.cong(Nat, Nat, w => M.dist(1n+bp, a, w), j, M.pos(1n+bp, a, z), Equal.sym(Nat, M.pos(1n+bp, a, z), j, pz)), M.dist_pos(bp, a, z, ha, hzn))
66 +hyz = L.subst(Nat, w => {Nat.is_le(M.dist(1n+bp, h, j), w) == True{} : Bool}, M.dist(1n+bp, a, j), z, dz, hle)
67 Empty.absurd({Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)) == M.dist(1n+bp, a, j) : Nat}, L.true_false(Equal.trans(Bool, True{}, Nat.is_le(M.dist(1n+bp, h, j), z), False{}, Equal.sym(Bool, Nat.is_le(M.dist(1n+bp, h, j), z), True{}, hyz), N.lt_not_le(z, M.dist(1n+bp, h, j), zy_lt(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j), z, hxz)))))
68
69# THEOREM: when h lies no further from j than a does, the path a -> j goes through h
70def dist_split(+bp: Nat, +a: Nat, +h: Nat, +j: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +hle: {Nat.is_le(M.dist(1n+bp, h, j), M.dist(1n+bp, a, j)) == True{} : Bool}) -> {Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)) == M.dist(1n+bp, a, j) : Nat}:
71 +x = M.dist(1n+bp, a, h)
72 +y = M.dist(1n+bp, h, j)
73 +pj = Equal.trans(Nat, M.pos(1n+bp, a, Nat.add(x, y)), M.pos(1n+bp, M.pos(1n+bp, a, x), y), j, Equal.sym(Nat, M.pos(1n+bp, M.pos(1n+bp, a, x), y), M.pos(1n+bp, a, Nat.add(x, y)), pos_add(bp, a, x, y)), Equal.trans(Nat, M.pos(1n+bp, M.pos(1n+bp, a, x), y), M.pos(1n+bp, h, y), j, Equal.cong(Nat, Nat, w => M.pos(1n+bp, w, y), M.pos(1n+bp, a, x), h, M.pos_dist(bp, a, h, ha, hh)), M.pos_dist(bp, h, j, hh, hj)))
74 ds_c(bp, a, h, j, ha, hh, hj, hle, pj, Nat.is_lt(Nat.add(x, y), 1n+bp), {==})
75
76# ---- two writes into a bucket list ----
77
78def bupd_over(+xs: List<&2, B.Bk>, +a: Nat, +u: B.Bk, +v: B.Bk) -> {IM.bupd(IM.bupd(xs, a, u), a, v) == IM.bupd(xs, a, v) : List<&2, B.Bk>}:
79 match xs a:
80 case Nil{} _:
81 {==}
82 case Con{c, t} 0n:
83 {==}
84 case Con{c, t} 1n+p:
85 Equal.cong(List<&2, B.Bk>, List<&2, B.Bk>, z => Con{c, z}, IM.bupd(IM.bupd(t, p, u), p, v), IM.bupd(t, p, v), bupd_over(t, p, u, v))
86
87def bupd_comm(+xs: List<&2, B.Bk>, +a: Nat, +b: Nat, +u: B.Bk, +v: B.Bk, +hne: {Nat.is_eq(a, b) == False{} : Bool}) -> {IM.bupd(IM.bupd(xs, a, u), b, v) == IM.bupd(IM.bupd(xs, b, v), a, u) : List<&2, B.Bk>}:
88 match xs a b:
89 case Nil{} _ _:
90 {==}
91 case Con{c, t} 0n 0n:
92 Empty.absurd({IM.bupd(IM.bupd(Con{c, t}, 0n, u), 0n, v) == IM.bupd(IM.bupd(Con{c, t}, 0n, v), 0n, u) : List<&2, B.Bk>}, L.true_false(hne))
93 case Con{c, t} 0n 1n+q:
94 {==}
95 case Con{c, t} 1n+p 0n:
96 {==}
97 case Con{c, t} 1n+p 1n+q:
98 Equal.cong(List<&2, B.Bk>, List<&2, B.Bk>, z => Con{c, z}, IM.bupd(IM.bupd(t, p, u), q, v), IM.bupd(IM.bupd(t, q, v), p, u), bupd_comm(t, p, q, u, v, hne))
99
100def len_bupd(+xs: List<&2, B.Bk>, +a: Nat, +u: B.Bk) -> {SC.length(B.Bk, IM.bupd(xs, a, u)) == SC.length(B.Bk, xs) : Nat}:
101 match xs a:
102 case Nil{} _:
103 {==}
104 case Con{c, t} 0n:
105 {==}
106 case Con{c, t} 1n+p:
107 Equal.cong(Nat, Nat, z => 1n+z, SC.length(B.Bk, IM.bupd(t, p, u)), SC.length(B.Bk, t), len_bupd(t, p, u))