-- Integer powers with natural-number exponents
-- 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.Int.Pow
import AbsoluteValueOrder
import Nat.PowLemmas

def integerPow (z : Integer, n : Nat) → Integer
  | z, zero => integerOne
  | z, succ(k) => z * integerPow(z, k)

theorem integerPow.zero (z : Integer)
  shows integerPow(z, 0) = 1
proof
  simp [integerPow]

theorem integerPow.succ (z : Integer, n : Nat)
  shows integerPow(z, succ(n)) = z * integerPow(z, n)
proof
  simp [integerPow]

theorem integerPow.add_one (z : Integer, n : Nat)
  shows integerPow(z, n + 1) = z * integerPow(z, n)
proof
  have shape := add.right_one at n
  rw shape
  exact integerPow.succ with *

theorem integerPow.integer (z : Integer, n : Nat)
  shows Integer(integerPow(z, n))
proof
  induction n
  | zero =>
    rw integerPow.zero
    exact integerOne.integer
  | succ(k) using ih =>
    rw integerPow.succ
    exact integerMulValue.integer with *

theorem integerPow.one_right (z : Integer)
  shows integerPow(z, 1) = z
proof
  simp [integerPow, integerMulValue.one_right]

theorem integerPow.two (z : Integer)
  shows integerPow(z, 2) = z * z
proof
  simp [integerPow, integerMulValue.one_right]

theorem integerPow.one_left (n : Nat)
  shows integerPow(integerOne, n) = 1
proof
  induction n
  | zero => exact integerPow.zero at integerOne
  | succ(k) using ih =>
    rw [integerPow.succ, ih]
    ring

theorem integerPow.zero_left (n : Nat)
  shows integerPow(integerZero, n + 1) = 0
proof
  have powInteger := integerPow.integer at integerZero, n
  rw integerPow.add_one
  ring

theorem integerPow.add (z : Integer, m n : Nat)
  shows integerPow(z, m + n) = integerPow(z, m) * integerPow(z, n)
proof
  induction n
  | zero =>
    have unit := add.right_unit at m
    have powInteger := integerPow.integer at z, m
    rw [unit, integerPow.zero]
    ring
  | succ(k) using ih =>
    have shape := add.succ_right at k, m
    have left := integerPow.integer at z, m
    have right := integerPow.integer at z, k
    rw [shape, integerPow.succ, integerPow.succ, ih]
    ring

theorem integerPow.mul_base (x y : Integer, n : Nat)
  shows integerPow(x * y, n) = integerPow(x, n) * integerPow(y, n)
proof
  induction n
  | zero =>
    rw [integerPow.zero, integerPow.zero, integerPow.zero]
    ring
  | succ(k) using ih =>
    have product := integerMulValue.integer at x, y
    have left := integerPow.integer at x, k
    have right := integerPow.integer at y, k
    rw [integerPow.succ, integerPow.succ, integerPow.succ, ih]
    ring

theorem integerPow.mul_exponent (z : Integer, m n : Nat)
  shows integerPow(integerPow(z, m), n) = integerPow(z, m * n)
proof
  induction n
  | zero =>
    have vanish := mul.right_zero at m
    rw [vanish, integerPow.zero, integerPow.zero]
    rfl
  | succ(k) using ih =>
    have base := integerPow.integer at z, m
    have productNat : Nat(m * k) by typecheck
    have shape : m * succ(k) = m + m * k by ring
    rw [integerPow.succ, ih, shape]
    have split := integerPow.add at z, m, m * k
    rw split
    rfl

theorem integerPow.ofNat (a n : Nat)
  shows integerPow(integerOfNat(a), n) = integerOfNat(a ^ n)
proof
  induction n
  | zero =>
    rw [integerPow.zero, pow.zero]
    unfold integerOne
    rfl
  | succ(k) using ih =>
    have powNat := pow.closed at a, k
    rw [integerPow.succ, ih, pow.succ]
    exact integerMulValue.ofNat with *

theorem integerPow.nonneg (z : Integer, n : Nat)
  requires nonnegative : 0 ≤ z
  shows 0 ≤ integerPow(z, n)
