ink

inductive Std.BinomialHeapImp.HeapNode (α : Type u) : Type u

• An empty forest, which has depth 0.

  nil: {α : Type u} → Std.BinomialHeapImp.HeapNode α

• 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} → α → Std.BinomialHeapImp.HeapNode α → Std.BinomialHeapImp.HeapNode α → Std.BinomialHeapImp.HeapNode α

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.

ink

instance Std.BinomialHeapImp.instReprHeapNode : {α : Type u_1} → [inst : Repr α] → Repr (Std.BinomialHeapImp.HeapNode α)

Equations

• Std.BinomialHeapImp.instReprHeapNode = { reprPrec := Std.BinomialHeapImp.reprHeapNode✝ }

ink

def Std.BinomialHeapImp.HeapNode.realSize {α : Type u_1} : Std.BinomialHeapImp.HeapNode α → Nat

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

• Std.BinomialHeapImp.HeapNode.realSize Std.BinomialHeapImp.HeapNode.nil = 0
• Std.BinomialHeapImp.HeapNode.realSize (Std.BinomialHeapImp.HeapNode.node a a_1 a_2) = Std.BinomialHeapImp.HeapNode.realSize a_1 + 1 + Std.BinomialHeapImp.HeapNode.realSize a_2

ink

def Std.BinomialHeapImp.HeapNode.singleton {α : Type u_1} (a : α) : Std.BinomialHeapImp.HeapNode α

A node containing a single element a.

Equations

• Std.BinomialHeapImp.HeapNode.singleton a = Std.BinomialHeapImp.HeapNode.node a Std.BinomialHeapImp.HeapNode.nil Std.BinomialHeapImp.HeapNode.nil

ink

@[inline]

def Std.BinomialHeapImp.HeapNode.rankTR {α : Type u_1} (s : Std.BinomialHeapImp.HeapNode α) : Nat

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

Equations

• Std.BinomialHeapImp.HeapNode.rankTR s = Std.BinomialHeapImp.HeapNode.rankTR.go s 0

ink

def Std.BinomialHeapImp.HeapNode.rankTR.go {α : Type u_1} : Std.BinomialHeapImp.HeapNode α → Nat → Nat

Computes s.rank + r

Equations

• Std.BinomialHeapImp.HeapNode.rankTR.go Std.BinomialHeapImp.HeapNode.nil x = x
• Std.BinomialHeapImp.HeapNode.rankTR.go (Std.BinomialHeapImp.HeapNode.node a child s) x = Std.BinomialHeapImp.HeapNode.rankTR.go s (x + 1)

ink

inductive Std.BinomialHeapImp.Heap (α : Type u) : Type u

• An empty heap.

  nil: {α : Type u} → Std.BinomialHeapImp.Heap α

• 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} → Nat → α → Std.BinomialHeapImp.HeapNode α → Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.Heap α

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

ink

instance Std.BinomialHeapImp.instReprHeap : {α : Type u_1} → [inst : Repr α] → Repr (Std.BinomialHeapImp.Heap α)

Equations

• Std.BinomialHeapImp.instReprHeap = { reprPrec := Std.BinomialHeapImp.reprHeap✝ }

ink

def Std.BinomialHeapImp.Heap.realSize {α : Type u_1} : Std.BinomialHeapImp.Heap α → Nat

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

• Std.BinomialHeapImp.Heap.realSize Std.BinomialHeapImp.Heap.nil = 0
• Std.BinomialHeapImp.Heap.realSize (Std.BinomialHeapImp.Heap.cons a a_1 a_2 a_3) = Std.BinomialHeapImp.HeapNode.realSize a_2 + 1 + Std.BinomialHeapImp.Heap.realSize a_3

ink

def Std.BinomialHeapImp.Heap.size {α : Type u_1} : Std.BinomialHeapImp.Heap α → Nat

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

Equations

• Std.BinomialHeapImp.Heap.size x = match x with | Std.BinomialHeapImp.Heap.nil => 0 | Std.BinomialHeapImp.Heap.cons r val node s => 1 <<< r + Std.BinomialHeapImp.Heap.realSize s

ink

