proofs/lib/lemmas/proofs/map_delete_below.bend
bend-collections-laws-containers@1.0.0.0 · 138 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/invariants.bend as Inv
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/string_compare.bend as N
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend as I
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_difference_order.bend as O
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_string_prefix.bend as Prefix
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_bounds.bend as Bounds
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_critbit_parts.bend as Parts
10
11law strict_transitive:
12 for +a: Nat
13 for +b: Nat
14 for +c: Nat
15 for ab: {Nat.is_lt(a, b) == True{} : Bool}
16 for bc: {Nat.is_lt(b, c) == True{} : Bool}
17 {Nat.is_lt(a, c) == True{} : Bool}
18def strict_transitive(a, b, c, ab, bc):
19 Prefix.predecessor_less(a, c, Bounds.le_transitive(1n+a, b, c, O.strict_successor(a, b, ab), O.less_is_le(b, c, bc)))
20
21law lower_parent:
22 for -V: Data
23 for tree: Map<&2, V>
24 for +parent: Nat
25 for +p: Nat
26 for lower: {Nat.is_lt(parent, p) == True{} : Bool}
27 for below: {Inv.below(V, tree, p) == True{} : Bool}
28 {Inv.below(V, tree, parent) == True{} : Bool}
29def lower_parent(V, tree, parent, p, lower, below):
30 match tree:
31 case MTip{}: {==}
32 case MLeaf{k, v}: {==}
33 case MNode{q, lo, hi}: strict_transitive(parent, p, q, lower, below)
34
35law low:
36 for -V: Data
37 for +p: Nat
38 for +parent: Nat
39 for hi: Map<&2, V>
40 for r: Map<&2, V> & Maybe<&2, V>
41 for lower: {Nat.is_lt(parent, p) == True{} : Bool}
42 for below: {Inv.below(V, hi, p) == True{} : Bool}
43 {Inv.below(V, Map.del.fin(&2, V, Map.pop.lo(&2, V, p, hi, r)), parent) == True{} : Bool}
44def low(V, p, parent, hi, r, lower, below):
45 match r:
46 case Tuple{tree, found}:
47 match tree:
48 case MTip{}: lower_parent(V, hi, parent, p, lower, below)
49 case MLeaf{k, v}: lower
50 case MNode{q, lo, other}: lower
51
52law high:
53 for -V: Data
54 for +p: Nat
55 for +parent: Nat
56 for lo: Map<&2, V>
57 for r: Map<&2, V> & Maybe<&2, V>
58 for lower: {Nat.is_lt(parent, p) == True{} : Bool}
59 for below: {Inv.below(V, lo, p) == True{} : Bool}
60 {Inv.below(V, Map.del.fin(&2, V, Map.pop.hi(&2, V, p, lo, r)), parent) == True{} : Bool}
61def high(V, p, parent, lo, r, lower, below):
62 match r:
63 case Tuple{tree, found}:
64 match tree:
65 case MTip{}: lower_parent(V, lo, parent, p, lower, below)
66 case MLeaf{k, v}: lower
67 case MNode{q, other, hi}: lower
68
69law leaf:
70 for -V: Data
71 for value: V
72 for key: String
73 for stored: String
74 for tag: Cmp
75 for parent: Nat
76 {Inv.below(V, Map.del.fin(&2, V, Map.pop.leaf(&2, V, value, ((key, stored), tag))), parent) == True{} : Bool}
77def leaf(V, value, key, stored, tag, parent):
78 match tag:
79 case LT{}: {==}
80 case EQ{}: {==}
81 case GT{}: {==}
82
83law branch:
84 for -V: Data
85 for +p: Nat
86 for +parent: Nat
87 for +lo: Map<&2, V>
88 for +hi: Map<&2, V>
89 for +key: String
90 for bit: Bool
91 for route: {Map.bit(key, p) == (key, bit) : String & Bool}
92 for lower: {Nat.is_lt(parent, p) == True{} : Bool}
93 for left: {Inv.below(V, lo, p) == True{} : Bool}
94 for right: {Inv.below(V, hi, p) == True{} : Bool}
95 {Inv.below(V, Map.del(&2, V, MNode{p, lo, hi}, key), parent) == True{} : Bool}
96def branch(V, p, parent, lo, hi, key, bit, route, lower, left, right):
97 match bit:
98 case False{}:
99 %Equal.sym(Map<&2, V> & Maybe<&2, V>, Map.pop(&2, V, MNode{p, lo, hi}, key), MB.pop_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.pop_node(&2, V, p, lo, hi, key)) : {Inv.below(V, Map.del.fin(&2, V, _), parent) == True{} : Bool}
100 %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), route) : {Inv.below(V, Map.del.fin(&2, V, MB.pop_bit(&2, V, lo, hi, p, _)), parent) == True{} : Bool}
101 low(V, p, parent, hi, Map.pop(&2, V, lo, key), lower, right)
102 case True{}:
103 %Equal.sym(Map<&2, V> & Maybe<&2, V>, Map.pop(&2, V, MNode{p, lo, hi}, key), MB.pop_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.pop_node(&2, V, p, lo, hi, key)) : {Inv.below(V, Map.del.fin(&2, V, _), parent) == True{} : Bool}
104 %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), route) : {Inv.below(V, Map.del.fin(&2, V, MB.pop_bit(&2, V, lo, hi, p, _)), parent) == True{} : Bool}
105 high(V, p, parent, lo, Map.pop(&2, V, hi, key), lower, left)
106
107law from_parts:
108 for -V: Data
109 for +p: Nat
110 for +parent: Nat
111 for +lo: Map<&2, V>
112 for +hi: Map<&2, V>
113 for +key: String
114 for below: {Nat.is_lt(parent, p) == True{} : Bool}
115 for parts: Parts.NodeFacts(V, p, lo, hi)
116 {Inv.below(V, Map.del(&2, V, MNode{p, lo, hi}, key), parent) == True{} : Bool}
117def from_parts(V, p, parent, lo, hi, key, below, parts):
118 (prefix, ln, hn, lb, hb, lr, hr, lv, hv) = parts
119 branch(V, p, parent, lo, hi, key, I.route_bit(Map.bit(key, p)), I.route_shape(key, p), below, lb, hb)
120
121# Native deletion either retains the root discriminator or promotes the untouched
122# sibling. The sibling's ordering is derived from the actual critbit predicate.
123law preserves_below:
124 for -V: Data
125 for tree: Map<&2, V>
126 for +key: String
127 for +parent: Nat
128 for valid: {Inv.critbit(V, tree) == True{} : Bool}
129 for below: {Inv.below(V, tree, parent) == True{} : Bool}
130 {Inv.below(V, Map.del(&2, V, tree, key), parent) == True{} : Bool}
131def preserves_below(V, tree, key, parent, valid, below):
132 match tree:
133 case MTip{}: {==}
134 case MLeaf{+stored, +value}:
135 %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)) : {Inv.below(V, Map.del.fin(&2, V, Map.pop.leaf(&2, V, value, _)), parent) == True{} : Bool}
136 leaf(V, value, key, stored, N.comparison_tag(String, String.cmp(key, stored)), parent)
137 case MNode{+p, +lo, +hi}:
138 from_parts(V, p, parent, lo, hi, key, below, Parts.node_parts(V, p, lo, hi, valid))