Adjacency list

StructureDirected adjacency graph#✓fully proved

A directed adjacency graph on a type \(V\) consists of a list of vertices that has no duplicates and contains every element of \(V\) (so \(V\) is finite), together with, for each vertex \(v\), an ordered list of the out-neighbors of \(v\), in which entries may repeat.

structure DirectedAdjacency (V : Type u) where
  /-- The complete deterministic enumeration of vertices. -/
  vertices : List V
  /-- The vertex enumeration contains no duplicates. -/
  vertices_nodup : vertices.Nodup
  /-- Every vertex occurs in the enumeration. -/
  vertices_complete : ∀ vertex, vertex ∈ vertices
  /-- The ordered outgoing neighbors of each vertex. Entries may repeat. -/
  adjacency : V → List V

Used by 221

Used byComplete graph as an ordered adjacency · Neighbours in the complete adjacency · Serializing along a topological order preserves conflict equivalence · The serializability theorem · A rank increasing along precedence edges gives conflict serializability · A conflict-serializable schedule has an acyclic precedence graph · Precedence graph · Weight-forgetting directed graph · Adjacency entry count · Dense Dijkstra's algorithm · Dijkstra's distance is infinite exactly at unreachable vertices · Dijkstra's finite distances are lower bounds on walk weights · Dijkstra's finite distances are realized by walks · Relaxation count of dense Dijkstra · Minimum-selection count of dense Dijkstra · Dijkstra's path reconstruction fails exactly at infinite distance · Reconstructed Dijkstra paths are simple and have the output weight · Dijkstra's predecessor pointers satisfy the distance equation · Running time of dense Dijkstra · Walks of a given weight · Reachability via weighted walks · Johnson's algorithm · Correctness of Johnson's algorithm · Johnson's algorithm fails exactly on reachable negative cycles · Cost bound for Johnson's algorithm · Exact cost of a successful run of Johnson's algorithm · Shortest paths in a DAG with a topology check · Failure output of DAG shortest paths · Successful output of DAG shortest paths · Infinite DAG distances are exactly unreachable vertices · Finite DAG distances are at most every path weight · Edge relaxation count of the DAG pass · Finite non-source vertices have predecessors · Unreached vertices have no DAG shortest-path predecessor · Predecessor extraction fails exactly at infinite distances · Paths extracted after topological relaxation are shortest paths · Predecessor edges of the DAG shortest-path pass · The DAG shortest-path pass keeps its source · The DAG shortest-path pass gives the source distance zero · The source has no DAG shortest-path predecessor · The DAG shortest-path pass is charged one vertex visit per vertex · Bottleneck augmentation preserves feasibility · No augmenting path remains after Edmonds–Karp · Directed path · Augmenting paths have positive bottleneck · Distance-guided path reconstruction · Soundness of distance-guided path reconstruction · Residual graph · Shortest path via breadth-first search · The shortest-path search fails exactly when the sink is unreachable · The shortest-path search succeeds exactly when the sink is reachable · Soundness of the shortest-path search · Prim's algorithm with an indexed binary heap · Adjacency inspections of Prim's algorithm on a simple graph · Logarithmic heap cost of Prim's algorithm · Number of adjacency inspections in Prim's algorithm · Prim's algorithm returns a tree · Bound on key comparisons in Prim's algorithm · Prim's algorithm returns a minimum spanning tree · Parents returned by Prim's algorithm are adjacency-list neighbors · The root has no parent in Prim's algorithm · Erasing an edge leaves the other out-neighbour lists unchanged · Out-neighbours of the source after erasing an edge · Concatenation of walks · Edge of a directed adjacency graph · Edges after erasing an edge · Edges of the transpose graph · Erasing a directed edge · Erasing an edge twice gives the same out-neighbour lists · Boolean edge test · The Boolean edge test is correct · The erased edge is absent · Reachability in a directed graph · Reachability after erasing an edge implies reachability in the original graph · Semantically equivalent graphs have the same reachability · Reachability by walks · Reachability in the associated transition system · Reachability is the reflexive-transitive closure of the edge relation · Reachability in the transpose graph · Semantic equivalence of directed adjacency graphs is reflexive · Transposing twice gives a semantically equivalent graph · Semantic equivalence of directed adjacency graphs · Semantic equivalence of directed adjacency graphs is symmetric · The digraph of a directed adjacency graph · Adjacency in the associated digraph · The transition system of a directed adjacency graph · Semantic equivalence of directed adjacency graphs is transitive · Transpose of a directed adjacency graph · Transposition preserves semantic equivalence · Erasing an edge keeps the vertex enumeration · Walks of a given length · Walks after erasing an edge are walks in the original graph · Semantically equivalent graphs have the same walks · Splitting off the first edge of a walk · Walks in the transpose are reversed walks · Walks of length zero · Breadth-first search · The executable BFS agrees with the list model · Breadth-first search on the vertices \(0, \dots, n-1\) · List model of breadth-first search · Breadth-first search with parent pointers · Breadth-first search with parents returns the ordinary BFS result · Exact cost of BFS with parents · Linear bound on the cost of BFS with parents · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS discovers vertices in nondecreasing distance · BFS lists exactly the reachable vertices · BFS discovers each vertex at most once · Path reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Cost of path reconstruction for an unreachable vertex · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · A BFS parent is one step closer to the source · BFS parents are joined by graph edges · The BFS parent is the first discovered in-neighbour · Exactly the source and the unreachable vertices have no BFS parent · The saved-parent relation is acyclic · Breadth-first search places the source at distance zero · A DFS child finishes before its parent · Decreasing finish order · Whole-graph decreasing finish order · Whole-graph decreasing finish order has no repeated vertices · Decreasing finish order has no repeated vertices · Left-first depth-first search · Depth-first search of the whole graph · Exact transition count of whole-graph depth-first search · Exact transition count of depth-first search · Executable DFS meets the left-first specification · The left-first DFS specification determines the traversal · A DFS forest root has no parent · DFS forest roots are scheduled roots · DFS forest roots are distinct · Left-first depth-first traversals · Whole-graph decreasing finish order contains every vertex · Decreasing finish order lists exactly the vertices reachable from the roots · Whole-graph DFS finishes every vertex · Whole-graph DFS discovers every vertex · Every discovered vertex is a forest root or has a unique parent · Depth-first search finishes exactly the reachable vertices · Depth-first search discovers exactly the reachable vertices · In preorder, a DFS parent precedes its child · In decreasing finish order, a DFS parent precedes its child · Parent chains in a DFS forest end at a forest root · No vertex is recorded twice as a DFS child · DFS parent pairs are graph edges · The DFS parent relation is acyclic · DFS finishes each vertex at most once · Depth-first search discovers every reachable vertex · Depth-first search discovers each vertex at most once · Depth-first search discovers only reachable vertices · Sequences of depth-first search machine steps · Edge list of a directed graph · Edge list of an adjacency function · Euler circuit criterion for directed multigraphs · Euler path criterion for directed multigraphs · Hierholzer's algorithm · Hierholzer's algorithm finds Euler circuits in directed multigraphs · Hierholzer's algorithm finds Euler paths in directed multigraphs · Running time of Hierholzer's algorithm · Hierholzer's algorithm returns a trail in a directed multigraph · Balanced directed multigraph · A directed multigraph with an Euler circuit is balanced · Euler circuit in a directed multigraph · Euler path in a directed multigraph · Semi-balanced directed multigraph · A directed multigraph with an Euler path is semi-balanced · Contract of Hierholzer's recursion · Each computed component is a full mutual-reachability class · Reachability between components · Strongly connected components algorithm · 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 · Acyclic condensation · SCC partition · The computed components cover the vertex list · Executable mutual-reachability test · The mutual-reachability test is correct · Vertices share a computed component exactly when strongly connected · Strongly connected vertices · Strong connectivity is reflexive · Strong connectivity as an equivalence relation · Strong connectivity is symmetric · Strong connectivity is transitive · Kahn's algorithm succeeds on acyclic graphs · Directed cycle within a vertex list · Characterization of directed cycles within a vertex list · A failed Kahn run leaves a directed cycle · Unprocessed vertices of a failed Kahn run have positive indegree among the unprocessed · A failed Kahn run splits the vertices into processed and unprocessed ones · Indegree · Indegree within a vertex list · Acyclic directed graph · Acyclicity means having no directed cycle · Topological order · Kahn's topological sort · Kahn's algorithm succeeds exactly on acyclic graphs · A successful topological sort lists every vertex · A successful topological sort points every edge forward · Success of Kahn's algorithm implies acyclicity · A successful topological sort is a topological order · A successful topological sort has no repeated vertex · A* search · A* leaves exactly the unreachable vertices at infinity · A* with a consistent heuristic is optimal · A*'s finite path weights are realized by paths · The final keys of A* · A*'s predecessor paths are simple and realize its path weights · A*'s predecessor edges are tight · Cost of A* · Admissible heuristic · A consistent heuristic that vanishes at the goal is admissible · Consistent heuristic · Reduced weights telescope along paths · Implication graph as a finite directed graph · Reachability in the finite implication graph

