Hamiltonian walks

A Hamiltonian walk visits every vertex of a graph exactly once. A Hamiltonian path is open (head ≠ tail in a simple graph); a Hamiltonian cycle is closed and returns to its start vertex.

Main definitions

• Walk.IsHamiltonian G w — the walk w visits every vertex of G exactly once.
• Walk.IsHamiltonianCycle G w — Hamiltonian and closed.
• SimpleWalk.IsHamiltonian G w — analogue for simple walks.
• SimpleWalk.IsHamiltonianCycle G w — Hamiltonian and closed.

def Walk.IsHamiltonian {α : Type u_1} {ε : Type u_2} (G : AlgoLib.Graph α ε) (w : Walk α ε) : Prop

A walk is Hamiltonian in G when every vertex of G is visited exactly once.

Equations

• Walk.IsHamiltonian G w = ((∀ (v : α), v ∈ G.vertexSet ↔ v ∈ w) ∧ w.toVertexList.Nodup)

def Walk.IsHamiltonianCycle {α : Type u_1} {ε : Type u_2} (G : AlgoLib.Graph α ε) (w : Walk α ε) : Prop

A Hamiltonian cycle is a Hamiltonian walk whose endpoints coincide. The closing return-edge means the interior — the walk with its last vertex dropped — is the part that visits every vertex exactly once.

Equations

• Walk.IsHamiltonianCycle G w = (Walk.IsHamiltonian G w.dropTail ∧ w.closed ∧ 3 ≤ w.length)

def SimpleWalk.IsHamiltonian {α : Type u_1} (G : AlgoLib.SimpleGraph α) (w : SimpleWalk α) : Prop

A simple walk is Hamiltonian in G when every vertex of G is visited exactly once.

Equations

• SimpleWalk.IsHamiltonian G w = ((∀ (v : α), v ∈ G.vertexSet ↔ v ∈ w.val) ∧ w.val.nodup)

def SimpleWalk.IsHamiltonianCycle {α : Type u_1} (G : AlgoLib.SimpleGraph α) (w : SimpleWalk α) : Prop

A Hamiltonian cycle is a closed simple walk whose interior visits every vertex of G exactly once.

Equations

• SimpleWalk.IsHamiltonianCycle G w = ((∀ (v : α), v ∈ G.vertexSet ↔ v ∈ w.val) ∧ w.val.dropTail.nodup ∧ w.val.closed ∧ 3 ≤ w.val.length)