Grace/Cumulus/GraphTheory/Connectivity.g17

Open in Workbench Download source

Imports

Reachability

Declarations

Source

1-- Finite reachability, connected components, and their partition laws.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.GraphTheory.Connectivity8import Reachability910-- Closure is relative to V; it also makes sense for directed graphs.11predicate EdgeClosed (V E A : Set) :=12  ∀ u ∈ A, ∀ v ∈ V, Adjacent(E, u, v) → v ∈ A1314-- One induction covers all finite lengths and arbitrary vertex sets.15theorem reachableWithin.in_closed_set (V E x A : Set, n : Nat)16  requires start : x ∈ A17  requires closed : EdgeClosed(V, E, A)18  shows reachableWithin(V, E, x, n) ⊆ A19proof20  induction n21  | zero =>22    rw reachableWithin.zero23    intros y member24    have equality := singleton.membership.forward with member25    rw equality26    exact start27  | succ(k) using ih =>28    rw reachableWithin.successor29    intros y member30    have alternatives := union2.membership.forward at y,31      reachableWithin(V, E, x, k), nextNeighbors(V, E, reachableWithin(V, E, x, k)) with member32    cases alternatives with old | new33      exact ih with y, old34    . have parts := nextNeighbors.membership.forward at V, E, reachableWithin(V, E, x, k), y with new35      rcases parts with ⟨hy, z, hz, edge⟩36      have zInA := ih with z, hz37      exact closed with z, zInA, y, hy, edge3839theorem Reachable.in_closed_set (V E x y A : Set)40  requires start : x ∈ A41  requires closed : EdgeClosed(V, E, A)42  requires path : Reachable(V, E, x, y)43  shows y ∈ A44proof45  rcases path with ⟨n, hn, reached⟩46  have nNat := nat.omega.backward with hn47  have included := reachableWithin.in_closed_set with nNat, start, closed48  exact included with y, reached4950theorem Reachable.vertex (V E x y : Set)51  requires hx : x ∈ V52  requires path : Reachable(V, E, x, y)53  shows y ∈ V54proof55  have closed : EdgeClosed(V, E, V)56    intros u hu v hv edge57    exact hv58  exact Reachable.in_closed_set with hx, closed, path5960theorem Reachable.extend (V E x y z : Set)61  requires path : Reachable(V, E, x, y)62  requires hz : z ∈ V63  requires edge : Adjacent(E, y, z)64  shows Reachable(V, E, x, z)65proof66  rcases path with ⟨n, hn, reached⟩67  have nNat := nat.omega.backward with hn68  have nextNat := Naturals.constructor.succ with nNat69  have nextIn := nat.omega.forward with nextNat70  have next := reachableWithin.advance with nNat, reached, hz, edge71  unfold Reachable72  refine ⟨succ(n), nextIn, next⟩7374-- Separation gives a set even when the graph is infinite.75def component (V E x : Set) : Set := { y ∈ V | Reachable(V, E, x, y) }7677theorem component.source (V E x : Set)78  requires hx : x ∈ V79  shows x ∈ component(V, E, x)80proof81  apply component.membership.backward82  have path := Reachable.reflexive at V, E, x83  refine ⟨hx, path⟩8485theorem component.closed (V E x : Set)86  shows EdgeClosed(V, E, component(V, E, x))87proof88  intros u hu v hv edge89  obtain ⟨uInV, reached⟩ := component.membership.forward with hu90  have extended := Reachable.extend with reached, hv, edge91  exact component.membership.backward with ⟨hv, extended⟩9293theorem component.minimal (V E x A : Set)94  requires start : x ∈ A95  requires closed : EdgeClosed(V, E, A)96  shows component(V, E, x) ⊆ A97proof98  intros y member99  obtain ⟨hy, path⟩ := component.membership.forward with member100  exact Reachable.in_closed_set with start, closed, path101102theorem Reachable.transitive (V E x y z : Set)103  requires hy : y ∈ V104  requires first : Reachable(V, E, x, y)105  requires second : Reachable(V, E, y, z)106  shows Reachable(V, E, x, z)107proof108  have start : y ∈ component(V, E, x) := component.membership.backward with ⟨hy, first⟩109  have member := Reachable.in_closed_set with start, second110  obtain ⟨hz, path⟩ := component.membership.forward with member111  exact path112113-- Reversal is proved at every finite length, using concatenation above.114theorem reachableWithin.reverse (V E x : Set, n : Nat)115  requires graph : SimpleGraph(V, E)116  requires hx : x ∈ V117  shows ∀ y ∈ reachableWithin(V, E, x, n), Reachable(V, E, y, x)118proof119  induction n120  | zero =>121    intros y member122    rw reachableWithin.zero at member123    have equality := singleton.membership.forward with member124    rw equality125    exact Reachable.reflexive126  | succ(k) using ih =>127    intros y member128    rw reachableWithin.successor at member129    have alternatives := union2.membership.forward at y,130      reachableWithin(V, E, x, k), nextNeighbors(V, E, reachableWithin(V, E, x, k)) with member131    cases alternatives with old | new132    . exact ih with y, old133    . have parts := nextNeighbors.membership.forward at V, E, reachableWithin(V, E, x, k), y with new134      rcases parts with ⟨hy, z, hz, edge⟩135      have back := ih with z, hz136      have reverseEdge := Adjacent.symmetric with graph, edge137      have bounds := Adjacent.bounds with graph, edge138      rcases bounds with ⟨zInV, yInV⟩139      have first := Reachable.of_edge with zInV, reverseEdge140      exact Reachable.transitive with zInV, first, back141142theorem Reachable.symmetric (V E x y : Set)143  requires graph : SimpleGraph(V, E)144  requires hx : x ∈ V145  requires path : Reachable(V, E, x, y)146  shows Reachable(V, E, y, x)147proof148  rcases path with ⟨n, hn, reached⟩149  have nNat := nat.omega.backward with hn150  have reverse := reachableWithin.reverse with nNat, graph, hx151  exact reverse with y, reached152153theorem component.subset_vertices (V E x : Set)154  shows component(V, E, x) ⊆ V155proof156  intros y member157  obtain ⟨hy, path⟩ := component.membership.forward with member158  exact hy159160theorem component.equal_of_reachable (V E x y : Set)161  requires graph : SimpleGraph(V, E)162  requires hx : x ∈ V163  requires hy : y ∈ V164  requires path : Reachable(V, E, x, y)165  shows component(V, E, x) = component(V, E, y)166proof167  have back := Reachable.symmetric with graph, hx, path168  ext z169  constructor170  . intro member171    obtain ⟨hz, xz⟩ := component.membership.forward with member172    have yz := Reachable.transitive with hx, back, xz173    exact component.membership.backward with ⟨hz, yz⟩174  . intro member175    obtain ⟨hz, yz⟩ := component.membership.forward with member176    have xz := Reachable.transitive with hy, path, yz177    exact component.membership.backward with ⟨hz, xz⟩178179theorem component.equal_iff (V E x y : Set)180  requires graph : SimpleGraph(V, E)181  requires hx : x ∈ V182  requires hy : y ∈ V183  shows component(V, E, x) = component(V, E, y) ↔ Reachable(V, E, x, y)184proof185  constructor186  . intro equality187    have member := component.source at V, E, y with hy188    rw ← equality at member189    obtain ⟨yInV, path⟩ := component.membership.forward with member190    exact path191  . intro path192    exact component.equal_of_reachable with graph, hx, hy, path193194theorem component.equal_of_common_vertex (V E x y z : Set)195  requires graph : SimpleGraph(V, E)196  requires hx : x ∈ V197  requires hy : y ∈ V198  requires first : z ∈ component(V, E, x)199  requires second : z ∈ component(V, E, y)200  shows component(V, E, x) = component(V, E, y)201proof202  have partsX := component.membership.forward with first203  have partsY := component.membership.forward with second204  rcases partsX with ⟨hz, xz⟩205  rcases partsY with ⟨hz2, yz⟩206  have firstEqual := component.equal_of_reachable with graph, hx, hz, xz207  have secondEqual := component.equal_of_reachable with graph, hy, hz, yz208  rw firstEqual209  symm210  exact secondEqual211212theorem component.equal_or_disjoint (V E x y : Set)213  requires graph : SimpleGraph(V, E)214  requires hx : x ∈ V215  requires hy : y ∈ V216  shows component(V, E, x) = component(V, E, y) ∨217    Disjoint(component(V, E, x), component(V, E, y))218proof219  have alternatives : component(V, E, x) = component(V, E, y) ∨ component(V, E, x) ≠ component(V, E, y) by tauto220  cases alternatives with equal | different221  . left222    exact equal223  . right224    unfold Disjoint225    ext z226    constructor227    . intro member228      obtain ⟨first, second⟩ := intersection.membership.forward with member229      exfalso230      apply different231      exact component.equal_of_common_vertex with graph, hx, hy, first, second232    . intro impossible233      exfalso234      exact set.empty with impossible235236predicate GraphConnected (V E : Set) :=237  ∀ x ∈ V, ∀ y ∈ V, Reachable(V, E, x, y)238239theorem component.connected (V E x : Set)240  requires graph : SimpleGraph(V, E)241  requires hx : x ∈ V242  shows ∀ u ∈ component(V, E, x), ∀ v ∈ component(V, E, x), Reachable(V, E, u, v)243proof244  intros u hu v hv245  have partsU := component.membership.forward with hu246  have partsV := component.membership.forward with hv247  rcases partsU with ⟨uInV, xu⟩248  rcases partsV with ⟨vInV, xv⟩249  have ux := Reachable.symmetric with graph, hx, xu250  exact Reachable.transitive with hx, ux, xv251252theorem GraphConnected.component (V E x : Set)253  requires connected : GraphConnected(V, E)254  requires hx : x ∈ V255  shows component(V, E, x) = V256proof257  ext y258  constructor259  . intro member260    have included := component.subset_vertices at V, E, x261    exact included with y, member262  . intro hy263    have path := connected with x, hx, y, hy264    exact component.membership.backward with ⟨hy, path⟩265266theorem GraphConnected.of_component (V E x : Set)267  requires graph : SimpleGraph(V, E)268  requires hx : x ∈ V269  requires entire : component(V, E, x) = V270  shows GraphConnected(V, E)271proof272  have connected := component.connected with graph, hx273  intros u hu v hv274  rw ← entire at hu275  rw ← entire at hv276  exact connected with u, hu, v, hv277278-- This set of sets is the component partition, bounded by the powerset.279def components (V E : Set) : Set :=280  { A ∈ 𝒫(V) | ∃ x ∈ V, A = component(V, E, x) }281282theorem components.contains (V E x : Set)283  requires hx : x ∈ V284  shows component(V, E, x) ∈ components(V, E)285proof286  have included := component.subset_vertices at V, E, x287  unfold Subset at included288  have inPower := set.powerset.backward with included289  exact components.membership.backward with ⟨inPower, x, hx, rfl⟩290291theorem components.nonempty_members (V E A : Set)292  requires member : A ∈ components(V, E)293  shows ∃ x ∈ A, x ∈ V294proof295  obtain ⟨inPower, x, hx, equality⟩ := components.membership.forward with member296  have source := component.source at V, E, x with hx297  rw ← equality at source298  refine ⟨x, source, hx⟩299300theorem components.cover (V E : Set)301  shows ⋃(components(V, E)) = V302proof303  ext x304  constructor305  . intro member306    obtain ⟨A, inFamily, inA⟩ := set.union.forward with member307    obtain ⟨inPower, witness⟩ := components.membership.forward with inFamily308    have included := set.powerset.forward with inPower309    exact included with x, inA310  . intro hx311    have inFamily := components.contains at V, E, x with hx312    have inComponent := component.source at V, E, x with hx313    exact union.contains with inFamily, inComponent314315theorem components.equal_or_disjoint (V E A B : Set)316  requires graph : SimpleGraph(V, E)317  requires first : A ∈ components(V, E)318  requires second : B ∈ components(V, E)319  shows A = B ∨ Disjoint(A, B)320proof321  have partsA := components.membership.forward with first322  have partsB := components.membership.forward with second323  rcases partsA with ⟨powerA, x, hx, equalityA⟩324  rcases partsB with ⟨powerB, y, hy, equalityB⟩325  rw [equalityA, equalityB]326  exact component.equal_or_disjoint with graph, hx, hy327328-- A route starting in an edge-closed set never needs to leave that set.329theorem reachableWithin.restrict_closed (V E x A : Set, n : Nat)330  requires start : x ∈ A331  requires closed : EdgeClosed(V, E, A)332  shows ∀ y ∈ reachableWithin(V, E, x, n), Reachable(A, inducedEdges(E, A), x, y)333proof334  induction n335  | zero =>336    intros y member337    rw reachableWithin.zero at member338    have equality := singleton.membership.forward with member339    rw equality340    exact Reachable.reflexive341  | succ(k) using ih =>342    intros y member343    rw reachableWithin.successor at member344    have alternatives := union2.membership.forward with member345    cases alternatives with old | new346    . exact ih with y, old347    . have parts := nextNeighbors.membership.forward at V, E, reachableWithin(V, E, x, k), y with new348      rcases parts with ⟨hy, z, hz, edge⟩349      have previous := ih with z, hz350      have included := reachableWithin.in_closed_set with start, closed351      have zInA := included with z, hz352      have yInA := closed with z, zInA, y, hy, edge353      have restricted : Adjacent(inducedEdges(E, A), z, y)354        unfold Adjacent355        exact inducedEdges.membership.backward with ⟨edge, zInA, yInA⟩356      exact Reachable.extend with previous, yInA, restricted357358theorem Reachable.restrict_closed (V E x y A : Set)359  requires start : x ∈ A360  requires closed : EdgeClosed(V, E, A)361  requires path : Reachable(V, E, x, y)362  shows Reachable(A, inducedEdges(E, A), x, y)363proof364  rcases path with ⟨n, hn, reached⟩365  have nNat := nat.omega.backward with hn366  have restricted := reachableWithin.restrict_closed with nNat, start, closed367  exact restricted with y, reached368369theorem component.induced_connected (V E x : Set)370  requires graph : SimpleGraph(V, E)371  requires hx : x ∈ V372  shows GraphConnected(component(V, E, x), inducedEdges(E, component(V, E, x)))373proof374  intros u hu v hv375  have connected := component.connected with graph, hx376  have path := connected with u, hu, v, hv377  exact Reachable.restrict_closed with hu, path378379theorem component.induced_graph (V E x : Set)380  requires graph : SimpleGraph(V, E)381  shows SimpleGraph(component(V, E, x), inducedEdges(E, component(V, E, x)))382proof383  have included := component.subset_vertices at V, E, x384  exact inducedEdges.graph with graph, included385386theorem component.no_crossing_edge (V E x u v : Set)387  requires inside : u ∈ component(V, E, x)388  requires hv : v ∈ V389  requires outside : ¬(v ∈ component(V, E, x))390  shows ¬Adjacent(E, u, v)391proof392  intro edge393  have closed := component.closed at V, E, x394  apply outside395  exact closed with u, inside, v, hv, edge396397theorem GraphConnected.closed_set (V E A x : Set)398  requires connected : GraphConnected(V, E)399  requires included : A ⊆ V400  requires start : x ∈ A401  requires closed : EdgeClosed(V, E, A)402  shows A = V403proof404  have hx := included with x, start405  have entire := GraphConnected.component with connected, hx406  have minimal := component.minimal with start, closed407  rw entire at minimal408  ext y409  constructor410  . intro hy411    exact included with y, hy412  . intro hy413    exact minimal with y, hy414415theorem component.empty_graph (V x : Set)416  requires hx : x ∈ V417  shows component(V, empty, x) = {x}418proof419  have closed : EdgeClosed(V, empty, {x})420    intros u hu v hv edge421    exfalso422    unfold Adjacent at edge423    unfold relates at edge424    exact set.empty with edge425  have start := singleton.self at x426  have minimal := component.minimal with start, closed427  ext y428  constructor429  . intro member430    exact minimal with y, member431  . intro member432    have equality := singleton.membership.forward with member433    rw equality434    exact component.source with hx435436theorem completeEdges.connected (V : Set)437  shows GraphConnected(V, completeEdges(V))438proof439  intros x hx y hy440  have alternatives : x = y ∨ x ≠ y by tauto441  cases alternatives with equal | distinct442  . rw equal443    exact Reachable.reflexive444  . apply Reachable.of_edge at V, completeEdges(V), x, y445    . exact hy446    . apply completeEdges.adjacent.backward at V, x, y447      refine ⟨hx, hy, distinct⟩448449-- This characterization also applies to directed graphs: GraphConnected450-- means that every vertex reaches every other vertex.451theorem GraphConnected.iff_closed_sets (V E : Set)452  shows GraphConnected(V, E) ↔453    (∀ A, A ⊆ V → EdgeClosed(V, E, A) → (A = ∅ ∨ A = V))454proof455  constructor456  . intros connected A included closed457    have alternatives : A = ∅ ∨ A ≠ ∅ by tauto458    cases alternatives with vacant | nonempty459    . left460      exact vacant461    . right462      have inhabited := Nonempty.of_ne_empty at A with *463      rcases inhabited with ⟨x, start⟩464      exact GraphConnected.closed_set at V, E, A, x with *465  . intros closedSets x hx y hy466    have included := component.subset_vertices at V, E, x467    have closed := component.closed at V, E, x468    have start := component.source at V, E, x with *469    have alternatives := closedSets with component(V, E, x), included, closed470    cases alternatives with vacant | entire471    . exfalso472      rw vacant at start473      exact set.empty with start474    . have member : y ∈ component(V, E, x)475        rwa entire476      have parts := component.membership.forward at V, E, x, y with *477      rcases parts with ⟨vertex, path⟩478      exact path479480theorem GraphConnected.no_closed_cut (V E A : Set)481  requires included : A ⊆ V482  requires inhabited : Nonempty(A)483  requires proper : A ≠ V484  requires closed : EdgeClosed(V, E, A)485  shows ¬GraphConnected(V, E)486proof487  intro connected488  rcases inhabited with ⟨x, start⟩489  have entire := GraphConnected.closed_set with *490  exact proper with entire491492-- Every nontrivial cut of a connected graph has an outgoing crossing edge.493theorem GraphConnected.crossing_edge (V E A : Set)494  requires connected : GraphConnected(V, E)495  requires included : A ⊆ V496  requires inhabited : Nonempty(A)497  requires proper : A ≠ V498  shows ∃ u ∈ A, ∃ v ∈ V, ¬(v ∈ A) ∧ Adjacent(E, u, v)499proof500  by_contra noCrossing501  have closed : EdgeClosed(V, E, A)502    intros u hu v hv edge503    by_contra outside504    apply noCrossing505    refine ⟨u, hu, v, hv, outside, edge⟩506  have disconnected := GraphConnected.no_closed_cut with *507  exact disconnected with connected508509-- Connectivity is equivalent to an outgoing edge across every nontrivial cut.510theorem GraphConnected.iff_crossing_cuts (V E : Set)511  shows GraphConnected(V, E) ↔512    (∀ A, A ⊆ V → Nonempty(A) → A ≠ V →513      ∃ u ∈ A, ∃ v ∈ V, ¬(v ∈ A) ∧ Adjacent(E, u, v))514proof515  constructor516  . intros connected A included inhabited proper517    exact GraphConnected.crossing_edge with *518  . intro crossingCuts519    apply GraphConnected.iff_closed_sets.backward520    intros A included closed521    have alternatives : A = ∅ ∨ A ≠ ∅ by tauto522    cases alternatives with vacant | nonempty523    . left524      exact vacant525    . right526      by_contra proper527      have inhabited := Nonempty.of_ne_empty with *528      obtain ⟨u, hu, v, hv, outside, edge⟩ := crossingCuts with A, included, inhabited, proper529      have inside := closed with u, hu, v, hv, edge530      exact outside with inside531