Grace/Cumulus/GraphTheory/Multigraph/Subgraph.g17

Open in Workbench Download source

Imports

Connectivity

Declarations

Source

1-- The side of a vertex set as a multigraph of its own: the edges inside a2-- vertex set, the end functions restricted to them, and the ends, degrees,3-- and cuts read through the restriction; a side crossed by no edge of a4-- bridgeless graph is bridgeless.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.Multigraph.Subgraph11import Connectivity1213-- The edges of F inside X are edges of F, grow with F, and have both ends14-- in X.15theorem inside.subset (leftEnd rightEnd F X : Set)16  shows inside(leftEnd, rightEnd, F, X) ⊆ F17proof18  intros e edge19  exact edge.left2021theorem inside.monotone (leftEnd rightEnd F G X : Set)22  requires subset : F ⊆ G23  shows inside(leftEnd, rightEnd, F, X) ⊆ inside(leftEnd, rightEnd, G, X)24proof25  intros e edge26  exact ⟨(subset with e, edge.left), edge.right⟩2728theorem inside.ends (leftEnd rightEnd F X : Set)29  shows ∀ e ∈ inside(leftEnd, rightEnd, F, X),30    leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X31proof32  intros e edge33  exact edge.right3435-- Two sets of ends agree when they agree on every pair (f, i).36theorem incidentEnds.ext (leftEnd rightEnd otherLeft otherRight F G v w : Set)37  requires agree : ∀ f, ∀ i,38    ((f, i) ∈ incidentEnds(leftEnd, rightEnd, F, v) ↔39      (f, i) ∈ incidentEnds(otherLeft, otherRight, G, w))40  shows incidentEnds(leftEnd, rightEnd, F, v) =41    incidentEnds(otherLeft, otherRight, G, w)42proof43  ext p44  constructor45  . intro hp46    obtain ⟨f, _, i, _, rfl⟩ := incidentEnds.shape with hp47    have rule := agree with f, i48    exact rule.forward with hp49  . intro hp50    obtain ⟨f, _, i, _, rfl⟩ := incidentEnds.shape with hp51    have rule := agree with f, i52    exact rule.backward with hp5354-- On the edges of D the restricted ends are the ends, so the ends at a55-- vertex, the degrees, and the cuts of an edge set inside D are the same56-- for both.57theorem incidentEnds.restricted (W E D F leftEnd rightEnd v : Set)58  requires graph : Graph(W, E, leftEnd, rightEnd)59  requires edges : D ⊆ E60  requires subset : F ⊆ D61  shows incidentEnds(restrict(leftEnd, D), restrict(rightEnd, D), F, v) =62    incidentEnds(leftEnd, rightEnd, F, v)63proof64  apply incidentEnds.ext65  intros f i66  by_cases inF : f ∈ F67  . have inD := subset with f, inF68    have leftValue := restrict.domain_apply with graph.left, edges, inD69    have rightValue := restrict.domain_apply with graph.right, edges, inD70    simp [incidentEnds.pair, leftValue, rightValue]71  . simp [incidentEnds.pair, inF]7273theorem degreeIn.restricted (W E D F leftEnd rightEnd v : Set)74  requires graph : Graph(W, E, leftEnd, rightEnd)75  requires edges : D ⊆ E76  requires subset : F ⊆ D77  shows degreeIn(restrict(leftEnd, D), restrict(rightEnd, D), F, v) =78    degreeIn(leftEnd, rightEnd, F, v)79proof80  unfold degreeIn81  rw incidentEnds.restricted with graph, edges, subset8283theorem crossing.restricted (W E D X leftEnd rightEnd : Set)84  requires graph : Graph(W, E, leftEnd, rightEnd)85  requires edges : D ⊆ E86  shows crossing(restrict(leftEnd, D), restrict(rightEnd, D), D, X) =87    crossing(leftEnd, rightEnd, D, X)88proof89  ext e90  by_cases inD : e ∈ D91  . have leftValue := restrict.domain_apply with graph.left, edges, inD92    have rightValue := restrict.domain_apply with graph.right, edges, inD93    simp [crossing, leftValue, rightValue]94  . simp [crossing, inD]9596-- A side of a split is a graph on its own vertices once the end functions97-- are restricted to its inside edges, and it stays bridgeless when no edge98-- crosses the split.99theorem inside.graph (V E leftEnd rightEnd X : Set)100  requires graph : Graph(V, E, leftEnd, rightEnd)101  requires subset : X ⊆ V102  shows Graph(X, inside(leftEnd, rightEnd, E, X),103    restrict(leftEnd, inside(leftEnd, rightEnd, E, X)),104    restrict(rightEnd, inside(leftEnd, rightEnd, E, X)))105proof106  have edges := inside.subset at leftEnd, rightEnd, E, X107  have ends := inside.ends at leftEnd, rightEnd, E, X108  have leftIn : ∀ e ∈ inside(leftEnd, rightEnd, E, X), leftEnd(e) ∈ X109    intros e he110    exact (ends with e, he).left111  have rightIn : ∀ e ∈ inside(leftEnd, rightEnd, E, X), rightEnd(e) ∈ X112    intros e he113    exact (ends with e, he).right114  exact ⟨(restrict.function with graph.left, edges, leftIn),115    (restrict.function with graph.right, edges, rightIn)⟩116117theorem inside.bridgeless (V E leftEnd rightEnd X : Set)118  requires graph : Graph(V, E, leftEnd, rightEnd)119  requires split : X ⊆ V ∧ crossing(leftEnd, rightEnd, E, X) = ∅120  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)121  shows Bridgeless(X, inside(leftEnd, rightEnd, E, X),122    restrict(leftEnd, inside(leftEnd, rightEnd, E, X)),123    restrict(rightEnd, inside(leftEnd, rightEnd, E, X)))124proof125  intros Y bound126  obtain ⟨subset, none⟩ := split127  have edges := inside.subset at leftEnd, rightEnd, E, X128  -- An edge leaving Y ⊆ X has its other end in X, as no edge leaves X, so129  -- the cut of Y within the side is its cut in the whole graph.130  have within : crossing(leftEnd, rightEnd, E, Y) ⊆131      inside(leftEnd, rightEnd, E, X)132    intros e he133    obtain ⟨inE, sides⟩ := he134    have notCross : ¬e ∈ crossing(leftEnd, rightEnd, E, X)135      rw none136      simp137    have both : leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X138      by_contra outside139      apply notCross140      refine ⟨inE, _⟩141      rcases sides with ⟨leftY, rightY⟩ | ⟨rightY, leftY⟩142      . left143        have leftX := bound with leftEnd(e), leftY144        refine ⟨leftX, _⟩145        intro rightX146        exact outside with ⟨leftX, rightX⟩147      . right148        have rightX := bound with rightEnd(e), rightY149        refine ⟨rightX, _⟩150        intro leftX151        exact outside with ⟨leftX, rightX⟩152    exact ⟨inE, both⟩153  have same : crossing(restrict(leftEnd, inside(leftEnd, rightEnd, E, X)),154      restrict(rightEnd, inside(leftEnd, rightEnd, E, X)),155      inside(leftEnd, rightEnd, E, X), Y) = crossing(leftEnd, rightEnd, E, Y)156    rw [(crossing.restricted with graph, edges), (crossing.restrict with edges)]157    exact intersection.eq_left_of_subset with within158  rw same159  exact bridgeless with Y, (Subset.transitive with bound, subset)160