proofs/containers/binary_heap/slots.bend
bend-collections-laws-containers@1.0.0.0 · 323 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
9
10# The slot list of an array heap, and heap order on it.
11#
12# Heap order is stated over CHILD indices -- "every j in [1, n) is not smaller
13# than the value at par(j)" -- so the predicate never divides an index it does
14# not have to, and every fact about it is pointwise: `ho_get` reads one pair
15# out of the conjunction and `ho_put` builds the conjunction from a function
16# that proves one pair at a time. Everything the sift proofs do is then a case
17# analysis on a single index, never an induction over a range.
18
19def unwrap(~A: Data, m: Maybe<&2, Maybe<&2, A>>) -> Maybe<&2, A>:
20 match m:
21 case None{}:
22 None{}
23 case Some{s}:
24 s
25
26def slot(~A: Data, ss: List<&2, Maybe<&2, A>>, +j: Nat) -> Maybe<&2, A>:
27 unwrap(~A, SC.nth(Maybe<&2, A>, ss, j))
28
29# Order between two slots; vacuously true when a slot is empty (the layout
30# invariant is what says the slots of interest are occupied).
31def mle(~A: Data, ~cmp: A -> A -> Cmp, a: Maybe<&2, A>, b: Maybe<&2, A>) -> Bool:
32 match a b:
33 case Some{x} Some{y}:
34 S.le(~A, ~cmp, x, y)
35 case _ _:
36 True{}
37
38def pair_ok(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, j: Nat) -> Bool:
39 match j:
40 case 0n:
41 True{}
42 case 1n+ +m:
43 mle(~A, ~cmp, slot(~A, ss, IX.par(1n+m)), slot(~A, ss, 1n+m))
44
45# Heap order over the children 0 .. k-1 (index 0 has no parent condition).
46def ho_upto(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat) -> Bool:
47 match k:
48 case 0n:
49 True{}
50 case 1n+ +m:
51 Bool.and(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m))
52
53# Every slot of [0, k) is occupied.
54def lay(~A: Data, +ss: List<&2, Maybe<&2, A>>, k: Nat) -> Bool:
55 match k:
56 case 0n:
57 True{}
58 case 1n+ +m:
59 Bool.and(Maybe.is_some(&2, A, slot(~A, ss, m)), lay(~A, ss, m))
60
61# ---- reading one pair out of the conjunction ----
62
63def ho_get_eq(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +j: Nat, +e: {Nat.is_eq(j, m) == True{} : Bool}, +hp: {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
64 L.subst(Nat, z => {pair_ok(~A, ~cmp, ss, z) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, e)), hp)
65
66def ho_get(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +j: Nat, +h: {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
67 match k b:
68 case 0n _:
69 Empty.absurd({pair_ok(~A, ~cmp, ss, j) == True{} : Bool}, N.lt_zero_absurd(j, hj))
70 case 1n+ +m True{}:
71 ho_get_eq(~A, ~cmp, ss, m, j, eb, L.and_left(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m), h))
72 case 1n+ +m False{}:
73 ho_get(~A, ~cmp, ss, m, j, L.and_right(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})
74
75def ho_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +j: Nat, +h: {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
76 ho_get(~A, ~cmp, ss, k, j, h, hj, Nat.is_eq(j, N.pred(k)), {==})
77
78# ---- updating one slot ----
79
80def slot_same(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +v: Maybe<&2, A>, +hi: {Nat.is_lt(i, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {slot(~A, SC.update(Maybe<&2, A>, ss, i, v), i) == v : Maybe<&2, A>}:
81 %Equal.sym(Maybe<&2, Maybe<&2, A>>, SC.nth(Maybe<&2, A>, SC.update(Maybe<&2, A>, ss, i, v), i), Some{v}, LL.nth_update_same(Maybe<&2, A>, ss, i, v, hi)) : {unwrap(~A, _) == v : Maybe<&2, A>}
82 {==}
83
84def slot_other(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +j: Nat, +v: Maybe<&2, A>, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {slot(~A, SC.update(Maybe<&2, A>, ss, i, v), j) == slot(~A, ss, j) : Maybe<&2, A>}:
85 Equal.cong(Maybe<&2, Maybe<&2, A>>, Maybe<&2, A>, m => unwrap(~A, m), SC.nth(Maybe<&2, A>, SC.update(Maybe<&2, A>, ss, i, v), j), SC.nth(Maybe<&2, A>, ss, j), LL.nth_update_other(Maybe<&2, A>, ss, i, j, v, ne))
86
87def flip_eq(c: Cmp, +h: {Cmp.is_eq(c) == False{} : Bool}) -> {Cmp.is_eq(O.flipc(c)) == False{} : Bool}:
88 match c:
89 case LT{}:
90 {==}
91 case EQ{}:
92 Empty.absurd({Cmp.is_eq(O.flipc(EQ{})) == False{} : Bool}, L.true_false(h))
93 case GT{}:
94 {==}
95
96def ne_sym(+a: Nat, +b: Nat, +h: {Nat.is_eq(b, a) == False{} : Bool}) -> {Nat.is_eq(a, b) == False{} : Bool}:
97 %Equal.sym(Cmp, Nat.cmp(a, b), O.flipc(Nat.cmp(b, a)), O.nat_flip(b, a)) : {Cmp.is_eq(_) == False{} : Bool}
98 flip_eq(Nat.cmp(b, a), h)
99
100# ---- mle ----
101
102def mle_some(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +y: A, +h: {mle(~A, ~cmp, Some{x}, Some{y}) == True{} : Bool}) -> {S.le(~A, ~cmp, x, y) == True{} : Bool}:
103 h
104
105def mle_mk(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +y: A, +h: {S.le(~A, ~cmp, x, y) == True{} : Bool}) -> {mle(~A, ~cmp, Some{x}, Some{y}) == True{} : Bool}:
106 h
107
108def mle_none_l(~A: Data, ~cmp: A -> A -> Cmp, +b: Maybe<&2, A>) -> {mle(~A, ~cmp, None{}, b) == True{} : Bool}:
109 match b:
110 case None{}:
111 {==}
112 case Some{y}:
113 {==}
114
115def mle_none_r(~A: Data, ~cmp: A -> A -> Cmp, +a: Maybe<&2, A>) -> {mle(~A, ~cmp, a, None{}) == True{} : Bool}:
116 match a:
117 case None{}:
118 {==}
119 case Some{x}:
120 {==}
121
122# transitivity through an OCCUPIED middle slot (with an empty middle there is
123# nothing to conclude: `mle` is vacuous there)
124def mle_trans(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), a: Maybe<&2, A>, +y: A, c: Maybe<&2, A>, +hab: {mle(~A, ~cmp, a, Some{y}) == True{} : Bool}, +hbc: {mle(~A, ~cmp, Some{y}, c) == True{} : Bool}) -> {mle(~A, ~cmp, a, c) == True{} : Bool}:
125 match a c:
126 case Some{+x} Some{+z}:
127 O.trans(~A, ~cmp, o, x, y, z, hab, hbc)
128 case Some{x} None{}:
129 {==}
130 case None{} Some{z}:
131 {==}
132 case None{} None{}:
133 {==}
134
135
136# ---- the layout, pointwise ----
137
138def lay_get_eq(~A: Data, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +j: Nat, +e: {Nat.is_eq(j, m) == True{} : Bool}, +hp: {Maybe.is_some(&2, A, slot(~A, ss, m)) == True{} : Bool}) -> {Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}:
139 L.subst(Nat, z => {Maybe.is_some(&2, A, slot(~A, ss, z)) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, e)), hp)
140
141def lay_get(~A: Data, +ss: List<&2, Maybe<&2, A>>, k: Nat, +j: Nat, +h: {lay(~A, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}:
142 match k b:
143 case 0n _:
144 Empty.absurd({Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}, N.lt_zero_absurd(j, hj))
145 case 1n+ +m True{}:
146 lay_get_eq(~A, ss, m, j, eb, L.and_left(Maybe.is_some(&2, A, slot(~A, ss, m)), lay(~A, ss, m), h))
147 case 1n+ +m False{}:
148 lay_get(~A, ss, m, j, L.and_right(Maybe.is_some(&2, A, slot(~A, ss, m)), lay(~A, ss, m), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})
149
150def lay_at(~A: Data, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +j: Nat, +h: {lay(~A, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}) -> {Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}:
151 lay_get(~A, ss, k, j, h, hj, Nat.is_eq(j, N.pred(k)), {==})
152
153# An occupied slot, as a value.
154def slot_some(~A: Data, m: Maybe<&2, A>, +h: {Maybe.is_some(&2, A, m) == True{} : Bool}) -> Sigma<&1, &1, A, v => {m == Some{v} : Maybe<&2, A>}>:
155 match m:
156 case None{}:
157 Empty.absurd(Sigma<&1, &1, A, v => {None{} == Some{v} : Maybe<&2, A>}>, L.false_true(h))
158 case Some{+v}:
159 (v, {==})
160
161# ---- nth of a slot inside the list ----
162
163def nth_slot(~A: Data, +ss: List<&2, Maybe<&2, A>>, +j: Nat, +hj: {Nat.is_lt(j, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {SC.nth(Maybe<&2, A>, ss, j) == Some{slot(~A, ss, j)} : Maybe<&2, Maybe<&2, A>>}:
164 match ss j:
165 case Nil{} _:
166 Empty.absurd({None{} == Some{slot(~A, Nil{}, j)} : Maybe<&2, Maybe<&2, A>>}, N.lt_zero_absurd(j, hj))
167 case Con{x, r} 0n:
168 {==}
169 case Con{x, +r} 1n+k:
170 nth_slot(~A, r, k, hj)
171
172# ---- heap order with one index excluded ----
173#
174# `ho_exc(ss, k, i)` is "every pair below k except the one into i holds". It
175# is a Bool, not a function over indices: a proof term of function type could
176# not be used twice, and a step needs its invariant more than once.
177
178def pair_skip(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat) -> Bool:
179 Bool.pick(Bool, Nat.is_eq(m, i), True{}, pair_ok(~A, ~cmp, ss, m))
180
181def ho_exc(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat) -> Bool:
182 match k:
183 case 0n:
184 True{}
185 case 1n+ +m:
186 Bool.and(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i))
187
188def skip_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +hne: {Nat.is_eq(m, i) == False{} : Bool}, +h: {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}:
189 L.subst(Bool, b => {Bool.pick(Bool, b, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}, Nat.is_eq(m, i), False{}, hne, h)
190
191def skip_eq(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {Nat.is_eq(m, i) == True{} : Bool}) -> {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}:
192 %Equal.sym(Bool, Nat.is_eq(m, i), True{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}
193 {==}
194
195def skip_ne(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {Nat.is_eq(m, i) == False{} : Bool}, +h: {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}) -> {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}:
196 %Equal.sym(Bool, Nat.is_eq(m, i), False{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}
197 h
198
199def exc_get(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat, +j: Nat, +h: {ho_exc(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {pair_skip(~A, ~cmp, ss, j, i) == True{} : Bool}:
200 match k b:
201 case 0n _:
202 Empty.absurd({pair_skip(~A, ~cmp, ss, j, i) == True{} : Bool}, N.lt_zero_absurd(j, hj))
203 case 1n+ +m True{}:
204 L.subst(Nat, z => {pair_skip(~A, ~cmp, ss, z, i) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, eb)), L.and_left(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h))
205 case 1n+ +m False{}:
206 exc_get(~A, ~cmp, ss, m, i, j, L.and_right(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})
207
208# one pair out of `ho_exc`
209def exc_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +i: Nat, +j: Nat, +h: {ho_exc(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, +hne: {Nat.is_eq(j, i) == False{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
210 skip_at(~A, ~cmp, ss, j, i, hne, exc_get(~A, ~cmp, ss, k, i, j, h, hj, Nat.is_eq(j, N.pred(k)), {==}))
211
212def pair_of_skip(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +hi: {pair_ok(~A, ~cmp, ss, i) == True{} : Bool}, +h: {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(m, i) == b : Bool}) -> {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}:
213 match b:
214 case True{}:
215 ho_get_eq(~A, ~cmp, ss, i, m, eb, hi)
216 case False{}:
217 skip_at(~A, ~cmp, ss, m, i, eb, h)
218
219# `ho_upto` follows from `ho_exc` plus the excluded pair
220def ho_of_exc(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat, +h: {ho_exc(~A, ~cmp, ss, k, i) == True{} : Bool}, +hi: {pair_ok(~A, ~cmp, ss, i) == True{} : Bool}) -> {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}:
221 match k:
222 case 0n:
223 {==}
224 case 1n+ +m:
225 L.and_intro(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m),
226 pair_of_skip(~A, ~cmp, ss, m, i, hi, L.and_left(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h), Nat.is_eq(m, i), {==}),
227 ho_of_exc(~A, ~cmp, ss, m, i, L.and_right(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h), hi))
228
229# ---- the children of one index ----
230
231def kid_le(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat) -> Bool:
232 Bool.pick(Bool, Nat.is_lt(c, n), mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{})
233
234def kids_le(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +i: Nat) -> Bool:
235 Bool.and(kid_le(~A, ~cmp, ss, n, u, IX.kidl(i)), kid_le(~A, ~cmp, ss, n, u, IX.kidr(i)))
236
237def kid_le_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat, +hc: {Nat.is_lt(c, n) == True{} : Bool}, +h: {kid_le(~A, ~cmp, ss, n, u, c) == True{} : Bool}) -> {mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)) == True{} : Bool}:
238 L.subst(Bool, b => {Bool.pick(Bool, b, mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{}) == True{} : Bool}, Nat.is_lt(c, n), True{}, hc, h)
239
240def kid_le_in(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat, +eb: {Nat.is_lt(c, n) == True{} : Bool}, +h: {mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)) == True{} : Bool}) -> {kid_le(~A, ~cmp, ss, n, u, c) == True{} : Bool}:
241 %Equal.sym(Bool, Nat.is_lt(c, n), True{}, eb) : {Bool.pick(Bool, _, mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{}) == True{} : Bool}
242 h
243
244def kid_le_out(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat, +eb: {Nat.is_lt(c, n) == False{} : Bool}) -> {kid_le(~A, ~cmp, ss, n, u, c) == True{} : Bool}:
245 %Equal.sym(Bool, Nat.is_lt(c, n), False{}, eb) : {Bool.pick(Bool, _, mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{}) == True{} : Bool}
246 {==}
247
248# ---- heap order with the two pairs below one index excluded ----
249#
250# This is what a sift-DOWN carries: the hole may be larger than its children,
251# so the two pairs whose parent is the hole are the ones left out.
252
253def kid_of(+m: Nat, +i: Nat) -> Bool:
254 Bool.or(Nat.is_eq(m, IX.kidl(i)), Nat.is_eq(m, IX.kidr(i)))
255
256def pair_skip2(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat) -> Bool:
257 Bool.pick(Bool, kid_of(m, i), True{}, pair_ok(~A, ~cmp, ss, m))
258
259def ho_exc2(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat) -> Bool:
260 match k:
261 case 0n:
262 True{}
263 case 1n+ +m:
264 Bool.and(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i))
265
266def skip2_eq(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {kid_of(m, i) == True{} : Bool}) -> {pair_skip2(~A, ~cmp, ss, m, i) == True{} : Bool}:
267 %Equal.sym(Bool, kid_of(m, i), True{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}
268 {==}
269
270def skip2_ne(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {kid_of(m, i) == False{} : Bool}, +h: {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}) -> {pair_skip2(~A, ~cmp, ss, m, i) == True{} : Bool}:
271 %Equal.sym(Bool, kid_of(m, i), False{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}
272 h
273
274def skip2_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +hne: {kid_of(m, i) == False{} : Bool}, +h: {pair_skip2(~A, ~cmp, ss, m, i) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}:
275 L.subst(Bool, b => {Bool.pick(Bool, b, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}, kid_of(m, i), False{}, hne, h)
276
277def exc2_get(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat, +j: Nat, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {pair_skip2(~A, ~cmp, ss, j, i) == True{} : Bool}:
278 match k b:
279 case 0n _:
280 Empty.absurd({pair_skip2(~A, ~cmp, ss, j, i) == True{} : Bool}, N.lt_zero_absurd(j, hj))
281 case 1n+ +m True{}:
282 L.subst(Nat, z => {pair_skip2(~A, ~cmp, ss, z, i) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, eb)), L.and_left(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i), h))
283 case 1n+ +m False{}:
284 exc2_get(~A, ~cmp, ss, m, i, j, L.and_right(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})
285
286def exc2_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +i: Nat, +j: Nat, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, +hne: {kid_of(j, i) == False{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
287 skip2_at(~A, ~cmp, ss, j, i, hne, exc2_get(~A, ~cmp, ss, k, i, j, h, hj, Nat.is_eq(j, N.pred(k)), {==}))
288
289def pair_of_kid(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +i: Nat, c: Nat, +epc: {IX.par(c) == i : Nat}, +hcpos: {Nat.is_le(1n, c) == True{} : Bool}, +h: {mle(~A, ~cmp, slot(~A, ss, i), slot(~A, ss, c)) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, c) == True{} : Bool}:
290 match c:
291 case 0n:
292 Empty.absurd({pair_ok(~A, ~cmp, ss, 0n) == True{} : Bool}, L.true_not_false(Nat.is_le(1n, 0n), hcpos, {==}))
293 case 1n+k:
294 %Equal.sym(Nat, IX.par(1n+k), i, epc) : {mle(~A, ~cmp, slot(~A, ss, _), slot(~A, ss, 1n+k)) == True{} : Bool}
295 h
296
297# one excluded pair, from "the hole is not larger than that child"
298def pair_kid_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +i: Nat, +j: Nat, +c: Nat, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +ej: {Nat.is_eq(j, c) == True{} : Bool}, +epc: {IX.par(c) == i : Nat}, +hc: {kid_le(~A, ~cmp, ss, n, i, c) == True{} : Bool}, +hcpos: {Nat.is_le(1n, c) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
299 L.subst(Nat, z => {pair_ok(~A, ~cmp, ss, z) == True{} : Bool}, c, j, Equal.sym(Nat, j, c, N.eq_from_is_eq(j, c, ej)),
300 pair_of_kid(~A, ~cmp, ss, n, i, c, epc, hcpos, kid_le_at(~A, ~cmp, ss, n, i, c, L.subst(Nat, z => {Nat.is_lt(z, n) == True{} : Bool}, j, c, N.eq_from_is_eq(j, c, ej), hjn), hc)))
301
302def or_false(a: Bool, b: Bool, +ea: {a == False{} : Bool}, +eb: {b == False{} : Bool}) -> {Bool.or(a, b) == False{} : Bool}:
303 %Equal.sym(Bool, a, False{}, ea) : {Bool.or(_, b) == False{} : Bool}
304 eb
305
306# `ho_upto` from `ho_exc2` plus "the hole is not larger than its children"
307def ho_of_exc2_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +k: Nat, +i: Nat, +j: Nat, +hjk: {Nat.is_lt(j, k) == True{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hkids: {kids_le(~A, ~cmp, ss, n, i, i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, IX.kidl(i)) == b : Bool}, c: Bool, +ec: {Nat.is_eq(j, IX.kidr(i)) == c : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
308 match b c:
309 case True{} _:
310 pair_kid_at(~A, ~cmp, ss, n, i, j, IX.kidl(i), hjn, eb, IX.par_kidl(i), L.and_left(kid_le(~A, ~cmp, ss, n, i, IX.kidl(i)), kid_le(~A, ~cmp, ss, n, i, IX.kidr(i)), hkids), IX.kidl_pos1(i))
311 case False{} True{}:
312 pair_kid_at(~A, ~cmp, ss, n, i, j, IX.kidr(i), hjn, ec, IX.par_kidr(i), L.and_right(kid_le(~A, ~cmp, ss, n, i, IX.kidl(i)), kid_le(~A, ~cmp, ss, n, i, IX.kidr(i)), hkids), IX.kidr_pos1(i))
313 case False{} False{}:
314 exc2_at(~A, ~cmp, ss, k, i, j, h, hjk, or_false(Nat.is_eq(j, IX.kidl(i)), Nat.is_eq(j, IX.kidr(i)), eb, ec))
315
316def ho_of_exc2(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, k: Nat, +i: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hkids: {kids_le(~A, ~cmp, ss, n, i, i) == True{} : Bool}) -> {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}:
317 match k:
318 case 0n:
319 {==}
320 case 1n+ +m:
321 L.and_intro(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m),
322 ho_of_exc2_at(~A, ~cmp, ss, n, 1n+m, i, m, N.lt_succ(m), N.lt_le_trans(m, 1n+m, n, N.lt_succ(m), hk), h, hkids, Nat.is_eq(m, IX.kidl(i)), {==}, Nat.is_eq(m, IX.kidr(i)), {==}),
323 ho_of_exc2(~A, ~cmp, ss, n, m, i, N.le_trans(m, 1n+m, n, N.le_succ(m), hk), L.and_right(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i), h), hkids))