proofs/lib/lemmas/proofs/map_bridge.bend
bend-collections-laws-containers@1.0.0.0 · 417 lines · 0 definitions
1import Base
2
3# Bend 2.0.32 rewrote Base's Map descents (get, has, put, pop, seek, ins) as
4# one-level `Map.X.go` functions over the whole node. The lemmas in this
5# library were written against 2.0.28's shape, where Map.X on a node branched
6# through a `.bit` helper (`.deep`/`.if` for ins) that recursed with Map.X on
7# the chosen child. Mutual recursion is no longer allowed, so those helpers
8# are defined here non-recursively, each calling Base's current Map.X on the
9# child, and each comes with a bridge law: Map.X on a node equals the helper.
10# Every bridge holds by unfolding both sides (no induction).
11
12# ---- the routed key: Map.bit keeps the key (from native_map.bend) ----
13
14def routed_key(r: String & Bool) -> String:
15 (key, bit) = r
16 key
17
18law recursive_bit_key:
19 for c: Char
20 for r: String & Bool
21 {routed_key(Map.bit.go.rec(c, r)) == SCon{c, routed_key(r)} : String}
22def recursive_bit_key(c, r):
23 match r:
24 case Tuple{key, bit}:
25 {==}
26
27law bit_go_preserves_key:
28 for key: String
29 for +character: Nat
30 for +offset: Nat
31 {routed_key(Map.bit.go(key, character, offset)) == key : String}
32def bit_go_preserves_key(key, character, offset):
33 match key character offset:
34 case SNil{} ci off:
35 {==}
36 case SCon{Chr{x}, tail} 0n 0n:
37 {==}
38 case SCon{Chr{x}, tail} 0n 1n+off:
39 {==}
40 case SCon{Chr{x}, +tail} 1n+ci off:
41 +c = {Chr{x} : Char}
42 Equal.trans(String, routed_key(Map.bit.go.rec(c, Map.bit.go(tail, ci, off))),
43 SCon{c, routed_key(Map.bit.go(tail, ci, off))}, SCon{c, tail},
44 recursive_bit_key(c, Map.bit.go(tail, ci, off)),
45 Equal.cong(String, String, t => SCon{c, t}, routed_key(Map.bit.go(tail, ci, off)), tail, bit_go_preserves_key(tail, ci, off)))
46
47law bit_at_preserves_key:
48 for key: String
49 for coordinates: Nat & Nat
50 {routed_key(Map.bit.at(key, coordinates)) == key : String}
51def bit_at_preserves_key(key, coordinates):
52 match coordinates:
53 case Tuple{ci, off}:
54 bit_go_preserves_key(key, ci, off)
55
56law bit_preserves_key:
57 for key: String
58 for position: Nat
59 {routed_key(Map.bit(key, position)) == key : String}
60def bit_preserves_key(key, position):
61 bit_at_preserves_key(key, Nat.divmod(position, 33n))
62
63# ---- one-step helpers (2.0.28's `.bit` shape over Base's current Map) ----
64
65def get_bit(-V: Data, d: V, lo: Map<&2, V>, hi: Map<&2, V>, p2: Nat, kb: String & Bool) -> Map<&2, V> & V:
66 (key2, b) = kb
67 match b:
68 case False{}:
69 Map.lo(&2, V, V, p2, hi, Map.get(V, d, lo, key2))
70 case True{}:
71 Map.hi(&2, V, V, p2, lo, Map.get(V, d, hi, key2))
72
73def has_bit(-a: Quant, -V: Kind(a), lo: Map<a, V>, hi: Map<a, V>, p2: Nat, kb: String & Bool) -> Map<a, V> & Bool:
74 (key2, b) = kb
75 match b:
76 case False{}:
77 Map.lo(a, V, Bool, p2, hi, Map.has(a, V, lo, key2))
78 case True{}:
79 Map.hi(a, V, Bool, p2, lo, Map.has(a, V, hi, key2))
80
81def put_bit(-a: Quant, -V: Kind(a), x: V, p2: Nat, lo: Map<a, V>, hi: Map<a, V>, kb: String & Bool) -> Map<a, V>:
82 (key2, b) = kb
83 match b:
84 case False{}:
85 MNode{p2, Map.put(a, V, lo, key2, x), hi}
86 case True{}:
87 MNode{p2, lo, Map.put(a, V, hi, key2, x)}
88
89def pop_bit(-a: Quant, -V: Kind(a), lo: Map<a, V>, hi: Map<a, V>, p2: Nat, kb: String & Bool) -> Map<a, V> & Maybe<a, V>:
90 (key2, b) = kb
91 match b:
92 case False{}:
93 Map.pop.lo(a, V, p2, hi, Map.pop(a, V, lo, key2))
94 case True{}:
95 Map.pop.hi(a, V, p2, lo, Map.pop(a, V, hi, key2))
96
97def seek_bit(-a: Quant, -V: Kind(a), lo: Map<a, V>, hi: Map<a, V>, p2: Nat, kb: String & Bool) -> Map<a, V> & String & Maybe<&2, String>:
98 (key2, b) = kb
99 match b:
100 case False{}:
101 Map.lo(a, V, String & Maybe<&2, String>, p2, hi, Map.seek(a, V, lo, key2))
102 case True{}:
103 Map.hi(a, V, String & Maybe<&2, String>, p2, lo, Map.seek(a, V, hi, key2))
104
105def ins_deep(-a: Quant, -V: Kind(a), x: V, lo: Map<a, V>, hi: Map<a, V>, pb: Nat, qb: Nat, kb: String & Bool) -> Map<a, V>:
106 (key2, b) = kb
107 match b:
108 case False{}:
109 MNode{qb, Map.ins(a, V, lo, key2, x, pb), hi}
110 case True{}:
111 MNode{qb, lo, Map.ins(a, V, hi, key2, x, pb)}
112
113def ins_if(-a: Quant, -V: Kind(a), key: String, x: V, lo: Map<a, V>, hi: Map<a, V>, +p2: Nat, pb: Nat, t: Bool) -> Map<a, V>:
114 match t:
115 case False{}:
116 Map.ins.splice(a, V, pb, key, x, MNode{p2, lo, hi})
117 case True{}:
118 ins_deep(a, V, x, lo, hi, pb, p2, Map.bit(key, p2))
119
120# ---- bridges: Base Map.X on a node is the one-step helper ----
121
122law get_go_bridge:
123 for -V: Data
124 for d: V
125for +p: Nat
126 for lo: Map<&2, V>
127 for hi: Map<&2, V>
128 for kb: String & Bool
129 {Map.get.go(V, MNode{p, lo, hi}, d, kb) == get_bit(V, d, lo, hi, p, kb) : Map<&2, V> & V}
130def get_go_bridge(V, d, p, lo, hi, kb):
131 match lo hi kb:
132 case MTip{} _ Tuple{key2, False{}}:
133 {==}
134 case MLeaf{k, v} _ Tuple{key2, False{}}:
135 {==}
136 case MNode{q, c, e} _ Tuple{key2, False{}}:
137 {==}
138 case _ MTip{} Tuple{key2, True{}}:
139 {==}
140 case _ MLeaf{k, v} Tuple{key2, True{}}:
141 {==}
142 case _ MNode{q, c, e} Tuple{key2, True{}}:
143 {==}
144
145law get_node:
146 for -V: Data
147 for d: V
148for +p: Nat
149 for lo: Map<&2, V>
150 for hi: Map<&2, V>
151 for key: String
152 {Map.get(V, d, MNode{p, lo, hi}, key) == get_bit(V, d, lo, hi, p, Map.bit(key, p)) : Map<&2, V> & V}
153def get_node(V, d, p, lo, hi, key):
154 get_go_bridge(V, d, p, lo, hi, Map.bit(key, p))
155
156law has_go_bridge:
157 for -a: Quant
158 for -V: Kind(a)
159 for +p: Nat
160 for lo: Map<a, V>
161 for hi: Map<a, V>
162 for kb: String & Bool
163 {Map.has.go(a, V, MNode{p, lo, hi}, kb) == has_bit(a, V, lo, hi, p, kb) : Map<a, V> & Bool}
164def has_go_bridge(a, V, p, lo, hi, kb):
165 match lo hi kb:
166 case MTip{} _ Tuple{key2, False{}}:
167 {==}
168 case MLeaf{k, v} _ Tuple{key2, False{}}:
169 {==}
170 case MNode{q, c, e} _ Tuple{key2, False{}}:
171 {==}
172 case _ MTip{} Tuple{key2, True{}}:
173 {==}
174 case _ MLeaf{k, v} Tuple{key2, True{}}:
175 {==}
176 case _ MNode{q, c, e} Tuple{key2, True{}}:
177 {==}
178
179law has_node:
180 for -a: Quant
181 for -V: Kind(a)
182 for +p: Nat
183 for lo: Map<a, V>
184 for hi: Map<a, V>
185 for key: String
186 {Map.has(a, V, MNode{p, lo, hi}, key) == has_bit(a, V, lo, hi, p, Map.bit(key, p)) : Map<a, V> & Bool}
187def has_node(a, V, p, lo, hi, key):
188 has_go_bridge(a, V, p, lo, hi, Map.bit(key, p))
189
190law put_go_bridge:
191 for -a: Quant
192 for -V: Kind(a)
193 for x: V
194for +p: Nat
195 for lo: Map<a, V>
196 for hi: Map<a, V>
197 for kb: String & Bool
198 {Map.put.go(a, V, MNode{p, lo, hi}, x, kb) == put_bit(a, V, x, p, lo, hi, kb) : Map<a, V>}
199def put_go_bridge(a, V, x, p, lo, hi, kb):
200 match lo hi kb:
201 case MTip{} _ Tuple{key2, False{}}:
202 {==}
203 case MLeaf{k, v} _ Tuple{key2, False{}}:
204 {==}
205 case MNode{q, c, e} _ Tuple{key2, False{}}:
206 {==}
207 case _ MTip{} Tuple{key2, True{}}:
208 {==}
209 case _ MLeaf{k, v} Tuple{key2, True{}}:
210 {==}
211 case _ MNode{q, c, e} Tuple{key2, True{}}:
212 {==}
213
214law put_node:
215 for -a: Quant
216 for -V: Kind(a)
217 for x: V
218for +p: Nat
219 for lo: Map<a, V>
220 for hi: Map<a, V>
221 for key: String
222 {Map.put(a, V, MNode{p, lo, hi}, key, x) == put_bit(a, V, x, p, lo, hi, Map.bit(key, p)) : Map<a, V>}
223def put_node(a, V, x, p, lo, hi, key):
224 put_go_bridge(a, V, x, p, lo, hi, Map.bit(key, p))
225
226law pop_go_bridge:
227 for -a: Quant
228 for -V: Kind(a)
229 for +p: Nat
230 for lo: Map<a, V>
231 for hi: Map<a, V>
232 for kb: String & Bool
233 {Map.pop.go(a, V, MNode{p, lo, hi}, kb) == pop_bit(a, V, lo, hi, p, kb) : Map<a, V> & Maybe<a, V>}
234def pop_go_bridge(a, V, p, lo, hi, kb):
235 match lo hi kb:
236 case MTip{} _ Tuple{key2, False{}}:
237 {==}
238 case MLeaf{k, v} _ Tuple{key2, False{}}:
239 {==}
240 case MNode{q, c, e} _ Tuple{key2, False{}}:
241 {==}
242 case _ MTip{} Tuple{key2, True{}}:
243 {==}
244 case _ MLeaf{k, v} Tuple{key2, True{}}:
245 {==}
246 case _ MNode{q, c, e} Tuple{key2, True{}}:
247 {==}
248
249law pop_node:
250 for -a: Quant
251 for -V: Kind(a)
252 for +p: Nat
253 for lo: Map<a, V>
254 for hi: Map<a, V>
255 for key: String
256 {Map.pop(a, V, MNode{p, lo, hi}, key) == pop_bit(a, V, lo, hi, p, Map.bit(key, p)) : Map<a, V> & Maybe<a, V>}
257def pop_node(a, V, p, lo, hi, key):
258 pop_go_bridge(a, V, p, lo, hi, Map.bit(key, p))
259
260law seek_go_bridge:
261 for -a: Quant
262 for -V: Kind(a)
263 for +p: Nat
264 for lo: Map<a, V>
265 for hi: Map<a, V>
266 for kb: String & Bool
267 {Map.seek.go(a, V, MNode{p, lo, hi}, kb) == seek_bit(a, V, lo, hi, p, kb) : Map<a, V> & String & Maybe<&2, String>}
268def seek_go_bridge(a, V, p, lo, hi, kb):
269 match lo hi kb:
270 case MTip{} _ Tuple{key2, False{}}:
271 {==}
272 case MLeaf{k, v} _ Tuple{key2, False{}}:
273 {==}
274 case MNode{q, c, e} _ Tuple{key2, False{}}:
275 {==}
276 case _ MTip{} Tuple{key2, True{}}:
277 {==}
278 case _ MLeaf{k, v} Tuple{key2, True{}}:
279 {==}
280 case _ MNode{q, c, e} Tuple{key2, True{}}:
281 {==}
282
283law seek_node:
284 for -a: Quant
285 for -V: Kind(a)
286 for +p: Nat
287 for lo: Map<a, V>
288 for hi: Map<a, V>
289 for key: String
290 {Map.seek(a, V, MNode{p, lo, hi}, key) == seek_bit(a, V, lo, hi, p, Map.bit(key, p)) : Map<a, V> & String & Maybe<&2, String>}
291def seek_node(a, V, p, lo, hi, key):
292 seek_go_bridge(a, V, p, lo, hi, Map.bit(key, p))
293
294law ins_splice_bridge:
295 for -a: Quant
296 for -V: Kind(a)
297 for +q: Nat
298 for lo: Map<a, V>
299 for hi: Map<a, V>
300 for x: V
301 for +p: Nat
302 for key: String
303 for kb: String & Bool
304 for hk: {routed_key(kb) == key : String}
305 {Map.ins.go(a, V, MNode{q, lo, hi}, x, p, kb, False{}) == Map.ins.splice(a, V, p, key, x, MNode{q, lo, hi}) : Map<a, V>}
306def ins_splice_bridge(a, V, q, lo, hi, x, p, key, kb, hk):
307 match lo hi kb:
308 case MTip{} MTip{} Tuple{k2, False{}}:
309 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MTip{}}) : Map<a, V>}
310 {==}
311 case MTip{} MTip{} Tuple{k2, True{}}:
312 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MTip{}}) : Map<a, V>}
313 {==}
314 case MTip{} MLeaf{k3, v3} Tuple{k2, False{}}:
315 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MLeaf{k3, v3}}) : Map<a, V>}
316 {==}
317 case MTip{} MLeaf{k3, v3} Tuple{k2, True{}}:
318 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MLeaf{k3, v3}}) : Map<a, V>}
319 {==}
320 case MTip{} MNode{r3, c3, e3} Tuple{k2, False{}}:
321 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) : Map<a, V>}
322 {==}
323 case MTip{} MNode{r3, c3, e3} Tuple{k2, True{}}:
324 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) : Map<a, V>}
325 {==}
326 case MLeaf{k1, v1} MTip{} Tuple{k2, False{}}:
327 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MTip{}}) : Map<a, V>}
328 {==}
329 case MLeaf{k1, v1} MTip{} Tuple{k2, True{}}:
330 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MTip{}}) : Map<a, V>}
331 {==}
332 case MLeaf{k1, v1} MLeaf{k3, v3} Tuple{k2, False{}}:
333 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) : Map<a, V>}
334 {==}
335 case MLeaf{k1, v1} MLeaf{k3, v3} Tuple{k2, True{}}:
336 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) : Map<a, V>}
337 {==}
338 case MLeaf{k1, v1} MNode{r3, c3, e3} Tuple{k2, False{}}:
339 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) : Map<a, V>}
340 {==}
341 case MLeaf{k1, v1} MNode{r3, c3, e3} Tuple{k2, True{}}:
342 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) : Map<a, V>}
343 {==}
344 case MNode{r1, c1, e1} MTip{} Tuple{k2, False{}}:
345 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) : Map<a, V>}
346 {==}
347 case MNode{r1, c1, e1} MTip{} Tuple{k2, True{}}:
348 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) : Map<a, V>}
349 {==}
350 case MNode{r1, c1, e1} MLeaf{k3, v3} Tuple{k2, False{}}:
351 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) : Map<a, V>}
352 {==}
353 case MNode{r1, c1, e1} MLeaf{k3, v3} Tuple{k2, True{}}:
354 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) : Map<a, V>}
355 {==}
356 case MNode{r1, c1, e1} MNode{r3, c3, e3} Tuple{k2, False{}}:
357 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) : Map<a, V>}
358 {==}
359 case MNode{r1, c1, e1} MNode{r3, c3, e3} Tuple{k2, True{}}:
360 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) : Map<a, V>}
361 {==}
362
363law ins_deep_bridge:
364 for -a: Quant
365 for -V: Kind(a)
366 for +q: Nat
367 for lo: Map<a, V>
368 for hi: Map<a, V>
369 for x: V
370 for +p: Nat
371 for kb: String & Bool
372 {Map.ins.go(a, V, MNode{q, lo, hi}, x, p, kb, True{}) == ins_deep(a, V, x, lo, hi, p, q, kb) : Map<a, V>}
373def ins_deep_bridge(a, V, q, lo, hi, x, p, kb):
374 match lo hi kb:
375 case MTip{} _ Tuple{key2, False{}}:
376 {==}
377 case MLeaf{k, v} _ Tuple{key2, False{}}:
378 {==}
379 case MNode{r, c, e} _ Tuple{key2, False{}}:
380 {==}
381 case _ MTip{} Tuple{key2, True{}}:
382 {==}
383 case _ MLeaf{k, v} Tuple{key2, True{}}:
384 {==}
385 case _ MNode{r, c, e} Tuple{key2, True{}}:
386 {==}
387
388law ins_t:
389 for -a: Quant
390 for -V: Kind(a)
391 for +pos: Nat
392 for lo: Map<a, V>
393 for hi: Map<a, V>
394 for +key: String
395 for x: V
396 for +p: Nat
397 for t: Bool
398 {Map.ins.go(a, V, MNode{pos, lo, hi}, x, p, Map.bit(key, pos), t) == ins_if(a, V, key, x, lo, hi, pos, p, t) : Map<a, V>}
399def ins_t(a, V, pos, lo, hi, key, x, p, t):
400 match t:
401 case False{}:
402 ins_splice_bridge(a, V, pos, lo, hi, x, p, key, Map.bit(key, pos), bit_preserves_key(key, pos))
403 case True{}:
404 ins_deep_bridge(a, V, pos, lo, hi, x, p, Map.bit(key, pos))
405
406law ins_node:
407 for -a: Quant
408 for -V: Kind(a)
409 for +pos: Nat
410 for lo: Map<a, V>
411 for hi: Map<a, V>
412 for +key: String
413 for x: V
414 for +p: Nat
415 {Map.ins(a, V, MNode{pos, lo, hi}, key, x, p) == ins_if(a, V, key, x, lo, hi, pos, p, Nat.is_lt(pos, p)) : Map<a, V>}
416def ins_node(a, V, pos, lo, hi, key, x, p):
417 ins_t(a, V, pos, lo, hi, key, x, p, Nat.is_lt(pos, p))