Grace/Cumulus/GraphTheory/Multigraph/Even.g17

Open in Workbench Download source

Imports

Degree · Cardinal.SumParity

Declarations

Source

1-- Even edge sets: every vertex meets an even number of edge ends. They are2-- the Eulerian subgraphs, and they form a group under symmetric difference.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.Even9import Degree10import Cardinal.SumParity1112predicate EvenEdgeSet (V leftEnd rightEnd F : Set) :=13  Finite(F) ∧ (∀ v ∈ V, Even(degreeIn(leftEnd, rightEnd, F, v)))1415theorem EvenEdgeSet.empty (V leftEnd rightEnd : Set)16  shows EvenEdgeSet(V, leftEnd, rightEnd, ∅)17proof18  constructor19  . exact Finite.empty20  . intros v hv21    rw degreeIn.empty22    exact Even.zero2324-- A loop contributes two ends at its vertex and none elsewhere.25theorem EvenEdgeSet.loop (V leftEnd rightEnd e : Set)26  requires loop : leftEnd(e) = rightEnd(e)27  shows EvenEdgeSet(V, leftEnd, rightEnd, {e})28proof29  constructor30  . exact Finite.singleton31  . intros v hv32    by_cases atV : leftEnd(e) = v33    . have right : rightEnd(e) = v by cc34      rw degreeIn.loop with atV, right35      exact Even.two36    . have right : rightEnd(e) ≠ v by cc37      rw degreeIn.absent with atV, right38      exact Even.zero3940-- Degrees add modulo two under symmetric difference, so even sets are closed41-- under it.42theorem EvenEdgeSet.symmetricDifference (V leftEnd rightEnd F G : Set)43  requires first : EvenEdgeSet(V, leftEnd, rightEnd, F)44  requires second : EvenEdgeSet(V, leftEnd, rightEnd, G)45  shows EvenEdgeSet(V, leftEnd, rightEnd, F △ G)46proof47  have finiteF := first.left48  have finiteG := second.left49  constructor50  . have inside : F △ G ⊆ F ∪ G :=51      symmetricDifference.subset with union2.subset_left, union2.subset_right52    exact Finite.subset with (Finite.union with finiteF, finiteG), inside53  . intros v hv54    rw degreeIn.symmetricDifference_parity with finiteF, finiteG55    have evenF := first.right with v, hv56    have evenG := second.right with v, hv57    tauto5859theorem EvenEdgeSet.union_disjoint (V leftEnd rightEnd F G : Set)60  requires first : EvenEdgeSet(V, leftEnd, rightEnd, F)61  requires second : EvenEdgeSet(V, leftEnd, rightEnd, G)62  requires apart : Disjoint(F, G)63  shows EvenEdgeSet(V, leftEnd, rightEnd, F ∪ G)64proof65  have finiteF := first.left66  have finiteG := second.left67  constructor68  . exact Finite.union with finiteF, finiteG69  . intros v hv70    rw degreeIn.union_disjoint with finiteF, finiteG, apart71    exact Even.add with (first.right with v, hv), (second.right with v, hv)7273-- Of F, G, and F △ G, if two are even so is the third.74theorem EvenEdgeSet.of_symmetricDifference (V leftEnd rightEnd F G : Set)75  requires first : EvenEdgeSet(V, leftEnd, rightEnd, F)76  requires finite : Finite(G)77  requires difference : EvenEdgeSet(V, leftEnd, rightEnd, F △ G)78  shows EvenEdgeSet(V, leftEnd, rightEnd, G)79proof80  have finiteF := first.left81  constructor82  . exact finite83  . intros v hv84    have evenD := difference.right with v, hv85    rw degreeIn.symmetricDifference_parity with finiteF, finite at evenD86    exact evenD.forward with (first.right with v, hv)87