proofs/containers/binary_heap/proof.bend
bend-collections-laws-containers@1.0.0.0 · 252 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/list.bend as LL
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
7import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
8import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as S
9import bend-collections-laws-containers@1.0.0.0/src/containers/binary_heap.bend as H
10import bend-collections-laws-containers@1.0.0.0/src/containers/types/binary_heap.bend as E
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/state.bend as ST
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/steps.bend as SP
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/trace.bend as TR
14import bend-collections-laws-containers@1.0.0.0/spec/lib/order.bend as SO
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/multiset.bend as M
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/vals.bend as VL
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/bag.bend as BG
18
19# Binary heap: public proof entry point.
20# representation a PACKED Base.Array block, element i with children 2i+1
21# and 2i+2 (src/binary_heap.bend). The block is linear, so
22# -- as in proofs/dynamic_array, proofs/bitset and
23# proofs/deque -- every law is about the heap BUILT from a
24# Data mirror tree (ST.real of a shadow).
25# abstraction ST.model / ST.abs (the sorted multiset of the occupied
26# slots; ST.abs reads an actual block through AR.freeze)
27# invariant ST.good / ST.Inv (perfect block, elements exactly in
28# [0, size), heap order over them, size <= 2^depth)
29# operations SP.step_ok (every operation, errors included)
30# traces trace_from / trace_new (arbitrary finite op lists)
31#
32# Laws are templates over a comparator ~cmp with total-order laws
33# ~o : O.Order(~A, ~cmp); each is instantiated and thereby checked below for
34# (U32, U32.cmp, O.u32_order) and (String, String.order, O.string_order), the
35# instances src/ exposes.
36#
37# The capacity condition of the representation, in terms of the heap's
38# SIZE: size + (elements the operations can add) < 2^q with q <= 31. A push
39# doubles the block only when it is full, and then 2^depth = size < 2^q
40# forces depth < 31, so every slot index stays a representable U32 (Base
41# arrays have at most 2^31 slots). It is a premise only of the step and
42# trace laws, it does not bound the length of a trace, and every other law
43# holds at every state satisfying the invariant.
44
45# ---- the constructor ----
46
47def new_real(~A: Data, ~cmp: A -> A -> Cmp) -> {H.new(~A) == ST.real(~A, ST.initial(~A)) : H.Heap<A>}:
48 ST.new_real(~A)
49
50def new_inv(~A: Data, ~cmp: A -> A -> Cmp) -> {ST.good(~A, ~cmp, ST.initial(~A)) == True{} : Bool}:
51 ST.new_good(~A, ~cmp)
52
53def new_abs(~A: Data, ~cmp: A -> A -> Cmp) -> {ST.model(~A, ~cmp, ST.initial(~A)) == Nil{} : List<&2, A>}:
54 ST.new_model(~A, ~cmp)
55
56# ---- every operation (errors included), on every reachable representation ----
57
58def step_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), sh: ST.Shadow<A>, op: E.Op<A>, +g: {ST.good(~A, ~cmp, sh) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh), SP.pushcost(~A, op)), SC.pow2(q)) == True{} : Bool}) -> SP.StepOK(~A, ~cmp, sh, op):
59 SP.step_ok(~A, ~cmp, ~o, sh, op, g, q, hq, room)
60
61# The abstraction of an actual heap is the model of its shadow: the laws
62# above, stated on shadows, are laws about actual heaps.
63def abs_real(~A: Data, ~cmp: A -> A -> Cmp, +sh: ST.Shadow<A>) -> {ST.abs(~A, ~cmp, ST.real(~A, sh)) == ST.model(~A, ~cmp, sh) : List<&2, A>}:
64 ST.abs_real(~A, ~cmp, sh)
65
66def new_heap_inv(~A: Data, ~cmp: A -> A -> Cmp) -> ST.Inv(~A, ~cmp, H.new(~A)):
67 (ST.initial(~A), (ST.new_real(~A), ST.new_good(~A, ~cmp)))
68
69# ---- arbitrary finite traces ----
70
71def trace_from(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ops: List<&2, E.Op<A>>, +sh0: ST.Shadow<A>, +g0: {ST.good(~A, ~cmp, sh0) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh0), TR.pushes(~A, ops)), SC.pow2(q)) == True{} : Bool}) -> TR.TraceOK(~A, ~cmp, ops, sh0):
72 TR.trace_from(~A, ~cmp, ~o, ops, sh0, g0, q, hq, room)
73
74def trace_new(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ops: List<&2, E.Op<A>>, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(TR.pushes(~A, ops), SC.pow2(q)) == True{} : Bool}) -> TR.TraceOK(~A, ~cmp, ops, ST.initial(~A)):
75 TR.trace_from(~A, ~cmp, ~o, ops, ST.initial(~A), ST.new_good(~A, ~cmp), q, hq, room)
76
77# ---- checked instances ----
78
79def u32_step_ok(sh: ST.Shadow<U32>, op: E.Op<U32>, +g: {ST.good(~U32, ~U32.cmp, sh) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(Nat.add(ST.sh_size(~U32, sh), SP.pushcost(~U32, op)), SC.pow2(q)) == True{} : Bool}) -> SP.StepOK(~U32, ~U32.cmp, sh, op):
80 step_ok(~U32, ~U32.cmp, ~O.u32_order, sh, op, g, q, hq, room)
81
82def u32_trace(+ops: List<&2, E.Op<U32>>, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(TR.pushes(~U32, ops), SC.pow2(q)) == True{} : Bool}) -> TR.TraceOK(~U32, ~U32.cmp, ops, ST.initial(~U32)):
83 trace_new(~U32, ~U32.cmp, ~O.u32_order, ops, q, hq, room)
84
85def u32_new_inv() -> ST.Inv(~U32, ~U32.cmp, H.new(~U32)):
86 new_heap_inv(~U32, ~U32.cmp)
87
88def string_step_ok(sh: ST.Shadow<String>, op: E.Op<String>, +g: {ST.good(~String, ~String.order, sh) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(Nat.add(ST.sh_size(~String, sh), SP.pushcost(~String, op)), SC.pow2(q)) == True{} : Bool}) -> SP.StepOK(~String, ~String.order, sh, op):
89 step_ok(~String, ~String.order, ~O.string_order, sh, op, g, q, hq, room)
90
91def string_trace(+ops: List<&2, E.Op<String>>, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(TR.pushes(~String, ops), SC.pow2(q)) == True{} : Bool}) -> TR.TraceOK(~String, ~String.order, ops, ST.initial(~String)):
92 trace_new(~String, ~String.order, ~O.string_order, ops, q, hq, room)
93
94def string_new_inv() -> ST.Inv(~String, ~String.order, H.new(~String)):
95 new_heap_inv(~String, ~String.order)
96
97# ==== the contract of binary_heap (stated in spec/containers/binary_heap.bend) ====================
98
99# ascending: each element is below all the later ones
100# ---- the implementation ----
101def Impl(~A: Data, ~cmp: A -> A -> Cmp, sh: ST.Shadow<A>, op: E.Op<A>, Post: (List<&2, A> & E.Obs<A>) -> Type) -> Type:
102 Sigma<&1, &1, ST.Shadow<A>, sh2 => Sigma<&1, &1, E.Obs<A>, o => {H.step(~A, ~cmp, ST.real(~A, sh), op) == (ST.real(~A, sh2), o) : H.Heap<A> & E.Obs<A>} & ({ST.good(~A, ~cmp, sh2) == True{} : Bool} & Post((ST.model(~A, ~cmp, sh2), o)))>>
103
104def impl_of(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow<A>, -op: E.Op<A>, -Post: (List<&2, A> & E.Obs<A>) -> Type, k: SP.StepOK(~A, ~cmp, sh, op), pf: Post(S.step(~A, ~cmp, ST.model(~A, ~cmp, sh), op))) -> Impl(~A, ~cmp, sh, op, Post):
105 match k:
106 case Tuple{sh2, Tuple{o, Tuple{e1, Tuple{g2, Tuple{e3, e4}}}}}:
107 (sh2, (o, (e1, (g2, L.subst(List<&2, A> & E.Obs<A>, Post, S.step(~A, ~cmp, ST.model(~A, ~cmp, sh), op), (ST.model(~A, ~cmp, sh2), o), Equal.sym(List<&2, A> & E.Obs<A>, (ST.model(~A, ~cmp, sh2), o), S.step(~A, ~cmp, ST.model(~A, ~cmp, sh), op), e3), pf)))))
108
109# the heap must have room for a push (size + pushes < 2^q, q <= 31)
110def impl(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), sh: ST.Shadow<A>, op: E.Op<A>, +g: {ST.good(~A, ~cmp, sh) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh), SP.pushcost(~A, op)), SC.pow2(q)) == True{} : Bool}, -Post: (List<&2, A> & E.Obs<A>) -> Type, pf: Post(S.step(~A, ~cmp, ST.model(~A, ~cmp, sh), op))) -> Impl(~A, ~cmp, sh, op, Post):
111 impl_of(~A, ~cmp, sh, op, Post, step_ok(~A, ~cmp, ~o, sh, op, g, q, hq, room), pf)
112
113# ---- ordering ----
114def ag_trans(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +x: A, +h: A, +t: List<&2, A>, +hxh: {S.le(~A, ~cmp, x, h) == True{} : Bool}, +hht: {S.all_ge(~A, ~cmp, h, t) == True{} : Bool}) -> {S.all_ge(~A, ~cmp, x, t) == True{} : Bool}:
115 match t:
116 case Nil{}:
117 {==}
118 case Con{+a, +r}:
119 L.and_intro(S.le(~A, ~cmp, x, a), S.all_ge(~A, ~cmp, x, r), O.trans(~A, ~cmp, o, x, h, a, hxh, L.and_left(S.le(~A, ~cmp, h, a), S.all_ge(~A, ~cmp, h, r), hht)), ag_trans(~A, ~cmp, ~o, x, h, r, hxh, L.and_right(S.le(~A, ~cmp, h, a), S.all_ge(~A, ~cmp, h, r), hht)))
120
121def is_c(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +x: A, +h: A, +t: List<&2, A>, +hs: {S.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}, +b: Bool, +eb: {S.le(~A, ~cmp, x, h) == b : Bool}, +ih: {S.sorted(~A, ~cmp, S.ins(~A, ~cmp, x, t)) == True{} : Bool}) -> {S.sorted(~A, ~cmp, S.ins(~A, ~cmp, x, Con{h, t})) == True{} : Bool}:
122 match b:
123 case True{}:
124 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Bool.pick(List<&2, A>, True{}, Con{x, Con{h, t}}, Con{h, S.ins(~A, ~cmp, x, t)}), M.ins_cons(~A, ~cmp, x, h, t, True{}, eb)) : {S.sorted(~A, ~cmp, _) == True{} : Bool}
125 L.and_intro(S.all_ge(~A, ~cmp, x, Con{h, t}), S.sorted(~A, ~cmp, Con{h, t}), L.and_intro(S.le(~A, ~cmp, x, h), S.all_ge(~A, ~cmp, x, t), eb, ag_trans(~A, ~cmp, ~o, x, h, t, eb, L.and_left(S.all_ge(~A, ~cmp, h, t), S.sorted(~A, ~cmp, t), hs))), hs)
126 case False{}:
127 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Bool.pick(List<&2, A>, False{}, Con{x, Con{h, t}}, Con{h, S.ins(~A, ~cmp, x, t)}), M.ins_cons(~A, ~cmp, x, h, t, False{}, eb)) : {S.sorted(~A, ~cmp, _) == True{} : Bool}
128 %Equal.sym(Bool, S.all_ge(~A, ~cmp, h, S.ins(~A, ~cmp, x, t)), Bool.and(S.le(~A, ~cmp, h, x), S.all_ge(~A, ~cmp, h, t)), M.all_ge_ins(~A, ~cmp, ~o, h, x, t)) : {Bool.and(_, S.sorted(~A, ~cmp, S.ins(~A, ~cmp, x, t))) == True{} : Bool}
129 L.and_intro(Bool.and(S.le(~A, ~cmp, h, x), S.all_ge(~A, ~cmp, h, t)), S.sorted(~A, ~cmp, S.ins(~A, ~cmp, x, t)), L.and_intro(S.le(~A, ~cmp, h, x), S.all_ge(~A, ~cmp, h, t), O.total(~A, ~cmp, ~o, x, h, eb), L.and_left(S.all_ge(~A, ~cmp, h, t), S.sorted(~A, ~cmp, t), hs)), ih)
130
131def ins_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +x: A, +xs: List<&2, A>, +hs: {S.sorted(~A, ~cmp, xs) == True{} : Bool}) -> {S.sorted(~A, ~cmp, S.ins(~A, ~cmp, x, xs)) == True{} : Bool}:
132 match xs:
133 case Nil{}:
134 {==}
135 case Con{+h, +t}:
136 is_c(~A, ~cmp, ~o, x, h, t, hs, S.le(~A, ~cmp, x, h), {==}, ins_sorted(~A, ~cmp, ~o, x, t, L.and_right(S.all_ge(~A, ~cmp, h, t), S.sorted(~A, ~cmp, t), hs)))
137
138def msort_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>) -> {S.sorted(~A, ~cmp, VL.msort(~A, ~cmp, xs)) == True{} : Bool}:
139 match xs:
140 case Nil{}:
141 {==}
142 case Con{+h, +t}:
143 ins_sorted(~A, ~cmp, ~o, h, VL.msort(~A, ~cmp, t), msort_sorted(~A, ~cmp, ~o, t))
144
145# every model (the multiset of a heap) is ascending
146def model_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +sh: ST.Shadow<A>) -> {S.sorted(~A, ~cmp, ST.model(~A, ~cmp, sh)) == True{} : Bool}:
147 match sh:
148 case ST.Sh{+size, +depth, +t}:
149 msort_sorted(~A, ~cmp, ~o, VL.vals(~A, AR.slots(Maybe<&2, A>, t), size))
150
151def from_list_sorted_go(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +ys: List<&2, A>, +acc: List<&2, A>, +hs: {S.sorted(~A, ~cmp, acc) == True{} : Bool}) -> {S.sorted(~A, ~cmp, S.from_list(~A, ~cmp, ys, acc)) == True{} : Bool}:
152 match ys:
153 case Nil{}:
154 hs
155 case Con{+y, +t}:
156 from_list_sorted_go(~A, ~cmp, ~o, t, S.ins(~A, ~cmp, y, acc), ins_sorted(~A, ~cmp, ~o, y, acc, hs))
157
158# ---- lengths ----
159def ins_len_c(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +h: A, +t: List<&2, A>, +b: Bool, +eb: {S.le(~A, ~cmp, x, h) == b : Bool}, +ih: {SC.length(A, S.ins(~A, ~cmp, x, t)) == 1n+SC.length(A, t) : Nat}) -> {SC.length(A, S.ins(~A, ~cmp, x, Con{h, t})) == 1n+SC.length(A, Con{h, t}) : Nat}:
160 match b:
161 case True{}:
162 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Bool.pick(List<&2, A>, True{}, Con{x, Con{h, t}}, Con{h, S.ins(~A, ~cmp, x, t)}), M.ins_cons(~A, ~cmp, x, h, t, True{}, eb)) : {SC.length(A, _) == 1n+SC.length(A, Con{h, t}) : Nat}
163 {==}
164 case False{}:
165 %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Bool.pick(List<&2, A>, False{}, Con{x, Con{h, t}}, Con{h, S.ins(~A, ~cmp, x, t)}), M.ins_cons(~A, ~cmp, x, h, t, False{}, eb)) : {SC.length(A, _) == 1n+SC.length(A, Con{h, t}) : Nat}
166 N.succ_cong(SC.length(A, S.ins(~A, ~cmp, x, t)), 1n+SC.length(A, t), ih)
167
168def ins_length(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +xs: List<&2, A>) -> {SC.length(A, S.ins(~A, ~cmp, x, xs)) == 1n+SC.length(A, xs) : Nat}:
169 match xs:
170 case Nil{}:
171 {==}
172 case Con{+h, +t}:
173 ins_len_c(~A, ~cmp, x, h, t, S.le(~A, ~cmp, x, h), {==}, ins_length(~A, ~cmp, x, t))
174
175def succ_add(+a: Nat, +b: Nat) -> {Nat.add(a, 1n+b) == Nat.add(1n+a, b) : Nat}:
176 Equal.trans(Nat, Nat.add(a, 1n+b), 1n+Nat.add(a, b), Nat.add(1n+a, b), N.add_succ(a, b),
177 Equal.trans(Nat, 1n+Nat.add(a, b), 1n+Nat.add(b, a), Nat.add(1n+a, b), N.succ_cong(Nat.add(a, b), Nat.add(b, a), N.add_comm(a, b)),
178 Equal.trans(Nat, 1n+Nat.add(b, a), Nat.add(b, 1n+a), Nat.add(1n+a, b), Equal.sym(Nat, Nat.add(b, 1n+a), 1n+Nat.add(b, a), N.add_succ(b, a)), N.add_comm(b, 1n+a))))
179
180def from_list_length_go(~A: Data, ~cmp: A -> A -> Cmp, +ys: List<&2, A>, +acc: List<&2, A>) -> {SC.length(A, S.from_list(~A, ~cmp, ys, acc)) == Nat.add(SC.length(A, ys), SC.length(A, acc)) : Nat}:
181 match ys:
182 case Nil{}:
183 Equal.sym(Nat, Nat.add(0n, SC.length(A, acc)), SC.length(A, acc), Equal.trans(Nat, Nat.add(0n, SC.length(A, acc)), Nat.add(SC.length(A, acc), 0n), SC.length(A, acc), N.add_comm(0n, SC.length(A, acc)), N.add_zero(SC.length(A, acc))))
184 case Con{+y, +t}:
185 %Equal.sym(Nat, SC.length(A, S.from_list(~A, ~cmp, t, S.ins(~A, ~cmp, y, acc))), Nat.add(SC.length(A, t), SC.length(A, S.ins(~A, ~cmp, y, acc))), from_list_length_go(~A, ~cmp, t, S.ins(~A, ~cmp, y, acc))) : {_ == Nat.add(1n+SC.length(A, t), SC.length(A, acc)) : Nat}
186 %Equal.sym(Nat, SC.length(A, S.ins(~A, ~cmp, y, acc)), 1n+SC.length(A, acc), ins_length(~A, ~cmp, y, acc)) : {Nat.add(SC.length(A, t), _) == Nat.add(1n+SC.length(A, t), SC.length(A, acc)) : Nat}
187 succ_add(SC.length(A, t), SC.length(A, acc))
188
189# ---- Length ----
190def length_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Length.length_result(~A, ~cmp, xs):
191 {==}
192
193def length_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Length.length_frame(~A, ~cmp, xs):
194 {==}
195
196# ---- Empty_Set ----
197def new_empty(~A: Data, ~cmp: A -> A -> Cmp) -> {ST.model(~A, ~cmp, ST.initial(~A)) == Nil{} : List<&2, A>}:
198 new_abs(~A, ~cmp)
199
200# ---- Insert: one more element, exactly one more occurrence of it, still ordered ----
201def push_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +x: A) -> S.Insert.push_length(~A, ~cmp, xs, x):
202 ins_length(~A, ~cmp, x, xs)
203
204def 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):
205 BG.del_ins(~A, ~cmp, ~o, x, xs)
206
207def push_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +x: A, +hs: {S.sorted(~A, ~cmp, xs) == True{} : Bool}) -> S.Insert.push_sorted(~A, ~cmp, ~o, xs, x, hs):
208 ins_sorted(~A, ~cmp, ~o, x, xs, hs)
209
210# ---- First_Element: the minimum; nothing changes ----
211def peek_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {S.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> S.First_Element.peek_min(~A, ~cmp, h, t, hs):
212 ({==}, L.and_left(S.all_ge(~A, ~cmp, h, t), S.sorted(~A, ~cmp, t), hs))
213
214def peek_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.First_Element.peek_frame(~A, ~cmp, xs):
215 {==}
216
217def peek_empty(~A: Data, ~cmp: A -> A -> Cmp) -> S.First_Element.peek_empty(~A, ~cmp):
218 {==}
219
220# ---- Delete_First: the minimum is removed once; the result is it ----
221def pop_length(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> S.Delete_First.pop_length(~A, ~cmp, h, t):
222 {==}
223
224def pop_result(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> S.Delete_First.pop_result(~A, ~cmp, h, t):
225 {==}
226
227def pop_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {S.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> S.Delete_First.pop_min(~A, ~cmp, h, t, hs):
228 L.and_left(S.all_ge(~A, ~cmp, h, t), S.sorted(~A, ~cmp, t), hs)
229
230# the old multiset is the new one with the minimum put back
231def pop_bag(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +h: A, +t: List<&2, A>, +hs: {S.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> S.Delete_First.pop_bag(~A, ~cmp, ~o, h, t, hs):
232 M.ins_min(~A, ~cmp, ~o, h, t, L.and_left(S.all_ge(~A, ~cmp, h, t), S.sorted(~A, ~cmp, t), hs))
233
234def pop_empty(~A: Data, ~cmp: A -> A -> Cmp) -> S.Delete_First.pop_empty(~A, ~cmp):
235 {==}
236
237# ---- To_Set: the multiset of the list, ordered ----
238def 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):
239 {==}
240
241def 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):
242 Equal.trans(Nat, SC.length(A, S.from_list(~A, ~cmp, ys, Nil{})), Nat.add(SC.length(A, ys), 0n), SC.length(A, ys), from_list_length_go(~A, ~cmp, ys, Nil{}), N.add_zero(SC.length(A, ys)))
243
244def 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):
245 from_list_sorted_go(~A, ~cmp, ~o, ys, Nil{}, {==})
246
247# ---- Elements: to_sorted_list returns the ordered model ----
248def to_sorted_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Elements.to_sorted_result(~A, ~cmp, xs):
249 {==}
250
251def to_sorted_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Elements.to_sorted_frame(~A, ~cmp, xs):
252 {==}