-- The cubic expansion of a multigraph along a rotation system: the vertices
-- are the edge ends, the spoke of an edge joins its two ends, and the ring
-- edges at a vertex run around the cycle of its ends. The expansion is a
-- graph, and it is cubic and loopless when every degree is at least two.
-- 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.Expansion
import RotationSystems

-- Section: The expanded graph.

-- The expanded graph has the ends as vertices. The spoke (0, e) of an edge
-- e joins its ends (e, 0) and (e, 1); the ring edge (1, h) of an end h joins
-- h to σ(h), so the ring edges at a vertex run around the cycle of its ends.
def spokes (E : Set) : Set := {0} × E
def rings (E : Set) : Set := {1} × halfEdges(E)
def expandedEdges (E : Set) : Set := spokes(E) ∪ rings(E)
def expandedLeft (E σ : Set) : Set :=
  { p ∈ expandedEdges(E) × halfEdges(E) |
    ∃ e ∈ E, p = ((0, e), (e, 0)) ∨
      (∃ h ∈ halfEdges(E), p = ((1, h), h)) }
def expandedRight (E σ : Set) : Set :=
  { p ∈ expandedEdges(E) × halfEdges(E) |
    ∃ e ∈ E, p = ((0, e), (e, 1)) ∨
      (∃ h ∈ halfEdges(E), p = ((1, h), σ(h))) }

theorem spokes.member (E e : Set)
  requires edge : e ∈ E
  shows (0, e) ∈ spokes(E)
proof
  unfold spokes
  simp [product.pair_membership, edge]

theorem rings.member (E h : Set)
  requires end : h ∈ halfEdges(E)
  shows (1, h) ∈ rings(E)
proof
  unfold rings
  simp [product.pair_membership, end]

theorem spokes.edge (E e : Set)
  requires edge : e ∈ E
  shows (0, e) ∈ expandedEdges(E)
proof
  unfold expandedEdges
  simp [(spokes.member with edge)]

theorem rings.edge (E h : Set)
  requires end : h ∈ halfEdges(E)
  shows (1, h) ∈ expandedEdges(E)
proof
  unfold expandedEdges
  simp [(rings.member with end)]

-- An edge of the expansion is a spoke or a ring edge.
theorem expandedEdges.cases (E x : Set)
  requires member : x ∈ expandedEdges(E)
  shows (∃ e ∈ E, x = (0, e)) ∨ (∃ h ∈ halfEdges(E), x = (1, h))
proof
  unfold expandedEdges at member
  have split := union2.membership.forward with member
  cases split with spoke | ring
  . unfold spokes at spoke
    obtain ⟨_, z, hz, e, he, rfl⟩ := product.membership.forward with spoke
    simp at hz
    left
    refine ⟨e, he, _⟩
    rw hz
  . unfold rings at ring
    obtain ⟨_, z, hz, h, hh, rfl⟩ := product.membership.forward with ring
    simp at hz
    right
    refine ⟨h, hh, _⟩
    rw hz

-- Spokes and ring edges are told apart by their first coordinate.
theorem expandedEdges.apart (E : Set)
  shows Disjoint(spokes(E), rings(E))
proof
  have heads : Disjoint({0}, {1})
    apply Disjoint.iff.backward
    intros x hx
    simp at hx
    rw hx
    simp
  unfold spokes
  unfold rings
  exact product.disjoint_of_left with heads

-- The expansion of a finite graph is finite.
theorem spokes.finite (E : Set)
  requires finiteEdges : Finite(E)
  shows Finite(spokes(E))
proof
  unfold spokes
  exact Finite.product with Finite.singleton, finiteEdges

theorem rings.finite (E : Set)
  requires finiteEdges : Finite(E)
  shows Finite(rings(E))
proof
  unfold rings
  have finiteEnds := halfEdges.finite with finiteEdges
  exact Finite.product with Finite.singleton, finiteEnds

theorem expandedEdges.finite (E : Set)
  requires finiteEdges : Finite(E)
  shows Finite(expandedEdges(E))
proof
  unfold expandedEdges
  exact Finite.union with (spokes.finite with finiteEdges),
    (rings.finite with finiteEdges)

-- The end maps, read off their graphs: a spoke (0, e) runs from (e, 0) to
-- (e, 1), a ring edge (1, h) from h to σ(h).
theorem expandedLeft.of_relates (E σ x y : Set)
  requires related : relates(expandedLeft(E, σ), x, y)
  shows (∃ e ∈ E, x = (0, e) ∧ y = (e, 0)) ∨
    (∃ h ∈ halfEdges(E), x = (1, h) ∧ y = h)
