proofs/containers/priority_queue/proof.bend
bend-collections-laws-containers@1.0.0.0 · 99 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/priority_queue.bend as P2
3import bend-collections-laws-containers@1.0.0.0/src/containers/binary_heap.bend as K2
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/binary_heap.bend as E2
5import bend-collections-laws-containers@1.0.0.0/spec/containers/priority_queue.bend as S
6import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as HS
7import bend-collections-laws-containers@1.0.0.0/spec/lib/order.bend as SO
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/proof.bend as UP
9
10# src/containers/priority_queue.bend: a binary heap behind the queue interface (put = push, get = pop, qsize = length).
11
12def priority_queue_put(q: K2.Heap<U32>, +v: U32) -> {P2.put(~U32, ~U32.cmp, q, v) == K2.push(~U32, ~U32.cmp, q, v) : K2.Heap<U32>}:
13 {==}
14
15def priority_queue_get(q: K2.Heap<U32>) -> {P2.get(~U32, ~U32.cmp, q) == K2.pop(~U32, ~U32.cmp, q) : K2.Heap<U32> & Result<&2, &2, E2.Error, U32>}:
16 {==}
17
18def priority_queue_qsize(q: K2.Heap<U32>) -> {P2.qsize(~U32, q) == K2.length(~U32, q) : K2.Heap<U32> & Nat}:
19 {==}
20
21# ==== the contract of priority_queue (stated in spec/containers/priority_queue.bend) ====================
22
23def new_is(~A: Data) -> {P2.new(~A) == K2.new(~A) : K2.Heap<A>}:
24 {==}
25
26def qsize_is(~A: Data, h: K2.Heap<A>) -> {P2.qsize(~A, h) == K2.length(~A, h) : K2.Heap<A> & Nat}:
27 {==}
28
29def put_is(~A: Data, ~cmp: A -> A -> Cmp, h: K2.Heap<A>, x: A) -> {P2.put(~A, ~cmp, h, x) == K2.push(~A, ~cmp, h, x) : K2.Heap<A>}:
30 {==}
31
32def peek_is(~A: Data, h: K2.Heap<A>) -> {P2.peek(~A, h) == K2.peek(~A, h) : K2.Heap<A> & Result<&2, &2, E2.Error, A>}:
33 {==}
34
35def get_is(~A: Data, ~cmp: A -> A -> Cmp, h: K2.Heap<A>) -> {P2.get(~A, ~cmp, h) == K2.pop(~A, ~cmp, h) : K2.Heap<A> & Result<&2, &2, E2.Error, A>}:
36 {==}
37
38def from_list_is(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>) -> {P2.from_list(~A, ~cmp, xs) == K2.from_list(~A, ~cmp, xs) : K2.Heap<A>}:
39 {==}
40
41def to_sorted_list_is(~A: Data, ~cmp: A -> A -> Cmp, h: K2.Heap<A>) -> {P2.to_sorted_list(~A, ~cmp, h) == K2.to_sorted_list(~A, ~cmp, h) : K2.Heap<A> & List<&2, A>}:
42 {==}
43
44# ---- the binary_heap's contract, carried: every clause is proved by the binary_heap ----
45
46def length_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Length.length_result(~A, ~cmp, xs):
47 UP.length_result(~A, ~cmp, xs)
48
49def length_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Length.length_frame(~A, ~cmp, xs):
50 UP.length_frame(~A, ~cmp, xs)
51
52def push_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +x: A) -> S.Insert.push_length(~A, ~cmp, xs, x):
53 UP.push_length(~A, ~cmp, xs, x)
54
55def push_bag(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +x: A) -> S.Insert.push_bag(~A, ~cmp, ~o, xs, x):
56 UP.push_bag(~A, ~cmp, ~o, xs, x)
57
58def push_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +x: A, +hs: {HS.sorted(~A, ~cmp, xs) == True{} : Bool}) -> S.Insert.push_sorted(~A, ~cmp, ~o, xs, x, hs):
59 UP.push_sorted(~A, ~cmp, ~o, xs, x, hs)
60
61def peek_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {HS.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> S.First_Element.peek_min(~A, ~cmp, h, t, hs):
62 UP.peek_min(~A, ~cmp, h, t, hs)
63
64def peek_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.First_Element.peek_frame(~A, ~cmp, xs):
65 UP.peek_frame(~A, ~cmp, xs)
66
67def peek_empty(~A: Data, ~cmp: A -> A -> Cmp) -> S.First_Element.peek_empty(~A, ~cmp):
68 UP.peek_empty(~A, ~cmp)
69
70def pop_length(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> S.Delete_First.pop_length(~A, ~cmp, h, t):
71 UP.pop_length(~A, ~cmp, h, t)
72
73def pop_result(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> S.Delete_First.pop_result(~A, ~cmp, h, t):
74 UP.pop_result(~A, ~cmp, h, t)
75
76def pop_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {HS.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> S.Delete_First.pop_min(~A, ~cmp, h, t, hs):
77 UP.pop_min(~A, ~cmp, h, t, hs)
78
79def pop_bag(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +h: A, +t: List<&2, A>, +hs: {HS.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> S.Delete_First.pop_bag(~A, ~cmp, ~o, h, t, hs):
80 UP.pop_bag(~A, ~cmp, ~o, h, t, hs)
81
82def pop_empty(~A: Data, ~cmp: A -> A -> Cmp) -> S.Delete_First.pop_empty(~A, ~cmp):
83 UP.pop_empty(~A, ~cmp)
84
85def from_list_model(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> S.To_Set.from_list_model(~A, ~cmp, xs, ys):
86 UP.from_list_model(~A, ~cmp, xs, ys)
87
88def from_list_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> S.To_Set.from_list_length(~A, ~cmp, xs, ys):
89 UP.from_list_length(~A, ~cmp, xs, ys)
90
91def from_list_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +ys: List<&2, A>) -> S.To_Set.from_list_sorted(~A, ~cmp, ~o, xs, ys):
92 UP.from_list_sorted(~A, ~cmp, ~o, xs, ys)
93
94def to_sorted_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Elements.to_sorted_result(~A, ~cmp, xs):
95 UP.to_sorted_result(~A, ~cmp, xs)
96
97def to_sorted_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Elements.to_sorted_frame(~A, ~cmp, xs):
98 UP.to_sorted_frame(~A, ~cmp, xs)
99