heapifyDown related lemmas

heapifyUp related lemmas

Other permutation related lemmas

theorem Batteries.BinaryHeap.popMax_perm {α : Type u_1} [Ord α] {heap : BinaryHeap α} (h : 0 < heap.size) : (heap.arr[0] :: heap.popMax.arr.toList).Perm heap.arr.toList

popMax returns a permutation: the original is a perm of max :: popMax

theorem Batteries.BinaryHeap.toSortedArray_perm {α : Type u_1} [Ord α] (heap : BinaryHeap α) : heap.toSortedArray.Perm heap.arr

toSortedArray produces a permutation of the heap.

@[simp]

theorem Batteries.BinaryHeap.size_empty {α : Type u_1} [Ord α] : empty.size = 0

@[simp]

theorem Batteries.BinaryHeap.size_singleton {α : Type u_1} [Ord α] {x : α} : (singleton x).size = 1

@[simp]

theorem Batteries.BinaryHeap.empty_wf {α : Type u_1} [Ord α] : empty.WF

@[simp]

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

@[simp]

theorem Batteries.BinaryHeap.max_empty {α : Type u_1} [Ord α] : empty.max = none

@[simp]

theorem Batteries.BinaryHeap.max_singleton {α : Type u_1} [Ord α] {x : α} : (singleton x).max = some x

@[simp]

theorem Batteries.BinaryHeap.mkHeap_wf {α : Type u_1} {sz : Nat} [Ord α] [Std.TransOrd α] {a : Vector α sz} : WF.TopDown (mkHeap a)

Constructing a heap from a vector produces a well-formed heap.

theorem Batteries.BinaryHeap.mkHeap_perm {α : Type u_1} {sz : Nat} [Ord α] {a : Vector α sz} : (mkHeap a).toArray.Perm a.toArray

@[simp]

theorem Batteries.BinaryHeap.extractMax_fst {α : Type u_1} [Ord α] (heap : BinaryHeap α) : heap.extractMax.fst = heap.max

@[simp]

theorem Batteries.BinaryHeap.extractMax_snd {α : Type u_1} [Ord α] (heap : BinaryHeap α) : heap.extractMax.snd = heap.popMax

@[simp]

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

@[simp]

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

@[simp]

theorem Batteries.BinaryHeap.insert_wf {α : Type u_1} {x : α} [Ord α] [Std.TransOrd α] {heap : BinaryHeap α} (h_wf : heap.WF) : (heap.insert x).WF

@[simp]

theorem Batteries.BinaryHeap.mem_empty {α : Type u_1} [Ord α] {x : α} : ¬x ∈ empty

theorem Batteries.BinaryHeap.mem_singleton {α : Type u_1} {y : α} [Ord α] {x : α} : x ∈ singleton y ↔ x = y

theorem Batteries.BinaryHeap.mem_insert {α : Type u_1} {x y : α} [Ord α] {heap : BinaryHeap α} : y ∈ heap.insert x ↔ y ∈ heap ∨ y = x

theorem Batteries.BinaryHeap.mem_iff_get {α : Type u_1} {a : α} [Ord α] {heap : BinaryHeap α} : a ∈ heap ↔ ∃ (i : Fin heap.size), heap.get i = a

@[simp]

theorem Batteries.BinaryHeap.max_ge_all {α : Type u_1} {y : α} [Ord α] [Std.TransOrd α] {heap : BinaryHeap α} (hwf : heap.WF) (h_in : y ∈ heap) (h_ne : heap.size > 0) : (compare (heap.max.get ⋯) y).isGE = true

@[simp]

theorem Batteries.BinaryHeap.popMax_wf {α : Type u_1} [Ord α] [Std.TransOrd α] {heap : BinaryHeap α} (h_wf : heap.WF) : heap.popMax.WF

Removing the maximum element from a well-formed heap preserves well-formedness.

@[simp]

theorem Batteries.BinaryHeap.replaceMax_wf {α : Type u_1} {x : α} [Ord α] [Std.TransOrd α] {heap : BinaryHeap α} (h_wf : heap.WF) : (heap.replaceMax x).snd.WF

Replacing the maximum element in a well-formed heap preserves well-formedness.

@[simp]

theorem Batteries.BinaryHeap.insertExtractMax_wf {α : Type u_1} {x : α} [Ord α] [Std.TransOrd α] {heap : BinaryHeap α} (h_wf : heap.WF) : (heap.insertExtractMax x).snd.WF

@[simp]

theorem Batteries.BinaryHeap.size_insertExtractMax {α : Type u_1} [Ord α] (heap : BinaryHeap α) (x : α) : (heap.insertExtractMax x).snd.size = heap.size

@[simp]

theorem Batteries.BinaryHeap.insertExtractMax_fst_of_empty {α : Type u_1} [Ord α] {heap : BinaryHeap α} (h : heap.size = 0) (x : α) : (heap.insertExtractMax x).fst = x

theorem Batteries.BinaryHeap.insertExtractMax_fst_of_lt {α : Type u_1} {m x : α} [Ord α] {heap : BinaryHeap α} (hmax : heap.max = some m) (h_lt : (compare x m).isLT = true) : (heap.insertExtractMax x).fst = m

