# Documentation

Std.Data.BinomialHeap

inductive Std.BinomialHeapImp.HeapNode (α : Type u) :
• An empty forest, which has depth 0.

nil: {α : Type u} →
• A forest of rank r + 1 consists of a root a, a forest child of rank r elements greater than a, and another forest sibling of rank r.

node: {α : Type u} →

A HeapNode is one of the internal nodes of the binomial heap. It is always a perfect binary tree, with the depth of the tree stored in the Heap. However the interpretation of the two pointers is different: we view the child as going to the first child of this node, and sibling goes to the next sibling of this tree. So it actually encodes a forest where each node has children node.child, node.child.sibling, node.child.sibling.sibling, etc.

Each edge in this forest denotes a le a b relation that has been checked, so the root is smaller than everything else under it.

Instances For
instance Std.BinomialHeapImp.instReprHeapNode :
{α : Type u_1} → [inst : Repr α] →
Equations
• Std.BinomialHeapImp.instReprHeapNode = { reprPrec := Std.BinomialHeapImp.reprHeapNode✝ }

The "real size" of the node, counting up how many values of type α are stored. This is O(n) and is intended mainly for specification purposes. For a well formed HeapNode the size is always 2^n - 1 where n is the depth.

Equations

A node containing a single element a.

Equations
@[inline]

O(log n). The rank, or the number of trees in the forest. It is also the depth of the forest.

Equations

Computes s.rank + r

Equations
inductive Std.BinomialHeapImp.Heap (α : Type u) :
• An empty heap.

nil: {α : Type u} →
• A cons node contains a tree of root val, children node and rank rank, and then next which is the rest of the forest.

cons: {α : Type u} →

A Heap is the top level structure in a binomial heap. It consists of a forest of HeapNodes with strictly increasing ranks.

Instances For
instance Std.BinomialHeapImp.instReprHeap :
{α : Type u_1} → [inst : Repr α] →
Equations
• Std.BinomialHeapImp.instReprHeap = { reprPrec := Std.BinomialHeapImp.reprHeap✝ }

O(n). The "real size" of the heap, counting up how many values of type α are stored. This is intended mainly for specification purposes. Prefer Heap.size, which is the same for well formed heaps.

Equations

O(log n). The number of elements in the heap.

Equations

O(1). Is the heap empty?

Equations
• = match x with | Std.BinomialHeapImp.Heap.nil => true | x => false
def Std.BinomialHeapImp.Heap.singleton {α : Type u_1} (a : α) :

O(1). The heap containing a single value a.

Equations

O(1). Auxiliary for Heap.merge: Is the minimum rank in Heap strictly larger than n?

Equations
instance Std.BinomialHeapImp.instDecidableRankGT :
{α : Type u_1} → {s : } → {n : Nat} →
Equations
• One or more equations did not get rendered due to their size.

O(log n). The number of trees in the forest.

