-- Even edge sets: every vertex meets an even number of edge ends. They are
-- the Eulerian subgraphs, and they form a group under symmetric difference.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.GraphTheory.Multigraph.Even
import Degree
import Cardinal.SumParity

predicate EvenEdgeSet (V leftEnd rightEnd F : Set) :=
  Finite(F) ∧ (∀ v ∈ V, Even(degreeIn(leftEnd, rightEnd, F, v)))

theorem EvenEdgeSet.empty (V leftEnd rightEnd : Set)
  shows EvenEdgeSet(V, leftEnd, rightEnd, ∅)
proof
  constructor
  . exact Finite.empty
  . intros v hv
    rw degreeIn.empty
    exact Even.zero

-- A loop contributes two ends at its vertex and none elsewhere.
theorem EvenEdgeSet.loop (V leftEnd rightEnd e : Set)
  requires loop : leftEnd(e) = rightEnd(e)
  shows EvenEdgeSet(V, leftEnd, rightEnd, {e})
proof
  constructor
  . exact Finite.singleton
  . intros v hv
    by_cases atV : leftEnd(e) = v
    . have right : rightEnd(e) = v by cc
      rw degreeIn.loop with atV, right
      exact Even.two
    . have right : rightEnd(e) ≠ v by cc
      rw degreeIn.absent with atV, right
      exact Even.zero

-- Degrees add modulo two under symmetric difference, so even sets are closed
-- under it.
theorem EvenEdgeSet.symmetricDifference (V leftEnd rightEnd F G : Set)
  requires first : EvenEdgeSet(V, leftEnd, rightEnd, F)
  requires second : EvenEdgeSet(V, leftEnd, rightEnd, G)
  shows EvenEdgeSet(V, leftEnd, rightEnd, F △ G)
proof
  have finiteF := first.left
  have finiteG := second.left
  constructor
  . have inside : F △ G ⊆ F ∪ G :=
      symmetricDifference.subset with union2.subset_left, union2.subset_right
    exact Finite.subset with (Finite.union with finiteF, finiteG), inside
  . intros v hv
    rw degreeIn.symmetricDifference_parity with finiteF, finiteG
    have evenF := first.right with v, hv
    have evenG := second.right with v, hv
    tauto

theorem EvenEdgeSet.union_disjoint (V leftEnd rightEnd F G : Set)
  requires first : EvenEdgeSet(V, leftEnd, rightEnd, F)
  requires second : EvenEdgeSet(V, leftEnd, rightEnd, G)
  requires apart : Disjoint(F, G)
  shows EvenEdgeSet(V, leftEnd, rightEnd, F ∪ G)
proof
  have finiteF := first.left
  have finiteG := second.left
  constructor
  . exact Finite.union with finiteF, finiteG
  . intros v hv
    rw degreeIn.union_disjoint with finiteF, finiteG, apart
    exact Even.add with (first.right with v, hv), (second.right with v, hv)

-- Of F, G, and F △ G, if two are even so is the third.
theorem EvenEdgeSet.of_symmetricDifference (V leftEnd rightEnd F G : Set)
  requires first : EvenEdgeSet(V, leftEnd, rightEnd, F)
  requires finite : Finite(G)
  requires difference : EvenEdgeSet(V, leftEnd, rightEnd, F △ G)
  shows EvenEdgeSet(V, leftEnd, rightEnd, G)
proof
  have finiteF := first.left
  constructor
  . exact finite
  . intros v hv
    have evenD := difference.right with v, hv
    rw degreeIn.symmetricDifference_parity with finiteF, finite at evenD
    exact evenD.forward with (first.right with v, hv)