Grace/Cumulus/GraphTheory/Multigraph/Trees.g17

Open in Workbench Download source

Imports

Components

Declarations

Source

1-- Forests and spanning trees as edge sets: a forest contains no nonempty2-- even edge set, a spanning tree connects V with one edge fewer than3-- vertices, and adding an edge to a tree closes exactly one even 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.Trees10import Components1112predicate Forest (V leftEnd rightEnd F : Set) :=13  Finite(F) ∧ (∀ C ⊆ F, EvenEdgeSet(V, leftEnd, rightEnd, C) → C = ∅)1415predicate SpanningTree (V leftEnd rightEnd T : Set) :=16  Finite(T) ∧ Connects(V, leftEnd, rightEnd, T)17  ∧ cardinality(T) + 1 = cardinality(V)1819theorem Forest.subset (V leftEnd rightEnd F G : Set)20  requires forest : Forest(V, leftEnd, rightEnd, F)21  requires subset : G ⊆ F22  shows Forest(V, leftEnd, rightEnd, G)23proof24  obtain ⟨finite, acyclic⟩ := forest25  constructor26  . exact Finite.subset with finite, subset27  . intros C bound even28    exact acyclic with C, (Subset.transitive with bound, subset), even2930-- In a forest the ends of an edge are joined only through that edge: a path31-- around it would close a nonempty even set, and a loop is one by itself.32theorem Forest.ends_apart (V leftEnd rightEnd F e : Set)33  requires ends : ∀ f ∈ F, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V34  requires forest : Forest(V, leftEnd, rightEnd, F)35  requires edge : e ∈ F36  shows ¬Joined(leftEnd, rightEnd, F ∖ {e}, leftEnd(e), rightEnd(e))37proof38  intro joined39  obtain ⟨finite, acyclic⟩ := forest40  have restSubset := difference.subset_left at F, {e}41  have restFinite := Finite.subset with finite, restSubset42  have restEnds := ends_in.subset with ends, restSubset43  have edgeSubset : {e} ⊆ F := singleton.subset_iff.backward with edge44  by_cases loop : leftEnd(e) = rightEnd(e)45  . have even := EvenEdgeSet.loop at V, leftEnd, rightEnd, e with loop46    have empty := acyclic with {e}, edgeSubset, even47    exact singleton.ne_empty with empty48  . obtain ⟨P, subsetP, path⟩ :=49      Joined.path with restFinite, restEnds, loop, joined50    have finiteP := Finite.subset with restFinite, subsetP51    have outside : ¬e ∈ P52      intro inP53      have inRest := subsetP with e, inP54      simp at inRest55    have even := EvenEdgeSet.of_path_edge with finiteP, outside, loop, path56    have inside : P ∪ {e} ⊆ F by simp57    have empty := acyclic with P ∪ {e}, inside, even58    rw union2.eq_empty_iff at empty59    exact singleton.ne_empty with empty.right6061-- Adding an edge between vertices a forest does not join keeps it a forest:62-- an even set through the new edge would join its ends by the old edges.63theorem Forest.add_edge (V leftEnd rightEnd F e : Set)64  requires finiteVertices : Finite(V)65  requires ends : ∀ f ∈ F, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V66  requires edgeEnds : leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V67  requires forest : Forest(V, leftEnd, rightEnd, F)68  requires apart : ¬Joined(leftEnd, rightEnd, F, leftEnd(e), rightEnd(e))69  shows Forest(V, leftEnd, rightEnd, F ∪ {e})70proof71  obtain ⟨finite, acyclic⟩ := forest72  have moreEnds := ends_in.union_edge with ends, edgeEnds73  constructor74  . exact Finite.union with finite, Finite.singleton75  . intros C bound even76    have endsC := ends_in.subset with moreEnds, bound77    have inF : C ∖ {e} ⊆ F by simp78    by_cases inC : e ∈ C79    . exfalso80      have joined := EvenEdgeSet.ends_joined with81        finiteVertices, endsC, even, inC82      exact apart with (Joined.monotone with inF, joined)83    . rw difference.singleton_of_absent with inC at inF84      exact acyclic with C, inF, even8586-- A forest on a finite vertex set has at most |V| − c edges, c the number of87-- its components: adding its edges one at a time, each merges two components,88-- since a forest joins the ends of an edge only through that edge.89theorem Forest.edge_bound (V leftEnd rightEnd F : Set)90  requires finiteVertices : Finite(V)91  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V92  requires forest : Forest(V, leftEnd, rightEnd, F)93  shows cardinality(F) + cardinality(componentsBy(V, leftEnd, rightEnd, F)) ≤94    cardinality(V)95proof96  obtain ⟨finite, _⟩ := forest97  induction finite with G e98  | empty =>99    rw [(componentsBy.empty_count with finiteVertices), cardinality.empty]100    arith101  | insert using ih =>102    have GEnds := ends_in.subset with ends, GSubset103    have edgeEnds := ends with e, eMember104    have apart : ¬Joined(leftEnd, rightEnd, G, leftEnd(e), rightEnd(e))105      have rest : G ⊆ F ∖ {e} by simp106      have apartRest := Forest.ends_apart with ends, forest, eMember107      intro joined108      exact apartRest with (Joined.monotone with rest, joined)109    have count := componentsBy.add_edge_apart with110      finiteVertices, GEnds, edgeEnds, apart111    have grown := cardinality.union_singleton with GFinite, eFresh112    arith113114-- An edge set on V with at least |V| − 1 edges that does not connect V115-- holds a nonempty even edge set: the key counting step of tree packing.116theorem EvenEdgeSet.of_dense_disconnected (V leftEnd rightEnd F : Set)117  requires finiteVertices : Finite(V)118  requires finite : Finite(F)119  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V120  requires dense : cardinality(V) ≤ cardinality(F) + 1121  requires disconnected : ¬Connects(V, leftEnd, rightEnd, F)122  shows ∃ C ⊆ F, C ≠ ∅ ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)123proof124  by_contra none125  -- Without a nonempty even subset, F is a forest with at least two components.126  have forest : Forest(V, leftEnd, rightEnd, F)127    constructor128    . exact finite129    . intros C bound even130      by_contra nonempty131      exact none with ⟨C, bound, nonempty, even⟩132  have upper := Forest.edge_bound with finiteVertices, ends, forest133  have two := componentsBy.two_of_disconnected with finiteVertices, disconnected134  arith135136-- A spanning tree is a forest: an edge of an even subset could be dropped137-- without disconnecting V, leaving too few edges for a connected edge set.138theorem SpanningTree.forest (V leftEnd rightEnd T : Set)139  requires finiteVertices : Finite(V)140  requires ends : ∀ e ∈ T, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V141  requires tree : SpanningTree(V, leftEnd, rightEnd, T)142  shows Forest(V, leftEnd, rightEnd, T)143proof144  obtain ⟨finite, connected, count⟩ := tree145  constructor146  . exact finite147  . intros C bound even148    by_contra nonempty149    obtain ⟨e, he⟩ := Nonempty.of_ne_empty with nonempty150    have inT := bound with e, he151    have restSubset := difference.subset_left at T, {e}152    have restFinite := Finite.subset with finite, restSubset153    have restEnds := ends_in.subset with ends, restSubset154    have edgeEnds := ends with e, inT155    have endsC := ends_in.subset with ends, bound156    have joinedC := EvenEdgeSet.ends_joined with finiteVertices, endsC, even, he157    have restC : C ∖ {e} ⊆ T ∖ {e} :=158      difference.subset_of_subset with bound159    have bridged := Joined.monotone with restC, joinedC160    have same := componentsBy.add_edge_joined with restEnds, edgeEnds, bridged161    have restored : (T ∖ {e}) ∪ {e} = T by ext y; simp162    rw restored at same163    have lower := componentsBy.lower_bound with164      finiteVertices, restFinite, restEnds165    rw ← same at lower166    have one := componentsBy.le_one_of_connected with connected167    have removed := cardinality.remove with finite, inT168    rw removed at count169    arith170171-- A connected forest on a nonempty vertex set has exactly |V| − 1 edges.172theorem SpanningTree.of_connected_forest (V leftEnd rightEnd T : Set)173  requires finiteVertices : Finite(V)174  requires nonempty : V ≠ ∅175  requires ends : ∀ e ∈ T, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V176  requires forest : Forest(V, leftEnd, rightEnd, T)177  requires connected : Connects(V, leftEnd, rightEnd, T)178  shows SpanningTree(V, leftEnd, rightEnd, T)179proof180  obtain ⟨finite, _⟩ := forest181  have upper := Forest.edge_bound with finiteVertices, ends, forest182  have lower := componentsBy.lower_bound with finiteVertices, finite, ends183  have one := componentsBy.connected_count with connected, nonempty184  refine ⟨finite, connected, _⟩185  arith186187-- The forests inside an edge set, a finite family when the edge set is finite.188def forestsIn (V leftEnd rightEnd E : Set) : Set :=189  { F ∈ 𝒫(E) | Forest(V, leftEnd, rightEnd, F) }190191-- Every connected finite multigraph has a spanning tree: a maximal forest192-- inside E is connected, else an edge of E leaving one of its components193-- could be added to it.194theorem SpanningTree.exists (V E leftEnd rightEnd : Set)195  requires graph : Graph(V, E, leftEnd, rightEnd)196  requires finiteVertices : Finite(V)197  requires finiteEdges : Finite(E)198  requires nonempty : V ≠ ∅199  requires connected : Connects(V, leftEnd, rightEnd, E)200  shows ∃ T ⊆ E, SpanningTree(V, leftEnd, rightEnd, T)201proof202  have endsE := Graph.ends with graph203  have finiteFamily : Finite(forestsIn(V, leftEnd, rightEnd, E))204    have subset : forestsIn(V, leftEnd, rightEnd, E) ⊆ 𝒫(E)205      intros F hF206      obtain ⟨inPowerset, _⟩ := hF207      exact inPowerset208    exact Finite.subset with (Finite.powerset with finiteEdges), subset209  have emptyForest : ∅ ∈ forestsIn(V, leftEnd, rightEnd, E)210    have emptySubset : ∅ ∈ 𝒫(E) :=211      powerset.membership_iff.backward with empty.subset212    have forest : Forest(V, leftEnd, rightEnd, ∅)213      constructor214      . exact Finite.empty215      . intros C bound even216        exact Subset.antisymmetric with bound, empty.subset217    exact ⟨emptySubset, forest⟩218  obtain ⟨T, inFamily, _, maximal⟩ :=219    Finite.maximal_extension with finiteFamily, emptyForest220  obtain ⟨inPowerset, forest⟩ := inFamily221  have subsetE := powerset.membership_iff.forward with inPowerset222  have endsT := ends_in.subset with endsE, subsetE223  have connectedT : Connects(V, leftEnd, rightEnd, T)224    by_contra disconnected225    obtain ⟨u, hu, v, hv, apart⟩ := Connects.witness_apart with disconnected226    have closedT := componentBy.closed at V, leftEnd, rightEnd, T, u227      with endsT228    have selfU := componentBy.self at V, leftEnd, rightEnd, T, u with hu229    -- Some edge of E leaves the T-component of u, since v lies outside it.230    have crossingEdge : ∃ e ∈ E,231        ¬(leftEnd(e) ∈ componentBy(V, leftEnd, rightEnd, T, u) ↔232          rightEnd(e) ∈ componentBy(V, leftEnd, rightEnd, T, u))233      by_contra none234      have closedE : ClosedUnder(leftEnd, rightEnd, E,235          componentBy(V, leftEnd, rightEnd, T, u))236        intros e he237        by_contra unbalanced238        exact none with ⟨e, he, unbalanced⟩239      have inComponent := connected with u, hu, v, hv,240        componentBy(V, leftEnd, rightEnd, T, u), selfU, closedE241      exact apart with inComponent.right242    obtain ⟨e, he, unbalanced⟩ := crossingEdge243    have edgeEnds := endsE with e, he244    have outside : ¬e ∈ T245      intro inT246      exact unbalanced with (closedT with e, inT)247    have apartEnds : ¬Joined(leftEnd, rightEnd, T, leftEnd(e), rightEnd(e))248      intro joined249      exact unbalanced with (Joined.balanced with250        endsT, edgeEnds.left, edgeEnds.right, joined, closedT)251    -- Then T ∪ {e} is a larger forest inside E, against maximality.252    have bigger := Forest.add_edge with253      finiteVertices, endsT, edgeEnds, forest, apartEnds254    have biggerSubset : T ∪ {e} ⊆ E := Subset.union2_iff.backward with255      ⟨subsetE, (singleton.subset_iff.backward with he)⟩256    have biggerIn : T ∪ {e} ∈ forestsIn(V, leftEnd, rightEnd, E) :=257      ⟨(powerset.membership_iff.backward with biggerSubset), bigger⟩258    have equal := maximal with T ∪ {e}, biggerIn, union2.subset_left259    have member : e ∈ T ∪ {e} by simp260    rw equal at member261    exact outside with member262  refine ⟨T, subsetE, _⟩263  exact SpanningTree.of_connected_forest with264    finiteVertices, nonempty, endsT, forest, connectedT265266-- The fundamental even set of an edge outside a spanning tree: an even set267-- inside T ∪ {e} that contains e.268theorem SpanningTree.fundamental (V leftEnd rightEnd T e : Set)269  requires finiteVertices : Finite(V)270  requires ends : (∀ f ∈ T, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V)271    ∧ leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V272  requires tree : SpanningTree(V, leftEnd, rightEnd, T)273  requires outside : ¬e ∈ T274  shows ∃ C ⊆ T ∪ {e}, e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)275proof276  obtain ⟨finite, connected, _⟩ := tree277  obtain ⟨endsT, leftIn, rightIn⟩ := ends278  have member : e ∈ {e} by simp279  by_cases loop : leftEnd(e) = rightEnd(e)280  . refine ⟨{e}, union2.subset_right, member, _⟩281    exact EvenEdgeSet.loop at V, leftEnd, rightEnd, e with loop282  . have joined := connected with leftEnd(e), leftIn, rightEnd(e), rightIn283    obtain ⟨P, subsetP, path⟩ :=284      Joined.path with finite, endsT, loop, joined285    have finiteP := Finite.subset with finite, subsetP286    have outsideP : ¬e ∈ P287      intro inP288      exact outside with (subsetP with e, inP)289    have even := EvenEdgeSet.of_path_edge with finiteP, outsideP, loop, path290    have inside : P ∪ {e} ⊆ T ∪ {e} := union2.monotone_left with subsetP291    have inC : e ∈ P ∪ {e} by simp292    exact ⟨P ∪ {e}, inside, inC, even⟩293294-- Exchanging an edge of a tree for another edge of the even set it closes295-- gives a tree again: the one-edge exchange of the tree-packing proof.296theorem SpanningTree.exchange (V leftEnd rightEnd T C e f : Set)297  requires finiteVertices : Finite(V)298  requires ends : (∀ g ∈ T, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V)299    ∧ leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V300  requires tree : SpanningTree(V, leftEnd, rightEnd, T)301  requires outside : ¬e ∈ T302  requires even : EvenEdgeSet(V, leftEnd, rightEnd, C)303  requires closes : C ⊆ T ∪ {e} ∧ e ∈ C304  requires other : f ∈ C ∧ f ≠ e305  shows SpanningTree(V, leftEnd, rightEnd, (T ∖ {f}) ∪ {e})306proof307  obtain ⟨finite, connected, count⟩ := tree308  obtain ⟨endsT, edgeEnds⟩ := ends309  obtain ⟨inside, inC⟩ := closes310  obtain ⟨fInC, different⟩ := other311  have fInT : f ∈ T by simp312  have fEnds := endsT with f, fInT313  have restSubset := difference.subset_left at T, {f}314  have restFinite := Finite.subset with finite, restSubset315  have restEnds := ends_in.subset with endsT, restSubset316  have newEnds := ends_in.union_edge with restEnds, edgeEnds317  have keep := union2.subset_left at T ∖ {f}, {e}318  refine ⟨(Finite.union with restFinite, Finite.singleton), _, _⟩319  . -- The ends of f stay joined through C ∖ {f}, so dropping f from320    -- T ∪ {e} loses no connection.321    have endsC := ends_in.subset with (ends_in.union_edge with endsT, edgeEnds),322      inside323    have joinedC := EvenEdgeSet.ends_joined with324      finiteVertices, endsC, even, fInC325    have restC : C ∖ {f} ⊆ (T ∖ {f}) ∪ {e}326      intros g hg327      obtain ⟨inCg, notF⟩ := difference.singleton_membership.forward with hg328      have inBig := inside with g, inCg329      simp330    have bridged := Joined.monotone with restC, joinedC331    have grow : T ⊆ ((T ∖ {f}) ∪ {e}) ∪ {f}332      intros g hg333      simp334    intros u hu v hv335    have joinedBig := Joined.monotone with grow, (connected with u, hu, v, hv)336    exact Joined.drop_edge with newEnds, fEnds, joinedBig, bridged337  . have fresh : ¬e ∈ T ∖ {f}338      intro inRest339      exact outside with (restSubset with e, inRest)340    have inserted := cardinality.union_singleton with restFinite, fresh341    have removed := cardinality.remove_add_one with finite, fInT342    rwa [inserted, ← removed]343