1	import Base
2	import ./map_insert.bend as I
3	import ./string_compare.bend as N
4	
5	# Structural membership names a real leaf and its exact value. No lookup
6	# algorithm or native-map axiom is hidden in this proposition.
7	def leaf(-V: Data, tree: Map<&2, Maybe<&2, V>>, key: String, value: V) -> Type:
8	  match tree:
9	    case MTip{}:
10	      Empty
11	    case MLeaf{stored, item}:
12	      {key == stored : String} & {Some{value} == item : Maybe<&2, V>}
13	    case MNode{p, lo, hi}:
14	      Either<&1, &1, leaf(V, lo, key, value), leaf(V, hi, key, value)>
15	
16	def certificate(-V: Data, tree: Map<&2, Maybe<&2, V>>, key: String, found: Maybe<&2, V>) -> Type:
17	  match found:
18	    case None{}:
19	      Unit
20	    case Some{value}:
21	      leaf(V, tree, key, value)
22	
23	law leaf_comparison:
24	  for -V: Data
25	  for +key: String
26	  for +stored: String
27	  for item: Maybe<&2, V>
28	  for cmp: Cmp
29	  for e: {N.comparison_tag(String, String.cmp(key, stored)) == cmp : Cmp}
30	  certificate(V, MLeaf{stored, item}, key, I.value(Maybe<&2, V>, Map.get.leaf(Maybe<&2, V>, None{}, item, ((key, stored), cmp))))
31	def leaf_comparison(V, key, stored, item, cmp, e):
32	  match item cmp:
33	    case None{} LT{}:
34	      Unit{}
35	    case None{} EQ{}:
36	      Unit{}
37	    case None{} GT{}:
38	      Unit{}
39	    case Some{value} LT{}:
40	      Unit{}
41	    case Some{value} GT{}:
42	      Unit{}
43	    case Some{value} EQ{}:
44	      (N.string_equal_from_comparison(key, stored, e), {==})
45	
46	law leaf_lookup:
47	  for -V: Data
48	  for +key: String
49	  for +stored: String
50	  for +item: Maybe<&2, V>
51	  certificate(V, MLeaf{stored, item}, key, I.lookup(Maybe<&2, V>, None{}, MLeaf{stored, item}, key))
52	def leaf_lookup(V, key, stored, item):
53	  %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)) : certificate(V, MLeaf{stored, item}, key, I.value(Maybe<&2, V>, Map.get.leaf(Maybe<&2, V>, None{}, item, _)))
54	  leaf_comparison(V, key, stored, item, N.comparison_tag(String, String.cmp(key, stored)), {==})
55	
56	law lift_left:
57	  for -V: Data
58	  for lo: Map<&2, Maybe<&2, V>>
59	  for hi: Map<&2, Maybe<&2, V>>
60	  for p: Nat
61	  for key: String
62	  for found: Maybe<&2, V>
63	  for cp: certificate(V, lo, key, found)
64	  certificate(V, MNode{p, lo, hi}, key, found)
65	def lift_left(V, lo, hi, p, key, found, cp):
66	  match found:
67	    case None{}:
68	      Unit{}
69	    case Some{value}:
70	      Inl{cp}
71	
72	law lift_right:
73	  for -V: Data
74	  for lo: Map<&2, Maybe<&2, V>>
75	  for hi: Map<&2, Maybe<&2, V>>
76	  for p: Nat
77	  for key: String
78	  for found: Maybe<&2, V>
79	  for cp: certificate(V, hi, key, found)
80	  certificate(V, MNode{p, lo, hi}, key, found)
81	def lift_right(V, lo, hi, p, key, found, cp):
82	  match found:
83	    case None{}:
84	      Unit{}
85	    case Some{value}:
86	      Inr{cp}
87	
88	law branch:
89	  for -V: Data
90	  for +lo: Map<&2, Maybe<&2, V>>
91	  for +hi: Map<&2, Maybe<&2, V>>
92	  for +p: Nat
93	  for +key: String
94	  for bit: Bool
95	  for e: {Map.bit(key, p) == (key, bit) : String & Bool}
96	  for lp: certificate(V, lo, key, I.lookup(Maybe<&2, V>, None{}, lo, key))
97	  for hp: certificate(V, hi, key, I.lookup(Maybe<&2, V>, None{}, hi, key))
98	  certificate(V, MNode{p, lo, hi}, key, I.lookup(Maybe<&2, V>, None{}, MNode{p, lo, hi}, key))
99	def branch(V, lo, hi, p, key, bit, e, lp, hp):
100	  match bit:
101	    case False{}:
102	      %Equal.sym(Maybe<&2, V>, I.lookup(Maybe<&2, V>, None{}, MNode{p, lo, hi}, key), I.lookup(Maybe<&2, V>, None{}, lo, key), I.node_left(Maybe<&2, V>, None{}, lo, hi, p, key, e)) : certificate(V, MNode{p, lo, hi}, key, _)
103	      lift_left(V, lo, hi, p, key, I.lookup(Maybe<&2, V>, None{}, lo, key), lp)
104	    case True{}:
105	      %Equal.sym(Maybe<&2, V>, I.lookup(Maybe<&2, V>, None{}, MNode{p, lo, hi}, key), I.lookup(Maybe<&2, V>, None{}, hi, key), I.node_right(Maybe<&2, V>, None{}, lo, hi, p, key, e)) : certificate(V, MNode{p, lo, hi}, key, _)
106	      lift_right(V, lo, hi, p, key, I.lookup(Maybe<&2, V>, None{}, hi, key), hp)
107	
108	law lookup_certificate:
109	  for -V: Data
110	  for tree: Map<&2, Maybe<&2, V>>
111	  for +key: String
112	  certificate(V, tree, key, I.lookup(Maybe<&2, V>, None{}, tree, key))
113	def lookup_certificate(V, tree, key):
114	  match tree:
115	    case MTip{}:
116	      Unit{}
117	    case MLeaf{stored, item}:
118	      leaf_lookup(V, key, stored, item)
119	    case MNode{+p, +lo, +hi}:
120	      branch(V, lo, hi, p, key, I.route_bit(Map.bit(key, p)), I.route_shape(key, p), lookup_certificate(V, lo, key), lookup_certificate(V, hi, key))
121	
122	# No tree validity premise is needed for this direction. Converse membership
123	# implies successful lookup still needs routing/uniqueness invariants.
124	law returned_value_is_stored:
125	  for -V: Data
126	  for +tree: Map<&2, Maybe<&2, V>>
127	  for +key: String
128	  for value: V
129	  for found: {I.lookup(Maybe<&2, V>, None{}, tree, key) == Some{value} : Maybe<&2, V>}
130	  leaf(V, tree, key, value)
131	def returned_value_is_stored(V, tree, key, value, found):
132	  %found : certificate(V, tree, key, _)
133	  lookup_certificate(V, tree, key)
134	
135	# Independent list membership for actual Map.to_list output.
136	def listed(-V: Data, entries: List<&2, Sigma<&2, &2, String, _ => Maybe<&2, V>>>, key: String, value: V) -> Type:
137	  match entries:
138	    case Nil{}:
139	      Empty
140	    case Con{Tuple{stored, item}, tail}:
141	      Either<&1, &1, {key == stored : String} & {Some{value} == item : Maybe<&2, V>}, listed(V, tail, key, value)>
142	
143	law accumulator_included:
144	  for -V: Data
145	  for tree: Map<&2, Maybe<&2, V>>
146	  for +acc: List<&2, Sigma<&2, &2, String, _ => Maybe<&2, V>>>
147	  for +key: String
148	  for +value: V
149	  for member: listed(V, acc, key, value)
150	  listed(V, Map.to_list.go(&2, Maybe<&2, V>, tree, acc), key, value)
151	def accumulator_included(V, tree, acc, key, value, member):
152	  match tree:
153	    case MTip{}:
154	      member
155	    case MLeaf{stored, item}:
156	      Inr{member}
157	    case MNode{p, lo, +hi}:
158	      accumulator_included(V, lo, Map.to_list.go(&2, Maybe<&2, V>, hi, acc), key, value, accumulator_included(V, hi, acc, key, value, member))
159	
160	law leaf_enumerated:
161	  for -V: Data
162	  for tree: Map<&2, Maybe<&2, V>>
163	  for +acc: List<&2, Sigma<&2, &2, String, _ => Maybe<&2, V>>>
164	  for +key: String
165	  for +value: V
166	  for member: leaf(V, tree, key, value)
167	  listed(V, Map.to_list.go(&2, Maybe<&2, V>, tree, acc), key, value)
168	def leaf_enumerated(V, tree, acc, key, value, member):
169	  match tree:
170	    case MTip{}:
171	      Empty.absurd(listed(V, acc, key, value), member)
172	    case MLeaf{stored, item}:
173	      Inl{member}
174	    case MNode{p, +lo, +hi}:
175	      match member:
176	        case Inl{lp}:
177	          leaf_enumerated(V, lo, Map.to_list.go(&2, Maybe<&2, V>, hi, acc), key, value, lp)
178	        case Inr{hp}:
179	          accumulator_included(V, lo, Map.to_list.go(&2, Maybe<&2, V>, hi, acc), key, value, leaf_enumerated(V, hi, acc, key, value, hp))
180	
181	law returned_value_enumerated:
182	  for -V: Data
183	  for +tree: Map<&2, Maybe<&2, V>>
184	  for +key: String
185	  for +value: V
186	  for found: {I.lookup(Maybe<&2, V>, None{}, tree, key) == Some{value} : Maybe<&2, V>}
187	  listed(V, Map.to_list(&2, Maybe<&2, V>, tree), key, value)
188	def returned_value_enumerated(V, tree, key, value, found):
189	  leaf_enumerated(V, tree, Nil{}, key, value, returned_value_is_stored(V, tree, key, value, found))