1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/list.bend as LL
5	import ../../lib/array.bend as AR
6	import ../../../spec/lib/common.bend as SC
7	import ../../../spec/containers/binary_heap.bend as S
8	import ../../../src/containers/binary_heap.bend as H
9	import ./idx.bend as IX
10	import ./slots.bend as SL
11	import ./vals.bend as V
12	import ./root.bend as RT
13	
14	# Doubling the block: the old block becomes the lower half of a block one
15	# level deeper, so every element keeps its index and nothing about the heap
16	# changes except the capacity. These are the lemmas that say so.
17	
18	def slots_grown(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>) -> {AR.slots(Maybe<&2, A>, AR.TNode{t, AR.trep(Maybe<&2, A>, d, None{})}) == SC.append(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), SC.replicate(Maybe<&2, A>, SC.pow2(d), None{})) : List<&2, Maybe<&2, A>>}:
19	  %Equal.sym(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, AR.trep(Maybe<&2, A>, d, None{})), SC.replicate(Maybe<&2, A>, SC.pow2(d), None{}), AR.trep_slots(Maybe<&2, A>, d, None{})) : {SC.append(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), _) == SC.append(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), SC.replicate(Maybe<&2, A>, SC.pow2(d), None{})) : List<&2, Maybe<&2, A>>}
20	  {==}
21	
22	# A slot inside the old block reads the same through the appended one.
23	def slot_left(~A: Data, +ss: List<&2, Maybe<&2, A>>, +ys: List<&2, Maybe<&2, A>>, +j: Nat, +h: {Nat.is_lt(j, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {SL.slot(~A, SC.append(Maybe<&2, A>, ss, ys), j) == SL.slot(~A, ss, j) : Maybe<&2, A>}:
24	  Equal.cong(Maybe<&2, Maybe<&2, A>>, Maybe<&2, A>, m => SL.unwrap(~A, m), SC.nth(Maybe<&2, A>, SC.append(Maybe<&2, A>, ss, ys), j), SC.nth(Maybe<&2, A>, ss, j), LL.nth_append_left(Maybe<&2, A>, ss, ys, j, h))
25	
26	def lay_grow(~A: Data, +ss: List<&2, Maybe<&2, A>>, +ys: List<&2, Maybe<&2, A>>, k: Nat, +hk: {Nat.is_le(k, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}, +h: {SL.lay(~A, ss, k) == True{} : Bool}) -> {SL.lay(~A, SC.append(Maybe<&2, A>, ss, ys), k) == True{} : Bool}:
27	  match k:
28	    case 0n:
29	      {==}
30	    case 1n+ +m:
31	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.append(Maybe<&2, A>, ss, ys), m), SL.slot(~A, ss, m), slot_left(~A, ss, ys, m, N.succ_le_lt(m, SC.length(Maybe<&2, A>, ss), hk))) : {Bool.and(Maybe.is_some(&2, A, _), SL.lay(~A, SC.append(Maybe<&2, A>, ss, ys), m)) == True{} : Bool}
32	      L.and_intro(Maybe.is_some(&2, A, SL.slot(~A, ss, m)), SL.lay(~A, SC.append(Maybe<&2, A>, ss, ys), m),
33	        L.and_left(Maybe.is_some(&2, A, SL.slot(~A, ss, m)), SL.lay(~A, ss, m), h),
34	        lay_grow(~A, ss, ys, m, N.le_trans(m, 1n+m, SC.length(Maybe<&2, A>, ss), N.le_succ(m), hk), L.and_right(Maybe.is_some(&2, A, SL.slot(~A, ss, m)), SL.lay(~A, ss, m), h)))
35	
36	# one heap-order pair, read through the appended block
37	def pair_grow(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +ys: List<&2, Maybe<&2, A>>, m: Nat, +hm: {Nat.is_lt(m, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}, +h: {SL.pair_ok(~A, ~cmp, ss, m) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, SC.append(Maybe<&2, A>, ss, ys), m) == True{} : Bool}:
38	  match m:
39	    case 0n:
40	      {==}
41	    case 1n+ +p:
42	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.append(Maybe<&2, A>, ss, ys), 1n+p), SL.slot(~A, ss, 1n+p), slot_left(~A, ss, ys, 1n+p, hm)) : {SL.mle(~A, ~cmp, SL.slot(~A, SC.append(Maybe<&2, A>, ss, ys), IX.par(1n+p)), _) == True{} : Bool}
43	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.append(Maybe<&2, A>, ss, ys), IX.par(1n+p)), SL.slot(~A, ss, IX.par(1n+p)), slot_left(~A, ss, ys, IX.par(1n+p), N.lt_trans(IX.par(1n+p), 1n+p, SC.length(Maybe<&2, A>, ss), IX.par_lt(1n+p, {==}), hm))) : {SL.mle(~A, ~cmp, _, SL.slot(~A, ss, 1n+p)) == True{} : Bool}
44	      h
45	
46	def ho_grow(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +ys: List<&2, Maybe<&2, A>>, k: Nat, +hk: {Nat.is_le(k, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}, +h: {SL.ho_upto(~A, ~cmp, ss, k) == True{} : Bool}) -> {SL.ho_upto(~A, ~cmp, SC.append(Maybe<&2, A>, ss, ys), k) == True{} : Bool}:
47	  match k:
48	    case 0n:
49	      {==}
50	    case 1n+ +m:
51	      L.and_intro(SL.pair_ok(~A, ~cmp, SC.append(Maybe<&2, A>, ss, ys), m), SL.ho_upto(~A, ~cmp, SC.append(Maybe<&2, A>, ss, ys), m),
52	        pair_grow(~A, ~cmp, ss, ys, m, N.succ_le_lt(m, SC.length(Maybe<&2, A>, ss), hk), L.and_left(SL.pair_ok(~A, ~cmp, ss, m), SL.ho_upto(~A, ~cmp, ss, m), h)),
53	        ho_grow(~A, ~cmp, ss, ys, m, N.le_trans(m, 1n+m, SC.length(Maybe<&2, A>, ss), N.le_succ(m), hk), L.and_right(SL.pair_ok(~A, ~cmp, ss, m), SL.ho_upto(~A, ~cmp, ss, m), h)))
54	
55	def vals_grow(~A: Data, +ss: List<&2, Maybe<&2, A>>, +ys: List<&2, Maybe<&2, A>>, k: Nat, +hk: {Nat.is_le(k, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {V.vals(~A, SC.append(Maybe<&2, A>, ss, ys), k) == V.vals(~A, ss, k) : List<&2, A>}:
56	  match k:
57	    case 0n:
58	      {==}
59	    case 1n+ +m:
60	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.append(Maybe<&2, A>, ss, ys), m), SL.slot(~A, ss, m), slot_left(~A, ss, ys, m, N.succ_le_lt(m, SC.length(Maybe<&2, A>, ss), hk))) : {V.cons_slot(~A, _, V.vals(~A, SC.append(Maybe<&2, A>, ss, ys), m)) == V.vals(~A, ss, 1n+m) : List<&2, A>}
61	      Equal.cong(List<&2, A>, List<&2, A>, zs => V.cons_slot(~A, SL.slot(~A, ss, m), zs), V.vals(~A, SC.append(Maybe<&2, A>, ss, ys), m), V.vals(~A, ss, m), vals_grow(~A, ss, ys, m, N.le_trans(m, 1n+m, SC.length(Maybe<&2, A>, ss), N.le_succ(m), hk)))
62	
63	# ---- the grown block, as a tree ----
64	
65	def gtree(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>) -> AR.Tree<Maybe<&2, A>>:
66	  AR.TNode{t, AR.trep(Maybe<&2, A>, d, None{})}
67	
68	def gtree_perfect(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {AR.perfect(Maybe<&2, A>, 1n+d, gtree(~A, d, t)) == True{} : Bool}:
69	  L.and_intro(AR.perfect(Maybe<&2, A>, d, t), AR.perfect(Maybe<&2, A>, d, AR.trep(Maybe<&2, A>, d, None{})), pf, AR.trep_perfect(Maybe<&2, A>, d, None{}))
70	
71	def gtree_real(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>) -> {H.grown(~A, d, AR.thaw(Maybe<&2, A>, t)) == AR.thaw(Maybe<&2, A>, gtree(~A, d, t)) : Array<Maybe<&2, A>>}:
72	  Equal.cong(Array<Maybe<&2, A>>, Array<Maybe<&2, A>>, a => ANode{AR.thaw(Maybe<&2, A>, t), a}, H.empty_slots(~A, d), AR.thaw(Maybe<&2, A>, AR.trep(Maybe<&2, A>, d, None{})), AR.new(Maybe<&2, A>, d, None{}))
73	
74	def gtree_lay(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +k: Nat, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hk: {Nat.is_le(k, SC.pow2(d)) == True{} : Bool}, +h: {SL.lay(~A, AR.slots(Maybe<&2, A>, t), k) == True{} : Bool}) -> {SL.lay(~A, AR.slots(Maybe<&2, A>, gtree(~A, d, t)), k) == True{} : Bool}:
75	  %Equal.sym(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, gtree(~A, d, t)), SC.append(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), SC.replicate(Maybe<&2, A>, SC.pow2(d), None{})), slots_grown(~A, d, t)) : {SL.lay(~A, _, k) == True{} : Bool}
76	  lay_grow(~A, AR.slots(Maybe<&2, A>, t), SC.replicate(Maybe<&2, A>, SC.pow2(d), None{}), k,
77	    L.subst(Nat, z => {Nat.is_le(k, z) == True{} : Bool}, SC.pow2(d), SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), Equal.sym(Nat, SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), SC.pow2(d), AR.slots_length(Maybe<&2, A>, d, t, pf)), hk), h)
78	
79	def gtree_ho(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +k: Nat, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hk: {Nat.is_le(k, SC.pow2(d)) == True{} : Bool}, +h: {SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), k) == True{} : Bool}) -> {SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, gtree(~A, d, t)), k) == True{} : Bool}:
80	  %Equal.sym(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, gtree(~A, d, t)), SC.append(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), SC.replicate(Maybe<&2, A>, SC.pow2(d), None{})), slots_grown(~A, d, t)) : {SL.ho_upto(~A, ~cmp, _, k) == True{} : Bool}
81	  ho_grow(~A, ~cmp, AR.slots(Maybe<&2, A>, t), SC.replicate(Maybe<&2, A>, SC.pow2(d), None{}), k,
82	    L.subst(Nat, z => {Nat.is_le(k, z) == True{} : Bool}, SC.pow2(d), SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), Equal.sym(Nat, SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), SC.pow2(d), AR.slots_length(Maybe<&2, A>, d, t, pf)), hk), h)
83	
84	def gtree_vals(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +k: Nat, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hk: {Nat.is_le(k, SC.pow2(d)) == True{} : Bool}) -> {V.vals(~A, AR.slots(Maybe<&2, A>, gtree(~A, d, t)), k) == V.vals(~A, AR.slots(Maybe<&2, A>, t), k) : List<&2, A>}:
85	  %Equal.sym(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, gtree(~A, d, t)), SC.append(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), SC.replicate(Maybe<&2, A>, SC.pow2(d), None{})), slots_grown(~A, d, t)) : {V.vals(~A, _, k) == V.vals(~A, AR.slots(Maybe<&2, A>, t), k) : List<&2, A>}
86	  vals_grow(~A, AR.slots(Maybe<&2, A>, t), SC.replicate(Maybe<&2, A>, SC.pow2(d), None{}), k,
87	    L.subst(Nat, z => {Nat.is_le(k, z) == True{} : Bool}, SC.pow2(d), SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), Equal.sym(Nat, SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), SC.pow2(d), AR.slots_length(Maybe<&2, A>, d, t, pf)), hk))