Simple paths

A SimplePath α is a SimpleWalk α whose vertices are pairwise distinct. This file keeps paths as a subtype of simple walks, so every path can be used where a simple walk is expected.

Main definitions

• SimpleWalk.IsPath — a simple walk with no repeated vertices.
• SimplePath — a simple walk bundled with a proof that its vertices are pairwise distinct.
• SimplePath.singleton, SimplePath.cycleErase — the two constructors: a one-vertex path, and the path underlying any simple walk.
• SimplePath.append, SimplePath.glue — join two paths, keeping resp. dropping the duplicated joining vertex.
• SimplePath.reverse, SimplePath.dropHead, SimplePath.dropTail, SimplePath.prefixUntil, SimplePath.suffixFrom, SimplePath.takeWhile, SimplePath.dropWhile, SimplePath.splitAt, SimplePath.map, SimplePath.zip, SimplePath.loopErase — the SimpleWalk operations, lifted.

Every operation is the SimpleWalk one plus a proof that nodup survives.

@[reducible, inline]

abbrev SimpleWalk.IsPath {α : Type u_1} (w : SimpleWalk α) : Prop

A simple walk is a path when it has no repeated vertices.

Equations

• w.IsPath = w.nodup

def SimplePath (α : Type u_2) : Type u_2

A simple path is a simple walk with no repeated vertex.

Equations

