// In a priority queue, `Dequeue` returns the *lowest* value on the queue.
module PriorityQueue {
  // Idea: store the queue as a balanced binary heap.

  datatype PriorityQueue =
    | Leaf
    | Node(x: int, left: PriorityQueue, right: PriorityQueue)

  // A *representation invariant*.
  ghost predicate Valid(pq: PriorityQueue) {
    IsBinaryHeap(pq) && IsBalanced(pq)
  }

  // 1. Write a recursive definition: the root of the tree is the lowest number,
  //                                  allowing ties
  ghost predicate IsBinaryHeap(pq: PriorityQueue) {
    true
  }

  // 2. Write a recursive definition: every left child has the same number of
  //                                  elements as its right sibling, or one more
  ghost predicate IsBalanced(pq: PriorityQueue) {
    true
  }

  // Use this *abstraction function* in predicate 2.
  // *Don't* use it in predicate 1...
  ghost function Elements(pq: PriorityQueue): multiset<int> {
    match pq
    case Leaf => multiset{}
    case Node(x, left, right) => multiset{x} + Elements(left) + Elements(right)
  }

  // 3. ... but now show that your IsBinaryHeap definition (without Elements)
  //        is correct:
  lemma {:induction false} BinaryHeapStoresMinimum(pq: PriorityQueue, y: int)
    requires IsBinaryHeap(pq) && y in Elements(pq)
    ensures pq.x <= y
  {
  }
}