Skip to content

Binomial heap

53 fully proved

Binomial Tree

InductiveBinomial tree#✓fully proved

A binomial tree over a type \(\alpha\) is a node that stores a rank, which is a natural number, a root value in \(\alpha\), and a list of binomial trees over \(\alpha\) as its children. The type imposes no invariant; the binomial-tree shape and heap order are expressed by a separate validity predicate.

public inductive BinomialTree (α : Type u) where
  | node (rank : Nat) (root : α) (children : List (BinomialTree α))
deriving Repr
Used by 51
Used byBinomial heap · Size of a valid binomial tree · Carry insertion into a binomial forest · Children of a valid binomial tree are valid · Children of a binomial tree · Child ranks of a valid binomial tree · Deleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Minimum deletion on a binomial forest · Binomial heap deletion agrees with forest deletion · Elements of a binomial tree · Elements of a binomial forest · Elements of a binomial heap · Insertion into a binomial heap adds one occurrence · Linking binomial trees adds their elements · Melding binomial heaps adds their elements · Melding binomial forests adds their elements · Empty binomial heap · Minimum of a binomial heap · The minimum lookup fails exactly on the empty binomial heap · The minimum lookup of a binomial heap returns a lower bound · The minimum lookup of a binomial heap returns one of its elements · A valid binomial forest with no elements has no trees · A valid binomial forest has logarithmically many trees · A binomial heap has logarithmically many trees · Linking two binomial trees · Linking preserves binomial-tree validity · Melding binomial heaps · Melding binomial forests · Melding preserves forest validity and rank lower bounds · Tree ranks in a valid forest are logarithmic · Rank of a binomial tree · The rank of a valid binomial tree is logarithmic · Tree ranks in a binomial heap are logarithmic · Rank lower bound for a forest · Removing a minimum-root tree from a forest · Removing a minimum-root tree · Root of a binomial tree · The root of a valid binomial tree is a lower bound · The root of a binomial tree is one of its elements · Singleton binomial heap · One-element binomial heap · Validity of binomial forests passes to sublists · Valid binomial tree · Valid binomial forest · The empty forest is valid · Reversed children of a valid binomial tree form a valid forest · Singleton binomial trees are valid

DefinitionRank of a binomial tree#✓fully proved

The rank of a binomial tree is the natural number stored at its root node.

@[expose] public def rank {α : Type u} : BinomialTree α → Nat
  | .node rank _ _ => rank
Uses 1 · Used by 32
Statement usesBinomial tree
Used bySize of a valid binomial tree · Carry insertion into a binomial forest · Children of a valid binomial tree are valid · Child ranks of a valid binomial tree · Deleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion · Linking binomial trees adds their elements · Melding binomial forests adds their elements · The minimum lookup of a binomial heap returns a lower bound · A valid binomial forest with no elements has no trees · A valid binomial forest has logarithmically many trees · Linking two binomial trees · Linking preserves binomial-tree validity · Melding binomial heaps · Melding binomial forests · Melding preserves forest validity and rank lower bounds · Tree ranks in a valid forest are logarithmic · The rank of a valid binomial tree is logarithmic · Tree ranks in a binomial heap are logarithmic · Rank lower bound for a forest · The root of a valid binomial tree is a lower bound · One-element binomial heap · Validity of binomial forests passes to sublists · Valid binomial tree · Valid binomial forest · The empty forest is valid · Reversed children of a valid binomial tree form a valid forest · Singleton binomial trees are valid

DefinitionRoot of a binomial tree#✓fully proved

The root of the binomial tree with rank \(r\), root value \(a\) and list of children \(c\) is \(a\).

@[expose] public def root {α : Type u} : BinomialTree α → α
  | .node _ root _ => root
Uses 1 · Used by 19
Statement usesBinomial tree
Used byDeleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Minimum deletion on a binomial forest · Binomial heap deletion agrees with forest deletion · Linking binomial trees adds their elements · Minimum of a binomial heap · The minimum lookup fails exactly on the empty binomial heap · The minimum lookup of a binomial heap returns a lower bound · The minimum lookup of a binomial heap returns one of its elements · Linking two binomial trees · Linking preserves binomial-tree validity · Melding preserves forest validity and rank lower bounds · Removing a minimum-root tree from a forest · Removing a minimum-root tree · The root of a valid binomial tree is a lower bound · The root of a binomial tree is one of its elements

DefinitionChildren of a binomial tree#✓fully proved

The children of a binomial tree are the binomial trees in the list stored at its root node, in their stored order.

The list carries no ordering constraint in general; in a valid binomial tree of rank \(r\) the children have ranks \(r - 1, \dots, 0\) in that order.

@[expose] public def children {α : Type u} : BinomialTree α → List (BinomialTree α)
  | .node _ _ children => children
Uses 1 · Used by 14
Statement usesBinomial tree
Used byChildren of a valid binomial tree are valid · Child ranks of a valid binomial tree · Deleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Minimum deletion on a binomial forest · Binomial heap deletion agrees with forest deletion · Linking binomial trees adds their elements · Linking two binomial trees · Linking preserves binomial-tree validity · Melding preserves forest validity and rank lower bounds · Reversed children of a valid binomial tree form a valid forest

DefinitionElements of a binomial tree#✓fully proved

The multiset of elements of a binomial tree with root value \(x\) and children \(t_1, \dots, t_k\) is defined recursively as \(\{x\}\) added to the multiset sum of the multisets of elements of \(t_1, \dots, t_k\); the stored rank plays no role.

@[expose] public def elements {α : Type u} : BinomialTree α → Multiset α
  | .node _ root children => root ::ₘ (children.map elements).sum
Uses 1 · Used by 24
Statement usesBinomial tree
Used bySize of a valid binomial tree · Children of a valid binomial tree are valid · Child ranks of a valid binomial tree · Deleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion · Elements of a binomial forest · Insertion into a binomial heap adds one occurrence · Linking binomial trees adds their elements · Melding binomial forests adds their elements · The minimum lookup of a binomial heap returns a lower bound · The minimum lookup of a binomial heap returns one of its elements · A valid binomial forest with no elements has no trees · Linking preserves binomial-tree validity · Tree ranks in a valid forest are logarithmic · The rank of a valid binomial tree is logarithmic · Removing a minimum-root tree · The root of a valid binomial tree is a lower bound · The root of a binomial tree is one of its elements · Valid binomial tree · Singleton binomial trees are valid

