proofs/lib/lemmas/proofs/map_delete.bend
bend-collections-laws-containers@1.0.0.0 · 179 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_bridge.bend as MB
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_lookup.bend as L
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as R
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Inv
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/string_compare.bend as N
8
9law different_sides:
10 for side: Bool
11 for e: {side == Bool.not(side) : Bool}
12 Empty
13def different_sides(side, e):
14 match side:
15 case False{}:
16 R.false_true(e)
17 case True{}:
18 R.false_true(Equal.sym(Bool, True{}, False{}, e))
19
20law opposite_routes:
21 for +key: String
22 for +pos: Nat
23 for +side: Bool
24 for a: {Map.bit(key, pos) == (key, side) : String & Bool}
25 for b: {Map.bit(key, pos) == (key, Bool.not(side)) : String & Bool}
26 Empty
27def opposite_routes(key, pos, side, a, b):
28 different_sides(side, Equal.trans(Bool, side, I.route_bit(Map.bit(key, pos)), Bool.not(side), Equal.sym(Bool, I.route_bit(Map.bit(key, pos)), side, Equal.cong(String & Bool, Bool, I.route_bit, Map.bit(key, pos), (key, side), a)), Equal.cong(String & Bool, Bool, I.route_bit, Map.bit(key, pos), (key, Bool.not(side)), b)))
29
30law opposite_case:
31 for -V: Data
32 for +tree: Map<&2, Maybe<&2, V>>
33 for +key: String
34 for +pos: Nat
35 for +side: Bool
36 for routes: R.routed(Maybe<&2, V>, tree, pos, Bool.not(side))
37 for bit: {Map.bit(key, pos) == (key, side) : String & Bool}
38 for found: Maybe<&2, V>
39 for result: {I.lookup(Maybe<&2, V>, None{}, tree, key) == found : Maybe<&2, V>}
40 for member: L.certificate(V, tree, key, found)
41 {I.lookup(Maybe<&2, V>, None{}, tree, key) == None{} : Maybe<&2, V>}
42def opposite_case(V, tree, key, pos, side, routes, bit, found, result, member):
43 match found:
44 case None{}:
45 result
46 case Some{value}:
47 Empty.absurd({I.lookup(Maybe<&2, V>, None{}, tree, key) == None{} : Maybe<&2, V>}, opposite_routes(key, pos, side, bit, R.member_routed(V, tree, key, value, pos, Bool.not(side), routes, member)))
48
49law opposite_missing:
50 for -V: Data
51 for +tree: Map<&2, Maybe<&2, V>>
52 for +key: String
53 for pos: Nat
54 for side: Bool
55 for routes: R.routed(Maybe<&2, V>, tree, pos, Bool.not(side))
56 for bit: {Map.bit(key, pos) == (key, side) : String & Bool}
57 {I.lookup(Maybe<&2, V>, None{}, tree, key) == None{} : Maybe<&2, V>}
58def opposite_missing(V, tree, key, pos, side, routes, bit):
59 opposite_case(V, tree, key, pos, side, routes, bit, I.lookup(Maybe<&2, V>, None{}, tree, key), {==}, L.lookup_certificate(V, tree, key))
60
61law collapse_low:
62 for -V: Data
63 for +hi: Map<&2, Maybe<&2, V>>
64 for +p: Nat
65 for +key: String
66 for bit: {Map.bit(key, p) == (key, False{}) : String & Bool}
67 for routes: R.routed(Maybe<&2, V>, hi, p, True{})
68 for r: Map<&2, Maybe<&2, V>> & Maybe<&2, Maybe<&2, V>>
69 for absent: {I.lookup(Maybe<&2, V>, None{}, Map.del.fin(&2, Maybe<&2, V>, r), key) == None{} : Maybe<&2, V>}
70 {I.lookup(Maybe<&2, V>, None{}, Map.del.fin(&2, Maybe<&2, V>, Map.pop.lo(&2, Maybe<&2, V>, p, hi, r)), key) == None{} : Maybe<&2, V>}
71def collapse_low(V, hi, p, key, bit, routes, r, absent):
72 match r:
73 case Tuple{tree, found}:
74 match tree:
75 case MTip{}:
76 opposite_missing(V, hi, key, p, False{}, routes, bit)
77 case MLeaf{+stored, +item}:
78 Equal.trans(Maybe<&2, V>, I.lookup(Maybe<&2, V>, None{}, MNode{p, MLeaf{stored, item}, hi}, key), I.lookup(Maybe<&2, V>, None{}, MLeaf{stored, item}, key), None{}, I.node_left(Maybe<&2, V>, None{}, MLeaf{stored, item}, hi, p, key, bit), absent)
79 case MNode{+q, +lo, +other}:
80 Equal.trans(Maybe<&2, V>, I.lookup(Maybe<&2, V>, None{}, MNode{p, MNode{q, lo, other}, hi}, key), I.lookup(Maybe<&2, V>, None{}, MNode{q, lo, other}, key), None{}, I.node_left(Maybe<&2, V>, None{}, MNode{q, lo, other}, hi, p, key, bit), absent)
81
82law collapse_high:
83 for -V: Data
84 for +lo: Map<&2, Maybe<&2, V>>
85 for +p: Nat
86 for +key: String
87 for bit: {Map.bit(key, p) == (key, True{}) : String & Bool}
88 for routes: R.routed(Maybe<&2, V>, lo, p, False{})
89 for r: Map<&2, Maybe<&2, V>> & Maybe<&2, Maybe<&2, V>>
90 for absent: {I.lookup(Maybe<&2, V>, None{}, Map.del.fin(&2, Maybe<&2, V>, r), key) == None{} : Maybe<&2, V>}
91 {I.lookup(Maybe<&2, V>, None{}, Map.del.fin(&2, Maybe<&2, V>, Map.pop.hi(&2, Maybe<&2, V>, p, lo, r)), key) == None{} : Maybe<&2, V>}
92def collapse_high(V, lo, p, key, bit, routes, r, absent):
93 match r:
94 case Tuple{tree, found}:
95 match tree:
96 case MTip{}:
97 opposite_missing(V, lo, key, p, True{}, routes, bit)
98 case MLeaf{+stored, +item}:
99 Equal.trans(Maybe<&2, V>, I.lookup(Maybe<&2, V>, None{}, MNode{p, lo, MLeaf{stored, item}}, key), I.lookup(Maybe<&2, V>, None{}, MLeaf{stored, item}, key), None{}, I.node_right(Maybe<&2, V>, None{}, lo, MLeaf{stored, item}, p, key, bit), absent)
100 case MNode{+q, +other, +hi}:
101 Equal.trans(Maybe<&2, V>, I.lookup(Maybe<&2, V>, None{}, MNode{p, lo, MNode{q, other, hi}}, key), I.lookup(Maybe<&2, V>, None{}, MNode{q, other, hi}, key), None{}, I.node_right(Maybe<&2, V>, None{}, lo, MNode{q, other, hi}, p, key, bit), absent)
102
103law leaf_case:
104 for -V: Data
105 for +item: Maybe<&2, V>
106 for +key: String
107 for +stored: String
108 for cmp: Cmp
109 for e: {String.cmp(key, stored) == ((key, stored), cmp) : (String & String) & Cmp}
110 {I.lookup(Maybe<&2, V>, None{}, Map.del.fin(&2, Maybe<&2, V>, Map.pop.leaf(&2, Maybe<&2, V>, item, ((key, stored), cmp))), key) == None{} : Maybe<&2, V>}
111def leaf_case(V, item, key, stored, cmp, e):
112 match cmp:
113 case LT{}:
114 %Equal.sym((String & String) & Cmp, String.cmp(key, stored), ((key, stored), LT{}), e) : {I.value(Maybe<&2, V>, Map.get.leaf(Maybe<&2, V>, None{}, item, _)) == None{} : Maybe<&2, V>}
115 {==}
116 case EQ{}:
117 {==}
118 case GT{}:
119 %Equal.sym((String & String) & Cmp, String.cmp(key, stored), ((key, stored), GT{}), e) : {I.value(Maybe<&2, V>, Map.get.leaf(Maybe<&2, V>, None{}, item, _)) == None{} : Maybe<&2, V>}
120 {==}
121
122law leaf_delete:
123 for -V: Data
124 for +item: Maybe<&2, V>
125 for +key: String
126 for +stored: String
127 {I.lookup(Maybe<&2, V>, None{}, Map.del(&2, Maybe<&2, V>, MLeaf{stored, item}, key), key) == None{} : Maybe<&2, V>}
128def leaf_delete(V, item, key, stored):
129 %Equal.sym((String & String) & Cmp, String.cmp(key, stored), ((key, stored), N.comparison_tag(String, String.cmp(key, stored))), N.string_comparison_shape(key, stored)) : {I.lookup(Maybe<&2, V>, None{}, Map.del.fin(&2, Maybe<&2, V>, Map.pop.leaf(&2, Maybe<&2, V>, item, _)), key) == None{} : Maybe<&2, V>}
130 leaf_case(V, item, key, stored, N.comparison_tag(String, String.cmp(key, stored)), N.string_comparison_shape(key, stored))
131
132law branch:
133 for -V: Data
134 for +lo: Map<&2, Maybe<&2, V>>
135 for +hi: Map<&2, Maybe<&2, V>>
136 for +p: Nat
137 for +key: String
138 for bit: Bool
139 for +e: {Map.bit(key, p) == (key, bit) : String & Bool}
140 for lr: R.routed(Maybe<&2, V>, lo, p, False{})
141 for hr: R.routed(Maybe<&2, V>, hi, p, True{})
142 for lp: {I.lookup(Maybe<&2, V>, None{}, Map.del(&2, Maybe<&2, V>, lo, key), key) == None{} : Maybe<&2, V>}
143 for hp: {I.lookup(Maybe<&2, V>, None{}, Map.del(&2, Maybe<&2, V>, hi, key), key) == None{} : Maybe<&2, V>}
144 {I.lookup(Maybe<&2, V>, None{}, Map.del(&2, Maybe<&2, V>, MNode{p, lo, hi}, key), key) == None{} : Maybe<&2, V>}
145def branch(V, lo, hi, p, key, bit, e, lr, hr, lp, hp):
146 match bit:
147 case False{}:
148 %Equal.sym(Map<&2, Maybe<&2, V>> & Maybe<&2, Maybe<&2, V>>, Map.pop(&2, Maybe<&2, V>, MNode{p, lo, hi}, key), MB.pop_bit(&2, Maybe<&2, V>, lo, hi, p, Map.bit(key, p)), MB.pop_node(&2, Maybe<&2, V>, p, lo, hi, key)) : {I.lookup(Maybe<&2, V>, None{}, Map.del.fin(&2, Maybe<&2, V>, _), key) == None{} : Maybe<&2, V>}
149 %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), e) : {I.lookup(Maybe<&2, V>, None{}, Map.del.fin(&2, Maybe<&2, V>, MB.pop_bit(&2, Maybe<&2, V>, lo, hi, p, _)), key) == None{} : Maybe<&2, V>}
150 collapse_low(V, hi, p, key, e, hr, Map.pop(&2, Maybe<&2, V>, lo, key), lp)
151 case True{}:
152 %Equal.sym(Map<&2, Maybe<&2, V>> & Maybe<&2, Maybe<&2, V>>, Map.pop(&2, Maybe<&2, V>, MNode{p, lo, hi}, key), MB.pop_bit(&2, Maybe<&2, V>, lo, hi, p, Map.bit(key, p)), MB.pop_node(&2, Maybe<&2, V>, p, lo, hi, key)) : {I.lookup(Maybe<&2, V>, None{}, Map.del.fin(&2, Maybe<&2, V>, _), key) == None{} : Maybe<&2, V>}
153 %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), e) : {I.lookup(Maybe<&2, V>, None{}, Map.del.fin(&2, Maybe<&2, V>, MB.pop_bit(&2, Maybe<&2, V>, lo, hi, p, _)), key) == None{} : Maybe<&2, V>}
154 collapse_high(V, lo, p, key, e, lr, Map.pop(&2, Maybe<&2, V>, hi, key), hp)
155
156law delete_same:
157 for -V: Data
158 for tree: Map<&2, Maybe<&2, V>>
159 for +key: String
160 for invariant: R.valid(Maybe<&2, V>, tree)
161 {I.lookup(Maybe<&2, V>, None{}, Map.del(&2, Maybe<&2, V>, tree, key), key) == None{} : Maybe<&2, V>}
162def delete_same(V, tree, key, invariant):
163 match tree:
164 case MTip{}:
165 {==}
166 case MLeaf{stored, item}:
167 leaf_delete(V, item, key, stored)
168 case MNode{+p, +lo, +hi}:
169 (lr, hr, lv, hv) = invariant
170 branch(V, lo, hi, p, key, I.route_bit(Map.bit(key, p)), I.route_shape(key, p), lr, hr, delete_same(V, lo, key, lv), delete_same(V, hi, key, hv))
171
172law critbit_delete_same:
173 for -V: Data
174 for +tree: Map<&2, Maybe<&2, V>>
175 for key: String
176 for invariant: {Inv.critbit(Maybe<&2, V>, tree) == True{} : Bool}
177 {I.lookup(Maybe<&2, V>, None{}, Map.del(&2, Maybe<&2, V>, tree, key), key) == None{} : Maybe<&2, V>}
178def critbit_delete_same(V, tree, key, invariant):
179 delete_same(V, tree, key, R.critbit_certificate(Maybe<&2, V>, tree, invariant))