-- A cubic loopless graph with an even cover has an even double cover indexed
-- by the eight vectors: the compatibility system is unobstructed, so it has
-- a solution, whose vertex vectors are compatible and give the labels.
-- 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.DoubleCover.CubicLabeling
import Obstruction
import Set.Choice

-- The base points of e at v, and a chosen sum of base points at the two
-- ends of each edge, as a function on E.
def basePoints (V E leftEnd rightEnd F v e : Set) : Set :=
  { c ∈ 𝒫(3) | BasePoint(V, E, leftEnd, rightEnd, F, v, e, c) }

def baseSum (V E leftEnd rightEnd F e : Set) : Set :=
  choose(basePoints(V, E, leftEnd, rightEnd, F, leftEnd(e), e)) △
  choose(basePoints(V, E, leftEnd, rightEnd, F, rightEnd(e), e))

def baseFunction (V E leftEnd rightEnd F : Set) : Set :=
  { p ∈ E × 𝒫(3) | ∃ e ∈ E, p = (e, baseSum(V, E, leftEnd, rightEnd, F, e)) }

-- The value of another edge at v is a base point of e there.
theorem basePoints.nonempty (V E leftEnd rightEnd F v e : Set)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires vertex : v ∈ V
  requires edge : e ∈ E
  requires incident : leftEnd(e) = v ∨ rightEnd(e) = v
  shows Nonempty(basePoints(V, E, leftEnd, rightEnd, F, v, e))
proof
  obtain ⟨f, hf, g, hg, distinct, atF, _⟩ :=
    Cubic.others with cubic, vertex, edge, incident
  have inside : flowValue(F, f) ∈ 𝒫(3) :=
    powerset.membership_iff.backward with flowValue.subset
  have fe : f ≠ e by cc
  have point : BasePoint(V, E, leftEnd, rightEnd, F, v, e, flowValue(F, f)) :=
    ⟨f, hf, fe, atF, rfl⟩
  witness flowValue(F, f)
  exact ⟨inside, point⟩

