Walks

In a simple graph, a walk is a finite sequence of adjacent vertices, and can be thought of equally well as a sequence of directed edges.

Warning: graph theorists mean something different by "path" than do homotopy theorists. A "walk" in graph theory is a "path" in homotopy theory. Another warning: some graph theorists use "path" and "simple path" for "walk" and "path."

Some definitions and theorems have inspiration from multigraph counterparts in [Cho94].

Main definitions

• SimpleGraph.Walk (with accompanying pattern definitions SimpleGraph.Walk.nil' and SimpleGraph.Walk.cons')
• SimpleGraph.Walk.Nil: A predicate for the empty walk
• SimpleGraph.Walk.length: The length of a walk
• SimpleGraph.Walk.support: The list of vertices a walk visits in order
• SimpleGraph.Walk.darts: The list of darts a walk visits in order
• SimpleGraph.Walk.edges: The list of edges a walk visits in order
• SimpleGraph.Walk.edgeSet: The set of edges of a walk visits

Tags

walks

inductive SimpleGraph.Walk {V : Type u} (G : SimpleGraph V) : V → V → Type u

A walk is a sequence of adjacent vertices. For vertices u v : V, the type walk u v consists of all walks starting at u and ending at v.

We say that a walk visits the vertices it contains. The set of vertices a walk visits is SimpleGraph.Walk.support.

See SimpleGraph.Walk.nil' and SimpleGraph.Walk.cons' for patterns that can be useful in definitions since they make the vertices explicit.

• nil {V : Type u} {G : SimpleGraph V} {u : V} : G.Walk u u
• cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : G.Walk u w