def Std.BinomialHeapImp.Heap.isEmpty {α : Type u_1} : Std.BinomialHeapImp.Heap α → Bool

O(1). Is the heap empty?

Equations

• Std.BinomialHeapImp.Heap.isEmpty x = match x with | Std.BinomialHeapImp.Heap.nil => true | x => false

ink

def Std.BinomialHeapImp.Heap.singleton {α : Type u_1} (a : α) : Std.BinomialHeapImp.Heap α

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

Equations

• Std.BinomialHeapImp.Heap.singleton a = Std.BinomialHeapImp.Heap.cons 0 a Std.BinomialHeapImp.HeapNode.nil Std.BinomialHeapImp.Heap.nil

ink

def Std.BinomialHeapImp.Heap.rankGT {α : Type u_1} : Std.BinomialHeapImp.Heap α → Nat → Prop

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

Equations

• Std.BinomialHeapImp.Heap.rankGT x x = match x, x with | Std.BinomialHeapImp.Heap.nil, x => True | Std.BinomialHeapImp.Heap.cons r val node next, n => n < r

ink

instance Std.BinomialHeapImp.instDecidableRankGT : {α : Type u_1} → {s : Std.BinomialHeapImp.Heap α} → {n : Nat} → Decidable (Std.BinomialHeapImp.Heap.rankGT s n)

Equations

• One or more equations did not get rendered due to their size.

ink

def Std.BinomialHeapImp.Heap.length {α : Type u_1} : Std.BinomialHeapImp.Heap α → Nat

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

Equations

• Std.BinomialHeapImp.Heap.length Std.BinomialHeapImp.Heap.nil = 0
• Std.BinomialHeapImp.Heap.length (Std.BinomialHeapImp.Heap.cons a a_1 a_2 a_3) = Std.BinomialHeapImp.Heap.length a_3 + 1

ink

