Hierholzer's algorithm for Euler circuits

DefinitionEdge list of an adjacency function#✓fully proved

Given a directed adjacency graph \(G\) and a function \(R\) assigning to each vertex \(u\) a list \(R(u)\) of vertices, the edge list of \(R\) is the list of pairs \((u, w)\), one for each entry \(w\) of \(R(u)\), taken over the vertices \(u\) in the order of the vertex enumeration of \(G\) and, for each \(u\), in the order of \(R(u)\). A repeated entry gives a repeated pair.

def edgeListOf (graph : DirectedAdjacency V) (R : V → List V) : List (V × V) :=
  graph.vertices.flatMap fun u => (R u).map (u, ·)

Uses 1 · Used by 5

Statement usesDirected adjacency graph

Used byEdge list of a directed graph · 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 · Contract of Hierholzer's recursion

DefinitionEdge list of a directed graph#✓fully proved

The edge list of a directed adjacency graph \(G\) is the list of pairs \((u, w)\), one for each entry \(w\) of the adjacency list of \(u\), taken over the vertices \(u\) in the order of the vertex enumeration of \(G\) and, for each \(u\), in adjacency-list order. A repeated adjacency entry gives a repeated pair, so \(G\) is read as a multigraph with one edge occurrence per entry.

def edgeList (graph : DirectedAdjacency V) : List (V × V) := edgeListOf graph graph.adjacency

Uses 2 · Used by 10

Statement usesDirected adjacency graph · Edge list of an adjacency function

Used byHierholzer'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 path in a directed multigraph · Semi-balanced directed multigraph · A directed multigraph with an Euler path is semi-balanced

DefinitionSteps of a walk#✓fully proved

For a finite sequence of vertices \(W = (w_0, w_1, \dots, w_n)\), the steps of \(W\) are the list of consecutive pairs \(((w_0, w_1), (w_1, w_2), \dots, (w_{n-1}, w_n))\), in order. A sequence with at most one vertex has no steps.

def walkEdges (W : List V) : List (V × V) := W.zip W.tail

Used by 14

Used byDegrees of an undirected Euler path · Degrees along a walk · 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 · Euler path in a directed multigraph · A directed multigraph with an Euler path is semi-balanced · Euler path in an undirected multigraph · Undirected Hierholzer's algorithm finds Euler paths · Cost of the undirected Hierholzer algorithm · Undirected Hierholzer's algorithm returns a trail · Invariant of the undirected Hierholzer recursion · Contract of Hierholzer's recursion · Steps of a concatenated walk

DefinitionBalanced directed multigraph#✓fully proved

A finite directed multigraph, read from its adjacency lists with each entry \(w\) in the list of \(u\) counted as one occurrence of the edge \(u \to w\), is balanced when every vertex is the source of as many edge occurrences as it is the target of.

def IsBalanced (graph : DirectedAdjacency V) : Prop :=
  ∀ x ∈ graph.vertices,
    ((edgeList graph).map Prod.fst).count x = ((edgeList graph).map Prod.snd).count x

Uses 2 · Used by 3

Statement usesDirected adjacency graph · Edge list of a directed graph

Used byEuler circuit criterion for directed multigraphs · Hierholzer's algorithm finds Euler circuits in directed multigraphs · A directed multigraph with an Euler circuit is balanced

DefinitionSemi-balanced directed multigraph#✓fully proved

A finite directed multigraph is semi-balanced for vertices \(s\) and \(t\) when, for every vertex \(x\), the number of edge occurrences leaving \(x\) plus \([x = t]\) equals the number entering \(x\) plus \([x = s]\), where \([P]\) is \(1\) if \(P\) holds and \(0\) otherwise. So for \(s \ne t\), one more edge occurrence leaves \(s\) than enters it, one more enters \(t\) than leaves it, and every other vertex is balanced; for \(s = t\) every vertex is balanced.

def IsSemiBalanced (graph : DirectedAdjacency V) (s t : V) : Prop :=
  ∀ x ∈ graph.vertices,
    ((edgeList graph).map Prod.fst).count x + (if x = t then 1 else 0) =
      ((edgeList graph).map Prod.snd).count x + (if x = s then 1 else 0)

Uses 2 · Used by 6

Statement usesDirected adjacency graph · Edge list of a directed graph

Used byEuler 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 · Hierholzer's algorithm returns a trail in a directed multigraph · A directed multigraph with an Euler path is semi-balanced

DefinitionEuler path in a directed multigraph#✓fully proved

In a finite directed multigraph, a list of vertices \(W = (w_0, \dots, w_k)\) is an Euler path from \(s\) to \(t\) when \(w_0 = s\), \(w_k = t\), and its list of steps \((w_0, w_1), \dots, (w_{k-1}, w_k)\) is a permutation of the list of edge occurrences of the graph, so that each edge occurrence, counted with multiplicity, is traversed exactly once.

def IsEulerPath (graph : DirectedAdjacency V) (s t : V) (W : List V) : Prop :=
  W.head? = some s ∧ W.getLast? = some t ∧ (walkEdges W).Perm (edgeList graph)

Uses 3 · Used by 4

Statement usesDirected adjacency graph · Edge list of a directed graph · Steps of a walk

Used byEuler path criterion for directed multigraphs · Hierholzer's algorithm finds Euler paths in directed multigraphs · Euler circuit in a directed multigraph · A directed multigraph with an Euler path is semi-balanced

DefinitionEuler circuit in a directed multigraph#✓fully proved