proof
  obtain ⟨_, e, he, shape⟩ := related
  rcases shape with spoke | ⟨h, hh, ring⟩
  . obtain ⟨rfl, rfl⟩ := orderedPair.injective with spoke
    left
    exact ⟨e, he, rfl, rfl⟩
  . obtain ⟨rfl, rfl⟩ := orderedPair.injective with ring
    right
    exact ⟨h, hh, rfl, rfl⟩

theorem expandedRight.of_relates (E σ x y : Set)
  requires related : relates(expandedRight(E, σ), x, y)
  shows (∃ e ∈ E, x = (0, e) ∧ y = (e, 1)) ∨
    (∃ h ∈ halfEdges(E), x = (1, h) ∧ y = σ(h))
proof
  obtain ⟨_, e, he, shape⟩ := related
  rcases shape with spoke | ⟨h, hh, ring⟩
  . obtain ⟨rfl, rfl⟩ := orderedPair.injective with spoke
    left
    exact ⟨e, he, rfl, rfl⟩
  . obtain ⟨rfl, rfl⟩ := orderedPair.injective with ring
    right
    exact ⟨h, hh, rfl, rfl⟩

theorem expandedLeft.spoke_relates (E σ e : Set)
  requires edge : e ∈ E
  shows relates(expandedLeft(E, σ), (0, e), (e, 0))
proof
  apply expandedLeft.membership.backward
  refine ⟨(product.pair with (spokes.edge with edge),
      (halfEdges.left with edge)), e, edge, _⟩
  left
  rfl

theorem expandedRight.spoke_relates (E σ e : Set)
  requires edge : e ∈ E
  shows relates(expandedRight(E, σ), (0, e), (e, 1))
proof
  apply expandedRight.membership.backward
  refine ⟨(product.pair with (spokes.edge with edge),
      (halfEdges.right with edge)), e, edge, _⟩
  left
  rfl

theorem expandedLeft.ring_relates (E σ h : Set)
  requires end : h ∈ halfEdges(E)
  shows relates(expandedLeft(E, σ), (1, h), h)
proof
  obtain ⟨e, he, _, _, _⟩ := halfEdges.shape with end
  apply expandedLeft.membership.backward
  refine ⟨(product.pair with (rings.edge with end), end), e, he, _⟩
  right
  exact ⟨h, end, rfl⟩

theorem expandedRight.ring_relates (E σ h : Set)
  requires function : σ : halfEdges(E) → halfEdges(E)
  requires end : h ∈ halfEdges(E)
  shows relates(expandedRight(E, σ), (1, h), σ(h))
proof
  obtain ⟨e, he, _, _, _⟩ := halfEdges.shape with end
  have image := FunctionBetween.apply_closed with function, end
  apply expandedRight.membership.backward
  refine ⟨(product.pair with (rings.edge with end), image), e, he, _⟩
  right
  exact ⟨h, end, rfl⟩

theorem expandedLeft.function (E σ : Set)
  shows expandedLeft(E, σ) : expandedEdges(E) → halfEdges(E)
proof
  constructor
  . intros p member
    exact member.left
  constructor
  . intros x y relatedY z relatedZ
    have shapeY := expandedLeft.of_relates with relatedY
    have shapeZ := expandedLeft.of_relates with relatedZ
    rcases shapeY with ⟨e, he, rfl, rfl⟩ | ⟨h, hh, rfl, rfl⟩
    . rcases shapeZ with ⟨f, hf, same, rfl⟩ | ⟨k, hk, same, rfl⟩
      . obtain ⟨_, rfl⟩ := orderedPair.injective with same
        rfl
      . obtain ⟨zeroOne, _⟩ := orderedPair.injective with same
        contradiction
    . rcases shapeZ with ⟨f, hf, same, rfl⟩ | ⟨k, hk, same, rfl⟩
      . obtain ⟨oneZero, _⟩ := orderedPair.injective with same
        contradiction
      . obtain ⟨_, rfl⟩ := orderedPair.injective with same
        rfl
  . intros x member
    have split := expandedEdges.cases with member
    rcases split with ⟨e, he, rfl⟩ | ⟨h, hh, rfl⟩
    . exact ⟨(e, 0), (halfEdges.left with he),
        (expandedLeft.spoke_relates with he)⟩
    . exact ⟨h, hh, (expandedLeft.ring_relates with hh)⟩

theorem expandedRight.function (E σ : Set)
  requires function : σ : halfEdges(E) → halfEdges(E)
  shows expandedRight(E, σ) : expandedEdges(E) → halfEdges(E)
