-- The handshake parity lemma for rooms and doors: with every room having
-- at most two doors and every door on one or two rooms, an odd number of
-- boundary doors forces an odd number of rooms with exactly one door
-- 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.Cardinal.Handshake
import DoubleCounting
import SumParity

def cofiber (I R d : Set) : Set := { r ∈ R | (r, d) ∈ I }
def completeRooms (I R D : Set) : Set := { r ∈ R | cardinality(fiber(I, D, r)) = 1 }
def boundaryDoors (I R D : Set) : Set := { d ∈ D | cardinality(cofiber(I, R, d)) = 1 }

-- The converse relation: its fibres are the cofibres, and it has the
-- same size.
theorem converse.subset (I R D : Set)
  shows converse(I, R, D) ⊆ D × R
proof
  intros p hp
  have parts := converse.membership.forward with hp
  exact parts.left

theorem cofiber.converse (I R D d : Set)
  requires hd : d ∈ D
  shows fiber(converse(I, R, D), R, d) = cofiber(I, R, d)
proof
  ext r
  constructor
  . intro hr
    have parts := fiber.membership.forward with hr
    have converseParts := converse.membership.forward with parts.right
    obtain ⟨x, hx, y, hy, shape, related⟩ := converseParts.right
    have coordinates := orderedPair.injective with shape
    rw [coordinates.left, coordinates.right]
    exact cofiber.membership.backward with ⟨hx, related⟩
  . intro hr
    have parts := cofiber.membership.forward with hr
    have related : relates(I, r, d) := parts.right
    have member := converse.relates with parts.left, hd, related
    have inConverse : (d, r) ∈ converse(I, R, D) := member
    exact fiber.membership.backward with ⟨parts.left, inConverse⟩

theorem converse.image (I R D : Set)
  requires inside : I ⊆ R × D
  shows functionImage(productSwap(R, D), I, D × R) = converse(I, R, D)
proof
  have function := Injective.function with (Bijective.injective with (productSwap.bijective at R, D))
  ext q
  constructor
  . intro hq
    simp [functionImage.membership] at hq
    obtain ⟨bound, p, hp, shape⟩ := hq
    obtain ⟨boundP, x, hx, y, hy, pairShape⟩ := product.membership.forward with (inside with p, hp)
    have swapped := productSwap.pair with hx, hy
    rw [pairShape, swapped] at shape
    rw pairShape at hp
    have related : relates(I, x, y) := hp
    have member := converse.relates with hx, hy, related
    rw shape
    exact member
  . intro hq
    have parts := converse.membership.forward with hq
    obtain ⟨x, hx, y, hy, shape, related⟩ := parts.right
    have inside2 : (x, y) ∈ R × D := product.pair with hx, hy
    have swapped := productSwap.pair with hx, hy
    rw [shape, ← swapped]
    have closed := FunctionBetween.apply_closed with function, inside2
    simp [functionImage.membership]
    constructor
    . exact closed
    . witness (x, y)
      constructor
      . exact related
      . rfl

theorem converse.cardinality (I R D : Set)
  requires finiteR : Finite(R)
  requires finiteD : Finite(D)
  requires inside : I ⊆ R × D
  shows cardinality(converse(I, R, D)) = cardinality(I)
proof
  have bijective := productSwap.bijective at R, D
  have injective := Bijective.injective with bijective
  have function := Injective.function with injective
  have finiteI := Finite.subset with (Finite.product with finiteR, finiteD), inside
  have closed : ∀ p ∈ I, productSwap(R, D)(p) ∈ D × R
    intros p hp
    exact FunctionBetween.apply_closed with function, (inside with p, hp)
  have restricted := restrict.function with function, inside, closed
  have restrictedInjective : InjectiveBetween(restrict(productSwap(R, D), I), I, converse(I, R, D))
    constructor
    . have image := converse.image with inside
      rw ← image
      apply restrict.function with function, inside
      intros p hp
      have value := FunctionBetween.apply_closed with function, (inside with p, hp)
      simp [functionImage.membership]
    . intros p hp q hq z hz hpz hqz
      have valueP := FunctionBetween.apply_value with restricted, hp, hpz
      have valueQ := FunctionBetween.apply_value with restricted, hq, hqz
      have stepP := restrict.apply with function, inside, closed, hp
      have stepQ := restrict.apply with function, inside, closed, hq
      rw stepP at valueP
      rw stepQ at valueQ
      have same : productSwap(R, D)(p) = productSwap(R, D)(q) by cc
      exact Injective.apply_cancel with injective, (inside with p, hp), (inside with q, hq), same
  have restrictedSurjective : SurjectiveBetween(restrict(productSwap(R, D), I), I, converse(I, R, D))
    constructor
    . exact restrictedInjective.left
    . intros q hq
      have image := converse.image with inside
      rw ← image at hq
      simp [functionImage.membership] at hq
      obtain ⟨bound, p, hp, shape⟩ := hq
      refine ⟨p, hp, ?_⟩
      have related := FunctionBetween.relates_apply with restrictedInjective.left, hp
      have step := restrict.apply with function, inside, closed, hp
      rwa [step, ← shape] at related
  have bijectiveRestricted : BijectiveBetween(restrict(productSwap(R, D), I), I, converse(I, R, D)) := ⟨restrictedInjective, restrictedSurjective⟩
  have same := cardinality.bijective with finiteI, bijectiveRestricted
  symm
  exact same

