Depth-first search

StructureDepth-first traversal record#✓fully proved

A traversal over a vertex type \(V\) consists of three lists: a preorder (discovery order) list of vertices, a postorder (finish order) list of vertices, and a list of parent pairs in \(V \times V\), each stored as \((\text{child}, \text{parent})\).

No condition relating the three lists is imposed by the record itself.

structure Traversal (V : Type u) where
  preorder : List V
  postorder : List V
  parents : List (V × V)
deriving Repr, DecidableEq

Used by 32

Used byA DFS child finishes before its parent · Decreasing finish order · 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 · Roots of a DFS forest · DFS forest roots are distinct · Left-first depth-first traversals · 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 · Executable mutual-reachability test · The mutual-reachability test is correct

DefinitionLeft-first depth-first search#✓fully proved

Given a directed graph \(G\) with ordered adjacency lists and an ordered list of roots, depth-first search processes the roots from left to right, skipping roots already visited. Visiting an unvisited vertex \(v\) marks it visited and records its discovery, then processes the out-neighbours of \(v\) in adjacency-list order, visiting each one not yet visited at that moment and recording \(v\) as its parent, and finally records that \(v\) has finished. The result is the traversal consisting of the vertices in discovery order (preorder), the vertices in finish order (postorder), and the (child, parent) pairs in the order the children were discovered.

def dfs {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) : Traversal V :=
  finish (loop adj roots (initial roots))

Uses 2 · Used by 28

Statement usesDepth-first traversal record · Directed adjacency graph

Used byA DFS child finishes before its parent · Decreasing finish order · Decreasing finish order has no repeated vertices · 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 · Decreasing finish order lists exactly the vertices reachable from the roots · Whole-graph DFS finishes 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 · Executable mutual-reachability test · The mutual-reachability test is correct

AbbreviationSequences of depth-first search machine steps#✓fully proved

Zero or more independent DFS machine steps.

abbrev Steps {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) :=
  Relation.ReflTransGen (Step adj roots)

Uses 1 · Used by 14

Statement usesDirected adjacency graph

Used byA DFS child finishes before its parent · Exact transition count of depth-first search · Executable DFS meets the left-first specification · The left-first DFS specification determines the traversal · DFS forest roots are scheduled roots · Left-first depth-first traversals · Depth-first search finishes exactly the reachable vertices · In preorder, a DFS parent precedes its child · No vertex is recorded twice as a DFS child · DFS parent pairs are graph edges · 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

DefinitionLeft-first depth-first traversals#✓fully proved

Let \(G\) be a finite directed graph given by ordered adjacency lists and let \(r = (r_1, \dots, r_k)\) be a list of root vertices. A traversal \(T\) is a left-first DFS of \(G\) from \(r\) when some finite run of the following machine ends with an empty work list and with recorded preorder, postorder and (child, parent) list equal to those of \(T\).

The machine holds a work list of frames, each either "enter \(v\) with parent \(p\)" (where the parent \(p\) may be absent) or "exit \(v\)", a set of visited vertices, and the three recorded lists. It starts with the frames "enter \(r_1\) with no parent", ..., "enter \(r_k\) with no parent", no visited vertex and empty recorded lists. A step removes the first frame of the work list. For "exit \(v\)" it appends \(v\) to the postorder. For "enter \(v\) with parent \(p\)" it does nothing more if \(v\) is visited; otherwise it marks \(v\) visited, appends \(v\) to the preorder, appends \((v, p)\) to the (child, parent) list if \(p\) is present, and puts in front of the remaining work the frames "enter \(w\) with parent \(v\)" for the entries \(w\) of the adjacency list of \(v\), in order, followed by "exit \(v\)".

