proofs/containers/binary_heap/vals.bend
bend-collections-laws-containers@1.0.0.0 · 96 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/multiset.bend as M
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
11
12# The multiset of an array heap: the values of the slots [0, n), sorted by
13# insertion. Sorting is what the specification calls a priority queue, and
14# `M.ins_comm` says the order the values are inserted in does not matter --
15# which is exactly why every swap a sift performs is invisible here.
16
17def cons_slot(~A: Data, m: Maybe<&2, A>, acc: List<&2, A>) -> List<&2, A>:
18 match m:
19 case None{}:
20 acc
21 case Some{v}:
22 Con{v, acc}
23
24def vals(~A: Data, +ss: List<&2, Maybe<&2, A>>, n: Nat) -> List<&2, A>:
25 match n:
26 case 0n:
27 Nil{}
28 case 1n+ +m:
29 cons_slot(~A, SL.slot(~A, ss, m), vals(~A, ss, m))
30
31def msort(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>) -> List<&2, A>:
32 match xs:
33 case Nil{}:
34 Nil{}
35 case Con{h, t}:
36 S.ins(~A, ~cmp, h, msort(~A, ~cmp, t))
37
38# ---- the slots below an update are untouched ----
39
40def vals_above(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +v: Maybe<&2, A>, m: Nat, +h: {Nat.is_le(m, i) == True{} : Bool}) -> {vals(~A, SC.update(Maybe<&2, A>, ss, i, v), m) == vals(~A, ss, m) : List<&2, A>}:
41 match m:
42 case 0n:
43 {==}
44 case 1n+ +k:
45 %Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.update(Maybe<&2, A>, ss, i, v), k), SL.slot(~A, ss, k), SL.slot_other(~A, ss, i, k, v, SL.ne_sym(i, k, N.is_eq_lt(k, i, N.succ_le_lt(k, i, h))))) : {cons_slot(~A, _, vals(~A, SC.update(Maybe<&2, A>, ss, i, v), k)) == vals(~A, ss, 1n+k) : List<&2, A>}
46 Equal.cong(List<&2, A>, List<&2, A>, ys => cons_slot(~A, SL.slot(~A, ss, k), ys), vals(~A, SC.update(Maybe<&2, A>, ss, i, v), k), vals(~A, ss, k), vals_above(~A, ss, i, v, k, N.lt_le(k, i, N.succ_le_lt(k, i, h))))
47
48# ---- sorting a list with one slot replaced ----
49
50def none_not_some(~A: Data, +old: A, +h: {None{} == Some{old} : Maybe<&2, A>}) -> Empty:
51 L.true_not_false(Maybe.is_some(&2, A, None{}), Equal.cong(Maybe<&2, A>, Bool, z => Maybe.is_some(&2, A, z), None{}, Some{old}, h), {==})
52
53def nth_of_slot_go(~A: Data, +old: A, m: Maybe<&2, Maybe<&2, A>>, +hold: {SL.unwrap(~A, m) == Some{old} : Maybe<&2, A>}) -> {m == Some{Some{old}} : Maybe<&2, Maybe<&2, A>>}:
54 match m:
55 case None{}:
56 Empty.absurd({None{} == Some{Some{old}} : Maybe<&2, Maybe<&2, A>>}, none_not_some(~A, old, hold))
57 case Some{s}:
58 Equal.cong(Maybe<&2, A>, Maybe<&2, Maybe<&2, A>>, z => Some{z}, s, Some{old}, hold)
59
60def nth_of_slot(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +old: A, +hold: {SL.slot(~A, ss, i) == Some{old} : Maybe<&2, A>}) -> {SC.nth(Maybe<&2, A>, ss, i) == Some{Some{old}} : Maybe<&2, Maybe<&2, A>>}:
61 nth_of_slot_go(~A, old, SC.nth(Maybe<&2, A>, ss, i), hold)
62
63def slot_in_range(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +old: A, +hold: {SL.slot(~A, ss, i) == Some{old} : Maybe<&2, A>}) -> {Nat.is_lt(i, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}:
64 LL.nth_lt_length(Maybe<&2, A>, ss, i, Some{old}, nth_of_slot(~A, ss, i, old, hold))
65
66def ins_set_same(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +i: Nat, +old: A, +v: A, +hold: {SL.slot(~A, ss, i) == Some{old} : Maybe<&2, A>}) -> {S.ins(~A, ~cmp, old, msort(~A, ~cmp, vals(~A, SC.update(Maybe<&2, A>, ss, i, Some{v}), 1n+i))) == S.ins(~A, ~cmp, v, msort(~A, ~cmp, vals(~A, ss, 1n+i))) : List<&2, A>}:
67 +up = SC.update(Maybe<&2, A>, ss, i, Some{v})
68 %Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.update(Maybe<&2, A>, ss, i, Some{v}), i), Some{v}, SL.slot_same(~A, ss, i, Some{v}, slot_in_range(~A, ss, i, old, hold))) : {S.ins(~A, ~cmp, old, msort(~A, ~cmp, cons_slot(~A, _, vals(~A, up, i)))) == S.ins(~A, ~cmp, v, msort(~A, ~cmp, vals(~A, ss, 1n+i))) : List<&2, A>}
69 %Equal.sym(List<&2, A>, vals(~A, SC.update(Maybe<&2, A>, ss, i, Some{v}), i), vals(~A, ss, i), vals_above(~A, ss, i, Some{v}, i, N.le_refl(i))) : {S.ins(~A, ~cmp, old, msort(~A, ~cmp, cons_slot(~A, Some{v}, _))) == S.ins(~A, ~cmp, v, msort(~A, ~cmp, vals(~A, ss, 1n+i))) : List<&2, A>}
70 %Equal.sym(Maybe<&2, A>, SL.slot(~A, ss, i), Some{old}, hold) : {S.ins(~A, ~cmp, old, S.ins(~A, ~cmp, v, msort(~A, ~cmp, vals(~A, ss, i)))) == S.ins(~A, ~cmp, v, msort(~A, ~cmp, cons_slot(~A, _, vals(~A, ss, i)))) : List<&2, A>}
71 M.ins_comm(~A, ~cmp, ~o, old, v, msort(~A, ~cmp, vals(~A, ss, i)))
72
73def ins_set_top(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +old: A, +v: A, +ei: {i == m : Nat}, +hold: {SL.slot(~A, ss, i) == Some{old} : Maybe<&2, A>}) -> {S.ins(~A, ~cmp, old, msort(~A, ~cmp, vals(~A, SC.update(Maybe<&2, A>, ss, i, Some{v}), 1n+m))) == S.ins(~A, ~cmp, v, msort(~A, ~cmp, vals(~A, ss, 1n+m))) : List<&2, A>}:
74 %ei : {S.ins(~A, ~cmp, old, msort(~A, ~cmp, vals(~A, SC.update(Maybe<&2, A>, ss, i, Some{v}), 1n+_))) == S.ins(~A, ~cmp, v, msort(~A, ~cmp, vals(~A, ss, 1n+_))) : List<&2, A>}
75 ins_set_same(~A, ~cmp, ~o, ss, i, old, v, hold)
76
77def ins_set_cons(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), s: Maybe<&2, A>, +old: A, +v: A, +xs: List<&2, A>, +ys: List<&2, A>, +ih: {S.ins(~A, ~cmp, old, msort(~A, ~cmp, xs)) == S.ins(~A, ~cmp, v, msort(~A, ~cmp, ys)) : List<&2, A>}) -> {S.ins(~A, ~cmp, old, msort(~A, ~cmp, cons_slot(~A, s, xs))) == S.ins(~A, ~cmp, v, msort(~A, ~cmp, cons_slot(~A, s, ys))) : List<&2, A>}:
78 match s:
79 case None{}:
80 ih
81 case Some{+w}:
82 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, old, S.ins(~A, ~cmp, w, msort(~A, ~cmp, xs))), S.ins(~A, ~cmp, w, S.ins(~A, ~cmp, old, msort(~A, ~cmp, xs))), M.ins_comm(~A, ~cmp, ~o, old, w, msort(~A, ~cmp, xs))) : {_ == S.ins(~A, ~cmp, v, S.ins(~A, ~cmp, w, msort(~A, ~cmp, ys))) : List<&2, A>}
83 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, v, S.ins(~A, ~cmp, w, msort(~A, ~cmp, ys))), S.ins(~A, ~cmp, w, S.ins(~A, ~cmp, v, msort(~A, ~cmp, ys))), M.ins_comm(~A, ~cmp, ~o, v, w, msort(~A, ~cmp, ys))) : {S.ins(~A, ~cmp, w, S.ins(~A, ~cmp, old, msort(~A, ~cmp, xs))) == _ : List<&2, A>}
84 Equal.cong(List<&2, A>, List<&2, A>, zs => S.ins(~A, ~cmp, w, zs), S.ins(~A, ~cmp, old, msort(~A, ~cmp, xs)), S.ins(~A, ~cmp, v, msort(~A, ~cmp, ys)), ih)
85
86def ins_set(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, n: Nat, +i: Nat, +old: A, +v: A, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hold: {SL.slot(~A, ss, i) == Some{old} : Maybe<&2, A>}, b: Bool, +eb: {Nat.is_eq(i, N.pred(n)) == b : Bool}) -> {S.ins(~A, ~cmp, old, msort(~A, ~cmp, vals(~A, SC.update(Maybe<&2, A>, ss, i, Some{v}), n))) == S.ins(~A, ~cmp, v, msort(~A, ~cmp, vals(~A, ss, n))) : List<&2, A>}:
87 match n b:
88 case 0n _:
89 Empty.absurd({S.ins(~A, ~cmp, old, msort(~A, ~cmp, vals(~A, SC.update(Maybe<&2, A>, ss, i, Some{v}), 0n))) == S.ins(~A, ~cmp, v, msort(~A, ~cmp, vals(~A, ss, 0n))) : List<&2, A>}, N.lt_zero_absurd(i, hi))
90 case 1n+m True{}:
91 ins_set_top(~A, ~cmp, ~o, ss, m, i, old, v, N.eq_from_is_eq(i, m, eb), hold)
92 case 1n+ +m False{}:
93 +up = SC.update(Maybe<&2, A>, ss, i, Some{v})
94 +hi2 = N.lt_or_eq(i, m, N.lt_succ_le(i, m, hi), eb)
95 %Equal.sym(Maybe<&2, A>, SL.slot(~A, up, m), SL.slot(~A, ss, m), SL.slot_other(~A, ss, i, m, Some{v}, N.is_eq_lt(i, m, hi2))) : {S.ins(~A, ~cmp, old, msort(~A, ~cmp, cons_slot(~A, _, vals(~A, up, m)))) == S.ins(~A, ~cmp, v, msort(~A, ~cmp, vals(~A, ss, 1n+m))) : List<&2, A>}
96 ins_set_cons(~A, ~cmp, ~o, SL.slot(~A, ss, m), old, v, vals(~A, up, m), vals(~A, ss, m), ins_set(~A, ~cmp, ~o, ss, m, i, old, v, hi2, hold, Nat.is_eq(i, N.pred(m)), {==}))