proofs/lib/lemmas/proofs/map_seek_empty.bend
bend-collections-laws-containers@1.0.0.0 · 72 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Inv
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend as I
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_critbit_parts.bend as Parts
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as R
6
7law branch:
8 for -V: Data
9 for +p: Nat
10 for +lo: Map<&2, V>
11 for +hi: Map<&2, V>
12 for +key: String
13 for bit: Bool
14 for route: {Map.bit(key, p) == (key, bit) : String & Bool}
15 for left: {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, lo, key))) == True{} : Bool}
16 for right: {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, hi, key))) == True{} : Bool}
17 {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key))) == True{} : Bool}
18def branch(V, p, lo, hi, key, bit, route, left, right):
19 match bit:
20 case False{}:
21 %Equal.sym(Maybe<&2, String>, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)), I.seek_found(V, Map.seek(&2, V, lo, key)), I.seek_left(V, lo, hi, p, key, route)) : {Maybe.is_some(&2, String, _) == True{} : Bool}
22 left
23 case True{}:
24 %Equal.sym(Maybe<&2, String>, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)), I.seek_found(V, Map.seek(&2, V, hi, key)), I.seek_right(V, lo, hi, p, key, route)) : {Maybe.is_some(&2, String, _) == True{} : Bool}
25 right
26
27law from_parts:
28 for -V: Data
29 for +p: Nat
30 for +lo: Map<&2, V>
31 for +hi: Map<&2, V>
32 for +key: String
33 for facts: Parts.NodeFacts(V, p, lo, hi)
34 for left: {Inv.critbit(V, lo) == True{} : Bool} -> {Inv.nonempty(V, lo) == True{} : Bool} -> {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, lo, key))) == True{} : Bool}
35 for right: {Inv.critbit(V, hi) == True{} : Bool} -> {Inv.nonempty(V, hi) == True{} : Bool} -> {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, hi, key))) == True{} : Bool}
36 {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key))) == True{} : Bool}
37def from_parts(V, p, lo, hi, key, facts, left, right):
38 match facts:
39 case (common, nl, nh, bl, bh, rl, rh, vl, vh):
40 branch(V, p, lo, hi, key, I.route_bit(Map.bit(key, p)), I.route_shape(key, p), left(vl, nl), right(vh, nh))
41
42# A valid nonempty native tree cannot seek into an empty child.
43law nonempty_seek:
44 for -V: Data
45 for tree: Map<&2, V>
46 for +key: String
47 for valid: {Inv.critbit(V, tree) == True{} : Bool}
48 for occupied: {Inv.nonempty(V, tree) == True{} : Bool}
49 {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, tree, key))) == True{} : Bool}
50def nonempty_seek(V, tree, key, valid, occupied):
51 match tree:
52 case MTip{}: Empty.absurd({Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, MTip{}, key))) == True{} : Bool}, R.false_true(occupied))
53 case MLeaf{stored, value}: {==}
54 case MNode{+p, +lo, +hi}:
55 from_parts(V, p, lo, hi, key, Parts.node_parts(V, p, lo, hi, valid), v => n => nonempty_seek(V, lo, key, v, n), v => n => nonempty_seek(V, hi, key, v, n))
56
57law empty_seek_is_tip:
58 for -V: Data
59 for tree: Map<&2, V>
60 for +key: String
61 for valid: {Inv.critbit(V, tree) == True{} : Bool}
62 for missing: {I.seek_found(V, Map.seek(&2, V, tree, key)) == None{} : Maybe<&2, String>}
63 {tree == MTip{} : Map<&2, V>}
64def empty_seek_is_tip(V, tree, key, valid, missing):
65 match tree:
66 case MTip{}: {==}
67 case MLeaf{stored, value}:
68 Empty.absurd({MLeaf{stored, value} == MTip{} : Map<&2, V>}, R.false_true(Equal.sym(Bool, True{}, False{}, Equal.cong(Maybe<&2, String>, Bool, m => Maybe.is_some(&2, String, m), Some{stored}, None{}, missing))))
69 case MNode{+p, +lo, +hi}:
70 present = nonempty_seek(V, MNode{p, lo, hi}, key, valid, {==})
71 absent = Equal.cong(Maybe<&2, String>, Bool, m => Maybe.is_some(&2, String, m), I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)), None{}, missing)
72 Empty.absurd({MNode{p, lo, hi} == MTip{} : Map<&2, V>}, R.false_true(Equal.trans(Bool, False{}, Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key))), True{}, Equal.sym(Bool, Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key))), False{}, absent), present)))