Decomposing multigraph walks

This file splits an edge-labelled multigraph walk at the first occurrence of a specified vertex and extracts a path by bypassing repeated vertices. The extracted path keeps its endpoints and uses vertices and edge identities in their original order, so it can replace a walk in connectivity arguments without losing the distinction between parallel edges.

The interface is adapted from Mathlib's SimpleGraph.Walk.takeUntil, SimpleGraph.Walk.dropUntil, and SimpleGraph.Walk.bypass.

def Graph.Walk.takeUntil {α : Type u} {β : Type v} {G : Graph α β} [DecidableEq α] {x y : α} (p : G.Walk x y) (a : α) : a ∈ p.support → G.Walk x a

The initial segment of a walk ending at the first occurrence of a specified vertex.

def Graph.Walk.dropUntil {α : Type u} {β : Type v} {G : Graph α β} [DecidableEq α] {x y : α} (p : G.Walk x y) (a : α) : a ∈ p.support → G.Walk a y

The final segment of a walk starting at the first occurrence of a specified vertex.

@[simp]

theorem Graph.Walk.takeUntil_cons_of_ne {α : Type u} {β : Type v} {G : Graph α β} {x y z a : α} [DecidableEq α] (e : β) (h : G.IsLink e x y) (p : G.Walk y z) (hxa : x ≠ a) (ha : a ∈ (cons e h p).support) : (cons e h p).takeUntil a ha = cons e h (p.takeUntil a ⋯)

@[simp]

theorem Graph.Walk.dropUntil_cons_of_ne {α : Type u} {β : Type v} {G : Graph α β} {x y z a : α} [DecidableEq α] (e : β) (h : G.IsLink e x y) (p : G.Walk y z) (hxa : x ≠ a) (ha : a ∈ (cons e h p).support) : (cons e h p).dropUntil a ha = p.dropUntil a ⋯

@[simp]

theorem Graph.Walk.takeUntil_first {α : Type u} {β : Type v} {G : Graph α β} {x y : α} [DecidableEq α] (p : G.Walk x y) : p.takeUntil x ⋯ = nil

@[simp]

theorem Graph.Walk.dropUntil_first {α : Type u} {β : Type v} {G : Graph α β} {x y : α} [DecidableEq α] (p : G.Walk x y) : p.dropUntil x ⋯ = p

@[simp]

