-- Laws of natural-number exponentiation: exponent arithmetic, positivity,
-- and monotonicity in the base and in the exponent
-- 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.Nat.PowLemmas
import Pow
import OrderLemmas

theorem pow.add_one (a n : Nat)
  shows a ^ (n + 1) = a * a ^ n
proof
  have shape := add.right_one at n
  rw shape
  exact pow.succ with *

theorem pow.succ_right (a n : Nat)
  shows a ^ (n + 1) = a ^ n * a
proof
  have powNat := pow.closed at a, n
  rw pow.add_one
  exact mul.commutative at a ^ n, a with *

theorem pow.one_right (a : Nat)
  shows a ^ 1 = a
proof
  simp [pow, mul.right_unit]

theorem pow.two (a : Nat)
  shows a ^ 2 = a * a
proof
  simp [pow, mul.right_unit]

theorem pow.one_left (n : Nat)
  shows 1 ^ n = 1
proof
  induction n
  | zero => simp [pow]
  | succ(k) using ih => simp [pow, ih, mul.left_unit]

theorem pow.zero_left (n : Nat)
  shows 0 ^ (n + 1) = 0
proof
  rw pow.add_one
  have powNat := pow.closed at 0, n
  exact mul.left_zero with *

theorem pow.mul_base (a b n : Nat)
  shows (a * b) ^ n = a ^ n * b ^ n
proof
  induction n
  | zero => simp [pow, mul.right_unit]
  | succ(k) using ih =>
    have productNat : Nat(a * b) by typecheck
    have aPow := pow.closed at a, k
    have bPow := pow.closed at b, k
    rw [pow.succ, pow.succ, pow.succ, ih]
    ring

theorem pow.mul_exponent (a m n : Nat)
  shows (a ^ m) ^ n = a ^ (m * n)
proof
  induction n
  | zero =>
    have vanish := mul.right_zero at m
    rw vanish
    have basePow := pow.closed at a, m
    rw [pow.zero, pow.zero]
    rfl
  | succ(k) using ih =>
    have basePow := pow.closed at a, m
    have productNat : Nat(m * k) by typecheck
    have shape : m * succ(k) = m + m * k by ring
    rw [pow.succ, ih, shape]
    have split := pow.add at a, m * k, m
    rw split
    rfl

theorem pow.double_exponent (a k : Nat)
  shows a ^ (2 * k) = (a ^ k) ^ 2
proof
  have inner := pow.mul_exponent at a, k, 2
  have shape : k * 2 = 2 * k by ring
  rw [inner, shape]
  rfl

theorem pow.positive (a n : Nat)
  requires positive : 0 < a
  shows 0 < a ^ n
proof
  induction n
  | zero =>
    rw pow.zero
    linarith
  | succ(k) using ih =>
    have powNat := pow.closed at a, k
    rw pow.succ
    exact Less.mul_positive with positive, ih

theorem pow.ne_zero (a n : Nat)
  requires nonzero : a ≠ 0
  shows a ^ n ≠ 0
proof
  have positive := Less.positive_of_ne_zero with nonzero
  have powPositive := pow.positive at a, n with positive
  exact Less.ne_zero_of_positive with powPositive

theorem pow.eq_zero (a n : Nat)
  requires zero : a ^ n = 0
  shows a = 0
proof
  by_contra nonzero
  have excluded := pow.ne_zero at a, n with nonzero
  exact excluded with zero

theorem pow.eq_zero_iff (a n : Nat)
  shows a ^ (n + 1) = 0 ↔ a = 0
proof
  constructor
  . intro zero
    exact pow.eq_zero with zero
  . intro zero
    rw zero
    exact pow.zero_left with *

theorem pow.ge_one (a n : Nat)
  requires one : 1 ≤ a
  shows 1 ≤ a ^ n
proof
  induction n
  | zero =>
    rw pow.zero
    linarith
  | succ(k) using ih =>
    have powNat := pow.closed at a, k
    rw pow.succ
    exact LessEqual.one_le_mul with one, ih

theorem pow.one_lt (a n : Nat)
  requires above : 1 < a
  shows 1 < a ^ (n + 1)
proof
  have powNat := pow.closed at a, n
  have one : 1 ≤ a by linarith
  have tail := pow.ge_one at a, n with one
  have bound := LessEqual.mul at 1, a, 1, a ^ n with one, tail
  rw pow.add_one
  have unit := mul.left_unit at 1
  rw unit at bound
  have strict : 1 < a * 1
    have unit2 := mul.right_unit at a
    rw unit2
    exact above
  have scaled := LessEqual.mul_left at 1, a ^ n, a with tail
  exact Less.transitive_LessEqual with strict, scaled

theorem pow.base_monotone (a b n : Nat)
  requires below : a ≤ b
  shows a ^ n ≤ b ^ n
proof
  induction n
  | zero =>
    rw [pow.zero, pow.zero]
    exact LessEqual.reflexive with *
  | succ(k) using ih =>
    have aPow := pow.closed at a, k
    have bPow := pow.closed at b, k
    rw [pow.succ, pow.succ]
    exact LessEqual.mul with below, ih

theorem pow.base_strict (a b n : Nat)
  requires below : a < b
  shows a ^ (n + 1) < b ^ (n + 1)