proof
  constructor
  . intros p member
    exact member.left
  constructor
  . intros x y relatedY z relatedZ
    have shapeY := expandedRight.of_relates with relatedY
    have shapeZ := expandedRight.of_relates with relatedZ
    rcases shapeY with ⟨e, he, rfl, rfl⟩ | ⟨h, hh, rfl, rfl⟩
    . rcases shapeZ with ⟨f, hf, same, rfl⟩ | ⟨k, hk, same, rfl⟩
      . obtain ⟨_, rfl⟩ := orderedPair.injective with same
        rfl
      . obtain ⟨zeroOne, _⟩ := orderedPair.injective with same
        contradiction
    . rcases shapeZ with ⟨f, hf, same, rfl⟩ | ⟨k, hk, same, rfl⟩
      . obtain ⟨oneZero, _⟩ := orderedPair.injective with same
        contradiction
      . obtain ⟨_, rfl⟩ := orderedPair.injective with same
        rfl
  . intros x member
    have split := expandedEdges.cases with member
    rcases split with ⟨e, he, rfl⟩ | ⟨h, hh, rfl⟩
    . exact ⟨(e, 1), (halfEdges.right with he),
        (expandedRight.spoke_relates with he)⟩
    . exact ⟨σ(h), (FunctionBetween.apply_closed with function, hh),
        (expandedRight.ring_relates with function, hh)⟩

theorem expansion.graph (V E leftEnd rightEnd σ : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)
  shows Graph(halfEdges(E), expandedEdges(E),
    expandedLeft(E, σ), expandedRight(E, σ))
proof
  have function := RotationSystem.function with rotation
  exact ⟨expandedLeft.function, (expandedRight.function with function)⟩

-- The values of the end maps.
theorem expandedLeft.spoke (E σ e : Set)
  requires edge : e ∈ E
  shows expandedLeft(E, σ)((0, e)) = (e, 0)
proof
  exact FunctionBetween.apply_value with expandedLeft.function,
    (spokes.edge with edge), (expandedLeft.spoke_relates with edge)

theorem expandedRight.spoke (E σ e : Set)
  requires function : σ : halfEdges(E) → halfEdges(E)
  requires edge : e ∈ E
  shows expandedRight(E, σ)((0, e)) = (e, 1)
proof
  exact FunctionBetween.apply_value with (expandedRight.function with function),
    (spokes.edge with edge), (expandedRight.spoke_relates with edge)

theorem expandedLeft.ring (E σ h : Set)
  requires end : h ∈ halfEdges(E)
  shows expandedLeft(E, σ)((1, h)) = h
proof
  exact FunctionBetween.apply_value with expandedLeft.function,
    (rings.edge with end), (expandedLeft.ring_relates with end)

theorem expandedRight.ring (E σ h : Set)
  requires function : σ : halfEdges(E) → halfEdges(E)
  requires end : h ∈ halfEdges(E)
  shows expandedRight(E, σ)((1, h)) = σ(h)
proof
  exact FunctionBetween.apply_value with (expandedRight.function with function),
    (rings.edge with end), (expandedRight.ring_relates with function, end)

-- Section: The ends of the expansion.

-- The spoke end at h = (e, i) is side i of the spoke of e.
theorem spokes.ends (E σ e i : Set)
  requires function : σ : halfEdges(E) → halfEdges(E)
  requires edge : e ∈ E
  requires side : i ∈ 2
  shows incidentEnds(expandedLeft(E, σ), expandedRight(E, σ), spokes(E),
    (e, i)) = {((0, e), i)}
proof
  ext p
  constructor
  . intro hp
    obtain ⟨x, hx, j, hj, rfl⟩ := incidentEnds.shape with hp
    have ending := (incidentEnds.pair.forward with hp).right
    unfold spokes at hx
    obtain ⟨_, z, hz, f, hf, rfl⟩ := product.membership.forward with hx
    simp at hz
    rw hz at ending
    rw hz
    rw [(expandedLeft.spoke with hf), (expandedRight.spoke with function, hf)]
      at ending
    rcases ending with ⟨rfl, same⟩ | ⟨rfl, same⟩
    . obtain ⟨rfl, rfl⟩ := orderedPair.injective with same
      simp
    . obtain ⟨rfl, rfl⟩ := orderedPair.injective with same
      simp
  . intro hp
    simp at hp
    rw hp
    have spoke := spokes.member with edge
    have sides := membership.two.forward with side
    rcases sides with rfl | rfl
    . simp [incidentEnds.pair, spoke,
        (expandedLeft.spoke at E, σ, e with edge)]
    . simp [incidentEnds.pair, spoke, (expandedRight.spoke with function, edge)]

-- The ring ends at h = (e, i): the left end of its own ring edge and the
-- right end of the ring edge of the end σ carries to h.
theorem rings.ends (E σ e i : Set)
  requires bijective : BijectiveBetween(σ, halfEdges(E), halfEdges(E))
  requires edge : e ∈ E
  requires side : i ∈ 2
  shows incidentEnds(expandedLeft(E, σ), expandedRight(E, σ), rings(E),
      (e, i)) =
    {((1, (e, i)), 0),
      ((1, converse(σ, halfEdges(E), halfEdges(E))((e, i))), 1)}
