Grace/Cumulus/GraphTheory/Multigraph/Cuts.g17

Open in Workbench Download source

Imports

Even · Cardinal.IndicatorSum

Declarations

Source

1-- Edge cuts of a multigraph: the edges with exactly one end in a vertex set,2-- edge-connectivity, and bridges. An even edge set crosses every cut an even3-- number of times, so a bridge lies in no even edge 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.Cuts10import Even11import Cardinal.IndicatorSum1213-- The edges of F with exactly one end in X.14def crossing (leftEnd rightEnd F X : Set) : Set :=15  { e ∈ F | (leftEnd(e) ∈ X ∧ rightEnd(e) ∉ X) ∨16            (rightEnd(e) ∈ X ∧ leftEnd(e) ∉ X) }1718-- At least k edges leave every nonempty proper vertex set.19predicate EdgeConnected (V E leftEnd rightEnd : Set, k : Nat) :=20  ∀ X ⊆ V, X ≠ ∅ → X ≠ V →21    k ≤ cardinality(crossing(leftEnd, rightEnd, E, X))2223-- No vertex set is left by exactly one edge.24predicate Bridgeless (V E leftEnd rightEnd : Set) :=25  ∀ X ⊆ V, cardinality(crossing(leftEnd, rightEnd, E, X)) ≠ 12627theorem crossing.subset (leftEnd rightEnd F X : Set)28  shows crossing(leftEnd, rightEnd, F, X) ⊆ F29proof30  intros e he31  exact he.left3233theorem crossing.finite (leftEnd rightEnd F X : Set)34  requires finite : Finite(F)35  shows Finite(crossing(leftEnd, rightEnd, F, X))36proof37  exact Finite.subset with finite, crossing.subset3839theorem crossing.monotone (leftEnd rightEnd F G X : Set)40  requires subset : F ⊆ G41  shows crossing(leftEnd, rightEnd, F, X) ⊆ crossing(leftEnd, rightEnd, G, X)42proof43  intros e he44  exact ⟨(subset with e, he.left), he.right⟩4546-- The cut of a subset of the edges is the restriction of the larger cut.47theorem crossing.restrict (leftEnd rightEnd E F X : Set)48  requires edges : F ⊆ E49  shows crossing(leftEnd, rightEnd, F, X) =50    crossing(leftEnd, rightEnd, E, X) ∩ F51proof52  ext e53  by_cases inF : e ∈ F54  . have inE := edges with e, inF55    simp [crossing, inF, inE]56  . simp [crossing, inF]5758-- A vertex set and its complement are left by the same edges.59theorem crossing.complement (V leftEnd rightEnd F X : Set)60  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V61  shows crossing(leftEnd, rightEnd, F, V ∖ X) =62    crossing(leftEnd, rightEnd, F, X)63proof64  ext e65  by_cases inF : e ∈ F66  . obtain ⟨leftV, rightV⟩ := ends with e, inF67    simp [crossing]68  . simp [crossing]6970-- The empty set and the whole vertex set are left by no edge.71theorem crossing.trivial (V leftEnd rightEnd F X : Set)72  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V73  requires trivial : X = ∅ ∨ X = V74  shows crossing(leftEnd, rightEnd, F, X) = ∅75proof76  apply Subset.antisymmetric77  . intros e member78    obtain ⟨edge, sides⟩ := member79    have inV := ends with e, edge80    exfalso81    rcases trivial with rfl | rfl82    . simp at sides83    . tauto84  . exact empty.subset8586-- A single edge contributes one end at each of its ends, two at a loop.87theorem degreeIn.singleton_indicators (leftEnd rightEnd e v : Set)88  shows degreeIn(leftEnd, rightEnd, {e}, v) =89    indicator({leftEnd(e)}, v) + indicator({rightEnd(e)}, v)90proof91  by_cases atLeft : leftEnd(e) = v92  . by_cases atRight : rightEnd(e) = v93    . rw [(degreeIn.loop with atLeft, atRight), atLeft, atRight,94        indicator.singleton_self]95      simp96    . have distinct : leftEnd(e) ≠ rightEnd(e) by cc97      rw [(degreeIn.end_left with distinct, atLeft), atLeft,98        indicator.singleton_self, (indicator.singleton_other with atRight)]99      simp100  . by_cases atRight : rightEnd(e) = v101    . have distinct : leftEnd(e) ≠ rightEnd(e) by cc102      rw [(degreeIn.end_right with distinct, atRight), atRight,103        indicator.singleton_self, (indicator.singleton_other with atLeft)]104      simp105    . rw [(degreeIn.absent with atLeft, atRight),106        (indicator.singleton_other with atLeft),107        (indicator.singleton_other with atRight)]108      simp109110-- The degrees of a single edge over X sum to the number of its ends in X.111theorem natSum.single_edge (X leftEnd rightEnd e : Set)112  requires finite : Finite(X)113  shows natSum(X, degreeWeights(X, leftEnd, rightEnd, {e})) =114    indicator(X, leftEnd(e)) + indicator(X, rightEnd(e))115proof116  have finiteE := Finite.singleton at e117  -- Pointwise, the degree of {e} is the sum of the two indicators.118  have agree : ∀ v ∈ X, degreeWeights(X, leftEnd, rightEnd, {e})(v) =119      indicatorMap({leftEnd(e)}, X)(v) + indicatorMap({rightEnd(e)}, X)(v)120    intros v hv121    rw [(degreeWeights.value with finiteE, hv), (indicatorMap.value with hv)]122    exact degreeIn.singleton_indicators123  rw [(natSum.add_pointwise124      with finite, indicatorMap.natural, indicatorMap.natural, agree),125    (natSum.indicator with finite),126    cardinality.intersection_singleton, cardinality.intersection_singleton]127128-- The number of ends of an edge of F that lie in X, as a weight on F.129defgraph endsIn (X leftEnd rightEnd F : Set) (e ∈ F) : ℕ :=130  indicator(X, leftEnd(e)) + indicator(X, rightEnd(e))131proof132  have sum : Nat(indicator(X, leftEnd(e)) + indicator(X, rightEnd(e)))133    by typecheck134  exact nat.omega.forward with sum135136theorem endsIn.natural (X leftEnd rightEnd F e : Set)137  requires member : e ∈ F138  shows endsIn(X, leftEnd, rightEnd, F)(e) ∈ ℕ139proof140  rw endsIn.value with member141  exact endsIn.closed with member142143-- An edge has zero, one, or two ends in X.144theorem endsIn.cases (X leftEnd rightEnd F e : Set)145  requires member : e ∈ F146  shows endsIn(X, leftEnd, rightEnd, F)(e) = 0 ∨147    endsIn(X, leftEnd, rightEnd, F)(e) = 1 ∨148    endsIn(X, leftEnd, rightEnd, F)(e) = 2149proof150  rw endsIn.value with member151  by_cases inLeft : leftEnd(e) ∈ X152  . by_cases inRight : rightEnd(e) ∈ X153    . rw [(indicator.member with inLeft), (indicator.member with inRight)]154      simp155    . rw [(indicator.member with inLeft), (indicator.absent with inRight)]156      simp157  . by_cases inRight : rightEnd(e) ∈ X158    . rw [(indicator.absent with inLeft), (indicator.member with inRight)]159      simp160    . rw [(indicator.absent with inLeft), (indicator.absent with inRight)]161      simp162163-- An edge has exactly one end in X precisely when it crosses the cut.164theorem endsIn.one_iff (X leftEnd rightEnd F e : Set)165  requires member : e ∈ F166  shows endsIn(X, leftEnd, rightEnd, F)(e) = 1 ↔167    (leftEnd(e) ∈ X ∧ rightEnd(e) ∉ X) ∨168    (rightEnd(e) ∈ X ∧ leftEnd(e) ∉ X)169proof170  rw endsIn.value with member171  by_cases inLeft : leftEnd(e) ∈ X172  . by_cases inRight : rightEnd(e) ∈ X173    . rw [(indicator.member with inLeft), (indicator.member with inRight)]174      simp [inLeft, inRight]175    . rw [(indicator.member with inLeft), (indicator.absent with inRight)]176      simp [inLeft, inRight]177  . by_cases inRight : rightEnd(e) ∈ X178    . rw [(indicator.absent with inLeft), (indicator.member with inRight)]179      simp [inLeft, inRight]180    . rw [(indicator.absent with inLeft), (indicator.absent with inRight)]181      simp [inLeft, inRight]182183-- Exchanging the order of summation: the degrees over X sum to the number of184-- edge ends in X, counted edge by edge. By induction on the edge set: adding185-- an edge a adds its degree at every vertex, and its number of ends in X.186theorem natSum.degrees_count_ends (X leftEnd rightEnd F : Set)187  requires finiteX : Finite(X)188  requires finite : Finite(F)189  shows natSum(X, degreeWeights(X, leftEnd, rightEnd, F)) =190    natSum(F, endsIn(X, leftEnd, rightEnd, F))191proof192  induction finite with G a193  | empty =>194    have vanish : ∀ v ∈ X, degreeWeights(X, leftEnd, rightEnd, ∅)(v) = 0195      intros v hv196      rw degreeWeights.value with Finite.empty, hv197      exact degreeIn.empty198    rw natSum.empty199    exact natSum.zero_weights with vanish200  | insert using ih =>201    have finiteA := Finite.singleton at a202    have finiteStep := Finite.union with GFinite, finiteA203    have member : a ∈ G ∪ {a} by simp204    have rest : (G ∪ {a}) ∖ {a} = G205      rw [difference.of_union2, (difference.singleton_of_absent with aFresh)]206    -- Over the vertices: the degree in G ∪ {a} is the degree in G plus the207    -- degree in {a}.208    have agree : ∀ v ∈ X,209        degreeWeights(X, leftEnd, rightEnd, G ∪ {a})(v) =210        degreeWeights(X, leftEnd, rightEnd, G)(v) +211        degreeWeights(X, leftEnd, rightEnd, {a})(v)212      intros v hv213      rw [(degreeWeights.value with finiteStep, hv),214        (degreeWeights.value with GFinite, hv),215        (degreeWeights.value with finiteA, hv),216        (degreeIn.remove with finiteStep, member), rest]217    have split := natSum.add_pointwise with finiteX,218      (degreeWeights.natural with GFinite),219      (degreeWeights.natural with finiteA), agree220    have single := natSum.single_edge at X, leftEnd, rightEnd, a with finiteX221    -- Over the edges: the sum over G ∪ {a} is the sum over G plus the ends222    -- of a in X, and the weight of an edge does not depend on the edge set.223    have endWeights : ∀ e ∈ G ∪ {a},224        endsIn(X, leftEnd, rightEnd, G ∪ {a})(e) ∈ ℕ225      intros e he226      exact endsIn.natural with he227    have removed := natSum.remove with finiteStep, member, endWeights228    rw [rest, (endsIn.value with member)] at removed229    have agreeEnds : ∀ e ∈ G, endsIn(X, leftEnd, rightEnd, G ∪ {a})(e) =230        endsIn(X, leftEnd, rightEnd, G)(e)231      intros e he232      have step : e ∈ G ∪ {a} by simp233      rw [(endsIn.value with step), (endsIn.value with he)]234    have restEnds := natSum.congr with agreeEnds235    rw [split, single, removed, restEnds, ih]236237-- The cut parity: the number of edges of F leaving X has the parity of the238-- sum of the degrees of F over X, because an edge inside X contributes two239-- ends there and an edge outside none.240theorem crossing.parity (leftEnd rightEnd F X : Set)241  requires finiteX : Finite(X)242  requires finite : Finite(F)243  shows Even(cardinality(crossing(leftEnd, rightEnd, F, X))) ↔244    Even(natSum(X, degreeWeights(X, leftEnd, rightEnd, F)))245proof246  have weights : ∀ e ∈ F, endsIn(X, leftEnd, rightEnd, F)(e) = 0 ∨247      endsIn(X, leftEnd, rightEnd, F)(e) = 1 ∨248      endsIn(X, leftEnd, rightEnd, F)(e) = 2249    intros e he250    exact endsIn.cases with he251  -- The edges with exactly one end in X are the crossing edges.252  have same : ones(F, endsIn(X, leftEnd, rightEnd, F)) =253      crossing(leftEnd, rightEnd, F, X)254    ext e255    by_cases he : e ∈ F256    . simp [ones, crossing, he]257      exact endsIn.one_iff with he258    . simp [ones, crossing, he]259  rw [(natSum.degrees_count_ends with finiteX, finite),260    (natSum.parity with finite, weights), same]261262theorem EvenEdgeSet.crossing_even (V leftEnd rightEnd F X : Set)263  requires finiteVertices : Finite(V)264  requires even : EvenEdgeSet(V, leftEnd, rightEnd, F)265  requires subset : X ⊆ V266  shows Even(cardinality(crossing(leftEnd, rightEnd, F, X)))267proof268  have finiteF := even.left269  have finiteX := Finite.subset with finiteVertices, subset270  -- The degrees over X are even, so their sum is.271  have evens : ∀ v ∈ X, Even(degreeWeights(X, leftEnd, rightEnd, F)(v))272    intros v hv273    rw degreeWeights.value with finiteF, hv274    exact even.right with v, (subset with v, hv)275  rw crossing.parity with finiteX, finiteF276  exact natSum.even_of_even_weights277    with finiteX, (degreeWeights.natural with finiteF), evens278279-- An even edge set never meets a cut in exactly one edge.280theorem EvenEdgeSet.crossing_ne_singleton (V leftEnd rightEnd F X g : Set)281  requires finiteVertices : Finite(V)282  requires even : EvenEdgeSet(V, leftEnd, rightEnd, F)283  requires subset : X ⊆ V284  shows crossing(leftEnd, rightEnd, F, X) ≠ {g}285proof286  intro single287  have evenCount := EvenEdgeSet.crossing_even288    with finiteVertices, even, subset289  rw [single, cardinality.singleton] at evenCount290  exact Even.not_one with evenCount291292-- A bridge is an edge that alone leaves some vertex set; no even edge set293-- contains one.294theorem EvenEdgeSet.avoids_bridge (V E leftEnd rightEnd F X e : Set)295  requires finiteVertices : Finite(V)296  requires even : EvenEdgeSet(V, leftEnd, rightEnd, F)297  requires subset : X ⊆ V298  requires edges : F ⊆ E299  requires ends : ∀ e ∈ E, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V300  requires cut : crossing(leftEnd, rightEnd, E, X) = {e}301  shows e ∉ F302proof303  intro inF304  have single : crossing(leftEnd, rightEnd, F, X) = {e}305    rw [(crossing.restrict with edges), cut]306    ext g307    simp [inF]308  exact EvenEdgeSet.crossing_ne_singleton309    with finiteVertices, even, subset, single310311-- If exactly one edge of a two-edge cut lies in F, that edge alone leaves X312-- within F.313theorem crossing.restrict_pair (leftEnd rightEnd E F X e f : Set)314  requires edges : F ⊆ E315  requires cut : crossing(leftEnd, rightEnd, E, X) = {e, f}316  requires inside : e ∈ F317  requires outside : f ∉ F318  shows crossing(leftEnd, rightEnd, F, X) = {e}319proof320  rw [(crossing.restrict with edges), cut]321  ext g322  by_cases ge : g = e323  . simp [ge, inside]324  . by_cases gf : g = f325    . simp [gf, outside]326    . simp [ge, gf]327328-- A cut of two edges is met by an even set in both or neither.329theorem EvenEdgeSet.two_cut (V E leftEnd rightEnd F X e f : Set)330  requires finiteVertices : Finite(V)331  requires even : EvenEdgeSet(V, leftEnd, rightEnd, F)332  requires subset : X ⊆ V333  requires edges : F ⊆ E334  requires ends : ∀ e ∈ E, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V335  requires cut : crossing(leftEnd, rightEnd, E, X) = {e, f}336  requires distinct : e ≠ f337  shows e ∈ F ↔ f ∈ F338proof339  have swapped : crossing(leftEnd, rightEnd, E, X) = {f, e}340    rw [cut, pair.commutative]341  constructor342  . intro eIn343    by_contra fOut344    have single := crossing.restrict_pair with edges, cut, eIn, fOut345    exact EvenEdgeSet.crossing_ne_singleton346      with finiteVertices, even, subset, single347  . intro fIn348    by_contra eOut349    have single := crossing.restrict_pair with edges, swapped, fIn, eOut350    exact EvenEdgeSet.crossing_ne_singleton351      with finiteVertices, even, subset, single352353theorem EdgeConnected.bridgeless (V E leftEnd rightEnd : Set, k : Nat)354  requires two : 2 ≤ k355  requires ends : ∀ e ∈ E, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V356  requires connected : EdgeConnected(V, E, leftEnd, rightEnd, k)357  shows Bridgeless(V, E, leftEnd, rightEnd)358proof359  intros X bound360  by_cases trivial : X = ∅ ∨ X = V361  . rw [(crossing.trivial with ends, trivial), cardinality.empty]362    arith363  . have nonempty : X ≠ ∅ by tauto364    have proper : X ≠ V by tauto365    have many := connected with X, bound, nonempty, proper366    arith367368theorem EdgeConnected.monotone (V E leftEnd rightEnd : Set, k m : Nat)369  requires order : m ≤ k370  requires connected : EdgeConnected(V, E, leftEnd, rightEnd, k)371  shows EdgeConnected(V, E, leftEnd, rightEnd, m)372proof373  intros X bound nonempty proper374  have above := connected with X, bound, nonempty, proper375  linarith376