proofs/containers/binary_heap/root.bend
bend-collections-laws-containers@1.0.0.0 · 210 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/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as S
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/idx.bend as IX
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/slots.bend as SL
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/vals.bend as V
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/multiset.bend as M
12
13# The root of a heap-ordered block is its minimum, and the block's multiset
14# has as many elements as the block has occupied slots. These are the two
15# facts the public operations need on top of the sift laws: `peek` and `pop`
16# observe slot 0, and `length` observes the cached size.
17#
18# `low_all(ss, k, x)` is "x is not larger than any of the slots [0, k)". It is
19# a Bool conjunction rather than a quantifier because a function-typed
20# hypothesis is a linear Type in Bend and could not be used twice.
21
22def low_all(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, n: Nat, +x: A) -> Bool:
23 match n:
24 case 0n:
25 True{}
26 case 1n+ +m:
27 Bool.and(SL.mle(~A, ~cmp, Some{x}, SL.slot(~A, ss, m)), low_all(~A, ~cmp, ss, m, x))
28
29# ---- the root is below every slot ----
30
31def mle_mid(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +a: A, m: Maybe<&2, A>, b: Maybe<&2, A>, +y: A, +hm: {m == Some{y} : Maybe<&2, A>}, +h1: {SL.mle(~A, ~cmp, Some{a}, m) == True{} : Bool}, +h2: {SL.mle(~A, ~cmp, m, b) == True{} : Bool}) -> {SL.mle(~A, ~cmp, Some{a}, b) == True{} : Bool}:
32 SL.mle_trans(~A, ~cmp, ~o, Some{a}, y, b,
33 L.subst(Maybe<&2, A>, z => {SL.mle(~A, ~cmp, Some{a}, z) == True{} : Bool}, m, Some{y}, hm, h1),
34 L.subst(Maybe<&2, A>, z => {SL.mle(~A, ~cmp, z, b) == True{} : Bool}, m, Some{y}, hm, h2))
35
36def root_at(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +root: A, +c: Nat, b: Maybe<&2, A>, sig: Sigma<&1, &1, A, v => {SL.slot(~A, ss, IX.par(c)) == Some{v} : Maybe<&2, A>}>, +h1: {SL.mle(~A, ~cmp, Some{root}, SL.slot(~A, ss, IX.par(c))) == True{} : Bool}, +h2: {SL.mle(~A, ~cmp, SL.slot(~A, ss, IX.par(c)), b) == True{} : Bool}) -> {SL.mle(~A, ~cmp, Some{root}, b) == True{} : Bool}:
37 match sig:
38 case Tuple{+y, hy}:
39 mle_mid(~A, ~cmp, ~o, root, SL.slot(~A, ss, IX.par(c)), b, y, hy, h1, h2)
40
41# Walking up the parent chain: the fuel is an upper bound on the index, and
42# the parent of a positive index is strictly smaller.
43def root_le(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +n: Nat, fuel: Nat, +root: A, j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +hjf: {Nat.is_le(j, fuel) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, n) == True{} : Bool}, +hlay: {SL.lay(~A, ss, n) == True{} : Bool}, +h0: {SL.slot(~A, ss, 0n) == Some{root} : Maybe<&2, A>}) -> {SL.mle(~A, ~cmp, Some{root}, SL.slot(~A, ss, j)) == True{} : Bool}:
44 match fuel j:
45 case _ 0n:
46 %Equal.sym(Maybe<&2, A>, SL.slot(~A, ss, 0n), Some{root}, h0) : {SL.mle(~A, ~cmp, Some{root}, _) == True{} : Bool}
47 O.le_refl(~A, ~cmp, ~o, root)
48 case 0n 1n+p:
49 Empty.absurd({SL.mle(~A, ~cmp, Some{root}, SL.slot(~A, ss, 1n+p)) == True{} : Bool}, L.true_not_false(Nat.is_le(1n+p, 0n), hjf, {==}))
50 case 1n+ +f 1n+ +p:
51 +hpn = N.lt_trans(IX.par(1n+p), 1n+p, n, IX.par_lt(1n+p, {==}), hj)
52 root_at(~A, ~cmp, ~o, ss, root, 1n+p, SL.slot(~A, ss, 1n+p),
53 SL.slot_some(~A, SL.slot(~A, ss, IX.par(1n+p)), SL.lay_at(~A, ss, n, IX.par(1n+p), hlay, hpn)),
54 root_le(~A, ~cmp, ~o, ss, n, f, root, IX.par(1n+p), hpn,
55 N.lt_succ_le(IX.par(1n+p), f, N.lt_le_trans(IX.par(1n+p), 1n+p, 1n+f, IX.par_lt(1n+p, {==}), hjf)),
56 hho, hlay, h0),
57 SL.ho_at(~A, ~cmp, ss, n, 1n+p, hho, hj))
58
59def low_all_mk(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +n: Nat, k: Nat, +root: A, +hk: {Nat.is_le(k, n) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, n) == True{} : Bool}, +hlay: {SL.lay(~A, ss, n) == True{} : Bool}, +h0: {SL.slot(~A, ss, 0n) == Some{root} : Maybe<&2, A>}) -> {low_all(~A, ~cmp, ss, k, root) == True{} : Bool}:
60 match k:
61 case 0n:
62 {==}
63 case 1n+ +m:
64 L.and_intro(SL.mle(~A, ~cmp, Some{root}, SL.slot(~A, ss, m)), low_all(~A, ~cmp, ss, m, root),
65 root_le(~A, ~cmp, ~o, ss, n, m, root, m, N.succ_le_lt(m, n, hk), N.le_refl(m), hho, hlay, h0),
66 low_all_mk(~A, ~cmp, ~o, ss, n, m, root, N.le_trans(m, 1n+m, n, N.le_succ(m), hk), hho, hlay, h0))
67
68# ---- from slots to the multiset ----
69
70def all_ge_cons(~A: Data, ~cmp: A -> A -> Cmp, +z: A, m: Maybe<&2, A>, +xs: List<&2, A>, +hm: {SL.mle(~A, ~cmp, Some{z}, m) == True{} : Bool}, +ih: {S.all_ge(~A, ~cmp, z, xs) == True{} : Bool}) -> {S.all_ge(~A, ~cmp, z, V.cons_slot(~A, m, xs)) == True{} : Bool}:
71 match m:
72 case None{}:
73 ih
74 case Some{+v}:
75 L.and_intro(S.le(~A, ~cmp, z, v), S.all_ge(~A, ~cmp, z, xs), hm, ih)
76
77def all_ge_vals(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, n: Nat, +z: A, +h: {low_all(~A, ~cmp, ss, n, z) == True{} : Bool}) -> {S.all_ge(~A, ~cmp, z, V.vals(~A, ss, n)) == True{} : Bool}:
78 match n:
79 case 0n:
80 {==}
81 case 1n+ +m:
82 all_ge_cons(~A, ~cmp, z, SL.slot(~A, ss, m), V.vals(~A, ss, m),
83 L.and_left(SL.mle(~A, ~cmp, Some{z}, SL.slot(~A, ss, m)), low_all(~A, ~cmp, ss, m, z), h),
84 all_ge_vals(~A, ~cmp, ss, m, z, L.and_right(SL.mle(~A, ~cmp, Some{z}, SL.slot(~A, ss, m)), low_all(~A, ~cmp, ss, m, z), h)))
85
86def all_ge_msort(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +z: A, xs: List<&2, A>, +h: {S.all_ge(~A, ~cmp, z, xs) == True{} : Bool}) -> {S.all_ge(~A, ~cmp, z, V.msort(~A, ~cmp, xs)) == True{} : Bool}:
87 match xs:
88 case Nil{}:
89 {==}
90 case Con{+x, +t}:
91 %Equal.sym(Bool, S.all_ge(~A, ~cmp, z, S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, t))), Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, V.msort(~A, ~cmp, t))), M.all_ge_ins(~A, ~cmp, ~o, z, x, V.msort(~A, ~cmp, t))) : {_ == True{} : Bool}
92 L.and_intro(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, V.msort(~A, ~cmp, t)),
93 L.and_left(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, t), h),
94 all_ge_msort(~A, ~cmp, ~o, z, t, L.and_right(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, t), h)))
95
96# x is not larger than any slot of [0, k) => it comes first in the multiset.
97def front(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +k: Nat, +z: A, +h: {low_all(~A, ~cmp, ss, k, z) == True{} : Bool}) -> {S.ins(~A, ~cmp, z, V.msort(~A, ~cmp, V.vals(~A, ss, k))) == Con{z, V.msort(~A, ~cmp, V.vals(~A, ss, k))} : List<&2, A>}:
98 M.ins_min(~A, ~cmp, ~o, z, V.msort(~A, ~cmp, V.vals(~A, ss, k)),
99 all_ge_msort(~A, ~cmp, ~o, z, V.vals(~A, ss, k), all_ge_vals(~A, ~cmp, ss, k, z, h)))
100
101# ---- the multiset has one element per occupied slot ----
102
103def length_ins_c(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +h: A, +t: List<&2, A>, +b: Bool, +e: {S.le(~A, ~cmp, x, h) == b : Bool}, +ih: {SC.length(A, S.ins(~A, ~cmp, x, t)) == 1n+SC.length(A, t) : Nat}) -> {SC.length(A, S.ins(~A, ~cmp, x, Con{h, t})) == 2n+SC.length(A, t) : Nat}:
104 match b:
105 case True{}:
106 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{x, Con{h, t}}, M.ins_cons(~A, ~cmp, x, h, t, True{}, e)) : {SC.length(A, _) == 2n+SC.length(A, t) : Nat}
107 {==}
108 case False{}:
109 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{h, S.ins(~A, ~cmp, x, t)}, M.ins_cons(~A, ~cmp, x, h, t, False{}, e)) : {SC.length(A, _) == 2n+SC.length(A, t) : Nat}
110 N.succ_cong(SC.length(A, S.ins(~A, ~cmp, x, t)), 1n+SC.length(A, t), ih)
111
112def length_ins(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +xs: List<&2, A>) -> {SC.length(A, S.ins(~A, ~cmp, x, xs)) == 1n+SC.length(A, xs) : Nat}:
113 match xs:
114 case Nil{}:
115 {==}
116 case Con{+h, +t}:
117 length_ins_c(~A, ~cmp, x, h, t, S.le(~A, ~cmp, x, h), {==}, length_ins(~A, ~cmp, x, t))
118
119def msort_length(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>) -> {SC.length(A, V.msort(~A, ~cmp, xs)) == SC.length(A, xs) : Nat}:
120 match xs:
121 case Nil{}:
122 {==}
123 case Con{+x, +t}:
124 Equal.trans(Nat, SC.length(A, S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, t))), 1n+SC.length(A, V.msort(~A, ~cmp, t)), 1n+SC.length(A, t),
125 length_ins(~A, ~cmp, x, V.msort(~A, ~cmp, t)),
126 N.succ_cong(SC.length(A, V.msort(~A, ~cmp, t)), SC.length(A, t), msort_length(~A, ~cmp, t)))
127
128def vals_length_c(~A: Data, +ss: List<&2, Maybe<&2, A>>, +m: Nat, s: Maybe<&2, A>, +es: {SL.slot(~A, ss, m) == s : Maybe<&2, A>}, +hs: {Maybe.is_some(&2, A, SL.slot(~A, ss, m)) == True{} : Bool}, +ih: {SC.length(A, V.vals(~A, ss, m)) == m : Nat}) -> {SC.length(A, V.vals(~A, ss, 1n+m)) == 1n+m : Nat}:
129 match s:
130 case None{}:
131 Empty.absurd({SC.length(A, V.vals(~A, ss, 1n+m)) == 1n+m : Nat}, L.false_true(L.subst(Maybe<&2, A>, z => {Maybe.is_some(&2, A, z) == True{} : Bool}, SL.slot(~A, ss, m), None{}, es, hs)))
132 case Some{+v}:
133 %Equal.sym(Maybe<&2, A>, SL.slot(~A, ss, m), Some{v}, es) : {SC.length(A, V.cons_slot(~A, _, V.vals(~A, ss, m))) == 1n+m : Nat}
134 N.succ_cong(SC.length(A, V.vals(~A, ss, m)), m, ih)
135
136def vals_length(~A: Data, +ss: List<&2, Maybe<&2, A>>, n: Nat, +hlay: {SL.lay(~A, ss, n) == True{} : Bool}) -> {SC.length(A, V.vals(~A, ss, n)) == n : Nat}:
137 match n:
138 case 0n:
139 {==}
140 case 1n+ +m:
141 vals_length_c(~A, ss, m, SL.slot(~A, ss, m), {==},
142 L.and_left(Maybe.is_some(&2, A, SL.slot(~A, ss, m)), SL.lay(~A, ss, m), hlay),
143 vals_length(~A, ss, m, L.and_right(Maybe.is_some(&2, A, SL.slot(~A, ss, m)), SL.lay(~A, ss, m), hlay)))
144
145def model_length(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +hlay: {SL.lay(~A, ss, n) == True{} : Bool}) -> {SC.length(A, V.msort(~A, ~cmp, V.vals(~A, ss, n))) == n : Nat}:
146 Equal.trans(Nat, SC.length(A, V.msort(~A, ~cmp, V.vals(~A, ss, n))), SC.length(A, V.vals(~A, ss, n)), n,
147 msort_length(~A, ~cmp, V.vals(~A, ss, n)),
148 vals_length(~A, ss, n, hlay))
149
150# ---- taking one element out of the multiset ----
151#
152# The mirror of vals.ins_set: emptying slot i removes exactly its value from
153# the sorted multiset. This is what makes the root observable: it is the
154# element the sorted multiset starts with.
155
156def ins_del_cons(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), s: Maybe<&2, A>, +old: A, +xs: List<&2, A>, +ys: List<&2, A>, +ih: {V.msort(~A, ~cmp, xs) == S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, ys)) : List<&2, A>}) -> {V.msort(~A, ~cmp, V.cons_slot(~A, s, xs)) == S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, V.cons_slot(~A, s, ys))) : List<&2, A>}:
157 match s:
158 case None{}:
159 ih
160 case Some{+w}:
161 Equal.trans(List<&2, A>, S.ins(~A, ~cmp, w, V.msort(~A, ~cmp, xs)), S.ins(~A, ~cmp, w, S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, ys))), S.ins(~A, ~cmp, old, S.ins(~A, ~cmp, w, V.msort(~A, ~cmp, ys))),
162 Equal.cong(List<&2, A>, List<&2, A>, zs => S.ins(~A, ~cmp, w, zs), V.msort(~A, ~cmp, xs), S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, ys)), ih),
163 M.ins_comm(~A, ~cmp, ~o, w, old, V.msort(~A, ~cmp, ys)))
164
165def ins_del_top(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +old: A, +ei: {i == m : Nat}, +hold: {SL.slot(~A, ss, i) == Some{old} : Maybe<&2, A>}) -> {V.msort(~A, ~cmp, V.vals(~A, ss, 1n+m)) == S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), 1n+m))) : List<&2, A>}:
166 %ei : {V.msort(~A, ~cmp, V.vals(~A, ss, 1n+_)) == S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), 1n+_))) : List<&2, A>}
167 Equal.trans(List<&2, A>, V.msort(~A, ~cmp, V.cons_slot(~A, SL.slot(~A, ss, i), V.vals(~A, ss, i))), S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, V.vals(~A, ss, i))), S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), 1n+i))),
168 Equal.cong(Maybe<&2, A>, List<&2, A>, ms => V.msort(~A, ~cmp, V.cons_slot(~A, ms, V.vals(~A, ss, i))), SL.slot(~A, ss, i), Some{old}, hold),
169 Equal.cong(List<&2, A>, List<&2, A>, zs => S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, zs)), V.vals(~A, ss, i), V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), 1n+i),
170 Equal.trans(List<&2, A>, V.vals(~A, ss, i), V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), i), V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), 1n+i),
171 Equal.sym(List<&2, A>, V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), i), V.vals(~A, ss, i), V.vals_above(~A, ss, i, None{}, i, N.le_refl(i))),
172 Equal.cong(Maybe<&2, A>, List<&2, A>, ms => V.cons_slot(~A, ms, V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), i)), None{}, SL.slot(~A, SC.update(Maybe<&2, A>, ss, i, None{}), i),
173 Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.update(Maybe<&2, A>, ss, i, None{}), i), None{}, SL.slot_same(~A, ss, i, None{}, V.slot_in_range(~A, ss, i, old, hold)))))))
174
175def ins_del(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, n: Nat, +i: Nat, +old: A, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hold: {SL.slot(~A, ss, i) == Some{old} : Maybe<&2, A>}, b: Bool, +eb: {Nat.is_eq(i, N.pred(n)) == b : Bool}) -> {V.msort(~A, ~cmp, V.vals(~A, ss, n)) == S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), n))) : List<&2, A>}:
176 match n b:
177 case 0n _:
178 Empty.absurd({V.msort(~A, ~cmp, V.vals(~A, ss, 0n)) == S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), 0n))) : List<&2, A>}, N.lt_zero_absurd(i, hi))
179 case 1n+m True{}:
180 ins_del_top(~A, ~cmp, ss, m, i, old, N.eq_from_is_eq(i, m, eb), hold)
181 case 1n+ +m False{}:
182 +hi2 = N.lt_or_eq(i, m, N.lt_succ_le(i, m, hi), eb)
183 %Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.update(Maybe<&2, A>, ss, i, None{}), m), SL.slot(~A, ss, m), SL.slot_other(~A, ss, i, m, None{}, N.is_eq_lt(i, m, hi2))) : {V.msort(~A, ~cmp, V.vals(~A, ss, 1n+m)) == S.ins(~A, ~cmp, old, V.msort(~A, ~cmp, V.cons_slot(~A, _, V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), m)))) : List<&2, A>}
184 ins_del_cons(~A, ~cmp, ~o, SL.slot(~A, ss, m), old, V.vals(~A, ss, m), V.vals(~A, SC.update(Maybe<&2, A>, ss, i, None{}), m),
185 ins_del(~A, ~cmp, ~o, ss, m, i, old, hi2, hold, Nat.is_eq(i, N.pred(m)), {==}))
186
187# ---- the sorted multiset of a heap-ordered block starts with its root ----
188
189def low_del_at(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +n: Nat, j: Nat, +root: A, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, n) == True{} : Bool}, +hlay: {SL.lay(~A, ss, n) == True{} : Bool}, +h0: {SL.slot(~A, ss, 0n) == Some{root} : Maybe<&2, A>}) -> {SL.mle(~A, ~cmp, Some{root}, SL.slot(~A, SC.update(Maybe<&2, A>, ss, 0n, None{}), j)) == True{} : Bool}:
190 match j:
191 case 0n:
192 %Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.update(Maybe<&2, A>, ss, 0n, None{}), 0n), None{}, SL.slot_same(~A, ss, 0n, None{}, V.slot_in_range(~A, ss, 0n, root, h0))) : {SL.mle(~A, ~cmp, Some{root}, _) == True{} : Bool}
193 SL.mle_none_r(~A, ~cmp, Some{root})
194 case 1n+ +p:
195 %Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.update(Maybe<&2, A>, ss, 0n, None{}), 1n+p), SL.slot(~A, ss, 1n+p), SL.slot_other(~A, ss, 0n, 1n+p, None{}, {==})) : {SL.mle(~A, ~cmp, Some{root}, _) == True{} : Bool}
196 root_le(~A, ~cmp, ~o, ss, n, 1n+p, root, 1n+p, hjn, N.le_refl(1n+p), hho, hlay, h0)
197
198def low_del(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +n: Nat, k: Nat, +root: A, +hk: {Nat.is_le(k, n) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, n) == True{} : Bool}, +hlay: {SL.lay(~A, ss, n) == True{} : Bool}, +h0: {SL.slot(~A, ss, 0n) == Some{root} : Maybe<&2, A>}) -> {low_all(~A, ~cmp, SC.update(Maybe<&2, A>, ss, 0n, None{}), k, root) == True{} : Bool}:
199 match k:
200 case 0n:
201 {==}
202 case 1n+ +m:
203 L.and_intro(SL.mle(~A, ~cmp, Some{root}, SL.slot(~A, SC.update(Maybe<&2, A>, ss, 0n, None{}), m)), low_all(~A, ~cmp, SC.update(Maybe<&2, A>, ss, 0n, None{}), m, root),
204 low_del_at(~A, ~cmp, ~o, ss, n, m, root, N.succ_le_lt(m, n, hk), hho, hlay, h0),
205 low_del(~A, ~cmp, ~o, ss, n, m, root, N.le_trans(m, 1n+m, n, N.le_succ(m), hk), hho, hlay, h0))
206
207def head_root(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +n: Nat, +root: A, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, ss, n) == True{} : Bool}, +hlay: {SL.lay(~A, ss, n) == True{} : Bool}, +h0: {SL.slot(~A, ss, 0n) == Some{root} : Maybe<&2, A>}) -> {V.msort(~A, ~cmp, V.vals(~A, ss, n)) == Con{root, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, ss, 0n, None{}), n))} : List<&2, A>}:
208 Equal.trans(List<&2, A>, V.msort(~A, ~cmp, V.vals(~A, ss, n)), S.ins(~A, ~cmp, root, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, ss, 0n, None{}), n))), Con{root, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, ss, 0n, None{}), n))},
209 ins_del(~A, ~cmp, ~o, ss, n, 0n, root, hn, h0, Nat.is_eq(0n, N.pred(n)), {==}),
210 front(~A, ~cmp, ~o, SC.update(Maybe<&2, A>, ss, 0n, None{}), n, root, low_del(~A, ~cmp, ~o, ss, n, n, root, N.le_refl(n), hho, hlay, h0)))