-- The values of an even cover at a vertex of a cubic loopless graph: vectors
-- over the two-element field with three coordinates are the subsets of 3, a
-- vertex meets exactly three edge ends, and the three values there are
-- nonzero, distinct, and sum to zero.
-- 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.CubicVertex
import Covers
import Flows.EvenCovers
import Combinatorics.ParityAlternative

-- Vectors over the two-element field with three coordinates are the subsets
-- of 3; the sum is the symmetric difference, the span of p is {∅, p}.
def span (p : Set) : Set := {∅, p}

theorem span.membership (p Z : Set)
  shows Z ∈ span(p) ↔ (Z = ∅ ∨ Z = p)
proof
  unfold span
  simp [pair.membership]

-- The span {∅, p} is closed under sums.
theorem span.sum (p X Y : Set)
  requires first : X ∈ span(p)
  requires second : Y ∈ span(p)
  shows X △ Y ∈ span(p)
proof
  rw span.membership at first, second
  rcases first with rfl | rfl
  . rcases second with rfl | rfl
    . simp [span.membership, symmetricDifference.self]
    . simp [span.membership, symmetricDifference.left_empty]
  . rcases second with rfl | rfl
    . simp [span.membership, symmetricDifference.empty]
    . simp [span.membership, symmetricDifference.self]

-- The value of an edge is a vector: a subset of 3, hence finite.
theorem flowValue.subset (F e : Set)
  shows flowValue(F, e) ⊆ 3
proof
  intros i hi
  exact hi.left

theorem flowValue.finite (F e : Set)
  shows Finite(flowValue(F, e))
proof
  exact Finite.subset with Finite.natural, flowValue.subset

-- A set of cardinality three is finite: the selected value of an infinite
-- set is the union of no candidates, which is empty.
theorem Finite.of_cardinality_three (A : Set)
  requires size : cardinality(A) = 3
  shows Finite(A)
proof
  by_contra infinite
  unfold cardinality at size
  have none : cardinality.candidates(A) = ∅
    ext n
    constructor
    . intro hn
      obtain ⟨_, has⟩ := hn
      exfalso
      exact infinite with ⟨n, has⟩
    . intro hn
      simp at hn
  rw none at size
  have twoIn : 2 ∈ 3 by simp [membership.three]
  rw ← size at twoIn
  rw union.membership at twoIn
  obtain ⟨y, hy, _⟩ := twoIn
  simp at hy

-- The parity of a subset of a three-element set, read off its members.
theorem EvenSet.of_three (S a b c : Set)
  requires apart : a ≠ b ∧ b ≠ c ∧ a ≠ c
  requires inside : S ⊆ ({a} ∪ {b}) ∪ {c}
  shows EvenSet(S) ↔ ((¬a ∈ S ↔ ¬b ∈ S) ↔ ¬c ∈ S)
proof
  have whole : S ∩ (({a} ∪ {b}) ∪ {c}) = S :=
    intersection.eq_left_of_subset with inside
  have finitePair : Finite({a} ∪ {b}) :=
    Finite.union with Finite.singleton, Finite.singleton
  have freshC : ¬c ∈ {a} ∪ {b} by simp
  have freshB : ¬b ∈ {a} by simp
  have stepC := EvenSet.intersection_union_part
    at S, {a} ∪ {b}, {c}, c with finitePair, Subset.reflexive, freshC
  have stepB := EvenSet.intersection_union_part
    at S, {a}, {b}, b with Finite.singleton, Subset.reflexive, freshB
  have stepA : EvenSet(S ∩ {a}) ↔ ¬a ∈ S
    rw intersection.commutative
    exact EvenSet.singleton_intersection
  rw whole at stepC
  rw [stepC, stepB, stepA]
  simp

-- Three distinct members of a three-element set are all of it: removing
-- them in turn leaves nothing.
theorem cardinality.three_members_eq (I a b c : Set)
  requires finite : Finite(I)
  requires size : cardinality(I) = 3
  requires members : a ∈ I ∧ b ∈ I ∧ c ∈ I
  requires apart : a ≠ b ∧ b ≠ c ∧ a ≠ c
  shows I = ({a} ∪ {b}) ∪ {c}
