d-ary heap

DefinitionNormalized heap arity#✓fully proved

The normalized arity of a requested arity \(r \in \mathbb{N}\) is \(\max(2, r)\): the requested arities \(0\) and \(1\) become \(2\) (the binary-heap policy), and every \(r \ge 2\) is left unchanged.

def normalizedArity (requested : Nat) : Nat := max 2 requested

Used by 4

Used byArity of a \(d\)-ary heap built from a list · Empty d-ary heap · Normalization leaves a valid arity unchanged · Normalized arities are at least two

TheoremNormalized arities are at least two#✓fully proved

For every natural number \(r\), the normalized arity \(\max(2, r)\) of \(r\) is at least \(2\).

theorem normalizedArity_valid (requested : Nat) : 2 ≤ normalizedArity requested

Uses 1 · Used by 1

Statement usesNormalized heap arity

Used byEmpty d-ary heap

TheoremNormalization leaves a valid arity unchanged#✓fully proved

For every natural number \(d \ge 2\), the normalized arity \(\max(2, d)\) of \(d\) equals \(d\).

@[simp] theorem normalizedArity_eq {d : Nat} (hd : 2 ≤ d) : normalizedArity d = d

Uses 1

Statement usesNormalized heap arity

DefinitionParent index in a \(d\)-ary tree#✓fully proved

For natural numbers \(d\) and \(i\), the \(d\)-ary parent of \(i\) is \(\lfloor (i - 1)/d \rfloor\), computed in the natural numbers: \(i - 1\) is truncated at \(0\), so the parent of \(0\) is \(0\), and division by \(0\) gives \(0\).

This is the parent index when a \(d\)-ary tree is stored in level order in an array with its root at index \(0\).

def daryParent (d i : Nat) : Nat := (i - 1) / d

Used by 17

Used by\(d\)-ary heap order · Last-to-root move in a \(d\)-ary heap is ready for sift-down · The parent of a \(d\)-ary child · A \(d\)-ary parent has a smaller index · The \(d\)-ary parent of a valid index is valid · Pushing onto a \(d\)-ary heap leaves it ready for sifting up · Sifting down restores \(d\)-ary heap order · Readiness for \(d\)-ary sift-down · \(d\)-ary sift-up · Sift-up restores \(d\)-ary heap order · Sifting up permutes the array · Arrays ready for \(d\)-ary sift-up · Empty d-ary heap · Extracted minimum and remaining d-ary heap recover the original elements · Removing the root of a \(d\)-ary min-heap · Removing the root of a \(d\)-ary heap preserves its arity · The root of a \(d\)-ary heap-ordered array is a minimum

DefinitionChild index in a \(d\)-ary heap array#✓fully proved

For natural numbers \(d\), \(i\) and \(k\), the child of index \(i\) with zero-based offset \(k\) in a contiguous level-order \(d\)-ary tree is the index \(d i + k + 1\).

def daryChild (d i k : Nat) : Nat := d * i + k + 1

Used by 5

Used byThe parent of a \(d\)-ary child · Sifting down restores \(d\)-ary heap order · Smallest child among the offsets from \(s\) · The smallest child lies after its parent · The smallest child is a valid index

TheoremThe parent of a \(d\)-ary child#✓fully proved

Let \(d\), \(i\) and \(k\) be natural numbers with \(d \ge 2\) and \(k < d\). Then the \(d\)-ary parent of the child of \(i\) with zero-based offset \(k\), that is, of the index \(di + k + 1\), is \(i\).

theorem daryParent_child {d i k : Nat} (_hd : 2 ≤ d) (hk : k < d) :
    daryParent d (daryChild d i k) = i

Uses 2 · Used by 1

Statement usesChild index in a \(d\)-ary heap array · Parent index in a \(d\)-ary tree

Used bySifting down restores \(d\)-ary heap order

TheoremA \(d\)-ary parent has a smaller index#✓fully proved

Let \(d\) and \(i\) be natural numbers with \(d \ge 2\) and \(i > 0\). Then the \(d\)-ary parent of \(i\) is strictly less than \(i\).

theorem daryParent_lt {d i : Nat} (_hd : 2 ≤ d) (hi : 0 < i) :
    daryParent d i < i

Uses 1 · Used by 8

Statement usesParent index in a \(d\)-ary tree

Used byLast-to-root move in a \(d\)-ary heap is ready for sift-down · The \(d\)-ary parent of a valid index is valid · Pushing onto a \(d\)-ary heap leaves it ready for sifting up · Sifting down restores \(d\)-ary heap order · \(d\)-ary sift-up · Sift-up restores \(d\)-ary heap order · Sifting up permutes the array · The root of a \(d\)-ary heap-ordered array is a minimum

TheoremThe \(d\)-ary parent of a valid index is valid#✓fully proved

Let \(d \ge 2\) be a natural number, let \(a\) be an array over any type, write \(|a|\) for its size, and let \(i\) be an index with \(0 < i < |a|\). Then the \(d\)-ary parent of \(i\) is also less than \(|a|\).

theorem daryParent_lt_size {α : Type u} (d : Nat) (hd : 2 ≤ d)
    (a : Array α) (i : Nat) (hi : i < a.size) (hpos : 0 < i) :
    daryParent d i < a.size

Uses 2 · Used by 14

Statement usesParent index in a \(d\)-ary tree

Proof usesA \(d\)-ary parent has a smaller index

Used by\(d\)-ary heap order · Last-to-root move in a \(d\)-ary heap is ready for sift-down · Pushing onto a \(d\)-ary heap leaves it ready for sifting up · Sifting down restores \(d\)-ary heap order · Readiness for \(d\)-ary sift-down · \(d\)-ary sift-up · Sift-up restores \(d\)-ary heap order · Sifting up permutes the array · Arrays ready for \(d\)-ary sift-up · Empty d-ary heap · Extracted minimum and remaining d-ary heap recover the original elements · Removing the root of a \(d\)-ary min-heap · Removing the root of a \(d\)-ary heap preserves its arity · The root of a \(d\)-ary heap-ordered array is a minimum

Structure\(d\)-ary heap order#✓fully proved

Let \(d\) be a natural number and \(a = (a_0, \dots, a_{n-1})\) an array with entries in a type carrying a relation \(\le\). The array \(a\) is \(d\)-ary heap ordered when \(d \ge 2\) and every nonroot entry is at least the entry at its parent index: \(a_{\lfloor (i-1)/d \rfloor} \le a_i\) for every index \(i\) with \(0 < i < n\).

structure DaryHeapOrdered {α : Type u} [LE α] (d : Nat) (a : Array α) : Prop where
  arity_valid : 2 ≤ d
  parent_le : ∀ i (hi : i < a.size), (hpos : 0 < i) →
    a[daryParent d i]'(daryParent_lt_size d arity_valid a i hi hpos) ≤ a[i]

Uses 2 · Used by 15

