Grace/Cumulus/GraphTheory/Multigraph/Connectivity.g17

Open in Workbench Download source

Imports

Cuts

Declarations

Source

1-- Connectivity through an edge set: two vertices are joined when a path of2-- edges of F links them, the component of a vertex collects the vertices3-- joined to it, and the components of F partition the vertex set.4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.GraphTheory.Multigraph.Connectivity10import Cuts1112-- A vertex set that no edge of F leaves.13predicate ClosedUnder (leftEnd rightEnd F A : Set) :=14  ∀ e ∈ F, (leftEnd(e) ∈ A ↔ rightEnd(e) ∈ A)1516-- v is reached from u along edges of F: every closed set containing u17-- contains v.18predicate Joined (leftEnd rightEnd F u v : Set) :=19  ∀ A, u ∈ A → ClosedUnder(leftEnd, rightEnd, F, A) → v ∈ A2021predicate Connects (V leftEnd rightEnd F : Set) :=22  ∀ u ∈ V, ∀ v ∈ V, Joined(leftEnd, rightEnd, F, u, v)2324-- The component of u: the vertices joined to u along F.25def componentBy (V leftEnd rightEnd F u : Set) : Set :=26  { v ∈ V | Joined(leftEnd, rightEnd, F, u, v) }2728def componentsBy (V leftEnd rightEnd F : Set) : Set :=29  { componentBy(V, leftEnd, rightEnd, F, u) | u ∈ V }3031theorem Joined.reflexive (leftEnd rightEnd F u : Set)32  shows Joined(leftEnd, rightEnd, F, u, u)33proof34  intros A start closed35  exact start3637theorem Joined.of_edge (leftEnd rightEnd F e : Set)38  requires edge : e ∈ F39  shows Joined(leftEnd, rightEnd, F, leftEnd(e), rightEnd(e))40proof41  intros A start closed42  have crossed := closed with e, edge43  exact crossed.forward with start4445theorem Joined.of_edge_reverse (leftEnd rightEnd F e : Set)46  requires edge : e ∈ F47  shows Joined(leftEnd, rightEnd, F, rightEnd(e), leftEnd(e))48proof49  intros A start closed50  have crossed := closed with e, edge51  exact crossed.backward with start5253theorem Joined.transitive (leftEnd rightEnd F u v w : Set)54  requires first : Joined(leftEnd, rightEnd, F, u, v)55  requires second : Joined(leftEnd, rightEnd, F, v, w)56  shows Joined(leftEnd, rightEnd, F, u, w)57proof58  intros A start closed59  have middle := first with A, start, closed60  exact second with A, middle, closed6162theorem Joined.monotone (leftEnd rightEnd F G u v : Set)63  requires subset : F ⊆ G64  requires joined : Joined(leftEnd, rightEnd, F, u, v)65  shows Joined(leftEnd, rightEnd, G, u, v)66proof67  intros A start closed68  have closedF : ClosedUnder(leftEnd, rightEnd, F, A)69    intros e edge70    exact closed with e, (subset with e, edge)71  exact joined with A, start, closedF7273-- Symmetry: the vertices joined to u form a closed set containing u, so it74-- contains every vertex that u is joined to.75def joinedTo (V leftEnd rightEnd F u : Set) : Set :=76  { w ∈ V | Joined(leftEnd, rightEnd, F, w, u) }7778theorem joinedTo.closed (V leftEnd rightEnd F u : Set)79  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V80  shows ClosedUnder(leftEnd, rightEnd, F, joinedTo(V, leftEnd, rightEnd, F, u))81proof82  intros e edge83  obtain ⟨leftV, rightV⟩ := ends with e, edge84  constructor85  . intro member86    exact ⟨rightV, (Joined.transitive87      with (Joined.of_edge_reverse with edge), member.right)⟩88  . intro member89    exact ⟨leftV, (Joined.transitive90      with (Joined.of_edge with edge), member.right)⟩9192theorem Joined.symmetric (V leftEnd rightEnd F u v : Set)93  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V94  requires first : u ∈ V95  requires second : v ∈ V96  requires joined : Joined(leftEnd, rightEnd, F, u, v)97  shows Joined(leftEnd, rightEnd, F, v, u)98proof99  have reached := joined with joinedTo(V, leftEnd, rightEnd, F, u),100    ⟨first, Joined.reflexive⟩, (joinedTo.closed with ends)101  exact reached.right102103-- A vertex outside V is a closed set on its own, so it is joined to nothing104-- else.105theorem Joined.start_in (V leftEnd rightEnd F u v : Set)106  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V107  requires distinct : u ≠ v108  requires joined : Joined(leftEnd, rightEnd, F, u, v)109  shows u ∈ V110proof111  by_contra outside112  have closed : ClosedUnder(leftEnd, rightEnd, F, {u})113    intros e edge114    have bounds := ends with e, edge115    simp116  have reached := joined with {u}, singleton.self, closed117  simp at reached118  cc119120-- A single non-loop edge has odd degree exactly at its two ends.121theorem degreeIn.single_parity (leftEnd rightEnd e : Set)122  requires distinct : leftEnd(e) ≠ rightEnd(e)123  shows ∀ x, (Even(degreeIn(leftEnd, rightEnd, {e}, x)) ↔124    (x ≠ leftEnd(e) ∧ x ≠ rightEnd(e)))125proof126  intro x127  by_cases hit : leftEnd(e) = x ∨ rightEnd(e) = x128  . rw degreeIn.end with distinct, hit129    simp [Even.not_one]130  . have notLeft : leftEnd(e) ≠ x by tauto131    have notRight : rightEnd(e) ≠ x by tauto132    rw degreeIn.absent with notLeft, notRight133    simp [Even.zero]134135-- The vertices reached from u by a path along F, with u itself: w ≠ u is136-- reached when some P ⊆ F has odd degree exactly at u and w.137def pathReached (V leftEnd rightEnd F u : Set) : Set :=138  { w ∈ V | w = u ∨ ∃ P ⊆ F, ∀ x ∈ V,139    (Even(degreeIn(leftEnd, rightEnd, P, x)) ↔ (x ≠ u ∧ x ≠ w)) }140141-- An edge with ends a and b carries a path from u to a on to b: the edge142-- alone when a = u, and otherwise the symmetric difference with the edge.143theorem pathReached.step (V leftEnd rightEnd F u e a b : Set)144  requires finite : Finite(F)145  requires edge : e ∈ F146  requires distinct : a ≠ b147  requires vertex : b ∈ V148  requires parity : ∀ x, (Even(degreeIn(leftEnd, rightEnd, {e}, x)) ↔149    (x ≠ a ∧ x ≠ b))150  requires reached : a ∈ pathReached(V, leftEnd, rightEnd, F, u)151  shows b ∈ pathReached(V, leftEnd, rightEnd, F, u)152proof153  have single : {e} ⊆ F := singleton.subset_iff.backward with edge154  refine ⟨vertex, _⟩155  by_cases start : a = u156  . right157    witness {e}158    refine ⟨single, _⟩159    intros x inV160    rw ← start161    exact parity with x162  rcases reached with ⟨_, same | ⟨P, subset, parityP⟩⟩163  . contradiction164  by_cases finish : b = u165  . left166    exact finish167  right168  witness P △ {e}169  refine ⟨(symmetricDifference.subset with subset, single), _⟩170  intros x inV171  have finiteP := Finite.subset with finite, subset172  have atP := parityP with x, inV173  have atEdge := parity with x174  -- P and {e} are both odd at a, so their sum is odd exactly at u and b.175  rw degreeIn.symmetricDifference_parity with finiteP, (Finite.singleton at e)176  simp [atP, atEdge]177178theorem pathReached.closed (V leftEnd rightEnd F u : Set)179  requires finite : Finite(F)180  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V181  shows ClosedUnder(leftEnd, rightEnd, F,182    pathReached(V, leftEnd, rightEnd, F, u))183proof184  intros e edge185  have bounds := ends with e, edge186  by_cases loop : leftEnd(e) = rightEnd(e)187  . simp [loop]188  have parity := degreeIn.single_parity with loop189  have flipped : ∀ x, (Even(degreeIn(leftEnd, rightEnd, {e}, x)) ↔190      (x ≠ rightEnd(e) ∧ x ≠ leftEnd(e)))191    intro x192    have direct := parity with x193    tauto194  have reverse : rightEnd(e) ≠ leftEnd(e) by cc195  constructor196  . intro reached197    exact pathReached.step198      with finite, edge, loop, bounds.right, parity, reached199  . intro reached200    exact pathReached.step201      with finite, edge, reverse, bounds.left, flipped, reached202203-- Along edges of F, a vertex joined to u is reached by a path from u: an204-- edge set P ⊆ F whose degrees are odd exactly at u and v when u ≠ v.205theorem Joined.path (V leftEnd rightEnd F u v : Set)206  requires finite : Finite(F)207  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V208  requires distinct : u ≠ v209  requires joined : Joined(leftEnd, rightEnd, F, u, v)210  shows ∃ P ⊆ F, ∀ w ∈ V,211    (Even(degreeIn(leftEnd, rightEnd, P, w)) ↔ (w ≠ u ∧ w ≠ v))212proof213  have start := Joined.start_in with ends, distinct, joined214  have self : u ∈ pathReached(V, leftEnd, rightEnd, F, u)215    by simp [pathReached, start]216  have reached := joined with pathReached(V, leftEnd, rightEnd, F, u), self,217    (pathReached.closed with finite, ends)218  rcases reached with ⟨_, same | path⟩219  . cc220  . exact path221222theorem componentBy.closed (V leftEnd rightEnd F u : Set)223  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V224  shows ClosedUnder(leftEnd, rightEnd, F,225    componentBy(V, leftEnd, rightEnd, F, u))226proof227  intros e edge228  obtain ⟨leftV, rightV⟩ := ends with e, edge229  constructor230  . intro member231    exact ⟨rightV, (Joined.transitive232      with member.right, (Joined.of_edge with edge))⟩233  . intro member234    exact ⟨leftV, (Joined.transitive235      with member.right, (Joined.of_edge_reverse with edge))⟩236237theorem componentBy.eq_of_joined (V leftEnd rightEnd F u w : Set)238  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V239  requires first : u ∈ V240  requires second : w ∈ V241  requires joined : Joined(leftEnd, rightEnd, F, u, w)242  shows componentBy(V, leftEnd, rightEnd, F, u) =243    componentBy(V, leftEnd, rightEnd, F, w)244proof245  have back := Joined.symmetric with ends, first, second, joined246  ext z247  constructor248  . intro member249    exact ⟨member.left, (Joined.transitive with back, member.right)⟩250  . intro member251    exact ⟨member.left, (Joined.transitive with joined, member.right)⟩252253-- The edges of F with both ends in X.254def inside (leftEnd rightEnd F X : Set) : Set :=255  { e ∈ F | leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X }256257-- A partition of V: nonempty classes, pairwise disjoint, covering V.258predicate Partition (V P : Set) :=259  (∀ X ∈ P, X ⊆ V ∧ X ≠ ∅) ∧260    (∀ X ∈ P, ∀ Y ∈ P, X ≠ Y → Disjoint(X, Y)) ∧261    (∀ v ∈ V, ∃ X ∈ P, v ∈ X)262263theorem componentsBy.partition (V leftEnd rightEnd F : Set)264  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V265  shows Partition(V, componentsBy(V, leftEnd, rightEnd, F))266proof267  constructor268  -- A component is a subset of V containing its own vertex.269  . intros X inFamily270    obtain ⟨u, inV, rfl⟩ := inFamily271    constructor272    . intros w member273      exact member.left274    . apply Nonempty.ne_empty275      witness u276      exact ⟨inV, Joined.reflexive⟩277  constructor278  -- Two components sharing a vertex are one component.279  . intros X inFamilyX Y inFamilyY different280    obtain ⟨u, uInV, rfl⟩ := inFamilyX281    obtain ⟨w, wInV, rfl⟩ := inFamilyY282    apply Disjoint.iff.backward283    intros x inU inW284    obtain ⟨xInV, fromU⟩ := inU285    obtain ⟨_, fromW⟩ := inW286    have back := Joined.symmetric with ends, wInV, xInV, fromW287    have joined := Joined.transitive with fromU, back288    apply different289    exact componentBy.eq_of_joined with ends, uInV, wInV, joined290  . intros v inV291    witness componentBy(V, leftEnd, rightEnd, F, v)292    exact ⟨⟨v, inV, rfl⟩, ⟨inV, Joined.reflexive⟩⟩293