inductive Batteries.BinomialHeap.Imp.HeapNode (α : Type u) : 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.

• nil: {α : Type u} → Batteries.BinomialHeap.Imp.HeapNode α

  An empty forest, which has depth 0.

• node: {α : Type u} → α → Batteries.BinomialHeap.Imp.HeapNode α → Batteries.BinomialHeap.Imp.HeapNode α → Batteries.BinomialHeap.Imp.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.

instance Batteries.BinomialHeap.Imp.instReprHeapNode : {α : Type u_1} → [inst : Repr α] → Repr (Batteries.BinomialHeap.Imp.HeapNode α)

Equations

• Batteries.BinomialHeap.Imp.instReprHeapNode = { reprPrec := Batteries.BinomialHeap.Imp.reprHeapNode✝ }

def Batteries.BinomialHeap.Imp.HeapNode.realSize {α : Type u_1} : Batteries.BinomialHeap.Imp.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

• Batteries.BinomialHeap.Imp.HeapNode.nil.realSize = 0
• (Batteries.BinomialHeap.Imp.HeapNode.node a a_1 a_2).realSize = a_1.realSize + 1 + a_2.realSize

def Batteries.BinomialHeap.Imp.HeapNode.singleton {α : Type u_1} (a : α) : Batteries.BinomialHeap.Imp.HeapNode α

A node containing a single element a.

Equations

• Batteries.BinomialHeap.Imp.HeapNode.singleton a = Batteries.BinomialHeap.Imp.HeapNode.node a Batteries.BinomialHeap.Imp.HeapNode.nil Batteries.BinomialHeap.Imp.HeapNode.nil

def Batteries.BinomialHeap.Imp.HeapNode.rank {α : Type u_1} : Batteries.BinomialHeap.Imp.HeapNode α → Nat

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

Equations

• Batteries.BinomialHeap.Imp.HeapNode.nil.rank = 0
• (Batteries.BinomialHeap.Imp.HeapNode.node a a_1 a_2).rank = a_2.rank + 1

inductive Batteries.BinomialHeap.Imp.Heap (α : Type u) : Type u

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

• nil: {α : Type u} → Batteries.BinomialHeap.Imp.Heap α

  An empty heap.

• cons: {α : Type u} → Nat → α → Batteries.BinomialHeap.Imp.HeapNode α → Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.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.

instance Batteries.BinomialHeap.Imp.instReprHeap : {α : Type u_1} → [inst : Repr α] → Repr (Batteries.BinomialHeap.Imp.Heap α)

Equations

• Batteries.BinomialHeap.Imp.instReprHeap = { reprPrec := Batteries.BinomialHeap.Imp.reprHeap✝ }

def Batteries.BinomialHeap.Imp.Heap.realSize {α : Type u_1} : Batteries.BinomialHeap.Imp.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

• Batteries.BinomialHeap.Imp.Heap.nil.realSize = 0
• (Batteries.BinomialHeap.Imp.Heap.cons a a_1 a_2 a_3).realSize = a_2.realSize + 1 + a_3.realSize

def Batteries.BinomialHeap.Imp.Heap.size {α : Type u_1} : Batteries.BinomialHeap.Imp.Heap α → Nat

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

Equations

• Batteries.BinomialHeap.Imp.Heap.nil.size = 0
• (Batteries.BinomialHeap.Imp.Heap.cons a a_1 a_2 a_3).size = 1 <<< a + a_3.size

@[inline]

def Batteries.BinomialHeap.Imp.Heap.isEmpty {α : Type u_1} : Batteries.BinomialHeap.Imp.Heap α → Bool

O(1). Is the heap empty?

Equations

• Batteries.BinomialHeap.Imp.Heap.nil.isEmpty = true
• x.isEmpty = false

@[inline]

def Batteries.BinomialHeap.Imp.Heap.singleton {α : Type u_1} (a : α) : Batteries.BinomialHeap.Imp.Heap α

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

Equations

