Disjoint-set data structure

StructureParent forest with a depth certificate#✓fully proved

A parent forest on the vertices \(\{0, \dots, n-1\}\) consists of a parent map \(p\) from the vertices to themselves (a vertex \(x\) with \(p(x) = x\) is a root) and a depth certificate \(d\) assigning a natural number to every vertex, such that every non-root edge strictly decreases the certificate: if \(p(x) \ne x\), then \(d(p(x)) < d(x)\).

public structure Forest (n : Nat) where
  /-- Parent pointer for every vertex; roots point to themselves. -/
  parent : Fin n → Fin n
  /-- A certificate bounding the remaining parent-path length. -/
  depth : Fin n → Nat
  /-- Every non-root edge strictly decreases the depth certificate. -/
  parent_lt : ∀ x, parent x ≠ x → depth (parent x) < depth x

Used by 32

Used byEquivalent vertices of a parent forest · Equivalence after a union · Root of a vertex in a parent forest · Every vertex is equivalent to its representative · Find returns a root · Find is unchanged along a parent pointer · Representatives after a union · Union preserves the representatives of unrelated classes · Find with cost · The cost of find is the path length plus one · The cost of find is at most the depth certificate plus one · Linking two roots of a parent forest · Depth certificate after linking two roots · Parent map after linking two roots · Path length to the root · Union in a union-find forest · Union of equivalent vertices changes nothing · Union makes its arguments equivalent · Union in a parent forest with cost · Cost bound for union in a parent forest · Greedy cut property of Kruskal's scan · Discrete parent forest · Kruskal's algorithm · Kruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal accepts light edges · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · Kruskal scan state · One Kruskal step

DefinitionRoot of a vertex in a parent forest#✓fully proved

For a parent forest \(F\) with parent map \(p\) and a vertex \(x\), the root of \(x\) is found by following parent pointers from \(x\): it is \(x\) itself if \(p(x) = x\), and otherwise it is the root of \(p(x)\).

public def find {n : Nat} (forest : Forest n) (x : Fin n) : Fin n :=
  if _h : forest.parent x = x then x else find forest (forest.parent x)
termination_by forest.depth x
decreasing_by exact forest.parent_lt x _h

Uses 1 · Used by 22

Statement usesParent forest with a depth certificate

Used byEquivalent vertices of a parent forest · Equivalence after a union · Every vertex is equivalent to its representative · Find returns a root · Find is unchanged along a parent pointer · Representatives after a union · Union preserves the representatives of unrelated classes · Find with cost · Linking two roots of a parent forest · Depth certificate after linking two roots · Union in a union-find forest · Union of equivalent vertices changes nothing · Union makes its arguments equivalent · Union in a parent forest with cost · Cost bound for union in a parent forest · Kruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · One Kruskal step

DefinitionPath length to the root#✓fully proved

For a parent forest \(F\) with parent map \(p\) and a vertex \(x\), the path length of \(x\) is the number of parent edges followed from \(x\) to its root: it is \(0\) if \(p(x) = x\), and otherwise one more than the path length of \(p(x)\).

public def pathLength {n : Nat} (forest : Forest n) (x : Fin n) : Nat :=
  if h : forest.parent x = x then 0 else pathLength forest (forest.parent x) + 1
termination_by forest.depth x
decreasing_by exact forest.parent_lt x h

Uses 1 · Used by 3

Statement usesParent forest with a depth certificate

Used byFind with cost · The cost of find is the path length plus one · The cost of find is at most the depth certificate plus one

DefinitionFind with cost#✓fully proved

For a vertex \(x\) of a parent forest \(F\), find with cost returns the root that find returns for \(x\), together with the cost \(\ell(x) + 1\), where \(\ell(x)\) is the path length of \(x\) (the number of non-root parent edges that find traverses from \(x\)). That is, it charges one unit for every visited vertex, including the root.

public def findWithCost {n : Nat} (forest : Forest n) (x : Fin n) : TimeM Nat (Fin n) :=
  ⟨find forest x, pathLength forest x + 1⟩

Uses 3 · Used by 4

Statement usesParent forest with a depth certificate · Root of a vertex in a parent forest · Path length to the root

Used byThe cost of find is the path length plus one · The cost of find is at most the depth certificate plus one · Union in a parent forest with cost · Cost bound for union in a parent forest

DefinitionEquivalent vertices of a parent forest#✓fully proved

Two vertices \(x\) and \(y\) of a parent forest \(F\) are equivalent when find returns the same root for \(x\) as for \(y\) in \(F\).

public def Equivalent {n : Nat} (forest : Forest n) (x y : Fin n) : Prop :=
  find forest x = find forest y

Uses 2 · Used by 17

Statement usesParent forest with a depth certificate · Root of a vertex in a parent forest

Used byEquivalence after a union · Every vertex is equivalent to its representative · Representatives after a union · Union preserves the representatives of unrelated classes · Linking two roots of a parent forest · Depth certificate after linking two roots · Union of equivalent vertices changes nothing · Union makes its arguments equivalent · Greedy cut property of Kruskal's scan · Kruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal accepts light edges · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · One Kruskal step

TheoremFind returns a root#✓fully proved

For every vertex \(x\) of a parent forest \(F\), the vertex \(r\) that find returns for \(x\) is a root of \(F\): the parent of \(r\) in \(F\) is \(r\) itself.

public theorem find_isRoot {n : Nat} (forest : Forest n) (x : Fin n) :
    forest.parent (find forest x) = find forest x

Uses 2 · Used by 4

Statement usesParent forest with a depth certificate · Root of a vertex in a parent forest

Used byEvery vertex is equivalent to its representative · Representatives after a union · Union in a union-find forest · Union of equivalent vertices changes nothing

TheoremFind is unchanged along a parent pointer#✓fully proved

For every vertex \(x\) of a parent forest \(F\), find returns the same root for the parent of \(x\) in \(F\) as for \(x\).

public theorem find_parent {n : Nat} (forest : Forest n) (x : Fin n) :
    find forest (forest.parent x) = find forest x

Uses 2 · Used by 2

Statement usesParent forest with a depth certificate · Root of a vertex in a parent forest

Used byRepresentatives after a union · Linking two roots of a parent forest

