-- Ordinals
-- 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.Set.Ordinal
import Classes
import Foundation

-- Von Neumann ordinals: transitive sets whose elements are transitive.
predicate Transitive (A : Set) := ∀ x ∈ A, (x ⊆ A)
class Ordinal (α : Set) := { α | Transitive(α) ∧ (∀ β ∈ α, Transitive(β)) }

def next (α : Set) : Set := α ∪ {α}
predicate Limit (λ : Set) := λ ∈ Ordinal ∧ λ ≠ ∅ ∧ (∀ α ∈ λ, next(α) ∈ λ)

-- Foundation supplies the well-founded relation used by both bounded and
-- class-sized ordinal recursion.  The subset premise exposes the usual API.
theorem membership.wellFounded (A : Set)
  shows ∀ s, (∀ x ∈ s, x ∈ A) → s ≠ ∅ → ∃ m ∈ s, (∀ y ∈ m, ¬y ∈ s)
proof
  simp [set.foundation]

theorem Transitive.empty
  shows Transitive(∅)
proof
  simp [Transitive, Subset, set.empty]

theorem Ordinal.empty
  shows empty ∈ Ordinal
proof
  simp [Ordinal, Transitive, set.empty]

theorem next.membership (x α : Set)
  shows x ∈ next(α) ↔ (x ∈ α ∨ x = α)
proof
  simp [next, union2.membership, singleton.membership]

theorem next.contains (α : Set)
  shows α ∈ next(α)
proof
  simp

theorem Ordinal.transitive (α : Set)
  requires h : α ∈ Ordinal
  shows Transitive(α)
proof
  simp [Ordinal]

theorem Ordinal.member_transitive (α β : Set)
  requires hAlpha : α ∈ Ordinal
  requires hBeta : β ∈ α
  shows Transitive(β)
proof
  simp [Ordinal]

theorem Ordinal.next (α : Set)
  requires h : α ∈ Ordinal
  shows next(α) ∈ Ordinal
proof
  simp [Ordinal, Transitive, Subset, next.membership]

theorem next.natural (n : Nat)
  shows succ(n) = next(n)
proof
  simp [nat.succ, next, union2, singleton]

theorem Ordinal.natural (n : Nat)
  shows n ∈ Ordinal
proof
  induction n
  | zero => settle with nat.zero, Ordinal.empty
  | succ(k) using ih => settle with next.natural, Ordinal.next

theorem Ordinal.member (α β : Set)
  requires hAlpha : α ∈ Ordinal
  requires hBeta : β ∈ α
  shows β ∈ Ordinal
proof
  simp [Ordinal, Transitive, Subset]

theorem Ordinal.union (A : Set)
  requires hOrdinal : ∀ α ∈ A, α ∈ Ordinal
  shows ⋃(A) ∈ Ordinal
proof
  simp [Ordinal, Transitive, Subset, Ordinal.transitive, set.union, Ordinal.member]

theorem Ordinal.trichotomy (α : Set)
  shows α ∈ Ordinal → ∀ β, β ∈ Ordinal → (α ∈ β ∨ α = β ∨ β ∈ α)
proof
  induction α using membership
  intros a ihA hA β
  induction β using membership
  intros b ihB hB
  by_contra hNotComparable
  apply hNotComparable
  right
  left
  ext z
  constructor
  . intro hzA
    have hzOrdinal := Ordinal.member with hA, hzA
    have hzComparison := ihA with hzA, hzOrdinal, b, hB
    cases hzComparison with hzB | hzRest
    . exact hzB
    . cases hzRest with hzbEqual | hbInZ
      . exfalso
        rw hzbEqual at hzA
        apply hNotComparable
        right
        right
        exact hzA
      . exfalso
        have hATransitive := Ordinal.transitive with hA
        have hzSubset := hATransitive with z, hzA
        apply hNotComparable
        right
        right
        exact hzSubset with b, hbInZ
  . intro hzB
    have hzOrdinal := Ordinal.member with hB, hzB
    have hzComparison := ihB with hzB, hzOrdinal
    cases hzComparison with haInZ | hzRest
    . exfalso
      have hBTransitive := Ordinal.transitive with hB
      have hzSubset := hBTransitive with z, hzB
      apply hNotComparable
      left
      exact hzSubset with a, haInZ
    . cases hzRest with hazEqual | hzA
      . exfalso
        rw ← hazEqual at hzB
        apply hNotComparable
        left
        exact hzB
      . exact hzA

theorem Ordinal.cases (β : Set)
  requires hBeta : β ∈ Ordinal
  shows β = ∅ ∨ (∃ α ∈ β, next(α) = β) ∨ Limit(β)
proof
  by_contra hNotCases
  apply hNotCases
  right
  right
  unfold Limit
  refine ⟨hBeta, ⟨?_, ?_⟩⟩
  . intro hEmpty
    apply hNotCases
    left
    exact hEmpty
  . intros α hAlpha
    have hAlphaOrdinal := Ordinal.member with hBeta, hAlpha
    have hNextOrdinal := Ordinal.next with hAlphaOrdinal
    have comparison := Ordinal.trichotomy with hNextOrdinal, β, hBeta
    cases comparison with hNextInBeta | hRest
    . exact hNextInBeta
    . cases hRest with hNextEqual | hBetaInNext
      . exfalso
        apply hNotCases
        right
        left
        refine ⟨α, hAlpha, hNextEqual⟩
      . exfalso
        simp [next.membership] at hBetaInNext
        cases hBetaInNext with hBetaInAlpha | hBetaEqual
        . have hTransitive := Ordinal.transitive with hBeta
          have hAlphaSubset := hTransitive with α, hAlpha
          exact membership.irreflexive with (hAlphaSubset with β, hBetaInAlpha)
        . rw hBetaEqual at hAlpha
          exact membership.irreflexive with hAlpha

theorem Ordinal.subset_bound (α β : Set)
  requires hAlpha : α ∈ Ordinal
  requires hBeta : β ∈ Ordinal
  requires hSubset : α ⊆ β
  shows α ∈ next(β)
proof
  simp [Subset, Ordinal.trichotomy, next.membership, membership.irreflexive]