In a finite directed multigraph, a list of vertices \(W\) is an Euler circuit from a vertex \(s\) when it is an Euler path from \(s\) to \(s\): it starts and ends at \(s\), and its list of consecutive pairs is a permutation of the list of edge occurrences of the graph.

def IsEulerCircuit (graph : DirectedAdjacency V) (s : V) (W : List V) : Prop :=
  IsEulerPath graph s s W

Uses 2 · Used by 3

Statement usesDirected adjacency graph · Euler path in a directed multigraph

Used byEuler circuit criterion for directed multigraphs · Hierholzer's algorithm finds Euler circuits in directed multigraphs · A directed multigraph with an Euler circuit is balanced

DefinitionHierholzer's recursion#✓fully proved

Given a fuel \(n\), a vertex \(v\), an assignment \(R\) of a list of remaining out-neighbours to each vertex, and a list \(\mathit{acc}\) of vertices, the recursion returns a list of vertices and a new assignment, with a cost. With fuel \(0\) it returns \((\mathit{acc}, R)\) at cost \(0\). With fuel \(n + 1\): if \(R(v)\) is empty, it returns \(v\) followed by \(\mathit{acc}\) together with \(R\), at cost \(0\); otherwise \(R(v)\) is \(w\) followed by a list \(\mathit{rest}\), and it replaces \(R(v)\) by \(\mathit{rest}\), runs the recursion with fuel \(n\) from \(w\) on the new assignment with accumulator \(\mathit{acc}\), obtaining \((L_1, R_1)\), and returns the result of the recursion with fuel \(n\) from \(v\) on \(R_1\) with accumulator \(L_1\), at cost \(1\) plus the costs of the two calls.

This follows unused edges depth first and splices sub-tours in; too little fuel can stop it early. Hierholzer's algorithm runs it with fuel one more than the number of edge occurrences.

def visit : ℕ → V → (V → List V) → List V → TimeM ℕ (List V × (V → List V))
  | 0, _, R, acc => pure (acc, R)
  | fuel + 1, v, R, acc =>
      match R v with
      | [] => pure (v :: acc, R)
      | w :: rest => do
          ✓
          let r ← visit fuel w (Function.update R v rest) acc
          visit fuel v r.2 r.1

Used by 5

Used byHierholzer's algorithm · 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 · Contract of Hierholzer's recursion

DefinitionHierholzer's algorithm#✓fully proved

Let \(G\) be a directed adjacency graph, read as a multigraph with one edge occurrence per adjacency entry, let \(s\) be a vertex, and let \(m\) be the number of edge occurrences of \(G\), that is, the length of its edge list. Hierholzer's algorithm on \(G\) from \(s\) runs Hierholzer's recursion from \(s\) with fuel \(m + 1\), with the adjacency list of each vertex as its list of remaining out-neighbours and the empty list as accumulator, and returns the list of vertices produced by the recursion, at the cost of the recursion.

def hierholzer (graph : DirectedAdjacency V) (s : V) : TimeM ℕ (List V) := do
  let r ← visit ((edgeList graph).length + 1) s graph.adjacency []
  pure r.1

Uses 3 · Used by 6

Statement usesDirected adjacency graph · Edge list of a directed graph · Hierholzer's recursion

Used byEuler 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 · Hierholzer's algorithm returns a trail in a directed multigraph

TheoremSteps of a concatenated walk#✓fully proved

Let \(A\) and \(B\) be nonempty vertex sequences, where \(A\) ends at the vertex \(a\) and \(B\) starts at the vertex \(b\). Then the steps of the concatenation \(A B\) are the steps of \(A\), followed by the step \((a, b)\), followed by the steps of \(B\).

theorem walkEdges_append {A B : List V} {a b : V} (ha : A.getLast? = some a)
    (hb : B.head? = some b) : walkEdges (A ++ B) = walkEdges A ++ (a, b) :: walkEdges B

Uses 1 · Used by 2

Statement usesSteps of a walk

Used byInvariant of the undirected Hierholzer recursion · Contract of Hierholzer's recursion

TheoremMoving a block of a list in front of an element is a permutation#✓fully proved

For an element \(e\) and lists \(A\), \(B\), \(C\) of the same type, the list \(e \cdot A \cdot B \cdot C\) is a permutation of \(B \cdot e \cdot A \cdot C\), where \(\cdot\) denotes concatenation and \(e\) stands for the one-element list.

This is how a sub-tour \(B\) is spliced in front of the edge \(e\).

theorem perm_splice {α : Type*} (e : α) (A B C : List α) :
    (e :: (A ++ (B ++ C))).Perm (B ++ e :: A ++ C)

Used by 2

Used byInvariant of the undirected Hierholzer recursion · Contract of Hierholzer's recursion

DefinitionSemi-balanced edge list#✓fully proved

A list \(E\) of ordered pairs of vertices is semi-balanced for vertices \(v\) and \(t\) when, for every vertex \(x\), the number of pairs in \(E\) with first component \(x\) plus \([x = t]\) equals the number with second component \(x\) plus \([x = v]\), where \([P]\) is \(1\) if \(P\) holds and \(0\) otherwise. So for \(v \ne t\), \(v\) has one more outgoing than incoming occurrence, \(t\) one more incoming than outgoing, and every other vertex is balanced; for \(v = t\) every vertex is balanced.

def SemiBalancedEdges (E : List (V × V)) (v t : V) : Prop :=
  ∀ x, (E.map Prod.fst).count x + (if x = t then 1 else 0) =
    (E.map Prod.snd).count x + (if x = v then 1 else 0)

Used by 1

