------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite summations over a monoid
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (Monoid)
module Algebra.Properties.Monoid.Sum {a ℓ} (M : Monoid a ℓ) where
open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero)
open import Data.Vec.Functional as Vector using (Vector; replicate; init;
last; head; tail)
open import Data.Fin.Base using (zero; suc)
open import Function.Base using (_∘_)
open import Relation.Binary.Core using (_Preserves_⟶_)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≗_; _≡_)
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.Mult M
open import Algebra.Definitions _≈_
open import Relation.Binary.Reasoning.Setoid setoid
------------------------------------------------------------------------
-- Definition
open import Algebra.Definitions.RawMonoid rawMonoid public
using (sum)
------------------------------------------------------------------------
-- An alternative mathematical-style syntax for sumₜ
infixl 10 sum-syntax sum⁺-syntax
sum-syntax : ∀ n → Vector Carrier n → Carrier
sum-syntax _ = sum
syntax sum-syntax n (λ i → x) = ∑[ i < n ] x
sum⁺-syntax = sum-syntax ∘ suc
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 = ≡.refl
sum-cong-≗ {suc n} xs≗ys = ≡.cong₂ _+_ (xs≗ys zero) (sum-cong-≗ (xs≗ys ∘ suc))
sum-replicate : ∀ n {x} → sum (replicate n 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 (replicate n x) ≈ x
sum-replicate-idem idem n = trans (sum-replicate n) (×-idem idem n)
sum-replicate-zero : ∀ n → sum (replicate n 0#) ≈ 0#
sum-replicate-zero zero = refl
sum-replicate-zero (suc n) = sum-replicate-idem (+-identityˡ 0#) (suc n)
-- When summing over a `Vector`, we can pull out last element
sum-init-last : ∀ {n} (t : Vector Carrier (suc n)) → sum t ≈ sum (init t) + last t
sum-init-last {zero} t = begin
t₀ + 0# ≈⟨ +-identityʳ t₀ ⟩
t₀ ≈⟨ +-identityˡ t₀ ⟨
0# + t₀ ∎ where t₀ = t zero
sum-init-last {suc n} t = begin
t₀ + ∑t ≈⟨ +-congˡ (sum-init-last (tail t)) ⟩
t₀ + (∑t′ + tₗ) ≈⟨ +-assoc _ _ _ ⟨
(t₀ + ∑t′) + tₗ ∎
where
t₀ = head t
tₗ = last t
∑t = sum (tail t)
∑t′ = sum (tail (init t))
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