inductive Hex.GraphIso.Nauty.Sparse.Walk {n : Nat} (G : SparseGraph n) (root : Fin n) : Fin n → Nat → Prop

A walk of a specified length in the native sparse graph.

• nil {n : Nat} {G : SparseGraph n} {root : Fin n} : Walk G root root 0
• step {n : Nat} {G : SparseGraph n} {root u v : Fin n} {length : Nat} : Walk G root u length → G.adj u v = true → Walk G root v (length + 1)

theorem Hex.GraphIso.Nauty.Sparse.Walk.map {n : Nat} {G H : SparseGraph n} {root v : Fin n} {length : Nat} (f : Fin n → Fin n) (ha : ∀ (u v : Fin n), G.adj u v = true → H.adj (f u) (f v) = true) (h : Walk G root v length) : Walk H (f root) (f v) length

theorem Hex.GraphIso.Nauty.Sparse.Walk.relabel {n : Nat} {G : SparseGraph n} {root v : Fin n} {length : Nat} (p : Perm n) : Walk (G.relabel p) root v length ↔ Walk G (p.get root) (p.get v) length

structure Hex.GraphIso.Nauty.Sparse.Distances {n : Nat} (G : SparseGraph n) (root : Fin n) (dist : Array Nat) : Prop

Shortest-path values with n representing exactly the unreachable vertices. This contract includes both an attaining walk and minimality.

• size_eq : dist.size = n
• bound (v : Fin n) : dist[↑v]! ≤ n
• sound (v : Fin n) : dist[↑v]! < n → Walk G root v dist[↑v]!
• complete {v : Fin n} {length : Nat} : Walk G root v length → dist[↑v]! < n ∧ dist[↑v]! ≤ length

theorem Hex.GraphIso.Nauty.Sparse.Distances.root_eq {n : Nat} {G : SparseGraph n} {root : Fin n} {dist : Array Nat} (h : Distances G root dist) : dist[↑root]! = 0

theorem Hex.GraphIso.Nauty.Sparse.Distances.unreachable {n : Nat} {G : SparseGraph n} {root v : Fin n} {dist : Array Nat} (h : Distances G root dist) : dist[↑v]! = n ↔ ¬∃ (length : Nat), Walk G root v length

theorem Hex.GraphIso.Nauty.Sparse.Distances.unique {n : Nat} {G : SparseGraph n} {root : Fin n} {a b : Array Nat} (ha : Distances G root a) (hb : Distances G root b) : a = b

theorem Hex.GraphIso.Nauty.Sparse.Distances.of_edges {n : Nat} {G : SparseGraph n} {root : Fin n} {dist : Array Nat} (hsize : dist.size = n) (hbound : ∀ (v : Fin n), dist[↑v]! ≤ n) (hroot : dist[↑root]! = 0) (hsound : ∀ (v : Fin n), dist[↑v]! < n → Walk G root v dist[↑v]!) (hedge : ∀ (u v : Fin n), dist[↑u]! < n → G.adj u v = true → dist[↑v]! < n ∧ dist[↑v]! ≤ dist[↑u]! + 1) : Distances G root dist

The final BFS obligations imply shortest paths: discovered vertices have attaining walks and are closed under adjacency, and each edge increases the assigned value by at most one.