-- The multigraph with every edge doubled: the edges are the pairs (e, i)
-- with i ∈ 2 and the ends of e, cuts double in size, and an edge set of the
-- doubled graph projects back to the edges with a copy in it.
-- 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.Multigraph.Doubling
import Multigraph.Trees
import Combinatorics.Basics

-- Section: The graph with every edge doubled.

-- Every edge doubled: the edges are the pairs (e, i) with i ∈ 2, with the
-- ends of e.
def doubledEdges (E : Set) : Set := E × 2
def doubledEnd (V E endpoint : Set) : Set :=
  { p ∈ (E × 2) × V | ∃ e ∈ E, ∃ i ∈ 2, p = ((e, i), endpoint(e)) }

-- The doubled end of (e, i) is the end of e.
theorem doubledEnd.function (V E endpoint : Set)
  requires function : endpoint : E → V
  shows doubledEnd(V, E, endpoint) : E × 2 → V
proof
  constructor
  . intros p member
    exact member.left
  constructor
  . intros x y relatedY z relatedZ
    obtain ⟨_, e, _, i, _, shapeY⟩ := relatedY
    obtain ⟨_, f, _, j, _, shapeZ⟩ := relatedZ
    obtain ⟨xY, valueY⟩ := orderedPair.injective with shapeY
    obtain ⟨xZ, valueZ⟩ := orderedPair.injective with shapeZ
    have pairs : (e, i) = (f, j) by cc
    obtain ⟨same, _⟩ := orderedPair.injective with pairs
    cc
  . intros x input
    obtain ⟨_, e, he, i, hi, rfl⟩ := product.membership.forward with input
    have vertex := FunctionBetween.apply_closed with function, he
    witness endpoint(e)
    refine ⟨vertex, _⟩
    exact doubledEnd.membership.backward
      with ⟨(product.pair with input, vertex), e, he, i, hi, rfl⟩

theorem doubledEnd.value (V E endpoint e i : Set)
  requires function : endpoint : E → V
  requires edge : e ∈ E
  requires side : i ∈ 2
  shows doubledEnd(V, E, endpoint)((e, i)) = endpoint(e)
proof
  have input : (e, i) ∈ E × 2 := product.pair with edge, side
  have vertex := FunctionBetween.apply_closed with function, edge
  have related : relates(doubledEnd(V, E, endpoint), (e, i), endpoint(e)) :=
    doubledEnd.membership.backward
      with ⟨(product.pair with input, vertex), e, edge, i, side, rfl⟩
  exact FunctionBetween.apply_value
    with (doubledEnd.function with function), input, related

theorem doubled.graph (V E leftEnd rightEnd : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  shows Graph(V, doubledEdges(E), doubledEnd(V, E, leftEnd),
    doubledEnd(V, E, rightEnd))
proof
  unfold doubledEdges
  exact ⟨(doubledEnd.function with graph.left),
    (doubledEnd.function with graph.right)⟩

-- The edges of the doubled graph leaving X are the two copies of each edge
-- of G leaving X.
theorem doubled.crossing (V E leftEnd rightEnd X : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  shows crossing(doubledEnd(V, E, leftEnd), doubledEnd(V, E, rightEnd),
    doubledEdges(E), X) = crossing(leftEnd, rightEnd, E, X) × 2
proof
  unfold doubledEdges
  ext p
  constructor
  . intro hp
    obtain ⟨inProduct, sides⟩ := hp
    obtain ⟨_, e, he, i, hi, rfl⟩ :=
      product.membership.forward with inProduct
    rw [(doubledEnd.value with graph.left, he, hi),
      (doubledEnd.value with graph.right, he, hi)] at sides
    exact product.pair with ⟨he, sides⟩, hi
  . intro hp
    obtain ⟨_, e, he, i, hi, rfl⟩ := product.membership.forward with hp
    obtain ⟨inE, sides⟩ := he
    refine ⟨(product.pair with inE, hi), _⟩
    rw [(doubledEnd.value with graph.left, inE, hi),
      (doubledEnd.value with graph.right, inE, hi)]
    exact sides

theorem doubled.edge_connected (V E leftEnd rightEnd : Set, k : Nat)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteEdges : Finite(E)
  requires connected : EdgeConnected(V, E, leftEnd, rightEnd, k)
  shows EdgeConnected(V, doubledEdges(E), doubledEnd(V, E, leftEnd),
    doubledEnd(V, E, rightEnd), 2 * k)
proof
  intros X bound nonempty proper
  have many := connected with X, bound, nonempty, proper
  have finiteCut := crossing.finite at leftEnd, rightEnd, E, X
    with finiteEdges
  rw [(doubled.crossing with graph),
    (cardinality.product_count with finiteCut, (Finite.natural at 2)),
    (cardinality.natural at 2)]
  arith

-- Section: Projecting doubled edge sets back to G.

-- The edges of G with a copy in a set S of doubled edges: the image of S
-- under the projection to the edge, so no larger than S.
def projected (E S : Set) : Set := { e ∈ E | ∃ i ∈ 2, (e, i) ∈ S }

defgraph copyEdge (E : Set) (p ∈ E × 2) : E := fst(p)
proof
  obtain ⟨_, e, he, i, hi, rfl⟩ := product.membership.forward with member
  rw fst.pair
  exact he

theorem projected.count (E S : Set)
  requires finiteEdges : Finite(E)
  requires subset : S ⊆ E × 2
  shows cardinality(projected(E, S)) ≤ cardinality(S)
proof
  have function := copyEdge.function at E
  have finiteS := Finite.subset
    with (Finite.product with finiteEdges, Finite.natural), subset
  have same : projected(E, S) = functionImage(copyEdge(E), S, E)
    ext e
    constructor
    . intro he
      obtain ⟨inE, i, hi, inS⟩ := he
      refine ⟨inE, (e, i), inS, _⟩
      rw [(copyEdge.value with (subset with (e, i), inS)), fst.pair]
    . intro he
      obtain ⟨inE, p, hp, shape⟩ := he
      obtain ⟨_, f, hf, i, hi, rfl⟩ :=
        product.membership.forward with (subset with p, hp)
      rw [(copyEdge.value with (subset with (f, i), hp)), fst.pair] at shape
      rw shape
      exact ⟨hf, i, hi, hp⟩
  rw same
  exact cardinality.image_le with function, subset, finiteS

-- The projections of a family of doubled edge sets, as a function on 3.
defgraph projectedTrees (E T : Set) (i ∈ 3) : 𝒫(E) := projected(E, T(i))
proof
  apply powerset.membership_iff.backward
  intros e he
  exact he.left