1 import Base 2 import ./logic.bend as L 3 import ./nat.bend as N 4 import ./list.bend as LL 5 import ../../spec/lib/common.bend as SC 6 import ../../src/containers/internal/vec.bend as V 7 import ./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 13 def slots(-T: Data, t: V.Vec) -> 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 20 def perfect(-T: Data, +d: Nat, t: V.Vec) -> 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 31 def pf_left(-T: Data, +p: Nat, +l: V.Vec, +r: V.Vec, +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 34 def pf_right(-T: Data, +p: Nat, +l: V.Vec, +r: V.Vec, +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 37 def slots_length(-T: Data, +d: Nat, +t: V.Vec, +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 51 def 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 54 def left_len(-T: Data, +p: Nat, +l: V.Vec, +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 59 def get_go(-T: Data, +d: Nat, +t: V.Vec, +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 86 def get(-T: Data, +d: Nat, +t: V.Vec, +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 91 def set_go_perfect(-T: Data, +d: Nat, +t: V.Vec, +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 104 def set_perfect(-T: Data, +d: Nat, +t: V.Vec, +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 107 def set_go_slots(-T: Data, +d: Nat, +t: V.Vec, +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 134 def set(-T: Data, +d: Nat, +t: V.Vec, +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 139 def 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. 147 def 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 154 def 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 163 def 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 189 def 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)