-- Degrees of vertices in an edge set of a multigraph: the ends of edges at a
-- vertex, counted with a loop contributing both of its ends.
-- 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.Degree
import Cardinal.Parity
import Multigraph
import Cardinal.NaturalSumLaws

-- The ends of the edges of F at v: (e, 0) for the left end of e, (e, 1) for
-- the right end.
def incidentEnds (leftEnd rightEnd F v : Set) : Set :=
  { p ∈ F × 2 | (snd(p) = 0 ∧ leftEnd(fst(p)) = v) ∨
    (snd(p) = 1 ∧ rightEnd(fst(p)) = v) }

-- The degree of v in F: the number of ends of edges of F at v.
def degreeIn (leftEnd rightEnd F v : Set) : Set :=
  cardinality(incidentEnds(leftEnd, rightEnd, F, v))

-- (e, i) is an end at v exactly when e ∈ F and side i of e is v.
theorem incidentEnds.pair (leftEnd rightEnd F v e i : Set)
  shows (e, i) ∈ incidentEnds(leftEnd, rightEnd, F, v) ↔
    e ∈ F ∧ ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))
proof
  unfold incidentEnds
  simp [fst.pair, snd.pair, product.pair_membership, membership.two]

theorem incidentEnds.shape (leftEnd rightEnd F v p : Set)
  requires member : p ∈ incidentEnds(leftEnd, rightEnd, F, v)
  shows ∃ e ∈ F, ∃ i ∈ 2, p = (e, i)
proof
  exact (product.membership.forward with member.left).right

theorem incidentEnds.subset_product (leftEnd rightEnd F v : Set)
  shows incidentEnds(leftEnd, rightEnd, F, v) ⊆ F × 2
proof
  intros p hp
  exact hp.left

theorem incidentEnds.finite (leftEnd rightEnd F v : Set)
  requires finite : Finite(F)
  shows Finite(incidentEnds(leftEnd, rightEnd, F, v))
proof
  have product : Finite(F × 2) :=
    Finite.product with finite, Finite.natural
  exact Finite.subset with product, incidentEnds.subset_product

theorem degreeIn.natural (leftEnd rightEnd F v : Set)
  requires finite : Finite(F)
  shows Nat(degreeIn(leftEnd, rightEnd, F, v))
proof
  unfold degreeIn
  exact cardinality.nat with (incidentEnds.finite with finite)

theorem degreeIn.empty (leftEnd rightEnd v : Set)
  shows degreeIn(leftEnd, rightEnd, ∅, v) = 0
proof
  have none : incidentEnds(leftEnd, rightEnd, ∅, v) = ∅
    ext p
    simp [incidentEnds, product.left_empty]
  unfold degreeIn
  rw none
  exact cardinality.empty

-- The ends of a single edge e at v: e paired with each side whose end is v.
theorem incidentEnds.singleton (leftEnd rightEnd e v S : Set)
  requires sides : ∀ i, i ∈ S ↔
    ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))
  shows incidentEnds(leftEnd, rightEnd, {e}, v) = {e} × S
proof
  ext p
  constructor
  . intro hp
    obtain ⟨x, hx, i, hi, rfl⟩ := incidentEnds.shape with hp
    simp [incidentEnds.pair] at hp
    simp [product.pair_membership, sides]
  . intro hp
    obtain ⟨_, x, hx, i, hi, rfl⟩ := product.membership.forward with hp
    simp [sides] at hx, hi
    simp [incidentEnds.pair]

theorem degreeIn.singleton (leftEnd rightEnd e v S : Set)
  requires finite : Finite(S)
  requires sides : ∀ i, i ∈ S ↔
    ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))
  shows degreeIn(leftEnd, rightEnd, {e}, v) = cardinality(S)
proof
  unfold degreeIn
  rw incidentEnds.singleton with sides
  exact cardinality.singleton_product with finite

-- A loop contributes two ends at its vertex.
theorem degreeIn.loop (leftEnd rightEnd e v : Set)
  requires left : leftEnd(e) = v
  requires right : rightEnd(e) = v
  shows degreeIn(leftEnd, rightEnd, {e}, v) = 2
proof
  have sides : ∀ i, i ∈ 2 ↔
      ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))
    intro i
    simp [membership.two, left, right]
  rw degreeIn.singleton with Finite.natural, sides
  exact cardinality.natural

