structure Batteries.BinaryHeap (α : Type u_1) (lt : α → α → Bool) : Type u_1

A max-heap data structure.

• arr : Array α

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

@[irreducible]

def Batteries.BinaryHeap.heapifyDown {α : Type u_1} {sz : Nat} (lt : α → α → Bool) (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.

def Batteries.BinaryHeap.mkHeap {α : Type u_1} {sz : Nat} (lt : α → α → Bool) (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 lt a = Batteries.BinaryHeap.mkHeap.loop lt (sz / 2) a ⋯

def Batteries.BinaryHeap.mkHeap.loop {α : Type u_1} {sz : Nat} (lt : α → α → Bool) (i : Nat) (a : Vector α sz) : i ≤ sz → Vector α sz

Inner loop for mkHeap.

Equations

• Batteries.BinaryHeap.mkHeap.loop lt 0 x x_3 = x
• Batteries.BinaryHeap.mkHeap.loop lt i.succ x h = Batteries.BinaryHeap.mkHeap.loop lt i (Batteries.BinaryHeap.heapifyDown lt x ⟨i, ⋯⟩) ⋯

@[irreducible]

def Batteries.BinaryHeap.heapifyUp {α : Type u_1} {sz : Nat} (lt : α → α → Bool) (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

• Batteries.BinaryHeap.heapifyUp lt a ⟨0, isLt⟩ = a
• Batteries.BinaryHeap.heapifyUp lt a ⟨i'.succ, hi⟩ = if lt a[i' / 2] a[⟨i'.succ, hi⟩] = true then Batteries.BinaryHeap.heapifyUp lt (a.swap (↑⟨i'.succ, hi⟩) (i' / 2) ⋯ ⋯) ⟨i' / 2, ⋯⟩ else a

def Batteries.BinaryHeap.empty {α : Type u_1} (lt : α → α → Bool) : Batteries.BinaryHeap α lt

O(1). Build a new empty heap.

Equations

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

instance Batteries.BinaryHeap.instInhabited {α : Type u_1} (lt : α → α → Bool) : Inhabited (Batteries.BinaryHeap α lt)

Equations

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

instance Batteries.BinaryHeap.instEmptyCollection {α : Type u_1} (lt : α → α → Bool) : EmptyCollection (Batteries.BinaryHeap α lt)

Equations

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

def Batteries.BinaryHeap.singleton {α : Type u_1} (lt : α → α → Bool) (x : α) : Batteries.BinaryHeap α lt

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

Equations

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

def Batteries.BinaryHeap.size {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) : Nat

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

Equations

• self.size = self.arr.size

def Batteries.BinaryHeap.vector {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) : Vector α self.size

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

Equations

• self.vector = { toArray := self.arr, size_toArray := ⋯ }

def Batteries.BinaryHeap.get {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) (i : Fin self.size) : α

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

Equations

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

def Batteries.BinaryHeap.insert {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) (x : α) : Batteries.BinaryHeap α lt

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

Equations

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

@[simp]

theorem Batteries.BinaryHeap.size_insert {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) (x : α) : (self.insert x).size = self.size + 1

def Batteries.BinaryHeap.max {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) : Option α

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

Equations

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

def Batteries.BinaryHeap.popMax {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) : Batteries.BinaryHeap α lt

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} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) : self.popMax.size = self.size - 1

def Batteries.BinaryHeap.extractMax {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) : Option α × Batteries.BinaryHeap α lt

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

Equations

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

theorem Batteries.BinaryHeap.size_pos_of_max {α : Type u_1} {lt : α → α → Bool} {x : α} {self : Batteries.BinaryHeap α lt} (h : self.max = some x) : 0 < self.size

def Batteries.BinaryHeap.insertExtractMax {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) (x : α) : α × Batteries.BinaryHeap α lt

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

Equations

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

def Batteries.BinaryHeap.replaceMax {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) (x : α) : Option α × Batteries.BinaryHeap α lt

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

Equations

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

def Batteries.BinaryHeap.decreaseKey {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) (i : Fin self.size) (x : α) : Batteries.BinaryHeap α lt

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

Equations

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

def Batteries.BinaryHeap.increaseKey {α : Type u_1} {lt : α → α → Bool} (self : Batteries.BinaryHeap α lt) (i : Fin self.size) (x : α) : Batteries.BinaryHeap α lt

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

Equations

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

def Batteries.Vector.toBinaryHeap {α : Type u_1} {n : Nat} (lt : α → α → Bool) (v : Vector α n) : Batteries.BinaryHeap α lt

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

Equations

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

def Array.toBinaryHeap {α : Type u_1} (lt : α → α → Bool) (a : Array α) : Batteries.BinaryHeap α lt

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

Equations

• Array.toBinaryHeap lt a = { arr := (Batteries.BinaryHeap.mkHeap lt { toArray := a, size_toArray := ⋯ }).toArray }

@[specialize #[]]

def Array.heapSort {α : Type u_1} (a : Array α) (lt : α → α → Bool) : Array α

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

Equations

• a.heapSort lt = Array.heapSort.loop lt (Array.toBinaryHeap (flip lt) a) #[]

@[irreducible]

def Array.heapSort.loop {α : Type u_1} (lt : α → α → Bool) (a : Batteries.BinaryHeap α (flip lt)) (out : Array α) : Array α

Inner loop for heapSort.

Equations

• Array.heapSort.loop lt a out = match e : a.max with | none => out | some x => let_fun this := ⋯; Array.heapSort.loop lt a.popMax (out.push x)