Statement usesParent index in a \(d\)-ary tree · The \(d\)-ary parent of a valid index is valid

Used by\(d\)-ary min-heap · Last-to-root move in a \(d\)-ary heap is ready for sift-down · Pushing onto a \(d\)-ary heap leaves it ready for sifting up · Sifting down restores \(d\)-ary heap order · Sift-up restores \(d\)-ary heap order · Empty d-ary heap · Extracted minimum and remaining d-ary heap recover the original elements · The extracted minimum of a d-ary heap is a lower bound · Extracting the minimum leaves a heap-ordered \(d\)-ary heap · Removing the root of a \(d\)-ary min-heap · Removing the root of a \(d\)-ary heap preserves its arity · The minimum query on a \(d\)-ary heap returns a least element · Insertion into a \(d\)-ary heap · Insertion keeps a \(d\)-ary heap ordered · The root of a \(d\)-ary heap-ordered array is a minimum

StructureArrays ready for \(d\)-ary sift-up#✓fully proved

Let \(a = (a_0, \dots, a_{|a|-1})\) be an array over a type with a relation \(\le\), let \(d\) and \(i\) be natural numbers, and write \(p(j) = \lfloor (j-1)/d \rfloor\) for the parent of an index \(j > 0\). The array \(a\) is ready for sift-up at \(i\) when \(d \ge 2\), \(i < |a|\), \(a_{p(j)} \le a_j\) for every \(0 < j < |a|\) with \(j \ne i\), and, if \(i > 0\), \(a_{p(i)} \le a_j\) for every \(0 < j < |a|\) with \(p(j) = i\).

So the only edge that may violate heap order is the one entering \(i\), and the parent of \(i\) is no greater than the children of \(i\).

structure DarySiftUpReady {α : Type u} [LE α]
    (d : Nat) (a : Array α) (i : Nat) : Prop where
  arity_valid : 2 ≤ d
  index_valid : i < a.size
  ordered_except : ∀ j (hj : j < a.size), (hjpos : 0 < j) → j ≠ i →
    a[daryParent d j]'(daryParent_lt_size d arity_valid a j hj hjpos) ≤ a[j]
  parent_below_children : ∀ j (hj : j < a.size), (hjpos : 0 < j) →
    daryParent d j = i → (hipos : 0 < i) →
    a[daryParent d i]'(daryParent_lt_size d arity_valid a i index_valid hipos) ≤ a[j]

Uses 2 · Used by 3

Statement usesParent index in a \(d\)-ary tree · The \(d\)-ary parent of a valid index is valid

Used byPushing onto a \(d\)-ary heap leaves it ready for sifting up · Sift-up restores \(d\)-ary heap order · Insertion into a \(d\)-ary heap

Definition\(d\)-ary sift-up#✓fully proved

Let \(d \ge 2\), let \(a\) be an array over a linearly ordered type, of length \(|a|\) with entries \(a_0, \dots, a_{|a|-1}\), let \(i\) be a natural number, and write \(p(i) = \lfloor (i-1)/d \rfloor\) for the parent of \(i > 0\). The sift-up of \(a\) from \(i\) is defined recursively: if \(0 < i < |a|\) and \(a_i < a_{p(i)}\), it is the sift-up from \(p(i)\) of the array obtained from \(a\) by swapping the entries at positions \(i\) and \(p(i)\); otherwise it is \(a\).

Cslib.Algorithms.Lean.darySiftUp · 16 lines

def darySiftUp {α : Type u} [LinearOrder α]
    (a : Array α) (i d : Nat) (hd : 2 ≤ d) : Array α :=
  if hi : i < a.size then
    if hpos : 0 < i then
      let p := daryParent d i
      if hlt : a[i] < a[p]'(daryParent_lt_size d hd a i hi hpos) then
        darySiftUp (a.swap i p hi (daryParent_lt_size d hd a i hi hpos)) p d hd
      else
        a
    else
      a
  else
    a
termination_by i
decreasing_by
  exact daryParent_lt hd hpos

Uses 3 · Used by 5

Statement usesParent index in a \(d\)-ary tree · A \(d\)-ary parent has a smaller index · The \(d\)-ary parent of a valid index is valid

Used bySifting up preserves the multiset of entries · Sift-up restores \(d\)-ary heap order · Sifting up permutes the array · Insertion into a d-ary heap adds one occurrence · Insertion into a \(d\)-ary heap

TheoremSifting up permutes the array#✓fully proved

Let \(d \ge 2\), let \(a\) be an array over a linearly ordered type and let \(i\) be a natural number. The array obtained from \(a\) by \(d\)-ary sift-up from index \(i\) is a permutation of \(a\).

theorem darySiftUp_perm {α : Type u} [LinearOrder α]
    (a : Array α) (i d : Nat) (hd : 2 ≤ d) :
    (darySiftUp a i d hd).Perm a

Uses 4 · Used by 2

Statement uses\(d\)-ary sift-up

Proof usesParent index in a \(d\)-ary tree · A \(d\)-ary parent has a smaller index · The \(d\)-ary parent of a valid index is valid

Used bySifting up preserves the multiset of entries · Insertion into a d-ary heap adds one occurrence

TheoremSifting up preserves the multiset of entries#✓fully proved

Let \(d \ge 2\), let \(a\) be an array over a linearly ordered type and let \(i\) be a natural number. The array obtained from \(a\) by \(d\)-ary sift-up from index \(i\) has the same multiset of entries as \(a\).

theorem darySiftUp_multiset {α : Type u} [LinearOrder α]
    (a : Array α) (i d : Nat) (hd : 2 ≤ d) :
    (↑(darySiftUp a i d hd).toList : Multiset α) = (↑a.toList : Multiset α)

Uses 2

Statement uses\(d\)-ary sift-up

Proof usesSifting up permutes the array

TheoremThe root of a \(d\)-ary heap-ordered array is a minimum#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(d \ge 2\), and let \(a\) be an array of elements of \(\alpha\) that is \(d\)-ary heap-ordered. Then \(a_0 \le a_i\) for every index \(i\) smaller than the size of \(a\).

theorem DaryHeapOrdered.root_le {α : Type u} [LinearOrder α]
    {d : Nat} (hd : 2 ≤ d) {a : Array α} (h : DaryHeapOrdered d a)
    (i : Nat) (hi : i < a.size) : a[0]'(by omega) ≤ a[i]

Uses 4 · Used by 2

Statement uses\(d\)-ary heap order

Proof usesParent index in a \(d\)-ary tree · A \(d\)-ary parent has a smaller index · The \(d\)-ary parent of a valid index is valid

Used byThe extracted minimum of a d-ary heap is a lower bound · The minimum query on a \(d\)-ary heap returns a least element

TheoremSift-up restores \(d\)-ary heap order#✓fully proved

