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

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

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

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

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 Algebra.Properties.Monoid.Mult M as U
  using () renaming (_×_ to _×ᵤ_)

open import Relation.Binary.Reasoning.Setoid setoid

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

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

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

1+× : ∀ n x → suc n × x ≈ x + n × x
1+×                x = sym (+-identityʳ x)
1+×                x = refl
1+× (suc n@(suc _)) x = begin
  (suc n × x) + x ≈⟨ +-congʳ (1+× n x) ⟩
  (x + n × x) + x ≈⟨ +-assoc x (n × x) x ⟩
  x + (n × x + x) ∎

-- The unoptimised (_×ᵤ_) and optimised (_×_) versions of multiplication
-- are extensionally equal (up to the setoid equivalence).

×ᵤ≈× : ∀ n x → n ×ᵤ x ≈ n × x
×ᵤ≈×        x = refl
×ᵤ≈× (suc n) x = begin
  x + n ×ᵤ x  ≈⟨ +-congˡ (×ᵤ≈× n x) ⟩
  x + n ×  x  ≈⟨ 1+× n x ⟨
  suc n ×  x  ∎

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

×-homo-+ : ∀ c m n → (m ℕ.+ n) × c ≈ m × c + n × c
×-homo-+ c m n = begin
  (m ℕ.+ n) ×  c   ≈⟨ ×ᵤ≈× (m ℕ.+ n) c ⟨
  (m ℕ.+ n) ×ᵤ c   ≈⟨ U.×-homo-+ c m n ⟩
  m ×ᵤ c + n ×ᵤ c  ≈⟨ +-cong (×ᵤ≈× m c) (×ᵤ≈× n c) ⟩
  m ×  c + n ×  c  ∎

-- _×_ preserves equality.

×-congʳ : ∀ n → (n ×_) Preserves _≈_ ⟶ _≈_
×-congʳ                x≈y = refl
×-congʳ                x≈y = x≈y
×-congʳ (suc n@(suc _)) x≈y = +-cong (×-congʳ n x≈y) x≈y

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

×-assocˡ : ∀ x m n → m × (n × x) ≈ (m ℕ.* n) × x
×-assocˡ x m n = begin
  m ×  (n ×  x)  ≈⟨ ×-congʳ m (×ᵤ≈× n x) ⟨
  m ×  (n ×ᵤ x)  ≈⟨ ×ᵤ≈× m (n ×ᵤ x) ⟨
  m ×ᵤ (n ×ᵤ x)  ≈⟨  U.×-assocˡ x m n ⟩
  (m ℕ.* n) ×ᵤ x ≈⟨  ×ᵤ≈× (m ℕ.* n) x ⟩
  (m ℕ.* n) ×  x ∎