Strongly connected components

DefinitionStrongly connected vertices#✓fully proved

In a directed adjacency graph \(G\), vertices \(u\) and \(v\) are strongly connected when \(v\) is reachable from \(u\) and \(u\) is reachable from \(v\) in \(G\).

public def StronglyConnected {V : Type u} (graph : DirectedAdjacency V)
    (left right : V) : Prop :=
  graph.Reachable left right ∧ graph.Reachable right left
Uses 2 · Used by 14
Statement usesDirected adjacency graph · Reachability in a directed graph
Used byEach computed component is a full mutual-reachability class · The condensation of the computed components is acyclic · The computed components form the SCC partition · Computed components are nonempty · Computed components are pairwise disjoint · SCC partition · The computed components cover the vertex list · The mutual-reachability test is correct · Vertices share a computed component exactly when strongly connected · Strong connectivity is reflexive · Strong connectivity as an equivalence relation · Strong connectivity is symmetric · Strong connectivity is transitive · Correctness of the SCC-based 2-SAT procedure

TheoremStrong connectivity is reflexive#✓fully proved

In a directed graph \(G\), every vertex is strongly connected to itself.

@[refl]
public theorem stronglyConnected_refl {V : Type u} (graph : DirectedAdjacency V)
    (vertex : V) : StronglyConnected graph vertex vertex
Uses 4 · Used by 4
Statement usesDirected adjacency graph · Strongly connected vertices
Proof usesEdge of a directed adjacency graph · Reachability in a directed graph
Used byComputed components are nonempty · The computed components cover the vertex list · Vertices share a computed component exactly when strongly connected · Strong connectivity as an equivalence relation

TheoremStrong connectivity is symmetric#✓fully proved

In a directed graph \(G\), if \(u\) is strongly connected to \(v\), then \(v\) is strongly connected to \(u\).

@[symm]
public theorem StronglyConnected.symm {V : Type u} {graph : DirectedAdjacency V}
    {left right : V} (connected : StronglyConnected graph left right) :
    StronglyConnected graph right left
Uses 3 · Used by 5
Statement usesDirected adjacency graph · Strongly connected vertices
Proof usesReachability in a directed graph
Used byEach computed component is a full mutual-reachability class · The condensation of the computed components is acyclic · Computed components are pairwise disjoint · Vertices share a computed component exactly when strongly connected · Strong connectivity as an equivalence relation

TheoremStrong connectivity is transitive#✓fully proved

In a directed graph \(G\), if \(u\) is strongly connected to \(v\) and \(v\) is strongly connected to \(w\), then \(u\) is strongly connected to \(w\).

@[trans]
public theorem StronglyConnected.trans {V : Type u} {graph : DirectedAdjacency V}
    {left middle right : V}
    (leftMiddle : StronglyConnected graph left middle)
    (middleRight : StronglyConnected graph middle right) :
    StronglyConnected graph left right
Uses 4 · Used by 5
Statement usesDirected adjacency graph · Strongly connected vertices
Proof usesEdge of a directed adjacency graph · Reachability in a directed graph
Used byEach computed component is a full mutual-reachability class · The condensation of the computed components is acyclic · Computed components are pairwise disjoint · Vertices share a computed component exactly when strongly connected · Strong connectivity as an equivalence relation

DefinitionStrong connectivity as an equivalence relation#✓fully proved

For a directed graph \(G\), the relation on the vertices of \(G\) that holds between \(u\) and \(v\) exactly when \(u\) and \(v\) are strongly connected in \(G\), packaged as an equivalence relation.

public def stronglyConnectedSetoid {V : Type u}
    (graph : DirectedAdjacency V) : Setoid V where
  r := StronglyConnected graph
  iseqv := ⟨stronglyConnected_refl graph, StronglyConnected.symm,
    StronglyConnected.trans⟩
Uses 5
Statement usesDirected adjacency graph · Strongly connected vertices · Strong connectivity is symmetric · Strong connectivity is transitive · Strong connectivity is reflexive

DefinitionExecutable mutual-reachability test#✓fully proved

For a directed graph \(G\) and vertices \(u\) and \(v\), the test returns true exactly when \(v\) occurs in the preorder of the depth-first search of \(G\) from the single root \(u\), and \(u\) occurs in the preorder of the depth-first search of \(G\) from the single root \(v\).