DefinitionEdge of a directed adjacency graph#✓fully proved

For a directed adjacency graph \(G\) on \(V\) and vertices \(s, t \in V\), there is an edge from \(s\) to \(t\) in \(G\) when \(t\) occurs in the adjacency list of \(s\).

def DirectedAdjacency.Edge {V : Type u} (graph : DirectedAdjacency V)
    (source target : V) : Prop :=
  target ∈ graph.adjacency source

Uses 1 · Used by 118

Statement usesDirected adjacency graph

Used bySerializing along a topological order preserves conflict equivalence · The serializability theorem · A rank increasing along precedence edges gives conflict serializability · A conflict-serializable schedule has an acyclic precedence graph · Edges of the weight-forgetting graph · Weighted paths give walks of the same length · Reachability by weighted paths · Dijkstra's distance is infinite exactly at unreachable vertices · Dijkstra's finite distances are lower bounds on walk weights · Dijkstra's finite distances are realized by walks · Relaxation count of dense Dijkstra · Dijkstra's path reconstruction fails exactly at infinite distance · Reconstructed Dijkstra paths are simple and have the output weight · Dijkstra's predecessor pointers satisfy the distance equation · Walks of a given weight · Reachability via weighted walks · Correctness of Johnson's algorithm · Infinite DAG distances are exactly unreachable vertices · Finite DAG distances are at most every path weight · Edge relaxation count of the DAG pass · Finite non-source vertices have predecessors · Unreached vertices have no DAG shortest-path predecessor · Predecessor extraction fails exactly at infinite distances · Paths extracted after topological relaxation are shortest paths · Predecessor edges of the DAG shortest-path pass · The DAG shortest-path pass keeps its source · The DAG shortest-path pass gives the source distance zero · The source has no DAG shortest-path predecessor · The DAG shortest-path pass is charged one vertex visit per vertex · Bottleneck augmentation preserves feasibility · Maximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · No augmenting path remains after Edmonds–Karp · The augmentation loop never decreases the flow value · One augmentation step keeps or strictly raises the flow value · Directed path · The Edmonds-Karp residual cut separates source and sink · Augmenting paths have positive bottleneck · Soundness of distance-guided path reconstruction · Edges of the residual graph · The shortest-path search succeeds exactly when the sink is reachable · Soundness of the shortest-path search · Concatenation of walks · Edges after erasing an edge · Edges of the transpose graph · The Boolean edge test is correct · Reachability in a directed graph · Reachability by walks · Reachability in the associated transition system · Reachability is the reflexive-transitive closure of the edge relation · Semantic equivalence of directed adjacency graphs is reflexive · Transposing twice gives a semantically equivalent graph · Semantic equivalence of directed adjacency graphs · Semantic equivalence of directed adjacency graphs is symmetric · The digraph of a directed adjacency graph · Adjacency in the associated digraph · The transition system of a directed adjacency graph · Semantic equivalence of directed adjacency graphs is transitive · Transposition preserves semantic equivalence · Walks of a given length · Walks after erasing an edge are walks in the original graph · Semantically equivalent graphs have the same walks · Splitting off the first edge of a walk · Walks in the transpose are reversed walks · Walks of length zero · The executable BFS agrees with the list model · Exact cost of BFS with parents · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS discovers vertices in nondecreasing distance · BFS lists exactly the reachable vertices · BFS discovers each vertex at most once · Path reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Cost of path reconstruction for an unreachable vertex · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · A BFS parent is one step closer to the source · BFS parents are joined by graph edges · The BFS parent is the first discovered in-neighbour · Exactly the source and the unreachable vertices have no BFS parent · The saved-parent relation is acyclic · Breadth-first search places the source at distance zero · DFS forest roots are scheduled roots · Whole-graph decreasing finish order contains every vertex · Whole-graph DFS finishes every vertex · Whole-graph DFS discovers every vertex · In preorder, a DFS parent precedes its child · No vertex is recorded twice as a DFS child · DFS parent pairs are graph edges · Depth-first search discovers every reachable vertex · Depth-first search discovers only reachable vertices · Euler circuit criterion for directed multigraphs · Euler path criterion for directed multigraphs · Hierholzer's algorithm finds Euler circuits in directed multigraphs · Hierholzer's algorithm finds Euler paths in directed multigraphs · Running time of Hierholzer's algorithm · The condensation of the computed components is acyclic · Strong connectivity is reflexive · Strong connectivity is transitive · Kahn's algorithm succeeds on acyclic graphs · Directed cycle within a vertex list · Characterization of directed cycles within a vertex list · A failed Kahn run leaves a directed cycle · Topological order · A successful topological sort points every edge forward · Success of Kahn's algorithm implies acyclicity · A successful topological sort is a topological order · A* with a consistent heuristic is optimal · A*'s finite path weights are realized by paths · The final keys of A* · A*'s predecessor paths are simple and realize its path weights · A*'s predecessor edges are tight · A consistent heuristic that vanishes at the goal is admissible · Consistent heuristic · Reduced weights telescope along paths · Reachability in the finite implication graph

