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

A max-heap data structure.

• arr : Array α

def BinaryHeap.heapifyDown {α : Type u_1} (lt : α → α → Bool) (a : Array α) (i : Fin (Array.size a)) : { a' : Array α // 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.

@[simp]

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

def BinaryHeap.mkHeap {α : Type u_1} (lt : α → α → Bool) (a : Array α) : { a' : Array α // 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 ⋯

def BinaryHeap.mkHeap.loop {α : Type u_1} (lt : α → α → Bool) (i : Nat) (a : Array α) : i ≤ Array.size a → { a' : Array α // 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 := ⋯ }

@[simp]

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

def BinaryHeap.heapifyUp {α : Type u_1} (lt : α → α → Bool) (a : Array α) (i : Fin (Array.size a)) : { a' : Array α // 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.

@[simp]

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

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

O(1). Build a new empty heap.

Equations

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

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

Equations

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

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

Equations

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

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] }

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

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

Equations

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

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

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

• BinaryHeap.insert self x = { arr := let n := BinaryHeap.size self; (BinaryHeap.heapifyUp lt (Array.push self.arr x) { val := n, isLt := ⋯ }).val }

@[simp]

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

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

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

Auxiliary for popMax.

Equations

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

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).val

@[simp]

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

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)

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

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.

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.

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.

Equations

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

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.

Equations

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

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).val }

@[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) #[]

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

Equations

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