-- An edge that is not a loop contributes one end at each of its ends.
theorem degreeIn.end (leftEnd rightEnd e v : Set)
  requires distinct : leftEnd(e) ≠ rightEnd(e)
  requires end : leftEnd(e) = v ∨ rightEnd(e) = v
  shows degreeIn(leftEnd, rightEnd, {e}, v) = 1
proof
  cases end with atLeft | atRight
  . have notRight : rightEnd(e) ≠ v by cc
    have sides : ∀ i, i ∈ {0} ↔
        ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))
      intro i
      simp [singleton.membership, atLeft, notRight]
    rw degreeIn.singleton with Finite.singleton, sides
    exact cardinality.singleton
  . have notLeft : leftEnd(e) ≠ v by cc
    have sides : ∀ i, i ∈ {1} ↔
        ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))
      intro i
      simp [singleton.membership, atRight, notLeft]
    rw degreeIn.singleton with Finite.singleton, sides
    exact cardinality.singleton

-- The two halves of degreeIn.end, by which end of e is v.
theorem degreeIn.end_left (leftEnd rightEnd e v : Set)
  requires distinct : leftEnd(e) ≠ rightEnd(e)
  requires atLeft : leftEnd(e) = v
  shows degreeIn(leftEnd, rightEnd, {e}, v) = 1
proof
  have atEnd : leftEnd(e) = v ∨ rightEnd(e) = v by left; exact atLeft
  exact degreeIn.end with distinct, atEnd

theorem degreeIn.end_right (leftEnd rightEnd e v : Set)
  requires distinct : leftEnd(e) ≠ rightEnd(e)
  requires atRight : rightEnd(e) = v
  shows degreeIn(leftEnd, rightEnd, {e}, v) = 1
proof
  have atEnd : leftEnd(e) = v ∨ rightEnd(e) = v by right; exact atRight
  exact degreeIn.end with distinct, atEnd

-- An edge with neither end at v contributes nothing there.
theorem degreeIn.absent (leftEnd rightEnd e v : Set)
  requires left : leftEnd(e) ≠ v
  requires right : rightEnd(e) ≠ v
  shows degreeIn(leftEnd, rightEnd, {e}, v) = 0
proof
  have sides : ∀ i, i ∈ ∅ ↔
      ((i = 0 ∧ leftEnd(e) = v) ∨ (i = 1 ∧ rightEnd(e) = v))
    intro i
    simp [left, right]
  rw degreeIn.singleton with Finite.empty, sides
  exact cardinality.empty

theorem incidentEnds.monotone (leftEnd rightEnd F G v : Set)
  requires subset : F ⊆ G
  shows incidentEnds(leftEnd, rightEnd, F, v) ⊆
    incidentEnds(leftEnd, rightEnd, G, v)
proof
  intros p hp
  obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with hp
  exact incidentEnds.pair.backward
    with ⟨(subset with e, he), (incidentEnds.pair.forward with hp).right⟩

-- Taking ends is pointwise in the edge set, so it commutes with ∪ and △ and
-- preserves disjointness.
theorem incidentEnds.union (leftEnd rightEnd F G v : Set)
  shows incidentEnds(leftEnd, rightEnd, F ∪ G, v) =
    incidentEnds(leftEnd, rightEnd, F, v) ∪
    incidentEnds(leftEnd, rightEnd, G, v)
proof
  ext p
  simp [incidentEnds.membership, product.union2_left]

theorem incidentEnds.disjoint (leftEnd rightEnd F G v : Set)
  requires apart : Disjoint(F, G)
  shows Disjoint(incidentEnds(leftEnd, rightEnd, F, v),
    incidentEnds(leftEnd, rightEnd, G, v))
proof
  have products : Disjoint(F × 2, G × 2) :=
    product.disjoint_of_left with apart
  have left : Disjoint(F × 2, incidentEnds(leftEnd, rightEnd, G, v)) :=
    Disjoint.of_subset_right with products, incidentEnds.subset_product
  exact Disjoint.of_subset_left with left, incidentEnds.subset_product

theorem incidentEnds.symmetricDifference (leftEnd rightEnd F G v : Set)
  shows incidentEnds(leftEnd, rightEnd, F △ G, v) =
    incidentEnds(leftEnd, rightEnd, F, v) △
    incidentEnds(leftEnd, rightEnd, G, v)