TheoremThe root of a binomial tree is one of its elements#✓fully proved

For every binomial tree \(t\), the root of \(t\) occurs in the multiset represented by \(t\).

public theorem root_mem_elements (tree : BinomialTree α) : tree.root ∈ tree.elements
Uses 3 · Used by 1
Statement usesBinomial tree · Elements of a binomial tree · Root of a binomial tree
Used byThe minimum lookup of a binomial heap returns one of its elements

InductiveValid binomial tree#✓fully proved

For a type \(\alpha\) with a relation \(\le\), validity of binomial trees over \(\alpha\) is defined inductively: the tree with stored rank \(r\), root \(a\) and list of children \(c_1, \dots, c_k\) is valid when every child \(c_i\) is valid, the ranks of \(c_1, \dots, c_k\) are exactly \(r - 1, r - 2, \dots, 0\) in this order, the multiset of elements of the tree (its root together with the elements of all its children) has exactly \(2^r\) members counted with multiplicity, and \(a \le x\) for every element \(x\) of the tree.

public inductive Valid {α : Type u} [LE α] : BinomialTree α → Prop
  | node {rank : Nat} {root : α} {children : List (BinomialTree α)}
      (children_valid : ∀ child ∈ children, Valid child)
      (children_ranks : children.map BinomialTree.rank = (List.range rank).reverse)
      (card_elements : (elements (.node rank root children)).card = 2 ^ rank)
      (root_le : ∀ value ∈ elements (.node rank root children), root ≤ value) :
      Valid (.node rank root children)
Uses 3 · Used by 23
Statement usesBinomial tree · Elements of a binomial tree · Rank of a binomial tree
Used bySize of a valid binomial tree · Children of a valid binomial tree are valid · Child ranks of a valid binomial tree · Deleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion · The minimum lookup of a binomial heap returns a lower bound · A valid binomial forest with no elements has no trees · A valid binomial forest has logarithmically many trees · Linking preserves binomial-tree validity · Melding preserves forest validity and rank lower bounds · Tree ranks in a valid forest are logarithmic · The rank of a valid binomial tree is logarithmic · The root of a valid binomial tree is a lower bound · One-element binomial heap · Validity of binomial forests passes to sublists · Valid binomial forest · The empty forest is valid · Reversed children of a valid binomial tree form a valid forest · Singleton binomial trees are valid

DefinitionSingleton binomial heap#✓fully proved

For a value \(a\) in a linear order, the binomial heap whose list of trees consists of exactly one tree: the tree of rank \(0\) with root \(a\) and no children.

@[expose] public def singleton (value : α) : BinomialTree α :=
  .node 0 value []
Uses 1 · Used by 3
Statement usesBinomial tree
Used byInsertion into a binomial heap adds one occurrence · One-element binomial heap · Singleton binomial trees are valid

Over a linear order, the link of binomial trees \(s\) and \(t\) is defined as follows. If the root of \(s\) is at most the root of \(t\), it is the tree whose rank is one more than the rank of \(s\), whose root is the root of \(s\), and whose children are \(t\) followed by the children of \(s\). Otherwise it is the tree whose rank is one more than the rank of \(s\), whose root is the root of \(t\), and whose children are \(s\) followed by the children of \(t\). In particular, the root of \(s\) is kept when the two roots are equal.

@[expose] public def link [LinearOrder α] (left right : BinomialTree α) : BinomialTree α :=
  if left.root ≤ right.root then
    .node (left.rank + 1) left.root (right :: left.children)
  else
    .node (left.rank + 1) right.root (left :: right.children)
Uses 4 · Used by 6
Statement usesBinomial tree · Children of a binomial tree · Rank of a binomial tree · Root of a binomial tree
Used byCarry insertion into a binomial forest · Linking binomial trees adds their elements · Melding binomial forests adds their elements · Linking preserves binomial-tree validity · Melding binomial forests · Melding preserves forest validity and rank lower bounds

For any two binomial trees \(s\) and \(t\) over a linearly ordered type, the multiset of elements of the tree obtained by linking \(s\) and \(t\) is the sum of the multisets of elements of \(s\) and \(t\).

public theorem elements_link [LinearOrder α] (left right : BinomialTree α) :
    (link left right).elements = left.elements + right.elements
Uses 6 · Used by 2
Statement usesBinomial tree · Elements of a binomial tree · Linking two binomial trees
Proof usesChildren of a binomial tree · Rank of a binomial tree · Root of a binomial tree
Used byMelding binomial forests adds their elements · Linking preserves binomial-tree validity

TheoremSingleton binomial trees are valid#✓fully proved

For a linearly ordered type \(\alpha\) and any \(a \in \alpha\), the singleton binomial tree with rank \(0\), root \(a\) and no children is valid.

public theorem valid_singleton [LinearOrder α] (value : α) : Valid (singleton value)
Uses 5 · Used by 1
Statement usesValid binomial tree · Singleton binomial heap
Proof usesBinomial tree · Elements of a binomial tree · Rank of a binomial tree
Used byOne-element binomial heap

TheoremChildren of a valid binomial tree are valid#✓fully proved

For a type \(\alpha\) with a relation \(\le\), every child of a valid binomial tree over \(\alpha\) is itself a valid binomial tree.

public theorem Valid.child_valid [LE α] {tree child : BinomialTree α}
    (valid : Valid tree) (member : child ∈ tree.children) : Valid child
Uses 5 · Used by 2
Statement usesBinomial tree · Valid binomial tree · Children of a binomial tree
Proof usesElements of a binomial tree · Rank of a binomial tree
Used byLinking preserves binomial-tree validity · Reversed children of a valid binomial tree form a valid forest

TheoremChild ranks of a valid binomial tree#✓fully proved

