1	import Base
2	import ./map_bridge.bend as MB
3	import ./map_insert.bend as I
4	import ./map_lookup.bend as L
5	import ./map_routing.bend as R
6	import ./invariants.bend as Inv
7	import ./string_compare.bend as N
8	
9	law different_sides:
10	  for side: Bool
11	  for e: {side == Bool.not(side) : Bool}
12	  Empty
13	def 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	
20	law 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
27	def 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	
30	law 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>}
42	def 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	
49	law 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>}
58	def 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	
61	law 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>}
71	def 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	
82	law 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>}
92	def 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	
103	law 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>}
111	def 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	
122	law 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>}
128	def 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	
132	law 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>}
145	def 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	
156	law 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>}
162	def 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	
172	law 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>}
178	def critbit_delete_same(V, tree, key, invariant):
179	  delete_same(V, tree, key, R.critbit_certificate(Maybe<&2, V>, tree, invariant))