proof/JSON_ListProof.bend
qasim-bend-kit@0.1.0.1 · 79 lines · 0 definitions
1import Base
2
3def append_nil(-A: Data, +xs: List<&2, A>) -> {List.append(&2, A, xs, Nil{}) == xs : List<&2, A>}:
4 match xs:
5 case Nil{}: {==}
6 case h <> t:
7 Equal.cong(List<&2, A>, List<&2, A>, ys => h <> ys, List.append(&2, A, t, Nil{}), t, append_nil(A, t))
8
9def append_assoc(-A: Data,
10 +xs: List<&2, A>,
11 +ys: List<&2, A>,
12 +zs: List<&2, A>) -> {List.append(&2, A, List.append(&2, A, xs, ys), zs) == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}:
13 match xs:
14 case Nil{}: {==}
15 case h <> t:
16 Equal.cong(List<&2, A>, List<&2, A>, q => h <> q,
17 List.append(&2, A, List.append(&2, A, t, ys), zs), List.append(&2, A, t, List.append(&2, A, ys, zs)), append_assoc(A, t, ys, zs))
18
19def reverse_shift(-A: Data,
20 +xs: List<&2, A>,
21 +acc: List<&2, A>,
22 +tail: List<&2, A>) -> {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, acc), tail) == List.reverse.go(&2, A, acc, List.append(&2, A, xs, tail)) : List<&2, A>}:
23 match xs:
24 case Nil{}: {==}
25 case h <> t: reverse_shift(A, t, h <> acc, tail)
26
27def reverse_go_append(-A: Data,
28 +xs: List<&2, A>,
29 +acc: List<&2, A>,
30 +tail: List<&2, A>) -> {List.reverse.go(&2, A, xs, List.append(&2, A, acc, tail)) == List.append(&2, A, List.reverse.go(&2, A, xs, acc), tail) : List<&2, A>}:
31 match xs:
32 case Nil{}: {==}
33 case h <> t:
34 reverse_go_append(A, t, h <> acc, tail)
35
36def reverse_cons(-A: Data,
37 +head: A,
38 +tail: List<&2, A>) -> {List.reverse(&2, A, head <> tail) == List.append(&2, A, List.reverse(&2, A, tail), head <> Nil{}) : List<&2, A>}:
39 reverse_go_append(A, tail, Nil{}, head <> Nil{})
40
41def reverse_append(-A: Data,
42 +xs: List<&2, A>,
43 +ys: List<&2, A>) -> {List.reverse(&2, A, List.append(&2, A, xs, ys)) == List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, xs)) : List<&2, A>}:
44 match xs:
45 case Nil{}:
46 Equal.sym(List<&2, A>, List.append(&2, A, List.reverse(&2, A, ys), Nil{}),
47 List.reverse(&2, A, ys),
48 append_nil(A, List.reverse(&2, A, ys)))
49 case h <> t:
50 Equal.trans(List<&2, A>,
51 List.reverse(&2, A, List.append(&2, A, h <> t, ys)),
52 List.append(&2, A, List.reverse(&2, A, List.append(&2, A, t, ys)), h <> Nil{}),
53 List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
54 reverse_go_append(A, List.append(&2, A, t, ys), Nil{}, h <> Nil{}),
55 Equal.trans(List<&2, A>,
56 List.append(&2, A, List.reverse(&2, A, List.append(&2, A, t, ys)), h <> Nil{}),
57 List.append(&2, A, List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)), h <> Nil{}),
58 List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
59 Equal.cong(List<&2, A>, List<&2, A>, xs => List.append(&2, A, xs, h <> Nil{}),
60 List.reverse(&2, A, List.append(&2, A, t, ys)),
61 List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)),
62 reverse_append(A, t, ys)),
63 Equal.trans(List<&2, A>,
64 List.append(&2, A, List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)), h <> Nil{}),
65 List.append(&2, A, List.reverse(&2, A, ys), List.append(&2, A, List.reverse(&2, A, t), h <> Nil{})),
66 List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
67 append_assoc(A, List.reverse(&2, A, ys), List.reverse(&2, A, t), h <> Nil{}),
68 Equal.cong(List<&2, A>, List<&2, A>, xs => List.append(&2, A, List.reverse(&2, A, ys), xs),
69 List.append(&2, A, List.reverse(&2, A, t), h <> Nil{}),
70 List.reverse(&2, A, h <> t),
71 Equal.sym(List<&2, A>,
72 List.reverse(&2, A, h <> t),
73 List.append(&2, A, List.reverse(&2, A, t), h <> Nil{}),
74 reverse_go_append(A, t, Nil{}, h <> Nil{}))))))
75
76def reverse_twice(-A: Data,
77 +xs: List<&2, A>) -> {List.reverse(&2, A, List.reverse(&2, A, xs)) == xs : List<&2, A>}:
78 Equal.trans(List<&2, A>, List.reverse(&2, A, List.reverse(&2, A, xs)), List.append(&2, A, xs, Nil{}), xs,
79 reverse_shift(A, xs, Nil{}, Nil{}), append_nil(A, xs))