proof
  induction n
  | zero =>
    have shape : 0 + 1 = 1 by ring
    rw [shape, pow.one_right, pow.one_right]
    exact below
  | succ(k) using ih =>
    have aPow := pow.closed at a, k + 1
    have bPow := pow.closed at b, k + 1
    have leftShape : a ^ (succ(k) + 1) = a * a ^ (k + 1)
      have step : succ(k) + 1 = (k + 1) + 1 by ring
      rw step
      exact pow.add_one with *
    have rightShape : b ^ (succ(k) + 1) = b * b ^ (k + 1)
      have step : succ(k) + 1 = (k + 1) + 1 by ring
      rw step
      exact pow.add_one with *
    rw [leftShape, rightShape]
    exact Less.mul with below, ih

theorem pow.two_monotone (a b : Nat)
  requires below : a ≤ b
  shows a ^ 2 ≤ b ^ 2
proof
  exact pow.base_monotone at a, b, 2 with below

theorem pow.two_strict (a b : Nat)
  requires below : a < b
  shows a ^ 2 < b ^ 2
proof
  have strict := pow.base_strict at a, b, 1 with below
  have shape : 1 + 1 = 2 by ring
  rw shape at strict
  exact strict

theorem pow.injective_base (a b n : Nat)
  requires same : a ^ (n + 1) = b ^ (n + 1)
  shows a = b
proof
  have comparison := Less.trichotomy at a, b with *
  rcases comparison with less | equal | greater
  . have strict := pow.base_strict at a, b, n with less
    rw same at strict
    exfalso
    exact Less.irreflexive with strict
  . exact equal
  . have strict := pow.base_strict at b, a, n with greater
    rw same at strict
    exfalso
    exact Less.irreflexive with strict

theorem pow.exponent_monotone (a m n : Nat)
  requires one : 1 ≤ a
  requires below : m ≤ n
  shows a ^ m ≤ a ^ n
proof
  obtain ⟨k, kNat, equation⟩ := below
  have aPow := pow.closed at a, m
  have tailNonzero : a ^ k ≠ 0
    have nonzero := LessEqual.one_iff_ne_zero.forward with one
    exact pow.ne_zero at a, k with nonzero
  have split := pow.add at a, k, m
  rw ← equation
  rw split
  exact LessEqual.le_mul_right at a ^ m, a ^ k with tailNonzero

theorem pow.exponent_strict (a m n : Nat)
  requires above : 1 < a
  requires below : m < n
  shows a ^ m < a ^ n
proof
  obtain ⟨k, kNat, equation⟩ := Less.exists_add_one with below
  have aPow := pow.closed at a, m
  have tail := pow.one_lt at a, k with above
  have headNonzero : a ^ m ≠ 0
    have one : 1 ≤ a by linarith
    have nonzero := LessEqual.one_iff_ne_zero.forward with one
    exact pow.ne_zero at a, m with nonzero
  have split := pow.add at a, k + 1, m
  have shape : m + k + 1 = m + (k + 1) by ring
  rw [equation, shape, split]
  have scaled := Less.mul_left at 1, a ^ (k + 1), a ^ m with headNonzero, tail
  have unit := mul.right_unit at a ^ m
  rw unit at scaled
  exact scaled

theorem pow.injective_exponent (a m n : Nat)
  requires above : 1 < a
  requires same : a ^ m = a ^ n
  shows m = n
proof
  have comparison := Less.trichotomy at m, n with *
  rcases comparison with less | equal | greater
  . have strict := pow.exponent_strict at a, m, n with above, less
    rw same at strict
    exfalso
    exact Less.irreflexive with strict
  . exact equal
  . have strict := pow.exponent_strict at a, n, m with above, greater
    rw same at strict
    exfalso
    exact Less.irreflexive with strict

theorem pow.le_self (a n : Nat)
  requires one : 1 ≤ a
  shows a ≤ a ^ (n + 1)
proof
  have bound : 1 ≤ n + 1 by linarith
  have monotone := pow.exponent_monotone at a, 1, n + 1 with one, bound
  rw pow.one_right at monotone
  exact monotone

theorem pow.eq_one (a n : Nat)
  requires one : a ^ (n + 1) = 1
  shows a = 1
proof
  have powNat := pow.closed at a, n
  rw pow.add_one at one
  have both := mul.eq_one with one
  exact both.left

theorem pow.two_succ (n : Nat)
  shows 2 ^ (n + 1) = 2 ^ n + 2 ^ n
proof
  have powNat := pow.closed at 2, n
  rw pow.add_one
  ring

theorem pow.two_gt (n : Nat)
  shows n < 2 ^ n
proof
  induction n
  | zero =>
    rw pow.zero
    linarith
  | succ(k) using ih =>
    have powNat := pow.closed at 2, k
    have positive : 0 < 2 ^ k
      have two : 0 < 2 by linarith
      exact pow.positive at 2, k with two
    have doubled := pow.two_succ at k
    have shape : succ(k) = k + 1 by ring
    rw [shape, doubled]
    linarith

theorem pow.add_one_le_two (n : Nat)
  shows n + 1 ≤ 2 ^ n
proof
  have powNat := pow.closed at 2, n
  have strict := pow.two_gt at n
  linarith

theorem pow.two_add (a b : Nat)
  shows (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
proof
  rw [pow.two, pow.two, pow.two]
  ring