Used byContract of Hierholzer's recursion

DefinitionBalanced edge list#✓fully proved

A list \(E\) of ordered pairs of vertices, read as directed edge occurrences, is balanced when every vertex \(x\) occurs as the first component of exactly as many entries of \(E\) as it occurs as the second component, counted with multiplicity.

def BalancedEdges (E : List (V × V)) : Prop :=
  ∀ x, (E.map Prod.fst).count x = (E.map Prod.snd).count x

Used by 4

Used byHierholzer's algorithm finds Euler paths in directed multigraphs · Running time of Hierholzer's algorithm · Hierholzer's algorithm returns a trail in a directed multigraph · Contract of Hierholzer's recursion

TheoremContract of Hierholzer's recursion#✓fully proved

Let \(G\) be a finite directed multigraph, let \(R\) assign to each vertex \(u\) a list \(R(u)\) of remaining out-neighbours, and let \(E(R)\) be the list of remaining edge occurrences, one pair \((u, w)\) for each entry \(w\) of \(R(u)\). Let \(v\) and \(t\) be vertices, \(\mathit{acc}\) a list of vertices and \(n\) a natural number with \(|E(R)| < n\), and suppose \(E(R)\) is semi-balanced for \(v\) and \(t\): for every vertex \(x\), the number of pairs in \(E(R)\) with first component \(x\) plus \([x = t]\) equals the number with second component \(x\) plus \([x = v]\), where \([P]\) is \(1\) if \(P\) holds and \(0\) otherwise. Let \((L, R')\) be the result and \(c\) the cost of Hierholzer's recursion with fuel \(n\) from \(v\) on \(R\) with accumulator \(\mathit{acc}\). Then there is a list of vertices \(W\) such that \(L\) is \(W\) followed by \(\mathit{acc}\); \(W\) starts at \(v\) and ends at \(t\); \(E(R)\) is a permutation of the steps (consecutive pairs) of \(W\) followed by \(E(R')\); every vertex is the first component of as many pairs of \(E(R')\) as it is the second component of; \(R'(x)\) is empty for every vertex \(x\) of \(W\); \(R'(x)\) is a suffix of \(R(x)\) for every vertex \(x\); and \(c + |E(R')| = |E(R)|\).

theorem visit_spec (graph : DirectedAdjacency V) : ∀ (fuel : ℕ) (v t : V)
    (R : V → List V) (acc : List V), (edgeListOf graph R).length < fuel →
    SemiBalancedEdges (edgeListOf graph R) v t →
    ∃ W, (visit fuel v R acc).ret.1 = W ++ acc ∧ W.head? = some v ∧ W.getLast? = some t ∧
      (edgeListOf graph R).Perm (walkEdges W ++ edgeListOf graph (visit fuel v R acc).ret.2) ∧
      BalancedEdges (edgeListOf graph (visit fuel v R acc).ret.2) ∧
      (∀ x ∈ W, (visit fuel v R acc).ret.2 x = []) ∧
      (∀ x, (visit fuel v R acc).ret.2 x <:+ R x) ∧
      (visit fuel v R acc).time + (edgeListOf graph (visit fuel v R acc).ret.2).length =
        (edgeListOf graph R).length

Uses 8 · Used by 3

Statement usesDirected adjacency graph · Balanced edge list · Semi-balanced edge list · Edge list of an adjacency function · Hierholzer's recursion · Steps of a walk

Proof usesMoving a block of a list in front of an element is a permutation · Steps of a concatenated walk

Used byHierholzer's algorithm finds Euler paths in directed multigraphs · Running time of Hierholzer's algorithm · Hierholzer's algorithm returns a trail in a directed multigraph

TheoremHierholzer's algorithm returns a trail in a directed multigraph#✓fully proved

Let \(G\) be a directed adjacency graph, read as a multigraph with one edge per adjacency entry, and let \(s\) and \(t\) be vertices such that \(G\) is semi-balanced for \(s\) and \(t\). Then the vertex sequence \(W\) returned by Hierholzer's algorithm on \(G\) from \(s\) starts at \(s\) and ends at \(t\), and the edge list of \(G\) is a permutation of the list of consecutive pairs of \(W\) followed by some further list of pairs. So \(W\) is a walk from \(s\) to \(t\) that uses each edge occurrence at most once; reachability is not assumed.

theorem hierholzer_trail (graph : DirectedAdjacency V) (s t : V)
    (hbal : IsSemiBalanced graph s t) :
    (hierholzer graph s).ret.head? = some s ∧ (hierholzer graph s).ret.getLast? = some t ∧
      ∃ rest, (edgeList graph).Perm (walkEdges (hierholzer graph s).ret ++ rest)

Uses 9

Statement usesDirected adjacency graph · Semi-balanced directed multigraph · Edge list of a directed graph · Hierholzer's algorithm · Steps of a walk

Proof usesBalanced edge list · Edge list of an adjacency function · Hierholzer's recursion · Contract of Hierholzer's recursion

TheoremHierholzer's algorithm finds Euler paths in directed multigraphs#✓fully proved

Let \(G\) be a directed adjacency graph, read as a multigraph with one edge per adjacency entry, and let \(s\) and \(t\) be vertices such that \(G\) is semi-balanced for \(s\) and \(t\) (at \(s\) one more edge occurrence leaves than enters, at \(t\) one more enters than leaves, and at every other vertex as many leave as enter; at every vertex when \(s = t\)) and the source of every edge of \(G\) is reachable from \(s\). Then the vertex sequence returned by Hierholzer's algorithm on \(G\) from \(s\) is an Euler path of \(G\) from \(s\) to \(t\).

theorem hierholzer_isEulerPath (graph : DirectedAdjacency V) (s t : V)
    (hbal : IsSemiBalanced graph s t) (hreach : ∀ u w, graph.Edge u w → graph.Reachable s u) :
    IsEulerPath graph s t (hierholzer graph s).ret

Uses 12 · Used by 2

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Reachability in a directed graph · Euler path in a directed multigraph · Semi-balanced directed multigraph · Hierholzer's algorithm

Proof usesBalanced edge list · Edge list of a directed graph · Edge list of an adjacency function · Hierholzer's recursion · Contract of Hierholzer's recursion · Steps of a walk

Used byEuler path criterion for directed multigraphs · Hierholzer's algorithm finds Euler circuits in directed multigraphs

TheoremHierholzer's algorithm finds Euler circuits in directed multigraphs#✓fully proved

Let \(G\) be a directed adjacency graph, read as a multigraph with one edge per adjacency entry, that is balanced (every vertex is the source of exactly as many edge occurrences as it is the target of), and let \(s\) be a vertex such that the source of every edge of \(G\) is reachable from \(s\). Then the vertex sequence returned by Hierholzer's algorithm on \(G\) from \(s\) is an Euler circuit of \(G\) from \(s\).

theorem hierholzer_isEulerCircuit (graph : DirectedAdjacency V) (s : V)
    (hbal : IsBalanced graph) (hreach : ∀ u w, graph.Edge u w → graph.Reachable s u) :
    IsEulerCircuit graph s (hierholzer graph s).ret

Sources

• CLRS, third edition, Problem 22-3, sufficiency with the algorithm; strong connectivity is weakened to reachability from \(s\) of the source of every edge.

Uses 9 · Used by 1

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Reachability in a directed graph · Balanced directed multigraph · Euler circuit in a directed multigraph · Hierholzer's algorithm

Proof usesSemi-balanced directed multigraph · Edge list of a directed graph · Hierholzer's algorithm finds Euler paths in directed multigraphs

Used byEuler circuit criterion for directed multigraphs

TheoremRunning time of Hierholzer's algorithm#✓fully proved

Let \(G\) be a directed adjacency graph, read as a multigraph with one edge per adjacency entry, and let \(s\) and \(t\) be vertices such that \(G\) is semi-balanced for \(s\) and \(t\) and the source of every edge of \(G\) is reachable from \(s\). Then Hierholzer's algorithm on \(G\) from \(s\) costs exactly \(|E|\) units, where \(|E|\) is the number of edge occurrences of \(G\), that is, the length of its edge list.

The cost model charges one unit per edge traversal (removing the head of an adjacency list); reading an adjacency list and emitting a vertex are free.

theorem hierholzer_time (graph : DirectedAdjacency V) (s t : V)
    (hbal : IsSemiBalanced graph s t) (hreach : ∀ u w, graph.Edge u w → graph.Reachable s u) :
    (hierholzer graph s).time = (edgeList graph).length

Uses 11

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Reachability in a directed graph · Semi-balanced directed multigraph · Edge list of a directed graph · Hierholzer's algorithm

Proof usesBalanced edge list · Edge list of an adjacency function · Hierholzer's recursion · Contract of Hierholzer's recursion · Steps of a walk

TheoremA directed multigraph with an Euler path is semi-balanced#✓fully proved

If a finite directed multigraph has an Euler path from \(s\) to \(t\), then it is semi-balanced for \(s\) and \(t\): counting edge occurrences, \(s\) has one more outgoing than incoming edge, \(t\) one more incoming than outgoing, and every other vertex is balanced (every vertex, when \(s = t\)).

theorem isSemiBalanced_of_isEulerPath {graph : DirectedAdjacency V} {s t : V} {W : List V}
    (h : IsEulerPath graph s t W) : IsSemiBalanced graph s t

Uses 5 · Used by 2

Statement usesDirected adjacency graph · Euler path in a directed multigraph · Semi-balanced directed multigraph

Proof usesEdge list of a directed graph · Steps of a walk

Used byEuler path criterion for directed multigraphs · A directed multigraph with an Euler circuit is balanced

TheoremA directed multigraph with an Euler circuit is balanced#✓fully proved

If a finite directed multigraph has an Euler circuit from some vertex \(s\), then it is balanced: every vertex is the source of as many edge occurrences as it is the target of.

This is the necessity direction of CLRS Problem 22-3.

theorem isBalanced_of_isEulerCircuit {graph : DirectedAdjacency V} {s : V} {W : List V}
    (h : IsEulerCircuit graph s W) : IsBalanced graph

Uses 5 · Used by 1

Statement usesDirected adjacency graph · Balanced directed multigraph · Euler circuit in a directed multigraph

Proof usesEdge list of a directed graph · A directed multigraph with an Euler path is semi-balanced

Used byEuler circuit criterion for directed multigraphs

TheoremEuler path criterion for directed multigraphs#✓fully proved

Let \(G\) be a directed adjacency graph, read as a multigraph with one edge per adjacency entry, and let \(s\) and \(t\) be vertices such that the source of every edge of \(G\) is reachable from \(s\). Then \(G\) has an Euler path from \(s\) to \(t\) if and only if \(G\) is semi-balanced for \(s\) and \(t\): at \(s\) one more edge occurrence leaves than enters, at \(t\) one more enters than leaves, and every other vertex is the source of exactly as many edge occurrences as it is the target of (every vertex, when \(s = t\)).

theorem exists_isEulerPath_iff (graph : DirectedAdjacency V) (s t : V)
    (hreach : ∀ u w, graph.Edge u w → graph.Reachable s u) :
    (∃ W, IsEulerPath graph s t W) ↔ IsSemiBalanced graph s t

Uses 8

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Reachability in a directed graph · Euler path in a directed multigraph · Semi-balanced directed multigraph

Proof usesHierholzer's algorithm · Hierholzer's algorithm finds Euler paths in directed multigraphs · A directed multigraph with an Euler path is semi-balanced

TheoremEuler circuit criterion for directed multigraphs#✓fully proved

Let \(G\) be a directed adjacency graph, read as a multigraph with one edge per adjacency entry, and let \(s\) be a vertex such that the source of every edge of \(G\) is reachable from \(s\). Then \(G\) has an Euler circuit from \(s\) if and only if \(G\) is balanced, that is, every vertex is the source of exactly as many edge occurrences as it is the target of.

theorem exists_isEulerCircuit_iff (graph : DirectedAdjacency V) (s : V)
    (hreach : ∀ u w, graph.Edge u w → graph.Reachable s u) :
    (∃ W, IsEulerCircuit graph s W) ↔ IsBalanced graph

Sources

• CLRS, third edition, Problem 22-3; strong connectivity is weakened to reachability from \(s\) of the source of every edge.

Uses 8

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Reachability in a directed graph · Balanced directed multigraph · Euler circuit in a directed multigraph

Proof usesHierholzer's algorithm · Hierholzer's algorithm finds Euler circuits in directed multigraphs · A directed multigraph with an Euler circuit is balanced

DefinitionUnordered edge of an ordered pair#✓fully proved

The ordered pair \((a, b)\) of vertices, viewed as the unordered pair \(\{a, b\}\), so that \((a, b)\) and \((b, a)\) give the same unordered edge.

def usym (e : V × V) : Sym2 V := s(e.1, e.2)

Used by 8

Used byDegrees of an undirected Euler path · Euler path in an undirected multigraph · Degrees depend only on the unordered edges · Undirected Hierholzer's algorithm finds Euler paths · Cost of the undirected Hierholzer algorithm · Undirected Hierholzer's algorithm returns a trail · An edge at a vertex joins it to its other endpoint · Invariant of the undirected Hierholzer recursion

DefinitionDegree in an undirected edge list#✓fully proved

For a finite list \(R\) of edges of an undirected multigraph, each given as a pair \((a, b)\), the degree of a vertex \(x\) is the number of edges in \(R\) whose first component is \(x\) plus the number whose second component is \(x\); parallel edges count separately and a loop \((x, x)\) counts twice.

def udeg (R : List (V × V)) (x : V) : ℕ := (R.map Prod.fst).count x + (R.map Prod.snd).count x

Used by 10

Used byDegree parity condition for two endpoints · Degrees of an undirected Euler path · Degrees along a walk · Degrees depend only on the unordered edges · Degree after removing an edge · Undirected Hierholzer's algorithm finds Euler circuits · Undirected Hierholzer's algorithm finds Euler paths · Cost of the undirected Hierholzer algorithm · Undirected Hierholzer's algorithm returns a trail · Invariant of the undirected Hierholzer recursion

DefinitionDegree parity condition for two endpoints#✓fully proved

For a finite list \(R\) of edges of an undirected multigraph and vertices \(v\), \(t\), the condition holds when for every vertex \(x\) the number \(\deg_R(x) + [x = v] + [x = t]\) is even, where \(\deg_R\) is the degree in \(R\) (a loop counts twice) and \([P]\) is \(1\) if \(P\) holds and \(0\) otherwise. Thus if \(v \ne t\), exactly \(v\) and \(t\) have odd degree, and if \(v = t\), every degree is even.

def EvenExcept (R : List (V × V)) (v t : V) : Prop :=
  ∀ x, (udeg R x + (if x = v then 1 else 0) + (if x = t then 1 else 0)) % 2 = 0

Uses 1 · Used by 7

Statement usesDegree in an undirected edge list

Used byDegrees of an undirected Euler path · Degrees along a walk · Euler's theorem for undirected multigraphs · Undirected Hierholzer's algorithm finds Euler paths · Cost of the undirected Hierholzer algorithm · Undirected Hierholzer's algorithm returns a trail · Invariant of the undirected Hierholzer recursion

DefinitionReachability in an undirected multigraph#✓fully proved

For a list \(E\) of edges (ordered pairs of vertices), a vertex \(x\) is reachable from a vertex \(s\) when there are vertices \(s = v_0, v_1, \dots, v_n = x\) with \(n \ge 0\) such that for each \(i < n\), \((v_i, v_{i+1})\) or \((v_{i+1}, v_i)\) belongs to \(E\).

def UReach (E : List (V × V)) (s x : V) : Prop :=
  Relation.ReflTransGen (fun a b => (a, b) ∈ E ∨ (b, a) ∈ E) s x

Used by 4

Used byEuler's theorem for undirected multigraphs · Undirected Hierholzer's algorithm finds Euler circuits · Undirected Hierholzer's algorithm finds Euler paths · Cost of the undirected Hierholzer algorithm

DefinitionEuler path in an undirected multigraph#✓fully proved

For a finite list \(E\) of edges of an undirected multigraph and vertices \(s\), \(t\), a sequence of vertices \(W = (w_0, \dots, w_n)\) is an Euler path of \(E\) from \(s\) to \(t\) when \(w_0 = s\), \(w_n = t\), and the multiset of unordered pairs \(\{w_{i-1}, w_i\}\) for \(1 \le i \le n\) equals the multiset of the edges of \(E\) taken as unordered pairs. Thus every edge is traversed exactly once, in either direction.

def IsUEulerPath (E : List (V × V)) (s t : V) (W : List V) : Prop :=
  W.head? = some s ∧ W.getLast? = some t ∧ ((walkEdges W).map usym).Perm (E.map usym)

Uses 2 · Used by 4

Statement usesUnordered edge of an ordered pair · Steps of a walk

Used byDegrees of an undirected Euler path · Euler's theorem for undirected multigraphs · Undirected Hierholzer's algorithm finds Euler circuits · Undirected Hierholzer's algorithm finds Euler paths

DefinitionOther endpoint of an edge#✓fully proved

For an edge \(e = (a, b)\) and a vertex \(v\), the other endpoint of \(e\) at \(v\) is \(b\) if \(a = v\), and \(a\) otherwise; in particular a loop \((v, v)\) gives \(v\).

def otherEnd (e : V × V) (v : V) : V := if e.1 = v then e.2 else e.1

Used by 3

Used byAn edge at a vertex joins it to its other endpoint · Undirected Hierholzer recursion · Invariant of the undirected Hierholzer recursion

DefinitionUndirected Hierholzer recursion#✓fully proved

The recursion takes a fuel \(f \in \mathbb{N}\), a vertex \(v\), a list \(R\) of remaining edges and an accumulator list \(A\) of vertices, and returns a list of vertices and a list of remaining edges. With fuel \(0\) it returns \(A\) and \(R\) unchanged. With fuel \(f + 1\): if no edge of \(R\) has \(v\) as an endpoint, it returns \(v\) prepended to \(A\), together with \(R\); otherwise, with \(e\) the first such edge, it removes \(e\) from \(R\) at a cost of one unit, recurses with fuel \(f\) from the other endpoint of \(e\) at \(v\) on the shortened list with accumulator \(A\), obtaining a vertex list \(A'\) and remaining edges \(R'\), and then recurses with fuel \(f\) from \(v\) on \(R'\) with accumulator \(A'\).

def uvisit : ℕ → V → List (V × V) → List V → TimeM ℕ (List V × List (V × V))
  | 0, _, R, acc => pure (acc, R)
  | fuel + 1, v, R, acc =>
      match R.find? (fun e => e.1 = v ∨ e.2 = v) with
      | none => pure (v :: acc, R)
      | some e => do
          ✓
          let r ← uvisit fuel (otherEnd e v) (R.erase e) acc
          uvisit fuel v r.2 r.1

Uses 1 · Used by 5

Statement usesOther endpoint of an edge

Used byUndirected Hierholzer's algorithm · Undirected Hierholzer's algorithm finds Euler paths · Cost of the undirected Hierholzer algorithm · Undirected Hierholzer's algorithm returns a trail · Invariant of the undirected Hierholzer recursion

DefinitionUndirected Hierholzer's algorithm#✓fully proved

Given a list \(E\) of undirected edges (ordered pairs of vertices) and a start vertex \(s\), run the undirected Hierholzer recursion from \(s\) on \(E\) with an empty accumulator and fuel \(|E| + 1\), and return the list of emitted vertices; its cost is the cost of that recursion.

def uhierholzer (E : List (V × V)) (s : V) : TimeM ℕ (List V) := do
  let r ← uvisit (E.length + 1) s E []
  pure r.1

Uses 1 · Used by 5

Statement usesUndirected Hierholzer recursion

Used byEuler's theorem for undirected multigraphs · Undirected Hierholzer's algorithm finds Euler circuits · Undirected Hierholzer's algorithm finds Euler paths · Cost of the undirected Hierholzer algorithm · Undirected Hierholzer's algorithm returns a trail

TheoremDegree after removing an edge#✓fully proved

Let \(R\) be a finite list of edges of an undirected multigraph, each an ordered pair of vertices, let \(e = (a, b)\) be an edge in \(R\), and let \(x\) be a vertex. Then the degree of \(x\) in \(R\) equals the degree of \(x\) in the list obtained from \(R\) by removing the first occurrence of \(e\), plus \([x = a] + [x = b]\), where \([P]\) is \(1\) if \(P\) holds and \(0\) otherwise.

theorem udeg_erase {R : List (V × V)} {e : V × V} (he : e ∈ R) (x : V) :
    udeg R x = udeg (R.erase e) x + (if x = e.1 then 1 else 0) + (if x = e.2 then 1 else 0)

Uses 1 · Used by 1

Statement usesDegree in an undirected edge list

Used byInvariant of the undirected Hierholzer recursion

TheoremAn edge at a vertex joins it to its other endpoint#✓fully proved

If an ordered pair \(e = (a, b)\) of vertices has \(a = v\) or \(b = v\), then the unordered pair \(\{a, b\}\) equals \(\{v, w\}\), where \(w\) is the other endpoint of \(e\) at \(v\).

theorem usym_eq_otherEnd {e : V × V} {v : V} (h : e.1 = v ∨ e.2 = v) :
    usym e = s(v, otherEnd e v)

Uses 2 · Used by 1

Statement usesOther endpoint of an edge · Unordered edge of an ordered pair

Used byInvariant of the undirected Hierholzer recursion

TheoremInvariant of the undirected Hierholzer recursion#✓fully proved

Let \(R\) be a list of edges, \(v\), \(t\) vertices such that exactly \(v\) and \(t\) have odd degree in \(R\) (no vertex when \(v = t\)), \(A\) a list of vertices, and \(f > |R|\) a fuel bound. Run the undirected Hierholzer recursion with fuel \(f\) from \(v\) on \(R\) with accumulator \(A\), and let \(R'\) be the remaining edge list it returns and \(c\) its cost. Then there is a vertex sequence \(W\) starting at \(v\) and ending at \(t\) such that the returned vertex list is \(W\) followed by \(A\); the edges of \(R\), as unordered pairs, are a permutation of the consecutive pairs of \(W\) followed by the edges of \(R'\), all as unordered pairs; every vertex has even degree in \(R'\); every vertex of \(W\) has degree \(0\) in \(R'\); \(R'\) is a sublist of \(R\); and \(c + |R'| = |R|\).

theorem uvisit_spec : ∀ (fuel : ℕ) (v t : V) (R : List (V × V)) (acc : List V),
    R.length < fuel → EvenExcept R v t →
    ∃ W, (uvisit fuel v R acc).ret.1 = W ++ acc ∧ W.head? = some v ∧ W.getLast? = some t ∧
      (R.map usym).Perm ((walkEdges W).map usym ++ (uvisit fuel v R acc).ret.2.map usym) ∧
      (∀ x, udeg (uvisit fuel v R acc).ret.2 x % 2 = 0) ∧
      (∀ x ∈ W, udeg (uvisit fuel v R acc).ret.2 x = 0) ∧
      (uvisit fuel v R acc).ret.2.Sublist R ∧
      (uvisit fuel v R acc).time + (uvisit fuel v R acc).ret.2.length = R.length

Uses 10 · Used by 3

Statement usesDegree parity condition for two endpoints · Degree in an undirected edge list · Unordered edge of an ordered pair · Undirected Hierholzer recursion · Steps of a walk

Proof usesOther endpoint of an edge · Moving a block of a list in front of an element is a permutation · Degree after removing an edge · An edge at a vertex joins it to its other endpoint · Steps of a concatenated walk

Used byUndirected Hierholzer's algorithm finds Euler paths · Cost of the undirected Hierholzer algorithm · Undirected Hierholzer's algorithm returns a trail

TheoremUndirected Hierholzer's algorithm returns a trail#✓fully proved

Let \(E\) be a list of undirected edges and \(s\), \(t\) vertices such that exactly \(s\) and \(t\) have odd degree in \(E\) (no vertex has odd degree when \(s = t\)). Then the vertex sequence \(W\) returned by the undirected Hierholzer algorithm on \(E\) from \(s\) starts at \(s\) and ends at \(t\), and the consecutive pairs of \(W\), as unordered pairs, form a sub-multiset of the edges of \(E\) as unordered pairs: no edge is traversed more often than it occurs in \(E\).

theorem uhierholzer_trail (E : List (V × V)) (s t : V) (hpar : EvenExcept E s t) :
    (uhierholzer E s).ret.head? = some s ∧ (uhierholzer E s).ret.getLast? = some t ∧
      ∃ rest, (E.map usym).Perm ((walkEdges (uhierholzer E s).ret).map usym ++ rest)

Uses 7

Statement usesDegree parity condition for two endpoints · Undirected Hierholzer's algorithm · Unordered edge of an ordered pair · Steps of a walk

Proof usesDegree in an undirected edge list · Undirected Hierholzer recursion · Invariant of the undirected Hierholzer recursion

TheoremUndirected Hierholzer's algorithm finds Euler paths#✓fully proved

Let \(E\) be a list of undirected edges (ordered pairs of vertices) and \(s\), \(t\) vertices such that exactly \(s\) and \(t\) have odd degree in \(E\) (no vertex has odd degree when \(s = t\)), and suppose the first endpoint of every edge of \(E\) is reachable from \(s\) through edges of \(E\). Then the vertex sequence returned by the undirected Hierholzer algorithm on \(E\) from \(s\) is an Euler path of \(E\) from \(s\) to \(t\).

theorem uhierholzer_isUEulerPath (E : List (V × V)) (s t : V) (hpar : EvenExcept E s t)
    (hreach : ∀ e ∈ E, UReach E s e.1) : IsUEulerPath E s t (uhierholzer E s).ret

Uses 9 · Used by 2

Statement usesDegree parity condition for two endpoints · Euler path in an undirected multigraph · Reachability in an undirected multigraph · Undirected Hierholzer's algorithm

Proof usesDegree in an undirected edge list · Unordered edge of an ordered pair · Undirected Hierholzer recursion · Invariant of the undirected Hierholzer recursion · Steps of a walk

Used byEuler's theorem for undirected multigraphs · Undirected Hierholzer's algorithm finds Euler circuits

TheoremUndirected Hierholzer's algorithm finds Euler circuits#✓fully proved

Let \(E\) be a list of undirected edges (ordered pairs of vertices) in which every vertex has even degree, and let \(s\) be a vertex such that the first endpoint of every edge of \(E\) is reachable from \(s\) through edges of \(E\). Then the vertex sequence returned by the undirected Hierholzer algorithm on \(E\) from \(s\) is an Euler path of \(E\) from \(s\) to \(s\), that is, an Euler circuit at \(s\).

theorem uhierholzer_isUEulerCircuit (E : List (V × V)) (s : V) (hpar : ∀ x, udeg E x % 2 = 0)
    (hreach : ∀ e ∈ E, UReach E s e.1) : IsUEulerPath E s s (uhierholzer E s).ret

Uses 5

Statement usesEuler path in an undirected multigraph · Reachability in an undirected multigraph · Degree in an undirected edge list · Undirected Hierholzer's algorithm

Proof usesUndirected Hierholzer's algorithm finds Euler paths

TheoremCost of the undirected Hierholzer algorithm#✓fully proved

Let \(E\) be a list of undirected edges and \(s\), \(t\) vertices such that exactly \(s\) and \(t\) have odd degree in \(E\) (no vertex has odd degree when \(s = t\)), and suppose the first endpoint of every edge of \(E\) is reachable from \(s\) through edges of \(E\). Then the undirected Hierholzer algorithm on \(E\) from \(s\) costs exactly \(|E|\), the number of edges of \(E\), in the cost model that charges one unit per removed edge.

theorem uhierholzer_time (E : List (V × V)) (s t : V) (hpar : EvenExcept E s t)
    (hreach : ∀ e ∈ E, UReach E s e.1) : (uhierholzer E s).time = E.length

Uses 8

Statement usesDegree parity condition for two endpoints · Reachability in an undirected multigraph · Undirected Hierholzer's algorithm

Proof usesDegree in an undirected edge list · Unordered edge of an ordered pair · Undirected Hierholzer recursion · Invariant of the undirected Hierholzer recursion · Steps of a walk

DefinitionMultiplicity of a vertex in an unordered edge#✓fully proved

For a vertex \(x\), this assigns to an unordered pair \(\{a, b\}\) the number \([x = a] + [x = b]\) of its endpoints equal to \(x\), where \([P]\) is \(1\) if \(P\) holds and \(0\) otherwise; in particular a loop \(\{x, x\}\) gives \(2\).

def endsAt (x : V) : Sym2 V → ℕ :=
  Sym2.lift ⟨fun a b => (if x = a then 1 else 0) + (if x = b then 1 else 0),
    fun _ _ => Nat.add_comm _ _⟩

Used by 1

Used byDegrees depend only on the unordered edges

TheoremDegrees depend only on the unordered edges#✓fully proved

Let \(A\) and \(B\) be finite lists of edges of an undirected multigraph such that the multiset of edges of \(A\), taken as unordered pairs, equals that of \(B\). Then every vertex has the same degree in \(A\) as in \(B\).

theorem udeg_eq_of_perm {A B : List (V × V)} (h : (A.map usym).Perm (B.map usym)) (x : V) :
    udeg A x = udeg B x

Uses 3 · Used by 1

Statement usesDegree in an undirected edge list · Unordered edge of an ordered pair

Proof usesMultiplicity of a vertex in an unordered edge

Used byDegrees of an undirected Euler path

TheoremDegrees along a walk#✓fully proved

Let \(W = (w_0, \dots, w_n)\) be a nonempty sequence of vertices with \(w_0 = s\) and \(w_n = t\), and consider the multigraph whose edges are the consecutive pairs \((w_{i-1}, w_i)\) for \(1 \le i \le n\). In it every vertex other than \(s\) and \(t\) has even degree (a loop counts twice); if \(s \ne t\), then \(s\) and \(t\) have odd degree, and if \(s = t\), every vertex has even degree.

theorem evenExcept_walkEdges : ∀ (W : List V) (s t : V), W.head? = some s →
    W.getLast? = some t → EvenExcept (walkEdges W) s t

Uses 3 · Used by 1

Statement usesDegree parity condition for two endpoints · Steps of a walk

Proof usesDegree in an undirected edge list

Used byDegrees of an undirected Euler path

TheoremDegrees of an undirected Euler path#✓fully proved

Let \(E\) be a finite list of edges of an undirected multigraph and let \(W\) be an Euler path of \(E\) from \(s\) to \(t\). Then every vertex other than \(s\) and \(t\) has even degree in \(E\) (a loop counts twice); if \(s \ne t\), then \(s\) and \(t\) have odd degree, and if \(s = t\), every vertex has even degree.

theorem evenExcept_of_isUEulerPath {E : List (V × V)} {s t : V} {W : List V}
    (h : IsUEulerPath E s t W) : EvenExcept E s t

Uses 7 · Used by 1

Statement usesDegree parity condition for two endpoints · Euler path in an undirected multigraph

Proof usesDegrees along a walk · Degree in an undirected edge list · Degrees depend only on the unordered edges · Unordered edge of an ordered pair · Steps of a walk

Used byEuler's theorem for undirected multigraphs

TheoremEuler's theorem for undirected multigraphs#✓fully proved

Let \(E\) be a finite list of edges of an undirected multigraph (parallel edges and loops allowed), each given as a pair \((a, b)\), and let \(s\), \(t\) be vertices such that the first endpoint \(a\) of every edge is reachable from \(s\) along edges of \(E\) traversed in either direction. Then \(E\) has an Euler path from \(s\) to \(t\) if and only if, when \(s \ne t\), exactly \(s\) and \(t\) have odd degree, and, when \(s = t\), every vertex has even degree (a loop counts twice towards the degree).

This is the algorithmic form: the proof shows that Hierholzer's algorithm started at \(s\) finds such a path.

theorem exists_isUEulerPath_iff (E : List (V × V)) (s t : V)
    (hreach : ∀ e ∈ E, UReach E s e.1) :
    (∃ W, IsUEulerPath E s t W) ↔ EvenExcept E s t

Uses 6

Statement usesDegree parity condition for two endpoints · Euler path in an undirected multigraph · Reachability in an undirected multigraph

Proof usesDegrees of an undirected Euler path · Undirected Hierholzer's algorithm · Undirected Hierholzer's algorithm finds Euler paths

42 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.