------------------------------------------------------------------------
-- 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+× 0 x = sym (+-identityʳ x)
1+× 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
×ᵤ≈× 0 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ʳ 0 x≈y = refl
×-congʳ 1 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 ∎
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4