Fibonacci heap

InductiveFibonacci tree#✓fully proved

A Fibonacci tree over a type \(\alpha\) is a rose tree: a node carrying a stored degree \(d \in \mathbb{N}\), a root value in \(\alpha\), and a finite list of child Fibonacci trees.

Heap order and the equality of the stored degree with the number of children are not part of the type; they are imposed by the validity predicate on trees.

public inductive FibonacciTree (α : Type u) where
  | node (degree : Nat) (root : α) (children : List (FibonacciTree α))
deriving Repr

Used by 83

Used byInserting a tree into a forest · Fibonacci trees are nonempty · Children of a valid Fibonacci tree are valid · Children of a Fibonacci tree · Consolidation of a forest · Consolidation yields distinct root degrees · Consolidation sorts root degrees · Cutting a subtree out of a Fibonacci tree · Cutting a subtree splits the elements of a Fibonacci tree · A cut without remainder extracts the whole tree · The remainder of a cut from a valid tree is valid · The subtree extracted by a cut from a valid tree is valid · A cut extracts the addressed subtree · Cutting a subtree out of a Fibonacci forest · Cutting a subtree splits the elements of a Fibonacci forest · Every addressed subtree of a forest can be cut out · Cutting a valid forest leaves valid parts · Decrease-key in a Fibonacci heap · Decrease-key preserves the number of elements · Decrease-key replaces one key · Decrease-key replaces one key, stated by address · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Minimum after decrease-key · Root list after decrease-key · Decrease-key yields a valid forest · Replacing the root key of a Fibonacci tree · Lowering the root keeps a Fibonacci tree valid · Degree of a Fibonacci tree · The degree of a valid Fibonacci tree is its number of children · Degree of the link of two trees of equal degree · The degree of a valid Fibonacci tree is less than its size · Deleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · After minimum deletion a Fibonacci heap has at most as many roots as elements · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Minimum deletion on a forest · Fibonacci heap minimum deletion agrees with its root-list version · Multiset of a Fibonacci tree · Multiset of a Fibonacci forest · Multiset of a Fibonacci heap · Elements of a concatenated forest · Consolidation preserves the elements · Elements after replacing the root key · The empty Fibonacci heap has no elements · Insertion adds one occurrence · Linking adds the elements · Melding adds the elements · Multiset of a singleton Fibonacci heap · Empty Fibonacci heap · Fibonacci heap · Find-min fails exactly on the empty Fibonacci heap · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap · Degree-sorted forests have at most as many trees as elements · Linking two Fibonacci trees · Linking preserves validity of Fibonacci trees · Melding Fibonacci heaps · Minimum root of a forest · Minimum root of a concatenated forest · Only the empty forest has no minimum root · The minimum root is a least root · Removing a minimum tree from a Fibonacci forest · Minimum-tree removal in a Fibonacci forest · Root of a Fibonacci tree · Roots of valid Fibonacci trees are lower bounds · The root of a Fibonacci tree is one of its elements · One-element Fibonacci heap · Singleton Fibonacci heap · Forests with strictly increasing degrees · Sublists of valid Fibonacci forests are valid · Subtree of a Fibonacci tree at a path · Subtrees of a valid Fibonacci tree are valid · Every addressed subtree can be cut out · Valid Fibonacci trees · Valid Fibonacci forests · Concatenation preserves validity of Fibonacci forests · Consolidation preserves validity · The empty Fibonacci forest is valid · Singleton Fibonacci trees are valid

DefinitionDegree of a Fibonacci tree#✓fully proved

The degree of the Fibonacci tree with stored degree \(d\), root value \(r\) and list of children \(c\) is the stored natural number \(d\); it is not computed from the children.

@[expose] public def degree : FibonacciTree α → Nat
  | .node degree _ _ => degree

Uses 1 · Used by 13

Statement usesFibonacci tree

Used byInserting a tree into a forest · Consolidation yields distinct root degrees · Consolidation sorts root degrees · The degree of a valid Fibonacci tree is its number of children · Degree of the link of two trees of equal degree · The degree of a valid Fibonacci tree is less than its size · Consolidation preserves the elements · Linking adds the elements · Degree-sorted forests have at most as many trees as elements · Linking two Fibonacci trees · Linking preserves validity of Fibonacci trees · Forests with strictly increasing degrees · Consolidation preserves validity

DefinitionRoot of a Fibonacci tree#✓fully proved

The root of a Fibonacci tree is the value stored at its top node.

@[expose] public def root : FibonacciTree α → α
  | .node _ root _ => root

Uses 1 · Used by 32

Statement usesFibonacci tree

Used byDecrease-key in a Fibonacci heap · Decrease-key preserves the number of elements · Decrease-key replaces one key · Decrease-key replaces one key, stated by address · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Minimum after decrease-key · Root list after decrease-key · Lowering the root keeps a Fibonacci tree valid · Degree of the link of two trees of equal degree · Deleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Minimum deletion on a forest · Fibonacci heap minimum deletion agrees with its root-list version · Elements after replacing the root key · Linking adds the elements · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap · Linking two Fibonacci trees · Linking preserves validity of Fibonacci trees · Minimum root of a forest · Minimum root of a concatenated forest · Only the empty forest has no minimum root · The minimum root is a least root · Removing a minimum tree from a Fibonacci forest · Minimum-tree removal in a Fibonacci forest · Roots of valid Fibonacci trees are lower bounds · The root of a Fibonacci tree is one of its elements

DefinitionChildren of a Fibonacci tree#✓fully proved

The children of the Fibonacci tree with stored degree \(d\), root value \(r\) and list of subtrees \(c\) are the trees of the list \(c\), in order.

@[expose] public def children : FibonacciTree α → List (FibonacciTree α)
  | .node _ _ children => children

Uses 1 · Used by 17

Statement usesFibonacci tree

Used byChildren of a valid Fibonacci tree are valid · The remainder of a cut from a valid tree is valid · The degree of a valid Fibonacci tree is its number of children · Degree of the link of two trees of equal degree · The degree of a valid Fibonacci tree is less than its size · Deleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Minimum deletion on a forest · Fibonacci heap minimum deletion agrees with its root-list version · Linking adds the elements · Linking two Fibonacci trees · Linking preserves validity of Fibonacci trees · Subtrees of a valid Fibonacci tree are valid

DefinitionMultiset of a Fibonacci tree#✓fully proved

The multiset \(M(t)\) of values stored in a Fibonacci tree \(t\), defined recursively: if \(t\) has root value \(r\) and children \(t_1, \dots, t_k\), then \(M(t) = \{r\} + M(t_1) + \cdots + M(t_k)\). The stored degree plays no role.

@[expose] public def elements : FibonacciTree α → Multiset α
  | .node _ root children => root ::ₘ (children.map elements).sum

Uses 1 · Used by 38

Statement usesFibonacci tree

Used byFibonacci trees are nonempty · Children of a valid Fibonacci tree are valid · Cutting a subtree splits the elements of a Fibonacci tree · The remainder of a cut from a valid tree is valid · Cutting a subtree splits the elements of a Fibonacci forest · Decrease-key in a Fibonacci heap · Decrease-key preserves the number of elements · Decrease-key replaces one key · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key · Lowering the root keeps a Fibonacci tree valid · The degree of a valid Fibonacci tree is its number of children · The degree of a valid Fibonacci tree is less than its size · Deleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version · Multiset of a Fibonacci forest · Elements of a concatenated forest · Consolidation preserves the elements · Elements after replacing the root key · The empty Fibonacci heap has no elements · Insertion adds one occurrence · Linking adds the elements · Multiset of a singleton Fibonacci heap · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap · Degree-sorted forests have at most as many trees as elements · Linking preserves validity of Fibonacci trees · Minimum-tree removal in a Fibonacci forest · Roots of valid Fibonacci trees are lower bounds · The root of a Fibonacci tree is one of its elements · Valid Fibonacci trees · Singleton Fibonacci trees are valid

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

For every Fibonacci tree, its root value belongs to the multiset of elements the tree represents.

public theorem root_mem_elements (tree : FibonacciTree α) : tree.root ∈ tree.elements

Uses 3 · Used by 7

Statement usesFibonacci tree · Multiset of a Fibonacci tree · Root of a Fibonacci tree

Used byDecrease-key in a Fibonacci heap · Decrease-key preserves the number of elements · Decrease-key replaces one key · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key · Find-min returns an element of the Fibonacci heap

TheoremFibonacci trees are nonempty#✓fully proved

Every Fibonacci tree represents at least one element: the multiset of elements of any Fibonacci tree has positive size.

public theorem card_elements_pos (tree : FibonacciTree α) : 0 < tree.elements.card

Uses 2 · Used by 1

Statement usesFibonacci tree · Multiset of a Fibonacci tree

Used byThe degree of a valid Fibonacci tree is less than its size

InductiveValid Fibonacci trees#✓fully proved

Let \(\alpha\) carry a relation \(\le\). A Fibonacci tree with stored degree \(d\), root \(r \in \alpha\) and list of children \(c\) is valid when every tree in \(c\) is valid, \(d\) equals the length of \(c\), and \(r \le x\) for every element \(x\) of the multiset represented by the tree (the root together with the elements of all children).

public inductive Valid {α : Type u} [LE α] : FibonacciTree α → Prop
  | node {degree : Nat} {root : α} {children : List (FibonacciTree α)}
      (children_valid : ∀ child ∈ children, Valid child)
      (degree_eq : degree = children.length)
      (root_le : ∀ value ∈ elements (.node degree root children), root ≤ value) :
      Valid (.node degree root children)

Uses 2 · Used by 27

Statement usesFibonacci tree · Multiset of a Fibonacci tree

Used byChildren of a valid Fibonacci tree are valid · The remainder of a cut from a valid tree is valid · The subtree extracted by a cut from a valid tree is valid · Cutting a valid forest leaves valid parts · Decrease-key in a Fibonacci heap · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key · Lowering the root keeps a Fibonacci tree valid · The degree of a valid Fibonacci tree is its number of children · The degree of a valid Fibonacci tree is less than its size · Deleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version · Linking preserves validity of Fibonacci trees · Roots of valid Fibonacci trees are lower bounds · Singleton Fibonacci heap · Subtrees of a valid Fibonacci tree are valid · Valid Fibonacci forests · Concatenation preserves validity of Fibonacci forests · Consolidation preserves validity · The empty Fibonacci forest is valid · Singleton Fibonacci trees are valid

DefinitionOne-element Fibonacci heap#✓fully proved

For a value \(x\) of a linearly ordered type, the one-element Fibonacci heap on \(x\) has as its only tree the single-node tree with root \(x\), and its cached minimum is \(x\).

@[expose] public def singleton (value : α) : FibonacciTree α :=
  .node 0 value []

Uses 1 · Used by 4

Statement usesFibonacci tree

Used byInsertion adds one occurrence · Multiset of a singleton Fibonacci heap · Singleton Fibonacci heap · Singleton Fibonacci trees are valid

DefinitionLinking two Fibonacci trees#✓fully proved

Let \(s\) and \(t\) be Fibonacci trees over a linearly ordered type. If the root of \(s\) is at most the root of \(t\), the link of \(s\) and \(t\) is the tree with the root of \(s\), stored degree one more than that of \(s\), and children \(t\) followed by the children of \(s\). Otherwise it is the tree with the root of \(t\), stored degree one more than that of \(t\), and children \(s\) followed by the children of \(t\).