theorem Graph.Walk.takeUntil_append_dropUntil {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : (p.takeUntil a ha).append (p.dropUntil a ha) = p

Splitting at a vertex and rejoining the two pieces recovers the original walk.

theorem Graph.Walk.mem_support_iff_exists_append {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} {p : G.Walk x y} : a ∈ p.support ↔ ∃ (q : G.Walk x a) (r : G.Walk a y), p = q.append r

A vertex occurs on a walk exactly when the walk can be split there.

@[simp]

theorem Graph.Walk.count_support_takeUntil_eq_one {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : List.count a (p.takeUntil a ha).support = 1

The splitting vertex occurs exactly once in the initial segment.

theorem Graph.Walk.support_takeUntil_prefix_support {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : (p.takeUntil a ha).support <+: p.support

The support of the initial segment is a prefix of the original support.

theorem Graph.Walk.support_dropUntil_suffix_support {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : (p.dropUntil a ha).support <:+ p.support

The support of the final segment is a suffix of the original support.

theorem Graph.Walk.edges_takeUntil_prefix_edges {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : (p.takeUntil a ha).edges <+: p.edges

The edges of the initial segment are a prefix of the original edge list.

theorem Graph.Walk.edges_dropUntil_suffix_edges {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : (p.dropUntil a ha).edges <:+ p.edges

The edges of the final segment are a suffix of the original edge list.

theorem Graph.Walk.support_takeUntil_subset_support {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : (p.takeUntil a ha).support ⊆ p.support

theorem Graph.Walk.support_dropUntil_subset_support {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : (p.dropUntil a ha).support ⊆ p.support

theorem Graph.Walk.edges_takeUntil_subset_edges {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : (p.takeUntil a ha).edges ⊆ p.edges

theorem Graph.Walk.edges_dropUntil_subset_edges {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : (p.dropUntil a ha).edges ⊆ p.edges

theorem Graph.Walk.length_takeUntil_le_length {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : (p.takeUntil a ha).length ≤ p.length

theorem Graph.Walk.length_dropUntil_le_length {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] (p : G.Walk x y) (ha : a ∈ p.support) : (p.dropUntil a ha).length ≤ p.length

theorem Graph.Walk.IsTrail.takeUntil {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] {p : G.Walk x y} (hp : p.IsTrail) (ha : a ∈ p.support) : (p.takeUntil a ha).IsTrail

An initial segment of a trail is a trail.

theorem Graph.Walk.IsTrail.dropUntil {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] {p : G.Walk x y} (hp : p.IsTrail) (ha : a ∈ p.support) : (p.dropUntil a ha).IsTrail

A final segment of a trail is a trail.

theorem Graph.Walk.IsPath.takeUntil {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] {p : G.Walk x y} (hp : p.IsPath) (ha : a ∈ p.support) : (p.takeUntil a ha).IsPath

An initial segment of a path is a path.

theorem Graph.Walk.IsPath.dropUntil {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} [DecidableEq α] {p : G.Walk x y} (hp : p.IsPath) (ha : a ∈ p.support) : (p.dropUntil a ha).IsPath

A final segment of a path is a path.

theorem Graph.Walk.IsPath.exists_initialSegment_to_set {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p : G.Walk x y} (hp : p.IsPath) {S : Set α} (hx : x ∉ S) (hy : y ∈ S) : ∃ (z : α) (q : G.Walk x z), q.IsPath ∧ z ∈ S ∧ (∀ w ∈ q.support, w ≠ x → w ≠ z → w ∉ S) ∧ q.support ⊆ p.support ∧ q.edges ⊆ p.edges

A path from outside a vertex set to a vertex in it has an initial segment whose endpoint is the first visited vertex in the set. Every other vertex of the segment is outside the set, and the segment uses only vertices and edge identities of the original path.

theorem Graph.Walk.mem_edges_iff_exists_append {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p : G.Walk x y} {e : β} : e ∈ p.edges ↔ ∃ (u : α) (v : α) (h : G.IsLink e u v) (q : G.Walk x u) (r : G.Walk v y), p = q.append (cons e h r)

An edge identity occurs on a walk exactly when the walk can be split around one traversal of that edge.

theorem Graph.Walk.IsPath.eq_toWalk_of_isLink_mem_edges {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} {p : G.Walk x y} (hp : p.IsPath) (h : G.IsLink e x y) (he : e ∈ p.edges) : p = h.toWalk

A path whose endpoints are joined by an edge that it traverses consists of that edge alone.

theorem Graph.Walk.IsPath.not_isLoopAt_of_mem_edges {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} {p : G.Walk x y} (hp : p.IsPath) (he : e ∈ p.edges) (a : α) : ¬G.IsLoopAt e a

A path cannot traverse a loop edge.

def Graph.Walk.bypass {α : Type u} {β : Type v} {G : Graph α β} [DecidableEq α] {x y : α} : G.Walk x y → G.Walk x y

Remove closed portions of a walk between repeated vertices, retaining the endpoints.

@[simp]

theorem Graph.Walk.bypass_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} [DecidableEq α] : nil.bypass = nil

theorem Graph.Walk.bypass_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} [DecidableEq α] (e : β) (h : G.IsLink e x y) (p : G.Walk y z) : (cons e h p).bypass = if hx : x ∈ p.bypass.support then p.bypass.dropUntil x hx else cons e h p.bypass

theorem Graph.Walk.bypass_isPath {α : Type u} {β : Type v} {G : Graph α β} {x y : α} [DecidableEq α] (p : G.Walk x y) : p.bypass.IsPath

Bypassing repeated vertices produces a path.

theorem Graph.Walk.support_bypass_sublist_support {α : Type u} {β : Type v} {G : Graph α β} {x y : α} [DecidableEq α] (p : G.Walk x y) : p.bypass.support.Sublist p.support

Bypassing preserves the order of the retained vertices.

theorem Graph.Walk.edges_bypass_sublist_edges {α : Type u} {β : Type v} {G : Graph α β} {x y : α} [DecidableEq α] (p : G.Walk x y) : p.bypass.edges.Sublist p.edges

Bypassing preserves the order and identity of the retained edges.

theorem Graph.Walk.support_bypass_subset_support {α : Type u} {β : Type v} {G : Graph α β} {x y : α} [DecidableEq α] (p : G.Walk x y) : p.bypass.support ⊆ p.support

theorem Graph.Walk.edges_bypass_subset_edges {α : Type u} {β : Type v} {G : Graph α β} {x y : α} [DecidableEq α] (p : G.Walk x y) : p.bypass.edges ⊆ p.edges

theorem Graph.Walk.length_bypass_le_length {α : Type u} {β : Type v} {G : Graph α β} {x y : α} [DecidableEq α] (p : G.Walk x y) : p.bypass.length ≤ p.length

theorem Graph.Walk.IsPath.bypass_eq_self {α : Type u} {β : Type v} {G : Graph α β} {x y : α} [DecidableEq α] {p : G.Walk x y} (hp : p.IsPath) : p.bypass = p

Bypassing a path does not change it.

@[simp]

theorem Graph.Walk.bypass_eq_self_iff_isPath {α : Type u} {β : Type v} {G : Graph α β} {x y : α} [DecidableEq α] {p : G.Walk x y} : p.bypass = p ↔ p.IsPath

theorem Graph.Reachable.exists_isPath {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (h : G.Reachable x y) : ∃ (p : G.Walk x y), p.IsPath

Every pair of reachable vertices is joined by a path retaining actual multigraph edge identities.