AbbreviationWalks of a given length#✓fully proved

For a directed adjacency graph \(G\), a natural number \(n\) and vertices \(s\) and \(t\), there is a walk of length \(n\) from \(s\) to \(t\) in \(G\) when there are vertices \(v_0, \dots, v_n\) with \(v_0 = s\) and \(v_n = t\) such that \((v_i, v_{i+1})\) is an edge of \(G\) for every \(i < n\).

abbrev DirectedAdjacency.Walk {V : Type u} (graph : DirectedAdjacency V)
    (length : Nat) (source target : V) : Prop :=
  Relation.RelatesInSteps graph.Edge source target length

Uses 2 · Used by 32

Statement usesDirected adjacency graph · Edge of a directed adjacency graph

Used byWeighted paths give walks of the same length · Reachability by weighted paths · Reachability via weighted walks · Infinite DAG distances are exactly unreachable vertices · Finite DAG distances are at most every path weight · Finite non-source vertices have predecessors · Unreached vertices have no DAG shortest-path predecessor · Predecessor edges of the DAG shortest-path pass · The DAG shortest-path pass keeps its source · The DAG shortest-path pass gives the source distance zero · The source has no DAG shortest-path predecessor · The shortest-path search succeeds exactly when the sink is reachable · Soundness of the shortest-path search · Concatenation of walks · Reachability after erasing an edge implies reachability in the original graph · Semantically equivalent graphs have the same reachability · Reachability by walks · Reachability in the associated transition system · Reachability in the transpose graph · Walks after erasing an edge are walks in the original graph · Semantically equivalent graphs have the same walks · Splitting off the first edge of a walk · Walks in the transpose are reversed walks · Walks of length zero · The executable BFS agrees with the list model · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS discovers vertices in nondecreasing distance · BFS lists exactly the reachable vertices · BFS discovers each vertex at most once · Reconstructed BFS paths are shortest paths · Breadth-first search places the source at distance zero

