def merge_all

bend-kit-scheduler@0.4.1.0 · queue_proof.bend:102

import Base
import bend-kit-collections@0.1.4.1/heap.bend as H
import bend-kit-scheduler@0.4.1.0/queue.bend as Q
import bend-kit-scheduler@0.4.1.0/queue_laws.bend as L

102# Merging cannot introduce an element that violates any predicate P. Fuel zero
103# returns the left heap, so this lemma does not trust cached heap sizes.
104def merge_all(~A: Data, -P: Q.Ticket<A> -> Data, +fuel: Nat, +a: H.Heap<Q.Ticket<A>>, +b: H.Heap<Q.Ticket<A>>, +ea: L.all.heap(A, P, a), +eb: L.all.heap(A, P, b)) -> L.all.heap(A, P, H.Heap.merge.go(~Q.Ticket<A>, ~(x => y => Q.le(A, x, y)), fuel, a, b)):
105  match fuel:
106    case 0n:
107      ea
108    case 1n+f:
109      match a b:
110        case H.HLeaf{} H.HLeaf{}:
111          Unit{}
112        case H.HLeaf{} H.HNode{nb, y, bl, br}:
113          eb
114        case H.HNode{na, x, al, ar} H.HLeaf{}:
115          ea
116        case H.HNode{na, x, al, ar} H.HNode{nb, y, bl, br}:
117          L.Both{ex, L.Both{eal, ear}} = ea
118          L.Both{ey, L.Both{ebl, ebr}} = eb
119          split(c => L.all.heap(A, P, H.HNode{Nat.add(na, nb), Bool.pick(Q.Ticket<A>, c, x, y), H.Heap.merge.go(~Q.Ticket<A>, ~(x => y => Q.le(A, x, y)), f, Bool.pick(H.Heap<Q.Ticket<A>>, c, ar, br), Bool.pick(H.Heap<Q.Ticket<A>>, c, H.HNode{nb, y, bl, br}, H.HNode{na, x, al, ar})), Bool.pick(H.Heap<Q.Ticket<A>>, c, al, bl)}), Q.le(A, x, y),
120            e => L.Both{ex, L.Both{merge_all(~A, P, f, ar, H.HNode{nb, y, bl, br}, ear, L.Both{ey, L.Both{ebl, ebr}}), eal}},
121            e => L.Both{ey, L.Both{merge_all(~A, P, f, br, H.HNode{na, x, al, ar}, ebr, L.Both{ex, L.Both{eal, ear}}), ebl}})