-- Choice-free selection by least code: a set coded injectively into the
-- naturals lets every point of a domain pick, among the candidates a
-- relation offers it, the one of least code; a domain whose points are
-- separated by candidates from a countable set is countable
-- 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.LeastCode
import Countable
import Set

-- Selection by least code. A relation R offers each point x of D the
-- candidates W ∈ B with relates(R, x, W); under an injective code
-- g : B → ℕ the point selects the candidate of least code. No choice is
-- involved: the least code is the least element of a set of naturals.

def candidates (R x B : Set) : Set := { W ∈ B | relates(R, x, W) }

def candidateCodes (g R x B : Set) : Set := { g(W) | W ∈ candidates(R, x, B) }

def leastCoded (g R D B : Set) : Set :=
  { p ∈ D × B | ∃ x ∈ D, ∃ W ∈ B, p = (x ↦ W) ∧
    relates(R, x, W) ∧ (∀ V ∈ B, relates(R, x, V) → g(W) ⊆ g(V)) }

theorem leastCoded.relates (g R D B x W : Set)
  shows relates(leastCoded(g, R, D, B), x, W) ↔
    x ∈ D ∧ W ∈ B ∧ relates(R, x, W) ∧
      (∀ V ∈ B, relates(R, x, V) → g(W) ⊆ g(V))
proof
  constructor
  . intro edge
    unfold relates at edge
    have parts := leastCoded.membership.forward with edge
    obtain ⟨x2, hx2, W2, hW2, shape, related, least⟩ := parts.right
    obtain ⟨rfl, rfl⟩ := orderedPair.injective with shape
    exact ⟨hx2, hW2, related, least⟩
  . intro h
    obtain ⟨hx, hW, related, least⟩ := h
    unfold relates
    apply leastCoded.membership.backward
    constructor
    . exact product.pair with hx, hW
    . exact ⟨x, hx, W, hW, rfl, related, least⟩

-- Existence: the codes of the candidates form a nonempty set of naturals,
-- hence of ordinals, and its least element is the code of a candidate.
theorem leastCoded.exists (g R D B x : Set)
  requires code : InjectiveBetween(g, B, ℕ)
  requires offered : ∀ x ∈ D, ∃ W ∈ B, relates(R, x, W)
  requires hx : x ∈ D
  shows ∃ W ∈ B, relates(leastCoded(g, R, D, B), x, W)
proof
  have function := Injective.function with code
  obtain ⟨W0, hW0, related0⟩ := offered with x, hx
  have candidate0 : W0 ∈ candidates(R, x, B)
    exact candidates.membership.backward with ⟨hW0, related0⟩
  have code0 : g(W0) ∈ candidateCodes(g, R, x, B)
    exact candidateCodes.membership.backward with ⟨W0, candidate0, rfl⟩
  have ordinals : ∀ n ∈ candidateCodes(g, R, x, B), n ∈ Ordinal
    intros n hn
    obtain ⟨W, hW, shape⟩ := candidateCodes.membership.forward with hn
    have parts := candidates.membership.forward with hW
    have natural := FunctionBetween.apply_closed with function, parts.left
    rw ← shape
    exact Ordinal.member with Ordinal.omega, natural
  have inhabited : Nonempty(candidateCodes(g, R, x, B)) := ⟨g(W0), code0⟩
  have nonempty := Nonempty.ne_empty with inhabited
  obtain ⟨m, hm, least⟩ := Ordinal.least with ordinals, nonempty
  obtain ⟨W, hW, shape⟩ := candidateCodes.membership.forward with hm
  have parts := candidates.membership.forward with hW
  witness W
  constructor
  . exact parts.left
  . apply leastCoded.relates.backward
    refine ⟨hx, parts.left, parts.right, ?_⟩
    intros V hV relatedV
    have candidateV : V ∈ candidates(R, x, B)
      exact candidates.membership.backward with ⟨hV, relatedV⟩
    have codeV : g(V) ∈ candidateCodes(g, R, x, B)
      exact candidateCodes.membership.backward with ⟨V, candidateV, rfl⟩
    rw shape
    exact least with g(V), codeV

-- Uniqueness: two least codes are each below the other, so they are equal,
-- and the code is injective.
theorem leastCoded.unique (g R D B x W V : Set)
  requires code : InjectiveBetween(g, B, ℕ)
  requires first : relates(leastCoded(g, R, D, B), x, W)
  requires second : relates(leastCoded(g, R, D, B), x, V)
  shows W = V
proof
  obtain ⟨hx, hW, relatedW, leastW⟩ := leastCoded.relates.forward with first
  obtain ⟨hx2, hV, relatedV, leastV⟩ := leastCoded.relates.forward with
    second
  have below := leastW with V, hV, relatedV
  have above := leastV with W, hW, relatedW
  have same := Subset.antisymmetric with below, above
  exact Injective.apply_cancel with code, hW, hV, same

theorem leastCoded.function (g R D B : Set)
  requires code : InjectiveBetween(g, B, ℕ)
  requires offered : ∀ x ∈ D, ∃ W ∈ B, relates(R, x, W)
  shows leastCoded(g, R, D, B) : D → B
proof
  refine ⟨?_, ?_, ?_⟩
  . intros p hp
    have parts := leastCoded.membership.forward with hp
    exact parts.left
  . intros x W first V second
    exact leastCoded.unique with code, first, second
  . intros x hx
    exact leastCoded.exists with code, offered, hx

-- When no candidate is offered to two different points, the selection is
-- injective.
theorem leastCoded.injective (g R D B : Set)
  requires code : InjectiveBetween(g, B, ℕ)
  requires offered : ∀ x ∈ D, ∃ W ∈ B, relates(R, x, W)
  requires separated : ∀ x ∈ D, ∀ y ∈ D, ∀ W ∈ B,
    relates(R, x, W) → relates(R, y, W) → x = y
  shows InjectiveBetween(leastCoded(g, R, D, B), D, B)
proof
  constructor
  . exact leastCoded.function with code, offered
  . intros x hx y hy W hW first second
    obtain ⟨hx2, hW2, relatedX, leastX⟩ := leastCoded.relates.forward with
      first
    obtain ⟨hy2, hW3, relatedY, leastY⟩ := leastCoded.relates.forward with
      second
    exact separated with x, hx, y, hy, W, hW, relatedX, relatedY

-- Hence a domain whose points are separated by candidates from a countable
-- set is countable: compose the selection with the code.
theorem leastCoded.countable (g R D B : Set)
  requires code : InjectiveBetween(g, B, ℕ)
  requires offered : ∀ x ∈ D, ∃ W ∈ B, relates(R, x, W)
  requires separated : ∀ x ∈ D, ∀ y ∈ D, ∀ W ∈ B,
    relates(R, x, W) → relates(R, y, W) → x = y
  shows Countable(D)
proof
  have injective := leastCoded.injective with code, offered, separated
  have composite := compose.injective with injective, code
  exact ⟨compose(g, leastCoded(g, R, D, B), D, B, ℕ), composite⟩