For a type \(\alpha\) with a relation \(\le\), if a valid binomial tree over \(\alpha\) has rank \(r\), then the ranks of its children, listed in their stored order, are \(r - 1, r - 2, \dots, 1, 0\); there are no children when \(r = 0\).

public theorem Valid.children_ranks [LE α] {tree : BinomialTree α} (valid : Valid tree) :
    tree.children.map BinomialTree.rank = (List.range tree.rank).reverse
Uses 5 · Used by 2
Statement usesBinomial tree · Valid binomial tree · Children of a binomial tree · Rank of a binomial tree
Proof usesElements of a binomial tree
Used byLinking preserves binomial-tree validity · Reversed children of a valid binomial tree form a valid forest

TheoremSize of a valid binomial tree#✓fully proved

For a type \(\alpha\) with a relation \(\le\), every valid binomial tree of rank \(r\) over \(\alpha\) represents a multiset of exactly \(2^r\) elements, counted with multiplicity.

public theorem Valid.card_elements [LE α] {tree : BinomialTree α} (valid : Valid tree) :
    tree.elements.card = 2 ^ tree.rank
Uses 4 · Used by 4
Statement usesBinomial tree · Valid binomial tree · Elements of a binomial tree · Rank of a binomial tree
Used byA valid binomial forest with no elements has no trees · Linking preserves binomial-tree validity · Tree ranks in a valid forest are logarithmic · The rank of a valid binomial tree is logarithmic

TheoremThe rank of a valid binomial tree is logarithmic#✓fully proved

A valid binomial tree of rank \(r\) holding \(n\) elements, counted with multiplicity, satisfies \(r \le \lfloor \log_2 n \rfloor\).

public theorem Valid.rank_le_log2_card [LE α] {tree : BinomialTree α} (valid : Valid tree) :
    tree.rank ≤ Nat.log2 tree.elements.card
Uses 5
Statement usesBinomial tree · Valid binomial tree · Elements of a binomial tree · Rank of a binomial tree
Proof usesSize of a valid binomial tree

TheoremThe root of a valid binomial tree is a lower bound#✓fully proved

For a type \(\alpha\) with a relation \(\le\) and a valid binomial tree \(t\) over \(\alpha\), the root \(a\) of \(t\) satisfies \(a \le v\) for every element \(v\) of the multiset represented by \(t\).

public theorem Valid.root_le [LE α] {tree : BinomialTree α} (valid : Valid tree)
    {value : α} (member : value ∈ tree.elements) : tree.root ≤ value
Uses 5 · Used by 3
Statement usesBinomial tree · Valid binomial tree · Elements of a binomial tree · Root of a binomial tree
Proof usesRank of a binomial tree
Used byThe value deleted from a binomial heap is a lower bound for its elements · The minimum lookup of a binomial heap returns a lower bound · Linking preserves binomial-tree validity

If \(s\) and \(t\) are valid binomial trees of equal rank, then the tree obtained by linking \(s\) with \(t\) is valid.

public theorem Valid.link [LinearOrder α] {left right : BinomialTree α}
    (left_valid : Valid left) (right_valid : Valid right)
    (ranks : left.rank = right.rank) : Valid (link left right)
Uses 12 · Used by 1
Statement usesBinomial tree · Valid binomial tree · Linking two binomial trees · Rank of a binomial tree
Proof usesSize of a valid binomial tree · Children of a valid binomial tree are valid · Child ranks of a valid binomial tree · The root of a valid binomial tree is a lower bound · Children of a binomial tree · Elements of a binomial tree · Linking binomial trees adds their elements · Root of a binomial tree
Used byMelding preserves forest validity and rank lower bounds

Binomial Forest

DefinitionValid binomial forest#✓fully proved

For a type \(\alpha\) with a relation \(\le\), a list of binomial trees over \(\alpha\) is a valid forest when every tree in it is a valid binomial tree and the ranks of its trees are strictly increasing along the list.

@[expose] public def BinomialForest.Valid {α : Type u} [LE α]
    (trees : List (BinomialTree α)) : Prop :=
  (∀ tree ∈ trees, tree.Valid) ∧
    (trees.map BinomialTree.rank).Pairwise (· < ·)
Uses 3 · Used by 20
Statement usesBinomial tree · Valid binomial tree · Rank of a binomial tree
Used byBinomial heap · Deleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion · Empty binomial heap · The minimum lookup of a binomial heap returns a lower bound · A valid binomial forest with no elements has no trees · A valid binomial forest has logarithmically many trees · A binomial heap has logarithmically many trees · Melding binomial heaps · Melding preserves forest validity and rank lower bounds · Tree ranks in a valid forest are logarithmic · Tree ranks in a binomial heap are logarithmic · One-element binomial heap · Validity of binomial forests passes to sublists · The empty forest is valid · Reversed children of a valid binomial tree form a valid forest

DefinitionElements of a binomial forest#✓fully proved

The multiset of elements of a list of binomial trees \(t_1, \dots, t_k\) is the multiset sum of the multisets of elements of \(t_1, \dots, t_k\); for the empty list it is the empty multiset.

@[expose] public def elements {α : Type u} (trees : List (BinomialTree α)) : Multiset α :=
  (trees.map BinomialTree.elements).sum
Uses 2 · Used by 14
Statement usesBinomial tree · Elements of a binomial tree
Used byDeleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion · Elements of a binomial heap · Melding binomial forests adds their elements · The minimum lookup of a binomial heap returns a lower bound · The minimum lookup of a binomial heap returns one of its elements · A valid binomial forest with no elements has no trees · A valid binomial forest has logarithmically many trees · Tree ranks in a valid forest are logarithmic · Removing a minimum-root tree

DefinitionRank lower bound for a forest#✓fully proved

For a natural number \(r\), a list of binomial trees has ranks at least \(r\) when every tree in it has rank at least \(r\).

public def RanksAtLeast {α : Type u} (rank : Nat)
    (trees : List (BinomialTree α)) : Prop :=
  ∀ tree ∈ trees, rank ≤ tree.rank
Uses 2 · Used by 8
Statement usesBinomial tree · Rank of a binomial tree
Used byDeleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion · Melding binomial heaps · Melding preserves forest validity and rank lower bounds

