1	import Base
2	import ../../spec/lib/common.bend as SC
3	import ./logic.bend as L
4	import ./nat.bend as N
5	import ./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
12	def memn(+s: Nat, xs: List<&2, Nat>) -> Bool:
13	  SC.memn(s, xs)
14	
15	def 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	
22	def 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	
29	def 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	
40	def 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	
47	def 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	
58	def 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	
70	def 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	
81	def 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	
88	def 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	
95	def 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	
109	def not_t_f(+b: Bool, +h: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:
110	  L.not_true(b, h)
111	
112	def 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	
119	def 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	
126	def 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	
135	def or_true_b(+b: Bool) -> {Bool.or(b, True{}) == True{} : Bool}:
136	  match b:
137	    case True{}:
138	      {==}
139	    case False{}:
140	      {==}
141	
142	def 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	
145	def 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	
148	def 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	
157	def 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	
167	def 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	
174	def 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	
177	def 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	
184	def 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	
191	def 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	
194	def 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	
197	def 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	
200	def 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	
209	def 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	
212	def 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	
219	def 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	
226	def 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	
234	def 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	
237	def 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	
244	def 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	
251	def 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	
254	def 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	
259	def 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	
266	def 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))