-- The laws of ordinal arithmetic: associativity of addition and
-- multiplication, left distributivity, and the two power laws, each by
-- transfinite induction on the right argument
-- 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.ArithmeticLaws
import Monotone

theorem ordinalAdd.associative (α β : Ordinal, γ : Set)
  shows γ ∈ Ordinal → (α + β) + γ = α + (β + γ)
proof
  induction γ using membership
  intros current ih hCurrent
  have βOrdinal : β ∈ Ordinal by assumption
  have sumOrdinal := ordinalAdd.ordinal at α, β with βOrdinal
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . rw zero
    rw ← nat.zero
    have first := ordinalAdd.zero at α + β
    have second := ordinalAdd.zero at β
    rw [first, second]
    rfl
  . cases rest with successor | limit
    . obtain ⟨δ, hδ, shape⟩ := successor
      rw ← shape
      have δOrdinal := Ordinal.member with hCurrent, hδ
      have step := ih with hδ, δOrdinal
      have innerOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal
      have first := ordinalAdd.next at α + β, δ
      have second := ordinalAdd.next at β, δ
      have third := ordinalAdd.next at α, β + δ
      rw [first, second, third, step]
      rfl
    . have innerLimit := ordinalAdd.limit_right at β, current with limit
      have innerOrdinal := ordinalAdd.ordinal at β, current with hCurrent
      apply Subset.antisymmetric
      . intros x hx
        obtain ⟨δ, hδ, hxδ⟩ :=
          ordinalAdd.limit_membership.forward at x, α + β, current
            with limit, hx
        have δOrdinal := Ordinal.member with hCurrent, hδ
        have step := ih with hδ, δOrdinal
        rw step at hxδ
        apply ordinalAdd.limit_membership.backward at x, α, β + current
          with innerLimit
        witness β + δ
        constructor
        . exact ordinalAdd.monotone at β, δ, current with hCurrent, hδ
        . exact hxδ
      . intros x hx
        obtain ⟨ε, hε, hxε⟩ :=
          ordinalAdd.limit_membership.forward at x, α, β + current
            with innerLimit, hx
        obtain ⟨δ, hδ, hεδ⟩ :=
          ordinalAdd.limit_membership.forward at ε, β, current with limit, hε
        have δOrdinal := Ordinal.member with hCurrent, hδ
        have stageOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal
        have εOrdinal := Ordinal.member with stageOrdinal, hεδ
        have grows := ordinalAdd.monotone at α, ε, β + δ with stageOrdinal, hεδ
        have sumStage := ordinalAdd.ordinal at α, β + δ with stageOrdinal
        have included := Ordinal.member_subset with sumStage, grows
        have step := ih with hδ, δOrdinal
        apply ordinalAdd.limit_membership.backward at x, α + β, current
          with limit
        witness δ
        constructor
        . exact hδ
        . rw step
          exact included with x, hxε

theorem ordinalMul.distributive (α β : Ordinal, γ : Set)
  shows γ ∈ Ordinal → α * (β + γ) = α * β + α * γ