TheoremThe empty forest is valid#✓fully proved

For every type \(\alpha\) with a relation \(\le\), the empty list of binomial trees over \(\alpha\) is a valid binomial forest.

public theorem valid_nil [LE α] : Valid ([] : List (BinomialTree α))
Uses 4 · Used by 3
Statement usesValid binomial forest · Binomial tree
Proof usesValid binomial tree · Rank of a binomial tree
Used byEmpty binomial heap · Melding preserves forest validity and rank lower bounds · One-element binomial heap

TheoremValidity of binomial forests passes to sublists#✓fully proved

For a type \(\alpha\) with a relation \(\le\) and lists \(L\), \(R\) of binomial trees over \(\alpha\), if \(L\) is a sublist of \(R\) (obtained by deleting entries while keeping the order of the rest) and \(R\) is a valid forest, then \(L\) is a valid forest.

public theorem Valid.sublist [LE α] {left right : List (BinomialTree α)}
    (sublist : left.Sublist right) (valid : Valid right) : Valid left
Uses 4 · Used by 6
Statement usesValid binomial forest · Binomial tree
Proof usesValid binomial tree · Rank of a binomial tree
Used byDeleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion

TheoremTree ranks in a valid forest are logarithmic#✓fully proved

If \(F\) is a valid binomial forest and \(T\) is a tree of \(F\) of rank \(r\), then \(r \le \lfloor \log_2 n \rfloor\), where \(n\) is the number of elements, counted with multiplicity, represented by \(F\).

public theorem Valid.member_rank_le_log2_card [LE α] {trees : List (BinomialTree α)}
    {tree : BinomialTree α} (valid : Valid trees) (member : tree ∈ trees) :
    tree.rank ≤ Nat.log2 (elements trees).card
Uses 7 · Used by 2
Statement usesValid binomial forest · Elements of a binomial forest · Binomial tree · Rank of a binomial tree
Proof usesValid binomial tree · Size of a valid binomial tree · Elements of a binomial tree
Used byA valid binomial forest has logarithmically many trees · Tree ranks in a binomial heap are logarithmic

TheoremA valid binomial forest has logarithmically many trees#✓fully proved

Let \(\alpha\) be a type with a relation \(\le\). If a valid binomial forest over \(\alpha\) has \(n\) elements, counted with multiplicity, then it consists of at most \(\lfloor \log_2 n \rfloor + 1\) trees, where \(\lfloor \log_2 0 \rfloor\) is taken to be \(0\).

public theorem Valid.length_le_log2_card_succ [LE α] {trees : List (BinomialTree α)}
    (valid : Valid trees) : trees.length ≤ Nat.log2 (elements trees).card + 1
Uses 6 · Used by 1
Statement usesValid binomial forest · Elements of a binomial forest · Binomial tree
Proof usesTree ranks in a valid forest are logarithmic · Valid binomial tree · Rank of a binomial tree
Used byA binomial heap has logarithmically many trees

TheoremA valid binomial forest with no elements has no trees#✓fully proved

Let \(\alpha\) be a type with a relation \(\le\). If a list of binomial trees over \(\alpha\) is a valid binomial forest and its multiset of elements has cardinality \(0\), then the list has length \(0\).

public theorem Valid.length_eq_zero_of_card_eq_zero [LE α] {trees : List (BinomialTree α)}
    (valid : Valid trees) (empty : (elements trees).card = 0) : trees.length = 0
Uses 7
Statement usesValid binomial forest · Elements of a binomial forest · Binomial tree
Proof usesValid binomial tree · Size of a valid binomial tree · Elements of a binomial tree · Rank of a binomial tree

DefinitionCarry insertion into a binomial forest#✓fully proved

For a linearly ordered type, the carry of a binomial tree \(t\) into a list \(F\) of binomial trees is defined by recursion on \(F\). If \(F\) is empty, the result is the one-tree list \([t]\). If \(F\) starts with a tree \(u\) followed by a list \(F'\) and the rank of \(t\) is less than the rank of \(u\), the result is \(F\) with \(t\) prepended. Otherwise the result is the carry of the link of \(t\) and \(u\) into \(F'\).

It is meant for a tree whose rank is no greater than every rank in the forest, where linking equal-rank trees propagates like a binary carry.

@[expose] public def carry [LinearOrder α] (tree : BinomialTree α) :
    List (BinomialTree α) → List (BinomialTree α)
  | [] => [tree]
  | other :: trees =>
      if tree.rank < other.rank then
        tree :: other :: trees
      else
        carry (tree.link other) trees
Uses 3 · Used by 3
Statement usesBinomial tree · Linking two binomial trees · Rank of a binomial tree
Used byMelding binomial forests adds their elements · Melding binomial forests · Melding preserves forest validity and rank lower bounds

DefinitionMelding binomial forests#✓fully proved

Over a linear order, the meld of two lists of binomial trees is defined by recursion on their total length. For every list \(L\), the meld of the empty list with \(L\) is \(L\), and the meld of \(L\) with the empty list is \(L\). For nonempty lists with first trees \(s\) and \(t\) and remaining lists \(F\) and \(G\): if the rank of \(s\) is less than the rank of \(t\), the meld is \(s\) followed by the meld of \(F\) with the second list; if the rank of \(t\) is less than the rank of \(s\), it is \(t\) followed by the meld of the first list with \(G\); and if the ranks are equal, it is the result of carrying the link of \(s\) with \(t\) into the meld of \(F\) and \(G\).

It is intended for forests of strictly increasing ranks, where equal-rank trees are linked and the carries are propagated.

@[expose] public def meldTrees [LinearOrder α] :
    List (BinomialTree α) → List (BinomialTree α) → List (BinomialTree α)
  | [], right => right
  | left, [] => left
  | leftTree :: leftTrees, rightTree :: rightTrees =>
      if leftTree.rank < rightTree.rank then
        leftTree :: meldTrees leftTrees (rightTree :: rightTrees)
      else if rightTree.rank < leftTree.rank then
        rightTree :: meldTrees (leftTree :: leftTrees) rightTrees
      else
        carry (leftTree.link rightTree) (meldTrees leftTrees rightTrees)
