-- Set-sized selection from the axiom of choice, without global Choice.
-- 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

-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.
module Grace.Cumulus.Set.ChoiceFunctions
import Core

def inhabitedSubsets (A : Set) : Set := {S ∈ 𝒫(A) | Nonempty(S)}
predicate SubsetChoice (c A : Set) := ∀ S ∈ 𝒫(A), Nonempty(S) → c[S] ∈ S

theorem SubsetChoice.exists (A : Set)
  shows ∃ c, SubsetChoice(c, A)
proof
  have inhabited : ∀ S ∈ inhabitedSubsets(A), ∃ x, x ∈ S
    intros S member
    obtain ⟨subset, nonempty⟩ := inhabitedSubsets.membership.forward with member
    exact nonempty
  obtain ⟨c, function, selects⟩ := set.choice with inhabited
  witness c
  intros S subset nonempty
  have member : S ∈ inhabitedSubsets(A) := inhabitedSubsets.membership.backward with ⟨subset, nonempty⟩
  exact selects with S, member

theorem SubsetChoice.member (c A S : Set)
  requires choice : SubsetChoice(c, A)
  requires subset : S ⊆ A
  requires inhabited : Nonempty(S)
  shows c[S] ∈ S
proof
  unfold Subset at subset
  have bounded := set.powerset.backward with subset
  exact choice with S, bounded, inhabited