1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/list.bend as LL
5	import ../../../spec/lib/common.bend as SC
6	
7	# List facts about take / drop / update at one position, used to describe the
8	# effect of an indexed loop over an array on the list of its slots.
9	
10	def take_zero(-A: Data, xs: List<&2, A>) -> {SC.take(A, xs, 0n) == Nil{} : List<&2, A>}:
11	  match xs:
12	    case Nil{}:
13	      {==}
14	    case Con{h, t}:
15	      {==}
16	
17	def drop_zero(-A: Data, xs: List<&2, A>) -> {SC.drop(A, xs, 0n) == xs : List<&2, A>}:
18	  match xs:
19	    case Nil{}:
20	      {==}
21	    case Con{h, t}:
22	      {==}
23	
24	# The element at q, pulled out of the tail that starts there.
25	def drop_cons(-A: Data, xs: List<&2, A>, q: Nat, +x: A, +hx: {SC.nth(A, xs, q) == Some{x} : Maybe<&2, A>}) -> {SC.drop(A, xs, q) == Con{x, SC.drop(A, xs, 1n+q)} : List<&2, A>}:
26	  match xs q:
27	    case Nil{} _:
28	      Empty.absurd({Nil{} == Con{x, Nil{}} : List<&2, A>}, L.none_some(A, x, hx))
29	    case Con{h, t} 0n:
30	      %Equal.sym(List<&2, A>, SC.drop(A, t, 0n), t, drop_zero(A, t)) : {Con{h, t} == Con{x, _} : List<&2, A>}
31	      %Equal.sym(A, h, x, L.some_inj(A, h, x, hx)) : {Con{_, t} == Con{x, t} : List<&2, A>}
32	      {==}
33	    case Con{h, t} 1n+p:
34	      drop_cons(A, t, p, x, hx)
35	
36	# One more element taken is that element appended.
37	def take_succ(-A: Data, xs: List<&2, A>, q: Nat, +x: A, +hx: {SC.nth(A, xs, q) == Some{x} : Maybe<&2, A>}) -> {SC.take(A, xs, 1n+q) == SC.snoc(A, SC.take(A, xs, q), x) : List<&2, A>}:
38	  match xs q:
39	    case Nil{} _:
40	      Empty.absurd({Nil{} == Con{x, Nil{}} : List<&2, A>}, L.none_some(A, x, hx))
41	    case Con{h, t} 0n:
42	      %Equal.sym(List<&2, A>, SC.take(A, t, 0n), Nil{}, take_zero(A, t)) : {Con{h, _} == SC.snoc(A, Nil{}, x) : List<&2, A>}
43	      %Equal.sym(A, h, x, L.some_inj(A, h, x, hx)) : {Con{_, Nil{}} == SC.snoc(A, Nil{}, x) : List<&2, A>}
44	      {==}
45	    case Con{h, t} 1n+p:
46	      Equal.cong(List<&2, A>, List<&2, A>, z => Con{h, z}, SC.take(A, t, 1n+p), SC.snoc(A, SC.take(A, t, p), x), take_succ(A, t, p, x, hx))
47	
48	# Replacing position q does not disturb what follows it.
49	def drop_update(-A: Data, xs: List<&2, A>, q: Nat, +v: A) -> {SC.drop(A, SC.update(A, xs, q, v), 1n+q) == SC.drop(A, xs, 1n+q) : List<&2, A>}:
50	  match xs q:
51	    case Nil{} _:
52	      {==}
53	    case Con{h, t} 0n:
54	      {==}
55	    case Con{h, t} 1n+p:
56	      drop_update(A, t, p, v)
57	
58	# ... nor what precedes it.
59	def take_update(-A: Data, xs: List<&2, A>, q: Nat, +v: A) -> {SC.take(A, SC.update(A, xs, q, v), q) == SC.take(A, xs, q) : List<&2, A>}:
60	  match xs q:
61	    case Nil{} _:
62	      {==}
63	    case Con{h, t} 0n:
64	      {==}
65	    case Con{h, t} 1n+p:
66	      Equal.cong(List<&2, A>, List<&2, A>, z => Con{h, z}, SC.take(A, SC.update(A, t, p, v), p), SC.take(A, t, p), take_update(A, t, p, v))
67	
68	def take_update_succ(-A: Data, xs: List<&2, A>, q: Nat, +v: A, +h: {Nat.is_lt(q, SC.length(A, xs)) == True{} : Bool}) -> {SC.take(A, SC.update(A, xs, q, v), 1n+q) == SC.snoc(A, SC.take(A, xs, q), v) : List<&2, A>}:
69	  match xs q:
70	    case Nil{} _:
71	      Empty.absurd({SC.take(A, Nil{}, 1n+q) == SC.snoc(A, Nil{}, v) : List<&2, A>}, N.lt_zero_absurd(q, h))
72	    case Con{h2, t} 0n:
73	      %Equal.sym(List<&2, A>, SC.take(A, t, 0n), Nil{}, take_zero(A, t)) : {Con{v, _} == SC.snoc(A, Nil{}, v) : List<&2, A>}
74	      {==}
75	    case Con{h2, t} 1n+p:
76	      Equal.cong(List<&2, A>, List<&2, A>, z => Con{h2, z}, SC.take(A, SC.update(A, t, p, v), 1n+p), SC.snoc(A, SC.take(A, t, p), v), take_update_succ(A, t, p, v, h))
77	
78	def take_all(-A: Data, xs: List<&2, A>) -> {SC.take(A, xs, SC.length(A, xs)) == xs : List<&2, A>}:
79	  match xs:
80	    case Nil{}:
81	      {==}
82	    case Con{h, t}:
83	      Equal.cong(List<&2, A>, List<&2, A>, z => Con{h, z}, SC.take(A, t, SC.length(A, t)), t, take_all(A, t))
84	
85	def drop_all(-A: Data, xs: List<&2, A>) -> {SC.drop(A, xs, SC.length(A, xs)) == Nil{} : List<&2, A>}:
86	  match xs:
87	    case Nil{}:
88	      {==}
89	    case Con{h, t}:
90	      drop_all(A, t)
91