proof
  have finiteA : Finite(I ∖ {a}) := Finite.difference with finite
  have finiteB : Finite((I ∖ {a}) ∖ {b}) := Finite.difference with finiteA
  have finiteC : Finite(((I ∖ {a}) ∖ {b}) ∖ {c}) :=
    Finite.difference with finiteB
  have inA : b ∈ I ∖ {a} by simp [members.right.left, apart.left]
  have inB : c ∈ (I ∖ {a}) ∖ {b}
    by simp [members.right.right, apart.right.left, apart.right.right]
  have removeA := cardinality.remove_add_one with finite, members.left
  have removeB := cardinality.remove_add_one with finiteA, inA
  have removeC := cardinality.remove_add_one with finiteB, inB
  have zero : cardinality(((I ∖ {a}) ∖ {b}) ∖ {c}) = 0 by arith
  have none := cardinality.eq_empty_of_zero with finiteC, zero
  ext x
  constructor
  . intro hx
    by_contra outside
    have inside : x ∈ ((I ∖ {a}) ∖ {b}) ∖ {c} by simp
    rw none at inside
    simp at inside
  . intro hx
    simp at hx
    rcases hx with rfl | rfl | rfl
    . exact members.left
    . exact members.right.left
    . exact members.right.right

-- An edge at v has an end there.
theorem incidentEnds.end_of (leftEnd rightEnd E v e : Set)
  requires edge : e ∈ E
  requires incident : leftEnd(e) = v ∨ rightEnd(e) = v
  shows ∃ i ∈ 2, (e, i) ∈ incidentEnds(leftEnd, rightEnd, E, v)
proof
  cases incident with atLeft | atRight
  . refine ⟨0, _, _⟩
    . simp [membership.two]
    . simp [incidentEnds.pair, edge, atLeft]
  . refine ⟨1, _, _⟩
    . simp [membership.two]
    . simp [incidentEnds.pair, edge, atRight]

-- The ends of three distinct edges at a cubic vertex are all of its ends.
theorem Cubic.ends_of_three (V E leftEnd rightEnd v e f g : Set)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires vertex : v ∈ V
  requires edges : e ∈ E ∧ f ∈ E ∧ g ∈ E
  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧
    (leftEnd(g) = v ∨ rightEnd(g) = v)
  requires distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g
  shows ∃ i ∈ 2, ∃ j ∈ 2, ∃ k ∈ 2,
    ((e, i) ≠ (f, j) ∧ (f, j) ≠ (g, k) ∧ (e, i) ≠ (g, k)) ∧
    incidentEnds(leftEnd, rightEnd, E, v) = ({(e, i)} ∪ {(f, j)}) ∪ {(g, k)}
proof
  obtain ⟨i, hi, endE⟩ := incidentEnds.end_of with edges.left, incident.left
  obtain ⟨j, hj, endF⟩ :=
    incidentEnds.end_of with edges.right.left, incident.right.left
  obtain ⟨k, hk, endG⟩ :=
    incidentEnds.end_of with edges.right.right, incident.right.right
  have degree := cubic.left with v, vertex
  unfold degreeIn at degree
  have finite := Finite.of_cardinality_three with degree
  have apartEF : (e, i) ≠ (f, j)
    intro same
    exact distinct.left with (orderedPair.injective with same).left
  have apartFG : (f, j) ≠ (g, k)
    intro same
    exact distinct.right.left with (orderedPair.injective with same).left
  have apartEG : (e, i) ≠ (g, k)
    intro same
    exact distinct.right.right with (orderedPair.injective with same).left
  have apart : (e, i) ≠ (f, j) ∧ (f, j) ≠ (g, k) ∧ (e, i) ≠ (g, k) :=
    ⟨apartEF, apartFG, apartEG⟩
  have shape := cardinality.three_members_eq
    with finite, degree, ⟨endE, endF, endG⟩, apart
  exact ⟨i, hi, j, hj, k, hk, apart, shape⟩

-- At a cubic vertex with the distinct edges e, f, g, every edge there is
-- one of them.
theorem Cubic.among (V E leftEnd rightEnd v e f g x : Set)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires vertex : v ∈ V
  requires edges : e ∈ E ∧ f ∈ E ∧ g ∈ E
  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧
    (leftEnd(g) = v ∨ rightEnd(g) = v)
  requires distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g
  requires edge : x ∈ E
  requires atV : leftEnd(x) = v ∨ rightEnd(x) = v
  shows x = e ∨ x = f ∨ x = g
proof
  obtain ⟨i, hi, j, hj, k, hk, _, shape⟩ :=
    Cubic.ends_of_three with cubic, vertex, edges, incident, distinct
  obtain ⟨m, hm, endX⟩ := incidentEnds.end_of with edge, atV
  rw shape at endX
  simp at endX
  rcases endX with hxe | hxf | hxg
  . left
    exact (orderedPair.injective with hxe).left
  . right
    left
    exact (orderedPair.injective with hxf).left
  . right
    right
    exact (orderedPair.injective with hxg).left