@[specialize #[]]

def Std.BinomialHeapImp.combine {α : Type u_1} (le : α → α → Bool) (a₁ : α) (a₂ : α) (n₁ : Std.BinomialHeapImp.HeapNode α) (n₂ : Std.BinomialHeapImp.HeapNode α) : α × Std.BinomialHeapImp.HeapNode α

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

Equations

• Std.BinomialHeapImp.combine le a₁ a₂ n₁ n₂ = if le a₁ a₂ = true then (a₁, Std.BinomialHeapImp.HeapNode.node a₂ n₂ n₁) else (a₂, Std.BinomialHeapImp.HeapNode.node a₁ n₁ n₂)

ink

@[specialize #[]]

def Std.BinomialHeapImp.Heap.merge {α : Type u_1} (le : α → α → Bool) : Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.Heap α

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

Equations

• One or more equations did not get rendered due to their size.
• Std.BinomialHeapImp.Heap.merge le Std.BinomialHeapImp.Heap.nil x = x
• Std.BinomialHeapImp.Heap.merge le x Std.BinomialHeapImp.Heap.nil = x

ink

def Std.BinomialHeapImp.HeapNode.toHeap {α : Type u_1} (s : Std.BinomialHeapImp.HeapNode α) : Std.BinomialHeapImp.Heap α

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

Equations

• Std.BinomialHeapImp.HeapNode.toHeap s = Std.BinomialHeapImp.HeapNode.toHeap.go s (Std.BinomialHeapImp.HeapNode.rankTR s) Std.BinomialHeapImp.Heap.nil

ink

def Std.BinomialHeapImp.HeapNode.toHeap.go {α : Type u_1} : Std.BinomialHeapImp.HeapNode α → Nat → Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.Heap α

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

Equations

• Std.BinomialHeapImp.HeapNode.toHeap.go Std.BinomialHeapImp.HeapNode.nil x x = x
• Std.BinomialHeapImp.HeapNode.toHeap.go (Std.BinomialHeapImp.HeapNode.node a c s) x x = Std.BinomialHeapImp.HeapNode.toHeap.go s (x - 1) (Std.BinomialHeapImp.Heap.cons (x - 1) a c x)

ink

@[specialize #[]]

def Std.BinomialHeapImp.Heap.headD {α : Type u_1} (le : α → α → Bool) (a : α) : Std.BinomialHeapImp.Heap α → α

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

Equations

• Std.BinomialHeapImp.Heap.headD le a Std.BinomialHeapImp.Heap.nil = a
• Std.BinomialHeapImp.Heap.headD le a (Std.BinomialHeapImp.Heap.cons a_1 a_2 a_3 a_4) = Std.BinomialHeapImp.Heap.headD le (if le a a_2 = true then a else a_2) a_4

ink

@[inline]

def Std.BinomialHeapImp.Heap.head? {α : Type u_1} (le : α → α → Bool) : Std.BinomialHeapImp.Heap α → Option α

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

Equations

• Std.BinomialHeapImp.Heap.head? le x = match x with | Std.BinomialHeapImp.Heap.nil => none | Std.BinomialHeapImp.Heap.cons rank h node hs => some (Std.BinomialHeapImp.Heap.headD le h hs)

ink

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 : Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.Heap α

• The minimum element.

  val : α

• The children of the minimum element.

  node : Std.BinomialHeapImp.HeapNode α

• The forest after the minimum element.

  next : Std.BinomialHeapImp.Heap α

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

ink

@[specialize #[]]

def Std.BinomialHeapImp.Heap.findMin {α : Type u_1} (le : α → α → Bool) (k : Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.Heap α) : Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.FindMin α → Std.BinomialHeapImp.FindMin α

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

• One or more equations did not get rendered due to their size.
• Std.BinomialHeapImp.Heap.findMin le k Std.BinomialHeapImp.Heap.nil x = x

ink

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

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.

ink

@[inline]

def Std.BinomialHeapImp.Heap.tail? {α : Type u_1} (le : α → α → Bool) (h : Std.BinomialHeapImp.Heap α) : Option (Std.BinomialHeapImp.Heap α)

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

Equations

• Std.BinomialHeapImp.Heap.tail? le h = Option.map (fun x => x.snd) (Std.BinomialHeapImp.Heap.deleteMin le h)

ink

@[inline]

def Std.BinomialHeapImp.Heap.tail {α : Type u_1} (le : α → α → Bool) (h : Std.BinomialHeapImp.Heap α) : Std.BinomialHeapImp.Heap α

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

Equations

• Std.BinomialHeapImp.Heap.tail le h = Option.getD (Std.BinomialHeapImp.Heap.tail? le h) Std.BinomialHeapImp.Heap.nil

ink

theorem Std.BinomialHeapImp.Heap.realSize_merge {α : Type u_1} (le : α → α → Bool) (s₁ : Std.BinomialHeapImp.Heap α) (s₂ : Std.BinomialHeapImp.Heap α) : Std.BinomialHeapImp.Heap.realSize (Std.BinomialHeapImp.Heap.merge le s₁ s₂) = Std.BinomialHeapImp.Heap.realSize s₁ + Std.BinomialHeapImp.Heap.realSize s₂

ink

theorem Std.BinomialHeapImp.Heap.realSize_findMin {α : Type u_1} {k : Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.Heap α} {n : Nat} {le : α → α → Bool} {res : Std.BinomialHeapImp.FindMin α} {s : Std.BinomialHeapImp.Heap α} (m : Nat) (hk : ∀ (s : Std.BinomialHeapImp.Heap α), Std.BinomialHeapImp.Heap.realSize (k s) = m + Std.BinomialHeapImp.Heap.realSize s) (eq : n = m + Std.BinomialHeapImp.Heap.realSize s) (hres : Std.BinomialHeapImp.FindMin.HasSize res n) : Std.BinomialHeapImp.FindMin.HasSize (Std.BinomialHeapImp.Heap.findMin le k s res) n

ink

theorem Std.BinomialHeapImp.HeapNode.realSize_toHeap {α : Type u_1} (s : Std.BinomialHeapImp.HeapNode α) : Std.BinomialHeapImp.Heap.realSize (Std.BinomialHeapImp.HeapNode.toHeap s) = Std.BinomialHeapImp.HeapNode.realSize s

ink

theorem Std.BinomialHeapImp.HeapNode.realSize_toHeap.go {α : Type u_1} {n : Nat} {res : Std.BinomialHeapImp.Heap α} (s : Std.BinomialHeapImp.HeapNode α) : Std.BinomialHeapImp.Heap.realSize (Std.BinomialHeapImp.HeapNode.toHeap.go s n res) = Std.BinomialHeapImp.HeapNode.realSize s + Std.BinomialHeapImp.Heap.realSize res

ink

theorem Std.BinomialHeapImp.Heap.realSize_deleteMin {α : Type u_1} {le : α → α → Bool} {a : α} {s' : Std.BinomialHeapImp.Heap α} {s : Std.BinomialHeapImp.Heap α} (eq : Std.BinomialHeapImp.Heap.deleteMin le s = some (a, s')) : Std.BinomialHeapImp.Heap.realSize s = Std.BinomialHeapImp.Heap.realSize s' + 1

ink

theorem Std.BinomialHeapImp.Heap.realSize_tail? {α : Type u_1} {le : α → α → Bool} {s' : Std.BinomialHeapImp.Heap α} {s : Std.BinomialHeapImp.Heap α} : Std.BinomialHeapImp.Heap.tail? le s = some s' → Std.BinomialHeapImp.Heap.realSize s = Std.BinomialHeapImp.Heap.realSize s' + 1

ink

theorem Std.BinomialHeapImp.Heap.realSize_tail {α : Type u_1} (le : α → α → Bool) (s : Std.BinomialHeapImp.Heap α) : Std.BinomialHeapImp.Heap.realSize (Std.BinomialHeapImp.Heap.tail le s) = Std.BinomialHeapImp.Heap.realSize s - 1

ink

@[specialize #[]]

def Std.BinomialHeapImp.Heap.foldM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (le : α → α → Bool) (s : Std.BinomialHeapImp.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.

ink

@[inline]

def Std.BinomialHeapImp.Heap.fold {α : Type u_1} {β : Type u_2} (le : α → α → Bool) (s : Std.BinomialHeapImp.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

• Std.BinomialHeapImp.Heap.fold le s init f = Id.run (Std.BinomialHeapImp.Heap.foldM le s init f)

ink

@[inline]

def Std.BinomialHeapImp.Heap.toArray {α : Type u_1} (le : α → α → Bool) (s : Std.BinomialHeapImp.Heap α) : Array α

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

Equations

• Std.BinomialHeapImp.Heap.toArray le s = Std.BinomialHeapImp.Heap.fold le s #[] Array.push

ink

@[inline]

def Std.BinomialHeapImp.Heap.toList {α : Type u_1} (le : α → α → Bool) (s : Std.BinomialHeapImp.Heap α) : List α

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

Equations

• Std.BinomialHeapImp.Heap.toList le s = Array.toList (Std.BinomialHeapImp.Heap.toArray le s)

ink

@[specialize #[]]

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

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

Equations

• One or more equations did not get rendered due to their size.
• Std.BinomialHeapImp.HeapNode.foldTreeM nil join Std.BinomialHeapImp.HeapNode.nil = pure nil

ink

@[specialize #[]]

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

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

Equations

• One or more equations did not get rendered due to their size.
• Std.BinomialHeapImp.Heap.foldTreeM nil join Std.BinomialHeapImp.Heap.nil = pure nil

ink

@[inline]

def Std.BinomialHeapImp.Heap.foldTree {β : Type u_1} {α : Type u_2} (nil : β) (join : α → β → β → β) (s : Std.BinomialHeapImp.Heap α) : β

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

Equations

• Std.BinomialHeapImp.Heap.foldTree nil join s = Id.run (Std.BinomialHeapImp.Heap.foldTreeM nil join s)

ink

def Std.BinomialHeapImp.Heap.toListUnordered {α : Type u_1} (s : Std.BinomialHeapImp.Heap α) : List α

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

Equations

• Std.BinomialHeapImp.Heap.toListUnordered s = Std.BinomialHeapImp.Heap.foldTree id (fun a c s l => a :: c (s l)) s []

ink

def Std.BinomialHeapImp.Heap.toArrayUnordered {α : Type u_1} (s : Std.BinomialHeapImp.Heap α) : Array α

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

Equations

• Std.BinomialHeapImp.Heap.toArrayUnordered s = Std.BinomialHeapImp.Heap.foldTree id (fun a c s r => s (c (Array.push r a))) s #[]

ink

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

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

• One or more equations did not get rendered due to their size.
• Std.BinomialHeapImp.HeapNode.WellFormed le a Std.BinomialHeapImp.HeapNode.nil x = (x = 0)

ink

def Std.BinomialHeapImp.Heap.WellFormed {α : Type u_1} (le : α → α → Bool) (n : Nat) : Std.BinomialHeapImp.Heap α → Prop

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

• One or more equations did not get rendered due to their size.
• Std.BinomialHeapImp.Heap.WellFormed le n Std.BinomialHeapImp.Heap.nil = True

ink

theorem Std.BinomialHeapImp.Heap.WellFormed.nil : ∀ {α : Type u_1} {le : α → α → Bool} {n : Nat}, Std.BinomialHeapImp.Heap.WellFormed le n Std.BinomialHeapImp.Heap.nil

ink

theorem Std.BinomialHeapImp.Heap.WellFormed.singleton : ∀ {α : Type u_1} {a : α} {le : α → α → Bool}, Std.BinomialHeapImp.Heap.WellFormed le 0 (Std.BinomialHeapImp.Heap.singleton a)

ink

theorem Std.BinomialHeapImp.Heap.WellFormed.of_rankGT : ∀ {α : Type u_1} {s : Std.BinomialHeapImp.Heap α} {le : α → α → Bool} {n' n : Nat}, Std.BinomialHeapImp.Heap.rankGT s n → Std.BinomialHeapImp.Heap.WellFormed le n' s → Std.BinomialHeapImp.Heap.WellFormed le (n + 1) s

ink

theorem Std.BinomialHeapImp.Heap.WellFormed.of_le {n : Nat} {n' : Nat} : ∀ {α : Type u_1} {s : Std.BinomialHeapImp.Heap α} {le : α → α → Bool}, n ≤ n' → Std.BinomialHeapImp.Heap.WellFormed le n' s → Std.BinomialHeapImp.Heap.WellFormed le n s

ink

theorem Std.BinomialHeapImp.Heap.rankGT.le_trans : ∀ {α : Type u_1} {s : Std.BinomialHeapImp.Heap α} {n n' : Nat}, Std.BinomialHeapImp.Heap.rankGT s n → n' ≤ n → Std.BinomialHeapImp.Heap.rankGT s n'

ink

theorem Std.BinomialHeapImp.Heap.WellFormed.rankGT : ∀ {α : Type u_1} {lt : α → α → Bool} {n : Nat} {s : Std.BinomialHeapImp.Heap α}, Std.BinomialHeapImp.Heap.WellFormed lt (n + 1) s → Std.BinomialHeapImp.Heap.rankGT s n

ink

theorem Std.BinomialHeapImp.Heap.WellFormed.merge' : ∀ {α : Type u_1} {le : α → α → Bool} {s₁ s₂ : Std.BinomialHeapImp.Heap α} {n : Nat}, Std.BinomialHeapImp.Heap.WellFormed le n s₁ → Std.BinomialHeapImp.Heap.WellFormed le n s₂ → Std.BinomialHeapImp.Heap.WellFormed le n (Std.BinomialHeapImp.Heap.merge le s₁ s₂) ∧ ((Std.BinomialHeapImp.Heap.rankGT s₁ n ↔ Std.BinomialHeapImp.Heap.rankGT s₂ n) → Std.BinomialHeapImp.Heap.rankGT (Std.BinomialHeapImp.Heap.merge le s₁ s₂) n)

ink

theorem Std.BinomialHeapImp.Heap.WellFormed.merge : ∀ {α : Type u_1} {le : α → α → Bool} {s₁ s₂ : Std.BinomialHeapImp.Heap α} {n : Nat}, Std.BinomialHeapImp.Heap.WellFormed le n s₁ → Std.BinomialHeapImp.Heap.WellFormed le n s₂ → Std.BinomialHeapImp.Heap.WellFormed le n (Std.BinomialHeapImp.Heap.merge le s₁ s₂)

ink

theorem Std.BinomialHeapImp.Heap.findMin_val {α : Type u_1} {s : Std.BinomialHeapImp.Heap α} {le : α → α → Bool} {k : Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.Heap α} {res : Std.BinomialHeapImp.FindMin α} : (Std.BinomialHeapImp.Heap.findMin le k s res).val = Std.BinomialHeapImp.Heap.headD le res.val s

ink

theorem Std.BinomialHeapImp.Heap.deleteMin_fst {α : Type u_1} {s : Std.BinomialHeapImp.Heap α} {le : α → α → Bool} : Option.map (fun x => x.fst) (Std.BinomialHeapImp.Heap.deleteMin le s) = Std.BinomialHeapImp.Heap.head? le s

ink

def Std.BinomialHeapImp.HeapNode.rank {α : Type u_1} : Std.BinomialHeapImp.HeapNode α → Nat

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

• Std.BinomialHeapImp.HeapNode.rank Std.BinomialHeapImp.HeapNode.nil = 0
• Std.BinomialHeapImp.HeapNode.rank (Std.BinomialHeapImp.HeapNode.node a a_1 a_2) = Std.BinomialHeapImp.HeapNode.rank a_2 + 1

ink

@[simp]

theorem Std.BinomialHeapImp.HeapNode.rankTR_eq {α : Type u_1} (s : Std.BinomialHeapImp.HeapNode α) : Std.BinomialHeapImp.HeapNode.rankTR s = Std.BinomialHeapImp.HeapNode.rank s

ink

theorem Std.BinomialHeapImp.HeapNode.rankTR_eq.go {α : Type u_1} (s : Std.BinomialHeapImp.HeapNode α) (n : Nat) : Std.BinomialHeapImp.HeapNode.rankTR.go s n = Std.BinomialHeapImp.HeapNode.rank s + n

ink

@[simp]

theorem Std.BinomialHeapImp.HeapNode.WellFormed.rank_eq {α : Type u_1} {le : α → α → Bool} {a : α} {n : Nat} {s : Std.BinomialHeapImp.HeapNode α} : Std.BinomialHeapImp.HeapNode.WellFormed le a s n → Std.BinomialHeapImp.HeapNode.rank s = n

ink

@[simp]

theorem Std.BinomialHeapImp.HeapNode.WellFormed.realSize_eq {α : Type u_1} {le : α → α → Bool} {a : α} {n : Nat} {s : Std.BinomialHeapImp.HeapNode α} : Std.BinomialHeapImp.HeapNode.WellFormed le a s n → Std.BinomialHeapImp.HeapNode.realSize s + 1 = 2 ^ n

ink

@[simp]

theorem Std.BinomialHeapImp.Heap.WellFormed.size_eq {α : Type u_1} {le : α → α → Bool} {n : Nat} {s : Std.BinomialHeapImp.Heap α} : Std.BinomialHeapImp.Heap.WellFormed le n s → Std.BinomialHeapImp.Heap.size s = Std.BinomialHeapImp.Heap.realSize s

ink

theorem Std.BinomialHeapImp.HeapNode.WellFormed.toHeap {α : Type u_1} {le : α → α → Bool} {a : α} {n : Nat} {s : Std.BinomialHeapImp.HeapNode α} (h : Std.BinomialHeapImp.HeapNode.WellFormed le a s n) : Std.BinomialHeapImp.Heap.WellFormed le 0 (Std.BinomialHeapImp.HeapNode.toHeap s)

ink

theorem Std.BinomialHeapImp.HeapNode.WellFormed.toHeap.go {α : Type u_1} {le : α → α → Bool} {a : α} {res : Std.BinomialHeapImp.Heap α} {n : Nat} {s : Std.BinomialHeapImp.HeapNode α} : Std.BinomialHeapImp.HeapNode.WellFormed le a s n → Std.BinomialHeapImp.Heap.WellFormed le (Std.BinomialHeapImp.HeapNode.rank s) res → Std.BinomialHeapImp.Heap.WellFormed le 0 (Std.BinomialHeapImp.HeapNode.toHeap.go s (Std.BinomialHeapImp.HeapNode.rank s) res)

ink

structure Std.BinomialHeapImp.FindMin.WellFormed {α : Type u_1} (le : α → α → Bool) (res : Std.BinomialHeapImp.FindMin α) : Type

• 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 : Std.BinomialHeapImp.Heap α}, Std.BinomialHeapImp.Heap.WellFormed le rank s → Std.BinomialHeapImp.Heap.WellFormed le 0 (Std.BinomialHeapImp.FindMin.before res 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.

ink

theorem Std.BinomialHeapImp.Heap.WellFormed.findMin {α : Type u_1} {le : α → α → Bool} {n : Nat} {k : Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.Heap α} {res : Std.BinomialHeapImp.FindMin α} {s : Std.BinomialHeapImp.Heap α} (h : Std.BinomialHeapImp.Heap.WellFormed le n s) (hr : Std.BinomialHeapImp.FindMin.WellFormed le res) (hk : ∀ {s : Std.BinomialHeapImp.Heap α}, Std.BinomialHeapImp.Heap.WellFormed le n s → Std.BinomialHeapImp.Heap.WellFormed le 0 (k s)) : Nonempty (Std.BinomialHeapImp.FindMin.WellFormed le (Std.BinomialHeapImp.Heap.findMin le k s res))

ink

theorem Std.BinomialHeapImp.Heap.WellFormed.deleteMin {α : Type u_1} {le : α → α → Bool} {n : Nat} {a : α} {s' : Std.BinomialHeapImp.Heap α} {s : Std.BinomialHeapImp.Heap α} (h : Std.BinomialHeapImp.Heap.WellFormed le n s) (eq : Std.BinomialHeapImp.Heap.deleteMin le s = some (a, s')) : Std.BinomialHeapImp.Heap.WellFormed le 0 s'

ink

theorem Std.BinomialHeapImp.Heap.WellFormed.tail? {α : Type u_1} {s : Std.BinomialHeapImp.Heap α} {le : α → α → Bool} {n : Nat} {tl : Std.BinomialHeapImp.Heap α} (hwf : Std.BinomialHeapImp.Heap.WellFormed le n s) : Std.BinomialHeapImp.Heap.tail? le s = some tl → Std.BinomialHeapImp.Heap.WellFormed le 0 tl

ink

theorem Std.BinomialHeapImp.Heap.WellFormed.tail {α : Type u_1} {s : Std.BinomialHeapImp.Heap α} {le : α → α → Bool} {n : Nat} (hwf : Std.BinomialHeapImp.Heap.WellFormed le n s) : Std.BinomialHeapImp.Heap.WellFormed le 0 (Std.BinomialHeapImp.Heap.tail le s)

ink

def Std.BinomialHeap (α : Type u) (le : α → α → Bool) : Type u

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

• Std.BinomialHeap α le = { h // Std.BinomialHeapImp.Heap.WellFormed le 0 h }

ink

@[inline]

def Std.mkBinomialHeap (α : Type u) (le : α → α → Bool) : Std.BinomialHeap α le

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

Equations

• Std.mkBinomialHeap α le = { val := Std.BinomialHeapImp.Heap.nil, property := (_ : Std.BinomialHeapImp.Heap.WellFormed le 0 Std.BinomialHeapImp.Heap.nil) }

ink

@[inline]

def Std.BinomialHeap.empty {α : Type u} {le : α → α → Bool} : Std.BinomialHeap α le

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

Equations

• Std.BinomialHeap.empty = Std.mkBinomialHeap α le

ink

instance Std.BinomialHeap.instInhabitedBinomialHeap {α : Type u} {le : α → α → Bool} : Inhabited (Std.BinomialHeap α le)

Equations

• Std.BinomialHeap.instInhabitedBinomialHeap = { default := Std.BinomialHeap.empty }

ink

@[inline]

def Std.BinomialHeap.isEmpty {α : Type u} {le : α → α → Bool} (b : Std.BinomialHeap α le) : Bool

O(1). Is the heap empty?

Equations

• Std.BinomialHeap.isEmpty b = Std.BinomialHeapImp.Heap.isEmpty b.val

ink

@[inline]

def Std.BinomialHeap.size {α : Type u} {le : α → α → Bool} (b : Std.BinomialHeap α le) : Nat

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

Equations

• Std.BinomialHeap.size b = Std.BinomialHeapImp.Heap.size b.val

ink

@[inline]

def Std.BinomialHeap.singleton {α : Type u} {le : α → α → Bool} (a : α) : Std.BinomialHeap α le

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

Equations

• Std.BinomialHeap.singleton a = { val := Std.BinomialHeapImp.Heap.singleton a, property := (_ : Std.BinomialHeapImp.Heap.WellFormed le 0 (Std.BinomialHeapImp.Heap.singleton a)) }

ink

@[inline]

def Std.BinomialHeap.merge {α : Type u} {le : α → α → Bool} : Std.BinomialHeap α le → Std.BinomialHeap α le → Std.BinomialHeap α le

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[inline]

def Std.BinomialHeap.insert {α : Type u} {le : α → α → Bool} (a : α) (h : Std.BinomialHeap α le) : Std.BinomialHeap α le

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

Equations

• Std.BinomialHeap.insert a h = Std.BinomialHeap.merge (Std.BinomialHeap.singleton a) h

ink

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

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

Equations

• Std.BinomialHeap.ofList le as = List.foldl (flip Std.BinomialHeap.insert) Std.BinomialHeap.empty as

ink

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

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

Equations

• Std.BinomialHeap.ofArray le as = Array.foldl (flip Std.BinomialHeap.insert) Std.BinomialHeap.empty as 0 (Array.size as)

ink

@[inline]

def Std.BinomialHeap.deleteMin {α : Type u} {le : α → α → Bool} (b : Std.BinomialHeap α le) : Option (α × Std.BinomialHeap α le)

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.

ink

@[inline]

def Std.BinomialHeap.head? {α : Type u} {le : α → α → Bool} (b : Std.BinomialHeap α le) : Option α

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

Equations

• Std.BinomialHeap.head? b = Std.BinomialHeapImp.Heap.head? le b.val

ink

@[inline]

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

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

Equations

• Std.BinomialHeap.head! b = Option.get! (Std.BinomialHeap.head? b)

ink

@[inline]

def Std.BinomialHeap.headI {α : Type u} {le : α → α → Bool} [inst : Inhabited α] (b : Std.BinomialHeap α le) : α

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

Equations

• Std.BinomialHeap.headI b = Option.getD (Std.BinomialHeap.head? b) default

ink

@[inline]

def Std.BinomialHeap.tail? {α : Type u} {le : α → α → Bool} (b : Std.BinomialHeap α le) : Option (Std.BinomialHeap α le)

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.

ink

@[inline]

def Std.BinomialHeap.tail {α : Type u} {le : α → α → Bool} (b : Std.BinomialHeap α le) : Std.BinomialHeap α le

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

Equations

• Std.BinomialHeap.tail b = { val := Std.BinomialHeapImp.Heap.tail le b.val, property := (_ : Std.BinomialHeapImp.Heap.WellFormed le 0 (Std.BinomialHeapImp.Heap.tail le b.val)) }

ink

@[inline]

def Std.BinomialHeap.toList {α : Type u} {le : α → α → Bool} (b : Std.BinomialHeap α le) : List α

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

Equations

• Std.BinomialHeap.toList b = Std.BinomialHeapImp.Heap.toList le b.val

ink

@[inline]

def Std.BinomialHeap.toArray {α : Type u} {le : α → α → Bool} (b : Std.BinomialHeap α le) : Array α

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

Equations

• Std.BinomialHeap.toArray b = Std.BinomialHeapImp.Heap.toArray le b.val

ink

@[inline]

def Std.BinomialHeap.toListUnordered {α : Type u} {le : α → α → Bool} (b : Std.BinomialHeap α le) : List α

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

Equations

• Std.BinomialHeap.toListUnordered b = Std.BinomialHeapImp.Heap.toListUnordered b.val

ink

@[inline]

def Std.BinomialHeap.toArrayUnordered {α : Type u} {le : α → α → Bool} (b : Std.BinomialHeap α le) : Array α

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

Equations

• Std.BinomialHeap.toArrayUnordered b = Std.BinomialHeapImp.Heap.toArrayUnordered b.val