proof
  ext p
  simp [incidentEnds.membership, product.symmetricDifference_left,
    symmetricDifference.membership]

theorem degreeIn.union_disjoint (leftEnd rightEnd F G v : Set)
  requires first : Finite(F)
  requires second : Finite(G)
  requires apart : Disjoint(F, G)
  shows degreeIn(leftEnd, rightEnd, F ∪ G, v) =
    degreeIn(leftEnd, rightEnd, F, v) + degreeIn(leftEnd, rightEnd, G, v)
proof
  unfold degreeIn
  rw incidentEnds.union
  exact cardinality.union_disjoint with (incidentEnds.finite with first),
    (incidentEnds.finite with second), (incidentEnds.disjoint with apart)

-- Removing an edge a from F takes the degree in {a} off every degree.
theorem degreeIn.remove (leftEnd rightEnd F a v : Set)
  requires finite : Finite(F)
  requires member : a ∈ F
  shows degreeIn(leftEnd, rightEnd, F, v) =
    degreeIn(leftEnd, rightEnd, F ∖ {a}, v) +
    degreeIn(leftEnd, rightEnd, {a}, v)
proof
  have restored : (F ∖ {a}) ∪ {a} = F
    ext y
    simp
  have sum := degreeIn.union_disjoint at leftEnd, rightEnd, F ∖ {a}, {a}, v
    with (Finite.difference with finite), Finite.singleton,
      Disjoint.difference_left
  rwa restored at sum

theorem degreeIn.monotone (leftEnd rightEnd F G v : Set)
  requires finite : Finite(G)
  requires subset : F ⊆ G
  shows degreeIn(leftEnd, rightEnd, F, v) ≤ degreeIn(leftEnd, rightEnd, G, v)
proof
  unfold degreeIn
  exact cardinality.monotone with (incidentEnds.finite with finite),
    (incidentEnds.monotone with subset)

-- Degrees add modulo two under symmetric difference.
theorem degreeIn.symmetricDifference_parity (leftEnd rightEnd F G v : Set)
  requires first : Finite(F)
  requires second : Finite(G)
  shows Even(degreeIn(leftEnd, rightEnd, F △ G, v)) ↔
    (Even(degreeIn(leftEnd, rightEnd, F, v)) ↔
      Even(degreeIn(leftEnd, rightEnd, G, v)))
proof
  unfold degreeIn
  rw incidentEnds.symmetricDifference
  exact EvenSet.symmetricDifference with (incidentEnds.finite with first),
    (incidentEnds.finite with second)

-- The degree function of F on V, as the weight of a natural sum.
def degreeWeights (V leftEnd rightEnd F : Set) : Set :=
  { p ∈ V × ℕ | ∃ v ∈ V, p = (v, degreeIn(leftEnd, rightEnd, F, v)) }

theorem degreeWeights.function (V leftEnd rightEnd F : Set)
  requires finite : Finite(F)
  shows degreeWeights(V, leftEnd, rightEnd, F) : V → ℕ
proof
  constructor
  . intros p member
    exact member.left
  . constructor
    . intros x y xy z xz
      obtain ⟨_, a, _, shapeY⟩ := xy
      obtain ⟨_, b, _, shapeZ⟩ := xz
      obtain ⟨sameA, valueY⟩ := orderedPair.injective with shapeY
      obtain ⟨sameB, valueZ⟩ := orderedPair.injective with shapeZ
      cc
    . intros x input
      have weight : degreeIn(leftEnd, rightEnd, F, x) ∈ ℕ :=
        degreeIn.natural with finite
      refine ⟨degreeIn(leftEnd, rightEnd, F, x), weight, _⟩
      exact degreeWeights.membership.backward
        with ⟨(product.pair with input, weight), x, input, rfl⟩

theorem degreeWeights.value (V leftEnd rightEnd F v : Set)
  requires finite : Finite(F)
  requires member : v ∈ V
  shows degreeWeights(V, leftEnd, rightEnd, F)(v) =
    degreeIn(leftEnd, rightEnd, F, v)
proof
  have weight : degreeIn(leftEnd, rightEnd, F, v) ∈ ℕ :=
    degreeIn.natural with finite
  have related : relates(degreeWeights(V, leftEnd, rightEnd, F), v,
      degreeIn(leftEnd, rightEnd, F, v)) :=
    degreeWeights.membership.backward
      with ⟨(product.pair with member, weight), v, member, rfl⟩
  exact FunctionBetween.apply_value
    with (degreeWeights.function with finite), member, related

