Migrate breadth-first search into AlgoLib

[nnhjy]

Add a layer-by-layer BFS on SimpleDiGraph (Algorithms/Graph/Traversal/BFS) with a full correctness proof: it computes reachability and the distance, and its layers are the spheres around the source. Add the directed reachability and distance specifications (Theory/Graph/Connectivity/Directed), the symmetric orientation SimpleGraph.toSimpleDiGraph with transfer lemmas, and define SimpleGraph.dist through it.

The connectivity layer's ad-hoc reachability closure is replaced: reachableFinset is now the BFS of the symmetric orientation, so the library has one search. Public API of Computable.lean is preserved; computeDist is added.

Also: SimpleDiGraph counterparts in Decidable.lean (decidable adjacency, computeOutNeighborFinset), coe_computeNeighborFinset, SimpleWalk.length_glue, Traversal umbrella module, and blueprint chapters for traversal and connectivity.

Summary

Migrates the directed breadth-first search from the nnhjy-backup / bfs-alg-diGraph branch (GraphAlgorithms/.../BreadthFirstSearch.lean) into AlgoLib, rebuilt on the current VertexSeq / SimpleWalk / SimpleDiGraph.IsSimpleWalkIn stack, and uses it as the only search in the connectivity layer.

New modules

• AlgoLib/Algorithms/Graph/Traversal/BFS.lean — layer-by-layer BFS on SimpleDiGraph (bfsLayer, bfsVisited, bfsReachableFinset, bfsDist) with a full correctness proof: soundness, completeness, the termination bound (at most |V(G)| non-empty layers), mem_bfsReachableFinset_iff, mem_bfsLayer_iff_dist_eq (layer k is the sphere of radius k), bfsDist_eq_dist, and Decidable (G.Reachable u v) for digraphs. Kernel-evaluated decide smoke tests included.
• AlgoLib/Theory/Graph/Connectivity/Directed.lean — the specifications BFS is checked against: SimpleDiGraph.Reachable, SimpleDiGraph.dist (nested ⨅ over realized walks, same shape as girth / κ, with the infimum API, attainment and the triangle inequality), the symmetric orientation transfer lemmas, and SimpleGraph.dist defined through the symmetric orientation (with dist_comm).

Connectivity layer now uses BFS

Theory/Graph/Connectivity/Computable.lean's ad-hoc reachStep / reachStart closure is removed. reachableFinset is now defined as the BFS of G.toSimpleDiGraph; its public API (mem_reachableFinset_iff, coe_reachableFinset, the Decidable instances, …) and all existing decide tests are unchanged. computeDist / computeDist_eq added.

Supporting changes

• Theory/Graph/Basic.lean: SimpleGraph.toSimpleDiGraph (symmetric orientation; deliberately not a Coe). Adjacency.lean: adj_toSimpleDiGraph_iff.
• Theory/Graph/Decidable.lean: SimpleDiGraph counterparts (notation bridges, DecidableRel Adj, computeOutNeighborFinset), instances for toSimpleDiGraph, and the old TODO coe_computeNeighborFinset resolved.
• Structures/SimpleWalk.lean: length_glue.
• Algorithms/Graph/Traversal/Basic.lean is now an umbrella module; AlgoLib.lean imports the new modules.
• Blueprint chapters for Traversal and Connectivity filled in (\lean{} / \leanok).

Design notes

• Rounds are iterated a fixed |V(G)| times (Nat.iterate) rather than by well-founded recursion, so the definitions reduce and decide works — the same choice Computable.lean already made. The original termination argument survives as the theorem lt_card_of_nonempty_bfsLayer.
• State is (visited, frontier) with layers rather than an accumulated α → ℕ∞ map; the distance is read off the layers with Finset.minENat.
• Walks, not paths, in all specifications, matching the existing Reachable rationale.
• ⚠️ Theory/Graph/Connectivity/Computable.lean now imports Algorithms/Graph/Traversal/BFS.lean. No module cycle, but it is the first Theory → Algorithms edge; happy to restructure if strict layering is preferred.

Verification

Full lake build succeeds (3425 jobs), no sorry, no warnings in any touched file. GraphAlgorithms/ is untouched.

🤖 Generated with Claude Code

[Copilot]

🟡 Changes recommended

Address the repeated BFS recomputation, the Theory-to-Algorithms dependency, and the incorrect zero-layer blueprint statement.

Get a fresh assessment by requesting another Copilot review.

Pull request overview

Adds a verified directed BFS, graph distance specifications, and BFS-backed connectivity APIs.

Changes:

• Adds BFS layers, reachability, distance computation, and correctness proofs.
• Adds symmetric graph orientation and directed distance specifications.
• Replaces the connectivity closure with BFS and adds supporting APIs.

File summaries

File	Summary
blueprint/src/chapters/Theory/Graph/Connectivity/Basic.tex	Documents connectivity, orientation, and distance.
blueprint/src/chapters/Algorithms/Graph/Traversal/Basic.tex	Documents BFS definitions and proofs.
AlgoLib/Theory/Graph/Structures/SimpleWalk.lean	Adds length_glue.
AlgoLib/Theory/Graph/Decidable.lean	Adds directed decidability and neighbor finsets.
AlgoLib/Theory/Graph/Connectivity/Directed.lean	Defines directed distance and orientation transfer lemmas.
AlgoLib/Theory/Graph/Connectivity/Computable.lean	Uses BFS for connectivity and distance.
AlgoLib/Theory/Graph/Connectivity/Basic.lean	Exposes the connectivity modules.
AlgoLib/Theory/Graph/Basic.lean	Adds symmetric graph orientation.
AlgoLib/Theory/Graph/Adjacency.lean	Adds orientation adjacency equivalence.
AlgoLib/Algorithms/Graph/Traversal/BFS.lean	Implements and proves BFS correctness.
AlgoLib/Algorithms/Graph/Traversal/Basic.lean	Provides the traversal umbrella module.
AlgoLib.lean	Imports the new modules.

Review details

Suppressed comments (2)

AlgoLib/Theory/Graph/Connectivity/Computable.lean:8

• This import makes Theory.Graph.Connectivity.Computable depend on Algorithms.Graph.Traversal.BFS; the rest of the AlgoLib/Theory tree has no Theory→Algorithms imports. That reverses the repository's established layer direction and means importing the theory umbrella now pulls an algorithm module, while future algorithm code depending on the computable connectivity API can create cycles. Please keep the BFS/specification bridge in an algorithm-independent layer or move this executable wrapper out of Theory.

import AlgoLib.Algorithms.Graph.Traversal.BFS

blueprint/src/chapters/Algorithms/Graph/Traversal/Basic.tex:85

• This proof paragraph is false for k = 0: with natural-number subtraction, k - 1 = 0, while the source in L₀ has distance 0, not a distance greater than 0. Split off the zero-layer case and state the lower-bound argument only for k > 0, matching the separate zero case handled by the Lean proof.

  If $v \in L_k$ then $\dist(s, v) \le k$ by soundness, and $\dist(s, v) > k - 1$
  because a walk of length at most $k - 1$ would place $v$ in $V_{k-1}$, which $L_k$
  avoids by construction. Conversely, if $\dist(s, v) = k$ then a shortest walk places
  $v \in V_k$, so $v \in L_j$ for some $j \le k$, and the first part gives $j = k$.

• Files reviewed: 12/12 changed files
• Comments generated: 1
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.