1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../lib/order.bend as O 6 import ../../lib/u32.bend as U 7 import ../../lib/array.bend as AR 8 import ../../../spec/lib/common.bend as SC 9 import ../../../spec/containers/binary_heap.bend as S 10 import ../../../src/containers/binary_heap.bend as H 11 import ../../../src/containers/types/binary_heap.bend as E 12 import ./idx.bend as IX 13 import ./u32idx.bend as UX 14 import ./slots.bend as SL 15 import ./vals.bend as V 16 import ./multiset.bend as M 17 import ./root.bend as RT 18 import ./up.bend as UPS 19 import ./down.bend as DN 20 import ./state.bend as ST 21 22 # pop: the root is taken out, the last element is lifted into the hole at the 23 # root and sifted down. `hole` is the logical block the sift-down works on: 24 # the last slot emptied, the root slot holding the lifted value. 25 26 # ---- small arithmetic the pop needs ---- 27 28 def scale_double(f: Nat, +m: Nat) -> {IX.scale(f, Nat.double(m)) == Nat.double(IX.scale(f, m)) : Nat}: 29 match f: 30 case 0n: 31 {==} 32 case 1n+ +g: 33 scale_double(g, Nat.double(m)) 34 35 def scale_one(d: Nat) -> {IX.scale(d, 1n) == SC.pow2(d) : Nat}: 36 match d: 37 case 0n: 38 {==} 39 case 1n+ +g: 40 Equal.trans(Nat, IX.scale(g, Nat.double(1n)), Nat.double(IX.scale(g, 1n)), Nat.double(SC.pow2(g)), 41 scale_double(g, 1n), 42 Equal.cong(Nat, Nat, z => Nat.double(z), IX.scale(g, 1n), SC.pow2(g), scale_one(g))) 43 44 def half_ge1(k: Nat, +h: {Nat.is_le(2n, k) == True{} : Bool}) -> {Nat.is_le(1n, IX.half(k)) == True{} : Bool}: 45 match k: 46 case 0n: 47 Empty.absurd({Nat.is_le(1n, IX.half(0n)) == True{} : Bool}, L.true_not_false(Nat.is_le(2n, 0n), h, {==})) 48 case 1n+0n: 49 Empty.absurd({Nat.is_le(1n, IX.half(1n)) == True{} : Bool}, L.true_not_false(Nat.is_le(2n, 1n), h, {==})) 50 case 1n+1n+ +r: 51 N.zero_le(IX.half_go(r, False{})) 52 53 # not a child of the root and positive => the parent is positive too 54 def par_pos(j: Nat, +hj: {Nat.is_le(1n, j) == True{} : Bool}, +hkf: {SL.kid_of(j, 0n) == False{} : Bool}) -> {Nat.is_le(1n, IX.par(j)) == True{} : Bool}: 55 match j: 56 case 0n: 57 Empty.absurd({Nat.is_le(1n, IX.par(0n)) == True{} : Bool}, L.true_not_false(Nat.is_le(1n, 0n), hj, {==})) 58 case 1n+0n: 59 Empty.absurd({Nat.is_le(1n, IX.par(1n)) == True{} : Bool}, L.true_not_false(SL.kid_of(1n, 0n), {==}, hkf)) 60 case 1n+1n+0n: 61 Empty.absurd({Nat.is_le(1n, IX.par(2n)) == True{} : Bool}, L.true_not_false(SL.kid_of(2n, 0n), {==}, hkf)) 62 case 1n+1n+1n+ +r: 63 half_ge1(2n+r, N.zero_le(r)) 64 65 # ---- the logical block the sift-down starts from ---- 66 67 def hole(~A: Data, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +last: A) -> List<&2, Maybe<&2, A>>: 68 SC.update(Maybe<&2, A>, ss, 0n, Some{last}) 69 70 def hole_at0(~A: Data, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +last: A, +hlen: {Nat.is_lt(0n, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {SL.slot(~A, hole(~A, ss, m, last), 0n) == Some{last} : Maybe<&2, A>}: 71 SL.slot_same(~A, ss, 0n, Some{last}, hlen) 72 73 def hole_off(~A: Data, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +last: A, +j: Nat, +hj0: {Nat.is_eq(0n, j) == False{} : Bool}) -> {SL.slot(~A, hole(~A, ss, m, last), j) == SL.slot(~A, ss, j) : Maybe<&2, A>}: 74 SL.slot_other(~A, ss, 0n, j, Some{last}, hj0) 75 76 # ---- every pair except the two below the root still holds ---- 77 78 def pop_pair(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +last: A, j: Nat, +hjm: {Nat.is_lt(j, m) == True{} : Bool}, +hkf: {SL.kid_of(j, 0n) == False{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, 1n+m) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, hole(~A, ss, m, last), j) == True{} : Bool}: 79 match j: 80 case 0n: 81 {==} 82 case 1n+ +p: 83 +hpp = par_pos(1n+p, N.zero_le(p), hkf) 84 %Equal.sym(Maybe<&2, A>, SL.slot(~A, hole(~A, ss, m, last), 1n+p), SL.slot(~A, ss, 1n+p), hole_off(~A, ss, m, last, 1n+p, {==})) : {SL.mle(~A, ~cmp, SL.slot(~A, hole(~A, ss, m, last), IX.par(1n+p)), _) == True{} : Bool} 85 %Equal.sym(Maybe<&2, A>, SL.slot(~A, hole(~A, ss, m, last), IX.par(1n+p)), SL.slot(~A, ss, IX.par(1n+p)), hole_off(~A, ss, m, last, IX.par(1n+p), N.is_eq_lt(0n, IX.par(1n+p), N.succ_le_lt(0n, IX.par(1n+p), hpp)))) : {SL.mle(~A, ~cmp, _, SL.slot(~A, ss, 1n+p)) == True{} : Bool} 86 SL.ho_at(~A, ~cmp, ss, 1n+m, 1n+p, hho, N.lt_trans(1n+p, m, 1n+m, hjm, N.lt_succ(m))) 87 88 def pop_skip(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +last: A, +j: Nat, +hjm: {Nat.is_lt(j, m) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, 1n+m) == True{} : Bool}, b: Bool, +eb: {SL.kid_of(j, 0n) == b : Bool}) -> {SL.pair_skip2(~A, ~cmp, hole(~A, ss, m, last), j, 0n) == True{} : Bool}: 89 match b: 90 case True{}: 91 SL.skip2_eq(~A, ~cmp, hole(~A, ss, m, last), j, 0n, eb) 92 case False{}: 93 SL.skip2_ne(~A, ~cmp, hole(~A, ss, m, last), j, 0n, eb, pop_pair(~A, ~cmp, ss, m, last, j, hjm, eb, hho)) 94 95 def pop_exc(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +last: A, k: Nat, +hk: {Nat.is_le(k, m) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, 1n+m) == True{} : Bool}) -> {SL.ho_exc2(~A, ~cmp, hole(~A, ss, m, last), k, 0n) == True{} : Bool}: 96 match k: 97 case 0n: 98 {==} 99 case 1n+ +p: 100 L.and_intro(SL.pair_skip2(~A, ~cmp, hole(~A, ss, m, last), p, 0n), SL.ho_exc2(~A, ~cmp, hole(~A, ss, m, last), p, 0n), 101 pop_skip(~A, ~cmp, ss, m, last, p, N.succ_le_lt(p, m, hk), hho, SL.kid_of(p, 0n), {==}), 102 pop_exc(~A, ~cmp, ss, m, last, p, N.le_trans(p, 1n+p, m, N.le_succ(p), hk), hho)) 103 104 # ---- the slots below m are still occupied ---- 105 106 def pop_some(~A: Data, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +last: A, j: Nat, +hjm: {Nat.is_lt(j, m) == True{} : Bool}, +hlay: {SL.lay(~A, ss, 1n+m) == True{} : Bool}, +hlen: {Nat.is_lt(0n, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {Maybe.is_some(&2, A, SL.slot(~A, hole(~A, ss, m, last), j)) == True{} : Bool}: 107 match j: 108 case 0n: 109 %Equal.sym(Maybe<&2, A>, SL.slot(~A, hole(~A, ss, m, last), 0n), Some{last}, hole_at0(~A, ss, m, last, hlen)) : {Maybe.is_some(&2, A, _) == True{} : Bool} 110 {==} 111 case 1n+ +p: 112 %Equal.sym(Maybe<&2, A>, SL.slot(~A, hole(~A, ss, m, last), 1n+p), SL.slot(~A, ss, 1n+p), hole_off(~A, ss, m, last, 1n+p, {==})) : {Maybe.is_some(&2, A, _) == True{} : Bool} 113 SL.lay_at(~A, ss, 1n+m, 1n+p, hlay, N.lt_trans(1n+p, m, 1n+m, hjm, N.lt_succ(m))) 114 115 def pop_lay(~A: Data, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +last: A, k: Nat, +hk: {Nat.is_le(k, m) == True{} : Bool}, +hlay: {SL.lay(~A, ss, 1n+m) == True{} : Bool}, +hlen: {Nat.is_lt(0n, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {SL.lay(~A, hole(~A, ss, m, last), k) == True{} : Bool}: 116 match k: 117 case 0n: 118 {==} 119 case 1n+ +p: 120 L.and_intro(Maybe.is_some(&2, A, SL.slot(~A, hole(~A, ss, m, last), p)), SL.lay(~A, hole(~A, ss, m, last), p), 121 pop_some(~A, ss, m, last, p, N.succ_le_lt(p, m, hk), hlay, hlen), 122 pop_lay(~A, ss, m, last, p, N.le_trans(p, 1n+p, m, N.le_succ(p), hk), hlay, hlen)) 123 124 # ---- the old root is still below the two slots the sift-down compares ---- 125 126 def pop_kid(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +m: Nat, +root: A, +c: Nat, +hm: {Nat.is_lt(0n, m) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, 1n+m) == True{} : Bool}, +hlay: {SL.lay(~A, ss, 1n+m) == True{} : Bool}, +h0: {SL.slot(~A, ss, 0n) == Some{root} : Maybe<&2, A>}, b: Bool, +eb: {Nat.is_lt(c, m) == b : Bool}) -> {SL.kid_le(~A, ~cmp, ss, m, 0n, c) == True{} : Bool}: 127 match b: 128 case True{}: 129 SL.kid_le_in(~A, ~cmp, ss, m, 0n, c, eb, 130 %Equal.sym(Maybe<&2, A>, SL.slot(~A, ss, 0n), Some{root}, h0) : {SL.mle(~A, ~cmp, _, SL.slot(~A, ss, c)) == True{} : Bool} 131 RT.root_le(~A, ~cmp, ~o, ss, 1n+m, c, root, c, N.lt_trans(c, m, 1n+m, eb, N.lt_succ(m)), N.le_refl(c), hho, hlay, h0)) 132 case False{}: 133 SL.kid_le_out(~A, ~cmp, ss, m, 0n, c, eb) 134 135 def pop_kids(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +m: Nat, +root: A, +hm: {Nat.is_lt(0n, m) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, 1n+m) == True{} : Bool}, +hlay: {SL.lay(~A, ss, 1n+m) == True{} : Bool}, +h0: {SL.slot(~A, ss, 0n) == Some{root} : Maybe<&2, A>}) -> {SL.kids_le(~A, ~cmp, ss, m, IX.par(0n), 0n) == True{} : Bool}: 136 L.and_intro(SL.kid_le(~A, ~cmp, ss, m, 0n, IX.kidl(0n)), SL.kid_le(~A, ~cmp, ss, m, 0n, IX.kidr(0n)), 137 pop_kid(~A, ~cmp, ~o, ss, m, root, IX.kidl(0n), hm, hho, hlay, h0, Nat.is_lt(IX.kidl(0n), m), {==}), 138 pop_kid(~A, ~cmp, ~o, ss, m, root, IX.kidr(0n), hm, hho, hlay, h0, Nat.is_lt(IX.kidr(0n), m), {==})) 139 140 # ---- the multiset loses exactly the root ---- 141 142 def pop_ms(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +m: Nat, +root: A, +last: A, +hm: {Nat.is_lt(0n, m) == True{} : Bool}, +h0: {SL.slot(~A, ss, 0n) == Some{root} : Maybe<&2, A>}, +hlast: {SL.slot(~A, ss, m) == Some{last} : Maybe<&2, A>}) -> {V.msort(~A, ~cmp, V.vals(~A, ss, 1n+m)) == S.ins(~A, ~cmp, root, V.msort(~A, ~cmp, V.vals(~A, hole(~A, ss, m, last), m))) : List<&2, A>}: 143 Equal.trans(List<&2, A>, V.msort(~A, ~cmp, V.vals(~A, ss, 1n+m)), S.ins(~A, ~cmp, last, V.msort(~A, ~cmp, V.vals(~A, ss, m))), S.ins(~A, ~cmp, root, V.msort(~A, ~cmp, V.vals(~A, hole(~A, ss, m, last), m))), 144 Equal.cong(Maybe<&2, A>, List<&2, A>, ms => V.msort(~A, ~cmp, V.cons_slot(~A, ms, V.vals(~A, ss, m))), SL.slot(~A, ss, m), Some{last}, hlast), 145 Equal.sym(List<&2, A>, S.ins(~A, ~cmp, root, V.msort(~A, ~cmp, V.vals(~A, hole(~A, ss, m, last), m))), S.ins(~A, ~cmp, last, V.msort(~A, ~cmp, V.vals(~A, ss, m))), 146 V.ins_set(~A, ~cmp, ~o, ss, m, 0n, root, last, hm, h0, Nat.is_eq(0n, N.pred(m)), {==}))) 147 148 # ---- the old root is still the minimum of what is left ---- 149 150 def pop_low_at(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +m: Nat, +root: A, +last: A, j: Nat, +hjm: {Nat.is_lt(j, m) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, 1n+m) == True{} : Bool}, +hlay: {SL.lay(~A, ss, 1n+m) == True{} : Bool}, +h0: {SL.slot(~A, ss, 0n) == Some{root} : Maybe<&2, A>}, +hlast: {SL.slot(~A, ss, m) == Some{last} : Maybe<&2, A>}, +hlen: {Nat.is_lt(0n, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {SL.mle(~A, ~cmp, Some{root}, SL.slot(~A, hole(~A, ss, m, last), j)) == True{} : Bool}: 151 match j: 152 case 0n: 153 %Equal.sym(Maybe<&2, A>, SL.slot(~A, hole(~A, ss, m, last), 0n), Some{last}, hole_at0(~A, ss, m, last, hlen)) : {SL.mle(~A, ~cmp, Some{root}, _) == True{} : Bool} 154 %hlast : {SL.mle(~A, ~cmp, Some{root}, _) == True{} : Bool} 155 RT.root_le(~A, ~cmp, ~o, ss, 1n+m, m, root, m, N.lt_succ(m), N.le_refl(m), hho, hlay, h0) 156 case 1n+ +p: 157 %Equal.sym(Maybe<&2, A>, SL.slot(~A, hole(~A, ss, m, last), 1n+p), SL.slot(~A, ss, 1n+p), hole_off(~A, ss, m, last, 1n+p, {==})) : {SL.mle(~A, ~cmp, Some{root}, _) == True{} : Bool} 158 RT.root_le(~A, ~cmp, ~o, ss, 1n+m, 1n+p, root, 1n+p, N.lt_trans(1n+p, m, 1n+m, hjm, N.lt_succ(m)), N.le_refl(1n+p), hho, hlay, h0) 159 160 def pop_low(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +m: Nat, +root: A, +last: A, k: Nat, +hk: {Nat.is_le(k, m) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, 1n+m) == True{} : Bool}, +hlay: {SL.lay(~A, ss, 1n+m) == True{} : Bool}, +h0: {SL.slot(~A, ss, 0n) == Some{root} : Maybe<&2, A>}, +hlast: {SL.slot(~A, ss, m) == Some{last} : Maybe<&2, A>}, +hlen: {Nat.is_lt(0n, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {RT.low_all(~A, ~cmp, hole(~A, ss, m, last), k, root) == True{} : Bool}: 161 match k: 162 case 0n: 163 {==} 164 case 1n+ +p: 165 L.and_intro(SL.mle(~A, ~cmp, Some{root}, SL.slot(~A, hole(~A, ss, m, last), p)), RT.low_all(~A, ~cmp, hole(~A, ss, m, last), p, root), 166 pop_low_at(~A, ~cmp, ~o, ss, m, root, last, p, N.succ_le_lt(p, m, hk), hho, hlay, h0, hlast, hlen), 167 pop_low(~A, ~cmp, ~o, ss, m, root, last, p, N.le_trans(p, 1n+p, m, N.le_succ(p), hk), hho, hlay, h0, hlast, hlen)) 168 169 # The observation of a pop: the multiset of the heap is the old root followed 170 # by the multiset the sift-down is given as its target. 171 def pop_split(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +m: Nat, +root: A, +last: A, +hm: {Nat.is_lt(0n, m) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, 1n+m) == True{} : Bool}, +hlay: {SL.lay(~A, ss, 1n+m) == True{} : Bool}, +h0: {SL.slot(~A, ss, 0n) == Some{root} : Maybe<&2, A>}, +hlast: {SL.slot(~A, ss, m) == Some{last} : Maybe<&2, A>}, +hlen: {Nat.is_lt(0n, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {V.msort(~A, ~cmp, V.vals(~A, ss, 1n+m)) == Con{root, V.msort(~A, ~cmp, V.vals(~A, hole(~A, ss, m, last), m))} : List<&2, A>}: 172 Equal.trans(List<&2, A>, V.msort(~A, ~cmp, V.vals(~A, ss, 1n+m)), S.ins(~A, ~cmp, root, V.msort(~A, ~cmp, V.vals(~A, hole(~A, ss, m, last), m))), Con{root, V.msort(~A, ~cmp, V.vals(~A, hole(~A, ss, m, last), m))}, 173 pop_ms(~A, ~cmp, ~o, ss, m, root, last, hm, h0, hlast), 174 RT.front(~A, ~cmp, ~o, hole(~A, ss, m, last), m, root, pop_low(~A, ~cmp, ~o, ss, m, root, last, m, N.le_refl(m), hho, hlay, h0, hlast, hlen))) 175 176 # ---- what the implementation computes ---- 177 178 def round_lt(+m: Nat, +d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hm: {Nat.is_lt(m, SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(U32.from_nat(m)), SC.pow2(d)) == True{} : Bool}: 179 L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, UX.nat_round(m, d, N.lt_le(d, 32n, hd), hm)), hm) 180 181 def round_nth(~A: Data, +t: AR.Tree>, +m: Nat, +d: Nat, +v: A, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hm: {Nat.is_lt(m, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), m) == Some{v} : Maybe<&2, A>}) -> {SC.nth(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), U32.to_nat(U32.from_nat(m))) == Some{Some{v}} : Maybe<&2, Maybe<&2, A>>}: 182 L.subst(Nat, z => {SC.nth(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), z) == Some{Some{v}} : Maybe<&2, Maybe<&2, A>>}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, UX.nat_round(m, d, N.lt_le(d, 32n, hd), hm)), 183 V.nth_of_slot(~A, AR.slots(Maybe<&2, A>, t), m, v, hv)) 184 185 # the last element is read, not cleared 186 def get_last(~A: Data, +d: Nat, +t: AR.Tree>, +m: Nat, +last: A, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hm: {Nat.is_lt(m, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hlast: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), m) == Some{last} : Maybe<&2, A>}) -> {Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(m)) == (AR.thaw(Maybe<&2, A>, t), Some{last}) : Array> & Maybe<&2, A>}: 187 AR.get(Maybe<&2, A>, d, t, U32.from_nat(m), Some{last}, hd, round_lt(m, d, hd, hm), round_nth(~A, t, m, d, last, hd, hm, pf, hlast), pf) 188 189 def get_root(~A: Data, +d: Nat, +t: AR.Tree>, +root: A, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +h0: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>}) -> {Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), 0) == (AR.thaw(Maybe<&2, A>, t), Some{root}) : Array> & Maybe<&2, A>}: 190 AR.get(Maybe<&2, A>, d, t, 0, Some{root}, hd, N.succ_le_lt(0n, SC.pow2(d), N.pow2_pos(d)), V.nth_of_slot(~A, AR.slots(Maybe<&2, A>, t), 0n, root, h0), pf) 191 192 # The pop of a nonempty heap, reduced to the move that follows reading the 193 # last element. Each step is an explicit substitution rather than a rewrite 194 # annotation: the goal is normalised between steps, so naming the redex is 195 # the only robust way to transport it. 196 def pop_to_move(~A: Data, ~cmp: A -> A -> Cmp, +depth: Nat, +m: Nat, +t: AR.Tree>, +root: A, +last: A, +hd: {Nat.is_le(depth, 31n) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, depth, t) == True{} : Bool}, +hs: {Nat.is_le(1n+m, SC.pow2(depth)) == True{} : Bool}, +h0: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>}, +hlast: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), m) == Some{last} : Maybe<&2, A>}) -> {H.pop(~A, ~cmp, ST.real(~A, ST.Sh{1n+m, depth, t})) == H.pop_move(~A, ~cmp, m, U32.from_nat(m), depth, U.pow2u(depth), root, last, AR.thaw(Maybe<&2, A>, t), U32.is_eq(U32.from_nat(m), 0)) : H.Heap & Result<&2, &2, E.Error, A>}: 197 +hd32 = ST.depth_lt32(depth, hd) 198 +hmp = N.succ_le_lt(m, SC.pow2(depth), hs) 199 +hsp = N.le_lt_trans(1n+m, SC.pow2(depth), SC.pow2(1n+depth), hs, N.pow2_lt_succ(depth)) 200 L.subst(Array> & Maybe<&2, A>, r => {H.pop(~A, ~cmp, ST.real(~A, ST.Sh{1n+m, depth, t})) == H.pop_last(~A, ~cmp, m, U32.from_nat(m), depth, U.pow2u(depth), root, r) : H.Heap & Result<&2, &2, E.Error, A>}, 201 Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(m)), (AR.thaw(Maybe<&2, A>, t), Some{last}), 202 get_last(~A, depth, t, m, last, hd32, hmp, pf, hlast), 203 L.subst(Nat, k => {H.pop(~A, ~cmp, ST.real(~A, ST.Sh{1n+m, depth, t})) == H.pop_last(~A, ~cmp, k, U32.from_nat(m), depth, U.pow2u(depth), root, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(m))) : H.Heap & Result<&2, &2, E.Error, A>}, 204 Nat.sub(1n+m, 1n), m, N.sub_zero(m), 205 L.subst(U32, i => {H.pop(~A, ~cmp, ST.real(~A, ST.Sh{1n+m, depth, t})) == H.pop_last(~A, ~cmp, Nat.sub(1n+m, 1n), i, depth, U.pow2u(depth), root, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), i)) : H.Heap & Result<&2, &2, E.Error, A>}, 206 U32.sub(U32.from_nat(1n+m), 1), U32.from_nat(m), 207 Equal.trans(U32, U32.sub(U32.from_nat(1n+m), 1), U32.from_nat(Nat.sub(1n+m, 1n)), U32.from_nat(m), UX.sub_one(1n+m, 1n+depth, hd, hsp, N.zero_le(m)), Equal.cong(Nat, U32, z => U32.from_nat(z), Nat.sub(1n+m, 1n), m, N.sub_zero(m))), 208 L.subst(Array> & Maybe<&2, A>, r => {H.pop(~A, ~cmp, ST.real(~A, ST.Sh{1n+m, depth, t})) == H.pop_root(~A, ~cmp, 1n+m, U32.from_nat(1n+m), depth, U.pow2u(depth), r) : H.Heap & Result<&2, &2, E.Error, A>}, 209 Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), 0), (AR.thaw(Maybe<&2, A>, t), Some{root}), 210 get_root(~A, depth, t, root, hd32, pf, h0), 211 L.subst(Bool, b => {H.pop(~A, ~cmp, ST.real(~A, ST.Sh{1n+m, depth, t})) == H.pop_go(~A, ~cmp, 1n+m, U32.from_nat(1n+m), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), b) : H.Heap & Result<&2, &2, E.Error, A>}, 212 U32.is_eq(U32.from_nat(1n+m), U32.from_nat(0n)), Nat.is_eq(1n+m, 0n), 213 UX.eq_bridge(1n+m, 0n, 1n+depth, hd, hsp, N.lt_le_trans(0n, SC.pow2(depth), SC.pow2(1n+depth), N.succ_le_lt(0n, SC.pow2(depth), N.pow2_pos(depth)), N.lt_le(SC.pow2(depth), SC.pow2(1n+depth), N.pow2_lt_succ(depth)))), 214 {==}))))) 215 216 # ---- the sift-down that follows the swap ---- 217 218 def pop_sift(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +depth: Nat, +m: Nat, +t: AR.Tree>, +root: A, +last: A, +hd: {Nat.is_le(depth, 31n) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, depth, t) == True{} : Bool}, +hs: {Nat.is_le(1n+m, SC.pow2(depth)) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), 1n+m) == True{} : Bool}, +hlay: {SL.lay(~A, AR.slots(Maybe<&2, A>, t), 1n+m) == True{} : Bool}, +h0: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>}, +hlast: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), m) == Some{last} : Maybe<&2, A>}, +hm: {Nat.is_lt(0n, m) == True{} : Bool}) -> DN.SiftDownOK(~A, ~cmp, depth, m, V.msort(~A, ~cmp, V.vals(~A, hole(~A, AR.slots(Maybe<&2, A>, t), m, last), m)), depth, t, 0n, last): 219 +ss = AR.slots(Maybe<&2, A>, t) 220 +hmp = N.succ_le_lt(m, SC.pow2(depth), hs) 221 +hlen = N.lt_le_trans(0n, m, SC.length(Maybe<&2, A>, ss), hm, N.lt_le(m, SC.length(Maybe<&2, A>, ss), L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, SC.pow2(depth), SC.length(Maybe<&2, A>, ss), Equal.sym(Nat, SC.length(Maybe<&2, A>, ss), SC.pow2(depth), AR.slots_length(Maybe<&2, A>, depth, t, pf)), hmp))) 222 DN.sift_down_ok(~A, ~cmp, ~o, depth, depth, m, V.msort(~A, ~cmp, V.vals(~A, hole(~A, ss, m, last), m)), t, 0n, last, 223 ST.depth_lt32(depth, hd), 224 N.succ_le_lt(0n, SC.pow2(depth), N.pow2_pos(depth)), 225 hm, 226 N.lt_le(m, SC.pow2(depth), hmp), 227 L.subst(Nat, z => {Nat.is_le(m, z) == True{} : Bool}, SC.pow2(depth), IX.scale(depth, 1n), Equal.sym(Nat, IX.scale(depth, 1n), SC.pow2(depth), scale_one(depth)), N.lt_le(m, SC.pow2(depth), hmp)), 228 pf, 229 pop_exc(~A, ~cmp, ss, m, last, m, N.le_refl(m), hho), 230 {==}, 231 pop_kids(~A, ~cmp, ~o, ss, m, root, hm, hho, hlay, h0), 232 pop_lay(~A, ss, m, last, m, N.le_refl(m), hlay, hlen), 233 {==}) 234 235 # ---- pop, as a step on shadows ---- 236 237 def PopRes(~A: Data, ~cmp: A -> A -> Cmp, sh: ST.Shadow) -> Type: 238 Sigma<&1, &1, ST.Shadow, sh2 => Sigma<&1, &1, Result<&2, &2, E.Error, A>, r => {H.pop(~A, ~cmp, ST.real(~A, sh)) == (ST.real(~A, sh2), r) : H.Heap & Result<&2, &2, E.Error, A>} & ({ST.good(~A, ~cmp, sh2) == True{} : Bool} & ({(ST.model(~A, ~cmp, sh2), E.OItem{r}) == S.pop(A, ST.model(~A, ~cmp, sh)) : List<&2, A> & E.Obs} & {ST.sh_depth(~A, sh2) == ST.sh_depth(~A, sh) : Nat}))>> 239 240 def pop_from(~A: Data, ~cmp: A -> A -> Cmp, +depth: Nat, +m: Nat, +t: AR.Tree>, +root: A, +last: A, +tgt: List<&2, A>, +hd: {Nat.is_le(depth, 31n) == True{} : Bool}, +hs: {Nat.is_le(1n+m, SC.pow2(depth)) == True{} : Bool}, +eq0: {H.pop(~A, ~cmp, ST.real(~A, ST.Sh{1n+m, depth, t})) == H.pop_move(~A, ~cmp, m, U32.from_nat(m), depth, U.pow2u(depth), root, last, AR.thaw(Maybe<&2, A>, t), False{}) : H.Heap & Result<&2, &2, E.Error, A>}, +hsplit: {ST.model(~A, ~cmp, ST.Sh{1n+m, depth, t}) == Con{root, tgt} : List<&2, A>}, r: DN.SiftDownOK(~A, ~cmp, depth, m, tgt, depth, t, 0n, last)) -> PopRes(~A, ~cmp, ST.Sh{1n+m, depth, t}): 241 match r: 242 case Tuple{+t3, Tuple{esift, Tuple{pf3, Tuple{hho3, Tuple{hlay3, hms3}}}}}: 243 (ST.Sh{m, depth, t3}, 244 (Done{root}, 245 (Equal.trans(H.Heap & Result<&2, &2, E.Error, A>, H.pop(~A, ~cmp, ST.real(~A, ST.Sh{1n+m, depth, t})), H.pop_move(~A, ~cmp, m, U32.from_nat(m), depth, U.pow2u(depth), root, last, AR.thaw(Maybe<&2, A>, t), False{}), (ST.real(~A, ST.Sh{m, depth, t3}), Done{root}), eq0, 246 Equal.cong(Array>, H.Heap & Result<&2, &2, E.Error, A>, a => (H.BH{m, U32.from_nat(m), depth, U.pow2u(depth), a}, Done{root}), H.sift_down(~A, ~cmp, depth, U32.from_nat(m), U32.from_nat(0n), last, AR.thaw(Maybe<&2, A>, t)), AR.thaw(Maybe<&2, A>, t3), esift)), 247 (ST.good_intro(~A, ~cmp, m, depth, t3, hd, pf3, hlay3, hho3, N.le_trans(m, 1n+m, SC.pow2(depth), N.le_succ(m), hs)), 248 (%Equal.sym(List<&2, A>, ST.model(~A, ~cmp, ST.Sh{1n+m, depth, t}), Con{root, tgt}, hsplit) : {(ST.model(~A, ~cmp, ST.Sh{m, depth, t3}), E.OItem{Done{root}}) == S.pop(A, _) : List<&2, A> & E.Obs} 249 Equal.cong(List<&2, A>, List<&2, A> & E.Obs, zs => (zs, E.OItem{Done{root}}), ST.model(~A, ~cmp, ST.Sh{m, depth, t3}), tgt, hms3), 250 {==}))))) 251 252 def pop_nonempty(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +depth: Nat, m: Nat, +t: AR.Tree>, +root: A, +last: A, +g: {ST.good(~A, ~cmp, ST.Sh{1n+m, depth, t}) == True{} : Bool}, +h0: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>}, +hlast: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), m) == Some{last} : Maybe<&2, A>}) -> PopRes(~A, ~cmp, ST.Sh{1n+m, depth, t}): 253 match m: 254 case 0n: 255 (ST.Sh{0n, depth, t}, 256 (Done{root}, 257 (pop_to_move(~A, ~cmp, depth, 0n, t, root, last, ST.g_depth(~A, ~cmp, 1n, depth, t, g), ST.g_perfect(~A, ~cmp, 1n, depth, t, g), ST.g_size(~A, ~cmp, 1n, depth, t, g), h0, hlast), 258 (ST.good_intro(~A, ~cmp, 0n, depth, t, ST.g_depth(~A, ~cmp, 1n, depth, t, g), ST.g_perfect(~A, ~cmp, 1n, depth, t, g), {==}, {==}, N.zero_le(SC.pow2(depth))), 259 (%Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n), Some{root}, h0) : {(Nil{}, E.OItem{Done{root}}) == S.pop(A, V.msort(~A, ~cmp, V.cons_slot(~A, _, Nil{}))) : List<&2, A> & E.Obs} 260 {==}, 261 {==}))))) 262 case 1n+ +k: 263 +hd = ST.g_depth(~A, ~cmp, 2n+k, depth, t, g) 264 +pf = ST.g_perfect(~A, ~cmp, 2n+k, depth, t, g) 265 +hs = ST.g_size(~A, ~cmp, 2n+k, depth, t, g) 266 +hho = ST.g_ho(~A, ~cmp, 2n+k, depth, t, g) 267 +hlay = ST.g_lay(~A, ~cmp, 2n+k, depth, t, g) 268 +ss = AR.slots(Maybe<&2, A>, t) 269 +hmp = N.succ_le_lt(1n+k, SC.pow2(depth), hs) 270 +hlen = N.lt_le_trans(0n, 1n+k, SC.length(Maybe<&2, A>, ss), {==}, N.lt_le(1n+k, SC.length(Maybe<&2, A>, ss), L.subst(Nat, z => {Nat.is_lt(1n+k, z) == True{} : Bool}, SC.pow2(depth), SC.length(Maybe<&2, A>, ss), Equal.sym(Nat, SC.length(Maybe<&2, A>, ss), SC.pow2(depth), AR.slots_length(Maybe<&2, A>, depth, t, pf)), hmp))) 271 +hsp = N.le_lt_trans(2n+k, SC.pow2(depth), SC.pow2(1n+depth), hs, N.pow2_lt_succ(depth)) 272 pop_from(~A, ~cmp, depth, 1n+k, t, root, last, V.msort(~A, ~cmp, V.vals(~A, hole(~A, ss, 1n+k, last), 1n+k)), hd, hs, 273 L.subst(Bool, bb => {H.pop(~A, ~cmp, ST.real(~A, ST.Sh{2n+k, depth, t})) == H.pop_move(~A, ~cmp, 1n+k, U32.from_nat(1n+k), depth, U.pow2u(depth), root, last, AR.thaw(Maybe<&2, A>, t), bb) : H.Heap & Result<&2, &2, E.Error, A>}, 274 U32.is_eq(U32.from_nat(1n+k), U32.from_nat(0n)), False{}, 275 UX.eq_bridge(1n+k, 0n, 1n+depth, hd, N.lt_trans(1n+k, 2n+k, SC.pow2(1n+depth), N.lt_succ(1n+k), hsp), N.lt_le_trans(0n, SC.pow2(depth), SC.pow2(1n+depth), N.succ_le_lt(0n, SC.pow2(depth), N.pow2_pos(depth)), N.lt_le(SC.pow2(depth), SC.pow2(1n+depth), N.pow2_lt_succ(depth)))), 276 pop_to_move(~A, ~cmp, depth, 1n+k, t, root, last, hd, pf, hs, h0, hlast)), 277 pop_split(~A, ~cmp, ~o, ss, 1n+k, root, last, {==}, hho, hlay, h0, hlast, hlen), 278 pop_sift(~A, ~cmp, ~o, depth, 1n+k, t, root, last, hd, pf, hs, hho, hlay, h0, hlast, {==})) 279 280 def pop_with_last(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +depth: Nat, +m: Nat, +t: AR.Tree>, +root: A, +g: {ST.good(~A, ~cmp, ST.Sh{1n+m, depth, t}) == True{} : Bool}, +h0: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>}, sig: Sigma<&1, &1, A, v => {SL.slot(~A, AR.slots(Maybe<&2, A>, t), m) == Some{v} : Maybe<&2, A>}>) -> PopRes(~A, ~cmp, ST.Sh{1n+m, depth, t}): 281 match sig: 282 case Tuple{+last, +hlast}: 283 pop_nonempty(~A, ~cmp, ~o, depth, m, t, root, last, g, h0, hlast) 284 285 def pop_with_root(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +depth: Nat, +m: Nat, +t: AR.Tree>, +g: {ST.good(~A, ~cmp, ST.Sh{1n+m, depth, t}) == True{} : Bool}, sig: Sigma<&1, &1, A, v => {SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n) == Some{v} : Maybe<&2, A>}>) -> PopRes(~A, ~cmp, ST.Sh{1n+m, depth, t}): 286 match sig: 287 case Tuple{+root, +h0}: 288 pop_with_last(~A, ~cmp, ~o, depth, m, t, root, g, h0, 289 SL.slot_some(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), m), SL.lay_at(~A, AR.slots(Maybe<&2, A>, t), 1n+m, m, ST.g_lay(~A, ~cmp, 1n+m, depth, t, g), N.lt_succ(m)))) 290 291 def pop_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +size: Nat, +depth: Nat, +t: AR.Tree>, +g: {ST.good(~A, ~cmp, ST.Sh{size, depth, t}) == True{} : Bool}) -> PopRes(~A, ~cmp, ST.Sh{size, depth, t}): 292 match size: 293 case 0n: 294 (ST.Sh{0n, depth, t}, (Fail{E.EmptyHeap{}}, ({==}, (g, ({==}, {==}))))) 295 case 1n+ +m: 296 pop_with_root(~A, ~cmp, ~o, depth, m, t, g, 297 SL.slot_some(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n), SL.lay_at(~A, AR.slots(Maybe<&2, A>, t), 1n+m, 0n, ST.g_lay(~A, ~cmp, 1n+m, depth, t, g), N.succ_le_lt(0n, 1n+m, N.zero_le(m)))))