Equations
@[specialize #[]]
def Std.BinomialHeapImp.combine {α : Type u_1} (le : ααBool) (a₁ : α) (a₂ : α) (n₁ : ) (n₂ : ) :

O(1). Auxiliary for Heap.merge: combines two heap nodes of the same rank into one with the next larger rank.

Equations
@[specialize #[]]
def Std.BinomialHeapImp.Heap.merge {α : Type u_1} (le : ααBool) :

Merge two forests of binomial trees. The forests are assumed to be ordered by rank and merge maintains this invariant.

Equations

O(log n). Convert a HeapNode to a Heap by reversing the order of the nodes along the sibling spine.

Equations

Computes s.toHeap ++ res tail-recursively, assuming n = s.rank.

Equations
@[specialize #[]]
def Std.BinomialHeapImp.Heap.headD {α : Type u_1} (le : ααBool) (a : α) :

O(log n). Get the smallest element in the heap, including the passed in value a.

Equations
@[inline]
def Std.BinomialHeapImp.Heap.head? {α : Type u_1} (le : ααBool) :

O(log n). Get the smallest element in the heap, if it has an element.

Equations
structure Std.BinomialHeapImp.FindMin (α : Type u_1) :
Type u_1
• The list of elements prior to the minimum element, encoded as a "difference list".

before :
• The minimum element.

val : α
• The children of the minimum element.

node :
• The forest after the minimum element.

next :

The return type of FindMin, which encodes various quantities needed to reconstruct the tree in deleteMin.

Instances For
@[specialize #[]]
def Std.BinomialHeapImp.Heap.findMin {α : Type u_1} (le : ααBool) (k : ) :

O(log n). Find the minimum element, and return a data structure FindMin with information needed to reconstruct the rest of the binomial heap.

Equations
def Std.BinomialHeapImp.Heap.deleteMin {α : Type u_1} (le : ααBool) :

O(log n). Find and remove the the minimum element from the binomial heap.

Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Std.BinomialHeapImp.Heap.tail? {α : Type u_1} (le : ααBool) (h : ) :

O(log n). Get the tail of the binomial heap after removing the minimum element.

Equations
@[inline]
def Std.BinomialHeapImp.Heap.tail {α : Type u_1} (le : ααBool) (h : ) :

O(log n). Remove the minimum element of the heap.

Equations
theorem Std.BinomialHeapImp.Heap.realSize_merge {α : Type u_1} (le : ααBool) (s₁ : ) (s₂ : ) :
theorem Std.BinomialHeapImp.Heap.realSize_findMin {α : Type u_1} {k : } {n : Nat} {le : ααBool} {res : } {s : } (m : Nat) (hk : ) (eq : ) (hres : ) :
theorem Std.BinomialHeapImp.HeapNode.realSize_toHeap.go {α : Type u_1} {n : Nat} {res : } (s : ) :
theorem Std.BinomialHeapImp.Heap.realSize_deleteMin {α : Type u_1} {le : ααBool} {a : α} {s' : } {s : } (eq : = some (a, s')) :
theorem Std.BinomialHeapImp.Heap.realSize_tail? {α : Type u_1} {le : ααBool} {s' : } {s : } :
theorem Std.BinomialHeapImp.Heap.realSize_tail {α : Type u_1} (le : ααBool) (s : ) :
@[specialize #[]]
def Std.BinomialHeapImp.Heap.foldM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : ] (le : ααBool) (s : ) (init : β) (f : βαm β) :
m β

O(n log n). Monadic fold over the elements of a heap in increasing order, by repeatedly pulling the minimum element out of the heap.

Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Std.BinomialHeapImp.Heap.fold {α : Type u_1} {β : Type u_2} (le : ααBool) (s : ) (init : β) (f : βαβ) :
β

O(n log n). Fold over the elements of a heap in increasing order, by repeatedly pulling the minimum element out of the heap.

Equations
@[inline]
def Std.BinomialHeapImp.Heap.toArray {α : Type u_1} (le : ααBool) (s : ) :

O(n log n). Convert the heap to an array in increasing order.

Equations
@[inline]
def Std.BinomialHeapImp.Heap.toList {α : Type u_1} (le : ααBool) (s : ) :
List α

O(n log n). Convert the heap to a list in increasing order.

Equations
@[specialize #[]]
def Std.BinomialHeapImp.HeapNode.foldTreeM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : ] (nil : β) (join : αββm β) :

O(n). Fold a monadic function over the tree structure to accumulate a value.

Equations
@[specialize #[]]
def Std.BinomialHeapImp.Heap.foldTreeM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : ] (nil : β) (join : αββm β) :
m β

O(n). Fold a monadic function over the tree structure to accumulate a value.

Equations
@[inline]
def Std.BinomialHeapImp.Heap.foldTree {β : Type u_1} {α : Type u_2} (nil : β) (join : αβββ) (s : ) :
β

O(n). Fold a function over the tree structure to accumulate a value.

Equations

O(n). Convert the heap to a list in arbitrary order.

Equations

O(n). Convert the heap to an array in arbitrary order.

Equations
def Std.BinomialHeapImp.HeapNode.WellFormed {α : Type u_1} (le : ααBool) (a : α) :

The well formedness predicate for a heap node. It asserts that:

• If a is added at the top to make the forest into a tree, the resulting tree is a le-min-heap (if le is well-behaved)
• When interpreting child and sibling as left and right children of a binary tree, it is a perfect binary tree with depth r
Equations
def Std.BinomialHeapImp.Heap.WellFormed {α : Type u_1} (le : ααBool) (n : Nat) :

The well formedness predicate for a binomial heap. It asserts that:

• It consists of a list of well formed trees with the specified ranks
• The ranks are in strictly increasing order, and all are at least n
Equations
theorem Std.BinomialHeapImp.Heap.WellFormed.nil :
∀ {α : Type u_1} {le : ααBool} {n : Nat}, Std.BinomialHeapImp.Heap.WellFormed le n Std.BinomialHeapImp.Heap.nil
theorem Std.BinomialHeapImp.Heap.WellFormed.singleton :
∀ {α : Type u_1} {a : α} {le : ααBool},
theorem Std.BinomialHeapImp.Heap.WellFormed.of_rankGT :
∀ {α : Type u_1} {s : } {le : ααBool} {n' n : Nat}, Std.BinomialHeapImp.Heap.WellFormed le (n + 1) s
theorem Std.BinomialHeapImp.Heap.WellFormed.of_le {n : Nat} {n' : Nat} :
∀ {α : Type u_1} {s : } {le : ααBool}, n n'
theorem Std.BinomialHeapImp.Heap.rankGT.le_trans :
∀ {α : Type u_1} {s : } {n n' : Nat}, n' n
theorem Std.BinomialHeapImp.Heap.WellFormed.rankGT :
∀ {α : Type u_1} {lt : ααBool} {n : Nat} {s : }, Std.BinomialHeapImp.Heap.WellFormed lt (n + 1) s
theorem Std.BinomialHeapImp.Heap.WellFormed.merge' :
∀ {α : Type u_1} {le : ααBool} {s₁ s₂ : } {n : Nat}, ()
theorem Std.BinomialHeapImp.Heap.WellFormed.merge :
∀ {α : Type u_1} {le : ααBool} {s₁ s₂ : } {n : Nat},
theorem Std.BinomialHeapImp.Heap.findMin_val {α : Type u_1} {s : } {le : ααBool} {k : } {res : } :
().val = Std.BinomialHeapImp.Heap.headD le res.val s
theorem Std.BinomialHeapImp.Heap.deleteMin_fst {α : Type u_1} {s : } {le : ααBool} :
Option.map (fun x => x.fst) () =

O(log n). The rank, or the number of trees in the forest. This is the same as rankTR but it is not tail recursive.

Equations
@[simp]
@[simp]
theorem Std.BinomialHeapImp.HeapNode.WellFormed.rank_eq {α : Type u_1} {le : ααBool} {a : α} {n : Nat} {s : } :
@[simp]
theorem Std.BinomialHeapImp.HeapNode.WellFormed.realSize_eq {α : Type u_1} {le : ααBool} {a : α} {n : Nat} {s : } :
@[simp]
theorem Std.BinomialHeapImp.Heap.WellFormed.size_eq {α : Type u_1} {le : ααBool} {n : Nat} {s : } :
theorem Std.BinomialHeapImp.HeapNode.WellFormed.toHeap {α : Type u_1} {le : ααBool} {a : α} {n : Nat} {s : } (h : ) :
theorem Std.BinomialHeapImp.HeapNode.WellFormed.toHeap.go {α : Type u_1} {le : ααBool} {a : α} {res : } {n : Nat} {s : } :
structure Std.BinomialHeapImp.FindMin.WellFormed {α : Type u_1} (le : ααBool) (res : ) :
• The rank of the minimum element

rank : Nat
• before is a difference list which can be appended to a binomial heap with ranks at least rank to produce another well formed heap.

before : ∀ {s : },
• node is a well formed forest of rank rank with val at the root.

node : Std.BinomialHeapImp.HeapNode.WellFormed le res.val res.node rank
• next is a binomial heap with ranks above rank + 1.

next : Std.BinomialHeapImp.Heap.WellFormed le (rank + 1) res.next

The well formedness predicate for a FindMin value. This is not actually a predicate, as it contains an additional data value rank corresponding to the rank of the returned node, which is omitted from findMin.

Instances For
theorem Std.BinomialHeapImp.Heap.WellFormed.findMin {α : Type u_1} {le : ααBool} {n : Nat} {k : } {res : } {s : } (h : ) (hr : ) (hk : ∀ {s : }, ) :
theorem Std.BinomialHeapImp.Heap.WellFormed.deleteMin {α : Type u_1} {le : ααBool} {n : Nat} {a : α} {s' : } {s : } (h : ) (eq : = some (a, s')) :
theorem Std.BinomialHeapImp.Heap.WellFormed.tail? {α : Type u_1} {s : } {le : ααBool} {n : Nat} {tl : } (hwf : ) :
theorem Std.BinomialHeapImp.Heap.WellFormed.tail {α : Type u_1} {s : } {le : ααBool} {n : Nat} (hwf : ) :
def Std.BinomialHeap (α : Type u) (le : ααBool) :

A binomial heap is a data structure which supports the following primary operations:

• insert : α → BinomialHeap α → BinomialHeap α→ BinomialHeap α → BinomialHeap α→ BinomialHeap α: add an element to the heap
• deleteMin : BinomialHeap α → Option (α × BinomialHeap α)→ Option (α × BinomialHeap α)× BinomialHeap α): remove the minimum element from the heap
• merge : BinomialHeap α → BinomialHeap α → BinomialHeap α→ BinomialHeap α → BinomialHeap α→ BinomialHeap α: combine two heaps

The first two operations are known as a "priority queue", so this could be called a "mergeable priority queue". The standard choice for a priority queue is a binary heap, which supports insert and deleteMin in O(log n), but merge is O(n). With a BinomialHeap, all three operations are O(log n).

Equations
• = { h // }
@[inline]
def Std.mkBinomialHeap (α : Type u) (le : ααBool) :

O(1). Make a new empty binomial heap.

Equations
@[inline]
def Std.BinomialHeap.empty {α : Type u} {le : ααBool} :

O(1). Make a new empty binomial heap.

Equations
• Std.BinomialHeap.empty =
instance Std.BinomialHeap.instInhabitedBinomialHeap {α : Type u} {le : ααBool} :
Equations
• Std.BinomialHeap.instInhabitedBinomialHeap = { default := Std.BinomialHeap.empty }
@[inline]
def Std.BinomialHeap.isEmpty {α : Type u} {le : ααBool} (b : ) :

O(1). Is the heap empty?

Equations
@[inline]
def Std.BinomialHeap.size {α : Type u} {le : ααBool} (b : ) :

O(log n). The number of elements in the heap.

Equations
@[inline]
def Std.BinomialHeap.singleton {α : Type u} {le : ααBool} (a : α) :

O(1). Make a new heap containing a.

Equations
• = { val := , property := }
@[inline]
def Std.BinomialHeap.merge {α : Type u} {le : ααBool} :

O(log n). Merge the contents of two heaps.

Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Std.BinomialHeap.insert {α : Type u} {le : ααBool} (a : α) (h : ) :

O(log n). Add element a to the given heap h.

Equations
def Std.BinomialHeap.ofList {α : Type u} (le : ααBool) (as : List α) :

O(n log n). Construct a heap from a list by inserting all the elements.

Equations
def Std.BinomialHeap.ofArray {α : Type u} (le : ααBool) (as : ) :

O(n log n). Construct a heap from a list by inserting all the elements.

Equations
@[inline]
def Std.BinomialHeap.deleteMin {α : Type u} {le : ααBool} (b : ) :
Option (α × )

O(log n). Remove and return the minimum element from the heap.

Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Std.BinomialHeap.head? {α : Type u} {le : ααBool} (b : ) :

O(log n). Returns the smallest element in the heap, or none if the heap is empty.

Equations
@[inline]
def Std.BinomialHeap.head! {α : Type u} {le : ααBool} [inst : ] (b : ) :
α

O(log n). Returns the smallest element in the heap, or panics if the heap is empty.

Equations
@[inline]
def Std.BinomialHeap.headI {α : Type u} {le : ααBool} [inst : ] (b : ) :
α

O(log n). Returns the smallest element in the heap, or default if the heap is empty.

Equations
@[inline]
def Std.BinomialHeap.tail? {α : Type u} {le : ααBool} (b : ) :

O(log n). Removes the smallest element from the heap, or none if the heap is empty.

Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Std.BinomialHeap.tail {α : Type u} {le : ααBool} (b : ) :

O(log n). Removes the smallest element from the heap, if possible.

Equations
• = { val := , property := (_ : ) }
@[inline]
def Std.BinomialHeap.toList {α : Type u} {le : ααBool} (b : ) :
List α

O(n log n). Convert the heap to a list in increasing order.

Equations
@[inline]
def Std.BinomialHeap.toArray {α : Type u} {le : ααBool} (b : ) :

O(n log n). Convert the heap to an array in increasing order.

Equations
@[inline]
def Std.BinomialHeap.toListUnordered {α : Type u} {le : ααBool} (b : ) :
List α

O(n). Convert the heap to a list in arbitrary order.

Equations
@[inline]
def Std.BinomialHeap.toArrayUnordered {α : Type u} {le : ααBool} (b : ) :

O(n). Convert the heap to an array in arbitrary order.

Equations