proofs/containers/binary_heap/bag.bend
bend-collections-laws-containers@1.0.0.0 · 108 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/slots.bend as SL
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/vals.bend as V
11
12# Cancellation for sorted insertion, and what it gives: swapping the values of
13# two slots does not change the sorted multiset. That is the whole reason a
14# sift may move values along a path -- every step is a swap.
15
16# The first element that compares EQ to z is removed. `b` is "does the head
17# compare EQ to z": a loop that branches on a computed value has to carry the
18# decision in its arguments (Bend matches only on parameters).
19# z is removed from a list it was just inserted into.
20def del_head(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +z: A, +xs: List<&2, A>) -> {S.delf(~A, ~cmp, z, Con{z, xs}) == xs : List<&2, A>}:
21 %Equal.sym(Cmp, cmp(z, z), EQ{}, O.refl(~A, ~cmp, ~o, z)) : {S.del(~A, ~cmp, z, Con{z, xs}, Cmp.is_eq(_)) == xs : List<&2, A>}
22 {==}
23
24def not_le_not_eq_c(c: Cmp, +e: {Cmp.is_le(c) == False{} : Bool}) -> {Cmp.is_eq(c) == False{} : Bool}:
25 match c:
26 case LT{}:
27 Empty.absurd({Cmp.is_eq(LT{}) == False{} : Bool}, L.true_false(e))
28 case EQ{}:
29 Empty.absurd({Cmp.is_eq(EQ{}) == False{} : Bool}, L.true_false(e))
30 case GT{}:
31 {==}
32
33def not_le_not_eq(~A: Data, ~cmp: A -> A -> Cmp, +z: A, +h: A, +e: {S.le(~A, ~cmp, z, h) == False{} : Bool}) -> {Cmp.is_eq(cmp(z, h)) == False{} : Bool}:
34 not_le_not_eq_c(cmp(z, h), e)
35
36def del_ins_cons(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +z: A, +h: A, +t: List<&2, A>, b: Bool, +eb: {S.le(~A, ~cmp, z, h) == b : Bool}, +ih: {S.delf(~A, ~cmp, z, S.ins(~A, ~cmp, z, t)) == t : List<&2, A>}) -> {S.delf(~A, ~cmp, z, S.ins(~A, ~cmp, z, Con{h, t})) == Con{h, t} : List<&2, A>}:
37 match b:
38 case True{}:
39 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, z, Con{h, t}), Con{z, Con{h, t}}, M.ins_cons(~A, ~cmp, z, h, t, True{}, eb)) : {S.delf(~A, ~cmp, z, _) == Con{h, t} : List<&2, A>}
40 del_head(~A, ~cmp, ~o, z, Con{h, t})
41 case False{}:
42 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, z, Con{h, t}), Con{h, S.ins(~A, ~cmp, z, t)}, M.ins_cons(~A, ~cmp, z, h, t, False{}, eb)) : {S.delf(~A, ~cmp, z, _) == Con{h, t} : List<&2, A>}
43 %Equal.sym(Bool, Cmp.is_eq(cmp(z, h)), False{}, not_le_not_eq(~A, ~cmp, z, h, eb)) : {S.del(~A, ~cmp, z, Con{h, S.ins(~A, ~cmp, z, t)}, _) == Con{h, t} : List<&2, A>}
44 LL.cons_cong(A, h, S.delf(~A, ~cmp, z, S.ins(~A, ~cmp, z, t)), t, ih)
45
46def del_ins(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +z: A, xs: List<&2, A>) -> {S.delf(~A, ~cmp, z, S.ins(~A, ~cmp, z, xs)) == xs : List<&2, A>}:
47 match xs:
48 case Nil{}:
49 del_head(~A, ~cmp, ~o, z, Nil{})
50 case Con{+h, +t}:
51 del_ins_cons(~A, ~cmp, ~o, z, h, t, S.le(~A, ~cmp, z, h), {==}, del_ins(~A, ~cmp, ~o, z, t))
52
53# Insertion is injective in the list: the sorted multiset is determined.
54def ins_inj(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +z: A, +xs: List<&2, A>, +ys: List<&2, A>, +e: {S.ins(~A, ~cmp, z, xs) == S.ins(~A, ~cmp, z, ys) : List<&2, A>}) -> {xs == ys : List<&2, A>}:
55 Equal.trans(List<&2, A>, xs, S.delf(~A, ~cmp, z, S.ins(~A, ~cmp, z, xs)), ys,
56 Equal.sym(List<&2, A>, S.delf(~A, ~cmp, z, S.ins(~A, ~cmp, z, xs)), xs, del_ins(~A, ~cmp, ~o, z, xs)),
57 Equal.trans(List<&2, A>, S.delf(~A, ~cmp, z, S.ins(~A, ~cmp, z, xs)), S.delf(~A, ~cmp, z, S.ins(~A, ~cmp, z, ys)), ys,
58 Equal.cong(List<&2, A>, List<&2, A>, l => S.delf(~A, ~cmp, z, l), S.ins(~A, ~cmp, z, xs), S.ins(~A, ~cmp, z, ys), e),
59 del_ins(~A, ~cmp, ~o, z, ys)))
60
61# ---- swapping two slots ----
62
63def upd_upd_same(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +u: Maybe<&2, A>, +v: Maybe<&2, A>) -> {SC.update(Maybe<&2, A>, SC.update(Maybe<&2, A>, ss, i, u), i, v) == SC.update(Maybe<&2, A>, ss, i, v) : List<&2, Maybe<&2, A>>}:
64 match ss i:
65 case Nil{} _:
66 {==}
67 case Con{x, r} 0n:
68 {==}
69 case Con{+x, +r} 1n+k:
70 LL.cons_cong(Maybe<&2, A>, x, SC.update(Maybe<&2, A>, SC.update(Maybe<&2, A>, r, k, u), k, v), SC.update(Maybe<&2, A>, r, k, v), upd_upd_same(~A, r, k, u, v))
71
72def slot_l1(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +p: Nat, +b: A, +hne: {Nat.is_eq(i, p) == False{} : Bool}, +hb: {SL.slot(~A, ss, p) == Some{b} : Maybe<&2, A>}) -> {SL.slot(~A, SC.update(Maybe<&2, A>, ss, i, Some{b}), p) == Some{b} : Maybe<&2, A>}:
73 Equal.trans(Maybe<&2, A>, SL.slot(~A, SC.update(Maybe<&2, A>, ss, i, Some{b}), p), SL.slot(~A, ss, p), Some{b}, SL.slot_other(~A, ss, i, p, Some{b}, hne), hb)
74
75# ---- a value below every slot is below every element of the multiset ----
76
77def all_ge_cons(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +z: A, +m: Maybe<&2, A>, +xs: List<&2, A>, +hm: {SL.mle(~A, ~cmp, Some{z}, m) == True{} : Bool}, +hxs: {S.all_ge(~A, ~cmp, z, V.msort(~A, ~cmp, xs)) == True{} : Bool}) -> {S.all_ge(~A, ~cmp, z, V.msort(~A, ~cmp, V.cons_slot(~A, m, xs))) == True{} : Bool}:
78 match m:
79 case None{}:
80 hxs
81 case Some{+w}:
82 %Equal.sym(Bool, S.all_ge(~A, ~cmp, z, S.ins(~A, ~cmp, w, V.msort(~A, ~cmp, xs))), Bool.and(S.le(~A, ~cmp, z, w), S.all_ge(~A, ~cmp, z, V.msort(~A, ~cmp, xs))), M.all_ge_ins(~A, ~cmp, ~o, z, w, V.msort(~A, ~cmp, xs))) : {_ == True{} : Bool}
83 L.and_intro(S.le(~A, ~cmp, z, w), S.all_ge(~A, ~cmp, z, V.msort(~A, ~cmp, xs)), hm, hxs)
84
85def low_all(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +z: A, k: Nat) -> Bool:
86 match k:
87 case 0n:
88 True{}
89 case 1n+ +m:
90 Bool.and(SL.mle(~A, ~cmp, Some{z}, SL.slot(~A, ss, m)), low_all(~A, ~cmp, ss, z, m))
91
92def all_ge_vals(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +z: A, k: Nat, +h: {low_all(~A, ~cmp, ss, z, k) == True{} : Bool}) -> {S.all_ge(~A, ~cmp, z, V.msort(~A, ~cmp, V.vals(~A, ss, k))) == True{} : Bool}:
93 match k:
94 case 0n:
95 {==}
96 case 1n+ +m:
97 all_ge_cons(~A, ~cmp, ~o, z, SL.slot(~A, ss, m), V.vals(~A, ss, m),
98 L.and_left(SL.mle(~A, ~cmp, Some{z}, SL.slot(~A, ss, m)), low_all(~A, ~cmp, ss, z, m), h),
99 all_ge_vals(~A, ~cmp, ~o, ss, z, m, L.and_right(SL.mle(~A, ~cmp, Some{z}, SL.slot(~A, ss, m)), low_all(~A, ~cmp, ss, z, m), h)))
100
101# Exchanging the values of two occupied slots leaves the sorted multiset
102# unchanged: two applications of `ins_set` and one cancellation.
103def vals_swap(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ss: List<&2, Maybe<&2, A>>, +n: Nat, +i: Nat, +p: Nat, +a: A, +b: A, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hp: {Nat.is_lt(p, n) == True{} : Bool}, +hne: {Nat.is_eq(i, p) == False{} : Bool}, +ha: {SL.slot(~A, ss, i) == Some{a} : Maybe<&2, A>}, +hb: {SL.slot(~A, ss, p) == Some{b} : Maybe<&2, A>}) -> {V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, SC.update(Maybe<&2, A>, ss, i, Some{b}), p, Some{a}), n)) == V.msort(~A, ~cmp, V.vals(~A, ss, n)) : List<&2, A>}:
104 +l1 = SC.update(Maybe<&2, A>, ss, i, Some{b})
105 +e1 = V.ins_set(~A, ~cmp, ~o, ss, n, i, a, b, hi, ha, Nat.is_eq(i, N.pred(n)), {==})
106 +e2 = V.ins_set(~A, ~cmp, ~o, l1, n, p, b, a, hp, slot_l1(~A, ss, i, p, b, hne, hb), Nat.is_eq(p, N.pred(n)), {==})
107 ins_inj(~A, ~cmp, ~o, b, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, l1, p, Some{a}), n)), V.msort(~A, ~cmp, V.vals(~A, ss, n)),
108 Equal.trans(List<&2, A>, S.ins(~A, ~cmp, b, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, l1, p, Some{a}), n))), S.ins(~A, ~cmp, a, V.msort(~A, ~cmp, V.vals(~A, l1, n))), S.ins(~A, ~cmp, b, V.msort(~A, ~cmp, V.vals(~A, ss, n))), e2, e1))