1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32.bend as U 5 import ../../lib/array.bend as AR 6 import ../../lib/array_ext.bend as AX 7 import ../../lib/list.bend as LL 8 import ../../../spec/lib/common.bend as SC 9 import ../dynamic_array/layout.bend as LY 10 11 # The canonical block of a list: a perfect tree of depth d whose slots are 12 # the list's items (Some) followed by empty slots (None). 13 14 15 # the first k slots of the items xs 16 def fill(-T: Data, +k: Nat, xs: List<&2, T>) -> List<&2, Maybe<&2, T>>: 17 match k xs: 18 case 0n _: 19 Nil{} 20 case 1n+j Nil{}: 21 Con{None{}, fill(T, j, Nil{})} 22 case 1n+j Con{x, r}: 23 Con{Some{x}, fill(T, j, r)} 24 25 def headm(-T: Data, xs: List<&2, T>) -> Maybe<&2, T>: 26 match xs: 27 case Nil{}: 28 None{} 29 case Con{x, r}: 30 Some{x} 31 32 def mk(-T: Data, +d: Nat, +xs: List<&2, T>) -> AR.Tree>: 33 match d: 34 case 0n: 35 AR.TLeaf{headm(T, xs)} 36 case 1n+p: 37 AR.TNode{mk(T, p, xs), mk(T, p, SC.drop(T, xs, SC.pow2(p)))} 38 39 def mk_perfect(-T: Data, +d: Nat, +xs: List<&2, T>) -> {AR.perfect(Maybe<&2, T>, d, mk(T, d, xs)) == True{} : Bool}: 40 match d: 41 case 0n: 42 {==} 43 case 1n+p: 44 L.and_intro(AR.perfect(Maybe<&2, T>, p, mk(T, p, xs)), AR.perfect(Maybe<&2, T>, p, mk(T, p, SC.drop(T, xs, SC.pow2(p)))), mk_perfect(T, p, xs), mk_perfect(T, p, SC.drop(T, xs, SC.pow2(p)))) 45 46 def fill_add(-T: Data, +a: Nat, +b: Nat, +xs: List<&2, T>) -> {fill(T, Nat.add(a, b), xs) == SC.append(Maybe<&2, T>, fill(T, a, xs), fill(T, b, SC.drop(T, xs, a))) : List<&2, Maybe<&2, T>>}: 47 match a xs: 48 case 0n _: 49 Equal.cong(List<&2, T>, List<&2, Maybe<&2, T>>, z => fill(T, b, z), xs, SC.drop(T, xs, 0n), Equal.sym(List<&2, T>, SC.drop(T, xs, 0n), xs, AX.drop_zero(T, xs))) 50 case 1n+j Nil{}: 51 LL.cons_cong(Maybe<&2, T>, None{}, fill(T, Nat.add(j, b), Nil{}), SC.append(Maybe<&2, T>, fill(T, j, Nil{}), fill(T, b, Nil{})), fill_add(T, j, b, Nil{})) 52 case 1n+j Con{x, +r}: 53 LL.cons_cong(Maybe<&2, T>, Some{x}, fill(T, Nat.add(j, b), r), SC.append(Maybe<&2, T>, fill(T, j, r), fill(T, b, SC.drop(T, r, j))), fill_add(T, j, b, r)) 54 55 def dbl(+p: Nat) -> {SC.pow2(1n+p) == Nat.add(SC.pow2(p), SC.pow2(p)) : Nat}: 56 Equal.trans(Nat, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), Nat.add(SC.pow2(p), 0n)), Nat.add(SC.pow2(p), SC.pow2(p)), U.double_pow(SC.pow2(p)), Equal.cong(Nat, Nat, z => Nat.add(SC.pow2(p), z), Nat.add(SC.pow2(p), 0n), SC.pow2(p), N.add_zero(SC.pow2(p)))) 57 58 def fill_one(-T: Data, +xs: List<&2, T>) -> {fill(T, 1n, xs) == Con{headm(T, xs), Nil{}} : List<&2, Maybe<&2, T>>}: 59 match xs: 60 case Nil{}: 61 {==} 62 case Con{x, r}: 63 {==} 64 65 # the slots of the canonical block 66 def mk_slots(-T: Data, +d: Nat, +xs: List<&2, T>) -> {AR.slots(Maybe<&2, T>, mk(T, d, xs)) == fill(T, SC.pow2(d), xs) : List<&2, Maybe<&2, T>>}: 67 match d: 68 case 0n: 69 Equal.sym(List<&2, Maybe<&2, T>>, fill(T, 1n, xs), Con{headm(T, xs), Nil{}}, fill_one(T, xs)) 70 case 1n+p: 71 +P = SC.pow2(p) 72 %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, mk(T, p, xs)), fill(T, P, xs), mk_slots(T, p, xs)) : {SC.append(Maybe<&2, T>, _, AR.slots(Maybe<&2, T>, mk(T, p, SC.drop(T, xs, P)))) == fill(T, SC.pow2(1n+p), xs) : List<&2, Maybe<&2, T>>} 73 %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, mk(T, p, SC.drop(T, xs, P))), fill(T, P, SC.drop(T, xs, P)), mk_slots(T, p, SC.drop(T, xs, P))) : {SC.append(Maybe<&2, T>, fill(T, P, xs), _) == fill(T, SC.pow2(1n+p), xs) : List<&2, Maybe<&2, T>>} 74 %Equal.sym(Nat, SC.pow2(1n+p), Nat.add(P, P), dbl(p)) : {SC.append(Maybe<&2, T>, fill(T, P, xs), fill(T, P, SC.drop(T, xs, P))) == fill(T, _, xs) : List<&2, Maybe<&2, T>>} 75 Equal.sym(List<&2, Maybe<&2, T>>, fill(T, Nat.add(P, P), xs), SC.append(Maybe<&2, T>, fill(T, P, xs), fill(T, P, SC.drop(T, xs, P))), fill_add(T, P, P, xs)) 76 77 # ---- the layout facts ---- 78 79 def fill_somes(-T: Data, +k: Nat, +xs: List<&2, T>, +h: {Nat.is_le(SC.length(T, xs), k) == True{} : Bool}) -> {LY.somes(T, fill(T, k, xs)) == xs : List<&2, T>}: 80 match k xs: 81 case 0n Nil{}: 82 {==} 83 case 0n Con{x, r}: 84 Empty.absurd({Nil{} == Con{x, r} : List<&2, T>}, L.false_true(h)) 85 case 1n+j Nil{}: 86 fill_somes(T, j, Nil{}, N.zero_le(j)) 87 case 1n+j Con{x, +r}: 88 LL.cons_cong(T, x, LY.somes(T, fill(T, j, r)), r, fill_somes(T, j, r, h)) 89 90 def fill_nones(-T: Data, +k: Nat) -> {LY.nones(T, fill(T, k, Nil{})) == True{} : Bool}: 91 match k: 92 case 0n: 93 {==} 94 case 1n+j: 95 fill_nones(T, j) 96 97 def fill_lay(-T: Data, +k: Nat, +xs: List<&2, T>, +h: {Nat.is_le(SC.length(T, xs), k) == True{} : Bool}) -> {LY.lay(T, fill(T, k, xs), SC.length(T, xs)) == True{} : Bool}: 98 match k xs: 99 case 0n Nil{}: 100 {==} 101 case 0n Con{x, r}: 102 Empty.absurd({LY.lay(T, Nil{}, 1n+SC.length(T, r)) == True{} : Bool}, L.false_true(h)) 103 case 1n+j Nil{}: 104 fill_nones(T, j) 105 case 1n+j Con{x, +r}: 106 fill_lay(T, j, r, h) 107 108 def fill_len(-T: Data, +k: Nat, +xs: List<&2, T>) -> {SC.length(Maybe<&2, T>, fill(T, k, xs)) == k : Nat}: 109 match k xs: 110 case 0n _: 111 {==} 112 case 1n+j Nil{}: 113 N.succ_cong(SC.length(Maybe<&2, T>, fill(T, j, Nil{})), j, fill_len(T, j, Nil{})) 114 case 1n+j Con{x, +r}: 115 N.succ_cong(SC.length(Maybe<&2, T>, fill(T, j, r)), j, fill_len(T, j, r)) 116 117 def fill_upd(-T: Data, +k: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> {SC.update(Maybe<&2, T>, fill(T, k, xs), i, Some{v}) == fill(T, k, SC.update(T, xs, i, v)) : List<&2, Maybe<&2, T>>}: 118 match k xs i: 119 case 0n _ _: 120 {==} 121 case 1n+j Nil{} _: 122 Empty.absurd({SC.update(Maybe<&2, T>, fill(T, 1n+j, Nil{}), i, Some{v}) == fill(T, 1n+j, Nil{}) : List<&2, Maybe<&2, T>>}, N.lt_zero_absurd(i, h)) 123 case 1n+j Con{x, r} 0n: 124 {==} 125 case 1n+j Con{x, +r} 1n+q: 126 LL.cons_cong(Maybe<&2, T>, Some{x}, SC.update(Maybe<&2, T>, fill(T, j, r), q, Some{v}), fill(T, j, SC.update(T, r, q, v)), fill_upd(T, j, r, q, v, h)) 127 128 def fill_snoc(-T: Data, +k: Nat, +xs: List<&2, T>, +v: T, +h: {Nat.is_lt(SC.length(T, xs), k) == True{} : Bool}) -> {SC.update(Maybe<&2, T>, fill(T, k, xs), SC.length(T, xs), Some{v}) == fill(T, k, SC.snoc(T, xs, v)) : List<&2, Maybe<&2, T>>}: 129 match k xs: 130 case 0n _: 131 Empty.absurd({SC.update(Maybe<&2, T>, Nil{}, SC.length(T, xs), Some{v}) == Nil{} : List<&2, Maybe<&2, T>>}, N.lt_zero_absurd(SC.length(T, xs), h)) 132 case 1n+j Nil{}: 133 {==} 134 case 1n+j Con{x, +r}: 135 LL.cons_cong(Maybe<&2, T>, Some{x}, SC.update(Maybe<&2, T>, fill(T, j, r), SC.length(T, r), Some{v}), fill(T, j, SC.snoc(T, r, v)), fill_snoc(T, j, r, v, h)) 136 137 # ---- trees equal to canonical blocks ---- 138 139 def mk_eq(-T: Data, +d: Nat, +u: AR.Tree>, +xs: List<&2, T>, +pu: {AR.perfect(Maybe<&2, T>, d, u) == True{} : Bool}, +e: {AR.slots(Maybe<&2, T>, u) == fill(T, SC.pow2(d), xs) : List<&2, Maybe<&2, T>>}) -> {u == mk(T, d, xs) : AR.Tree>}: 140 AX.tree_ext(Maybe<&2, T>, d, u, mk(T, d, xs), pu, mk_perfect(T, d, xs), Equal.trans(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, u), fill(T, SC.pow2(d), xs), AR.slots(Maybe<&2, T>, mk(T, d, xs)), e, Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, mk(T, d, xs)), fill(T, SC.pow2(d), xs), mk_slots(T, d, xs)))) 141 142 # a slot written below the length 143 def mk_set(-T: Data, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {AR.upd(Maybe<&2, T>, d, mk(T, d, xs), i, Some{v}) == mk(T, d, SC.update(T, xs, i, v)) : AR.Tree>}: 144 +hi = N.lt_le_trans(i, SC.length(T, xs), SC.pow2(d), h, hc) 145 +es = Equal.trans(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, mk(T, d, xs), i, Some{v})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, mk(T, d, xs)), i, Some{v}), fill(T, SC.pow2(d), SC.update(T, xs, i, v)), AR.upd_slots(Maybe<&2, T>, d, mk(T, d, xs), i, Some{v}, hi, mk_perfect(T, d, xs)), Equal.trans(List<&2, Maybe<&2, T>>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, mk(T, d, xs)), i, Some{v}), SC.update(Maybe<&2, T>, fill(T, SC.pow2(d), xs), i, Some{v}), fill(T, SC.pow2(d), SC.update(T, xs, i, v)), Equal.cong(List<&2, Maybe<&2, T>>, List<&2, Maybe<&2, T>>, z => SC.update(Maybe<&2, T>, z, i, Some{v}), AR.slots(Maybe<&2, T>, mk(T, d, xs)), fill(T, SC.pow2(d), xs), mk_slots(T, d, xs)), fill_upd(T, SC.pow2(d), xs, i, v, h))) 146 mk_eq(T, d, AR.upd(Maybe<&2, T>, d, mk(T, d, xs), i, Some{v}), SC.update(T, xs, i, v), AR.upd_perfect(Maybe<&2, T>, d, mk(T, d, xs), i, Some{v}, mk_perfect(T, d, xs)), es) 147 148 # the slot at the length written (a push with room) 149 def mk_push(-T: Data, +d: Nat, +xs: List<&2, T>, +v: T, +h: {Nat.is_lt(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {AR.upd(Maybe<&2, T>, d, mk(T, d, xs), SC.length(T, xs), Some{v}) == mk(T, d, SC.snoc(T, xs, v)) : AR.Tree>}: 150 +es = Equal.trans(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, mk(T, d, xs), SC.length(T, xs), Some{v})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, mk(T, d, xs)), SC.length(T, xs), Some{v}), fill(T, SC.pow2(d), SC.snoc(T, xs, v)), AR.upd_slots(Maybe<&2, T>, d, mk(T, d, xs), SC.length(T, xs), Some{v}, h, mk_perfect(T, d, xs)), Equal.trans(List<&2, Maybe<&2, T>>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, mk(T, d, xs)), SC.length(T, xs), Some{v}), SC.update(Maybe<&2, T>, fill(T, SC.pow2(d), xs), SC.length(T, xs), Some{v}), fill(T, SC.pow2(d), SC.snoc(T, xs, v)), Equal.cong(List<&2, Maybe<&2, T>>, List<&2, Maybe<&2, T>>, z => SC.update(Maybe<&2, T>, z, SC.length(T, xs), Some{v}), AR.slots(Maybe<&2, T>, mk(T, d, xs)), fill(T, SC.pow2(d), xs), mk_slots(T, d, xs)), fill_snoc(T, SC.pow2(d), xs, v, h))) 151 mk_eq(T, d, AR.upd(Maybe<&2, T>, d, mk(T, d, xs), SC.length(T, xs), Some{v}), SC.snoc(T, xs, v), AR.upd_perfect(Maybe<&2, T>, d, mk(T, d, xs), SC.length(T, xs), Some{v}, mk_perfect(T, d, xs)), es) 152 153 def fill_rep(-T: Data, +k: Nat) -> {fill(T, k, Nil{}) == SC.replicate(Maybe<&2, T>, k, None{}) : List<&2, Maybe<&2, T>>}: 154 match k: 155 case 0n: 156 {==} 157 case 1n+j: 158 LL.cons_cong(Maybe<&2, T>, None{}, fill(T, j, Nil{}), SC.replicate(Maybe<&2, T>, j, None{}), fill_rep(T, j)) 159 160 def drop_all(-T: Data, +xs: List<&2, T>, +k: Nat, +h: {Nat.is_le(SC.length(T, xs), k) == True{} : Bool}) -> {SC.drop(T, xs, k) == Nil{} : List<&2, T>}: 161 match xs k: 162 case Nil{} _: 163 {==} 164 case Con{x, r} 0n: 165 Empty.absurd({Con{x, r} == Nil{} : List<&2, T>}, L.false_true(h)) 166 case Con{x, +r} 1n+j: 167 drop_all(T, r, j, h) 168 169 # the doubled block of a full list (old block and an empty half) 170 def mk_grow(-T: Data, +d: Nat, +xs: List<&2, T>, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {AR.TNode{mk(T, d, xs), AR.trep(Maybe<&2, T>, d, None{})} == mk(T, 1n+d, xs) : AR.Tree>}: 171 +e1 = Equal.trans(AR.Tree>, AR.trep(Maybe<&2, T>, d, None{}), mk(T, d, Nil{}), mk(T, d, SC.drop(T, xs, SC.pow2(d))), mk_eq(T, d, AR.trep(Maybe<&2, T>, d, None{}), Nil{}, AR.trep_perfect(Maybe<&2, T>, d, None{}), Equal.trans(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), fill(T, SC.pow2(d), Nil{}), AR.trep_slots(Maybe<&2, T>, d, None{}), Equal.sym(List<&2, Maybe<&2, T>>, fill(T, SC.pow2(d), Nil{}), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), fill_rep(T, SC.pow2(d))))), Equal.cong(List<&2, T>, AR.Tree>, z => mk(T, d, z), Nil{}, SC.drop(T, xs, SC.pow2(d)), Equal.sym(List<&2, T>, SC.drop(T, xs, SC.pow2(d)), Nil{}, drop_all(T, xs, SC.pow2(d), hc)))) 172 Equal.cong(AR.Tree>, AR.Tree>, z => AR.TNode{mk(T, d, xs), z}, AR.trep(Maybe<&2, T>, d, None{}), mk(T, d, SC.drop(T, xs, SC.pow2(d))), e1) 173 174 def mk_empty(-T: Data, +d: Nat) -> {AR.trep(Maybe<&2, T>, d, None{}) == mk(T, d, Nil{}) : AR.Tree>}: 175 mk_eq(T, d, AR.trep(Maybe<&2, T>, d, None{}), Nil{}, AR.trep_perfect(Maybe<&2, T>, d, None{}), Equal.trans(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), fill(T, SC.pow2(d), Nil{}), AR.trep_slots(Maybe<&2, T>, d, None{}), Equal.sym(List<&2, Maybe<&2, T>>, fill(T, SC.pow2(d), Nil{}), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), fill_rep(T, SC.pow2(d)))))