proof
  induction γ using membership
  intros current ih hCurrent
  have αOrdinal : α ∈ Ordinal by assumption
  have βOrdinal : β ∈ Ordinal by assumption
  have productOrdinal := ordinalMul.ordinal at α, β with βOrdinal
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . rw zero
    rw ← nat.zero
    have first := ordinalAdd.zero at β
    have second := ordinalMul.zero at α
    have third := ordinalAdd.zero at α * β
    rw nat.zero at third
    rw [first, second, third]
    rfl
  . cases rest with successor | limit
    . obtain ⟨δ, hδ, shape⟩ := successor
      rw ← shape
      have δOrdinal := Ordinal.member with hCurrent, hδ
      have step := ih with hδ, δOrdinal
      have sumOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal
      have stageOrdinal := ordinalMul.ordinal at α, δ with δOrdinal
      have first := ordinalAdd.next at β, δ
      have second := ordinalMul.next at α, β + δ
      have third := ordinalMul.next at α, δ
      have fourth := ordinalAdd.associative at α * β, α * δ, α with αOrdinal
      rw [first, second, step, third, fourth]
      rfl
    . have zeroCases := Ordinal.trichotomy at ∅ with Ordinal.empty, α, αOrdinal
      cases zeroCases with positive | rest2
      . have innerLimit := ordinalAdd.limit_right at β, current with limit
        have productLimit := ordinalMul.limit_right at α, current
          with positive, limit
        have innerOrdinal := ordinalAdd.ordinal at β, current with hCurrent
        have productCurrent := ordinalMul.ordinal at α, current with hCurrent
        apply Subset.antisymmetric
        . intros x hx
          obtain ⟨ε, hε, hxε⟩ :=
            ordinalMul.limit_membership.forward at x, α, β + current
              with innerLimit, hx
          obtain ⟨δ, hδ, hεδ⟩ :=
            ordinalAdd.limit_membership.forward at ε, β, current with limit, hε
          have δOrdinal := Ordinal.member with hCurrent, hδ
          have sumOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal
          have εOrdinal := Ordinal.member with sumOrdinal, hεδ
          have included := ordinalMul.subset_monotone at α, ε, β + δ
            with sumOrdinal, hεδ
          have step := ih with hδ, δOrdinal
          have inStage : x ∈ α * (β + δ) := included with x, hxε
          rw step at inStage
          apply ordinalAdd.limit_membership.backward at x, α * β, α * current
            with productLimit
          witness α * δ
          constructor
          . exact ordinalMul.monotone at α, δ, current
            with positive, hCurrent, hδ
          . exact inStage
        . intros x hx
          obtain ⟨ε, hε, hxε⟩ :=
            ordinalAdd.limit_membership.forward at x, α * β, α * current
              with productLimit, hx
          obtain ⟨δ, hδ, hεδ⟩ :=
            ordinalMul.limit_membership.forward at ε, α, current with limit, hε
          have δOrdinal := Ordinal.member with hCurrent, hδ
          have stageOrdinal := ordinalMul.ordinal at α, δ with δOrdinal
          have εOrdinal := Ordinal.member with stageOrdinal, hεδ
          have grows := ordinalAdd.monotone at α * β, ε, α * δ
            with stageOrdinal, hεδ
          have sumStage := ordinalAdd.ordinal at α * β, α * δ with stageOrdinal
          have included := Ordinal.member_subset with sumStage, grows
          have step := ih with hδ, δOrdinal
          apply ordinalMul.limit_membership.backward at x, α, β + current
            with innerLimit
          witness β + δ
          constructor
          . exact ordinalAdd.monotone at β, δ, current with hCurrent, hδ
          . rw step
            exact included with x, hxε
      . cases rest2 with equal | below
        . rw ← nat.zero at equal
          rw ← equal
          have innerOrdinal := ordinalAdd.ordinal at β, current with hCurrent
          have first := ordinalMul.zero_left at β + current with innerOrdinal
          have second := ordinalMul.zero_left at β with βOrdinal
          have third := ordinalMul.zero_left at current with hCurrent
          rw [first, second, third]
          symm
          exact ordinalAdd.zero at 0
        . exfalso
          exact set.empty with below

theorem ordinalMul.associative (α β : Ordinal, γ : Set)
  shows γ ∈ Ordinal → (α * β) * γ = α * (β * γ)
