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

A max-heap data structure.

• arr : Array α

  Backing array for BinaryHeap.

@[irreducible]

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

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 Batteries.BinaryHeap.size_heapifyDown {α : Type u_1} (lt : α → α → Bool) (a : Array α) (i : Fin a.size) : (Batteries.BinaryHeap.heapifyDown lt a i).val.size = a.size

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

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 (a.size / 2) a ⋯

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

Inner loop for mkHeap.

Equations

• Batteries.BinaryHeap.mkHeap.loop lt 0 x x_1 = ⟨x, ⋯⟩
• Batteries.BinaryHeap.mkHeap.loop lt i.succ x x_1 = match Batteries.BinaryHeap.mkHeap.loop lt i (Batteries.BinaryHeap.heapifyDown lt x ⟨i, ⋯⟩).val ⋯ with | ⟨a₂, h₂⟩ => ⟨a₂, ⋯⟩

@[simp]

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

@[irreducible]

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

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 Batteries.BinaryHeap.size_heapifyUp {α : Type u_1} (lt : α → α → Bool) (a : Array α) (i : Fin a.size) : (Batteries.BinaryHeap.heapifyUp lt a i).val.size = a.size

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.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.get 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 := let n := self.size; (Batteries.BinaryHeap.heapifyUp lt (self.arr.push x) ⟨n, ⋯⟩).val }

@[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.get? 0

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

Auxiliary for popMax.

Equations

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

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

• self.popMax = self.popMaxAux.val

@[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} (e : 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.arr.set i x) ⟨↑i, ⋯⟩).val }

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.arr.set i x) ⟨↑i, ⋯⟩).val }

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

• 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)