proofs/lib/u32seq.bend
bend-collections-laws-containers@1.0.0.0 · 126 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as UA
7import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
8import bend-collections-laws-containers@1.0.0.0/spec/lib/u32seq.bend as Q
9
10# Wrapping sums of U32 sequences and point additions (addat).
11
12def 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
21def 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
29def 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
37def 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.
47def 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
60def 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
69def 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
80def 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.
94def 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
105def 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
111def 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
124def 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))