-- The expansion of a bridgeless graph is bridgeless, and an even double
-- cover of the expansion projects along the spokes to an even double cover
-- of the graph.
-- 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.Projection
import Expansion

-- Section: Bridgelessness.

-- A set with one element has a member that every member equals.
theorem cardinality.member_of_one (A : Set)
  requires finite : Finite(A)
  requires one : cardinality(A) = 1
  shows ∃ a ∈ A, ∀ x ∈ A, x = a
proof
  have inhabited : A ≠ ∅
    intro empty
    rw [empty, cardinality.empty] at one
    contradiction
  obtain ⟨a, ha⟩ := Nonempty.of_ne_empty with inhabited
  have count := cardinality.remove_add_one with finite, ha
  have restFinite := Finite.difference at A, {a} with finite
  have zero : cardinality(A ∖ {a}) = 0 by arith
  have rest := cardinality.eq_empty_of_zero with restFinite, zero
  refine ⟨a, ha, _⟩
  intros x hx
  by_contra different
  have outside : x ∈ A ∖ {a} by simp [hx, different]
  rw rest at outside
  simp at outside

-- A vertex of degree one has a single end (e, i), and e is then the one
-- edge leaving {v}: a bridge. So a bridgeless graph has no such vertex.
theorem Bridgeless.degrees (V E leftEnd rightEnd : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteEdges : Finite(E)
  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)
  shows ∀ v ∈ V, degreeIn(leftEnd, rightEnd, E, v) ≠ 1
proof
  intros v hv one
  unfold degreeIn at one
  have finiteEnds := incidentEnds.finite at leftEnd, rightEnd, E, v
    with finiteEdges
  obtain ⟨p, hp, only⟩ := cardinality.member_of_one with finiteEnds, one
  obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with hp
  -- An edge leaving {v} has an end at v, so it is e; and e does leave {v},
  -- since its other end is not at v.
  have cut : crossing(leftEnd, rightEnd, E, {v}) = {e}
    ext f
    constructor
    . intro hf
      obtain ⟨inE, crosses⟩ := hf
      simp at crosses
      cases crosses with atLeft | atRight
      . have end : (f, 0) ∈ incidentEnds(leftEnd, rightEnd, E, v)
          simp [incidentEnds.pair, inE, atLeft]
        have same := only with (f, 0), end
        obtain ⟨rfl, _⟩ := orderedPair.injective with same
        simp
      . have end : (f, 1) ∈ incidentEnds(leftEnd, rightEnd, E, v)
          simp [incidentEnds.pair, inE, atRight]
        have same := only with (f, 1), end
        obtain ⟨rfl, _⟩ := orderedPair.injective with same
        simp
    . intro hf
      simp at hf
      rw hf
      refine ⟨he, _⟩
      have sides := (incidentEnds.pair.forward with hp).right
      rcases sides with ⟨rfl, atLeft⟩ | ⟨rfl, atRight⟩
      . have notRight : rightEnd(e) ≠ v
          intro atRight
          have end : (e, 1) ∈ incidentEnds(leftEnd, rightEnd, E, v)
            simp [incidentEnds.pair, he, atRight]
          have same := only with (e, 1), end
          have oneZero := (orderedPair.injective with same).right
          contradiction
        simp [atLeft, notRight]
      . have notLeft : leftEnd(e) ≠ v
          intro atLeft
          have end : (e, 0) ∈ incidentEnds(leftEnd, rightEnd, E, v)
            simp [incidentEnds.pair, he, atLeft]
          have same := only with (e, 0), end
          have oneZero := (orderedPair.injective with same).right
          contradiction
        simp [atRight, notLeft]
  have inV : {v} ⊆ V := singleton.subset_iff.backward with hv
  have bridge := bridgeless with {v}, inV
  rw [cut, cardinality.singleton] at bridge
  exact bridge with rfl

-- The vertices all of whose ends lie in a set X of ends.
def enclosed (V E leftEnd rightEnd X : Set) : Set :=
  { v ∈ V | incidentEnds(leftEnd, rightEnd, E, v) ⊆ X }

-- When X holds all or none of the ends at each vertex, an end of e lies in X
-- exactly when its vertex is enclosed.
theorem enclosed.left (V E leftEnd rightEnd X e : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires edge : e ∈ E
  requires whole : ∀ v ∈ V, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),
    h ∈ X → ∀ k ∈ incidentEnds(leftEnd, rightEnd, E, v), k ∈ X
  shows (e, 0) ∈ X ↔ leftEnd(e) ∈ enclosed(V, E, leftEnd, rightEnd, X)
