def AP.set_leaves
bend-osdev-array@0.1.0.1 · PROOF.bend:1108
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
import bend-osdev-array@0.1.0.1/array.bend as A
1108def AP.set_leaves(-T: Data, +d: Nat, +t: AP.Tree<T>, +i: U32, +v: T, b: Bool, +eb: {U32.is_lt(i, U32.shr(U32.shln(1, d))) == b : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}) -> {A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, t, U32.shln(1, d), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), U32.to_nat(i), v) : List<&2, T>}:
1109 match d t b:
1110 case 0n APLeaf{+x} _:
1111 %Equal.sym(Nat, U32.to_nat(i), 0n, AP.lt_one(U32.to_nat(i), hi)) : {Con{v, Nil{}} == List.set(&2, T, Con{x, Nil{}}, _, v) : List<&2, T>}
1112 {==}
1113 case 0n APNode{xs, ys} _:
1114 Empty.absurd({A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, APNode{xs, ys}, U32.shln(1, 0n), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys})), U32.to_nat(i), v) : List<&2, T>}, AP.ft(hp))
1115 case 1n+p APLeaf{x} _:
1116 Empty.absurd({A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, APLeaf{x}, U32.shln(1, 1n+p), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, APLeaf{x})), U32.to_nat(i), v) : List<&2, T>}, AP.ft(hp))
1117 case 1n+ +p APNode{xs, ys} True{}:
1118 +hd1 = AP.lt_succ_l(p, 32n, hd)
1119 +s = A.Arrays.slots(p)
1120 +sh = U32.shln(1, p)
1121 +lx = A.Arrays.leaves(T, AP.build(T, xs))
1122 +ly = A.Arrays.leaves(T, AP.build(T, ys))
1123 +k = U32.to_nat(i)
1124 +z1 = U32.is_lt(i, U32.shr(sh))
1125 +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1126 +hi1 = AP.lt_true(i, p, hd1, AP.eb_fix(i, p, True{}, hd, eb))
1127 +hl = AP.lt_rw_r(k, List.length(&2, T, lx), s, AP.len_perf(T, p, xs, hpx), hi1)
1128 %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.append(&2, T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, _, i, v, U32.is_lt(i, U32.shr(_))))), ly) == List.set(&2, T, List.append(&2, T, lx, ly), k, v) : List<&2, T>}
1129 Equal.trans(List<&2, T>, List.append(&2, T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, sh, i, v, z1))), ly), List.append(&2, T, List.set(&2, T, lx, k, v), ly), List.set(&2, T, List.append(&2, T, lx, ly), k, v), AP.app_cong_l(T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, sh, i, v, z1))), List.set(&2, T, lx, k, v), ly, AP.set_leaves(T, p, xs, i, v, z1, {==}, hd1, hpx, hi1)), Equal.sym(List<&2, T>, List.set(&2, T, List.append(&2, T, lx, ly), k, v), List.append(&2, T, List.set(&2, T, lx, k, v), ly), AP.set_app_l(T, lx, ly, k, v, hl)))
1130 case 1n+ +p APNode{xs, ys} False{}:
1131 +hd1 = AP.lt_succ_l(p, 32n, hd)
1132 +s = A.Arrays.slots(p)
1133 +sh = U32.shln(1, p)
1134 +lx = A.Arrays.leaves(T, AP.build(T, xs))
1135 +ly = A.Arrays.leaves(T, AP.build(T, ys))
1136 +j = U32.sub(i, sh)
1137 +w = U32.to_nat(j)
1138 +z1 = U32.is_lt(j, U32.shr(sh))
1139 +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1140 +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1141 +hs = AP.split(i, p, hd1, AP.eb_fix(i, p, False{}, hd, eb))
1142 +hj = AP.lt_split2(w, s, AP.lt_rw_l(Nat.add(s, w), U32.to_nat(i), Nat.double(s), hs, hi))
1143 %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, _, U32.sub(i, _), v, U32.is_lt(U32.sub(i, _), U32.shr(_)))))) == List.set(&2, T, List.append(&2, T, lx, ly), U32.to_nat(i), v) : List<&2, T>}
1144 %hs : {List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))) == List.set(&2, T, List.append(&2, T, lx, ly), _, v) : List<&2, T>}
1145 %AP.len_perf(T, p, xs, hpx) : {List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))) == List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(_, w), v) : List<&2, T>}
1146 Equal.trans(List<&2, T>, List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))), List.append(&2, T, lx, List.set(&2, T, ly, w, v)), List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w), v), AP.app_cong_r(T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1))), List.set(&2, T, ly, w, v), AP.set_leaves(T, p, ys, j, v, z1, {==}, hd1, hpy, hj)), Equal.sym(List<&2, T>, List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w), v), List.append(&2, T, lx, List.set(&2, T, ly, w, v)), AP.set_app_r(T, lx, ly, w, v)))