proofs/lib/vec.bend
bend-collections-laws-containers@1.0.0.0 · 192 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/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/src/containers/internal/vec.bend as V
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
8
9# Functional correctness of the persistent vector src/internal/vec.bend:
10# a perfect tree of depth d means its in-order slot list (length 2^d);
11# get reads, set updates that list.
12
13def slots(-T: Data, t: V.Vec<T>) -> List<&2, T>:
14 match t:
15 case V.VLeaf{x}:
16 Con{x, Nil{}}
17 case V.VNode{l, r}:
18 SC.append(T, slots(T, l), slots(T, r))
19
20def perfect(-T: Data, +d: Nat, t: V.Vec<T>) -> Bool:
21 match d t:
22 case 0n V.VLeaf{x}:
23 True{}
24 case 0n V.VNode{l, r}:
25 False{}
26 case 1n+p V.VLeaf{x}:
27 False{}
28 case 1n+p V.VNode{l, r}:
29 Bool.and(perfect(T, p, l), perfect(T, p, r))
30
31def pf_left(-T: Data, +p: Nat, +l: V.Vec<T>, +r: V.Vec<T>, +pf: {perfect(T, 1n+p, V.VNode{l, r}) == True{} : Bool}) -> {perfect(T, p, l) == True{} : Bool}:
32 L.and_left(perfect(T, p, l), perfect(T, p, r), pf)
33
34def pf_right(-T: Data, +p: Nat, +l: V.Vec<T>, +r: V.Vec<T>, +pf: {perfect(T, 1n+p, V.VNode{l, r}) == True{} : Bool}) -> {perfect(T, p, r) == True{} : Bool}:
35 L.and_right(perfect(T, p, l), perfect(T, p, r), pf)
36
37def slots_length(-T: Data, +d: Nat, +t: V.Vec<T>, +pf: {perfect(T, d, t) == True{} : Bool}) -> {SC.length(T, slots(T, t)) == V.pow2(d) : Nat}:
38 match d t:
39 case 0n V.VLeaf{x}:
40 {==}
41 case 0n V.VNode{l, r}:
42 Empty.absurd({SC.length(T, slots(T, V.VNode{l, r})) == 1n : Nat}, L.false_true(pf))
43 case 1n+p V.VLeaf{x}:
44 Empty.absurd({1n == Nat.double(V.pow2(p)) : Nat}, L.false_true(pf))
45 case 1n+ +p V.VNode{+l, +r}:
46 %Equal.sym(Nat, SC.length(T, SC.append(T, slots(T, l), slots(T, r))), Nat.add(SC.length(T, slots(T, l)), SC.length(T, slots(T, r))), LL.length_append(T, slots(T, l), slots(T, r))) : {_ == Nat.double(V.pow2(p)) : Nat}
47 %Equal.sym(Nat, SC.length(T, slots(T, l)), V.pow2(p), slots_length(T, p, l, pf_left(T, p, l, r, pf))) : {Nat.add(_, SC.length(T, slots(T, r))) == Nat.double(V.pow2(p)) : Nat}
48 %Equal.sym(Nat, SC.length(T, slots(T, r)), V.pow2(p), slots_length(T, p, r, pf_right(T, p, l, r, pf))) : {Nat.add(V.pow2(p), _) == Nat.double(V.pow2(p)) : Nat}
49 Equal.sym(Nat, Nat.double(V.pow2(p)), Nat.add(V.pow2(p), V.pow2(p)), NA.double_self(V.pow2(p)))
50
51def upper_lt(+j: Nat, +p: Nat, +hj: {Nat.is_lt(j, V.pow2(1n+p)) == True{} : Bool}, +le: {Nat.is_le(V.pow2(p), j) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(j, V.pow2(p)), V.pow2(p)) == True{} : Bool}:
52 N.sub_lt(j, V.pow2(p), V.pow2(p), le, L.subst(Nat, n => {Nat.is_lt(j, n) == True{} : Bool}, Nat.double(V.pow2(p)), Nat.add(V.pow2(p), V.pow2(p)), NA.double_self(V.pow2(p)), hj))
53
54def left_len(-T: Data, +p: Nat, +l: V.Vec<T>, +pl: {perfect(T, p, l) == True{} : Bool}) -> {V.pow2(p) == SC.length(T, slots(T, l)) : Nat}:
55 Equal.sym(Nat, SC.length(T, slots(T, l)), V.pow2(p), slots_length(T, p, l, pl))
56
57# ---- get ----
58
59def get_go(-T: Data, +d: Nat, +t: V.Vec<T>, +j: Nat, +hj: {Nat.is_lt(j, V.pow2(d)) == True{} : Bool}, +b: Bool, +eb: {V.dec(d, j) == b : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {V.get_go(T, d, t, j, b) == SC.nth(T, slots(T, t), j) : Maybe<&2, T>}:
60 match d t b:
61 case 0n V.VLeaf{x} _:
62 match j:
63 case 0n:
64 {==}
65 case 1n+q:
66 Empty.absurd({Some{x} == SC.nth(T, Con{x, Nil{}}, 1n+q) : Maybe<&2, T>}, N.lt_zero_absurd(q, hj))
67 case 0n V.VNode{l, r} _:
68 Empty.absurd({None{} == SC.nth(T, slots(T, V.VNode{l, r}), j) : Maybe<&2, T>}, L.false_true(pf))
69 case 1n+p V.VLeaf{x} _:
70 Empty.absurd({None{} == SC.nth(T, Con{x, Nil{}}, j) : Maybe<&2, T>}, L.false_true(pf))
71 case 1n+ +p V.VNode{+l, +r} True{}:
72 +hl = L.subst(Nat, k => {Nat.is_lt(j, k) == True{} : Bool}, V.pow2(p), SC.length(T, slots(T, l)), left_len(T, p, l, pf_left(T, p, l, r, pf)), eb)
73 Equal.trans(Maybe<&2, T>, V.get_go(T, p, l, j, V.dec(p, j)), SC.nth(T, slots(T, l), j), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), j),
74 get_go(T, p, l, j, eb, V.dec(p, j), {==}, pf_left(T, p, l, r, pf)),
75 Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), j), SC.nth(T, slots(T, l), j), LL.nth_append_left(T, slots(T, l), slots(T, r), j, hl)))
76 case 1n+ +p V.VNode{+l, +r} False{}:
77 +k = Nat.sub(j, V.pow2(p))
78 +le = N.not_lt_le(j, V.pow2(p), eb)
79 +hr = L.subst(Nat, q => {Nat.is_le(q, j) == True{} : Bool}, V.pow2(p), SC.length(T, slots(T, l)), left_len(T, p, l, pf_left(T, p, l, r, pf)), le)
80 Equal.trans(Maybe<&2, T>, V.get_go(T, p, r, k, V.dec(p, k)), SC.nth(T, slots(T, r), k), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), j),
81 get_go(T, p, r, k, upper_lt(j, p, hj, le), V.dec(p, k), {==}, pf_right(T, p, l, r, pf)),
82 Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), j), SC.nth(T, slots(T, r), k),
83 %Equal.sym(Nat, V.pow2(p), SC.length(T, slots(T, l)), left_len(T, p, l, pf_left(T, p, l, r, pf))) : {SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), j) == SC.nth(T, slots(T, r), Nat.sub(j, _)) : Maybe<&2, T>}
84 LL.nth_append_right(T, slots(T, l), slots(T, r), j, hr)))
85
86def get(-T: Data, +d: Nat, +t: V.Vec<T>, +j: Nat, +hj: {Nat.is_lt(j, V.pow2(d)) == True{} : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {V.get(T, d, t, j) == SC.nth(T, slots(T, t), j) : Maybe<&2, T>}:
87 get_go(T, d, t, j, hj, V.dec(d, j), {==}, pf)
88
89# ---- set ----
90
91def set_go_perfect(-T: Data, +d: Nat, +t: V.Vec<T>, +j: Nat, +v: T, +b: Bool, +pf: {perfect(T, d, t) == True{} : Bool}) -> {perfect(T, d, V.set_go(T, d, t, j, v, b)) == True{} : Bool}:
92 match d t b:
93 case 0n V.VLeaf{x} _:
94 {==}
95 case 0n V.VNode{l, r} _:
96 pf
97 case 1n+p V.VLeaf{x} _:
98 pf
99 case 1n+ +p V.VNode{+l, +r} True{}:
100 L.and_intro(perfect(T, p, V.set_go(T, p, l, j, v, V.dec(p, j))), perfect(T, p, r), set_go_perfect(T, p, l, j, v, V.dec(p, j), pf_left(T, p, l, r, pf)), pf_right(T, p, l, r, pf))
101 case 1n+ +p V.VNode{+l, +r} False{}:
102 L.and_intro(perfect(T, p, l), perfect(T, p, V.set_go(T, p, r, Nat.sub(j, V.pow2(p)), v, V.dec(p, Nat.sub(j, V.pow2(p))))), pf_left(T, p, l, r, pf), set_go_perfect(T, p, r, Nat.sub(j, V.pow2(p)), v, V.dec(p, Nat.sub(j, V.pow2(p))), pf_right(T, p, l, r, pf)))
103
104def set_perfect(-T: Data, +d: Nat, +t: V.Vec<T>, +j: Nat, +v: T, +pf: {perfect(T, d, t) == True{} : Bool}) -> {perfect(T, d, V.set(T, d, t, j, v)) == True{} : Bool}:
105 set_go_perfect(T, d, t, j, v, V.dec(d, j), pf)
106
107def set_go_slots(-T: Data, +d: Nat, +t: V.Vec<T>, +j: Nat, +v: T, +hj: {Nat.is_lt(j, V.pow2(d)) == True{} : Bool}, +b: Bool, +eb: {V.dec(d, j) == b : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {slots(T, V.set_go(T, d, t, j, v, b)) == SC.update(T, slots(T, t), j, v) : List<&2, T>}:
108 match d t b:
109 case 0n V.VLeaf{x} _:
110 match j:
111 case 0n:
112 {==}
113 case 1n+q:
114 Empty.absurd({Con{v, Nil{}} == SC.update(T, Con{x, Nil{}}, 1n+q, v) : List<&2, T>}, N.lt_zero_absurd(q, hj))
115 case 0n V.VNode{l, r} _:
116 Empty.absurd({slots(T, V.VNode{l, r}) == SC.update(T, slots(T, V.VNode{l, r}), j, v) : List<&2, T>}, L.false_true(pf))
117 case 1n+p V.VLeaf{x} _:
118 Empty.absurd({Con{x, Nil{}} == SC.update(T, Con{x, Nil{}}, j, v) : List<&2, T>}, L.false_true(pf))
119 case 1n+ +p V.VNode{+l, +r} True{}:
120 +hl = L.subst(Nat, k => {Nat.is_lt(j, k) == True{} : Bool}, V.pow2(p), SC.length(T, slots(T, l)), left_len(T, p, l, pf_left(T, p, l, r, pf)), eb)
121 Equal.trans(List<&2, T>, SC.append(T, slots(T, V.set_go(T, p, l, j, v, V.dec(p, j))), slots(T, r)), SC.append(T, SC.update(T, slots(T, l), j, v), slots(T, r)), SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v),
122 Equal.cong(List<&2, T>, List<&2, T>, xs => SC.append(T, xs, slots(T, r)), slots(T, V.set_go(T, p, l, j, v, V.dec(p, j))), SC.update(T, slots(T, l), j, v), set_go_slots(T, p, l, j, v, eb, V.dec(p, j), {==}, pf_left(T, p, l, r, pf))),
123 Equal.sym(List<&2, T>, SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v), SC.append(T, SC.update(T, slots(T, l), j, v), slots(T, r)), LL.update_append_left(T, slots(T, l), slots(T, r), j, v, hl)))
124 case 1n+ +p V.VNode{+l, +r} False{}:
125 +k = Nat.sub(j, V.pow2(p))
126 +le = N.not_lt_le(j, V.pow2(p), eb)
127 +hr = L.subst(Nat, q => {Nat.is_le(q, j) == True{} : Bool}, V.pow2(p), SC.length(T, slots(T, l)), left_len(T, p, l, pf_left(T, p, l, r, pf)), le)
128 Equal.trans(List<&2, T>, SC.append(T, slots(T, l), slots(T, V.set_go(T, p, r, k, v, V.dec(p, k)))), SC.append(T, slots(T, l), SC.update(T, slots(T, r), k, v)), SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v),
129 Equal.cong(List<&2, T>, List<&2, T>, xs => SC.append(T, slots(T, l), xs), slots(T, V.set_go(T, p, r, k, v, V.dec(p, k))), SC.update(T, slots(T, r), k, v), set_go_slots(T, p, r, k, v, upper_lt(j, p, hj, le), V.dec(p, k), {==}, pf_right(T, p, l, r, pf))),
130 Equal.sym(List<&2, T>, SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v), SC.append(T, slots(T, l), SC.update(T, slots(T, r), k, v)),
131 %Equal.sym(Nat, V.pow2(p), SC.length(T, slots(T, l)), left_len(T, p, l, pf_left(T, p, l, r, pf))) : {SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v) == SC.append(T, slots(T, l), SC.update(T, slots(T, r), Nat.sub(j, _), v)) : List<&2, T>}
132 LL.update_append_right(T, slots(T, l), slots(T, r), j, v, hr)))
133
134def set(-T: Data, +d: Nat, +t: V.Vec<T>, +j: Nat, +v: T, +hj: {Nat.is_lt(j, V.pow2(d)) == True{} : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {slots(T, V.set(T, d, t, j, v)) == SC.update(T, slots(T, t), j, v) : List<&2, T>}:
135 set_go_slots(T, d, t, j, v, hj, V.dec(d, j), {==}, pf)
136
137# ---- capacity chosen by depth_for ----
138
139def pow2_pos(+d: Nat) -> {Nat.is_le(1n, V.pow2(d)) == True{} : Bool}:
140 match d:
141 case 0n:
142 {==}
143 case 1n+p:
144 N.le_trans(1n, V.pow2(p), Nat.double(V.pow2(p)), pow2_pos(p), N.double_self_le(V.pow2(p)))
145
146# n + 2^d <= 2^(depth_go n d room) + room, for room <= 2^d.
147def arr(+p: Nat, +a: Nat, +c: Nat) -> {Nat.add(p, Nat.add(Nat.add(1n, a), c)) == Nat.add(Nat.add(1n+p, c), a) : Nat}:
148 %Equal.sym(Nat, Nat.add(Nat.add(1n, a), c), Nat.add(1n, Nat.add(a, c)), N.add_assoc(1n, a, c)) : {Nat.add(p, _) == Nat.add(Nat.add(1n+p, c), a) : Nat}
149 %Equal.sym(Nat, Nat.add(p, 1n+Nat.add(a, c)), 1n+Nat.add(p, Nat.add(a, c)), N.add_succ(p, Nat.add(a, c))) : {_ == Nat.add(Nat.add(1n+p, c), a) : Nat}
150 %Equal.sym(Nat, Nat.add(a, c), Nat.add(c, a), N.add_comm(a, c)) : {1n+Nat.add(p, _) == Nat.add(Nat.add(1n+p, c), a) : Nat}
151 %N.add_assoc(p, c, a) : {1n+_ == Nat.add(Nat.add(1n+p, c), a) : Nat}
152 {==}
153
154def le_add_cancel(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
155 match c:
156 case 0n:
157 L.subst(Nat, q => {Nat.is_le(q, b) == True{} : Bool}, Nat.add(a, 0n), a, N.add_zero(a), L.subst(Nat, q => {Nat.is_le(Nat.add(a, 0n), q) == True{} : Bool}, Nat.add(b, 0n), b, N.add_zero(b), h))
158 case 1n+k:
159 le_add_cancel(a, b, k, L.subst(Nat, q => {Nat.is_le(q, Nat.add(b, k)) == True{} : Bool}, Nat.add(a, k), Nat.add(a, k), {==},
160 L.subst(Nat, q => {Nat.is_le(1n+Nat.add(a, k), q) == True{} : Bool}, Nat.add(b, 1n+k), 1n+Nat.add(b, k), N.add_succ(b, k),
161 L.subst(Nat, q => {Nat.is_le(q, Nat.add(b, 1n+k)) == True{} : Bool}, Nat.add(a, 1n+k), 1n+Nat.add(a, k), N.add_succ(a, k), h))))
162
163def depth_go_cap(+n: Nat, +d: Nat, +room: Nat, +h: {Nat.is_le(room, V.pow2(d)) == True{} : Bool}) -> {Nat.is_le(Nat.add(n, V.pow2(d)), Nat.add(V.pow2(V.depth_go(n, d, room)), room)) == True{} : Bool}:
164 match n room:
165 case 0n _:
166 N.le_add_right(V.pow2(d), room)
167 case 1n+p 0n:
168 +c = V.pow2(d)
169 +c1 = Nat.sub(c, 1n)
170 +pos = pow2_pos(d)
171 +e1 = N.sub_add(c, 1n, pos)
172 +R = V.pow2(V.depth_go(p, 1n+d, c1))
173 +ih = depth_go_cap(p, 1n+d, c1, N.le_trans(c1, c, Nat.double(c), L.subst(Nat, q => {Nat.is_le(c1, q) == True{} : Bool}, Nat.add(1n, c1), c, e1, N.le_succ(c1)), N.double_self_le(c)))
174 # ih : p + 2c <= R + (c - 1); with 2c = (1 + (c - 1)) + c this is 1 + p + c <= R.
175 +e2 = Equal.trans(Nat, Nat.double(c), Nat.add(c, c), Nat.add(Nat.add(1n, c1), c), NA.double_self(c), Equal.cong(Nat, Nat, q => Nat.add(q, c), c, Nat.add(1n, c1), Equal.sym(Nat, Nat.add(1n, c1), c, e1)))
176 +ih2 = L.subst(Nat, q => {Nat.is_le(Nat.add(p, q), Nat.add(R, c1)) == True{} : Bool}, Nat.double(c), Nat.add(Nat.add(1n, c1), c), e2, ih)
177 # rearrange: p + ((1 + c1) + c) == (1 + p + c) + c1 and R + c1
178 +e3 = arr(p, c1, c)
179 +ih3 = L.subst(Nat, q => {Nat.is_le(q, Nat.add(R, c1)) == True{} : Bool}, Nat.add(p, Nat.add(Nat.add(1n, c1), c)), Nat.add(Nat.add(1n+p, c), c1), e3, ih2)
180 %Equal.sym(Nat, Nat.add(R, 0n), R, N.add_zero(R)) : {Nat.is_le(Nat.add(1n+p, c), _) == True{} : Bool}
181 le_add_cancel(Nat.add(1n+p, c), R, c1, ih3)
182 case 1n+p 1n+r:
183 +ih = depth_go_cap(p, d, r, N.le_trans(r, 1n+r, V.pow2(d), N.le_succ(r), h))
184 %Equal.sym(Nat, Nat.add(V.pow2(V.depth_go(p, d, r)), 1n+r), 1n+Nat.add(V.pow2(V.depth_go(p, d, r)), r), N.add_succ(V.pow2(V.depth_go(p, d, r)), r)) : {Nat.is_le(Nat.add(1n+p, V.pow2(d)), _) == True{} : Bool}
185 ih
186
187# p + ((1 + a) + c) == ((1 + p) + c) + a
188# a + c <= b + c implies a <= b
189def depth_for(+n: Nat) -> {Nat.is_le(n, V.pow2(V.depth_for(n))) == True{} : Bool}:
190 +h = depth_go_cap(n, 0n, 1n, {==})
191 %Equal.sym(Nat, Nat.add(n, 1n), 1n+n, N.add_comm(n, 1n)) : {Nat.is_le(n, V.pow2(V.depth_for(n))) == True{} : Bool}
192 le_add_cancel(n, V.pow2(V.depth_for(n)), 1n, h)