-- Least members of inhabited sets of natural numbers, in ZF.
-- 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.Nat.Least
import Order
import Set.Core

-- Minimality is expressed by membership here; the public order law below
-- hides the von Neumann representation. No arbitrary choice is involved.
defunique leastNatural (S : Set) (n ∈ ℕ) :=
  n ∈ S ∧ (∀ m ∈ n, ¬m ∈ S)
requires inhabited : Nonempty(S)
requires naturals : S ⊆ ℕ
proof
  have nonempty := Nonempty.ne_empty at S with inhabited
  obtain ⟨n, member, minimal⟩ := set.foundation at S with nonempty
  unfold Subset at naturals
  have natural := naturals with n, member
  witness n
  refine ⟨natural, member, minimal⟩
uniqueness
  intros n nNatural nData k kNatural kData
  rcases nData with ⟨nMember, nMinimal⟩
  rcases kData with ⟨kMember, kMinimal⟩
  have nNat := nat.omega.backward at n with nNatural
  have kNat := nat.omega.backward at k with kNatural
  have comparison := Less.trichotomy at n, k with *
  cases comparison with before | rest
  . have inside := membership.of_Less at n, k with *, before
    exfalso
    exact kMinimal with n, inside, nMember
  . cases rest with same | after
    . exact same
    . have inside := membership.of_Less at k, n with *, after
      exfalso
      exact nMinimal with k, inside, kMember

theorem leastNatural.member (S : Set)
  requires inhabited : Nonempty(S)
  requires naturals : S ⊆ ℕ
  shows leastNatural(S) ∈ S
proof
  simp [leastNatural.selected]

theorem leastNatural.least (S : Set, m : Nat)
  requires inhabited : Nonempty(S)
  requires naturals : S ⊆ ℕ
  requires member : m ∈ S
  shows leastNatural(S) ≤ m
proof
  have selected := leastNatural.selected at S with *
  rcases selected with ⟨natural, chosen, minimal⟩
  have chosenNat := nat.omega.backward with natural
  by_contra notLeast
  have before := Less.of_not_LessEqual with *
  have inside := membership.of_Less with *, before
  exact minimal with m, inside, member