-- Every finite bridgeless multigraph has an even cover: the eight-flow
-- theorem of Jaeger and Kilpatrick, by induction on the number of vertices
-- through cuts of size zero and two, with three spanning trees in the
-- 3-edge-connected case.
-- 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.Flows.EightFlow
import Splits

-- Section: The cases of the induction.

-- A bridgeless graph that is neither split nor 3-edge-connected has a cut of
-- exactly two edges, and both of its edges are proper.
theorem Bridgeless.two_cut (V E leftEnd rightEnd : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires finiteEdges : Finite(E)
  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)
  requires unsplit : ∀ X ⊆ V, X ≠ ∅ → X ≠ V →
    crossing(leftEnd, rightEnd, E, X) ≠ ∅
  requires loose : ¬EdgeConnected(V, E, leftEnd, rightEnd, 3)
  shows ∃ X, ∃ e ∈ E, ∃ f ∈ E, X ⊆ V ∧ e ≠ f ∧
    crossing(leftEnd, rightEnd, E, X) = {e, f}
proof
  -- Some nonempty proper vertex set is left by fewer than three edges.
  have witnessX : ∃ X ⊆ V, X ≠ ∅ ∧ X ≠ V ∧
      ¬(3 ≤ cardinality(crossing(leftEnd, rightEnd, E, X)))
    by_contra none
    apply loose
    intros X bound nonempty proper
    by_contra few
    exact none with ⟨X, bound, nonempty, proper, few⟩
  obtain ⟨X, bound, nonempty, proper, few⟩ := witnessX
  have finiteCut := crossing.finite at leftEnd, rightEnd, E, X with finiteEdges
  have natCut := cardinality.nat with finiteCut
  have notOne := bridgeless with X, bound
  have notZero : cardinality(crossing(leftEnd, rightEnd, E, X)) ≠ 0
    intro zero
    exact unsplit with X, bound, nonempty, proper,
      (cardinality.eq_empty_of_zero with finiteCut, zero)
  -- Neither zero, one, nor three or more: the cut has exactly two edges.
  have less := Less.of_not_LessEqual with few
  have upper : cardinality(crossing(leftEnd, rightEnd, E, X)) ≤ 2 by arith
  have lower : 2 ≤ cardinality(crossing(leftEnd, rightEnd, E, X))
    have cases := natural.zero_one_or_above_one
      at cardinality(crossing(leftEnd, rightEnd, E, X))
    rcases cases with zero | one | above
    . exfalso
      exact notZero with zero
    . exfalso
      exact notOne with one
    . have strict := Less.of_membership with above
      arith
  have two := LessEqual.antisymmetric with upper, lower
  -- One edge of the cut, and the rest is a single other edge.
  have positive : 0 < cardinality(crossing(leftEnd, rightEnd, E, X)) by arith
  obtain ⟨e, he⟩ := cardinality.member_of_positive with finiteCut, positive
  have removed := cardinality.remove_add_one with finiteCut, he
  have oneLeft : cardinality(crossing(leftEnd, rightEnd, E, X) ∖ {e}) = 1
    arith
  have finiteRest := Finite.difference
    at crossing(leftEnd, rightEnd, E, X), {e} with finiteCut
  have oneIff := cardinality.one_iff with finiteRest
  obtain ⟨f, single⟩ := oneIff.forward with oneLeft
  have fMember : f ∈ crossing(leftEnd, rightEnd, E, X) ∖ {e}
    rw single
    exact singleton.self
  obtain ⟨fIn, fNotE⟩ := difference.membership.forward with fMember
  have distinct : e ≠ f
    intro same
    apply fNotE
    rw same
    exact singleton.self
  have cutEdges := crossing.subset at leftEnd, rightEnd, E, X
  refine ⟨X, e, (cutEdges with e, he), f, (cutEdges with f, fIn),
    bound, distinct, _⟩
  ext g
  constructor
  . intro hg
    by_cases ge : g = e
    . simp [ge]
    . have inRest : g ∈ crossing(leftEnd, rightEnd, E, X) ∖ {e}
        simp [hg, ge]
      rw single at inRest
      simp at inRest
      simp [inRest]
  . intro hg
    simp at hg
    rcases hg with rfl | rfl
    . exact he
    . exact fIn

