-- Infinite sets survive removing a point and pass through injections,
-- subsets of a given size under inclusion, insertion, and removal, and the
-- infinite pigeonhole principle: a map from an infinite set to a finite set
-- has an infinite fibre
-- 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.Combinatorics.RamseyPigeonhole
import Partitions
import Cardinal.Dominance

-- Infinite sets

theorem Infinite.nonempty (A : Set)
  requires infinite : Infinite(A)
  shows Nonempty(A)
proof
  by_contra none
  have empty : A = ∅
    by_contra different
    exact none with (Nonempty.of_ne_empty with different)
  unfold Infinite at infinite
  apply infinite
  rw empty
  exact Finite.empty

theorem Infinite.remove (A a : Set)
  requires infinite : Infinite(A)
  shows Infinite(A ∖ {a})
proof
  unfold Infinite
  intro finite
  unfold Infinite at infinite
  apply infinite
  have inserted := Finite.insert at A ∖ {a}, a with finite
  have covered : A ⊆ insert(a, A ∖ {a}) by simp
  exact Finite.subset with inserted, covered

theorem Infinite.of_equipotent (A B : Set)
  requires infinite : Infinite(A)
  requires equipotent : A ≃ B
  shows Infinite(B)
proof
  unfold Infinite
  intro finite
  unfold Infinite at infinite
  apply infinite
  exact Finite.of_equipotent with finite, (Equipotent.symmetric with equipotent)

theorem Infinite.injective_image (f A B : Set)
  requires injective : InjectiveBetween(f, A, B)
  requires infinite : Infinite(A)
  shows Infinite(functionImage(f, A, B))
proof
  exact Infinite.of_equipotent with infinite, (Equipotent.image with injective)

-- Subsets of a given size

theorem subsetsOfSize.subset (T A k : Set)
  requires member : T ∈ subsetsOfSize(A, k)
  shows T ⊆ A
proof
  have parts := subsetsOfSize.membership.forward with member
  exact powerset.membership_iff.forward with parts.left

theorem subsetsOfSize.counted (T A k : Set)
  requires member : T ∈ subsetsOfSize(A, k)
  shows HasCardinality(T, k)
proof
  have parts := subsetsOfSize.membership.forward with member
  exact parts.right

theorem subsetsOfSize.of_subset (T A k : Set)
  requires subset : T ⊆ A
  requires counted : HasCardinality(T, k)
  shows T ∈ subsetsOfSize(A, k)
proof
  apply subsetsOfSize.membership.backward
  exact ⟨powerset.membership_iff.backward with subset, counted⟩

theorem subsetsOfSize.monotone (A B k : Set)
  requires subset : A ⊆ B
  shows subsetsOfSize(A, k) ⊆ subsetsOfSize(B, k)
proof
  intros T hT
  have inA := subsetsOfSize.subset with hT
  have counted := subsetsOfSize.counted with hT
  have inB := Subset.transitive with inA, subset
  exact subsetsOfSize.of_subset with inB, counted

theorem subsetsOfSize.member_of_subset (T A B k : Set)
  requires subset : A ⊆ B
  requires member : T ∈ subsetsOfSize(A, k)
  shows T ∈ subsetsOfSize(B, k)
proof
  have inA := subsetsOfSize.subset with member
  have counted := subsetsOfSize.counted with member
  have inB := Subset.transitive with inA, subset
  exact subsetsOfSize.of_subset with inB, counted

-- Adjoining a fresh point of A to an n-subset of A gives an (n + 1)-subset.
theorem subsetsOfSize.insert_member (T A a : Set) (n : Nat)
  requires member : T ∈ subsetsOfSize(A, n)
  requires ha : a ∈ A
  requires fresh : ¬a ∈ T
  shows insert(a, T) ∈ subsetsOfSize(A, n + 1)
proof
  have subset := subsetsOfSize.subset with member
  have counted := subsetsOfSize.counted with member
  have one : n + 1 = succ(n) := add.right_one with *
  rw one
  have inserted : insert(a, T) ⊆ A
    intros x hx
    have split := insert.membership.forward with hx
    cases split with same | inT
    . rw same
      exact ha
    . exact subset with x, inT
  have insertedCount := HasCardinality.insert_fresh with counted, fresh
  exact subsetsOfSize.of_subset with inserted, insertedCount

-- Removing a point of an (n + 1)-subset leaves an n-subset.
theorem subsetsOfSize.remove_member (U A a : Set) (n : Nat)
  requires member : U ∈ subsetsOfSize(A, n + 1)
  requires ha : a ∈ U
  shows U ∖ {a} ∈ subsetsOfSize(A, n)
proof
  have subset := subsetsOfSize.subset with member
  have counted := subsetsOfSize.counted with member
  have one : n + 1 = succ(n) := add.right_one with *
  rw one at counted
  have removed : U ∖ {a} ⊆ A :=
    Subset.transitive with (difference.subset_left at U, {a}), subset
  have removedCount := HasCardinality.remove with counted, ha
  exact subsetsOfSize.of_subset with removed, removedCount

theorem subsetsOfSize.exists_member (U A : Set) (n : Nat)
  requires member : U ∈ subsetsOfSize(A, n + 1)
  shows ∃ u, u ∈ U
proof
  have counted := subsetsOfSize.counted with member
  have one : n + 1 = succ(n) := add.right_one with *
  rw one at counted
  exact HasCardinality.exists_member with counted

-- The infinite pigeonhole principle

-- The fibre of g over a point of the codomain, as a map into the subsets of
-- the domain.
defgraph fiberOf (g A K : Set) (c ∈ K) : 𝒫(A) :=
  functionPreimage(g, A, {c})
proof
  have subset := functionPreimage.subset at g, A, {c}
  exact powerset.membership_iff.backward with subset

theorem pigeonhole.infinite_fiber (g A K : Set)
  requires function : g : A → K
  requires infinite : Infinite(A)
  requires finite : Finite(K)
  shows ∃ c ∈ K, Infinite(functionPreimage(g, A, {c}))
proof
  by_contra none
  have graph := fiberOf.function at g, A, K
  have fibresFinite : ∀ F ∈ functionImage(fiberOf(g, A, K), K, 𝒫(A)),
      Finite(F)
    intros F hF
    have parts := functionImage.membership.forward with hF
    obtain ⟨c, hc, shape⟩ := parts.right
    have value := fiberOf.value at g, A, K, c with hc
    rw [shape, value]
    by_contra notFinite
    apply none
    exact ⟨c, hc, notFinite⟩
  have familyFinite := Finite.function_image with
    graph, finite, (Subset.reflexive at K)
  have unionFinite := Finite.big_union with familyFinite, fibresFinite
  have covered : A ⊆ ⋃(functionImage(fiberOf(g, A, K), K, 𝒫(A)))
    intros x hx
    have valueK := FunctionBetween.apply_closed with function, hx
    have inFibre : x ∈ functionPreimage(g, A, {g(x)}) :=
      functionPreimage.point_membership.backward with ⟨hx, rfl⟩
    have value := fiberOf.value at g, A, K, g(x) with valueK
    have fibreIn := functionImage.value with graph, valueK
    rw value at fibreIn
    exact union.contains with fibreIn, inFibre
  unfold Infinite at infinite
  apply infinite
  exact Finite.subset with unionFinite, covered