-- The handshake lemma.
theorem handshake (I R D : Set)
  requires finiteR : Finite(R)
  requires finiteD : Finite(D)
  requires inside : I ⊆ R × D
  requires rooms : ∀ r ∈ R, cardinality(fiber(I, D, r)) = 0 ∨ cardinality(fiber(I, D, r)) = 1 ∨ cardinality(fiber(I, D, r)) = 2
  requires doors : ∀ d ∈ D, cardinality(cofiber(I, R, d)) = 1 ∨ cardinality(cofiber(I, R, d)) = 2
  requires boundary : Odd(cardinality(boundaryDoors(I, R, D)))
  shows Odd(cardinality(completeRooms(I, R, D)))
proof
  have sizeR : cardinality(R) = cardinality(R) by rfl
  have sizeD : cardinality(D) = cardinality(D) by rfl
  have correctR := cardinality.correct with finiteR
  have correctD := cardinality.correct with finiteD
  have natR := correctR.left
  have natD := correctD.left
  have rowCount := relation.count with finiteR, finiteD, sizeR, inside
  have converseInside := converse.subset at I, R, D
  have columnCount := relation.count with finiteD, finiteR, sizeD, converseInside
  have sameCount := converse.cardinality with finiteR, finiteD, inside
  have rowGraph := fiberSize.function at I, R, D with finiteD
  have columnGraph := fiberSize.function at converse(I, R, D), D, R with finiteR
  have rowWeights : ∀ r ∈ R, fiberSize(I, R, D)(r) = 0 ∨ fiberSize(I, R, D)(r) = 1 ∨ fiberSize(I, R, D)(r) = 2
    intros r hr
    have value := fiberSize.value at I, R, D, r with finiteD
    rw value
    exact rooms with r, hr
  have columnWeights : ∀ d ∈ D, fiberSize(converse(I, R, D), D, R)(d) = 0 ∨ fiberSize(converse(I, R, D), D, R)(d) = 1 ∨ fiberSize(converse(I, R, D), D, R)(d) = 2
    intros d hd
    have value := fiberSize.value at converse(I, R, D), D, R, d with finiteR
    have same := cofiber.converse at I, R, D, d with hd
    rw [value, same]
    have split := doors with d, hd
    cases split with one | two
    . right
      left
      exact one
    . right
      right
      exact two
  have rowParity := natSum.parity_of_size with finiteR, sizeR, rowWeights
  have columnParity := natSum.parity_of_size with finiteD, sizeD, columnWeights
  have rowOnes : ones(R, fiberSize(I, R, D)) = completeRooms(I, R, D)
    ext r
    constructor
    . intro hr
      have parts := ones.membership.forward with hr
      have inR := parts.left
      have value := fiberSize.value at I, R, D, r with finiteD, inR
      have weight := parts.right
      have one : cardinality(fiber(I, D, r)) = 1 by cc
      exact completeRooms.membership.backward with ⟨parts.left, one⟩
    . intro hr
      have parts := completeRooms.membership.forward with hr
      have inR := parts.left
      have value := fiberSize.value at I, R, D, r with finiteD, inR
      have count := parts.right
      have one : fiberSize(I, R, D)(r) = 1 by cc
      exact ones.membership.backward with ⟨parts.left, one⟩
  have columnOnes : ones(D, fiberSize(converse(I, R, D), D, R)) = boundaryDoors(I, R, D)
    ext d
    constructor
    . intro hd
      have parts := ones.membership.forward with hd
      have inD := parts.left
      have value := fiberSize.value at converse(I, R, D), D, R, d with finiteR, inD
      have same := cofiber.converse at I, R, D, d with parts.left
      have weight := parts.right
      have one : cardinality(cofiber(I, R, d)) = 1 by cc
      exact boundaryDoors.membership.backward with ⟨parts.left, one⟩
    . intro hd
      have parts := boundaryDoors.membership.forward with hd
      have inD := parts.left
      have value := fiberSize.value at converse(I, R, D), D, R, d with finiteR, inD
      have same := cofiber.converse at I, R, D, d with parts.left
      have count := parts.right
      have one : fiberSize(converse(I, R, D), D, R)(d) = 1 by cc
      exact ones.membership.backward with ⟨parts.left, one⟩
  rw rowOnes at rowParity
  rw columnOnes at columnParity
  rw ← rowCount at rowParity
  rw [← columnCount, sameCount] at columnParity
  have completeInside : completeRooms(I, R, D) ⊆ R
    intros r hr
    have parts := completeRooms.membership.forward with hr
    exact parts.left
  have finiteComplete := Finite.subset with finiteR, completeInside
  have correctComplete := cardinality.correct with finiteComplete
  have natComplete := correctComplete.left
  have notEvenBoundary := Odd.not_even with boundary
  have notEvenI : ¬Even(cardinality(I))
    intro evenI
    exact notEvenBoundary with (columnParity.forward with evenI)
  have notEvenComplete : ¬Even(cardinality(completeRooms(I, R, D)))
    intro evenComplete
    exact notEvenI with (rowParity.backward with evenComplete)
  have characterization := Odd.iff_not_even at cardinality(completeRooms(I, R, D))
  exact characterization.backward with notEvenComplete