Documentation

Batteries.Data.BinomialHeap.Basic

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
Equations
  • Batteries.BinomialHeap.Imp.instReprHeapNode = { reprPrec := Batteries.BinomialHeap.Imp.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

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

Equations

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

Instances For
Equations
  • Batteries.BinomialHeap.Imp.instReprHeap = { reprPrec := Batteries.BinomialHeap.Imp.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
@[inline]

O(1). Is the heap empty?

Equations
  • Batteries.BinomialHeap.Imp.Heap.nil.isEmpty = true
  • x.isEmpty = false
@[inline]

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
Instances For
instance Batteries.BinomialHeap.Imp.instDecidableRankGT :
{α : Type u_1} → {s : Batteries.BinomialHeap.Imp.Heap α} → {n : Nat} → Decidable (s.rankGT n)
Equations

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

Equations
@[inline]

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

Equations
@[irreducible, specialize #[]]

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 Batteries.BinomialHeap.Imp.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]

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

Equations
structure Batteries.BinomialHeap.Imp.FindMin (α : Type u_1) :
Type u_1

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

@[specialize #[]]

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

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

Equations
@[inline]

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

Equations
@[inline]

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

Equations
@[irreducible]
theorem Batteries.BinomialHeap.Imp.Heap.realSize_merge {α : Type u_1} (le : ααBool) (s₁ : Batteries.BinomialHeap.Imp.Heap α) (s₂ : Batteries.BinomialHeap.Imp.Heap α) :
(Batteries.BinomialHeap.Imp.Heap.merge le s₁ s₂).realSize = s₁.realSize + s₂.realSize
theorem Batteries.BinomialHeap.Imp.Heap.realSize_deleteMin {α : Type u_1} {le : ααBool} {a : α} {s' : Batteries.BinomialHeap.Imp.Heap α} {s : Batteries.BinomialHeap.Imp.Heap α} (eq : Batteries.BinomialHeap.Imp.Heap.deleteMin le s = some (a, s')) :
s.realSize = s'.realSize + 1
@[irreducible, specialize #[]]
def Batteries.BinomialHeap.Imp.Heap.foldM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (le : ααBool) (s : Batteries.BinomialHeap.Imp.Heap α) (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 Batteries.BinomialHeap.Imp.Heap.fold {α : Type u_1} {β : Type u_2} (le : ααBool) (s : Batteries.BinomialHeap.Imp.Heap α) (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]

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

Equations
@[inline]

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

Equations
@[specialize #[]]
def Batteries.BinomialHeap.Imp.HeapNode.foldTreeM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (nil : β) (join : αββm β) :

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

Equations
@[specialize #[]]
def Batteries.BinomialHeap.Imp.Heap.foldTreeM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (nil : β) (join : αββm β) :

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

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

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 Batteries.BinomialHeap.Imp.HeapNode.WF {α : 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 Batteries.BinomialHeap.Imp.Heap.WF {α : 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 Batteries.BinomialHeap.Imp.Heap.WF.nil :
∀ {α : Type u_1} {le : ααBool} {n : Nat}, Batteries.BinomialHeap.Imp.Heap.WF le n Batteries.BinomialHeap.Imp.Heap.nil
theorem Batteries.BinomialHeap.Imp.Heap.WF.of_rankGT :
∀ {α : Type u_1} {le : ααBool} {n' : Nat} {s : Batteries.BinomialHeap.Imp.Heap α} {n : Nat}, s.rankGT nBatteries.BinomialHeap.Imp.Heap.WF le n' sBatteries.BinomialHeap.Imp.Heap.WF le (n + 1) s
theorem Batteries.BinomialHeap.Imp.Heap.rankGT.of_le :
∀ {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {n n' : Nat}, s.rankGT nn' ns.rankGT n'
theorem Batteries.BinomialHeap.Imp.Heap.WF.rankGT :
∀ {α : Type u_1} {lt : ααBool} {n : Nat} {s : Batteries.BinomialHeap.Imp.Heap α}, Batteries.BinomialHeap.Imp.Heap.WF lt (n + 1) ss.rankGT n
@[irreducible]
theorem Batteries.BinomialHeap.Imp.Heap.WF.merge' :
∀ {α : Type u_1} {le : ααBool} {s₁ s₂ : Batteries.BinomialHeap.Imp.Heap α} {n : Nat}, Batteries.BinomialHeap.Imp.Heap.WF le n s₁Batteries.BinomialHeap.Imp.Heap.WF le n s₂Batteries.BinomialHeap.Imp.Heap.WF le n (Batteries.BinomialHeap.Imp.Heap.merge le s₁ s₂) ((s₁.rankGT n s₂.rankGT n)(Batteries.BinomialHeap.Imp.Heap.merge le s₁ s₂).rankGT n)
theorem Batteries.BinomialHeap.Imp.HeapNode.WF.rank_eq {α : Type u_1} {le : ααBool} {a : α} {n : Nat} {s : Batteries.BinomialHeap.Imp.HeapNode α} :
structure Batteries.BinomialHeap.Imp.FindMin.WF {α : Type u_1} (le : ααBool) (res : Batteries.BinomialHeap.Imp.FindMin α) :

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.

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

node is a well formed forest of rank rank with val at the root.

next is a binomial heap with ranks above rank + 1.

The conditions under which findMin is well-formed.

Equations
  • One or more equations did not get rendered due to their size.
  • h_2.findMin hr hk = hr
def Batteries.BinomialHeap (α : Type u) (le : ααBool) :
Type (max 0 u)

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

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
Instances For
@[inline]
def Batteries.mkBinomialHeap (α : Type u) (le : ααBool) :

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

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

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

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

O(1). Is the heap empty?

Equations
  • b.isEmpty = b.val.isEmpty
@[inline]
def Batteries.BinomialHeap.size {α : Type u} {le : ααBool} (b : Batteries.BinomialHeap α le) :

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

Equations
  • b.size = b.val.size
@[inline]
def Batteries.BinomialHeap.singleton {α : Type u} {le : ααBool} (a : α) :

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

Equations
@[inline]

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

Equations
@[inline]
def Batteries.BinomialHeap.insert {α : Type u} {le : ααBool} (a : α) (h : Batteries.BinomialHeap α le) :

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

Equations
def Batteries.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 Batteries.BinomialHeap.ofArray {α : Type u} (le : ααBool) (as : Array α) :

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

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

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

Equations
instance Batteries.BinomialHeap.instStream {α : Type u} {le : ααBool} :
Equations
  • Batteries.BinomialHeap.instStream = { next? := Batteries.BinomialHeap.deleteMin }
def Batteries.BinomialHeap.forIn {α : Type u} {le : ααBool} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (b : Batteries.BinomialHeap α le) (x : β) (f : αβm (ForInStep β)) :
m β

O(n log n). Implementation of for x in (b : BinomialHeap α le) ... notation, which iterates over the elements in the heap in increasing order.

Equations
instance Batteries.BinomialHeap.instForIn {α : Type u} {le : ααBool} {m : Type u_1 → Type u_2} :
Equations
  • Batteries.BinomialHeap.instForIn = { forIn := fun {β : Type ?u.29} [Monad m] => Batteries.BinomialHeap.forIn }
@[inline]
def Batteries.BinomialHeap.head? {α : Type u} {le : ααBool} (b : Batteries.BinomialHeap α le) :

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

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

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

Equations
  • b.head! = b.head?.get!
@[inline]
def Batteries.BinomialHeap.headI {α : Type u} {le : ααBool} [Inhabited α] (b : Batteries.BinomialHeap α le) :
α

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

Equations
  • b.headI = b.head?.getD default
@[inline]
def Batteries.BinomialHeap.tail? {α : Type u} {le : ααBool} (b : Batteries.BinomialHeap α le) :

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

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

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

Equations
@[inline]
def Batteries.BinomialHeap.foldM {α : Type u} {le : ααBool} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (b : Batteries.BinomialHeap α le) (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
@[inline]
def Batteries.BinomialHeap.fold {α : Type u} {le : ααBool} {β : Type u_1} (b : Batteries.BinomialHeap α le) (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 Batteries.BinomialHeap.toList {α : Type u} {le : ααBool} (b : Batteries.BinomialHeap α le) :
List α

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

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

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

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

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

Equations
  • b.toListUnordered = b.val.toListUnordered
@[inline]
def Batteries.BinomialHeap.toArrayUnordered {α : Type u} {le : ααBool} (b : Batteries.BinomialHeap α le) :

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

Equations
  • b.toArrayUnordered = b.val.toArrayUnordered