-- Arithmetic at ω, the first limit ordinal: finite ordinals are absorbed
-- on the left, so addition, multiplication, and exponentiation are not
-- commutative
-- 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.Omega
import ArithmeticLaws
import Nat.Foundation

-- Finite ordinals are closed under the three operations.

theorem ordinalAdd.natural (n m : Nat)
  shows Nat(ordinalAdd(n, m))
proof
  induction m
  | zero =>
    have nOrdinal := Ordinal.natural at n
    have base := ordinalAdd.zero at n
    rw base
    assumption
  | succ(k) using ih =>
    have nOrdinal := Ordinal.natural at n
    have kOrdinal := Ordinal.natural at k
    have shape := next.natural at k
    rw [shape, ordinalAdd.next]
    have back := next.natural at ordinalAdd(n, k)
    rw ← back
    exact Naturals.constructor.succ with ih

theorem ordinalMul.natural (n m : Nat)
  shows Nat(ordinalMul(n, m))
proof
  induction m
  | zero =>
    have nOrdinal := Ordinal.natural at n
    have base := ordinalMul.zero at n
    rw [base, ← nat.zero]
    exact Naturals.constructor.zero
  | succ(k) using ih =>
    have nOrdinal := Ordinal.natural at n
    have kOrdinal := Ordinal.natural at k
    have shape := next.natural at k
    rw [shape, ordinalMul.next]
    exact ordinalAdd.natural at ordinalMul(n, k), n

theorem ordinalPow.natural (n m : Nat)
  shows Nat(ordinalPow(n, m))
proof
  induction m
  | zero =>
    have nOrdinal := Ordinal.natural at n
    have base := ordinalPow.zero at n
    rw base
    exact Naturals.constructor.succ with Naturals.constructor.zero
  | succ(k) using ih =>
    have nOrdinal := Ordinal.natural at n
    have kOrdinal := Ordinal.natural at k
    have shape := next.natural at k
    rw [shape, ordinalPow.next]
    exact ordinalMul.natural at ordinalPow(n, k), n

-- Addition: every finite ordinal is absorbed by ω on the left.

theorem ordinalAdd.natural_omega (n : Nat)
  shows ordinalAdd(n, ω) = ω
proof
  have nOrdinal := Ordinal.natural at n
  have limit := Limit.omega
  have ωOrdinal := Ordinal.omega
  apply Subset.antisymmetric
  . intros x hx
    obtain ⟨m, hm, hxm⟩ :=
      ordinalAdd.limit_membership.forward at x, n, ω with limit, hx
    have mNat := nat.omega.backward with hm
    have sumNat := ordinalAdd.natural at n, m
    have sumIn := nat.omega.forward with sumNat
    have included := Ordinal.member_subset with ωOrdinal, sumIn
    exact included with x, hxm
  . intros m hm
    have mNat := nat.omega.backward with hm
    have mOrdinal := Ordinal.natural at m
    have included := ordinalAdd.subset_right at n, m with mOrdinal
    have sumOrdinal := ordinalAdd.ordinal at n, m with mOrdinal
    have bound := Ordinal.subset_bound with mOrdinal, sumOrdinal, included
    apply ordinalAdd.limit_membership.backward at m, n, ω with limit
    witness next(m)
    constructor
    . exact limit.right.right with m, hm
    . rw ordinalAdd.next
      exact bound

theorem ordinalAdd.one_omega
  shows 1 + ω = ω
proof
  exact ordinalAdd.natural_omega at 1

theorem ordinalAdd.not_commutative
  shows 1 + ω ≠ ω + 1
proof
  intro equal
  have ωOrdinal := Ordinal.omega
  rw [ordinalAdd.one_omega, ordinalAdd.one] at equal
  have self := next.contains at ω
  rw ← equal at self
  exact Ordinal.not_member_self with self

-- Multiplication: every positive finite ordinal is absorbed by ω on the left.

theorem ordinalMul.natural_omega (n : Nat)
  requires positive : ∅ ∈ n
  shows ordinalMul(n, ω) = ω
