# Documentation

Std.Data.PairingHeap

inductive Std.PairingHeapImp.Heap (α : Type u) :
• nil: {α : Type u} →

An empty forest, which has depth 0.

• node: {α : Type u} →

A forest consists of a root a, a forest child elements greater than a, and another forest sibling.

A Heap is the nodes of the pairing heap. Each node have two pointers: child 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.PairingHeapImp.instReprHeap :
{α : Type u_1} → [inst : Repr α] →

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

Equations
Instances For
def Std.PairingHeapImp.Heap.singleton {α : Type u_1} (a : α) :

A node containing a single element a.

Instances For

O(1). Is the heap empty?

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

O(1). Merge two heaps. Ignore siblings.

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

Auxiliary for Heap.deleteMin: merge the forest in pairs.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
def Std.PairingHeapImp.Heap.headD {α : Type u_1} (a : α) :

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

Instances For
@[inline]

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

Instances For
@[inline]
def Std.PairingHeapImp.Heap.deleteMin {α : Type u_1} (le : ααBool) :

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

Instances For
@[inline]
def Std.PairingHeapImp.Heap.tail? {α : Type u_1} (le : ααBool) (h : ) :

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

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

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

Instances For

A predicate says there is no more than one tree.

Instances For
theorem Std.PairingHeapImp.Heap.noSibling_merge {α : Type u_1} (le : ααBool) (s₁ : ) (s₂ : ) :
theorem Std.PairingHeapImp.Heap.noSibling_combine {α : Type u_1} (le : ααBool) (s : ) :
theorem Std.PairingHeapImp.Heap.noSibling_deleteMin {α : Type u_1} {le : ααBool} {a : α} {s' : } {s : } (eq : = some (a, s')) :
theorem Std.PairingHeapImp.Heap.noSibling_tail? {α : Type u_1} {le : ααBool} {s' : } {s : } :
theorem Std.PairingHeapImp.Heap.noSibling_tail {α : Type u_1} (le : ααBool) (s : ) :
theorem Std.PairingHeapImp.Heap.size_merge_node {α : Type u_1} (le : ααBool) (a₁ : α) (c₁ : ) (s₁ : ) (a₂ : α) (c₂ : ) (s₂ : ) :
theorem Std.PairingHeapImp.Heap.size_merge {α : Type u_1} (le : ααBool) {s₁ : } {s₂ : } (h₁ : ) (h₂ : ) :
theorem Std.PairingHeapImp.Heap.size_combine {α : Type u_1} (le : ααBool) (s : ) :
theorem Std.PairingHeapImp.Heap.size_deleteMin {α : Type u_1} {le : ααBool} {a : α} {s' : } {s : } (eq : = some (a, s')) :
theorem Std.PairingHeapImp.Heap.size_tail? {α : Type u_1} {le : ααBool} {s' : } {s : } :
theorem Std.PairingHeapImp.Heap.size_tail {α : Type u_1} (le : ααBool) {s : } :
theorem Std.PairingHeapImp.Heap.size_deleteMin_lt {α : Type u_1} {le : ααBool} {a : α} {s' : } {s : } (eq : = some (a, s')) :
theorem Std.PairingHeapImp.Heap.size_tail?_lt {α : Type u_1} {le : ααBool} {s' : } {s : } :
@[specialize #[]]
def Std.PairingHeapImp.Heap.foldM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (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.
Instances For
@[inline]
def Std.PairingHeapImp.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.

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

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

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

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

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

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

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

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

Instances For

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

Instances For

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

Instances For
def Std.PairingHeapImp.Heap.NodeWF {α : 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)
Equations
Instances For
inductive Std.PairingHeapImp.Heap.WF {α : Type u_1} (le : ααBool) :

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

• There is no more than one tree.
• It is a le-min-heap (if le is well-behaved)
Instances For
theorem Std.PairingHeapImp.Heap.WF.singleton :
∀ {α : Type u_1} {a : α} {le : ααBool},
theorem Std.PairingHeapImp.Heap.WF.merge_node :
∀ {α : Type u_1} {le : ααBool} {a₁ : α} {c₁ : } {a₂ : α} {c₂ s₁ s₂ : }, Std.PairingHeapImp.Heap.WF le (Std.PairingHeapImp.Heap.merge le () ())
theorem Std.PairingHeapImp.Heap.WF.merge :
∀ {α : Type u_1} {le : ααBool} {s₁ s₂ : },
theorem Std.PairingHeapImp.Heap.WF.combine :
∀ {α : Type u_1} {le : ααBool} {s : } {a : α},
theorem Std.PairingHeapImp.Heap.WF.deleteMin {α : Type u_1} {le : ααBool} {a : α} {s' : } {s : } (h : ) (eq : = some (a, s')) :
theorem Std.PairingHeapImp.Heap.WF.tail? {α : Type u_1} {s : } {le : ααBool} {tl : } (hwf : ) :
theorem Std.PairingHeapImp.Heap.WF.tail {α : Type u_1} {s : } {le : ααBool} (hwf : ) :
theorem Std.PairingHeapImp.Heap.deleteMin_fst {α : Type u_1} {s : } {le : ααBool} :
Option.map (fun x => x.fst) () =
def Std.PairingHeap (α : Type u) (le : ααBool) :

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

• insert : α → PairingHeap α → PairingHeap α: add an element to the heap
• deleteMin : PairingHeap α → Option (α × PairingHeap α): remove the minimum element from the heap
• merge : PairingHeap α → PairingHeap α → PairingHeap α: 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 PairingHeap, insert and merge are O(1), deleteMin is amortized O(log n).

Note that deleteMin may be O(n) in a single operation. So if you need an efficient persistent priority queue, you should use other data structures with better worst-case time.

Instances For
@[inline]
def Std.mkPairingHeap (α : Type u) (le : ααBool) :

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

Instances For
@[inline]
def Std.PairingHeap.empty {α : Type u} {le : ααBool} :

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

Instances For
instance Std.PairingHeap.instInhabitedPairingHeap {α : Type u} {le : ααBool} :
@[inline]
def Std.PairingHeap.isEmpty {α : Type u} {le : ααBool} (b : ) :

O(1). Is the heap empty?

Instances For
@[inline]
def Std.PairingHeap.size {α : Type u} {le : ααBool} (b : ) :

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

Instances For
@[inline]
def Std.PairingHeap.singleton {α : Type u} {le : ααBool} (a : α) :

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

Instances For
@[inline]
def Std.PairingHeap.merge {α : Type u} {le : ααBool} :

O(1). Merge the contents of two heaps.

Instances For
@[inline]
def Std.PairingHeap.insert {α : Type u} {le : ααBool} (a : α) (h : ) :

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

Instances For
def Std.PairingHeap.ofList {α : Type u} (le : ααBool) (as : List α) :

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

Instances For
def Std.PairingHeap.ofArray {α : Type u} (le : ααBool) (as : ) :

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

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

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

Instances For
@[inline]
def Std.PairingHeap.head? {α : Type u} {le : ααBool} (b : ) :

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

Instances For
@[inline]
def Std.PairingHeap.head! {α : Type u} {le : ααBool} [] (b : ) :
α

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

Instances For
@[inline]
def Std.PairingHeap.headI {α : Type u} {le : ααBool} [] (b : ) :
α

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

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

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

Instances For
@[inline]
def Std.PairingHeap.tail {α : Type u} {le : ααBool} (b : ) :

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

Instances For
@[inline]
def Std.PairingHeap.toList {α : Type u} {le : ααBool} (b : ) :
List α

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

Instances For
@[inline]
def Std.PairingHeap.toArray {α : Type u} {le : ααBool} (b : ) :

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

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

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

Instances For
@[inline]
def Std.PairingHeap.toArrayUnordered {α : Type u} {le : ααBool} (b : ) :

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

Instances For