proof
  induction γ using membership
  intros current ih hCurrent
  have αOrdinal : α ∈ Ordinal by assumption
  have βOrdinal : β ∈ Ordinal by assumption
  have productOrdinal := ordinalMul.ordinal at α, β with βOrdinal
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . rw zero
    rw ← nat.zero
    have first := ordinalMul.zero at α * β
    have second := ordinalMul.zero at β
    have third := ordinalMul.zero at α
    rw nat.zero at third
    rw [first, second, third]
    rfl
  . cases rest with successor | limit
    . obtain ⟨δ, hδ, shape⟩ := successor
      rw ← shape
      have δOrdinal := Ordinal.member with hCurrent, hδ
      have step := ih with hδ, δOrdinal
      have innerOrdinal := ordinalMul.ordinal at β, δ with δOrdinal
      have first := ordinalMul.next at α * β, δ
      have second := ordinalMul.next at β, δ
      have third := ordinalMul.distributive at α, β * δ, β with βOrdinal
      rw [first, step, second, third]
      rfl
    . have zeroCases := Ordinal.trichotomy at ∅ with Ordinal.empty, β, βOrdinal
      cases zeroCases with positive | rest2
      . have innerLimit := ordinalMul.limit_right at β, current
          with positive, limit
        have innerOrdinal := ordinalMul.ordinal at β, current with hCurrent
        apply Subset.antisymmetric
        . intros x hx
          obtain ⟨δ, hδ, hxδ⟩ :=
            ordinalMul.limit_membership.forward at x, α * β, current
              with limit, hx
          have δOrdinal := Ordinal.member with hCurrent, hδ
          have step := ih with hδ, δOrdinal
          rw step at hxδ
          apply ordinalMul.limit_membership.backward at x, α, β * current
            with innerLimit
          witness β * δ
          constructor
          . exact ordinalMul.monotone at β, δ, current
            with positive, hCurrent, hδ
          . exact hxδ
        . intros x hx
          obtain ⟨ε, hε, hxε⟩ :=
            ordinalMul.limit_membership.forward at x, α, β * current
              with innerLimit, hx
          obtain ⟨δ, hδ, hεδ⟩ :=
            ordinalMul.limit_membership.forward at ε, β, current with limit, hε
          have δOrdinal := Ordinal.member with hCurrent, hδ
          have stageOrdinal := ordinalMul.ordinal at β, δ with δOrdinal
          have εOrdinal := Ordinal.member with stageOrdinal, hεδ
          have included := ordinalMul.subset_monotone at α, ε, β * δ
            with stageOrdinal, hεδ
          have step := ih with hδ, δOrdinal
          apply ordinalMul.limit_membership.backward at x, α * β, current
            with limit
          witness δ
          constructor
          . exact hδ
          . rw step
            exact included with x, hxε
      . cases rest2 with equal | below
        . rw ← nat.zero at equal
          rw ← equal
          have first : α * 0 = 0
            rw ordinalMul.zero
            symm
            exact nat.zero
          have second := ordinalMul.zero_left at current with hCurrent
          rw [first, second, first]
          rfl
        . exfalso
          exact set.empty with below

-- Powers

theorem ordinalPow.one_left (β : Set)
  shows β ∈ Ordinal → ordinalPow(1, β) = 1
proof
  induction β using membership
  intros current ih hCurrent
  have oneOrdinal := Ordinal.natural at 1
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . rw zero
    have base := ordinalPow.zero at 1
    rw nat.zero at base
    exact base
  . cases rest with successor | limit
    . obtain ⟨γ, hγ, shape⟩ := successor
      rw ← shape
      have γOrdinal := Ordinal.member with hCurrent, hγ
      have step := ih with hγ, γOrdinal
      rw [ordinalPow.next, step]
      exact ordinalMul.one at 1
    . apply Subset.antisymmetric
      . intros x hx
        obtain ⟨stage, hStage, hxStage⟩ :=
          ordinalPow.limit_membership.forward at x, 1, current with limit, hx
        have step := ih with hStage, (Ordinal.member with hCurrent, hStage)
        rw step at hxStage
        exact hxStage
      . intros x hx
        apply ordinalPow.limit_membership.backward at x, 1, current with limit
        witness ∅
        constructor
        . exact Ordinal.zero_member with limit.right.left
        . have base := ordinalPow.zero at 1
          rw nat.zero at base
          rw base
          exact hx

-- A positive ordinal is one or lies above one.
theorem Ordinal.one_or_above_one (α : Ordinal)
  requires positive : ∅ ∈ α
  shows α = 1 ∨ 1 ∈ α
proof
  have αOrdinal : α ∈ Ordinal by assumption
  have oneOrdinal := Ordinal.natural at 1
  have cases := Ordinal.trichotomy at α with αOrdinal, 1, oneOrdinal
  cases cases with below | rest
  . exfalso
    have one : 1 = next(0) by simp [next.natural]
    rw one at below
    simp [next.membership] at below
    cases below with inZero | isZero
    . rw nat.zero at inZero
      exact set.empty with inZero
    . rw isZero at positive
      rw nat.zero at positive
      exact set.empty with positive
  . cases rest with equal | above
    . left
      exact equal
    . right
      exact above

