1	import Base
2	
3	# Lemmas about Bool, Nat and List that Base lacks, used by the array proofs.
4	# Some are copied from ../framebender/proof_base.bend (same author, MIT).
5	
6	# Equality
7	# ========
8	
9	# Transport along an equation.
10	def subst(-A: Type, -P: A -> Type, -x: A, -y: A, e: {x == y : A}, p: P(x)) -> P(y):
11	  %e : P(_)
12	  p
13	
14	# Bool
15	# ====
16	
17	def Bool.disc_ft(b: Bool) -> Type:
18	  match b:
19	    case False{}:
20	      Unit
21	    case True{}:
22	      Empty
23	
24	law false_ne_true:
25	  for e: {False{} == True{} : Bool}
26	  Empty
27	
28	def false_ne_true(e):
29	  %e : Bool.disc_ft(_)
30	  Unit{}
31	
32	law true_ne_false:
33	  for e: {True{} == False{} : Bool}
34	  Empty
35	
36	def true_ne_false(e):
37	  false_ne_true(Equal.sym(Bool, True{}, False{}, e))
38	
39	law and_true_l:
40	  for +a: Bool
41	  for +b: Bool
42	  for e: {Bool.and(a, b) == True{} : Bool}
43	  {a == True{} : Bool}
44	
45	def and_true_l(a, b, e):
46	  match a:
47	    case True{}:
48	      {==}
49	    case False{}:
50	      Empty.absurd({False{} == True{} : Bool}, false_ne_true(e))
51	
52	law and_true_r:
53	  for +a: Bool
54	  for +b: Bool
55	  for e: {Bool.and(a, b) == True{} : Bool}
56	  {b == True{} : Bool}
57	
58	def and_true_r(a, b, e):
59	  match a:
60	    case True{}:
61	      e
62	    case False{}:
63	      Empty.absurd({b == True{} : Bool}, false_ne_true(e))
64	
65	# Nat
66	# ===
67	
68	def Nat.disc_z(n: Nat) -> Type:
69	  match n:
70	    case 0n:
71	      Empty
72	    case 1n+p:
73	      Unit
74	
75	law succ_ne_zero:
76	  for -n: Nat
77	  for e: {1n+n == 0n : Nat}
78	  Empty
79	
80	def succ_ne_zero(n, e):
81	  %e : Nat.disc_z(_)
82	  Unit{}
83	
84	def pred(n: Nat) -> Nat:
85	  match n:
86	    case 0n:
87	      0n
88	    case 1n+p:
89	      p
90	
91	law succ_inj:
92	  for -a: Nat
93	  for -b: Nat
94	  for e: {1n+a == 1n+b : Nat}
95	  {a == b : Nat}
96	
97	def succ_inj(a, b, e):
98	  Equal.cong(Nat, Nat, n => pred(n), 1n+a, 1n+b, e)
99	
100	law add_zero:
101	  for +n: Nat
102	  {Nat.add(n, 0n) == n : Nat}
103	
104	def add_zero(n):
105	  match n:
106	    case 0n:
107	      {==}
108	    case 1n+p:
109	      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
110	      {==}
111	
112	law add_succ:
113	  for +a: Nat
114	  for +b: Nat
115	  {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}
116	
117	def add_succ(a, b):
118	  match a:
119	    case 0n:
120	      {==}
121	    case 1n+p:
122	      %add_succ(p, b) : {1n+Nat.add(p, 1n+b) == 1n+_ : Nat}
123	      {==}
124	
125	law sub_zero:
126	  for +i: Nat
127	  {Nat.sub(i, 0n) == i : Nat}
128	
129	def sub_zero(i):
130	  match i:
131	    case 0n:
132	      {==}
133	    case 1n+k:
134	      {==}
135	
136	law lt_zero:
137	  for +i: Nat
138	  {Nat.is_lt(i, 0n) == False{} : Bool}
139	
140	def lt_zero(i):
141	  match i:
142	    case 0n:
143	      {==}
144	    case 1n+k:
145	      {==}
146	
147	law lt_zero_absurd:
148	  for +i: Nat
149	  for e: {Nat.is_lt(i, 0n) == True{} : Bool}
150	  Empty
151	
152	def lt_zero_absurd(i, e):
153	  false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(i, 0n), True{},
154	    Equal.sym(Bool, Nat.is_lt(i, 0n), False{}, lt_zero(i)), e))
155	
156	# Below 1 is 0.
157	law lt_one:
158	  for +k: Nat
159	  for e: {Nat.is_lt(k, 1n) == True{} : Bool}
160	  {k == 0n : Nat}
161	
162	def lt_one(k, e):
163	  match k:
164	    case 0n:
165	      {==}
166	    case 1n+j:
167	      Empty.absurd({1n+j == 0n : Nat}, lt_zero_absurd(j, e))
168	
169	law not_lt_le:
170	  for +a: Nat
171	  for +b: Nat
172	  for e: {Nat.is_lt(a, b) == False{} : Bool}
173	  {Nat.is_le(b, a) == True{} : Bool}
174	
175	def not_lt_le(a, b, e):
176	  match a b:
177	    case 0n 0n:
178	      {==}
179	    case 0n 1n+q:
180	      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, true_ne_false(e))
181	    case 1n+p 0n:
182	      {==}
183	    case 1n+p 1n+q:
184	      not_lt_le(p, q, e)
185	
186	# k is at least m and below m + m2, so k - m is below m2.
187	law lt_sub:
188	  for +m: Nat
189	  for +k: Nat
190	  for +m2: Nat
191	  for h1: {Nat.is_lt(k, m) == False{} : Bool}
192	  for h2: {Nat.is_lt(k, Nat.add(m, m2)) == True{} : Bool}
193	  {Nat.is_lt(Nat.sub(k, m), m2) == True{} : Bool}
194	
195	def lt_sub(m, k, m2, h1, h2):
196	  match m k:
197	    case 0n _:
198	      %Equal.sym(Nat, Nat.sub(k, 0n), k, sub_zero(k)) : {Nat.is_lt(_, m2) == True{} : Bool}
199	      h2
200	    case 1n+q 0n:
201	      Empty.absurd({Nat.is_lt(Nat.sub(0n, 1n+q), m2) == True{} : Bool}, true_ne_false(h1))
202	    case 1n+q 1n+j:
203	      lt_sub(q, j, m2, h1, h2)
204	
205	law lt0_add:
206	  for +a: Nat
207	  for +b: Nat
208	  for e: {Nat.is_lt(0n, a) == True{} : Bool}
209	  {Nat.is_lt(0n, Nat.add(a, b)) == True{} : Bool}
210	
211	def lt0_add(a, b, e):
212	  match a:
213	    case 0n:
214	      Empty.absurd({Nat.is_lt(0n, b) == True{} : Bool}, false_ne_true(e))
215	    case 1n+p:
216	      {==}
217	
218	law pow_pos:
219	  for +d: Nat
220	  {Nat.is_lt(0n, Nat.pow(2n, d)) == True{} : Bool}
221	
222	def pow_pos(d):
223	  match d:
224	    case 0n:
225	      {==}
226	    case 1n+p:
227	      lt0_add(Nat.pow(2n, p), Nat.add(Nat.pow(2n, p), 0n), pow_pos(p))
228	
229	# 2^(1+p) unfolds to p' + (p' + 0); this is p' + p'.
230	law pow_succ:
231	  for +p: Nat
232	  {Nat.pow(2n, 1n+p) == Nat.add(Nat.pow(2n, p), Nat.pow(2n, p)) : Nat}
233	
234	def pow_succ(p):
235	  %add_zero(Nat.pow(2n, p)) :
236	    {Nat.pow(2n, 1n+p) == Nat.add(Nat.pow(2n, p), _) : Nat}
237	  {==}
238	
239	law lt_dbl:
240	  for +a: Nat
241	  for +b: Nat
242	  for e: {Nat.is_lt(a, b) == True{} : Bool}
243	  {Nat.is_lt(Nat.add(a, a), Nat.add(b, b)) == True{} : Bool}
244	
245	def lt_dbl(a, b, e):
246	  match a b:
247	    case _ 0n:
248	      Empty.absurd({Nat.is_lt(Nat.add(a, a), 0n) == True{} : Bool}, lt_zero_absurd(a, e))
249	    case 0n 1n+q:
250	      {==}
251	    case 1n+p 1n+q:
252	      %Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), add_succ(p, p)) :
253	        {Nat.is_lt(_, Nat.add(q, 1n+q)) == True{} : Bool}
254	      %Equal.sym(Nat, Nat.add(q, 1n+q), 1n+Nat.add(q, q), add_succ(q, q)) :
255	        {Nat.is_lt(1n+Nat.add(p, p), _) == True{} : Bool}
256	      lt_dbl(p, q, e)
257	
258	law lt_one_dbl:
259	  for +b: Nat
260	  for e: {Nat.is_lt(0n, b) == True{} : Bool}
261	  {Nat.is_lt(1n, Nat.add(b, b)) == True{} : Bool}
262	
263	def lt_one_dbl(b, e):
264	  match b:
265	    case 0n:
266	      Empty.absurd({Nat.is_lt(1n, 0n) == True{} : Bool}, false_ne_true(e))
267	    case 1n+q:
268	      %Equal.sym(Nat, Nat.add(q, 1n+q), 1n+Nat.add(q, q), add_succ(q, q)) :
269	        {Nat.is_lt(1n, 1n+_) == True{} : Bool}
270	      {==}
271	
272	law pow_lt:
273	  for +d: Nat
274	  for +e: Nat
275	  for h: {Nat.is_lt(d, e) == True{} : Bool}
276	  {Nat.is_lt(Nat.pow(2n, d), Nat.pow(2n, e)) == True{} : Bool}
277	
278	def pow_lt(d, e, h):
279	  match d e:
280	    case _ 0n:
281	      Empty.absurd({Nat.is_lt(Nat.pow(2n, d), 1n) == True{} : Bool}, lt_zero_absurd(d, h))
282	    case 0n 1n+q:
283	      %Equal.sym(Nat, Nat.pow(2n, 1n+q), Nat.add(Nat.pow(2n, q), Nat.pow(2n, q)), pow_succ(q)) :
284	        {Nat.is_lt(1n, _) == True{} : Bool}
285	      lt_one_dbl(Nat.pow(2n, q), pow_pos(q))
286	    case 1n+p 1n+q:
287	      %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.add(Nat.pow(2n, p), Nat.pow(2n, p)), pow_succ(p)) :
288	        {Nat.is_lt(_, Nat.pow(2n, 1n+q)) == True{} : Bool}
289	      %Equal.sym(Nat, Nat.pow(2n, 1n+q), Nat.add(Nat.pow(2n, q), Nat.pow(2n, q)), pow_succ(q)) :
290	        {Nat.is_lt(Nat.add(Nat.pow(2n, p), Nat.pow(2n, p)), _) == True{} : Bool}
291	      lt_dbl(Nat.pow(2n, p), Nat.pow(2n, q), pow_lt(p, q, h))
292	
293	# List
294	# ====
295	
296	law length_append:
297	  for -A: Data
298	  for +xs: List<&2, A>
299	  for +ys: List<&2, A>
300	  {List.length(&2, A, List.append(&2, A, xs, ys))
301	    == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}
302	
303	def length_append(A, xs, ys):
304	  match xs:
305	    case Nil{}:
306	      {==}
307	    case h <> t:
308	      %length_append(A, t, ys) :
309	        {1n+List.length(&2, A, List.append(&2, A, t, ys)) == 1n+_ : Nat}
310	      {==}
311	
312	# Before index length(xs), xs ++ ys reads like xs.
313	law get_append_l:
314	  for -A: Data
315	  for +xs: List<&2, A>
316	  for +ys: List<&2, A>
317	  for +i: Nat
318	  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool}
319	  {List.get(&2, A, List.append(&2, A, xs, ys), i) == List.get(&2, A, xs, i) : Maybe<&2, A>}
320	
321	def get_append_l(A, xs, ys, i, e):
322	  match xs i:
323	    case Nil{} _:
324	      Empty.absurd({List.get(&2, A, ys, i) == None{} : Maybe<&2, A>}, lt_zero_absurd(i, e))
325	    case h <> t 0n:
326	      {==}
327	    case h <> t 1n+k:
328	      get_append_l(A, t, ys, k, e)
329	
330	# From index length(xs) on, xs ++ ys reads like ys.
331	law get_append_r:
332	  for -A: Data
333	  for +xs: List<&2, A>
334	  for +ys: List<&2, A>
335	  for +i: Nat
336	  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == False{} : Bool}
337	  {List.get(&2, A, List.append(&2, A, xs, ys), i)
338	    == List.get(&2, A, ys, Nat.sub(i, List.length(&2, A, xs))) : Maybe<&2, A>}
339	
340	def get_append_r(A, xs, ys, i, e):
341	  match xs i:
342	    case Nil{} _:
343	      %Equal.sym(Nat, Nat.sub(i, 0n), i, sub_zero(i)) : {List.get(&2, A, ys, i) == List.get(&2, A, ys, _) : Maybe<&2, A>}
344	      {==}
345	    case h <> t 0n:
346	      Empty.absurd({Some{h} == List.get(&2, A, ys, 0n) : Maybe<&2, A>}, true_ne_false(e))
347	    case h <> t 1n+k:
348	      get_append_r(A, t, ys, k, e)
349	
350	law set_append_l:
351	  for -A: Data
352	  for +xs: List<&2, A>
353	  for +ys: List<&2, A>
354	  for +i: Nat
355	  for +v: A
356	  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool}
357	  {List.set(&2, A, List.append(&2, A, xs, ys), i, v)
358	    == List.append(&2, A, List.set(&2, A, xs, i, v), ys) : List<&2, A>}
359	
360	def set_append_l(A, xs, ys, i, v, e):
361	  match xs i:
362	    case Nil{} _:
363	      Empty.absurd({List.set(&2, A, ys, i, v) == ys : List<&2, A>}, lt_zero_absurd(i, e))
364	    case h <> t 0n:
365	      {==}
366	    case h <> t 1n+k:
367	      %set_append_l(A, t, ys, k, v, e) :
368	        {h <> List.set(&2, A, List.append(&2, A, t, ys), k, v) == h <> _ : List<&2, A>}
369	      {==}
370	
371	law set_append_r:
372	  for -A: Data
373	  for +xs: List<&2, A>
374	  for +ys: List<&2, A>
375	  for +i: Nat
376	  for +v: A
377	  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == False{} : Bool}
378	  {List.set(&2, A, List.append(&2, A, xs, ys), i, v)
379	    == List.append(&2, A, xs, List.set(&2, A, ys, Nat.sub(i, List.length(&2, A, xs)), v)) : List<&2, A>}
380	
381	def set_append_r(A, xs, ys, i, v, e):
382	  match xs i:
383	    case Nil{} _:
384	      %Equal.sym(Nat, Nat.sub(i, 0n), i, sub_zero(i)) : {List.set(&2, A, ys, i, v) == List.set(&2, A, ys, _, v) : List<&2, A>}
385	      {==}
386	    case h <> t 0n:
387	      Empty.absurd({v <> List.append(&2, A, t, ys)
388	        == h <> List.append(&2, A, t, List.set(&2, A, ys, 0n, v)) : List<&2, A>}, true_ne_false(e))
389	    case h <> t 1n+k:
390	      %set_append_r(A, t, ys, k, v, e) :
391	        {h <> List.set(&2, A, List.append(&2, A, t, ys), k, v) == h <> _ : List<&2, A>}
392	      {==}
393	
394	law replicate_add:
395	  for -A: Data
396	  for +m: Nat
397	  for +n: Nat
398	  for +v: A
399	  {List.replicate(A, Nat.add(m, n), v)
400	    == List.append(&2, A, List.replicate(A, m, v), List.replicate(A, n, v)) : List<&2, A>}
401	
402	def replicate_add(A, m, n, v):
403	  match m:
404	    case 0n:
405	      {==}
406	    case 1n+p:
407	      %replicate_add(A, p, n, v) :
408	        {v <> List.replicate(A, Nat.add(p, n), v) == v <> _ : List<&2, A>}
409	      {==}
410	
411	# Writing index i does not change index j != i.
412	law get_set_ne:
413	  for -A: Data
414	  for +xs: List<&2, A>
415	  for +i: Nat
416	  for +j: Nat
417	  for +v: A
418	  for e: {Nat.is_eq(i, j) == False{} : Bool}
419	  {List.get(&2, A, List.set(&2, A, xs, i, v), j) == List.get(&2, A, xs, j) : Maybe<&2, A>}
420	
421	def get_set_ne(A, xs, i, j, v, e):
422	  match xs i j:
423	    case Nil{} _ _:
424	      {==}
425	    case h <> t 0n 0n:
426	      Empty.absurd({Some{v} == Some{h} : Maybe<&2, A>}, true_ne_false(e))
427	    case h <> t 0n 1n+q:
428	      {==}
429	    case h <> t 1n+p 0n:
430	      {==}
431	    case h <> t 1n+p 1n+q:
432	      get_set_ne(A, t, p, q, v, e)
433	
434	def head_or(-A: Data, +d: A, xs: List<&2, A>) -> A:
435	  match xs:
436	    case Nil{}:
437	      d
438	    case h <> t:
439	      h
440	
441	def tail(-A: Data, xs: List<&2, A>) -> List<&2, A>:
442	  match xs:
443	    case Nil{}:
444	      Nil{}
445	    case h <> t:
446	      t
447	
448	law cons_inj_h:
449	  for -A: Data
450	  for -x: A
451	  for -y: A
452	  for -xs: List<&2, A>
453	  for -ys: List<&2, A>
454	  for e: {x <> xs == y <> ys : List<&2, A>}
455	  {x == y : A}
456	
457	def cons_inj_h(A, x, y, xs, ys, e):
458	  Equal.cong(List<&2, A>, A, l => head_or(A, x, l), x <> xs, y <> ys, e)
459	
460	law cons_inj_t:
461	  for -A: Data
462	  for -x: A
463	  for -y: A
464	  for -xs: List<&2, A>
465	  for -ys: List<&2, A>
466	  for e: {x <> xs == y <> ys : List<&2, A>}
467	  {xs == ys : List<&2, A>}
468	
469	def cons_inj_t(A, x, y, xs, ys, e):
470	  Equal.cong(List<&2, A>, List<&2, A>, l => tail(A, l), x <> xs, y <> ys, e)
471	
472	# Two appends with equally long first parts: the first parts are equal...
473	law append_inj_l:
474	  for -A: Data
475	  for +x1: List<&2, A>
476	  for +x2: List<&2, A>
477	  for -y1: List<&2, A>
478	  for -y2: List<&2, A>
479	  for hl: {List.length(&2, A, x1) == List.length(&2, A, x2) : Nat}
480	  for +e: {List.append(&2, A, x1, y1) == List.append(&2, A, x2, y2) : List<&2, A>}
481	  {x1 == x2 : List<&2, A>}
482	
483	def append_inj_l(A, x1, x2, y1, y2, hl, e):
484	  match x1 x2:
485	    case Nil{} Nil{}:
486	      {==}
487	    case Nil{} h2 <> t2:
488	      Empty.absurd({Nil{} == h2 <> t2 : List<&2, A>},
489	        succ_ne_zero(List.length(&2, A, t2), Equal.sym(Nat, 0n, 1n+List.length(&2, A, t2), hl)))
490	    case h1 <> t1 Nil{}:
491	      Empty.absurd({h1 <> t1 == Nil{} : List<&2, A>}, succ_ne_zero(List.length(&2, A, t1), hl))
492	    case h1 <> t1 h2 <> t2:
493	      %cons_inj_h(A, h1, h2, List.append(&2, A, t1, y1), List.append(&2, A, t2, y2), e) :
494	        {h1 <> t1 == _ <> t2 : List<&2, A>}
495	      %append_inj_l(A, t1, t2, y1, y2,
496	        succ_inj(List.length(&2, A, t1), List.length(&2, A, t2), hl),
497	        cons_inj_t(A, h1, h2, List.append(&2, A, t1, y1), List.append(&2, A, t2, y2), e)) :
498	        {h1 <> t1 == h1 <> _ : List<&2, A>}
499	      {==}
500	
501	# ...and so are the second parts.
502	law append_cancel_l:
503	  for -A: Data
504	  for +xs: List<&2, A>
505	  for -y1: List<&2, A>
506	  for -y2: List<&2, A>
507	  for e: {List.append(&2, A, xs, y1) == List.append(&2, A, xs, y2) : List<&2, A>}
508	  {y1 == y2 : List<&2, A>}
509	
510	def append_cancel_l(A, xs, y1, y2, e):
511	  match xs:
512	    case Nil{}:
513	      e
514	    case h <> t:
515	      append_cancel_l(A, t, y1, y2,
516	        cons_inj_t(A, h, h, List.append(&2, A, t, y1), List.append(&2, A, t, y2), e))