@[expose] public def link [LinearOrder α] (left right : FibonacciTree α) : FibonacciTree α :=
  if left.root ≤ right.root then
    .node (left.degree + 1) left.root (right :: left.children)
  else
    .node (right.degree + 1) right.root (left :: right.children)

Uses 4 · Used by 7

Statement usesFibonacci tree · Children of a Fibonacci tree · Degree of a Fibonacci tree · Root of a Fibonacci tree

Used byInserting a tree into a forest · Consolidation sorts root degrees · Degree of the link of two trees of equal degree · Consolidation preserves the elements · Linking adds the elements · Linking preserves validity of Fibonacci trees · Consolidation preserves validity

TheoremDegree of the link of two trees of equal degree#✓fully proved

If two Fibonacci trees \(s\) and \(t\) over a linearly ordered type have the same degree \(d\), then their link has degree \(d + 1\).

public theorem degree_link_of_eq [LinearOrder α] {left right : FibonacciTree α}
    (degrees : left.degree = right.degree) :
    (link left right).degree = left.degree + 1

Uses 5 · Used by 1

Statement usesFibonacci tree · Degree of a Fibonacci tree · Linking two Fibonacci trees

Proof usesChildren of a Fibonacci tree · Root of a Fibonacci tree

Used byConsolidation sorts root degrees

TheoremLinking adds the elements#✓fully proved

For any two Fibonacci trees \(S\) and \(T\) over a linearly ordered type, the tree obtained by linking \(S\) and \(T\) represents the sum of the multisets represented by \(S\) and by \(T\).

public theorem elements_link [LinearOrder α] (left right : FibonacciTree α) :
    (link left right).elements = left.elements + right.elements

Uses 6 · Used by 2

Statement usesFibonacci tree · Multiset of a Fibonacci tree · Linking two Fibonacci trees

Proof usesChildren of a Fibonacci tree · Degree of a Fibonacci tree · Root of a Fibonacci tree

Used byConsolidation preserves the elements · Linking preserves validity of Fibonacci trees

TheoremSingleton Fibonacci trees are valid#✓fully proved

Let \(\alpha\) be a linearly ordered type. For every \(v \in \alpha\), the Fibonacci tree of degree \(0\) with root \(v\) and no children is valid.

public theorem valid_singleton [LinearOrder α] (value : α) : Valid (singleton value)

Uses 4 · Used by 1

Statement usesValid Fibonacci trees · One-element Fibonacci heap

Proof usesFibonacci tree · Multiset of a Fibonacci tree

Used bySingleton Fibonacci heap

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

Every child of a valid Fibonacci tree is itself a valid Fibonacci tree.

public theorem Valid.child_valid [LE α] {tree child : FibonacciTree α}
    (valid : Valid tree) (member : child ∈ tree.children) : Valid child

Uses 4 · Used by 11

Statement usesFibonacci tree · Valid Fibonacci trees · Children of a Fibonacci tree

Proof usesMultiset of a Fibonacci tree

Used byThe remainder of a cut from a valid tree is valid · Lowering the root keeps a Fibonacci tree valid · Deleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version · Linking preserves validity of Fibonacci trees · Subtrees of a valid Fibonacci tree are valid

TheoremThe degree of a valid Fibonacci tree is its number of children#✓fully proved

For every valid Fibonacci tree, its stored degree equals the number of its children.

public theorem Valid.degree_eq [LE α] {tree : FibonacciTree α} (valid : Valid tree) :
    tree.degree = tree.children.length

Uses 5 · Used by 3

Statement usesFibonacci tree · Valid Fibonacci trees · Children of a Fibonacci tree · Degree of a Fibonacci tree

Proof usesMultiset of a Fibonacci tree

Used byLowering the root keeps a Fibonacci tree valid · The degree of a valid Fibonacci tree is less than its size · Linking preserves validity of Fibonacci trees

TheoremRoots of valid Fibonacci trees are lower bounds#✓fully proved

The root of a valid Fibonacci tree is no greater than every element of the multiset the tree represents.

public theorem Valid.root_le [LE α] {tree : FibonacciTree α} (valid : Valid tree)
    {value : α} (member : value ∈ tree.elements) : tree.root ≤ value

Uses 4 · Used by 5

Statement usesFibonacci tree · Valid Fibonacci trees · Multiset of a Fibonacci tree · Root of a Fibonacci tree

Used byThe remainder of a cut from a valid tree is valid · Lowering the root keeps a Fibonacci tree valid · Fibonacci heap minimum deletion returns a lower bound · Find-min returns a lower bound of the Fibonacci heap · Linking preserves validity of Fibonacci trees

TheoremThe degree of a valid Fibonacci tree is less than its size#✓fully proved

For every valid Fibonacci tree over a type with a relation \(\le\), the degree of the tree is strictly less than the number of elements, counted with multiplicity, of the multiset the tree represents, since every child contributes at least one element.

public theorem Valid.degree_lt_card [LE α] {tree : FibonacciTree α} (valid : Valid tree) :
    tree.degree < tree.elements.card

Uses 7 · Used by 1

Statement usesFibonacci tree · Valid Fibonacci trees · Degree of a Fibonacci tree · Multiset of a Fibonacci tree

Proof usesThe degree of a valid Fibonacci tree is its number of children · Fibonacci trees are nonempty · Children of a Fibonacci tree

Used byDegree-sorted forests have at most as many trees as elements

TheoremLinking preserves validity of Fibonacci trees#✓fully proved

If \(s\) and \(t\) are valid Fibonacci trees over a linearly ordered type, then the link of \(s\) and \(t\) is a valid Fibonacci tree.

public theorem Valid.link [LinearOrder α] {left right : FibonacciTree α}
    (left_valid : Valid left) (right_valid : Valid right) : Valid (link left right)

Uses 11 · Used by 1

Statement usesFibonacci tree · Valid Fibonacci trees · Linking two Fibonacci trees

Proof usesChildren of a valid Fibonacci tree are valid · The degree of a valid Fibonacci tree is its number of children · Roots of valid Fibonacci trees are lower bounds · Children of a Fibonacci tree · Degree of a Fibonacci tree · Multiset of a Fibonacci tree · Linking adds the elements · Root of a Fibonacci tree

Used byConsolidation preserves validity

DefinitionValid Fibonacci forests#✓fully proved

Let \(\alpha\) carry a relation \(\le\). A Fibonacci forest, a list of Fibonacci trees with values in \(\alpha\), is valid when every tree in it is a valid Fibonacci tree.

Root degrees may repeat; consolidation is what makes them distinct.

@[expose] public def FibonacciForest.Valid {α : Type u} [LE α]
    (trees : List (FibonacciTree α)) : Prop :=
  ∀ tree ∈ trees, tree.Valid

Uses 2 · Used by 24

Statement usesFibonacci tree · Valid Fibonacci trees

Used byCutting a valid forest leaves valid parts · Decrease-key in a Fibonacci heap · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key · Decrease-key yields a valid forest · Deleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · After minimum deletion a Fibonacci heap has at most as many roots as elements · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version · Empty Fibonacci heap · Fibonacci heap · Find-min returns a lower bound of the Fibonacci heap · Degree-sorted forests have at most as many trees as elements · Melding Fibonacci heaps · Singleton Fibonacci heap · Sublists of valid Fibonacci forests are valid · Concatenation preserves validity of Fibonacci forests · Consolidation preserves validity · The empty Fibonacci forest is valid

DefinitionMultiset of a Fibonacci forest#✓fully proved

Write \(M(t)\) for the multiset of values stored in a Fibonacci tree \(t\). The multiset represented by a Fibonacci forest, a list of Fibonacci trees \(t_1, \dots, t_k\), is the sum \(M(t_1) + \cdots + M(t_k)\); the empty forest represents the empty multiset.

@[expose] public def elements (trees : List (FibonacciTree α)) : Multiset α :=
  (trees.map FibonacciTree.elements).sum

Uses 2 · Used by 21

Statement usesFibonacci tree · Multiset of a Fibonacci tree

Used byCutting a subtree splits the elements of a Fibonacci forest · Decrease-key in a Fibonacci heap · Decrease-key preserves the number of elements · Decrease-key replaces one key · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key · Deleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version · Multiset of a Fibonacci heap · Elements of a concatenated forest · Consolidation preserves the elements · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap · Degree-sorted forests have at most as many trees as elements · Minimum-tree removal in a Fibonacci forest

DefinitionForests with strictly increasing degrees#✓fully proved

A Fibonacci forest, a list of Fibonacci trees \(t_1, \dots, t_k\), has sorted degrees when the stored degrees of its trees strictly increase along the list: \(\deg t_i < \deg t_j\) whenever \(i < j\).

@[expose] public def SortedDegrees (trees : List (FibonacciTree α)) : Prop :=
  trees.Pairwise fun a b => a.degree < b.degree

Uses 2 · Used by 3

Statement usesFibonacci tree · Degree of a Fibonacci tree

Used byConsolidation sorts root degrees · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Degree-sorted forests have at most as many trees as elements

TheoremThe empty Fibonacci forest is valid#✓fully proved

Let \(\alpha\) carry a relation \(\le\). The empty forest, containing no Fibonacci trees with values in \(\alpha\), is valid.

public theorem valid_nil [LE α] : Valid ([] : List (FibonacciTree α))

Uses 3 · Used by 1

Statement usesValid Fibonacci forests · Fibonacci tree

Proof usesValid Fibonacci trees

Used byEmpty Fibonacci heap

TheoremConcatenation preserves validity of Fibonacci forests#✓fully proved

Let \(\alpha\) carry a relation \(\le\). If \(F\) and \(G\) are valid Fibonacci forests with values in \(\alpha\), then the forest consisting of the trees of \(F\) followed by the trees of \(G\) is valid.

public theorem valid_append [LE α] {left right : List (FibonacciTree α)}
    (left_valid : Valid left) (right_valid : Valid right) : Valid (left ++ right)

Uses 3 · Used by 8

Statement usesValid Fibonacci forests · Fibonacci tree

Proof usesValid Fibonacci trees

Used byDeleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version · Melding Fibonacci heaps

TheoremSublists of valid Fibonacci forests are valid#✓fully proved

If a list of Fibonacci trees is a valid forest, then every sublist of it (a subsequence, not necessarily contiguous) is a valid forest.

public theorem Valid.sublist [LE α] {left right : List (FibonacciTree α)}
    (sublist : left.Sublist right) (valid : Valid right) : Valid left

Uses 2 · Used by 7

Statement usesValid Fibonacci forests · Fibonacci tree

Used byDeleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version

TheoremElements of a concatenated forest#✓fully proved

For any two lists \(L\) and \(R\) of Fibonacci trees, the forest made of the trees of \(L\) followed by the trees of \(R\) represents the sum of the multisets represented by \(L\) and by \(R\).

public theorem elements_append (left right : List (FibonacciTree α)) :
    elements (left ++ right) = elements left + elements right

Uses 3 · Used by 3

Statement usesMultiset of a Fibonacci forest · Fibonacci tree

Proof usesMultiset of a Fibonacci tree

Used byFibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Melding adds the elements

DefinitionMinimum root of a forest#✓fully proved

The minimum root of a forest of Fibonacci trees over a linearly ordered type is an optional value: it is absent for the empty forest, and for a nonempty forest it is the least of the roots of its trees.

@[expose] public def minRoot [LinearOrder α] : List (FibonacciTree α) → Option α
  | [] => none
  | tree :: trees =>
      match minRoot trees with
      | none => some tree.root
      | some minimum => some (min tree.root minimum)

Uses 2 · Used by 21

