Grace/Cumulus/GraphTheory/Multigraph/Degree.g17

Open in Workbench Download source

Imports

Cardinal.Parity · Multigraph · Cardinal.NaturalSumLaws

Declarations

Source

1-- Degrees of vertices in an edge set of a multigraph: the ends of edges at a2-- vertex, counted with a loop contributing both of its ends.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.GraphTheory.Multigraph.Degree9import Cardinal.Parity10import Multigraph11import Cardinal.NaturalSumLaws1213-- The ends of the edges of F at v: (e, 0) for the left end of e, (e, 1) for14-- the right end.15def incidentEnds (leftEnd rightEnd F v : Set) : Set :=16  { p ∈ F × 2 | (snd(p) = 0 ∧ leftEnd(fst(p)) = v) ∨17    (snd(p) = 1 ∧ rightEnd(fst(p)) = v) }1819-- The degree of v in F: the number of ends of edges of F at v.20def degreeIn (leftEnd rightEnd F v : Set) : Set :=21  cardinality(incidentEnds(leftEnd, rightEnd, F, v))2223-- (e, i) is an end at v exactly when e ∈ F and side i of e is v.24theorem incidentEnds.pair (leftEnd rightEnd F v e i : Set)25  shows (e, i) ∈ incidentEnds(leftEnd, rightEnd, F, v) ↔26    e ∈ F ∧ ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))27proof28  unfold incidentEnds29  simp [fst.pair, snd.pair, product.pair_membership, membership.two]3031theorem incidentEnds.shape (leftEnd rightEnd F v p : Set)32  requires member : p ∈ incidentEnds(leftEnd, rightEnd, F, v)33  shows ∃ e ∈ F, ∃ i ∈ 2, p = (e, i)34proof35  exact (product.membership.forward with member.left).right3637theorem incidentEnds.subset_product (leftEnd rightEnd F v : Set)38  shows incidentEnds(leftEnd, rightEnd, F, v) ⊆ F × 239proof40  intros p hp41  exact hp.left4243theorem incidentEnds.finite (leftEnd rightEnd F v : Set)44  requires finite : Finite(F)45  shows Finite(incidentEnds(leftEnd, rightEnd, F, v))46proof47  have product : Finite(F × 2) :=48    Finite.product with finite, Finite.natural49  exact Finite.subset with product, incidentEnds.subset_product5051theorem degreeIn.natural (leftEnd rightEnd F v : Set)52  requires finite : Finite(F)53  shows Nat(degreeIn(leftEnd, rightEnd, F, v))54proof55  unfold degreeIn56  exact cardinality.nat with (incidentEnds.finite with finite)5758theorem degreeIn.empty (leftEnd rightEnd v : Set)59  shows degreeIn(leftEnd, rightEnd, ∅, v) = 060proof61  have none : incidentEnds(leftEnd, rightEnd, ∅, v) = ∅62    ext p63    simp [incidentEnds, product.left_empty]64  unfold degreeIn65  rw none66  exact cardinality.empty6768-- The ends of a single edge e at v: e paired with each side whose end is v.69theorem incidentEnds.singleton (leftEnd rightEnd e v S : Set)70  requires sides : ∀ i, i ∈ S ↔71    ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))72  shows incidentEnds(leftEnd, rightEnd, {e}, v) = {e} × S73proof74  ext p75  constructor76  . intro hp77    obtain ⟨x, hx, i, hi, rfl⟩ := incidentEnds.shape with hp78    simp [incidentEnds.pair] at hp79    simp [product.pair_membership, sides]80  . intro hp81    obtain ⟨_, x, hx, i, hi, rfl⟩ := product.membership.forward with hp82    simp [sides] at hx, hi83    simp [incidentEnds.pair]8485theorem degreeIn.singleton (leftEnd rightEnd e v S : Set)86  requires finite : Finite(S)87  requires sides : ∀ i, i ∈ S ↔88    ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))89  shows degreeIn(leftEnd, rightEnd, {e}, v) = cardinality(S)90proof91  unfold degreeIn92  rw incidentEnds.singleton with sides93  exact cardinality.singleton_product with finite9495-- A loop contributes two ends at its vertex.96theorem degreeIn.loop (leftEnd rightEnd e v : Set)97  requires left : leftEnd(e) = v98  requires right : rightEnd(e) = v99  shows degreeIn(leftEnd, rightEnd, {e}, v) = 2100proof101  have sides : ∀ i, i ∈ 2 ↔102      ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))103    intro i104    simp [membership.two, left, right]105  rw degreeIn.singleton with Finite.natural, sides106  exact cardinality.natural107108-- An edge that is not a loop contributes one end at each of its ends.109theorem degreeIn.end (leftEnd rightEnd e v : Set)110  requires distinct : leftEnd(e) ≠ rightEnd(e)111  requires end : leftEnd(e) = v ∨ rightEnd(e) = v112  shows degreeIn(leftEnd, rightEnd, {e}, v) = 1113proof114  cases end with atLeft | atRight115  . have notRight : rightEnd(e) ≠ v by cc116    have sides : ∀ i, i ∈ {0} ↔117        ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))118      intro i119      simp [singleton.membership, atLeft, notRight]120    rw degreeIn.singleton with Finite.singleton, sides121    exact cardinality.singleton122  . have notLeft : leftEnd(e) ≠ v by cc123    have sides : ∀ i, i ∈ {1} ↔124        ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))125      intro i126      simp [singleton.membership, atRight, notLeft]127    rw degreeIn.singleton with Finite.singleton, sides128    exact cardinality.singleton129130-- The two halves of degreeIn.end, by which end of e is v.131theorem degreeIn.end_left (leftEnd rightEnd e v : Set)132  requires distinct : leftEnd(e) ≠ rightEnd(e)133  requires atLeft : leftEnd(e) = v134  shows degreeIn(leftEnd, rightEnd, {e}, v) = 1135proof136  have atEnd : leftEnd(e) = v ∨ rightEnd(e) = v by left; exact atLeft137  exact degreeIn.end with distinct, atEnd138139theorem degreeIn.end_right (leftEnd rightEnd e v : Set)140  requires distinct : leftEnd(e) ≠ rightEnd(e)141  requires atRight : rightEnd(e) = v142  shows degreeIn(leftEnd, rightEnd, {e}, v) = 1143proof144  have atEnd : leftEnd(e) = v ∨ rightEnd(e) = v by right; exact atRight145  exact degreeIn.end with distinct, atEnd146147-- An edge with neither end at v contributes nothing there.148theorem degreeIn.absent (leftEnd rightEnd e v : Set)149  requires left : leftEnd(e) ≠ v150  requires right : rightEnd(e) ≠ v151  shows degreeIn(leftEnd, rightEnd, {e}, v) = 0152proof153  have sides : ∀ i, i ∈ ∅ ↔154      ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))155    intro i156    simp [left, right]157  rw degreeIn.singleton with Finite.empty, sides158  exact cardinality.empty159160theorem incidentEnds.monotone (leftEnd rightEnd F G v : Set)161  requires subset : F ⊆ G162  shows incidentEnds(leftEnd, rightEnd, F, v) ⊆163    incidentEnds(leftEnd, rightEnd, G, v)164proof165  intros p hp166  obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with hp167  exact incidentEnds.pair.backward168    with ⟨(subset with e, he), (incidentEnds.pair.forward with hp).right⟩169170-- Taking ends is pointwise in the edge set, so it commutes with ∪ and △ and171-- preserves disjointness.172theorem incidentEnds.union (leftEnd rightEnd F G v : Set)173  shows incidentEnds(leftEnd, rightEnd, F ∪ G, v) =174    incidentEnds(leftEnd, rightEnd, F, v) ∪175    incidentEnds(leftEnd, rightEnd, G, v)176proof177  ext p178  simp [incidentEnds.membership, product.union2_left]179180theorem incidentEnds.disjoint (leftEnd rightEnd F G v : Set)181  requires apart : Disjoint(F, G)182  shows Disjoint(incidentEnds(leftEnd, rightEnd, F, v),183    incidentEnds(leftEnd, rightEnd, G, v))184proof185  have products : Disjoint(F × 2, G × 2) :=186    product.disjoint_of_left with apart187  have left : Disjoint(F × 2, incidentEnds(leftEnd, rightEnd, G, v)) :=188    Disjoint.of_subset_right with products, incidentEnds.subset_product189  exact Disjoint.of_subset_left with left, incidentEnds.subset_product190191theorem incidentEnds.symmetricDifference (leftEnd rightEnd F G v : Set)192  shows incidentEnds(leftEnd, rightEnd, F △ G, v) =193    incidentEnds(leftEnd, rightEnd, F, v) △194    incidentEnds(leftEnd, rightEnd, G, v)195proof196  ext p197  simp [incidentEnds.membership, product.symmetricDifference_left,198    symmetricDifference.membership]199200theorem degreeIn.union_disjoint (leftEnd rightEnd F G v : Set)201  requires first : Finite(F)202  requires second : Finite(G)203  requires apart : Disjoint(F, G)204  shows degreeIn(leftEnd, rightEnd, F ∪ G, v) =205    degreeIn(leftEnd, rightEnd, F, v) + degreeIn(leftEnd, rightEnd, G, v)206proof207  unfold degreeIn208  rw incidentEnds.union209  exact cardinality.union_disjoint with (incidentEnds.finite with first),210    (incidentEnds.finite with second), (incidentEnds.disjoint with apart)211212-- Removing an edge a from F takes the degree in {a} off every degree.213theorem degreeIn.remove (leftEnd rightEnd F a v : Set)214  requires finite : Finite(F)215  requires member : a ∈ F216  shows degreeIn(leftEnd, rightEnd, F, v) =217    degreeIn(leftEnd, rightEnd, F ∖ {a}, v) +218    degreeIn(leftEnd, rightEnd, {a}, v)219proof220  have restored : (F ∖ {a}) ∪ {a} = F221    ext y222    simp223  have sum := degreeIn.union_disjoint at leftEnd, rightEnd, F ∖ {a}, {a}, v224    with (Finite.difference with finite), Finite.singleton,225      Disjoint.difference_left226  rwa restored at sum227228theorem degreeIn.monotone (leftEnd rightEnd F G v : Set)229  requires finite : Finite(G)230  requires subset : F ⊆ G231  shows degreeIn(leftEnd, rightEnd, F, v) ≤ degreeIn(leftEnd, rightEnd, G, v)232proof233  unfold degreeIn234  exact cardinality.monotone with (incidentEnds.finite with finite),235    (incidentEnds.monotone with subset)236237-- Degrees add modulo two under symmetric difference.238theorem degreeIn.symmetricDifference_parity (leftEnd rightEnd F G v : Set)239  requires first : Finite(F)240  requires second : Finite(G)241  shows Even(degreeIn(leftEnd, rightEnd, F △ G, v)) ↔242    (Even(degreeIn(leftEnd, rightEnd, F, v)) ↔243      Even(degreeIn(leftEnd, rightEnd, G, v)))244proof245  unfold degreeIn246  rw incidentEnds.symmetricDifference247  exact EvenSet.symmetricDifference with (incidentEnds.finite with first),248    (incidentEnds.finite with second)249250-- The degree function of F on V, as the weight of a natural sum.251def degreeWeights (V leftEnd rightEnd F : Set) : Set :=252  { p ∈ V × ℕ | ∃ v ∈ V, p = (v, degreeIn(leftEnd, rightEnd, F, v)) }253254theorem degreeWeights.function (V leftEnd rightEnd F : Set)255  requires finite : Finite(F)256  shows degreeWeights(V, leftEnd, rightEnd, F) : V → ℕ257proof258  constructor259  . intros p member260    exact member.left261  . constructor262    . intros x y xy z xz263      obtain ⟨_, a, _, shapeY⟩ := xy264      obtain ⟨_, b, _, shapeZ⟩ := xz265      obtain ⟨sameA, valueY⟩ := orderedPair.injective with shapeY266      obtain ⟨sameB, valueZ⟩ := orderedPair.injective with shapeZ267      cc268    . intros x input269      have weight : degreeIn(leftEnd, rightEnd, F, x) ∈ ℕ :=270        degreeIn.natural with finite271      refine ⟨degreeIn(leftEnd, rightEnd, F, x), weight, _⟩272      exact degreeWeights.membership.backward273        with ⟨(product.pair with input, weight), x, input, rfl⟩274275theorem degreeWeights.value (V leftEnd rightEnd F v : Set)276  requires finite : Finite(F)277  requires member : v ∈ V278  shows degreeWeights(V, leftEnd, rightEnd, F)(v) =279    degreeIn(leftEnd, rightEnd, F, v)280proof281  have weight : degreeIn(leftEnd, rightEnd, F, v) ∈ ℕ :=282    degreeIn.natural with finite283  have related : relates(degreeWeights(V, leftEnd, rightEnd, F), v,284      degreeIn(leftEnd, rightEnd, F, v)) :=285    degreeWeights.membership.backward286      with ⟨(product.pair with member, weight), v, member, rfl⟩287  exact FunctionBetween.apply_value288    with (degreeWeights.function with finite), member, related289290theorem degreeWeights.natural (V leftEnd rightEnd F : Set)291  requires finite : Finite(F)292  shows ∀ v ∈ V, degreeWeights(V, leftEnd, rightEnd, F)(v) ∈ ℕ293proof294  intros v hv295  rw degreeWeights.value with finite, hv296  exact degreeIn.natural with finite297298-- One edge with both ends in V contributes two to the degree sum over V:299-- the sum restricts to the ends of e, where a loop weighs two at one vertex300-- and any other edge one at each of two.301theorem degreeWeights.single_sum (V leftEnd rightEnd e : Set)302  requires finiteVertices : Finite(V)303  requires atLeft : leftEnd(e) ∈ V304  requires atRight : rightEnd(e) ∈ V305  shows natSum(V, degreeWeights(V, leftEnd, rightEnd, {e})) = 2306proof307  have finite : Finite({e}) := Finite.singleton308  have weights := degreeWeights.natural at V, leftEnd, rightEnd, {e} with finite309  have ends : {leftEnd(e), rightEnd(e)} ⊆ V :=310    pair.subset_iff.backward with ⟨atLeft, atRight⟩311  have outside : ∀ v ∈ V ∖ {leftEnd(e), rightEnd(e)},312      degreeWeights(V, leftEnd, rightEnd, {e})(v) = 0313    intros v hv314    have away : leftEnd(e) ≠ v ∧ rightEnd(e) ≠ v by simp315    rw degreeWeights.value with finite, hv.left316    exact degreeIn.absent with away.left, away.right317  rw natSum.restrict with finiteVertices, ends, weights, outside318  by_cases loop : leftEnd(e) = rightEnd(e)319  . rw [loop, pair.self,320      (natSum.singleton with (weights with rightEnd(e), atRight)),321      (degreeWeights.value with finite, atRight)]322    exact degreeIn.loop with loop, rfl323  . rw [(natSum.pair with (weights with leftEnd(e), atLeft),324        (weights with rightEnd(e), atRight), loop),325      (degreeWeights.value with finite, atLeft),326      (degreeWeights.value with finite, atRight),327      (degreeIn.end_left with loop, rfl),328      (degreeIn.end_right with loop, rfl)]329    compute330331-- Handshake: the degrees over V sum to twice the number of edges, when every332-- edge has both ends in V. By induction on F: adjoining an edge a adds the333-- degree in {a} at every vertex, hence two to the sum.334theorem degreeIn.handshake (V leftEnd rightEnd F : Set)335  requires finiteVertices : Finite(V)336  requires finite : Finite(F)337  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V338  shows natSum(V, degreeWeights(V, leftEnd, rightEnd, F)) = 2 * cardinality(F)339proof340  induction finite with G a341  | empty =>342    have vanish : ∀ v ∈ V, degreeWeights(V, leftEnd, rightEnd, ∅)(v) = 0343      intros v hv344      rw degreeWeights.value with Finite.empty, hv345      exact degreeIn.empty346    rw [(natSum.zero_weights with vanish), cardinality.empty]347    compute348  | insert using ih =>349    have endsG : ∀ e ∈ G, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V350      intros e he351      exact ends with e, (GSubset with e, he)352    have endsA := ends with a, aMember353    have single := degreeWeights.single_sum354      with finiteVertices, endsA.left, endsA.right355    have unionFinite : Finite(G ∪ {a}) :=356      Finite.union with GFinite, Finite.singleton357    have apart : Disjoint(G, {a}) by simp [Disjoint.iff, aFresh]358    -- The degree at each vertex splits along G ∪ {a}.359    have pointwise : ∀ v ∈ V,360        degreeWeights(V, leftEnd, rightEnd, G ∪ {a})(v) =361        degreeWeights(V, leftEnd, rightEnd, G)(v) +362        degreeWeights(V, leftEnd, rightEnd, {a})(v)363      intros v hv364      rw degreeWeights.value with hv365      exact degreeIn.union_disjoint with GFinite, Finite.singleton, apart366    rw natSum.add_pointwise with finiteVertices,367      (degreeWeights.natural with GFinite),368      (degreeWeights.natural with Finite.singleton), pointwise369    rw [ih, single, (cardinality.union_singleton with GFinite, aFresh)]370    ring371