Skip to content

Use vec.functional for commutative monoids #1097

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed

Use vec.functional for commutative monoids #1097

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions src/Algebra/Operations/CommutativeMonoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ open import Data.Nat.Base using (ℕ; zero; suc)
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 Data.Vec.Functional as V
open import Function using (_∘_; _⟨_⟩_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
Expand Down Expand Up @@ -59,15 +59,15 @@ suc n ×′ x = x + n ×′ x
sumₗ : List Carrier → Carrier
sumₗ = List.foldr _+_ 0#

sumₜ : ∀ {n} → Table Carrier n → Carrier
sumₜ = Table.foldr _+_ 0#
sumₜ : ∀ {n} → Vector Carrier n → Carrier
sumₜ = V.foldr _+_ 0#

-- An alternative mathematical-style syntax for sumₜ

infixl 10 sumₜ-syntax

sumₜ-syntax : ∀ n → (Fin n → Carrier) → Carrier
sumₜ-syntax _ = sumₜ ∘ Table.tabulate
sumₜ-syntax _ = sumₜ

syntax sumₜ-syntax n (λ i → x) = ∑[ i < n ] x

Expand Down
46 changes: 24 additions & 22 deletions src/Algebra/Properties/CommutativeMonoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,11 @@ open import Data.List.Base as List using ([]; _∷_)
import Data.Fin.Properties as FP
open import Data.Fin.Permutation as Perm using (Permutation; Permutation′; _⟨$⟩ˡ_; _⟨$⟩ʳ_)
open import Data.Fin.Permutation.Components as PermC
open import Data.Table as Table
open import Data.Table.Relation.Binary.Equality as TE using (_≗_)
open import Data.Unit using (tt)
import Data.Table.Properties as TP
open import Data.Vec.Functional as VF
open import Data.Vec.Functional.Relation.Binary.Pointwise as VFP using ()
open import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as VFPP using (_≗_)
import Data.Vec.Functional.Properties as VProp
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary as Nullary using (¬_; does; _because_)
open import Relation.Nullary.Negation using (contradiction)
Expand All @@ -50,13 +51,14 @@ open import Algebra.Definitions _≈_
open import Relation.Binary.Reasoning.Setoid setoid

module _ {n} where
open B.Setoid (TE.setoid setoid n) public
open B.Setoid (VFPP.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 : ∀ {n} {i : Fin (suc n)} t → sumₜ t ≈ t i + sumₜ (remove i t)
sumₜ-remove {_} {zero} t = refl
sumₜ-remove {suc n} {suc i} t′ =
begin
Expand All @@ -66,7 +68,7 @@ sumₜ-remove {suc n} {suc i} t′ =
where
t = tail t′
t₀ = head t′
tᵢ = lookup t i
tᵢ = t i
∑t = sumₜ t
∑t′ = sumₜ (remove i t)

Expand Down Expand Up @@ -133,26 +135,26 @@ sumₜ-permute {zero} {zero} t π = refl
sumₜ-permute {zero} {suc n} t π = contradiction π (Perm.refute λ())
sumₜ-permute {suc m} {zero} t π = contradiction π (Perm.refute λ())
sumₜ-permute {suc m} {suc n} t π = begin
sumₜ t ≡⟨⟩
lookup t 0i + sumₜ (remove 0i t) ≡⟨ P.cong₂ _+_ (P.cong (lookup t) (P.sym (Perm.inverseʳ π))) P.refl ⟩
lookup πt (π ⟨$⟩ˡ 0i) + sumₜ (remove 0i t) ≈⟨ +-congˡ (sumₜ-permute (remove 0i t) (Perm.remove (π ⟨$⟩ˡ 0i) π)) ⟩
lookup πt (π ⟨$⟩ˡ 0i) + sumₜ (permute (Perm.remove (π ⟨$⟩ˡ 0i) π) (remove 0i t)) ≡⟨ P.cong₂ _+_ P.refl (sumₜ-cong-≡ (P.sym ∘ TP.remove-permute π 0i t)) ⟩
lookup πt (π ⟨$⟩ˡ 0i) + sumₜ (remove (π ⟨$⟩ˡ 0i) πt) ≈⟨ sym (sumₜ-remove (permute π t)) ⟩
sumₜ t ≡⟨⟩
t 0i + sumₜ (remove 0i t) ≡⟨ P.cong₂ _+_ (P.cong t (P.sym (Perm.inverseʳ π))) P.refl ⟩
πt (π ⟨$⟩ˡ 0i) + sumₜ (remove 0i t) ≈⟨ +-congˡ (sumₜ-permute (remove 0i t) (Perm.remove (π ⟨$⟩ˡ 0i) π)) ⟩
πt (π ⟨$⟩ˡ 0i) + sumₜ (permute (Perm.remove (π ⟨$⟩ˡ 0i) π) (remove 0i t)) ≡⟨ P.cong₂ _+_ P.refl (sumₜ-cong-≡ (P.sym ∘ VProp.remove-permute π 0i t)) ⟩
πt (π ⟨$⟩ˡ 0i) + sumₜ (remove (π ⟨$⟩ˡ 0i) πt) ≈⟨ sym (sumₜ-remove (permute π t)) ⟩
sumₜ πt ∎
where
0i = zero
πt = permute π t

∑-permute : ∀ {m n} f (π : Permutation m n) → ∑[ i < n ] f i ≈ ∑[ i < m ] f (π ⟨$⟩ʳ i)
∑-permute = sumₜ-permute ∘ tabulate
∑-permute = sumₜ-permute -- ∘ tabulate

-- 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'.

select-transpose :
∀ {n} t (i j : Fin n) → lookup t i ≈ lookup t j →
∀ k → (lookup (select 0# j t) ∘ PermC.transpose i j) k
≈ lookup (select 0# i t) k
∀ {n} t (i j : Fin n) → t i ≈ t j →
∀ k → (select 0# j t ∘ PermC.transpose i j) k
≈ select 0# i t k
select-transpose _ i j e k with k FP.≟ i
... | true because _ rewrite dec-true (j FP.≟ j) P.refl = sym e
... | false because [k≢i] with k FP.≟ j
Expand All @@ -163,13 +165,13 @@ select-transpose _ i j e k with k FP.≟ i

-- Summing over a pulse gives you the single value picked out by the pulse.

sumₜ-select : ∀ {n i} (t : Table Carrier n) → sumₜ (select 0# i t) ≈ lookup t i
sumₜ-select : ∀ {n i} (t : Vector Carrier n) → sumₜ (select 0# i t) ≈ t i
sumₜ-select {suc n} {i} t = begin
sumₜ (select 0# i t) ≈⟨ sumₜ-remove {i = i} (select 0# i t) ⟩
lookup (select 0# i t) i + sumₜ (remove i (select 0# i t)) ≡⟨ P.cong₂ _+_ (TP.select-lookup t) (sumₜ-cong-≡ (TP.select-remove i t)) ⟩
lookup t i + sumₜ (replicate {n = n} 0#) ≈⟨ +-congˡ (sumₜ-zero n) ⟩
lookup t i + 0# ≈⟨ +-identityʳ _ ⟩
lookup t i ∎
sumₜ (select 0# i t) ≈⟨ sumₜ-remove {i = i} (select 0# i t) ⟩
select 0# i t i + sumₜ (remove i (select 0# i t)) ≡⟨ P.cong₂ _+_ (VProp.select-lookup t) (sumₜ-cong-≡ (VProp.select-remove i t)) ⟩
t i + sumₜ (replicate {n = n} 0#) ≈⟨ +-congˡ (sumₜ-zero n) ⟩
t i + 0# ≈⟨ +-identityʳ _ ⟩
t i ∎

-- Converting to a table then summing is the same as summing the original list

Expand All @@ -179,6 +181,6 @@ sumₜ-fromList (x ∷ xs) = P.cong (_ +_) (sumₜ-fromList xs)

-- Converting to a list then summing is the same as summing the original table

sumₜ-toList : ∀ {n} (t : Table Carrier n) → sumₜ t ≡ sumₗ (toList t)
sumₜ-toList : ∀ {n} (t : Vector Carrier n) → sumₜ t ≡ sumₗ (toList t)
sumₜ-toList {zero} _ = P.refl
sumₜ-toList {suc n} _ = P.cong (_ +_) (sumₜ-toList {n} _)
114 changes: 20 additions & 94 deletions src/Data/Vec/Functional.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,107 +4,33 @@
-- Vectors defined as functions from a finite set to a type.
------------------------------------------------------------------------

-- This implementation is designed for reasoning about fixed-size
-- vectors where ease of retrieval of elements is prioritised.

-- See `Data.Vec` for an alternative implementation using inductive
-- data-types, which is more suitable for reasoning about vectors that
-- will grow or shrink in size.

{-# OPTIONS --without-K --safe #-}

module Data.Vec.Functional where

open import Data.Fin.Base using (Fin; zero; suc; splitAt; punchIn)
open import Data.List.Base as L using (List)
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec.Base as V using (Vec)
open import Function
open import Level using (Level)

infixr 5 _∷_ _++_
infixl 4 _⊛_

private
variable
a b c : Level
A : Set a
B : Set b
C : Set c

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

Vector : Set a → ℕ → Set a
Vector A n = Fin n → A

------------------------------------------------------------------------
-- Conversion

toVec : ∀ {n} → Vector A n → Vec A n
toVec = V.tabulate

fromVec : ∀ {n} → Vec A n → Vector A n
fromVec = V.lookup

toList : ∀ {n} → Vector A n → List A
toList = L.tabulate

fromList : ∀ (xs : List A) → Vector A (L.length xs)
fromList = L.lookup

------------------------------------------------------------------------
-- Construction and deconstruction

[] : Vector A zero
[] ()

_∷_ : ∀ {n} → A → Vector A n → Vector A (suc n)
(x ∷ xs) zero = x
(x ∷ xs) (suc i) = xs i

head : ∀ {n} → Vector A (suc n) → A
head xs = xs zero

tail : ∀ {n} → Vector A (suc n) → Vector A n
tail xs = xs ∘ suc

uncons : ∀ {n} → Vector A (suc n) → A × Vector A n
uncons xs = head xs , tail xs

replicate : ∀ {n} → A → Vector A n
replicate = const

remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n
remove i t = t ∘ punchIn i

------------------------------------------------------------------------
-- Transformations

map : (A → B) → ∀ {n} → Vector A n → Vector B n
map f xs = f ∘ xs

_++_ : ∀ {m n} → Vector A m → Vector A n → Vector A (m + n)
_++_ {m = m} xs ys i = [ xs , ys ] (splitAt m i)
open import Data.Vec.Functional.Base public

foldr : (A → B → B) → B → ∀ {n} → Vector A n → B
foldr f z {n = zero} xs = z
foldr f z {n = suc n} xs = f (head xs) (foldr f z (tail xs))
open import Data.Bool.Base using (true; false)
open import Data.Fin using (Fin; _≟_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (Inverse; _↔_)
open import Relation.Nullary using (does)
open import Relation.Nullary.Decidable using (⌊_⌋)

foldl : (B → A → B) → B → ∀ {n} → Vector A n → B
foldl f z {n = zero} xs = z
foldl f z {n = suc n} xs = foldl f (f z (head xs)) (tail xs)
--------------------------------------------------------------------------------
-- Combinators
--------------------------------------------------------------------------------

rearrange : ∀ {m n} → (Fin m → Fin n) → Vector A n → Vector A m
rearrange r xs = xs ∘ r
-- Changes the order of elements in the table according to a permutation (i.e.
-- an 'Inverse' object on the indices).

_⊛_ : ∀ {n} → Vector (A → B) n → Vector A n → Vector B n
_⊛_ = _ˢ_
permute : ∀ {m n a} {A : Set a} → Fin m ↔ Fin n → Vector A n → Vector A m
permute π = rearrange (Inverse.to π ⟨$⟩_)

zipWith : (A → B → C) → ∀ {n} → Vector A n → Vector B n → Vector C n
zipWith f xs ys i = f (xs i) (ys i)
-- The result of 'select z i t' takes the value of 'lookup t i' at index 'i',
-- and 'z' everywhere else.

zip : ∀ {n} → Vector A n → Vector B n → Vector (A × B) n
zip = zipWith _,_
select : ∀ {n} {a} {A : Set a} → A → Fin n → Vector A n → Vector A n
select z i t j with does (j ≟ i)
... | true = t i
... | false = z
110 changes: 110 additions & 0 deletions src/Data/Vec/Functional/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,110 @@
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors defined as functions from a finite set to a type.
------------------------------------------------------------------------

-- This implementation is designed for reasoning about fixed-size
-- vectors where ease of retrieval of elements is prioritised.

-- See `Data.Vec` for an alternative implementation using inductive
-- data-types, which is more suitable for reasoning about vectors that
-- will grow or shrink in size.

{-# OPTIONS --without-K --safe #-}

module Data.Vec.Functional.Base where

open import Data.Fin.Base using (Fin; zero; suc; splitAt; punchIn)
open import Data.List.Base as L using (List)
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec.Base as V using (Vec)
open import Function
open import Level using (Level)

infixr 5 _∷_ _++_
infixl 4 _⊛_

private
variable
a b c : Level
A : Set a
B : Set b
C : Set c

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

Vector : Set a → ℕ → Set a
Vector A n = Fin n → A

------------------------------------------------------------------------
-- Conversion

toVec : ∀ {n} → Vector A n → Vec A n
toVec = V.tabulate

fromVec : ∀ {n} → Vec A n → Vector A n
fromVec = V.lookup

toList : ∀ {n} → Vector A n → List A
toList = L.tabulate

fromList : ∀ (xs : List A) → Vector A (L.length xs)
fromList = L.lookup

------------------------------------------------------------------------
-- Construction and deconstruction

[] : Vector A zero
[] ()

_∷_ : ∀ {n} → A → Vector A n → Vector A (suc n)
(x ∷ xs) zero = x
(x ∷ xs) (suc i) = xs i

head : ∀ {n} → Vector A (suc n) → A
head xs = xs zero

tail : ∀ {n} → Vector A (suc n) → Vector A n
tail xs = xs ∘ suc

uncons : ∀ {n} → Vector A (suc n) → A × Vector A n
uncons xs = head xs , tail xs

replicate : ∀ {n} → A → Vector A n
replicate = const

remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n
remove i t = t ∘ punchIn i

------------------------------------------------------------------------
-- Transformations

map : (A → B) → ∀ {n} → Vector A n → Vector B n
map f xs = f ∘ xs

_++_ : ∀ {m n} → Vector A m → Vector A n → Vector A (m + n)
_++_ {m = m} xs ys i = [ xs , ys ] (splitAt m i)

foldr : (A → B → B) → B → ∀ {n} → Vector A n → B
foldr f z {n = zero} xs = z
foldr f z {n = suc n} xs = f (head xs) (foldr f z (tail xs))

foldl : (B → A → B) → B → ∀ {n} → Vector A n → B
foldl f z {n = zero} xs = z
foldl f z {n = suc n} xs = foldl f (f z (head xs)) (tail xs)

rearrange : ∀ {m n} → (Fin m → Fin n) → Vector A n → Vector A m
rearrange r xs = xs ∘ r

_⊛_ : ∀ {n} → Vector (A → B) n → Vector A n → Vector B n
_⊛_ = _ˢ_

zipWith : (A → B → C) → ∀ {n} → Vector A n → Vector B n → Vector C n
zipWith f xs ys i = f (xs i) (ys i)

zip : ∀ {n} → Vector A n → Vector B n → Vector (A × B) n
zip = zipWith _,_
Loading