proofs/lib/nat_list.bend
bend-collections-laws-containers@1.0.0.0 · 271 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
6
7# Lists of Nat (ids, slots): membership, duplicate-freedom and how both
8# split over appends; the last of a list; splitting a list at a member; the
9# reversed append. Shared by every structure that threads ids through arrays.
10
11# stated in spec/lib/common.bend
12def memn(+s: Nat, xs: List<&2, Nat>) -> Bool:
13 SC.memn(s, xs)
14
15def nodupn(xs: List<&2, Nat>) -> Bool:
16 match xs:
17 case Nil{}:
18 True{}
19 case Con{+x, +t}:
20 Bool.and(Bool.not(memn(x, t)), nodupn(t))
21
22def or_assoc(+a: Bool, +b: Bool, +c: Bool) -> {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}:
23 match a:
24 case True{}:
25 {==}
26 case False{}:
27 {==}
28
29def or_comm(+a: Bool, +b: Bool) -> {Bool.or(a, b) == Bool.or(b, a) : Bool}:
30 match a b:
31 case True{} True{}:
32 {==}
33 case True{} False{}:
34 {==}
35 case False{} True{}:
36 {==}
37 case False{} False{}:
38 {==}
39
40def and_assoc(+a: Bool, +b: Bool, +c: Bool) -> {Bool.and(a, Bool.and(b, c)) == Bool.and(Bool.and(a, b), c) : Bool}:
41 match a:
42 case True{}:
43 {==}
44 case False{}:
45 {==}
46
47def and_comm(+a: Bool, +b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}:
48 match a b:
49 case True{} True{}:
50 {==}
51 case True{} False{}:
52 {==}
53 case False{} True{}:
54 {==}
55 case False{} False{}:
56 {==}
57
58def bt_mid(+x: Bool, +y: Bool, +z: Bool, +w: Bool) -> {Bool.and(Bool.not(Bool.or(x, y)), Bool.and(z, Bool.not(w))) == Bool.and(Bool.and(Bool.not(x), z), Bool.not(Bool.or(y, w))) : Bool}:
59 match x y z w:
60 case True{} y2 z2 w2:
61 {==}
62 case False{} True{} z2 w2:
63 +e = and_comm(z2, False{})
64 Equal.trans(Bool, Bool.and(False{}, Bool.and(z2, Bool.not(w2))), False{}, Bool.and(z2, False{}), {==}, Equal.sym(Bool, Bool.and(z2, False{}), False{}, Equal.trans(Bool, Bool.and(z2, False{}), Bool.and(False{}, z2), False{}, e, {==})))
65 case False{} False{} True{} w2:
66 {==}
67 case False{} False{} False{} w2:
68 {==}
69
70def is_eq_sym(+a: Nat, +b: Nat) -> {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}:
71 match a b:
72 case 0n 0n:
73 {==}
74 case 0n 1n+q:
75 {==}
76 case 1n+p 0n:
77 {==}
78 case 1n+p 1n+q:
79 is_eq_sym(p, q)
80
81def memn_app(+x: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>) -> {memn(x, SC.append(Nat, a, b)) == Bool.or(memn(x, a), memn(x, b)) : Bool}:
82 match a:
83 case Nil{}:
84 {==}
85 case Con{+h, +t}:
86 Equal.trans(Bool, Bool.or(Nat.is_eq(h, x), memn(x, SC.append(Nat, t, b))), Bool.or(Nat.is_eq(h, x), Bool.or(memn(x, t), memn(x, b))), Bool.or(Bool.or(Nat.is_eq(h, x), memn(x, t)), memn(x, b)), Equal.cong(Bool, Bool, z => Bool.or(Nat.is_eq(h, x), z), memn(x, SC.append(Nat, t, b)), Bool.or(memn(x, t), memn(x, b)), memn_app(x, t, b)), or_assoc(Nat.is_eq(h, x), memn(x, t), memn(x, b)))
87
88def memn_mid(+x: Nat, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>) -> {memn(x, SC.append(Nat, a, Con{s, b})) == Bool.or(memn(x, SC.append(Nat, a, b)), Nat.is_eq(s, x)) : Bool}:
89 match a:
90 case Nil{}:
91 or_comm(Nat.is_eq(s, x), memn(x, b))
92 case Con{+h, +t}:
93 Equal.trans(Bool, Bool.or(Nat.is_eq(h, x), memn(x, SC.append(Nat, t, Con{s, b}))), Bool.or(Nat.is_eq(h, x), Bool.or(memn(x, SC.append(Nat, t, b)), Nat.is_eq(s, x))), Bool.or(Bool.or(Nat.is_eq(h, x), memn(x, SC.append(Nat, t, b))), Nat.is_eq(s, x)), Equal.cong(Bool, Bool, z => Bool.or(Nat.is_eq(h, x), z), memn(x, SC.append(Nat, t, Con{s, b})), Bool.or(memn(x, SC.append(Nat, t, b)), Nat.is_eq(s, x)), memn_mid(x, t, s, b)), or_assoc(Nat.is_eq(h, x), memn(x, SC.append(Nat, t, b)), Nat.is_eq(s, x)))
94
95def nd_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>) -> {nodupn(SC.append(Nat, a, Con{s, b})) == Bool.and(nodupn(SC.append(Nat, a, b)), Bool.not(memn(s, SC.append(Nat, a, b)))) : Bool}:
96 match a:
97 case Nil{}:
98 and_comm(Bool.not(memn(s, b)), nodupn(b))
99 case Con{+h, +t}:
100 +X = memn(h, SC.append(Nat, t, b))
101 +Z = nodupn(SC.append(Nat, t, b))
102 +Wm = memn(s, SC.append(Nat, t, b))
103 +e1 = Equal.cong(Bool, Bool, z => Bool.and(Bool.not(z), nodupn(SC.append(Nat, t, Con{s, b}))), memn(h, SC.append(Nat, t, Con{s, b})), Bool.or(X, Nat.is_eq(s, h)), memn_mid(h, t, s, b))
104 +e2 = Equal.cong(Bool, Bool, z => Bool.and(Bool.not(Bool.or(X, Nat.is_eq(s, h))), z), nodupn(SC.append(Nat, t, Con{s, b})), Bool.and(Z, Bool.not(Wm)), nd_mid(t, s, b))
105 +e3 = bt_mid(X, Nat.is_eq(s, h), Z, Wm)
106 +e4 = Equal.cong(Bool, Bool, z => Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(z, Wm))), Nat.is_eq(s, h), Nat.is_eq(h, s), is_eq_sym(s, h))
107 Equal.trans(Bool, nodupn(SC.append(Nat, Con{h, t}, Con{s, b})), Bool.and(Bool.not(Bool.or(X, Nat.is_eq(s, h))), nodupn(SC.append(Nat, t, Con{s, b}))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(Nat.is_eq(h, s), Wm))), e1, Equal.trans(Bool, Bool.and(Bool.not(Bool.or(X, Nat.is_eq(s, h))), nodupn(SC.append(Nat, t, Con{s, b}))), Bool.and(Bool.not(Bool.or(X, Nat.is_eq(s, h))), Bool.and(Z, Bool.not(Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(Nat.is_eq(h, s), Wm))), e2, Equal.trans(Bool, Bool.and(Bool.not(Bool.or(X, Nat.is_eq(s, h))), Bool.and(Z, Bool.not(Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(Nat.is_eq(s, h), Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(Nat.is_eq(h, s), Wm))), e3, e4)))
108
109def not_t_f(+b: Bool, +h: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:
110 L.not_true(b, h)
111
112def or_f_l(+a: Bool, +b: Bool, +h: {Bool.or(a, b) == False{} : Bool}) -> {a == False{} : Bool}:
113 match a:
114 case True{}:
115 Empty.absurd({True{} == False{} : Bool}, L.true_false(h))
116 case False{}:
117 {==}
118
119def nd_r(+a: List<&2, Nat>, +x: List<&2, Nat>, +h: {nodupn(SC.append(Nat, a, x)) == True{} : Bool}) -> {nodupn(x) == True{} : Bool}:
120 match a:
121 case Nil{}:
122 h
123 case Con{+h0, +t}:
124 nd_r(t, x, L.and_right(Bool.not(memn(h0, SC.append(Nat, t, x))), nodupn(SC.append(Nat, t, x)), h))
125
126def nd_l(+a: List<&2, Nat>, +x: List<&2, Nat>, +h: {nodupn(SC.append(Nat, a, x)) == True{} : Bool}) -> {nodupn(a) == True{} : Bool}:
127 match a:
128 case Nil{}:
129 {==}
130 case Con{+h0, +t}:
131 +hm = not_t_f(memn(h0, SC.append(Nat, t, x)), L.and_left(Bool.not(memn(h0, SC.append(Nat, t, x))), nodupn(SC.append(Nat, t, x)), h))
132 +hm2 = or_f_l(memn(h0, t), memn(h0, x), L.subst(Bool, z => {z == False{} : Bool}, memn(h0, SC.append(Nat, t, x)), Bool.or(memn(h0, t), memn(h0, x)), memn_app(h0, t, x), hm))
133 L.and_intro(Bool.not(memn(h0, t)), nodupn(t), L.subst(Bool, z => {Bool.not(z) == True{} : Bool}, False{}, memn(h0, t), Equal.sym(Bool, memn(h0, t), False{}, hm2), {==}), nd_l(t, x, L.and_right(Bool.not(memn(h0, SC.append(Nat, t, x))), nodupn(SC.append(Nat, t, x)), h)))
134
135def or_true_b(+b: Bool) -> {Bool.or(b, True{}) == True{} : Bool}:
136 match b:
137 case True{}:
138 {==}
139 case False{}:
140 {==}
141
142def mem_app_r(+y: Nat, +a: List<&2, Nat>, +x: List<&2, Nat>, +h: {memn(y, x) == True{} : Bool}) -> {memn(y, SC.append(Nat, a, x)) == True{} : Bool}:
143 L.subst(Bool, z => {z == True{} : Bool}, Bool.or(memn(y, a), memn(y, x)), memn(y, SC.append(Nat, a, x)), Equal.sym(Bool, memn(y, SC.append(Nat, a, x)), Bool.or(memn(y, a), memn(y, x)), memn_app(y, a, x)), L.subst(Bool, z => {Bool.or(memn(y, a), z) == True{} : Bool}, True{}, memn(y, x), Equal.sym(Bool, memn(y, x), True{}, h), or_true_b(memn(y, a))))
144
145def mem_app_l(+y: Nat, +a: List<&2, Nat>, +x: List<&2, Nat>, +h: {memn(y, a) == True{} : Bool}) -> {memn(y, SC.append(Nat, a, x)) == True{} : Bool}:
146 L.subst(Bool, z => {z == True{} : Bool}, Bool.or(memn(y, a), memn(y, x)), memn(y, SC.append(Nat, a, x)), Equal.sym(Bool, memn(y, SC.append(Nat, a, x)), Bool.or(memn(y, a), memn(y, x)), memn_app(y, a, x)), L.subst(Bool, z => {Bool.or(z, memn(y, x)) == True{} : Bool}, True{}, memn(y, a), Equal.sym(Bool, memn(y, a), True{}, h), {==}))
147
148def dj_c(+y: Nat, +h0: Nat, +t: List<&2, Nat>, +x: List<&2, Nat>, +hy: {memn(y, x) == True{} : Bool}, +hn: {Bool.not(memn(h0, SC.append(Nat, t, x))) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(h0, y) == c : Bool}) -> {c == False{} : Bool}:
149 match c:
150 case True{}:
151 +e = N.eq_from_is_eq(h0, y, hc)
152 +hm = mem_app_r(y, t, x, hy)
153 Empty.absurd({True{} == False{} : Bool}, L.false_true(L.subst(Bool, z => {Bool.not(z) == True{} : Bool}, memn(h0, SC.append(Nat, t, x)), True{}, L.subst(Nat, w => {memn(w, SC.append(Nat, t, x)) == True{} : Bool}, y, h0, Equal.sym(Nat, h0, y, e), hm), hn)))
154 case False{}:
155 {==}
156
157def nd_dj(+a: List<&2, Nat>, +x: List<&2, Nat>, +h: {nodupn(SC.append(Nat, a, x)) == True{} : Bool}, +y: Nat, +hy: {memn(y, x) == True{} : Bool}) -> {memn(y, a) == False{} : Bool}:
158 match a:
159 case Nil{}:
160 {==}
161 case Con{+h0, +t}:
162 +hn = L.and_left(Bool.not(memn(h0, SC.append(Nat, t, x))), nodupn(SC.append(Nat, t, x)), h)
163 +e1 = dj_c(y, h0, t, x, hy, hn, Nat.is_eq(h0, y), {==})
164 +e2 = nd_dj(t, x, L.and_right(Bool.not(memn(h0, SC.append(Nat, t, x))), nodupn(SC.append(Nat, t, x)), h), y, hy)
165 L.subst(Bool, z => {Bool.or(z, memn(y, t)) == False{} : Bool}, False{}, Nat.is_eq(h0, y), Equal.sym(Bool, Nat.is_eq(h0, y), False{}, e1), e2)
166
167def dj2_c(+a: List<&2, Nat>, +x: List<&2, Nat>, +h: {nodupn(SC.append(Nat, a, x)) == True{} : Bool}, +y: Nat, +hy: {memn(y, a) == True{} : Bool}, +c: Bool, +hc: {memn(y, x) == c : Bool}) -> {c == False{} : Bool}:
168 match c:
169 case True{}:
170 Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, memn(y, a), False{}, Equal.sym(Bool, memn(y, a), True{}, hy), nd_dj(a, x, h, y, hc))))
171 case False{}:
172 {==}
173
174def nd_dj2(+a: List<&2, Nat>, +x: List<&2, Nat>, +h: {nodupn(SC.append(Nat, a, x)) == True{} : Bool}, +y: Nat, +hy: {memn(y, a) == True{} : Bool}) -> {memn(y, x) == False{} : Bool}:
175 dj2_c(a, x, h, y, hy, memn(y, x), {==})
176
177def or_ff_l(+a: Bool, +b: Bool, +h: {Bool.or(a, b) == False{} : Bool}) -> {a == False{} : Bool}:
178 match a:
179 case True{}:
180 Empty.absurd({True{} == False{} : Bool}, L.true_false(h))
181 case False{}:
182 {==}
183
184def or_ff_r(+a: Bool, +b: Bool, +h: {Bool.or(a, b) == False{} : Bool}) -> {b == False{} : Bool}:
185 match a:
186 case True{}:
187 Empty.absurd({b == False{} : Bool}, L.true_false(h))
188 case False{}:
189 h
190
191def not_f(+a: Bool, +h: {a == False{} : Bool}) -> {Bool.not(a) == True{} : Bool}:
192 L.subst(Bool, z => {Bool.not(z) == True{} : Bool}, False{}, a, Equal.sym(Bool, a, False{}, h), {==})
193
194def or_tl(+a: Bool, +b: Bool, +h: {a == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}:
195 L.subst(Bool, z => {Bool.or(z, b) == True{} : Bool}, True{}, a, Equal.sym(Bool, a, True{}, h), {==})
196
197def or_tr(+a: Bool, +b: Bool, +h: {b == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}:
198 Equal.trans(Bool, Bool.or(a, b), Bool.or(b, a), True{}, or_comm(a, b), or_tl(b, a, h))
199
200def and3(+a: Bool, +b: Bool, +c: Bool, +d: Bool) -> {Bool.and(a, Bool.and(b, Bool.and(c, d))) == Bool.and(Bool.and(a, Bool.and(b, c)), d) : Bool}:
201 match a b:
202 case True{} True{}:
203 {==}
204 case True{} False{}:
205 {==}
206 case False{} b2:
207 {==}
208
209def ne_sym(+x: Nat, +y: Nat, +h: {Nat.is_eq(x, y) == False{} : Bool}) -> {Nat.is_eq(y, x) == False{} : Bool}:
210 Equal.trans(Bool, Nat.is_eq(y, x), Nat.is_eq(x, y), False{}, is_eq_sym(y, x), h)
211
212def lastn(t: List<&2, Nat>, +a: Nat) -> Nat:
213 match t:
214 case Nil{}:
215 a
216 case Con{+b, +t2}:
217 lastn(t2, b)
218
219def lastn_mem(+t: List<&2, Nat>, +a: Nat) -> {memn(lastn(t, a), Con{a, t}) == True{} : Bool}:
220 match t:
221 case Nil{}:
222 or_tl(Nat.is_eq(a, a), False{}, N.is_eq_refl(a))
223 case Con{+b, +t2}:
224 or_tr(Nat.is_eq(a, lastn(t2, b)), memn(lastn(t2, b), Con{b, t2}), lastn_mem(t2, b))
225
226def ne_mem_c(+a: Nat, +z: Nat, +xs: List<&2, Nat>, +h1: {Bool.not(memn(a, xs)) == True{} : Bool}, +h2: {memn(z, xs) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(z, a) == c : Bool}) -> {c == False{} : Bool}:
227 match c:
228 case True{}:
229 +e = N.eq_from_is_eq(z, a, hc)
230 Empty.absurd({True{} == False{} : Bool}, L.false_true(L.subst(Bool, b => {Bool.not(b) == True{} : Bool}, memn(a, xs), True{}, L.subst(Nat, w => {memn(w, xs) == True{} : Bool}, z, a, e, h2), h1)))
231 case False{}:
232 {==}
233
234def ne_mem(+a: Nat, +z: Nat, +xs: List<&2, Nat>, +h1: {Bool.not(memn(a, xs)) == True{} : Bool}, +h2: {memn(z, xs) == True{} : Bool}) -> {Nat.is_eq(z, a) == False{} : Bool}:
235 ne_mem_c(a, z, xs, h1, h2, Nat.is_eq(z, a), {==})
236
237def rapp(l: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
238 match l:
239 case Nil{}:
240 b
241 case Con{+x, r}:
242 rapp(r, Con{x, b})
243
244def len_rapp(+l: List<&2, Nat>, +b: List<&2, Nat>) -> {SC.length(Nat, rapp(l, b)) == Nat.add(SC.length(Nat, l), SC.length(Nat, b)) : Nat}:
245 match l:
246 case Nil{}:
247 {==}
248 case Con{+x, +r}:
249 Equal.trans(Nat, SC.length(Nat, rapp(r, Con{x, b})), Nat.add(SC.length(Nat, r), 1n+SC.length(Nat, b)), 1n+Nat.add(SC.length(Nat, r), SC.length(Nat, b)), len_rapp(r, Con{x, b}), N.add_succ(SC.length(Nat, r), SC.length(Nat, b)))
250
251def Split(+s: Nat, +sl: List<&2, Nat>) -> Type:
252 Sigma<&1, &1, List<&2, Nat>, a => Sigma<&1, &1, List<&2, Nat>, b => {sl == SC.append(Nat, a, Con{s, b}) : List<&2, Nat>}>>
253
254def sp_up(+x: Nat, +s: Nat, +t: List<&2, Nat>, r: Split(s, t)) -> Split(s, Con{x, t}):
255 match r:
256 case Tuple{+a, Tuple{+b, e}}:
257 (Con{x, a}, (b, LL.cons_cong(Nat, x, t, SC.append(Nat, a, Con{s, b}), e)))
258
259def sp_c(+x: Nat, +s: Nat, +t: List<&2, Nat>, +c: Bool, +hc: {Nat.is_eq(x, s) == c : Bool}, +hm: {Bool.or(c, memn(s, t)) == True{} : Bool}, rec: @h: {memn(s, t) == True{} : Bool} -> Split(s, t)) -> Split(s, Con{x, t}):
260 match c:
261 case True{}:
262 (Nil{}, (t, Equal.cong(Nat, List<&2, Nat>, z => Con{z, t}, x, s, N.eq_from_is_eq(x, s, hc))))
263 case False{}:
264 sp_up(x, s, t, rec(hm))
265
266def split_mem(+s: Nat, +sl: List<&2, Nat>, +hm: {memn(s, sl) == True{} : Bool}) -> Split(s, sl):
267 match sl:
268 case Nil{}:
269 Empty.absurd(Split(s, Nil{}), L.false_true(hm))
270 case Con{+x, +t}:
271 sp_c(x, s, t, Nat.is_eq(x, s), {==}, hm, h => split_mem(s, t, h))