termination_by left right => left.length + right.length
Uses 4 · Used by 10
Statement usesCarry insertion into a binomial forest · Binomial tree · Linking two binomial trees · Rank of a binomial tree
Used byDeleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Minimum deletion on a binomial forest · Binomial heap deletion agrees with forest deletion · Melding binomial forests adds their elements · Melding binomial heaps · Melding preserves forest validity and rank lower bounds

TheoremMelding binomial forests adds their elements#✓fully proved

For any two lists \(L\) and \(R\) of binomial trees over a linearly ordered type, the multiset of elements of the meld of \(L\) and \(R\) is the sum of the multisets of elements of \(L\) and \(R\).

theorem elements_meldTrees [LinearOrder α]
    (left right : List (BinomialTree α)) :
    elements (meldTrees left right) = elements left + elements right
Uses 8 · Used by 3
Statement usesElements of a binomial forest · Melding binomial forests · Binomial tree
Proof usesCarry insertion into a binomial forest · Elements of a binomial tree · Linking binomial trees adds their elements · Linking two binomial trees · Rank of a binomial tree
Used byDeleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Melding binomial heaps adds their elements

TheoremMelding preserves forest validity and rank lower bounds#✓fully proved

Let \(r\) be a natural number and let \(F\) and \(G\) be valid binomial forests in which every tree has rank at least \(r\). Then the meld of \(F\) and \(G\) is a valid binomial forest in which every tree has rank at least \(r\).

public theorem meldTrees_correct [LinearOrder α] {rank : Nat}
    {left right : List (BinomialTree α)} (left_valid : Valid left)
    (right_valid : Valid right) (left_lower : RanksAtLeast rank left)
    (right_lower : RanksAtLeast rank right) :
    Valid (meldTrees left right) ∧ RanksAtLeast rank (meldTrees left right)
Uses 12 · Used by 7
Statement usesRank lower bound for a forest · Valid binomial forest · Melding binomial forests · Binomial tree
Proof usesCarry insertion into a binomial forest · The empty forest is valid · Valid binomial tree · Linking preserves binomial-tree validity · Children of a binomial tree · Linking two binomial trees · Rank of a binomial tree · Root of a binomial tree
Used byDeleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion · Melding binomial heaps

DefinitionRemoving a minimum-root tree from a forest#✓fully proved

For a list \(T\) of binomial trees over a linear order, the result is nothing when \(T\) is empty. Otherwise it is the first tree \(m\) of \(T\) whose root is minimal among the roots of the trees of \(T\), together with the list obtained from \(T\) by deleting that occurrence of \(m\), the remaining trees keeping their order.

@[expose] public def removeMinTree [LinearOrder α] :
    List (BinomialTree α) → Option (BinomialTree α × List (BinomialTree α))
  | [] => none
  | tree :: trees =>
      match removeMinTree trees with
      | none => some (tree, [])
      | some (minimum, rest) =>
          if minimum.root < tree.root then
            some (minimum, tree :: rest)
          else
            some (tree, trees)
Uses 2 · Used by 12
Statement usesBinomial tree · Root of a binomial tree
Used byDeleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Minimum deletion on a binomial forest · Binomial heap deletion agrees with forest deletion · Minimum of a binomial heap · The minimum lookup fails exactly on the empty binomial heap · The minimum lookup of a binomial heap returns a lower bound · The minimum lookup of a binomial heap returns one of its elements · Removing a minimum-root tree

TheoremRemoving a minimum-root tree#✓fully proved

Let \(T\) be a list of binomial trees over a linear order, and suppose that removing a minimum tree from \(T\) returns the tree \(m\) and the list \(R\). Then the multiset represented by \(m\) plus the multiset represented by the forest \(R\) equals the multiset represented by the forest \(T\); \(m\) is a member of \(T\); \(R\) is a sublist of \(T\); and the root of \(m\) is at most the root of every tree in \(T\).

public theorem removeMinTree_spec [LinearOrder α]
    {trees : List (BinomialTree α)} {minimum : BinomialTree α}
    {rest : List (BinomialTree α)} (result : removeMinTree trees = some (minimum, rest)) :
    minimum.elements + elements rest = elements trees ∧
      minimum ∈ trees ∧ rest.Sublist trees ∧
      ∀ tree ∈ trees, minimum.root ≤ tree.root
Uses 5 · Used by 8
Statement usesElements of a binomial forest · Removing a minimum-root tree from a forest · Binomial tree · Elements of a binomial tree · Root of a binomial tree
Used byDeleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion · The minimum lookup of a binomial heap returns a lower bound · The minimum lookup of a binomial heap returns one of its elements

TheoremReversed children of a valid binomial tree form a valid forest#✓fully proved

For a linearly ordered type \(\alpha\) and a valid binomial tree \(t\) over \(\alpha\), the children of \(t\) listed in reverse order form a valid binomial forest: every tree in the list is valid and the ranks strictly increase along the list.

public theorem valid_reverse_children [LinearOrder α] {tree : BinomialTree α}
    (valid : tree.Valid) : Valid tree.children.reverse
Uses 7 · Used by 6
Statement usesValid binomial forest · Binomial tree · Valid binomial tree · Children of a binomial tree
Proof usesChildren of a valid binomial tree are valid · Child ranks of a valid binomial tree · Rank of a binomial tree
Used byDeleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion

Binomial Heap

StructureBinomial heap#✓fully proved

A binomial min-heap over a linearly ordered type \(\alpha\) consists of a list of binomial trees over \(\alpha\) together with a proof that this list is a valid binomial forest: every tree in it is a valid binomial tree and the tree ranks are strictly increasing along the list.

public structure BinomialHeap (α : Type u) [LinearOrder α] where
  /-- The binomial trees, in strictly increasing rank order. -/
  trees : List (BinomialTree α)
  valid : BinomialForest.Valid trees
