proofs/lib/lemmas/proofs/map_lookup.bend
bend-collections-laws-containers@1.0.0.0 · 189 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend as I
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/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.
7def 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
16def 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
23law 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))))
31def 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
46law 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))
52def 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
56law 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)
65def 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
72law 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)
81def 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
88law 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))
99def 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
108law 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))
113def 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.
124law 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)
131def 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.
136def 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
143law 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)
151def 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
160law 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)
168def 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
181law 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)
188def 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))