-- The compatibility condition as a parity system: the unknowns are the
-- coordinates of the vertex vectors and one switch per edge, the rows the
-- coordinates of the edges, and a solution gives a compatible assignment.
-- 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.CompatibilitySystem
import Labels

-- The parity system of the compatibility condition: unknowns are the
-- coordinates (v, i) of the vertex vectors and one switch (e, 3) per edge,
-- tagged so that it never coincides with a vertex coordinate; rows are the
-- coordinates (e, i) of the edges.
def compatibilityMatrix (V E leftEnd rightEnd F : Set) : Set :=
  { p ∈ (E × 3) × ((V × 3) ∪ (E × {3})) | ∃ e ∈ E, ∃ i ∈ 3,
    p = ((e, i), (leftEnd(e), i)) ∨ p = ((e, i), (rightEnd(e), i)) ∨
    (i ∈ flowValue(F, e) ∧ p = ((e, i), (e, 3))) }

def compatibilitySide (E d : Set) : Set :=
  { p ∈ E × 3 | ∃ e ∈ E, ∃ i ∈ 3, i ∈ d(e) ∧ p = (e, i) }

-- A coordinate of 3 is not the tag 3.
theorem membership.three.ne (i : Set)
  requires coordinate : i ∈ 3
  shows i ≠ 3
proof
  have cases := membership.three.forward with coordinate
  rcases cases with rfl | rfl | rfl
  . simp
  . simp
  . simp

