Grace/Cumulus/GraphTheory/Counting.g17

Open in Workbench Download source

Imports

Basic · Set.Indicator · Cardinal.Finite

Declarations

Source

1-- Finite degree sums and undirected edge counts.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.Counting8import Basic9import Set.Indicator10import Cardinal.Finite1112namespace GraphCount1314-- f enumerates the vertices. Degree counts adjacent entries in its prefix.15-- A bijection f : n → V gives the usual degree in a finite graph.16def degree (E f x : Set, n : Nat) → Set17  | E, f, x, zero => 018  | E, f, x, succ(k) => add(degree(E, f, x, k), indicator(E, (x, f[k])))1920-- Sum the degrees of the first m vertices, using n vertices as neighbors.21def degreeSum (E f : Set, n m : Nat) → Set22  | E, f, n, zero => 023  | E, f, n, succ(k) => add(degreeSum(E, f, n, k), degree(E, f, f[k], n))24  descends m2526-- Count each undirected edge once: its larger enumeration index is last.27-- In particular this is NOT the cardinality of the symmetric relation E.28def edgeCount (E f : Set, n : Nat) → Set29  | E, f, zero => 030  | E, f, succ(k) => add(edgeCount(E, f, k), degree(E, f, f[k], k))3132theorem degree.natural (E f x : Set, n : Nat)33  shows Nat(degree(E, f, x, n))34proof35  induction n36  | zero =>37    rw degree38    typecheck39  | succ(k) using ih =>40    rw degree41    typecheck4243theorem degreeSum.natural (E f : Set, n m : Nat)44  shows Nat(degreeSum(E, f, n, m))45proof46  induction m47  | zero =>48    rw degreeSum49    typecheck50  | succ(k) using ih =>51    rw degreeSum52    have value := degree.natural at E, f, f[k], n with assumption53    typecheck5455theorem edgeCount.natural (E f : Set, n : Nat)56  shows Nat(edgeCount(E, f, n))57proof58  induction n59  | zero =>60    rw edgeCount61    typecheck62  | succ(k) using ih =>63    rw edgeCount64    have value := degree.natural at E, f, f[k], k with assumption65    typecheck6667theorem indicator.symmetric (V E x y : Set)68  requires graph : SimpleGraph(V, E)69  shows indicator(E, (x, y)) = indicator(E, (y, x))70proof71  apply indicator.congr72  constructor73  . intro edge74    have adjacent : Adjacent(E, x, y)75      unfold Adjacent76      exact edge77    have reversed := Adjacent.symmetric with graph, adjacent78    unfold Adjacent at reversed79    exact reversed80  . intro edge81    have adjacent : Adjacent(E, y, x)82      unfold Adjacent83      exact edge84    have reversed := Adjacent.symmetric with graph, adjacent85    unfold Adjacent at reversed86    exact reversed8788theorem indicator.diagonal (V E x : Set)89  requires graph : SimpleGraph(V, E)90  shows indicator(E, (x, x)) = 091proof92  apply indicator.absent93  intro loop94  have adjacent : Adjacent(E, x, x)95    unfold Adjacent96    exact loop97  have distinct := Adjacent.distinct with graph, adjacent98  apply distinct99  rfl100101-- Adding one possible neighbor adds its incidence count to the degree sum.102theorem degreeSum.extend_neighbors (V E f : Set, n m : Nat)103  requires graph : SimpleGraph(V, E)104  shows degreeSum(E, f, succ(n), m) =105    add(degreeSum(E, f, n, m), degree(E, f, f[n], m))106proof107  induction m108  | zero =>109    simp [degreeSum, degree, add]110  | succ(k) using ih =>111    rw [degreeSum, degreeSum, degree, degree, ih]112    have symmetric := indicator.symmetric at V, E, f[k], f[n] with graph113    rw symmetric114    have a := degreeSum.natural at E, f, n, k with *115    have b := degree.natural at E, f, f[n], k116    have c := degree.natural at E, f, f[k], n117    have d := indicator.natural at E, (f[n], f[k])118    exact add.four_shuffle with a, b, c, d119120-- Each new edge contributes to two degrees, and no loop contributes a third.121theorem handshaking (V E f : Set, n : Nat)122  requires graph : SimpleGraph(V, E)123  shows degreeSum(E, f, n, n) = mul(2, edgeCount(E, f, n))124proof125  induction n126  | zero =>127    simp [degreeSum, edgeCount, mul, add]128  | succ(k) using ih =>129    rw degreeSum130    have extended := degreeSum.extend_neighbors at V, E, f, k, k with *131    rw [extended, degree]132    have noLoop := indicator.diagonal at V, E, f[k] with graph133    rw [noLoop, ih, edgeCount]134    simp [mul.two_left, add.right_unit]135    ring136137-- The degree really counts membership in the previously defined neighbor set.138theorem degree.neighbors (V E f x : Set, n : Nat)139  shows (∀ i ∈ n, f[i] ∈ V) →140    degree(E, f, x, n) = countMembers(neighbors(V, E, x), f, n)141proof142  induction n143  | zero =>144    intro enumeration145    simp [degree, countMembers]146  | succ(k) using ih =>147    intro enumeration148    have prefix : ∀ i ∈ k, f[i] ∈ V149      intros i before150      have earlier : i ∈ k ∨ i = k151        left152        exact before153      have included := membership.successor_backward{n := k} with earlier154      exact enumeration with i, included155    have last := enumeration with k, membership.self_successor at k with assumption156    have equivalent : (x, f[k]) ∈ E ↔ f[k] ∈ neighbors(V, E, x)157      have member := neighbors.membership at V, E, x, f[k]158      have edgeIff : Adjacent(E, x, f[k]) ↔ (x, f[k]) ∈ E159        constructor160        . intro edge161          unfold Adjacent at edge162          exact edge163        . intro edge164          unfold Adjacent165          exact edge166      tauto167    have same := indicator.congr with equivalent168    have previous := ih with prefix169    rw [degree, countMembers, previous, same]170    rfl171172end GraphCount173174-- Public finite-graph formulation. A bijection lists every vertex exactly175-- once, so the lower triangle counts every undirected edge exactly once.176theorem SimpleGraph.handshaking (V E f : Set, n : Nat)177  requires graph : SimpleGraph(V, E)178  requires enumeration : BijectiveBetween(f, n, V)179  shows GraphCount.degreeSum(E, f, n, n) = 2 * GraphCount.edgeCount(E, f, n)180proof181  exact GraphCount.handshaking with graph182183-- Finiteness supplies an enumeration; no fixed size or numeric vertex labels184-- are imposed on V.185theorem Finite.handshaking (V E : Set)186  requires graph : SimpleGraph(V, E)187  requires finite : Finite(V)188  shows ∃ n ∈ ℕ, ∃ f, BijectiveBetween(f, n, V) ∧189    GraphCount.degreeSum(E, f, n, n) = 2 * GraphCount.edgeCount(E, f, n)190proof191  rcases finite with ⟨n, natural, equivalent⟩192  obtain ⟨f, enumeration⟩ := Equipotent.symmetric with equivalent193  witness n194  constructor195  . exact nat.omega.forward at n with natural196  . refine ⟨f, enumeration, (SimpleGraph.handshaking at V, E, f, n with natural, graph, enumeration)⟩197