-- Finite cardinality and equipotence
-- 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.Finite
import Function
import Set.Ordinal
import Nat

-- Cardinal comparison starts from set-valued bijections.  There is no
-- quotient or meta-level notion of cardinal behind these definitions.
predicate Equipotent (A B : Set) := ∃ f, BijectiveBetween(f, A, B)
notation infix 50 "≃" => Equipotent

predicate HasCardinality (A n : Set) := Nat(n) ∧ A ≃ n
predicate Finite (A : Set) := ∃ n, HasCardinality(A, n)

-- The unique graph carrying x to 0. Since 1 is the von Neumann singleton
-- {0}, this is the canonical bijection from {x} to 1.
def singletonEquiv (x : Set) : Set := {(x ↦ 0)}

theorem one.membership (z : Set)
  shows z ∈ 1 ↔ z = 0
proof
  have successorZero := next.natural at 0
  rw successorZero
  simp [next.membership, nat.zero, set.empty]

theorem singletonEquiv.membership (p x : Set)
  shows p ∈ singletonEquiv(x) ↔ p = (x ↦ 0)
proof
  simp [singletonEquiv, singleton.membership]

theorem singletonEquiv.relation (x : Set)
  shows RelationBetween(singletonEquiv(x), {x}, 1)
proof
  intros p hp
  simp [singletonEquiv.membership] at hp
  rw hp
  apply product.pair
  exact singleton.self
  apply one.membership.backward
  rfl

theorem singletonEquiv.functional (x : Set)
  shows Functional(singletonEquiv(x))
proof
  intros a b hab c hac
  unfold relates at hab
  simp [singletonEquiv.membership] at hab
  obtain (hax, hb0) := orderedPair.injective with hab
  unfold relates at hac
  simp [singletonEquiv.membership] at hac
  obtain (hax2, hc0) := orderedPair.injective with hac
  rw [hb0, hc0]
  rfl

theorem singletonEquiv.function (x : Set)
  shows singletonEquiv(x) : {x} → 1
proof
  constructor
  exact singletonEquiv.relation
  constructor
  exact singletonEquiv.functional
  intros a ha
  witness 0
  constructor
  apply one.membership.backward
  rfl
  unfold relates
  apply singletonEquiv.membership.backward
  simp [singleton.membership] at ha
  rw ha
  rfl

theorem singletonEquiv.injective (x : Set)
  shows InjectiveBetween(singletonEquiv(x), {x}, 1)
proof
  simp [InjectiveBetween, singletonEquiv.function]

theorem singletonEquiv.surjective (x : Set)
  shows SurjectiveBetween(singletonEquiv(x), {x}, 1)
proof
  constructor
  exact singletonEquiv.function
  intros z hz
  simp [one.membership] at hz
  witness x
  constructor
  exact singleton.self
  unfold relates
  apply singletonEquiv.membership.backward
  rw hz
  rfl

theorem singletonEquiv.bijective (x : Set)
  shows BijectiveBetween(singletonEquiv(x), {x}, 1)
proof
  refine ⟨singletonEquiv.injective at x, singletonEquiv.surjective at x⟩

theorem Equipotent.singleton_one (x : Set)
  shows Equipotent({x}, 1)
proof
  witness singletonEquiv(x)
  exact singletonEquiv.bijective

theorem Equipotent.reflexive (A : Set)
  shows Equipotent(A, A)
proof
  witness identity(A)
  exact identity.bijective

theorem HasCardinality.empty_set
  shows HasCardinality(∅, 0)
proof
  constructor
  . exact Naturals.constructor.zero
  . rw nat.zero
    exact Equipotent.reflexive

theorem Equipotent.symmetric (A B : Set)
  requires h : Equipotent(A, B)
  shows Equipotent(B, A)
proof
  simp [Equipotent, converse.bijective]

theorem Equipotent.transitive (A B C : Set)
  requires hAB : Equipotent(A, B)
  requires hBC : Equipotent(B, C)
  shows Equipotent(A, C)
proof
  obtain (f, hf) := hAB
  obtain (g, hg) := hBC
  witness compose(g, f, A, B, C)
  exact compose.bijective with hf, hg

