-- Natural powers in a monoid
-- 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.Algebra.Group.Power
import Core
import Nat.Core

-- Natural powers belong to every monoid.  The carrier and its multiplication
-- remain explicit here so all concrete algebraic structures share one
-- recursion and one collection of laws.
def monoidPow (op unit x : Set, n : Nat) → Set
  | op, unit, x, zero => unit
  | op, unit, x, succ(n) => op(x, monoidPow(op, unit, x, n))

notation scoped monoidPow(R, x, n) => monoidPow(R.mul, R.one, x, n)

theorem monoidPow.zero (op unit x : Set)
  shows monoidPow(op, unit, x, 0) = unit
proof
  simp [monoidPow]

theorem monoidPow.succ (op unit x : Set, n : Nat)
  shows monoidPow(op, unit, x, succ(n)) =
    op(x, monoidPow(op, unit, x, n))
proof
  simp [monoidPow]

theorem monoidPow.closed (A op unit x : Set, n : Nat)
  requires monoid : IsMonoid(A, op, unit)
  requires xInA : x ∈ A
  shows monoidPow(op, unit, x, n) ∈ A
proof
  induction n
  | zero =>
    rw monoidPow.zero
    exact IsMonoid.unit_in_carrier with monoid
  | succ(k) using ih =>
    rw monoidPow.succ
    exact IsMonoid.closed with monoid, xInA, ih

theorem monoidPow.add (A op unit x : Set, m n : Nat)
  requires monoid : IsMonoid(A, op, unit)
  requires xInA : x ∈ A
  shows monoidPow(op, unit, x, m + n) =
    op(monoidPow(op, unit, x, m), monoidPow(op, unit, x, n))
proof
  induction m
  | zero =>
    have powerNInA := monoidPow.closed with monoid, xInA
    rw [add.left_unit, monoidPow.zero]
    have leftIdentity := IsMonoid.left_identity with monoid, powerNInA
    rw leftIdentity
    rfl
  | succ(k) using ih =>
    have powerKInA := monoidPow.closed at A, op, unit, x, k with
      monoid, xInA
    have powerNInA := monoidPow.closed at A, op, unit, x, n with
      monoid, xInA
    have associative := IsMonoid.associative with monoid
    rw [add, monoidPow.succ, monoidPow.succ, ih]
    have reassociate := Associative.law with associative, xInA, powerKInA, powerNInA
    rw reassociate
    rfl

theorem monoidPow.one (A op unit x : Set)
  requires monoid : IsMonoid(A, op, unit)
  requires hx : x ∈ A
  shows monoidPow(op, unit, x, 1) = x
proof
  have identity := IsMonoid.right_identity with monoid, hx
  simp [monoidPow, identity]

theorem monoidPow.succ_right (A op unit x : Set, n : Nat)
  requires monoid : IsMonoid(A, op, unit)
  requires hx : x ∈ A
  shows monoidPow(op, unit, x, n + 1) =
    op(monoidPow(op, unit, x, n), x)
proof
  have split := monoidPow.add at A, op, unit, x, n, 1 with monoid, hx
  have one := monoidPow.one with monoid, hx
  rw [split, one]
  rfl

theorem monoidPow.succ_left (A op unit x : Set, n : Nat)
  requires monoid : IsMonoid(A, op, unit)
  requires hx : x ∈ A
  shows monoidPow(op, unit, x, n + 1) =
    op(x, monoidPow(op, unit, x, n))
proof
  rw add.right_one
  exact monoidPow.succ

theorem monoidPow.commute (A op unit x : Set, n : Nat)
  requires monoid : IsMonoid(A, op, unit)
  requires hx : x ∈ A
  shows op(x, monoidPow(op, unit, x, n)) =
    op(monoidPow(op, unit, x, n), x)
proof
  have left := monoidPow.succ_left with monoid, hx
  have right := monoidPow.succ_right with monoid, hx
  cc

theorem monoidPow.add_commute (A op unit x : Set, m n : Nat)
  requires monoid : IsMonoid(A, op, unit)
  requires hx : x ∈ A
  shows op(monoidPow(op, unit, x, m), monoidPow(op, unit, x, n)) =
    op(monoidPow(op, unit, x, n), monoidPow(op, unit, x, m))
proof
  have first := monoidPow.add at A, op, unit, x, m, n with monoid, hx
  have second := monoidPow.add at A, op, unit, x, n, m with monoid, hx
  have swap := add.commutative at n, m
  rw [← first, ← second, swap]
  rfl

theorem monoidPow.unit (A op unit : Set, n : Nat)
  requires monoid : IsMonoid(A, op, unit)
  shows monoidPow(op, unit, unit, n) = unit
proof
  induction n
  | zero =>
    exact monoidPow.zero at op, unit, unit
  | succ(k) using ih =>
    have unitIn := IsMonoid.unit_in_carrier with monoid
    have identity := IsMonoid.left_identity with monoid, unitIn
    rw [monoidPow.succ, ih]
    exact identity

theorem monoidPow.mul (A op unit x : Set, m n : Nat)
  requires monoid : IsMonoid(A, op, unit)
  requires hx : x ∈ A
  shows monoidPow(op, unit, x, mul(m, n)) =
    monoidPow(op, unit, monoidPow(op, unit, x, m), n)
proof
  induction n
  | zero =>
    rw [mul.right_zero, monoidPow.zero, monoidPow.zero]
    rfl
  | succ(k) using ih =>
    have powerM := monoidPow.closed at A, op, unit, x, m with monoid, hx
    have step := mul.succ_right at k, m
    have split := monoidPow.add at A, op, unit, x, m, mul(m, k) with monoid, hx
    rw [step, split, ih, monoidPow.succ]
    rfl