proof
  have nOrdinal := Ordinal.natural at n
  have limit := Limit.omega
  have ωOrdinal := Ordinal.omega
  apply Subset.antisymmetric
  . intros x hx
    obtain ⟨m, hm, hxm⟩ :=
      ordinalMul.limit_membership.forward at x, n, ω with limit, hx
    have mNat := nat.omega.backward with hm
    have productNat := ordinalMul.natural at n, m
    have productIn := nat.omega.forward with productNat
    have included := Ordinal.member_subset with ωOrdinal, productIn
    exact included with x, hxm
  . intros m hm
    have mNat := nat.omega.backward with hm
    have mOrdinal := Ordinal.natural at m
    have nextOrdinal := Ordinal.next with mOrdinal
    have included := ordinalMul.subset_right at n, next(m)
      with positive, nextOrdinal
    apply ordinalMul.limit_membership.backward at m, n, ω with limit
    witness next(m)
    constructor
    . exact limit.right.right with m, hm
    . exact included with m, (next.contains at m)

theorem ordinalMul.two (α : Ordinal)
  shows α * 2 = α + α
proof
  have two : 2 = next(1) by simp [next.natural]
  rw [two, ordinalMul.next, ordinalMul.one]
  rfl

theorem ordinalMul.two_omega
  shows 2 * ω = ω
proof
  have positive : ∅ ∈ 2
    apply membership.two.backward
    left
    symm
    exact nat.zero
  exact ordinalMul.natural_omega at 2 with positive

theorem ordinalMul.not_commutative
  shows 2 * ω ≠ ω * 2
proof
  intro equal
  have ωOrdinal := Ordinal.omega
  rw [ordinalMul.two_omega, ordinalMul.two] at equal
  have limit := Limit.omega
  have zeroIn := Ordinal.zero_member with limit.right.left
  have grows := ordinalAdd.member_right at ω, ω with zeroIn
  rw ← equal at grows
  exact Ordinal.not_member_self with grows

-- Exponentiation: every finite base above one is absorbed by ω.

theorem ordinalPow.natural_omega (n : Nat)
  requires above : 1 ∈ n
  shows ordinalPow(n, ω) = ω
proof
  have nOrdinal := Ordinal.natural at n
  have limit := Limit.omega
  have ωOrdinal := Ordinal.omega
  apply Subset.antisymmetric
  . intros x hx
    obtain ⟨m, hm, hxm⟩ :=
      ordinalPow.limit_membership.forward at x, n, ω with limit, hx
    have mNat := nat.omega.backward with hm
    have powerNat := ordinalPow.natural at n, m
    have powerIn := nat.omega.forward with powerNat
    have included := Ordinal.member_subset with ωOrdinal, powerIn
    exact included with x, hxm
  . intros m hm
    have mNat := nat.omega.backward with hm
    have mOrdinal := Ordinal.natural at m
    have nextOrdinal := Ordinal.next with mOrdinal
    have included := ordinalPow.subset_right at n, next(m)
      with above, nextOrdinal
    apply ordinalPow.limit_membership.backward at m, n, ω with limit
    witness next(m)
    constructor
    . exact limit.right.right with m, hm
    . exact included with m, (next.contains at m)

theorem ordinalPow.two_omega
  shows 2 ^ ω = ω
proof
  have above : 1 ∈ 2
    apply membership.two.backward
    right
    rfl
  exact ordinalPow.natural_omega at 2 with above

theorem ordinalPow.not_commutative
  shows 2 ^ ω ≠ ω ^ 2
proof
  intro equal
  have ωOrdinal := Ordinal.omega
  have two : 2 = next(1) by simp [next.natural]
  rw [ordinalPow.two_omega, two, ordinalPow.next, ordinalPow.one] at equal
  have limit := Limit.omega
  have zeroIn := Ordinal.zero_member with limit.right.left
  have oneNat := Naturals.constructor.succ with Naturals.constructor.zero
  have oneIn := nat.omega.forward with oneNat
  have grows := ordinalMul.member_right at ω, ω with zeroIn, oneIn
  rw ← equal at grows
  exact Ordinal.not_member_self with grows