theorem HasCardinality.natural (A n : Set)
  requires h : HasCardinality(A, n)
  shows Nat(n)
proof
  rcases h with (natural, equipotent)
  exact natural

theorem HasCardinality.equipotent (A n : Set)
  requires h : HasCardinality(A, n)
  shows Equipotent(A, n)
proof
  rcases h with (natural, equipotent)
  exact equipotent

theorem Finite.from_cardinality (A n : Set)
  requires h : HasCardinality(A, n)
  shows Finite(A)
proof
  witness n
  exact h

theorem Finite.natural (n : Nat)
  shows Finite(n)
proof
  witness n
  refine ⟨assumption, Equipotent.reflexive at n⟩

theorem Finite.enumeration (D : Set)
  requires finite : Finite(D)
  shows ∃ n, Nat(n) ∧ ∃ f, BijectiveBetween(f, n, D)
proof
  obtain ⟨n, natural, equivalent⟩ := finite
  obtain ⟨f, bijective⟩ := equivalent
  have inverse := converse.bijective with bijective
  refine ⟨n, natural, converse(f, D, n), inverse⟩

theorem Finite.of_equipotent (A B : Set)
  requires finiteA : Finite(A)
  requires hAB : Equipotent(A, B)
  shows Finite(B)
proof
  obtain ⟨n, natural, hAn⟩ := finiteA
  witness n
  constructor
  exact natural
  have hBA := Equipotent.symmetric with hAB
  exact Equipotent.transitive with hBA, hAn

theorem Finite.zero
  shows Finite(0)
proof
  simp [Finite.natural, Naturals.constructor.zero]

theorem Finite.empty
  shows Finite(∅)
proof
  rw ← nat.zero
  exact Finite.zero

theorem Finite.singleton (x : Set)
  shows Finite({x})
proof
  witness 1
  constructor
  have zeroNatural := Naturals.constructor.zero
  exact Naturals.constructor.succ with zeroNatural
  exact Equipotent.singleton_one

-- A finite sequence of natural-valued function outputs has a common strict
-- bound.  This graph-level lemma is the bridge from cardinal finiteness to
-- number-theoretic boundedness.
lemma TotalBetween.bounded_step (f A a : Set, k b c : Nat)
  requires bounded : ∀ x ∈ k, ∀ y ∈ A, relates(f, x, y) → y ∈ succ(b)
  requires functional : Functional(f)
  requires hka : relates(f, k, a)
  requires aIn : a ∈ succ(c)
  requires lift : ∀ y ∈ succ(b), y ∈ succ(c)
  shows ∀ x ∈ succ(k), ∀ y ∈ A, relates(f, x, y) → y ∈ succ(c)
proof
  intros x hx y hyA hxy
  have xShape := membership.successor_forward{n := k} at x
  cases xShape with hxOld | hxCurrent
  . exact lift with y, (bounded with x, hxOld, y, hyA, hxy)
  . rw hxCurrent at hxy
    have unique := Functional.unique with functional, hxy, hka
    rwa unique

lemma TotalBetween.natural_values_bounded (f A : Set, n : Nat)
  requires functional : Functional(f)
  requires naturalValues : ∀ y ∈ A, Nat(y)
  shows TotalBetween(f, n, A) → ∃ b, Nat(b) ∧ (∀ x ∈ n, ∀ y ∈ A, relates(f, x, y) → y ∈ succ(b))
