structure Batteries.BinaryHeap (α : Type w) [Ord α] : Type w

A max-heap data structure.

• arr : Array α

  O(1). Get data array for a BinaryHeap.

@[inline]

def Batteries.BinaryHeap.maxChild {α : Type u_1} {sz : Nat} [Ord α] (a : Vector α sz) (i : Fin sz) : Option (Fin sz)

Given a node, return the index of its larger child, if it exists

Equations

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

theorem Batteries.BinaryHeap.maxChild_gt {α : Type u_1} {sz : Nat} [Ord α] {a : Vector α sz} {i j : Fin sz} (h : maxChild a i = some j) : i < j

maxChild returns an index greater than i.

@[irreducible, specialize #[]]

def Batteries.BinaryHeap.heapifyDown {α : Type u_1} {sz : Nat} [Ord α] (a : Vector α sz) (i : Fin sz) : Vector α sz

Core operation for binary heaps, expressed directly on arrays. Given an array which is a max-heap, push item i down to restore the max-heap property.

Equations

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

@[inline]

def Batteries.BinaryHeap.mkHeap {α : Type u_1} {sz : Nat} [Ord α] (a : Vector α sz) : Vector α sz

Core operation for binary heaps, expressed directly on arrays. Construct a heap from an unsorted array, by heapifying all the elements.

Equations

• Batteries.BinaryHeap.mkHeap a = Batteries.BinaryHeap.mkHeap.loop✝ (sz / 2) a ⋯

@[irreducible, specialize #[]]

def Batteries.BinaryHeap.heapifyUp {α : Type u_1} {sz : Nat} [Ord α] (a : Vector α sz) (i : Fin sz) : Vector α sz

Core operation for binary heaps, expressed directly on arrays. Given an array which is a max-heap, push item i up to restore the max-heap property.

Equations

• One or more equations did not get rendered due to their size.
• Batteries.BinaryHeap.heapifyUp a ⟨0, isLt⟩ = a

@[inline]

def Batteries.BinaryHeap.empty {α : Type u_1} [Ord α] : BinaryHeap α

O(1). Build a new empty heap.

Equations

• Batteries.BinaryHeap.empty = { arr := #[] }

@[instance_reducible]

instance Batteries.BinaryHeap.instInhabited {α : Type u_1} [Ord α] : Inhabited (BinaryHeap α)

Equations

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

@[instance_reducible]

instance Batteries.BinaryHeap.instEmptyCollection {α : Type u_1} [Ord α] : EmptyCollection (BinaryHeap α)

Equations

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

@[instance_reducible]

instance Batteries.BinaryHeap.instMembership {α : Type u_1} [Ord α] : Membership α (BinaryHeap α)

Equations

• Batteries.BinaryHeap.instMembership = { mem := fun (h : Batteries.BinaryHeap α) (x : α) => x ∈ h.arr }

theorem Batteries.BinaryHeap.mem_def {α : Type u_1} [Ord α] {x : α} {h : BinaryHeap α} : x ∈ h ↔ x ∈ h.arr

@[inline]

def Batteries.BinaryHeap.singleton {α : Type u_1} [Ord α] (x : α) : BinaryHeap α

O(1). Build a one-element heap.

Equations

• Batteries.BinaryHeap.singleton x = { arr := #[x] }

@[inline]

def Batteries.BinaryHeap.size {α : Type u_1} [Ord α] (heap : BinaryHeap α) : Nat

O(1). Get the number of elements in a BinaryHeap.

Equations

• heap.size = heap.arr.size

@[inline]

def Batteries.BinaryHeap.vector {α : Type u_1} [Ord α] (heap : BinaryHeap α) : Vector α heap.size

O(1). Get data vector of a BinaryHeap.

Equations

• heap.vector = Vector.mk heap.arr ⋯

@[simp]

theorem Batteries.BinaryHeap.toArray_vector {α : Type u_1} [Ord α] (heap : BinaryHeap α) : heap.vector.toArray = heap.arr

@[simp]

theorem Batteries.BinaryHeap.mem_vector {α : Type u_1} {x : α} [Ord α] {heap : BinaryHeap α} : x ∈ heap.vector ↔ x ∈ heap.arr

@[inline]

def Batteries.BinaryHeap.get {α : Type u_1} [Ord α] (heap : BinaryHeap α) (i : Fin heap.size) : α

O(1). Get an element in the heap by index.

Equations

• heap.get i = heap.arr[i]

@[inline]

def Batteries.BinaryHeap.insert {α : Type u_1} [Ord α] (heap : BinaryHeap α) (x : α) : BinaryHeap α

O(log n). Insert an element into a BinaryHeap, preserving the max-heap property.

Equations

• heap.insert x = { arr := (Batteries.BinaryHeap.heapifyUp (heap.vector.push x) ⟨heap.size, ⋯⟩).toArray }

@[simp]

theorem Batteries.BinaryHeap.size_insert {α : Type u_1} [Ord α] (heap : BinaryHeap α) (x : α) : (heap.insert x).size = heap.size + 1

@[inline]

def Batteries.BinaryHeap.max {α : Type u_1} [Ord α] (heap : BinaryHeap α) : Option α

O(1). Get the maximum element in a BinaryHeap.

Equations

• heap.max = heap.arr[0]?

@[inline]

def Batteries.BinaryHeap.popMax {α : Type u_1} [Ord α] (heap : BinaryHeap α) : BinaryHeap α

O(log n). Remove the maximum element from a BinaryHeap. Call max first to actually retrieve the maximum element.

Equations

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

@[simp]

theorem Batteries.BinaryHeap.size_popMax {α : Type u_1} [Ord α] (heap : BinaryHeap α) : heap.popMax.size = heap.size - 1

@[inline]

def Batteries.BinaryHeap.extractMax {α : Type u_1} [Ord α] (heap : BinaryHeap α) : Option α × BinaryHeap α

O(log n). Return and remove the maximum element from a BinaryHeap.

Equations

• heap.extractMax = (heap.max, heap.popMax)

@[simp]

theorem Batteries.BinaryHeap.max_eq_none_iff {α : Type u_1} [Ord α] {heap : BinaryHeap α} : heap.max = none ↔ heap.size = 0

theorem Batteries.BinaryHeap.size_pos_of_max {α : Type u_1} {x : α} [Ord α] {heap : BinaryHeap α} (h : heap.max = some x) : 0 < heap.size

@[inline]

def Batteries.BinaryHeap.insertExtractMax {α : Type u_1} [Ord α] (heap : BinaryHeap α) (x : α) : α × BinaryHeap α

O(log n). Equivalent to extractMax (heap.insert x), except that extraction cannot fail.

Equations

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

@[inline]

def Batteries.BinaryHeap.replaceMax {α : Type u_1} [Ord α] (heap : BinaryHeap α) (x : α) : Option α × BinaryHeap α

O(log n). Equivalent to (heap.max, heap.popMax.insert x).

Equations

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

@[inline]

def Batteries.BinaryHeap.decreaseKey {α : Type u_1} [Ord α] (heap : BinaryHeap α) (i : Fin heap.size) (x : α) : BinaryHeap α

O(log n). Replace the value at index i by x. Assumes that x ≤ heap.get i.

Equations

• heap.decreaseKey i x = { arr := (Batteries.BinaryHeap.heapifyDown (heap.vector.set (↑i) x ⋯) i).toArray }

@[inline]

def Batteries.BinaryHeap.increaseKey {α : Type u_1} [Ord α] (heap : BinaryHeap α) (i : Fin heap.size) (x : α) : BinaryHeap α

O(log n). Replace the value at index i by x. Assumes that heap.get i ≤ x.

Equations

• heap.increaseKey i x = { arr := (Batteries.BinaryHeap.heapifyUp (heap.vector.set (↑i) x ⋯) i).toArray }

@[inline]

def Batteries.BinaryHeap.toSortedArray {α : Type u_1} [Ord α] (heap : BinaryHeap α) : Array α

O(n log n). Return the contents of heap as an array sorted in descending order.

Equations

• heap.toSortedArray = Batteries.BinaryHeap.toSortedArray.loop✝ heap (Array.emptyWithCapacity heap.size)

@[inline]

def Vector.toBinaryHeap {α : Type u_1} {n : Nat} [Ord α] (v : Vector α n) : Batteries.BinaryHeap α

O(n). Convert an unsorted vector to a BinaryHeap.

Equations

• v.toBinaryHeap = { arr := (Batteries.BinaryHeap.mkHeap v).toArray }

@[inline]

def Array.toBinaryHeap {α : Type u_1} [Ord α] (a : Array α) : Batteries.BinaryHeap α

O(n). Convert an unsorted array to a BinaryHeap.

Equations

• a.toBinaryHeap = { arr := (Batteries.BinaryHeap.mkHeap (Vector.mk a ⋯)).toArray }

@[inline]

def Array.heapSort {α : Type u_1} [instOrd : Ord α] (a : Array α) : Array α

O(n log n). Sort an array using a BinaryHeap.

Equations

• a.heapSort = a.toBinaryHeap.toSortedArray