TheoremEvery vertex is equivalent to its representative#✓fully proved

For every vertex \(x\) of a parent forest \(F\), the vertex \(x\) is equivalent in \(F\) to the root that find returns for \(x\).

public theorem find_in_class {n : Nat} (forest : Forest n) (x : Fin n) :
    Equivalent forest x (find forest x)

Uses 4

Statement usesEquivalent vertices of a parent forest · Parent forest with a depth certificate · Root of a vertex in a parent forest

Proof usesFind returns a root

TheoremThe cost of find is the path length plus one#✓fully proved

For every vertex \(x\) of a parent forest \(F\), the cost that find with cost charges on \(x\) equals \(\ell(x) + 1\), where \(\ell(x)\) is the path length of \(x\): the number of non-root parent edges that find traverses from \(x\).

public theorem findWithCost_time {n : Nat} (forest : Forest n) (x : Fin n) :
    (findWithCost forest x).time = pathLength forest x + 1

Uses 3 · Used by 1

Statement usesParent forest with a depth certificate · Find with cost · Path length to the root

Used byThe cost of find is at most the depth certificate plus one

TheoremThe cost of find is at most the depth certificate plus one#✓fully proved

For every vertex \(x\) of a parent forest \(F\) with depth certificate \(d\), the cost that find with cost charges on \(x\) is at most \(d(x) + 1\).

public theorem findWithCost_time_le_depth {n : Nat} (forest : Forest n) (x : Fin n) :
  (findWithCost forest x).time ≤ forest.depth x + 1

Uses 4 · Used by 1

Statement usesParent forest with a depth certificate · Find with cost

Proof usesThe cost of find is the path length plus one · Path length to the root

Used byCost bound for union in a parent forest

DefinitionParent map after linking two roots#✓fully proved

Let \(F\) be a parent forest with parent map \(p\), and let \(r\) and \(s\) be vertices. The linked parent map sends \(r\) to \(s\) and agrees with \(p\) on every other vertex: it maps \(z\) to \(s\) if \(z = r\), and to \(p(z)\) otherwise.

public def linkParent {n : Nat} (forest : Forest n) (fromRoot toRoot : Fin n) :
    Fin n → Fin n := fun z => if z = fromRoot then toRoot else forest.parent z

Uses 1 · Used by 1

Statement usesParent forest with a depth certificate

Used byLinking two roots of a parent forest

DefinitionDepth certificate after linking two roots#✓fully proved

Let \(F\) be a parent forest with depth certificate \(d\), and let \(r\) and \(s\) be vertices. The linked depth certificate assigns to a vertex \(z\) the number \(d(z) + d(s) + 1\) if \(z\) is equivalent to \(r\) in \(F\) (that is, \(z\) and \(r\) have the same root), and \(d(z)\) otherwise.

public def linkDepth {n : Nat} (forest : Forest n) (fromRoot toRoot : Fin n) :
    Fin n → Nat := fun z =>
      if Equivalent forest z fromRoot
      then forest.depth z + forest.depth toRoot + 1
      else forest.depth z

Uses 3 · Used by 1

Statement usesEquivalent vertices of a parent forest · Parent forest with a depth certificate · Root of a vertex in a parent forest

Used byLinking two roots of a parent forest

DefinitionLinking two roots of a parent forest#✓fully proved

Let \(F\) be a parent forest with parent map \(p\) and depth certificate \(d\), and let \(r \ne s\) be two distinct roots of \(F\). Linking \(r\) to \(s\) gives the parent forest whose parent map is the linked parent map (the parent of \(r\) becomes \(s\) and all other parents are unchanged) and whose depth certificate is the linked depth certificate (the certificate of every vertex equivalent to \(r\) grows by \(d(s) + 1\) and all others are unchanged). These still satisfy the decreasing-certificate condition.

Cslib.Algorithms.Lean.UnionFind.link · 33 lines

public def link {n : Nat} (forest : Forest n) (fromRoot toRoot : Fin n)
    (hFrom : forest.parent fromRoot = fromRoot)
    (hTo : forest.parent toRoot = toRoot) (hne : fromRoot ≠ toRoot) : Forest n where
  parent := linkParent forest fromRoot toRoot
  depth := linkDepth forest fromRoot toRoot
  parent_lt z hz := by
    by_cases hzr : z = fromRoot
    · subst z
      have hFromEq : Equivalent forest fromRoot fromRoot := by
        simp [Equivalent]
      have hToNe : ¬Equivalent forest toRoot fromRoot := by
        intro h
        have : toRoot = fromRoot := by
          simpa [Equivalent, find_eq_self_of_parent_eq forest _ hTo,
            find_eq_self_of_parent_eq forest _ hFrom] using h
        exact hne this.symm
      simp [linkParent, linkDepth, hFromEq, hToNe]
      omega
    · have hparent : forest.parent z ≠ z := by
        intro h
        apply hz
        simp [linkParent, hzr, h]
      have hlt := forest.parent_lt z hparent
      have heq : Equivalent forest (forest.parent z) fromRoot ↔
          Equivalent forest z fromRoot := by
        simp only [Equivalent, find_parent]
      by_cases hzClass : Equivalent forest z fromRoot
      · have hpClass : Equivalent forest (forest.parent z) fromRoot := heq.mpr hzClass
        simp [linkParent, linkDepth, hzr, hzClass, hpClass]
        omega
      · have hpClass : ¬Equivalent forest (forest.parent z) fromRoot :=
          fun h => hzClass (heq.mp h)
        simpa [linkParent, linkDepth, hzr, hzClass, hpClass] using hlt

Uses 6 · Used by 3

Statement usesEquivalent vertices of a parent forest · Parent forest with a depth certificate · Root of a vertex in a parent forest · Find is unchanged along a parent pointer · Depth certificate after linking two roots · Parent map after linking two roots

Used byRepresentatives after a union · Union in a union-find forest · Union of equivalent vertices changes nothing

DefinitionUnion in a union-find forest#✓fully proved