proof
  have inV := (Graph.ends with graph, e, edge).left
  have atLeft : (e, 0) ∈ incidentEnds(leftEnd, rightEnd, E, leftEnd(e))
    simp [incidentEnds.pair, edge]
  constructor
  . intro inX
    exact ⟨inV, (whole with leftEnd(e), inV, (e, 0), atLeft, inX)⟩
  . intro inside
    exact inside.right with (e, 0), atLeft

theorem enclosed.right (V E leftEnd rightEnd X e : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires edge : e ∈ E
  requires whole : ∀ v ∈ V, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),
    h ∈ X → ∀ k ∈ incidentEnds(leftEnd, rightEnd, E, v), k ∈ X
  shows (e, 1) ∈ X ↔ rightEnd(e) ∈ enclosed(V, E, leftEnd, rightEnd, X)
proof
  have inV := (Graph.ends with graph, e, edge).right
  have atRight : (e, 1) ∈ incidentEnds(leftEnd, rightEnd, E, rightEnd(e))
    simp [incidentEnds.pair, edge]
  constructor
  . intro inX
    exact ⟨inV, (whole with rightEnd(e), inV, (e, 1), atRight, inX)⟩
  . intro inside
    exact inside.right with (e, 1), atRight

-- When no ring edge leaves X, the edges of the expansion leaving X are the
-- spokes of the edges leaving the enclosed vertices.
theorem enclosed.crossing (V E leftEnd rightEnd σ X : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)
  requires stable : ∀ h ∈ halfEdges(E), (h ∈ X ↔ σ(h) ∈ X)
  requires whole : ∀ v ∈ V, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),
    h ∈ X → ∀ k ∈ incidentEnds(leftEnd, rightEnd, E, v), k ∈ X
  shows crossing(expandedLeft(E, σ), expandedRight(E, σ),
      expandedEdges(E), X) =
    {0} × crossing(leftEnd, rightEnd, E, enclosed(V, E, leftEnd, rightEnd, X))
proof
  have function := RotationSystem.function with rotation
  ext x
  constructor
  . intro hx
    obtain ⟨inExpanded, crosses⟩ := hx
    have split := expandedEdges.cases with inExpanded
    rcases split with ⟨e, he, rfl⟩ | ⟨h, hh, rfl⟩
    . rw [(expandedLeft.spoke with he),
        (expandedRight.spoke with function, he),
        (enclosed.left with graph, he, whole),
        (enclosed.right with graph, he, whole)] at crosses
      apply product.pair_membership.backward
      constructor
      . simp
      . exact ⟨he, crosses⟩
    . rw [(expandedLeft.ring with hh),
        (expandedRight.ring with function, hh)] at crosses
      have same := stable with h, hh
      exfalso
      tauto
  . intro hx
    obtain ⟨_, z, hz, e, he, rfl⟩ := product.membership.forward with hx
    simp at hz
    rw hz
    obtain ⟨inE, crosses⟩ := he
    refine ⟨(spokes.edge with inE), _⟩
    rw [(expandedLeft.spoke with inE),
      (expandedRight.spoke with function, inE),
      (enclosed.left with graph, inE, whole),
      (enclosed.right with graph, inE, whole)]
    exact crosses

-- A cut of the expansion crossed by one edge is crossed by no ring edge, as
-- the ring edges form an even edge set; so it holds all or none of the ends
-- at each vertex, and pulling the ends of each vertex together gives a cut
-- of the graph crossed by one edge.
theorem expansion.bridgeless (V E leftEnd rightEnd σ : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires finiteEdges : Finite(E)
  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)
  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)
  shows Bridgeless(halfEdges(E), expandedEdges(E),
    expandedLeft(E, σ), expandedRight(E, σ))
