1 import Base
2 import ../../lib/logic.bend as L
3 import ../../lib/list.bend as LL
4 import ../../lib/nat.bend as N
5 import ../../lib/array.bend as AR
6 import ../../lib/order.bend as O
7 import ../../../spec/lib/common.bend as SC
8 import ../../../spec/containers/binary_heap.bend as S
9 import ../../../src/containers/binary_heap.bend as H
10 import ../../../src/containers/types/binary_heap.bend as E
11 import ./state.bend as ST
12 import ./steps.bend as SP
13 import ./trace.bend as TR
14 import ../../../spec/lib/order.bend as SO
15 import ./multiset.bend as M
16 import ./vals.bend as VL
17 import ./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
47 def new_real(~A: Data, ~cmp: A -> A -> Cmp) -> {H.new(~A) == ST.real(~A, ST.initial(~A)) : H.Heap}:
48 ST.new_real(~A)
49
50 def new_inv(~A: Data, ~cmp: A -> A -> Cmp) -> {ST.good(~A, ~cmp, ST.initial(~A)) == True{} : Bool}:
51 ST.new_good(~A, ~cmp)
52
53 def 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
58 def step_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), sh: ST.Shadow, op: E.Op, +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.
63 def abs_real(~A: Data, ~cmp: A -> A -> Cmp, +sh: ST.Shadow) -> {ST.abs(~A, ~cmp, ST.real(~A, sh)) == ST.model(~A, ~cmp, sh) : List<&2, A>}:
64 ST.abs_real(~A, ~cmp, sh)
65
66 def 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
71 def trace_from(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ops: List<&2, E.Op>, +sh0: ST.Shadow, +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
74 def trace_new(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ops: List<&2, E.Op>, +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
79 def u32_step_ok(sh: ST.Shadow, op: E.Op, +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
82 def u32_trace(+ops: List<&2, E.Op>, +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
85 def u32_new_inv() -> ST.Inv(~U32, ~U32.cmp, H.new(~U32)):
86 new_heap_inv(~U32, ~U32.cmp)
87
88 def string_step_ok(sh: ST.Shadow, op: E.Op, +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
91 def string_trace(+ops: List<&2, E.Op>, +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
94 def 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 ----
101 def Impl(~A: Data, ~cmp: A -> A -> Cmp, sh: ST.Shadow, op: E.Op, Post: (List<&2, A> & E.Obs) -> Type) -> Type:
102 Sigma<&1, &1, ST.Shadow, sh2 => Sigma<&1, &1, E.Obs, o => {H.step(~A, ~cmp, ST.real(~A, sh), op) == (ST.real(~A, sh2), o) : H.Heap & E.Obs} & ({ST.good(~A, ~cmp, sh2) == True{} : Bool} & Post((ST.model(~A, ~cmp, sh2), o)))>>
103
104 def impl_of(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow, -op: E.Op, -Post: (List<&2, A> & E.Obs) -> 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, Post, S.step(~A, ~cmp, ST.model(~A, ~cmp, sh), op), (ST.model(~A, ~cmp, sh2), o), Equal.sym(List<&2, A> & E.Obs, (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)
110 def impl(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), sh: ST.Shadow, op: E.Op, +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) -> 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 ----
114 def 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
121 def 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
131 def 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
138 def 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
146 def model_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +sh: ST.Shadow) -> {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
151 def 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 ----
159 def 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
168 def 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
175 def 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
180 def 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 ----
190 def length_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Length.length_result(~A, ~cmp, xs):
191 {==}
192
193 def length_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Length.length_frame(~A, ~cmp, xs):
194 {==}
195
196 # ---- Empty_Set ----
197 def 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 ----
201 def 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
204 def 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
207 def 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 ----
211 def 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
214 def peek_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.First_Element.peek_frame(~A, ~cmp, xs):
215 {==}
216
217 def 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 ----
221 def 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
224 def 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
227 def 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
231 def 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
234 def 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 ----
238 def 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
241 def 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
244 def 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 ----
248 def to_sorted_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Elements.to_sorted_result(~A, ~cmp, xs):
249 {==}
250
251 def to_sorted_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Elements.to_sorted_frame(~A, ~cmp, xs):
252 {==}