structure Hex.GraphIso.Nauty.Sparse.Bfs {n : Nat} (G : SparseGraph n) (root : Fin n) (dist queue : Array Nat) (head tail : Nat) extends Hex.GraphIso.Nauty.Sparse.Queue n dist queue head tail : Prop

BFS queue invariants together with attaining walks and the completed rows' edge inequalities.

• dist_size : dist.size = n
• queue_size : queue.size = n
• head_le : head ≤ tail
• tail_le : tail ≤ n
• vertex (i : Nat) : i < tail → queue[i]! < n
• injective (i j : Nat) : i < tail → j < tail → queue[i]! = queue[j]! → i = j
• bound (v : Nat) : v < n → dist[v]! ≤ n
• found (v : Nat) : v < n → (dist[v]! < n ↔ ∃ (i : Nat), i < tail ∧ queue[i]! = v)
• index (i : Nat) : i < tail → dist[queue[i]!]! ≤ i
• sorted (i j : Nat) : i ≤ j → j < tail → dist[queue[i]!]! ≤ dist[queue[j]!]!
• band (i j : Nat) : head ≤ i → i < tail → j < tail → dist[queue[j]!]! ≤ dist[queue[i]!]! + 1
• root_eq : dist[↑root]! = 0
• sound (v : Nat) (hv : v < n) : dist[v]! < n → Walk G root ⟨v, hv⟩ dist[v]!
• edges (i : Nat) (hi : i < head) (v : Fin n) : G.adj ⟨queue[i]!, ⋯⟩ v = true → dist[↑v]! < n ∧ dist[↑v]! ≤ dist[queue[i]!]! + 1

theorem Hex.GraphIso.Nauty.Sparse.Bfs.initial {n : Nat} (G : SparseGraph n) (root : Fin n) : Bfs G root ((Array.replicate n n).set! (↑root) 0) ((Array.replicate n 0).set! 0 ↑root) 0 1

theorem Hex.GraphIso.Nauty.Sparse.Bfs.add {n : Nat} {G : SparseGraph n} {root : Fin n} {dist queue : Array Nat} {head tail : Nat} (h : Bfs G root dist queue head tail) (hh : head < tail) (v : Fin n) (hd : dist[↑v]! = n) (hn : dist[queue[head]!]! + 1 < n) (ha : G.adj ⟨queue[head]!, ⋯⟩ v = true) : Bfs G root (dist.set! (↑v) (dist[queue[head]!]! + 1)) (queue.set! tail ↑v) head (tail + 1)

theorem Hex.GraphIso.Nauty.Sparse.Bfs.advance {n : Nat} {G : SparseGraph n} {root : Fin n} {dist queue : Array Nat} {head tail : Nat} (h : Bfs G root dist queue head tail) (hh : head < tail) (he : ∀ (v : Fin n), G.adj ⟨queue[head]!, ⋯⟩ v = true → dist[↑v]! < n ∧ dist[↑v]! ≤ dist[queue[head]!]! + 1) : Bfs G root dist queue (head + 1) tail

theorem Hex.GraphIso.Nauty.Sparse.Bfs.complete {n : Nat} {G : SparseGraph n} {root : Fin n} {dist queue : Array Nat} {head tail : Nat} (h : Bfs G root dist queue head tail) (hdone : n ≤ tail ∨ tail ≤ head) : Distances G root dist

Both executable stopping conditions produce shortest paths. If the queue is full, its distance band covers the unprocessed rows as well.