Let \(F\) be a union-find forest on \(n\) vertices: each vertex \(z\) has a parent \(p(z)\), where roots are their own parents, and a depth certificate \(d(z) \in \mathbb{N}\) with \(d(p(z)) < d(z)\) whenever \(p(z) \ne z\). Let \(x\) and \(y\) be vertices, and let \(r_x\) and \(r_y\) be the roots reached from \(x\) and \(y\) by following parent pointers. If \(r_x = r_y\), the union of \(x\) and \(y\) in \(F\) is \(F\) itself. Otherwise it is the forest obtained from \(F\) by linking \(r_x\) to \(r_y\): the parent of \(r_x\) becomes \(r_y\), all other parent pointers are unchanged, every vertex \(z\) whose root is \(r_x\) gets depth certificate \(d(z) + d(r_y) + 1\), and every other vertex keeps \(d(z)\).

The operation is persistent: it returns a new forest and does not modify \(F\).

public def union {n : Nat} (forest : Forest n) (x y : Fin n) : Forest n :=
  let fromRoot := find forest x
  let toRoot := find forest y
  if h : fromRoot = toRoot then forest
  else link forest fromRoot toRoot (find_isRoot forest x) (find_isRoot forest y) h

Uses 4 · Used by 13

Statement usesParent forest with a depth certificate · Root of a vertex in a parent forest · Find returns a root · Linking two roots of a parent forest

Used byEquivalence after a union · Representatives after a union · Union preserves the representatives of unrelated classes · Union of equivalent vertices changes nothing · Union makes its arguments equivalent · Union in a parent forest with cost · Kruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · One Kruskal step

TheoremRepresentatives after a union#✓fully proved