Uses 2 · Used by 19
Statement usesValid binomial forest · Binomial tree
Used byDeleting the minimum of a binomial heap · Deleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion · Elements of a binomial heap · Insertion into a binomial heap adds one occurrence · Melding binomial heaps adds their elements · Empty binomial heap · Minimum of a binomial heap · The minimum lookup fails exactly on the empty binomial heap · The minimum lookup of a binomial heap returns a lower bound · The minimum lookup of a binomial heap returns one of its elements · Insertion into a binomial heap · A binomial heap has logarithmically many trees · Melding binomial heaps · Tree ranks in a binomial heap are logarithmic · One-element binomial heap

DefinitionElements of a binomial heap#✓fully proved

Over a linearly ordered type, the multiset of elements of a binomial heap is the multiset of elements of its list of binomial trees, that is, the multiset sum of the multisets of elements of its trees.

@[expose] public def elements [LinearOrder α] (heap : BinomialHeap α) : Multiset α :=
  BinomialForest.elements heap.trees
Uses 3 · Used by 9
Statement usesElements of a binomial forest · Binomial heap · Binomial tree
Used byDeleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · The value deleted from a binomial heap is a lower bound for its elements · Insertion into a binomial heap adds one occurrence · Melding binomial heaps adds their elements · The minimum lookup of a binomial heap returns a lower bound · The minimum lookup of a binomial heap returns one of its elements · A binomial heap has logarithmically many trees · Tree ranks in a binomial heap are logarithmic

TheoremTree ranks in a binomial heap are logarithmic#✓fully proved

Every tree in a binomial heap holding \(n\) elements, counted with multiplicity, has rank at most \(\lfloor \log_2 n \rfloor\).

public theorem rank_le_log2_card [LinearOrder α] (heap : BinomialHeap α)
    {tree : BinomialTree α} (member : tree ∈ heap.trees) :
    tree.rank ≤ Nat.log2 heap.elements.card
Uses 6
Statement usesBinomial heap · Elements of a binomial heap · Binomial tree · Rank of a binomial tree
Proof usesValid binomial forest · Tree ranks in a valid forest are logarithmic

TheoremA binomial heap has logarithmically many trees#✓fully proved

If a binomial heap over a linearly ordered type has \(n\) elements, counted with multiplicity, then its number of trees is at most \(\lfloor \log_2 n \rfloor + 1\), where \(\lfloor \log_2 0 \rfloor\) is taken to be \(0\).

public theorem length_le_log2_card_succ [LinearOrder α] (heap : BinomialHeap α) :
    heap.trees.length ≤ Nat.log2 heap.elements.card + 1
Uses 5
Statement usesBinomial heap · Elements of a binomial heap · Binomial tree
Proof usesValid binomial forest · A valid binomial forest has logarithmically many trees

DefinitionEmpty binomial heap#✓fully proved

For a linearly ordered type \(\alpha\), the empty binomial heap over \(\alpha\) is the binomial heap whose list of trees is empty.

@[expose] public def empty [LinearOrder α] : BinomialHeap α :=
  ⟨[], BinomialForest.valid_nil⟩
Uses 4
Statement usesValid binomial forest · The empty forest is valid · Binomial heap · Binomial tree

DefinitionMelding binomial heaps#✓fully proved

Over a linear order, the meld of two binomial heaps is the binomial heap whose forest is the meld of the forests of the two heaps.

@[expose] public def meld [LinearOrder α] (left right : BinomialHeap α) : BinomialHeap α :=
  ⟨BinomialForest.meldTrees left.trees right.trees,
    (BinomialForest.meldTrees_correct (rank := 0) left.valid right.valid
      (by simp [BinomialForest.RanksAtLeast])
      (by simp [BinomialForest.RanksAtLeast])).1⟩
Uses 7 · Used by 3
Statement usesRank lower bound for a forest · Valid binomial forest · Melding binomial forests · Melding preserves forest validity and rank lower bounds · Binomial heap · Binomial tree · Rank of a binomial tree
Used byInsertion into a binomial heap adds one occurrence · Melding binomial heaps adds their elements · Insertion into a binomial heap

DefinitionOne-element binomial heap#✓fully proved

For a value \(a\) in a linearly ordered type \(\alpha\), the one-element binomial heap of \(a\) is the binomial heap whose list of trees consists of exactly one tree: the binomial tree of rank \(0\) with root \(a\) and no children.

@[expose] public def singleton [LinearOrder α] (value : α) : BinomialHeap α :=
  ⟨[BinomialTree.singleton value], by
    apply BinomialForest.valid_cons (BinomialTree.valid_singleton value)
      BinomialForest.valid_nil
    simp⟩
Uses 8 · Used by 2
Statement usesValid binomial forest · The empty forest is valid · Binomial heap · Binomial tree · Valid binomial tree · Rank of a binomial tree · Singleton binomial heap · Singleton binomial trees are valid
Used byInsertion into a binomial heap adds one occurrence · Insertion into a binomial heap

DefinitionInsertion into a binomial heap#✓fully proved

Inserting a value \(x\) into a binomial heap \(H\) over a linearly ordered type gives the meld of the one-element binomial heap containing \(x\) with \(H\).

@[expose] public def insert [LinearOrder α] (heap : BinomialHeap α) (value : α) : BinomialHeap α :=
  (singleton value).meld heap
Uses 3 · Used by 1
Statement usesBinomial heap · Melding binomial heaps · One-element binomial heap
Used byInsertion into a binomial heap adds one occurrence

DefinitionMinimum of a binomial heap#✓fully proved

The minimum lookup of a binomial heap over a linearly ordered type returns no value when the heap has no trees, and otherwise returns the least of the root values of its trees, leaving the heap unchanged.

@[expose] public def findMin [LinearOrder α] (heap : BinomialHeap α) : Option α :=
  (BinomialForest.removeMinTree heap.trees).map fun result => result.1.root
Uses 4 · Used by 3
Statement usesRemoving a minimum-root tree from a forest · Binomial heap · Binomial tree · Root of a binomial tree
Used byThe minimum lookup fails exactly on the empty binomial heap · The minimum lookup of a binomial heap returns a lower bound · The minimum lookup of a binomial heap returns one of its elements

DefinitionMinimum deletion on a binomial forest#✓fully proved

