-- The side of a vertex set as a multigraph of its own: the edges inside a
-- vertex set, the end functions restricted to them, and the ends, degrees,
-- and cuts read through the restriction; a side crossed by no edge of a
-- bridgeless graph is bridgeless.
-- 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.Subgraph
import Connectivity

-- The edges of F inside X are edges of F, grow with F, and have both ends
-- in X.
theorem inside.subset (leftEnd rightEnd F X : Set)
  shows inside(leftEnd, rightEnd, F, X) ⊆ F
proof
  intros e edge
  exact edge.left

theorem inside.monotone (leftEnd rightEnd F G X : Set)
  requires subset : F ⊆ G
  shows inside(leftEnd, rightEnd, F, X) ⊆ inside(leftEnd, rightEnd, G, X)
proof
  intros e edge
  exact ⟨(subset with e, edge.left), edge.right⟩

theorem inside.ends (leftEnd rightEnd F X : Set)
  shows ∀ e ∈ inside(leftEnd, rightEnd, F, X),
    leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X
proof
  intros e edge
  exact edge.right

-- Two sets of ends agree when they agree on every pair (f, i).
theorem incidentEnds.ext (leftEnd rightEnd otherLeft otherRight F G v w : Set)
  requires agree : ∀ f, ∀ i,
    ((f, i) ∈ incidentEnds(leftEnd, rightEnd, F, v) ↔
      (f, i) ∈ incidentEnds(otherLeft, otherRight, G, w))
  shows incidentEnds(leftEnd, rightEnd, F, v) =
    incidentEnds(otherLeft, otherRight, G, w)
proof
  ext p
  constructor
  . intro hp
    obtain ⟨f, _, i, _, rfl⟩ := incidentEnds.shape with hp
    have rule := agree with f, i
    exact rule.forward with hp
  . intro hp
    obtain ⟨f, _, i, _, rfl⟩ := incidentEnds.shape with hp
    have rule := agree with f, i
    exact rule.backward with hp

-- On the edges of D the restricted ends are the ends, so the ends at a
-- vertex, the degrees, and the cuts of an edge set inside D are the same
-- for both.
theorem incidentEnds.restricted (W E D F leftEnd rightEnd v : Set)
  requires graph : Graph(W, E, leftEnd, rightEnd)
  requires edges : D ⊆ E
  requires subset : F ⊆ D
  shows incidentEnds(restrict(leftEnd, D), restrict(rightEnd, D), F, v) =
    incidentEnds(leftEnd, rightEnd, F, v)
proof
  apply incidentEnds.ext
  intros f i
  by_cases inF : f ∈ F
  . have inD := subset with f, inF
    have leftValue := restrict.domain_apply with graph.left, edges, inD
    have rightValue := restrict.domain_apply with graph.right, edges, inD
    simp [incidentEnds.pair, leftValue, rightValue]
  . simp [incidentEnds.pair, inF]

theorem degreeIn.restricted (W E D F leftEnd rightEnd v : Set)
  requires graph : Graph(W, E, leftEnd, rightEnd)
  requires edges : D ⊆ E
  requires subset : F ⊆ D
  shows degreeIn(restrict(leftEnd, D), restrict(rightEnd, D), F, v) =
    degreeIn(leftEnd, rightEnd, F, v)
proof
  unfold degreeIn
  rw incidentEnds.restricted with graph, edges, subset

theorem crossing.restricted (W E D X leftEnd rightEnd : Set)
  requires graph : Graph(W, E, leftEnd, rightEnd)
  requires edges : D ⊆ E
  shows crossing(restrict(leftEnd, D), restrict(rightEnd, D), D, X) =
    crossing(leftEnd, rightEnd, D, X)
proof
  ext e
  by_cases inD : e ∈ D
  . have leftValue := restrict.domain_apply with graph.left, edges, inD
    have rightValue := restrict.domain_apply with graph.right, edges, inD
    simp [crossing, leftValue, rightValue]
  . simp [crossing, inD]

-- A side of a split is a graph on its own vertices once the end functions
-- are restricted to its inside edges, and it stays bridgeless when no edge
-- crosses the split.
theorem inside.graph (V E leftEnd rightEnd X : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires subset : X ⊆ V
  shows Graph(X, inside(leftEnd, rightEnd, E, X),
    restrict(leftEnd, inside(leftEnd, rightEnd, E, X)),
    restrict(rightEnd, inside(leftEnd, rightEnd, E, X)))
proof
  have edges := inside.subset at leftEnd, rightEnd, E, X
  have ends := inside.ends at leftEnd, rightEnd, E, X
  have leftIn : ∀ e ∈ inside(leftEnd, rightEnd, E, X), leftEnd(e) ∈ X
    intros e he
    exact (ends with e, he).left
  have rightIn : ∀ e ∈ inside(leftEnd, rightEnd, E, X), rightEnd(e) ∈ X
    intros e he
    exact (ends with e, he).right
  exact ⟨(restrict.function with graph.left, edges, leftIn),
    (restrict.function with graph.right, edges, rightIn)⟩

theorem inside.bridgeless (V E leftEnd rightEnd X : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires split : X ⊆ V ∧ crossing(leftEnd, rightEnd, E, X) = ∅
  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)
  shows Bridgeless(X, inside(leftEnd, rightEnd, E, X),
    restrict(leftEnd, inside(leftEnd, rightEnd, E, X)),
    restrict(rightEnd, inside(leftEnd, rightEnd, E, X)))
proof
  intros Y bound
  obtain ⟨subset, none⟩ := split
  have edges := inside.subset at leftEnd, rightEnd, E, X
  -- An edge leaving Y ⊆ X has its other end in X, as no edge leaves X, so
  -- the cut of Y within the side is its cut in the whole graph.
  have within : crossing(leftEnd, rightEnd, E, Y) ⊆
      inside(leftEnd, rightEnd, E, X)
    intros e he
    obtain ⟨inE, sides⟩ := he
    have notCross : ¬e ∈ crossing(leftEnd, rightEnd, E, X)
      rw none
      simp
    have both : leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X
      by_contra outside
      apply notCross
      refine ⟨inE, _⟩
      rcases sides with ⟨leftY, rightY⟩ | ⟨rightY, leftY⟩
      . left
        have leftX := bound with leftEnd(e), leftY
        refine ⟨leftX, _⟩
        intro rightX
        exact outside with ⟨leftX, rightX⟩
      . right
        have rightX := bound with rightEnd(e), rightY
        refine ⟨rightX, _⟩
        intro leftX
        exact outside with ⟨leftX, rightX⟩
    exact ⟨inE, both⟩
  have same : crossing(restrict(leftEnd, inside(leftEnd, rightEnd, E, X)),
      restrict(rightEnd, inside(leftEnd, rightEnd, E, X)),
      inside(leftEnd, rightEnd, E, X), Y) = crossing(leftEnd, rightEnd, E, Y)
    rw [(crossing.restricted with graph, edges), (crossing.restrict with edges)]
    exact intersection.eq_left_of_subset with within
  rw same
  exact bridgeless with Y, (Subset.transitive with bound, subset)