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 ./root.bend as RT 17 import ./down.bend as DN 18 import ./state.bend as ST 19 import ./pop.bend as PO 20 21 # to_sorted_list drains a COPY of the block: every iteration is exactly the 22 # pop of the copy, so the lemmas of pop.bend carry the whole induction. The 23 # heap itself is returned unchanged (the copy is what is drained). 24 25 # One drain iteration: the root comes out and the last element is sifted down 26 # over the copy -- the same reduction pop performs, on the copy. 27 def drain_unfold(~A: Data, ~cmp: A -> A -> Cmp, +depth: Nat, +m: Nat, +f: 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>}, +hm: {Nat.is_lt(0n, m) == True{} : Bool}) -> {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_probe(~A, U32.from_nat(1n+m), AR.thaw(Maybe<&2, A>, t))) == Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(m), H.sift_down(~A, ~cmp, depth, U32.from_nat(m), U32.from_nat(0n), last, AR.thaw(Maybe<&2, A>, t))))} : List<&2, A>}: 28 +hd32 = ST.depth_lt32(depth, hd) 29 +hmp = N.succ_le_lt(m, SC.pow2(depth), hs) 30 +hsp = N.le_lt_trans(1n+m, SC.pow2(depth), SC.pow2(1n+depth), hs, N.pow2_lt_succ(depth)) 31 +hzp = 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))) 32 %Equal.sym(Bool, U32.is_eq(U32.from_nat(1n+m), U32.from_nat(0n)), Nat.is_eq(1n+m, 0n), UX.eq_bridge(1n+m, 0n, 1n+depth, hd, hsp, hzp)) : {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_take_go(~A, U32.from_nat(1n+m), AR.thaw(Maybe<&2, A>, t), _)) == Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(m), H.sift_down(~A, ~cmp, depth, U32.from_nat(m), U32.from_nat(0n), last, AR.thaw(Maybe<&2, A>, t))))} : List<&2, A>} 33 %Equal.sym(U32, U32.sub(U32.from_nat(1n+m), 1), U32.from_nat(m), 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)))) : {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_take(~A, _, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), 0))) == Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(m), H.sift_down(~A, ~cmp, depth, U32.from_nat(m), U32.from_nat(0n), last, AR.thaw(Maybe<&2, A>, t))))} : List<&2, A>} 34 %Equal.sym(Array> & Maybe<&2, A>, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), 0), (AR.thaw(Maybe<&2, A>, t), Some{root}), PO.get_root(~A, depth, t, root, hd32, pf, h0)) : {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_take(~A, U32.from_nat(m), _)) == Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(m), H.sift_down(~A, ~cmp, depth, U32.from_nat(m), U32.from_nat(0n), last, AR.thaw(Maybe<&2, A>, t))))} : List<&2, A>} 35 %Equal.sym(Array> & 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}), PO.get_last(~A, depth, t, m, last, hd32, hmp, pf, hlast)) : {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_last(~A, root, U32.from_nat(m), U32.is_eq(U32.from_nat(m), 0), _)) == Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(m), H.sift_down(~A, ~cmp, depth, U32.from_nat(m), U32.from_nat(0n), last, AR.thaw(Maybe<&2, A>, t))))} : List<&2, A>} 36 %Equal.sym(Bool, U32.is_eq(U32.from_nat(m), U32.from_nat(0n)), Nat.is_eq(m, 0n), UX.eq_bridge(m, 0n, 1n+depth, hd, N.lt_trans(m, 1n+m, SC.pow2(1n+depth), N.lt_succ(m), hsp), hzp)) : {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_mb(~A, AR.thaw(Maybe<&2, A>, t), root, U32.from_nat(m), Some{last}, _)) == Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(m), H.sift_down(~A, ~cmp, depth, U32.from_nat(m), U32.from_nat(0n), last, AR.thaw(Maybe<&2, A>, t))))} : List<&2, A>} 37 %Equal.sym(Bool, Nat.is_eq(m, 0n), False{}, SL.ne_sym(m, 0n, N.is_eq_lt(0n, m, hm))) : {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_mb(~A, AR.thaw(Maybe<&2, A>, t), root, U32.from_nat(m), Some{last}, _)) == Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(m), H.sift_down(~A, ~cmp, depth, U32.from_nat(m), U32.from_nat(0n), last, AR.thaw(Maybe<&2, A>, t))))} : List<&2, A>} 38 {==} 39 40 # The last element of the copy: the drain stops with it. 41 def drain_one(~A: Data, ~cmp: A -> A -> Cmp, +depth: Nat, +f: 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, 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), 0n) == Some{last} : Maybe<&2, A>}) -> {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_probe(~A, U32.from_nat(1n), AR.thaw(Maybe<&2, A>, t))) == Con{root, Nil{}} : List<&2, A>}: 42 +hd32 = ST.depth_lt32(depth, hd) 43 +hmp = N.succ_le_lt(0n, SC.pow2(depth), hs) 44 +hsp = N.le_lt_trans(1n, SC.pow2(depth), SC.pow2(1n+depth), hs, N.pow2_lt_succ(depth)) 45 +hzp = 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))) 46 %Equal.sym(Bool, U32.is_eq(U32.from_nat(1n), U32.from_nat(0n)), Nat.is_eq(1n, 0n), UX.eq_bridge(1n, 0n, 1n+depth, hd, hsp, hzp)) : {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_take_go(~A, U32.from_nat(1n), AR.thaw(Maybe<&2, A>, t), _)) == Con{root, Nil{}} : List<&2, A>} 47 %Equal.sym(U32, U32.sub(U32.from_nat(1n), 1), U32.from_nat(0n), Equal.trans(U32, U32.sub(U32.from_nat(1n), 1), U32.from_nat(Nat.sub(1n, 1n)), U32.from_nat(0n), UX.sub_one(1n, 1n+depth, hd, hsp, N.zero_le(0n)), Equal.cong(Nat, U32, z => U32.from_nat(z), Nat.sub(1n, 1n), 0n, N.sub_zero(0n)))) : {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_take(~A, _, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), 0))) == Con{root, Nil{}} : List<&2, A>} 48 %Equal.sym(Array> & Maybe<&2, A>, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), 0), (AR.thaw(Maybe<&2, A>, t), Some{root}), PO.get_root(~A, depth, t, root, hd32, pf, h0)) : {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_take(~A, U32.from_nat(0n), _)) == Con{root, Nil{}} : List<&2, A>} 49 %Equal.sym(Array> & Maybe<&2, A>, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(0n)), (AR.thaw(Maybe<&2, A>, t), Some{last}), PO.get_last(~A, depth, t, 0n, last, hd32, hmp, pf, hlast)) : {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_last(~A, root, U32.from_nat(0n), U32.is_eq(U32.from_nat(0n), 0), _)) == Con{root, Nil{}} : List<&2, A>} 50 %Equal.sym(Bool, U32.is_eq(U32.from_nat(0n), U32.from_nat(0n)), Nat.is_eq(0n, 0n), UX.eq_bridge(0n, 0n, 1n+depth, hd, hzp, hzp)) : {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_mb(~A, AR.thaw(Maybe<&2, A>, t), root, U32.from_nat(0n), Some{last}, _)) == Con{root, Nil{}} : List<&2, A>} 51 {==} 52 53 # The recursive call the drain makes, as a (linear) function argument: Bend 54 # has no mutual recursion, so the induction hands its own instance down. 55 def DrainRec(~A: Data, ~cmp: A -> A -> Cmp, f: Nat, depth: Nat, m: Nat) -> Type: 56 @+t3: AR.Tree> -> @+g3: {ST.good(~A, ~cmp, ST.Sh{m, depth, t3}) == True{} : Bool} -> {H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(m), AR.thaw(Maybe<&2, A>, t3))) == ST.model(~A, ~cmp, ST.Sh{m, depth, t3}) : List<&2, A>} 57 58 def drain_move(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +depth: Nat, +f: Nat, +k: Nat, +t: AR.Tree>, +root: A, +last: A, +g: {ST.good(~A, ~cmp, ST.Sh{2n+k, 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), 1n+k) == Some{last} : Maybe<&2, A>}, rec: DrainRec(~A, ~cmp, f, depth, 1n+k), r: DN.SiftDownOK(~A, ~cmp, depth, 1n+k, V.msort(~A, ~cmp, V.vals(~A, PO.hole(~A, AR.slots(Maybe<&2, A>, t), 1n+k, last), 1n+k)), depth, t, 0n, last)) -> {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_probe(~A, U32.from_nat(2n+k), AR.thaw(Maybe<&2, A>, t))) == ST.model(~A, ~cmp, ST.Sh{2n+k, depth, t}) : List<&2, A>}: 59 match r: 60 case Tuple{+t3, Tuple{esift, Tuple{pf3, Tuple{hho3, Tuple{hlay3, hms3}}}}}: 61 +hd = ST.g_depth(~A, ~cmp, 2n+k, depth, t, g) 62 +hs = ST.g_size(~A, ~cmp, 2n+k, depth, t, g) 63 +hlen = N.lt_le_trans(0n, 1n+k, SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), N.succ_le_lt(0n, 1n+k, N.zero_le(k)), N.lt_le(1n+k, SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), L.subst(Nat, z => {Nat.is_lt(1n+k, z) == True{} : Bool}, SC.pow2(depth), SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), Equal.sym(Nat, SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), SC.pow2(depth), AR.slots_length(Maybe<&2, A>, depth, t, ST.g_perfect(~A, ~cmp, 2n+k, depth, t, g))), N.succ_le_lt(1n+k, SC.pow2(depth), hs)))) 64 Equal.trans(List<&2, A>, H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_probe(~A, U32.from_nat(2n+k), AR.thaw(Maybe<&2, A>, t))), Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(1n+k), AR.thaw(Maybe<&2, A>, t3)))}, ST.model(~A, ~cmp, ST.Sh{2n+k, depth, t}), 65 Equal.trans(List<&2, A>, H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_probe(~A, U32.from_nat(2n+k), AR.thaw(Maybe<&2, A>, t))), Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(1n+k), H.sift_down(~A, ~cmp, depth, U32.from_nat(1n+k), U32.from_nat(0n), last, AR.thaw(Maybe<&2, A>, t))))}, Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(1n+k), AR.thaw(Maybe<&2, A>, t3)))}, 66 drain_unfold(~A, ~cmp, depth, 1n+k, f, t, root, last, hd, ST.g_perfect(~A, ~cmp, 2n+k, depth, t, g), hs, h0, hlast, N.succ_le_lt(0n, 1n+k, N.zero_le(k))), 67 Equal.cong(Array>, List<&2, A>, a => Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(1n+k), a))}, H.sift_down(~A, ~cmp, depth, U32.from_nat(1n+k), U32.from_nat(0n), last, AR.thaw(Maybe<&2, A>, t)), AR.thaw(Maybe<&2, A>, t3), esift)), 68 Equal.trans(List<&2, A>, Con{root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(1n+k), AR.thaw(Maybe<&2, A>, t3)))}, Con{root, ST.model(~A, ~cmp, ST.Sh{1n+k, depth, t3})}, ST.model(~A, ~cmp, ST.Sh{2n+k, depth, t}), 69 LL.cons_cong(A, root, H.drain_go(~A, ~cmp, f, depth, H.drain_probe(~A, U32.from_nat(1n+k), AR.thaw(Maybe<&2, A>, t3))), ST.model(~A, ~cmp, ST.Sh{1n+k, depth, t3}), 70 rec(t3, ST.good_intro(~A, ~cmp, 1n+k, depth, t3, hd, pf3, hlay3, hho3, N.le_trans(1n+k, 2n+k, SC.pow2(depth), N.le_succ(1n+k), hs)))), 71 Equal.trans(List<&2, A>, Con{root, ST.model(~A, ~cmp, ST.Sh{1n+k, depth, t3})}, Con{root, V.msort(~A, ~cmp, V.vals(~A, PO.hole(~A, AR.slots(Maybe<&2, A>, t), 1n+k, last), 1n+k))}, ST.model(~A, ~cmp, ST.Sh{2n+k, depth, t}), 72 LL.cons_cong(A, root, ST.model(~A, ~cmp, ST.Sh{1n+k, depth, t3}), V.msort(~A, ~cmp, V.vals(~A, PO.hole(~A, AR.slots(Maybe<&2, A>, t), 1n+k, last), 1n+k)), hms3), 73 Equal.sym(List<&2, A>, ST.model(~A, ~cmp, ST.Sh{2n+k, depth, t}), Con{root, V.msort(~A, ~cmp, V.vals(~A, PO.hole(~A, AR.slots(Maybe<&2, A>, t), 1n+k, last), 1n+k))}, 74 PO.pop_split(~A, ~cmp, ~o, AR.slots(Maybe<&2, A>, t), 1n+k, root, last, N.succ_le_lt(0n, 1n+k, N.zero_le(k)), ST.g_ho(~A, ~cmp, 2n+k, depth, t, g), ST.g_lay(~A, ~cmp, 2n+k, depth, t, g), h0, hlast, hlen))))) 75 76 # the one-element copy 77 def drain_single(~A: Data, ~cmp: A -> A -> Cmp, +depth: Nat, +f: Nat, +t: AR.Tree>, +g: {ST.good(~A, ~cmp, ST.Sh{1n, 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>}>) -> {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_probe(~A, U32.from_nat(1n), AR.thaw(Maybe<&2, A>, t))) == ST.model(~A, ~cmp, ST.Sh{1n, depth, t}) : List<&2, A>}: 78 match sig: 79 case Tuple{+root, +h0}: 80 Equal.trans(List<&2, A>, H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_probe(~A, U32.from_nat(1n), AR.thaw(Maybe<&2, A>, t))), Con{root, Nil{}}, ST.model(~A, ~cmp, ST.Sh{1n, depth, t}), 81 drain_one(~A, ~cmp, depth, f, t, root, root, ST.g_depth(~A, ~cmp, 1n, depth, t, g), ST.g_perfect(~A, ~cmp, 1n, depth, t, g), N.pow2_pos(depth), h0, h0), 82 Equal.sym(List<&2, A>, ST.model(~A, ~cmp, ST.Sh{1n, depth, t}), Con{root, Nil{}}, 83 Equal.cong(Maybe<&2, A>, List<&2, A>, ms => V.msort(~A, ~cmp, V.cons_slot(~A, ms, Nil{})), SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n), Some{root}, h0))) 84 85 def drain_two(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +depth: Nat, +f: Nat, +k: Nat, +t: AR.Tree>, +root: A, +g: {ST.good(~A, ~cmp, ST.Sh{2n+k, depth, t}) == True{} : Bool}, +h0: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>}, rec: DrainRec(~A, ~cmp, f, depth, 1n+k), sig: Sigma<&1, &1, A, v => {SL.slot(~A, AR.slots(Maybe<&2, A>, t), 1n+k) == Some{v} : Maybe<&2, A>}>) -> {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_probe(~A, U32.from_nat(2n+k), AR.thaw(Maybe<&2, A>, t))) == ST.model(~A, ~cmp, ST.Sh{2n+k, depth, t}) : List<&2, A>}: 86 match sig: 87 case Tuple{+last, +hlast}: 88 drain_move(~A, ~cmp, ~o, depth, f, k, t, root, last, g, h0, hlast, rec, 89 PO.pop_sift(~A, ~cmp, ~o, depth, 1n+k, t, root, last, ST.g_depth(~A, ~cmp, 2n+k, depth, t, g), ST.g_perfect(~A, ~cmp, 2n+k, depth, t, g), ST.g_size(~A, ~cmp, 2n+k, depth, t, g), ST.g_ho(~A, ~cmp, 2n+k, depth, t, g), ST.g_lay(~A, ~cmp, 2n+k, depth, t, g), h0, hlast, N.succ_le_lt(0n, 1n+k, N.zero_le(k)))) 90 91 def drain_pair(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +depth: Nat, +f: Nat, +k: Nat, +t: AR.Tree>, +g: {ST.good(~A, ~cmp, ST.Sh{2n+k, depth, t}) == True{} : Bool}, rec: DrainRec(~A, ~cmp, f, depth, 1n+k), sig: Sigma<&1, &1, A, v => {SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n) == Some{v} : Maybe<&2, A>}>) -> {H.drain_go(~A, ~cmp, 1n+f, depth, H.drain_probe(~A, U32.from_nat(2n+k), AR.thaw(Maybe<&2, A>, t))) == ST.model(~A, ~cmp, ST.Sh{2n+k, depth, t}) : List<&2, A>}: 92 match sig: 93 case Tuple{+root, +h0}: 94 drain_two(~A, ~cmp, ~o, depth, f, k, t, root, g, h0, rec, 95 SL.slot_some(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), 1n+k), SL.lay_at(~A, AR.slots(Maybe<&2, A>, t), 2n+k, 1n+k, ST.g_lay(~A, ~cmp, 2n+k, depth, t, g), N.lt_succ(1n+k)))) 96 97 # The whole drain: as many iterations as the copy has elements. 98 def drain_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), fuel: Nat, +depth: Nat, size: Nat, +t: AR.Tree>, +g: {ST.good(~A, ~cmp, ST.Sh{size, depth, t}) == True{} : Bool}, +hf: {Nat.is_le(size, fuel) == True{} : Bool}) -> {H.drain_go(~A, ~cmp, fuel, depth, H.drain_probe(~A, U32.from_nat(size), AR.thaw(Maybe<&2, A>, t))) == ST.model(~A, ~cmp, ST.Sh{size, depth, t}) : List<&2, A>}: 99 match fuel size: 100 case 0n 0n: 101 {==} 102 case 1n+f 0n: 103 {==} 104 case 0n 1n+m: 105 Empty.absurd({H.drain_go(~A, ~cmp, 0n, depth, H.drain_probe(~A, U32.from_nat(1n+m), AR.thaw(Maybe<&2, A>, t))) == ST.model(~A, ~cmp, ST.Sh{1n+m, depth, t}) : List<&2, A>}, L.true_not_false(Nat.is_le(1n+m, 0n), hf, {==})) 106 case 1n+f 1n+0n: 107 drain_single(~A, ~cmp, depth, f, t, g, 108 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, 0n, ST.g_lay(~A, ~cmp, 1n, depth, t, g), {==}))) 109 case 1n+ +f 1n+1n+ +k: 110 drain_pair(~A, ~cmp, ~o, depth, f, k, t, g, 111 t3 => g3 => drain_ok(~A, ~cmp, ~o, f, depth, 1n+k, t3, g3, N.lt_succ_le(1n+k, f, N.succ_le_lt(1n+k, 1n+f, hf))), 112 SL.slot_some(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n), SL.lay_at(~A, AR.slots(Maybe<&2, A>, t), 2n+k, 0n, ST.g_lay(~A, ~cmp, 2n+k, depth, t, g), N.succ_le_lt(0n, 2n+k, N.zero_le(1n+k))))) 113 114 # ---- to_sorted_list ---- 115 # 116 # The heap is returned unchanged and the observation is its sorted multiset: 117 # the drain runs on the clone. 118 def to_sorted_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}) -> {H.to_sorted_list(~A, ~cmp, ST.real(~A, ST.Sh{size, depth, t})) == (ST.real(~A, ST.Sh{size, depth, t}), ST.model(~A, ~cmp, ST.Sh{size, depth, t})) : H.Heap & List<&2, A>}: 119 %Equal.sym(Array> & Array>, Array.clone(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t)), (AR.thaw(Maybe<&2, A>, t), AR.thaw(Maybe<&2, A>, t)), AR.clone(Maybe<&2, A>, t)) : {H.sorted_of(~A, ~cmp, size, U32.from_nat(size), depth, U.pow2u(depth), _) == (ST.real(~A, ST.Sh{size, depth, t}), ST.model(~A, ~cmp, ST.Sh{size, depth, t})) : H.Heap & List<&2, A>} 120 Equal.cong(List<&2, A>, H.Heap & List<&2, A>, zs => (ST.real(~A, ST.Sh{size, depth, t}), zs), H.drain_go(~A, ~cmp, size, depth, H.drain_probe(~A, U32.from_nat(size), AR.thaw(Maybe<&2, A>, t))), ST.model(~A, ~cmp, ST.Sh{size, depth, t}), 121 drain_ok(~A, ~cmp, ~o, size, depth, size, t, g, N.le_refl(size)))