------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic auxiliary definitions for monoid-like structures
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Algebra.Bundles using (RawMonoid)
 
module Algebra.Definitions.RawMonoid {a ℓ} (M : RawMonoid a ℓ) where
 
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
open import Data.Vec.Functional as Vector using (Vector)
open RawMonoid M renaming ( _∙_ to _+_ ; ε to 0# )
 
------------------------------------------------------------------------
-- Re-export definitions over a magma
------------------------------------------------------------------------
 
open import Algebra.Definitions.RawMagma rawMagma public
 
------------------------------------------------------------------------
-- Multiplication by natural number
------------------------------------------------------------------------
-- Standard definition
 
-- A simple definition, easy to use and prove properties about.
 
infixr  _×_
 
_×_ : ℕ → Carrier → Carrier
     × x = 0#
suc n × x = x + (n × x)
 
------------------------------------------------------------------------
-- Type-checking optimised definition
 
-- For use in code where high performance at type-checking time is
-- important, e.g. solvers and tactics. Firstly it avoids unnecessarily
-- multiplying by the unit if possible, speeding up type-checking and
-- makes for much more readable proofs:
--
--     Standard definition:  x * 2 = x + x + 0#
--     Optimised definition: x * 2 = x + x
--
-- Secondly, associates to the left which, counterintuitive as it may
-- seem, also speeds up typechecking.
--
--     Standard definition: x * 3 = x + (x + (x + 0#))
--     Our definition:      x * 3 = (x + x) + x
 
infixl  _×′_
 
_×′_ : ℕ → Carrier → Carrier
     ×′ x = 0#
     ×′ x = x
suc n ×′ x = n ×′ x + x
 
{-# INLINE _×′_ #-}
 
------------------------------------------------------------------------
-- Summation
------------------------------------------------------------------------
 
sum : ∀ {n} → Vector Carrier n → Carrier
sum = Vector.foldr _+_ 0#