theorem baseSum.subset (V E leftEnd rightEnd F e : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires edge : e ∈ E
  shows baseSum(V, E, leftEnd, rightEnd, F, e) ⊆ 3
proof
  have ends := Graph.ends with graph
  obtain ⟨vertexL, vertexR⟩ := ends with e, edge
  have atL : leftEnd(e) = leftEnd(e) ∨ rightEnd(e) = leftEnd(e) by simp
  have atR : leftEnd(e) = rightEnd(e) ∨ rightEnd(e) = rightEnd(e) by simp
  have chosenL := choose.member
    with (basePoints.nonempty at _, _, _, _, F, _, _
      with cubic, vertexL, edge, atL)
  have chosenR := choose.member
    with (basePoints.nonempty at _, _, _, _, F, _, _
      with cubic, vertexR, edge, atR)
  have insideL := powerset.membership_iff.forward with chosenL.left
  have insideR := powerset.membership_iff.forward with chosenR.left
  unfold baseSum
  exact symmetricDifference.subset with insideL, insideR

theorem baseFunction.function (V E leftEnd rightEnd F : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  shows baseFunction(V, E, leftEnd, rightEnd, F) : E → 𝒫(3)
proof
  constructor
  . intros p member
    exact member.left
  . constructor
    . intros x y xy z xz
      obtain ⟨_, a, _, shapeY⟩ := xy
      obtain ⟨_, b, _, shapeZ⟩ := xz
      obtain ⟨sameA, valueY⟩ := orderedPair.injective with shapeY
      obtain ⟨sameB, valueZ⟩ := orderedPair.injective with shapeZ
      cc
    . intros e he
      have inside : baseSum(V, E, leftEnd, rightEnd, F, e) ∈ 𝒫(3) :=
        powerset.membership_iff.backward
          with (baseSum.subset with graph, cubic, he)
      refine ⟨baseSum(V, E, leftEnd, rightEnd, F, e), inside, _⟩
      exact baseFunction.membership.backward
        with ⟨(product.pair with he, inside), e, he, rfl⟩

theorem baseFunction.value (V E leftEnd rightEnd F e : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires member : e ∈ E
  shows baseFunction(V, E, leftEnd, rightEnd, F)(e) =
    baseSum(V, E, leftEnd, rightEnd, F, e)
proof
  have inside : baseSum(V, E, leftEnd, rightEnd, F, e) ∈ 𝒫(3) :=
    powerset.membership_iff.backward
      with (baseSum.subset with graph, cubic, member)
  have related : relates(baseFunction(V, E, leftEnd, rightEnd, F), e,
      baseSum(V, E, leftEnd, rightEnd, F, e)) :=
    baseFunction.membership.backward
      with ⟨(product.pair with member, inside), e, member, rfl⟩
  have function := baseFunction.function at _, _, _, _, F with graph, cubic
  exact FunctionBetween.apply_value with function, member, related

-- The chosen sums of base points form a base assignment.
theorem baseFunction.base (V E leftEnd rightEnd F : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  shows FunctionBetween(baseFunction(V, E, leftEnd, rightEnd, F), E, 𝒫(3)) ∧
    (∀ e ∈ E, ∃ a, ∃ b,
      BasePoint(V, E, leftEnd, rightEnd, F, leftEnd(e), e, a) ∧
      BasePoint(V, E, leftEnd, rightEnd, F, rightEnd(e), e, b) ∧
      baseFunction(V, E, leftEnd, rightEnd, F)(e) = a △ b)
proof
  have ends := Graph.ends with graph
  constructor
  . exact baseFunction.function at _, _, _, _, F with graph, cubic
  . intros e he
    obtain ⟨vertexL, vertexR⟩ := ends with e, he
    have atL : leftEnd(e) = leftEnd(e) ∨ rightEnd(e) = leftEnd(e) by simp
    have atR : leftEnd(e) = rightEnd(e) ∨ rightEnd(e) = rightEnd(e) by simp
    have chosenL := choose.member
      with (basePoints.nonempty at _, _, _, _, F, _, _
        with cubic, vertexL, he, atL)
    have chosenR := choose.member
      with (basePoints.nonempty at _, _, _, _, F, _, _
        with cubic, vertexR, he, atR)
    have value := baseFunction.value at _, _, _, _, F, _ with graph, cubic, he
    unfold baseSum at value
    witness choose(basePoints(V, E, leftEnd, rightEnd, F, leftEnd(e), e))
    witness choose(basePoints(V, E, leftEnd, rightEnd, F, rightEnd(e), e))
    exact ⟨chosenL.right, chosenR.right, value⟩

-- A cubic loopless graph with an even cover has an even double cover indexed
-- by the eight vectors: the compatibility system is unobstructed, so it has
-- a solution, whose vertex vectors are compatible and give the labels.
theorem Cubic.even_double_cover (V E leftEnd rightEnd F : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires finiteEdges : Finite(E)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)
  shows ∃ H, EvenDoubleCover(V, E, leftEnd, rightEnd, H, 𝒫(3))
proof
  have base := baseFunction.base at _, _, _, _, F with graph, cubic
  have unobstructed := compatibility.unobstructed
    with graph, finiteVertices, finiteEdges, cubic, cover, base
  have finiteThree := Finite.natural at 3
  have finiteRows : Finite(E × 3) :=
    Finite.product with finiteEdges, finiteThree
  have finiteColumns : Finite((V × 3) ∪ (E × {3})) :=
    Finite.union with (Finite.product with finiteVertices, finiteThree),
      (Finite.product with finiteEdges, Finite.singleton)
  have matrix : compatibilityMatrix(V, E, leftEnd, rightEnd, F) ⊆
      (E × 3) × ((V × 3) ∪ (E × {3}))
    intros p hp
    exact hp.left
  have side : compatibilitySide(E, baseFunction(V, E, leftEnd, rightEnd, F)) ⊆
      E × 3
    intros p hp
    exact hp.left
  have alternative := paritySystem.alternative
    with finiteRows, finiteColumns, matrix, side
  obtain ⟨t, solution⟩ := alternative.backward with unobstructed
  obtain ⟨u, compatible⟩ :=
    Compatible.of_solution with graph, cubic, base.left, solution
  obtain ⟨P, function, two, balanced⟩ := Compatible.labels
    with graph, finiteEdges, cubic, cover, base, compatible
  have finiteLabels : Finite(𝒫(3)) := Finite.powerset with finiteThree
  have labels : FunctionBetween(P, E, 𝒫(𝒫(3))) ∧
      (∀ e ∈ E, cardinality(P(e)) = 2) := ⟨function, two⟩
  witness labelFamily(E, P, 𝒫(3))
  exact labels.double_cover
    with graph, finiteEdges, finiteLabels, labels, balanced