Given a list of binomial trees over a linearly ordered type, if the list is empty there is no result. Otherwise, remove the first tree whose root is minimal among the roots of the list; the result is the root of that tree together with the forest obtained by melding its children, in reversed order, with the remaining trees.

@[expose] public def deleteMinTrees [LinearOrder α]
    (trees : List (BinomialTree α)) : Option (α × List (BinomialTree α)) :=
  match BinomialForest.removeMinTree trees with
  | none => none
  | some (minimum, rest) =>
      some (minimum.root,
        BinomialForest.meldTrees minimum.children.reverse rest)
Uses 5 · Used by 1
Statement usesMelding binomial forests · Removing a minimum-root tree from a forest · Binomial tree · Children of a binomial tree · Root of a binomial tree
Used byBinomial heap deletion agrees with forest deletion

DefinitionDeleting the minimum of a binomial heap#✓fully proved

If the binomial heap \(H\) has no trees, there is no result. Otherwise, remove from the list of trees of \(H\) the first tree whose root is minimal; the result is that root together with the binomial heap whose list of trees is obtained by melding the children of the removed tree, in reversed order, with the remaining trees.

Cslib.Algorithms.Lean.BinomialHeap.deleteMin · 15 lines 
public def deleteMin [LinearOrder α]
    (heap : BinomialHeap α) : Option (α × BinomialHeap α) :=
  match found : BinomialForest.removeMinTree heap.trees with
  | none => none
  | some (minimum, rest) =>
      have spec := BinomialForest.removeMinTree_spec found
      have minimum_valid : minimum.Valid := heap.valid.1 minimum spec.2.1
      have rest_valid : BinomialForest.Valid rest := heap.valid.sublist spec.2.2.1
      have children_valid := BinomialForest.valid_reverse_children minimum_valid
      let trees := BinomialForest.meldTrees minimum.children.reverse rest
      have trees_valid : BinomialForest.Valid trees :=
        (BinomialForest.meldTrees_correct (rank := 0) children_valid rest_valid
          (by simp [BinomialForest.RanksAtLeast])
          (by simp [BinomialForest.RanksAtLeast])).1
      some (minimum.root, ⟨trees, trees_valid⟩)
Uses 16 · Used by 5
Statement usesRank lower bound for a forest · Valid binomial forest · Validity of binomial forests passes to sublists · Elements of a binomial forest · Melding binomial forests · Melding preserves forest validity and rank lower bounds · Removing a minimum-root tree from a forest · Removing a minimum-root tree · Reversed children of a valid binomial tree form a valid forest · Binomial heap · Binomial tree · Valid binomial tree · Children of a binomial tree · Elements of a binomial tree · Rank of a binomial tree · Root of a binomial tree
Used byDeleting the minimum of a binomial heap splits its multiset · Deleting the minimum of a binomial heap removes one occurrence · Deleting the minimum fails only on the empty binomial heap · The value deleted from a binomial heap is a lower bound for its elements · Binomial heap deletion agrees with forest deletion

TheoremBinomial heap deletion agrees with forest deletion#✓fully proved

For every binomial heap \(H\) over a linearly ordered type, deleting the minimum of \(H\) and then replacing the remaining heap by its list of trees gives the same result as minimum deletion on the list of trees of \(H\): both have no result, or both return the same minimum value and the same list of trees.

public theorem deleteMin_trees [LinearOrder α] (heap : BinomialHeap α) :
    heap.deleteMin.map (fun result => (result.1, result.2.trees)) =
      deleteMinTrees heap.trees
Uses 18
Statement usesBinomial heap · Deleting the minimum of a binomial heap · Minimum deletion on a binomial forest · Binomial tree
Proof usesRank lower bound for a forest · Valid binomial forest · Validity of binomial forests passes to sublists · Elements of a binomial forest · Melding binomial forests · Melding preserves forest validity and rank lower bounds · Removing a minimum-root tree from a forest · Removing a minimum-root tree · Reversed children of a valid binomial tree form a valid forest · Valid binomial tree · Children of a binomial tree · Elements of a binomial tree · Rank of a binomial tree · Root of a binomial tree

TheoremMelding binomial heaps adds their elements#✓fully proved

For any two binomial heaps \(H_1\) and \(H_2\) over a linearly ordered type, the multiset of elements of the meld of \(H_1\) and \(H_2\) is the sum of the multisets of elements of \(H_1\) and \(H_2\).

public theorem elements_meld [LinearOrder α] (left right : BinomialHeap α) :
    (left.meld right).elements = left.elements + right.elements
Uses 5 · Used by 1
Statement usesBinomial heap · Elements of a binomial heap · Melding binomial heaps
Proof usesMelding binomial forests adds their elements · Binomial tree
Used byInsertion into a binomial heap adds one occurrence

TheoremInsertion into a binomial heap adds one occurrence#✓fully proved

For every binomial heap \(H\) over a linearly ordered type and every value \(v\), the multiset of elements of the heap obtained by inserting \(v\) into \(H\) is the multiset of elements of \(H\) with one more occurrence of \(v\).

public theorem elements_insert [LinearOrder α] (heap : BinomialHeap α) (value : α) :
    (heap.insert value).elements = value ::ₘ heap.elements
Uses 9
Statement usesBinomial heap · Elements of a binomial heap · Insertion into a binomial heap
Proof usesMelding binomial heaps adds their elements · Melding binomial heaps · One-element binomial heap · Binomial tree · Elements of a binomial tree · Singleton binomial heap

TheoremThe minimum lookup fails exactly on the empty binomial heap#✓fully proved

For a binomial heap \(H\) over a linearly ordered type, the minimum lookup of \(H\) returns no value if and only if the list of trees of \(H\) is empty.

public theorem findMin_eq_none_iff [LinearOrder α] (heap : BinomialHeap α) :
    heap.findMin = none ↔ heap.trees = []
Uses 5
Statement usesBinomial heap · Minimum of a binomial heap · Binomial tree
Proof usesRemoving a minimum-root tree from a forest · Root of a binomial tree

TheoremThe minimum lookup of a binomial heap returns one of its elements#✓fully proved