proof
  have function := Injective.function with (Bijective.injective with bijective)
  have end : (e, i) ∈ halfEdges(E) :=
    halfEdges.pair.backward with ⟨edge, side⟩
  have inverse := converse.function_of_bijective with bijective
  have preimage := FunctionBetween.apply_closed with inverse, end
  have back := Bijective.apply_inverse with bijective, end
  ext p
  constructor
  . intro hp
    obtain ⟨x, hx, j, hj, rfl⟩ := incidentEnds.shape with hp
    have ending := (incidentEnds.pair.forward with hp).right
    unfold rings at hx
    obtain ⟨_, z, hz, k, hk, rfl⟩ := product.membership.forward with hx
    simp at hz
    rw hz at ending
    rw hz
    rw [(expandedLeft.ring with hk), (expandedRight.ring with function, hk)]
      at ending
    rcases ending with ⟨rfl, rfl⟩ | ⟨rfl, same⟩
    . simp
    . have forward := Bijective.inverse_apply with bijective, hk
      rw same at forward
      rw ← forward
      simp
  . intro hp
    simp at hp
    rcases hp with rfl | rfl
    . simp [incidentEnds.pair, (rings.member with end),
        (expandedLeft.ring at E, σ, (e, i) with end)]
    . simp [incidentEnds.pair, (rings.member with preimage),
        (expandedRight.ring with function, preimage), back]

-- Each end meets one spoke and two ring edges.
theorem spokes.degree (E σ e i : Set)
  requires function : σ : halfEdges(E) → halfEdges(E)
  requires edge : e ∈ E
  requires side : i ∈ 2
  shows degreeIn(expandedLeft(E, σ), expandedRight(E, σ), spokes(E),
    (e, i)) = 1
proof
  unfold degreeIn
  rw spokes.ends with function, edge, side
  exact cardinality.singleton

theorem rings.degree (E σ e i : Set)
  requires bijective : BijectiveBetween(σ, halfEdges(E), halfEdges(E))
  requires edge : e ∈ E
  requires side : i ∈ 2
  shows degreeIn(expandedLeft(E, σ), expandedRight(E, σ), rings(E),
    (e, i)) = 2
proof
  have fresh : ((1, converse(σ, halfEdges(E), halfEdges(E))((e, i))), 1) ∉
      {((1, (e, i)), 0)}
    intro same
    simp at same
  unfold degreeIn
  rw [(rings.ends with bijective, edge, side), pair.eq_union2,
    (cardinality.union_disjoint with Finite.singleton, Finite.singleton,
      (Disjoint.singleton_of_fresh with fresh)),
    cardinality.singleton, cardinality.singleton]
  compute

-- The ring edges form an even edge set of the expansion.
theorem rings.even (E σ : Set)
  requires finiteEdges : Finite(E)
  requires bijective : BijectiveBetween(σ, halfEdges(E), halfEdges(E))
  shows EvenEdgeSet(halfEdges(E), expandedLeft(E, σ), expandedRight(E, σ),
    rings(E))
proof
  constructor
  . exact rings.finite with finiteEdges
  . intros h hh
    obtain ⟨e, he, i, hi, rfl⟩ := halfEdges.shape with hh
    rw rings.degree with bijective, he, hi
    exact Even.two

-- With every degree at least two the expansion is cubic and loopless: each
-- end meets its spoke and two ring edges, a spoke joins the two distinct
-- ends of its edge, and a ring edge joins an end to a different end.
theorem expansion.cubic (V E leftEnd rightEnd σ : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteEdges : Finite(E)
  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)
  requires degrees : ∀ v ∈ V, 2 ≤ degreeIn(leftEnd, rightEnd, E, v)
  shows Cubic(halfEdges(E), expandedEdges(E),
    expandedLeft(E, σ), expandedRight(E, σ))
proof
  have function := RotationSystem.function with rotation
  constructor
  . intros h hh
    obtain ⟨e, he, i, hi, rfl⟩ := halfEdges.shape with hh
    unfold expandedEdges
    rw [(degreeIn.union_disjoint with (spokes.finite with finiteEdges),
        (rings.finite with finiteEdges), expandedEdges.apart),
      (spokes.degree with function, he, hi),
      (rings.degree with rotation.left, he, hi)]
    compute
  . intros x hx
    have split := expandedEdges.cases with hx
    rcases split with ⟨e, he, rfl⟩ | ⟨h, hh, rfl⟩
    . rw [(expandedLeft.spoke with he), (expandedRight.spoke with function, he)]
      intro same
      have sides := (orderedPair.injective with same).right
      contradiction
    . rw [(expandedLeft.ring with hh), (expandedRight.ring with function, hh)]
      have moves := RotationSystem.moves
        with graph, finiteEdges, rotation, degrees, hh
      cc