theorem degreeWeights.natural (V leftEnd rightEnd F : Set)
  requires finite : Finite(F)
  shows ∀ v ∈ V, degreeWeights(V, leftEnd, rightEnd, F)(v) ∈ ℕ
proof
  intros v hv
  rw degreeWeights.value with finite, hv
  exact degreeIn.natural with finite

-- One edge with both ends in V contributes two to the degree sum over V:
-- the sum restricts to the ends of e, where a loop weighs two at one vertex
-- and any other edge one at each of two.
theorem degreeWeights.single_sum (V leftEnd rightEnd e : Set)
  requires finiteVertices : Finite(V)
  requires atLeft : leftEnd(e) ∈ V
  requires atRight : rightEnd(e) ∈ V
  shows natSum(V, degreeWeights(V, leftEnd, rightEnd, {e})) = 2
proof
  have finite : Finite({e}) := Finite.singleton
  have weights := degreeWeights.natural at V, leftEnd, rightEnd, {e} with finite
  have ends : {leftEnd(e), rightEnd(e)} ⊆ V :=
    pair.subset_iff.backward with ⟨atLeft, atRight⟩
  have outside : ∀ v ∈ V ∖ {leftEnd(e), rightEnd(e)},
      degreeWeights(V, leftEnd, rightEnd, {e})(v) = 0
    intros v hv
    have away : leftEnd(e) ≠ v ∧ rightEnd(e) ≠ v by simp
    rw degreeWeights.value with finite, hv.left
    exact degreeIn.absent with away.left, away.right
  rw natSum.restrict with finiteVertices, ends, weights, outside
  by_cases loop : leftEnd(e) = rightEnd(e)
  . rw [loop, pair.self,
      (natSum.singleton with (weights with rightEnd(e), atRight)),
      (degreeWeights.value with finite, atRight)]
    exact degreeIn.loop with loop, rfl
  . rw [(natSum.pair with (weights with leftEnd(e), atLeft),
        (weights with rightEnd(e), atRight), loop),
      (degreeWeights.value with finite, atLeft),
      (degreeWeights.value with finite, atRight),
      (degreeIn.end_left with loop, rfl),
      (degreeIn.end_right with loop, rfl)]
    compute

-- Handshake: the degrees over V sum to twice the number of edges, when every
-- edge has both ends in V. By induction on F: adjoining an edge a adds the
-- degree in {a} at every vertex, hence two to the sum.
theorem degreeIn.handshake (V leftEnd rightEnd F : Set)
  requires finiteVertices : Finite(V)
  requires finite : Finite(F)
  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V
  shows natSum(V, degreeWeights(V, leftEnd, rightEnd, F)) = 2 * cardinality(F)
proof
  induction finite with G a
  | empty =>
    have vanish : ∀ v ∈ V, degreeWeights(V, leftEnd, rightEnd, ∅)(v) = 0
      intros v hv
      rw degreeWeights.value with Finite.empty, hv
      exact degreeIn.empty
    rw [(natSum.zero_weights with vanish), cardinality.empty]
    compute
  | insert using ih =>
    have endsG : ∀ e ∈ G, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V
      intros e he
      exact ends with e, (GSubset with e, he)
    have endsA := ends with a, aMember
    have single := degreeWeights.single_sum
      with finiteVertices, endsA.left, endsA.right
    have unionFinite : Finite(G ∪ {a}) :=
      Finite.union with GFinite, Finite.singleton
    have apart : Disjoint(G, {a}) by simp [Disjoint.iff, aFresh]
    -- The degree at each vertex splits along G ∪ {a}.
    have pointwise : ∀ v ∈ V,
        degreeWeights(V, leftEnd, rightEnd, G ∪ {a})(v) =
        degreeWeights(V, leftEnd, rightEnd, G)(v) +
        degreeWeights(V, leftEnd, rightEnd, {a})(v)
      intros v hv
      rw degreeWeights.value with hv
      exact degreeIn.union_disjoint with GFinite, Finite.singleton, apart
    rw natSum.add_pointwise with finiteVertices,
      (degreeWeights.natural with GFinite),
      (degreeWeights.natural with Finite.singleton), pointwise
    rw [ih, single, (cardinality.union_singleton with GFinite, aFresh)]
    ring