• Batteries.BinomialHeap.Imp.Heap.singleton a = Batteries.BinomialHeap.Imp.Heap.cons 0 a Batteries.BinomialHeap.Imp.HeapNode.nil Batteries.BinomialHeap.Imp.Heap.nil

def Batteries.BinomialHeap.Imp.Heap.rankGT {α : Type u_1} : Batteries.BinomialHeap.Imp.Heap α → Nat → Prop

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

Equations

• Batteries.BinomialHeap.Imp.Heap.nil.rankGT x = True
• (Batteries.BinomialHeap.Imp.Heap.cons r val node next).rankGT x = (x < r)

instance Batteries.BinomialHeap.Imp.instDecidableRankGT : {α : Type u_1} → {s : Batteries.BinomialHeap.Imp.Heap α} → {n : Nat} → Decidable (s.rankGT n)

Equations

• Batteries.BinomialHeap.Imp.instDecidableRankGT = inferInstanceAs (Decidable True)
• Batteries.BinomialHeap.Imp.instDecidableRankGT = inferInstanceAs (Decidable (n < a))

def Batteries.BinomialHeap.Imp.Heap.length {α : Type u_1} : Batteries.BinomialHeap.Imp.Heap α → Nat

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

Equations

• Batteries.BinomialHeap.Imp.Heap.nil.length = 0
• (Batteries.BinomialHeap.Imp.Heap.cons a a_1 a_2 a_3).length = a_3.length + 1

@[inline]

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

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

Equations

• Batteries.BinomialHeap.Imp.combine le a₁ a₂ n₁ n₂ = if le a₁ a₂ = true then (a₁, Batteries.BinomialHeap.Imp.HeapNode.node a₂ n₂ n₁) else (a₂, Batteries.BinomialHeap.Imp.HeapNode.node a₁ n₁ n₂)

