proofs/containers/binary_heap/pop.bend
bend-collections-laws-containers@1.0.0.0 · 297 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
8import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
9import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as S
10import bend-collections-laws-containers@1.0.0.0/src/containers/binary_heap.bend as H
11import bend-collections-laws-containers@1.0.0.0/src/containers/types/binary_heap.bend as E
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/idx.bend as IX
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/u32idx.bend as UX
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/slots.bend as SL
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/vals.bend as V
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/multiset.bend as M
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/root.bend as RT
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/up.bend as UPS
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/down.bend as DN
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/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
28def 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
35def 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
44def 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
54def 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
67def 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
70def 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
73def 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
78def 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
88def 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
95def 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
106def 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
115def 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
126def 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
135def 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
142def 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
150def 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
160def 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.
171def 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
178def 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
181def round_nth(~A: Data, +t: AR.Tree<Maybe<&2, A>>, +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
186def get_last(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +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>> & 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
189def get_root(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +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>> & 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.
196def pop_to_move(~A: Data, ~cmp: A -> A -> Cmp, +depth: Nat, +m: Nat, +t: AR.Tree<Maybe<&2, A>>, +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<A> & 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>> & 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<A> & 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<A> & 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<A> & 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>> & 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<A> & 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<A> & 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
218def pop_sift(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +depth: Nat, +m: Nat, +t: AR.Tree<Maybe<&2, A>>, +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
237def PopRes(~A: Data, ~cmp: A -> A -> Cmp, sh: ST.Shadow<A>) -> Type:
238 Sigma<&1, &1, ST.Shadow<A>, 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<A> & 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<A>} & {ST.sh_depth(~A, sh2) == ST.sh_depth(~A, sh) : Nat}))>>
239
240def pop_from(~A: Data, ~cmp: A -> A -> Cmp, +depth: Nat, +m: Nat, +t: AR.Tree<Maybe<&2, A>>, +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<A> & 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<A> & 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<Maybe<&2, A>>, H.Heap<A> & 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<A>}
249 Equal.cong(List<&2, A>, List<&2, A> & E.Obs<A>, zs => (zs, E.OItem{Done{root}}), ST.model(~A, ~cmp, ST.Sh{m, depth, t3}), tgt, hms3),
250 {==})))))
251
252def pop_nonempty(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +depth: Nat, m: Nat, +t: AR.Tree<Maybe<&2, A>>, +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<A>}
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<A> & 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
280def pop_with_last(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +depth: Nat, +m: Nat, +t: AR.Tree<Maybe<&2, A>>, +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
285def pop_with_root(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +depth: Nat, +m: Nat, +t: AR.Tree<Maybe<&2, A>>, +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
291def pop_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +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)))))