def IsLeftFirstDFS {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (traversal : Traversal V) : Prop :=
  ∃ final, Steps adj roots (initial roots) final ∧ final.work = [] ∧
    finish final = traversal

Uses 3 · Used by 3

Statement usesSequences of depth-first search machine steps · Depth-first traversal record · Directed adjacency graph

Used byExact transition count of depth-first search · Executable DFS meets the left-first specification · The left-first DFS specification determines the traversal

TheoremExecutable DFS meets the left-first specification#✓fully proved

For every directed graph \(G\) with ordered adjacency lists and every ordered list of roots, the traversal computed by left-first depth-first search of \(G\) from these roots conforms to left-first DFS for \(G\) and these roots.

theorem dfs_is_left_first {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) :
    IsLeftFirstDFS adj roots (dfs adj roots)

Uses 5 · Used by 1

Statement usesLeft-first depth-first traversals · Left-first depth-first search · Directed adjacency graph

Proof usesSequences of depth-first search machine steps · Depth-first traversal record

Used byExact transition count of depth-first search

TheoremThe left-first DFS specification determines the traversal#✓fully proved

Let \(G\) be a directed graph with ordered adjacency lists, fix an ordered list of roots, and let \(T\) be a traversal. If \(T\) conforms to left-first DFS for \(G\) and these roots, then \(T\) equals the traversal computed by left-first depth-first search of \(G\) from these roots.

theorem IsLeftFirstDFS.eq_dfs {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    {adj : DirectedAdjacency V} {roots : List V} {traversal : Traversal V}
    (h : IsLeftFirstDFS adj roots traversal) : traversal = dfs adj roots

Uses 5

Statement usesLeft-first depth-first traversals · Depth-first traversal record · Left-first depth-first search · Directed adjacency graph

Proof usesSequences of depth-first search machine steps

TheoremDepth-first search discovers only reachable vertices#✓fully proved

Let \(G\) be a finite directed graph given by ordered adjacency lists and let \(R\) be a list of roots. Every vertex in the preorder (discovery order) of the depth-first search of \(G\) from \(R\) is reachable in \(G\) from some root in \(R\) by a directed path (possibly of length zero).

theorem preorder_sound {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (v : V)
    (hv : v ∈ (dfs adj roots).preorder) :
    ∃ root ∈ roots, adj.Reachable root v

Uses 6 · Used by 1

Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph · Reachability in a directed graph

Proof usesSequences of depth-first search machine steps · Edge of a directed adjacency graph

Used byDepth-first search discovers exactly the reachable vertices

TheoremDepth-first search discovers every reachable vertex#✓fully proved

Let \(G\) be a finite directed graph given by ordered adjacency lists and let \(R\) be a list of roots. If a vertex \(v\) is reachable in \(G\) from some root in \(R\) by a directed path (possibly of length zero), then \(v\) occurs in the preorder (discovery order) of the depth-first search of \(G\) from \(R\).

theorem preorder_complete {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (v : V)
    (hv : ∃ root ∈ roots, adj.Reachable root v) :
    v ∈ (dfs adj roots).preorder

Uses 6 · Used by 2

Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph · Reachability in a directed graph

Proof usesSequences of depth-first search machine steps · Edge of a directed adjacency graph

Used byWhole-graph DFS discovers every vertex · Depth-first search discovers exactly the reachable vertices

TheoremDepth-first search discovers exactly the reachable vertices#✓fully proved

Let \(G\) be a finite directed graph and \(R\) a list of root vertices. A vertex \(v\) occurs in the discovery order (preorder) of the depth-first search of \(G\) from \(R\) if and only if there is a root \(r\) in \(R\) from which \(v\) is reachable in \(G\) by a directed path of length zero or more.

theorem mem_preorder_iff_reachable {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (v : V) :
    v ∈ (dfs adj roots).preorder ↔
      ∃ root ∈ roots, adj.Reachable root v

Uses 6 · Used by 2

Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph · Reachability in a directed graph

Proof usesDepth-first search discovers every reachable vertex · Depth-first search discovers only reachable vertices

Used byDepth-first search finishes exactly the reachable vertices · The mutual-reachability test is correct

TheoremDepth-first search discovers each vertex at most once#✓fully proved

For every finite directed graph \(G\) given by ordered adjacency lists and every list \(R\) of roots, the preorder (discovery order) of the depth-first search of \(G\) from \(R\) contains no vertex twice.

theorem preorder_nodup {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) : (dfs adj roots).preorder.Nodup

Uses 4 · Used by 4

Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph

Proof usesSequences of depth-first search machine steps

Used byExact transition count of whole-graph depth-first search · DFS forest roots are distinct · Parent chains in a DFS forest end at a forest root · The DFS parent relation is acyclic

TheoremDepth-first search finishes exactly the reachable vertices#✓fully proved

Let \(G\) be a finite directed graph and \(R\) a list of root vertices. A vertex \(v\) occurs in the finish order (postorder) of the depth-first search of \(G\) from \(R\) if and only if there is a root \(r\) in \(R\) from which \(v\) is reachable in \(G\) by a directed path of length zero or more.

theorem mem_postorder_iff_reachable {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (v : V) :
    v ∈ (dfs adj roots).postorder ↔
      ∃ root ∈ roots, adj.Reachable root v

Uses 6 · Used by 2

Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph · Reachability in a directed graph

Proof usesSequences of depth-first search machine steps · Depth-first search discovers exactly the reachable vertices

Used byDecreasing finish order lists exactly the vertices reachable from the roots · Whole-graph DFS finishes every vertex

TheoremDFS finishes each vertex at most once#✓fully proved

Let \(G\) be a finite directed graph and \(R\) a list of root vertices. The finish order (postorder) of the depth-first search of \(G\) from \(R\) contains no vertex twice.

theorem postorder_nodup {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) : (dfs adj roots).postorder.Nodup

Uses 4 · Used by 1

Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph

Proof usesSequences of depth-first search machine steps

Used byDecreasing finish order has no repeated vertices

DefinitionOccurring before in a list#✓fully proved

For elements \(x\) and \(y\) and a list \(xs\), \(x\) occurs before \(y\) in \(xs\) when there are lists \(a\), \(b\) and \(c\) such that \(xs\) is the concatenation of \(a\), the element \(x\), \(b\), the element \(y\) and \(c\); that is, some occurrence of \(x\) lies at a strictly earlier position than some occurrence of \(y\).

def Before {V : Type u} (x y : V) (xs : List V) : Prop :=
  ∃ a b c, xs = a ++ x :: b ++ y :: c

Used by 8

Used byA DFS child finishes before its parent · DFS forest roots are scheduled roots · 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

DefinitionParent relation of a list of pairs#✓fully proved

Given a list \(P\) of (child, parent) pairs, \(p\) is a parent of \(c\) in \(P\) when the pair \((c, p)\) occurs in \(P\).

def ParentRel {V : Type u} (parents : List (V × V)) (child parent : V) : Prop :=
  (child, parent) ∈ parents

Used by 6

Used byDFS forest roots are scheduled roots · In preorder, 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

DefinitionRoots of a DFS forest#✓fully proved

The forest roots of a traversal \(T\) are the vertices of the preorder of \(T\) that do not occur as the child in any (child, parent) pair recorded by \(T\), listed in the order in which they occur in the preorder.

def Traversal.forestRoots {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (traversal : Traversal V) : List V :=
  let parented : Std.HashSet V := Std.HashSet.ofList (traversal.parents.map Prod.fst)
  traversal.preorder.filter fun vertex => vertex ∉ parented

Uses 1 · Used by 5

Statement usesDepth-first traversal record

Used byA DFS forest root has no parent · DFS forest roots are scheduled roots · DFS forest roots are distinct · Every discovered vertex is a forest root or has a unique parent · Parent chains in a DFS forest end at a forest root

TheoremDFS forest roots are distinct#✓fully proved

For every finite directed graph \(G\) given by ordered adjacency lists and every list \(r\) of root vertices, the list of forest roots of the left-first depth-first search of \(G\) from \(r\) contains no vertex twice.

theorem forestRoots_nodup {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) :
    (dfs adj roots).forestRoots.Nodup

Uses 5

Statement usesRoots of a DFS forest · Left-first depth-first search · Directed adjacency graph

Proof usesDepth-first traversal record · Depth-first search discovers each vertex at most once

TheoremA DFS forest root has no parent#✓fully proved

Let \(G\) be a finite directed graph given by ordered adjacency lists, let \(r\) be a list of root vertices, and let \(v\) and \(p\) be vertices. If \(v\) is a forest root of the left-first depth-first search of \(G\) from \(r\), then \((v, p)\) is not among the (child, parent) pairs recorded by that search.

theorem forestRoot_has_no_parent {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (root parent : V)
    (hroot : root ∈ (dfs adj roots).forestRoots) :
    (root, parent) ∉ (dfs adj roots).parents

Uses 4 · Used by 1

Statement usesDepth-first traversal record · Roots of a DFS forest · Left-first depth-first search · Directed adjacency graph

Used byDFS forest roots are scheduled roots

TheoremDFS parent pairs are graph edges#✓fully proved

Let \(G\) be a finite directed graph and \(R\) a list of root vertices, and run depth-first search on \(G\) from \(R\). If the pair \((c, p)\) occurs in the list of (child, parent) pairs recorded by the search, then \(G\) has a directed edge from \(p\) to \(c\).

theorem parent_edge {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (child parent : V)
    (h : (child, parent) ∈ (dfs adj roots).parents) : adj.Edge parent child

Uses 7

Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph · Edge of a directed adjacency graph

Proof usesOccurring before in a list · Sequences of depth-first search machine steps · Parent relation of a list of pairs

TheoremNo vertex is recorded twice as a DFS child#✓fully proved

Let \(G\) be a finite directed graph and \(R\) a list of root vertices, and run depth-first search on \(G\) from \(R\). In the list of (child, parent) pairs recorded by the search, no vertex occurs as the child of more than one entry; that is, the list of children has no repeated entries.

theorem parent_children_nodup {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) :
    ((dfs adj roots).parents.map Prod.fst).Nodup

Uses 7 · Used by 1

Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph

Proof usesOccurring before in a list · Sequences of depth-first search machine steps · Parent relation of a list of pairs · Edge of a directed adjacency graph

Used byEvery discovered vertex is a forest root or has a unique parent

TheoremEvery discovered vertex is a forest root or has a unique parent#✓fully proved

Let \(G\) be a finite directed graph given by ordered adjacency lists, let \(r\) be a list of root vertices, and let \(v\) be a vertex in the preorder of the left-first depth-first search of \(G\) from \(r\). Then \(v\) is a forest root of that search, or there is exactly one vertex \(p\) such that \((v, p)\) is among the (child, parent) pairs recorded by the search.

theorem mem_forestRoots_or_existsUnique_parent {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (v : V)
    (hv : v ∈ (dfs adj roots).preorder) :
    v ∈ (dfs adj roots).forestRoots ∨
      ∃! parent, (v, parent) ∈ (dfs adj roots).parents

Uses 5 · Used by 1

Statement usesDepth-first traversal record · Roots of a DFS forest · Left-first depth-first search · Directed adjacency graph

Proof usesNo vertex is recorded twice as a DFS child

Used byParent chains in a DFS forest end at a forest root

TheoremIn preorder, a DFS parent precedes its child#✓fully proved

Let \(G\) be a finite directed graph and \(R\) a list of root vertices, and run depth-first search on \(G\) from \(R\). If the pair \((c, p)\) occurs in the list of (child, parent) pairs recorded by the search, then \(p\) occurs strictly before \(c\) in the discovery order (preorder) of the search.

theorem parent_before_child {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (child parent : V)
    (h : (child, parent) ∈ (dfs adj roots).parents) :
    Before parent child (dfs adj roots).preorder

Uses 7 · Used by 2

Statement usesOccurring before in a list · Depth-first traversal record · Left-first depth-first search · Directed adjacency graph

Proof usesSequences of depth-first search machine steps · Parent relation of a list of pairs · Edge of a directed adjacency graph

Used byParent chains in a DFS forest end at a forest root · The DFS parent relation is acyclic

TheoremA DFS child finishes before its parent#✓fully proved

Let \(G\) be a directed graph with ordered adjacency lists and fix an ordered list of roots. If \((c, p)\) is one of the (child, parent) pairs recorded by the left-first depth-first search of \(G\) from these roots, then \(c\) occurs before \(p\) in the postorder (finish order) of that search.

theorem child_before_parent_postorder {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (child parent : V)
    (h : (child, parent) ∈ (dfs adj roots).parents) :
    Before child parent (dfs adj roots).postorder

Uses 5 · Used by 1

Statement usesOccurring before in a list · Depth-first traversal record · Left-first depth-first search · Directed adjacency graph

Proof usesSequences of depth-first search machine steps

Used byIn decreasing finish order, a DFS parent precedes its child

DefinitionDecreasing finish order#✓fully proved

For a directed graph \(G\) with ordered adjacency lists and an ordered list of roots, the decreasing finish order is the reverse of the postorder of the left-first depth-first search of \(G\) from those roots: the vertices that search visits, listed from the latest finished to the earliest finished.

def decreasingFinish {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) : List V :=
  (dfs adj roots).postorder.reverse

Uses 3 · Used by 5

Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph

Used byWhole-graph decreasing finish order · Decreasing finish order has no repeated vertices · Whole-graph decreasing finish order contains every vertex · Decreasing finish order lists exactly the vertices reachable from the roots · In decreasing finish order, a DFS parent precedes its child

TheoremIn decreasing finish order, a DFS parent precedes its child#✓fully proved

Let \(G\) be a finite directed graph and \(R\) a list of root vertices, and run depth-first search on \(G\) from \(R\). If the pair \((c, p)\) occurs in the list of (child, parent) pairs recorded by the search, then \(p\) occurs strictly before \(c\) in the decreasing finish order, the reverse of the finish order.

theorem parent_before_child_decreasingFinish {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (child parent : V)
    (h : (child, parent) ∈ (dfs adj roots).parents) :
    Before parent child (decreasingFinish adj roots)

Uses 6

Statement usesOccurring before in a list · Depth-first traversal record · Decreasing finish order · Left-first depth-first search · Directed adjacency graph

Proof usesA DFS child finishes before its parent

TheoremDecreasing finish order lists exactly the vertices reachable from the roots#✓fully proved

Let \(G\) be a finite directed graph given by ordered adjacency lists, let \(r\) be a list of root vertices, and let \(v\) be a vertex. Then \(v\) occurs in the decreasing finish order of the left-first depth-first search of \(G\) from \(r\) if and only if \(v\) is reachable in \(G\) from some vertex of \(r\).

theorem mem_decreasingFinish_iff_reachable {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (v : V) :
    v ∈ decreasingFinish adj roots ↔
      ∃ root ∈ roots, adj.Reachable root v

Uses 6 · Used by 1

Statement usesDecreasing finish order · Directed adjacency graph · Reachability in a directed graph

Proof usesDepth-first traversal record · Left-first depth-first search · Depth-first search finishes exactly the reachable vertices

Used byWhole-graph decreasing finish order contains every vertex

TheoremDecreasing finish order has no repeated vertices#✓fully proved

For every directed graph \(G\) with ordered adjacency lists and every ordered list of roots, the decreasing finish order of the depth-first search of \(G\) from those roots contains no vertex twice.

theorem decreasingFinish_nodup {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) :
    (decreasingFinish adj roots).Nodup

Uses 5 · Used by 1

Statement usesDecreasing finish order · Directed adjacency graph

Proof usesDepth-first traversal record · Left-first depth-first search · DFS finishes each vertex at most once

Used byWhole-graph decreasing finish order has no repeated vertices

TheoremParent chains in a DFS forest end at a forest root#✓fully proved

Let \(G\) be a finite directed graph and \(R\) a list of root vertices, and run depth-first search on \(G\) from \(R\). Say that \(p\) is a recorded parent of \(c\) when the pair \((c, p)\) occurs in the list of (child, parent) pairs recorded by the search, and call a discovered vertex with no recorded parent a forest root. Then for every vertex \(v\) in the discovery order (preorder) there are \(k \ge 0\) and vertices \(v = v_0, v_1, \dots, v_k\) such that each \(v_{i+1}\) is a recorded parent of \(v_i\) and \(v_k\) is a forest root.

theorem parent_chain_reaches_root {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (v : V)
    (hv : v ∈ (dfs adj roots).preorder) :
    ∃ r ∈ (dfs adj roots).forestRoots,
      Relation.ReflTransGen (ParentRel (dfs adj roots).parents) v r

Uses 9

Statement usesParent relation of a list of pairs · Depth-first traversal record · Roots of a DFS forest · Left-first depth-first search · Directed adjacency graph

Proof usesOccurring before in a list · Every discovered vertex is a forest root or has a unique parent · In preorder, a DFS parent precedes its child · Depth-first search discovers each vertex at most once

TheoremThe DFS parent relation is acyclic#✓fully proved

Let \(G\) be a finite directed graph and \(R\) a list of root vertices, and run depth-first search on \(G\) from \(R\). Say that \(p\) is a recorded parent of \(c\) when the pair \((c, p)\) occurs in the list of (child, parent) pairs recorded by the search. Then there are no \(k \ge 1\) and vertices \(v_0, v_1, \dots, v_k\) with \(v_k = v_0\) such that each \(v_{i+1}\) is a recorded parent of \(v_i\).

theorem parent_relation_acyclic {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (v : V) :
    ¬ Relation.TransGen (ParentRel (dfs adj roots).parents) v v

Uses 7

Statement usesParent relation of a list of pairs · Depth-first traversal record · Left-first depth-first search · Directed adjacency graph

Proof usesOccurring before in a list · In preorder, a DFS parent precedes its child · Depth-first search discovers each vertex at most once

TheoremDFS forest roots are scheduled roots#✓fully proved

Let \(G\) be a finite directed graph given by ordered adjacency lists, let \(r\) be a list of root vertices, and let \(v\) be a vertex. If \(v\) is a forest root of the left-first depth-first search of \(G\) from \(r\), then \(v\) occurs in \(r\).

theorem forestRoot_mem_roots {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) (root : V)
    (hroot : root ∈ (dfs adj roots).forestRoots) : root ∈ roots

Uses 9

Statement usesRoots of a DFS forest · Left-first depth-first search · Directed adjacency graph

Proof usesOccurring before in a list · Sequences of depth-first search machine steps · Parent relation of a list of pairs · Depth-first traversal record · A DFS forest root has no parent · Edge of a directed adjacency graph

DefinitionDepth-first search of the whole graph#✓fully proved

For a directed graph \(G\) with ordered adjacency lists, the whole-graph traversal is the left-first depth-first search of \(G\) whose roots are all vertices of \(G\), taken in the graph's fixed vertex enumeration order.

def dfsAll {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) : Traversal V :=
  dfs adj adj.vertices

Uses 3 · Used by 3

Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph

Used byExact transition count of whole-graph depth-first search · Whole-graph DFS finishes every vertex · Whole-graph DFS discovers every vertex

TheoremWhole-graph DFS discovers every vertex#✓fully proved

For every finite directed graph \(G\) given by ordered adjacency lists and every vertex \(v\) of \(G\), \(v\) occurs in the preorder of the whole-graph depth-first search of \(G\), that is, the left-first depth-first search of \(G\) whose roots are all vertices of \(G\) in the graph's vertex order.

theorem mem_dfsAll_preorder {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (vertex : V) :
    vertex ∈ (dfsAll adj).preorder

Uses 6 · Used by 1

Statement usesDepth-first traversal record · Depth-first search of the whole graph · Directed adjacency graph

Proof usesDepth-first search discovers every reachable vertex · Edge of a directed adjacency graph · Reachability in a directed graph

Used byExact transition count of whole-graph depth-first search

TheoremWhole-graph DFS finishes every vertex#✓fully proved

For every finite directed graph \(G\) given by ordered adjacency lists and every vertex \(v\) of \(G\), \(v\) occurs in the postorder of the whole-graph depth-first search of \(G\), that is, the left-first depth-first search of \(G\) whose roots are all vertices of \(G\) in the graph's vertex order.

theorem mem_dfsAll_postorder {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (vertex : V) :
    vertex ∈ (dfsAll adj).postorder

Uses 7

Statement usesDepth-first traversal record · Depth-first search of the whole graph · Directed adjacency graph

Proof usesLeft-first depth-first search · Depth-first search finishes exactly the reachable vertices · Edge of a directed adjacency graph · Reachability in a directed graph

DefinitionWhole-graph decreasing finish order#✓fully proved

For a directed graph \(G\) with ordered adjacency lists, the whole-graph decreasing finish order is the decreasing finish order of the left-first depth-first search of \(G\) whose roots are all vertices of \(G\), taken in the graph's vertex enumeration order; its vertices are listed from the latest finished to the earliest finished.

def decreasingFinishAll {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) : List V :=
  decreasingFinish adj adj.vertices

Uses 2 · Used by 10

Statement usesDecreasing finish order · Directed adjacency graph

Used byWhole-graph decreasing finish order has no repeated vertices · Whole-graph decreasing finish order contains every vertex · Each 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 · Vertices share a computed component exactly when strongly connected

TheoremWhole-graph decreasing finish order contains every vertex#✓fully proved

For every finite directed graph \(G\) given by ordered adjacency lists and every vertex \(v\) of \(G\), \(v\) occurs in the whole-graph decreasing finish order of \(G\), that is, the decreasing finish order of the left-first depth-first search of \(G\) whose roots are all vertices of \(G\) in the graph's vertex order.

theorem mem_decreasingFinishAll {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (vertex : V) :
    vertex ∈ decreasingFinishAll adj

Uses 6 · Used by 2

Statement usesWhole-graph decreasing finish order · Directed adjacency graph

Proof usesDecreasing finish order · Decreasing finish order lists exactly the vertices reachable from the roots · Edge of a directed adjacency graph · Reachability in a directed graph

Used byThe computed components cover the vertex list · Vertices share a computed component exactly when strongly connected

TheoremWhole-graph decreasing finish order has no repeated vertices#✓fully proved

For every directed graph \(G\) with ordered adjacency lists, the whole-graph decreasing finish order of \(G\) contains no vertex twice.

theorem decreasingFinishAll_nodup {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) : (decreasingFinishAll adj).Nodup

Uses 3 · Used by 1

Statement usesWhole-graph decreasing finish order · Directed adjacency graph

Proof usesDecreasing finish order has no repeated vertices

Used byComputed components have no repeated vertices

TheoremExact transition count of depth-first search#✓fully proved

Let \(G\) be a finite directed graph with ordered adjacency lists \(N(v)\), whose entries may repeat, and let \(R\) be a list of roots, possibly with repetitions. Run the depth-first search machine from \(R\) (each transition drops a pending vertex that is already visited, discovers a new vertex, or finishes a vertex). Let \(v_1, \dots, v_k\) be the preorder of the depth-first search of \(G\) from \(R\). Then there is a terminal machine state, with no work left, whose recorded output is the depth-first traversal of \(G\) from \(R\) and which is reached from the initial state in exactly \(|R| + k + \sum_{i=1}^{k} |N(v_i)|\) transitions, where \(|R|\) is the length of \(R\) and \(|N(v)|\) is the length of the adjacency list of \(v\).

public theorem dfs_exact_steps
    {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) (roots : List V) :
    ∃ final : Internal.Machine V, final.work = [] ∧
      Internal.finish final = dfs adj roots ∧
      Relation.RelatesInSteps (Internal.Step adj roots) (Internal.initial roots) final
        (roots.length + (dfs adj roots).preorder.length +
          ((dfs adj roots).preorder.map fun v => (adj.adjacency v).length).sum)

Uses 6 · Used by 1

Statement usesDepth-first traversal record · Left-first depth-first search · Directed adjacency graph

Proof usesSequences of depth-first search machine steps · Left-first depth-first traversals · Executable DFS meets the left-first specification

Used byExact transition count of whole-graph depth-first search

TheoremExact transition count of whole-graph depth-first search#✓fully proved

Let \(G\) be a finite directed graph whose vertices are listed without repetition as \(v_1, \dots, v_n\), with ordered adjacency lists \(N(v)\) whose entries may repeat. Run the depth-first search machine with roots \(v_1, \dots, v_n\) in this order (each transition drops a pending vertex that is already visited, discovers a new vertex, or finishes a vertex). Then there is a terminal machine state, with no work left, whose recorded output is the whole-graph depth-first traversal of \(G\) and which is reached from the initial state in exactly \(2n + \sum_{i=1}^{n} |N(v_i)|\) transitions, where \(|N(v)|\) is the length of the adjacency list of \(v\), counting repeated entries and self-loops.

public theorem dfsAll_exact_steps
    {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (adj : DirectedAdjacency V) :
    ∃ final : Internal.Machine V, final.work = [] ∧
      Internal.finish final = dfsAll adj ∧
      Relation.RelatesInSteps (Internal.Step adj adj.vertices)
        (Internal.initial adj.vertices) final
        (2 * adj.vertices.length + (adj.vertices.map fun v => (adj.adjacency v).length).sum)

Uses 7

Statement usesDepth-first traversal record · Depth-first search of the whole graph · Directed adjacency graph

Proof usesLeft-first depth-first search · Exact transition count of depth-first search · Whole-graph DFS discovers every vertex · Depth-first search discovers each vertex at most once

37 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.