proofs/containers/dynamic_array/layout.bend
bend-collections-laws-containers@1.0.0.0 · 310 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6
7# Slot layout of a dynamic array: the first n slots are Some, the rest None.
8
9def somes(-T: Data, xs: List<&2, Maybe<&2, T>>) -> List<&2, T>:
10 match xs:
11 case Nil{}:
12 Nil{}
13 case Con{None{}, r}:
14 somes(T, r)
15 case Con{Some{x}, r}:
16 Con{x, somes(T, r)}
17
18def nones(-T: Data, xs: List<&2, Maybe<&2, T>>) -> Bool:
19 match xs:
20 case Nil{}:
21 True{}
22 case Con{None{}, r}:
23 nones(T, r)
24 case Con{Some{x}, r}:
25 False{}
26
27def lay(-T: Data, xs: List<&2, Maybe<&2, T>>, n: Nat) -> Bool:
28 match xs n:
29 case Nil{} 0n:
30 True{}
31 case Nil{} 1n+m:
32 False{}
33 case Con{None{}, r} 0n:
34 nones(T, r)
35 case Con{None{}, r} 1n+m:
36 False{}
37 case Con{Some{x}, r} 0n:
38 False{}
39 case Con{Some{x}, r} 1n+m:
40 lay(T, r, m)
41
42def nones_somes(-T: Data, +xs: List<&2, Maybe<&2, T>>, +h: {nones(T, xs) == True{} : Bool}) -> {somes(T, xs) == Nil{} : List<&2, T>}:
43 match xs:
44 case Nil{}:
45 {==}
46 case Con{None{}, +r}:
47 nones_somes(T, r, h)
48 case Con{Some{x}, r}:
49 Empty.absurd({Con{x, somes(T, r)} == Nil{} : List<&2, T>}, L.false_true(h))
50
51def lay_len(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +h: {lay(T, xs, n) == True{} : Bool}) -> {SC.length(T, somes(T, xs)) == n : Nat}:
52 match xs n:
53 case Nil{} 0n:
54 {==}
55 case Nil{} 1n+m:
56 Empty.absurd({0n == 1n+m : Nat}, L.false_true(h))
57 case Con{None{}, +r} 0n:
58 %Equal.sym(List<&2, T>, somes(T, r), Nil{}, nones_somes(T, r, h)) : {SC.length(T, _) == 0n : Nat}
59 {==}
60 case Con{None{}, r} 1n+m:
61 Empty.absurd({SC.length(T, somes(T, r)) == 1n+m : Nat}, L.false_true(h))
62 case Con{Some{x}, r} 0n:
63 Empty.absurd({1n+SC.length(T, somes(T, r)) == 0n : Nat}, L.false_true(h))
64 case Con{Some{x}, +r} 1n+m:
65 N.succ_cong(SC.length(T, somes(T, r)), m, lay_len(T, r, m, h))
66
67def lay_le(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +h: {lay(T, xs, n) == True{} : Bool}) -> {Nat.is_le(n, SC.length(Maybe<&2, T>, xs)) == True{} : Bool}:
68 match xs n:
69 case Nil{} 0n:
70 {==}
71 case Nil{} 1n+m:
72 Empty.absurd({Nat.is_le(1n+m, 0n) == True{} : Bool}, L.false_true(h))
73 case Con{None{}, r} 0n:
74 {==}
75 case Con{None{}, r} 1n+m:
76 Empty.absurd({Nat.is_le(1n+m, 1n+SC.length(Maybe<&2, T>, r)) == True{} : Bool}, L.false_true(h))
77 case Con{Some{x}, r} 0n:
78 {==}
79 case Con{Some{x}, +r} 1n+m:
80 lay_le(T, r, m, h)
81
82def lay_nil_pos(-T: Data, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {lay(T, Nil{}, n) == False{} : Bool}:
83 match n:
84 case 0n:
85 Empty.absurd({True{} == False{} : Bool}, N.lt_zero_absurd(i, hi))
86 case 1n+m:
87 {==}
88
89# Slot i (< n) holds exactly the i-th item.
90def lay_nth(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +i: Nat, +h: {lay(T, xs, n) == True{} : Bool}, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {SC.nth(Maybe<&2, T>, xs, i) == Some{SC.nth(T, somes(T, xs), i)} : Maybe<&2, Maybe<&2, T>>}:
91 match xs n i:
92 case Nil{} _ _:
93 Empty.absurd({None{} == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, L.true_not_false(lay(T, Nil{}, n), h, lay_nil_pos(T, n, i, hi)))
94 case Con{None{}, r} 0n _:
95 Empty.absurd({SC.nth(Maybe<&2, T>, Con{None{}, r}, i) == Some{SC.nth(T, somes(T, r), i)} : Maybe<&2, Maybe<&2, T>>}, N.lt_zero_absurd(i, hi))
96 case Con{None{}, r} 1n+m _:
97 Empty.absurd({SC.nth(Maybe<&2, T>, Con{None{}, r}, i) == Some{SC.nth(T, somes(T, r), i)} : Maybe<&2, Maybe<&2, T>>}, L.false_true(h))
98 case Con{Some{x}, r} 0n _:
99 Empty.absurd({SC.nth(Maybe<&2, T>, Con{Some{x}, r}, i) == Some{SC.nth(T, Con{x, somes(T, r)}, i)} : Maybe<&2, Maybe<&2, T>>}, L.false_true(h))
100 case Con{Some{x}, r} 1n+m 0n:
101 {==}
102 case Con{Some{x}, +r} 1n+m 1n+j:
103 lay_nth(T, r, m, j, h, hi)
104
105def nones_nth(-T: Data, +xs: List<&2, Maybe<&2, T>>, +i: Nat, +h: {nones(T, xs) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.length(Maybe<&2, T>, xs)) == True{} : Bool}) -> {SC.nth(Maybe<&2, T>, xs, i) == Some{None{}} : Maybe<&2, Maybe<&2, T>>}:
106 match xs i:
107 case Nil{} _:
108 Empty.absurd({None{} == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, N.lt_zero_absurd(i, hi))
109 case Con{None{}, r} 0n:
110 {==}
111 case Con{None{}, +r} 1n+j:
112 nones_nth(T, r, j, h, hi)
113 case Con{Some{x}, r} _:
114 Empty.absurd({SC.nth(Maybe<&2, T>, Con{Some{x}, r}, i) == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, L.false_true(h))
115
116def nones_rep(-T: Data, +k: Nat) -> {nones(T, SC.replicate(Maybe<&2, T>, k, None{})) == True{} : Bool}:
117 match k:
118 case 0n:
119 {==}
120 case 1n+j:
121 nones_rep(T, j)
122
123def somes_rep(-T: Data, +k: Nat) -> {somes(T, SC.replicate(Maybe<&2, T>, k, None{})) == Nil{} : List<&2, T>}:
124 match k:
125 case 0n:
126 {==}
127 case 1n+j:
128 somes_rep(T, j)
129
130def lay_rep(-T: Data, +k: Nat) -> {lay(T, SC.replicate(Maybe<&2, T>, k, None{}), 0n) == True{} : Bool}:
131 match k:
132 case 0n:
133 {==}
134 case 1n+j:
135 nones_rep(T, j)
136
137def nones_lay0(-T: Data, +xs: List<&2, Maybe<&2, T>>, +h: {nones(T, xs) == True{} : Bool}) -> {lay(T, xs, 0n) == True{} : Bool}:
138 match xs:
139 case Nil{}:
140 {==}
141 case Con{None{}, r}:
142 h
143 case Con{Some{x}, r}:
144 h
145
146def lay0_nones(-T: Data, +xs: List<&2, Maybe<&2, T>>, +h: {lay(T, xs, 0n) == True{} : Bool}) -> {nones(T, xs) == True{} : Bool}:
147 match xs:
148 case Nil{}:
149 {==}
150 case Con{None{}, r}:
151 h
152 case Con{Some{x}, r}:
153 h
154
155def nones_append(-T: Data, +xs: List<&2, Maybe<&2, T>>, +ys: List<&2, Maybe<&2, T>>, +hx: {nones(T, xs) == True{} : Bool}, +hy: {nones(T, ys) == True{} : Bool}) -> {nones(T, SC.append(Maybe<&2, T>, xs, ys)) == True{} : Bool}:
156 match xs:
157 case Nil{}:
158 hy
159 case Con{None{}, +r}:
160 nones_append(T, r, ys, hx, hy)
161 case Con{Some{x}, r}:
162 hx
163
164# ---- set ----
165
166def lay_set(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +i: Nat, +v: T, +h: {lay(T, xs, n) == True{} : Bool}, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {lay(T, SC.update(Maybe<&2, T>, xs, i, Some{v}), n) == True{} : Bool}:
167 match xs n i:
168 case Nil{} _ _:
169 Empty.absurd({lay(T, Nil{}, n) == True{} : Bool}, L.true_not_false(lay(T, Nil{}, n), h, lay_nil_pos(T, n, i, hi)))
170 case Con{None{}, r} 0n _:
171 Empty.absurd({lay(T, SC.update(Maybe<&2, T>, Con{None{}, r}, i, Some{v}), 0n) == True{} : Bool}, N.lt_zero_absurd(i, hi))
172 case Con{None{}, r} 1n+m _:
173 Empty.absurd({lay(T, SC.update(Maybe<&2, T>, Con{None{}, r}, i, Some{v}), 1n+m) == True{} : Bool}, L.false_true(h))
174 case Con{Some{x}, r} 0n _:
175 Empty.absurd({lay(T, SC.update(Maybe<&2, T>, Con{Some{x}, r}, i, Some{v}), 0n) == True{} : Bool}, L.false_true(h))
176 case Con{Some{x}, r} 1n+m 0n:
177 h
178 case Con{Some{x}, +r} 1n+m 1n+j:
179 lay_set(T, r, m, j, v, h, hi)
180
181def somes_set(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +i: Nat, +v: T, +h: {lay(T, xs, n) == True{} : Bool}, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {somes(T, SC.update(Maybe<&2, T>, xs, i, Some{v})) == SC.update(T, somes(T, xs), i, v) : List<&2, T>}:
182 match xs n i:
183 case Nil{} _ _:
184 Empty.absurd({Nil{} == Nil{} : List<&2, T>}, L.true_not_false(lay(T, Nil{}, n), h, lay_nil_pos(T, n, i, hi)))
185 case Con{None{}, r} 0n _:
186 Empty.absurd({somes(T, SC.update(Maybe<&2, T>, Con{None{}, r}, i, Some{v})) == SC.update(T, somes(T, r), i, v) : List<&2, T>}, N.lt_zero_absurd(i, hi))
187 case Con{None{}, r} 1n+m _:
188 Empty.absurd({somes(T, SC.update(Maybe<&2, T>, Con{None{}, r}, i, Some{v})) == SC.update(T, somes(T, r), i, v) : List<&2, T>}, L.false_true(h))
189 case Con{Some{x}, r} 0n _:
190 Empty.absurd({somes(T, SC.update(Maybe<&2, T>, Con{Some{x}, r}, i, Some{v})) == SC.update(T, Con{x, somes(T, r)}, i, v) : List<&2, T>}, L.false_true(h))
191 case Con{Some{x}, r} 1n+m 0n:
192 {==}
193 case Con{Some{+x}, +r} 1n+m 1n+j:
194 LL.cons_cong(T, x, somes(T, SC.update(Maybe<&2, T>, r, j, Some{v})), SC.update(T, somes(T, r), j, v), somes_set(T, r, m, j, v, h, hi))
195
196# ---- push (slot n is the first free one) ----
197
198def push_free(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +h: {lay(T, xs, n) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.length(Maybe<&2, T>, xs)) == True{} : Bool}) -> {SC.nth(Maybe<&2, T>, xs, n) == Some{None{}} : Maybe<&2, Maybe<&2, T>>}:
199 match xs n:
200 case Nil{} _:
201 Empty.absurd({None{} == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, N.lt_zero_absurd(n, hn))
202 case Con{None{}, r} 0n:
203 {==}
204 case Con{None{}, r} 1n+m:
205 Empty.absurd({SC.nth(Maybe<&2, T>, r, m) == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, L.false_true(h))
206 case Con{Some{x}, r} 0n:
207 Empty.absurd({Some{Some{x}} == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, L.false_true(h))
208 case Con{Some{x}, +r} 1n+m:
209 push_free(T, r, m, h, hn)
210
211def lay_push(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +v: T, +h: {lay(T, xs, n) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.length(Maybe<&2, T>, xs)) == True{} : Bool}) -> {lay(T, SC.update(Maybe<&2, T>, xs, n, Some{v}), 1n+n) == True{} : Bool}:
212 match xs n:
213 case Nil{} _:
214 Empty.absurd({lay(T, Nil{}, 1n+n) == True{} : Bool}, N.lt_zero_absurd(n, hn))
215 case Con{None{}, +r} 0n:
216 nones_lay0(T, r, h)
217 case Con{None{}, r} 1n+m:
218 Empty.absurd({lay(T, Con{None{}, SC.update(Maybe<&2, T>, r, m, Some{v})}, 2n+m) == True{} : Bool}, L.false_true(h))
219 case Con{Some{x}, r} 0n:
220 Empty.absurd({lay(T, Con{Some{v}, r}, 1n) == True{} : Bool}, L.false_true(h))
221 case Con{Some{x}, +r} 1n+m:
222 lay_push(T, r, m, v, h, hn)
223
224def somes_push(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +v: T, +h: {lay(T, xs, n) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.length(Maybe<&2, T>, xs)) == True{} : Bool}) -> {somes(T, SC.update(Maybe<&2, T>, xs, n, Some{v})) == SC.snoc(T, somes(T, xs), v) : List<&2, T>}:
225 match xs n:
226 case Nil{} _:
227 Empty.absurd({Nil{} == Con{v, Nil{}} : List<&2, T>}, N.lt_zero_absurd(n, hn))
228 case Con{None{}, +r} 0n:
229 %Equal.sym(List<&2, T>, somes(T, r), Nil{}, nones_somes(T, r, h)) : {Con{v, _} == SC.snoc(T, _, v) : List<&2, T>}
230 {==}
231 case Con{None{}, r} 1n+m:
232 Empty.absurd({somes(T, Con{None{}, SC.update(Maybe<&2, T>, r, m, Some{v})}) == SC.snoc(T, somes(T, r), v) : List<&2, T>}, L.false_true(h))
233 case Con{Some{x}, r} 0n:
234 Empty.absurd({Con{v, somes(T, r)} == SC.snoc(T, Con{x, somes(T, r)}, v) : List<&2, T>}, L.false_true(h))
235 case Con{Some{+x}, +r} 1n+m:
236 LL.cons_cong(T, x, somes(T, SC.update(Maybe<&2, T>, r, m, Some{v})), SC.snoc(T, somes(T, r), v), somes_push(T, r, m, v, h, hn))
237
238# ---- pop (slot m of a layout with m+1 items) ----
239
240def lay_pop(-T: Data, +xs: List<&2, Maybe<&2, T>>, +m: Nat, +h: {lay(T, xs, 1n+m) == True{} : Bool}) -> {lay(T, SC.update(Maybe<&2, T>, xs, m, None{}), m) == True{} : Bool}:
241 match xs m:
242 case Nil{} _:
243 Empty.absurd({lay(T, Nil{}, m) == True{} : Bool}, L.false_true(h))
244 case Con{None{}, r} _:
245 Empty.absurd({lay(T, SC.update(Maybe<&2, T>, Con{None{}, r}, m, None{}), m) == True{} : Bool}, L.false_true(h))
246 case Con{Some{x}, +r} 0n:
247 lay0_nones(T, r, h)
248 case Con{Some{x}, +r} 1n+k:
249 lay_pop(T, r, k, h)
250
251def init_cons(-T: Data, +x: T, +ys: List<&2, T>, +k: Nat, +h: {SC.length(T, ys) == 1n+k : Nat}) -> {SC.init(T, Con{x, ys}) == Con{x, SC.init(T, ys)} : List<&2, T>}:
252 match ys:
253 case Nil{}:
254 Empty.absurd({Nil{} == Con{x, Nil{}} : List<&2, T>}, N.zero_succ(k, h))
255 case Con{y, t}:
256 {==}
257
258def somes_pop(-T: Data, +xs: List<&2, Maybe<&2, T>>, +m: Nat, +h: {lay(T, xs, 1n+m) == True{} : Bool}) -> {somes(T, SC.update(Maybe<&2, T>, xs, m, None{})) == SC.init(T, somes(T, xs)) : List<&2, T>}:
259 match xs m:
260 case Nil{} _:
261 Empty.absurd({Nil{} == Nil{} : List<&2, T>}, L.false_true(h))
262 case Con{None{}, r} _:
263 Empty.absurd({somes(T, SC.update(Maybe<&2, T>, Con{None{}, r}, m, None{})) == SC.init(T, somes(T, r)) : List<&2, T>}, L.false_true(h))
264 case Con{Some{x}, +r} 0n:
265 %Equal.sym(List<&2, T>, somes(T, r), Nil{}, nones_somes(T, r, lay0_nones(T, r, h))) : {_ == SC.init(T, Con{x, _}) : List<&2, T>}
266 {==}
267 case Con{Some{+x}, +r} 1n+k:
268 Equal.trans(List<&2, T>, Con{x, somes(T, SC.update(Maybe<&2, T>, r, k, None{}))}, Con{x, SC.init(T, somes(T, r))}, SC.init(T, Con{x, somes(T, r)}),
269 LL.cons_cong(T, x, somes(T, SC.update(Maybe<&2, T>, r, k, None{})), SC.init(T, somes(T, r)), somes_pop(T, r, k, h)),
270 Equal.sym(List<&2, T>, SC.init(T, Con{x, somes(T, r)}), Con{x, SC.init(T, somes(T, r))}, init_cons(T, x, somes(T, r), k, lay_len(T, r, 1n+k, h))))
271
272# nth at the last position is last.
273def nth_last(-T: Data, +ys: List<&2, T>, +m: Nat, +h: {SC.length(T, ys) == 1n+m : Nat}) -> {SC.nth(T, ys, m) == SC.last(T, ys) : Maybe<&2, T>}:
274 match ys m:
275 case Nil{} _:
276 Empty.absurd({None{} == None{} : Maybe<&2, T>}, N.zero_succ(m, h))
277 case Con{y, Nil{}} 0n:
278 {==}
279 case Con{y, Con{y2, t2}} 0n:
280 Empty.absurd({Some{y} == SC.last(T, Con{y2, t2}) : Maybe<&2, T>}, N.succ_zero(SC.length(T, t2), N.succ_inj(1n+SC.length(T, t2), 0n, h)))
281 case Con{y, Nil{}} 1n+k:
282 Empty.absurd({SC.nth(T, Nil{}, k) == Some{y} : Maybe<&2, T>}, N.zero_succ(k, N.succ_inj(0n, 1n+k, h)))
283 case Con{y, Con{+y2, +t2}} 1n+k:
284 nth_last(T, Con{y2, t2}, k, N.succ_inj(1n+SC.length(T, t2), 1n+k, h))
285
286# ---- growth (append free slots) and clear ----
287
288def lay_grow(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +k: Nat, +h: {lay(T, xs, n) == True{} : Bool}) -> {lay(T, SC.append(Maybe<&2, T>, xs, SC.replicate(Maybe<&2, T>, k, None{})), n) == True{} : Bool}:
289 match xs n:
290 case Nil{} 0n:
291 lay_rep(T, k)
292 case Nil{} 1n+m:
293 Empty.absurd({lay(T, SC.replicate(Maybe<&2, T>, k, None{}), 1n+m) == True{} : Bool}, L.false_true(h))
294 case Con{None{}, +r} 0n:
295 nones_append(T, r, SC.replicate(Maybe<&2, T>, k, None{}), h, nones_rep(T, k))
296 case Con{None{}, r} 1n+m:
297 h
298 case Con{Some{x}, r} 0n:
299 h
300 case Con{Some{x}, +r} 1n+m:
301 lay_grow(T, r, m, k, h)
302
303def somes_grow(-T: Data, +xs: List<&2, Maybe<&2, T>>, +k: Nat) -> {somes(T, SC.append(Maybe<&2, T>, xs, SC.replicate(Maybe<&2, T>, k, None{}))) == somes(T, xs) : List<&2, T>}:
304 match xs:
305 case Nil{}:
306 somes_rep(T, k)
307 case Con{None{}, +r}:
308 somes_grow(T, r, k)
309 case Con{Some{+x}, +r}:
310 LL.cons_cong(T, x, somes(T, SC.append(Maybe<&2, T>, r, SC.replicate(Maybe<&2, T>, k, None{}))), somes(T, r), somes_grow(T, r, k))