------------------------------------------------------------------------
-- The Agda standard library
--
-- Multiplication over a monoid (i.e. repeated addition)
------------------------------------------------------------------------

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

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

module Algebra.Properties.Monoid.Mult {a } (M : Monoid a ) where

-- View of the monoid operator as addition
open Monoid M
renaming
( _∙_       to _+_
; ∙-cong    to +-cong
; ∙-congʳ   to +-congʳ
; ∙-congˡ   to +-congˡ
; identityˡ to +-identityˡ
; identityʳ to +-identityʳ
; assoc     to +-assoc
; ε         to 0#
)

open import Relation.Binary.Reasoning.Setoid setoid

open import Algebra.Definitions _≈_

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

open import Algebra.Definitions.RawMonoid rawMonoid public
using (_×_)

------------------------------------------------------------------------
-- Properties of _×_

×-congʳ :  n  (n ×_) Preserves _≈_  _≈_
×-congʳ 0       x≈x′ = refl
×-congʳ (suc n) x≈x′ = +-cong x≈x′ (×-congʳ n x≈x′)

×-cong : _×_ Preserves₂ _≡_  _≈_  _≈_
×-cong {n} P.refl x≈x′ = ×-congʳ n x≈x′

×-congˡ :  {x}  ( x) Preserves _≡_  _≈_
×-congˡ m≡n = ×-cong m≡n refl

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

×-homo-+ :  x m n  (m ℕ.+ n) × x  m × x + n × x
×-homo-+ x 0       n = sym (+-identityˡ (n × x))
×-homo-+ x (suc m) n = begin
x + (m ℕ.+ n) × x    ≈⟨ +-cong refl (×-homo-+ x m n)
x + (m × x + n × x)  ≈⟨ sym (+-assoc x (m × x) (n × x))
x + m × x + n × x

×-idem :  {c}  _+_ IdempotentOn c
n  .{{_ : NonZero n}}  n × c  c
×-idem {c} idem (suc zero)    = +-identityʳ c
×-idem {c} idem (suc n@(suc _)) = begin
c + (n × c) ≈⟨ +-congˡ (×-idem idem n )
c + c       ≈⟨ idem
c

×-assocˡ :  x m n  m × (n × x)  (m ℕ.* n) × x
×-assocˡ x zero    n = refl
×-assocˡ x (suc m) n = begin
n × x + m × n × x     ≈⟨ +-congˡ (×-assocˡ x m n)
n × x + (m ℕ.* n) × x ≈˘⟨ ×-homo-+ x n (m ℕ.* n)
(suc m ℕ.* n) × x