• SimplePath α = { w : SimpleWalk α // w.IsPath }

Basic accessors

@[reducible, inline]

abbrev SimplePath.val {α : Type u_1} (p : SimplePath α) : SimpleWalk α

The underlying simple walk.

Equations

• p.val = ↑p

@[reducible, inline]

abbrev SimplePath.vertices {α : Type u_1} (p : SimplePath α) : VertexSeq α

The underlying vertex sequence.

Equations

• p.vertices = p.val.val

@[reducible, inline]

abbrev SimplePath.support {α : Type u_1} (p : SimplePath α) : List α

The list of vertices visited by the path.

Equations

• p.support = p.vertices.toList

@[reducible, inline]

abbrev SimplePath.edges {α : Type u_1} (p : SimplePath α) : List (Sym2 α)

The unordered edges traversed by the path.

Equations

• p.edges = p.vertices.edges

@[reducible, inline]

abbrev SimplePath.arcs {α : Type u_1} (p : SimplePath α) : List (α × α)

The directed arcs traversed by the path.

Equations

• p.arcs = p.vertices.arcs

@[reducible, inline]

abbrev SimplePath.head {α : Type u_1} (p : SimplePath α) : α

The first vertex of the path.

Equations

• p.head = p.vertices.head

@[reducible, inline]

abbrev SimplePath.tail {α : Type u_1} (p : SimplePath α) : α

The last vertex of the path.

Equations

• p.tail = p.vertices.tail

@[reducible, inline]

abbrev SimplePath.length {α : Type u_1} (p : SimplePath α) : ℕ

The number of edges in the path.

Equations

• p.length = p.vertices.length

theorem SimplePath.nodup {α : Type u_1} (p : SimplePath α) : p.vertices.nodup

A path has no repeated vertices.

@[implicit_reducible]

instance SimplePath.instCoeSimpleWalk {α : Type u_1} : Coe (SimplePath α) (SimpleWalk α)

A simple path is, in particular, a simple walk.

Equations

• SimplePath.instCoeSimpleWalk = { coe := SimplePath.val }

Constructors

def SimplePath.singleton {α : Type u_1} (v : α) : SimplePath α

The singleton path at v: a single vertex and no edges.

Equations

• SimplePath.singleton v = ⟨⟨VertexSeq.singleton v, True.intro⟩, True.intro⟩

@[simp]

theorem SimplePath.vertices_singleton {α : Type u_1} (v : α) : (singleton v).vertices = VertexSeq.singleton v

The vertex sequence of a singleton path. This is the bridge that lets simp see through SimplePath.singleton down to the VertexSeq layer, where the singleton API lives.

@[simp]

theorem SimplePath.length_singleton {α : Type u_1} (v : α) : (singleton v).length = 0

@[simp]

theorem SimplePath.head_singleton {α : Type u_1} (v : α) : (singleton v).head = v

@[simp]

theorem SimplePath.tail_singleton {α : Type u_1} (v : α) : (singleton v).tail = v

def SimplePath.cycleErase {α : Type u_1} [DecidableEq α] (w : SimpleWalk α) : SimplePath α

Cycle erasure of any simple walk produces a simple path.

Equations

• SimplePath.cycleErase w = ⟨w.cycleErase, ⋯⟩

dropHead, dropTail

def SimplePath.dropHead {α : Type u_1} (p : SimplePath α) : SimplePath α

Drop the first vertex of a path. Removing an endpoint preserves nodup.

Equations

• p.dropHead = ⟨p.val.dropHead, ⋯⟩

def SimplePath.dropTail {α : Type u_1} (p : SimplePath α) : SimplePath α

Drop the last vertex of a path. Removing an endpoint preserves nodup.

Equations

• p.dropTail = ⟨p.val.dropTail, ⋯⟩

append, glue

def SimplePath.append {α : Type u_1} (p q : SimplePath α) (hdisj : ∀ v ∈ p.vertices, v ∈ q.vertices → False) : SimplePath α

Concatenate two vertex-disjoint paths, keeping both joining vertices. The disjointness hypothesis is what preserves nodup; it also rules out a stall at the junction.

Equations

• p.append q hdisj = ⟨p.val.append q.val ⋯, ⋯⟩

@[simp]

theorem SimplePath.vertices_append {α : Type u_1} (p q : SimplePath α) (hdisj : ∀ v ∈ p.vertices, v ∈ q.vertices → False) : (p.append q hdisj).vertices = p.vertices.append q.vertices

The vertex sequence of an append is the append of the vertex sequences. This is the bridge that lets simp see through SimplePath.append down to the VertexSeq layer, where head_append / tail_append / length_append / mem_append live.

def SimplePath.glue {α : Type u_1} (p q : SimplePath α) (h : p.tail = q.head) (hdisj : p.vertices.length ≠ 0 → ∀ v ∈ p.vertices.dropTail, v ∈ q.vertices → False) : SimplePath α

Concatenate two paths meeting at a shared vertex, dropping the duplicated joining vertex. When p is nontrivial its remaining vertices must be disjoint from q; when p is a single vertex the result is just q, so no disjointness is required. Guarding the hypothesis by length ≠ 0 keeps the singleton-left case usable, since dropTail leaves a singleton unchanged.

Equations

• p.glue q h hdisj = ⟨p.val.glue q.val h, ⋯⟩

reverse

def SimplePath.reverse {α : Type u_1} (p : SimplePath α) : SimplePath α

Reverse a path. Reversal preserves nodup.

Equations

• p.reverse = ⟨p.val.reverse, ⋯⟩

prefixUntil, suffixFrom

def SimplePath.prefixUntil {α : Type u_1} [DecidableEq α] (p : SimplePath α) (v : α) (h : v ∈ p.vertices) : SimplePath α

The prefix of a path ending at the first occurrence of v. A contiguous prefix of a path is a path.

Equations

• p.prefixUntil v h = ⟨p.val.prefixUntil v h, ⋯⟩

def SimplePath.suffixFrom {α : Type u_1} [DecidableEq α] (p : SimplePath α) (v : α) (h : v ∈ p.vertices) : SimplePath α

The suffix of a path starting at the first occurrence of v. A contiguous suffix of a path is a path.

Equations

• p.suffixFrom v h = ⟨p.val.suffixFrom v h, ⋯⟩

map

def SimplePath.map {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Function.Injective f) (p : SimplePath α) : SimplePath β

Map a path through an injective function. Injectivity preserves distinct vertices.

Equations

• SimplePath.map f hf p = ⟨SimpleWalk.map f hf p.val, ⋯⟩

takeWhile, dropWhile

def SimplePath.takeWhile {α : Type u_1} (p : SimplePath α) (q : α → Prop) [DecidablePred q] : SimplePath α

Take a contiguous prefix of a path, including the first failure if any.

Equations

• p.takeWhile q = ⟨p.val.takeWhile q, ⋯⟩

def SimplePath.dropWhile {α : Type u_1} (p : SimplePath α) (q : α → Prop) [DecidablePred q] (h : ∃ v ∈ p.vertices.toList, ¬q v) : SimplePath α

Drop the longest prefix of a path on which q holds. The result is a contiguous suffix, hence a path.

Equations

• p.dropWhile q h = ⟨p.val.dropWhile q h, ⋯⟩

splitAt

def SimplePath.splitAt {α : Type u_1} [DecidableEq α] (p : SimplePath α) (v : α) : List (SimplePath α)

Split a path at every occurrence of v. Every produced piece is a contiguous subpath.

Equations

• p.splitAt v = List.pmap (fun (w : VertexSeq α) (hw : w.nonstalling ∧ w.nodup) => ⟨⟨w, ⋯⟩, ⋯⟩) (p.vertices.splitAt v) ⋯

zip

def SimplePath.zip {α : Type u_1} {β : Type u_2} (p : SimplePath α) (q : SimplePath β) : SimplePath (α × β)

Zip two paths into a path of pairs. Pairwise distinct first components are enough to make the pairs pairwise distinct.

Equations

• p.zip q = ⟨p.val.zip q.val, ⋯⟩

loopErase

def SimplePath.loopErase {α : Type u_1} [DecidableEq α] (p : SimplePath α) : SimplePath α

Remove immediate stalls from a path. Since a path has no repeated vertices, this preserves nodup.

Equations

• p.loopErase = ⟨p.val.loopErase, ⋯⟩

edges

@[simp]

theorem SimplePath.length_edges {α : Type u_1} (p : SimplePath α) : p.edges.length = p.length

The number of traversed edges equals the path's length.

theorem SimplePath.edges_nodup {α : Type u_1} (p : SimplePath α) : p.edges.Nodup

A path traverses each edge at most once (a path is a trail).

@[simp]

theorem SimplePath.edges_reverse {α : Type u_1} (p : SimplePath α) : p.reverse.edges = p.edges.reverse

Reversal reverses the edge list.

theorem SimplePath.edges_dropTail_subset {α : Type u_1} (p : SimplePath α) : p.dropTail.edges ⊆ p.edges

Dropping the last vertex cannot introduce new edges.

theorem SimplePath.edges_dropHead_subset {α : Type u_1} (p : SimplePath α) : p.dropHead.edges ⊆ p.edges

Dropping the first vertex cannot introduce new edges.

theorem SimplePath.edges_prefixUntil_subset {α : Type u_1} [DecidableEq α] (p : SimplePath α) (v : α) (h : v ∈ p.vertices) : (p.prefixUntil v h).edges ⊆ p.edges

Taking a prefix cannot introduce new edges.

theorem SimplePath.edges_suffixFrom_subset {α : Type u_1} [DecidableEq α] (p : SimplePath α) (v : α) (h : v ∈ p.vertices) : (p.suffixFrom v h).edges ⊆ p.edges

Taking a suffix cannot introduce new edges.

arcs

@[simp]

theorem SimplePath.length_arcs {α : Type u_1} (p : SimplePath α) : p.arcs.length = p.length

The number of traversed arcs equals the path's length.

theorem SimplePath.arcs_nodup {α : Type u_1} (p : SimplePath α) : p.arcs.Nodup

A path traverses each directed arc at most once.

@[simp]

theorem SimplePath.arcs_reverse {α : Type u_1} (p : SimplePath α) : p.reverse.arcs = List.map (fun (a : α × α) => (a.2, a.1)) p.arcs.reverse

Reversal reverses the arc list and swaps every arc's endpoints.

theorem SimplePath.arcs_dropTail_subset {α : Type u_1} (p : SimplePath α) : p.dropTail.arcs ⊆ p.arcs

Dropping the last vertex cannot introduce new arcs.

theorem SimplePath.arcs_dropHead_subset {α : Type u_1} (p : SimplePath α) : p.dropHead.arcs ⊆ p.arcs

Dropping the first vertex cannot introduce new arcs.

theorem SimplePath.arcs_prefixUntil_subset {α : Type u_1} [DecidableEq α] (p : SimplePath α) (v : α) (h : v ∈ p.vertices) : (p.prefixUntil v h).arcs ⊆ p.arcs

Taking a prefix cannot introduce new arcs.

theorem SimplePath.arcs_suffixFrom_subset {α : Type u_1} [DecidableEq α] (p : SimplePath α) (v : α) (h : v ∈ p.vertices) : (p.suffixFrom v h).arcs ⊆ p.arcs

Taking a suffix cannot introduce new arcs.