proof
  induction n
  | zero =>
    rw integerPow.zero
    exact integerLe.zero_one
  | succ(k) using ih =>
    have powInteger := integerPow.integer at z, k
    rw integerPow.succ
    exact integerLe.mul_nonneg with nonnegative, ih

theorem integerPow.positive (z : Integer, n : Nat)
  requires positive : 0 < z
  shows 0 < integerPow(z, n)
proof
  induction n
  | zero =>
    rw integerPow.zero
    exact integerLess.zero_one
  | succ(k) using ih =>
    have powInteger := integerPow.integer at z, k
    rw integerPow.succ
    exact integerLess.mul_positive with positive, ih

theorem integerPow.square_nonneg (z : Integer)
  shows 0 ≤ integerPow(z, 2)
proof
  rw integerPow.two
  exact integerLe.square_nonneg with *

theorem integerPow.square_eq_zero_iff (z : Integer)
  shows integerPow(z, 2) = 0 ↔ z = 0
proof
  rw integerPow.two
  exact integerMulValue.square_eq_zero_iff with *

theorem integerPow.eq_zero (z : Integer, n : Nat)
  requires zero : integerPow(z, n) = 0
  shows z = 0
proof
  induction n
  | zero =>
    intro zero
    rw integerPow.zero at zero
    have strict := integerLess.zero_one
    rw zero at strict
    exfalso
    exact integerLess.irreflexive with strict
  | succ(k) using ih =>
    intro zero
    have powInteger := integerPow.integer at z, k
    rw integerPow.succ at zero
    have split := integerMulValue.eq_zero with zero
    cases split with base | tail
    . exact base
    . exact ih with tail

theorem integerPow.ne_zero (z : Integer, n : Nat)
  requires nonzero : z ≠ 0
  shows integerPow(z, n) ≠ 0
proof
  intro zero
  have same := integerPow.eq_zero with zero
  exact nonzero with same

theorem integerPow.abs (z : Integer, n : Nat)
  shows integerAbs(integerPow(z, n)) = integerPow(integerAbs(z), n)
proof
  induction n
  | zero =>
    rw [integerPow.zero, integerPow.zero]
    exact integerAbs.one
  | succ(k) using ih =>
    have powInteger := integerPow.integer at z, k
    rw [integerPow.succ, integerPow.succ, integerAbs.mul, ih]
    rfl

theorem integerPow.abs_square (z : Integer)
  shows integerPow(integerAbs(z), 2) = integerPow(z, 2)
proof
  rw [integerPow.two, integerPow.two]
  exact integerAbs.square with *

theorem integerPow.neg_double (z : Integer, k : Nat)
  shows integerPow(-z, k + k) = integerPow(z, k + k)
proof
  have split := integerPow.add at -z, k, k
  have splitZ := integerPow.add at z, k, k
  have negPow := integerPow.integer at -z, k
  have zPow := integerPow.integer at z, k
  have square : integerPow(-z, k) * integerPow(-z, k) =
      integerPow(z, k) * integerPow(z, k)
    have product := integerPow.mul_base at -z, -z, k
    have productZ := integerPow.mul_base at z, z, k
    have shape : (-z) * (-z) = z * z by ring
    rw [← product, shape, productZ]
    rfl
  rw [split, splitZ, square]
  rfl

theorem integerPow.neg_double_add_one (z : Integer, k : Nat)
  shows integerPow(-z, k + k + 1) = -integerPow(z, k + k + 1)
proof
  have doubleNeg := integerPow.integer at -z, k + k
  have doubleZ := integerPow.integer at z, k + k
  have even := integerPow.neg_double at z, k
  rw [integerPow.add_one, integerPow.add_one, even]
  ring

theorem integerPow.base_monotone (x y : Integer, n : Nat)
  requires nonnegative : 0 ≤ x
  requires below : x ≤ y
  shows integerPow(x, n) ≤ integerPow(y, n)
proof
  induction n
  | zero =>
    rw [integerPow.zero, integerPow.zero]
    exact integerLe.reflexive with *
  | succ(k) using ih =>
    have xPow := integerPow.integer at x, k
    have yPow := integerPow.integer at y, k
    have xPowNonnegative := integerPow.nonneg at x, k with nonnegative
    rw [integerPow.succ, integerPow.succ]
    exact integerLe.mul with nonnegative, below, xPowNonnegative, ih