-- The row (e, i) of the matrix meets the two vertex columns of the ends of
-- e and, when i lies in the value of e, the switch column of e.
theorem compatibilityMatrix.row (V E leftEnd rightEnd F e i c : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires edge : e ∈ E
  requires coordinate : i ∈ 3
  shows ((e, i), c) ∈ compatibilityMatrix(V, E, leftEnd, rightEnd, F) ↔
    (c = (leftEnd(e), i) ∨ c = (rightEnd(e), i) ∨
      (i ∈ flowValue(F, e) ∧ c = (e, 3)))
proof
  have ends := Graph.ends with graph
  obtain ⟨vertexL, vertexR⟩ := ends with e, edge
  constructor
  . intro hp
    obtain ⟨_, x, hx, j, hj, shape⟩ := hp
    rcases shape with h | h | h
    . have parts := orderedPair.injective with h
      have inner := orderedPair.injective with parts.left
      left
      cc
    . have parts := orderedPair.injective with h
      have inner := orderedPair.injective with parts.left
      right
      left
      cc
    . have parts := orderedPair.injective with h.right
      have inner := orderedPair.injective with parts.left
      have value := h.left
      right
      right
      constructor
      . cc
      . cc
  . intro hc
    have row : (e, i) ∈ E × 3 := product.pair with edge, coordinate
    have column : c ∈ (V × 3) ∪ (E × {3})
      rcases hc with h | h | h
      . rw h
        simp [product.pair_membership, vertexL, coordinate]
      . rw h
        simp [product.pair_membership, vertexR, coordinate]
      . rw h.right
        simp [product.pair_membership, edge]
    have shape : ((e, i), c) = ((e, i), (leftEnd(e), i)) ∨
        ((e, i), c) = ((e, i), (rightEnd(e), i)) ∨
        (i ∈ flowValue(F, e) ∧ ((e, i), c) = ((e, i), (e, 3)))
      rcases hc with h | h | h
      . left
        cc
      . right
        left
        cc
      . right
        right
        constructor
        . exact h.left
        . cc
    apply compatibilityMatrix.membership.backward
    exact ⟨(product.pair with row, column), e, edge, i, coordinate, shape⟩

-- The entries of the row (e, i): the column of either end of e, and the
-- switch column of e exactly when i lies in the value of e.
theorem compatibilityMatrix.end (V E leftEnd rightEnd F e i v : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires edge : e ∈ E
  requires coordinate : i ∈ 3
  requires incident : leftEnd(e) = v ∨ rightEnd(e) = v
  shows ((e, i), (v, i)) ∈ compatibilityMatrix(V, E, leftEnd, rightEnd, F)
proof
  rw compatibilityMatrix.row with graph, edge, coordinate
  rcases incident with h | h
  . left
    cc
  . right
    left
    cc

theorem compatibilityMatrix.switch (V E leftEnd rightEnd F e i : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires edge : e ∈ E
  requires coordinate : i ∈ 3
  shows ((e, i), (e, 3)) ∈ compatibilityMatrix(V, E, leftEnd, rightEnd, F) ↔
    i ∈ flowValue(F, e)
proof
  have tag := membership.three.ne with coordinate
  have notL : (e, 3) ≠ (leftEnd(e), i)
    intro same
    apply tag
    symm
    exact (orderedPair.injective with same).right
  have notR : (e, 3) ≠ (rightEnd(e), i)
    intro same
    apply tag
    symm
    exact (orderedPair.injective with same).right
  rw compatibilityMatrix.row with graph, edge, coordinate
  simp [notL, notR]

theorem compatibilitySide.pair (E d e i : Set)
  requires edge : e ∈ E
  requires coordinate : i ∈ 3
  shows (e, i) ∈ compatibilitySide(E, d) ↔ i ∈ d(e)
proof
  constructor
  . intro hp
    obtain ⟨_, x, hx, j, hj, value, shape⟩ := hp
    have parts := orderedPair.injective with shape
    cc
  . intro value
    apply compatibilitySide.membership.backward
    exact ⟨(product.pair with edge, coordinate), e, edge, i, coordinate,
      value, rfl⟩

-- The vertex vectors read off a solution t: v ↦ {i ∈ 3 | (v, i) ∈ t}; the
-- switch of e is value(e) when (e, 3) ∈ t and ∅ otherwise.
def coordinates (t v : Set) : Set := { i ∈ 3 | (v, i) ∈ t }

def vertexVectors (V t : Set) : Set :=
  { p ∈ V × 𝒫(3) | ∃ v ∈ V, p = (v, coordinates(t, v)) }

def switch (F t e : Set) : Set := { i ∈ flowValue(F, e) | (e, 3) ∈ t }

theorem coordinates.subset (t v : Set)
  shows coordinates(t, v) ⊆ 3
proof
  intros i hi
  exact hi.left

theorem vertexVectors.function (V t : Set)
  shows vertexVectors(V, t) : V → 𝒫(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 v hv
      have inside : coordinates(t, v) ∈ 𝒫(3) :=
        powerset.membership_iff.backward with coordinates.subset
      refine ⟨coordinates(t, v), inside, _⟩
      exact vertexVectors.membership.backward
        with ⟨(product.pair with hv, inside), v, hv, rfl⟩

theorem vertexVectors.value (V t v : Set)
  requires member : v ∈ V
  shows vertexVectors(V, t)(v) = coordinates(t, v)
proof
  have inside : coordinates(t, v) ∈ 𝒫(3) :=
    powerset.membership_iff.backward with coordinates.subset
  have related : relates(vertexVectors(V, t), v, coordinates(t, v)) :=
    vertexVectors.membership.backward
      with ⟨(product.pair with member, inside), v, member, rfl⟩
  exact FunctionBetween.apply_value
    with vertexVectors.function, member, related

theorem switch.span (F t e : Set)
  shows switch(F, t, e) ∈ span(flowValue(F, e))
proof
  rw span.membership
  by_cases on : (e, 3) ∈ t
  . right
    ext i
    simp [switch.membership, on]
  . left
    ext i
    simp [switch.membership, on]

-- A solution of the compatibility system gives compatible vertex vectors:
-- the row (e, i) says that t differs at (leftEnd(e), i) and (rightEnd(e), i)
-- exactly when i ∈ d(e), corrected by the switch when i ∈ value(e).
theorem Compatible.of_solution (V E leftEnd rightEnd F d t : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires side : FunctionBetween(d, E, 𝒫(3))
  requires solution : Solves(compatibilityMatrix(V, E, leftEnd, rightEnd, F),
    E × 3, (V × 3) ∪ (E × {3}), compatibilitySide(E, d), t)
  shows ∃ u, Compatible(V, E, leftEnd, rightEnd, F, u, d)
proof
  have ends := Graph.ends with graph
  witness vertexVectors(V, t)
  refine ⟨vertexVectors.function, ?_⟩
  intros e he
  obtain ⟨vertexL, vertexR⟩ := ends with e, he
  have loopless := cubic.right with e, he
  have inside : d(e) ⊆ 3 := powerset.membership_iff.forward
    with (FunctionBetween.apply_closed with side, he)
  witness switch(F, t, e)
  refine ⟨switch.span, ?_⟩
  rw [vertexVectors.value with vertexL, vertexVectors.value with vertexR]
  ext i
  rw [symmetricDifference.membership, symmetricDifference.membership]
  by_cases hi : i ∈ 3
  . -- The row (e, i) of the system, read on the three columns it can meet.
    have row : (e, i) ∈ E × 3 := product.pair with he, hi
    have parity := solution.right with (e, i), row
    rw compatibilitySide.pair with he, hi at parity
    have tag := membership.three.ne with hi
    have apartLR : (leftEnd(e), i) ≠ (rightEnd(e), i)
      intro same
      exact loopless with (orderedPair.injective with same).left
    have apartRS : (rightEnd(e), i) ≠ (e, 3)
      intro same
      exact tag with (orderedPair.injective with same).right
    have apartLS : (leftEnd(e), i) ≠ (e, 3)
      intro same
      exact tag with (orderedPair.injective with same).right
    have apart : (leftEnd(e), i) ≠ (rightEnd(e), i) ∧
        (rightEnd(e), i) ≠ (e, 3) ∧ (leftEnd(e), i) ≠ (e, 3) :=
      ⟨apartLR, apartRS, apartLS⟩
    have columns : fiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),
        (V × 3) ∪ (E × {3}), (e, i)) ∩ t ⊆
        ({(leftEnd(e), i)} ∪ {(rightEnd(e), i)}) ∪ {(e, 3)}
      intros c hc
      have entry := hc.left.right
      rw compatibilityMatrix.row with graph, he, hi at entry
      simp
    rw EvenSet.of_three with apart, columns at parity
    have columnL : (leftEnd(e), i) ∈ (V × 3) ∪ (E × {3})
      by simp [product.pair_membership, vertexL, hi]
    have columnR : (rightEnd(e), i) ∈ (V × 3) ∪ (E × {3})
      by simp [product.pair_membership, vertexR, hi]
    have columnS : (e, 3) ∈ (V × 3) ∪ (E × {3})
      by simp [product.pair_membership, 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 entryL : ((e, i), (leftEnd(e), i)) ∈
        compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=
      compatibilityMatrix.end with graph, he, hi, atL
    have entryR : ((e, i), (rightEnd(e), i)) ∈
        compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=
      compatibilityMatrix.end with graph, he, hi, atR
    have entryS : ((e, i), (e, 3)) ∈
        compatibilityMatrix(V, E, leftEnd, rightEnd, F) ↔
        i ∈ flowValue(F, e) :=
      compatibilityMatrix.switch with graph, he, hi
    simp [fiber.membership, columnL, columnR, columnS, entryL, entryR,
      entryS] at parity
    simp [coordinates.membership, switch.membership, hi]
  . -- Outside 3 none of the four sets holds i.
    have notD : ¬i ∈ d(e)
      intro h
      exact hi with (inside with i, h)
    simp [coordinates.membership, switch.membership, flowValue, hi, notD]