From e5947b30160d80723e06d5fba39a69c88c0c0a44 Mon Sep 17 00:00:00 2001 From: nnhjy <43530784+nnhjy@users.noreply.github.com> Date: Thu, 17 Sep 2026 18:08:04 +0200 Subject: [PATCH 1/2] Migrate breadth-first search into AlgoLib 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. Co-Authored-By: Claude Fable 5.1 --- AlgoLib.lean | 2 + AlgoLib/Algorithms/Graph/Traversal/BFS.lean | 462 ++++++++++++++++++ AlgoLib/Algorithms/Graph/Traversal/Basic.lean | 25 + AlgoLib/Theory/Graph/Adjacency.lean | 5 + AlgoLib/Theory/Graph/Basic.lean | 34 ++ AlgoLib/Theory/Graph/Connectivity/Basic.lean | 21 +- .../Theory/Graph/Connectivity/Computable.lean | 169 +++---- .../Theory/Graph/Connectivity/Directed.lean | 258 ++++++++++ AlgoLib/Theory/Graph/Decidable.lean | 108 +++- .../Theory/Graph/Structures/SimpleWalk.lean | 10 + .../Algorithms/Graph/Traversal/Basic.tex | 101 +++- .../Theory/Graph/Connectivity/Basic.tex | 34 ++ 12 files changed, 1105 insertions(+), 124 deletions(-) create mode 100644 AlgoLib/Algorithms/Graph/Traversal/BFS.lean create mode 100644 AlgoLib/Theory/Graph/Connectivity/Directed.lean diff --git a/AlgoLib.lean b/AlgoLib.lean index e2fea55..a708cdc 100644 --- a/AlgoLib.lean +++ b/AlgoLib.lean @@ -8,6 +8,7 @@ import AlgoLib.Theory.Graph.Connectivity.Components import AlgoLib.Theory.Graph.Connectivity.Computable import AlgoLib.Theory.Graph.Connectivity.Connectivity import AlgoLib.Theory.Graph.Connectivity.Cuts +import AlgoLib.Theory.Graph.Connectivity.Directed import AlgoLib.Theory.Graph.Connectivity.Reachable import AlgoLib.Theory.Graph.Decidable import AlgoLib.Theory.Graph.Degree @@ -68,6 +69,7 @@ import AlgoLib.Algorithms.Graph.MST.Basic import AlgoLib.Algorithms.Graph.SCC.Basic import AlgoLib.Algorithms.Graph.Search.Basic import AlgoLib.Algorithms.Graph.ShortestPath.Basic +import AlgoLib.Algorithms.Graph.Traversal.BFS import AlgoLib.Algorithms.Graph.Traversal.Basic -- Data structures diff --git a/AlgoLib/Algorithms/Graph/Traversal/BFS.lean b/AlgoLib/Algorithms/Graph/Traversal/BFS.lean new file mode 100644 index 0000000..c555069 --- /dev/null +++ b/AlgoLib/Algorithms/Graph/Traversal/BFS.lean @@ -0,0 +1,462 @@ +/- +Copyright (c) 2026 AlgoLib working group. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Huang.JiangYi (co/ Claude Fable 5.1) +-/ +import AlgoLib.Theory.Graph.Decidable +import AlgoLib.Theory.Graph.Connectivity.Directed +import AlgoLib.Util.Finset + +/-! +# Breadth-first search + +Breadth-first search (BFS) from a source vertex `s` of a simple directed graph `G` +explores the graph *layer by layer*: the layer `L₀ = {s}` is the source, and the layer +`Lₖ₊₁` consists of the out-neighbours of `Lₖ` that lie in no earlier layer. The layers +are the *spheres* around `s`: `Lₖ` is exactly the set of vertices at distance `k` from +`s`, and their union is the set of vertices reachable from `s`. + +This file defines the search on a graph whose vertex set is finite as data and whose +arcs have decidable membership, and proves it correct against the specifications +`SimpleDiGraph.Reachable` and `SimpleDiGraph.dist` of +`AlgoLib.Theory.Graph.Connectivity.Directed`. + +## Main definitions + +* `SimpleDiGraph.BFSState` — the state of the search: the vertices `visited` so far and + the current `frontier`, i.e. the most recent layer. +* `SimpleDiGraph.bfsStep G` — one round: expand the frontier to its unvisited + out-neighbours. +* `SimpleDiGraph.bfsRun G s k` — the state after `k` rounds from `s`; + `SimpleDiGraph.bfsLayer G s k` and `SimpleDiGraph.bfsVisited G s k` are its two + components. +* `SimpleDiGraph.bfsReachableFinset G s` — the vertices reachable from `s`: the visited + set after `|V(G)|` rounds. +* `SimpleDiGraph.bfsDist G s v` — the distance from `s` to `v`: the index of the layer + containing `v`, or `⊤` if there is none. + +## Main results + +* `SimpleDiGraph.exists_walk_of_mem_bfsLayer` — *soundness*: a vertex of layer `k` is the + endpoint of a walk of length `k` from `s`. +* `SimpleDiGraph.mem_bfsVisited_of_isVertexSeqIn` — *completeness*: the endpoint of a + walk of length `ℓ` from `s` is visited after `ℓ` rounds. +* `SimpleDiGraph.lt_card_of_nonempty_bfsLayer` — *termination*: at most `|V(G)|` layers + are non-empty, because the layers are pairwise disjoint subsets of `V(G)`. +* `SimpleDiGraph.mem_bfsReachableFinset_iff` — BFS computes reachability. +* `SimpleDiGraph.mem_bfsLayer_iff_dist_eq` — the `k`-th layer is the sphere of radius `k`. +* `SimpleDiGraph.bfsDist_eq_dist` — BFS computes the distance. +* `SimpleDiGraph.instDecidableReachable` — reachability in a finite directed graph is + decidable. + +## Design choices + +* **Rounds by `Nat.iterate`, not well-founded recursion.** A recursive BFS whose + termination rests on the measure `|V(G) \ visited|` is irreducible to the kernel, so + `decide` cannot evaluate it. Iterating one round a fixed number of times is + structurally recursive, hence reduces, and `|V(G)|` rounds always suffice: each + non-empty layer contains a vertex no earlier layer does, so there are at most `|V(G)|` + of them. The termination *argument* of the recursive formulation survives as the + theorem `lt_card_of_nonempty_bfsLayer`, where it belongs. +* **Layers, not a distance map.** The state is the pair (visited, frontier) rather than + a partial function `α → ℕ∞`: the frontier *is* the current sphere, so the level + invariant "every frontier vertex is at distance `k`" is a statement about a `Finset` + and needs no bookkeeping over an accumulated map. The distance is read off afterwards + as the least layer index containing the vertex, using `Finset.minENat` from + `AlgoLib.Util.Finset` — the same device that makes the connectivity numbers compute. +* **Walks, not paths, in the correctness statements**, matching `dist`. Soundness builds + a walk by appending one arc per round; completeness inducts on the `IsVertexSeqIn` + derivation of an arbitrary walk, so no cycle erasure is ever needed. +* **The source is guarded.** `bfsStart G s` is `{s}` when `s` is a vertex of `G` and `∅` + otherwise, so every statement below holds with no hypothesis on `s`: nothing outside + `V(G)` reaches anything, and `Reachable s s ↔ s ∈ V(G)` is reproduced exactly. +-/ + +namespace AlgoLib + +variable {α : Type*} + +open scoped AlgoLib + +namespace SimpleDiGraph + +/-! ## The search -/ + +/-- The state of a breadth-first search: the set of vertices discovered so far, and the +*frontier* — the vertices discovered in the most recent round, whose out-neighbours are +explored next. The frontier is always contained in the visited set. -/ +structure BFSState (α : Type*) where + /-- All vertices discovered so far. -/ + visited : Finset α + /-- The vertices discovered in the last round: the current layer. -/ + frontier : Finset α + +/-- The next layer: the out-neighbours of the frontier that have not been visited. -/ +def bfsNext (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] (S : BFSState α) : Finset α := + S.frontier.biUnion G.computeOutNeighborFinset \ S.visited + +/-- One round of breadth-first search: the next layer is discovered, and becomes the new +frontier. -/ +def bfsStep (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] (S : BFSState α) : BFSState α := + ⟨S.visited ∪ G.bfsNext S, G.bfsNext S⟩ + +/-- The initial state of the search from `s`: the single layer `{s}` if `s` is a vertex +of `G`, and the empty search otherwise. -/ +def bfsStart (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertexSet] (s : α) : + BFSState α := + if s ∈ G.computeVertexFinset then ⟨{s}, {s}⟩ else ⟨∅, ∅⟩ + +/-- The state of the search from `s` after `k` rounds. -/ +def bfsRun (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] (s : α) (k : ℕ) : BFSState α := + (G.bfsStep)^[k] (G.bfsStart s) + +/-- The `k`-th *layer* of the search from `s`: the frontier after `k` rounds. By +`mem_bfsLayer_iff_dist_eq` this is the set of vertices at distance exactly `k` from `s`. -/ +def bfsLayer (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] (s : α) (k : ℕ) : Finset α := + (G.bfsRun s k).frontier + +/-- The vertices visited within `k` rounds of the search from `s`: the union of the layers +`0, …, k` (see `mem_bfsVisited_iff`), i.e. the vertices at distance at most `k`. -/ +def bfsVisited (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] (s : α) (k : ℕ) : Finset α := + (G.bfsRun s k).visited + +/-- The vertices reachable from `s`, computed by breadth-first search: the visited set +after `|V(G)|` rounds, by which time every layer has been exhausted +(`lt_card_of_nonempty_bfsLayer`). -/ +def bfsReachableFinset (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] (s : α) : Finset α := + G.bfsVisited s G.computeVertexFinset.card + +/-- The distance from `s` to `v`, computed by breadth-first search: the least index of a +layer containing `v`, and `⊤` if no layer does. Only the indices below `|V(G)|` need to be +inspected, since no later layer is non-empty. -/ +def bfsDist (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] (s v : α) : ℕ∞ := + ((Finset.range G.computeVertexFinset.card).filter fun k => v ∈ G.bfsLayer s k).minENat + +variable {G : SimpleDiGraph α} [DecidableEq α] [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] {s v : α} + +/-! ## Unfolding the rounds -/ + +lemma mem_bfsNext {S : BFSState α} : + v ∈ G.bfsNext S ↔ (∃ u ∈ S.frontier, G.Adj u v) ∧ v ∉ S.visited := by + simp [bfsNext] + +@[simp] lemma bfsRun_zero : G.bfsRun s 0 = G.bfsStart s := rfl + +lemma bfsRun_succ (k : ℕ) : G.bfsRun s (k + 1) = G.bfsStep (G.bfsRun s k) := + Function.iterate_succ_apply' _ _ _ + +/-- The zeroth layer is the source, provided it is a vertex. -/ +lemma mem_bfsLayer_zero : v ∈ G.bfsLayer s 0 ↔ v = s ∧ s ∈ V(G) := by + unfold bfsLayer bfsRun bfsStart + split_ifs with h <;> simp_all + +/-- Initially only the source is visited, provided it is a vertex. -/ +lemma mem_bfsVisited_zero : v ∈ G.bfsVisited s 0 ↔ v = s ∧ s ∈ V(G) := by + unfold bfsVisited bfsRun bfsStart + split_ifs with h <;> simp_all + +/-- The `(k + 1)`-st layer: unvisited out-neighbours of the `k`-th layer. -/ +lemma mem_bfsLayer_succ (k : ℕ) : + v ∈ G.bfsLayer s (k + 1) ↔ (∃ u ∈ G.bfsLayer s k, G.Adj u v) ∧ v ∉ G.bfsVisited s k := by + rw [bfsLayer, bfsRun_succ] + exact mem_bfsNext + +/-- After `k + 1` rounds, the visited set has grown by exactly the `(k + 1)`-st layer. -/ +lemma bfsVisited_succ (k : ℕ) : + G.bfsVisited s (k + 1) = G.bfsVisited s k ∪ G.bfsLayer s (k + 1) := by + rw [bfsVisited, bfsLayer, bfsRun_succ] + rfl + +/-! ## Invariants of the search -/ + +/-- The frontier is part of the visited set. -/ +lemma bfsLayer_subset_bfsVisited (k : ℕ) : G.bfsLayer s k ⊆ G.bfsVisited s k := by + cases k with + | zero => intro v hv; rw [mem_bfsVisited_zero]; exact mem_bfsLayer_zero.1 hv + | succ k => rw [bfsVisited_succ]; exact Finset.subset_union_right + +/-- The visited set only grows. -/ +lemma bfsVisited_subset_succ (k : ℕ) : G.bfsVisited s k ⊆ G.bfsVisited s (k + 1) := by + rw [bfsVisited_succ]; exact Finset.subset_union_left + +/-- The visited set is monotone in the number of rounds. -/ +lemma bfsVisited_mono {j k : ℕ} (h : j ≤ k) : G.bfsVisited s j ⊆ G.bfsVisited s k := by + induction h with + | refl => exact subset_rfl + | step _ ih => exact ih.trans (bfsVisited_subset_succ _) + +/-- A new layer is disjoint from everything visited before it. -/ +lemma disjoint_bfsLayer_succ_bfsVisited (k : ℕ) : + Disjoint (G.bfsLayer s (k + 1)) (G.bfsVisited s k) := by + rw [bfsLayer, bfsRun_succ] + exact Finset.sdiff_disjoint + +/-- Only vertices of `G` are ever visited. -/ +lemma bfsVisited_subset_computeVertexFinset (k : ℕ) : + G.bfsVisited s k ⊆ G.computeVertexFinset := by + induction k with + | zero => + intro v hv + obtain ⟨rfl, hs⟩ := mem_bfsVisited_zero.1 hv + simpa using hs + | succ k ih => + rw [bfsVisited_succ] + refine Finset.union_subset ih fun v hv => ?_ + obtain ⟨⟨u, -, hadj⟩, -⟩ := (mem_bfsLayer_succ k).1 hv + simpa using hadj.right_mem + +/-- The visited set after `k` rounds is the union of the first `k + 1` layers. -/ +lemma mem_bfsVisited_iff (k : ℕ) : v ∈ G.bfsVisited s k ↔ ∃ j ≤ k, v ∈ G.bfsLayer s j := by + induction k with + | zero => + rw [mem_bfsVisited_zero] + refine ⟨fun h => ⟨0, le_rfl, mem_bfsLayer_zero.2 h⟩, ?_⟩ + rintro ⟨j, hj, hv⟩ + rw [Nat.le_zero.1 hj] at hv + exact mem_bfsLayer_zero.1 hv + | succ k ih => + rw [bfsVisited_succ, Finset.mem_union, ih] + constructor + · rintro (⟨j, hj, hv⟩ | hv) + · exact ⟨j, hj.trans (Nat.le_succ k), hv⟩ + · exact ⟨k + 1, le_rfl, hv⟩ + · rintro ⟨j, hj, hv⟩ + rcases Nat.lt_or_ge j (k + 1) with hlt | hge + · exact Or.inl ⟨j, Nat.lt_succ_iff.1 hlt, hv⟩ + · exact Or.inr (le_antisymm hj hge ▸ hv) + +/-! ## Soundness: every layer vertex is the end of a walk of that length -/ + +/-- A vertex of the `k`-th layer is the endpoint of a walk of length `k` from `s`. -/ +theorem exists_walk_of_mem_bfsLayer {k : ℕ} (hv : v ∈ G.bfsLayer s k) : + ∃ w : SimpleWalk α, G.IsSimpleWalkIn w ∧ w.head = s ∧ w.tail = v ∧ w.length = k := by + induction k generalizing v with + | zero => + obtain ⟨rfl, hs⟩ := mem_bfsLayer_zero.1 hv + exact ⟨(SimplePath.singleton v).val, IsVertexSeqIn.singleton v hs, rfl, rfl, rfl⟩ + | succ k ih => + obtain ⟨⟨u, hu, hadj⟩, -⟩ := (mem_bfsLayer_succ k).1 hv + obtain ⟨w, hw, hhead, htail, hlen⟩ := ih hu + have htail' : w.val.tail = u := htail + have hlen' : w.val.length = k := hlen + have hne : w.val.tail ≠ v := by rw [htail']; exact hadj.ne + refine ⟨⟨w.val.cons v, ⟨w.nonstalling, hne⟩⟩, ?_, hhead, rfl, ?_⟩ + · exact IsVertexSeqIn.cons w.val v hw (by rw [htail']; exact hadj) + · change 1 + w.val.length = k + 1 + omega + +/-- Every visited vertex is reachable from the source. -/ +theorem reachable_of_mem_bfsVisited {k : ℕ} (hv : v ∈ G.bfsVisited s k) : + G.Reachable s v := by + obtain ⟨j, -, hj⟩ := (mem_bfsVisited_iff k).1 hv + obtain ⟨w, hw, hhead, htail, -⟩ := exists_walk_of_mem_bfsLayer hj + exact ⟨w, hw, hhead, htail⟩ + +/-! ## Completeness: the end of a walk of length `ℓ` is visited within `ℓ` rounds -/ + +/-- The out-neighbours of a visited vertex are visited one round later. -/ +lemma mem_bfsVisited_succ_of_adj {u : α} {k : ℕ} (hu : u ∈ G.bfsVisited s k) + (hadj : G.Adj u v) : v ∈ G.bfsVisited s (k + 1) := by + induction k generalizing u with + | zero => + rw [bfsVisited_succ, Finset.mem_union] + by_cases hv : v ∈ G.bfsVisited s 0 + · exact Or.inl hv + · exact Or.inr ((mem_bfsLayer_succ 0).2 + ⟨⟨u, mem_bfsLayer_zero.2 (mem_bfsVisited_zero.1 hu), hadj⟩, hv⟩) + | succ k ih => + rw [bfsVisited_succ, Finset.mem_union] at hu + rcases hu with hu | hu + · exact bfsVisited_subset_succ (k + 1) (ih hu hadj) + · rw [bfsVisited_succ, Finset.mem_union] + by_cases hv : v ∈ G.bfsVisited s (k + 1) + · exact Or.inl hv + · exact Or.inr ((mem_bfsLayer_succ (k + 1)).2 ⟨⟨u, hu, hadj⟩, hv⟩) + +/-- The endpoint of a realized vertex sequence of length `ℓ` starting at `s` is visited +within `ℓ` rounds. -/ +theorem mem_bfsVisited_of_isVertexSeqIn {w : VertexSeq α} (hw : G.IsVertexSeqIn w) + (hhead : w.head = s) : w.tail ∈ G.bfsVisited s w.length := by + induction hw with + | singleton x hx => + rw [VertexSeq.head_singleton] at hhead + subst hhead + exact mem_bfsVisited_zero.2 ⟨rfl, hx⟩ + | cons w u hw hadj ih => + rw [VertexSeq.head_cons] at hhead + rw [VertexSeq.tail_cons, VertexSeq.length, Nat.add_comm] + exact mem_bfsVisited_succ_of_adj (ih hhead) hadj + +/-! ## Termination: at most `|V(G)|` layers are non-empty -/ + +/-- Once a layer is empty, so is the next. -/ +lemma bfsLayer_succ_eq_empty {k : ℕ} (h : G.bfsLayer s k = ∅) : + G.bfsLayer s (k + 1) = ∅ := + Finset.eq_empty_of_forall_notMem fun v hv => by + obtain ⟨⟨u, hu, -⟩, -⟩ := (mem_bfsLayer_succ k).1 hv + simp [h] at hu + +/-- A non-empty layer is preceded by a non-empty layer. -/ +lemma nonempty_bfsLayer_of_succ {k : ℕ} (h : (G.bfsLayer s (k + 1)).Nonempty) : + (G.bfsLayer s k).Nonempty := by + by_contra hcon + rw [Finset.not_nonempty_iff_eq_empty] at hcon + exact h.ne_empty (bfsLayer_succ_eq_empty hcon) + +/-- If the `k`-th layer is non-empty then at least `k + 1` vertices have been visited: +each of the layers `0, …, k` contributed a new one. -/ +lemma succ_le_card_bfsVisited {k : ℕ} (h : (G.bfsLayer s k).Nonempty) : + k + 1 ≤ (G.bfsVisited s k).card := by + induction k with + | zero => exact Finset.card_pos.2 (h.mono (bfsLayer_subset_bfsVisited 0)) + | succ k ih => + have hk := ih (nonempty_bfsLayer_of_succ h) + have hpos := Finset.card_pos.2 h + rw [bfsVisited_succ, Finset.card_union_of_disjoint (disjoint_bfsLayer_succ_bfsVisited k).symm] + omega + +/-- The termination bound: a non-empty layer has index below `|V(G)|`. -/ +theorem lt_card_of_nonempty_bfsLayer {k : ℕ} (h : (G.bfsLayer s k).Nonempty) : + k < G.computeVertexFinset.card := + Nat.lt_of_lt_of_le (Nat.lt_succ_self k) + ((succ_le_card_bfsVisited h).trans + (Finset.card_le_card (bfsVisited_subset_computeVertexFinset k))) + +/-- Every visited vertex lies in a layer of index below `|V(G)|`. -/ +lemma exists_bfsLayer_lt_card_of_mem_bfsVisited {k : ℕ} (hv : v ∈ G.bfsVisited s k) : + ∃ j, j ≤ k ∧ j < G.computeVertexFinset.card ∧ v ∈ G.bfsLayer s j := by + obtain ⟨j, hj, hvj⟩ := (mem_bfsVisited_iff k).1 hv + exact ⟨j, hj, lt_card_of_nonempty_bfsLayer ⟨v, hvj⟩, hvj⟩ + +/-! ## Correctness -/ + +/-- **BFS computes reachability.** -/ +@[simp] theorem mem_bfsReachableFinset_iff : v ∈ G.bfsReachableFinset s ↔ G.Reachable s v := by + refine ⟨reachable_of_mem_bfsVisited, ?_⟩ + rintro ⟨w, hw, rfl, rfl⟩ + obtain ⟨j, -, hjlt, hvj⟩ := + exists_bfsLayer_lt_card_of_mem_bfsVisited (mem_bfsVisited_of_isVertexSeqIn hw rfl) + exact bfsVisited_mono hjlt.le (bfsLayer_subset_bfsVisited j hvj) + +/-- The reachable set, as a set, is the set of vertices reachable from `s`. -/ +lemma coe_bfsReachableFinset : + (G.bfsReachableFinset s : Set α) = {v | G.Reachable s v} := + Set.ext fun _ => by simp + +/-- Reachability in a finite simple directed graph is decidable, by breadth-first search. -/ +instance instDecidableReachable (u v : α) : Decidable (G.Reachable u v) := + decidable_of_iff _ mem_bfsReachableFinset_iff + +/-- A vertex of the `k`-th layer is at distance at most `k`, by soundness. -/ +lemma dist_le_of_mem_bfsLayer {k : ℕ} (hv : v ∈ G.bfsLayer s k) : G.dist s v ≤ k := by + obtain ⟨w, hw, hhead, htail, hlen⟩ := exists_walk_of_mem_bfsLayer hv + rw [← hlen] + exact dist_le_length hw hhead htail + +/-- A vertex of the `(k + 1)`-st layer is at distance more than `k`: by completeness, a +walk of length at most `k` would have had it visited within `k` rounds, but a new layer +avoids everything visited before it. -/ +lemma lt_dist_of_mem_bfsLayer_succ {k : ℕ} (hv : v ∈ G.bfsLayer s (k + 1)) : + (k : ℕ∞) < G.dist s v := by + obtain ⟨-, hnot⟩ := (mem_bfsLayer_succ k).1 hv + rw [← not_le] + intro hle + have hr : G.Reachable s v := + reachable_iff_dist_ne_top.2 (ne_top_of_le_ne_top (ENat.coe_ne_top k) hle) + obtain ⟨w, hw, hhead, htail, hlen⟩ := dist_exists hr + rw [← hlen, Nat.cast_le] at hle + have htail' : w.val.tail = v := htail + have hvis := mem_bfsVisited_of_isVertexSeqIn hw hhead + rw [htail'] at hvis + exact hnot (bfsVisited_mono hle hvis) + +/-- A vertex of the `k`-th layer is at distance exactly `k`. -/ +theorem dist_eq_of_mem_bfsLayer {k : ℕ} (hv : v ∈ G.bfsLayer s k) : G.dist s v = k := by + refine le_antisymm (dist_le_of_mem_bfsLayer hv) ?_ + cases k with + | zero => exact zero_le + | succ k => + rw [Nat.cast_succ] + exact (ENat.add_one_le_iff (ENat.coe_ne_top k)).2 (lt_dist_of_mem_bfsLayer_succ hv) + +/-- **The layers are the spheres.** The `k`-th layer of the search from `s` is exactly the +set of vertices at distance `k` from `s`. -/ +theorem mem_bfsLayer_iff_dist_eq (k : ℕ) : v ∈ G.bfsLayer s k ↔ G.dist s v = k := by + refine ⟨dist_eq_of_mem_bfsLayer, fun hd => ?_⟩ + have hr : G.Reachable s v := reachable_iff_dist_ne_top.2 (by rw [hd]; exact ENat.coe_ne_top k) + obtain ⟨w, hw, hhead, htail, -⟩ := dist_exists hr + have htail' : w.val.tail = v := htail + have hvis := mem_bfsVisited_of_isVertexSeqIn hw hhead + rw [htail'] at hvis + obtain ⟨j, -, hvj⟩ := (mem_bfsVisited_iff _).1 hvis + have hjk : j = k := by exact_mod_cast (dist_eq_of_mem_bfsLayer hvj).symm.trans hd + exact hjk ▸ hvj + +/-- **BFS computes the distance.** -/ +theorem bfsDist_eq_dist : G.bfsDist s v = G.dist s v := by + refine le_antisymm (le_dist_iff.2 fun w hw hhead htail => ?_) (Finset.le_minENat_iff.2 ?_) + · have htail' : w.val.tail = v := htail + have hvis := mem_bfsVisited_of_isVertexSeqIn hw hhead + rw [htail'] at hvis + obtain ⟨j, hj, hjlt, hvj⟩ := exists_bfsLayer_lt_card_of_mem_bfsVisited hvis + calc G.bfsDist s v ≤ (j : ℕ∞) := + Finset.minENat_le (Finset.mem_filter.2 ⟨Finset.mem_range.2 hjlt, hvj⟩) + _ ≤ (w.length : ℕ∞) := by exact_mod_cast hj + · intro k hk + exact dist_le_of_mem_bfsLayer (Finset.mem_filter.1 hk).2 + +/-- The distance is infinite exactly when BFS never reaches the vertex. -/ +theorem bfsDist_eq_top_iff : G.bfsDist s v = ⊤ ↔ v ∉ G.bfsReachableFinset s := by + rw [bfsDist_eq_dist, dist_eq_top_iff, mem_bfsReachableFinset_iff] + +/-! ## Smoke tests + +Concrete evaluation on a small directed graph, confirming that the search really reduces +in the kernel. As in `AlgoLib.Theory.Graph.Connectivity.Computable`, the `Fintype` and +`DecidablePred` instances of a concrete graph have to be given by hand. -/ + +section Examples + +/-- The directed path `0 → 1 → 2`, with the arc `2 → 0` closing a cycle, and an isolated +vertex `3`. -/ +private def cycleG : SimpleDiGraph (Fin 4) where + vertexSet := {0, 1, 2, 3} + edgeSet := {(0, 1), (1, 2), (2, 0)} + incidence' := by decide + loopless' := by decide + +private instance : Fintype cycleG.vertexSet := + inferInstanceAs (Fintype ({0, 1, 2, 3} : Set (Fin 4))) + +private instance : DecidablePred (· ∈ cycleG.edgeSet) := + inferInstanceAs (DecidablePred (· ∈ ({(0, 1), (1, 2), (2, 0)} : Set (Fin 4 × Fin 4)))) + +example : cycleG.bfsLayer 0 0 = {0} := by decide +example : cycleG.bfsLayer 0 1 = {1} := by decide +example : cycleG.bfsLayer 0 2 = {2} := by decide +example : cycleG.bfsLayer 0 3 = ∅ := by decide +example : cycleG.bfsReachableFinset 0 = {0, 1, 2} := by decide +example : cycleG.bfsReachableFinset 3 = {3} := by decide +example : cycleG.bfsDist 0 2 = 2 := by decide +example : cycleG.bfsDist 2 1 = 2 := by decide +example : cycleG.bfsDist 0 3 = ⊤ := by decide +example : cycleG.Reachable 1 0 := by decide +example : ¬ cycleG.Reachable 0 3 := by decide + +-- …and therefore `dist 0 2 = 2`, through the agreement theorem. +example : cycleG.dist 0 2 = 2 := by + rw [← bfsDist_eq_dist]; decide + +end Examples + +end SimpleDiGraph + +end AlgoLib diff --git a/AlgoLib/Algorithms/Graph/Traversal/Basic.lean b/AlgoLib/Algorithms/Graph/Traversal/Basic.lean index 8b13789..9444925 100644 --- a/AlgoLib/Algorithms/Graph/Traversal/Basic.lean +++ b/AlgoLib/Algorithms/Graph/Traversal/Basic.lean @@ -1 +1,26 @@ +/- +Copyright (c) 2026 AlgoLib working group. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Huang.JiangYi (co/ Claude Fable 5.1) +-/ +import AlgoLib.Algorithms.Graph.Traversal.BFS +/-! +# `AlgoLib.Algorithms.Graph.Traversal` + +Graph traversal algorithms: systematic exploration of the vertices reachable from a +source. This file defines nothing itself: it is an *umbrella* module that re-exports the +development, which is split across `AlgoLib/Algorithms/Graph/Traversal/`: + +* `BFS` — breadth-first search on a `SimpleDiGraph`, layer by layer, with the proofs + that it computes reachability (`SimpleDiGraph.mem_bfsReachableFinset_iff`) and the + distance (`SimpleDiGraph.bfsDist_eq_dist`), and that its layers are the spheres around + the source (`SimpleDiGraph.mem_bfsLayer_iff_dist_eq`). + +Undirected graphs are traversed through their symmetric orientation +`SimpleGraph.toSimpleDiGraph`; the undirected wrappers `SimpleGraph.reachableFinset` and +`SimpleGraph.computeDist` live in `AlgoLib.Theory.Graph.Connectivity.Computable`, next to +the specifications they compute. + +Depth-first search is not yet implemented. +-/ diff --git a/AlgoLib/Theory/Graph/Adjacency.lean b/AlgoLib/Theory/Graph/Adjacency.lean index 59bdd0e..b84aff5 100644 --- a/AlgoLib/Theory/Graph/Adjacency.lean +++ b/AlgoLib/Theory/Graph/Adjacency.lean @@ -81,6 +81,11 @@ some edge points from `u` to `v`. A loop at `v` is a self-arc. -/ @[grind] def SimpleDiGraph.Adj (G : SimpleDiGraph α) (u v : α) : Prop := (u, v) ∈ E(G) +/-- Adjacency in the symmetric orientation of a simple graph is adjacency in the graph: +there is an arc from `u` to `v` exactly when `s(u, v)` is an edge. -/ +@[simp] lemma SimpleGraph.adj_toSimpleDiGraph_iff (G : SimpleGraph α) {u v : α} : + G.toSimpleDiGraph.Adj u v ↔ G.Adj u v := Iff.rfl + /-! ## Symmetry (undirected types) -/ /-- Adjacency in a multigraph is symmetric. -/ diff --git a/AlgoLib/Theory/Graph/Basic.lean b/AlgoLib/Theory/Graph/Basic.lean index 2b7d9be..9200175 100644 --- a/AlgoLib/Theory/Graph/Basic.lean +++ b/AlgoLib/Theory/Graph/Basic.lean @@ -51,6 +51,14 @@ preferred API restates these in terms of `V(G)` and `E(G)`: * `SimpleDiGraph.toDiGraph`: forget the looplessness axiom of a simple directed graph. The corresponding `Coe` instances are registered. + +## Symmetric orientation + +* `SimpleGraph.toSimpleDiGraph`: the *symmetric orientation* of a simple graph, in which + every edge `s(u, v)` becomes the two arcs `(u, v)` and `(v, u)`. This is how the + undirected library reuses directed developments — reachability, distance, + breadth-first search — instead of duplicating them. It is not registered as a + coercion: an undirected graph should be viewed as directed only on purpose. -/ namespace AlgoLib @@ -139,6 +147,28 @@ instance : Coe (SimpleGraph α) (Graph α (Sym2 α)) := ⟨SimpleGraph.toGraph instance : Coe (SimpleDiGraph α) (DiGraph α (α × α)) := ⟨SimpleDiGraph.toDiGraph⟩ +/-- The *symmetric orientation* of a simple graph: the simple directed graph on the same +vertices whose arcs are the ordered pairs `(u, v)` with `s(u, v)` an edge of `G`. Every +edge thus contributes exactly the two arcs `(u, v)` and `(v, u)`. + +Walks, reachability and distances in `G` coincide with those in `G.toSimpleDiGraph` +(see `AlgoLib.Theory.Graph.Connectivity.Directed`), which lets the undirected theory reuse +the directed one — in particular breadth-first search — rather than duplicating it. -/ +def SimpleGraph.toSimpleDiGraph (G : SimpleGraph α) : SimpleDiGraph α where + vertexSet := G.vertexSet + edgeSet := {a | s(a.1, a.2) ∈ G.edgeSet} + incidence' := fun a ha => + ⟨G.incidence' _ ha a.1 (Sym2.mem_mk_left _ _), G.incidence' _ ha a.2 (Sym2.mem_mk_right _ _)⟩ + loopless' := fun _ ha h => G.loopless' _ ha (Sym2.mk_isDiag_iff.2 h) + +@[simp] lemma SimpleGraph.vertexSet_toSimpleDiGraph (G : SimpleGraph α) : + G.toSimpleDiGraph.vertexSet = G.vertexSet := rfl + +/-- An ordered pair is an arc of the symmetric orientation exactly when the unordered +pair is an edge. -/ +@[simp] lemma SimpleGraph.mem_edgeSet_toSimpleDiGraph (G : SimpleGraph α) {a : α × α} : + a ∈ G.toSimpleDiGraph.edgeSet ↔ s(a.1, a.2) ∈ G.edgeSet := Iff.rfl + /-- Typeclass for graph-like structures that have a vertex set. -/ class HasVertexSet (G : Type*) (V : outParam Type*) where /-- The vertex set of the graph. -/ @@ -204,4 +234,8 @@ theorem SimpleDiGraph.loopless (G : SimpleDiGraph α) {e : α × α} (he : e ∈ e.1 ≠ e.2 := G.loopless' e he +/-- The symmetric orientation has the same vertices, in the `V(·)` notation. -/ +@[simp] lemma SimpleGraph.mem_vertexSet_toSimpleDiGraph_iff (G : SimpleGraph α) {v : α} : + v ∈ V(G.toSimpleDiGraph) ↔ v ∈ V(G) := Iff.rfl + end AlgoLib diff --git a/AlgoLib/Theory/Graph/Connectivity/Basic.lean b/AlgoLib/Theory/Graph/Connectivity/Basic.lean index 06a7fcc..28eff9e 100644 --- a/AlgoLib/Theory/Graph/Connectivity/Basic.lean +++ b/AlgoLib/Theory/Graph/Connectivity/Basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5), Basil Rohner, Sorrachai Yingchareonthawornchai -/ import AlgoLib.Theory.Graph.Connectivity.Reachable +import AlgoLib.Theory.Graph.Connectivity.Directed import AlgoLib.Theory.Graph.Connectivity.Components import AlgoLib.Theory.Graph.Connectivity.Cuts import AlgoLib.Theory.Graph.Connectivity.Connectivity @@ -20,19 +21,25 @@ development, which is split across `AlgoLib/Theory/Connectivity/`: * `Reachable` — `SimpleGraph.Reachable`, its equivalence properties, the path witness, and `IsPreconnected` / `IsConnected`. +* `Directed` — `SimpleDiGraph.Reachable` and the distance `SimpleDiGraph.dist`, the + undirected distance `SimpleGraph.dist` defined through the symmetric orientation + `SimpleGraph.toSimpleDiGraph`, and the transfer lemmas between the two. * `Components` — `componentOf`, `components`, `numComponents`, and the facts that make "more than one component" usable. * `Cuts` — the edge boundary `∂(G, S)`, vertex and edge cuts, cut vertices and cut edges, and separators between vertices and between sets of vertices. * `Connectivity` — `κ(G)` and `κ'(G)`, with the `girth`-style infimum API. -* `Computable` — the computable reachability closure `reachableFinset`, the connected - components as a `Finset`, the four connectivity numbers as executable definitions, and - the `Decidable` instances for reachability, connectedness, cuts and separating sets. +* `Computable` — the computable reachability closure `reachableFinset` and distance + `computeDist`, both by the breadth-first search of + `AlgoLib.Algorithms.Graph.Traversal.BFS`, the connected components as a `Finset`, the + four connectivity numbers as executable definitions, and the `Decidable` instances for + reachability, connectedness, cuts and separating sets. Downstream files should import this umbrella; the split is internal. The submodules form the acyclic spine `Reachable ← Components ← Cuts ← Connectivity`, on top of the deletion operations in `AlgoLib.Graph.Delete` and the walk development in -`AlgoLib.Theory.Structures.InSimpleGraph`. +`AlgoLib.Theory.Structures.InSimpleGraph`; `Directed` sits beside `Reachable`, and +`Computable` closes the development by importing the search algorithm. ## Main definitions @@ -51,7 +58,11 @@ Definitions based on lecture note "Graph Theory ETH 2026" by Benny Sudakov sets of vertices. * `SimpleGraph.vertexConnectivity G`, `SimpleGraph.edgeConnectivity G`, written `κ(G)` and `κ'(G)`. -* `SimpleGraph.reachableFinset G u` — the computable counterpart of `componentOf`, and +* `SimpleDiGraph.Reachable G u v`, `SimpleDiGraph.dist G u v`, `SimpleGraph.dist G u v` — + directed reachability and the distance, the undirected one through + `SimpleGraph.toSimpleDiGraph`. +* `SimpleGraph.reachableFinset G u` — the computable counterpart of `componentOf`, + `SimpleGraph.computeDist G u v` — the computable counterpart of `dist`, and `SimpleGraph.computeVertexConnectivity G` — the computable counterpart of `κ(G)`. ## Notation diff --git a/AlgoLib/Theory/Graph/Connectivity/Computable.lean b/AlgoLib/Theory/Graph/Connectivity/Computable.lean index 6a5b35a..ebf2ca1 100644 --- a/AlgoLib/Theory/Graph/Connectivity/Computable.lean +++ b/AlgoLib/Theory/Graph/Connectivity/Computable.lean @@ -5,6 +5,7 @@ Authors: Huang.JiangYi (co/ Claude Opus 5) -/ import AlgoLib.Theory.Graph.Decidable import AlgoLib.Theory.Graph.Connectivity.Connectivity +import AlgoLib.Algorithms.Graph.Traversal.BFS import AlgoLib.Util.Finset /-! @@ -15,8 +16,8 @@ over all subsets of an arbitrary type, so nothing in the connectivity developmen computes. This file supplies the executable counterparts, on a graph whose vertex set is finite as *data* and whose edge set has decidable membership: -* reachability, as a `Finset` closure, and the `Decidable` instances it yields for - reachability, connectedness, cuts and separating sets; +* reachability and distance, by breadth-first search, and the `Decidable` instances + reachability yields for connectedness, cuts and separating sets; * the connected components, as a `Finset` of `Finset`s; * the four connectivity numbers `κ(G)`, `κ'(G)` and the two cut numbers. @@ -26,6 +27,7 @@ specifications, and every definition here is proved *equal* to the one it comput ## Main definitions * `SimpleGraph.reachableFinset G u` — the vertices reachable from `u`. +* `SimpleGraph.computeDist G u v` — the distance from `u` to `v`. * `SimpleGraph.componentFinset G` — the connected components. * `SimpleGraph.computeNumComponents G` — their number. * `SimpleGraph.computeVertexConnectivity G` / `computeEdgeConnectivity G` / @@ -35,6 +37,7 @@ specifications, and every definition here is proved *equal* to the one it comput * `SimpleGraph.mem_reachableFinset_iff` — `v ∈ G.reachableFinset u ↔ G.Reachable u v`; `SimpleGraph.coe_reachableFinset` identifies the closure with `componentOf`. +* `SimpleGraph.computeDist_eq` — `= G.dist u v`. * `SimpleGraph.numComponents_eq_card` and `SimpleGraph.computeNumComponents_eq`. * `SimpleGraph.computeVertexConnectivity_eq` — `= κ(G)`; likewise for the other three. * `Decidable` instances for `Reachable`, `IsPreconnected`, `IsConnected`, `IsVertexCut`, @@ -42,25 +45,23 @@ specifications, and every definition here is proved *equal* to the one it comput ## Design choices -* **Iteration, not recursion.** `reachableFinset` iterates one breadth-first layer - `|V(G)| + 1` times rather than recursing to a fixed point. There is then no - termination obligation, no equation compiler, and the definition reduces, so `#eval` - and `decide` work. Correctness rests on `Finset.iterate_isFixed_of_inflationary` - (`AlgoLib.Util.Finset`): the iterate *is* a fixed point, hence closed under - adjacency, and completeness follows by induction on the `IsVertexSeqIn` derivation of - the witnessing walk — with no bound on its length, hence no `loopErase` and no - `[DecidableEq α]` inside a `Prop`, which is what - `AlgoLib.Theory.Connectivity.Reachable` set out to avoid. +* **One search, not two.** Reachability and distance are computed by the breadth-first + search of `AlgoLib.Algorithms.Graph.Traversal.BFS`, run on the symmetric orientation + `G.toSimpleDiGraph`. The library thus has a single BFS, stated once for directed + graphs and proved correct once; this file only transports its correctness theorems + through `SimpleGraph.reachable_toSimpleDiGraph_iff`. The search iterates a fixed + number of rounds rather than recursing to a fixed point, so the definitions reduce and + `decide` works — see the design notes of the BFS file. * **One generic bridge for all four numbers.** Each connectivity number is an infimum of `Set.encard` over sets that are, by the first conjunct of their defining predicate, contained in `V(G)` or `E(G)`. `Set.iInf_encard_eq_minENat_powerset` turns exactly that shape into a minimum over a filtered powerset, so each of the four agreement theorems is a one-line corollary and the `⊤` convention is preserved on the nose (`vertexCutNumber Kₙ = ⊤` because `Kₙ` has no vertex cut). -* **Complexity.** `reachableFinset` runs `|V(G)| + 1` layers even after stabilizing, and - the connectivity numbers enumerate all `2^|V(G)|` subsets, testing preconnectedness of - a deleted graph for each. This is a *specification that computes*, not an algorithm: - `decide` is realistic up to about six vertices. See `GraphAlgorithms` for real BFS. +* **Complexity.** The search runs `|V(G)|` rounds even after the last layer has emptied, + and the connectivity numbers enumerate all `2^|V(G)|` subsets, testing preconnectedness + of a deleted graph for each. The latter is a *specification that computes*, not an + algorithm: `decide` is realistic up to about six vertices. -/ namespace AlgoLib @@ -74,114 +75,42 @@ namespace SimpleGraph variable {G : SimpleGraph α} [DecidableEq α] [Fintype G.vertexSet] [DecidablePred (· ∈ G.edgeSet)] -/-! ## One breadth-first layer +/-! ## Reachability, by breadth-first search -`reachStep` and `reachStart` are the construction; the exported contract is -`reachableFinset` together with `mem_reachableFinset_iff`. -/ +The search itself lives in `AlgoLib.Algorithms.Graph.Traversal.BFS` and is directed; an +undirected graph is searched through its symmetric orientation, in which every edge is +traversable both ways. The exported contract is `reachableFinset` together with +`mem_reachableFinset_iff`. -/ -/-- One layer of breadth-first search: adjoin every neighbour of a vertex of `T`. -/ -private def reachStep (G : SimpleGraph α) [DecidableEq α] [Fintype G.vertexSet] - [DecidablePred (· ∈ G.edgeSet)] (T : Finset α) : Finset α := - T ∪ T.biUnion G.computeNeighborFinset - -private lemma mem_reachStep {T : Finset α} {v : α} : - v ∈ G.reachStep T ↔ v ∈ T ∨ ∃ w ∈ T, G.Adj w v := by - simp [reachStep, Finset.mem_biUnion] - -private lemma subset_reachStep (T : Finset α) : T ⊆ G.reachStep T := - Finset.subset_union_left - -private lemma reachStep_subset {T : Finset α} (hT : T ⊆ G.computeVertexFinset) : - G.reachStep T ⊆ G.computeVertexFinset := - Finset.union_subset hT - (Finset.biUnion_subset.2 fun w _ => G.computeNeighborFinset_subset w) - -/-- The start set of the search from `u`: the singleton `{u}` if `u` is a vertex of `G`, -and `∅` otherwise — nothing outside `V(G)` reaches anything. -/ -private def reachStart (G : SimpleGraph α) [DecidableEq α] [Fintype G.vertexSet] +/-- The vertices reachable from `u`, as a `Finset`: breadth-first search from `u` in the +symmetric orientation of `G`. -/ +def reachableFinset (G : SimpleGraph α) [DecidableEq α] [Fintype G.vertexSet] [DecidablePred (· ∈ G.edgeSet)] (u : α) : Finset α := - if u ∈ G.computeVertexFinset then {u} else ∅ - -private lemma mem_reachStart {u v : α} : v ∈ G.reachStart u ↔ v = u ∧ u ∈ V(G) := by - unfold reachStart - split_ifs with h <;> simp_all + G.toSimpleDiGraph.bfsReachableFinset u -private lemma reachStart_subset (u : α) : G.reachStart u ⊆ G.computeVertexFinset := by - unfold reachStart - split_ifs with h <;> simp [h] +/-- The computable closure is exactly the set of vertices reachable from `u`: the +correctness of BFS, transported along the symmetric orientation. -/ +@[simp] lemma mem_reachableFinset_iff {u v : α} : + v ∈ G.reachableFinset u ↔ G.Reachable u v := by + rw [reachableFinset, SimpleDiGraph.mem_bfsReachableFinset_iff, reachable_toSimpleDiGraph_iff] -/-! ## The reachability closure -/ +lemma reachable_of_mem_reachableFinset {u v : α} (h : v ∈ G.reachableFinset u) : + G.Reachable u v := + mem_reachableFinset_iff.1 h -/-- The vertices reachable from `u`, as a `Finset`: iterate one breadth-first layer from -`{u}` often enough to reach a fixed point. -/ -def reachableFinset (G : SimpleGraph α) [DecidableEq α] [Fintype G.vertexSet] - [DecidablePred (· ∈ G.edgeSet)] (u : α) : Finset α := - (G.reachStep)^[G.computeVertexFinset.card + 1] (G.reachStart u) +lemma mem_reachableFinset_of_reachable {u v : α} (h : G.Reachable u v) : + v ∈ G.reachableFinset u := + mem_reachableFinset_iff.2 h lemma reachableFinset_subset (u : α) : G.reachableFinset u ⊆ G.computeVertexFinset := - Finset.iterate_subset (fun _ h => reachStep_subset h) (reachStart_subset u) _ + fun _ hv => by simpa using (mem_reachableFinset_iff.1 hv).right_mem lemma self_mem_reachableFinset {u : α} (hu : u ∈ V(G)) : u ∈ G.reachableFinset u := - Finset.subset_iterate (fun _ => subset_reachStep _) _ (mem_reachStart.2 ⟨rfl, hu⟩) - -/-- The closure is a fixed point of the search step: this is the stabilization argument, -and it is what makes the closure closed under adjacency. -/ -private lemma reachStep_reachableFinset (u : α) : - G.reachStep (G.reachableFinset u) = G.reachableFinset u := - Finset.iterate_isFixed_of_inflationary (fun _ => subset_reachStep _) - (fun _ h => reachStep_subset h) (reachStart_subset u) + mem_reachableFinset_iff.2 (Reachable.refl G hu) lemma mem_reachableFinset_of_adj {u v w : α} (hw : w ∈ G.reachableFinset u) - (hadj : G.Adj w v) : v ∈ G.reachableFinset u := by - rw [← reachStep_reachableFinset u, mem_reachStep] - exact Or.inr ⟨w, hw, hadj⟩ - -/-! ## Correctness -/ - -private lemma reachable_of_mem_iterate {u : α} : - ∀ (n : ℕ) (v : α), v ∈ (G.reachStep)^[n] (G.reachStart u) → G.Reachable u v := by - intro n - induction n with - | zero => - intro v hv - rw [Function.iterate_zero, id_eq, mem_reachStart] at hv - obtain ⟨rfl, hu⟩ := hv - exact Reachable.refl G hu - | succ n ih => - intro v hv - rw [Function.iterate_succ_apply', mem_reachStep] at hv - rcases hv with hv | ⟨w, hw, hadj⟩ - · exact ih v hv - · exact (ih w hw).trans hadj.reachable - -lemma reachable_of_mem_reachableFinset {u v : α} (h : v ∈ G.reachableFinset u) : - G.Reachable u v := - reachable_of_mem_iterate _ v h - -private lemma mem_reachableFinset_of_isVertexSeqIn {u : α} : - ∀ {w : VertexSeq α}, G.IsVertexSeqIn w → w.head = u → - w.tail ∈ G.reachableFinset u := by - intro w hw - induction hw with - | singleton x hx => - intro hhead - simp only [VertexSeq.head_singleton] at hhead - subst hhead - exact self_mem_reachableFinset (by simpa using hx) - | cons w x hw hadj ih => - intro hhead - rw [VertexSeq.head_cons] at hhead - exact mem_reachableFinset_of_adj (ih hhead) hadj - -lemma mem_reachableFinset_of_reachable {u v : α} (h : G.Reachable u v) : - v ∈ G.reachableFinset u := by - obtain ⟨w, hw, rfl, rfl⟩ := h - exact mem_reachableFinset_of_isVertexSeqIn hw rfl - -/-- The computable closure is exactly the set of vertices reachable from `u`. -/ -@[simp] lemma mem_reachableFinset_iff {u v : α} : - v ∈ G.reachableFinset u ↔ G.Reachable u v := - ⟨reachable_of_mem_reachableFinset, mem_reachableFinset_of_reachable⟩ + (hadj : G.Adj w v) : v ∈ G.reachableFinset u := + mem_reachableFinset_iff.2 ((mem_reachableFinset_iff.1 hw).trans hadj.reachable) /-- The closure, as a set, is the connected component of `u`. -/ @[simp] lemma coe_reachableFinset (u : α) : @@ -193,6 +122,19 @@ lemma mem_reachableFinset_of_reachable {u v : α} (h : G.Reachable u v) : instance instDecidableReachable (u v : α) : Decidable (G.Reachable u v) := decidable_of_iff _ mem_reachableFinset_iff +/-! ## Distance -/ + +/-- The distance from `u` to `v`, computed by breadth-first search in the symmetric +orientation of `G`. -/ +def computeDist (G : SimpleGraph α) [DecidableEq α] [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] (u v : α) : ℕ∞ := + G.toSimpleDiGraph.bfsDist u v + +/-- The computed distance is the distance: BFS is correct, and `SimpleGraph.dist` *is* the +distance in the symmetric orientation. -/ +theorem computeDist_eq {u v : α} : G.computeDist u v = G.dist u v := + SimpleDiGraph.bfsDist_eq_dist + /-! ## Connectedness -/ lemma isPreconnected_iff_forall_subset : @@ -376,6 +318,10 @@ example : pathG.IsConnected := by decide example : pathG.IsCutVertex 1 := by decide example : ¬ pathG.IsCutVertex 0 := by decide example : pathG.computeNumComponents = 1 := by decide +example : pathG.computeDist 0 2 = 2 := by decide +example : pathG.computeDist 2 0 = 2 := by decide +example : pathG.dist 0 2 = 2 := by + rw [← computeDist_eq]; decide -- Removing the middle vertex, or either edge, disconnects a path. example : pathG.computeVertexConnectivity = 1 := by decide @@ -403,6 +349,7 @@ example : splitG.reachableFinset 3 = {3} := by decide example : ¬ splitG.Reachable 0 3 := by decide example : ¬ splitG.IsPreconnected := by decide example : splitG.computeNumComponents = 2 := by decide +example : splitG.computeDist 0 3 = ⊤ := by decide -- A disconnected graph is separated by the empty set. example : splitG.computeVertexConnectivity = 0 := by decide diff --git a/AlgoLib/Theory/Graph/Connectivity/Directed.lean b/AlgoLib/Theory/Graph/Connectivity/Directed.lean new file mode 100644 index 0000000..b6614f4 --- /dev/null +++ b/AlgoLib/Theory/Graph/Connectivity/Directed.lean @@ -0,0 +1,258 @@ +/- +Copyright (c) 2026 AlgoLib working group. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Huang.JiangYi (co/ Claude Fable 5.1) +-/ +import AlgoLib.Theory.Graph.Structures.InSimpleDiGraph +import AlgoLib.Theory.Graph.Connectivity.Reachable +import Mathlib.Data.ENat.Lattice + +/-! +# Reachability and distance in a simple directed graph + +The directed analogue of `AlgoLib.Theory.Graph.Connectivity.Reachable`, together with the +*distance* — the least length of a walk between two vertices. The distance is the +specification that breadth-first search (`AlgoLib.Algorithms.Graph.Traversal.BFS`) is +proved to compute. + +Because every simple graph has a symmetric orientation `SimpleGraph.toSimpleDiGraph` in +which walks are the same walks, the undirected distance is *defined* through the directed +one rather than duplicated; the transfer lemmas at the end of this file are what make +that definition usable. + +## Main definitions + +* `SimpleDiGraph.Reachable G u v` — some simple walk realized in `G` runs from `u` to `v`. +* `SimpleDiGraph.dist G u v` — the least length of such a walk, in `ℕ∞`; `⊤` when `v` is + not reachable from `u`. +* `SimpleGraph.dist G u v` — the distance in the symmetric orientation. + +## Main results + +* `SimpleDiGraph.Reachable.refl`, `SimpleDiGraph.Reachable.trans` — reachability is a + preorder on `V(G)`. There is no symmetry: this is the directed setting. +* `SimpleDiGraph.dist_le_length`, `SimpleDiGraph.le_dist_iff` — the infimum API. +* `SimpleDiGraph.dist_eq_top_iff`, `SimpleDiGraph.reachable_iff_dist_ne_top` — the + distance is finite exactly on reachable pairs. +* `SimpleDiGraph.dist_exists` — a finite distance is attained by a walk. +* `SimpleGraph.reachable_toSimpleDiGraph_iff` — reachability in `G` is reachability in + its symmetric orientation, and likewise `SimpleGraph.dist_comm` for the distance. + +## Design choices + +* **Walks, not paths, in the definitions**, for the same reason as in the undirected + file: gluing two walks is a walk, while gluing two paths needs cycle erasure, hence + `[DecidableEq α]` inside a `Prop`. A shortest walk is automatically a path, so nothing + is lost. +* **Nested `⨅`, mirroring `girth` and `κ`.** `dist` has the shape + `⨅ (w) (_ : P w), f w`, so the standard infimum API (`le_iInf₂_iff`, `iInf₂_le`, + `iInf_eq_top`) applies verbatim, and `⊤` on unreachable pairs is the empty-index + convention rather than a special case. +* **The undirected distance is the directed one.** `SimpleGraph.dist` unfolds to + `SimpleDiGraph.dist` on `G.toSimpleDiGraph`: one definition, one algorithm, and one + correctness proof serve both kinds of graph. +-/ + +variable {α : Type*} + +namespace AlgoLib + +open scoped AlgoLib + +namespace SimpleDiGraph + +/-! ## Reachability -/ + +/-- `v` is *reachable* from `u` in the simple directed graph `G` when some simple walk +realized in `G` runs from `u` to `v`. Reachability is reflexive only at vertices of `G` +and, unlike the undirected notion, not symmetric. -/ +@[grind] def Reachable (G : SimpleDiGraph α) (u v : α) : Prop := + ∃ w : SimpleWalk α, G.IsSimpleWalkIn w ∧ w.head = u ∧ w.tail = v + +/-- The source of a reachability is a vertex of `G`. -/ +@[grind →] theorem Reachable.left_mem {G : SimpleDiGraph α} {u v : α} + (h : G.Reachable u v) : u ∈ V(G) := by + obtain ⟨w, hw, rfl, -⟩ := h + exact IsSimpleWalkIn.head_mem G hw + +/-- The target of a reachability is a vertex of `G`. -/ +@[grind →] theorem Reachable.right_mem {G : SimpleDiGraph α} {u v : α} + (h : G.Reachable u v) : v ∈ V(G) := by + obtain ⟨w, hw, -, rfl⟩ := h + exact IsSimpleWalkIn.tail_mem G hw + +/-- Reachability is reflexive on `V(G)`, witnessed by the one-vertex walk. -/ +theorem Reachable.refl (G : SimpleDiGraph α) {v : α} (hv : v ∈ V(G)) : G.Reachable v v := + ⟨(SimplePath.singleton v).val, IsVertexSeqIn.singleton v hv, rfl, rfl⟩ + +/-- Reachability is transitive: glue the two witnessing walks at their shared vertex. -/ +theorem Reachable.trans {G : SimpleDiGraph α} {u v w : α} + (h₁ : G.Reachable u v) (h₂ : G.Reachable v w) : G.Reachable u w := by + obtain ⟨p, hp, rfl, rfl⟩ := h₁ + obtain ⟨q, hq, hqh, rfl⟩ := h₂ + exact ⟨p.glue q hqh.symm, IsSimpleWalkIn.glue G hp hq hqh.symm, + SimpleWalk.head_glue p q _, SimpleWalk.tail_glue p q _⟩ + +/-- A vertex reaches itself exactly when it is a vertex of `G`. -/ +@[simp] theorem reachable_self_iff {G : SimpleDiGraph α} {v : α} : + G.Reachable v v ↔ v ∈ V(G) := + ⟨Reachable.left_mem, Reachable.refl G⟩ + +/-- The target of an arc is reachable from its source, by the length-one walk. -/ +theorem Adj.reachable {G : SimpleDiGraph α} {u v : α} (h : G.Adj u v) : G.Reachable u v := by + refine ⟨⟨(VertexSeq.singleton u).cons v, by simpa [VertexSeq.nonstalling] using h.ne⟩, + ?_, rfl, rfl⟩ + exact IsVertexSeqIn.cons (VertexSeq.singleton u) v + (IsVertexSeqIn.singleton u h.left_mem) (by simpa using h) + +/-- Reachability is monotone under passing to a supergraph. -/ +theorem Reachable.mono {G H : SimpleDiGraph α} {u v : α} (h : H.Reachable u v) + (hsub : SimpleDiGraph.subgraphOf H G) : G.Reachable u v := by + obtain ⟨w, hw, h1, h2⟩ := h + exact ⟨w, IsSimpleWalkIn.mono G H hw hsub, h1, h2⟩ + +/-! ## Distance -/ + +/-- The *distance* from `u` to `v` in `G`: the least length of a simple walk realized in +`G` from `u` to `v`, and `⊤` when there is none. -/ +noncomputable def dist (G : SimpleDiGraph α) (u v : α) : ℕ∞ := + ⨅ (w : SimpleWalk α) (_ : G.IsSimpleWalkIn w ∧ w.head = u ∧ w.tail = v), (w.length : ℕ∞) + +/-- Every walk from `u` to `v` bounds the distance from above. -/ +lemma dist_le_length {G : SimpleDiGraph α} {u v : α} {w : SimpleWalk α} + (hw : G.IsSimpleWalkIn w) (hu : w.head = u) (hv : w.tail = v) : + G.dist u v ≤ w.length := + iInf₂_le w ⟨hw, hu, hv⟩ + +/-- The lower-bound characterization of the distance: the workhorse lemma. -/ +theorem le_dist_iff {G : SimpleDiGraph α} {u v : α} {n : ℕ∞} : + n ≤ G.dist u v ↔ + ∀ w : SimpleWalk α, G.IsSimpleWalkIn w → w.head = u → w.tail = v → n ≤ w.length := by + simp [dist, le_iInf_iff] + +/-- The distance is infinite exactly when `v` is not reachable from `u`. -/ +theorem dist_eq_top_iff {G : SimpleDiGraph α} {u v : α} : + G.dist u v = ⊤ ↔ ¬ G.Reachable u v := by + simp [dist, iInf_eq_top, Reachable] + +/-- `v` is reachable from `u` exactly when the distance is finite. -/ +theorem reachable_iff_dist_ne_top {G : SimpleDiGraph α} {u v : α} : + G.Reachable u v ↔ G.dist u v ≠ ⊤ := by + rw [Ne, dist_eq_top_iff, not_not] + +/-- A finite distance is attained: some walk from `u` to `v` has exactly that length. -/ +theorem dist_exists {G : SimpleDiGraph α} {u v : α} (h : G.Reachable u v) : + ∃ w : SimpleWalk α, G.IsSimpleWalkIn w ∧ w.head = u ∧ w.tail = v ∧ + (w.length : ℕ∞) = G.dist u v := by + have hne : Nonempty {w : SimpleWalk α // G.IsSimpleWalkIn w ∧ w.head = u ∧ w.tail = v} := + nonempty_subtype.mpr h + obtain ⟨w, hw⟩ := @ENat.exists_eq_iInf _ hne fun w => (w.val.length : ℕ∞) + exact ⟨w.val, w.property.1, w.property.2.1, w.property.2.2, hw.trans iInf_subtype⟩ + +/-- A vertex is at distance zero from itself, by the one-vertex walk. -/ +@[simp] theorem dist_self {G : SimpleDiGraph α} {v : α} (hv : v ∈ V(G)) : G.dist v v = 0 := by + have hw : G.IsSimpleWalkIn (SimplePath.singleton v).val := IsVertexSeqIn.singleton v hv + have := dist_le_length (u := v) (v := v) hw rfl rfl + simp only [SimpleWalk.length, SimplePath.vertices_singleton, VertexSeq.length_singleton, + Nat.cast_zero, nonpos_iff_eq_zero] at this + exact this + +/-- The endpoints of an arc are at distance at most one, by the length-one walk. -/ +theorem dist_le_one_of_adj {G : SimpleDiGraph α} {u v : α} (h : G.Adj u v) : + G.dist u v ≤ 1 := by + have := dist_le_length (u := u) (v := v) + (w := ⟨(VertexSeq.singleton u).cons v, by simpa [VertexSeq.nonstalling] using h.ne⟩) + (IsVertexSeqIn.cons (VertexSeq.singleton u) v (IsVertexSeqIn.singleton u h.left_mem) + (by simpa using h)) rfl rfl + simpa [VertexSeq.length] using this + +/-- The triangle inequality: a shortest walk to `v` glued to a shortest walk from `v` to +`w` is a walk from `u` to `w` of the summed length. -/ +theorem dist_triangle (G : SimpleDiGraph α) (u v w : α) : + G.dist u w ≤ G.dist u v + G.dist v w := by + by_cases h₁ : G.Reachable u v + · by_cases h₂ : G.Reachable v w + · obtain ⟨p, hp, hpu, hpv, hplen⟩ := dist_exists h₁ + obtain ⟨q, hq, hqv, hqw, hqlen⟩ := dist_exists h₂ + rw [← hplen, ← hqlen] + calc G.dist u w ≤ ((p.glue q (hpv.trans hqv.symm)).length : ℕ∞) := + dist_le_length (IsSimpleWalkIn.glue G hp hq _) (by simp [hpu]) (by simp [hqw]) + _ = (p.length : ℕ∞) + q.length := by rw [SimpleWalk.length_glue]; push_cast; rfl + · rw [dist_eq_top_iff.2 h₂, add_top] + exact le_top + · rw [dist_eq_top_iff.2 h₁, top_add] + exact le_top + +end SimpleDiGraph + +/-! ## The symmetric orientation + +A simple walk is realized in `G` exactly when it is realized in the symmetric orientation +`G.toSimpleDiGraph`, because adjacency is the same relation. Reachability and distance +transfer accordingly, and the undirected distance is defined through the directed one. -/ + +namespace SimpleGraph + +/-- A vertex sequence is realized in the symmetric orientation exactly when it is realized +in the graph. -/ +@[simp] theorem isVertexSeqIn_toSimpleDiGraph_iff (G : SimpleGraph α) {w : VertexSeq α} : + G.toSimpleDiGraph.IsVertexSeqIn w ↔ G.IsVertexSeqIn w := by + induction w with + | singleton v => simp + | cons w u ih => simp [ih] + +/-- A simple walk is realized in the symmetric orientation exactly when it is realized in +the graph. -/ +@[simp] theorem isSimpleWalkIn_toSimpleDiGraph_iff (G : SimpleGraph α) {w : SimpleWalk α} : + G.toSimpleDiGraph.IsSimpleWalkIn w ↔ G.IsSimpleWalkIn w := + G.isVertexSeqIn_toSimpleDiGraph_iff + +/-- Reachability in the symmetric orientation is reachability in the graph. -/ +@[simp] theorem reachable_toSimpleDiGraph_iff (G : SimpleGraph α) {u v : α} : + G.toSimpleDiGraph.Reachable u v ↔ G.Reachable u v := by + simp [SimpleDiGraph.Reachable, Reachable] + +/-- The *distance* between `u` and `v` in the simple graph `G`: the least length of a +simple walk realized in `G` from `u` to `v`, and `⊤` when there is none. Defined as the +distance in the symmetric orientation, so that the directed theory and the breadth-first +search that computes it serve both kinds of graph. -/ +noncomputable def dist (G : SimpleGraph α) (u v : α) : ℕ∞ := G.toSimpleDiGraph.dist u v + +/-- Every walk from `u` to `v` bounds the distance from above. -/ +lemma dist_le_length {G : SimpleGraph α} {u v : α} {w : SimpleWalk α} + (hw : G.IsSimpleWalkIn w) (hu : w.head = u) (hv : w.tail = v) : + G.dist u v ≤ w.length := + SimpleDiGraph.dist_le_length (G.isSimpleWalkIn_toSimpleDiGraph_iff.2 hw) hu hv + +/-- The lower-bound characterization of the undirected distance. -/ +theorem le_dist_iff {G : SimpleGraph α} {u v : α} {n : ℕ∞} : + n ≤ G.dist u v ↔ + ∀ w : SimpleWalk α, G.IsSimpleWalkIn w → w.head = u → w.tail = v → n ≤ w.length := by + simp [dist, SimpleDiGraph.le_dist_iff] + +/-- The distance is infinite exactly when `u` and `v` are not reachable. -/ +theorem dist_eq_top_iff {G : SimpleGraph α} {u v : α} : + G.dist u v = ⊤ ↔ ¬ G.Reachable u v := by + rw [dist, SimpleDiGraph.dist_eq_top_iff, reachable_toSimpleDiGraph_iff] + +/-- `u` and `v` are reachable exactly when their distance is finite. -/ +theorem reachable_iff_dist_ne_top {G : SimpleGraph α} {u v : α} : + G.Reachable u v ↔ G.dist u v ≠ ⊤ := by + rw [Ne, dist_eq_top_iff, not_not] + +/-- A vertex is at distance zero from itself. -/ +@[simp] theorem dist_self {G : SimpleGraph α} {v : α} (hv : v ∈ V(G)) : G.dist v v = 0 := + SimpleDiGraph.dist_self hv + +/-- The undirected distance is symmetric: reverse the witnessing walks. -/ +theorem dist_comm (G : SimpleGraph α) (u v : α) : G.dist u v = G.dist v u := by + have key : ∀ a b : α, G.dist a b ≤ G.dist b a := fun a b => + le_dist_iff.2 fun w hw hb ha => by + have := dist_le_length (u := a) (v := b) (IsSimpleWalkIn.reverse G hw) + (by simp [SimpleWalk.reverse, ha]) (by simp [SimpleWalk.reverse, hb]) + simpa [SimpleWalk.reverse] using this + exact le_antisymm (key u v) (key v u) + +end SimpleGraph + +end AlgoLib diff --git a/AlgoLib/Theory/Graph/Decidable.lean b/AlgoLib/Theory/Graph/Decidable.lean index 26f05bc..45e87ba 100644 --- a/AlgoLib/Theory/Graph/Decidable.lean +++ b/AlgoLib/Theory/Graph/Decidable.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5) -/ import AlgoLib.Theory.Graph.Delete +import AlgoLib.Theory.Graph.Degree import AlgoLib.Theory.Graph.Finite import AlgoLib.Util.Decidable @@ -20,13 +21,19 @@ graph, so that a predicate about `G.deleteVertices S` is decidable whenever the corresponding predicate about `G` is. Reachability and connectedness are decided in `AlgoLib.Theory.Connectivity.Computable`, -on top of what is here. +on top of what is here and of the breadth-first search in +`AlgoLib.Algorithms.Graph.Traversal.BFS`. ## Main results -* `SimpleGraph.instDecidableRelAdj` — adjacency is decidable when edge membership is. +* `SimpleGraph.instDecidableRelAdj`, `SimpleDiGraph.instDecidableRelAdj` — adjacency is + decidable when edge membership is. +* `SimpleGraph.computeNeighborFinset`, `SimpleDiGraph.computeOutNeighborFinset` — the + neighbours, resp. out-neighbours, of a vertex as a `Finset`, identified with the + `Set`-valued neighbourhoods of `AlgoLib.Graph.Degree` by the `coe_compute…` lemmas. * Instances propagating `Fintype` on the vertex set and `DecidablePred` on the edge set - through `SimpleGraph.deleteEdges` and `SimpleGraph.deleteVertices`. + through `SimpleGraph.deleteEdges` and `SimpleGraph.deleteVertices`, and to the + symmetric orientation `SimpleGraph.toSimpleDiGraph`. * Instances stating the same data in the `V(·)` / `E(·)` notation, which is how the connectivity predicates are phrased. @@ -106,10 +113,9 @@ beside `computeVertexFinset` in `AlgoLib.Graph.Finite` because it is exactly the `Finset` that decidable adjacency buys: the neighbours of `v` are the vertices the adjacency test accepts. -TODO: once `AlgoLib.Graph.Degree` compiles, add -`coe_computeNeighborFinset : ↑(G.computeNeighborFinset v) = G.neighborSet v`, and keep -the `compute` prefix — `Degree.lean` reserves the plain name `neighborFinset` for the -`[Finite V(G)]` variant. -/ +The `compute` prefix is kept deliberately — `Degree.lean` reserves the plain names +`neighborSet` / `outNeighborSet` for the `Set`-valued specifications, and the +`coe_compute…Finset` lemmas below identify the two. -/ /-- The neighbours of `v` in `G`, as a `Finset`. -/ def SimpleGraph.computeNeighborFinset (G : SimpleGraph α) [DecidableEq α] @@ -127,6 +133,94 @@ lemma SimpleGraph.computeNeighborFinset_subset (G : SimpleGraph α) [DecidableEq G.computeNeighborFinset v ⊆ G.computeVertexFinset := Finset.filter_subset _ _ +/-- The computable neighbour finset is the neighbour set of `AlgoLib.Graph.Degree`. -/ +@[simp] lemma SimpleGraph.coe_computeNeighborFinset (G : SimpleGraph α) [DecidableEq α] + [Fintype G.vertexSet] [DecidablePred (· ∈ G.edgeSet)] (v : α) : + (G.computeNeighborFinset v : Set α) = G.neighborSet v := + Set.ext fun u => by + rw [Finset.mem_coe, mem_computeNeighborFinset] + exact ⟨fun h => h.symm, fun h => h.symm⟩ + +/-! ## The directed counterparts + +`SimpleDiGraph` gets the same bridge instances, decidable adjacency and an +*out*-neighbour finset: these are exactly the data a breadth-first search consumes +(`AlgoLib.Algorithms.Graph.Traversal.BFS`). -/ + +/-- The `V(·)` counterpart of `SimpleGraph.mem_vertexSet_notation`. -/ +@[simp] lemma SimpleDiGraph.mem_vertexSet_notation (G : SimpleDiGraph α) {v : α} : + v ∈ (V(G) : Set α) ↔ v ∈ G.vertexSet := Iff.rfl + +/-- The `E(·)` counterpart of `SimpleGraph.mem_edgeSet_notation`. -/ +@[simp] lemma SimpleDiGraph.mem_edgeSet_notation (G : SimpleDiGraph α) {a : α × α} : + a ∈ (E(G) : Set (α × α)) ↔ a ∈ G.edgeSet := Iff.rfl + +/-- The `V(·)` spelling of `[Fintype G.vertexSet]`. -/ +instance SimpleDiGraph.instFintypeVertexSetNotation (G : SimpleDiGraph α) + [Fintype G.vertexSet] : Fintype (V(G) : Set α) := + inferInstanceAs (Fintype G.vertexSet) + +/-- Membership in the vertex set is decidable once it is finite; see +`SimpleGraph.instDecidablePredMemVertexSet` for why this is safe as an instance. -/ +instance SimpleDiGraph.instDecidablePredMemVertexSet (G : SimpleDiGraph α) [DecidableEq α] + [Fintype G.vertexSet] : DecidablePred (· ∈ G.vertexSet) := + Set.decidableMemOfFintype _ + +/-- The `V(·)` spelling of `SimpleDiGraph.instDecidablePredMemVertexSet`. -/ +instance SimpleDiGraph.instDecidablePredMemVertexSetNotation (G : SimpleDiGraph α) + [DecidableEq α] [Fintype G.vertexSet] : DecidablePred (· ∈ (V(G) : Set α)) := + inferInstanceAs (DecidablePred (· ∈ G.vertexSet)) + +/-- The `E(·)` spelling of `[DecidablePred (· ∈ G.edgeSet)]`. -/ +instance SimpleDiGraph.instDecidablePredMemEdgeSetNotation (G : SimpleDiGraph α) + [DecidablePred (· ∈ G.edgeSet)] : DecidablePred (· ∈ (E(G) : Set (α × α))) := + inferInstanceAs (DecidablePred (· ∈ G.edgeSet)) + +/-- Directed adjacency is decidable exactly when edge membership is: `G.Adj u v` is by +definition `(u, v) ∈ E(G)`. -/ +instance SimpleDiGraph.instDecidableRelAdj (G : SimpleDiGraph α) + [DecidablePred (· ∈ G.edgeSet)] : DecidableRel G.Adj := + fun u v => decidable_of_iff ((u, v) ∈ G.edgeSet) Iff.rfl + +/-- The out-neighbours of `v` in `G` — the targets of the arcs leaving `v` — as a +`Finset`. -/ +def SimpleDiGraph.computeOutNeighborFinset (G : SimpleDiGraph α) [DecidableEq α] + [Fintype G.vertexSet] [DecidablePred (· ∈ G.edgeSet)] (v : α) : Finset α := + G.computeVertexFinset.filter (G.Adj v ·) + +@[simp] lemma SimpleDiGraph.mem_computeOutNeighborFinset (G : SimpleDiGraph α) + [DecidableEq α] [Fintype G.vertexSet] [DecidablePred (· ∈ G.edgeSet)] {v u : α} : + u ∈ G.computeOutNeighborFinset v ↔ G.Adj v u := by + simp only [computeOutNeighborFinset, Finset.mem_filter, mem_computeVertexFinset] + exact ⟨And.right, fun h => ⟨h.right_mem, h⟩⟩ + +lemma SimpleDiGraph.computeOutNeighborFinset_subset (G : SimpleDiGraph α) [DecidableEq α] + [Fintype G.vertexSet] [DecidablePred (· ∈ G.edgeSet)] (v : α) : + G.computeOutNeighborFinset v ⊆ G.computeVertexFinset := + Finset.filter_subset _ _ + +/-- The computable out-neighbour finset is the out-neighbour set of +`AlgoLib.Graph.Degree`. -/ +@[simp] lemma SimpleDiGraph.coe_computeOutNeighborFinset (G : SimpleDiGraph α) + [DecidableEq α] [Fintype G.vertexSet] [DecidablePred (· ∈ G.edgeSet)] (v : α) : + (G.computeOutNeighborFinset v : Set α) = G.outNeighborSet v := + Set.ext fun u => by rw [Finset.mem_coe, mem_computeOutNeighborFinset]; exact Iff.rfl + +/-! ## The symmetric orientation + +The data of a simple graph transfers to `SimpleGraph.toSimpleDiGraph`, whose vertex set +is the same set and whose arc membership is edge membership of the unordered pair. -/ + +/-- The symmetric orientation has the same, finite, vertex set. -/ +instance SimpleGraph.instFintypeVertexSetToSimpleDiGraph (G : SimpleGraph α) + [Fintype G.vertexSet] : Fintype G.toSimpleDiGraph.vertexSet := + inferInstanceAs (Fintype G.vertexSet) + +/-- Arc membership in the symmetric orientation is decided by edge membership. -/ +instance SimpleGraph.instDecidablePredMemEdgeSetToSimpleDiGraph (G : SimpleGraph α) + [DecidablePred (· ∈ G.edgeSet)] : DecidablePred (· ∈ G.toSimpleDiGraph.edgeSet) := + fun a => decidable_of_iff (s(a.1, a.2) ∈ G.edgeSet) Iff.rfl + /-! ## Propagating the data through deletions -/ /-- Edge deletion keeps the vertex set, hence its `Fintype`. -/ diff --git a/AlgoLib/Theory/Graph/Structures/SimpleWalk.lean b/AlgoLib/Theory/Graph/Structures/SimpleWalk.lean index 273f7ee..4406646 100644 --- a/AlgoLib/Theory/Graph/Structures/SimpleWalk.lean +++ b/AlgoLib/Theory/Graph/Structures/SimpleWalk.lean @@ -139,6 +139,16 @@ the result is `q`, whose head is that same vertex. -/ · rfl · exact VertexSeq.tail_append _ _ +/-- Gluing adds the lengths: the duplicated joining vertex contributes no edge. -/ +@[simp] lemma length_glue (p q : SimpleWalk α) (h : p.val.tail = q.val.head) : + (p.glue q h).length = p.length + q.length := by + rw [SimpleWalk.glue] + split <;> rename_i hp + · simp [hp] + · change (p.val.dropTail.append q.val).length = p.val.length + q.val.length + rw [VertexSeq.length_append, ← VertexSeq.length_dropTail_succ p.val hp] + omega + /-! ## reverse -/ /-- Reverse a simple walk: the head becomes the tail and vice versa. Reversal diff --git a/blueprint/src/chapters/Algorithms/Graph/Traversal/Basic.tex b/blueprint/src/chapters/Algorithms/Graph/Traversal/Basic.tex index 2d99b9c..4eede5d 100644 --- a/blueprint/src/chapters/Algorithms/Graph/Traversal/Basic.tex +++ b/blueprint/src/chapters/Algorithms/Graph/Traversal/Basic.tex @@ -1,2 +1,101 @@ -% Mirrors `AlgoLib.Algorithms.Graph.Traversal.Basic` +% Mirrors `AlgoLib.Algorithms.Graph.Traversal.*` % +\subsection{Breadth-first search} +% Mirrors `AlgoLib.Algorithms.Graph.Traversal.BFS` + +Throughout, $G$ is a simple directed graph whose vertex set $\V{G}$ is finite and given as +data, and whose arc membership is decidable. Undirected graphs are searched through their +symmetric orientation (Definition~\ref{def:symmetric-orientation}), so one search serves +both kinds of graph. + +\begin{definition}[BFS layers] + \label{def:bfs-layers} + \lean{AlgoLib.SimpleDiGraph.bfsLayer, AlgoLib.SimpleDiGraph.bfsVisited} + \leanok + Let $s \in \V{G}$. The \emph{layers} of breadth-first search from $s$ are the sets + \[ + L_0 = \{s\}, \qquad + L_{k+1} = N^+(L_k) \setminus (L_0 \cup \dots \cup L_k), + \] + where $N^+(L)$ denotes the set of out-neighbours of the vertices of $L$. The set of + vertices \emph{visited} within $k$ rounds is $V_k = L_0 \cup \dots \cup L_k$. When + $s \notin \V{G}$ every layer is empty. + In Lean the search is a state $(V_k, L_k)$ iterated $k$ times from $(\{s\}, \{s\})$, + so that the definition reduces and \texttt{decide} can evaluate it. +\end{definition} + +\begin{lemma}[Soundness] + \label{lem:bfs-sound} + \lean{AlgoLib.SimpleDiGraph.exists_walk_of_mem_bfsLayer} + \leanok + \uses{def:bfs-layers} + Every vertex of $L_k$ is the endpoint of a walk of length $k$ from $s$. +\end{lemma} +\begin{proof} + \leanok + By induction on $k$: a vertex of $L_{k+1}$ is an out-neighbour of a vertex of $L_k$, + and appending that arc to the walk given by the induction hypothesis yields a walk of + length $k + 1$. +\end{proof} + +\begin{lemma}[Completeness] + \label{lem:bfs-complete} + \lean{AlgoLib.SimpleDiGraph.mem_bfsVisited_of_isVertexSeqIn} + \leanok + \uses{def:bfs-layers} + The endpoint of a walk of length $\ell$ from $s$ lies in $V_\ell$. +\end{lemma} +\begin{proof} + \leanok + By induction on the walk. The key step is that the out-neighbours of a vertex of $V_k$ + lie in $V_{k+1}$: such a vertex lies in some $L_j$ with $j \le k$, and its + out-neighbours are either already in $V_j$ or in $L_{j+1}$. +\end{proof} + +\begin{lemma}[Termination] + \label{lem:bfs-termination} + \lean{AlgoLib.SimpleDiGraph.lt_card_of_nonempty_bfsLayer} + \leanok + \uses{def:bfs-layers} + If $L_k \neq \emptyset$ then $k < |\V{G}|$. Hence the search from $s$ has exhausted every + layer after $|\V{G}|$ rounds. +\end{lemma} +\begin{proof} + \leanok + An empty layer is followed by an empty layer, so $L_0, \dots, L_k$ are all non-empty. + They are pairwise disjoint subsets of $\V{G}$, so $k + 1 \le |V_k| \le |\V{G}|$. +\end{proof} + +\begin{theorem}[The layers are the spheres] + \label{thm:bfs-layers-spheres} + \lean{AlgoLib.SimpleDiGraph.mem_bfsLayer_iff_dist_eq} + \leanok + \uses{def:bfs-layers, def:dist} + For every vertex $v$ and every $k \in \N$, + \[ + v \in L_k \iff \dist(s, v) = k . + \] +\end{theorem} +\begin{proof} + \leanok + \uses{lem:bfs-sound, lem:bfs-complete} + 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$. +\end{proof} + +\begin{theorem}[BFS computes reachability and distance] + \label{thm:bfs-correct} + \lean{AlgoLib.SimpleDiGraph.mem_bfsReachableFinset_iff, AlgoLib.SimpleDiGraph.bfsDist_eq_dist} + \leanok + \uses{def:bfs-layers, def:reachable-directed, def:dist} + The set $V_{|\V{G}|}$ is exactly the set of vertices reachable from $s$, and the least + $k < |\V{G}|$ with $v \in L_k$ (or $\infty$ if there is none) is exactly $\dist(s, v)$. +\end{theorem} +\begin{proof} + \leanok + \uses{lem:bfs-sound, lem:bfs-complete, lem:bfs-termination} + Soundness gives one inclusion and one inequality; completeness together with the + termination bound gives the other. +\end{proof} diff --git a/blueprint/src/chapters/Theory/Graph/Connectivity/Basic.tex b/blueprint/src/chapters/Theory/Graph/Connectivity/Basic.tex index 53094d9..6c60939 100644 --- a/blueprint/src/chapters/Theory/Graph/Connectivity/Basic.tex +++ b/blueprint/src/chapters/Theory/Graph/Connectivity/Basic.tex @@ -1,2 +1,36 @@ % Mirrors `AlgoLib.Theory.Graph.Connectivity.*` % +\subsection{Reachability and distance} +% Mirrors `AlgoLib.Theory.Graph.Connectivity.Reachable` and +% `AlgoLib.Theory.Graph.Connectivity.Directed` + +\begin{definition}[Reachability] + \label{def:reachable-directed} + \lean{AlgoLib.SimpleGraph.Reachable, AlgoLib.SimpleDiGraph.Reachable} + \leanok + Let $G$ be a simple graph or a simple directed graph. A vertex $v$ is \emph{reachable} + from $u$ if some walk realized in $G$ runs from $u$ to $v$. In the undirected case + reachability is an equivalence relation on $\V{G}$; in the directed case it is only a + preorder, since walks cannot be reversed. +\end{definition} + +\begin{definition}[Symmetric orientation] + \label{def:symmetric-orientation} + \lean{AlgoLib.SimpleGraph.toSimpleDiGraph} + \leanok + The \emph{symmetric orientation} of a simple graph $G$ is the simple directed graph on + $\V{G}$ whose arcs are the ordered pairs $(u, v)$ with $\{u, v\} \in \E{G}$. A walk is + realized in $G$ exactly when it is realized in the symmetric orientation, so + reachability and distances agree. +\end{definition} + +\begin{definition}[Distance] + \label{def:dist} + \lean{AlgoLib.SimpleDiGraph.dist, AlgoLib.SimpleGraph.dist} + \leanok + \uses{def:reachable-directed, def:symmetric-orientation} + The \emph{distance} $\dist(u, v) \in \N \cup \{\infty\}$ from $u$ to $v$ in a simple + directed graph is the least length of a walk from $u$ to $v$, and $\infty$ if $v$ is not + reachable from $u$. For a simple graph it is the distance in the symmetric orientation, + and is then symmetric in $u$ and $v$. +\end{definition} From a177a1f6f5c5270ee24fedfa8ef3896f929a1210 Mon Sep 17 00:00:00 2001 From: nnhjy <43530784+nnhjy@users.noreply.github.com> Date: Fri, 18 Sep 2026 14:56:00 +0200 Subject: [PATCH 2/2] Address PR review: layering, single-run BFS distance, blueprint fix - Move the executable connectivity layer out of AlgoLib.Theory: the former Theory/Graph/Connectivity/Computable.lean is now Algorithms/Graph/Connectivity/Basic.lean, so no Theory module imports an Algorithms module. Umbrella docs, doc pointers, AlgoLib.lean and the blueprint TOC (new Connectivity section under Graph Algorithms) follow. - bfsDist no longer reruns the search per candidate index: one run collects the layers (bfsLayersFrom / bfsLayers) and bfsDist is the index of the first layer containing the vertex. Correctness restated via bfsDist_eq_coe_iff and eq_of_mem_bfsLayer; Finset.minENat no longer used. - Blueprint: the spheres proof now treats k = 0 separately, matching the Lean proof. Co-Authored-By: Claude Fable 5.1 --- AlgoLib.lean | 2 +- .../Graph/Connectivity/Basic.lean} | 6 + AlgoLib/Algorithms/Graph/Traversal/BFS.lean | 140 +++++++++++++++--- AlgoLib/Algorithms/Graph/Traversal/Basic.lean | 4 +- AlgoLib/Theory/Graph/Connectivity/Basic.lean | 23 +-- .../Graph/Connectivity/Connectivity.lean | 12 +- AlgoLib/Theory/Graph/Decidable.lean | 2 +- .../Algorithms/Graph/Connectivity/Basic.tex | 26 ++++ .../Algorithms/Graph/Traversal/Basic.tex | 10 +- 9 files changed, 184 insertions(+), 41 deletions(-) rename AlgoLib/{Theory/Graph/Connectivity/Computable.lean => Algorithms/Graph/Connectivity/Basic.lean} (97%) create mode 100644 blueprint/src/chapters/Algorithms/Graph/Connectivity/Basic.tex diff --git a/AlgoLib.lean b/AlgoLib.lean index a708cdc..4a06627 100644 --- a/AlgoLib.lean +++ b/AlgoLib.lean @@ -5,7 +5,6 @@ import AlgoLib.Theory.Graph.Basic' import AlgoLib.Theory.Graph.Coloring.Basic import AlgoLib.Theory.Graph.Connectivity.Basic import AlgoLib.Theory.Graph.Connectivity.Components -import AlgoLib.Theory.Graph.Connectivity.Computable import AlgoLib.Theory.Graph.Connectivity.Connectivity import AlgoLib.Theory.Graph.Connectivity.Cuts import AlgoLib.Theory.Graph.Connectivity.Directed @@ -64,6 +63,7 @@ import AlgoLib.Theory.Graph.Structures.Walk import AlgoLib.Theory.Graph.Subgraph -- Algorithms +import AlgoLib.Algorithms.Graph.Connectivity.Basic import AlgoLib.Algorithms.Graph.Flow.Basic import AlgoLib.Algorithms.Graph.MST.Basic import AlgoLib.Algorithms.Graph.SCC.Basic diff --git a/AlgoLib/Theory/Graph/Connectivity/Computable.lean b/AlgoLib/Algorithms/Graph/Connectivity/Basic.lean similarity index 97% rename from AlgoLib/Theory/Graph/Connectivity/Computable.lean rename to AlgoLib/Algorithms/Graph/Connectivity/Basic.lean index ebf2ca1..6d9006b 100644 --- a/AlgoLib/Theory/Graph/Connectivity/Computable.lean +++ b/AlgoLib/Algorithms/Graph/Connectivity/Basic.lean @@ -24,6 +24,12 @@ finite as *data* and whose edge set has decidable membership: Nothing in the `Set` / `ℕ∞`-valued development changes: those definitions are the specifications, and every definition here is proved *equal* to the one it computes. +This file lives under `AlgoLib.Algorithms`, not `AlgoLib.Theory`, because reachability is +decided by the breadth-first search of `AlgoLib.Algorithms.Graph.Traversal.BFS` and +everything else here depends on that decision procedure. The specifications it is checked +against are the theory umbrella `AlgoLib.Theory.Graph.Connectivity.Basic`; the theory tree +never imports the algorithms tree. + ## Main definitions * `SimpleGraph.reachableFinset G u` — the vertices reachable from `u`. diff --git a/AlgoLib/Algorithms/Graph/Traversal/BFS.lean b/AlgoLib/Algorithms/Graph/Traversal/BFS.lean index c555069..e20df68 100644 --- a/AlgoLib/Algorithms/Graph/Traversal/BFS.lean +++ b/AlgoLib/Algorithms/Graph/Traversal/BFS.lean @@ -5,7 +5,6 @@ Authors: Huang.JiangYi (co/ Claude Fable 5.1) -/ import AlgoLib.Theory.Graph.Decidable import AlgoLib.Theory.Graph.Connectivity.Directed -import AlgoLib.Util.Finset /-! # Breadth-first search @@ -32,6 +31,7 @@ arcs have decidable membership, and proves it correct against the specifications components. * `SimpleDiGraph.bfsReachableFinset G s` — the vertices reachable from `s`: the visited set after `|V(G)|` rounds. +* `SimpleDiGraph.bfsLayers G s` — the list of all layers, collected by one run. * `SimpleDiGraph.bfsDist G s v` — the distance from `s` to `v`: the index of the layer containing `v`, or `⊤` if there is none. @@ -62,8 +62,9 @@ arcs have decidable membership, and proves it correct against the specifications a partial function `α → ℕ∞`: the frontier *is* the current sphere, so the level invariant "every frontier vertex is at distance `k`" is a statement about a `Finset` and needs no bookkeeping over an accumulated map. The distance is read off afterwards - as the least layer index containing the vertex, using `Finset.minENat` from - `AlgoLib.Util.Finset` — the same device that makes the connectivity numbers compute. + as the index of the first layer containing the vertex, in the list of layers + `bfsLayers` that a single run of the search collects — so a distance query runs the + search once, not once per candidate index. * **Walks, not paths, in the correctness statements**, matching `dist`. Soundness builds a walk by appending one arc per round; completeness inducts on the `IsVertexSeqIn` derivation of an arbitrary walk, so no cycle erasure is ever needed. @@ -132,12 +133,28 @@ def bfsReachableFinset (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertex [DecidablePred (· ∈ G.edgeSet)] (s : α) : Finset α := G.bfsVisited s G.computeVertexFinset.card -/-- The distance from `s` to `v`, computed by breadth-first search: the least index of a -layer containing `v`, and `⊤` if no layer does. Only the indices below `|V(G)|` need to be -inspected, since no later layer is non-empty. -/ +/-- The first `m` layers of the search started in state `S`, collected along a single run: +`[S.frontier, (bfsStep S).frontier, …]`. -/ +def bfsLayersFrom (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] : ℕ → BFSState α → List (Finset α) + | 0, _ => [] + | m + 1, S => S.frontier :: G.bfsLayersFrom m (G.bfsStep S) + +/-- All the layers of the search from `s`, as the list `[L₀, …, L_{|V(G)|-1}]`, computed by +one run of the search. Every later layer is empty (`lt_card_of_nonempty_bfsLayer`), so +nothing is lost by stopping there. -/ +def bfsLayers (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] (s : α) : List (Finset α) := + G.bfsLayersFrom G.computeVertexFinset.card (G.bfsStart s) + +/-- The distance from `s` to `v`, computed by breadth-first search: the index of the first +layer containing `v`, and `⊤` if no layer does. The layers come from a single run of the +search (`bfsLayers`). -/ def bfsDist (G : SimpleDiGraph α) [DecidableEq α] [Fintype G.vertexSet] [DecidablePred (· ∈ G.edgeSet)] (s v : α) : ℕ∞ := - ((Finset.range G.computeVertexFinset.card).filter fun k => v ∈ G.bfsLayer s k).minENat + match (G.bfsLayers s).findIdx? (fun L => decide (v ∈ L)) with + | some k => k + | none => ⊤ variable {G : SimpleDiGraph α} [DecidableEq α] [Fintype G.vertexSet] [DecidablePred (· ∈ G.edgeSet)] {s v : α} @@ -400,18 +417,104 @@ theorem mem_bfsLayer_iff_dist_eq (k : ℕ) : v ∈ G.bfsLayer s k ↔ G.dist s v have hjk : j = k := by exact_mod_cast (dist_eq_of_mem_bfsLayer hvj).symm.trans hd exact hjk ▸ hvj +/-! ## The list of layers -/ + +lemma length_bfsLayersFrom (m : ℕ) (S : BFSState α) : (G.bfsLayersFrom m S).length = m := by + induction m generalizing S with + | zero => rfl + | succ m ih => simp [bfsLayersFrom, ih] + +/-- The `k`-th entry of the collected layers is the frontier after `k` rounds. -/ +lemma getElem_bfsLayersFrom (m : ℕ) (S : BFSState α) {k : ℕ} (hk : k < m) : + (G.bfsLayersFrom m S)[k]'(by rw [length_bfsLayersFrom]; exact hk) = + ((G.bfsStep)^[k] S).frontier := by + induction m generalizing S k with + | zero => exact absurd hk (Nat.not_lt_zero k) + | succ m ih => + cases k with + | zero => rfl + | succ k => + simp only [bfsLayersFrom, List.getElem_cons_succ, Function.iterate_succ_apply] + exact ih _ (Nat.lt_of_succ_lt_succ hk) + +@[simp] lemma length_bfsLayers : (G.bfsLayers s).length = G.computeVertexFinset.card := + length_bfsLayersFrom _ _ + +/-- The `k`-th collected layer is the `k`-th layer. -/ +lemma getElem_bfsLayers {k : ℕ} (hk : k < G.computeVertexFinset.card) : + (G.bfsLayers s)[k]'(by rw [length_bfsLayers]; exact hk) = G.bfsLayer s k := + getElem_bfsLayersFrom _ _ hk + +/-- The collected layers are exactly the layers of index below `|V(G)|`. -/ +lemma mem_bfsLayers_iff {L : Finset α} : + L ∈ G.bfsLayers s ↔ ∃ k < G.computeVertexFinset.card, G.bfsLayer s k = L := by + rw [List.mem_iff_getElem] + constructor + · rintro ⟨k, hk, rfl⟩ + rw [length_bfsLayers] at hk + exact ⟨k, hk, (getElem_bfsLayers hk).symm⟩ + · rintro ⟨k, hk, rfl⟩ + exact ⟨k, by rw [length_bfsLayers]; exact hk, getElem_bfsLayers hk⟩ + +/-! ## The computed distance -/ + +/-- Two layers of different index are disjoint: the later one avoids everything visited +before it, and the earlier one has been visited. -/ +lemma disjoint_bfsLayer_of_lt {j k : ℕ} (h : j < k) : + Disjoint (G.bfsLayer s j) (G.bfsLayer s k) := by + obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt h + exact Finset.disjoint_of_subset_left + ((bfsLayer_subset_bfsVisited j).trans (bfsVisited_mono (Nat.le_add_right j m))) + (disjoint_bfsLayer_succ_bfsVisited (j + m)).symm + +/-- A vertex lies in at most one layer. -/ +lemma eq_of_mem_bfsLayer {j k : ℕ} (hj : v ∈ G.bfsLayer s j) (hk : v ∈ G.bfsLayer s k) : + j = k := by + by_contra hne + rcases Nat.lt_or_gt_of_ne hne with h | h + · exact Finset.disjoint_left.1 (disjoint_bfsLayer_of_lt h) hj hk + · exact Finset.disjoint_left.1 (disjoint_bfsLayer_of_lt h) hk hj + +/-- The computed distance is `k` exactly when `v` lies in the `k`-th layer. -/ +theorem bfsDist_eq_coe_iff {k : ℕ} : G.bfsDist s v = k ↔ v ∈ G.bfsLayer s k := by + unfold bfsDist + rcases hfind : (G.bfsLayers s).findIdx? (fun L => decide (v ∈ L)) with _ | j + · simp only [ENat.top_ne_coe, false_iff] + intro hv + have hlt := lt_card_of_nonempty_bfsLayer ⟨v, hv⟩ + have := List.findIdx?_eq_none_iff.1 hfind _ (mem_bfsLayers_iff.2 ⟨k, hlt, rfl⟩) + simp [hv] at this + · obtain ⟨hj, hvj, -⟩ := List.findIdx?_eq_some_iff_getElem.1 hfind + rw [length_bfsLayers] at hj + rw [getElem_bfsLayers hj, decide_eq_true_iff] at hvj + simp only [Nat.cast_inj] + exact ⟨fun h => h ▸ hvj, fun hk => eq_of_mem_bfsLayer hvj hk⟩ + +/-- The computed distance is infinite exactly when no layer contains `v`. -/ +theorem bfsDist_eq_top_iff_forall : G.bfsDist s v = ⊤ ↔ ∀ k, v ∉ G.bfsLayer s k := by + constructor + · intro htop k hv + have := bfsDist_eq_coe_iff.2 hv + rw [htop] at this + exact ENat.top_ne_coe k this + · intro h + unfold bfsDist + rcases hfind : (G.bfsLayers s).findIdx? (fun L => decide (v ∈ L)) with _ | j + · rfl + · obtain ⟨hj, hvj, -⟩ := List.findIdx?_eq_some_iff_getElem.1 hfind + rw [length_bfsLayers] at hj + rw [getElem_bfsLayers hj, decide_eq_true_iff] at hvj + exact absurd hvj (h j) + /-- **BFS computes the distance.** -/ theorem bfsDist_eq_dist : G.bfsDist s v = G.dist s v := by - refine le_antisymm (le_dist_iff.2 fun w hw hhead htail => ?_) (Finset.le_minENat_iff.2 ?_) - · have htail' : w.val.tail = v := htail - have hvis := mem_bfsVisited_of_isVertexSeqIn hw hhead - rw [htail'] at hvis - obtain ⟨j, hj, hjlt, hvj⟩ := exists_bfsLayer_lt_card_of_mem_bfsVisited hvis - calc G.bfsDist s v ≤ (j : ℕ∞) := - Finset.minENat_le (Finset.mem_filter.2 ⟨Finset.mem_range.2 hjlt, hvj⟩) - _ ≤ (w.length : ℕ∞) := by exact_mod_cast hj - · intro k hk - exact dist_le_of_mem_bfsLayer (Finset.mem_filter.1 hk).2 + by_cases hr : G.Reachable s v + · obtain ⟨k, hk⟩ := WithTop.ne_top_iff_exists.1 (reachable_iff_dist_ne_top.1 hr) + rw [← hk] + exact bfsDist_eq_coe_iff.2 ((mem_bfsLayer_iff_dist_eq k).2 hk.symm) + · rw [dist_eq_top_iff.2 hr] + exact bfsDist_eq_top_iff_forall.2 fun k hk => + hr (reachable_of_mem_bfsVisited (bfsLayer_subset_bfsVisited k hk)) /-- The distance is infinite exactly when BFS never reaches the vertex. -/ theorem bfsDist_eq_top_iff : G.bfsDist s v = ⊤ ↔ v ∉ G.bfsReachableFinset s := by @@ -420,7 +523,7 @@ theorem bfsDist_eq_top_iff : G.bfsDist s v = ⊤ ↔ v ∉ G.bfsReachableFinset /-! ## Smoke tests Concrete evaluation on a small directed graph, confirming that the search really reduces -in the kernel. As in `AlgoLib.Theory.Graph.Connectivity.Computable`, the `Fintype` and +in the kernel. As in `AlgoLib.Algorithms.Graph.Connectivity.Basic`, the `Fintype` and `DecidablePred` instances of a concrete graph have to be given by hand. -/ section Examples @@ -445,6 +548,7 @@ example : cycleG.bfsLayer 0 2 = {2} := by decide example : cycleG.bfsLayer 0 3 = ∅ := by decide example : cycleG.bfsReachableFinset 0 = {0, 1, 2} := by decide example : cycleG.bfsReachableFinset 3 = {3} := by decide +example : cycleG.bfsLayers 0 = [{0}, {1}, {2}, ∅] := by decide example : cycleG.bfsDist 0 2 = 2 := by decide example : cycleG.bfsDist 2 1 = 2 := by decide example : cycleG.bfsDist 0 3 = ⊤ := by decide diff --git a/AlgoLib/Algorithms/Graph/Traversal/Basic.lean b/AlgoLib/Algorithms/Graph/Traversal/Basic.lean index 9444925..f1007e3 100644 --- a/AlgoLib/Algorithms/Graph/Traversal/Basic.lean +++ b/AlgoLib/Algorithms/Graph/Traversal/Basic.lean @@ -19,8 +19,8 @@ development, which is split across `AlgoLib/Algorithms/Graph/Traversal/`: Undirected graphs are traversed through their symmetric orientation `SimpleGraph.toSimpleDiGraph`; the undirected wrappers `SimpleGraph.reachableFinset` and -`SimpleGraph.computeDist` live in `AlgoLib.Theory.Graph.Connectivity.Computable`, next to -the specifications they compute. +`SimpleGraph.computeDist` live in `AlgoLib.Algorithms.Graph.Connectivity.Basic`, together +with the rest of the executable connectivity layer. Depth-first search is not yet implemented. -/ diff --git a/AlgoLib/Theory/Graph/Connectivity/Basic.lean b/AlgoLib/Theory/Graph/Connectivity/Basic.lean index 28eff9e..a49aba7 100644 --- a/AlgoLib/Theory/Graph/Connectivity/Basic.lean +++ b/AlgoLib/Theory/Graph/Connectivity/Basic.lean @@ -8,7 +8,6 @@ import AlgoLib.Theory.Graph.Connectivity.Directed import AlgoLib.Theory.Graph.Connectivity.Components import AlgoLib.Theory.Graph.Connectivity.Cuts import AlgoLib.Theory.Graph.Connectivity.Connectivity -import AlgoLib.Theory.Graph.Connectivity.Computable /-! # `AlgoLib.Theory.Graph.Connectivity` @@ -29,17 +28,19 @@ development, which is split across `AlgoLib/Theory/Connectivity/`: * `Cuts` — the edge boundary `∂(G, S)`, vertex and edge cuts, cut vertices and cut edges, and separators between vertices and between sets of vertices. * `Connectivity` — `κ(G)` and `κ'(G)`, with the `girth`-style infimum API. -* `Computable` — the computable reachability closure `reachableFinset` and distance - `computeDist`, both by the breadth-first search of - `AlgoLib.Algorithms.Graph.Traversal.BFS`, the connected components as a `Finset`, the - four connectivity numbers as executable definitions, and the `Decidable` instances for - reachability, connectedness, cuts and separating sets. + +The *executable* layer — the reachability closure `reachableFinset` and distance +`computeDist` by breadth-first search, the connected components as a `Finset`, the four +connectivity numbers as executable definitions, and the `Decidable` instances for +reachability, connectedness, cuts and separating sets — lives in +`AlgoLib.Algorithms.Graph.Connectivity.Basic`. It depends on the search algorithm of +`AlgoLib.Algorithms.Graph.Traversal.BFS`, which is why it is not part of this theory +umbrella: `AlgoLib.Theory` never imports `AlgoLib.Algorithms`. Downstream files should import this umbrella; the split is internal. The submodules form the acyclic spine `Reachable ← Components ← Cuts ← Connectivity`, on top of the deletion operations in `AlgoLib.Graph.Delete` and the walk development in -`AlgoLib.Theory.Structures.InSimpleGraph`; `Directed` sits beside `Reachable`, and -`Computable` closes the development by importing the search algorithm. +`AlgoLib.Theory.Structures.InSimpleGraph`; `Directed` sits beside `Reachable`. ## Main definitions @@ -61,9 +62,9 @@ Definitions based on lecture note "Graph Theory ETH 2026" by Benny Sudakov * `SimpleDiGraph.Reachable G u v`, `SimpleDiGraph.dist G u v`, `SimpleGraph.dist G u v` — directed reachability and the distance, the undirected one through `SimpleGraph.toSimpleDiGraph`. -* `SimpleGraph.reachableFinset G u` — the computable counterpart of `componentOf`, - `SimpleGraph.computeDist G u v` — the computable counterpart of `dist`, and - `SimpleGraph.computeVertexConnectivity G` — the computable counterpart of `κ(G)`. +* The computable counterparts `SimpleGraph.reachableFinset G u` (of `componentOf`), + `SimpleGraph.computeDist G u v` (of `dist`) and `SimpleGraph.computeVertexConnectivity G` + (of `κ(G)`) are in `AlgoLib.Algorithms.Graph.Connectivity.Basic`. ## Notation diff --git a/AlgoLib/Theory/Graph/Connectivity/Connectivity.lean b/AlgoLib/Theory/Graph/Connectivity/Connectivity.lean index 96a82b5..04fed1a 100644 --- a/AlgoLib/Theory/Graph/Connectivity/Connectivity.lean +++ b/AlgoLib/Theory/Graph/Connectivity/Connectivity.lean @@ -91,13 +91,15 @@ disconnects `G` or leaves at most one vertex. It is `⊤` exactly when no set of vertices does either — for instance in an infinite complete graph. See `IsVertexSeparating` for the convention on complete graphs. -The computable counterpart `computeVertexConnectivity` is available in `./Computable.lean`. -/ +The computable counterpart `computeVertexConnectivity` is available in +`AlgoLib.Algorithms.Graph.Connectivity.Basic`. -/ noncomputable def vertexConnectivity (G : SimpleGraph α) : ℕ∞ := ⨅ (S : Set α) (_ : G.IsVertexSeparating S), S.encard /-- The *edge connectivity* `κ'(G)`: the least number of edges whose deletion disconnects `G`, with the convention `κ'(G) = 0` when `G` has at most one vertex. -The computable counterpart `computeEdgeConnectivity` is available in `./Computable.lean`. -/ +The computable counterpart `computeEdgeConnectivity` is available in +`AlgoLib.Algorithms.Graph.Connectivity.Basic`. -/ noncomputable def edgeConnectivity (G : SimpleGraph α) : ℕ∞ := ⨅ (F : Set (Sym2 α)) (_ : G.IsEdgeSeparating F), F.encard @@ -279,13 +281,15 @@ comparison and are *degenerate on complete graphs*: `Kₙ` has no vertex cut at Degenerate on complete graphs, which have no vertex cut: `vertexCutNumber Kₙ = ⊤`, whereas `κ(Kₙ) = n - 1`. -The computable counterpart `computeVertexCutNumber` is available in `./Computable.lean`. -/ +The computable counterpart `computeVertexCutNumber` is available in +`AlgoLib.Algorithms.Graph.Connectivity.Basic`. -/ noncomputable def vertexCutNumber (G : SimpleGraph α) : ℕ∞ := ⨅ (S : Set α) (_ : G.IsVertexCut S), S.encard /-- The least size of an edge cut of `G`. Degenerate on graphs with at most one vertex, which have no edge cut. -The computable counterpart `computeEdgeCutNumber` is available in `./Computable.lean`. -/ +The computable counterpart `computeEdgeCutNumber` is available in +`AlgoLib.Algorithms.Graph.Connectivity.Basic`. -/ noncomputable def edgeCutNumber (G : SimpleGraph α) : ℕ∞ := ⨅ (F : Set (Sym2 α)) (_ : G.IsEdgeCut F), F.encard diff --git a/AlgoLib/Theory/Graph/Decidable.lean b/AlgoLib/Theory/Graph/Decidable.lean index 45e87ba..14a7bb2 100644 --- a/AlgoLib/Theory/Graph/Decidable.lean +++ b/AlgoLib/Theory/Graph/Decidable.lean @@ -20,7 +20,7 @@ procedures*: adjacency becomes decidable, and the deletion operations of graph, so that a predicate about `G.deleteVertices S` is decidable whenever the corresponding predicate about `G` is. -Reachability and connectedness are decided in `AlgoLib.Theory.Connectivity.Computable`, +Reachability and connectedness are decided in `AlgoLib.Algorithms.Graph.Connectivity.Basic`, on top of what is here and of the breadth-first search in `AlgoLib.Algorithms.Graph.Traversal.BFS`. diff --git a/blueprint/src/chapters/Algorithms/Graph/Connectivity/Basic.tex b/blueprint/src/chapters/Algorithms/Graph/Connectivity/Basic.tex new file mode 100644 index 0000000..a6177b7 --- /dev/null +++ b/blueprint/src/chapters/Algorithms/Graph/Connectivity/Basic.tex @@ -0,0 +1,26 @@ +% Mirrors `AlgoLib.Algorithms.Graph.Connectivity.Basic` +% +\begin{definition}[Computable reachability and distance] + \label{def:reachable-finset} + \lean{AlgoLib.SimpleGraph.reachableFinset, AlgoLib.SimpleGraph.computeDist} + \leanok + \uses{def:bfs-layers, def:symmetric-orientation} + For a simple graph $G$ with finite vertex set and decidable edge membership, the set of + vertices reachable from $u$ and the distance $\dist(u, v)$ are computed by running + breadth-first search from $u$ in the symmetric orientation of $G$. +\end{definition} + +\begin{theorem}[Correctness] + \label{thm:reachable-finset-correct} + \lean{AlgoLib.SimpleGraph.mem_reachableFinset_iff, AlgoLib.SimpleGraph.computeDist_eq} + \leanok + \uses{def:reachable-finset, def:reachable-directed, def:dist} + The computed set is exactly the set of vertices reachable from $u$, and the computed + distance is exactly $\dist(u, v)$. +\end{theorem} +\begin{proof} + \leanok + \uses{thm:bfs-correct} + Walks in $G$ and in its symmetric orientation are the same walks, so this is the + correctness of breadth-first search transported along that identification. +\end{proof} diff --git a/blueprint/src/chapters/Algorithms/Graph/Traversal/Basic.tex b/blueprint/src/chapters/Algorithms/Graph/Traversal/Basic.tex index 4eede5d..5435ebe 100644 --- a/blueprint/src/chapters/Algorithms/Graph/Traversal/Basic.tex +++ b/blueprint/src/chapters/Algorithms/Graph/Traversal/Basic.tex @@ -79,10 +79,12 @@ \subsection{Breadth-first search} \begin{proof} \leanok \uses{lem:bfs-sound, lem:bfs-complete} - 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$. + Let $v \in L_k$. Soundness gives $\dist(s, v) \le k$. For the reverse inequality there + is nothing to show when $k = 0$; when $k = j + 1$, a walk from $s$ to $v$ of length at + most $j$ would place $v$ in $V_j$ by completeness, whereas $L_{j+1}$ avoids $V_j$ by + construction, so $\dist(s, v) > j$, i.e. $\dist(s, v) \ge k$. 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$. \end{proof} \begin{theorem}[BFS computes reachability and distance]