-- One vertex: every edge is a loop and E itself is an even set.
theorem EvenCover.single_vertex (V E leftEnd rightEnd : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteEdges : Finite(E)
  requires single : ∃ v, V = {v}
  shows ∃ F, EvenCover(V, E, leftEnd, rightEnd, F)
proof
  obtain ⟨v, rfl⟩ := single
  have endsE := Graph.ends with graph
  have vertex : v ∈ {v} := singleton.self
  -- Every edge is a loop at v, so E is even: its degree at v is 2|E|.
  have even : EvenEdgeSet({v}, leftEnd, rightEnd, E)
    constructor
    . exact finiteEdges
    . intros w hw
      rw singleton.membership at hw
      rw hw
      have sum := degreeIn.handshake
        with (Finite.singleton at v), finiteEdges, endsE
      have weights := degreeWeights.natural at {v}, leftEnd, rightEnd, E
        with finiteEdges
      rw [(natSum.singleton with (weights with v, vertex)),
        (degreeWeights.value with finiteEdges, vertex)] at sum
      rw sum
      exact Even.two_mul
  have member : E ∈ 𝒫(E) :=
    powerset.membership_iff.backward with Subset.reflexive
  have values := tripleMap.value with member, member, member
  have zero : 0 ∈ 3 by simp [membership.three]
  witness tripleMap(𝒫(E), E, E, E)
  refine ⟨(tripleMap.function with member, member, member), _, _⟩
  . intros i hi
    have cases := membership.three.forward with hi
    rcases cases with rfl | rfl | rfl
    . rw values.left
      exact even
    . rw values.right.left
      exact even
    . rw values.right.right
      exact even
  . intros e he
    refine ⟨0, zero, _⟩
    rw values.left
    exact he

-- Without vertices there are no edges, and the empty triple is a cover.
theorem EvenCover.of_no_vertices (V E leftEnd rightEnd : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires noVertices : V = ∅
  shows ∃ F, EvenCover(V, E, leftEnd, rightEnd, F)
proof
  have noEdges : E = ∅
    ext e
    constructor
    . intro he
      have inV := (Graph.ends with graph, e, he).left
      rw noVertices at inV
      simp at inV
    . intro he
      simp at he
  have member : ∅ ∈ 𝒫(E) :=
    powerset.membership_iff.backward with empty.subset
  have values := tripleMap.value with member, member, member
  witness tripleMap(𝒫(E), ∅, ∅, ∅)
  refine ⟨(tripleMap.function with member, member, member), _, _⟩
  . intros i hi
    have cases := membership.three.forward with hi
    rcases cases with rfl | rfl | rfl
    . rw values.left
      exact EvenEdgeSet.empty
    . rw values.right.left
      exact EvenEdgeSet.empty
    . rw values.right.right
      exact EvenEdgeSet.empty
  . intros e he
    rw noEdges at he
    simp at he

-- Section: The eight-flow theorem.

-- A side of a split, with the ends restricted to its inside, is a finite
-- bridgeless graph on fewer vertices; the induction hypothesis covers it, and
-- the cover is one for the original ends.
theorem eightFlow.side (V E leftEnd rightEnd X : Set, n : Nat)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires finiteEdges : Finite(E)
  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)
  requires split : X ⊆ V ∧ crossing(leftEnd, rightEnd, E, X) = ∅
  requires proper : X ≠ V
  requires bound : cardinality(V) ≤ n + 1
  requires ih : ∀ W, ∀ D, ∀ leftW, ∀ rightW,
    Graph(W, D, leftW, rightW) → Finite(W) → Finite(D) →
    Bridgeless(W, D, leftW, rightW) → cardinality(W) ≤ n →
    ∃ F, EvenCover(W, D, leftW, rightW, F)
  shows ∃ F, EvenCover(X, inside(leftEnd, rightEnd, E, X), leftEnd, rightEnd,
    F)
proof
  have edges := inside.subset at leftEnd, rightEnd, E, X
  have sideGraph := inside.graph with graph, split.left
  have sideBridgeless := inside.bridgeless with graph, split, bridgeless
  have finiteX := Finite.subset with finiteVertices, split.left
  have finiteInside := Finite.subset with finiteEdges, edges
  have less := cardinality.strict_of_ne with finiteVertices, split.left, proper
  have smaller : cardinality(X) ≤ n by arith
  have recursive := ih with X, inside(leftEnd, rightEnd, E, X),
    restrict(leftEnd, inside(leftEnd, rightEnd, E, X)),
    restrict(rightEnd, inside(leftEnd, rightEnd, E, X))
  obtain ⟨F, cover⟩ := recursive
    with sideGraph, finiteX, finiteInside, sideBridgeless, smaller
  exact ⟨F, (EvenCover.of_restricted with graph, edges, cover)⟩

-- The theorem, by induction on the number of vertices: a split joins the
-- covers of its two sides, a cut of two edges contracts one of them to a
-- graph with one vertex fewer, and otherwise the graph is 3-edge-connected.
theorem eightFlow.of_vertex_count (n : Nat)
  shows ∀ V, ∀ E, ∀ leftEnd, ∀ rightEnd,
    Graph(V, E, leftEnd, rightEnd) → Finite(V) → Finite(E) →
    Bridgeless(V, E, leftEnd, rightEnd) → cardinality(V) ≤ n →
    ∃ F, EvenCover(V, E, leftEnd, rightEnd, F)
proof
  induction n
  | zero =>
    intros V E leftEnd rightEnd graph finiteVertices finiteEdges bridgeless
      bound
    have natV := cardinality.nat with finiteVertices
    have zero : cardinality(V) = 0 by arith
    exact EvenCover.of_no_vertices
      with graph, (cardinality.eq_empty_of_zero with finiteVertices, zero)
  | k + 1 using ih =>
    intros V E leftEnd rightEnd graph finiteVertices finiteEdges bridgeless
      bound
    have endsE := Graph.ends with graph
    have natV := cardinality.nat with finiteVertices
    by_cases nonempty : V = ∅
    . exact EvenCover.of_no_vertices with graph, nonempty
    by_cases unsplit : ∀ X ⊆ V, X ≠ ∅ → X ≠ V →
      crossing(leftEnd, rightEnd, E, X) ≠ ∅
    . by_cases connected : EdgeConnected(V, E, leftEnd, rightEnd, 3)
      . exact EvenCover.of_three_edge_connected
          with graph, finiteVertices, finiteEdges, nonempty, connected
      . -- A cut of two edges: contract one of them and lift the cover.
        obtain ⟨X, e, eInE, f, fInE, subset, distinct, cut⟩ :=
          Bridgeless.two_cut with graph, finiteVertices, finiteEdges,
            bridgeless, unsplit, connected
        have eInCut : e ∈ crossing(leftEnd, rightEnd, E, X)
          rw cut
          exact pair.left
        have proper : leftEnd(e) ≠ rightEnd(e)
          intro same
          rcases eInCut.right with ⟨leftX, rightX⟩ | ⟨rightX, leftX⟩
          . rw same at leftX
            exact rightX with leftX
          . rw same at leftX
            exact leftX with rightX
        have count := contraction.vertex_count
          with graph, finiteVertices, eInE, proper
        have finiteClasses :
            Finite(contractionPartition(V, leftEnd, rightEnd, e))
          unfold contractionPartition
          exact componentsBy.finite with finiteVertices
        have natClasses := cardinality.nat with finiteClasses
        have smaller :
            cardinality(contractionPartition(V, leftEnd, rightEnd, e)) ≤ k
          arith
        have recursive := ih
          with contractionPartition(V, leftEnd, rightEnd, e), E ∖ {e},
            contractedLeft(V, E, leftEnd, rightEnd, e),
            contractedRight(V, E, leftEnd, rightEnd, e)
        obtain ⟨F, cover⟩ := recursive
          with (contraction.graph with graph, eInE), finiteClasses,
          (Finite.difference with finiteEdges),
          (contraction.bridgeless with graph, finiteEdges, eInE, bridgeless),
          smaller
        exact contraction.lift_cover with graph, finiteVertices, finiteEdges,
          ⟨subset, cut, distinct⟩, cover
    . -- A nonempty proper vertex set left by no edge: cover each side.
      have witnessX : ∃ X ⊆ V, X ≠ ∅ ∧ X ≠ V ∧
          crossing(leftEnd, rightEnd, E, X) = ∅
        by_contra none
        apply unsplit
        intros X inV nonemptyX properX split
        exact none with ⟨X, inV, nonemptyX, properX, split⟩
      obtain ⟨X, subsetX, nonemptyX, properX, none⟩ := witnessX
      have complement : V ∖ X ⊆ V ∧
          crossing(leftEnd, rightEnd, E, V ∖ X) = ∅
        refine ⟨difference.subset_left, _⟩
        rw crossing.complement with endsE
        exact none
      have properY : V ∖ X ≠ V
        intro same
        obtain ⟨v, hv⟩ := Nonempty.of_ne_empty with nonemptyX
        have inV := subsetX with v, hv
        rw ← same at inV
        exact (difference.membership.forward with inV).right with hv
      obtain ⟨F, coverX⟩ := eightFlow.side with graph, finiteVertices,
        finiteEdges, bridgeless, ⟨subsetX, none⟩, properX, bound, ih
      obtain ⟨G, coverY⟩ := eightFlow.side with graph, finiteVertices,
        finiteEdges, bridgeless, complement, properY, bound, ih
      exact EvenCover.join with graph, ⟨subsetX, none⟩, coverX, coverY

theorem eightFlow (V E leftEnd rightEnd : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires finiteEdges : Finite(E)
  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)
  shows ∃ F, EvenCover(V, E, leftEnd, rightEnd, F)
proof
  have natV := cardinality.nat with finiteVertices
  have all := eightFlow.of_vertex_count at cardinality(V)
  exact all with V, E, leftEnd, rightEnd, graph, finiteVertices, finiteEdges,
    bridgeless, (LessEqual.reflexive at cardinality(V))