------------------------------------------------------------------------
-- The Agda standard library
--
-- Some defined operations (multiplication by natural number and
-- exponentiation)
------------------------------------------------------------------------

open import Algebra

module Algebra.Operations {s₁ s₂} (S : Semiring s₁ s₂) where

open Semiring S renaming (zero to *-zero)
open import Data.Nat.Base
using (zero; suc; ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
open import Data.Product using (module Σ)
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
import Relation.Binary.EqReasoning as EqR
open EqR setoid

------------------------------------------------------------------------
-- Operations

-- Multiplication by natural number.

infixr 7 _×_ _×′_

_×_ :   Carrier  Carrier
0     × x = 0#
suc n × x = x + n × x

-- A variant that includes a "redundant" case which ensures that 1 × y
-- is definitionally equal to y.

_×′_ :   Carrier  Carrier
0     ×′ x = 0#
1     ×′ x = x
suc n ×′ x = x + n ×′ x

-- Exponentiation.

infixr 8 _^_

_^_ : Carrier    Carrier
x ^ zero  = 1#
x ^ suc n = x * x ^ n

------------------------------------------------------------------------
-- Some properties

-- Unfolding lemma for _×′_.

1+×′ :  n x  suc n ×′ x  x + n ×′ x
1+×′ 0 x = begin
x       ≈⟨ sym \$ Σ.proj₂ +-identity x
x + 0#
1+×′ (suc n) x = begin
x + suc n ×′ x  ≡⟨⟩
x + suc n ×′ x

-- _×_ and _×′_ are extensionally equal (up to the setoid
-- equivalence).

×≈×′ :  n x  n × x  n ×′ x
×≈×′ 0       x = begin 0#
×≈×′ (suc n) x = begin
x + n × x   ≈⟨ +-cong refl (×≈×′ n x)
x + n ×′ x  ≈⟨ sym \$ 1+×′ n x
suc n ×′ x

-- _×_ is homomorphic with respect to _ℕ+_/_+_.

×-homo-+ :  c m n  (m ℕ+ n) × c  m × c + n × c
×-homo-+ c 0 n = begin
n × c       ≈⟨ sym \$ Σ.proj₁ +-identity (n × c)
0# + n × c
×-homo-+ c (suc m) n = begin
c + (m ℕ+ n) × c     ≈⟨ +-cong refl (×-homo-+ c m n)
c + (m × c + n × c)  ≈⟨ sym \$ +-assoc c (m × c) (n × c)
c + m × c + n × c

-- _×′_ is homomorphic with respect to _ℕ+_/_+_.

×′-homo-+ :  c m n  (m ℕ+ n) ×′ c  m ×′ c + n ×′ c
×′-homo-+ c m n = begin
(m ℕ+ n) ×′ c    ≈⟨ sym \$ ×≈×′ (m ℕ+ n) c
(m ℕ+ n) ×  c    ≈⟨ ×-homo-+ c m n
m ×  c + n ×  c  ≈⟨ +-cong (×≈×′ m c) (×≈×′ n c)
m ×′ c + n ×′ c

-- _× 1# is homomorphic with respect to _ℕ*_/_*_.

×1-homo-* :  m n  (m ℕ* n) × 1#  (m × 1#) * (n × 1#)
×1-homo-* 0 n = begin
0#             ≈⟨ sym \$ Σ.proj₁ *-zero (n × 1#)
0# * (n × 1#)
×1-homo-* (suc m) n = begin
(n ℕ+ m ℕ* n) × 1#                   ≈⟨ ×-homo-+ 1# n (m ℕ* n)
n × 1# + (m ℕ* n) × 1#               ≈⟨ +-cong refl (×1-homo-* m n)
n × 1# + (m × 1#) * (n × 1#)         ≈⟨ sym \$ +-cong (Σ.proj₁ *-identity (n × 1#)) refl
1# * (n × 1#) + (m × 1#) * (n × 1#)  ≈⟨ sym \$ Σ.proj₂ distrib (n × 1#) 1# (m × 1#)
(1# + m × 1#) * (n × 1#)

-- _×′ 1# is homomorphic with respect to _ℕ*_/_*_.

×′1-homo-* :  m n  (m ℕ* n) ×′ 1#  (m ×′ 1#) * (n ×′ 1#)
×′1-homo-* m n = begin
(m ℕ* n) ×′ 1#         ≈⟨ sym \$ ×≈×′ (m ℕ* n) 1#
(m ℕ* n) ×  1#         ≈⟨ ×1-homo-* m n
(m ×  1#) * (n ×  1#)  ≈⟨ *-cong (×≈×′ m 1#) (×≈×′ n 1#)
(m ×′ 1#) * (n ×′ 1#)

-- _×_ preserves equality.

×-cong : _×_ Preserves₂ _≡_  _≈_  _≈_
×-cong {n} {n′} {x} {x′} n≡n′ x≈x′ = begin
n  × x   ≈⟨ reflexive \$ PropEq.cong  n  n × x) n≡n′
n′ × x   ≈⟨ ×-congʳ n′ x≈x′
n′ × x′
where
×-congʳ :  n  (_×_ n) Preserves _≈_  _≈_
×-congʳ 0       x≈x′ = refl
×-congʳ (suc n) x≈x′ = x≈x′  +-cong  ×-congʳ n x≈x′

-- _×′_ preserves equality.

×′-cong : _×′_ Preserves₂ _≡_  _≈_  _≈_
×′-cong {n} {n′} {x} {x′} n≡n′ x≈x′ = begin
n  ×′ x   ≈⟨ sym \$ ×≈×′ n x
n  ×  x   ≈⟨ ×-cong n≡n′ x≈x′
n′ ×  x′  ≈⟨ ×≈×′ n′ x′
n′ ×′ x′

-- _^_ preserves equality.

^-cong : _^_ Preserves₂ _≈_  _≡_  _≈_
^-cong {x} {x'} {n} {n'} x≈x' n≡n' = begin
x  ^ n   ≈⟨ reflexive \$ PropEq.cong (_^_ x) n≡n'
x  ^ n'  ≈⟨ ^-congˡ n' x≈x'
x' ^ n'
where
^-congˡ :  n   x  x ^ n) Preserves _≈_  _≈_
^-congˡ zero    x≈x' = refl
^-congˡ (suc n) x≈x' = x≈x'  *-cong  ^-congˡ n x≈x'