------------------------------------------------------------------------
-- The Agda standard library
--
-- Exponentiation defined over a semiring as repeated multiplication
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra
open import Data.Nat.Base as  using (; zero; suc)
open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
import Data.Nat.Properties as 

module Algebra.Properties.Semiring.Exp
  {a } (S : Semiring a ) where

open Semiring S
open import Relation.Binary.Reasoning.Setoid setoid
import Algebra.Properties.Monoid.Mult *-monoid as Mult

------------------------------------------------------------------------
-- Definition

open import Algebra.Definitions.RawSemiring rawSemiring public
  using (_^_)

------------------------------------------------------------------------
-- Properties

^-congˡ :  n  (_^ n) Preserves _≈_  _≈_
^-congˡ = Mult.×-congʳ

^-cong : _^_ Preserves₂ _≈_  _≡_  _≈_
^-cong x≈y u≡v = Mult.×-cong u≡v x≈y

^-congʳ :  x  (x ^_) Preserves _≡_  _≈_
^-congʳ x = Mult.×-congˡ

-- xᵐ⁺ⁿ ≈ xᵐxⁿ
^-homo-* :  x m n  x ^ (m ℕ.+ n)  (x ^ m) * (x ^ n)
^-homo-* = Mult.×-homo-+

-- (xᵐ)ⁿ≈xᵐ*ⁿ
^-assocʳ :  x m n  (x ^ m) ^ n  x ^ (m ℕ.* n)
^-assocʳ x m n rewrite ℕ.*-comm m n = Mult.×-assocˡ x n m

------------------------------------------------------------------------
-- A lemma using commutativity, needed for the Binomial Theorem

y*x^m*y^n≈x^m*y^[n+1] :  {x} {y} (x*y≈y*x : x * y  y * x) 
                         m n  y * (x ^ m * y ^ n)  x ^ m * y ^ suc n
y*x^m*y^n≈x^m*y^[n+1] {x} {y} x*y≈y*x = helper
  where
    helper :  m n  y * (x ^ m * y ^ n)  x ^ m * y ^ suc n
    helper zero    n = begin
      y * (x ^ ℕ.zero * y ^ n)  ≡⟨⟩
      y * (1# * y ^ n)          ≈⟨ *-congˡ (*-identityˡ (y ^ n)) 
      y * (y ^ n)               ≡⟨⟩
      y ^ (suc n)               ≈˘⟨ *-identityˡ (y ^ suc n) 
      1# * y ^ (suc n)          ≡⟨⟩
      x ^ ℕ.zero * y ^ (suc n)  
    helper (suc m) n = begin
      y * (x ^ suc m * y ^ n)    ≡⟨⟩
      y * ((x * x ^ m) * y ^ n)  ≈⟨ *-congˡ (*-assoc x (x ^ m) (y ^ n)) 
      y * (x * (x ^ m * y ^ n))  ≈˘⟨ *-assoc y x (x ^ m * y ^ n) 
      y * x * (x ^ m * y ^ n)    ≈˘⟨ *-congʳ x*y≈y*x 
      x * y * (x ^ m * y ^ n)    ≈⟨ *-assoc x y _ 
      x * (y * (x ^ m * y ^ n))  ≈⟨ *-congˡ (helper m n) 
      x * (x ^ m * y ^ suc n)    ≈˘⟨ *-assoc x (x ^ m) (y ^ suc n) 
      (x * x ^ m) * y ^ suc n    ≡⟨⟩
      x ^ suc m * y ^ suc n