proofs/lib/list.bend

bend-collections-laws-crypto@1.0.0.0 · 414 lines · 46 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
5
6# Lemmas about the specification list vocabulary (spec/common.bend).
7
8def cons_cong(-A: Data, +h: A, +xs: List<&2, A>, +ys: List<&2, A>, +e: {xs == ys : List<&2, A>}) -> {Con{h, xs} == Con{h, ys} : List<&2, A>}:
9  Equal.cong(List<&2, A>, List<&2, A>, zs => Con{h, zs}, xs, ys, e)
10
11def append_nil(-A: Data, +xs: List<&2, A>) -> {SC.append(A, xs, Nil{}) == xs : List<&2, A>}:
12  match xs:
13    case Nil{}:
14      {==}
15    case Con{+h, +t}:
16      cons_cong(A, h, SC.append(A, t, Nil{}), t, append_nil(A, t))
17
18def append_assoc(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +zs: List<&2, A>) -> {SC.append(A, SC.append(A, xs, ys), zs) == SC.append(A, xs, SC.append(A, ys, zs)) : List<&2, A>}:
19  match xs:
20    case Nil{}:
21      {==}
22    case Con{+h, +t}:
23      cons_cong(A, h, SC.append(A, SC.append(A, t, ys), zs), SC.append(A, t, SC.append(A, ys, zs)), append_assoc(A, t, ys, zs))
24
25def length_append(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) -> {SC.length(A, SC.append(A, xs, ys)) == Nat.add(SC.length(A, xs), SC.length(A, ys)) : Nat}:
26  match xs:
27    case Nil{}:
28      {==}
29    case Con{+h, +t}:
30      N.succ_cong(SC.length(A, SC.append(A, t, ys)), Nat.add(SC.length(A, t), SC.length(A, ys)), length_append(A, t, ys))
31
32def snoc_append(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.snoc(A, xs, x) == SC.append(A, xs, Con{x, Nil{}}) : List<&2, A>}:
33  match xs:
34    case Nil{}:
35      {==}
36    case Con{+h, +t}:
37      cons_cong(A, h, SC.snoc(A, t, x), SC.append(A, t, Con{x, Nil{}}), snoc_append(A, t, x))
38
39def length_snoc(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.length(A, SC.snoc(A, xs, x)) == 1n+SC.length(A, xs) : Nat}:
40  match xs:
41    case Nil{}:
42      {==}
43    case Con{+h, +t}:
44      N.succ_cong(SC.length(A, SC.snoc(A, t, x)), 1n+SC.length(A, t), length_snoc(A, t, x))
45
46def length_replicate(-A: Data, +n: Nat, +x: A) -> {SC.length(A, SC.replicate(A, n, x)) == n : Nat}:
47  match n:
48    case 0n:
49      {==}
50    case 1n+p:
51      N.succ_cong(SC.length(A, SC.replicate(A, p, x)), p, length_replicate(A, p, x))
52
53def replicate_add(-A: Data, +m: Nat, +n: Nat, +x: A) -> {SC.append(A, SC.replicate(A, m, x), SC.replicate(A, n, x)) == SC.replicate(A, Nat.add(m, n), x) : List<&2, A>}:
54  match m:
55    case 0n:
56      {==}
57    case 1n+p:
58      cons_cong(A, x, SC.append(A, SC.replicate(A, p, x), SC.replicate(A, n, x)), SC.replicate(A, Nat.add(p, n), x), replicate_add(A, p, n, x))
59
60# ---- nth / update across append ----
61
62def nth_append_left(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}) -> {SC.nth(A, SC.append(A, xs, ys), i) == SC.nth(A, xs, i) : Maybe<&2, A>}:
63  match xs i:
64    case Nil{} _:
65      Empty.absurd({SC.nth(A, ys, i) == None{} : Maybe<&2, A>}, N.lt_zero_absurd(i, h))
66    case Con{h1, t} 0n:
67      {==}
68    case Con{h1, t} 1n+p:
69      nth_append_left(A, t, ys, p, h)
70
71def nth_append_right(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +h: {Nat.is_le(SC.length(A, xs), i) == True{} : Bool}) -> {SC.nth(A, SC.append(A, xs, ys), i) == SC.nth(A, ys, Nat.sub(i, SC.length(A, xs))) : Maybe<&2, A>}:
72  match xs i:
73    case Nil{} _:
74      %Equal.sym(Nat, Nat.sub(i, 0n), i, N.sub_zero(i)) : {SC.nth(A, ys, i) == SC.nth(A, ys, _) : Maybe<&2, A>}
75      {==}
76    case Con{h1, t} 0n:
77      Empty.absurd({SC.nth(A, SC.append(A, Con{h1, t}, ys), 0n) == SC.nth(A, ys, Nat.sub(0n, 1n+SC.length(A, t))) : Maybe<&2, A>}, L.false_true(h))
78    case Con{h1, t} 1n+p:
79      nth_append_right(A, t, ys, p, h)
80
81def update_append_left(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +v: A, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}) -> {SC.update(A, SC.append(A, xs, ys), i, v) == SC.append(A, SC.update(A, xs, i, v), ys) : List<&2, A>}:
82  match xs i:
83    case Nil{} _:
84      Empty.absurd({SC.update(A, ys, i, v) == SC.append(A, Nil{}, ys) : List<&2, A>}, N.lt_zero_absurd(i, h))
85    case Con{h1, t} 0n:
86      {==}
87    case Con{+h1, t} 1n+p:
88      cons_cong(A, h1, SC.update(A, SC.append(A, t, ys), p, v), SC.append(A, SC.update(A, t, p, v), ys), update_append_left(A, t, ys, p, v, h))
89
90def update_append_right(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +v: A, +h: {Nat.is_le(SC.length(A, xs), i) == True{} : Bool}) -> {SC.update(A, SC.append(A, xs, ys), i, v) == SC.append(A, xs, SC.update(A, ys, Nat.sub(i, SC.length(A, xs)), v)) : List<&2, A>}:
91  match xs i:
92    case Nil{} _:
93      %Equal.sym(Nat, Nat.sub(i, 0n), i, N.sub_zero(i)) : {SC.update(A, ys, i, v) == SC.update(A, ys, _, v) : List<&2, A>}
94      {==}
95    case Con{h1, t} 0n:
96      Empty.absurd({SC.update(A, SC.append(A, Con{h1, t}, ys), 0n, v) == SC.append(A, Con{h1, t}, SC.update(A, ys, Nat.sub(0n, 1n+SC.length(A, t)), v)) : List<&2, A>}, L.false_true(h))
97    case Con{+h1, t} 1n+p:
98      cons_cong(A, h1, SC.update(A, SC.append(A, t, ys), p, v), SC.append(A, t, SC.update(A, ys, Nat.sub(p, SC.length(A, t)), v)), update_append_right(A, t, ys, p, v, h))
99
100def length_update(-A: Data, +xs: List<&2, A>, +i: Nat, +v: A) -> {SC.length(A, SC.update(A, xs, i, v)) == SC.length(A, xs) : Nat}:
101  match xs i:
102    case Nil{} _:
103      {==}
104    case Con{h1, t} 0n:
105      {==}
106    case Con{h1, t} 1n+p:
107      N.succ_cong(SC.length(A, SC.update(A, t, p, v)), SC.length(A, t), length_update(A, t, p, v))
108
109def nth_lt_length(-A: Data, +xs: List<&2, A>, +i: Nat, +x: A, +h: {SC.nth(A, xs, i) == Some{x} : Maybe<&2, A>}) -> {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}:
110  match xs i:
111    case Nil{} _:
112      Empty.absurd({Nat.is_lt(i, 0n) == True{} : Bool}, L.none_some(A, x, h))
113    case Con{h1, t} 0n:
114      {==}
115    case Con{h1, t} 1n+p:
116      nth_lt_length(A, t, p, x, h)
117
118def nth_update_same(-A: Data, +xs: List<&2, A>, +i: Nat, +v: A, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}) -> {SC.nth(A, SC.update(A, xs, i, v), i) == Some{v} : Maybe<&2, A>}:
119  match xs i:
120    case Nil{} _:
121      Empty.absurd({SC.nth(A, Nil{}, i) == Some{v} : Maybe<&2, A>}, N.lt_zero_absurd(i, h))
122    case Con{h1, t} 0n:
123      {==}
124    case Con{h1, t} 1n+p:
125      nth_update_same(A, t, p, v, h)
126
127def nth_none(-A: Data, +xs: List<&2, A>, +i: Nat, +h: {Nat.is_le(SC.length(A, xs), i) == True{} : Bool}) -> {SC.nth(A, xs, i) == None{} : Maybe<&2, A>}:
128  match xs i:
129    case Nil{} _:
130      {==}
131    case Con{x, t} 0n:
132      Empty.absurd({Some{x} == None{} : Maybe<&2, A>}, L.false_true(h))
133    case Con{x, +t} 1n+p:
134      nth_none(A, t, p, h)
135
136# Base List.append agrees with the specification append.
137def base_append(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) -> {List.append(&2, A, xs, ys) == SC.append(A, xs, ys) : List<&2, A>}:
138  match xs:
139    case Nil{}:
140      {==}
141    case Con{+h, +t}:
142      cons_cong(A, h, List.append(&2, A, t, ys), SC.append(A, t, ys), base_append(A, t, ys))
143
144def length_zero_nil(-A: Data, +xs: List<&2, A>, +h: {SC.length(A, xs) == 0n : Nat}) -> {xs == Nil{} : List<&2, A>}:
145  match xs:
146    case Nil{}:
147      {==}
148    case Con{x, t}:
149      Empty.absurd({Con{x, t} == Nil{} : List<&2, A>}, N.succ_zero(SC.length(A, t), h))
150
151# reverse.go(reverse.go(xs, a), b) == reverse.go(a, xs ++ b)
152def rev_go_twice(-A: Data, +xs: List<&2, A>, +a: List<&2, A>, +b: List<&2, A>) -> {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, a), b) == List.reverse.go(&2, A, a, SC.append(A, xs, b)) : List<&2, A>}:
153  match xs:
154    case Nil{}:
155      {==}
156    case Con{+h, +t}:
157      rev_go_twice(A, t, Con{h, a}, b)
158
159def rev_rev(-A: Data, +xs: List<&2, A>) -> {List.reverse(&2, A, List.reverse.go(&2, A, xs, Nil{})) == xs : List<&2, A>}:
160  Equal.trans(List<&2, A>, List.reverse.go(&2, A, List.reverse.go(&2, A, xs, Nil{}), Nil{}), SC.append(A, xs, Nil{}), xs, rev_go_twice(A, xs, Nil{}, Nil{}), append_nil(A, xs))
161
162def nth_update_other(-A: Data, +xs: List<&2, A>, +i: Nat, +j: Nat, +v: A, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {SC.nth(A, SC.update(A, xs, i, v), j) == SC.nth(A, xs, j) : Maybe<&2, A>}:
163  match xs i j:
164    case Nil{} _ _:
165      {==}
166    case Con{h, t} 0n 0n:
167      Empty.absurd({Some{v} == Some{h} : Maybe<&2, A>}, L.true_false(ne))
168    case Con{h, t} 0n 1n+q:
169      {==}
170    case Con{h, t} 1n+p 0n:
171      {==}
172    case Con{h, +t} 1n+p 1n+q:
173      nth_update_other(A, t, p, q, v, ne)
174
175# ---- snoc / reverse ----
176
177def append_snoc(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +x: A) -> {SC.append(A, xs, SC.snoc(A, ys, x)) == SC.snoc(A, SC.append(A, xs, ys), x) : List<&2, A>}:
178  match xs:
179    case Nil{}:
180      {==}
181    case Con{+h, +t}:
182      cons_cong(A, h, SC.append(A, t, SC.snoc(A, ys, x)), SC.snoc(A, SC.append(A, t, ys), x), append_snoc(A, t, ys, x))
183
184def snoc_append_cons(-A: Data, +xs: List<&2, A>, +x: A, +acc: List<&2, A>) -> {SC.append(A, SC.snoc(A, xs, x), acc) == SC.append(A, xs, Con{x, acc}) : List<&2, A>}:
185  match xs:
186    case Nil{}:
187      {==}
188    case Con{+h, +t}:
189      cons_cong(A, h, SC.append(A, SC.snoc(A, t, x), acc), SC.append(A, t, Con{x, acc}), snoc_append_cons(A, t, x, acc))
190
191def rev_snoc(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.reverse(A, SC.snoc(A, xs, x)) == Con{x, SC.reverse(A, xs)} : List<&2, A>}:
192  match xs:
193    case Nil{}:
194      {==}
195    case Con{+h, +t}:
196      Equal.cong(List<&2, A>, List<&2, A>, zs => SC.snoc(A, zs, h), SC.reverse(A, SC.snoc(A, t, x)), Con{x, SC.reverse(A, t)}, rev_snoc(A, t, x))
197
198def spec_rev_rev(-A: Data, +xs: List<&2, A>) -> {SC.reverse(A, SC.reverse(A, xs)) == xs : List<&2, A>}:
199  match xs:
200    case Nil{}:
201      {==}
202    case Con{+h, +t}:
203      Equal.trans(List<&2, A>, SC.reverse(A, SC.snoc(A, SC.reverse(A, t), h)), Con{h, SC.reverse(A, SC.reverse(A, t))}, Con{h, t},
204        rev_snoc(A, SC.reverse(A, t), h), cons_cong(A, h, SC.reverse(A, SC.reverse(A, t)), t, spec_rev_rev(A, t)))
205
206def rev_append(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) -> {SC.reverse(A, SC.append(A, xs, ys)) == SC.append(A, SC.reverse(A, ys), SC.reverse(A, xs)) : List<&2, A>}:
207  match xs:
208    case Nil{}:
209      Equal.sym(List<&2, A>, SC.append(A, SC.reverse(A, ys), Nil{}), SC.reverse(A, ys), append_nil(A, SC.reverse(A, ys)))
210    case Con{+h, +t}:
211      Equal.trans(List<&2, A>, SC.snoc(A, SC.reverse(A, SC.append(A, t, ys)), h), SC.snoc(A, SC.append(A, SC.reverse(A, ys), SC.reverse(A, t)), h), SC.append(A, SC.reverse(A, ys), SC.snoc(A, SC.reverse(A, t), h)),
212        Equal.cong(List<&2, A>, List<&2, A>, zs => SC.snoc(A, zs, h), SC.reverse(A, SC.append(A, t, ys)), SC.append(A, SC.reverse(A, ys), SC.reverse(A, t)), rev_append(A, t, ys)),
213        Equal.sym(List<&2, A>, SC.append(A, SC.reverse(A, ys), SC.snoc(A, SC.reverse(A, t), h)), SC.snoc(A, SC.append(A, SC.reverse(A, ys), SC.reverse(A, t)), h), append_snoc(A, SC.reverse(A, ys), SC.reverse(A, t), h)))
214
215def length_rev(-A: Data, +xs: List<&2, A>) -> {SC.length(A, SC.reverse(A, xs)) == SC.length(A, xs) : Nat}:
216  match xs:
217    case Nil{}:
218      {==}
219    case Con{+h, +t}:
220      Equal.trans(Nat, SC.length(A, SC.snoc(A, SC.reverse(A, t), h)), 1n+SC.length(A, SC.reverse(A, t)), 1n+SC.length(A, t), length_snoc(A, SC.reverse(A, t), h), N.succ_cong(SC.length(A, SC.reverse(A, t)), SC.length(A, t), length_rev(A, t)))
221
222def base_rev_go(-A: Data, +xs: List<&2, A>, +acc: List<&2, A>) -> {List.reverse.go(&2, A, xs, acc) == SC.append(A, SC.reverse(A, xs), acc) : List<&2, A>}:
223  match xs:
224    case Nil{}:
225      {==}
226    case Con{+h, +t}:
227      Equal.trans(List<&2, A>, List.reverse.go(&2, A, t, Con{h, acc}), SC.append(A, SC.reverse(A, t), Con{h, acc}), SC.append(A, SC.snoc(A, SC.reverse(A, t), h), acc),
228        base_rev_go(A, t, Con{h, acc}), Equal.sym(List<&2, A>, SC.append(A, SC.snoc(A, SC.reverse(A, t), h), acc), SC.append(A, SC.reverse(A, t), Con{h, acc}), snoc_append_cons(A, SC.reverse(A, t), h, acc)))
229
230def base_rev(-A: Data, +xs: List<&2, A>) -> {List.reverse(&2, A, xs) == SC.reverse(A, xs) : List<&2, A>}:
231  Equal.trans(List<&2, A>, List.reverse.go(&2, A, xs, Nil{}), SC.append(A, SC.reverse(A, xs), Nil{}), SC.reverse(A, xs), base_rev_go(A, xs, Nil{}), append_nil(A, SC.reverse(A, xs)))
232
233# ---- Base take / drop ----
234
235def base_take_drop(-A: Data, +xs: List<&2, A>, +k: Nat) -> {SC.append(A, List.take(&2, A, xs, k), List.drop(&2, A, xs, k)) == xs : List<&2, A>}:
236  match xs k:
237    case Nil{} _:
238      {==}
239    case Con{h, t} 0n:
240      {==}
241    case Con{+h, +t} 1n+p:
242      cons_cong(A, h, SC.append(A, List.take(&2, A, t, p), List.drop(&2, A, t, p)), t, base_take_drop(A, t, p))
243
244def length_take(-A: Data, +xs: List<&2, A>, +k: Nat, +h: {Nat.is_le(k, SC.length(A, xs)) == True{} : Bool}) -> {SC.length(A, List.take(&2, A, xs, k)) == k : Nat}:
245  match xs k:
246    case Nil{} 0n:
247      {==}
248    case Nil{} 1n+p:
249      Empty.absurd({0n == 1n+p : Nat}, L.false_true(h))
250    case Con{x, t} 0n:
251      {==}
252    case Con{x, +t} 1n+p:
253      N.succ_cong(SC.length(A, List.take(&2, A, t, p)), p, length_take(A, t, p, h))
254
255def length_drop(-A: Data, +xs: List<&2, A>, +k: Nat) -> {SC.length(A, List.drop(&2, A, xs, k)) == Nat.sub(SC.length(A, xs), k) : Nat}:
256  match xs k:
257    case Nil{} 0n:
258      {==}
259    case Nil{} 1n+p:
260      {==}
261    case Con{x, t} 0n:
262      {==}
263    case Con{x, +t} 1n+p:
264      length_drop(A, t, p)
265
266# ---- last / init ----
267
268def last_snoc(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.last(A, SC.snoc(A, xs, x)) == Some{x} : Maybe<&2, A>}:
269  match xs:
270    case Nil{}:
271      {==}
272    case Con{h, Nil{}}:
273      {==}
274    case Con{h, Con{+h2, +t2}}:
275      last_snoc(A, Con{h2, t2}, x)
276
277def init_snoc(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.init(A, SC.snoc(A, xs, x)) == xs : List<&2, A>}:
278  match xs:
279    case Nil{}:
280      {==}
281    case Con{h, Nil{}}:
282      {==}
283    case Con{+h, Con{+h2, +t2}}:
284      cons_cong(A, h, SC.init(A, SC.snoc(A, Con{h2, t2}, x)), Con{h2, t2}, init_snoc(A, Con{h2, t2}, x))
285
286# ---- take / drop over spec/common (generic) ----
287
288def sc_length_take(-A: Data, +xs: List<&2, A>, +n: Nat, +h: {Nat.is_le(n, SC.length(A, xs)) == True{} : Bool}) -> {SC.length(A, SC.take(A, xs, n)) == n : Nat}:
289  match xs n:
290    case Nil{} 0n:
291      {==}
292    case Nil{} 1n+m:
293      Empty.absurd({SC.length(A, SC.take(A, Nil{}, 1n+m)) == 1n+m : Nat}, L.false_true(h))
294    case Con{a, t} 0n:
295      {==}
296    case Con{a, t} 1n+m:
297      N.succ_cong(SC.length(A, SC.take(A, t, m)), m, sc_length_take(A, t, m, h))
298
299def sc_nth_take(-A: Data, +xs: List<&2, A>, +n: Nat, +i: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {SC.nth(A, SC.take(A, xs, n), i) == SC.nth(A, xs, i) : Maybe<&2, A>}:
300  match xs n i:
301    case Nil{} _ _:
302      {==}
303    case Con{a, t} 0n _:
304      Empty.absurd({SC.nth(A, SC.take(A, Con{a, t}, 0n), i) == SC.nth(A, Con{a, t}, i) : Maybe<&2, A>}, N.lt_zero_absurd(i, h))
305    case Con{a, t} 1n+m 0n:
306      {==}
307    case Con{a, t} 1n+m 1n+j:
308      sc_nth_take(A, t, m, j, h)
309
310def sc_take_take(-A: Data, +xs: List<&2, A>, +n: Nat, +e: Nat, +h: {Nat.is_le(e, n) == True{} : Bool}) -> {SC.take(A, SC.take(A, xs, n), e) == SC.take(A, xs, e) : List<&2, A>}:
311  match xs n e:
312    case Nil{} _ _:
313      {==}
314    case Con{a, t} 0n 0n:
315      {==}
316    case Con{a, t} 1n+m 0n:
317      {==}
318    case Con{a, t} 0n 1n+f:
319      Empty.absurd({SC.take(A, SC.take(A, Con{a, t}, 0n), 1n+f) == SC.take(A, Con{a, t}, 1n+f) : List<&2, A>}, L.false_true(h))
320    case Con{a, t} 1n+m 1n+f:
321      cons_cong(A, a, SC.take(A, SC.take(A, t, m), f), SC.take(A, t, f), sc_take_take(A, t, m, f, h))
322
323def sc_take_zero(-A: Data, +xs: List<&2, A>) -> {SC.take(A, xs, 0n) == Nil{} : List<&2, A>}:
324  match xs:
325    case Nil{}:
326      {==}
327    case Con{a, t}:
328      {==}
329
330def sc_take_append_left(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +h: {Nat.is_le(i, SC.length(A, xs)) == True{} : Bool}) -> {SC.take(A, SC.append(A, xs, ys), i) == SC.take(A, xs, i) : List<&2, A>}:
331  match xs i:
332    case Nil{} 0n:
333      sc_take_zero(A, ys)
334    case Nil{} 1n+j:
335      Empty.absurd({SC.take(A, ys, 1n+j) == Nil{} : List<&2, A>}, L.false_true(h))
336    case Con{a, t} 0n:
337      {==}
338    case Con{a, t} 1n+j:
339      cons_cong(A, a, SC.take(A, SC.append(A, t, ys), j), SC.take(A, t, j), sc_take_append_left(A, t, ys, j, h))
340
341def sc_take_append_right(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +h: {Nat.is_le(SC.length(A, xs), i) == True{} : Bool}) -> {SC.take(A, SC.append(A, xs, ys), i) == SC.append(A, xs, SC.take(A, ys, Nat.sub(i, SC.length(A, xs)))) : List<&2, A>}:
342  match xs i:
343    case Nil{} 0n:
344      {==}
345    case Nil{} 1n+j:
346      {==}
347    case Con{a, t} 0n:
348      Empty.absurd({SC.take(A, SC.append(A, Con{a, t}, ys), 0n) == SC.append(A, Con{a, t}, SC.take(A, ys, Nat.sub(0n, 1n+SC.length(A, t)))) : List<&2, A>}, L.false_true(h))
349    case Con{a, t} 1n+j:
350      cons_cong(A, a, SC.take(A, SC.append(A, t, ys), j), SC.append(A, t, SC.take(A, ys, Nat.sub(j, SC.length(A, t)))), sc_take_append_right(A, t, ys, j, h))
351
352# take r == take l ++ (next r - l after l), for l <= r
353def sub_zero_eq(+r: Nat) -> {Nat.sub(r, 0n) == r : Nat}:
354  N.sub_zero(r)
355
356def sc_take_split(-A: Data, +xs: List<&2, A>, +l: Nat, +r: Nat, +h: {Nat.is_le(l, r) == True{} : Bool}) -> {SC.take(A, xs, r) == SC.append(A, SC.take(A, xs, l), SC.take(A, SC.drop(A, xs, l), Nat.sub(r, l))) : List<&2, A>}:
357  match xs l r:
358    case Nil{} _ _:
359      {==}
360    case Con{a, t} 0n r:
361      %Equal.sym(Nat, Nat.sub(r, 0n), r, sub_zero_eq(r)) : {SC.take(A, Con{a, t}, r) == SC.take(A, Con{a, t}, _) : List<&2, A>}
362      {==}
363    case Con{a, t} 1n+k 0n:
364      Empty.absurd({SC.take(A, Con{a, t}, 0n) == SC.append(A, SC.take(A, Con{a, t}, 1n+k), SC.take(A, SC.drop(A, Con{a, t}, 1n+k), Nat.sub(0n, 1n+k))) : List<&2, A>}, L.false_true(h))
365    case Con{a, t} 1n+k 1n+s:
366      cons_cong(A, a, SC.take(A, t, s), SC.append(A, SC.take(A, t, k), SC.take(A, SC.drop(A, t, k), Nat.sub(s, k))), sc_take_split(A, t, k, s, h))
367
368# drop l (take n xs) == take (n - l) (drop l xs)
369def sc_drop_take(-A: Data, +xs: List<&2, A>, +n: Nat, +l: Nat) -> {SC.drop(A, SC.take(A, xs, n), l) == SC.take(A, SC.drop(A, xs, l), Nat.sub(n, l)) : List<&2, A>}:
370  match xs n l:
371    case Nil{} _ _:
372      {==}
373    case Con{a, t} 0n 0n:
374      {==}
375    case Con{a, t} 0n 1n+k:
376      Equal.sym(List<&2, A>, SC.take(A, SC.drop(A, t, k), 0n), Nil{}, sc_take_zero(A, SC.drop(A, t, k)))
377    case Con{a, t} 1n+m 0n:
378      {==}
379    case Con{a, t} 1n+m 1n+k:
380      sc_drop_take(A, t, m, k)
381
382def sc_take_update(-A: Data, +xs: List<&2, A>, +i: Nat, +v: A, +n: Nat) -> {SC.take(A, SC.update(A, xs, i, v), n) == SC.update(A, SC.take(A, xs, n), i, v) : List<&2, A>}:
383  match xs i n:
384    case Nil{} _ _:
385      {==}
386    case Con{a, t} 0n 0n:
387      {==}
388    case Con{a, t} 1n+j 0n:
389      {==}
390    case Con{a, t} 0n 1n+m:
391      {==}
392    case Con{a, t} 1n+j 1n+m:
393      cons_cong(A, a, SC.take(A, SC.update(A, t, j, v), m), SC.update(A, SC.take(A, t, m), j, v), sc_take_update(A, t, j, v, m))
394
395def sc_take_rep(-A: Data, +m: Nat, +x: A, +n: Nat, +h: {Nat.is_le(n, m) == True{} : Bool}) -> {SC.take(A, SC.replicate(A, m, x), n) == SC.replicate(A, n, x) : List<&2, A>}:
396  match m n:
397    case 0n 0n:
398      {==}
399    case 0n 1n+k:
400      Empty.absurd({SC.take(A, Nil{}, 1n+k) == SC.replicate(A, 1n+k, x) : List<&2, A>}, L.false_true(h))
401    case 1n+j 0n:
402      {==}
403    case 1n+j 1n+k:
404      cons_cong(A, x, SC.take(A, SC.replicate(A, j, x), k), SC.replicate(A, k, x), sc_take_rep(A, j, x, k, h))
405
406# nth below the length is not None
407def sc_nth_some(-A: Data, +xs: List<&2, A>, +i: Nat, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}, +e: {SC.nth(A, xs, i) == None{} : Maybe<&2, A>}) -> Empty:
408  match xs i:
409    case Nil{} _:
410      N.lt_zero_absurd(i, h)
411    case Con{a, t} 0n:
412      L.none_some(A, a, Equal.sym(Maybe<&2, A>, Some{a}, None{}, e))
413    case Con{a, t} 1n+j:
414      sc_nth_some(A, t, j, h, e)