Let \(a\) be an array over a linearly ordered type, of length \(|a|\) with entries \(a_0, \dots, a_{|a|-1}\), let \(d\) and \(i\) be natural numbers, and write \(p(j) = \lfloor (j-1)/d \rfloor\) for the parent of an index \(j > 0\). Suppose \(a\) is ready for sift-up at \(i\): \(d \ge 2\), \(i < |a|\), \(a_{p(j)} \le a_j\) for every \(0 < j < |a|\) with \(j \ne i\), and, if \(i > 0\), \(a_{p(i)} \le a_j\) for every \(0 < j < |a|\) with \(p(j) = i\). Then the array \(b\), of length \(|b|\) with entries \(b_0, \dots, b_{|b|-1}\), obtained from \(a\) by \(d\)-ary sift-up from index \(i\) is \(d\)-ary heap ordered: \(b_{p(j)} \le b_j\) for every \(0 < j < |b|\).

theorem darySiftUp_ordered {α : Type u} [LinearOrder α]
    (d : Nat) (a : Array α) (i : Nat) (h : DarySiftUpReady d a i) :
    DaryHeapOrdered d (darySiftUp a i d h.arity_valid)

Uses 6 · Used by 1

Statement uses\(d\)-ary heap order · Arrays ready for \(d\)-ary sift-up · \(d\)-ary sift-up

Proof usesParent index in a \(d\)-ary tree · A \(d\)-ary parent has a smaller index · The \(d\)-ary parent of a valid index is valid

Used byInsertion into a \(d\)-ary heap

TheoremPushing onto a \(d\)-ary heap leaves it ready for sifting up#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(d \ge 2\), and let \(a\) be an array over \(\alpha\) that is \(d\)-ary heap ordered, with size \(|a|\). Then for every \(x \in \alpha\), the array obtained by appending \(x\) to \(a\) is ready for \(d\)-ary sifting up at index \(|a|\), the position of \(x\); in particular every nonroot entry other than \(x\) is at least its \(d\)-ary parent.

theorem daryPush_siftUpReady {α : Type u} [LinearOrder α]
    (d : Nat) (hd : 2 ≤ d) (a : Array α) (h : DaryHeapOrdered d a) (x : α) :
    DarySiftUpReady d (a.push x) a.size

Uses 5 · Used by 1

Statement uses\(d\)-ary heap order · Arrays ready for \(d\)-ary sift-up

Proof usesParent index in a \(d\)-ary tree · A \(d\)-ary parent has a smaller index · The \(d\)-ary parent of a valid index is valid

Used byInsertion into a \(d\)-ary heap

StructureReadiness for \(d\)-ary sift-down#✓fully proved

Let \(a\) be an array over a type with a relation \(\le\), and let \(d\) and \(i\) be natural numbers. Write \(|a|\) for the size of \(a\) and \(p(j)\) for the \(d\)-ary parent of an index \(j\). The array \(a\) is ready for \(d\)-ary sifting down at \(i\) when \(d \ge 2\), \(i < |a|\), every index \(j\) with \(0 < j < |a|\) and \(p(j) \ne i\) satisfies \(a_{p(j)} \le a_j\), and, if \(i > 0\), every index \(j\) with \(0 < j < |a|\) and \(p(j) = i\) satisfies \(a_{p(i)} \le a_j\).

Thus the only edges that may violate heap order leave \(i\), and lifting a smallest child to \(i\) keeps the edge entering \(i\) ordered.

structure DarySiftDownReady {α : Type u} [LE α] (d : Nat) (a : Array α)
    (i : Nat) : Prop where
  arity_valid : 2 ≤ d
  index_valid : i < a.size
  ordered_except : ∀ j (hj : j < a.size), (hjpos : 0 < j) →
    daryParent d j ≠ i →
    a[daryParent d j]'(daryParent_lt_size d arity_valid a j hj hjpos) ≤ a[j]
  parent_below_children : ∀ j (hj : j < a.size), (hjpos : 0 < j) →
    daryParent d j = i → (hipos : 0 < i) →
    a[daryParent d i]'(daryParent_lt_size d arity_valid a i index_valid hipos) ≤
      a[j]

Uses 2 · Used by 2

Statement usesParent index in a \(d\)-ary tree · The \(d\)-ary parent of a valid index is valid

Used byLast-to-root move in a \(d\)-ary heap is ready for sift-down · Sifting down restores \(d\)-ary heap order

DefinitionSmallest child among the offsets from \(s\)#✓fully proved

Let \(a\) be an array over a linearly ordered type, of length \(|a|\), let \(d\), \(i\) and \(s\) be natural numbers, and call \(d i + k + 1\) the child of \(i\) at offset \(k\). Scanning the offsets \(s, s + 1, \dots, d - 1\), this returns the index of a scanned child of \(i\) below \(|a|\) whose entry in \(a\) is least among those, taking the smallest offset among ties, or nothing if no scanned child index is below \(|a|\).

Cslib.Algorithms.Lean.darySmallestChildFrom · 18 lines

def darySmallestChildFrom {α : Type u} [LinearOrder α]
    (a : Array α) (d i start : Nat) : Option Nat :=
  if hk : start < d then
    let c := daryChild d i start
    if hc : c < a.size then
      match darySmallestChildFrom a d i (start + 1) with
      | none => some c
      | some best =>
          if hbest : best < a.size then
            if a[best] < a[c] then some best else some c
          else
            some c
    else
      none
  else
    none
termination_by d - start
decreasing_by omega

Uses 1 · Used by 4

Statement usesChild index in a \(d\)-ary heap array

Used bySifting down restores \(d\)-ary heap order · Smallest child in a \(d\)-ary heap array · The smallest child lies after its parent · The smallest child is a valid index

DefinitionSmallest child in a \(d\)-ary heap array#✓fully proved

Let \(a\) be an array of length \(|a|\) over a linearly ordered type and let \(d\) and \(i\) be natural numbers. The children of \(i\) are the indices \(d i + k + 1\) for \(0 \le k < d\), and a child is valid when it is below \(|a|\). The smallest child of \(i\) is the valid child of \(i\) with the least entry, taking the smallest offset \(k\) among ties, or nothing if \(i\) has no valid child.

def darySmallestChild {α : Type u} [LinearOrder α]
    (a : Array α) (d i : Nat) : Option Nat :=
  darySmallestChildFrom a d i 0

Uses 1 · Used by 5

Statement usesSmallest child among the offsets from \(s\)

Used by\(d\)-ary sift-down · Sifting down restores \(d\)-ary heap order · Sifting down in a \(d\)-ary heap permutes the array · The smallest child lies after its parent · The smallest child is a valid index

TheoremThe smallest child is a valid index#✓fully proved

Let \(a\) be an array of length \(|a|\) over a linearly ordered type and let \(d\), \(i\) and \(c\) be natural numbers. If the smallest valid child of \(i\) in the \(d\)-ary heap array \(a\) is \(c\), then \(c < |a|\).