DefinitionThe digraph of a directed adjacency graph#✓fully proved

The digraph associated with a directed adjacency graph \(G\) on a vertex type \(V\) is the directed graph on \(V\) in which \(s\) is adjacent to \(t\) exactly when \(G\) has an edge from \(s\) to \(t\). It forgets the order of the adjacency lists and the multiplicity of their entries.

def toDigraph (graph : DirectedAdjacency V) : Digraph V where
  Adj := graph.Edge

Uses 2 · Used by 1

Statement usesDirected adjacency graph · Edge of a directed adjacency graph

Used byAdjacency in the associated digraph

TheoremAdjacency in the associated digraph#✓fully proved

For a directed adjacency graph \(G\) and vertices \(s\) and \(t\), \(s\) is adjacent to \(t\) in the digraph associated with \(G\) if and only if \(G\) has an edge from \(s\) to \(t\), that is, \(t\) occurs in the adjacency list of \(s\).

@[simp]
theorem toDigraph_adj : graph.toDigraph.Adj source target ↔ graph.Edge source target

Uses 3

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · The digraph of a directed adjacency graph

TheoremWalks of length zero#✓fully proved

In a directed adjacency graph, there is a walk of length \(0\) from a vertex \(s\) to a vertex \(t\) if and only if \(s = t\).

@[simp]
theorem walk_zero_iff : Walk graph 0 source target ↔ source = target

Uses 3 · Used by 1

Statement usesDirected adjacency graph · Walks of a given length

Proof usesEdge of a directed adjacency graph

Used byThe shortest-path search succeeds exactly when the sink is reachable

TheoremSplitting off the first edge of a walk#✓fully proved

In a directed adjacency graph \(G\), for every natural number \(n\) and all vertices \(s\) and \(t\), there is a walk of length \(n + 1\) from \(s\) to \(t\) if and only if there is a vertex \(v\) such that \((s, v)\) is an edge of \(G\) and there is a walk of length \(n\) from \(v\) to \(t\).

theorem walk_succ_iff :
    Walk graph (Nat.succ length) source target ↔
      ∃ next, graph.Edge source next ∧ Walk graph length next target

Uses 3 · Used by 1

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Walks of a given length

Used byThe shortest-path search succeeds exactly when the sink is reachable

TheoremConcatenation of walks#✓fully proved

Let \(G\) be a directed adjacency graph on \(V\) and let \(s, m, t \in V\). If \(G\) has a walk of length exactly \(a\) from \(s\) to \(m\) and a walk of length exactly \(b\) from \(m\) to \(t\), then \(G\) has a walk of length exactly \(a + b\) from \(s\) to \(t\).

theorem Walk.append
    (left : Walk graph leftLength source middle)
    (right : Walk graph rightLength middle target) :
    Walk graph (leftLength + rightLength) source target

Uses 3

Statement usesDirected adjacency graph · Walks of a given length

Proof usesEdge of a directed adjacency graph

DefinitionReachability in a directed graph#✓fully proved

For a directed adjacency graph \(G\) and vertices \(s\) and \(t\), \(t\) is reachable from \(s\) when the pair \((s, t)\) lies in the reflexive-transitive closure of the edge relation of \(G\): either \(s = t\), or a finite sequence of edges of \(G\) leads from \(s\) to \(t\).

def Reachable (graph : DirectedAdjacency V) (source target : V) : Prop :=
  Relation.ReflTransGen graph.Edge source target

Uses 2 · Used by 58

Statement usesDirected adjacency graph · Edge of a directed adjacency graph