theorem ordinalPow.add (α β : Ordinal, γ : Set)
  requires positive : ∅ ∈ α
  shows γ ∈ Ordinal → α ^ (β + γ) = α ^ β * α ^ γ
proof
  induction γ using membership
  intros current ih hCurrent
  have αOrdinal : α ∈ Ordinal by assumption
  have βOrdinal : β ∈ Ordinal by assumption
  have powerOrdinal := ordinalPow.ordinal at α, β with βOrdinal
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . rw zero
    rw ← nat.zero
    have first := ordinalAdd.zero at β
    have second := ordinalPow.zero at α
    have third := ordinalMul.one at α ^ β
    rw [first, second, third]
    rfl
  . cases rest with successor | limit
    . obtain ⟨δ, hδ, shape⟩ := successor
      rw ← shape
      have δOrdinal := Ordinal.member with hCurrent, hδ
      have step := ih with hδ, δOrdinal
      have sumOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal
      have stageOrdinal := ordinalPow.ordinal at α, δ with δOrdinal
      have first := ordinalAdd.next at β, δ
      have second := ordinalPow.next at α, β + δ
      have third := ordinalPow.next at α, δ
      have fourth := ordinalMul.associative at α ^ β, α ^ δ, α with αOrdinal
      rw [first, second, step, third, fourth]
      rfl
    . have oneCases := Ordinal.one_or_above_one with positive
      cases oneCases with one | above
      . rw one
        have innerOrdinal := ordinalAdd.ordinal at β, current with hCurrent
        have first := ordinalPow.one_left at β + current with innerOrdinal
        have second := ordinalPow.one_left at β with βOrdinal
        have third := ordinalPow.one_left at current with hCurrent
        rw [first, second, third]
        symm
        exact ordinalMul.one at 1
      . have innerLimit := ordinalAdd.limit_right at β, current with limit
        have powerLimit := ordinalPow.limit_right at α, current
          with above, limit
        have innerOrdinal := ordinalAdd.ordinal at β, current with hCurrent
        have powerCurrent := ordinalPow.ordinal at α, current with hCurrent
        apply Subset.antisymmetric
        . intros x hx
          obtain ⟨ε, hε, hxε⟩ :=
            ordinalPow.limit_membership.forward at x, α, β + current
              with innerLimit, hx
          obtain ⟨δ, hδ, hεδ⟩ :=
            ordinalAdd.limit_membership.forward at ε, β, current with limit, hε
          have δOrdinal := Ordinal.member with hCurrent, hδ
          have sumOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal
          have εOrdinal := Ordinal.member with sumOrdinal, hεδ
          have included := ordinalPow.subset_monotone at α, ε, β + δ
            with positive, sumOrdinal, hεδ
          have step := ih with hδ, δOrdinal
          have inStage : x ∈ α ^ (β + δ) := included with x, hxε
          rw step at inStage
          apply ordinalMul.limit_membership.backward at x, α ^ β, α ^ current
            with powerLimit
          witness α ^ δ
          constructor
          . exact ordinalPow.monotone at α, δ, current with above, hCurrent, hδ
          . exact inStage
        . intros x hx
          obtain ⟨ε, hε, hxε⟩ :=
            ordinalMul.limit_membership.forward at x, α ^ β, α ^ current
              with powerLimit, hx
          obtain ⟨δ, hδ, hεδ⟩ :=
            ordinalPow.limit_membership.forward at ε, α, current with limit, hε
          have δOrdinal := Ordinal.member with hCurrent, hδ
          have stageOrdinal := ordinalPow.ordinal at α, δ with δOrdinal
          have εOrdinal := Ordinal.member with stageOrdinal, hεδ
          have included := ordinalMul.subset_monotone at α ^ β, ε, α ^ δ
            with stageOrdinal, hεδ
          have step := ih with hδ, δOrdinal
          apply ordinalPow.limit_membership.backward at x, α, β + current
            with innerLimit
          witness β + δ
          constructor
          . exact ordinalAdd.monotone at β, δ, current with hCurrent, hδ
          . rw step
            exact included with x, hxε