proof
  induction n
  | zero =>
    intro total
    witness 0
    intros x hx
    exfalso
    simp [nat.zero, set.empty]
  | succ(k) using ih =>
    intro total
    have previousTotal := TotalBetween.predecessor with h_k, total
    obtain ⟨b, hbNat, bounded⟩ := ih with previousTotal
    have kMember := membership.self_successor with h_k
    obtain ⟨a, haA, hka⟩ := total with k, kMember
    have haNat := naturalValues with haA
    have haOrdinal := Ordinal.natural with haNat
    have hbOrdinal := Ordinal.natural with hbNat
    have comparison := Ordinal.trichotomy with haOrdinal, b, hbOrdinal
    cases comparison with haInB | hRest
    . have aIn : a ∈ succ(b) by simp
      have lift : ∀ y ∈ succ(b), y ∈ succ(b) by simp
      exact ⟨b, hbNat, (TotalBetween.bounded_step with bounded, functional, hka, aIn, lift)⟩
    . cases hRest with haEqB | hbInA
      . have aIn : a ∈ succ(b) by simp
        have lift : ∀ y ∈ succ(b), y ∈ succ(b) by simp
        exact ⟨b, hbNat, (TotalBetween.bounded_step with bounded, functional, hka, aIn, lift)⟩
      . have aIn := membership.self_successor with haNat
        have lift : ∀ y ∈ succ(b), y ∈ succ(a)
          intros y hy
          exact membership.successor_monotone with haNat, hbNat, hbInA, hy
        exact ⟨a, haNat, (TotalBetween.bounded_step with bounded, functional, hka, aIn, lift)⟩

lemma Subset.omega_elements_natural (A : Set)
  requires hNatural : A ⊆ ℕ
  shows ∀ y ∈ A, Nat(y)
proof
  simp [Subset, omega.natural]

theorem Finite.naturals_bounded (A : Set)
  requires hNatural : A ⊆ ℕ
  requires hFinite : Finite(A)
  shows ∃ b, Nat(b) ∧ (∀ y ∈ A, y ∈ succ(b))
proof
  obtain ⟨n, hnNat, f, hf⟩ := hFinite
  have inverse := converse.bijective with hf
  have surjective := Bijective.surjective with inverse
  have fn := Surjective.function with surjective
  have functional := FunctionBetween.functional with fn
  have total := FunctionBetween.total with fn
  have naturalValues := Subset.omega_elements_natural with hNatural
  obtain ⟨b, hbNat, bounded⟩ := TotalBetween.natural_values_bounded with hnNat, functional, naturalValues, total
  witness b
  intros y hyA
  rcases surjective with ⟨surjectiveFunction, onto⟩
  specialize onto with y, hyA
  obtain ⟨x, hxN, hxy⟩ := onto
  exact bounded with x, hxN, y, hyA, hxy

-- A reusable public bridge from finite cardinality to Nat order:
-- no finite set of naturals can have an element strictly above every bound.
theorem infinite.of_unbounded_naturals (A : Set)
  requires hNatural : A ⊆ ℕ
  requires hUnbounded : ∀ n, Nat(n) → ∃ y ∈ A, n < y
  shows ¬Finite(A)
proof
  intro hFinite
  obtain ⟨b, hbNat, allBounded⟩ := Finite.naturals_bounded with hNatural, hFinite
  obtain ⟨y, hyA, hbLessY⟩ := hUnbounded with hbNat
  have naturalValues := Subset.omega_elements_natural with hNatural
  have hyNat := naturalValues with hyA
  have hbInY := membership.of_Less with hbNat, hyNat, hbLessY
  specialize allBounded with y, hyA
  have shape := membership.successor_forward{n := b} at y
  cases shape with hyInB | hyEqB
  . have hyOrdinal := Ordinal.natural at y with hyNat
    have transitive := Ordinal.transitive with hyOrdinal
    have bSubsetY := transitive with hbInY, y, hyInB
    exact membership.irreflexive with bSubsetY
  . rw hyEqB at hbInY
    exact membership.irreflexive with hbInY

theorem omega.order_unbounded (n : Set)
  requires hn : Nat(n)
  shows ∃ y ∈ ℕ, n < y
proof
  witness succ(n)
  constructor
  . have successor := Naturals.constructor.succ at n with hn
    exact nat.omega.forward with successor
  . unfold Less
    have successor := Naturals.constructor.succ with hn
    exact LessEqual.reflexive with successor

theorem omega.infinite
  shows ¬Finite(ℕ)
proof
  have natural := Subset.reflexive at ℕ
  have unbounded : ∀ n, Nat(n) → ∃ y ∈ ℕ, n < y by exact omega.order_unbounded
  exact infinite.of_unbounded_naturals with natural, unbounded