theorem darySmallestChild_valid {α : Type u} [LinearOrder α]
    (a : Array α) (d i c : Nat) (h : darySmallestChild a d i = some c) :
    c < a.size

Uses 3 · Used by 3

Statement usesSmallest child in a \(d\)-ary heap array

Proof usesChild index in a \(d\)-ary heap array · Smallest child among the offsets from \(s\)

Used by\(d\)-ary sift-down · Sifting down restores \(d\)-ary heap order · Sifting down in a \(d\)-ary heap permutes the array

TheoremThe smallest child lies after its parent#✓fully proved

Let \(d \ge 2\), let \(a\) be an array over a linearly ordered type and let \(i\) and \(c\) be natural numbers. If the smallest valid child of \(i\) in the \(d\)-ary heap array \(a\) is \(c\), then \(i < c\).

theorem darySmallestChild_gt {α : Type u} [LinearOrder α]
    {a : Array α} {d i c : Nat} (hd : 2 ≤ d)
    (h : darySmallestChild a d i = some c) : i < c

Uses 3 · Used by 3

Statement usesSmallest child in a \(d\)-ary heap array

Proof usesChild index in a \(d\)-ary heap array · Smallest child among the offsets from \(s\)

Used by\(d\)-ary sift-down · Sifting down restores \(d\)-ary heap order · Sifting down in a \(d\)-ary heap permutes the array

Definition\(d\)-ary sift-down#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(a\) be an array over \(\alpha\), and let \(i\) and \(d\) be natural numbers with \(d \ge 2\). Sifting down from \(i\) in \(a\) returns \(a\) if \(i\) has no valid \(d\)-ary child in \(a\). Otherwise let \(c\) be the smallest valid \(d\)-ary child of \(i\), with ties broken toward the lowest child offset: if \(a_c < a_i\), swap the entries at \(i\) and \(c\) and sift down from \(c\) in the resulting array; otherwise return \(a\).

Cslib.Algorithms.Lean.darySiftDown · 16 lines

def darySiftDown {α : Type u} [LinearOrder α]
    (a : Array α) (i d : Nat) (hd : 2 ≤ d) : Array α :=
  match hchild : darySmallestChild a d i with
  | none => a
  | some c =>
    have hc : c < a.size := darySmallestChild_valid a d i c hchild
    have hi : i < a.size := (darySmallestChild_gt hd hchild).trans hc
    if hlt : a[c] < a[i] then
      darySiftDown (a.swap i c hi hc) c d hd
    else
      a
termination_by a.size - i
decreasing_by
  simp only [Array.size_swap]
  have := darySmallestChild_gt hd hchild
  omega

Uses 3 · Used by 6

Statement usesSmallest child in a \(d\)-ary heap array · The smallest child lies after its parent · The smallest child is a valid index

Used bySifting down in a \(d\)-ary heap preserves the multiset of entries · Sifting down restores \(d\)-ary heap order · Sifting down in a \(d\)-ary heap permutes the array · Extracted minimum and remaining d-ary heap recover the original elements · Removing the root of a \(d\)-ary min-heap · Removing the root of a \(d\)-ary heap preserves its arity

TheoremSifting down in a \(d\)-ary heap permutes the array#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(a\) be an array over \(\alpha\), and let \(i\) and \(d\) be natural numbers with \(d \ge 2\). The array produced by \(d\)-ary sifting down from index \(i\) in \(a\) is a permutation of \(a\).

theorem darySiftDown_perm {α : Type u} [LinearOrder α]
    (a : Array α) (i d : Nat) (hd : 2 ≤ d) :
    (darySiftDown a i d hd).Perm a

Uses 4 · Used by 2

Statement uses\(d\)-ary sift-down

Proof usesSmallest child in a \(d\)-ary heap array · The smallest child lies after its parent · The smallest child is a valid index

Used bySifting down in a \(d\)-ary heap preserves the multiset of entries · Extracted minimum and remaining d-ary heap recover the original elements

TheoremSifting down in a \(d\)-ary heap preserves the multiset of entries#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(a\) be an array over \(\alpha\), and let \(i\) and \(d\) be natural numbers with \(d \ge 2\). The array produced by \(d\)-ary sifting down from index \(i\) in \(a\) has the same multiset of entries as \(a\).

theorem darySiftDown_multiset {α : Type u} [LinearOrder α]
    (a : Array α) (i d : Nat) (hd : 2 ≤ d) :
    (↑(darySiftDown a i d hd).toList : Multiset α) = (↑a.toList : Multiset α)

Uses 2

Statement uses\(d\)-ary sift-down

Proof usesSifting down in a \(d\)-ary heap permutes the array

TheoremSifting down restores \(d\)-ary heap order#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(d \ge 2\), and let \(a\) be an array over \(\alpha\) that is ready for \(d\)-ary sifting down at an index \(i\). Then the array produced by \(d\)-ary sifting down from index \(i\) in \(a\) is \(d\)-ary heap ordered.

theorem darySiftDown_ordered {α : Type u} [LinearOrder α]
    (d : Nat) (a : Array α) (i : Nat) (hd : 2 ≤ d)
    (h : DarySiftDownReady d a i) :
    DaryHeapOrdered d (darySiftDown a i d hd)

Uses 12 · Used by 3

Statement uses\(d\)-ary heap order · Readiness for \(d\)-ary sift-down · \(d\)-ary sift-down

Proof usesChild index in a \(d\)-ary heap array · Parent index in a \(d\)-ary tree · The parent of a \(d\)-ary child · A \(d\)-ary parent has a smaller index · The \(d\)-ary parent of a valid index is valid · Smallest child in a \(d\)-ary heap array · Smallest child among the offsets from \(s\) · The smallest child lies after its parent · The smallest child is a valid index

Used byExtracted minimum and remaining d-ary heap recover the original elements · Removing the root of a \(d\)-ary min-heap · Removing the root of a \(d\)-ary heap preserves its arity

DefinitionLast-to-root move on an array#✓fully proved

For a nonempty array \(a = (a_0, \dots, a_{n-1})\), the last-to-root move swaps \(a_0\) and \(a_{n-1}\) and then deletes the last entry, producing an array \(b = (b_0, \dots, b_{n-2})\) of length \(n - 1\): when \(n \ge 2\), \(b_0 = a_{n-1}\) and \(b_i = a_i\) for \(0 < i < n - 1\), and \(b\) is empty when \(n = 1\).

def daryMoveLastToRoot {α : Type u} (a : Array α) (hne : 0 < a.size) :
    Array α :=
  (a.swap 0 (a.size - 1) hne (by omega)).pop

Used by 5

Used byLast-to-root move in a \(d\)-ary heap removes one copy of the root · Last-to-root move in a \(d\)-ary heap is ready for sift-down · Extracted minimum and remaining d-ary heap recover the original elements · Removing the root of a \(d\)-ary min-heap · Removing the root of a \(d\)-ary heap preserves its arity

