Grace/Cumulus/GraphTheory/Multigraph.g17

Open in Workbench Download source

Imports

Cardinal.Enumeration · Nat.Parity

Declarations

Source

1-- Multigraphs with distinct edge identities and finite walks.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.GraphTheory.Multigraph8import Cardinal.Enumeration9import Nat.Parity1011-- Endpoint maps need not be injective: parallel edges remain distinct.12-- Loops are allowed and contribute twice to incidence counts.13predicate Graph (V E leftEnd rightEnd : Set) :=14  FunctionBetween(leftEnd, E, V) ∧ FunctionBetween(rightEnd, E, V)1516predicate Traverses (E leftEnd rightEnd e u v : Set) :=17  e ∈ E ∧ ((leftEnd(e) = u ∧ rightEnd(e) = v) ∨18    (leftEnd(e) = v ∧ rightEnd(e) = u))1920-- The first n edge entries join successive entries of the vertex sequence.21-- Only finite prefixes matter; the sequences may be defined on larger domains.22predicate Walk (V E leftEnd rightEnd edges vertices n : Set) :=23  (∀ i ∈ succ(n), vertices[i] ∈ V) ∧24  (∀ i ∈ n, Traverses(E, leftEnd, rightEnd, edges[i], vertices[i], vertices[succ(i)]))2526predicate Trail (V E leftEnd rightEnd edges vertices n : Set) :=27  Walk(V, E, leftEnd, rightEnd, edges, vertices, n) ∧ DistinctValues(edges, n)2829predicate EulerTrail (V E leftEnd rightEnd edges vertices n : Set) :=30  Trail(V, E, leftEnd, rightEnd, edges, vertices, n) ∧31  (∀ e ∈ E, Occurs(edges, n, e))3233theorem Traverses.reverse (E leftEnd rightEnd e u v : Set)34  requires edge : Traverses(E, leftEnd, rightEnd, e, u, v)35  shows Traverses(E, leftEnd, rightEnd, e, v, u)36proof37  unfold Traverses at edge38  unfold Traverses39  tauto4041theorem Traverses.bounds (V E leftEnd rightEnd e u v : Set)42  requires graph : Graph(V, E, leftEnd, rightEnd)43  requires edge : Traverses(E, leftEnd, rightEnd, e, u, v)44  shows u ∈ V ∧ v ∈ V45proof46  rcases graph with ⟨leftMap, rightMap⟩47  rcases edge with ⟨member, orientation⟩48  have leftIn := FunctionBetween.apply_closed at leftEnd, E, V, e with *49  have rightIn := FunctionBetween.apply_closed at rightEnd, E, V, e with *50  cases orientation with forward | backward51  . rcases forward with ⟨leftEq, rightEq⟩52    rw leftEq at leftIn53    rw rightEq at rightIn54    tauto55  . rcases backward with ⟨leftEq, rightEq⟩56    rw leftEq at leftIn57    rw rightEq at rightIn58    tauto5960theorem Walk.prefix (V E leftEnd rightEnd edges vertices : Set, n : Nat)61  requires walk : Walk(V, E, leftEnd, rightEnd, edges, vertices, succ(n))62  shows Walk(V, E, leftEnd, rightEnd, edges, vertices, n)63proof64  rcases walk with ⟨verticesIn, steps⟩65  constructor66  . intros i before67    have included := membership.into_successor with before68    exact verticesIn with i, included69  . intros i before70    have included := membership.into_successor with before71    exact steps with i, included7273theorem Trail.prefix (V E leftEnd rightEnd edges vertices : Set, n : Nat)74  requires trail : Trail(V, E, leftEnd, rightEnd, edges, vertices, succ(n))75  shows Trail(V, E, leftEnd, rightEnd, edges, vertices, n)76proof77  rcases trail with ⟨walk, distinct⟩78  have shorter := Walk.prefix with *79  have unique := DistinctValues.prefix with *80  unfold Trail81  tauto8283-- Each endpoint is counted separately, including the two ends of a loop.84def incidences (leftEnd rightEnd edges x : Set, n : Nat) → Set85  | leftEnd, rightEnd, edges, x, zero => 086  | leftEnd, rightEnd, edges, x, succ(k) =>87    add(incidences(leftEnd, rightEnd, edges, x, k),88      add(indicator({x}, leftEnd(edges[k])), indicator({x}, rightEnd(edges[k]))))8990theorem incidences.natural (leftEnd rightEnd edges x : Set, n : Nat)91  shows Nat(incidences(leftEnd, rightEnd, edges, x, n))92proof93  induction n94  | zero =>95    rw incidences96    typecheck97  | succ(k) using ih =>98    rw incidences99    typecheck100101theorem Traverses.incidence (E leftEnd rightEnd e u v x : Set)102  requires edge : Traverses(E, leftEnd, rightEnd, e, u, v)103  shows add(indicator({x}, leftEnd(e)), indicator({x}, rightEnd(e))) =104    add(indicator({x}, u), indicator({x}, v))105proof106  rcases edge with ⟨member, orientation⟩107  cases orientation with forward | backward108  . rcases forward with ⟨leftEq, rightEq⟩109    rw [leftEq, rightEq]110    rfl111  . rcases backward with ⟨leftEq, rightEq⟩112    rw [leftEq, rightEq]113    ring114115-- Telescoping incidence balance, valid for walks of arbitrary finite length.116-- countMembers({x}, vertices, n) counts departures from x.117theorem Walk.incidence_balance (V E leftEnd rightEnd edges vertices x : Set, n : Nat)118  shows Walk(V, E, leftEnd, rightEnd, edges, vertices, n) →119    add(incidences(leftEnd, rightEnd, edges, x, n), indicator({x}, vertices[0])) =120    add(add(countMembers({x}, vertices, n), countMembers({x}, vertices, n)),121      indicator({x}, vertices[n]))122proof123  induction n124  | zero =>125    intro walk126    simp [incidences, countMembers, add]127  | succ(k) using ih =>128    intro walk129    have prefix := Walk.prefix at V, E, leftEnd, rightEnd, edges, vertices, k with *130    have balance := ih with prefix131    rcases walk with ⟨verticesIn, steps⟩132    have last := membership.self_successor at k with *133    have edge := steps with k, last134    have contribution := Traverses.incidence at E, leftEnd, rightEnd, edges[k],135      vertices[k], vertices[succ(k)], x with edge136    rw [incidences, contribution, countMembers]137    have regroup : add(add(incidences(leftEnd, rightEnd, edges, x, k),138        add(indicator({x}, vertices[k]), indicator({x}, vertices[succ(k)]))),139        indicator({x}, vertices[0])) =140      add(add(incidences(leftEnd, rightEnd, edges, x, k), indicator({x}, vertices[0])),141        add(indicator({x}, vertices[k]), indicator({x}, vertices[succ(k)])))142      ring143    rw [regroup, balance]144    ring145146-- A closed walk has even incidence count at every vertex, loops included.147theorem Walk.closed_even (V E leftEnd rightEnd edges vertices x : Set, n : Nat)148  requires walk : Walk(V, E, leftEnd, rightEnd, edges, vertices, n)149  requires closed : vertices[n] = vertices[0]150  shows Even(incidences(leftEnd, rightEnd, edges, x, n))151proof152  have balance := Walk.incidence_balance at V, E, leftEnd, rightEnd, edges, vertices, x, n with walk153  rw closed at balance154  have equality := add.right_cancel with balance155  rw equality156  exact Even.double with *157158theorem Walk.nonendpoint_even (V E leftEnd rightEnd edges vertices x : Set, n : Nat)159  requires walk : Walk(V, E, leftEnd, rightEnd, edges, vertices, n)160  requires notStart : x ≠ vertices[0]161  requires notEnd : x ≠ vertices[n]162  shows Even(incidences(leftEnd, rightEnd, edges, x, n))163proof164  have startMissing : ¬(vertices[0] ∈ {x})165    intro member166    have equal := singleton.membership.forward with member167    apply notStart168    symm169    exact equal170  have endMissing : ¬(vertices[n] ∈ {x})171    intro member172    have equal := singleton.membership.forward with member173    apply notEnd174    symm175    exact equal176  have startZero := indicator.absent with startMissing177  have endZero := indicator.absent with endMissing178  have balance := Walk.incidence_balance at V, E, leftEnd, rightEnd, edges, vertices, x, n with walk179  rw [startZero, endZero] at balance180  simp [add.right_unit] at balance181  rw balance182  exact Even.double with *183184theorem Walk.noneven_endpoint (V E leftEnd rightEnd edges vertices x : Set, n : Nat)185  requires walk : Walk(V, E, leftEnd, rightEnd, edges, vertices, n)186  requires noneven : ¬Even(incidences(leftEnd, rightEnd, edges, x, n))187  shows x = vertices[0] ∨ x = vertices[n]188proof189  have alternatives : (x = vertices[0] ∨ x = vertices[n]) ∨190      (x ≠ vertices[0] ∧ x ≠ vertices[n])191    tauto192  cases alternatives with endpoint | interior193  . exact endpoint194  . rcases interior with ⟨notStart, notEnd⟩195    have even := Walk.nonendpoint_even with *196    tauto197198-- The fiber records edge identities, so two parallel edges count separately.199def endpointFiber (E endpoint x : Set) : Set := { e ∈ E | endpoint(e) = x }200201theorem endpointFiber.indicator (E endpoint x e : Set)202  requires member : e ∈ E203  shows indicator({x}, endpoint(e)) = indicator(endpointFiber(E, endpoint, x), e)204proof205  have equivalent : endpoint(e) ∈ {x} ↔ e ∈ endpointFiber(E, endpoint, x)206    have singleton := singleton.membership at endpoint(e), x207    have fiber := endpointFiber.membership at E, endpoint, x, e208    tauto209  exact indicator.congr with equivalent210211-- Degree expressed as two finite set counts.212theorem incidences.counts (E leftEnd rightEnd edges x : Set, n : Nat)213  shows (∀ i ∈ n, edges[i] ∈ E) →214    incidences(leftEnd, rightEnd, edges, x, n) =215    add(countMembers(endpointFiber(E, leftEnd, x), edges, n),216      countMembers(endpointFiber(E, rightEnd, x), edges, n))217proof218  induction n219  | zero =>220    intro values221    simp [incidences, countMembers, add]222  | succ(k) using ih =>223    intro values224    have prefix : ∀ i ∈ k, edges[i] ∈ E225      intros i before226      have included := membership.into_successor with before227      exact values with i, included228    have last := membership.self_successor at k with *229    have member := values with k, last230    have leftValue := endpointFiber.indicator at E, leftEnd, x, edges[k] with member231    have rightValue := endpointFiber.indicator at E, rightEnd, x, edges[k] with member232    have previous := ih with prefix233    rw [incidences, previous, leftValue, rightValue, countMembers, countMembers]234    ring235236theorem Walk.edge_values (V E leftEnd rightEnd edges vertices n : Set)237  requires walk : Walk(V, E, leftEnd, rightEnd, edges, vertices, n)238  shows ∀ i ∈ n, edges[i] ∈ E239proof240  rcases walk with ⟨verticesIn, steps⟩241  intros i before242  have edge := steps with i, before243  unfold Traverses at edge244  tauto245246-- Any complete edge enumeration gives the same degrees as an Euler trail.247theorem EulerTrail.incidence_reindex (V E leftEnd rightEnd edges vertices enumeration x : Set, n m : Nat)248  requires trail : EulerTrail(V, E, leftEnd, rightEnd, edges, vertices, n)249  requires bijective : BijectiveBetween(enumeration, m, E)250  shows incidences(leftEnd, rightEnd, edges, x, n) =251    incidences(leftEnd, rightEnd, enumeration, x, m)252proof253  rcases trail with ⟨path, covers⟩254  rcases path with ⟨walk, distinct⟩255  have values := Walk.edge_values with walk256  have otherValues := Bijective.values with bijective257  have injective := Bijective.injective with bijective258  have onto := Bijective.surjective with bijective259  have otherDistinct := Injective.distinct_values with injective260  have covered : ∀ i ∈ n, Occurs(enumeration, m, edges[i])261    intros i before262    have member := values with i, before263    exact Surjective.occurs with *264  have otherCovered : ∀ i ∈ m, Occurs(edges, n, enumeration[i])265    intros i before266    have member := otherValues with i, before267    exact covers with enumeration[i], member268  have leftCount := countMembers.same_entries at endpointFiber(E, leftEnd, x), edges, enumeration, n, m with *269  have rightCount := countMembers.same_entries at endpointFiber(E, rightEnd, x), edges, enumeration, n, m with *270  have original := incidences.counts at E, leftEnd, rightEnd, edges, x, n with values271  have reordered := incidences.counts at E, leftEnd, rightEnd, enumeration, x, m with otherValues272  rw [original, reordered, leftCount, rightCount]273  rfl274275theorem EulerTrail.noneven_endpoint (V E leftEnd rightEnd edges vertices enumeration x : Set, n m : Nat)276  requires trail : EulerTrail(V, E, leftEnd, rightEnd, edges, vertices, n)277  requires bijective : BijectiveBetween(enumeration, m, E)278  requires noneven : ¬Even(incidences(leftEnd, rightEnd, enumeration, x, m))279  shows x = vertices[0] ∨ x = vertices[n]280proof281  have reindex := EulerTrail.incidence_reindex at V, E, leftEnd, rightEnd, edges, vertices, enumeration, x, n, m with *282  rw ← reindex at noneven283  rcases trail with ⟨path, covers⟩284  rcases path with ⟨walk, distinct⟩285  exact Walk.noneven_endpoint with *286287-- Three distinct vertices of non-even degree obstruct every Euler trail.288-- Degrees may be computed in any fixed bijective edge enumeration.289theorem EulerTrail.three_noneven_obstruction (V E leftEnd rightEnd edges vertices enumeration a b c : Set, n m : Nat)290  requires bijective : BijectiveBetween(enumeration, m, E)291  requires ab : a ≠ b292  requires ac : a ≠ c293  requires bc : b ≠ c294  requires degreeA : ¬Even(incidences(leftEnd, rightEnd, enumeration, a, m))295  requires degreeB : ¬Even(incidences(leftEnd, rightEnd, enumeration, b, m))296  requires degreeC : ¬Even(incidences(leftEnd, rightEnd, enumeration, c, m))297  shows ¬EulerTrail(V, E, leftEnd, rightEnd, edges, vertices, n)298proof299  intro trail300  have aEnds := EulerTrail.noneven_endpoint at V, E, leftEnd, rightEnd, edges, vertices, enumeration, a, n, m with *301  have bEnds := EulerTrail.noneven_endpoint at V, E, leftEnd, rightEnd, edges, vertices, enumeration, b, n, m with *302  have cEnds := EulerTrail.noneven_endpoint at V, E, leftEnd, rightEnd, edges, vertices, enumeration, c, n, m with *303  cases aEnds with aStart | aEnd304  . cases bEnds with bStart | bEnd305    . cc306    . cases cEnds with cStart | cEnd307      . cc308      . cc309  . cases bEnds with bStart | bEnd310    . cases cEnds with cStart | cEnd311      . cc312      . cc313    . cc314315-- Conventional parity statements derived from the incidence obstruction.316theorem Walk.odd_endpoint (V E leftEnd rightEnd edges vertices x : Set, n : Nat)317  requires walk : Walk(V, E, leftEnd, rightEnd, edges, vertices, n)318  requires odd : Odd(incidences(leftEnd, rightEnd, edges, x, n))319  shows x = vertices[0] ∨ x = vertices[n]320proof321  have noneven := Odd.not_even with odd322  exact Walk.noneven_endpoint with *323324theorem EulerTrail.odd_endpoint (V E leftEnd rightEnd edges vertices enumeration x : Set, n m : Nat)325  requires trail : EulerTrail(V, E, leftEnd, rightEnd, edges, vertices, n)326  requires bijective : BijectiveBetween(enumeration, m, E)327  requires odd : Odd(incidences(leftEnd, rightEnd, enumeration, x, m))328  shows x = vertices[0] ∨ x = vertices[n]329proof330  have noneven := Odd.not_even with odd331  exact EulerTrail.noneven_endpoint with *332333theorem EulerTrail.three_odd_obstruction (V E leftEnd rightEnd edges vertices enumeration a b c : Set, n m : Nat)334  requires bijective : BijectiveBetween(enumeration, m, E)335  requires ab : a ≠ b336  requires ac : a ≠ c337  requires bc : b ≠ c338  requires oddA : Odd(incidences(leftEnd, rightEnd, enumeration, a, m))339  requires oddB : Odd(incidences(leftEnd, rightEnd, enumeration, b, m))340  requires oddC : Odd(incidences(leftEnd, rightEnd, enumeration, c, m))341  shows ¬EulerTrail(V, E, leftEnd, rightEnd, edges, vertices, n)342proof343  have degreeA := Odd.not_even with oddA344  have degreeB := Odd.not_even with oddB345  have degreeC := Odd.not_even with oddC346  exact EulerTrail.three_noneven_obstruction with degreeA, degreeB, degreeC347