proofs/containers/binary_heap/idx.bend
bend-collections-laws-containers@1.0.0.0 · 264 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/spec/lib/common.bend as SC
5
6# Heap index arithmetic: the shape of an array heap IS its index arithmetic.
7# Element i has children 2i+1 and 2i+2 and, for i >= 1, parent (i - 1) / 2.
8# Halving carries a flag because Bend patterns only take 0n and 1n+p and
9# definitions may not be mutually recursive.
10
11def kidl(+i: Nat) -> Nat:
12 1n+Nat.double(i)
13
14def kidr(+i: Nat) -> Nat:
15 2n+Nat.double(i)
16
17def half_go(n: Nat, odd: Bool) -> Nat:
18 match n odd:
19 case 0n _:
20 0n
21 case 1n+p False{}:
22 half_go(p, True{})
23 case 1n+p True{}:
24 1n+half_go(p, False{})
25
26def half(n: Nat) -> Nat:
27 half_go(n, False{})
28
29def par(+j: Nat) -> Nat:
30 half(Nat.sub(j, 1n))
31
32# ---- halving ----
33
34def hg_false(+i: Nat) -> {half_go(Nat.double(i), False{}) == i : Nat}:
35 match i:
36 case 0n:
37 {==}
38 case 1n+p:
39 N.succ_cong(half_go(Nat.double(p), False{}), p, hg_false(p))
40
41def hg_true(+i: Nat) -> {half_go(Nat.double(i), True{}) == i : Nat}:
42 match i:
43 case 0n:
44 {==}
45 case 1n+p:
46 N.succ_cong(half_go(Nat.double(p), True{}), p, hg_true(p))
47
48def half_double(+i: Nat) -> {half(Nat.double(i)) == i : Nat}:
49 hg_false(i)
50
51def half_succ_double(+i: Nat) -> {half(1n+Nat.double(i)) == i : Nat}:
52 hg_true(i)
53
54def sub0(+n: Nat) -> {n == Nat.sub(n, 0n) : Nat}:
55 Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n))
56
57# ---- the parent of a child ----
58
59def par_kidl(+i: Nat) -> {par(kidl(i)) == i : Nat}:
60 %sub0(Nat.double(i)) : {half(_) == i : Nat}
61 half_double(i)
62
63def par_kidr(+i: Nat) -> {par(kidr(i)) == i : Nat}:
64 %sub0(1n+Nat.double(i)) : {half(_) == i : Nat}
65 half_succ_double(i)
66
67# ---- j = 2 * half(j) or 1 + 2 * half(j) ----
68
69# p = 2h => 1 + p = 1 + 2 * half(1 + p), because half(1 + 2h) = h
70def half_even_succ(+p: Nat, +ep: {p == Nat.double(half(p)) : Nat}) -> {Nat.is_eq(1n+p, 1n+Nat.double(half(1n+p))) == True{} : Bool}:
71 +h = half(p)
72 %Equal.sym(Nat, p, Nat.double(h), ep) : {Nat.is_eq(1n+_, 1n+Nat.double(half(1n+_))) == True{} : Bool}
73 %Equal.sym(Nat, half(1n+Nat.double(h)), h, half_succ_double(h)) : {Nat.is_eq(1n+Nat.double(h), 1n+Nat.double(_)) == True{} : Bool}
74 N.is_eq_refl(1n+Nat.double(h))
75
76# p = 1 + 2h => 1 + p = 2 * half(1 + p), because half(2 + 2h) = 1 + h
77def half_odd_succ(+p: Nat, +ep: {p == 1n+Nat.double(half(p)) : Nat}) -> {Nat.is_eq(1n+p, Nat.double(half(1n+p))) == True{} : Bool}:
78 +h = half(p)
79 %Equal.sym(Nat, p, 1n+Nat.double(h), ep) : {Nat.is_eq(1n+_, Nat.double(half(1n+_))) == True{} : Bool}
80 %Equal.sym(Nat, half(Nat.double(1n+h)), 1n+h, half_double(1n+h)) : {Nat.is_eq(2n+Nat.double(h), Nat.double(_)) == True{} : Bool}
81 N.is_eq_refl(2n+Nat.double(h))
82
83def half_split_succ(+p: Nat, e: {Nat.is_eq(p, Nat.double(half(p))) == True{} : Bool} | {Nat.is_eq(p, 1n+Nat.double(half(p))) == True{} : Bool}) -> {Nat.is_eq(1n+p, Nat.double(half(1n+p))) == True{} : Bool} | {Nat.is_eq(1n+p, 1n+Nat.double(half(1n+p))) == True{} : Bool}:
84 match e:
85 case Inl{ep}:
86 Inr{half_even_succ(p, N.eq_from_is_eq(p, Nat.double(half(p)), ep))}
87 case Inr{ep}:
88 Inl{half_odd_succ(p, N.eq_from_is_eq(p, 1n+Nat.double(half(p)), ep))}
89
90def half_split(+j: Nat) -> {Nat.is_eq(j, Nat.double(half(j))) == True{} : Bool} | {Nat.is_eq(j, 1n+Nat.double(half(j))) == True{} : Bool}:
91 match j:
92 case 0n:
93 Inl{{==}}
94 case 1n+p:
95 half_split_succ(p, half_split(p))
96
97# ---- every index >= 1 is the left or the right child of its parent ----
98
99def kid_left(+p: Nat, +ep: {p == Nat.double(half(p)) : Nat}) -> {1n+p == kidl(par(1n+p)) : Nat}:
100 %sub0(p) : {1n+p == kidl(half(_)) : Nat}
101 N.succ_cong(p, Nat.double(half(p)), ep)
102
103def kid_right(+p: Nat, +ep: {p == 1n+Nat.double(half(p)) : Nat}) -> {1n+p == kidr(par(1n+p)) : Nat}:
104 %sub0(p) : {1n+p == kidr(half(_)) : Nat}
105 N.succ_cong(p, 1n+Nat.double(half(p)), ep)
106
107def kid_split_succ(+p: Nat, e: {Nat.is_eq(p, Nat.double(half(p))) == True{} : Bool} | {Nat.is_eq(p, 1n+Nat.double(half(p))) == True{} : Bool}) -> {1n+p == kidl(par(1n+p)) : Nat} | {1n+p == kidr(par(1n+p)) : Nat}:
108 match e:
109 case Inl{ep}:
110 Inl{kid_left(p, N.eq_from_is_eq(p, Nat.double(half(p)), ep))}
111 case Inr{ep}:
112 Inr{kid_right(p, N.eq_from_is_eq(p, 1n+Nat.double(half(p)), ep))}
113
114def kid_split(+j: Nat, +hj: {Nat.is_lt(0n, j) == True{} : Bool}) -> {j == kidl(par(j)) : Nat} | {j == kidr(par(j)) : Nat}:
115 match j:
116 case 0n:
117 Empty.absurd({0n == kidl(par(0n)) : Nat} | {0n == kidr(par(0n)) : Nat}, L.true_not_false(Nat.is_lt(0n, 0n), hj, N.lt_irrefl(0n)))
118 case 1n+p:
119 kid_split_succ(p, half_split(p))
120
121# ---- a parent index is smaller than its child index ----
122
123def double_le(+i: Nat) -> {Nat.is_le(i, Nat.double(i)) == True{} : Bool}:
124 match i:
125 case 0n:
126 {==}
127 case 1n+p:
128 N.le_trans(p, Nat.double(p), 1n+Nat.double(p), double_le(p), N.le_succ(Nat.double(p)))
129
130def kidl_gt(+i: Nat) -> {Nat.is_lt(i, kidl(i)) == True{} : Bool}:
131 N.le_lt_succ(i, Nat.double(i), double_le(i))
132
133def kidr_gt(+i: Nat) -> {Nat.is_lt(i, kidr(i)) == True{} : Bool}:
134 N.lt_trans(i, kidl(i), kidr(i), kidl_gt(i), N.lt_succ(kidl(i)))
135
136def kidl_pos(+i: Nat) -> {Nat.is_lt(0n, kidl(i)) == True{} : Bool}:
137 N.le_lt_succ(0n, Nat.double(i), N.zero_le(Nat.double(i)))
138
139def kidr_pos(+i: Nat) -> {Nat.is_lt(0n, kidr(i)) == True{} : Bool}:
140 N.le_lt_succ(0n, 1n+Nat.double(i), N.zero_le(1n+Nat.double(i)))
141
142def par_lt_of(+j: Nat, e: {j == kidl(par(j)) : Nat} | {j == kidr(par(j)) : Nat}) -> {Nat.is_lt(par(j), j) == True{} : Bool}:
143 match e:
144 case Inl{ej}:
145 L.subst(Nat, z => {Nat.is_lt(par(j), z) == True{} : Bool}, kidl(par(j)), j, Equal.sym(Nat, j, kidl(par(j)), ej), kidl_gt(par(j)))
146 case Inr{ej}:
147 L.subst(Nat, z => {Nat.is_lt(par(j), z) == True{} : Bool}, kidr(par(j)), j, Equal.sym(Nat, j, kidr(par(j)), ej), kidr_gt(par(j)))
148
149def par_lt(+j: Nat, +hj: {Nat.is_lt(0n, j) == True{} : Bool}) -> {Nat.is_lt(par(j), j) == True{} : Bool}:
150 par_lt_of(j, kid_split(j, hj))
151
152def kidl_pos1(+y: Nat) -> {Nat.is_le(1n, kidl(y)) == True{} : Bool}:
153 N.zero_le(Nat.double(y))
154
155def kidr_pos1(+y: Nat) -> {Nat.is_le(1n, kidr(y)) == True{} : Bool}:
156 N.zero_le(1n+Nat.double(y))
157
158# ---- halving a bound ----
159
160def double_le_of(+j: Nat, e: {Nat.is_eq(j, Nat.double(half(j))) == True{} : Bool} | {Nat.is_eq(j, 1n+Nat.double(half(j))) == True{} : Bool}) -> {Nat.is_le(Nat.double(half(j)), j) == True{} : Bool}:
161 match e:
162 case Inl{ej}:
163 N.eq_le(Nat.double(half(j)), j, Equal.sym(Nat, j, Nat.double(half(j)), N.eq_from_is_eq(j, Nat.double(half(j)), ej)))
164 case Inr{ej}:
165 L.subst(Nat, z => {Nat.is_le(Nat.double(half(j)), z) == True{} : Bool}, 1n+Nat.double(half(j)), j, Equal.sym(Nat, j, 1n+Nat.double(half(j)), N.eq_from_is_eq(j, 1n+Nat.double(half(j)), ej)), N.le_succ(Nat.double(half(j))))
166
167def double_le_self(+j: Nat) -> {Nat.is_le(Nat.double(half(j)), j) == True{} : Bool}:
168 double_le_of(j, half_split(j))
169
170def double_lt_inj(+a: Nat, +b: Nat, +h: {Nat.is_lt(Nat.double(a), Nat.double(b)) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
171 match a b:
172 case _ 0n:
173 Empty.absurd({Nat.is_lt(a, 0n) == True{} : Bool}, N.lt_zero_absurd(Nat.double(a), h))
174 case 0n 1n+q:
175 {==}
176 case 1n+p 1n+q:
177 double_lt_inj(p, q, h)
178
179def sub_le_self(+j: Nat) -> {Nat.is_le(Nat.sub(j, 1n), j) == True{} : Bool}:
180 match j:
181 case 0n:
182 {==}
183 case 1n+k:
184 %Equal.sym(Nat, Nat.sub(k, 0n), k, N.sub_zero(k)) : {Nat.is_le(_, 1n+k) == True{} : Bool}
185 N.le_succ(k)
186
187# the parent of an index below 2^(k+1) is below 2^k
188def par_bound(+i: Nat, +k: Nat, +h: {Nat.is_lt(i, SC.pow2(1n+k)) == True{} : Bool}) -> {Nat.is_lt(par(i), SC.pow2(k)) == True{} : Bool}:
189 double_lt_inj(half(Nat.sub(i, 1n)), SC.pow2(k),
190 N.le_lt_trans(Nat.double(half(Nat.sub(i, 1n))), Nat.sub(i, 1n), Nat.double(SC.pow2(k)), double_le_self(Nat.sub(i, 1n)),
191 N.le_lt_trans(Nat.sub(i, 1n), i, Nat.double(SC.pow2(k)), sub_le_self(i), h)))
192
193def double_lt(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.double(a), Nat.double(b)) == True{} : Bool}:
194 match a b:
195 case _ 0n:
196 Empty.absurd({Nat.is_lt(Nat.double(a), 0n) == True{} : Bool}, N.lt_zero_absurd(a, h))
197 case 0n 1n+q:
198 {==}
199 case 1n+p 1n+q:
200 double_lt(p, q, h)
201
202# one more than an even number below an even number is still below it
203def double_lt_succ(+a: Nat, +q: Nat, +h: {Nat.is_lt(Nat.double(a), Nat.double(q)) == True{} : Bool}) -> {Nat.is_lt(1n+Nat.double(a), Nat.double(q)) == True{} : Bool}:
204 match a q:
205 case _ 0n:
206 Empty.absurd({Nat.is_lt(1n+Nat.double(a), 0n) == True{} : Bool}, N.lt_zero_absurd(Nat.double(a), h))
207 case 0n 1n+r:
208 {==}
209 case 1n+p 1n+r:
210 double_lt_succ(p, r, h)
211
212# a child index of an index below 2^d is below 2^(d+1)
213def kidl_bound(+i: Nat, +d: Nat, +h: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(kidl(i), SC.pow2(1n+d)) == True{} : Bool}:
214 double_lt_succ(i, SC.pow2(d), double_lt(i, SC.pow2(d), h))
215
216# l + 1 < n is l < n - 1
217def succ_lt_sub(+l: Nat, +n: Nat) -> {Nat.is_lt(1n+l, n) == Nat.is_lt(l, Nat.sub(n, 1n)) : Bool}:
218 match n:
219 case 0n:
220 Equal.sym(Bool, Nat.is_lt(l, 0n), False{}, N.not_lt_zero(l))
221 case 1n+m:
222 %Equal.sym(Nat, Nat.sub(m, 0n), m, N.sub_zero(m)) : {Nat.is_lt(1n+l, 1n+m) == Nat.is_lt(l, _) : Bool}
223 {==}
224
225# ---- how much room a sift-down still has ----
226#
227# `scale(f, m)` is m * 2^f, written by structural recursion so that no
228# multiplication appears. The sift-down invariant is `n <= scale(fuel, i + 1)`:
229# the hole index at least doubles at every step, so the loop cannot run out of
230# fuel before it runs out of children.
231
232def scale(f: Nat, m: Nat) -> Nat:
233 match f:
234 case 0n:
235 m
236 case 1n+g:
237 scale(g, Nat.double(m))
238
239def double_le_mono(+a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.double(a), Nat.double(b)) == True{} : Bool}:
240 match a b:
241 case 0n _:
242 N.zero_le(Nat.double(b))
243 case 1n+p 0n:
244 Empty.absurd({Nat.is_le(Nat.double(1n+p), 0n) == True{} : Bool}, L.false_true(h))
245 case 1n+p 1n+q:
246 double_le_mono(p, q, h)
247
248def scale_mono(f: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(scale(f, a), scale(f, b)) == True{} : Bool}:
249 match f:
250 case 0n:
251 h
252 case 1n+g:
253 scale_mono(g, Nat.double(a), Nat.double(b), double_le_mono(a, b, h))
254
255def kid_double_of(+i: Nat, +c: Nat, +ep: {par(c) == i : Nat}, e: {c == kidl(par(c)) : Nat} | {c == kidr(par(c)) : Nat}) -> {Nat.is_le(Nat.double(1n+i), 1n+c) == True{} : Bool}:
256 match e:
257 case Inl{ec}:
258 L.subst(Nat, z => {Nat.is_le(Nat.double(1n+i), 1n+z) == True{} : Bool}, kidl(i), c, Equal.sym(Nat, c, kidl(i), L.subst(Nat, z => {c == kidl(z) : Nat}, par(c), i, ep, ec)), N.le_refl(2n+Nat.double(i)))
259 case Inr{ec}:
260 L.subst(Nat, z => {Nat.is_le(Nat.double(1n+i), 1n+z) == True{} : Bool}, kidr(i), c, Equal.sym(Nat, c, kidr(i), L.subst(Nat, z => {c == kidr(z) : Nat}, par(c), i, ep, ec)), N.le_succ(2n+Nat.double(i)))
261
262# a child index is at least twice the parent's, so 1 + kid >= 2 * (1 + i)
263def kid_double(+i: Nat, +c: Nat, +ep: {par(c) == i : Nat}, +hcpos: {Nat.is_le(1n, c) == True{} : Bool}) -> {Nat.is_le(Nat.double(1n+i), 1n+c) == True{} : Bool}:
264 kid_double_of(i, c, ep, kid_split(c, N.succ_le_lt(0n, c, hcpos)))