Used byBellman-Ford leaves exactly the unreachable vertices at infinite distance · Reachability by weighted paths · Dijkstra's distance is infinite exactly at unreachable vertices · Dijkstra's finite distances are lower bounds on walk weights · Dijkstra's finite distances are realized by walks · Relaxation count of dense Dijkstra · Dijkstra's path reconstruction fails exactly at infinite distance · Reconstructed Dijkstra paths are simple and have the output weight · Dijkstra's predecessor pointers satisfy the distance equation · Reachability via weighted walks · Correctness of Johnson's algorithm · Unreachable vertices are exactly those at infinite DAG distance · Infinite DAG distances are exactly unreachable vertices · Maximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · No augmenting path remains after Edmonds–Karp · The Edmonds-Karp residual cut separates source and sink · The shortest-path search fails exactly when the sink is unreachable · The shortest-path search succeeds exactly when the sink is reachable · Reachability after erasing an edge implies reachability in the original graph · Semantically equivalent graphs have the same reachability · Reachability by walks · Reachability in the associated transition system · Reachability is the reflexive-transitive closure of the edge relation · Reachability in the transpose graph · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS lists exactly the reachable vertices · Path reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Cost of path reconstruction for an unreachable vertex · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · Exactly the source and the unreachable vertices have no BFS parent · Whole-graph decreasing finish order contains every vertex · Decreasing finish order lists exactly the vertices reachable from the roots · Whole-graph DFS finishes every vertex · Whole-graph DFS discovers every vertex · Depth-first search finishes exactly the reachable vertices · Depth-first search discovers exactly the reachable vertices · Depth-first search discovers every reachable vertex · Depth-first search discovers only reachable vertices · Euler circuit criterion for directed multigraphs · Euler path criterion for directed multigraphs · Hierholzer's algorithm finds Euler circuits in directed multigraphs · Hierholzer's algorithm finds Euler paths in directed multigraphs · Running time of Hierholzer's algorithm · Reachability between components · The condensation of the computed components is acyclic · The mutual-reachability test is correct · Strongly connected vertices · Strong connectivity is reflexive · Strong connectivity is symmetric · Strong connectivity is transitive · A* leaves exactly the unreachable vertices at infinity · Correctness of the SCC-based 2-SAT procedure · Reachability in the finite implication graph

TheoremReachability by walks#✓fully proved

In a directed adjacency graph \(G\), a vertex \(t\) is reachable from a vertex \(s\) if and only if there is a natural number \(n\) such that \(G\) has a walk of length exactly \(n\) from \(s\) to \(t\).

theorem reachable_iff_exists_walk :
    graph.Reachable source target ↔ ∃ length, Walk graph length source target

Uses 4 · Used by 10

Statement usesDirected adjacency graph · Reachability in a directed graph · Walks of a given length

Proof usesEdge of a directed adjacency graph

Used byReachability by weighted paths · Reachability via weighted walks · The shortest-path search succeeds exactly when the sink is reachable · Reachability after erasing an edge implies reachability in the original graph · Semantically equivalent graphs have the same reachability · Reachability in the associated transition system · Reachability in the transpose graph · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS lists exactly the reachable vertices

TheoremReachability is the reflexive-transitive closure of the edge relation#✓fully proved

In a directed adjacency graph \(G\), a vertex \(t\) is reachable from a vertex \(s\) if and only if \((s, t)\) lies in the reflexive-transitive closure of the edge relation of \(G\).

theorem reachable_iff_reflTransGen :
    graph.Reachable source target ↔
      Relation.ReflTransGen graph.Edge source target

Uses 3

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Reachability in a directed graph

DefinitionThe transition system of a directed adjacency graph#✓fully proved

The labelled transition system of a directed adjacency graph \(G\) has the vertices of \(G\) as states and a single label, and it has a transition from \(s\) to \(t\) exactly when \(G\) has an edge from \(s\) to \(t\).

def toLTS (graph : DirectedAdjacency V) : _root_.Cslib.LTS V Unit where
  Tr source _ target := graph.Edge source target

Uses 2 · Used by 1

Statement usesDirected adjacency graph · Edge of a directed adjacency graph

Used byReachability in the associated transition system

TheoremReachability in the associated transition system#✓fully proved

In a directed adjacency graph \(G\), a vertex \(t\) is reachable from a vertex \(s\) if and only if, in the unit-labelled labelled transition system of \(G\), there is a finite list of labels along which \(s\) reaches \(t\) by a multistep transition.

theorem reachable_iff_lts :
    graph.Reachable source target ↔
      ∃ labels, graph.toLTS.MTr source labels target

Uses 6

Statement usesDirected adjacency graph · Reachability in a directed graph · The transition system of a directed adjacency graph

Proof usesEdge of a directed adjacency graph · Walks of a given length · Reachability by walks

DefinitionTranspose of a directed adjacency graph#✓fully proved

For a directed adjacency graph \(G\) on a vertex type with decidable equality, the transpose of \(G\) has the same vertex enumeration as \(G\), and the adjacency list of a vertex \(v\) consists of the vertices \(u\) such that \(v\) occurs in the adjacency list of \(u\) in \(G\), each listed once and in the order of the vertex enumeration.

def transpose [DecidableEq V] (graph : DirectedAdjacency V) : DirectedAdjacency V where
  vertices := graph.vertices
  vertices_nodup := graph.vertices_nodup
  vertices_complete := graph.vertices_complete
  adjacency target := graph.vertices.filter fun source => target ∈ graph.adjacency source

Uses 1 · Used by 8

Statement usesDirected adjacency graph

Used byShortest path via breadth-first search · The shortest-path search succeeds exactly when the sink is reachable · Soundness of the shortest-path search · Edges of the transpose graph · Reachability in the transpose graph · Transposing twice gives a semantically equivalent graph · Transposition preserves semantic equivalence · Walks in the transpose are reversed walks

TheoremEdges of the transpose graph#✓fully proved

Let \(V\) have decidable equality and let \(G\) be a directed adjacency graph on \(V\). For all \(s, t \in V\), the transpose of \(G\) has an edge from \(s\) to \(t\) if and only if \(G\) has an edge from \(t\) to \(s\).

@[simp]
theorem edge_transpose [DecidableEq V] :
    (graph.transpose).Edge source target ↔ graph.Edge target source