Let \(H\) be a binomial heap over a linearly ordered type. If the minimum lookup of \(H\) returns \(m\), then \(m\) is an element of \(H\).

public theorem findMin_mem [LinearOrder α] {heap : BinomialHeap α} {minimum : α}
    (result : heap.findMin = some minimum) : minimum ∈ heap.elements
Uses 10
Statement usesBinomial heap · Elements of a binomial heap · Minimum of a binomial heap
Proof usesElements of a binomial forest · Removing a minimum-root tree from a forest · Removing a minimum-root tree · Binomial tree · Elements of a binomial tree · Root of a binomial tree · The root of a binomial tree is one of its elements

TheoremThe minimum lookup of a binomial heap returns a lower bound#✓fully proved

Let \(H\) be a binomial heap over a linearly ordered type. If the minimum lookup of \(H\) returns \(m\), then \(m \le v\) for every element \(v\) of \(H\).

public theorem findMin_le [LinearOrder α] {heap : BinomialHeap α} {minimum value : α}
    (result : heap.findMin = some minimum) (member : value ∈ heap.elements) :
    minimum ≤ value
Uses 13
Statement usesBinomial heap · Elements of a binomial heap · Minimum of a binomial heap
Proof usesValid binomial forest · Elements of a binomial forest · Removing a minimum-root tree from a forest · Removing a minimum-root tree · Binomial tree · Valid binomial tree · The root of a valid binomial tree is a lower bound · Elements of a binomial tree · Rank of a binomial tree · Root of a binomial tree

TheoremDeleting the minimum fails only on the empty binomial heap#✓fully proved

For a binomial heap \(H\) over a linearly ordered type, deleting the minimum of \(H\) returns no result if and only if the list of trees of \(H\) is empty.

public theorem deleteMin_eq_none_iff [LinearOrder α] (heap : BinomialHeap α) :
    heap.deleteMin = none ↔ heap.trees = []
Uses 17
Statement usesBinomial heap · Deleting the minimum of a binomial heap · Binomial tree
Proof usesRank lower bound for a forest · Valid binomial forest · Validity of binomial forests passes to sublists · Elements of a binomial forest · Melding binomial forests · Melding preserves forest validity and rank lower bounds · Removing a minimum-root tree from a forest · Removing a minimum-root tree · Reversed children of a valid binomial tree form a valid forest · Valid binomial tree · Children of a binomial tree · Elements of a binomial tree · Rank of a binomial tree · Root of a binomial tree

TheoremDeleting the minimum of a binomial heap removes one occurrence#✓fully proved

For a binomial heap \(H\) over a linearly ordered type, if deleting the minimum of \(H\) succeeds and returns a value \(m\) and a heap \(H'\), then the multiset of elements of \(H'\) is the multiset of elements of \(H\) with one occurrence of \(m\) removed.

public theorem deleteMin_elements [LinearOrder α] {heap : BinomialHeap α} {minimum : α}
    {rest : BinomialHeap α} (result : heap.deleteMin = some (minimum, rest)) :
    rest.elements = heap.elements.erase minimum
Uses 19
Statement usesBinomial heap · Deleting the minimum of a binomial heap · Elements of a binomial heap
Proof usesRank lower bound for a forest · Valid binomial forest · Validity of binomial forests passes to sublists · Elements of a binomial forest · Melding binomial forests adds their elements · Melding binomial forests · Melding preserves forest validity and rank lower bounds · Removing a minimum-root tree from a forest · Removing a minimum-root tree · Reversed children of a valid binomial tree form a valid forest · Binomial tree · Valid binomial tree · Children of a binomial tree · Elements of a binomial tree · Rank of a binomial tree · Root of a binomial tree

TheoremDeleting the minimum of a binomial heap splits its multiset#✓fully proved

For a binomial heap \(H\) over a linearly ordered type, if deleting the minimum of \(H\) succeeds and returns a value \(m\) and a heap \(H'\), then the multiset of elements of \(H\) equals the multiset of elements of \(H'\) with one more occurrence of \(m\).

public theorem deleteMin_cons_elements [LinearOrder α] {heap : BinomialHeap α} {minimum : α}
    {rest : BinomialHeap α} (result : heap.deleteMin = some (minimum, rest)) :
    minimum ::ₘ rest.elements = heap.elements
Uses 19
Statement usesBinomial heap · Deleting the minimum of a binomial heap · Elements of a binomial heap
Proof usesRank lower bound for a forest · Valid binomial forest · Validity of binomial forests passes to sublists · Elements of a binomial forest · Melding binomial forests adds their elements · Melding binomial forests · Melding preserves forest validity and rank lower bounds · Removing a minimum-root tree from a forest · Removing a minimum-root tree · Reversed children of a valid binomial tree form a valid forest · Binomial tree · Valid binomial tree · Children of a binomial tree · Elements of a binomial tree · Rank of a binomial tree · Root of a binomial tree

TheoremThe value deleted from a binomial heap is a lower bound for its elements#✓fully proved

If deleting the minimum of a binomial heap \(H\) over a linearly ordered type succeeds and returns a value \(m\) together with a remaining heap, then \(m \le v\) for every value \(v\) in the multiset of elements of \(H\).

public theorem deleteMin_le [LinearOrder α] {heap : BinomialHeap α} {minimum value : α}
    {rest : BinomialHeap α} (result : heap.deleteMin = some (minimum, rest))
    (member : value ∈ heap.elements) : minimum ≤ value
Uses 19
Statement usesBinomial heap · Deleting the minimum of a binomial heap · Elements of a binomial heap
Proof usesRank lower bound for a forest · Valid binomial forest · Validity of binomial forests passes to sublists · Elements of a binomial forest · Melding binomial forests · Melding preserves forest validity and rank lower bounds · Removing a minimum-root tree from a forest · Removing a minimum-root tree · Reversed children of a valid binomial tree form a valid forest · Binomial tree · Valid binomial tree · The root of a valid binomial tree is a lower bound · Children of a binomial tree · Elements of a binomial tree · Rank of a binomial tree · Root of a binomial tree

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.