@[irreducible, specialize #[]]

def Batteries.BinomialHeap.Imp.Heap.merge {α : Type u_1} (le : α → α → Bool) : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.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.
• Batteries.BinomialHeap.Imp.Heap.merge le Batteries.BinomialHeap.Imp.Heap.nil x = x
• Batteries.BinomialHeap.Imp.Heap.merge le x Batteries.BinomialHeap.Imp.Heap.nil = x

def Batteries.BinomialHeap.Imp.HeapNode.toHeap {α : Type u_1} (s : Batteries.BinomialHeap.Imp.HeapNode α) : Batteries.BinomialHeap.Imp.Heap α

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

Equations

• s.toHeap = Batteries.BinomialHeap.Imp.HeapNode.toHeap.go s s.rank Batteries.BinomialHeap.Imp.Heap.nil

def Batteries.BinomialHeap.Imp.HeapNode.toHeap.go {α : Type u_1} : Batteries.BinomialHeap.Imp.HeapNode α → Nat → Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α

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

Equations

• One or more equations did not get rendered due to their size.
• Batteries.BinomialHeap.Imp.HeapNode.toHeap.go Batteries.BinomialHeap.Imp.HeapNode.nil x✝ x = x

@[specialize #[]]

def Batteries.BinomialHeap.Imp.Heap.headD {α : Type u_1} (le : α → α → Bool) (a : α) : Batteries.BinomialHeap.Imp.Heap α → α

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

Equations

• Batteries.BinomialHeap.Imp.Heap.headD le a Batteries.BinomialHeap.Imp.Heap.nil = a
• Batteries.BinomialHeap.Imp.Heap.headD le a (Batteries.BinomialHeap.Imp.Heap.cons a_1 a_2 a_3 a_4) = Batteries.BinomialHeap.Imp.Heap.headD le (if le a a_2 = true then a else a_2) a_4

@[inline]

def Batteries.BinomialHeap.Imp.Heap.head? {α : Type u_1} (le : α → α → Bool) : Batteries.BinomialHeap.Imp.Heap α → Option α

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

Equations

• Batteries.BinomialHeap.Imp.Heap.head? le Batteries.BinomialHeap.Imp.Heap.nil = none
• Batteries.BinomialHeap.Imp.Heap.head? le (Batteries.BinomialHeap.Imp.Heap.cons a a_1 a_2 a_3) = some (Batteries.BinomialHeap.Imp.Heap.headD le a_1 a_3)

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.

• before : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α

  The list of elements prior to the minimum element, encoded as a "difference list".

• val : α

  The minimum element.

• node : Batteries.BinomialHeap.Imp.HeapNode α

  The children of the minimum element.

• next : Batteries.BinomialHeap.Imp.Heap α

  The forest after the minimum element.

@[specialize #[]]

def Batteries.BinomialHeap.Imp.Heap.findMin {α : Type u_1} (le : α → α → Bool) (k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α) : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.FindMin α → Batteries.BinomialHeap.Imp.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.
• Batteries.BinomialHeap.Imp.Heap.findMin le k Batteries.BinomialHeap.Imp.Heap.nil x = x

def Batteries.BinomialHeap.Imp.Heap.deleteMin {α : Type u_1} (le : α → α → Bool) : Batteries.BinomialHeap.Imp.Heap α → Option (α × Batteries.BinomialHeap.Imp.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.
• Batteries.BinomialHeap.Imp.Heap.deleteMin le Batteries.BinomialHeap.Imp.Heap.nil = none

@[inline]

def Batteries.BinomialHeap.Imp.Heap.tail? {α : Type u_1} (le : α → α → Bool) (h : Batteries.BinomialHeap.Imp.Heap α) : Option (Batteries.BinomialHeap.Imp.Heap α)

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

Equations

• Batteries.BinomialHeap.Imp.Heap.tail? le h = Option.map (fun (x : α × Batteries.BinomialHeap.Imp.Heap α) => x.snd) (Batteries.BinomialHeap.Imp.Heap.deleteMin le h)

@[inline]

def Batteries.BinomialHeap.Imp.Heap.tail {α : Type u_1} (le : α → α → Bool) (h : Batteries.BinomialHeap.Imp.Heap α) : Batteries.BinomialHeap.Imp.Heap α

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

Equations

• Batteries.BinomialHeap.Imp.Heap.tail le h = (Batteries.BinomialHeap.Imp.Heap.tail? le h).getD Batteries.BinomialHeap.Imp.Heap.nil

@[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.HeapNode.realSize_toHeap {α : Type u_1} (s : Batteries.BinomialHeap.Imp.HeapNode α) : s.toHeap.realSize = s.realSize

theorem Batteries.BinomialHeap.Imp.HeapNode.realSize_toHeap.go {α : Type u_1} {n : Nat} {res : Batteries.BinomialHeap.Imp.Heap α} (s : Batteries.BinomialHeap.Imp.HeapNode α) : (Batteries.BinomialHeap.Imp.HeapNode.toHeap.go s n res).realSize = s.realSize + res.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

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

theorem Batteries.BinomialHeap.Imp.Heap.realSize_tail {α : Type u_1} (le : α → α → Bool) (s : Batteries.BinomialHeap.Imp.Heap α) : (Batteries.BinomialHeap.Imp.Heap.tail le 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

• Batteries.BinomialHeap.Imp.Heap.fold le s init f = (Batteries.BinomialHeap.Imp.Heap.foldM le s init f).run

@[inline]

def Batteries.BinomialHeap.Imp.Heap.toArray {α : Type u_1} (le : α → α → Bool) (s : Batteries.BinomialHeap.Imp.Heap α) : Array α

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

Equations

• Batteries.BinomialHeap.Imp.Heap.toArray le s = Batteries.BinomialHeap.Imp.Heap.fold le s #[] Array.push

@[inline]

def Batteries.BinomialHeap.Imp.Heap.toList {α : Type u_1} (le : α → α → Bool) (s : Batteries.BinomialHeap.Imp.Heap α) : List α

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

Equations

• Batteries.BinomialHeap.Imp.Heap.toList le s = (Batteries.BinomialHeap.Imp.Heap.toArray le s).toList

@[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 β) : Batteries.BinomialHeap.Imp.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.
• Batteries.BinomialHeap.Imp.HeapNode.foldTreeM nil join Batteries.BinomialHeap.Imp.HeapNode.nil = pure nil

@[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 β) : Batteries.BinomialHeap.Imp.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.
• Batteries.BinomialHeap.Imp.Heap.foldTreeM nil join Batteries.BinomialHeap.Imp.Heap.nil = pure nil

@[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

• Batteries.BinomialHeap.Imp.Heap.foldTree nil join s = (Batteries.BinomialHeap.Imp.Heap.foldTreeM nil join s).run

def Batteries.BinomialHeap.Imp.Heap.toListUnordered {α : Type u_1} (s : Batteries.BinomialHeap.Imp.Heap α) : List α

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

Equations

• s.toListUnordered = Batteries.BinomialHeap.Imp.Heap.foldTree id (fun (a : α) (c s : List α → List α) (l : List α) => a :: c (s l)) s []

def Batteries.BinomialHeap.Imp.Heap.toArrayUnordered {α : Type u_1} (s : Batteries.BinomialHeap.Imp.Heap α) : Array α

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

Equations

• s.toArrayUnordered = Batteries.BinomialHeap.Imp.Heap.foldTree id (fun (a : α) (c s : Array α → Array α) (r : Array α) => s (c (r.push a))) s #[]

def Batteries.BinomialHeap.Imp.HeapNode.WF {α : Type u_1} (le : α → α → Bool) (a : α) : Batteries.BinomialHeap.Imp.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.
• Batteries.BinomialHeap.Imp.HeapNode.WF le a Batteries.BinomialHeap.Imp.HeapNode.nil x = (x = 0)

def Batteries.BinomialHeap.Imp.Heap.WF {α : Type u_1} (le : α → α → Bool) (n : Nat) : Batteries.BinomialHeap.Imp.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.
• Batteries.BinomialHeap.Imp.Heap.WF le n Batteries.BinomialHeap.Imp.Heap.nil = True

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.singleton : ∀ {α : Type u_1} {a : α} {le : α → α → Bool}, Batteries.BinomialHeap.Imp.Heap.WF le 0 (Batteries.BinomialHeap.Imp.Heap.singleton a)

theorem Batteries.BinomialHeap.Imp.Heap.WF.of_rankGT : ∀ {α : Type u_1} {le : α → α → Bool} {n' : Nat} {s : Batteries.BinomialHeap.Imp.Heap α} {n : Nat}, s.rankGT n → Batteries.BinomialHeap.Imp.Heap.WF le n' s → Batteries.BinomialHeap.Imp.Heap.WF le (n + 1) s

theorem Batteries.BinomialHeap.Imp.Heap.WF.of_le {n : Nat} {n' : Nat} : ∀ {α : Type u_1} {le : α → α → Bool} {s : Batteries.BinomialHeap.Imp.Heap α}, n ≤ n' → Batteries.BinomialHeap.Imp.Heap.WF le n' s → Batteries.BinomialHeap.Imp.Heap.WF le n s

theorem Batteries.BinomialHeap.Imp.Heap.rankGT.of_le : ∀ {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {n n' : Nat}, s.rankGT n → n' ≤ n → s.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) s → s.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.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₂)

theorem Batteries.BinomialHeap.Imp.HeapNode.WF.rank_eq {α : Type u_1} {le : α → α → Bool} {a : α} {n : Nat} {s : Batteries.BinomialHeap.Imp.HeapNode α} : Batteries.BinomialHeap.Imp.HeapNode.WF le a s n → s.rank = n

theorem Batteries.BinomialHeap.Imp.HeapNode.WF.toHeap {α : Type u_1} {le : α → α → Bool} {a : α} {n : Nat} {s : Batteries.BinomialHeap.Imp.HeapNode α} (h : Batteries.BinomialHeap.Imp.HeapNode.WF le a s n) : Batteries.BinomialHeap.Imp.Heap.WF le 0 s.toHeap

theorem Batteries.BinomialHeap.Imp.HeapNode.WF.toHeap.go {α : Type u_1} {le : α → α → Bool} {a : α} {res : Batteries.BinomialHeap.Imp.Heap α} {n : Nat} {s : Batteries.BinomialHeap.Imp.HeapNode α} : Batteries.BinomialHeap.Imp.HeapNode.WF le a s n → Batteries.BinomialHeap.Imp.Heap.WF le s.rank res → Batteries.BinomialHeap.Imp.Heap.WF le 0 (Batteries.BinomialHeap.Imp.HeapNode.toHeap.go s s.rank res)

structure Batteries.BinomialHeap.Imp.FindMin.WF {α : Type u_1} (le : α → α → Bool) (res : Batteries.BinomialHeap.Imp.FindMin α) : Type

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.

• rank : Nat

  The rank of the minimum element

• before : ∀ {s : Batteries.BinomialHeap.Imp.Heap α}, Batteries.BinomialHeap.Imp.Heap.WF le self.rank s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s)

  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 : Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node self.rank

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

• next : Batteries.BinomialHeap.Imp.Heap.WF le (self.rank + 1) res.next

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

theorem Batteries.BinomialHeap.Imp.FindMin.WF.before {α : Type u_1} {le : α → α → Bool} {res : Batteries.BinomialHeap.Imp.FindMin α} (self : Batteries.BinomialHeap.Imp.FindMin.WF le res) {s : Batteries.BinomialHeap.Imp.Heap α} : Batteries.BinomialHeap.Imp.Heap.WF le self.rank s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s)

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

theorem Batteries.BinomialHeap.Imp.FindMin.WF.node {α : Type u_1} {le : α → α → Bool} {res : Batteries.BinomialHeap.Imp.FindMin α} (self : Batteries.BinomialHeap.Imp.FindMin.WF le res) : Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node self.rank

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

theorem Batteries.BinomialHeap.Imp.FindMin.WF.next {α : Type u_1} {le : α → α → Bool} {res : Batteries.BinomialHeap.Imp.FindMin α} (self : Batteries.BinomialHeap.Imp.FindMin.WF le res) : Batteries.BinomialHeap.Imp.Heap.WF le (self.rank + 1) res.next

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

def Batteries.BinomialHeap.Imp.Heap.WF.findMin {α : Type u_1} {le : α → α → Bool} {n : Nat} {k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α} {res : Batteries.BinomialHeap.Imp.FindMin α} {s : Batteries.BinomialHeap.Imp.Heap α} (h : Batteries.BinomialHeap.Imp.Heap.WF le n s) (hr : Batteries.BinomialHeap.Imp.FindMin.WF le res) (hk : ∀ {s : Batteries.BinomialHeap.Imp.Heap α}, Batteries.BinomialHeap.Imp.Heap.WF le n s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (k s)) : Batteries.BinomialHeap.Imp.FindMin.WF le (Batteries.BinomialHeap.Imp.Heap.findMin le k s res)

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

theorem Batteries.BinomialHeap.Imp.Heap.WF.deleteMin {α : Type u_1} {le : α → α → Bool} {n : Nat} {a : α} {s' : Batteries.BinomialHeap.Imp.Heap α} {s : Batteries.BinomialHeap.Imp.Heap α} (h : Batteries.BinomialHeap.Imp.Heap.WF le n s) (eq : Batteries.BinomialHeap.Imp.Heap.deleteMin le s = some (a, s')) : Batteries.BinomialHeap.Imp.Heap.WF le 0 s'

theorem Batteries.BinomialHeap.Imp.Heap.WF.tail? {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {le : α → α → Bool} {n : Nat} {tl : Batteries.BinomialHeap.Imp.Heap α} (hwf : Batteries.BinomialHeap.Imp.Heap.WF le n s) : Batteries.BinomialHeap.Imp.Heap.tail? le s = some tl → Batteries.BinomialHeap.Imp.Heap.WF le 0 tl

theorem Batteries.BinomialHeap.Imp.Heap.WF.tail {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {le : α → α → Bool} {n : Nat} (hwf : Batteries.BinomialHeap.Imp.Heap.WF le n s) : Batteries.BinomialHeap.Imp.Heap.WF le 0 (Batteries.BinomialHeap.Imp.Heap.tail le s)

def Batteries.BinomialHeap (α : Type u) (le : α → α → Bool) : Type (max 0 u)

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

• insert : α → BinomialHeap α → BinomialHeap α: add an element to the heap
• deleteMin : BinomialHeap α → Option (α × BinomialHeap α): remove the minimum element from the heap
• merge : 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

• Batteries.BinomialHeap α le = { h : Batteries.BinomialHeap.Imp.Heap α // Batteries.BinomialHeap.Imp.Heap.WF le 0 h }

@[inline]

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

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

Equations

• Batteries.mkBinomialHeap α le = ⟨Batteries.BinomialHeap.Imp.Heap.nil, ⋯⟩

@[inline]

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

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

Equations

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

instance Batteries.BinomialHeap.instEmptyCollection {α : Type u} {le : α → α → Bool} : EmptyCollection (Batteries.BinomialHeap α le)

Equations

• Batteries.BinomialHeap.instEmptyCollection = { emptyCollection := Batteries.BinomialHeap.empty }

instance Batteries.BinomialHeap.instInhabited {α : Type u} {le : α → α → Bool} : Inhabited (Batteries.BinomialHeap α le)

Equations

• Batteries.BinomialHeap.instInhabited = { default := Batteries.BinomialHeap.empty }

@[inline]

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

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) : Nat

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 : α) : Batteries.BinomialHeap α le

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

Equations

• Batteries.BinomialHeap.singleton a = ⟨Batteries.BinomialHeap.Imp.Heap.singleton a, ⋯⟩

@[inline]

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

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

Equations

• Batteries.BinomialHeap.merge ⟨b₁, h₁⟩ ⟨b₂, h₂⟩ = ⟨Batteries.BinomialHeap.Imp.Heap.merge le b₁ b₂, ⋯⟩

@[inline]

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• Batteries.BinomialHeap.ofArray le as = Array.foldl (flip Batteries.BinomialHeap.insert) Batteries.BinomialHeap.empty as

@[inline]

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

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

Equations

• b.deleteMin = match eq : Batteries.BinomialHeap.Imp.Heap.deleteMin le b.val with | none => none | some (a, tl) => some (a, ⟨tl, ⋯⟩)

instance Batteries.BinomialHeap.instStream {α : Type u} {le : α → α → Bool} : Stream (Batteries.BinomialHeap α le) α

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

• b.forIn x f = ForInStep.run <$> Batteries.BinomialHeap.Imp.Heap.foldM le b.val (ForInStep.yield x) fun (x : ForInStep β) (a : α) => x.bind (f a)

instance Batteries.BinomialHeap.instForIn {α : Type u} {le : α → α → Bool} {m : Type u_1 → Type u_2} : ForIn m (Batteries.BinomialHeap α le) α

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) : Option α

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

Equations

• b.head? = Batteries.BinomialHeap.Imp.Heap.head? le b.val

@[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) : Option (Batteries.BinomialHeap α le)

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

Equations

• b.tail? = match eq : Batteries.BinomialHeap.Imp.Heap.tail? le b.val with | none => none | some tl => some ⟨tl, ⋯⟩

@[inline]

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

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

Equations

• b.tail = ⟨Batteries.BinomialHeap.Imp.Heap.tail le b.val, ⋯⟩

@[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

• b.foldM init f = Batteries.BinomialHeap.Imp.Heap.foldM le b.val init f

@[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

• b.fold init f = Batteries.BinomialHeap.Imp.Heap.fold le b.val init f

@[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

• b.toList = Batteries.BinomialHeap.Imp.Heap.toList le b.val

@[inline]

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

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

Equations

• b.toArray = Batteries.BinomialHeap.Imp.Heap.toArray le b.val

@[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) : Array α

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

Equations

• b.toArrayUnordered = b.val.toArrayUnordered