Uses 3 · Used by 3

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Transpose of a directed adjacency graph

Used byTransposing twice gives a semantically equivalent graph · Transposition preserves semantic equivalence · Walks in the transpose are reversed walks

TheoremWalks in the transpose are reversed walks#✓fully proved

For a directed adjacency graph \(G\) on a vertex type with decidable equality, every natural number \(n\) and all vertices \(s\) and \(t\), there is a walk of length \(n\) from \(s\) to \(t\) in the transpose of \(G\) if and only if there is a walk of length \(n\) from \(t\) to \(s\) in \(G\).

theorem walk_transpose_iff [DecidableEq V] :
    Walk graph.transpose length source target ↔ Walk graph length target source

Uses 5 · Used by 3

Statement usesDirected adjacency graph · Walks of a given length · Transpose of a directed adjacency graph

Proof usesEdge of a directed adjacency graph · Edges of the transpose graph

Used byThe shortest-path search succeeds exactly when the sink is reachable · Soundness of the shortest-path search · Reachability in the transpose graph

TheoremReachability in the transpose graph#✓fully proved

Let \(G\) be a directed adjacency graph on a vertex type with decidable equality, and let \(G^{\mathsf{T}}\) be its transpose. For all vertices \(s\) and \(t\), \(t\) is reachable from \(s\) in \(G^{\mathsf{T}}\) if and only if \(s\) is reachable from \(t\) in \(G\).

theorem reachable_transpose_iff [DecidableEq V] :
    graph.transpose.Reachable source target ↔ graph.Reachable target source

Uses 6 · Used by 1

Statement usesDirected adjacency graph · Reachability in a directed graph · Transpose of a directed adjacency graph

Proof usesWalks of a given length · Reachability by walks · Walks in the transpose are reversed walks

Used byThe shortest-path search succeeds exactly when the sink is reachable

DefinitionSemantic equivalence of directed adjacency graphs#✓fully proved

Two directed adjacency graphs \(G_1\) and \(G_2\) on the same vertex type are semantically equivalent when they have the same edges: for all vertices \(s\) and \(t\), \(G_1\) has an edge from \(s\) to \(t\) if and only if \(G_2\) does.

def SemanticallyEquivalent (graph₁ graph₂ : DirectedAdjacency V) : Prop :=
  ∀ source target, graph₁.Edge source target ↔ graph₂.Edge source target

Uses 2 · Used by 7

Statement usesDirected adjacency graph · Edge of a directed adjacency graph

Used bySemantically equivalent graphs have the same reachability · Semantic equivalence of directed adjacency graphs is reflexive · Transposing twice gives a semantically equivalent graph · Semantic equivalence of directed adjacency graphs is symmetric · Semantic equivalence of directed adjacency graphs is transitive · Transposition preserves semantic equivalence · Semantically equivalent graphs have the same walks

TheoremSemantic equivalence of directed adjacency graphs is reflexive#✓fully proved

Every directed adjacency graph \(G\) is semantically equivalent to itself.

@[refl]
theorem semanticEquivalent_refl : SemanticallyEquivalent graph graph

Uses 3

Statement usesDirected adjacency graph · Semantic equivalence of directed adjacency graphs

Proof usesEdge of a directed adjacency graph

TheoremSemantic equivalence of directed adjacency graphs is symmetric#✓fully proved

If a directed adjacency graph \(G_1\) is semantically equivalent to a directed adjacency graph \(G_2\), then \(G_2\) is semantically equivalent to \(G_1\).

@[symm]
theorem SemanticallyEquivalent.symm
    (equivalent : SemanticallyEquivalent graph₁ graph₂) :
    SemanticallyEquivalent graph₂ graph₁

Uses 3

Statement usesDirected adjacency graph · Semantic equivalence of directed adjacency graphs

Proof usesEdge of a directed adjacency graph

TheoremSemantic equivalence of directed adjacency graphs is transitive#✓fully proved

If a directed adjacency graph \(G_1\) is semantically equivalent to \(G_2\), and \(G_2\) is semantically equivalent to \(G_3\), then \(G_1\) is semantically equivalent to \(G_3\).

@[trans]
theorem SemanticallyEquivalent.trans
    (equivalent₁₂ : SemanticallyEquivalent graph₁ graph₂)
    (equivalent₂₃ : SemanticallyEquivalent graph₂ graph₃) :
    SemanticallyEquivalent graph₁ graph₃

Uses 3

Statement usesDirected adjacency graph · Semantic equivalence of directed adjacency graphs

Proof usesEdge of a directed adjacency graph

TheoremSemantically equivalent graphs have the same walks#✓fully proved

If two directed adjacency graphs \(G_1\) and \(G_2\) are semantically equivalent, then for every natural number \(n\) and all vertices \(s\) and \(t\), there is a walk of length \(n\) from \(s\) to \(t\) in \(G_1\) if and only if there is a walk of length \(n\) from \(s\) to \(t\) in \(G_2\).

theorem SemanticallyEquivalent.walk_iff
    (equivalent : SemanticallyEquivalent graph₁ graph₂) :
    Walk graph₁ length source target ↔ Walk graph₂ length source target

Uses 4 · Used by 1