Statement usesFibonacci tree · Root of a Fibonacci tree

Used byDecrease-key in a Fibonacci heap · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key · Deleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version · Empty Fibonacci heap · Fibonacci heap · Find-min fails exactly on the empty Fibonacci heap · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap · Melding Fibonacci heaps · Minimum root of a concatenated forest · Only the empty forest has no minimum root · The minimum root is a least root · Singleton Fibonacci heap

DefinitionMinimum of two optional values#✓fully proved

For optional values \(x\) and \(y\) of a linearly ordered type, their combined minimum is defined as follows: if \(x\) and \(y\) are both present, with values \(a\) and \(b\), it is \(\min(a, b)\); if exactly one of \(x\) and \(y\) is present, it is that value; and if both are absent, it is absent.

@[expose] public def minOption [LinearOrder α] (left right : Option α) : Option α :=
  match left, right with
  | some a, some b => some (min a b)
  | some a, none => some a
  | none, some b => some b
  | none, none => none

Used by 2

Used byMelding Fibonacci heaps · Minimum root of a concatenated forest

TheoremOnly the empty forest has no minimum root#✓fully proved

A forest of Fibonacci trees over a linearly ordered type has no minimum root exactly when it is empty.

public theorem minRoot_eq_none_iff [LinearOrder α] (trees : List (FibonacciTree α)) :
    minRoot trees = none ↔ trees = []

Uses 3 · Used by 6

Statement usesMinimum root of a forest · Fibonacci tree

Proof usesRoot of a Fibonacci tree

Used byDecrease-key in a Fibonacci heap · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key · Find-min fails exactly on the empty Fibonacci heap · The minimum root is a least root

TheoremThe minimum root is a least root#✓fully proved

If a forest \(F\) of Fibonacci trees over a linearly ordered type has minimum root \(m\), then \(m\) is the root of some tree of \(F\) and \(m\) is at most the root of every tree of \(F\).

public theorem minRoot_spec [LinearOrder α] {trees : List (FibonacciTree α)} {minimum : α}
    (result : minRoot trees = some minimum) :
    (∃ tree ∈ trees, tree.root = minimum) ∧ ∀ tree ∈ trees, minimum ≤ tree.root

Uses 4 · Used by 2

Statement usesMinimum root of a forest · Fibonacci tree · Root of a Fibonacci tree

Proof usesOnly the empty forest has no minimum root

Used byFind-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap

TheoremMinimum root of a concatenated forest#✓fully proved

For forests \(F\) and \(G\) of Fibonacci trees over a linearly ordered type, the minimum root of \(F\) followed by \(G\) is the combined minimum of the optional minimum roots of \(F\) and of \(G\): their minimum if both exist, the one that exists if only one does, and absent if neither does.

public theorem minRoot_append [LinearOrder α] (left right : List (FibonacciTree α)) :
    minRoot (left ++ right) = minOption (minRoot left) (minRoot right)

Uses 4 · Used by 1

Statement usesMinimum of two optional values · Minimum root of a forest · Fibonacci tree

Proof usesRoot of a Fibonacci tree

Used byMelding Fibonacci heaps

DefinitionInserting a tree into a forest#✓fully proved

Given a Fibonacci tree \(t\) and a list of Fibonacci trees, the insertion of \(t\) into the list is defined recursively. Inserting \(t\) into the empty list gives the one-tree list \([t]\). For a list with first tree \(s\) and remaining list \(L\): if the stored degree of \(t\) is less than the stored degree of \(s\), the result is \(t\) followed by \(s\) and then \(L\); if the two stored degrees are equal, the result is the insertion of the link of \(t\) and \(s\) into \(L\); otherwise the result is \(s\) followed by the insertion of \(t\) into \(L\).

On a list whose stored degrees strictly increase, this links \(t\) with any tree of equal degree and carries the linked tree forward, as in binary addition.

@[expose] public def addTree [LinearOrder α] (tree : FibonacciTree α) :
    List (FibonacciTree α) → List (FibonacciTree α)
  | [] => [tree]
  | other :: trees =>
      if tree.degree < other.degree then
        tree :: other :: trees
      else if tree.degree = other.degree then
        addTree (tree.link other) trees
      else
        other :: addTree tree trees

Uses 3 · Used by 4

Statement usesFibonacci tree · Degree of a Fibonacci tree · Linking two Fibonacci trees

Used byConsolidation of a forest · Consolidation sorts root degrees · Consolidation preserves the elements · Consolidation preserves validity

DefinitionConsolidation of a forest#✓fully proved

The consolidation of a list of Fibonacci trees is defined recursively: the consolidation of the empty list is the empty list, and the consolidation of a list with first tree \(t\) and remaining list \(L\) is the insertion of \(t\) into the consolidation of \(L\).

Each insertion links trees of equal stored degree as in binary addition, so the result has strictly increasing, hence distinct, stored root degrees, as in the consolidate step of CLRS.

@[expose] public def consolidate [LinearOrder α] :
    List (FibonacciTree α) → List (FibonacciTree α)
  | [] => []
  | tree :: trees => addTree tree (consolidate trees)

Uses 2 · Used by 12

Statement usesInserting a tree into a forest · Fibonacci tree

Used byConsolidation yields distinct root degrees · Consolidation sorts root degrees · Deleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Minimum deletion on a forest · Fibonacci heap minimum deletion agrees with its root-list version · Consolidation preserves the elements · Consolidation preserves validity

TheoremConsolidation preserves the elements#✓fully proved

For every list of Fibonacci trees over a linearly ordered type, its consolidation represents the same multiset as the original list.

public theorem elements_consolidate [LinearOrder α] (trees : List (FibonacciTree α)) :
    elements (consolidate trees) = elements trees

Uses 8 · Used by 2

Statement usesConsolidation of a forest · Multiset of a Fibonacci forest · Fibonacci tree

Proof usesInserting a tree into a forest · Degree of a Fibonacci tree · Multiset of a Fibonacci tree · Linking adds the elements · Linking two Fibonacci trees

Used byFibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum

TheoremConsolidation preserves validity#✓fully proved

Let \(\alpha\) be a linearly ordered type. If a Fibonacci forest with values in \(\alpha\) is valid, then its consolidation is valid.

public theorem valid_consolidate [LinearOrder α] {trees : List (FibonacciTree α)}
    (valid : Valid trees) : Valid (consolidate trees)

Uses 8 · Used by 7

Statement usesValid Fibonacci forests · Consolidation of a forest · Fibonacci tree

Proof usesInserting a tree into a forest · Valid Fibonacci trees · Linking preserves validity of Fibonacci trees · Degree of a Fibonacci tree · Linking two Fibonacci trees

Used byDeleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version

TheoremConsolidation sorts root degrees#✓fully proved

For every list of Fibonacci trees, the stored degrees of the trees in its consolidation are strictly increasing in list order.

public theorem consolidate_sorted [LinearOrder α] (trees : List (FibonacciTree α)) :
    SortedDegrees (consolidate trees)

Uses 7 · Used by 2

Statement usesForests with strictly increasing degrees · Consolidation of a forest · Fibonacci tree

Proof usesInserting a tree into a forest · Degree of a Fibonacci tree · Degree of the link of two trees of equal degree · Linking two Fibonacci trees

Used byConsolidation yields distinct root degrees · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees

TheoremConsolidation yields distinct root degrees#✓fully proved

For every list of Fibonacci trees, the trees in its consolidation have pairwise distinct stored degrees.

public theorem consolidate_degrees_nodup [LinearOrder α]
    (trees : List (FibonacciTree α)) :
    ((consolidate trees).map FibonacciTree.degree).Nodup

Uses 4

Statement usesConsolidation of a forest · Fibonacci tree · Degree of a Fibonacci tree

Proof usesConsolidation sorts root degrees

TheoremDegree-sorted forests have at most as many trees as elements#✓fully proved

Let \(F\) be a valid forest of Fibonacci trees whose degrees are strictly increasing along the list. Then the number of trees in \(F\) is at most the number of elements, counted with multiplicity, that \(F\) represents.

Every degree is smaller than the total element count and the degrees are distinct.

public theorem length_le_card_of_sorted [LE α] {trees : List (FibonacciTree α)}
    (valid : Valid trees) (sorted : SortedDegrees trees) :
    trees.length ≤ (elements trees).card

Uses 7 · Used by 1

Statement usesForests with strictly increasing degrees · Valid Fibonacci forests · Multiset of a Fibonacci forest · Fibonacci tree

Proof usesThe degree of a valid Fibonacci tree is less than its size · Degree of a Fibonacci tree · Multiset of a Fibonacci tree

Used byAfter minimum deletion a Fibonacci heap has at most as many roots as elements

DefinitionRemoving a minimum tree from a Fibonacci forest#✓fully proved

For a list of Fibonacci trees over a linearly ordered type, this returns nothing on the empty list. Otherwise it returns the first tree whose root is minimal among all roots in the list, so earlier trees win ties, together with the list of the remaining trees in their original order.

@[expose] public def removeMinTree [LinearOrder α] :
    List (FibonacciTree α) → Option (FibonacciTree α × List (FibonacciTree α))
  | [] => 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 9

Statement usesFibonacci tree · Root of a Fibonacci tree

Used byDeleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Minimum deletion on a forest · Fibonacci heap minimum deletion agrees with its root-list version · Minimum-tree removal in a Fibonacci forest

TheoremMinimum-tree removal in a Fibonacci forest#✓fully proved

