proof_base.bend

lawful-arrays@0.1.0.0 · 516 lines · 37 definitions

1import 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.
10def 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
17def Bool.disc_ft(b: Bool) -> Type:
18  match b:
19    case False{}:
20      Unit
21    case True{}:
22      Empty
23
24law false_ne_true:
25  for e: {False{} == True{} : Bool}
26  Empty
27
28def false_ne_true(e):
29  %e : Bool.disc_ft(_)
30  Unit{}
31
32law true_ne_false:
33  for e: {True{} == False{} : Bool}
34  Empty
35
36def true_ne_false(e):
37  false_ne_true(Equal.sym(Bool, True{}, False{}, e))
38
39law 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
45def 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
52law 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
58def 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
68def Nat.disc_z(n: Nat) -> Type:
69  match n:
70    case 0n:
71      Empty
72    case 1n+p:
73      Unit
74
75law succ_ne_zero:
76  for -n: Nat
77  for e: {1n+n == 0n : Nat}
78  Empty
79
80def succ_ne_zero(n, e):
81  %e : Nat.disc_z(_)
82  Unit{}
83
84def pred(n: Nat) -> Nat:
85  match n:
86    case 0n:
87      0n
88    case 1n+p:
89      p
90
91law succ_inj:
92  for -a: Nat
93  for -b: Nat
94  for e: {1n+a == 1n+b : Nat}
95  {a == b : Nat}
96
97def succ_inj(a, b, e):
98  Equal.cong(Nat, Nat, n => pred(n), 1n+a, 1n+b, e)
99
100law add_zero:
101  for +n: Nat
102  {Nat.add(n, 0n) == n : Nat}
103
104def 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
112law add_succ:
113  for +a: Nat
114  for +b: Nat
115  {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}
116
117def 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
125law sub_zero:
126  for +i: Nat
127  {Nat.sub(i, 0n) == i : Nat}
128
129def sub_zero(i):
130  match i:
131    case 0n:
132      {==}
133    case 1n+k:
134      {==}
135
136law lt_zero:
137  for +i: Nat
138  {Nat.is_lt(i, 0n) == False{} : Bool}
139
140def lt_zero(i):
141  match i:
142    case 0n:
143      {==}
144    case 1n+k:
145      {==}
146
147law lt_zero_absurd:
148  for +i: Nat
149  for e: {Nat.is_lt(i, 0n) == True{} : Bool}
150  Empty
151
152def 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.
157law lt_one:
158  for +k: Nat
159  for e: {Nat.is_lt(k, 1n) == True{} : Bool}
160  {k == 0n : Nat}
161
162def 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
169law 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
175def 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.
187law 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
195def 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
205law 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
211def 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
218law pow_pos:
219  for +d: Nat
220  {Nat.is_lt(0n, Nat.pow(2n, d)) == True{} : Bool}
221
222def 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'.
230law pow_succ:
231  for +p: Nat
232  {Nat.pow(2n, 1n+p) == Nat.add(Nat.pow(2n, p), Nat.pow(2n, p)) : Nat}
233
234def 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
239law 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
245def 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
258law 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
263def 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
272law 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
278def 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
296law 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
303def 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.
313law 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
321def 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.
331law 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
340def 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
350law 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
360def 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
371law 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
381def 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
394law 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
402def 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.
412law 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
421def 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
434def 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
441def 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
448law 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
457def 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
460law 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
469def 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...
473law 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
483def 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.
502law 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
510def 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))