proof
  intros X subset one
  have function := RotationSystem.function with rotation
  have finiteRingCut : Finite(crossing(expandedLeft(E, σ),
      expandedRight(E, σ), rings(E), X)) :=
    crossing.finite with (rings.finite with finiteEdges)
  -- No ring edge leaves X: an even number of them do, and at most one.
  have evenCount := EvenEdgeSet.crossing_even
    with (halfEdges.finite with finiteEdges),
      (rings.even with finiteEdges, rotation.left), subset
  have ringsInside : rings(E) ⊆ expandedEdges(E)
    unfold expandedEdges
    exact union2.subset_right
  have ringCut :
      crossing(expandedLeft(E, σ), expandedRight(E, σ), rings(E), X) ⊆
      crossing(expandedLeft(E, σ), expandedRight(E, σ), expandedEdges(E), X) :=
    crossing.monotone with ringsInside
  have bound := cardinality.monotone
    with (crossing.finite with (expandedEdges.finite with finiteEdges)),
      ringCut
  rw one at bound
  obtain ⟨m, hm, double⟩ := evenCount
  have zero : cardinality(crossing(expandedLeft(E, σ), expandedRight(E, σ),
      rings(E), X)) = 0
    rw double at bound
    rw double
    arith
  have noRing := cardinality.eq_empty_of_zero with finiteRingCut, zero
  have stable : ∀ h ∈ halfEdges(E), (h ∈ X ↔ σ(h) ∈ X)
    intros h hh
    by_contra
    have crosses : (1, h) ∈ crossing(expandedLeft(E, σ),
        expandedRight(E, σ), rings(E), X)
      refine ⟨(rings.member with hh), _⟩
      rw [(expandedLeft.ring with hh), (expandedRight.ring with function, hh)]
      tauto
    rw noRing at crosses
    simp at crosses
  -- So X holds all the ends at a vertex or none: σ runs through them all.
  have whole : ∀ v ∈ V, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),
      h ∈ X → ∀ k ∈ incidentEnds(leftEnd, rightEnd, E, v), k ∈ X
    intros v hv h hh inX k hk
    obtain ⟨n, hn, reach⟩ := rotation.right.right with v, hv, h, hh, k, hk
    have closed : ∀ x ∈ X, σ(x) ∈ X
      intros x hx
      exact (stable with x, (subset with x, hx)).forward with hx
    rw ← reach
    exact orbitStep.closed with closed, inX
  -- The enclosed vertices are then left by exactly one edge of the graph.
  have enclosedSubset : enclosed(V, E, leftEnd, rightEnd, X) ⊆ V
    intros v hv
    exact hv.left
  rw [(enclosed.crossing with graph, rotation, stable, whole),
    (cardinality.singleton_product
      with (crossing.finite with finiteEdges))] at one
  exact bridgeless with enclosed(V, E, leftEnd, rightEnd, X),
    enclosedSubset, one

-- Section: Projection.

-- The projection of an edge set of the expansion: the edges whose spokes it
-- holds.
def projected (E F : Set) : Set := { e ∈ E | (0, e) ∈ F }

theorem projected.subset (E F : Set)
  shows projected(E, F) ⊆ E
proof
  intros e he
  exact he.left

-- The edges of F leaving the ends at v are the spokes of the edges of the
-- projection leaving v: a ring edge has both ends at one vertex.
theorem projected.crossing (V E leftEnd rightEnd σ F v : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)
  requires edges : F ⊆ expandedEdges(E)
  requires vertex : v ∈ V
  shows crossing(expandedLeft(E, σ), expandedRight(E, σ), F,
      incidentEnds(leftEnd, rightEnd, E, v)) =
    {0} × crossing(leftEnd, rightEnd, projected(E, F), {v})
proof
  have function := RotationSystem.function with rotation
  ext x
  constructor
  . intro hx
    obtain ⟨inF, crosses⟩ := hx
    have split := expandedEdges.cases with (edges with x, inF)
    rcases split with ⟨e, he, rfl⟩ | ⟨h, hh, rfl⟩
    . rw [(expandedLeft.spoke with he), (expandedRight.spoke with function, he),
        (incidentEnds.left with he), (incidentEnds.right with he)] at crosses
      apply product.pair_membership.backward
      constructor
      . simp
      . have inProjection : e ∈ projected(E, F) := ⟨he, inF⟩
        refine ⟨inProjection, _⟩
        simp
    . rw [(expandedLeft.ring with hh),
        (expandedRight.ring with function, hh)] at crosses
      have same := RotationSystem.at_vertex with graph, rotation, vertex, hh
      exfalso
      tauto
  . intro hx
    obtain ⟨_, z, hz, e, he, rfl⟩ := product.membership.forward with hx
    simp at hz
    rw hz
    obtain ⟨inProjection, crosses⟩ := he
    obtain ⟨inE, inF⟩ := inProjection
    refine ⟨inF, _⟩
    rw [(expandedLeft.spoke with inE), (expandedRight.spoke with function, inE),
      (incidentEnds.left with inE), (incidentEnds.right with inE)]
    simp at crosses
    tauto

-- The projection of an even edge set is even: the edges of the projection
-- leaving v are counted by the edges of F leaving the ends at v, an even
-- number.
theorem projected.even (V E leftEnd rightEnd σ F : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteEdges : Finite(E)
  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)
  requires edges : F ⊆ expandedEdges(E)
  requires even : EvenEdgeSet(halfEdges(E), expandedLeft(E, σ),
    expandedRight(E, σ), F)
  shows EvenEdgeSet(V, leftEnd, rightEnd, projected(E, F))