Statement usesDirected adjacency graph · Semantic equivalence of directed adjacency graphs · Walks of a given length

Proof usesEdge of a directed adjacency graph

Used bySemantically equivalent graphs have the same reachability

TheoremSemantically equivalent graphs have the same reachability#✓fully proved

If two directed adjacency graphs \(G_1\) and \(G_2\) on \(V\) are semantically equivalent, then for all \(s, t \in V\), \(t\) is reachable from \(s\) in \(G_1\) if and only if \(t\) is reachable from \(s\) in \(G_2\).

theorem SemanticallyEquivalent.reachable_iff
    (equivalent : SemanticallyEquivalent graph₁ graph₂) :
    graph₁.Reachable source target ↔ graph₂.Reachable source target

Uses 6 · Used by 1

Statement usesDirected adjacency graph · Reachability in a directed graph · Semantic equivalence of directed adjacency graphs

Proof usesSemantically equivalent graphs have the same walks · Walks of a given length · Reachability by walks

Used byCorrectness of Johnson's algorithm

TheoremTransposition preserves semantic equivalence#✓fully proved

For directed adjacency graphs \(G_1\) and \(G_2\) on a vertex type with decidable equality, if \(G_1\) and \(G_2\) are semantically equivalent, then their transposes are semantically equivalent.

theorem SemanticallyEquivalent.transpose [DecidableEq V]
    (equivalent : SemanticallyEquivalent graph₁ graph₂) :
    SemanticallyEquivalent graph₁.transpose graph₂.transpose

Uses 5

Statement usesDirected adjacency graph · Semantic equivalence of directed adjacency graphs · Transpose of a directed adjacency graph

Proof usesEdge of a directed adjacency graph · Edges of the transpose graph

TheoremTransposing twice gives a semantically equivalent graph#✓fully proved

Let \(G\) be a directed adjacency graph on a vertex type with decidable equality. The transpose of the transpose of \(G\) is semantically equivalent to \(G\), that is, it has exactly the same edges as \(G\).

theorem semanticEquivalent_transpose_transpose [DecidableEq V] :
    SemanticallyEquivalent graph.transpose.transpose graph

Uses 5

Statement usesDirected adjacency graph · Semantic equivalence of directed adjacency graphs · Transpose of a directed adjacency graph

Proof usesEdge of a directed adjacency graph · Edges of the transpose graph

DefinitionBoolean edge test#✓fully proved

For a type \(V\) with decidable equality, a directed adjacency graph \(G\) on \(V\) and vertices \(s, t \in V\), the edge test of \(G\) at \((s, t)\) is the Boolean value that is true exactly when \(t\) occurs in the adjacency list of \(s\).

public def hasEdge {α : Type u} [DecidableEq α]
    (g : DirectedAdjacency α) (source target : α) : Bool :=
  decide (target ∈ g.adjacency source)

Uses 1 · Used by 10

Statement usesDirected adjacency graph

Used byThe Boolean edge test is correct · The erased edge is absent · A failed Kahn run leaves a directed cycle · Unprocessed vertices of a failed Kahn run have positive indegree among the unprocessed · A failed Kahn run splits the vertices into processed and unprocessed ones · Indegree within a vertex list · Kahn's topological sort · A successful topological sort lists every vertex · A successful topological sort points every edge forward · A successful topological sort has no repeated vertex

TheoremThe Boolean edge test is correct#✓fully proved

For a type \(V\) with decidable equality, a directed adjacency graph \(G\) on \(V\) and vertices \(s, t \in V\), the Boolean edge test of \(G\) at \((s, t)\) returns true if and only if \(G\) has an edge from \(s\) to \(t\).

public theorem hasEdge_eq_true {α : Type u} [DecidableEq α]
    (g : DirectedAdjacency α) (source target : α) :
    g.hasEdge source target = true ↔ g.Edge source target

Uses 3 · Used by 2

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Boolean edge test

Used byA failed Kahn run leaves a directed cycle · A successful topological sort points every edge forward

DefinitionErasing a directed edge#✓fully proved

Given a directed-adjacency graph \(G\) and vertices \(s\) and \(t\), erasing the edge \(s \to t\) gives the directed-adjacency graph with the same vertex enumeration as \(G\) whose out-neighbour list at \(s\) is the out-neighbour list of \(s\) in \(G\) with every occurrence of \(t\) removed (the remaining entries keep their order), and whose out-neighbour list at every other vertex is the same as in \(G\).

def eraseEdge [DecidableEq V] (graph : DirectedAdjacency V)
    (source target : V) : DirectedAdjacency V where
  vertices := graph.vertices
  vertices_nodup := graph.vertices_nodup
  vertices_complete := graph.vertices_complete
  adjacency vertex :=
    if vertex = source then
      (graph.adjacency vertex).filter fun neighbor => decide (neighbor ≠ target)
    else
      graph.adjacency vertex

Uses 1 · Used by 8

Statement usesDirected adjacency graph

Used byErasing an edge leaves the other out-neighbour lists unchanged · Out-neighbours of the source after erasing an edge · Edges after erasing an edge · Erasing an edge twice gives the same out-neighbour lists · The erased edge is absent · Reachability after erasing an edge implies reachability in the original graph · Erasing an edge keeps the vertex enumeration · Walks after erasing an edge are walks in the original graph

