ink

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

• arr : Array α

A max-heap data structure.

ink

def BinaryHeap.heapifyDown {α : Type u_1} (lt : α → α → Bool) (a : Array α) (i : Fin (Array.size a)) : { a' // Array.size a' = Array.size a }

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.

ink

@[simp]

theorem BinaryHeap.size_heapifyDown {α : Type u_1} (lt : α → α → Bool) (a : Array α) (i : Fin (Array.size a)) : Array.size ↑(BinaryHeap.heapifyDown lt a i) = Array.size a

ink

def BinaryHeap.mkHeap {α : Type u_1} (lt : α → α → Bool) (a : Array α) : { a' // Array.size a' = Array.size a }

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

Equations

• BinaryHeap.mkHeap lt a = BinaryHeap.mkHeap.loop lt (Array.size a / 2) a (_ : Array.size a / 2 ≤ Array.size a)

ink

def BinaryHeap.mkHeap.loop {α : Type u_1} (lt : α → α → Bool) (i : ℕ) (a : Array α) : i ≤ Array.size a → { a' // Array.size a' = Array.size a }

Equations

• One or more equations did not get rendered due to their size.
• BinaryHeap.mkHeap.loop lt 0 x x_1 = { val := x, property := (_ : Array.size x = Array.size x) }

ink

@[simp]

theorem BinaryHeap.size_mkHeap {α : Type u_1} (lt : α → α → Bool) (a : Array α) : Array.size ↑(BinaryHeap.mkHeap lt a) = Array.size a

ink

def BinaryHeap.heapifyUp {α : Type u_1} (lt : α → α → Bool) (a : Array α) (i : Fin (Array.size a)) : { a' // Array.size a' = Array.size a }

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.

ink

@[simp]

theorem BinaryHeap.size_heapifyUp {α : Type u_1} (lt : α → α → Bool) (a : Array α) (i : Fin (Array.size a)) : Array.size ↑(BinaryHeap.heapifyUp lt a i) = Array.size a

ink

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

O(1). Build a new empty heap.

Equations

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

ink

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

Equations

• BinaryHeap.instInhabitedBinaryHeap lt = { default := BinaryHeap.empty lt }

ink

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

Equations

• BinaryHeap.instEmptyCollectionBinaryHeap lt = { emptyCollection := BinaryHeap.empty lt }

ink

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

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

Equations

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

ink

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

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

Equations

• BinaryHeap.size self = Array.size self.arr

ink

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

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

Equations

• BinaryHeap.get self i = Array.get self.arr i

ink

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

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

Equations

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

ink

@[simp]

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

ink

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

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

Equations

• BinaryHeap.max self = Array.get? self.arr 0

ink

def BinaryHeap.popMaxAux {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) : { a' // BinaryHeap.size a' = BinaryHeap.size self - 1 }

Auxiliary for popMax.

Equations

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

ink

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

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

Equations

• BinaryHeap.popMax self = ↑(BinaryHeap.popMaxAux self)

ink

@[simp]

theorem BinaryHeap.size_popMax {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) : BinaryHeap.size (BinaryHeap.popMax self) = BinaryHeap.size self - 1

ink

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

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

Equations

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

ink

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

ink

def BinaryHeap.insertExtractMax {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) (x : α) : α × 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.

ink

def BinaryHeap.replaceMax {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) (x : α) : Option α × 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.

ink

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

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

Equations

• BinaryHeap.decreaseKey self i x = { arr := ↑(BinaryHeap.heapifyDown lt (Array.set self.arr i x) { val := ↑i, isLt := (_ : ↑i < Array.size (Array.set self.arr i x)) }) }

ink

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

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

Equations

• BinaryHeap.increaseKey self i x = { arr := ↑(BinaryHeap.heapifyUp lt (Array.set self.arr i x) { val := ↑i, isLt := (_ : ↑i < Array.size (Array.set self.arr i x)) }) }

ink

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

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

Equations

• Array.toBinaryHeap lt a = { arr := ↑(BinaryHeap.mkHeap lt a) }

ink

@[specialize #[]]

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

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

Equations

• Array.heapSort a lt = let gt := fun y x => lt x y; Array.heapSort.loop lt (Array.toBinaryHeap gt a) #[]

ink

def Array.heapSort.loop {α : Type u_1} (lt : α → α → Bool) (a : BinaryHeap α fun y x => lt x y) (out : Array α) : Array α

Equations

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