Let \(T\) be a list of Fibonacci trees over a linearly ordered type. If removing a minimum tree from \(T\) returns a tree \(m\) and a list \(R\), then the multiset of elements of \(m\) plus the multiset of elements of \(R\) equals the multiset of elements of \(T\), the tree \(m\) belongs to \(T\), the list \(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 (FibonacciTree α)} {minimum : FibonacciTree α}
    {rest : List (FibonacciTree α)} (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 7

Statement usesMultiset of a Fibonacci forest · Removing a minimum tree from a Fibonacci forest · Fibonacci tree · Multiset of a Fibonacci tree · Root of a Fibonacci tree

Used byDeleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version

StructureFibonacci heap#✓fully proved

A Fibonacci min-heap over a linearly ordered type consists of a list of Fibonacci trees, each valid (heap-ordered, and at every node the stored degree equals the number of children), together with a cached minimum equal to the least root value of these trees, absent when the list is empty.

public structure FibonacciHeap (α : Type u) [LinearOrder α] where
  /-- The heap-ordered trees; root degrees may repeat between deletions. -/
  trees : List (FibonacciTree α)
  /-- The cached minimum element. -/
  cachedMin : Option α
  valid : FibonacciForest.Valid trees
  min_eq : cachedMin = FibonacciForest.minRoot trees

Uses 3 · Used by 34

Statement usesValid Fibonacci forests · Minimum root of a forest · Fibonacci tree

Used byInsertion increases the size of a Fibonacci heap by one · Melding adds the sizes of Fibonacci heaps · Decrease-key in a Fibonacci heap · Decrease-key preserves the number of elements · Decrease-key replaces one key · Decrease-key replaces one key, stated by address · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Minimum after decrease-key · Root list after decrease-key · Decrease-key yields a valid forest · Deleting the minimum of a Fibonacci heap · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · After minimum deletion a Fibonacci heap has at most as many roots as elements · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version · Multiset of a Fibonacci heap · The empty Fibonacci heap has no elements · Insertion adds one occurrence · Melding adds the elements · Multiset of a singleton Fibonacci heap · The union of Fibonacci heaps adds their multisets · Empty Fibonacci heap · Find-min for Fibonacci heaps · Find-min fails exactly on the empty Fibonacci heap · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap · Insertion into a Fibonacci heap · Melding Fibonacci heaps · Singleton Fibonacci heap · Union of Fibonacci heaps

DefinitionMultiset of a Fibonacci heap#✓fully proved

The multiset represented by a Fibonacci heap over a linearly ordered type is the multiset of its list of trees: the sum, over the trees in the list, of the multisets of values stored in them. The cached minimum plays no role.

@[expose] public def elements [LinearOrder α] (heap : FibonacciHeap α) : Multiset α :=
  FibonacciForest.elements heap.trees

Uses 3 · Used by 21

Statement usesMultiset of a Fibonacci forest · Fibonacci heap · Fibonacci tree

Used byInsertion increases the size of a Fibonacci heap by one · Melding adds the sizes of Fibonacci heaps · Decrease-key in a Fibonacci heap · Decrease-key preserves the number of elements · Decrease-key replaces one key · Decrease-key replaces one key, stated by address · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Minimum after decrease-key · Root list after decrease-key · Fibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion returns a lower bound · After minimum deletion a Fibonacci heap has at most as many roots as elements · The empty Fibonacci heap has no elements · Insertion adds one occurrence · Melding adds the elements · Multiset of a singleton Fibonacci heap · The union of Fibonacci heaps adds their multisets · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap

DefinitionEmpty Fibonacci heap#✓fully proved

The Fibonacci heap over a linearly ordered type whose list of trees is empty and whose cached minimum is absent.

@[expose] public def empty [LinearOrder α] : FibonacciHeap α :=
  ⟨[], none, FibonacciForest.valid_nil, rfl⟩

Uses 5 · Used by 1

Statement usesValid Fibonacci forests · Minimum root of a forest · The empty Fibonacci forest is valid · Fibonacci heap · Fibonacci tree

Used byThe empty Fibonacci heap has no elements

DefinitionSingleton Fibonacci heap#✓fully proved

For a value \(x\) of a linearly ordered type, the singleton Fibonacci heap on \(x\) has as its only tree the single-node tree with root \(x\), stored degree \(0\) and no children, and its cached minimum is \(x\).

@[expose] public def singleton [LinearOrder α] (value : α) : FibonacciHeap α :=
  ⟨[FibonacciTree.singleton value], some value, by
    intro tree member
    simp only [List.mem_singleton] at member
    subst member
    exact FibonacciTree.valid_singleton value, by
    simp [FibonacciForest.minRoot, FibonacciTree.singleton, FibonacciTree.root]⟩

Uses 7 · Used by 3

Statement usesValid Fibonacci forests · Minimum root of a forest · Fibonacci heap · Fibonacci tree · Valid Fibonacci trees · One-element Fibonacci heap · Singleton Fibonacci trees are valid

Used byInsertion adds one occurrence · Multiset of a singleton Fibonacci heap · Insertion into a Fibonacci heap

DefinitionMelding Fibonacci heaps#✓fully proved

The meld of Fibonacci heaps \(H_1\) and \(H_2\) is the Fibonacci heap whose root list is the root list of \(H_1\) followed by that of \(H_2\), and whose cached minimum is the smaller of the two cached minima when both heaps have one, and otherwise the cached minimum of whichever heap has one (none if neither does).

No linking happens until the next minimum deletion.

@[expose] public def meld [LinearOrder α] (left right : FibonacciHeap α) : FibonacciHeap α :=
  ⟨left.trees ++ right.trees,
    FibonacciForest.minOption left.cachedMin right.cachedMin,
    FibonacciForest.valid_append left.valid right.valid,
    by rw [FibonacciForest.minRoot_append, left.min_eq, right.min_eq]⟩

Uses 7 · Used by 5

Statement usesValid Fibonacci forests · Minimum of two optional values · Minimum root of a forest · Minimum root of a concatenated forest · Concatenation preserves validity of Fibonacci forests · Fibonacci heap · Fibonacci tree

Used byMelding adds the sizes of Fibonacci heaps · Insertion adds one occurrence · Melding adds the elements · Insertion into a Fibonacci heap · Union of Fibonacci heaps

DefinitionUnion of Fibonacci heaps#✓fully proved

The union of Fibonacci heaps \(H_1\) and \(H_2\) is their meld: the heap whose trees are those of \(H_1\) followed by those of \(H_2\), and whose cached minimum is the smaller of the two cached minima (the one that exists if a heap is empty, none if both are).

CLRS calls this operation union.

@[expose] public def union [LinearOrder α] (left right : FibonacciHeap α) : FibonacciHeap α :=
  left.meld right

Uses 2 · Used by 1

Statement usesFibonacci heap · Melding Fibonacci heaps

Used byThe union of Fibonacci heaps adds their multisets

DefinitionInsertion into a Fibonacci heap#✓fully proved

Inserting a value \(x\) into a Fibonacci heap \(H\) gives the meld of the one-element Fibonacci heap containing \(x\) with \(H\), the one-element heap coming first.

@[expose] public def insert [LinearOrder α] (heap : FibonacciHeap α) (value : α) :
    FibonacciHeap α :=
  (singleton value).meld heap

Uses 3 · Used by 2

Statement usesFibonacci heap · Melding Fibonacci heaps · Singleton Fibonacci heap

Used byInsertion increases the size of a Fibonacci heap by one · Insertion adds one occurrence

DefinitionFind-min for Fibonacci heaps#✓fully proved

Find-min on a Fibonacci heap returns its cached minimum without modifying the heap: the least root value of its trees, or no value when the heap has no trees.

@[expose] public def findMin [LinearOrder α] (heap : FibonacciHeap α) : Option α :=
  heap.cachedMin

Uses 1 · Used by 8

Statement usesFibonacci heap

Used byDecrease-key in a Fibonacci heap · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Minimum after decrease-key · Root list after decrease-key · Find-min fails exactly on the empty Fibonacci heap · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap

DefinitionMinimum deletion on a forest#✓fully proved

Given a list of Fibonacci trees over a linearly ordered type, the result is nothing if the list is empty. Otherwise the first tree whose root is minimal is removed, and the result is its root value together with the consolidation of the forest made of the removed tree's children followed by the remaining trees.

This is the forest-level computation behind deleting the minimum of a Fibonacci heap, without the validity proofs.

@[expose] public def deleteMinTrees [LinearOrder α]
    (trees : List (FibonacciTree α)) : Option (α × List (FibonacciTree α)) :=
  match FibonacciForest.removeMinTree trees with
  | none => none
  | some (minimum, rest) =>
      some (minimum.root, FibonacciForest.consolidate (minimum.children ++ rest))

Uses 5 · Used by 1

Statement usesConsolidation of a forest · Removing a minimum tree from a Fibonacci forest · Fibonacci tree · Children of a Fibonacci tree · Root of a Fibonacci tree

Used byFibonacci heap minimum deletion agrees with its root-list version

DefinitionDeleting the minimum of a Fibonacci heap#✓fully proved

If the root list of the heap is empty, the result is nothing. Otherwise the first tree of the root list whose root is minimal is removed, and the result is its root value together with the heap whose root list is the consolidation of the removed tree's children followed by the remaining trees, and whose cached minimum is the minimum root of this consolidated forest.

Cslib.Algorithms.Lean.FibonacciHeap.deleteMin · 16 lines

public def deleteMin [LinearOrder α]
    (heap : FibonacciHeap α) : Option (α × FibonacciHeap α) :=
  match found : FibonacciForest.removeMinTree heap.trees with
  | none => none
  | some (minimum, rest) =>
      have spec := FibonacciForest.removeMinTree_spec found
      have minimum_valid : minimum.Valid := heap.valid minimum spec.2.1
      have rest_valid : FibonacciForest.Valid rest := heap.valid.sublist spec.2.2.1
      have children_valid : FibonacciForest.Valid minimum.children :=
        fun _ member => minimum_valid.child_valid member
      have combined_valid : FibonacciForest.Valid (minimum.children ++ rest) :=
        FibonacciForest.valid_append children_valid rest_valid
      let trees := FibonacciForest.consolidate (minimum.children ++ rest)
      have trees_valid : FibonacciForest.Valid trees :=
        FibonacciForest.valid_consolidate combined_valid
      some (minimum.root, ⟨trees, FibonacciForest.minRoot trees, trees_valid, rfl⟩)

Uses 16 · Used by 7

Statement usesValid Fibonacci forests · Sublists of valid Fibonacci forests are valid · Consolidation of a forest · Multiset of a Fibonacci forest · Minimum root of a forest · Removing a minimum tree from a Fibonacci forest · Minimum-tree removal in a Fibonacci forest · Concatenation preserves validity of Fibonacci forests · Consolidation preserves validity · Fibonacci heap · Fibonacci tree · Valid Fibonacci trees · Children of a valid Fibonacci tree are valid · Children of a Fibonacci tree · Multiset of a Fibonacci tree · Root of a Fibonacci tree

Used byFibonacci heap minimum deletion splits off the minimum · Fibonacci heap minimum deletion removes one copy of the minimum · Fibonacci heap minimum deletion fails exactly on the empty heap · Fibonacci heap minimum deletion returns a lower bound · After minimum deletion a Fibonacci heap has at most as many roots as elements · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees · Fibonacci heap minimum deletion agrees with its root-list version

TheoremFibonacci heap minimum deletion agrees with its root-list version#✓fully proved

For every Fibonacci heap \(H\), deleting the minimum of \(H\) and keeping only the returned value and the root list of the resulting heap gives the same result as the root-list minimum deletion applied to the root list of \(H\): either both fail, or both return the same value and the same list of trees.

public theorem deleteMin_trees [LinearOrder α] (heap : FibonacciHeap α) :
    heap.deleteMin.map (fun result => (result.1, result.2.trees)) =
      deleteMinTrees heap.trees

Uses 18

Statement usesFibonacci heap · Deleting the minimum of a Fibonacci heap · Minimum deletion on a forest · Fibonacci tree

Proof usesValid Fibonacci forests · Sublists of valid Fibonacci forests are valid · Consolidation of a forest · Multiset of a Fibonacci forest · Minimum root of a forest · Removing a minimum tree from a Fibonacci forest · Minimum-tree removal in a Fibonacci forest · Concatenation preserves validity of Fibonacci forests · Consolidation preserves validity · Valid Fibonacci trees · Children of a valid Fibonacci tree are valid · Children of a Fibonacci tree · Multiset of a Fibonacci tree · Root of a Fibonacci tree

TheoremThe empty Fibonacci heap has no elements#✓fully proved

The empty Fibonacci heap represents the empty multiset.

public theorem elements_empty [LinearOrder α] : (empty : FibonacciHeap α).elements = 0

Uses 5

Statement usesMultiset of a Fibonacci heap · Empty Fibonacci heap

Proof usesFibonacci heap · Fibonacci tree · Multiset of a Fibonacci tree

TheoremMultiset of a singleton Fibonacci heap#✓fully proved

For every value \(x\) of a linearly ordered type, the singleton Fibonacci heap on \(x\), whose only tree is the single-node tree with root \(x\), represents the multiset \(\{x\}\).

public theorem elements_singleton [LinearOrder α] (value : α) :
    (singleton value).elements = {value}

Uses 6

Statement usesMultiset of a Fibonacci heap · Singleton Fibonacci heap

Proof usesFibonacci heap · Fibonacci tree · Multiset of a Fibonacci tree · One-element Fibonacci heap

TheoremMelding adds the elements#✓fully proved

For any two Fibonacci heaps \(H_1\) and \(H_2\) over a linearly ordered type, the meld of \(H_1\) and \(H_2\) represents the sum of the multisets represented by \(H_1\) and by \(H_2\).

public theorem elements_meld [LinearOrder α] (left right : FibonacciHeap α) :
    (left.meld right).elements = left.elements + right.elements

Uses 5 · Used by 3

Statement usesFibonacci heap · Multiset of a Fibonacci heap · Melding Fibonacci heaps

Proof usesElements of a concatenated forest · Fibonacci tree

Used byMelding adds the sizes of Fibonacci heaps · Insertion adds one occurrence · The union of Fibonacci heaps adds their multisets

TheoremThe union of Fibonacci heaps adds their multisets#✓fully proved

For Fibonacci heaps \(H_1\) and \(H_2\) over a linearly ordered type, the multiset represented by the union of \(H_1\) and \(H_2\) is the sum of the multisets represented by \(H_1\) and by \(H_2\).

public theorem elements_union [LinearOrder α] (left right : FibonacciHeap α) :
    (left.union right).elements = left.elements + right.elements

Uses 4

Statement usesFibonacci heap · Multiset of a Fibonacci heap · Union of Fibonacci heaps

Proof usesMelding adds the elements

TheoremInsertion adds one occurrence#✓fully proved

For every Fibonacci heap \(H\) over a linearly ordered type and every value \(x\), the heap obtained by inserting \(x\) into \(H\) represents the multiset of \(H\) with one more occurrence of \(x\).

public theorem elements_insert [LinearOrder α] (heap : FibonacciHeap α) (value : α) :
    (heap.insert value).elements = value ::ₘ heap.elements

Uses 9 · Used by 1

Statement usesFibonacci heap · Multiset of a Fibonacci heap · Insertion into a Fibonacci heap

Proof usesMelding adds the elements · Melding Fibonacci heaps · Singleton Fibonacci heap · Fibonacci tree · Multiset of a Fibonacci tree · One-element Fibonacci heap

Used byInsertion increases the size of a Fibonacci heap by one

TheoremMelding adds the sizes of Fibonacci heaps#✓fully proved

For Fibonacci heaps \(H_1\) and \(H_2\), the number of elements of the meld of \(H_1\) and \(H_2\), counted with multiplicity, is the number of elements of \(H_1\) plus the number of elements of \(H_2\).

public theorem card_elements_meld [LinearOrder α] (left right : FibonacciHeap α) :
    (left.meld right).elements.card = left.elements.card + right.elements.card

Uses 4

Statement usesFibonacci heap · Multiset of a Fibonacci heap · Melding Fibonacci heaps

Proof usesMelding adds the elements

TheoremInsertion increases the size of a Fibonacci heap by one#✓fully proved

For every Fibonacci heap \(H\) and every value \(x\), the number of elements of the heap obtained by inserting \(x\) into \(H\), counted with multiplicity, is the number of elements of \(H\) plus one.

public theorem card_elements_insert [LinearOrder α] (heap : FibonacciHeap α) (value : α) :
    (heap.insert value).elements.card = heap.elements.card + 1

Uses 4

Statement usesFibonacci heap · Multiset of a Fibonacci heap · Insertion into a Fibonacci heap

Proof usesInsertion adds one occurrence

TheoremFind-min fails exactly on the empty Fibonacci heap#✓fully proved

For a Fibonacci heap \(H\) over a linearly ordered type, find-min on \(H\) returns no value if and only if \(H\) has no trees.

public theorem findMin_eq_none_iff [LinearOrder α] (heap : FibonacciHeap α) :
    heap.findMin = none ↔ heap.trees = []

Uses 5 · Used by 5

Statement usesFibonacci heap · Find-min for Fibonacci heaps · Fibonacci tree

Proof usesMinimum root of a forest · Only the empty forest has no minimum root

Used byDecrease-key in a Fibonacci heap · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Minimum after decrease-key · Root list after decrease-key

TheoremFind-min returns an element of the Fibonacci heap#✓fully proved

Let \(H\) be a Fibonacci heap over a linearly ordered type. If find-min on \(H\) returns \(m\), then \(m\) belongs to the multiset represented by \(H\).

public theorem findMin_mem [LinearOrder α] {heap : FibonacciHeap α} {minimum : α}
    (result : heap.findMin = some minimum) : minimum ∈ heap.elements

Uses 10 · Used by 5

Statement usesFibonacci heap · Multiset of a Fibonacci heap · Find-min for Fibonacci heaps

Proof usesMultiset of a Fibonacci forest · Minimum root of a forest · The minimum root is a least root · Fibonacci tree · Multiset of a Fibonacci tree · Root of a Fibonacci tree · The root of a Fibonacci tree is one of its elements

Used byDecrease-key in a Fibonacci heap · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Minimum after decrease-key · Root list after decrease-key

TheoremFind-min returns a lower bound of the Fibonacci heap#✓fully proved

Let \(H\) be a Fibonacci heap over a linearly ordered type. If find-min on \(H\) returns \(m\), then \(m \le v\) for every value \(v\) in the multiset represented by \(H\).

public theorem findMin_le [LinearOrder α] {heap : FibonacciHeap α} {minimum value : α}
    (result : heap.findMin = some minimum) (member : value ∈ heap.elements) :
    minimum ≤ value

Uses 11 · Used by 5

Statement usesFibonacci heap · Multiset of a Fibonacci heap · Find-min for Fibonacci heaps

Proof usesValid Fibonacci forests · Multiset of a Fibonacci forest · Minimum root of a forest · The minimum root is a least root · Fibonacci tree · Roots of valid Fibonacci trees are lower bounds · Multiset of a Fibonacci tree · Root of a Fibonacci tree

Used byDecrease-key in a Fibonacci heap · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Minimum after decrease-key · Root list after decrease-key

TheoremFibonacci heap minimum deletion fails exactly on the empty heap#✓fully proved

Deleting the minimum of a Fibonacci heap fails if and only if the heap's list of root trees is empty.

public theorem deleteMin_eq_none_iff [LinearOrder α] (heap : FibonacciHeap α) :
    heap.deleteMin = none ↔ heap.trees = []

Uses 17

Statement usesFibonacci heap · Deleting the minimum of a Fibonacci heap · Fibonacci tree

Proof usesValid Fibonacci forests · Sublists of valid Fibonacci forests are valid · Consolidation of a forest · Multiset of a Fibonacci forest · Minimum root of a forest · Removing a minimum tree from a Fibonacci forest · Minimum-tree removal in a Fibonacci forest · Concatenation preserves validity of Fibonacci forests · Consolidation preserves validity · Valid Fibonacci trees · Children of a valid Fibonacci tree are valid · Children of a Fibonacci tree · Multiset of a Fibonacci tree · Root of a Fibonacci tree

TheoremFibonacci heap minimum deletion removes one copy of the minimum#✓fully proved

If deleting the minimum of a Fibonacci heap \(H\) succeeds and returns the value \(m\) and the 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 : FibonacciHeap α} {minimum : α}
    {rest : FibonacciHeap α} (result : heap.deleteMin = some (minimum, rest)) :
    rest.elements = heap.elements.erase minimum