TheoremLast-to-root move in a \(d\)-ary heap is ready for sift-down#✓fully proved

Let \(d\) be a natural number, let \(a\) be a \(d\)-ary heap ordered array with at least two entries over a linearly ordered type, and let \(b = (b_0, \dots, b_{m-1})\) be the array obtained from \(a\) by the last-to-root move. Then \(b\) is ready for a \(d\)-ary sift-down at index \(0\): \(d \ge 2\), \(0 < m\), and \(b_{\lfloor (j-1)/d \rfloor} \le b_j\) for every index \(j\) with \(0 < j < m\) whose parent index \(\lfloor (j-1)/d \rfloor\) is not \(0\).

theorem daryMoveLastToRoot_siftDownReady {α : Type u} [LinearOrder α]
    (d : Nat) (a : Array α) (h : DaryHeapOrdered d a) (htwo : 1 < a.size) :
    DarySiftDownReady d (daryMoveLastToRoot a (by omega)) 0

Uses 6 · Used by 3

Statement uses\(d\)-ary heap order · Readiness for \(d\)-ary sift-down · Last-to-root move on an array

Proof usesParent index in a \(d\)-ary tree · A \(d\)-ary parent has a smaller index · The \(d\)-ary parent of a valid index is valid

Used byExtracted minimum and remaining d-ary heap recover the original elements · Removing the root of a \(d\)-ary min-heap · Removing the root of a \(d\)-ary heap preserves its arity

TheoremLast-to-root move in a \(d\)-ary heap removes one copy of the root#✓fully proved

For every nonempty array \(a = (a_0, \dots, a_{n-1})\) over a linearly ordered type, the multiset of entries of the array obtained from \(a\) by the last-to-root move equals the multiset of entries of \(a\) with one occurrence of \(a_0\) removed.

