/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
public import Mathlib.Combinatorics.SimpleGraph.Paths
public import Mathlib.Combinatorics.SimpleGraph.Walk.Counting@[expose] public sectionnamespace SimpleGraphvariable {V : Type*} {G : SimpleGraph V}open Finset ListTwo walks are internally disjoint if they share no vertices other than their endpoints.
def InternallyDisjoint {u v x y : V} (p : G.Walk u v) (q : G.Walk x y) : Prop :=
Disjoint p.support.tail.dropLast q.support.tail.dropLastWe say a graph is infinitely connected if any two vertices are connected by infinitely many pairwise disjoint paths. Note that graphs with at most one vertex are not classed as infinitely connected.
def InfinitelyConnected (G : SimpleGraph V) : Prop := Nontrivial V ∧
Pairwise fun u v ↦ ∃ P : Set (G.Walk u v),
P.Infinite ∧ (∀ p ∈ P, p.IsPath) ∧ P.Pairwise InternallyDisjoint
G is k-connected: it has more than k vertices, and it stays connected after the
removal of any set of fewer than k vertices.
Mathlib has SimpleGraph.IsEdgeConnected, but it has no vertex connectivity.
def IsKConnected {V : Type*} [Fintype V] (G : SimpleGraph V) (k : ℕ) : Prop :=
k < Fintype.card V ∧ ∀ S : Finset V, S.card < k → (G.induce ((S : Set V)ᶜ)).Connected
A graph on at most k vertices is not k-connected.
theorem not_isKConnected_of_card_le {V : Type*} [Fintype V] {G : SimpleGraph V} {k : ℕ}
(h : Fintype.card V ≤ k) : ¬ IsKConnected G k :=
fun hG => absurd hG.1 (not_lt.mpr h)Deciding reachability by breadth-first search
This section provides efficient decidability instances for reachability and (pre)connectedness of finite graphs through a breadth-first search (BFS) algorithm.
The algorithm is as follows: we maintain a finset of visited vertices which we grow with all its
neighbors at each round of breadth-first search at, stopping as soon as a round adds no new vertex:
a search costs O((diam G + 1) * (card V) ^ 2) adjacency tests.
Vertices u and v are then reachable if v lies in the BFS-constructed finset of vertices
reachable from u, and a graph is (pre)connected iff it's non-empty and (/empty or) every vertex is
lies in the reachability finset of an arbitrarily-chosen vertex.
section BFSvariable [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {m n : ℕ} {s t : Finset V} {u v w : V}variable (G s) in
One round of breadth-first search: G.bfsStep s consists of the vertices of s together with
their neighbours.
def bfsStep : Finset V := {w | w ∈ s ∨ ∃ v ∈ s, G.Adj v w}@[simp, grind =]
lemma mem_bfsStep : w ∈ G.bfsStep s ↔ w ∈ s ∨ ∃ v ∈ s, G.Adj v w := V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjs:Finset Vw:V⊢ w ∈ G.bfsStep s ↔ w ∈ s ∨ ∃ v ∈ s, G.Adj v w All goals completed! 🐙lemma subset_bfsStep : s ⊆ G.bfsStep s := fun _ hw ↦ G.mem_bfsStep.2 <| .inl hw@[gcongr] lemma bfsStep_mono (hst : s ⊆ t) : G.bfsStep s ⊆ G.bfsStep t := V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjs:Finset Vt:Finset Vhst:s ⊆ t⊢ G.bfsStep s ⊆ G.bfsStep t All goals completed! 🐙@[gcongr]
lemma iterate_bfsStep_mono (hst : s ⊆ t) : G.bfsStep^[n] s ⊆ G.bfsStep^[n] t := V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjn:ℕs:Finset Vt:Finset Vhst:s ⊆ t⊢ G.bfsStep^[n] s ⊆ G.bfsStep^[n] t
induction n generalizing s t with
V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjs:Finset Vt:Finset Vhst:s ⊆ t⊢ G.bfsStep^[0] s ⊆ G.bfsStep^[0] t All goals completed! 🐙
V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjn:ℕih:∀ {s t : Finset V}, s ⊆ t → G.bfsStep^[n] s ⊆ G.bfsStep^[n] ts:Finset Vt:Finset Vhst:s ⊆ t⊢ G.bfsStep^[n + 1] s ⊆ G.bfsStep^[n + 1] t All goals completed! 🐙lemma subset_iterate_bfsStep : s ⊆ G.bfsStep^[n] s := V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjn:ℕs:Finset V⊢ s ⊆ G.bfsStep^[n] s
induction n with
V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjn:ℕs:Finset V⊢ s ⊆ G.bfsStep^[0] s All goals completed! 🐙
V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjn✝:ℕs:Finset Vn:ℕih:s ⊆ G.bfsStep^[n] s⊢ s ⊆ G.bfsStep^[n + 1] s grw [V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjn✝:ℕs:Finset Vn:ℕih:s ⊆ G.bfsStep^[n] s⊢ s ⊆ G.bfsStep (G.bfsStep^[n] s) V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjn✝:ℕs:Finset Vn:ℕih:s ⊆ G.bfsStep^[n] s⊢ s ⊆ G.bfsStep s V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjn✝:ℕs:Finset Vn:ℕih:s ⊆ G.bfsStep^[n] s⊢ s ⊆ sAll goals completed! 🐙V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjm:ℕs:Finset Vk:ℕhmn:m ≤ m + k⊢ G.bfsStep^[m] s ⊆ G.bfsStep^[m] (G.bfsStep^[k] s)
All goals completed! 🐙V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adju:Vv:Vu✝:Vv✝:Vw✝:Vh:G.Adj u✝ v✝p:G.Walk v✝ w✝ih:w✝ ∈ G.bfsStep^[p.length] {v✝}⊢ w✝ ∈ G.bfsStep^[p.length] (G.bfsStep {u✝})
exact G.iterate_bfsStep_mono (V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adju:Vv:Vu✝:Vv✝:Vw✝:Vh:G.Adj u✝ v✝p:G.Walk v✝ w✝ih:w✝ ∈ G.bfsStep^[p.length] {v✝}⊢ {v✝} ⊆ G.bfsStep {u✝} All goals completed! 🐙) ihV:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adju:Vn:ℕih:∀ {v : V}, v ∈ G.bfsStep^[n] {u} → G.Reachable u vv:Vhv:v ∈ G.bfsStep^[n] {u} ∨ ∃ v_1 ∈ G.bfsStep^[n] {u}, G.Adj v_1 v⊢ G.Reachable u v
V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adju:Vn:ℕih:∀ {v : V}, v ∈ G.bfsStep^[n] {u} → G.Reachable u vv:Vhv:v ∈ G.bfsStep^[n] {u}⊢ G.Reachable u vV:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adju:Vn:ℕih:∀ {v : V}, v ∈ G.bfsStep^[n] {u} → G.Reachable u vv:Vw:Vhw:w ∈ G.bfsStep^[n] {u}hwv:G.Adj w v⊢ G.Reachable u v
V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adju:Vn:ℕih:∀ {v : V}, v ∈ G.bfsStep^[n] {u} → G.Reachable u vv:Vhv:v ∈ G.bfsStep^[n] {u}⊢ G.Reachable u v All goals completed! 🐙
V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adju:Vn:ℕih:∀ {v : V}, v ∈ G.bfsStep^[n] {u} → G.Reachable u vv:Vw:Vhw:w ∈ G.bfsStep^[n] {u}hwv:G.Adj w v⊢ G.Reachable u v All goals completed! 🐙
Iterate G.bfsStep at most n times, stopping as soon as no new vertex shows up.
def bfsIterate : ℕ → Finset V → Finset V
| 0, s => s
| n + 1, s => if (G.bfsStep s).card ≤ s.card then s else bfsIterate n (G.bfsStep s)All goals completed! 🐙
The finset of vertices reachable from u, computed by breadth-first search.
def reachableFinset (u : V) : Finset V := G.bfsIterate (Fintype.card V) {u}V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adju:Vv:V⊢ v ∈ G.bfsStep^[Fintype.card V] {u} ↔ G.Reachable u v
V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adju:Vv:Vh:G.Reachable u vp:G.Path u v⊢ v ∈ G.bfsStep^[Fintype.card V] {u}
All goals completed! 🐙
Decides reachability of vertices u and v by performing a breadth-first search from u.
instance decidableReachable : DecidableRel G.Reachable :=
fun _ _ ↦ decidable_of_iff _ G.mem_reachableFinsetlemma preconnected_iff_forall_mem_reachableFinset (u : V) :
G.Preconnected ↔ ∀ v, v ∈ G.reachableFinset u := V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adju:V⊢ G.Preconnected ↔ ∀ (v : V), v ∈ reachableFinset u
V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adju:V⊢ G.Preconnected ↔ ∀ (v : V), G.Reachable u v
All goals completed! 🐙
Decides preconnectedness of G by checking whether the vertex set is empty and, if not,
by performing a breadth-first search from an arbitrarily chosen vertex.
V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjm:ℕn:ℕs:Finset Vt:Finset Vu:Vv:Vw:Vh:IsEmpty V⊢ G.Preconnected; All goals completed! 🐙)
else
(truncOfCardPos <| V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjm:ℕn:ℕs:Finset Vt:Finset Vu:Vv:Vw:Vh:¬Fintype.card V = 0⊢ 0 < Fintype.card V All goals completed! 🐙).lift
(fun u ↦ decidable_of_iff _ (G.preconnected_iff_forall_mem_reachableFinset u).symm)
fun _ _ ↦ Subsingleton.elim _ _All goals completed! 🐙
Decides preconnectedness of G by checking whether the vertex set is empty and, if not,
by performing a breadth-first search from an arbitrarily chosen vertex.
instance decidableConnected : Decidable G.Connected :=
if h : Fintype.card V = 0 then
isFalse fun hG ↦ (Fintype.card_eq_zero_iff.1 h).false hG.nonempty.some
else
(truncOfCardPos <| V:Type u_1G:SimpleGraph Vinst✝²:Fintype Vinst✝¹:DecidableEq Vinst✝:DecidableRel G.Adjm:ℕn:ℕs:Finset Vt:Finset Vu:Vv:Vw:Vh:¬Fintype.card V = 0⊢ 0 < Fintype.card V All goals completed! 🐙).lift
(fun u ↦ decidable_of_iff _ (G.connected_iff_forall_mem_reachableFinset u).symm)
fun _ _ ↦ Subsingleton.elim ..end BFSend SimpleGraph