Let \(F\) be a parent forest, let \(x, y, z\) be vertices of \(F\), and let \(F'\) be the forest obtained from \(F\) by the union of \(x\) and \(y\). If \(z\) is equivalent to \(x\) in \(F\), then find returns for \(z\) in \(F'\) the root that find returns for \(y\) in \(F\); otherwise find returns the same root for \(z\) in \(F'\) as in \(F\).

public theorem find_union {n : Nat} (forest : Forest n) (x y z : Fin n) :
    find (union forest x y) z =
      if Equivalent forest z x then find forest y else find forest z

Uses 7 · Used by 3

Statement usesEquivalent vertices of a parent forest · Parent forest with a depth certificate · Root of a vertex in a parent forest · Union in a union-find forest

Proof usesFind returns a root · Find is unchanged along a parent pointer · Linking two roots of a parent forest

Used byEquivalence after a union · Union preserves the representatives of unrelated classes · Union makes its arguments equivalent

TheoremUnion makes its arguments equivalent#✓fully proved

For every parent forest \(F\) and vertices \(x\) and \(y\), the vertices \(x\) and \(y\) are equivalent in the forest obtained from \(F\) by the union of \(x\) and \(y\).

public theorem union_equivalent {n : Nat} (forest : Forest n) (x y : Fin n) :
    Equivalent (union forest x y) x y

Uses 5 · Used by 2

Statement usesEquivalent vertices of a parent forest · Parent forest with a depth certificate · Union in a union-find forest

Proof usesRoot of a vertex in a parent forest · Representatives after a union

Used byKruskal's greedy cut property · Kruskal's selected edges span the graph

TheoremUnion of equivalent vertices changes nothing#✓fully proved

If \(x\) and \(y\) are equivalent vertices of a parent forest \(F\), then the union of \(x\) and \(y\) in \(F\) is \(F\) itself.

public theorem union_eq_self_of_equivalent {n : Nat} {forest : Forest n} {x y : Fin n}
    (h : Equivalent forest x y) : union forest x y = forest

Uses 6

Statement usesEquivalent vertices of a parent forest · Parent forest with a depth certificate · Union in a union-find forest

Proof usesRoot of a vertex in a parent forest · Find returns a root · Linking two roots of a parent forest

TheoremEquivalence after a union#✓fully proved

Let \(F\) be a parent forest and let \(x, y, a, b\) be vertices of \(F\). Then \(a\) and \(b\) are equivalent in the forest obtained from \(F\) by the union of \(x\) and \(y\) if and only if \(a\) and \(b\) are equivalent in \(F\), or \(a\) is equivalent to \(x\) and \(b\) is equivalent to \(y\) in \(F\), or \(a\) is equivalent to \(y\) and \(b\) is equivalent to \(x\) in \(F\).

Thus the union merges exactly the old classes of \(x\) and \(y\).

public theorem equivalent_union_iff {n : Nat} (forest : Forest n) (x y a b : Fin n) :
    Equivalent (union forest x y) a b ↔
      Equivalent forest a b ∨
        (Equivalent forest a x ∧ Equivalent forest b y) ∨
        (Equivalent forest a y ∧ Equivalent forest b x)

Uses 5 · Used by 4

Statement usesEquivalent vertices of a parent forest · Parent forest with a depth certificate · Union in a union-find forest

Proof usesRoot of a vertex in a parent forest · Representatives after a union

Used byKruskal's output is acyclic · Kruskal's greedy cut property · Kruskal's algorithm gives a minimum spanning forest · Kruskal's selected edges span the graph

TheoremUnion preserves the representatives of unrelated classes#✓fully proved

Let \(F\) be a parent forest and let \(x, y, z\) be vertices of \(F\). If \(z\) is not equivalent to \(x\) in \(F\), then find returns the same root for \(z\) in the forest obtained from \(F\) by the union of \(x\) and \(y\) as in \(F\).

No hypothesis on \(y\) is needed.

public theorem find_union_of_unrelated {n : Nat} (forest : Forest n) (x y z : Fin n)
    (hx : ¬Equivalent forest z x) :
    find (union forest x y) z = find forest z

Uses 5

Statement usesEquivalent vertices of a parent forest · Parent forest with a depth certificate · Root of a vertex in a parent forest · Union in a union-find forest

Proof usesRepresentatives after a union

DefinitionUnion in a parent forest with cost#✓fully proved

For a parent forest \(F\) and vertices \(x\) and \(y\), the costed union returns the union of \(x\) and \(y\) in \(F\) together with a cost equal to the cost of finding the root of \(x\) plus the cost of finding the root of \(y\) (each one unit per visited vertex, including the root), plus one more unit when the roots of \(x\) and \(y\) are distinct; when they coincide, union performs no link and none is charged.

public def unionWithCost {n : Nat} (forest : Forest n) (x y : Fin n) :
    TimeM Nat (Forest n) :=
  ⟨union forest x y,
    (findWithCost forest x).time + (findWithCost forest y).time +
      (if find forest x = find forest y then 0 else 1)⟩

Uses 4 · Used by 1

Statement usesParent forest with a depth certificate · Root of a vertex in a parent forest · Find with cost · Union in a union-find forest

Used byCost bound for union in a parent forest

TheoremCost bound for union in a parent forest#✓fully proved

For every parent forest \(F\) with depth certificate \(d\) and vertices \(x\) and \(y\), the cost charged for the union of \(x\) and \(y\) in \(F\) (two root searches at one unit per visited vertex, plus one unit for the link when the roots differ) is at most \(d(x) + d(y) + 3\).

public theorem unionWithCost_time_le_depth {n : Nat} (forest : Forest n) (x y : Fin n) :
    (unionWithCost forest x y).time ≤ forest.depth x + forest.depth y + 3

Uses 5

Statement usesParent forest with a depth certificate · Union in a parent forest with cost

Proof usesRoot of a vertex in a parent forest · Find with cost · The cost of find is at most the depth certificate plus one

TheoremCorrectness of the union-find equivalence query#✓fully proved

Call two natural numbers \(a\) and \(c\) equivalent in a union-find structure when they have the same root, where a number that is not a node is its own root. Let \(U\) be a union-find structure with nodes \(0, \dots, N-1\) and let \(x, y < N\). The equivalence query on \(x\) and \(y\), which runs FIND-SET with path compression on \(x\) and then on \(y\), returns a union-find structure \(U'\) and a boolean \(b\) such that \(U'\) has \(N\) nodes, \(b\) is true if and only if \(x\) and \(y\) are equivalent in \(U\), and for all natural numbers \(a\) and \(c\), \(a\) and \(c\) are equivalent in \(U'\) if and only if they are equivalent in \(U\).

public theorem checkEquiv_spec :
  ∀ (uf : UnionFind) (x y : Fin uf.size),
    (uf.checkEquiv x y).1.size = uf.size ∧
    ((uf.checkEquiv x y).2 = true ↔ UnionFind.Equiv uf x.val y.val) ∧
    ∀ (a b : Nat), UnionFind.Equiv (uf.checkEquiv x y).1 a b ↔ UnionFind.Equiv uf a b

Used by 2

Used byConnected components computes reachability · Operation counts of connected components

DefinitionConnected components via union-find#✓fully proved

Given a natural number \(n\) and a list \(E\) of pairs of vertices in \(\{0, \dots, n-1\}\), CONNECTED-COMPONENTS first builds the union-find structure with \(n\) singleton nodes \(0, \dots, n-1\) by \(n\) MAKE-SET calls. It then processes the pairs \((u, v)\) of \(E\) in list order: it asks whether \(u\) and \(v\) are equivalent using two FIND-SET calls, keeping the path compression done by the query, and if they are not equivalent it performs UNION on \(u\) and \(v\) (union by rank with path compression). It returns the final union-find structure, which has \(n\) nodes, together with the numbers of MAKE-SET, FIND-SET and UNION calls made.

Batteries.UnionFind.connectedComponents · 16 lines

public def connectedComponents (n : Nat) (edges : List (Fin n × Fin n)) :
    TimeM (Nat × Nat × Nat) {s : UnionFind // s.size = n} := do
  let initial ← allocateVertices n
  edges.foldlM (fun state edge ↦ do
    TimeM.tick (0, 2, 0)
    let x := Fin.cast state.property.symm edge.1
    let y := Fin.cast state.property.symm edge.2
    let checked := state.val.checkEquiv x y
    have hc : checked.1.size = n := (checkSize state.val x y).trans state.property
    if checked.2 then
      pure ⟨checked.1, hc⟩
    else
      TimeM.tick (0, 0, 1)
      let x' := Fin.cast hc.symm edge.1
      let y' := Fin.cast hc.symm edge.2
      pure ⟨checked.1.union x' y', (unionSize checked.1 x' y').trans hc⟩) initial

Used by 3

Used byConnected components computes reachability · Connected components allocates \(n\) nodes · Operation counts of connected components

TheoremConnected components allocates \(n\) nodes#✓fully proved

For every natural number \(n\) and every list \(E\) of pairs of vertices in \(\{0, \dots, n-1\}\), the union-find structure returned by CONNECTED-COMPONENTS on \(n\) and \(E\) has exactly \(n\) nodes.

public theorem connectedComponents_size (n : Nat) (edges : List (Fin n × Fin n)) :
    (connectedComponents n edges).ret.val.size = n

Uses 1

Statement usesConnected components via union-find

TheoremConnected components computes reachability#✓fully proved

Let \(n\) be a natural number and let \(E\) be a list of pairs of vertices in \(\{0, \dots, n-1\}\). For all vertices \(a, b < n\), \(a\) and \(b\) are equivalent in the union-find structure returned by CONNECTED-COMPONENTS on \(n\) and \(E\) if and only if \(a\) and \(b\) are joined by a path in the simple graph on \(\{0, \dots, n-1\}\) whose edges are the unordered pairs \(\{u, v\}\) with \((u, v)\) in \(E\) and \(u \ne v\).

public theorem connectedComponents_equiv_iff_reachable (n : Nat)
    (edges : List (Fin n × Fin n)) (a b : Fin n) :
    UnionFind.Equiv (connectedComponents n edges).ret.val a.val b.val ↔
      (SimpleGraph.fromEdgeSet {e | e ∈ edges.map (fun q ↦ s(q.1, q.2))}).Reachable a b

Uses 2

Statement usesConnected components via union-find

Proof usesCorrectness of the union-find equivalence query

TheoremOperation counts of connected components#✓fully proved

Let \(n\) be a natural number, let \(E\) be a list of pairs of vertices in \(\{0, \dots, n-1\}\) and let \(m\) be the length of \(E\). Let \(G\) be the simple graph on \(\{0, \dots, n-1\}\) whose edges are the unordered pairs \(\{u, v\}\) with \((u, v)\) in \(E\) and \(u \ne v\), and let \(k\) be the number of connected components of \(G\). Running CONNECTED-COMPONENTS on \(n\) and \(E\) makes exactly \(n\) MAKE-SET calls, \(2m\) FIND-SET calls and \(n - k\) UNION calls. Moreover, \(k\) plus the number of UNION calls equals \(n\), and if \(n > 0\) then the number of UNION calls is at most \(n - 1\).

These are the call counts recorded by the cost annotation, not bounds on parent-pointer visits.

public theorem connectedComponents_time_spec :
  ∀ (n : Nat) (edges : List (Fin n × Fin n)),
    let graph : SimpleGraph (Fin n) :=
      SimpleGraph.fromEdgeSet {e | e ∈ edges.map (fun p ↦ s(p.1, p.2))}
    (connectedComponents n edges).time =
      (n, 2 * edges.length, n - Nat.card graph.ConnectedComponent) ∧
    Nat.card graph.ConnectedComponent + (connectedComponents n edges).time.2.2 = n ∧
    (0 < n → (connectedComponents n edges).time.2.2 ≤ n - 1)

Uses 2

Statement usesConnected components via union-find

Proof usesCorrectness of the union-find equivalence query

DefinitionCost-counted FIND auxiliary#✓fully proved

For a union-find structure \(S\) with node array \(A\) and a node \(x < |S|\), this is the recursive path-compression routine of FIND, paired with a cost in \(\mathbb{N} \times \mathbb{N}\). It charges \((1, 0)\) for testing whether \(x\) is a root. If the parent \(y\) of \(x\) in \(A\) equals \(x\), it returns \(A\) and the root \(x\). Otherwise it runs on \(y\), obtaining an array \(A'\) and a root \(r\), charges \((0, 1)\) for one parent write, and returns \(A'\) with the parent of \(x\) set to \(r\), together with \(r\). The first cost coordinate thus counts root tests and the second counts parent writes.

The returned array and root are exactly those of the Batteries FIND auxiliary; only the costs are added.

@[no_expose] def countedAux (self : UnionFind) (x : Fin self.size) :
    TimeM (Nat × Nat) (UnionFind.FindAux self.size) := do
  TimeM.tick (1, 0)
  let y := self.arr[x.val].parent
  if h : y = x then
    pure ⟨self.arr, x, rfl⟩
  else
    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ h)
    let result ← countedAux self ⟨y, self.parent'_lt _ x.isLt⟩
    TimeM.tick (0, 1)
    pure ⟨result.s.modify x fun node ↦ { node with parent := result.root },
      result.root, by simp [result.size_eq]⟩
termination_by self.rankMax - self.rank x

Used by 8

Used byThe cost-counted FIND auxiliary returns the uncounted result · Root tests exceed parent writes by one · Cost of the FIND auxiliary at a root · Cost recurrence of the FIND auxiliary at a non-root · Parent writes are bounded by the rank gap · Cost-counted FIND · The cost-counted FIND returns the FIND result · The root is reached in fewer parent steps than there are nodes

TheoremThe cost-counted FIND auxiliary returns the uncounted result#✓fully proved

For a union-find structure \(S\) and a node \(x < |S|\), the value returned by the cost-counted FIND auxiliary on \(x\) (the compressed node array together with the root of \(x\)), with its cost discarded, equals the result of the Batteries path-compression auxiliary routine of FIND on \(x\).

theorem countedAux_ret (self : UnionFind) (x : Fin self.size) :
    (countedAux self x).ret = self.findAux x

Uses 1 · Used by 2

Statement usesCost-counted FIND auxiliary

Used byCost-counted FIND · The cost-counted FIND returns the FIND result

TheoremCost of the FIND auxiliary at a root#✓fully proved

Let \(S\) be a union-find structure and \(x < |S|\) a node. If the parent of \(x\) in \(S\) is \(x\) itself, then the cost-counted FIND auxiliary on \(x\) has cost \((1, 0)\): one root test and no parent writes.

theorem countedAux_time_root (self : UnionFind) (x : Fin self.size)
    (h : self.arr[x.val].parent = x) : (countedAux self x).time = (1, 0)

Uses 1 · Used by 3

Statement usesCost-counted FIND auxiliary

Used byRoot tests exceed parent writes by one · Parent writes are bounded by the rank gap · The root is reached in fewer parent steps than there are nodes

TheoremCost recurrence of the FIND auxiliary at a non-root#✓fully proved

Let \(S\) be a union-find structure and \(x < |S|\) a node whose parent \(y\) in \(S\) differs from \(x\). If \(c_x\) and \(c_y\) are the costs of the cost-counted FIND auxiliary on \(x\) and on \(y\), then \(c_x = (1, 0) + (c_y + (0, 1))\): one root test at \(x\), then the run on \(y\), then one parent write.

theorem countedAux_time_step (self : UnionFind) (x : Fin self.size)
    (h : self.arr[x.val].parent ≠ x) :
    (countedAux self x).time = (1, 0) +
      ((countedAux self ⟨self.arr[x.val].parent, self.parent'_lt _ x.isLt⟩).time +
        (0, 1))

Uses 1 · Used by 3

Statement usesCost-counted FIND auxiliary

Used byRoot tests exceed parent writes by one · Parent writes are bounded by the rank gap · The root is reached in fewer parent steps than there are nodes

TheoremRoot tests exceed parent writes by one#✓fully proved

For a union-find structure \(S\) and a node \(x < |S|\), if the cost-counted FIND auxiliary on \(x\) has cost \((t, w)\), where \(t\) counts root tests and \(w\) counts parent writes, then \(t = w + 1\).

theorem countedAux_time_balance (self : UnionFind) (x : Fin self.size) :
    (countedAux self x).time.1 = (countedAux self x).time.2 + 1

Uses 3 · Used by 1

Statement usesCost-counted FIND auxiliary

Proof usesCost of the FIND auxiliary at a root · Cost recurrence of the FIND auxiliary at a non-root

Used byThe FIND phases of a union make two more root tests than parent writes

DefinitionCost-counted FIND#✓fully proved

For a union-find structure \(S\) and a node \(x < |S|\), this runs the cost-counted FIND auxiliary on \(x\), obtaining a node array \(A'\), a root \(r\) and a cost \((t, w)\). It returns the union-find structure with node array \(A'\), together with \(r\) as a node of that structure (whose size equals \(|S|\)), at cost \((t, w)\).

It reuses the array and root of that single run; FIND is not run a second time.

Batteries.UnionFind.Internal.countedFind · 20 lines

@[no_expose] def countedFind (self : UnionFind) (x : Fin self.size) :
    TimeM (Nat × Nat) ((s : UnionFind) × {_root : Fin s.size // s.size = self.size}) :=
  let result := countedAux self x
  let r := result.ret
  ⟨{ 1.arr := r.s
     2.1.val := r.root
     1.parentD_lt := fun h ↦ by
       have hret := countedAux_ret self x
       change UnionFind.parentD r.s _ < r.s.size at *
       dsimp [r] at *
       rw [hret] at *
       simp only [UnionFind.FindAux.size_eq] at *
       exact UnionFind.parentD_findAux_lt h
     1.rankD_lt := fun h ↦ by
       dsimp [r] at *
       rw [countedAux_ret self x] at *
       rw [UnionFind.rankD_findAux, UnionFind.rankD_findAux]
       exact UnionFind.lt_rankD_findAux h
     2.1.isLt := show _ < r.s.size by rw [r.size_eq]; exact r.root.isLt
     2.2 := by simp [UnionFind.size, r.size_eq] }, result.time⟩

Uses 2 · Used by 5

Statement usesCost-counted FIND auxiliary · The cost-counted FIND auxiliary returns the uncounted result

Used byThe cost-counted FIND returns the FIND result · Union by rank with operation counts · The FIND phases of a union make two more root tests than parent writes · Counted union returns the union's array · The root is reached in fewer parent steps than there are nodes

TheoremThe cost-counted FIND returns the FIND result#✓fully proved

For a union-find structure \(S\) and a node \(x < |S|\), the value returned by the cost-counted FIND on \(x\) (the compressed union-find structure together with the root of \(x\)), with its cost discarded, equals the result of the Batteries FIND with path compression on \(x\).

theorem countedFind_ret (self : UnionFind) (x : Fin self.size) :
    (countedFind self x).ret = self.find x

Uses 3 · Used by 1

Statement usesCost-counted FIND

Proof usesCost-counted FIND auxiliary · The cost-counted FIND auxiliary returns the uncounted result

Used byCounted union returns the union's array

TheoremParent writes are bounded by the rank gap#✓fully proved

Let \(S\) be a union-find structure, let \(R\) be one more than the maximum rank of a node of \(S\), and let \(x < |S|\) be a node. The number of parent writes performed by the cost-counted FIND auxiliary on \(x\) (the second coordinate of its cost) is at most \(R - \operatorname{rank}(x)\).

This is a per-call bound, not a logarithmic or amortized inverse-Ackermann bound.

theorem countedAux_writes_rank (self : UnionFind) (x : Fin self.size) :
    (countedAux self x).time.2 ≤ self.rankMax - self.rank x

Uses 3

Statement usesCost-counted FIND auxiliary

Proof usesCost of the FIND auxiliary at a root · Cost recurrence of the FIND auxiliary at a non-root

TheoremFIND compresses exactly the original path to the root#✓fully proved

Let \(S\) be a union-find structure with parent map \(p\) (where \(p(i) = i\) for \(i \ge |S|\)), let \(x < |S|\), and let \(p'\) be the parent map of the structure produced by FIND with path compression on \(x\). Then for every natural number \(i\), \(p'(i)\) is the root of \(x\) if \(i = p^k(x)\) for some \(k \ge 0\), and \(p'(i) = p(i)\) otherwise.

public theorem find_parent_eq_ite_iterate (self : UnionFind)
    (x : Fin self.size) (i : Nat) :
    (self.find x).1.parent i =
      if ∃ k : Nat, Nat.iterate self.parent k x.val = i then self.rootD x.val
      else self.parent i

Used by 1

Used byEffect of path-compressing find on each node

TheoremEffect of path-compressing find on each node#✓fully proved

Let \(s\) be a union-find structure on the indices \(0, \dots, n-1\) with parent function \(p\), let \(x < n\), and let \(r\) be the root of \(x\) in \(s\). After find with path compression is run on \(x\), for every index \(i < n\) the node at \(i\) in the resulting array keeps its rank from \(s\), and its parent is \(r\) if \(i = p^k(x)\) for some \(k \ge 0\), and is its original parent \(p(i)\) otherwise.

public theorem getElem_find (self : UnionFind) (x : Fin self.size)
    (i : Nat) (hi : i < self.size) :
    (self.find x).1.arr[i]'(by simpa using hi) =
      { parent := if ∃ k : Nat, Nat.iterate self.parent k x.val = i then
          self.rootD x.val else self.arr[i].parent
        rank := self.arr[i].rank }

Uses 1

Proof usesFIND compresses exactly the original path to the root

TheoremThe root is reached in fewer parent steps than there are nodes#✓fully proved

Let \(S\) be a union-find structure with \(n\) nodes and parent map \(p\), and let \(x < n\). Then there is \(d < n\) such that \(p^d(x)\) is the root of \(x\) and \(p^k(x)\) is not the root of \(x\) for every \(k < d\).

public theorem exists_first_iterate_rootD (self : UnionFind) (x : Fin self.size) :
    ∃ d : Nat,
      Nat.iterate self.parent d x.val = self.rootD x.val ∧
      (∀ k < d, Nat.iterate self.parent k x.val ≠ self.rootD x.val) ∧
      d < self.size

Uses 4

Proof usesCost-counted FIND auxiliary · Cost of the FIND auxiliary at a root · Cost recurrence of the FIND auxiliary at a non-root · Cost-counted FIND

TheoremRanks after linking two nodes of an array#✓fully proved

For an array \(A\) of union-find nodes, write \(\rho_A(i)\) for the rank stored at index \(i\) of \(A\), or \(0\) if \(i\) is not an index of \(A\). Let \(x, y\) be indices of \(A\) and let \(A'\) be the array obtained from \(A\) by the Batteries link by rank of \(x\) and \(y\). Then for every natural number \(i\), \(\rho_{A'}(i) = \rho_A(y) + 1\) if \(x \ne y\), \(\rho_A(x) = \rho_A(y)\) and \(i = y\), and \(\rho_{A'}(i) = \rho_A(i)\) otherwise.

theorem rankD_linkAux (arr : Array UFNode) (x y : Fin arr.size) (i : Nat) :
    UnionFind.rankD (UnionFind.linkAux arr x y) i =
      if x.val ≠ y.val ∧ arr[x.val].rank = arr[y.val].rank ∧ y.val = i then
        arr[y.val].rank + 1 else UnionFind.rankD arr i

Used by 1

Used byRanks after linking in a union-find structure

TheoremRanks after linking in a union-find structure#✓fully proved

Let \(S\) be a union-find structure, write \(\rho(i)\) for the rank of \(i\) in \(S\) (\(0\) if \(i\) is not a node of \(S\)), and let \(x, y\) be nodes of \(S\) such that \(y\) is a root, that is, the parent of \(y\) is \(y\). Let \(S'\) be the result of linking \(x\) and \(y\) by rank. Then for every natural number \(i\), the rank of \(i\) in \(S'\) is \(\rho(y) + 1\) if \(x \ne y\), \(\rho(x) = \rho(y)\) and \(i = y\), and is \(\rho(i)\) otherwise.

public theorem rank_link (self : UnionFind) (x y : Fin self.size)
    (yroot : self.parent y = y) (i : Nat) :
    (self.link x y yroot).rank i =
      if x.val ≠ y.val ∧ self.rank x = self.rank y ∧ y.val = i then
        self.rank y + 1 else self.rank i

Uses 1 · Used by 1

Proof usesRanks after linking two nodes of an array

Used byRanks after a union

TheoremLinking two roots by rank#✓fully proved

Let \(U\) be a union-find structure on \(\{0, \dots, n-1\}\) and let \(x, y < n\) be roots of \(U\), i.e. each is its own parent. Let \(U'\) be obtained by linking \(x\) and \(y\) by rank: nothing changes if \(x = y\); otherwise, if \(\operatorname{rank}(y) < \operatorname{rank}(x)\) then \(y\) gets parent \(x\), and if not then \(x\) gets parent \(y\) and, when the two ranks are equal, the rank of \(y\) increases by one. Then for every natural number \(i\), where the root of an index \(i \ge n\) is \(i\) itself: if the root of \(i\) in \(U\) is \(x\) or \(y\), the root of \(i\) in \(U'\) is \(x\) when \(\operatorname{rank}(y) < \operatorname{rank}(x)\) and \(y\) otherwise; if the root of \(i\) in \(U\) is neither \(x\) nor \(y\), its root in \(U'\) is the same as in \(U\).

public theorem rootD_link_eq_ite (self : UnionFind) (x y : Fin self.size)
    (xroot : self.parent x = x) (yroot : self.parent y = y) (i : Nat) :
    (self.link x y yroot).rootD i =
      if self.rootD i = x.val ∨ self.rootD i = y.val then
        if self.rank y < self.rank x then x.val else y.val
      else self.rootD i

TheoremUnion unfolds to two finds and a link#✓fully proved

Let \(U\) be a union-find structure on \(\{0, \dots, n-1\}\) and let \(x, y < n\). Run find with path compression on \(x\) in \(U\), giving a structure \(U_1\) and a root \(r_x\); then run find on \(y\) in \(U_1\) (not in \(U\)), giving a structure \(U_2\) and a root \(r_y\). Then the node array of the union of \(x\) and \(y\) in \(U\) equals the array obtained from the node array of \(U_2\) by linking \(r_x\) and \(r_y\) by rank: nothing changes if \(r_x = r_y\); otherwise, if \(\operatorname{rank}(r_y) < \operatorname{rank}(r_x)\) then \(r_y\) gets parent \(r_x\), and if not then \(r_x\) gets parent \(r_y\) and, when the two ranks are equal, the rank of \(r_y\) increases by one.

theorem union_carried (self : UnionFind) (x y : Fin self.size) :
    let first := self.find x
    let y₁ : Fin first.1.size := ⟨y.val, by rw [first.2.property]; exact y.isLt⟩
    let second := first.1.find y₁
    let rx : Fin second.1.size :=
      ⟨first.2.val.val, by rw [second.2.property]; exact first.2.val.isLt⟩
    (self.union x y).arr = UnionFind.linkAux second.1.arr rx second.2.val

Used by 1

Used byCounted union returns the union's array

TheoremPath compression preserves ranks#✓fully proved

Let \(S\) be a union-find structure and \(x\) a node of \(S\), and let \(S'\) be the structure returned by FIND on \(x\) with path compression. For every natural number \(i\), the rank of \(i\) in \(S'\) equals the rank of \(i\) in \(S\), where the rank of an index that is not a node is \(0\).

theorem rank_find (self : UnionFind) (x : Fin self.size) (i : Nat) :
    (self.find x).1.rank i = self.rank i

Used by 1

Used byRanks after a union

TheoremRanks after a union#✓fully proved

Let \(S\) be a union-find structure, write \(\rho(i)\) for the rank of \(i\) in \(S\) (\(0\) if \(i\) is not a node of \(S\)) and \(r(i)\) for the root of \(i\) in \(S\). For nodes \(x, y\) of \(S\) and every natural number \(i\), the rank of \(i\) in the union of \(x\) and \(y\) in \(S\) (union by rank with path compression) is \(\rho(r(y)) + 1\) if \(r(x) \ne r(y)\), \(\rho(r(x)) = \rho(r(y))\) and \(r(y) = i\), and is \(\rho(i)\) otherwise.

public theorem rank_union (self : UnionFind) (x y : Fin self.size) (i : Nat) :
    (self.union x y).rank i =
      if self.rootD x ≠ self.rootD y ∧
          self.rank (self.rootD x) = self.rank (self.rootD y) ∧ self.rootD y = i then
        self.rank (self.rootD y) + 1 else self.rank i

Uses 2

Proof usesPath compression preserves ranks · Ranks after linking in a union-find structure

DefinitionLinking by rank with operation counts#✓fully proved

Given an array \(A\) of union-find nodes, each storing a parent index and a rank, and indices \(x, y\) of \(A\), this computation returns an array together with a count \((t, p, w)\) of rank tests \(t\), parent writes \(p\) and rank writes \(w\). If \(x = y\) it returns \(A\) with count \((0, 0, 0)\). Otherwise it makes one rank test; if the rank of \(y\) is less than the rank of \(x\), it sets the parent of \(y\) to \(x\) (one parent write). If not, it sets the parent of \(x\) to \(y\) (one parent write) and makes a second rank test, and if the ranks of \(x\) and \(y\) are equal it also increases the rank of \(y\) by one (one rank write).

The equality test \(x = y\) is not counted as a rank test.

Batteries.UnionFind.LinkInternal.countedLinkAux · 20 lines

@[no_expose] def countedLinkAux (arr : Array UFNode) (x y : Fin arr.size) :
    TimeM (Nat × Nat × Nat) (Array UFNode) := do
  if x.val = y then
    pure arr
  else
    let nx := arr[x.val]
    let ny := arr[y.val]
    TimeM.tick (1, 0, 0)
    if ny.rank < nx.rank then
      TimeM.tick (0, 1, 0)
      pure (arr.set y { ny with parent := x })
    else
      TimeM.tick (0, 1, 0)
      let arr₁ := arr.set x { nx with parent := y }
      TimeM.tick (1, 0, 0)
      if nx.rank = ny.rank then
        TimeM.tick (0, 0, 1)
        pure (arr₁.set y { ny with rank := ny.rank + 1 } (by simp [arr₁]))
      else
        pure arr₁

Used by 4

Used byCounted linking returns the linked array · Operation counts of linking by rank · Union by rank with operation counts · Counted union returns the union's array

TheoremCounted linking returns the linked array#✓fully proved

For an array \(A\) of union-find nodes and indices \(x, y\) of \(A\), the array returned by counted linking of \(x\) and \(y\) in \(A\) is exactly the array produced by the uncounted Batteries link by rank of \(x\) and \(y\) in \(A\).

theorem countedLinkAux_ret (arr : Array UFNode) (x y : Fin arr.size) :
    (countedLinkAux arr x y).ret = UnionFind.linkAux arr x y

Uses 1 · Used by 1

Statement usesLinking by rank with operation counts

Used byCounted union returns the union's array

TheoremOperation counts of linking by rank#✓fully proved

Let \(A\) be an array of union-find nodes, let \(x, y\) be indices of \(A\), and write \(r_x\) and \(r_y\) for the ranks stored at \(x\) and \(y\). Counted linking of \(x\) and \(y\) in \(A\) makes \((t, p, w)\) rank tests, parent writes and rank writes, where \((t, p, w)\) is \((0, 0, 0)\) if \(x = y\), is \((1, 1, 0)\) if \(x \ne y\) and \(r_y < r_x\), is \((2, 1, 1)\) if \(x \ne y\) and \(r_x = r_y\), and is \((2, 1, 0)\) otherwise, that is, if \(x \ne y\) and \(r_x < r_y\).

theorem countedLinkAux_time (arr : Array UFNode) (x y : Fin arr.size) :
    (countedLinkAux arr x y).time =
      if x.val = y.val then (0, 0, 0)
      else if arr[y.val].rank < arr[x.val].rank then (1, 1, 0)
      else if arr[x.val].rank = arr[y.val].rank then (2, 1, 1)
      else (2, 1, 0)

Uses 1

Statement usesLinking by rank with operation counts

DefinitionUnion by rank with operation counts#✓fully proved

For a union-find structure \(S\) and indices \(x, y\) of \(S\), this computation runs counted FIND on \(x\) in \(S\), giving a structure \(S_1\) and a root \(r_x\); then counted FIND on \(y\) in \(S_1\), giving a structure \(S_2\) and a root \(r_y\); then counted linking of \(r_x\) and \(r_y\) in the node array of \(S_2\). It returns the array produced by the linking, with cost \(((a, b), (t, p, w))\), where \(a\) and \(b\) are the total numbers of root tests and parent writes of the two FIND calls, and \((t, p, w)\) counts the rank tests, parent writes and rank writes of the linking.

@[no_expose] def countedUnion (self : UnionFind) (x y : Fin self.size) :
    TimeM ((Nat × Nat) × (Nat × Nat × Nat)) (Array UFNode) :=
  let first := Internal.countedFind self x
  let y₁ : Fin first.ret.1.size :=
    ⟨y.val, by rw [first.ret.2.property]; exact y.isLt⟩
  let second := Internal.countedFind first.ret.1 y₁
  let rx : Fin second.ret.1.size :=
    ⟨first.ret.2.val.val, by rw [second.ret.2.property]; exact first.ret.2.val.isLt⟩
  let linked := LinkInternal.countedLinkAux second.ret.1.arr rx second.ret.2.val
  ⟨linked.ret, (first.time + second.time, linked.time)⟩

Uses 2 · Used by 2

Statement usesCost-counted FIND · Linking by rank with operation counts

Used byThe FIND phases of a union make two more root tests than parent writes · Counted union returns the union's array

TheoremCounted union returns the union's array#✓fully proved

For a union-find structure \(S\) and indices \(x, y\) of \(S\), the array returned by the counted union of \(x\) and \(y\) in \(S\) equals the node array of the Batteries union of \(x\) and \(y\) in \(S\) (union by rank with path compression).

theorem countedUnion_ret (self : UnionFind) (x y : Fin self.size) :
    (countedUnion self x y).ret = (self.union x y).arr

Uses 6

Statement usesUnion by rank with operation counts

Proof usesCost-counted FIND · The cost-counted FIND returns the FIND result · Linking by rank with operation counts · Counted linking returns the linked array · Union unfolds to two finds and a link

TheoremThe FIND phases of a union make two more root tests than parent writes#✓fully proved

For a union-find structure \(S\) and indices \(x, y\) of \(S\), in the counted union of \(x\) and \(y\) in \(S\) the total number of root tests made by its two FIND calls equals the total number of parent writes they make plus \(2\).

theorem countedUnion_find_balance (self : UnionFind) (x y : Fin self.size) :
    (countedUnion self x y).time.1.1 = (countedUnion self x y).time.1.2 + 2

Uses 3

Statement usesUnion by rank with operation counts

Proof usesRoot tests exceed parent writes by one · Cost-counted FIND

49 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.