proof
  have finiteProjected : Finite(projected(E, F)) :=
    Finite.subset with finiteEdges, projected.subset
  constructor
  . exact finiteProjected
  . intros v hv
    have finiteEnds := halfEdges.finite with finiteEdges
    have finitePoint : Finite({v}) := Finite.singleton
    have subset := incidentEnds.subset_halfEdges at leftEnd, rightEnd, E, v
    have evenCut := EvenEdgeSet.crossing_even with finiteEnds, even, subset
    rw [(projected.crossing with graph, rotation, edges, hv),
      (cardinality.singleton_product
        with (crossing.finite with finiteProjected)),
      (crossing.parity with finitePoint, finiteProjected)] at evenCut
    have inSingleton : v ∈ {v} by simp
    have weight := degreeWeights.value
      at {v}, leftEnd, rightEnd, projected(E, F), v
      with finiteProjected, inSingleton
    have natural :
        degreeWeights({v}, leftEnd, rightEnd, projected(E, F))(v) ∈ ℕ
      rw weight
      exact degreeIn.natural with finiteProjected
    rw [(natSum.singleton with natural), weight] at evenCut
    exact evenCut

-- The projection of a family of edge sets, member by member.
def projectedFamily (E H I : Set) : Set :=
  { p ∈ I × 𝒫(E) | ∃ i ∈ I, p = (i, projected(E, H(i))) }

theorem projectedFamily.function (E H I : Set)
  shows projectedFamily(E, H, I) : I → 𝒫(E)
proof
  constructor
  . intros p member
    exact member.left
  constructor
  . intros x y relatedY z relatedZ
    obtain ⟨_, a, _, shapeY⟩ := relatedY
    obtain ⟨_, b, _, shapeZ⟩ := relatedZ
    obtain ⟨sameA, valueY⟩ := orderedPair.injective with shapeY
    obtain ⟨sameB, valueZ⟩ := orderedPair.injective with shapeZ
    cc
  . intros i hi
    have inside : projected(E, H(i)) ∈ 𝒫(E) :=
      powerset.membership.backward with projected.subset
    refine ⟨projected(E, H(i)), inside, _⟩
    exact projectedFamily.membership.backward
      with ⟨(product.pair with hi, inside), i, hi, rfl⟩

theorem projectedFamily.value (E H I i : Set)
  requires index : i ∈ I
  shows projectedFamily(E, H, I)(i) = projected(E, H(i))
proof
  have inside : projected(E, H(i)) ∈ 𝒫(E) :=
    powerset.membership.backward with projected.subset
  have related : relates(projectedFamily(E, H, I), i, projected(E, H(i))) :=
    projectedFamily.membership.backward
      with ⟨(product.pair with index, inside), i, index, rfl⟩
  exact FunctionBetween.apply_value
    with projectedFamily.function, index, related

-- The members of the projected family holding e are those holding its spoke.
theorem projected.holding (E H I e : Set)
  requires edge : e ∈ E
  shows holding(projectedFamily(E, H, I), I, e) = holding(H, I, (0, e))
proof
  ext i
  by_cases hi : i ∈ I
  . have value := projectedFamily.value at E, H, I, i with hi
    simp [holding, projected, value, hi, edge]
  . simp [holding, hi]

-- An even double cover of the expansion projects to one of the graph: each
-- member projects to an even edge set, and an edge is held as often as its
-- spoke.
theorem projected.double_cover (V E leftEnd rightEnd σ H I : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteEdges : Finite(E)
  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)
  requires cover : EvenDoubleCover(halfEdges(E), expandedEdges(E),
    expandedLeft(E, σ), expandedRight(E, σ), H, I)
  shows EvenDoubleCover(V, E, leftEnd, rightEnd, projectedFamily(E, H, I), I)
proof
  obtain ⟨finiteIndex, family, evens, twice⟩ := cover
  refine ⟨finiteIndex, projectedFamily.function, _, _⟩
  . intros i hi
    rw projectedFamily.value with hi
    have edges : H(i) ⊆ expandedEdges(E) :=
      powerset.membership.forward
        with (FunctionBetween.apply_closed with family, hi)
    exact projected.even
      with graph, finiteEdges, rotation, edges, (evens with i, hi)
  . intros e he
    have spoke := twice with (0, e), (spokes.edge with he)
    unfold multiplicity at spoke
    unfold multiplicity
    rw projected.holding with he
    exact spoke