theorem daryMoveLastToRoot_elements {α : Type u} [LinearOrder α]
    (a : Array α) (hne : 0 < a.size) :
    (↑(daryMoveLastToRoot a hne).toList : Multiset α) =
      (↑a.toList : Multiset α).erase (a[0]'hne)

Uses 1

Statement usesLast-to-root move on an array

Structure\(d\)-ary min-heap#✓fully proved

A \(d\)-ary min-heap over a linearly ordered type \(\alpha\) consists of a natural number \(d \ge 2\), its arity, and an array \(a = (a_0, \dots, a_{n-1})\) of elements of \(\alpha\), stored in level order, that is \(d\)-ary heap ordered: \(a_{\lfloor (i-1)/d \rfloor} \le a_i\) for every index \(i\) with \(0 < i < n\).

structure DaryMinHeap (α : Type u) [LinearOrder α] where
  /-- The normalized arity, always at least two. -/
  arity : Nat
  arity_valid : 2 ≤ arity
  /-- The level-order storage array. -/
  data : Array α
  ordered : DaryHeapOrdered arity data

Uses 1 · Used by 26

Statement uses\(d\)-ary heap order

Used byArity of a \(d\)-ary heap built from a list · Size of a \(d\)-ary min-heap · Insertion into a \(d\)-ary heap preserves other multiplicities · Insertion into a \(d\)-ary heap raises the multiplicity by one · Elements of a d-ary heap · Building a heap from a list keeps its elements · Insertion into a d-ary heap adds one occurrence · Empty d-ary heap · Extracting the minimum of a \(d\)-ary min-heap · Extracting the minimum preserves the arity of a d-ary heap · Extracted minimum and remaining d-ary heap recover the original elements · Extracting the minimum of a d-ary heap lowers its multiplicity by one · Extracting the minimum of a d-ary heap removes one occurrence · Extracting the minimum of a d-ary heap fails exactly on the empty heap · The extracted minimum of a d-ary heap is a lower bound · The extracted minimum of a d-ary heap is one of its elements · Extracting the minimum leaves a heap-ordered \(d\)-ary heap · Removing the root of a \(d\)-ary min-heap · Removing the root of a \(d\)-ary heap preserves its arity · Minimum query on a \(d\)-ary min-heap · The minimum query on a \(d\)-ary heap fails exactly when it is empty · The minimum query on a \(d\)-ary heap returns a least element · The minimum query on a \(d\)-ary heap returns an element of the heap · Building a \(d\)-ary min-heap from a list · Insertion into a \(d\)-ary heap · Insertion keeps a \(d\)-ary heap ordered

DefinitionElements of a d-ary heap#✓fully proved

The multiset of elements of a \(d\)-ary min-heap \(h\) over a linearly ordered type is the multiset of the entries of its level-order storage array, counted with multiplicity.

def DaryMinHeap.elements {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) : Multiset α := h.data.toList

Uses 1 · Used by 12

Statement uses\(d\)-ary min-heap

Used bySize of a \(d\)-ary min-heap · Insertion into a \(d\)-ary heap preserves other multiplicities · Insertion into a \(d\)-ary heap raises the multiplicity by one · Building a heap from a list keeps its elements · Insertion into a d-ary heap adds one occurrence · Extracted minimum and remaining d-ary heap recover the original elements · Extracting the minimum of a d-ary heap lowers its multiplicity by one · Extracting the minimum of a d-ary heap removes one occurrence · The extracted minimum of a d-ary heap is a lower bound · The extracted minimum of a d-ary heap is one of its elements · The minimum query on a \(d\)-ary heap returns a least element · The minimum query on a \(d\)-ary heap returns an element of the heap

DefinitionEmpty d-ary heap#✓fully proved

For a natural number \(r\) (the requested arity), the empty heap is the \(d\)-ary min-heap over a linearly ordered type with arity \(d = \max(2, r)\) and an empty storage array; a requested arity below two is thus normalized to two.

def DaryMinHeap.empty {α : Type u} [LinearOrder α]
    (requestedArity : Nat) : DaryMinHeap α where
  arity := normalizedArity requestedArity
  arity_valid := normalizedArity_valid requestedArity
  data := #[]
  ordered := {
    arity_valid := normalizedArity_valid requestedArity
    parent_le := by simp
  }

Uses 6 · Used by 1

Statement uses\(d\)-ary heap order · \(d\)-ary min-heap · Parent index in a \(d\)-ary tree · The \(d\)-ary parent of a valid index is valid · Normalized heap arity · Normalized arities are at least two

Used byBuilding a \(d\)-ary min-heap from a list

DefinitionInsertion into a \(d\)-ary heap#✓fully proved

Inserting a value \(x\) into a \(d\)-ary min-heap \(h\) of arity \(d\) gives the heap of the same arity \(d\) whose array is obtained by appending \(x\) at the end of the level-order array of \(h\) and sifting it up from that last index: while the current index \(i > 0\) holds an entry strictly smaller than the entry at its parent index \(\lfloor (i-1)/d \rfloor\), the two entries are swapped and the process continues from the parent. Only the ancestor path of the new entry is changed.

def DaryMinHeap.push {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) (x : α) : DaryMinHeap α where
  arity := h.arity
  arity_valid := h.arity_valid
  data := darySiftUp (h.data.push x) h.data.size h.arity h.arity_valid
  ordered := darySiftUp_ordered h.arity _ _
    (daryPush_siftUpReady h.arity h.arity_valid h.data h.ordered x)

Uses 6 · Used by 6

Statement uses\(d\)-ary heap order · \(d\)-ary min-heap · Arrays ready for \(d\)-ary sift-up · Pushing onto a \(d\)-ary heap leaves it ready for sifting up · \(d\)-ary sift-up · Sift-up restores \(d\)-ary heap order

Used byInsertion into a \(d\)-ary heap preserves other multiplicities · Insertion into a \(d\)-ary heap raises the multiplicity by one · Building a heap from a list keeps its elements · Insertion into a d-ary heap adds one occurrence · Building a \(d\)-ary min-heap from a list · Insertion keeps a \(d\)-ary heap ordered

DefinitionMinimum query on a \(d\)-ary min-heap#✓fully proved

The minimum query on a \(d\)-ary min-heap \(h\) returns the entry at index \(0\) (the root) of the storage array of \(h\), or nothing if the array is empty.

def DaryMinHeap.min? {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) : Option α := h.data[0]?

Uses 1 · Used by 3

Statement uses\(d\)-ary min-heap

Used byThe minimum query on a \(d\)-ary heap fails exactly when it is empty · The minimum query on a \(d\)-ary heap returns a least element · The minimum query on a \(d\)-ary heap returns an element of the heap

TheoremThe minimum query on a \(d\)-ary heap fails exactly when it is empty#✓fully proved

For a \(d\)-ary min-heap \(h\), the minimum query on \(h\) (which returns the entry at index \(0\) of the storage array, if any) returns nothing if and only if the storage array of \(h\) is empty.

theorem DaryMinHeap.min?_eq_none_iff {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) : h.min? = none ↔ h.data.size = 0

Uses 2

Statement uses\(d\)-ary min-heap · Minimum query on a \(d\)-ary min-heap

TheoremThe minimum query on a \(d\)-ary heap returns an element of the heap#✓fully proved

Let \(h\) be a \(d\)-ary min-heap. If the minimum query on \(h\) returns \(x\), then \(x\) belongs to the multiset of elements of \(h\).

theorem DaryMinHeap.min?_mem {α : Type u} [LinearOrder α]
    {h : DaryMinHeap α} {x : α} (hx : h.min? = some x) : x ∈ h.elements

Uses 3

Statement uses\(d\)-ary min-heap · Elements of a d-ary heap · Minimum query on a \(d\)-ary min-heap

TheoremThe minimum query on a \(d\)-ary heap returns a least element#✓fully proved

Let \(h\) be a \(d\)-ary min-heap. If the minimum query on \(h\) returns \(x\), then \(x \le y\) for every element \(y\) of the multiset of elements of \(h\).

theorem DaryMinHeap.min?_le {α : Type u} [LinearOrder α]
    {h : DaryMinHeap α} {x y : α} (hx : h.min? = some x) (hy : y ∈ h.elements) :
    x ≤ y

Uses 5

Statement uses\(d\)-ary min-heap · Elements of a d-ary heap · Minimum query on a \(d\)-ary min-heap

Proof uses\(d\)-ary heap order · The root of a \(d\)-ary heap-ordered array is a minimum

TheoremInsertion into a d-ary heap adds one occurrence#✓fully proved

For a \(d\)-ary min-heap \(h\) over a linearly ordered type and a value \(x\), the multiset of elements of the heap obtained by inserting \(x\) into \(h\) is the multiset of elements of \(h\) with one more occurrence of \(x\).

theorem DaryMinHeap.elements_push {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) (x : α) :
    (h.push x).elements = x ::ₘ h.elements

Uses 5 · Used by 3

Statement uses\(d\)-ary min-heap · Elements of a d-ary heap · Insertion into a \(d\)-ary heap

Proof uses\(d\)-ary sift-up · Sifting up permutes the array

Used byInsertion into a \(d\)-ary heap preserves other multiplicities · Insertion into a \(d\)-ary heap raises the multiplicity by one · Building a heap from a list keeps its elements

TheoremInsertion keeps a \(d\)-ary heap ordered#✓fully proved

Let \(h\) be a \(d\)-ary min-heap of arity \(d\) and let \(x\) be a value. Then the level-order array of the heap obtained by inserting \(x\) into \(h\) is \(d\)-ary heap-ordered for the same arity \(d\).

theorem DaryMinHeap.push_ordered {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) (x : α) :
    DaryHeapOrdered h.arity (h.push x).data

Uses 3

Statement uses\(d\)-ary heap order · \(d\)-ary min-heap · Insertion into a \(d\)-ary heap

TheoremInsertion into a \(d\)-ary heap raises the multiplicity by one#✓fully proved

For every \(d\)-ary min-heap \(h\) over a linearly ordered type and every value \(x\), the multiplicity of \(x\) among the elements of the heap obtained by inserting \(x\) into \(h\) is one more than its multiplicity among the elements of \(h\).

theorem DaryMinHeap.count_push_self {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) (x : α) :
    Multiset.count x (h.push x).elements = Multiset.count x h.elements + 1

Uses 4

Statement uses\(d\)-ary min-heap · Elements of a d-ary heap · Insertion into a \(d\)-ary heap

Proof usesInsertion into a d-ary heap adds one occurrence

TheoremInsertion into a \(d\)-ary heap preserves other multiplicities#✓fully proved

For every \(d\)-ary min-heap \(h\) over a linearly ordered type and all values \(x \ne y\), the multiplicity of \(y\) among the elements of the heap obtained by inserting \(x\) into \(h\) equals the multiplicity of \(y\) among the elements of \(h\).

theorem DaryMinHeap.count_push_of_ne {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) {x y : α} (hyx : y ≠ x) :
    Multiset.count y (h.push x).elements = Multiset.count y h.elements

Uses 4

Statement uses\(d\)-ary min-heap · Elements of a d-ary heap · Insertion into a \(d\)-ary heap

Proof usesInsertion into a d-ary heap adds one occurrence

DefinitionRemoving the root of a \(d\)-ary min-heap#✓fully proved

Let \(h\) be a \(d\)-ary min-heap whose storage array \(a\) is nonempty. Removing the root of \(h\) gives the heap of arity \(d\) whose storage array is empty if \(a\) has one entry. Otherwise the last entry of \(a\) replaces the root, the last position is dropped, and the new root is repeatedly swapped with its smallest \(d\)-ary child while that child is smaller.

def DaryMinHeap.extractTail {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) (hne : 0 < h.data.size) : DaryMinHeap α :=
  if hone : h.data.size = 1 then
    ⟨h.arity, h.arity_valid, #[], {
      arity_valid := h.arity_valid
      parent_le := by simp
    }⟩
  else
    have htwo : 1 < h.data.size := by omega
    let moved := daryMoveLastToRoot h.data hne
    ⟨h.arity, h.arity_valid, darySiftDown moved 0 h.arity h.arity_valid,
      darySiftDown_ordered h.arity moved 0 h.arity_valid
        (daryMoveLastToRoot_siftDownReady h.arity h.data h.ordered htwo)⟩

