------------------------------------------------------------------------ -- 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 ∎