-- Natural powers of real numbers
-- 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.Real.Power
import Ring
import Algebra.Group.Power

-- Real powers are the specialization of monoid powers to multiplication.
-- The heterogeneous notation records its type: Real × Nat → Real.
def realPow (A : Real, n : Nat) : Real :=
  monoidPow(realMul, realOne, A, n)

notation infixr 80 "^" => realPow for Real, Nat

theorem realPow.real (A : Real, n : Nat)
  shows Real(A ^ n)
proof
  have typedA : Real(A) by typecheck
  unfold realPow
  have closed := monoidPow.closed at
    ℝ, realMul, realOne, A, n with realMul.monoid, typedA
  exact closed

theorem realPow.zero (A : Real)
  shows A ^ 0 = 1
proof
  unfold realPow
  exact monoidPow.zero

theorem realPow.succ (A : Real, n : Nat)
  shows A ^ succ(n) = A * A ^ n
proof
  unfold realPow
  exact monoidPow.succ with assumption

theorem realPow.add (A : Real, m n : Nat)
  shows A ^ (m + n) = A ^ m * A ^ n
proof
  have typedA : Real(A) by typecheck
  unfold Real at typedA
  unfold realPow
  exact monoidPow.add with realMul.monoid, typedA

theorem realPow.one (n : Nat)
  shows (1:R) ^ n = (1:R)
proof
  induction n
  | zero =>
    rw realPow.zero
    rfl
  | succ(k) using ih =>
    rw [realPow.succ, ih]
    ring

theorem realPow.zero_succ (n : Nat)
  shows (0:R) ^ succ(n) = (0:R)
proof
  rw realPow.succ
  ring

theorem realPow.mul (A B : Real, n : Nat)
  shows (A * B) ^ n = A ^ n * B ^ n
proof
  induction n
  | zero =>
    rw [realPow.zero, realPow.zero, realPow.zero]
    ring
  | succ(k) using ih =>
    rw [realPow.succ, realPow.succ, realPow.succ, ih]
    ring

theorem realPow.two (A : Real)
  shows A ^ succ(succ(0)) = A * A
proof
  rw [realPow.succ, realPow.succ, realPow.zero]
  ring