Uses 8 · Used by 6

Statement uses\(d\)-ary heap order · \(d\)-ary min-heap · Last-to-root move on an array · Last-to-root move in a \(d\)-ary heap is ready for sift-down · Parent index in a \(d\)-ary tree · The \(d\)-ary parent of a valid index is valid · \(d\)-ary sift-down · Sifting down restores \(d\)-ary heap order

Used byExtracting the minimum of a \(d\)-ary min-heap · Extracting the minimum preserves the arity of a d-ary heap · Extracted minimum and remaining d-ary heap recover the original elements · Extracting the minimum of a d-ary heap fails exactly on the empty heap · The extracted minimum of a d-ary heap is a lower bound · Removing the root of a \(d\)-ary heap preserves its arity

TheoremRemoving the root of a \(d\)-ary heap preserves its arity#✓fully proved

For a \(d\)-ary min-heap \(h\) with nonempty storage array, the heap obtained from \(h\) by removing its root has the same arity \(d\) as \(h\).

theorem DaryMinHeap.extractTail_arity {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) (hne : 0 < h.data.size) :
    (h.extractTail hne).arity = h.arity

Uses 9 · Used by 1

Statement uses\(d\)-ary min-heap · Removing the root of a \(d\)-ary min-heap

Proof uses\(d\)-ary heap order · Last-to-root move on an array · Last-to-root move in a \(d\)-ary heap is ready for sift-down · Parent index in a \(d\)-ary tree · The \(d\)-ary parent of a valid index is valid · \(d\)-ary sift-down · Sifting down restores \(d\)-ary heap order

Used byExtracting the minimum preserves the arity of a d-ary heap

DefinitionBuilding a \(d\)-ary min-heap from a list#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(r \in \mathbb{N}\) be a requested arity, and let \(d = \max(2, r)\). The min-heap built from the empty list is the empty min-heap of arity \(d\), and the min-heap built from a list with head \(x\) and tail \(xs\) of elements of \(\alpha\) is obtained by inserting \(x\) into the min-heap built from \(xs\). Thus the min-heap built from \([x_1, \dots, x_n]\) starts from the empty min-heap of arity \(d\) and inserts \(x_n\), then \(x_{n-1}\), and so on, ending with \(x_1\), each by \(d\)-ary insertion.

def DaryMinHeap.ofList {α : Type u} [LinearOrder α]
    (requestedArity : Nat) : List α → DaryMinHeap α
  | [] => DaryMinHeap.empty requestedArity
  | x :: xs => (DaryMinHeap.ofList requestedArity xs).push x

Uses 3 · Used by 2

Statement uses\(d\)-ary min-heap · Empty d-ary heap · Insertion into a \(d\)-ary heap

Used byArity of a \(d\)-ary heap built from a list · Building a heap from a list keeps its elements

TheoremBuilding a heap from a list keeps its elements#✓fully proved

For every requested arity \(r\) and every list \(xs\) over a linearly ordered type, the multiset of elements of the min-heap of arity \(\max(2, r)\) built from \(xs\) by successive insertions equals the multiset of entries of \(xs\).

theorem DaryMinHeap.elements_ofList {α : Type u} [LinearOrder α]
    (requestedArity : Nat) (xs : List α) :
    (DaryMinHeap.ofList requestedArity xs).elements = (↑xs : Multiset α)

Uses 5

Statement usesElements of a d-ary heap · Building a \(d\)-ary min-heap from a list

Proof uses\(d\)-ary min-heap · Insertion into a d-ary heap adds one occurrence · Insertion into a \(d\)-ary heap

TheoremArity of a \(d\)-ary heap built from a list#✓fully proved

For every requested arity \(r \in \mathbb{N}\) and every list \(xs\) over a linearly ordered type, the \(d\)-ary min-heap built from \(xs\) with requested arity \(r\) has arity equal to the normalized arity of \(r\), namely \(\max(2, r)\).

theorem DaryMinHeap.arity_ofList {α : Type u} [LinearOrder α]
    (requestedArity : Nat) (xs : List α) :
    (DaryMinHeap.ofList requestedArity xs).arity = normalizedArity requestedArity

Uses 3

Statement uses\(d\)-ary min-heap · Building a \(d\)-ary min-heap from a list · Normalized heap arity

DefinitionExtracting the minimum of a \(d\)-ary min-heap#✓fully proved

For a \(d\)-ary min-heap \(h\), extracting the minimum returns nothing if the storage array of \(h\) is empty. Otherwise it returns the root entry (the entry at index \(0\)) together with the heap obtained from \(h\) by removing its root: the last entry moves to the root and sifts down along a single \(d\)-ary child path.

