proofs/containers/binary_heap/grow.bend
bend-collections-laws-containers@1.0.0.0 · 87 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/array.bend as AR
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/src/containers/binary_heap.bend as H
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/idx.bend as IX
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/slots.bend as SL
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/vals.bend as V
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/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
18def 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.
23def 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
26def 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
37def 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
46def 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
55def 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
65def 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
68def 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
71def 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
74def 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
79def 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
84def 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))