theorem ordinalPow.mul (α β : Ordinal, γ : Set)
  requires positive : ∅ ∈ α
  shows γ ∈ Ordinal → (α ^ β) ^ γ = α ^ (β * γ)
proof
  induction γ using membership
  intros current ih hCurrent
  have αOrdinal : α ∈ Ordinal by assumption
  have βOrdinal : β ∈ Ordinal by assumption
  have powerOrdinal := ordinalPow.ordinal at α, β with βOrdinal
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . rw zero
    rw ← nat.zero
    have first := ordinalPow.zero at α ^ β
    have second := ordinalMul.zero at β
    have third := ordinalPow.zero at α
    rw nat.zero at third
    rw [first, second, third]
    rfl
  . cases rest with successor | limit
    . obtain ⟨δ, hδ, shape⟩ := successor
      rw ← shape
      have δOrdinal := Ordinal.member with hCurrent, hδ
      have step := ih with hδ, δOrdinal
      have innerOrdinal := ordinalMul.ordinal at β, δ with δOrdinal
      have first := ordinalPow.next at α ^ β, δ
      have second := ordinalMul.next at β, δ
      have third := ordinalPow.add at α, β * δ, β with positive, βOrdinal
      rw [first, step, second, third]
      rfl
    . have oneCases := Ordinal.one_or_above_one with positive
      cases oneCases with one | above
      . rw one
        have innerOrdinal := ordinalMul.ordinal at β, current with hCurrent
        have first := ordinalPow.one_left at β with βOrdinal
        have second := ordinalPow.one_left at current with hCurrent
        have third := ordinalPow.one_left at β * current with innerOrdinal
        rw [first, second, third]
        rfl
      . have zeroCases := Ordinal.trichotomy at ∅
        with Ordinal.empty, β, βOrdinal
        cases zeroCases with βPositive | rest2
        . have innerLimit := ordinalMul.limit_right at β, current
            with βPositive, limit
          have innerOrdinal := ordinalMul.ordinal at β, current with hCurrent
          apply Subset.antisymmetric
          . intros x hx
            obtain ⟨δ, hδ, hxδ⟩ :=
              ordinalPow.limit_membership.forward at x, α ^ β, current
                with limit, hx
            have δOrdinal := Ordinal.member with hCurrent, hδ
            have step := ih with hδ, δOrdinal
            rw step at hxδ
            apply ordinalPow.limit_membership.backward at x, α, β * current
              with innerLimit
            witness β * δ
            constructor
            . exact ordinalMul.monotone at β, δ, current
                with βPositive, hCurrent, hδ
            . exact hxδ
          . intros x hx
            obtain ⟨ε, hε, hxε⟩ :=
              ordinalPow.limit_membership.forward at x, α, β * current
                with innerLimit, hx
            obtain ⟨δ, hδ, hεδ⟩ :=
              ordinalMul.limit_membership.forward at ε, β, current
                with limit, hε
            have δOrdinal := Ordinal.member with hCurrent, hδ
            have stageOrdinal := ordinalMul.ordinal at β, δ with δOrdinal
            have εOrdinal := Ordinal.member with stageOrdinal, hεδ
            have included := ordinalPow.subset_monotone at α, ε, β * δ
              with positive, stageOrdinal, hεδ
            have step := ih with hδ, δOrdinal
            apply ordinalPow.limit_membership.backward at x, α ^ β, current
              with limit
            witness δ
            constructor
            . exact hδ
            . rw step
              exact included with x, hxε
        . cases rest2 with equal | below
          . rw ← nat.zero at equal
            rw ← equal
            have first := ordinalPow.zero at α
            have second := ordinalMul.zero_left at current with hCurrent
            have third := ordinalPow.one_left at current with hCurrent
            rw [first, second, third, first]
            rfl
          . exfalso
            exact set.empty with below