def DaryMinHeap.extractMin {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) : Option (α × DaryMinHeap α) :=
  if hne : 0 < h.data.size then
    some (h.data[0]'hne, h.extractTail hne)
  else
    none

Uses 2 · Used by 8

Statement uses\(d\)-ary min-heap · Removing the root of a \(d\)-ary min-heap

Used byExtracting the minimum preserves the arity of a d-ary heap · Extracted minimum and remaining d-ary heap recover the original elements · Extracting the minimum of a d-ary heap lowers its multiplicity by one · Extracting the minimum of a d-ary heap removes one occurrence · Extracting the minimum of a d-ary heap fails exactly on the empty heap · The extracted minimum of a d-ary heap is a lower bound · The extracted minimum of a d-ary heap is one of its elements · Extracting the minimum leaves a heap-ordered \(d\)-ary heap

TheoremExtracting the minimum of a d-ary heap fails exactly on the empty heap#✓fully proved

For a \(d\)-ary min-heap \(h\) over a linearly ordered type, extracting the minimum from \(h\) returns no result if and only if the storage array of \(h\) is empty.

theorem DaryMinHeap.extractMin_eq_none_iff {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) : h.extractMin = none ↔ h.data.size = 0

Uses 3

Statement uses\(d\)-ary min-heap · Extracting the minimum of a \(d\)-ary min-heap

Proof usesRemoving the root of a \(d\)-ary min-heap

TheoremExtracted minimum and remaining d-ary heap recover the original elements#✓fully proved

Let \(h\) be a \(d\)-ary min-heap over a linearly ordered type. If extracting the minimum from \(h\) succeeds, returning a value \(x\) and a heap \(h'\), then the multiset of elements of \(h\) is the multiset of elements of \(h'\) with one more occurrence of \(x\).

theorem DaryMinHeap.extractMin_cons_elements {α : Type u} [LinearOrder α]
    {h : DaryMinHeap α} {x : α} {rest : DaryMinHeap α}
    (hx : h.extractMin = some (x, rest)) :
    x ::ₘ rest.elements = h.elements

Uses 12 · Used by 3

Statement uses\(d\)-ary min-heap · Elements of a d-ary heap · Extracting the minimum of a \(d\)-ary min-heap

Proof uses\(d\)-ary heap order · Removing the root of a \(d\)-ary min-heap · Last-to-root move on an array · Last-to-root move in a \(d\)-ary heap is ready for sift-down · Parent index in a \(d\)-ary tree · The \(d\)-ary parent of a valid index is valid · \(d\)-ary sift-down · Sifting down restores \(d\)-ary heap order · Sifting down in a \(d\)-ary heap permutes the array

Used byExtracting the minimum of a d-ary heap lowers its multiplicity by one · Extracting the minimum of a d-ary heap removes one occurrence · The extracted minimum of a d-ary heap is one of its elements

TheoremExtracting the minimum of a d-ary heap removes one occurrence#✓fully proved

Let \(h\) be a \(d\)-ary min-heap over a linearly ordered type. If extracting the minimum from \(h\) succeeds, returning a value \(x\) and a heap \(h'\), then the multiset of elements of \(h'\) is obtained from the multiset of elements of \(h\) by removing one occurrence of \(x\).

theorem DaryMinHeap.extractMin_elements {α : Type u} [LinearOrder α]
    {h : DaryMinHeap α} {x : α} {rest : DaryMinHeap α}
    (hx : h.extractMin = some (x, rest)) :
    rest.elements = h.elements.erase x

Uses 4

Statement uses\(d\)-ary min-heap · Elements of a d-ary heap · Extracting the minimum of a \(d\)-ary min-heap

Proof usesExtracted minimum and remaining d-ary heap recover the original elements

TheoremExtracting the minimum of a d-ary heap lowers its multiplicity by one#✓fully proved

Let \(h\) be a \(d\)-ary min-heap over a linearly ordered type. If extracting the minimum from \(h\) succeeds, returning a value \(x\) and a heap \(h'\), then the multiplicity of \(x\) in the multiset of elements of \(h'\) is its multiplicity in the multiset of elements of \(h\) minus one.

theorem DaryMinHeap.extractMin_count {α : Type u} [LinearOrder α]
    {h : DaryMinHeap α} {x : α} {rest : DaryMinHeap α}
    (hx : h.extractMin = some (x, rest)) :
    Multiset.count x rest.elements = Multiset.count x h.elements - 1

Uses 4

Statement uses\(d\)-ary min-heap · Elements of a d-ary heap · Extracting the minimum of a \(d\)-ary min-heap

Proof usesExtracted minimum and remaining d-ary heap recover the original elements

TheoremThe extracted minimum of a d-ary heap is one of its elements#✓fully proved

Let \(h\) be a \(d\)-ary min-heap over a linearly ordered type. If extracting the minimum from \(h\) succeeds, returning a value \(x\) and a heap \(h'\), then \(x\) belongs to the multiset of elements of \(h\).

theorem DaryMinHeap.extractMin_mem {α : Type u} [LinearOrder α]
    {h : DaryMinHeap α} {x : α} {rest : DaryMinHeap α}
    (hx : h.extractMin = some (x, rest)) : x ∈ h.elements

Uses 4

Statement uses\(d\)-ary min-heap · Elements of a d-ary heap · Extracting the minimum of a \(d\)-ary min-heap

Proof usesExtracted minimum and remaining d-ary heap recover the original elements

TheoremThe extracted minimum of a d-ary heap is a lower bound#✓fully proved

Let \(h\) be a \(d\)-ary min-heap over a linearly ordered type. If extracting the minimum from \(h\) succeeds, returning a value \(x\) and a heap \(h'\), then \(x \le y\) for every element \(y\) of the multiset of elements of \(h\).

theorem DaryMinHeap.extractMin_le {α : Type u} [LinearOrder α]
    {h : DaryMinHeap α} {x y : α} {rest : DaryMinHeap α}
    (hx : h.extractMin = some (x, rest)) (hy : y ∈ h.elements) : x ≤ y

Uses 6

Statement uses\(d\)-ary min-heap · Elements of a d-ary heap · Extracting the minimum of a \(d\)-ary min-heap

Proof uses\(d\)-ary heap order · The root of a \(d\)-ary heap-ordered array is a minimum · Removing the root of a \(d\)-ary min-heap

TheoremExtracting the minimum preserves the arity of a d-ary heap#✓fully proved

Let \(h\) be a \(d\)-ary min-heap over a linearly ordered type. If extracting the minimum from \(h\) succeeds, returning a value \(x\) and a heap \(h'\), then \(h'\) has the same arity as \(h\).

theorem DaryMinHeap.extractMin_arity {α : Type u} [LinearOrder α]
    {h : DaryMinHeap α} {x : α} {rest : DaryMinHeap α}
    (hx : h.extractMin = some (x, rest)) : rest.arity = h.arity

Uses 4

Statement uses\(d\)-ary min-heap · Extracting the minimum of a \(d\)-ary min-heap

Proof usesRemoving the root of a \(d\)-ary min-heap · Removing the root of a \(d\)-ary heap preserves its arity

TheoremExtracting the minimum leaves a heap-ordered \(d\)-ary heap#✓fully proved

Let \(h\) be a \(d\)-ary min-heap. If extracting the minimum of \(h\) returns a value \(x\) and a heap \(h'\) of arity \(d'\), then \(d' \ge 2\) and the storage array \(a\) of \(h'\) is heap-ordered: for every index \(i\) with \(0 < i < |a|\), the entry \(a_{\lfloor (i-1)/d' \rfloor}\) is at most \(a_i\).

theorem DaryMinHeap.extractMin_ordered {α : Type u} [LinearOrder α]
    {h : DaryMinHeap α} {x : α} {rest : DaryMinHeap α}
    (_hx : h.extractMin = some (x, rest)) :
    DaryHeapOrdered rest.arity rest.data

Uses 3

Statement uses\(d\)-ary heap order · \(d\)-ary min-heap · Extracting the minimum of a \(d\)-ary min-heap

TheoremSize of a \(d\)-ary min-heap#✓fully proved

For every \(d\)-ary min-heap \(h\) over a linearly ordered type, the number of elements of \(h\), counted with multiplicity, equals the length of its backing array.

theorem DaryMinHeap.card_elements {α : Type u} [LinearOrder α]
    (h : DaryMinHeap α) : h.elements.card = h.data.size

Uses 2

Statement uses\(d\)-ary min-heap · Elements of a d-ary heap

55 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.