Grace/Cumulus/GraphTheory/Flows/Contraction.g17

Open in Workbench Download source

Imports

EvenCovers

Declarations

Source

1-- Contracting an edge of a multigraph: the quotient by the partition merging2-- its two ends. The contraction of a bridgeless graph is bridgeless, its cuts3-- are the cuts of the graph not separating the ends of the edge, and the4-- degrees of its classes are read off from the graph.5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.GraphTheory.Flows.Contraction11import EvenCovers1213-- Section: The contraction of an edge.1415-- The partition of V that merges the two ends of e: the components of {e}.16def contractionPartition (V leftEnd rightEnd e : Set) : Set :=17  componentsBy(V, leftEnd, rightEnd, {e})1819def contractedLeft (V E leftEnd rightEnd e : Set) : Set :=20  quotientEnd(E ∖ {e}, contractionPartition(V, leftEnd, rightEnd, e), leftEnd)21def contractedRight (V E leftEnd rightEnd e : Set) : Set :=22  quotientEnd(E ∖ {e}, contractionPartition(V, leftEnd, rightEnd, e),23    rightEnd)2425theorem contractionPartition.partition (V E leftEnd rightEnd e : Set)26  requires graph : Graph(V, E, leftEnd, rightEnd)27  requires edge : e ∈ E28  shows Partition(V, contractionPartition(V, leftEnd, rightEnd, e))29proof30  have ends : ∀ f ∈ {e}, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V31    intros f hf32    rw singleton.membership at hf33    rw hf34    exact Graph.ends with graph, e, edge35  unfold contractionPartition36  exact componentsBy.partition with ends3738-- The quotient ends of a subset of the edges, as a function on that subset.39theorem quotientEnd.function_subset (V E D P endpoint : Set)40  requires function : endpoint : E → V41  requires partition : Partition(V, P)42  requires edges : D ⊆ E43  shows quotientEnd(D, P, endpoint) : D → P44proof45  constructor46  . intros p member47    exact member.left48  constructor49  . intros x y relatedY z relatedZ50    obtain ⟨_, valueY⟩ := quotientEnd.relates with relatedY51    obtain ⟨_, valueZ⟩ := quotientEnd.relates with relatedZ52    cc53  . intros x edge54    have vertex := FunctionBetween.apply_closed55      with function, (edges with x, edge)56    obtain ⟨class, _⟩ := classOf.member with partition, vertex57    witness classOf(P, endpoint(x))58    refine ⟨class, _⟩59    exact quotientEnd.membership.backward60      with ⟨(product.pair with edge, class), x, edge, rfl⟩6162theorem quotientEnd.value_subset (V E D P endpoint f : Set)63  requires function : endpoint : E → V64  requires partition : Partition(V, P)65  requires edges : D ⊆ E66  requires edge : f ∈ D67  shows quotientEnd(D, P, endpoint)(f) = classOf(P, endpoint(f))68proof69  have vertex := FunctionBetween.apply_closed70    with function, (edges with f, edge)71  obtain ⟨class, _⟩ := classOf.member with partition, vertex72  have related :73      relates(quotientEnd(D, P, endpoint), f, classOf(P, endpoint(f))) :=74    quotientEnd.membership.backward75      with ⟨(product.pair with edge, class), f, edge, rfl⟩76  exact FunctionBetween.apply_value77    with (quotientEnd.function_subset with function, partition, edges),78      edge, related7980theorem contraction.graph (V E leftEnd rightEnd e : Set)81  requires graph : Graph(V, E, leftEnd, rightEnd)82  requires edge : e ∈ E83  shows Graph(contractionPartition(V, leftEnd, rightEnd, e), E ∖ {e},84    contractedLeft(V, E, leftEnd, rightEnd, e),85    contractedRight(V, E, leftEnd, rightEnd, e))86proof87  have partition := contractionPartition.partition with graph, edge88  have edges := difference.subset_left at E, {e}89  unfold contractedLeft90  unfold contractedRight91  exact ⟨(quotientEnd.function_subset with graph.left, partition, edges),92    (quotientEnd.function_subset with graph.right, partition, edges)⟩9394-- The ends of an edge of the contraction are the classes of its ends.95theorem contraction.value (V E leftEnd rightEnd e f : Set)96  requires graph : Graph(V, E, leftEnd, rightEnd)97  requires edge : e ∈ E98  requires other : f ∈ E ∖ {e}99  shows contractedLeft(V, E, leftEnd, rightEnd, e)(f) =100      classOf(contractionPartition(V, leftEnd, rightEnd, e), leftEnd(f)) ∧101    contractedRight(V, E, leftEnd, rightEnd, e)(f) =102      classOf(contractionPartition(V, leftEnd, rightEnd, e), rightEnd(f))103proof104  have partition := contractionPartition.partition with graph, edge105  have edges := difference.subset_left at E, {e}106  unfold contractedLeft107  unfold contractedRight108  exact ⟨(quotientEnd.value_subset with graph.left, partition, edges, other),109    (quotientEnd.value_subset with graph.right, partition, edges, other)⟩110111-- Along no edges, distinct vertices stay apart.112theorem Joined.not_empty (leftEnd rightEnd u v : Set)113  requires distinct : u ≠ v114  shows ¬Joined(leftEnd, rightEnd, ∅, u, v)115proof116  intro joined117  have same := Joined.empty with joined118  cc119120theorem ends_in.empty (V leftEnd rightEnd : Set)121  shows ∀ f ∈ ∅, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V122proof123  intros f hf124  simp at hf125126-- Contracting a proper edge loses one vertex.127theorem contraction.vertex_count (V E leftEnd rightEnd e : Set)128  requires graph : Graph(V, E, leftEnd, rightEnd)129  requires finiteVertices : Finite(V)130  requires edge : e ∈ E131  requires proper : leftEnd(e) ≠ rightEnd(e)132  shows cardinality(contractionPartition(V, leftEnd, rightEnd, e)) + 1 =133    cardinality(V)134proof135  have edgeEnds := Graph.ends with graph, e, edge136  -- Along no edges the two ends of e are apart, so e merges two singletons.137  have apart : ¬Joined(leftEnd, rightEnd, ∅, leftEnd(e), rightEnd(e)) :=138    Joined.not_empty with proper139  have count := componentsBy.add_edge_apart140    with finiteVertices, ends_in.empty, edgeEnds, apart141  rw [union2.left_empty, (componentsBy.empty_count with finiteVertices)]142    at count143  unfold contractionPartition144  exact count145146-- The two ends of e share a class of the contraction.147theorem contraction.same_class (V E leftEnd rightEnd e : Set)148  requires graph : Graph(V, E, leftEnd, rightEnd)149  requires edge : e ∈ E150  shows classOf(contractionPartition(V, leftEnd, rightEnd, e), leftEnd(e)) =151    classOf(contractionPartition(V, leftEnd, rightEnd, e), rightEnd(e))152proof153  have partition := contractionPartition.partition with graph, edge154  unfold contractionPartition at partition155  unfold contractionPartition156  have apart := partition.right.left157  obtain ⟨leftIn, rightIn⟩ := Graph.ends with graph, e, edge158  have joined : Joined(leftEnd, rightEnd, {e}, leftEnd(e), rightEnd(e)) :=159    Joined.of_edge with singleton.self160  have class : componentBy(V, leftEnd, rightEnd, {e}, leftEnd(e)) ∈161      componentsBy(V, leftEnd, rightEnd, {e}) :=162    componentsBy.contains at V, leftEnd, rightEnd, {e}, leftEnd(e) with leftIn163  have leftMember :164      leftEnd(e) ∈ componentBy(V, leftEnd, rightEnd, {e}, leftEnd(e)) :=165    componentBy.self with leftIn166  have rightMember :167      rightEnd(e) ∈ componentBy(V, leftEnd, rightEnd, {e}, leftEnd(e)) :=168    ⟨rightIn, joined⟩169  rw [(classOf.eq_of_member with apart, class, leftMember),170    (classOf.eq_of_member with apart, class, rightMember)]171172-- Section: Cuts of the contraction.173174-- A cut of the contraction is a cut of the graph not separating the ends of175-- e, which e therefore does not cross.176theorem contraction.crossing (V E leftEnd rightEnd e Y : Set)177  requires graph : Graph(V, E, leftEnd, rightEnd)178  requires edge : e ∈ E179  requires classes : Y ⊆ contractionPartition(V, leftEnd, rightEnd, e)180  shows crossing(contractedLeft(V, E, leftEnd, rightEnd, e),181      contractedRight(V, E, leftEnd, rightEnd, e), E ∖ {e}, Y) =182    crossing(leftEnd, rightEnd, E, ⋃(Y))183proof184  have partition := contractionPartition.partition with graph, edge185  have endsE := Graph.ends with graph186  ext f187  by_cases inRest : f ∈ E ∖ {e}188  . obtain ⟨leftValue, rightValue⟩ :=189      contraction.value with graph, edge, inRest190    obtain ⟨inE, _⟩ := difference.membership.forward with inRest191    obtain ⟨leftIn, rightIn⟩ := endsE with f, inE192    have leftIff := classOf.mem_union_iff with partition, classes, leftIn193    have rightIff := classOf.mem_union_iff with partition, classes, rightIn194    simp [crossing, leftValue, rightValue, leftIff, rightIff, inRest, inE]195  . by_cases same : f = e196    . rw same197      obtain ⟨leftIn, rightIn⟩ := endsE with e, edge198      have leftIff := classOf.mem_union_iff with partition, classes, leftIn199      have rightIff := classOf.mem_union_iff with partition, classes, rightIn200      have sameClass := contraction.same_class with graph, edge201      have absent : ¬e ∈ E ∖ {e} by simp202      simp [crossing, leftIff, rightIff, sameClass, absent]203    . have notE : ¬f ∈ E204        intro inE205        apply inRest206        simp [inE, same]207      simp [crossing, inRest, notE]208209-- Every cut of the contraction is a cut of the graph, so none has one edge.210theorem contraction.bridgeless (V E leftEnd rightEnd e : Set)211  requires graph : Graph(V, E, leftEnd, rightEnd)212  requires finiteEdges : Finite(E)213  requires edge : e ∈ E214  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)215  shows Bridgeless(contractionPartition(V, leftEnd, rightEnd, e), E ∖ {e},216    contractedLeft(V, E, leftEnd, rightEnd, e),217    contractedRight(V, E, leftEnd, rightEnd, e))218proof219  intros Y classes220  have partition := contractionPartition.partition with graph, edge221  have inV : ⋃(Y) ⊆ V222    intros v hv223    obtain ⟨X, inY, inX⟩ := union.membership.forward with hv224    exact (partition.left with X, (classes with X, inY)).left with v, inX225  rw contraction.crossing with graph, edge, classes226  exact bridgeless with ⋃(Y), inV227228-- Section: The classes of the contraction and their degrees.229230-- The class of a vertex in the contraction is its component along {e}: a231-- vertex apart from the ends of e is a class by itself, and the ends of e232-- form the one other class.233theorem contraction.class (V E leftEnd rightEnd e v : Set)234  requires graph : Graph(V, E, leftEnd, rightEnd)235  requires edge : e ∈ E236  requires vertex : v ∈ V237  shows classOf(contractionPartition(V, leftEnd, rightEnd, e), v) =238    componentBy(V, leftEnd, rightEnd, {e}, v)239proof240  have partition := contractionPartition.partition with graph, edge241  unfold contractionPartition at partition242  unfold contractionPartition243  have class : componentBy(V, leftEnd, rightEnd, {e}, v) ∈244      componentsBy(V, leftEnd, rightEnd, {e}) :=245    componentsBy.contains at V, leftEnd, rightEnd, {e}, v with vertex246  have member : v ∈ componentBy(V, leftEnd, rightEnd, {e}, v) :=247    componentBy.self with vertex248  exact classOf.eq_of_member with partition.right.left, class, member249250theorem contraction.class_apart (V E leftEnd rightEnd e v : Set)251  requires graph : Graph(V, E, leftEnd, rightEnd)252  requires edge : e ∈ E253  requires vertex : v ∈ V254  requires left : v ≠ leftEnd(e)255  requires right : v ≠ rightEnd(e)256  shows classOf(contractionPartition(V, leftEnd, rightEnd, e), v) = {v}257proof258  rw contraction.class with graph, edge, vertex259  -- Along no edges v reaches neither end of e, so e does not move v.260  have apartLeft : ¬Joined(leftEnd, rightEnd, ∅, v, leftEnd(e)) :=261    Joined.not_empty with left262  have apartRight : ¬Joined(leftEnd, rightEnd, ∅, v, rightEnd(e)) :=263    Joined.not_empty with right264  have unchanged := componentBy.add_edge_apart265    with ends_in.empty, vertex, apartLeft, apartRight266  rw union2.left_empty at unchanged267  rw unchanged268  ext w269  constructor270  . intro hw271    have same := Joined.empty with hw.right272    rw same273    exact singleton.self274  . intro hw275    rw singleton.membership at hw276    rw hw277    exact componentBy.self with vertex278279theorem contraction.class_end (V E leftEnd rightEnd e : Set)280  requires graph : Graph(V, E, leftEnd, rightEnd)281  requires edge : e ∈ E282  shows classOf(contractionPartition(V, leftEnd, rightEnd, e), leftEnd(e)) =283    {leftEnd(e), rightEnd(e)}284proof285  obtain ⟨leftIn, rightIn⟩ := Graph.ends with graph, e, edge286  rw contraction.class with graph, edge, leftIn287  ext w288  constructor289  . intro hw290    -- The pair of ends is closed under e, so it holds all that e reaches.291    have closed : ClosedUnder(leftEnd, rightEnd, {e},292        {leftEnd(e), rightEnd(e)})293      intros f hf294      rw singleton.membership at hf295      rw hf296      simp297    have start : leftEnd(e) ∈ {leftEnd(e), rightEnd(e)} := pair.left298    exact hw.right with {leftEnd(e), rightEnd(e)}, start, closed299  . intro hw300    rw pair.membership at hw301    rcases hw with rfl | rfl302    . exact componentBy.self with leftIn303    . have joined : Joined(leftEnd, rightEnd, {e}, leftEnd(e), rightEnd(e)) :=304        Joined.of_edge with singleton.self305      exact ⟨rightIn, joined⟩306307-- An end (f, i) of the contraction at a class Y is an end of f at a vertex308-- of Y.309theorem incidentEnds.contraction (V E leftEnd rightEnd e F Y f i : Set)310  requires graph : Graph(V, E, leftEnd, rightEnd)311  requires edge : e ∈ E312  requires edges : F ⊆ E ∖ {e}313  requires class : Y ∈ contractionPartition(V, leftEnd, rightEnd, e)314  shows (f, i) ∈ incidentEnds(contractedLeft(V, E, leftEnd, rightEnd, e),315      contractedRight(V, E, leftEnd, rightEnd, e), F, Y) ↔316    f ∈ F ∧ ((i = 0 ∧ leftEnd(f) ∈ Y) ∨ (i = 1 ∧ rightEnd(f) ∈ Y))317proof318  have partition := contractionPartition.partition with graph, edge319  rw incidentEnds.pair320  by_cases inF : f ∈ F321  . have other := edges with f, inF322    obtain ⟨leftValue, rightValue⟩ :=323      contraction.value with graph, edge, other324    obtain ⟨inE, _⟩ := difference.membership.forward with other325    obtain ⟨leftIn, rightIn⟩ := Graph.ends with graph, f, inE326    have leftIff := classOf.eq_iff_member with partition, class, leftIn327    have rightIff := classOf.eq_iff_member with partition, class, rightIn328    simp [leftValue, rightValue, leftIff, rightIff, inF]329  . simp [inF]330331-- The degree of a singleton class is the degree of its vertex, and the332-- degree of the class of the two ends of a proper edge e is the sum of333-- their degrees.334theorem degreeIn.contraction_singleton (V E leftEnd rightEnd e F v : Set)335  requires graph : Graph(V, E, leftEnd, rightEnd)336  requires edge : e ∈ E337  requires edges : F ⊆ E ∖ {e}338  requires class : {v} ∈ contractionPartition(V, leftEnd, rightEnd, e)339  shows degreeIn(contractedLeft(V, E, leftEnd, rightEnd, e),340      contractedRight(V, E, leftEnd, rightEnd, e), F, {v}) =341    degreeIn(leftEnd, rightEnd, F, v)342proof343  unfold degreeIn344  have same : incidentEnds(contractedLeft(V, E, leftEnd, rightEnd, e),345      contractedRight(V, E, leftEnd, rightEnd, e), F, {v}) =346      incidentEnds(leftEnd, rightEnd, F, v)347    apply incidentEnds.ext348    intros f i349    rw [(incidentEnds.contraction with graph, edge, edges, class),350      incidentEnds.pair]351    simp [singleton.membership]352  rw same353354theorem degreeIn.contraction_pair (V E leftEnd rightEnd e F : Set)355  requires graph : Graph(V, E, leftEnd, rightEnd)356  requires edge : e ∈ E357  requires finite : Finite(F)358  requires edges : F ⊆ E ∖ {e}359  requires proper : leftEnd(e) ≠ rightEnd(e)360  shows degreeIn(contractedLeft(V, E, leftEnd, rightEnd, e),361      contractedRight(V, E, leftEnd, rightEnd, e), F,362      {leftEnd(e), rightEnd(e)}) =363    degreeIn(leftEnd, rightEnd, F, leftEnd(e)) +364      degreeIn(leftEnd, rightEnd, F, rightEnd(e))365proof366  have partition := contractionPartition.partition with graph, edge367  obtain ⟨leftIn, _⟩ := Graph.ends with graph, e, edge368  have class : {leftEnd(e), rightEnd(e)} ∈369      contractionPartition(V, leftEnd, rightEnd, e)370    rw ← contraction.class_end with graph, edge371    exact (classOf.member with partition, leftIn).left372  -- The ends at the class are the ends at either vertex, and no end is at373  -- both since the vertices differ.374  have same : incidentEnds(contractedLeft(V, E, leftEnd, rightEnd, e),375      contractedRight(V, E, leftEnd, rightEnd, e), F,376      {leftEnd(e), rightEnd(e)}) =377      incidentEnds(leftEnd, rightEnd, F, leftEnd(e)) ∪378      incidentEnds(leftEnd, rightEnd, F, rightEnd(e))379    ext p380    by_cases shape : ∃ f ∈ F, ∃ i ∈ 2, p = (f, i)381    . obtain ⟨f, hf, i, hi, rfl⟩ := shape382      rw [(incidentEnds.contraction with graph, edge, edges, class),383        union2.membership, incidentEnds.pair, incidentEnds.pair]384      simp [pair.membership]385    . constructor386      . intro hp387        exfalso388        exact shape with (incidentEnds.shape with hp)389      . intro hp390        rw union2.membership at hp391        exfalso392        rcases hp with hp | hp393        . exact shape with (incidentEnds.shape with hp)394        . exact shape with (incidentEnds.shape with hp)395  have apart : Disjoint(incidentEnds(leftEnd, rightEnd, F, leftEnd(e)),396      incidentEnds(leftEnd, rightEnd, F, rightEnd(e)))397    rw Disjoint.iff398    intros p hp inRight399    obtain ⟨f, _, i, _, rfl⟩ := incidentEnds.shape with hp400    rw incidentEnds.pair at hp, inRight401    have apart01 : 0 ≠ 1 by simp402    rcases hp.right with ⟨_, atLeft⟩ | ⟨_, atLeft⟩403    . rcases inRight.right with ⟨_, atRight⟩ | ⟨_, atRight⟩404      . cc405      . cc406    . rcases inRight.right with ⟨_, atRight⟩ | ⟨_, atRight⟩407      . cc408      . cc409  unfold degreeIn410  rw same411  exact cardinality.union_disjoint with (incidentEnds.finite with finite),412    (incidentEnds.finite with finite), apart413