1	import Base
2	import ./logic.bend as L
3	import ./nat.bend as N
4	import ./list.bend as LL
5	import ./u32.bend as U
6	import ./u32alg.bend as UA
7	import ../../spec/lib/common.bend as SC
8	import ../../spec/lib/u32seq.bend as Q
9	
10	# Wrapping sums of U32 sequences and point additions (addat).
11	
12	def addat(xs: List<&2, U32>, +i: Nat, +v: U32) -> List<&2, U32>:
13	  match xs i:
14	    case Nil{} _:
15	      Nil{}
16	    case Con{h, t} 0n:
17	      Con{U32.add(h, v), t}
18	    case Con{h, t} 1n+j:
19	      Con{h, addat(t, j, v)}
20	
21	def sum_append(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {Q.sum(SC.append(U32, xs, ys)) == U32.add(Q.sum(xs), Q.sum(ys)) : U32}:
22	  match xs:
23	    case Nil{}:
24	      Equal.sym(U32, U32.add(0, Q.sum(ys)), Q.sum(ys), UA.zero_add(Q.sum(ys)))
25	    case Con{h, t}:
26	      %Equal.sym(U32, Q.sum(SC.append(U32, t, ys)), U32.add(Q.sum(t), Q.sum(ys)), sum_append(t, ys)) : {U32.add(h, _) == U32.add(U32.add(h, Q.sum(t)), Q.sum(ys)) : U32}
27	      Equal.sym(U32, U32.add(U32.add(h, Q.sum(t)), Q.sum(ys)), U32.add(h, U32.add(Q.sum(t), Q.sum(ys))), UA.assoc(h, Q.sum(t), Q.sum(ys)))
28	
29	def sum_zeros(+n: Nat) -> {Q.sum(Q.zeros(n)) == 0 : U32}:
30	  match n:
31	    case 0n:
32	      {==}
33	    case 1n+k:
34	      %Equal.sym(U32, Q.sum(Q.zeros(k)), 0, sum_zeros(k)) : {U32.add(0, _) == 0 : U32}
35	      UA.zero_add(0)
36	
37	def length_addat(+xs: List<&2, U32>, +i: Nat, +v: U32) -> {SC.length(U32, addat(xs, i, v)) == SC.length(U32, xs) : Nat}:
38	  match xs i:
39	    case Nil{} _:
40	      {==}
41	    case Con{h, t} 0n:
42	      {==}
43	    case Con{h, t} 1n+j:
44	      N.succ_cong(SC.length(U32, addat(t, j, v)), SC.length(U32, t), length_addat(t, j, v))
45	
46	# Adding v at an index below the length adds v to the sum.
47	def sum_addat(+xs: List<&2, U32>, +i: Nat, +v: U32, +h: {Nat.is_lt(i, SC.length(U32, xs)) == True{} : Bool}) -> {Q.sum(addat(xs, i, v)) == U32.add(Q.sum(xs), v) : U32}:
48	  match xs i:
49	    case Nil{} _:
50	      Empty.absurd({0 == U32.add(0, v) : U32}, N.lt_zero_absurd(i, h))
51	    case Con{x, t} 0n:
52	      %Equal.sym(U32, U32.add(U32.add(x, v), Q.sum(t)), U32.add(x, U32.add(v, Q.sum(t))), UA.assoc(x, v, Q.sum(t))) : {_ == U32.add(U32.add(x, Q.sum(t)), v) : U32}
53	      %Equal.sym(U32, U32.add(U32.add(x, Q.sum(t)), v), U32.add(x, U32.add(Q.sum(t), v)), UA.assoc(x, Q.sum(t), v)) : {U32.add(x, U32.add(v, Q.sum(t))) == _ : U32}
54	      %U32.add_comm(v, Q.sum(t)) : {U32.add(x, U32.add(v, Q.sum(t))) == U32.add(x, _) : U32}
55	      {==}
56	    case Con{x, t} 1n+j:
57	      %Equal.sym(U32, Q.sum(addat(t, j, v)), U32.add(Q.sum(t), v), sum_addat(t, j, v, h)) : {U32.add(x, _) == U32.add(U32.add(x, Q.sum(t)), v) : U32}
58	      Equal.sym(U32, U32.add(U32.add(x, Q.sum(t)), v), U32.add(x, U32.add(Q.sum(t), v)), UA.assoc(x, Q.sum(t), v))
59	
60	def addat_left(+xs: List<&2, U32>, +ys: List<&2, U32>, +i: Nat, +v: U32, +h: {Nat.is_lt(i, SC.length(U32, xs)) == True{} : Bool}) -> {addat(SC.append(U32, xs, ys), i, v) == SC.append(U32, addat(xs, i, v), ys) : List<&2, U32>}:
61	  match xs i:
62	    case Nil{} _:
63	      Empty.absurd({addat(ys, i, v) == ys : List<&2, U32>}, N.lt_zero_absurd(i, h))
64	    case Con{x, t} 0n:
65	      {==}
66	    case Con{x, t} 1n+j:
67	      LL.cons_cong(U32, x, addat(SC.append(U32, t, ys), j, v), SC.append(U32, addat(t, j, v), ys), addat_left(t, ys, j, v, h))
68	
69	def addat_right(+xs: List<&2, U32>, +ys: List<&2, U32>, +i: Nat, +v: U32, +h: {Nat.is_le(SC.length(U32, xs), i) == True{} : Bool}) -> {addat(SC.append(U32, xs, ys), i, v) == SC.append(U32, xs, addat(ys, Nat.sub(i, SC.length(U32, xs)), v)) : List<&2, U32>}:
70	  match xs i:
71	    case Nil{} 0n:
72	      {==}
73	    case Nil{} 1n+j:
74	      {==}
75	    case Con{x, t} 0n:
76	      Empty.absurd({addat(SC.append(U32, Con{x, t}, ys), 0n, v) == SC.append(U32, Con{x, t}, addat(ys, Nat.sub(0n, 1n+SC.length(U32, t)), v)) : List<&2, U32>}, L.false_true(h))
77	    case Con{x, t} 1n+j:
78	      LL.cons_cong(U32, x, addat(SC.append(U32, t, ys), j, v), SC.append(U32, t, addat(ys, Nat.sub(j, SC.length(U32, t)), v)), addat_right(t, ys, j, v, h))
79	
80	def take_addat(+xs: List<&2, U32>, +i: Nat, +v: U32, +n: Nat) -> {SC.take(U32, addat(xs, i, v), n) == addat(SC.take(U32, xs, n), i, v) : List<&2, U32>}:
81	  match xs i n:
82	    case Nil{} _ _:
83	      {==}
84	    case Con{x, t} 0n 0n:
85	      {==}
86	    case Con{x, t} 1n+j 0n:
87	      {==}
88	    case Con{x, t} 0n 1n+m:
89	      {==}
90	    case Con{x, t} 1n+j 1n+m:
91	      LL.cons_cong(U32, x, SC.take(U32, addat(t, j, v), m), addat(SC.take(U32, t, m), j, v), take_addat(t, j, v, m))
92	
93	# The spec's "update index i with (old + v)" is addat.
94	def update_addat(+xs: List<&2, U32>, +i: Nat, +y: U32, +v: U32, +e: {SC.nth(U32, xs, i) == Some{y} : Maybe<&2, U32>}) -> {SC.update(U32, xs, i, U32.add(y, v)) == addat(xs, i, v) : List<&2, U32>}:
95	  match xs i:
96	    case Nil{} _:
97	      Empty.absurd({Nil{} == Nil{} : List<&2, U32>}, L.none_some(U32, y, e))
98	    case Con{x, t} 0n:
99	      %L.some_inj(U32, x, y, e) : {Con{U32.add(_, v), t} == Con{U32.add(x, v), t} : List<&2, U32>}
100	      {==}
101	    case Con{x, t} 1n+j:
102	      LL.cons_cong(U32, x, SC.update(U32, t, j, U32.add(y, v)), addat(t, j, v), update_addat(t, j, y, v, e))
103	
104	# sum of the slice [l, r) is the difference of prefix sums
105	def sum_slice(+xs: List<&2, U32>, +l: Nat, +r: Nat, +h: {Nat.is_le(l, r) == True{} : Bool}) -> {U32.sub(Q.sum(SC.take(U32, xs, r)), Q.sum(SC.take(U32, xs, l))) == Q.sum(Q.slice(xs, l, r)) : U32}:
106	  %Equal.sym(List<&2, U32>, SC.take(U32, xs, r), SC.append(U32, SC.take(U32, xs, l), SC.take(U32, SC.drop(U32, xs, l), Nat.sub(r, l))), LL.sc_take_split(U32, xs, l, r, h)) : {U32.sub(Q.sum(_), Q.sum(SC.take(U32, xs, l))) == Q.sum(Q.slice(xs, l, r)) : U32}
107	  %Equal.sym(U32, Q.sum(SC.append(U32, SC.take(U32, xs, l), Q.slice(xs, l, r))), U32.add(Q.sum(SC.take(U32, xs, l)), Q.sum(Q.slice(xs, l, r))), sum_append(SC.take(U32, xs, l), Q.slice(xs, l, r))) : {U32.sub(_, Q.sum(SC.take(U32, xs, l))) == Q.sum(Q.slice(xs, l, r)) : U32}
108	  UA.add_sub(Q.sum(SC.take(U32, xs, l)), Q.sum(Q.slice(xs, l, r)))
109	
110	# slicing the first n values equals slicing the whole list when r <= n
111	def sub_le_mono(+l: Nat, +r: Nat, +n: Nat, +h: {Nat.is_le(r, n) == True{} : Bool}) -> {Nat.is_le(Nat.sub(r, l), Nat.sub(n, l)) == True{} : Bool}:
112	  match l r n:
113	    case 0n _ _:
114	      %Equal.sym(Nat, Nat.sub(r, 0n), r, N.sub_zero(r)) : {Nat.is_le(_, Nat.sub(n, 0n)) == True{} : Bool}
115	      %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) : {Nat.is_le(r, _) == True{} : Bool}
116	      h
117	    case 1n+k 0n _:
118	      N.zero_le(Nat.sub(n, 1n+k))
119	    case 1n+k 1n+s 0n:
120	      Empty.absurd({Nat.is_le(Nat.sub(s, k), 0n) == True{} : Bool}, L.false_true(h))
121	    case 1n+k 1n+s 1n+m:
122	      sub_le_mono(k, s, m, h)
123	
124	def slice_take(+xs: List<&2, U32>, +n: Nat, +l: Nat, +r: Nat, +h: {Nat.is_le(r, n) == True{} : Bool}, +hl: {Nat.is_le(l, r) == True{} : Bool}) -> {Q.slice(SC.take(U32, xs, n), l, r) == Q.slice(xs, l, r) : List<&2, U32>}:
125	  %Equal.sym(List<&2, U32>, SC.drop(U32, SC.take(U32, xs, n), l), SC.take(U32, SC.drop(U32, xs, l), Nat.sub(n, l)), LL.sc_drop_take(U32, xs, n, l)) : {SC.take(U32, _, Nat.sub(r, l)) == Q.slice(xs, l, r) : List<&2, U32>}
126	  LL.sc_take_take(U32, SC.drop(U32, xs, l), Nat.sub(n, l), Nat.sub(r, l), sub_le_mono(l, r, n, h))