theorem Batteries.BinaryHeap.insertExtractMax_fst_of_not_lt {α : Type u_1} {m x : α} [Ord α] {heap : BinaryHeap α} (hmax : heap.max = some m) (h_nlt : ¬(compare x m).isLT = true) : (heap.insertExtractMax x).fst = x

@[simp]

theorem Batteries.BinaryHeap.insertExtractMax_empty {α : Type u_1} [Ord α] (x : α) : empty.insertExtractMax x = (x, empty)

@[simp]

theorem Batteries.BinaryHeap.replaceMax_empty {α : Type u_1} [Ord α] (x : α) : empty.replaceMax x = (none, singleton x)

@[simp]

theorem Batteries.BinaryHeap.size_replaceMax_of_empty {α : Type u_1} [Ord α] {heap : BinaryHeap α} (h : heap.size = 0) (x : α) : (heap.replaceMax x).snd.size = 1

@[simp]

theorem Batteries.BinaryHeap.size_replaceMax_of_nonempty {α : Type u_1} [Ord α] {heap : BinaryHeap α} (h : heap.size ≠ 0) (x : α) : (heap.replaceMax x).snd.size = heap.size

@[simp]

theorem Batteries.BinaryHeap.replaceMax_fst {α : Type u_1} [Ord α] (heap : BinaryHeap α) (x : α) : (heap.replaceMax x).fst = heap.max

@[simp]

theorem Batteries.BinaryHeap.popMax_empty {α : Type u_1} [Ord α] : empty.popMax = empty

@[simp]

theorem Batteries.BinaryHeap.extractMax_empty {α : Type u_1} [Ord α] : empty.extractMax = (none, empty)

theorem Batteries.BinaryHeap.mem_of_mem_popMax {α : Type u_1} {x : α} [Ord α] {heap : BinaryHeap α} (h : x ∈ heap.popMax) : x ∈ heap

Elements in popMax were in the original heap

@[simp]

theorem Batteries.BinaryHeap.decreaseKey_wf {α : Type u_1} {x : α} [Ord α] [Std.TransOrd α] {heap : BinaryHeap α} {i : Fin heap.size} (hwf : heap.WF) (h_ge : (compare (heap.get i) x).isGE = true) : (heap.decreaseKey i x).WF

Decreasing a key value in a well-formed heap and reheapifying downward preserves well-formedness.

@[simp]

theorem Batteries.BinaryHeap.increaseKey_wf {α : Type u_1} {x : α} [Ord α] [Std.TransOrd α] {heap : BinaryHeap α} {i : Fin heap.size} (h_wf : heap.WF) (h_ge : (compare x (heap.get i)).isGE = true) : (heap.increaseKey i x).WF

Increasing a key value in a well-formed heap and reheapifying upward preserves well-formedness.

theorem Batteries.BinaryHeap.toSortedArray_sorted {α : Type u_1} [Ord α] [Std.TransOrd α] {heap : BinaryHeap α} (hwf : heap.WF) : List.Pairwise (fun (x1 x2 : α) => (compare x1 x2).isGE = true) heap.toSortedArray.toList

toSortedArray produces a sorted array if the heap is well-formed

@[simp]

theorem Batteries.BinaryHeap.size_toSortedArray {α : Type u_1} [Ord α] {heap : BinaryHeap α} : heap.toSortedArray.size = heap.size

@[simp]

theorem Batteries.BinaryHeap.mem_toSortedArray {α : Type u_1} [Ord α] {heap : BinaryHeap α} {x : α} : x ∈ heap.toSortedArray ↔ x ∈ heap

@[simp]

theorem Array.toBinaryHeap_wf {α : Type u_1} [Ord α] [Std.TransOrd α] {a : Array α} : a.toBinaryHeap.WF

Converting an array to a binary heap produces a well-formed heap.

@[simp]

theorem Vector.toBinaryHeap_wf {α : Type u_1} {sz : Nat} [Ord α] [Std.TransOrd α] {a : Vector α sz} : a.toBinaryHeap.WF

Converting a vector to a binary heap produces a well-formed heap.

@[simp]

theorem Array.size_toBinaryHeap {α : Type u_1} [Ord α] {a : Array α} : a.toBinaryHeap.size = a.size

@[simp]

theorem Batteries.Vector.size_toBinaryHeap {α : Type u_1} {sz : Nat} [Ord α] {a : Vector α sz} : a.toBinaryHeap.size = sz

@[simp]

theorem Array.mem_toBinaryHeap {α : Type u_1} {x : α} [Ord α] {a : Array α} : x ∈ a.toBinaryHeap ↔ x ∈ a

@[simp]

theorem Batteries.Vector.mem_toBinaryHeap {α : Type u_1} {sz : Nat} [Ord α] {a : Vector α sz} {x : α} : x ∈ a.toBinaryHeap ↔ x ∈ a

theorem Array.heapSort_perm {α : Type u_1} [instOrd : Ord α] {a : Array α} : a.heapSort.Perm a

@[simp]

theorem Array.size_heapSort {α : Type u_1} [Ord α] {a : Array α} : a.heapSort.size = a.size

theorem Array.heapSort_sorted {α : Type u_1} [instOrd : Ord α] [Std.TransOrd α] {a : Array α} : List.Pairwise (fun (x1 x2 : α) => (compare x1 x2).isLE = true) a.heapSort.toList

heapSort produces a sorted array.