1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../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	
11	def kidl(+i: Nat) -> Nat:
12	  1n+Nat.double(i)
13	
14	def kidr(+i: Nat) -> Nat:
15	  2n+Nat.double(i)
16	
17	def 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	
26	def half(n: Nat) -> Nat:
27	  half_go(n, False{})
28	
29	def par(+j: Nat) -> Nat:
30	  half(Nat.sub(j, 1n))
31	
32	# ---- halving ----
33	
34	def 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	
41	def 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	
48	def half_double(+i: Nat) -> {half(Nat.double(i)) == i : Nat}:
49	  hg_false(i)
50	
51	def half_succ_double(+i: Nat) -> {half(1n+Nat.double(i)) == i : Nat}:
52	  hg_true(i)
53	
54	def 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	
59	def par_kidl(+i: Nat) -> {par(kidl(i)) == i : Nat}:
60	  %sub0(Nat.double(i)) : {half(_) == i : Nat}
61	  half_double(i)
62	
63	def 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
70	def 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
77	def 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	
83	def 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	
90	def 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	
99	def 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	
103	def 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	
107	def 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	
114	def 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	
123	def 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	
130	def 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	
133	def 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	
136	def 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	
139	def 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	
142	def 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	
149	def 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	
152	def kidl_pos1(+y: Nat) -> {Nat.is_le(1n, kidl(y)) == True{} : Bool}:
153	  N.zero_le(Nat.double(y))
154	
155	def 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	
160	def 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	
167	def double_le_self(+j: Nat) -> {Nat.is_le(Nat.double(half(j)), j) == True{} : Bool}:
168	  double_le_of(j, half_split(j))
169	
170	def 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	
179	def 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
188	def 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	
193	def 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
203	def 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)
213	def 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
217	def 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	
232	def 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	
239	def 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	
248	def 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	
255	def 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)
263	def 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)))