Uses 20

Statement usesFibonacci heap · Deleting the minimum of a Fibonacci heap · Multiset of a Fibonacci heap

Proof usesValid Fibonacci forests · Sublists of valid Fibonacci forests are valid · Consolidation of a forest · Multiset of a Fibonacci forest · Elements of a concatenated forest · Consolidation preserves the elements · Minimum root of a forest · Removing a minimum tree from a Fibonacci forest · Minimum-tree removal in a Fibonacci forest · Concatenation preserves validity of Fibonacci forests · Consolidation preserves validity · Fibonacci tree · Valid Fibonacci trees · Children of a valid Fibonacci tree are valid · Children of a Fibonacci tree · Multiset of a Fibonacci tree · Root of a Fibonacci tree

TheoremFibonacci heap minimum deletion splits off the minimum#✓fully proved

If deleting the minimum of a Fibonacci heap \(H\) succeeds and returns the value \(m\) and the heap \(H'\), then the multiset of elements of \(H\) is the multiset of elements of \(H'\) with one copy of \(m\) added.

public theorem deleteMin_cons_elements [LinearOrder α] {heap : FibonacciHeap α}
    {minimum : α} {rest : FibonacciHeap α}
    (result : heap.deleteMin = some (minimum, rest)) :
    minimum ::ₘ rest.elements = heap.elements

Uses 20

Statement usesFibonacci heap · Deleting the minimum of a Fibonacci heap · Multiset of a Fibonacci heap

Proof usesValid Fibonacci forests · Sublists of valid Fibonacci forests are valid · Consolidation of a forest · Multiset of a Fibonacci forest · Elements of a concatenated forest · Consolidation preserves the elements · Minimum root of a forest · Removing a minimum tree from a Fibonacci forest · Minimum-tree removal in a Fibonacci forest · Concatenation preserves validity of Fibonacci forests · Consolidation preserves validity · Fibonacci tree · Valid Fibonacci trees · Children of a valid Fibonacci tree are valid · Children of a Fibonacci tree · Multiset of a Fibonacci tree · Root of a Fibonacci tree

TheoremFibonacci heap minimum deletion returns a lower bound#✓fully proved

If deleting the minimum of a Fibonacci heap \(H\) succeeds and returns the value \(m\), then \(m \le v\) for every element \(v\) of \(H\).

public theorem deleteMin_le [LinearOrder α] {heap : FibonacciHeap α} {minimum value : α}
    {rest : FibonacciHeap α} (result : heap.deleteMin = some (minimum, rest))
    (member : value ∈ heap.elements) : minimum ≤ value

Uses 19

Statement usesFibonacci heap · Deleting the minimum of a Fibonacci heap · Multiset of a Fibonacci heap

Proof usesValid Fibonacci forests · Sublists of valid Fibonacci forests are valid · Consolidation of a forest · Multiset of a Fibonacci forest · Minimum root of a forest · Removing a minimum tree from a Fibonacci forest · Minimum-tree removal in a Fibonacci forest · Concatenation preserves validity of Fibonacci forests · Consolidation preserves validity · Fibonacci tree · Valid Fibonacci trees · Children of a valid Fibonacci tree are valid · Roots of valid Fibonacci trees are lower bounds · Children of a Fibonacci tree · Multiset of a Fibonacci tree · Root of a Fibonacci tree

TheoremMinimum deletion leaves a Fibonacci heap with strictly increasing root degrees#✓fully proved

If deleting the minimum of a Fibonacci heap succeeds and returns the heap \(H'\), then the degrees of the root trees of \(H'\), in list order, are strictly increasing; consolidation is what makes them so.

public theorem deleteMin_sortedDegrees [LinearOrder α] {heap : FibonacciHeap α}
    {minimum : α} {rest : FibonacciHeap α}
    (result : heap.deleteMin = some (minimum, rest)) :
    FibonacciForest.SortedDegrees rest.trees

Uses 19 · Used by 1

Statement usesForests with strictly increasing degrees · Fibonacci heap · Deleting the minimum of a Fibonacci heap · Fibonacci tree

Proof usesValid Fibonacci forests · Sublists of valid Fibonacci forests are valid · Consolidation of a forest · Consolidation sorts root degrees · Multiset of a Fibonacci forest · Minimum root of a forest · Removing a minimum tree from a Fibonacci forest · Minimum-tree removal in a Fibonacci forest · Concatenation preserves validity of Fibonacci forests · Consolidation preserves validity · Valid Fibonacci trees · Children of a valid Fibonacci tree are valid · Children of a Fibonacci tree · Multiset of a Fibonacci tree · Root of a Fibonacci tree

