From a6e80ba21b24108d7322696867b8bf8e4e2d6996 Mon Sep 17 00:00:00 2001 From: = Date: Mon, 9 Nov 2020 12:03:40 +0800 Subject: [PATCH 1/2] Deprecate `Algebra.Operations.CommutativeMonoid` --- CHANGELOG.md | 24 ++++ src/Algebra/Operations/CommutativeMonoid.agda | 99 ++-------------- src/Algebra/Properties/CommutativeMonoid.agda | 90 ++++++++++----- .../CommutativeMonoid/Summation.agda | 107 +++++++++++++++++ .../Properties/Monoid/Multiplication.agda | 109 ++++++++++++++++++ src/Algebra/Properties/Monoid/Summation.agda | 72 ++++++++++++ src/Data/Vec/Functional.agda | 2 +- .../Relation/Binary/Equality/Setoid.agda | 71 ++++++++++++ 8 files changed, 455 insertions(+), 119 deletions(-) create mode 100644 src/Algebra/Properties/CommutativeMonoid/Summation.agda create mode 100644 src/Algebra/Properties/Monoid/Multiplication.agda create mode 100644 src/Algebra/Properties/Monoid/Summation.agda create mode 100644 src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 161ba48eca..cfa5b7e39b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -41,6 +41,14 @@ Deprecated modules complete. The new definitions are parameterised by raw bundles instead of bundles meaning they are much more flexible to work with. +* The module `Algebra.Operations.CommutativeMonoid` has been deprecated. The definition + of multiplication and the associated properties have been moved to + `Algebra.Properties.CommutativeMonoid.Multiplication`. The definition of summation + which was defined over the deprecated `Data.Table` has been redefined in terms of + `Data.Vec.Functional` and been moved to `Algbra.Properties.CommutativeMonoid.Summation`. + The properties of summation in `Algebra.Properties.CommutativeMonoid` have likewise + been deprecated and moved to `Algebra.Properties.CommutativeMonoid.Summation`. + Deprecated names ---------------- @@ -90,6 +98,22 @@ New modules Algebra.Properties.CommutativeSemigroup.Divisibility ``` +* Generic summations over algebraic structures + ``` + Algebra.Properties.Monoid.Summation + Algebra.Properties.CommutativeMonoid.Summation + ``` + +* Generic multiplication over algebraic structures + ``` + Algebra.Properties.Monoid.Multiplication + ``` + +* Setoid equality over vectors: + ``` + Data.Vec.Functional.Relation.Binary.Equality.Setoid + ``` + Other major changes ------------------- diff --git a/src/Algebra/Operations/CommutativeMonoid.agda b/src/Algebra/Operations/CommutativeMonoid.agda index aeb1fccfb1..b0c8421cd9 100644 --- a/src/Algebra/Operations/CommutativeMonoid.agda +++ b/src/Algebra/Operations/CommutativeMonoid.agda @@ -1,8 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Some defined operations (multiplication by natural number and --- exponentiation) +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -11,51 +10,26 @@ {-# OPTIONS --warn=noUserWarning #-} open import Algebra +open import Data.List.Base as List using (List; []; _∷_; _++_) +open import Data.Fin.Base using (Fin; zero) +open import Data.Table.Base as Table using (Table) +open import Function using (_∘_) +open import Relation.Binary.PropositionalEquality as P using (_≡_) module Algebra.Operations.CommutativeMonoid {s₁ s₂} (CM : CommutativeMonoid s₁ s₂) where -open import Data.Nat.Base using (ℕ; zero; suc) - renaming (_+_ to _ℕ+_; _*_ to _ℕ*_) -open import Data.List.Base as List using (List; []; _∷_; _++_) -open import Data.Fin.Base using (Fin; zero) -open import Data.Product using (proj₁; proj₂) -open import Data.Table.Base as Table using (Table) -open import Function using (_∘_; _⟨_⟩_) -open import Relation.Binary -open import Relation.Binary.PropositionalEquality as P using (_≡_) +{-# WARNING_ON_IMPORT +"Algebra.Operations.CommutativeMonoid was deprecated in v1.5. +Use Algebra.Properties.CommutativeMonoid.(Summation/Multiplication) instead." +#-} open CommutativeMonoid CM renaming ( _∙_ to _+_ - ; ∙-cong to +-cong - ; identityˡ to +-identityˡ - ; identityʳ to +-identityʳ - ; assoc to +-assoc - ; comm to +-comm ; ε to 0# ) -open import Relation.Binary.Reasoning.Setoid setoid - ------------------------------------------------------------------------- --- Operations - --- Multiplication by natural number. - -infixr 8 _×_ _×′_ - -_×_ : ℕ → Carrier → Carrier -0 × x = 0# -suc n × x = x + n × x - --- A variant that includes a "redundant" case which ensures that `1 × x` --- is definitionally equal to `x`. - -_×′_ : ℕ → Carrier → Carrier -0 ×′ x = 0# -1 ×′ x = x -suc n ×′ x = x + n ×′ x -- Summation over lists/tables @@ -75,55 +49,6 @@ sumₜ-syntax _ = sumₜ ∘ Table.tabulate syntax sumₜ-syntax n (λ i → x) = ∑[ i < n ] x ------------------------------------------------------------------------ --- Properties of _×_ - -×-congʳ : ∀ n → (n ×_) Preserves _≈_ ⟶ _≈_ -×-congʳ 0 x≈x′ = refl -×-congʳ (suc n) x≈x′ = x≈x′ ⟨ +-cong ⟩ ×-congʳ n x≈x′ - -×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_ -×-cong {u} P.refl x≈x′ = ×-congʳ u x≈x′ - --- _×_ is homomorphic with respect to _ℕ+_/_+_. - -×-homo-+ : ∀ c m n → (m ℕ+ n) × c ≈ m × c + n × c -×-homo-+ c 0 n = sym (+-identityˡ (n × c)) -×-homo-+ c (suc m) n = begin - c + (m ℕ+ n) × c ≈⟨ +-cong refl (×-homo-+ c m n) ⟩ - c + (m × c + n × c) ≈⟨ sym (+-assoc c (m × c) (n × c)) ⟩ - c + m × c + n × c ∎ - ------------------------------------------------------------------------- --- Properties of _×′_ - -1+×′ : ∀ n x → suc n ×′ x ≈ x + n ×′ x -1+×′ 0 x = sym (+-identityʳ x) -1+×′ (suc n) x = refl - --- _×_ and _×′_ are extensionally equal (up to the setoid --- equivalence). - -×≈×′ : ∀ n x → n × x ≈ n ×′ x -×≈×′ 0 x = begin 0# ∎ -×≈×′ (suc n) x = begin - x + n × x ≈⟨ +-cong refl (×≈×′ n x) ⟩ - x + n ×′ x ≈⟨ sym (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 ≈⟨ sym (×≈×′ (m ℕ+ n) c) ⟩ - (m ℕ+ n) × c ≈⟨ ×-homo-+ c m n ⟩ - m × c + n × c ≈⟨ +-cong (×≈×′ m c) (×≈×′ n c) ⟩ - m ×′ c + n ×′ c ∎ - --- _×′_ preserves equality. +-- Operations -×′-cong : _×′_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_ -×′-cong {n} {_} {x} {y} P.refl x≈y = begin - n ×′ x ≈⟨ sym (×≈×′ n x) ⟩ - n × x ≈⟨ ×-congʳ n x≈y ⟩ - n × y ≈⟨ ×≈×′ n y ⟩ - n ×′ y ∎ +open import Algebra.Properties.Monoid.Multiplication public diff --git a/src/Algebra/Properties/CommutativeMonoid.agda b/src/Algebra/Properties/CommutativeMonoid.agda index 19dafdcdd0..1c6b19c27f 100644 --- a/src/Algebra/Properties/CommutativeMonoid.agda +++ b/src/Algebra/Properties/CommutativeMonoid.agda @@ -52,41 +52,35 @@ open CommutativeMonoid M open import Algebra.Definitions _≈_ open import Relation.Binary.Reasoning.Setoid setoid -module _ {n} where - open B.Setoid (TE.setoid setoid n) public - using () - renaming (_≈_ to _≋_) --- When summing over a function from a finite set, we can pull out any value and move it to the front. -sumₜ-remove : ∀ {n} {i : Fin (suc n)} t → sumₜ t ≈ lookup t i + sumₜ (remove i t) -sumₜ-remove {_} {zero} t = refl -sumₜ-remove {suc n} {suc i} t′ = - begin - t₀ + ∑t ≈⟨ +-congˡ (sumₜ-remove t) ⟩ - t₀ + (tᵢ + ∑t′) ≈⟨ solve 3 (λ x y z → x ⊕ (y ⊕ z) ⊜ y ⊕ (x ⊕ z)) refl t₀ tᵢ ∑t′ ⟩ - tᵢ + (t₀ + ∑t′) ∎ - where - t = tail t′ - t₀ = head t′ - tᵢ = lookup t i - ∑t = sumₜ t - ∑t′ = sumₜ (remove i t) +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +module _ {n} where + open B.Setoid (TE.setoid setoid n) public + using () renaming (_≈_ to _≋_) --- '_≈_' is a congruence over 'sumTable n'. +-- Version 1.5 sumₜ-cong-≈ : ∀ {n} → sumₜ {n} Preserves _≋_ ⟶ _≈_ sumₜ-cong-≈ {zero} p = refl sumₜ-cong-≈ {suc n} p = +-cong (p _) (sumₜ-cong-≈ (p ∘ suc)) - --- '_≡_' is a congruence over 'sum n'. +{-# WARNING_ON_USAGE sumₜ-cong-≈ +"Warning: sumₜ-cong-≈ was deprecated in v1.5. +Please use sum-cong-≋ from `Algebra.Properties.CommutativeMonoid.Summation` instead." +#-} sumₜ-cong-≡ : ∀ {n} → sumₜ {n} Preserves _≗_ ⟶ _≡_ sumₜ-cong-≡ {zero} p = P.refl sumₜ-cong-≡ {suc n} p = P.cong₂ _+_ (p _) (sumₜ-cong-≡ (p ∘ suc)) - --- If addition is idempotent on a particular value 'x', then summing over a --- nonzero number of copies of 'x' gives back 'x'. +{-# WARNING_ON_USAGE sumₜ-cong-≡ +"Warning: sumₜ-cong-≡ was deprecated in v1.5. +Please use sum-cong-≗ from `Algebra.Properties.CommutativeMonoid.Summation` instead." +#-} sumₜ-idem-replicate : ∀ n {x} → _+_ IdempotentOn x → sumₜ (replicate {n = suc n} x) ≈ x sumₜ-idem-replicate zero idem = +-identityʳ _ @@ -95,16 +89,38 @@ sumₜ-idem-replicate (suc n) {x} idem = begin (x + x) + sumₜ (replicate {n = n} x) ≈⟨ +-congʳ idem ⟩ x + sumₜ (replicate {n = n} x) ≈⟨ sumₜ-idem-replicate n idem ⟩ x ∎ - --- The sum over the constantly zero function is zero. +{-# WARNING_ON_USAGE sumₜ-idem-replicate +"Warning: sumₜ-idem-replicate was deprecated in v1.5. +Please use sum-replicate-idem from `Algebra.Properties.CommutativeMonoid.Summation` instead." +#-} sumₜ-zero : ∀ n → sumₜ (replicate {n = n} 0#) ≈ 0# sumₜ-zero n = begin sumₜ (replicate {n = n} 0#) ≈⟨ sym (+-identityˡ _) ⟩ 0# + sumₜ (replicate {n = n} 0#) ≈⟨ sumₜ-idem-replicate n (+-identityˡ 0#) ⟩ 0# ∎ +{-# WARNING_ON_USAGE sumₜ-zero +"Warning: sumₜ-zero was deprecated in v1.5. +Please use sum-replicate-zero from `Algebra.Properties.CommutativeMonoid.Summation` instead." +#-} --- The '∑' operator distributes over addition. +sumₜ-remove : ∀ {n} {i : Fin (suc n)} t → sumₜ t ≈ lookup t i + sumₜ (remove i t) +sumₜ-remove {_} {zero} t = refl +sumₜ-remove {suc n} {suc i} t′ = + begin + t₀ + ∑t ≈⟨ +-congˡ (sumₜ-remove t) ⟩ + t₀ + (tᵢ + ∑t′) ≈⟨ solve 3 (λ x y z → x ⊕ (y ⊕ z) ⊜ y ⊕ (x ⊕ z)) refl t₀ tᵢ ∑t′ ⟩ + tᵢ + (t₀ + ∑t′) ∎ + where + t = tail t′ + t₀ = head t′ + tᵢ = lookup t i + ∑t = sumₜ t + ∑t′ = sumₜ (remove i t) +{-# WARNING_ON_USAGE sumₜ-remove +"Warning: sumₜ-remove was deprecated in v1.5. +Please use sum-remove from `Algebra.Properties.CommutativeMonoid.Summation` instead." +#-} ∑-distrib-+ : ∀ n (f g : Fin n → Carrier) → ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i ∑-distrib-+ zero f g = sym (+-identityˡ _) @@ -119,8 +135,10 @@ sumₜ-zero n = begin ∑f = ∑[ i < n ] f (suc i) ∑g = ∑[ i < n ] g (suc i) ∑fg = ∑[ i < n ] (f (suc i) + g (suc i)) - --- The '∑' operator commutes with itself. +{-# WARNING_ON_USAGE ∑-distrib-+ +"Warning: ∑-distrib-+ was deprecated in v1.5. +Please use ∑-distrib-+ from `Algebra.Properties.CommutativeMonoid.Summation` instead." +#-} ∑-comm : ∀ n m (f : Fin n → Fin m → Carrier) → ∑[ i < n ] ∑[ j < m ] f i j ≈ ∑[ j < m ] ∑[ i < n ] f i j ∑-comm zero m f = sym (sumₜ-zero m) @@ -128,8 +146,10 @@ sumₜ-zero n = begin ∑[ j < m ] f zero j + ∑[ i < n ] ∑[ j < m ] f (suc i) j ≈⟨ +-congˡ (∑-comm n m _) ⟩ ∑[ j < m ] f zero j + ∑[ j < m ] ∑[ i < n ] f (suc i) j ≈⟨ sym (∑-distrib-+ m _ _) ⟩ ∑[ j < m ] (f zero j + ∑[ i < n ] f (suc i) j) ∎ - --- Any permutation of a table has the same sum as the original. +{-# WARNING_ON_USAGE ∑-distrib-+ +"Warning: ∑-comm was deprecated in v1.5. +Please use ∑-comm from `Algebra.Properties.CommutativeMonoid.Summation` instead." +#-} sumₜ-permute : ∀ {m n} t (π : Permutation m n) → sumₜ t ≈ sumₜ (permute π t) sumₜ-permute {zero} {zero} t π = refl @@ -145,9 +165,17 @@ sumₜ-permute {suc m} {suc n} t π = begin where 0i = zero πt = permute π t +{-# WARNING_ON_USAGE sumₜ-permute +"Warning: sumₜ-permute was deprecated in v1.5. +Please use sum-permute from `Algebra.Properties.CommutativeMonoid.Summation` instead." +#-} ∑-permute : ∀ {m n} f (π : Permutation m n) → ∑[ i < n ] f i ≈ ∑[ i < m ] f (π ⟨$⟩ʳ i) ∑-permute = sumₜ-permute ∘ tabulate +{-# WARNING_ON_USAGE ∑-permute +"Warning: ∑-permute was deprecated in v1.5. +Please use ∑-permute from `Algebra.Properties.CommutativeMonoid.Summation` instead." +#-} -- If the function takes the same value at 'i' and 'j', then transposing 'i' and -- 'j' then selecting 'j' is the same as selecting 'i'. diff --git a/src/Algebra/Properties/CommutativeMonoid/Summation.agda b/src/Algebra/Properties/CommutativeMonoid/Summation.agda new file mode 100644 index 0000000000..aa06a0bfce --- /dev/null +++ b/src/Algebra/Properties/CommutativeMonoid/Summation.agda @@ -0,0 +1,107 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Finite summations over a commutative monoid +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Bundles using (CommutativeMonoid) +open import Data.Bool.Base using (Bool; true; false) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero) +open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Fin.Permutation as Perm using (Permutation; _⟨$⟩ˡ_; _⟨$⟩ʳ_) +open import Data.Fin.Patterns using (0F) +open import Data.Vec.Functional +open import Function.Base using (_∘_) +open import Function.Equality using (_⟨$⟩_) +open import Relation.Binary.PropositionalEquality as P using (_≡_) +open import Relation.Nullary.Negation using (contradiction) + +module Algebra.Properties.CommutativeMonoid.Summation + {a ℓ} (M : CommutativeMonoid a ℓ) where + +open CommutativeMonoid M + renaming + ( _∙_ to _+_ + ; ∙-cong to +-cong + ; ∙-congˡ to +-congˡ + ; identityˡ to +-identityˡ + ; identityʳ to +-identityʳ + ; assoc to +-assoc + ; ε to 0# + ) + +open import Algebra.Definitions _≈_ +open import Algebra.Solver.CommutativeMonoid M +open import Data.Vec.Functional.Relation.Binary.Equality.Setoid setoid +open import Relation.Binary.Reasoning.Setoid setoid + +------------------------------------------------------------------------ +-- Re-export summation over monoids + +open import Algebra.Properties.Monoid.Summation monoid public + +------------------------------------------------------------------------ +-- Properties + +-- When summing over a function from a finite set, we can pull out any +-- value and move it to the front. +sum-remove : ∀ {n} {i : Fin (suc n)} t → sum t ≈ t i + sum (remove i t) +sum-remove {_} {zero} xs = refl +sum-remove {suc n} {suc i} xs = begin + t₀ + ∑t ≈⟨ +-congˡ (sum-remove t) ⟩ + t₀ + (tᵢ + ∑t′) ≈⟨ solve 3 (λ x y z → x ⊕ (y ⊕ z) ⊜ y ⊕ (x ⊕ z)) refl t₀ tᵢ ∑t′ ⟩ + tᵢ + (t₀ + ∑t′) ∎ + where + t = tail xs + t₀ = head xs + tᵢ = t i + ∑t = sum t + ∑t′ = sum (remove i t) + +-- The '∑' operator distributes over addition. +∑-distrib-+ : ∀ {n} (f g : Vector Carrier n) → ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i +∑-distrib-+ {zero} f g = sym (+-identityˡ _) +∑-distrib-+ {suc n} f g = begin + f₀ + g₀ + ∑fg ≈⟨ +-assoc _ _ _ ⟩ + f₀ + (g₀ + ∑fg) ≈⟨ +-congˡ (+-congˡ (∑-distrib-+ (f ∘ suc) (g ∘ suc))) ⟩ + f₀ + (g₀ + (∑f + ∑g)) ≈⟨ solve 4 (λ a b c d → a ⊕ (c ⊕ (b ⊕ d)) ⊜ (a ⊕ b) ⊕ (c ⊕ d)) refl f₀ ∑f g₀ ∑g ⟩ + (f₀ + ∑f) + (g₀ + ∑g) ∎ + where + f₀ = f 0F + g₀ = g 0F + ∑f = ∑[ i < n ] f (suc i) + ∑g = ∑[ i < n ] g (suc i) + ∑fg = ∑[ i < n ] (f (suc i) + g (suc i)) + +-- The '∑' operator commutes with itself. +∑-comm : ∀ {m n} (f : Fin m → Fin n → Carrier) → + ∑[ i < m ] ∑[ j < n ] f i j ≈ ∑[ j < n ] ∑[ i < m ] f i j +∑-comm {zero} {n} f = sym (sum-replicate-zero n) +∑-comm {suc m} {n} f = begin + ∑[ j < n ] f zero j + ∑[ i < m ] ∑[ j < n ] f (suc i) j ≈⟨ +-congˡ (∑-comm (f ∘ suc)) ⟩ + ∑[ j < n ] f zero j + ∑[ j < n ] ∑[ i < m ] f (suc i) j ≈⟨ sym (∑-distrib-+ (f zero) _) ⟩ + ∑[ j < n ] (f zero j + ∑[ i < m ] f (suc i) j) ∎ + +-- Summation is insensitive to permutations of the input +sum-permute : ∀ {m n} f (π : Permutation m n) → sum f ≈ sum (rearrange (π ⟨$⟩ʳ_) f) +sum-permute {zero} {zero} f π = refl +sum-permute {zero} {suc n} f π = contradiction π (Perm.refute λ()) +sum-permute {suc m} {zero} f π = contradiction π (Perm.refute λ()) +sum-permute {suc m} {suc n} f π = begin + sum f ≡⟨⟩ + f 0F + sum f/0 ≡˘⟨ P.cong (_+ sum f/0) (P.cong f (Perm.inverseʳ π)) ⟩ + πf π₀ + sum f/0 ≈⟨ +-congˡ (sum-permute f/0 (Perm.remove π₀ π)) ⟩ + πf π₀ + sum (rearrange (π/0 ⟨$⟩ʳ_) f/0) ≡˘⟨ P.cong (πf π₀ +_) (sum-cong-≗ (P.cong f ∘ Perm.punchIn-permute′ π 0F)) ⟩ + πf π₀ + sum (remove π₀ πf) ≈⟨ sym (sum-remove πf) ⟩ + sum πf ∎ + where + f/0 = remove 0F f + π₀ = π ⟨$⟩ˡ 0F + π/0 = Perm.remove π₀ π + πf = rearrange (π ⟨$⟩ʳ_) f + +∑-permute : ∀ {m n} (f : Vector Carrier n) (π : Permutation m n) → + ∑[ i < n ] f i ≈ ∑[ i < m ] f (π ⟨$⟩ʳ i) +∑-permute f π = sum-permute f π diff --git a/src/Algebra/Properties/Monoid/Multiplication.agda b/src/Algebra/Properties/Monoid/Multiplication.agda new file mode 100644 index 0000000000..a6263bca78 --- /dev/null +++ b/src/Algebra/Properties/Monoid/Multiplication.agda @@ -0,0 +1,109 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Multiplication over a monoid (i.e. repeated addition) +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Bundles using (Monoid) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero) +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as P using (_≡_) + +module Algebra.Properties.Monoid.Multiplication {a ℓ} (M : Monoid a ℓ) where + +-- View of the monoid operator as an addition +open Monoid M + renaming + ( _∙_ to _+_ + ; ∙-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 + +-- Multiplication by natural number. + +infixr 8 _×_ _×′_ + +_×_ : ℕ → Carrier → Carrier +0 × x = 0# +suc n × x = x + (n × x) + +-- A variant that includes a "redundant" case which ensures that `1 × x` +-- is definitionally equal to `x`. + +_×′_ : ℕ → Carrier → Carrier +0 ×′ x = 0# +1 ×′ x = x +suc n ×′ x = x + n ×′ x + +------------------------------------------------------------------------ +-- 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 {u} P.refl x≈x′ = ×-congʳ u x≈x′ + +-- _×_ is homomorphic with respect to _ℕ+_/_+_. + +×-homo-+ : ∀ c m n → (m ℕ.+ n) × c ≈ m × c + n × c +×-homo-+ c 0 n = sym (+-identityˡ (n × c)) +×-homo-+ c (suc m) n = begin + c + (m ℕ.+ n) × c ≈⟨ +-cong refl (×-homo-+ c m n) ⟩ + c + (m × c + n × c) ≈⟨ sym (+-assoc c (m × c) (n × c)) ⟩ + c + m × c + n × c ∎ + +×-idem : ∀ {c} → _+_ IdempotentOn c → + ∀ n → .{{_ : NonZero n}} → n × c ≈ c +×-idem {c} idem (suc zero) = +-identityʳ c +×-idem {c} idem (suc (suc n)) = begin + c + (suc n × c) ≈⟨ ∙-congˡ (×-idem idem (suc n) ) ⟩ + c + c ≈⟨ idem ⟩ + c ∎ + +------------------------------------------------------------------------ +-- Properties of _×′_ + +1+×′ : ∀ n x → suc n ×′ x ≈ x + n ×′ x +1+×′ 0 x = sym (+-identityʳ x) +1+×′ (suc n) x = refl + +-- _×_ and _×′_ 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 refl (×≈×′ n x) ⟩ + x + n ×′ x ≈⟨ sym (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 ≈⟨ sym (×≈×′ (m ℕ.+ n) c) ⟩ + (m ℕ.+ n) × c ≈⟨ ×-homo-+ c m n ⟩ + m × c + n × c ≈⟨ +-cong (×≈×′ m c) (×≈×′ n c) ⟩ + m ×′ c + n ×′ c ∎ + +-- _×′_ preserves equality. + +×′-cong : _×′_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_ +×′-cong {n} {_} {x} {y} P.refl x≈y = begin + n ×′ x ≈⟨ sym (×≈×′ n x) ⟩ + n × x ≈⟨ ×-congʳ n x≈y ⟩ + n × y ≈⟨ ×≈×′ n y ⟩ + n ×′ y ∎ diff --git a/src/Algebra/Properties/Monoid/Summation.agda b/src/Algebra/Properties/Monoid/Summation.agda new file mode 100644 index 0000000000..aac92997e2 --- /dev/null +++ b/src/Algebra/Properties/Monoid/Summation.agda @@ -0,0 +1,72 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Finite summations over a monoid +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Bundles using (Monoid) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero) +open import Data.Vec.Functional as Vector +open import Data.Fin.Base using (zero; suc) +open import Data.Unit using (tt) +open import Function.Base using (_∘_) +open import Relation.Binary as B using (_Preserves_⟶_) +open import Relation.Binary.PropositionalEquality as P using (_≗_; _≡_) + +module Algebra.Properties.Monoid.Summation {a ℓ} (M : Monoid a ℓ) where + +open Monoid M + renaming + ( _∙_ to _+_ + ; ∙-cong to +-cong + ; ∙-congˡ to +-congˡ + ; identityˡ to +-identityˡ + ; identityʳ to +-identityʳ + ; assoc to +-assoc + ; ε to 0# + ) + +open import Data.Vec.Functional.Relation.Binary.Equality.Setoid setoid +open import Algebra.Properties.Monoid.Multiplication M +open import Algebra.Definitions _≈_ + +------------------------------------------------------------------------ +-- Definition + +sum : ∀ {n} → Vector Carrier n → Carrier +sum = Vector.foldr _+_ 0# + +------------------------------------------------------------------------ +-- An alternative mathematical-style syntax for sumₜ + +infixl 10 sum-syntax + +sum-syntax : ∀ n → Vector Carrier n → Carrier +sum-syntax _ = sum + +syntax sum-syntax n (λ i → x) = ∑[ i < n ] x + +------------------------------------------------------------------------ +-- Properties + +sum-cong-≋ : ∀ {n} → sum {n} Preserves _≋_ ⟶ _≈_ +sum-cong-≋ {zero} xs≋ys = refl +sum-cong-≋ {suc n} xs≋ys = +-cong (xs≋ys zero) (sum-cong-≋ (xs≋ys ∘ suc)) + +sum-cong-≗ : ∀ {n} → sum {n} Preserves _≗_ ⟶ _≡_ +sum-cong-≗ {zero} xs≗ys = P.refl +sum-cong-≗ {suc n} xs≗ys = P.cong₂ _+_ (xs≗ys zero) (sum-cong-≗ (xs≗ys ∘ suc)) + +sum-replicate : ∀ n {x} → sum {n} (replicate x) ≈ n × x +sum-replicate zero = refl +sum-replicate (suc n) = +-congˡ (sum-replicate n) + +sum-replicate-idem : ∀ {x} → _+_ IdempotentOn x → + ∀ n → .{{_ : NonZero n}} → sum {n} (replicate x) ≈ x +sum-replicate-idem idem n = trans (sum-replicate n) (×-idem idem n) + +sum-replicate-zero : ∀ n → sum {n} (replicate 0#) ≈ 0# +sum-replicate-zero zero = refl +sum-replicate-zero (suc n) = sum-replicate-idem (+-identityˡ 0#) (suc n) diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda index b0398c1fa3..45d5b06554 100644 --- a/src/Data/Vec/Functional.agda +++ b/src/Data/Vec/Functional.agda @@ -21,7 +21,7 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc) open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]) open import Data.Vec.Base as V using (Vec) -open import Function +open import Function.Base open import Level using (Level) infixr 5 _∷_ _++_ diff --git a/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda new file mode 100644 index 0000000000..f248ac57d1 --- /dev/null +++ b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda @@ -0,0 +1,71 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Pointwise lifting of relations over Vector +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Data.Fin.Base +open import Data.Nat.Base +open import Data.Vec.Functional as VF hiding (map) +open import Data.Vec.Functional.Relation.Binary.Pointwise + using (Pointwise) +import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as PW +open import Level using (Level) +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as P using (_≡_) + +module Data.Vec.Functional.Relation.Binary.Equality.Setoid + {a ℓ} (S : Setoid a ℓ) where + +open Setoid S renaming (Carrier to A) + +------------------------------------------------------------------------ +-- Definition +------------------------------------------------------------------------ + +_≋_ : ∀ {n} → Vector A n → Vector A n → Set ℓ +_≋_ = Pointwise _≈_ + +------------------------------------------------------------------------ +-- Relational properties +------------------------------------------------------------------------ + +≋-refl : ∀ {n} → Reflexive (_≋_ {n = n}) +≋-refl {n} = PW.refl {R = _≈_} refl + +≋-reflexive : ∀ {n} → _≡_ ⇒ (_≋_ {n = n}) +≋-reflexive P.refl = ≋-refl + +≋-sym : ∀ {n} → Symmetric (_≋_ {n = n}) +≋-sym = PW.sym {R = _≈_} sym + +≋-trans : ∀ {n} → Transitive (_≋_ {n = n}) +≋-trans = PW.trans {R = _≈_} trans + +≋-isEquivalence : ∀ n → IsEquivalence (_≋_ {n = n}) +≋-isEquivalence = PW.isEquivalence isEquivalence + +≋-setoid : ℕ → Setoid _ _ +≋-setoid = PW.setoid S + +------------------------------------------------------------------------ +-- Properties +------------------------------------------------------------------------ + +open PW public + using + ( map⁺ + ; head⁺; tail⁺ + ; ++⁺; ++⁻ˡ; ++⁻ʳ; ++⁻ + ; replicate⁺ + ; ⊛⁺ + ; zipWith⁺; zip⁺; zip⁻ + ) + +foldr-cong : ∀ {f g} → (∀ {w x y z} → w ≈ x → y ≈ z → f w y ≈ g x z) → + ∀ {d e : A} → d ≈ e → + ∀ {n} {xs ys : Vector A n} → xs ≋ ys → + foldr f d xs ≈ foldr g e ys +foldr-cong = PW.foldr-cong From 4696cb7810a7073040f74ded34a4f3be489e48ac Mon Sep 17 00:00:00 2001 From: = Date: Tue, 10 Nov 2020 10:42:59 +0800 Subject: [PATCH 2/2] Fixed deprecation warnings --- src/Algebra/Operations/CommutativeMonoid.agda | 2 +- src/Algebra/Operations/Semiring.agda | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Operations/CommutativeMonoid.agda b/src/Algebra/Operations/CommutativeMonoid.agda index b0c8421cd9..67e0905caa 100644 --- a/src/Algebra/Operations/CommutativeMonoid.agda +++ b/src/Algebra/Operations/CommutativeMonoid.agda @@ -51,4 +51,4 @@ syntax sumₜ-syntax n (λ i → x) = ∑[ i < n ] x ------------------------------------------------------------------------ -- Operations -open import Algebra.Properties.Monoid.Multiplication public +open import Algebra.Properties.Monoid.Multiplication monoid public diff --git a/src/Algebra/Operations/Semiring.agda b/src/Algebra/Operations/Semiring.agda index bb7c67a604..a3854852b3 100644 --- a/src/Algebra/Operations/Semiring.agda +++ b/src/Algebra/Operations/Semiring.agda @@ -7,6 +7,10 @@ {-# OPTIONS --without-K --safe #-} +-- Disabled to prevent warnings from deprecated +-- Algebra.Operations.CommutativeMonoid +{-# OPTIONS --warn=noUserWarning #-} + open import Algebra module Algebra.Operations.Semiring {s₁ s₂} (S : Semiring s₁ s₂) where