proofs/containers/hash_table/speclem.bend
bend-collections-laws-containers@1.0.0.0 · 190 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/spec/containers/hash_table.bend as S
4import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
5
6# Facts about the specification's association-list map.
7
8def pick_t(~A: Data, +c: Bool, +h: {c == True{} : Bool}, +x: A, +y: A) -> {Bool.pick(A, c, x, y) == x : A}:
9 match c:
10 case True{}:
11 {==}
12 case False{}:
13 Empty.absurd({Bool.pick(A, False{}, x, y) == x : A}, L.false_true(h))
14
15def pick_f(~A: Data, +c: Bool, +h: {c == False{} : Bool}, +x: A, +y: A) -> {Bool.pick(A, c, x, y) == y : A}:
16 match c:
17 case True{}:
18 Empty.absurd({Bool.pick(A, True{}, x, y) == y : A}, L.true_false(h))
19 case False{}:
20 {==}
21
22# two keys equal to the same key are equal to each other, by str_eq
23def eq_tr(+a: String, +b: String, +c: String, +hab: {S.str_eq(a, b) == True{} : Bool}, +e: Bool, +he: {S.str_eq(b, c) == e : Bool}) -> {S.str_eq(a, c) == e : Bool}:
24 L.subst(String, z => {S.str_eq(z, c) == e : Bool}, b, a, Equal.sym(String, a, b, K.str_eq_of(a, b, hab)), he)
25
26# comparing with keys equal by str_eq agrees
27def eq_tr2(+j: String, +key: String, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}) -> {S.str_eq(j, key) == S.str_eq(j, q) : Bool}:
28 Equal.cong(String, Bool, z => S.str_eq(j, z), key, q, K.str_eq_of(key, q, hq))
29
30# ---- set ----
31
32def ls_same_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +c: Bool, +hc: {S.str_eq(j, key) == c : Bool}, rec: @hc2: {S.str_eq(j, key) == False{} : Bool} -> {S.lookup(~V, S.set(~V, t, key, x), q) == Some{x} : Maybe<&2, V>}) -> {S.lookup(~V, Bool.pick(List<&2, S.Entry<V>>, c, Con{S.E{key, x}, t}, Con{S.E{j, v}, S.set(~V, t, key, x)}), q) == Some{x} : Maybe<&2, V>}:
33 match c:
34 case True{}:
35 pick_t(~Maybe<&2, V>, S.str_eq(key, q), hq, Some{x}, S.lookup(~V, t, q))
36 case False{}:
37 +jq = eq_tr(q, key, j, K.str_eq_true(q, key, Equal.sym(String, key, q, K.str_eq_of(key, q, hq))), False{}, Equal.trans(Bool, S.str_eq(key, j), S.str_eq(j, key), False{}, K.str_sym(key, j), hc))
38 +jq2 = Equal.trans(Bool, S.str_eq(j, q), S.str_eq(q, j), False{}, K.str_sym(j, q), jq)
39 Equal.trans(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, S.set(~V, t, key, x), q)), S.lookup(~V, S.set(~V, t, key, x), q), Some{x}, pick_f(~Maybe<&2, V>, S.str_eq(j, q), jq2, Some{v}, S.lookup(~V, S.set(~V, t, key, x), q)), rec(hc))
40
41# looking up the key just set (or any key equal to it)
42def lookup_set_same(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}) -> {S.lookup(~V, S.set(~V, m, key, x), q) == Some{x} : Maybe<&2, V>}:
43 match m:
44 case Nil{}:
45 pick_t(~Maybe<&2, V>, S.str_eq(key, q), hq, Some{x}, None{})
46 case Con{S.E{+j, +v}, +t}:
47 ls_same_c(~V, j, v, t, key, x, q, hq, S.str_eq(j, key), {==}, hc2 => lookup_set_same(~V, t, key, x, q, hq))
48
49def ls_other_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +c: Bool, +hc: {S.str_eq(j, key) == c : Bool}, +ih: {S.lookup(~V, S.set(~V, t, key, x), q) == S.lookup(~V, t, q) : Maybe<&2, V>}) -> {S.lookup(~V, Bool.pick(List<&2, S.Entry<V>>, c, Con{S.E{key, x}, t}, Con{S.E{j, v}, S.set(~V, t, key, x)}), q) == Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)) : Maybe<&2, V>}:
50 match c:
51 case True{}:
52 +jq = eq_tr(j, key, q, hc, False{}, hq)
53 Equal.trans(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(key, q), Some{x}, S.lookup(~V, t, q)), S.lookup(~V, t, q), Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)), pick_f(~Maybe<&2, V>, S.str_eq(key, q), hq, Some{x}, S.lookup(~V, t, q)), Equal.sym(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)), S.lookup(~V, t, q), pick_f(~Maybe<&2, V>, S.str_eq(j, q), jq, Some{v}, S.lookup(~V, t, q))))
54 case False{}:
55 Equal.cong(Maybe<&2, V>, Maybe<&2, V>, z => Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, z), S.lookup(~V, S.set(~V, t, key, x), q), S.lookup(~V, t, q), ih)
56
57# setting key leaves every other key's lookup
58def lookup_set_other(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}) -> {S.lookup(~V, S.set(~V, m, key, x), q) == S.lookup(~V, m, q) : Maybe<&2, V>}:
59 match m:
60 case Nil{}:
61 pick_f(~Maybe<&2, V>, S.str_eq(key, q), hq, Some{x}, None{})
62 case Con{S.E{+j, +v}, +t}:
63 ls_other_c(~V, j, v, t, key, x, q, hq, S.str_eq(j, key), {==}, lookup_set_other(~V, t, key, x, q, hq))
64
65def lr_other_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry<V>>, +key: String, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +c: Bool, +hc: {S.str_eq(j, key) == c : Bool}, +ih: {S.lookup(~V, S.remove(~V, t, key), q) == S.lookup(~V, t, q) : Maybe<&2, V>}) -> {S.lookup(~V, Bool.pick(List<&2, S.Entry<V>>, c, t, Con{S.E{j, v}, S.remove(~V, t, key)}), q) == Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)) : Maybe<&2, V>}:
66 match c:
67 case True{}:
68 Equal.sym(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)), S.lookup(~V, t, q), pick_f(~Maybe<&2, V>, S.str_eq(j, q), eq_tr(j, key, q, hc, False{}, hq), Some{v}, S.lookup(~V, t, q)))
69 case False{}:
70 Equal.cong(Maybe<&2, V>, Maybe<&2, V>, z => Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, z), S.lookup(~V, S.remove(~V, t, key), q), S.lookup(~V, t, q), ih)
71
72# removing key leaves every other key's lookup
73def lookup_remove_other(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}) -> {S.lookup(~V, S.remove(~V, m, key), q) == S.lookup(~V, m, q) : Maybe<&2, V>}:
74 match m:
75 case Nil{}:
76 {==}
77 case Con{S.E{+j, +v}, +t}:
78 lr_other_c(~V, j, v, t, key, q, hq, S.str_eq(j, key), {==}, lookup_remove_other(~V, t, key, q, hq))
79
80def or_false_l(+a: Bool, +b: Bool, +h: {Bool.or(a, b) == False{} : Bool}) -> {a == False{} : Bool}:
81 match a:
82 case True{}:
83 Empty.absurd({True{} == False{} : Bool}, L.true_false(h))
84 case False{}:
85 {==}
86
87def or_false_r(+a: Bool, +b: Bool, +h: {Bool.or(a, b) == False{} : Bool}) -> {b == False{} : Bool}:
88 match a:
89 case True{}:
90 Empty.absurd({b == False{} : Bool}, L.true_false(h))
91 case False{}:
92 h
93
94# a key not among the keys has no value
95def lookup_not_mem(~V: Data, +m: List<&2, S.Entry<V>>, +q: String, +h: {S.mem(q, S.keys(~V, m)) == False{} : Bool}) -> {S.lookup(~V, m, q) == None{} : Maybe<&2, V>}:
96 match m:
97 case Nil{}:
98 {==}
99 case Con{S.E{+j, +v}, +t}:
100 Equal.trans(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)), S.lookup(~V, t, q), None{}, pick_f(~Maybe<&2, V>, S.str_eq(j, q), or_false_l(S.str_eq(j, q), S.mem(q, S.keys(~V, t)), h), Some{v}, S.lookup(~V, t, q)), lookup_not_mem(~V, t, q, or_false_r(S.str_eq(j, q), S.mem(q, S.keys(~V, t)), h)))
101
102def lr_same_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry<V>>, +key: String, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +hnm: {Bool.not(S.mem(j, S.keys(~V, t))) == True{} : Bool}, +c: Bool, +hc: {S.str_eq(j, key) == c : Bool}, rec: @hc2: {S.str_eq(j, key) == False{} : Bool} -> {S.lookup(~V, S.remove(~V, t, key), q) == None{} : Maybe<&2, V>}) -> {S.lookup(~V, Bool.pick(List<&2, S.Entry<V>>, c, t, Con{S.E{j, v}, S.remove(~V, t, key)}), q) == None{} : Maybe<&2, V>}:
103 match c:
104 case True{}:
105 +ejq = K.str_eq_of(j, q, eq_tr(j, key, q, hc, True{}, hq))
106 lookup_not_mem(~V, t, q, L.subst(String, z => {S.mem(z, S.keys(~V, t)) == False{} : Bool}, j, q, ejq, K.not_true_eq(S.mem(j, S.keys(~V, t)), hnm)))
107 case False{}:
108 +jq = Equal.trans(Bool, S.str_eq(j, q), S.str_eq(j, key), False{}, Equal.sym(Bool, S.str_eq(j, key), S.str_eq(j, q), eq_tr2(j, key, q, hq)), hc)
109 Equal.trans(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, S.remove(~V, t, key), q)), S.lookup(~V, S.remove(~V, t, key), q), None{}, pick_f(~Maybe<&2, V>, S.str_eq(j, q), jq, Some{v}, S.lookup(~V, S.remove(~V, t, key), q)), rec(hc))
110
111# with keys unique, a removed key has no value
112def lookup_remove_same(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +hnd: {S.nodup(S.keys(~V, m)) == True{} : Bool}) -> {S.lookup(~V, S.remove(~V, m, key), q) == None{} : Maybe<&2, V>}:
113 match m:
114 case Nil{}:
115 {==}
116 case Con{S.E{+j, +v}, +t}:
117 lr_same_c(~V, j, v, t, key, q, hq, L.and_left(Bool.not(S.mem(j, S.keys(~V, t))), S.nodup(S.keys(~V, t)), hnd), S.str_eq(j, key), {==}, hc2 => lookup_remove_same(~V, t, key, q, hq, L.and_right(Bool.not(S.mem(j, S.keys(~V, t))), S.nodup(S.keys(~V, t)), hnd)))
118
119# ---- sizes ----
120
121def none_pick(~V: Data, +c: Bool, +v: V, +r: Maybe<&2, V>, +h: {Bool.pick(Maybe<&2, V>, c, Some{v}, r) == None{} : Maybe<&2, V>}) -> {c == False{} : Bool} & {r == None{} : Maybe<&2, V>}:
122 match c:
123 case True{}:
124 Empty.absurd({True{} == False{} : Bool} & {r == None{} : Maybe<&2, V>}, L.none_some(V, v, Equal.sym(Maybe<&2, V>, Some{v}, None{}, h)))
125 case False{}:
126 ({==}, h)
127
128def ssn_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry<V>>, +key: String, +x: V, +c: Bool, +hc: {c == False{} : Bool}, +ih: {S.size(~V, S.set(~V, t, key, x)) == 1n+S.size(~V, t) : Nat}) -> {S.size(~V, Bool.pick(List<&2, S.Entry<V>>, c, Con{S.E{key, x}, t}, Con{S.E{j, v}, S.set(~V, t, key, x)})) == 2n+S.size(~V, t) : Nat}:
129 match c:
130 case True{}:
131 Empty.absurd({S.size(~V, Con{S.E{key, x}, t}) == 2n+S.size(~V, t) : Nat}, L.true_false(hc))
132 case False{}:
133 Equal.cong(Nat, Nat, z => 1n+z, S.size(~V, S.set(~V, t, key, x)), 1n+S.size(~V, t), ih)
134
135# setting an absent key adds one entry
136def size_set_new(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V, +h: {S.lookup(~V, m, key) == None{} : Maybe<&2, V>}) -> {S.size(~V, S.set(~V, m, key, x)) == 1n+S.size(~V, m) : Nat}:
137 match m:
138 case Nil{}:
139 {==}
140 case Con{S.E{+j, +v}, +t}:
141 +c0 = Pair.fst({S.str_eq(j, key) == False{} : Bool}, {S.lookup(~V, t, key) == None{} : Maybe<&2, V>}, none_pick(~V, S.str_eq(j, key), v, S.lookup(~V, t, key), h))
142 +r0 = Pair.snd({S.str_eq(j, key) == False{} : Bool}, {S.lookup(~V, t, key) == None{} : Maybe<&2, V>}, none_pick(~V, S.str_eq(j, key), v, S.lookup(~V, t, key), h))
143 ssn_c(~V, j, v, t, key, x, S.str_eq(j, key), c0, size_set_new(~V, t, key, x, r0))
144
145def sso_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry<V>>, +key: String, +x: V, +v0: V, +c: Bool, +h: {Bool.pick(Maybe<&2, V>, c, Some{v}, S.lookup(~V, t, key)) == Some{v0} : Maybe<&2, V>}, rec: @h2: {S.lookup(~V, t, key) == Some{v0} : Maybe<&2, V>} -> {S.size(~V, S.set(~V, t, key, x)) == S.size(~V, t) : Nat}) -> {S.size(~V, Bool.pick(List<&2, S.Entry<V>>, c, Con{S.E{key, x}, t}, Con{S.E{j, v}, S.set(~V, t, key, x)})) == 1n+S.size(~V, t) : Nat}:
146 match c:
147 case True{}:
148 {==}
149 case False{}:
150 Equal.cong(Nat, Nat, z => 1n+z, S.size(~V, S.set(~V, t, key, x)), S.size(~V, t), rec(h))
151
152# setting a present key keeps the size
153def size_set_old(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V, +v0: V, +h: {S.lookup(~V, m, key) == Some{v0} : Maybe<&2, V>}) -> {S.size(~V, S.set(~V, m, key, x)) == S.size(~V, m) : Nat}:
154 match m:
155 case Nil{}:
156 Empty.absurd({S.size(~V, S.set(~V, Nil{}, key, x)) == S.size(~V, Nil{}) : Nat}, L.none_some(V, v0, h))
157 case Con{S.E{+j, +v}, +t}:
158 sso_c(~V, j, v, t, key, x, v0, S.str_eq(j, key), h, h2 => size_set_old(~V, t, key, x, v0, h2))
159
160def sro_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry<V>>, +key: String, +v0: V, +c: Bool, +h: {Bool.pick(Maybe<&2, V>, c, Some{v}, S.lookup(~V, t, key)) == Some{v0} : Maybe<&2, V>}, rec: @h2: {S.lookup(~V, t, key) == Some{v0} : Maybe<&2, V>} -> {1n+S.size(~V, S.remove(~V, t, key)) == S.size(~V, t) : Nat}) -> {1n+S.size(~V, Bool.pick(List<&2, S.Entry<V>>, c, t, Con{S.E{j, v}, S.remove(~V, t, key)})) == 1n+S.size(~V, t) : Nat}:
161 match c:
162 case True{}:
163 {==}
164 case False{}:
165 Equal.cong(Nat, Nat, z => 1n+z, 1n+S.size(~V, S.remove(~V, t, key)), S.size(~V, t), rec(h))
166
167# removing a present key drops one entry
168def size_remove_old(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +v0: V, +h: {S.lookup(~V, m, key) == Some{v0} : Maybe<&2, V>}) -> {1n+S.size(~V, S.remove(~V, m, key)) == S.size(~V, m) : Nat}:
169 match m:
170 case Nil{}:
171 Empty.absurd({1n+S.size(~V, S.remove(~V, Nil{}, key)) == S.size(~V, Nil{}) : Nat}, L.none_some(V, v0, h))
172 case Con{S.E{+j, +v}, +t}:
173 sro_c(~V, j, v, t, key, v0, S.str_eq(j, key), h, h2 => size_remove_old(~V, t, key, v0, h2))
174
175def rn_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry<V>>, +key: String, +c: Bool, +hc: {c == False{} : Bool}, +ih: {S.remove(~V, t, key) == t : List<&2, S.Entry<V>>}) -> {Bool.pick(List<&2, S.Entry<V>>, c, t, Con{S.E{j, v}, S.remove(~V, t, key)}) == Con{S.E{j, v}, t} : List<&2, S.Entry<V>>}:
176 match c:
177 case True{}:
178 Empty.absurd({t == Con{S.E{j, v}, t} : List<&2, S.Entry<V>>}, L.true_false(hc))
179 case False{}:
180 Equal.cong(List<&2, S.Entry<V>>, List<&2, S.Entry<V>>, z => Con{S.E{j, v}, z}, S.remove(~V, t, key), t, ih)
181
182# removing an absent key changes nothing
183def remove_none(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +h: {S.lookup(~V, m, key) == None{} : Maybe<&2, V>}) -> {S.remove(~V, m, key) == m : List<&2, S.Entry<V>>}:
184 match m:
185 case Nil{}:
186 {==}
187 case Con{S.E{+j, +v}, +t}:
188 +c0 = Pair.fst({S.str_eq(j, key) == False{} : Bool}, {S.lookup(~V, t, key) == None{} : Maybe<&2, V>}, none_pick(~V, S.str_eq(j, key), v, S.lookup(~V, t, key), h))
189 +r0 = Pair.snd({S.str_eq(j, key) == False{} : Bool}, {S.lookup(~V, t, key) == None{} : Maybe<&2, V>}, none_pick(~V, S.str_eq(j, key), v, S.lookup(~V, t, key), h))
190 rn_c(~V, j, v, t, key, S.str_eq(j, key), c0, remove_none(~V, t, key, r0))