Used byAfter minimum deletion a Fibonacci heap has at most as many roots as elements

TheoremAfter minimum deletion a Fibonacci heap has at most as many roots as elements#✓fully proved

If deleting the minimum of a Fibonacci heap succeeds and returns the heap \(H'\), then the number of root trees of \(H'\) is at most the number of elements of \(H'\), counted with multiplicity.

public theorem deleteMin_length_le_card [LinearOrder α] {heap : FibonacciHeap α}
    {minimum : α} {rest : FibonacciHeap α}
    (result : heap.deleteMin = some (minimum, rest)) :
    rest.trees.length ≤ rest.elements.card

Uses 7

Statement usesFibonacci heap · Deleting the minimum of a Fibonacci heap · Multiset of a Fibonacci heap · Fibonacci tree

Proof usesValid Fibonacci forests · Degree-sorted forests have at most as many trees as elements · Minimum deletion leaves a Fibonacci heap with strictly increasing root degrees

DefinitionSubtree of a Fibonacci tree at a path#✓fully proved

For a list \(p = (i_1, \dots, i_n)\) of natural numbers and a Fibonacci tree \(t\), the subtree of \(t\) at \(p\) is found by starting at the root and moving to the child with zero-based index \(i_1\), then to its child with index \(i_2\), and so on. The result is absent when some index is at least the number of children of the current node. The empty path addresses the whole tree \(t\).

@[expose] public def subtreeAt : List Nat → FibonacciTree α → Option (FibonacciTree α)
  | [], t => some t
  | i :: p, .node _ _ children => (children[i]?).bind (subtreeAt p)

Uses 1 · Used by 5

Statement usesFibonacci tree

Used byA cut extracts the addressed subtree · Every addressed subtree of a forest can be cut out · Decrease-key replaces one key, stated by address · Subtrees of a valid Fibonacci tree are valid · Every addressed subtree can be cut out

DefinitionCutting a subtree out of a Fibonacci tree#✓fully proved

For a path \(p\) of child indices and a Fibonacci tree \(t\), the cut of \(t\) at \(p\) is either undefined or a pair of an extracted subtree and an optional remainder tree. For the empty path, the extracted subtree is \(t\) and there is no remainder. For a path consisting of an index \(i\) followed by a path \(q\), where \(t\) has root \(r\) and children \(c_0, \dots, c_{k-1}\), the cut is undefined if \(i \ge k\) or if the cut of \(c_i\) at \(q\) is undefined. Otherwise, with \(s\) the subtree extracted from \(c_i\), the extracted subtree is \(s\) and the remainder is the tree with root \(r\) whose children are those of \(t\) with \(c_i\) removed (if the cut of \(c_i\) left no remainder) or with \(c_i\) replaced by that remainder (otherwise), and whose stored degree is its new number of children.

When the cut is defined, there is no remainder exactly when \(p\) is empty.

Cslib.Algorithms.Lean.FibonacciTree.cutAt · 15 lines

@[expose] public def cutAt : List Nat → FibonacciTree α →
    Option (FibonacciTree α × Option (FibonacciTree α))
  | [], t => some (t, none)
  | i :: p, .node _ root children =>
      match children[i]? with
      | none => none
      | some child =>
          match cutAt p child with
          | none => none
          | some (sub, none) =>
              some (sub, some (.node (children.eraseIdx i).length root
                (children.eraseIdx i)))
          | some (sub, some child') =>
              some (sub, some (.node (children.set i child').length root
                (children.set i child')))

Uses 1 · Used by 14

Statement usesFibonacci tree

Used byCutting a subtree splits the elements of a Fibonacci tree · A cut without remainder extracts the whole tree · The remainder of a cut from a valid tree is valid · The subtree extracted by a cut from a valid tree is valid · A cut extracts the addressed subtree · Cutting a subtree out of a Fibonacci forest · Cutting a subtree splits the elements of a Fibonacci forest · Every addressed subtree of a forest can be cut out · Cutting a valid forest leaves valid parts · Decrease-key in a Fibonacci heap · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key · Every addressed subtree can be cut out

DefinitionReplacing the root key of a Fibonacci tree#✓fully proved

For a Fibonacci tree \(t\) and a key \(k\), this is the tree whose root value is \(k\) and whose stored degree and list of children are those of \(t\).

It is used on an extracted subtree with a key no larger than the old root.

@[expose] public def decreaseRoot (t : FibonacciTree α) (newKey : α) : FibonacciTree α :=
  match t with
  | .node degree _ children => .node degree newKey children

Uses 1 · Used by 8

Statement usesFibonacci tree

Used byDecrease-key in a Fibonacci heap · Decrease-key replaces one key · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Minimum after decrease-key · Root list after decrease-key · Lowering the root keeps a Fibonacci tree valid · Elements after replacing the root key

TheoremElements after replacing the root key#✓fully proved

For a Fibonacci tree \(t\) and any key \(k\), the multiset of elements represented by the tree obtained from \(t\) by replacing its root value with \(k\) equals the multiset of elements of \(t\) with one occurrence of the root of \(t\) removed and \(k\) added.

public theorem elements_decreaseRoot [DecidableEq α] (t : FibonacciTree α) (newKey : α) :
    (t.decreaseRoot newKey).elements = newKey ::ₘ t.elements.erase t.root

Uses 4 · Used by 5

Statement usesFibonacci tree · Replacing the root key of a Fibonacci tree · Multiset of a Fibonacci tree · Root of a Fibonacci tree

Used byDecrease-key in a Fibonacci heap · Decrease-key replaces one key · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key

TheoremLowering the root keeps a Fibonacci tree valid#✓fully proved

Let \(T\) be a valid Fibonacci tree over a preordered type and let \(k\) be a key that is at most the root of \(T\). Then the tree obtained from \(T\) by replacing its root by \(k\), keeping its degree and children, is valid: the new root is still no greater than every represented element.

public theorem Valid.decreaseRoot [Preorder α] {t : FibonacciTree α} (hv : Valid t)
    {newKey : α} (hle : newKey ≤ t.root) : Valid (t.decreaseRoot newKey)

Uses 8 · Used by 4

Statement usesFibonacci tree · Valid Fibonacci trees · Replacing the root key of a Fibonacci tree · Root of a Fibonacci tree

Proof usesChildren of a valid Fibonacci tree are valid · The degree of a valid Fibonacci tree is its number of children · Roots of valid Fibonacci trees are lower bounds · Multiset of a Fibonacci tree

Used byDecrease-key in a Fibonacci heap · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key

TheoremSubtrees of a valid Fibonacci tree are valid#✓fully proved

If a Fibonacci tree \(t\) is valid and a path \(p\) of child indices addresses a subtree \(s\) of \(t\), then \(s\) is valid.

public theorem Valid.subtreeAt [LE α] {t sub : FibonacciTree α} (hv : Valid t)
    {p : List Nat} (h : subtreeAt p t = some sub) : Valid sub

Uses 5 · Used by 1

Statement usesFibonacci tree · Valid Fibonacci trees · Subtree of a Fibonacci tree at a path

Proof usesChildren of a valid Fibonacci tree are valid · Children of a Fibonacci tree

Used byThe subtree extracted by a cut from a valid tree is valid

TheoremA cut extracts the addressed subtree#✓fully proved

Let \(t\) be a Fibonacci tree and \(p\) a path of child indices. If cutting \(t\) at \(p\) extracts a subtree \(s\) (with or without a remainder), then \(s\) is the subtree of \(t\) at \(p\).

public theorem cutAt_subtreeAt {p : List Nat} {t sub : FibonacciTree α}
    {rem : Option (FibonacciTree α)} (h : cutAt p t = some (sub, rem)) :
    subtreeAt p t = some sub

Uses 3 · Used by 1

Statement usesFibonacci tree · Cutting a subtree out of a Fibonacci tree · Subtree of a Fibonacci tree at a path

Used byThe subtree extracted by a cut from a valid tree is valid

TheoremEvery addressed subtree can be cut out#✓fully proved

If a path \(p\) of child indices addresses a subtree \(s\) of a Fibonacci tree \(t\), then cutting \(t\) at \(p\) succeeds and extracts exactly \(s\), together with some remainder, which may be absent.

public theorem subtreeAt_cutAt {p : List Nat} {t sub : FibonacciTree α}
    (h : subtreeAt p t = some sub) : ∃ rem, cutAt p t = some (sub, rem)

Uses 3 · Used by 1

Statement usesFibonacci tree · Cutting a subtree out of a Fibonacci tree · Subtree of a Fibonacci tree at a path

Used byEvery addressed subtree of a forest can be cut out

TheoremA cut without remainder extracts the whole tree#✓fully proved

Let \(t\) be a Fibonacci tree and \(p\) a path of child indices. If cutting \(t\) at \(p\) extracts a subtree \(s\) and leaves no remainder, then \(s = t\).

public theorem cutAt_eq_self {p : List Nat} {t sub : FibonacciTree α}
    (h : cutAt p t = some (sub, none)) : sub = t

Uses 2 · Used by 2

Statement usesFibonacci tree · Cutting a subtree out of a Fibonacci tree

Used byCutting a subtree splits the elements of a Fibonacci tree · Cutting a subtree splits the elements of a Fibonacci forest

TheoremCutting a subtree splits the elements of a Fibonacci tree#✓fully proved

Let \(t\) be a Fibonacci tree and \(p\) a path of child indices. If cutting \(t\) at \(p\) extracts a subtree \(s\) and leaves a remainder tree \(t'\), then the multiset of elements of \(t\) is the sum of the multisets of elements of \(t'\) and of \(s\).

public theorem cutAt_elements {p : List Nat} {t sub t' : FibonacciTree α}
    (h : cutAt p t = some (sub, some t')) :
    t.elements = t'.elements + sub.elements

Uses 4 · Used by 2

Statement usesFibonacci tree · Cutting a subtree out of a Fibonacci tree · Multiset of a Fibonacci tree

Proof usesA cut without remainder extracts the whole tree

Used byThe remainder of a cut from a valid tree is valid · Cutting a subtree splits the elements of a Fibonacci forest

TheoremThe subtree extracted by a cut from a valid tree is valid#✓fully proved

Let \(t\) be a valid Fibonacci tree over a type with a relation \(\le\), and \(p\) a path of child indices. If cutting \(t\) at \(p\) extracts a subtree \(s\) (with or without a remainder), then \(s\) is valid.

public theorem cutAt_sub_valid [LE α] {p : List Nat} {t sub : FibonacciTree α}
    {rem : Option (FibonacciTree α)} (hv : Valid t)
    (h : cutAt p t = some (sub, rem)) : Valid sub

Uses 5 · Used by 1

Statement usesFibonacci tree · Valid Fibonacci trees · Cutting a subtree out of a Fibonacci tree

Proof usesSubtrees of a valid Fibonacci tree are valid · A cut extracts the addressed subtree

Used byCutting a valid forest leaves valid parts

TheoremThe remainder of a cut from a valid tree is valid#✓fully proved

Let \(t\) be a valid Fibonacci tree over a type with a relation \(\le\), and \(p\) a path of child indices. If cutting \(t\) at \(p\) extracts a subtree and leaves a remainder tree \(t'\), then \(t'\) is valid: its children are valid, its stored degree equals its number of children, and its root is \(\le\) every element of \(t'\).

public theorem cutAt_remainder_valid [LE α] {p : List Nat} {t sub t' : FibonacciTree α}
    (hv : Valid t) (h : cutAt p t = some (sub, some t')) : Valid t'

Uses 8 · Used by 1

Statement usesFibonacci tree · Valid Fibonacci trees · Cutting a subtree out of a Fibonacci tree

Proof usesChildren of a valid Fibonacci tree are valid · Roots of valid Fibonacci trees are lower bounds · Children of a Fibonacci tree · Cutting a subtree splits the elements of a Fibonacci tree · Multiset of a Fibonacci tree

Used byCutting a valid forest leaves valid parts

DefinitionCutting a subtree out of a Fibonacci forest#✓fully proved

For a forest given as a list of Fibonacci trees, an index \(i\) and a path \(p\) of child indices, the cut is undefined if the list has no tree at position \(i\) (counting from \(0\)) or if cutting that tree \(t\) at \(p\) is undefined. Otherwise, if cutting \(t\) at \(p\) extracts the subtree \(s\), the result is \(s\) together with the list in which the tree at position \(i\) is removed (if the cut of \(t\) left no remainder) or replaced by the remainder (otherwise).

@[expose] public def cutTreeAt (trees : List (FibonacciTree α)) (i : Nat) (p : List Nat) :
    Option (FibonacciTree α × List (FibonacciTree α)) :=
  match trees[i]? with
  | none => none
  | some t =>
      match t.cutAt p with
      | none => none
      | some (sub, none) => some (sub, trees.eraseIdx i)
      | some (sub, some t') => some (sub, trees.set i t')

Uses 2 · Used by 11

Statement usesFibonacci tree · Cutting a subtree out of a Fibonacci tree

Used byCutting a subtree splits the elements of a Fibonacci forest · Every addressed subtree of a forest can be cut out · Cutting a valid forest leaves valid parts · Decrease-key in a Fibonacci heap · Decrease-key preserves the number of elements · Decrease-key replaces one key · Decrease-key replaces one key, stated by address · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Minimum after decrease-key · Root list after decrease-key

TheoremCutting a subtree splits the elements of a Fibonacci forest#✓fully proved

Let \(F\) be a forest of Fibonacci trees, \(i\) an index and \(p\) a path of child indices. If cutting \(F\) at the \(i\)-th tree and path \(p\) extracts a subtree \(s\) and leaves the forest \(F'\), then the multiset of elements of \(F\) is the sum of the multisets of elements of \(F'\) and of \(s\).

public theorem cutTreeAt_elements {trees : List (FibonacciTree α)} {i : Nat} {p : List Nat}
    {sub : FibonacciTree α} {rest : List (FibonacciTree α)}
    (h : cutTreeAt trees i p = some (sub, rest)) :
    elements trees = elements rest + sub.elements

Uses 7 · Used by 6

Statement usesCutting a subtree out of a Fibonacci forest · Multiset of a Fibonacci forest · Fibonacci tree · Multiset of a Fibonacci tree

Proof usesCutting a subtree out of a Fibonacci tree · Cutting a subtree splits the elements of a Fibonacci tree · A cut without remainder extracts the whole tree

Used byDecrease-key in a Fibonacci heap · Decrease-key preserves the number of elements · Decrease-key replaces one key · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key

TheoremCutting a valid forest leaves valid parts#✓fully proved

Let \(F\) be a valid forest of Fibonacci trees over a type with a relation \(\le\), \(i\) an index and \(p\) a path of child indices. If cutting \(F\) at index \(i\) and path \(p\) extracts a subtree \(s\) and leaves the forest \(F'\), then \(s\) is a valid tree and \(F'\) is a valid forest.

public theorem cutTreeAt_valid [LE α] {trees : List (FibonacciTree α)} {i : Nat}
    {p : List Nat} {sub : FibonacciTree α} {rest : List (FibonacciTree α)}
    (hv : Valid trees) (h : cutTreeAt trees i p = some (sub, rest)) :
    sub.Valid ∧ Valid rest

Uses 7 · Used by 4

Statement usesValid Fibonacci forests · Cutting a subtree out of a Fibonacci forest · Fibonacci tree · Valid Fibonacci trees

Proof usesCutting a subtree out of a Fibonacci tree · The remainder of a cut from a valid tree is valid · The subtree extracted by a cut from a valid tree is valid

Used byDecrease-key in a Fibonacci heap · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Root list after decrease-key

TheoremEvery addressed subtree of a forest can be cut out#✓fully proved

Let \(F\) be a forest of Fibonacci trees whose tree at position \(i\) is \(t\), and let \(p\) be a path of child indices such that the subtree of \(t\) at \(p\) is \(s\). Then cutting \(F\) at index \(i\) and path \(p\) is defined and extracts \(s\), together with some remaining forest.

public theorem cutTreeAt_of_subtreeAt {trees : List (FibonacciTree α)} {i : Nat}
    {p : List Nat} {t sub : FibonacciTree α} (htree : trees[i]? = some t)
    (hpath : t.subtreeAt p = some sub) :
    ∃ rest, cutTreeAt trees i p = some (sub, rest)

Uses 5 · Used by 1

Statement usesCutting a subtree out of a Fibonacci forest · Fibonacci tree · Subtree of a Fibonacci tree at a path

Proof usesCutting a subtree out of a Fibonacci tree · Every addressed subtree can be cut out

Used byDecrease-key replaces one key, stated by address

DefinitionDecrease-key in a Fibonacci heap#✓fully proved

Given a Fibonacci heap \(H\) over a linearly ordered type, a root index \(i\), a path \(p\) of child indices and a key \(k\), decrease-key cuts the subtree \(S\) at path \(p\) out of the \(i\)-th tree of the root list of \(H\), replaces the root of \(S\) by \(k\), and puts the resulting tree in front of the remaining forest (the root list with the \(i\)-th tree replaced by what is left of it after the cut, or removed when \(S\) is that whole tree). The cached minimum of the result is the smaller of \(k\) and the previous cached minimum, computed without rescanning the root list. When the cut fails (the address does not resolve) or \(k\) is greater than the root of \(S\), the heap \(H\) is returned unchanged.

Unlike CLRS decrease-key, this performs no cascading cuts: the trees carry no mark field.

Cslib.Algorithms.Lean.FibonacciHeap.decreaseKey · 70 lines

public def decreaseKey [LinearOrder α] (heap : FibonacciHeap α) (i : Nat) (p : List Nat)
    (newKey : α) : FibonacciHeap α :=
  match found : FibonacciForest.cutTreeAt heap.trees i p with
  | none => heap
  | some (sub, rest) =>
      if hle : newKey ≤ sub.root then
        have hv := FibonacciForest.cutTreeAt_valid heap.valid found
        let trees := sub.decreaseRoot newKey :: rest
        have trees_valid : FibonacciForest.Valid trees := by
          intro t ht
          have ht' : t ∈ sub.decreaseRoot newKey :: rest := ht
          rw [List.mem_cons] at ht'
          rcases ht' with rfl | ht'
          · exact hv.1.decreaseRoot hle
          · exact hv.2 t ht'
        let newMin : Option α := match heap.cachedMin with
          | none => some newKey
          | some m => some (min newKey m)
        have hmin : newMin = FibonacciForest.minRoot trees := by
          have hElemTrees : FibonacciForest.elements trees =
              newKey ::ₘ (FibonacciForest.elements heap.trees).erase sub.root := by
            have hElem := FibonacciForest.cutTreeAt_elements found
            show FibonacciForest.elements (sub.decreaseRoot newKey :: rest) = _
            rw [hElem,
              Multiset.erase_add_right_pos _ (FibonacciTree.root_mem_elements sub)]
            change (sub.decreaseRoot newKey).elements +
                FibonacciForest.elements rest = _
            rw [FibonacciTree.elements_decreaseRoot, Multiset.cons_add,
              Multiset.add_comm (sub.elements.erase sub.root)]
          cases hc : heap.cachedMin with
          | none =>
              exfalso
              have hfind : heap.findMin = none := hc
              have htrees : heap.trees = [] := (findMin_eq_none_iff heap).mp hfind
              rw [htrees] at found
              simp [FibonacciForest.cutTreeAt] at found
          | some m =>
              have hnew : newMin = some (min newKey m) := by
                show (match heap.cachedMin with
                  | none => some newKey
                  | some m' => some (min newKey m')) = some (min newKey m)
                rw [hc]
              have hfind : heap.findMin = some m := hc
              have hmMem : m ∈ heap.elements := findMin_mem hfind
              change m ∈ FibonacciForest.elements heap.trees at hmMem
              have hmem : min newKey m ∈ FibonacciForest.elements trees := by
                by_cases hm : m = sub.root
                · have hmin' : min newKey m = newKey :=
                    min_eq_left (hm ▸ hle)
                  rw [hElemTrees, hmin']
                  exact Multiset.mem_cons_self _ _
                · rw [hElemTrees]
                  rcases le_total newKey m with hnm | hnm
                  · rw [min_eq_left hnm]
                    exact Multiset.mem_cons_self _ _
                  · rw [min_eq_right hnm]
                    exact Multiset.mem_cons_of_mem
                      ((Multiset.mem_erase_of_ne hm).mpr hmMem)
              have hleast : ∀ y ∈ FibonacciForest.elements trees,
                  min newKey m ≤ y := by
                intro y hy
                rw [hElemTrees] at hy
                rcases Multiset.mem_cons.mp hy with rfl | hy
                · exact min_le_left _ _
                · exact (min_le_right newKey m).trans
                    (findMin_le hfind (Multiset.mem_of_mem_erase hy))
              rw [hnew]
              exact (minRoot_eq_some_of_least trees_valid hmem hleast).symm
        ⟨trees, newMin, trees_valid, hmin⟩
      else heap

Uses 22 · Used by 8

Statement usesValid Fibonacci forests · Cutting a subtree out of a Fibonacci forest · Cutting a subtree splits the elements of a Fibonacci forest · Cutting a valid forest leaves valid parts · Multiset of a Fibonacci forest · Minimum root of a forest · Only the empty forest has no minimum root · Fibonacci heap · Multiset of a Fibonacci heap · Find-min for Fibonacci heaps · Find-min fails exactly on the empty Fibonacci heap · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap · Fibonacci tree · Valid Fibonacci trees · Lowering the root keeps a Fibonacci tree valid · Cutting a subtree out of a Fibonacci tree · Replacing the root key of a Fibonacci tree · Multiset of a Fibonacci tree · Elements after replacing the root key · Root of a Fibonacci tree · The root of a Fibonacci tree is one of its elements

Used byDecrease-key preserves the number of elements · Decrease-key replaces one key · Decrease-key replaces one key, stated by address · Decrease-key at an unresolved address does nothing · Decrease-key with a larger key does nothing · Minimum after decrease-key · Root list after decrease-key · Decrease-key yields a valid forest

TheoremRoot list after decrease-key#✓fully proved

Let \(H\) be a Fibonacci heap, \(i\) a root index, \(p\) a path of child indices and \(k\) a key. Suppose that cutting the subtree at path \(p\) out of the \(i\)-th tree of the root list of \(H\) succeeds, extracting the subtree \(S\) and leaving the forest \(R\), and that \(k\) is at most the root of \(S\). Then the root list of the heap obtained from \(H\) by decreasing the key at root index \(i\) and path \(p\) to \(k\) consists of \(S\) with its root replaced by \(k\), followed by the trees of \(R\) in order.

public theorem decreaseKey_trees_of_cut [LinearOrder α] {heap : FibonacciHeap α}
    {i : Nat} {p : List Nat} {newKey : α} {sub : FibonacciTree α}
    {rest : List (FibonacciTree α)}
    (hcut : FibonacciForest.cutTreeAt heap.trees i p = some (sub, rest))
    (hle : newKey ≤ sub.root) :
    (heap.decreaseKey i p newKey).trees = sub.decreaseRoot newKey :: rest

Uses 23 · Used by 2

Statement usesCutting a subtree out of a Fibonacci forest · Fibonacci heap · Decrease-key in a Fibonacci heap · Fibonacci tree · Replacing the root key of a Fibonacci tree · Root of a Fibonacci tree

Proof usesValid Fibonacci forests · Cutting a subtree splits the elements of a Fibonacci forest · Cutting a valid forest leaves valid parts · Multiset of a Fibonacci forest · Minimum root of a forest · Only the empty forest has no minimum root · Multiset of a Fibonacci heap · Find-min for Fibonacci heaps · Find-min fails exactly on the empty Fibonacci heap · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap · Valid Fibonacci trees · Lowering the root keeps a Fibonacci tree valid · Cutting a subtree out of a Fibonacci tree · Multiset of a Fibonacci tree · Elements after replacing the root key · The root of a Fibonacci tree is one of its elements

Used byDecrease-key replaces one key · Minimum after decrease-key

TheoremDecrease-key at an unresolved address does nothing#✓fully proved

Let \(H\) be a Fibonacci heap, \(i\) a root index and \(p\) a path of child indices. If cutting the subtree at path \(p\) out of the \(i\)-th tree of the root list of \(H\) fails, then for every key \(k\), decreasing the key at root index \(i\) and path \(p\) to \(k\) returns \(H\) unchanged.

public theorem decreaseKey_eq_self_of_cut_none [LinearOrder α] {heap : FibonacciHeap α}
    {i : Nat} {p : List Nat} {newKey : α}
    (hcut : FibonacciForest.cutTreeAt heap.trees i p = none) :
    heap.decreaseKey i p newKey = heap

Uses 23

Statement usesCutting a subtree out of a Fibonacci forest · Fibonacci heap · Decrease-key in a Fibonacci heap · Fibonacci tree

Proof usesValid Fibonacci forests · Cutting a subtree splits the elements of a Fibonacci forest · Cutting a valid forest leaves valid parts · Multiset of a Fibonacci forest · Minimum root of a forest · Only the empty forest has no minimum root · Multiset of a Fibonacci heap · Find-min for Fibonacci heaps · Find-min fails exactly on the empty Fibonacci heap · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap · Valid Fibonacci trees · Lowering the root keeps a Fibonacci tree valid · Cutting a subtree out of a Fibonacci tree · Replacing the root key of a Fibonacci tree · Multiset of a Fibonacci tree · Elements after replacing the root key · Root of a Fibonacci tree · The root of a Fibonacci tree is one of its elements

TheoremDecrease-key with a larger key does nothing#✓fully proved

Let \(H\) be a Fibonacci heap, \(i\) a root index, \(p\) a path of child indices and \(k\) a key. Suppose that cutting the subtree at path \(p\) out of the \(i\)-th tree of the root list of \(H\) succeeds and extracts the subtree \(S\), and that \(k\) is not at most the root of \(S\) (keys are linearly ordered, so \(k\) is greater than that root). Then decreasing the key at root index \(i\) and path \(p\) to \(k\) returns \(H\) unchanged.

public theorem decreaseKey_eq_self_of_not_le [LinearOrder α] {heap : FibonacciHeap α}
    {i : Nat} {p : List Nat} {newKey : α} {sub : FibonacciTree α}
    {rest : List (FibonacciTree α)}
    (hcut : FibonacciForest.cutTreeAt heap.trees i p = some (sub, rest))
    (hle : ¬ newKey ≤ sub.root) :
    heap.decreaseKey i p newKey = heap

Uses 23

Statement usesCutting a subtree out of a Fibonacci forest · Fibonacci heap · Decrease-key in a Fibonacci heap · Fibonacci tree · Root of a Fibonacci tree

Proof usesValid Fibonacci forests · Cutting a subtree splits the elements of a Fibonacci forest · Cutting a valid forest leaves valid parts · Multiset of a Fibonacci forest · Minimum root of a forest · Only the empty forest has no minimum root · Multiset of a Fibonacci heap · Find-min for Fibonacci heaps · Find-min fails exactly on the empty Fibonacci heap · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap · Valid Fibonacci trees · Lowering the root keeps a Fibonacci tree valid · Cutting a subtree out of a Fibonacci tree · Replacing the root key of a Fibonacci tree · Multiset of a Fibonacci tree · Elements after replacing the root key · The root of a Fibonacci tree is one of its elements

TheoremDecrease-key replaces one key#✓fully proved

Let \(H\) be a Fibonacci heap, \(i\) a root index, \(p\) a path of child indices and \(k\) a key. Suppose that cutting the subtree at path \(p\) out of the \(i\)-th tree of the root list of \(H\) succeeds and extracts the subtree \(S\), and that \(k\) is at most the root of \(S\). Then the multiset represented by the heap obtained from \(H\) by decreasing the key at root index \(i\) and path \(p\) to \(k\) is the multiset represented by \(H\) with one occurrence of the root of \(S\) removed and one occurrence of \(k\) added.

public theorem decreaseKey_elements [LinearOrder α] {heap : FibonacciHeap α} {i : Nat}
    {p : List Nat} {newKey : α} {sub : FibonacciTree α} {rest : List (FibonacciTree α)}
    (hcut : FibonacciForest.cutTreeAt heap.trees i p = some (sub, rest))
    (hle : newKey ≤ sub.root) :
    (heap.decreaseKey i p newKey).elements =
      newKey ::ₘ heap.elements.erase sub.root

Uses 13 · Used by 3

Statement usesCutting a subtree out of a Fibonacci forest · Fibonacci heap · Decrease-key in a Fibonacci heap · Multiset of a Fibonacci heap · Fibonacci tree · Root of a Fibonacci tree

Proof usesCutting a subtree splits the elements of a Fibonacci forest · Multiset of a Fibonacci forest · Root list after decrease-key · Replacing the root key of a Fibonacci tree · Multiset of a Fibonacci tree · Elements after replacing the root key · The root of a Fibonacci tree is one of its elements

Used byDecrease-key preserves the number of elements · Decrease-key replaces one key, stated by address · Minimum after decrease-key

TheoremDecrease-key replaces one key, stated by address#✓fully proved

Let \(H\) be a Fibonacci heap, let \(T\) be the \(i\)-th tree of its root list, and let \(S\) be the subtree of \(T\) at the path \(p\) of child indices. If the key \(k\) is at most the root of \(S\), then the multiset represented by the heap obtained from \(H\) by decreasing the key at root index \(i\) and path \(p\) to \(k\) is the multiset represented by \(H\) with one occurrence of the root of \(S\) removed and one occurrence of \(k\) added.

public theorem decreaseKey_elements_of_subtreeAt [LinearOrder α]
    {heap : FibonacciHeap α} {i : Nat} {p : List Nat} {newKey : α}
    {t sub : FibonacciTree α} (htree : heap.trees[i]? = some t)
    (hpath : t.subtreeAt p = some sub) (hle : newKey ≤ sub.root) :
    (heap.decreaseKey i p newKey).elements =
      newKey ::ₘ heap.elements.erase sub.root

Uses 9

Statement usesFibonacci heap · Decrease-key in a Fibonacci heap · Multiset of a Fibonacci heap · Fibonacci tree · Root of a Fibonacci tree · Subtree of a Fibonacci tree at a path

Proof usesCutting a subtree out of a Fibonacci forest · Every addressed subtree of a forest can be cut out · Decrease-key replaces one key

TheoremDecrease-key preserves the number of elements#✓fully proved

Let \(H\) be a Fibonacci heap, \(i\) a root index, \(p\) a path of child indices and \(k\) a key. Suppose that cutting the subtree at path \(p\) out of the \(i\)-th tree of the root list of \(H\) succeeds and extracts the subtree \(S\), and that \(k\) is at most the root of \(S\). Then the multiset represented by the heap obtained from \(H\) by decreasing the key at root index \(i\) and path \(p\) to \(k\) has the same number of elements, counted with multiplicity, as the multiset represented by \(H\).

public theorem decreaseKey_card_elements [LinearOrder α] {heap : FibonacciHeap α}
    {i : Nat} {p : List Nat} {newKey : α} {sub : FibonacciTree α}
    {rest : List (FibonacciTree α)}
    (hcut : FibonacciForest.cutTreeAt heap.trees i p = some (sub, rest))
    (hle : newKey ≤ sub.root) :
    (heap.decreaseKey i p newKey).elements.card = heap.elements.card

Uses 11

Statement usesCutting a subtree out of a Fibonacci forest · Fibonacci heap · Decrease-key in a Fibonacci heap · Multiset of a Fibonacci heap · Fibonacci tree · Root of a Fibonacci tree

Proof usesCutting a subtree splits the elements of a Fibonacci forest · Multiset of a Fibonacci forest · Decrease-key replaces one key · Multiset of a Fibonacci tree · The root of a Fibonacci tree is one of its elements

TheoremMinimum after decrease-key#✓fully proved

Let \(H\) be a Fibonacci heap whose minimum, as returned by find-min, is \(m\), and let \(i\) be a root index, \(p\) a path of child indices and \(k\) a key. Suppose that cutting the subtree at path \(p\) out of the \(i\)-th tree of the root list of \(H\) succeeds and extracts the subtree \(S\), and that \(k\) is at most the root of \(S\). Then find-min on the heap obtained from \(H\) by decreasing the key at root index \(i\) and path \(p\) to \(k\) returns \(\min(k, m)\).

public theorem decreaseKey_findMin [LinearOrder α] {heap : FibonacciHeap α} {i : Nat}
    {p : List Nat} {newKey m : α} {sub : FibonacciTree α}
    {rest : List (FibonacciTree α)}
    (hcut : FibonacciForest.cutTreeAt heap.trees i p = some (sub, rest))
    (hle : newKey ≤ sub.root) (hmin : heap.findMin = some m) :
    (heap.decreaseKey i p newKey).findMin = some (min newKey m)

Uses 13

Statement usesCutting a subtree out of a Fibonacci forest · Fibonacci heap · Decrease-key in a Fibonacci heap · Find-min for Fibonacci heaps · Fibonacci tree · Root of a Fibonacci tree

Proof usesDecrease-key replaces one key · Root list after decrease-key · Multiset of a Fibonacci heap · Find-min fails exactly on the empty Fibonacci heap · Find-min returns a lower bound of the Fibonacci heap · Find-min returns an element of the Fibonacci heap · Replacing the root key of a Fibonacci tree

TheoremDecrease-key yields a valid forest#✓fully proved

For every Fibonacci heap \(H\), root index \(i\), path \(p\) of child indices and key \(k\), the root list of the heap obtained from \(H\) by decreasing the key at root index \(i\) and path \(p\) to \(k\) is a valid forest, that is, every tree in it is valid.

This holds by construction: every Fibonacci heap carries a valid forest.

public theorem decreaseKey_valid [LinearOrder α] (heap : FibonacciHeap α) (i : Nat)
    (p : List Nat) (newKey : α) :
    FibonacciForest.Valid (heap.decreaseKey i p newKey).trees

Uses 4

Statement usesValid Fibonacci forests · Fibonacci heap · Decrease-key in a Fibonacci heap · Fibonacci tree

91 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.