proofs/containers/hash_table/delmv.bend
bend-collections-laws-containers@1.0.0.0 · 194 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/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
6import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
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/state.bend as ST
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/lookup.bend as LK
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/tools.bend as T
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insm.bend as IM
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/rehash.bend as RH
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/ring.bend as RG
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K2
16
17# Moving the scanned bucket b from k into the empty gap h keeps the table a
18# set of copies of the original buckets, keys and links unique, and the
19# number of full buckets.
20
21
22def hlen2(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}) -> {Nat.is_lt(h, SC.length(B.Bk, IM.bupd(V, k, B.BE{}))) == True{} : Bool}:
23 L.subst(Nat, z => {Nat.is_lt(h, z) == True{} : Bool}, SC.length(B.Bk, V), SC.length(B.Bk, IM.bupd(V, k, B.BE{})), Equal.sym(Nat, SC.length(B.Bk, IM.bupd(V, k, B.BE{})), SC.length(B.Bk, V), RG.len_bupd(V, k, B.BE{})), hlh)
24
25def at_vh(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}) -> {B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), h) == b : B.Bk}:
26 IM.at_bupd_same(IM.bupd(V, k, B.BE{}), h, b, hlen2(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk))
27
28def at_vk(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}) -> {B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), k) == B.BE{} : B.Bk}:
29 Equal.trans(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), k), B.at(IM.bupd(V, k, B.BE{}), k), B.BE{}, IM.at_bupd_other(IM.bupd(V, k, B.BE{}), h, b, k, hhk), IM.at_bupd_same(V, k, B.BE{}, hlk))
30
31def at_vo(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +j: Nat, +hh: {Nat.is_eq(h, j) == False{} : Bool}, +hk: {Nat.is_eq(k, j) == False{} : Bool}) -> {B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), j) == B.at(V, j) : B.Bk}:
32 Equal.trans(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), j), B.at(IM.bupd(V, k, B.BE{}), j), B.at(V, j), IM.at_bupd_other(IM.bupd(V, k, B.BE{}), h, b, j, hh), IM.at_bupd_other(V, k, B.BE{}, j, hk))
33
34# ---- copies ----
35
36
37def fm_o(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +src: List<&2, B.Bk>, +m: Nat, +hf: {B.all_lt(B.PFrom{V, src, m}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +hch: {Nat.is_eq(h, j) == False{} : Bool}, +ck: Bool, +hck: {Nat.is_eq(k, j) == ck : Bool}) -> {B.eval(B.PFrom{IM.bupd(IM.bupd(V, k, B.BE{}), h, b), src, m}, j) == True{} : Bool}:
38 match ck:
39 case True{}:
40 +e = Equal.trans(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), j), B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), k), B.BE{}, Equal.cong(Nat, B.Bk, z => B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), z), j, k, Equal.sym(Nat, k, j, N.eq_from_is_eq(k, j, hck))), at_vk(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk))
41 L.subst(B.Bk, y => {B.implies(B.occ(y), B.anyeq(src, m, y)) == True{} : Bool}, B.BE{}, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), j), Equal.sym(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), j), B.BE{}, e), {==})
42 case False{}:
43 L.subst(B.Bk, y => {B.implies(B.occ(y), B.anyeq(src, m, y)) == True{} : Bool}, B.at(V, j), B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), j), Equal.sym(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), j), B.at(V, j), at_vo(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk, j, hch, hck)), B.all_inst(B.PFrom{V, src, m}, n, hf, j, hj))
44
45def fm_k(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +src: List<&2, B.Bk>, +m: Nat, +hf: {B.all_lt(B.PFrom{V, src, m}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +ch: Bool, +hch: {Nat.is_eq(h, j) == ch : Bool}, +hkn: {Nat.is_lt(k, n) == True{} : Bool}) -> {B.eval(B.PFrom{IM.bupd(IM.bupd(V, k, B.BE{}), h, b), src, m}, j) == True{} : Bool}:
46 match ch:
47 case True{}:
48 +e = Equal.trans(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), j), B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), h), b, Equal.cong(Nat, B.Bk, z => B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), z), j, h, Equal.sym(Nat, h, j, N.eq_from_is_eq(h, j, hch))), at_vh(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk))
49 L.subst(B.Bk, y => {B.implies(B.occ(y), B.anyeq(src, m, y)) == True{} : Bool}, b, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), j), Equal.sym(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), j), b, e), L.subst(B.Bk, y => {B.implies(B.occ(y), B.anyeq(src, m, y)) == True{} : Bool}, B.at(V, k), b, hbk, B.all_inst(B.PFrom{V, src, m}, n, hf, k, hkn)))
50 case False{}:
51 fm_o(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk, src, m, hf, j, hj, hch, Nat.is_eq(k, j), {==})
52
53def from_move_m(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +src: List<&2, B.Bk>, +m: Nat, +hf: {B.all_lt(B.PFrom{V, src, m}, n) == True{} : Bool}, +hkn: {Nat.is_lt(k, n) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, n) == True{} : Bool}) -> {B.all_lt(B.PFrom{IM.bupd(IM.bupd(V, k, B.BE{}), h, b), src, m}, q) == True{} : Bool}:
54 match q:
55 case 0n:
56 {==}
57 case 1n+j:
58 +hj = N.succ_le_lt(j, n, hq)
59 L.and_intro(B.eval(B.PFrom{IM.bupd(IM.bupd(V, k, B.BE{}), h, b), src, m}, j), B.all_lt(B.PFrom{IM.bupd(IM.bupd(V, k, B.BE{}), h, b), src, m}, j), fm_k(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk, src, m, hf, j, hj, Nat.is_eq(h, j), {==}, hkn), from_move_m(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk, src, m, hf, hkn, j, N.lt_le(j, n, hj)))
60
61# THEOREM: after the move every full bucket is still a copy
62def from_move(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +src: List<&2, B.Bk>, +m: Nat, +hf: {B.all_lt(B.PFrom{V, src, m}, n) == True{} : Bool}, +hkn: {Nat.is_lt(k, n) == True{} : Bool}) -> {B.all_lt(B.PFrom{IM.bupd(IM.bupd(V, k, B.BE{}), h, b), src, m}, n) == True{} : Bool}:
63 from_move_m(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk, src, m, hf, hkn, n, N.le_refl(n))
64
65def tw_c(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +x: B.Bk, +hox: {B.occ(x) == True{} : Bool}, +p: Nat, +hp: {Nat.is_lt(p, n) == True{} : Bool}, +hat: {B.at(V, p) == x : B.Bk}, +hhn: {Nat.is_lt(h, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(k, p) == c : Bool}) -> {B.anyeq(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n, x) == True{} : Bool}:
66 match c:
67 case True{}:
68 +ebx = Equal.trans(B.Bk, b, B.at(V, k), x, Equal.sym(B.Bk, B.at(V, k), b, hbk), Equal.trans(B.Bk, B.at(V, k), B.at(V, p), x, Equal.cong(Nat, B.Bk, z => B.at(V, z), k, p, N.eq_from_is_eq(k, p, hc)), hat))
69 RH.anyeq_intro(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n, x, h, hhn, L.subst(B.Bk, y => {B.bk_eq(y, x) == True{} : Bool}, x, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), h), Equal.sym(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), h), x, Equal.trans(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), h), b, x, at_vh(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk), ebx)), RH.bk_refl(x)))
70 case False{}:
71 +hpo = L.subst(B.Bk, y => {B.occ(y) == True{} : Bool}, x, B.at(V, p), Equal.sym(B.Bk, B.at(V, p), x, hat), hox)
72 +hhp = RH.ne_occ(V, h, hzh, p, hpo, Nat.is_eq(h, p), {==})
73 RH.anyeq_intro(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n, x, p, hp, L.subst(B.Bk, y => {B.bk_eq(y, x) == True{} : Bool}, x, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), p), Equal.sym(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), p), x, Equal.trans(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), p), B.at(V, p), x, at_vo(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk, p, hhp, hc), hat)), RH.bk_refl(x)))
74
75def tw(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +x: B.Bk, +hox: {B.occ(x) == True{} : Bool}, +hhn: {Nat.is_lt(h, n) == True{} : Bool}, w0: RH.EqAt(V, n, x)) -> {B.anyeq(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n, x) == True{} : Bool}:
76 match w0:
77 case Tuple{+p, Tuple{+hp, +hat}}:
78 tw_c(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk, x, hox, p, hp, hat, hhn, Nat.is_eq(k, p), {==})
79
80def tm_i(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +hhn: {Nat.is_lt(h, n) == True{} : Bool}, +x: B.Bk, +hx: {B.implies(B.occ(x), B.anyeq(V, n, x)) == True{} : Bool}, +c: Bool, +hc: {B.occ(x) == c : Bool}) -> {B.implies(c, B.anyeq(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n, x)) == True{} : Bool}:
81 match c:
82 case False{}:
83 {==}
84 case True{}:
85 tw(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk, x, hc, hhn, RH.find_eq(V, n, x, B.imp_elim(B.occ(x), B.anyeq(V, n, x), hx, hc)))
86
87def to_move_m(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +src: List<&2, B.Bk>, +ms: Nat, +ht: {B.all_lt(B.PTo{src, V, n}, ms) == True{} : Bool}, +hhn: {Nat.is_lt(h, n) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, ms) == True{} : Bool}) -> {B.all_lt(B.PTo{src, IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n}, q) == True{} : Bool}:
88 match q:
89 case 0n:
90 {==}
91 case 1n+j:
92 +hj = N.succ_le_lt(j, ms, hq)
93 +x = B.at(src, j)
94 L.and_intro(B.eval(B.PTo{src, IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n}, j), B.all_lt(B.PTo{src, IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n}, j), L.subst(Bool, c => {B.implies(c, B.anyeq(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n, x)) == True{} : Bool}, B.occ(x), B.occ(x), {==}, tm_i(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk, hhn, x, B.all_inst(B.PTo{src, V, n}, ms, ht, j, hj), B.occ(x), {==})), to_move_m(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk, src, ms, ht, hhn, j, N.lt_le(j, ms, hj)))
95
96# THEOREM: after the move every original bucket still has a copy
97def to_move(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +src: List<&2, B.Bk>, +ms: Nat, +ht: {B.all_lt(B.PTo{src, V, n}, ms) == True{} : Bool}, +hhn: {Nat.is_lt(h, n) == True{} : Bool}) -> {B.all_lt(B.PTo{src, IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n}, ms) == True{} : Bool}:
98 to_move_m(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk, src, ms, ht, hhn, ms, N.le_refl(ms))
99
100# ---- uniqueness ----
101
102def uqr_b(+bs: List<&2, B.Bk>, +k: Nat, +hlk: {Nat.is_lt(k, SC.length(B.Bk, bs)) == True{} : Bool}, +j: Nat, +x: B.Bk, +hu: {B.uq_b(bs, j, x) == True{} : Bool}) -> {B.uq_b(IM.bupd(bs, k, B.BE{}), j, x) == True{} : Bool}:
103 match x:
104 case B.BE{}:
105 {==}
106 case B.BF{w, +l, +key}:
107 L.and_intro(B.nohb(IM.bupd(bs, k, B.BE{}), key, j), B.nolb(IM.bupd(bs, k, B.BE{}), l, j), IM.nohb_up(bs, k, B.BE{}, hlk, key, {==}, j, L.and_left(B.nohb(bs, key, j), B.nolb(bs, l, j), hu)), IM.nolb_up(bs, k, B.BE{}, hlk, l, {==}, j, L.and_right(B.nohb(bs, key, j), B.nolb(bs, l, j), hu)))
108
109def uqr_i(+bs: List<&2, B.Bk>, +k: Nat, +hlk: {Nat.is_lt(k, SC.length(B.Bk, bs)) == True{} : Bool}, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(k, j) == c : Bool}) -> {B.eval(B.PUniq{IM.bupd(bs, k, B.BE{})}, j) == True{} : Bool}:
110 match c:
111 case True{}:
112 L.subst(B.Bk, y => {B.uq_b(IM.bupd(bs, k, B.BE{}), j, y) == True{} : Bool}, B.BE{}, B.at(IM.bupd(bs, k, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(bs, k, B.BE{}), j), B.BE{}, IM.at_bu_eq(bs, k, B.BE{}, hlk, j, hc)), {==})
113 case False{}:
114 L.subst(B.Bk, y => {B.uq_b(IM.bupd(bs, k, B.BE{}), j, y) == True{} : Bool}, B.at(bs, j), B.at(IM.bupd(bs, k, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(bs, k, B.BE{}), j), B.at(bs, j), IM.at_bupd_other(bs, k, B.BE{}, j, hc)), uqr_b(bs, k, hlk, j, B.at(bs, j), B.all_inst(B.PUniq{bs}, n, huq, j, hj)))
115
116# THEOREM: emptying a bucket keeps keys and links unique
117def uq_rm(+bs: List<&2, B.Bk>, +k: Nat, +hlk: {Nat.is_lt(k, SC.length(B.Bk, bs)) == True{} : Bool}, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PUniq{IM.bupd(bs, k, B.BE{})}, m) == True{} : Bool}:
118 match m:
119 case 0n:
120 {==}
121 case 1n+j:
122 +hj = N.succ_le_lt(j, n, hm)
123 L.and_intro(B.eval(B.PUniq{IM.bupd(bs, k, B.BE{})}, j), B.all_lt(B.PUniq{IM.bupd(bs, k, B.BE{})}, j), uqr_i(bs, k, hlk, n, huq, j, hj, Nat.is_eq(k, j), {==}), uq_rm(bs, k, hlk, n, huq, j, N.lt_le(j, n, hj)))
124
125
126def pno_rm_i(+V: List<&2, B.Bk>, +n: Nat, +k: Nat, +hkn: {Nat.is_lt(k, n) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{V}, n) == True{} : Bool}, +w: U32, +l: U32, +key: String, +hbk: {B.at(V, k) == B.BF{w, l, key} : B.Bk}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(k, j) == c : Bool}) -> {B.eval(B.PNo{IM.bupd(V, k, B.BE{}), key}, j) == True{} : Bool}:
127 match c:
128 case True{}:
129 L.subst(B.Bk, y => {Bool.not(B.hold(key, y)) == True{} : Bool}, B.BE{}, B.at(IM.bupd(V, k, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(V, k, B.BE{}), j), B.BE{}, IM.at_bu_eq(V, k, B.BE{}, hlk, j, hc)), {==})
130 case False{}:
131 +hk = L.subst(B.Bk, y => {B.hold(key, y) == True{} : Bool}, B.BF{w, l, key}, B.at(V, k), Equal.sym(B.Bk, B.at(V, k), B.BF{w, l, key}, hbk), K2.str_refl(key))
132 L.subst(B.Bk, y => {Bool.not(B.hold(key, y)) == True{} : Bool}, B.at(V, j), B.at(IM.bupd(V, k, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(V, k, B.BE{}), j), B.at(V, j), IM.at_bupd_other(V, k, B.BE{}, j, hc)), LK.other(V, n, key, huq, k, hkn, hk, j, hj, N.is_eq_sym_false(k, j, hc)))
133
134def pno_rm(+V: List<&2, B.Bk>, +n: Nat, +k: Nat, +hkn: {Nat.is_lt(k, n) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{V}, n) == True{} : Bool}, +w: U32, +l: U32, +key: String, +hbk: {B.at(V, k) == B.BF{w, l, key} : B.Bk}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PNo{IM.bupd(V, k, B.BE{}), key}, m) == True{} : Bool}:
135 match m:
136 case 0n:
137 {==}
138 case 1n+j:
139 +hj = N.succ_le_lt(j, n, hm)
140 L.and_intro(B.eval(B.PNo{IM.bupd(V, k, B.BE{}), key}, j), B.all_lt(B.PNo{IM.bupd(V, k, B.BE{}), key}, j), pno_rm_i(V, n, k, hkn, hlk, huq, w, l, key, hbk, j, hj, Nat.is_eq(k, j), {==}), pno_rm(V, n, k, hkn, hlk, huq, w, l, key, hbk, j, N.lt_le(j, n, hj)))
141
142def nsr_o(+V: List<&2, B.Bk>, +n: Nat, +k: Nat, +hkn: {Nat.is_lt(k, n) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{V}, n) == True{} : Bool}, +w: U32, +l: U32, +key: String, +hbk: {B.at(V, k) == B.BF{w, l, key} : B.Bk}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +hc: {Nat.is_eq(k, j) == False{} : Bool}, +o: Bool, +ho: {B.occ(B.at(V, j)) == o : Bool}) -> {Bool.not(Bool.and(o, Nat.is_eq(UD.v(H.slot(B.lnk(B.at(V, j)))), UD.v(H.slot(l))))) == True{} : Bool}:
143 match o:
144 case False{}:
145 {==}
146 case True{}:
147 +ok = L.subst(B.Bk, y => {B.occ(y) == True{} : Bool}, B.BF{w, l, key}, B.at(V, k), Equal.sym(B.Bk, B.at(V, k), B.BF{w, l, key}, hbk), {==})
148 +ne = T.slot_ne(V, n, huq, k, j, hkn, hj, N.is_eq_sym_false(k, j, hc), ok, ho)
149 +ne2 = L.subst(B.Bk, y => {Nat.is_eq(UD.v(H.slot(B.lnk(B.at(V, j)))), UD.v(H.slot(B.lnk(y)))) == False{} : Bool}, B.at(V, k), B.BF{w, l, key}, hbk, ne)
150 IM.not_f(Nat.is_eq(UD.v(H.slot(B.lnk(B.at(V, j)))), UD.v(H.slot(l))), ne2)
151
152def nsr_i(+V: List<&2, B.Bk>, +n: Nat, +k: Nat, +hkn: {Nat.is_lt(k, n) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{V}, n) == True{} : Bool}, +w: U32, +l: U32, +key: String, +hbk: {B.at(V, k) == B.BF{w, l, key} : B.Bk}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(k, j) == c : Bool}) -> {Bool.not(Bool.and(B.occ(B.at(IM.bupd(V, k, B.BE{}), j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(IM.bupd(V, k, B.BE{}), j)))), UD.v(H.slot(l))))) == True{} : Bool}:
153 match c:
154 case True{}:
155 L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), UD.v(H.slot(l))))) == True{} : Bool}, B.BE{}, B.at(IM.bupd(V, k, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(V, k, B.BE{}), j), B.BE{}, IM.at_bu_eq(V, k, B.BE{}, hlk, j, hc)), {==})
156 case False{}:
157 L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), UD.v(H.slot(l))))) == True{} : Bool}, B.at(V, j), B.at(IM.bupd(V, k, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(V, k, B.BE{}), j), B.at(V, j), IM.at_bupd_other(V, k, B.BE{}, j, hc)), nsr_o(V, n, k, hkn, hlk, huq, w, l, key, hbk, j, hj, hc, B.occ(B.at(V, j)), {==}))
158
159def ns_rm(+V: List<&2, B.Bk>, +n: Nat, +k: Nat, +hkn: {Nat.is_lt(k, n) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{V}, n) == True{} : Bool}, +w: U32, +l: U32, +key: String, +hbk: {B.at(V, k) == B.BF{w, l, key} : B.Bk}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {ST.noslot(IM.bupd(V, k, B.BE{}), UD.v(H.slot(l)), m) == True{} : Bool}:
160 match m:
161 case 0n:
162 {==}
163 case 1n+j:
164 +hj = N.succ_le_lt(j, n, hm)
165 L.and_intro(Bool.not(Bool.and(B.occ(B.at(IM.bupd(V, k, B.BE{}), j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(IM.bupd(V, k, B.BE{}), j)))), UD.v(H.slot(l))))), ST.noslot(IM.bupd(V, k, B.BE{}), UD.v(H.slot(l)), j), nsr_i(V, n, k, hkn, hlk, huq, w, l, key, hbk, j, hj, Nat.is_eq(k, j), {==}), ns_rm(V, n, k, hkn, hlk, huq, w, l, key, hbk, j, N.lt_le(j, n, hj)))
166
167
168# THEOREM: moving a bucket into an empty bucket keeps keys and links unique
169def uq_move(+V: List<&2, B.Bk>, +n: Nat, +k: Nat, +hkn: {Nat.is_lt(k, n) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{V}, n) == True{} : Bool}, +w: U32, +l: U32, +key: String, +hbk: {B.at(V, k) == B.BF{w, l, key} : B.Bk}, +h: Nat, +hhn: {Nat.is_lt(h, n) == True{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}) -> {B.all_lt(B.PUniq{IM.bupd(IM.bupd(V, k, B.BE{}), h, B.BF{w, l, key})}, n) == True{} : Bool}:
170 +hl2 = L.subst(Nat, z => {Nat.is_lt(h, z) == True{} : Bool}, SC.length(B.Bk, V), SC.length(B.Bk, IM.bupd(V, k, B.BE{})), Equal.sym(Nat, SC.length(B.Bk, IM.bupd(V, k, B.BE{})), SC.length(B.Bk, V), RG.len_bupd(V, k, B.BE{})), hlh)
171 IM.uq_up(IM.bupd(V, k, B.BE{}), h, hl2, w, l, key, n, hhn, uq_rm(V, k, hlk, n, huq, n, N.le_refl(n)), pno_rm(V, n, k, hkn, hlk, huq, w, l, key, hbk, n, N.le_refl(n)), ns_rm(V, n, k, hkn, hlk, huq, w, l, key, hbk, n, N.le_refl(n)))
172
173# ---- the count ----
174
175def bupd_self(+xs: List<&2, B.Bk>, +k: Nat) -> {IM.bupd(xs, k, B.at(xs, k)) == xs : List<&2, B.Bk>}:
176 match xs k:
177 case Nil{} _:
178 {==}
179 case Con{c, t} 0n:
180 {==}
181 case Con{c, t} 1n+p:
182 Equal.cong(List<&2, B.Bk>, List<&2, B.Bk>, z => Con{c, z}, IM.bupd(t, p, B.at(t, p)), t, bupd_self(t, p))
183
184# emptying a full bucket k < n: one fewer full bucket
185def occn_rm(+V: List<&2, B.Bk>, +n: Nat, +k: Nat, +hkn: {Nat.is_lt(k, n) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +hok: {B.occ(B.at(V, k)) == True{} : Bool}) -> {IV.occn(V, n) == 1n+IV.occn(IM.bupd(V, k, B.BE{}), n) : Nat}:
186 +hl2 = L.subst(Nat, z => {Nat.is_lt(k, z) == True{} : Bool}, SC.length(B.Bk, V), SC.length(B.Bk, IM.bupd(V, k, B.BE{})), Equal.sym(Nat, SC.length(B.Bk, IM.bupd(V, k, B.BE{})), SC.length(B.Bk, V), RG.len_bupd(V, k, B.BE{})), hlk)
187 +ev = Equal.trans(List<&2, B.Bk>, IM.bupd(IM.bupd(V, k, B.BE{}), k, B.at(V, k)), IM.bupd(V, k, B.at(V, k)), V, RG.bupd_over(V, k, B.BE{}, B.at(V, k)), bupd_self(V, k))
188 Equal.trans(Nat, IV.occn(V, n), IV.occn(IM.bupd(IM.bupd(V, k, B.BE{}), k, B.at(V, k)), n), 1n+IV.occn(IM.bupd(V, k, B.BE{}), n), Equal.cong(List<&2, B.Bk>, Nat, z => IV.occn(z, n), V, IM.bupd(IM.bupd(V, k, B.BE{}), k, B.at(V, k)), Equal.sym(List<&2, B.Bk>, IM.bupd(IM.bupd(V, k, B.BE{}), k, B.at(V, k)), V, ev)), IM.occn_up(IM.bupd(V, k, B.BE{}), k, B.at(V, k), hok, hl2, IM.at_bupd_same(V, k, B.BE{}, hlk), n, hkn))
189
190# THEOREM: the move keeps the number of full buckets
191def occn_move(+V: List<&2, B.Bk>, +n: Nat, +h: Nat, +k: Nat, +b: B.Bk, +hbk: {B.at(V, k) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hzh: {B.at(V, h) == B.BE{} : B.Bk}, +hhk: {Nat.is_eq(h, k) == False{} : Bool}, +hlh: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(k, SC.length(B.Bk, V)) == True{} : Bool}, +hkn: {Nat.is_lt(k, n) == True{} : Bool}, +hhn: {Nat.is_lt(h, n) == True{} : Bool}) -> {IV.occn(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n) == IV.occn(V, n) : Nat}:
192 +hok = L.subst(B.Bk, y => {B.occ(y) == True{} : Bool}, b, B.at(V, k), Equal.sym(B.Bk, B.at(V, k), b, hbk), hbo)
193 +hzr = Equal.trans(B.Bk, B.at(IM.bupd(V, k, B.BE{}), h), B.at(V, h), B.BE{}, IM.at_bupd_other(V, k, B.BE{}, h, N.is_eq_sym_false(h, k, hhk)), hzh)
194 Equal.trans(Nat, IV.occn(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n), 1n+IV.occn(IM.bupd(V, k, B.BE{}), n), IV.occn(V, n), IM.occn_up(IM.bupd(V, k, B.BE{}), h, b, hbo, hlen2(V, n, h, k, b, hbk, hbo, hzh, hhk, hlh, hlk), hzr, n, hhn), Equal.sym(Nat, IV.occn(V, n), 1n+IV.occn(IM.bupd(V, k, B.BE{}), n), occn_rm(V, n, k, hkn, hlk, hok)))