TheoremErasing an edge keeps the vertex enumeration#✓fully proved

For every directed-adjacency graph \(G\) and vertices \(s\) and \(t\), the graph obtained from \(G\) by erasing the edge \(s \to t\) has the same vertex enumeration as \(G\): the same list of vertices, in the same order.

@[simp]
theorem vertices_eraseEdge [DecidableEq V] :
    (eraseEdge graph source target).vertices = graph.vertices

Uses 2

Statement usesDirected adjacency graph · Erasing a directed edge

TheoremOut-neighbours of the source after erasing an edge#✓fully proved

For every directed-adjacency graph \(G\) and vertices \(s\) and \(t\), the out-neighbour list of \(s\) in the graph obtained from \(G\) by erasing the edge \(s \to t\) is the out-neighbour list of \(s\) in \(G\) with every occurrence of \(t\) removed, the remaining entries kept in their original order.

@[simp]
theorem adjacency_eraseEdge_source [DecidableEq V] :
    (eraseEdge graph source target).adjacency source =
      (graph.adjacency source).filter (fun vertex => decide (vertex ≠ target))

Uses 2

Statement usesDirected adjacency graph · Erasing a directed edge

TheoremErasing an edge leaves the other out-neighbour lists unchanged#✓fully proved

For every directed-adjacency graph \(G\) and vertices \(s\), \(t\) and \(u\) with \(u \ne s\), the out-neighbour list of \(u\) in the graph obtained from \(G\) by erasing the edge \(s \to t\) equals the out-neighbour list of \(u\) in \(G\).

theorem adjacency_eraseEdge_of_ne [DecidableEq V]
    (different : left ≠ source) :
    (eraseEdge graph source target).adjacency left = graph.adjacency left

Uses 2

Statement usesDirected adjacency graph · Erasing a directed edge

TheoremEdges after erasing an edge#✓fully proved

For every directed-adjacency graph \(G\) and vertices \(s\), \(t\), \(u\) and \(v\), there is an edge from \(u\) to \(v\) in the graph obtained from \(G\) by erasing the edge \(s \to t\) if and only if there is an edge from \(u\) to \(v\) in \(G\) and it is not the case that both \(u = s\) and \(v = t\).

@[simp]
theorem edge_eraseEdge [DecidableEq V] :
    (eraseEdge graph source target).Edge left right ↔
      graph.Edge left right ∧ ¬(left = source ∧ right = target)

Uses 3 · Used by 1

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Erasing a directed edge

Used byWalks after erasing an edge are walks in the original graph

TheoremThe erased edge is absent#✓fully proved

For every directed-adjacency graph \(G\) and vertices \(s\) and \(t\), the Boolean edge lookup for \(s \to t\) in the graph obtained from \(G\) by erasing the edge \(s \to t\) returns false.

@[simp]
theorem hasEdge_eraseEdge_self [DecidableEq V] :
    (eraseEdge graph source target).hasEdge source target = false

Uses 3

Statement usesDirected adjacency graph · Erasing a directed edge · Boolean edge test

TheoremErasing an edge twice gives the same out-neighbour lists#✓fully proved

For every directed-adjacency graph \(G\) and vertices \(s\) and \(t\), erasing the edge \(s \to t\) from \(G\) and then erasing it again gives, at every vertex, the same out-neighbour list as erasing it once.

theorem eraseEdge_idempotent [DecidableEq V] :
    (eraseEdge (eraseEdge graph source target) source target).adjacency =
      (eraseEdge graph source target).adjacency

Uses 2

Statement usesDirected adjacency graph · Erasing a directed edge

TheoremWalks after erasing an edge are walks in the original graph#✓fully proved

For every directed-adjacency graph \(G\), vertices \(s\), \(t\), \(u\) and \(v\), and natural number \(n\), if there is a walk of length \(n\) from \(u\) to \(v\) in the graph obtained from \(G\) by erasing the edge \(s \to t\), then there is a walk of length \(n\) from \(u\) to \(v\) in \(G\).

theorem walk_eraseEdge_imp [DecidableEq V]
    (walk : Walk (eraseEdge graph source target) length left right) :
    Walk graph length left right

Uses 5 · Used by 1

Statement usesDirected adjacency graph · Walks of a given length · Erasing a directed edge

Proof usesEdge of a directed adjacency graph · Edges after erasing an edge

Used byReachability after erasing an edge implies reachability in the original graph

TheoremReachability after erasing an edge implies reachability in the original graph#✓fully proved

For every directed-adjacency graph \(G\) and vertices \(s\), \(t\), \(u\) and \(v\), if \(v\) is reachable from \(u\) in the graph obtained from \(G\) by erasing the edge \(s \to t\), then \(v\) is reachable from \(u\) in \(G\).

theorem reachable_eraseEdge_imp [DecidableEq V]
    (reachable : (eraseEdge graph source target).Reachable left right) :
    graph.Reachable left right

Uses 6

Statement usesDirected adjacency graph · Reachability in a directed graph · Erasing a directed edge

Proof usesWalks of a given length · Reachability by walks · Walks after erasing an edge are walks in the original graph

36 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.