def SimpleGraph.instDecidableEqWalk.decEq {V✝ : Type u_1} {G✝ : SimpleGraph V✝} {a✝ a✝¹ : V✝} [DecidableEq V✝] (x✝ x✝¹ : G✝.Walk a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• SimpleGraph.instDecidableEqWalk.decEq SimpleGraph.Walk.nil SimpleGraph.Walk.nil = isTrue ⋯
• SimpleGraph.instDecidableEqWalk.decEq SimpleGraph.Walk.nil (SimpleGraph.Walk.cons h p) = isFalse ⋯
• SimpleGraph.instDecidableEqWalk.decEq (SimpleGraph.Walk.cons h p) SimpleGraph.Walk.nil = isFalse ⋯

instance SimpleGraph.instDecidableEqWalk {V✝ : Type u_1} {G✝ : SimpleGraph V✝} {a✝ a✝¹ : V✝} [DecidableEq V✝] : DecidableEq (G✝.Walk a✝ a✝¹)

Equations

• SimpleGraph.instDecidableEqWalk = SimpleGraph.instDecidableEqWalk.decEq

instance SimpleGraph.Walk.instInhabited {V : Type u} (G : SimpleGraph V) (v : V) : Inhabited (G.Walk v v)

Equations

• SimpleGraph.Walk.instInhabited G v = { default := SimpleGraph.Walk.nil }

@[simp]

theorem SimpleGraph.Walk.default_def {V : Type u} (G : SimpleGraph V) (v : V) : default = nil

@[reducible, match_pattern]

def SimpleGraph.Adj.toWalk {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : G.Walk u v

The one-edge walk associated to a pair of adjacent vertices.

Equations

• h.toWalk = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil

@[reducible, match_pattern, inline]

abbrev SimpleGraph.Walk.nil' {V : Type u} {G : SimpleGraph V} (u : V) : G.Walk u u

Pattern to get Walk.nil with the vertex as an explicit argument.

Equations

• SimpleGraph.Walk.nil' u = SimpleGraph.Walk.nil

@[reducible, match_pattern, inline]

abbrev SimpleGraph.Walk.cons' {V : Type u} {G : SimpleGraph V} (u v w : V) (h : G.Adj u v) (p : G.Walk v w) : G.Walk u w

Pattern to get Walk.cons with the vertices as explicit arguments.

Equations

• SimpleGraph.Walk.cons' u v w h p = SimpleGraph.Walk.cons h p

theorem SimpleGraph.Walk.exists_eq_cons_of_ne {V : Type u} {G : SimpleGraph V} {u v : V} (hne : u ≠ v) (p : G.Walk u v) : ∃ (w : V) (h : G.Adj u w) (p' : G.Walk w v), p = cons h p'

def SimpleGraph.Walk.length {V : Type u} {G : SimpleGraph V} {u v : V} : G.Walk u v → ℕ

The length of a walk is the number of edges/darts along it.

Equations

• SimpleGraph.Walk.nil.length = 0
• (SimpleGraph.Walk.cons h q).length = q.length.succ

@[simp]

theorem SimpleGraph.Walk.length_nil {V : Type u} {G : SimpleGraph V} {u : V} : nil.length = 0

@[simp]

theorem SimpleGraph.Walk.length_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (cons h p).length = p.length + 1

theorem SimpleGraph.Walk.eq_of_length_eq_zero {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.length = 0 → u = v

theorem SimpleGraph.Walk.adj_of_length_eq_one {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.length = 1 → G.Adj u v

@[simp]

theorem SimpleGraph.Walk.exists_length_eq_zero_iff {V : Type u} {G : SimpleGraph V} {u v : V} : (∃ (p : G.Walk u v), p.length = 0) ↔ u = v

@[simp]

theorem SimpleGraph.Walk.exists_length_eq_one_iff {V : Type u} {G : SimpleGraph V} {u v : V} : (∃ (p : G.Walk u v), p.length = 1) ↔ G.Adj u v

@[simp]

theorem SimpleGraph.Walk.length_eq_zero_iff {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} : p.length = 0 ↔ p = nil

def SimpleGraph.Walk.support {V : Type u} {G : SimpleGraph V} {u v : V} : G.Walk u v → List V

The support of a walk is the list of vertices it visits in order.

Equations

• SimpleGraph.Walk.nil.support = [u]
• (SimpleGraph.Walk.cons h q).support = u :: q.support

def SimpleGraph.Walk.darts {V : Type u} {G : SimpleGraph V} {u v : V} : G.Walk u v → List G.Dart

The darts of a walk is the list of darts it visits in order.

Equations

• SimpleGraph.Walk.nil.darts = []
• (SimpleGraph.Walk.cons h q).darts = { fst := u, snd := v_3, adj := h } :: q.darts

def SimpleGraph.Walk.edges {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List (Sym2 V)

The edges of a walk is the list of edges it visits in order. This is defined to be the list of edges underlying SimpleGraph.Walk.darts.

Equations

• p.edges = List.map SimpleGraph.Dart.edge p.darts

@[simp]

theorem SimpleGraph.Walk.support_nil {V : Type u} {G : SimpleGraph V} {u : V} : nil.support = [u]

@[simp]

theorem SimpleGraph.Walk.support_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (cons h p).support = u :: p.support

@[simp]

theorem SimpleGraph.Walk.support_ne_nil {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support ≠ []

@[simp]

theorem SimpleGraph.Walk.head_support {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b) : p.support.head ⋯ = a

@[simp]

theorem SimpleGraph.Walk.getLast_support {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b) : p.support.getLast ⋯ = b

theorem SimpleGraph.Walk.support_eq_cons {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support = u :: p.support.tail

@[simp]

theorem SimpleGraph.Walk.start_mem_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : u ∈ p.support

@[simp]

theorem SimpleGraph.Walk.end_mem_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : v ∈ p.support

@[simp]

theorem SimpleGraph.Walk.support_nonempty {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : {w : V | w ∈ p.support}.Nonempty

theorem SimpleGraph.Walk.mem_support_iff {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) : w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail

theorem SimpleGraph.Walk.mem_support_nil_iff {V : Type u} {G : SimpleGraph V} {u v : V} : u ∈ nil.support ↔ u = v

@[simp]

theorem SimpleGraph.Walk.end_mem_tail_support_of_ne {V : Type u} {G : SimpleGraph V} {u v : V} (h : u ≠ v) (p : G.Walk u v) : v ∈ p.support.tail

theorem SimpleGraph.Walk.support_subset_support_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk v w) (hadj : G.Adj u v) : p.support ⊆ (cons hadj p).support

theorem SimpleGraph.Walk.coe_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : ↑p.support = {u} + ↑p.support.tail

theorem SimpleGraph.Walk.isChain_adj_cons_support {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : List.IsChain G.Adj (u :: p.support)

@[deprecated SimpleGraph.Walk.isChain_adj_cons_support (since := "2025-09-24")]

theorem SimpleGraph.Walk.chain_adj_support {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : List.IsChain G.Adj (u :: p.support)

Alias of SimpleGraph.Walk.isChain_adj_cons_support.

theorem SimpleGraph.Walk.isChain_adj_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.IsChain G.Adj p.support

@[deprecated SimpleGraph.Walk.isChain_adj_support (since := "2025-09-24")]

theorem SimpleGraph.Walk.chain'_adj_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.IsChain G.Adj p.support

Alias of SimpleGraph.Walk.isChain_adj_support.

theorem SimpleGraph.Walk.isChain_dartAdj_cons_darts {V : Type u} {G : SimpleGraph V} {d : G.Dart} {v w : V} (h : d.toProd.2 = v) (p : G.Walk v w) : List.IsChain G.DartAdj (d :: p.darts)

theorem SimpleGraph.Walk.isChain_dartAdj_darts {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.IsChain G.DartAdj p.darts

@[deprecated SimpleGraph.Walk.isChain_dartAdj_cons_darts (since := "2025-09-24")]

theorem SimpleGraph.Walk.chain_dartAdj_darts {V : Type u} {G : SimpleGraph V} {d : G.Dart} {v w : V} (h : d.toProd.2 = v) (p : G.Walk v w) : List.IsChain G.DartAdj (d :: p.darts)

Alias of SimpleGraph.Walk.isChain_dartAdj_cons_darts.

@[deprecated SimpleGraph.Walk.isChain_dartAdj_darts (since := "2025-09-24")]

theorem SimpleGraph.Walk.chain'_dartAdj_darts {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.IsChain G.DartAdj p.darts

Alias of SimpleGraph.Walk.isChain_dartAdj_darts.

theorem SimpleGraph.Walk.edges_subset_edgeSet {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) ⦃e : Sym2 V⦄ : e ∈ p.edges → e ∈ G.edgeSet

Every edge in a walk's edge list is an edge of the graph. It is written in this form (rather than using ⊆) to avoid unsightly coercions.

theorem SimpleGraph.Walk.adj_of_mem_edges {V : Type u} {G : SimpleGraph V} {u v x y : V} (p : G.Walk u v) (h : s(x, y) ∈ p.edges) : G.Adj x y

@[simp]

theorem SimpleGraph.Walk.darts_nil {V : Type u} {G : SimpleGraph V} {u : V} : nil.darts = []

@[simp]

theorem SimpleGraph.Walk.darts_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (cons h p).darts = { fst := u, snd := v, adj := h } :: p.darts

theorem SimpleGraph.Walk.cons_map_snd_darts {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : u :: List.map (fun (x : G.Dart) => x.toProd.2) p.darts = p.support

theorem SimpleGraph.Walk.map_snd_darts {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.map (fun (x : G.Dart) => x.toProd.2) p.darts = p.support.tail

theorem SimpleGraph.Walk.map_fst_darts_append {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.map (fun (x : G.Dart) => x.toProd.1) p.darts ++ [v] = p.support

theorem SimpleGraph.Walk.map_fst_darts {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.map (fun (x : G.Dart) => x.toProd.1) p.darts = p.support.dropLast

@[simp]

theorem SimpleGraph.Walk.head_darts_fst {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) : (p.darts.head hp).toProd.1 = a

@[simp]

theorem SimpleGraph.Walk.getLast_darts_snd {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) : (p.darts.getLast hp).toProd.2 = b

@[simp]

theorem SimpleGraph.Walk.edges_nil {V : Type u} {G : SimpleGraph V} {u : V} : nil.edges = []

@[simp]

theorem SimpleGraph.Walk.edges_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (cons h p).edges = s(u, v) :: p.edges

@[simp]

theorem SimpleGraph.Walk.length_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support.length = p.length + 1

@[simp]

theorem SimpleGraph.Walk.length_darts {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.darts.length = p.length

@[simp]

theorem SimpleGraph.Walk.length_edges {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.edges.length = p.length

theorem SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {d : G.Dart} : d ∈ p.darts → d.toProd.1 ∈ p.support

theorem SimpleGraph.Walk.mem_support_iff_exists_mem_edges {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} : w ∈ p.support ↔ w = v ∨ ∃ e ∈ p.edges, w ∈ e

theorem SimpleGraph.Walk.darts_nodup_of_support_nodup {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.support.Nodup) : p.darts.Nodup

theorem SimpleGraph.Walk.edges_eq_zipWith_support {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.edges = List.zipWith (fun (x1 x2 : V) => s(x1, x2)) p.support p.support.tail

theorem SimpleGraph.Walk.edges_injective {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective edges

theorem SimpleGraph.Walk.darts_injective {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective darts

def SimpleGraph.Walk.edgeSet {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : Set (Sym2 V)

The Set of edges of a walk.

Equations

• p.edgeSet = {e : Sym2 V | e ∈ p.edges}

@[simp]

theorem SimpleGraph.Walk.mem_edgeSet {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {e : Sym2 V} : e ∈ p.edgeSet ↔ e ∈ p.edges

@[simp]

theorem SimpleGraph.Walk.edgeSet_nil {V : Type u} {G : SimpleGraph V} (u : V) : nil.edgeSet = ∅

@[simp]

theorem SimpleGraph.Walk.edgeSet_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (cons h p).edgeSet = insert s(u, v) p.edgeSet

theorem SimpleGraph.Walk.coe_edges_toFinset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : ↑p.edges.toFinset = p.edgeSet

inductive SimpleGraph.Walk.Nil {V : Type u} {G : SimpleGraph V} {v w : V} : G.Walk v w → Prop

Predicate for the empty walk.

Solves the dependent type problem where p = G.Walk.nil typechecks only if p has defeq endpoints.

• nil {V : Type u} {G : SimpleGraph V} {u : V} : Walk.nil.Nil

@[simp]

theorem SimpleGraph.Walk.nil_nil {V : Type u} {G : SimpleGraph V} {u : V} : nil.Nil

@[simp]

theorem SimpleGraph.Walk.not_nil_cons {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w} : ¬(cons h p).Nil

instance SimpleGraph.Walk.instDecidableNil {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) : Decidable p.Nil

Equations

• SimpleGraph.Walk.nil.instDecidableNil = isTrue ⋯
• (SimpleGraph.Walk.cons h q).instDecidableNil = isFalse ⋯

theorem SimpleGraph.Walk.Nil.eq {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.Nil → v = w

theorem SimpleGraph.Walk.not_nil_of_ne {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : v ≠ w → ¬p.Nil

theorem SimpleGraph.Walk.nil_iff_support_eq {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.Nil ↔ p.support = [v]

theorem SimpleGraph.Walk.nil_iff_length_eq {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.Nil ↔ p.length = 0

theorem SimpleGraph.Walk.not_nil_iff_lt_length {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : ¬p.Nil ↔ 0 < p.length

theorem SimpleGraph.Walk.not_nil_iff {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : ¬p.Nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u w), p = cons h q

theorem SimpleGraph.Walk.nil_iff_eq_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} : p.Nil ↔ p = nil

A walk with its endpoints defeq is Nil if and only if it is equal to nil.

theorem SimpleGraph.Walk.Nil.eq_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} : p.Nil → p = Walk.nil

Alias of the forward direction of SimpleGraph.Walk.nil_iff_eq_nil.

---

A walk with its endpoints defeq is Nil if and only if it is equal to nil.

def SimpleGraph.Walk.notNilRec {V : Type u} {G : SimpleGraph V} {u w : V} {motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1} (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (cons h q) ⋯) (p : G.Walk u w) (hp : ¬p.Nil) : motive p hp

The recursion principle for nonempty walks

Equations

• SimpleGraph.Walk.notNilRec cons SimpleGraph.Walk.nil = fun (hp : ¬SimpleGraph.Walk.nil.Nil) => absurd ⋯ hp
• SimpleGraph.Walk.notNilRec cons (SimpleGraph.Walk.cons h q) = fun (x : ¬(SimpleGraph.Walk.cons h q).Nil) => cons h q

@[simp]

theorem SimpleGraph.Walk.notNilRec_cons {V : Type u} {G : SimpleGraph V} {u v w : V} {motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1} (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (cons h q) ⋯) (h' : G.Adj u v) (q' : G.Walk v w) : notNilRec (fun {u v w : V} => cons) (Walk.cons h' q') ⋯ = cons h' q'

theorem SimpleGraph.Walk.end_mem_tail_support {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : ¬p.Nil) : v ∈ p.support.tail

theorem SimpleGraph.Walk.mem_support_iff_exists_mem_edges_of_not_nil {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hnil : ¬p.Nil) : w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e

theorem SimpleGraph.Walk.exists_boundary_dart {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (S : Set V) (uS : u ∈ S) (vS : v ∉ S) : ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Given a set S and a walk w from u to v such that u ∈ S but v ∉ S, there exists a dart in the walk whose start is in S but whose end is not.