proofs/containers/binary_heap/multiset.bend
bend-collections-laws-containers@1.0.0.0 · 125 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/order.bend as O
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as S
7
8# Insertion-sorted lists as canonical multisets, under a total order ~o.
9# All lemmas are templates over (~A, ~cmp, ~o); they are checked through the
10# U32 and String instances at the end of this file and in END_TO_END.bend.
11
12def and_swap(+a: Bool, +b: Bool, +c: Bool) -> {Bool.and(a, Bool.and(b, c)) == Bool.and(b, Bool.and(a, c)) : Bool}:
13 match a b:
14 case True{} True{}:
15 {==}
16 case True{} False{}:
17 {==}
18 case False{} True{}:
19 {==}
20 case False{} False{}:
21 {==}
22
23def ins_cons(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +h: A, +t: List<&2, A>, +b: Bool, +e: {S.le(~A, ~cmp, x, h) == b : Bool}) -> {S.ins(~A, ~cmp, x, Con{h, t}) == Bool.pick(List<&2, A>, b, Con{x, Con{h, t}}, Con{h, S.ins(~A, ~cmp, x, t)}) : List<&2, A>}:
24 %e : {S.ins(~A, ~cmp, x, Con{h, t}) == Bool.pick(List<&2, A>, _, Con{x, Con{h, t}}, Con{h, S.ins(~A, ~cmp, x, t)}) : List<&2, A>}
25 {==}
26
27def all_ge_ins_c(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +z: A, +x: A, +h: A, +t: List<&2, A>, +b: Bool, +e: {S.le(~A, ~cmp, x, h) == b : Bool}, +ih: {S.all_ge(~A, ~cmp, z, S.ins(~A, ~cmp, x, t)) == Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, t)) : Bool}) -> {S.all_ge(~A, ~cmp, z, S.ins(~A, ~cmp, x, Con{h, t})) == Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, Con{h, t})) : Bool}:
28 match b:
29 case True{}:
30 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{x, Con{h, t}}, ins_cons(~A, ~cmp, x, h, t, True{}, e)) : {S.all_ge(~A, ~cmp, z, _) == Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, Con{h, t})) : Bool}
31 {==}
32 case False{}:
33 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{h, S.ins(~A, ~cmp, x, t)}, ins_cons(~A, ~cmp, x, h, t, False{}, e)) : {S.all_ge(~A, ~cmp, z, _) == Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, Con{h, t})) : Bool}
34 %Equal.sym(Bool, S.all_ge(~A, ~cmp, z, S.ins(~A, ~cmp, x, t)), Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, t)), ih) : {Bool.and(S.le(~A, ~cmp, z, h), _) == Bool.and(S.le(~A, ~cmp, z, x), Bool.and(S.le(~A, ~cmp, z, h), S.all_ge(~A, ~cmp, z, t))) : Bool}
35 and_swap(S.le(~A, ~cmp, z, h), S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, t))
36
37def all_ge_ins(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +z: A, +x: A, +xs: List<&2, A>) -> {S.all_ge(~A, ~cmp, z, S.ins(~A, ~cmp, x, xs)) == Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, xs)) : Bool}:
38 match xs:
39 case Nil{}:
40 {==}
41 case Con{+h, +t}:
42 all_ge_ins_c(~A, ~cmp, ~o, z, x, h, t, S.le(~A, ~cmp, x, h), {==}, all_ge_ins(~A, ~cmp, ~o, z, x, t))
43
44# A value not larger than every element goes first.
45def ins_min(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +x: A, +xs: List<&2, A>, +h: {S.all_ge(~A, ~cmp, x, xs) == True{} : Bool}) -> {S.ins(~A, ~cmp, x, xs) == Con{x, xs} : List<&2, A>}:
46 match xs:
47 case Nil{}:
48 {==}
49 case Con{+y, +t}:
50 %Equal.sym(Bool, S.le(~A, ~cmp, x, y), True{}, L.and_left(S.le(~A, ~cmp, x, y), S.all_ge(~A, ~cmp, x, t), h)) : {Bool.pick(List<&2, A>, _, Con{x, Con{y, t}}, Con{y, S.ins(~A, ~cmp, x, t)}) == Con{x, Con{y, t}} : List<&2, A>}
51 {==}
52
53# Insertion order is irrelevant (uses totality, transitivity, antisymmetry).
54def comm_nil(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +x: A, +y: A, +bxy: Bool, +exy: {S.le(~A, ~cmp, x, y) == bxy : Bool}, +byx: Bool, +eyx: {S.le(~A, ~cmp, y, x) == byx : Bool}) -> {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Nil{})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Nil{})) : List<&2, A>}:
55 match bxy byx:
56 case True{} True{}:
57 %O.le_antisym(~A, ~cmp, ~o, x, y, exy, eyx) : {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, _, Nil{})) == S.ins(~A, ~cmp, _, S.ins(~A, ~cmp, x, Nil{})) : List<&2, A>}
58 {==}
59 case True{} False{}:
60 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{y, Nil{}}), Con{x, Con{y, Nil{}}}, ins_cons(~A, ~cmp, x, y, Nil{}, True{}, exy)) : {_ == S.ins(~A, ~cmp, y, Con{x, Nil{}}) : List<&2, A>}
61 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{x, Nil{}}), Con{x, Con{y, Nil{}}}, ins_cons(~A, ~cmp, y, x, Nil{}, False{}, eyx)) : {Con{x, Con{y, Nil{}}} == _ : List<&2, A>}
62 {==}
63 case False{} True{}:
64 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{y, Nil{}}), Con{y, Con{x, Nil{}}}, ins_cons(~A, ~cmp, x, y, Nil{}, False{}, exy)) : {_ == S.ins(~A, ~cmp, y, Con{x, Nil{}}) : List<&2, A>}
65 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{x, Nil{}}), Con{y, Con{x, Nil{}}}, ins_cons(~A, ~cmp, y, x, Nil{}, True{}, eyx)) : {Con{y, Con{x, Nil{}}} == _ : List<&2, A>}
66 {==}
67 case False{} False{}:
68 Empty.absurd({S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Nil{})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Nil{})) : List<&2, A>}, L.true_not_false(S.le(~A, ~cmp, y, x), O.total(~A, ~cmp, ~o, x, y, exy), eyx))
69
70def comm_cons(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +x: A, +y: A, +h: A, +t: List<&2, A>, +bxy: Bool, +exy: {S.le(~A, ~cmp, x, y) == bxy : Bool}, +byx: Bool, +eyx: {S.le(~A, ~cmp, y, x) == byx : Bool}, +bxh: Bool, +exh: {S.le(~A, ~cmp, x, h) == bxh : Bool}, +byh: Bool, +eyh: {S.le(~A, ~cmp, y, h) == byh : Bool}, +ih: {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t)) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, t)) : List<&2, A>}) -> {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Con{h, t})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}:
71 match bxy byx bxh byh:
72 case False{} False{} _ _:
73 Empty.absurd({S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Con{h, t})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}, L.true_not_false(S.le(~A, ~cmp, y, x), O.total(~A, ~cmp, ~o, x, y, exy), eyx))
74 case True{} True{} _ _:
75 %O.le_antisym(~A, ~cmp, ~o, x, y, exy, eyx) : {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, _, Con{h, t})) == S.ins(~A, ~cmp, _, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
76 {==}
77 case True{} False{} True{} True{}:
78 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{y, Con{h, t}}, ins_cons(~A, ~cmp, y, h, t, True{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
79 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{x, Con{h, t}}, ins_cons(~A, ~cmp, x, h, t, True{}, exh)) : {S.ins(~A, ~cmp, x, Con{y, Con{h, t}}) == S.ins(~A, ~cmp, y, _) : List<&2, A>}
80 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{y, Con{h, t}}), Con{x, Con{y, Con{h, t}}}, ins_cons(~A, ~cmp, x, y, Con{h, t}, True{}, exy)) : {_ == S.ins(~A, ~cmp, y, Con{x, Con{h, t}}) : List<&2, A>}
81 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{x, Con{h, t}}), Con{x, S.ins(~A, ~cmp, y, Con{h, t})}, ins_cons(~A, ~cmp, y, x, Con{h, t}, False{}, eyx)) : {Con{x, Con{y, Con{h, t}}} == _ : List<&2, A>}
82 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{y, Con{h, t}}, ins_cons(~A, ~cmp, y, h, t, True{}, eyh)) : {Con{x, Con{y, Con{h, t}}} == Con{x, _} : List<&2, A>}
83 {==}
84 case True{} False{} False{} True{}:
85 Empty.absurd({S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Con{h, t})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}, L.true_not_false(S.le(~A, ~cmp, x, h), O.trans(~A, ~cmp, o, x, y, h, exy, eyh), exh))
86 case True{} False{} True{} False{}:
87 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{h, S.ins(~A, ~cmp, y, t)}, ins_cons(~A, ~cmp, y, h, t, False{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
88 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, S.ins(~A, ~cmp, y, t)}), Con{x, Con{h, S.ins(~A, ~cmp, y, t)}}, ins_cons(~A, ~cmp, x, h, S.ins(~A, ~cmp, y, t), True{}, exh)) : {_ == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
89 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{x, Con{h, t}}, ins_cons(~A, ~cmp, x, h, t, True{}, exh)) : {Con{x, Con{h, S.ins(~A, ~cmp, y, t)}} == S.ins(~A, ~cmp, y, _) : List<&2, A>}
90 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{x, Con{h, t}}), Con{x, S.ins(~A, ~cmp, y, Con{h, t})}, ins_cons(~A, ~cmp, y, x, Con{h, t}, False{}, eyx)) : {Con{x, Con{h, S.ins(~A, ~cmp, y, t)}} == _ : List<&2, A>}
91 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{h, S.ins(~A, ~cmp, y, t)}, ins_cons(~A, ~cmp, y, h, t, False{}, eyh)) : {Con{x, Con{h, S.ins(~A, ~cmp, y, t)}} == Con{x, _} : List<&2, A>}
92 {==}
93 case True{} False{} False{} False{}:
94 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{h, S.ins(~A, ~cmp, y, t)}, ins_cons(~A, ~cmp, y, h, t, False{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
95 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, S.ins(~A, ~cmp, y, t)}), Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))}, ins_cons(~A, ~cmp, x, h, S.ins(~A, ~cmp, y, t), False{}, exh)) : {_ == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
96 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{h, S.ins(~A, ~cmp, x, t)}, ins_cons(~A, ~cmp, x, h, t, False{}, exh)) : {Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))} == S.ins(~A, ~cmp, y, _) : List<&2, A>}
97 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, S.ins(~A, ~cmp, x, t)}), Con{h, S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, t))}, ins_cons(~A, ~cmp, y, h, S.ins(~A, ~cmp, x, t), False{}, eyh)) : {Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))} == _ : List<&2, A>}
98 LL.cons_cong(A, h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t)), S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, t)), ih)
99 case False{} True{} True{} True{}:
100 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{y, Con{h, t}}, ins_cons(~A, ~cmp, y, h, t, True{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
101 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{y, Con{h, t}}), Con{y, S.ins(~A, ~cmp, x, Con{h, t})}, ins_cons(~A, ~cmp, x, y, Con{h, t}, False{}, exy)) : {_ == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
102 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{x, Con{h, t}}, ins_cons(~A, ~cmp, x, h, t, True{}, exh)) : {Con{y, _} == S.ins(~A, ~cmp, y, _) : List<&2, A>}
103 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{x, Con{h, t}}), Con{y, Con{x, Con{h, t}}}, ins_cons(~A, ~cmp, y, x, Con{h, t}, True{}, eyx)) : {Con{y, Con{x, Con{h, t}}} == _ : List<&2, A>}
104 {==}
105 case False{} True{} False{} True{}:
106 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{y, Con{h, t}}, ins_cons(~A, ~cmp, y, h, t, True{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
107 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{y, Con{h, t}}), Con{y, S.ins(~A, ~cmp, x, Con{h, t})}, ins_cons(~A, ~cmp, x, y, Con{h, t}, False{}, exy)) : {_ == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
108 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{h, S.ins(~A, ~cmp, x, t)}, ins_cons(~A, ~cmp, x, h, t, False{}, exh)) : {Con{y, _} == S.ins(~A, ~cmp, y, _) : List<&2, A>}
109 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, S.ins(~A, ~cmp, x, t)}), Con{y, Con{h, S.ins(~A, ~cmp, x, t)}}, ins_cons(~A, ~cmp, y, h, S.ins(~A, ~cmp, x, t), True{}, eyh)) : {Con{y, Con{h, S.ins(~A, ~cmp, x, t)}} == _ : List<&2, A>}
110 {==}
111 case False{} True{} True{} False{}:
112 Empty.absurd({S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Con{h, t})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}, L.true_not_false(S.le(~A, ~cmp, y, h), O.trans(~A, ~cmp, o, y, x, h, eyx, exh), eyh))
113 case False{} True{} False{} False{}:
114 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{h, S.ins(~A, ~cmp, y, t)}, ins_cons(~A, ~cmp, y, h, t, False{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
115 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, S.ins(~A, ~cmp, y, t)}), Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))}, ins_cons(~A, ~cmp, x, h, S.ins(~A, ~cmp, y, t), False{}, exh)) : {_ == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
116 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{h, S.ins(~A, ~cmp, x, t)}, ins_cons(~A, ~cmp, x, h, t, False{}, exh)) : {Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))} == S.ins(~A, ~cmp, y, _) : List<&2, A>}
117 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, S.ins(~A, ~cmp, x, t)}), Con{h, S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, t))}, ins_cons(~A, ~cmp, y, h, S.ins(~A, ~cmp, x, t), False{}, eyh)) : {Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))} == _ : List<&2, A>}
118 LL.cons_cong(A, h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t)), S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, t)), ih)
119
120def ins_comm(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +x: A, +y: A, +s: List<&2, A>) -> {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, s)) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, s)) : List<&2, A>}:
121 match s:
122 case Nil{}:
123 comm_nil(~A, ~cmp, ~o, x, y, S.le(~A, ~cmp, x, y), {==}, S.le(~A, ~cmp, y, x), {==})
124 case Con{+h, +t}:
125 comm_cons(~A, ~cmp, ~o, x, y, h, t, S.le(~A, ~cmp, x, y), {==}, S.le(~A, ~cmp, y, x), {==}, S.le(~A, ~cmp, x, h), {==}, S.le(~A, ~cmp, y, h), {==}, ins_comm(~A, ~cmp, ~o, x, y, t))