-- Two ends of a non-loop edge at the same vertex are the same end.
theorem incidentEnds.same_edge (leftEnd rightEnd E v e i j : Set)
  requires loopless : leftEnd(e) ≠ rightEnd(e)
  requires first : (e, i) ∈ incidentEnds(leftEnd, rightEnd, E, v)
  requires second : (e, j) ∈ incidentEnds(leftEnd, rightEnd, E, v)
  shows i = j
proof
  have sidesI := (incidentEnds.pair.forward with first).right
  have sidesJ := (incidentEnds.pair.forward with second).right
  rcases sidesI with ⟨hi, atLeft⟩ | ⟨hi, atRight⟩
  . rcases sidesJ with ⟨hj, _⟩ | ⟨hj, atRight⟩
    . cc
    . exfalso
      apply loopless
      cc
  . rcases sidesJ with ⟨hj, atLeft⟩ | ⟨hj, _⟩
    . exfalso
      apply loopless
      cc
    . cc

-- Two further edges at an end v of e: removing the end of e from the three
-- ends at v leaves two, and distinct ends at a loopless vertex belong to
-- distinct edges.
theorem Cubic.others (V E leftEnd rightEnd 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 ∃ f ∈ E, ∃ g ∈ E, (e ≠ f ∧ f ≠ g ∧ e ≠ g) ∧
    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧ (leftEnd(g) = v ∨ rightEnd(g) = v)
proof
  obtain ⟨i, hi, endE⟩ := incidentEnds.end_of with edge, incident
  have degree := cubic.left with v, vertex
  unfold degreeIn at degree
  have finite := Finite.of_cardinality_three with degree
  have removeE := cardinality.remove_add_one with finite, endE
  have finiteRest :
      Finite(incidentEnds(leftEnd, rightEnd, E, v) ∖ {(e, i)}) :=
    Finite.difference with finite
  have positive :
      0 < cardinality(incidentEnds(leftEnd, rightEnd, E, v) ∖ {(e, i)})
    by arith
  obtain ⟨a, ha⟩ := cardinality.member_of_positive with finiteRest, positive
  have removeA := cardinality.remove_add_one with finiteRest, ha
  have finiteRest2 :
      Finite((incidentEnds(leftEnd, rightEnd, E, v) ∖ {(e, i)}) ∖ {a}) :=
    Finite.difference with finiteRest
  have positive2 : 0 <
      cardinality((incidentEnds(leftEnd, rightEnd, E, v) ∖ {(e, i)}) ∖ {a})
    by arith
  obtain ⟨b, hb⟩ := cardinality.member_of_positive with finiteRest2, positive2
  have partsA := difference.singleton_membership.forward with ha
  have partsB := difference.singleton_membership.forward with hb
  have partsB2 := difference.singleton_membership.forward with partsB.left
  obtain ⟨f, hf, j, hj, rfl⟩ := incidentEnds.shape with partsA.left
  obtain ⟨g, hg, k, hk, rfl⟩ := incidentEnds.shape with partsB2.left
  have atF := (incidentEnds.pair.forward with partsA.left).right
  have atG := (incidentEnds.pair.forward with partsB2.left).right
  have ef : e ≠ f
    intro same
    rw ← same at partsA
    have sides := incidentEnds.same_edge
      with (cubic.right with e, edge), partsA.left, endE
    apply partsA.right
    cc
  have eg : e ≠ g
    intro same
    rw ← same at partsB2
    have sides := incidentEnds.same_edge
      with (cubic.right with e, edge), partsB2.left, endE
    apply partsB2.right
    cc
  have fg : f ≠ g
    intro same
    rw same at partsA, partsB
    have sides := incidentEnds.same_edge
      with (cubic.right with g, hg), partsB2.left, partsA.left
    apply partsB.right
    cc
  have incidentF : leftEnd(f) = v ∨ rightEnd(f) = v by tauto
  have incidentG : leftEnd(g) = v ∨ rightEnd(g) = v by tauto
  have distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g := ⟨ef, fg, eg⟩
  exact ⟨f, hf, g, hg, distinct, incidentF, incidentG⟩

-- Three distinct edges at a cubic vertex.
theorem Cubic.ends_at (V E leftEnd rightEnd v : Set)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires vertex : v ∈ V
  shows ∃ e ∈ E, ∃ f ∈ E, ∃ g ∈ E, (e ≠ f ∧ f ≠ g ∧ e ≠ g) ∧
    (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧
    (leftEnd(g) = v ∨ rightEnd(g) = v)
proof
  have degree := cubic.left with v, vertex
  unfold degreeIn at degree
  have finite := Finite.of_cardinality_three with degree
  have positive : 0 < cardinality(incidentEnds(leftEnd, rightEnd, E, v))
    by arith
  obtain ⟨a, ha⟩ := cardinality.member_of_positive with finite, positive
  obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with ha
  have atE := (incidentEnds.pair.forward with ha).right
  have incidentE : leftEnd(e) = v ∨ rightEnd(e) = v by tauto
  obtain ⟨f, hf, g, hg, distinct, incidentF, incidentG⟩ :=
    Cubic.others with cubic, vertex, he, incidentE
  exact ⟨e, he, f, hf, g, hg, distinct, incidentE, incidentF, incidentG⟩

-- At a cubic vertex the three values are nonzero, pairwise distinct, and
-- their sum vanishes: the third is the sum of the other two.
theorem flowValue.cubic_vertex (V E leftEnd rightEnd F v e f g : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)
  requires vertex : v ∈ V
  requires edges : e ∈ E ∧ f ∈ E ∧ g ∈ E
  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧
    (leftEnd(g) = v ∨ rightEnd(g) = v)
  requires distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g
  shows flowValue(F, e) ≠ flowValue(F, f) ∧
    flowValue(F, g) = flowValue(F, e) △ flowValue(F, f)
proof
  obtain ⟨i, hi, j, hj, k, hk, apart, shape⟩ :=
    Cubic.ends_of_three with cubic, vertex, edges, incident, distinct
  have endE : (e, i) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp
  have endF : (f, j) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp
  have endG : (g, k) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp
  -- Conservation at v, coordinate by coordinate: the ends carrying x are
  -- even in number, so g carries x exactly when one of e, f does.
  have coordinate : ∀ x ∈ 3, (x ∈ flowValue(F, g) ↔
      ¬(x ∈ flowValue(F, e) ↔ x ∈ flowValue(F, f)))
    intros x hx
    have even := flowValue.conservation with cover, vertex, hx
    have inside : coordinateEnds(leftEnd, rightEnd, E, F, v, x) ⊆
        ({(e, i)} ∪ {(f, j)}) ∪ {(g, k)}
      rw ← shape
      intros p hp
      exact hp.left
    rw EvenSet.of_three with apart, inside at even
    simp [coordinateEnds.membership, endE, endF, endG, fst.pair] at even
    tauto
  have sum : flowValue(F, g) = flowValue(F, e) △ flowValue(F, f)
    ext x
    rw symmetricDifference.membership
    by_cases hx : x ∈ 3
    . exact coordinate with x, hx
    . simp [flowValue, hx]
  constructor
  . -- Equal values at e and f would make the value of g vanish.
    intro same
    have zero : flowValue(F, g) = ∅
      rw [sum, same]
      exact symmetricDifference.self
    have nonzero := flowValue.nonzero with cover, edges.right.right
    exact nonzero with zero
  . exact sum

-- Two distinct edges at a cubic vertex have distinct values: with the third
-- edge x there, value(f) is value(e) △ value(x), and value(x) is nonzero.
theorem flowValue.cubic_distinct (V E leftEnd rightEnd F v e f : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)
  requires vertex : v ∈ V
  requires edges : e ∈ E ∧ f ∈ E
  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
    (leftEnd(f) = v ∨ rightEnd(f) = v)
  requires distinct : e ≠ f
  shows flowValue(F, e) ≠ flowValue(F, f)
proof
  obtain ⟨x, hx, z, hz, apart, atX, atZ⟩ :=
    Cubic.others with cubic, vertex, edges.left, incident.left
  have edges3 : e ∈ E ∧ x ∈ E ∧ z ∈ E := ⟨edges.left, hx, hz⟩
  have incident3 : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
      (leftEnd(x) = v ∨ rightEnd(x) = v) ∧
      (leftEnd(z) = v ∨ rightEnd(z) = v) :=
    ⟨incident.left, atX, atZ⟩
  have triple := flowValue.cubic_vertex
    with graph, cubic, cover, vertex, edges3, incident3, apart
  have nonzeroX := flowValue.nonzero with cover, hx
  have cases := Cubic.among
    with cubic, vertex, edges3, incident3, apart, edges.right, incident.right
  rcases cases with same | same | same
  . cc
  . rw same
    exact triple.left
  . rw same
    intro equal
    apply nonzeroX
    ext i
    have bit := symmetricDifference.membership
      at i, flowValue(F, e), flowValue(F, x)
    rw [← triple.right, ← equal] at bit
    have none : ¬i ∈ flowValue(F, x) by tauto
    simp [none]