public def sameComponentB {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (left right : V) : Bool :=
  decide (right ∈ (dfs graph [left]).preorder) &&
    decide (left ∈ (dfs graph [right]).preorder)
Uses 3 · Used by 9
Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph
Used byEach computed component is a full mutual-reachability class · Strongly connected components algorithm · The condensation of the computed components is acyclic · Computed components have no repeated vertices · Computed components are nonempty · Computed components are pairwise disjoint · The computed components cover the vertex list · The mutual-reachability test is correct · Vertices share a computed component exactly when strongly connected

TheoremThe mutual-reachability test is correct#✓fully proved

For a directed graph \(G\) and vertices \(u\) and \(v\), the executable mutual-reachability test on \(u\) and \(v\) returns true if and only if \(u\) and \(v\) are strongly connected in \(G\).

public theorem sameComponentB_eq_true {V : Type u} [BEq V] [Hashable V]
    [LawfulBEq V] (graph : DirectedAdjacency V) (left right : V) :
    sameComponentB graph left right = true ↔ StronglyConnected graph left right
Uses 7 · Used by 6
Statement usesDirected adjacency graph · Strongly connected vertices · Executable mutual-reachability test
Proof usesDepth-first traversal record · Left-first depth-first search · Depth-first search discovers exactly the reachable vertices · Reachability in a directed graph
Used byEach computed component is a full mutual-reachability class · The condensation of the computed components is acyclic · Computed components are nonempty · Computed components are pairwise disjoint · The computed components cover the vertex list · Vertices share a computed component exactly when strongly connected

DefinitionStrongly connected components algorithm#✓fully proved

Let \(G\) be a directed graph and let \(v_1, \dots, v_n\) be its vertices in decreasing order of finishing time in a depth-first search of the whole graph that takes its roots in the vertex order of \(G\). For each \(i\), let \(C_i\) be the list of those \(v_j\), in increasing order of \(j\), such that \(v_i\) and \(v_j\) are strongly connected (tested by two depth-first searches). The output is the list \(C_1, \dots, C_n\) with repeated blocks removed, keeping the last occurrence of each.

The result is deterministic: within a block, vertices appear in decreasing finish order.

public def components {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) : List (List V) :=
  let vertices := decreasingFinishAll graph
  (vertices.map fun pivot => vertices.filter (sameComponentB graph pivot)).dedup
Uses 3 · Used by 10
Statement usesWhole-graph decreasing finish order · Directed adjacency graph · Executable mutual-reachability test
Used byEach computed component is a full mutual-reachability class · The condensation of the computed components is acyclic · The computed components form the SCC partition · Computed components have no repeated vertices · Computed components are nonempty · Computed components are pairwise disjoint · The computed components cover the vertex list · Vertices share a computed component exactly when strongly connected · SCC-based 2-SAT decision procedure · Correctness of the SCC-based 2-SAT procedure

TheoremComputed components are nonempty#✓fully proved

For every directed graph \(G\), each block returned by the strongly connected components algorithm on \(G\) contains at least one vertex.

public theorem components_nonempty {V : Type u} [BEq V] [Hashable V]
    [LawfulBEq V] (graph : DirectedAdjacency V) :
    ∀ block ∈ components graph, block ≠ []
Uses 7 · Used by 1
Statement usesDirected adjacency graph · Strongly connected components algorithm
Proof usesWhole-graph decreasing finish order · Strongly connected vertices · Executable mutual-reachability test · The mutual-reachability test is correct · Strong connectivity is reflexive
Used byThe computed components form the SCC partition

TheoremComputed components have no repeated vertices#✓fully proved

For every directed graph \(G\), each block returned by the strongly connected components algorithm on \(G\) contains no vertex more than once.

public theorem components_nodup {V : Type u} [BEq V] [Hashable V]
    [LawfulBEq V] (graph : DirectedAdjacency V) :
    ∀ block ∈ components graph, block.Nodup
Uses 5 · Used by 1
Statement usesDirected adjacency graph · Strongly connected components algorithm
Proof usesWhole-graph decreasing finish order · Whole-graph decreasing finish order has no repeated vertices · Executable mutual-reachability test
Used byThe computed components form the SCC partition

TheoremComputed components are pairwise disjoint#✓fully proved

For every directed graph \(G\), any two blocks at different positions of the list returned by the strongly connected components algorithm on \(G\) have no vertex in common.

public theorem components_pairwise_disjoint {V : Type u} [BEq V] [Hashable V]
    [LawfulBEq V] (graph : DirectedAdjacency V) :
    (components graph).Pairwise List.Disjoint
Uses 8 · Used by 3
Statement usesDirected adjacency graph · Strongly connected components algorithm
Proof usesWhole-graph decreasing finish order · Strongly connected vertices · Strong connectivity is symmetric · Strong connectivity is transitive · Executable mutual-reachability test · The mutual-reachability test is correct
Used byEach computed component is a full mutual-reachability class · The condensation of the computed components is acyclic · The computed components form the SCC partition

TheoremThe computed components cover the vertex list#✓fully proved

For a directed graph \(G\) and a vertex \(v\), \(v\) belongs to some block of the computed strongly connected components of \(G\) if and only if \(v\) occurs in the vertex enumeration of \(G\).

public theorem mem_flatten_components {V : Type u} [BEq V] [Hashable V]
    [LawfulBEq V] (graph : DirectedAdjacency V) (vertex : V) :
    vertex ∈ (components graph).flatten ↔ vertex ∈ graph.vertices
Uses 8 · Used by 1
Statement usesDirected adjacency graph · Strongly connected components algorithm
Proof usesWhole-graph decreasing finish order · Whole-graph decreasing finish order contains every vertex · Strongly connected vertices · Executable mutual-reachability test · The mutual-reachability test is correct · Strong connectivity is reflexive
Used byThe computed components form the SCC partition

TheoremVertices share a computed component exactly when strongly connected#✓fully proved

For a directed graph \(G\) and vertices \(u\) and \(v\), some block of the computed strongly connected components of \(G\) contains both \(u\) and \(v\) if and only if \(u\) and \(v\) are strongly connected in \(G\).

public theorem share_component_iff_stronglyConnected {V : Type u} [BEq V]
    [Hashable V] [LawfulBEq V] (graph : DirectedAdjacency V) (left right : V) :
    (∃ block ∈ components graph, left ∈ block ∧ right ∈ block) ↔
      StronglyConnected graph left right
Uses 10 · Used by 3
Statement usesDirected adjacency graph · Strongly connected vertices · Strongly connected components algorithm
Proof usesWhole-graph decreasing finish order · Whole-graph decreasing finish order contains every vertex · Strong connectivity is symmetric · Strong connectivity is transitive · Executable mutual-reachability test · The mutual-reachability test is correct · Strong connectivity is reflexive
Used byEach computed component is a full mutual-reachability class · The computed components form the SCC partition · Correctness of the SCC-based 2-SAT procedure

TheoremEach computed component is a full mutual-reachability class#✓fully proved

Let \(G\) be a directed graph, let \(B\) be one of the blocks returned by the strongly connected components algorithm on \(G\), and let \(m\) be a vertex of \(B\). Then for every vertex \(v\) of \(G\), the vertices \(m\) and \(v\) are strongly connected (each is reachable from the other) if and only if \(v\) lies in \(B\).

public theorem component_maximal {V : Type u} [BEq V] [Hashable V]
    [LawfulBEq V] (graph : DirectedAdjacency V) (block : List V)
    (blockMem : block ∈ components graph) (member : V) (memberMem : member ∈ block)
    (vertex : V) :
    StronglyConnected graph member vertex ↔ vertex ∈ block
Uses 10 · Used by 2
Statement usesDirected adjacency graph · Strongly connected vertices · Strongly connected components algorithm
Proof usesWhole-graph decreasing finish order · Strong connectivity is symmetric · Strong connectivity is transitive · Computed components are pairwise disjoint · Executable mutual-reachability test · The mutual-reachability test is correct · Vertices share a computed component exactly when strongly connected
Used byThe condensation of the computed components is acyclic · The computed components form the SCC partition

StructureSCC partition#✓fully proved

A list \(\mathcal{B}\) of vertex lists is an SCC partition of a directed graph \(G\) when every block of \(\mathcal{B}\) is nonempty and contains no vertex twice, blocks at different positions of \(\mathcal{B}\) are disjoint, a vertex lies in some block exactly when it is a vertex of \(G\), two vertices lie in a common block exactly when they are strongly connected (each is reachable from the other), and for every block \(B\), every \(m \in B\) and every vertex \(v\), the vertices \(m\) and \(v\) are strongly connected exactly when \(v \in B\).

Cslib.Algorithms.Lean.StronglyConnectedComponents.IsSCCPartition · 17 lines 
public structure IsSCCPartition {V : Type u} (graph : DirectedAdjacency V)
    (blocks : List (List V)) : Prop where
  /-- Every block has a vertex. -/
  nonempty : ∀ block ∈ blocks, block ≠ []
  /-- No block repeats a vertex. -/
  blocksNodup : ∀ block ∈ blocks, block.Nodup
  /-- Different blocks are disjoint. -/
  pairwiseDisjoint : blocks.Pairwise List.Disjoint
  /-- Flattening covers exactly the certified vertex carrier. -/
  covers : ∀ vertex, vertex ∈ blocks.flatten ↔ vertex ∈ graph.vertices
  /-- Co-membership is exactly mutual reachability. -/
  characterizes : ∀ left right,
    (∃ block ∈ blocks, left ∈ block ∧ right ∈ block) ↔
      StronglyConnected graph left right
  /-- Every block is maximal under mutual reachability. -/
  maximal : ∀ block ∈ blocks, ∀ member ∈ block, ∀ vertex,
    StronglyConnected graph member vertex ↔ vertex ∈ block
Uses 2 · Used by 1
Statement usesDirected adjacency graph · Strongly connected vertices
Used byThe computed components form the SCC partition

TheoremThe computed components form the SCC partition#✓fully proved

For every directed graph \(G\), the list of blocks returned by the strongly connected components algorithm on \(G\) is an SCC partition of \(G\): every block is nonempty and contains no vertex twice, blocks at different positions of the list are disjoint, every vertex of \(G\) lies in some block, two vertices lie in a common block exactly when they are strongly connected, and for every vertex \(m\) of a block \(B\) and every vertex \(v\), the vertices \(m\) and \(v\) are strongly connected exactly when \(v\) lies in \(B\).

public theorem components_isSCCPartition {V : Type u} [BEq V] [Hashable V]
    [LawfulBEq V] (graph : DirectedAdjacency V) :
    IsSCCPartition graph (components graph)
Uses 10
Statement usesDirected adjacency graph · SCC partition · Strongly connected components algorithm
Proof usesStrongly connected vertices · Each computed component is a full mutual-reachability class · Computed components have no repeated vertices · Computed components are nonempty · Computed components are pairwise disjoint · The computed components cover the vertex list · Vertices share a computed component exactly when strongly connected

DefinitionReachability between components#✓fully proved

In a directed graph \(G\), a list \(S\) of vertices reaches a list \(T\) of vertices when some vertex of \(S\) reaches some vertex of \(T\) by a directed path in \(G\), possibly of length zero.

public def ComponentReaches {V : Type u} (graph : DirectedAdjacency V)
    (source target : List V) : Prop :=
  ∃ sourceVertex ∈ source, ∃ targetVertex ∈ target,
    graph.Reachable sourceVertex targetVertex
Uses 2 · Used by 2
Statement usesDirected adjacency graph · Reachability in a directed graph
Used byThe condensation of the computed components is acyclic · Acyclic condensation

DefinitionAcyclic condensation#✓fully proved

A list \(\mathcal{B}\) of vertex lists of a directed graph \(G\) has an acyclic condensation when, for all \(S, T \in \mathcal{B}\), if some vertex of \(S\) reaches some vertex of \(T\) in \(G\) and some vertex of \(T\) reaches some vertex of \(S\), then \(S = T\). That is, reachability between the blocks is antisymmetric.

public def CondensationAcyclic {V : Type u} (graph : DirectedAdjacency V)
    (blocks : List (List V)) : Prop :=
  ∀ source ∈ blocks, ∀ target ∈ blocks,
    ComponentReaches graph source target →
      ComponentReaches graph target source → source = target
Uses 2 · Used by 1
Statement usesDirected adjacency graph · Reachability between components
Used byThe condensation of the computed components is acyclic

TheoremThe condensation of the computed components is acyclic#✓fully proved

Let \(G\) be a directed graph and let \(S\) and \(T\) be blocks returned by the strongly connected components algorithm on \(G\). If some vertex of \(S\) reaches some vertex of \(T\) and some vertex of \(T\) reaches some vertex of \(S\), then \(S = T\).

Equivalently, the condensation relation has no nontrivial directed cycle.

public theorem components_condensationAcyclic {V : Type u} [BEq V]
    [Hashable V] [LawfulBEq V] (graph : DirectedAdjacency V) :
    CondensationAcyclic graph (components graph)
Uses 14
Statement usesDirected adjacency graph · Acyclic condensation · Strongly connected components algorithm
Proof usesWhole-graph decreasing finish order · Edge of a directed adjacency graph · Reachability in a directed graph · Reachability between components · Strongly connected vertices · Strong connectivity is symmetric · Strong connectivity is transitive · Each computed component is a full mutual-reachability class · Computed components are pairwise disjoint · Executable mutual-reachability test · The mutual-reachability test is correct
19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.