diff options
| -rw-r--r-- | Data/Matrix/BaseChange.agda | 171 | ||||
| -rw-r--r-- | Data/Matrix/Cast.agda | 20 | ||||
| -rw-r--r-- | Data/Matrix/Category.agda | 13 | ||||
| -rw-r--r-- | Data/Matrix/Core.agda | 272 | ||||
| -rw-r--r-- | Data/Matrix/Dagger-2-Poset.agda | 7 | ||||
| -rw-r--r-- | Data/Matrix/Endofunctor.agda | 32 | ||||
| -rw-r--r-- | Data/Matrix/FreeSemimodule.agda | 2 | ||||
| -rw-r--r-- | Data/Matrix/Matrices.agda | 110 | ||||
| -rw-r--r-- | Data/Matrix/Monoid.agda | 5 | ||||
| -rw-r--r-- | Data/Matrix/Raw.agda | 320 | ||||
| -rw-r--r-- | Data/Matrix/SemiadditiveDagger.agda | 20 | ||||
| -rw-r--r-- | Data/Matrix/Transform.agda | 46 | ||||
| -rw-r--r-- | Data/Matrix/Vec.agda | 3 | ||||
| -rw-r--r-- | Data/Vector/Bifunctor.agda | 57 | ||||
| -rw-r--r-- | Data/Vector/Bisemimodule.agda | 2 | ||||
| -rw-r--r-- | Data/Vector/Core.agda | 129 | ||||
| -rw-r--r-- | Data/Vector/Endofunctor.agda | 68 | ||||
| -rw-r--r-- | Data/Vector/Endofunctor/Monoid.agda | 106 | ||||
| -rw-r--r-- | Data/Vector/Endofunctor/Setoid.agda | 81 | ||||
| -rw-r--r-- | Data/Vector/Monoid.agda | 12 | ||||
| -rw-r--r-- | Data/Vector/Raw.agda | 95 | ||||
| -rw-r--r-- | Data/Vector/Vec.agda | 15 |
22 files changed, 1160 insertions, 426 deletions
diff --git a/Data/Matrix/BaseChange.agda b/Data/Matrix/BaseChange.agda new file mode 100644 index 0000000..906d1dd --- /dev/null +++ b/Data/Matrix/BaseChange.agda @@ -0,0 +1,171 @@ +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Bundles using (Semiring) +open import Algebra.Morphism.Bundles using (SemiringHomomorphism) +open import Level using (Level) + +module Data.Matrix.BaseChange + {c ℓ : Level} + (R S : Semiring c ℓ) + (open Semiring using (rawSemiring)) + (f : SemiringHomomorphism (rawSemiring R) (rawSemiring S)) + where + +module R = Semiring R +module S = Semiring S + +import Data.Matrix.Category as MCat +import Data.Matrix.Core as MC +import Data.Matrix.Endofunctor as Endo +import Data.Matrix.Monoid as MM +import Data.Matrix.Raw as MR +import Data.Matrix.Transform as MT +import Data.Vec.Relation.Binary.Pointwise.Inductive as PW +import Data.Vector.Bisemimodule as VB +import Data.Vector.Core as VC +import Data.Vector.Endofunctor.Monoid as MonEndo +import Data.Vector.Endofunctor.Setoid as VecEndo +import Data.Vector.Monoid as VM +import Relation.Binary.PropositionalEquality as ≡ +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Categories.Functor using (Functor) +open import Category.Instance.Monoids using (MonoidHomomorphism; mk-⇒) +open import Data.Matrix.Category using (Mat) +open import Data.Matrix.Transform using (I) +open import Data.Nat using (ℕ) +open import Data.Vec using (map; []; _∷_; zipWith; replicate) +open import Data.Vec.Properties using (map-∘; map-replicate) +open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺) +open import Data.Vector.Core S.setoid using (_≊_) +open import Data.Vector.Core using (Vector) +open import Data.Vector.Monoid using (⟨ε⟩) +open import Data.Vector.Raw using (module Relation) +open import Function using (id; Func; _⟶ₛ_; _⟨$⟩_; _∘_) +open import Level using (0ℓ) + +open Func +open Functor +open MC using (Matrix) +open SemiringHomomorphism f +open ℕ +private module Mat {A B : ℕ} = Functor (Endo.Mat A B {c} {ℓ}) + +open MR hiding (map; Matrix) + +module MatR where + open MC R.setoid public + open MM R.+-monoid public + open MT R public + open MCat R using (_·_) public + +module MatS where + open MC S.setoid public + open MM S.+-monoid public + open MT S public + open MCat S using (_·_) public + +module VecR where + open VC R.setoid public + open VM R.+-monoid public + open VB R public + +module VecS where + open VC S.setoid public + open VM S.+-monoid public + open VB S public + +func : R.setoid ⟶ₛ S.setoid +func .to = ⟦_⟧ +func .cong = ⟦⟧-cong + +change + : {A B : ℕ} + → Matrix R.setoid A B + → Matrix S.setoid A B +change = to (Mat.₁ func) + +resp + : {A B : ℕ} + {M M′ : MatR.Matrix A B} + → M MatR.≋ M′ + → change M MatS.≋ change M′ +resp = cong (Mat.₁ func) + +opaque + unfolding I _ᵀ _∷ₕ_ Endo.mapₛ + ident : {A : ℕ} → change (I R) MatS.≋ I S {A} + ident {zero} = PW.[] + ident {suc A} = (1#-homo PW.∷ ⟨ε⟩-homo) PW.∷ map-⟨ε⟩∷ₕI + where + ⟨ε⟩-homo : (map ⟦_⟧) VecR.⟨ε⟩ ≊ VecS.⟨ε⟩ {A} + ⟨ε⟩-homo = MonoidHomomorphism.ε-homo (MonEndo.mapₘ A (mk-⇒ +-monoidHomomorphism)) + map-⟨ε⟩∷ₕI : map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ MatR.I) MatS.≋ VecS.⟨ε⟩ ∷ₕ MatS.I {A} + map-⟨ε⟩∷ₕI = begin + map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ MatR.I) ≡⟨ ≡.cong (λ h → map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ h)) MatR.Iᵀ ⟨ + map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ MatR.I ᵀ) ≡⟨ ≡.cong (map (map ⟦_⟧)) (∷ᵥ-ᵀ VecR.⟨ε⟩ MatR.I) ⟨ + map (map ⟦_⟧) ((VecR.⟨ε⟩ ∷ᵥ MatR.I) ᵀ) ≡⟨ Natural.α-ᵀ ⟦_⟧ (VecR.⟨ε⟩ ∷ᵥ MatR.I) ⟩ + map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ᵥ MatR.I) ᵀ ≡⟨⟩ + (map ⟦_⟧ VecR.⟨ε⟩ ∷ᵥ map (map ⟦_⟧) MatR.I) ᵀ ≡⟨ ∷ᵥ-ᵀ (map ⟦_⟧ VecR.⟨ε⟩) (map (map ⟦_⟧) MatR.I) ⟩ + map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ (map (map ⟦_⟧) MatR.I ᵀ) ≡⟨ ≡.cong (map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ_) (Natural.α-ᵀ ⟦_⟧ MatR.I) ⟨ + map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ map (map ⟦_⟧) (MatR.I ᵀ) ≡⟨ ≡.cong (λ h → map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ map (map ⟦_⟧) h) MatR.Iᵀ ⟩ + map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ map (map ⟦_⟧) MatR.I ≈⟨ MatS.∷ₕ-cong ⟨ε⟩-homo ident ⟩ + VecS.⟨ε⟩ ∷ₕ MatS.I ∎ + where + open ≈-Reasoning (MatS.Matrixₛ (suc A) A) + +opaque + unfolding VecR._∙_ + ⟦⟧-∙ : {n : ℕ} (V W : VecR.Vector n) → ⟦ V VecR.∙ W ⟧ S.≈ map ⟦_⟧ V VecS.∙ map ⟦_⟧ W + ⟦⟧-∙ {zero} [] [] = 0#-homo + ⟦⟧-∙ {suc n} (x ∷ V) (y ∷ W) = begin + ⟦ x VecR.R.* y VecR.R.+ V VecR.∙ W ⟧ ≈⟨ +-homo (x VecR.R.* y) (V VecR.∙ W) ⟩ + ⟦ x VecR.R.* y ⟧ S.+ ⟦ V VecR.∙ W ⟧ ≈⟨ S.+-cong (*-homo x y) (⟦⟧-∙ V W) ⟩ + ⟦ x ⟧ VecS.R.* ⟦ y ⟧ S.+ (map ⟦_⟧ V VecS.∙ map ⟦_⟧ W) ∎ + where + open ≈-Reasoning S.setoid + +opaque + unfolding VecR.⟨ε⟩ + ⟦⟧-⟨ε⟩ : {n : ℕ} → map ⟦_⟧ (VecR.⟨ε⟩ {n}) VecS.≊ VecS.⟨ε⟩ + ⟦⟧-⟨ε⟩ {n} = begin + map ⟦_⟧ (replicate n R.0#) ≡⟨ map-replicate ⟦_⟧ R.0# n ⟩ + replicate n ⟦ R.0# ⟧ ≈⟨ VecS.replicate-cong 0#-homo ⟩ + replicate n VecS.R.0# ∎ + where + open ≈-Reasoning (VecS.Vectorₛ n) + +opaque + unfolding MatR.[_]_ Endo.mapₛ + ⟦⟧-[-]- + : {n m : ℕ} + (V : VecR.Vector n) + (M : MatR.Matrix m n) + → map ⟦_⟧ (MatR.[ V ] M) VecS.≊ MatS.[ map ⟦_⟧ V ] (change M) + ⟦⟧-[-]- {n} {m} V M = begin + map ⟦_⟧ (map (V VecR.∙_) (M ᵀ)) ≡⟨ map-∘ ⟦_⟧ (V VecR.∙_) (M ᵀ) ⟨ + map (λ x → ⟦ V VecR.∙ x ⟧) (M ᵀ) ≈⟨ PW.map⁺ (λ {x y} ≈xy → S.trans (⟦⟧-cong (VecR.∙-cong VecR.≊.refl ≈xy)) (⟦⟧-∙ V y)) MatR.≋.refl ⟩ + map (λ x → map ⟦_⟧ V VecS.∙ map ⟦_⟧ x) (M ᵀ) ≡⟨ map-∘ ((map ⟦_⟧ V) VecS.∙_) (map ⟦_⟧) (M ᵀ) ⟩ + map ((map ⟦_⟧ V) VecS.∙_) (map (map ⟦_⟧) (M ᵀ)) ≡⟨ ≡.cong ( map ((map ⟦_⟧ V) VecS.∙_)) (Natural.α-ᵀ ⟦_⟧ M) ⟩ + map ((map ⟦_⟧ V) VecS.∙_) (map (map ⟦_⟧) M ᵀ) ∎ + where + open ≈-Reasoning (VecS.Vectorₛ m) + +opaque + unfolding Endo.mapₛ MatR.[_]_ + homo + : {X Y Z : ℕ} + {M : MatR.Matrix X Y} + {N : MatR.Matrix Y Z} + → change (N MatR.· M) MatS.≋ change N MatS.· change M + homo {X} {Y} {Z} {M} {[]} = PW.[] + homo {X} {Y} {suc Z} {M} {N₀ ∷ N} = ⟦⟧-[-]- N₀ M PW.∷ homo {X} {Y} {Z} {M} {N} + +ChangeBase : Functor (Mat R) (Mat S) +ChangeBase = record + { F₀ = id + ; F₁ = change + ; identity = ident + ; homomorphism = homo + ; F-resp-≈ = resp + } diff --git a/Data/Matrix/Cast.agda b/Data/Matrix/Cast.agda index a171c7a..43c50c8 100644 --- a/Data/Matrix/Cast.agda +++ b/Data/Matrix/Cast.agda @@ -7,12 +7,13 @@ module Data.Matrix.Cast {c ℓ : Level} (S : Setoid c ℓ) where module S = Setoid S -open import Data.Matrix.Core S using (Matrix; _∥_; _≑_; _∷ₕ_; []ᵥ; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥; head-∷-tailₕ; headₕ; tailₕ) +open import Data.Matrix.Raw using (_∥_; _≑_; _∷ₕ_; []ᵥ; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥; head-∷-tailₕ; headₕ; tailₕ) +open import Data.Matrix.Core S using (Matrix; _≋_) open import Data.Nat using (ℕ; _+_) open import Data.Nat.Properties using (suc-injective; +-assoc) -open import Data.Vec using (Vec; map) renaming (cast to castVec) +open import Data.Vec using (Vec; map; _++_) renaming (cast to castVec) open import Data.Vec.Properties using (++-assoc-eqFree) renaming (cast-is-id to castVec-is-id) -open import Data.Vector.Core S using (Vector; _++_) +open import Data.Vector.Core S using (Vector) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) open Vec @@ -23,30 +24,24 @@ private A B C D E F : ℕ opaque - unfolding Matrix Vector + + unfolding Matrix + cast₁ : .(A ≡ B) → Matrix A C → Matrix B C cast₁ eq = map (castVec eq) -opaque - unfolding Matrix cast₂ : .(B ≡ C) → Matrix A B → Matrix A C cast₂ eq [] = castVec eq [] cast₂ {B} {suc C} {A} eq (x ∷ M) = x ∷ cast₂ (suc-injective eq) M -opaque - unfolding cast₁ cast₁-is-id : .(eq : A ≡ A) (M : Matrix A B) → cast₁ eq M ≡ M cast₁-is-id _ [] = ≡.refl cast₁-is-id _ (M₀ ∷ M) = ≡.cong₂ _∷_ (castVec-is-id _ M₀) (cast₁-is-id _ M) -opaque - unfolding cast₂ cast₂-is-id : .(eq : B ≡ B) (M : Matrix A B) → cast₂ eq M ≡ M cast₂-is-id _ [] = ≡.refl cast₂-is-id eq (M₀ ∷ M) = ≡.cong (M₀ ∷_) (cast₂-is-id (suc-injective eq) M) -opaque - unfolding cast₂ cast₂-trans : .(eq₁ : B ≡ C) (eq₂ : C ≡ D) (M : Matrix A B) → cast₂ eq₂ (cast₂ eq₁ M) ≡ cast₂ (≡.trans eq₁ eq₂) M cast₂-trans {zero} {zero} {zero} {A} eq₁ eq₂ [] = ≡.refl cast₂-trans {suc B} {suc C} {suc D} {A} eq₁ eq₂ (M₀ ∷ M) = ≡.cong (M₀ ∷_) (cast₂-trans (suc-injective eq₁) (suc-injective eq₂) M) @@ -123,7 +118,6 @@ opaque open ≡-Reasoning opaque - unfolding Vector cast : .(A ≡ B) → Vector A → Vector B cast = castVec diff --git a/Data/Matrix/Category.agda b/Data/Matrix/Category.agda index 5a33440..b4b0f23 100644 --- a/Data/Matrix/Category.agda +++ b/Data/Matrix/Category.agda @@ -12,7 +12,8 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Categories.Category using (Category) open import Categories.Category.Helper using (categoryHelper) -open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; ≋-isEquiv; _ᵀ; -ᵀ-cong; _∷ₕ_; mapRows; _ᵀᵀ; module ≋; _∥_; _≑_) +open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; _ᵀᵀ; _∥_; _≑_; mapRows) +open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; ≋-isEquiv; ᵀ-cong; module ≋) open import Data.Matrix.Monoid R.+-monoid using (𝟎; _[+]_) open import Data.Matrix.Transform R using ([_]_; _[_]; -[-]-cong; [-]--cong; -[-]ᵀ; []-∙; [-]--∥; [++]-≑; I; Iᵀ; I[-]; map--[-]-I; [-]-𝟎; [⟨0⟩]-) open import Data.Nat using (ℕ) @@ -112,7 +113,7 @@ opaque opaque - unfolding Matrix + unfolding _≋_ ·-resp-≋ : {X X′ : Matrix n p} {Y Y′ : Matrix m n} → X ≋ X′ → Y ≋ Y′ → X · Y ≋ X′ · Y′ ·-resp-≋ ≋X ≋Y = PW.map⁺ (λ {_} {y} ≋V → [-]--cong ≋V ≋Y) ≋X @@ -128,7 +129,7 @@ opaque ·-Iˡ : {f : Matrix n m} → I · f ≋ f ·-Iˡ {A} {B} {f} = begin I · f ≡⟨ ·-·′ I f ⟩ - map (I [_]) (f ᵀ) ᵀ ≈⟨ -ᵀ-cong (PW.map⁺ (λ {x} ≊V → ≊.trans (I[-] x) ≊V) {xs = f ᵀ} ≋.refl) ⟩ + map (I [_]) (f ᵀ) ᵀ ≈⟨ ᵀ-cong (PW.map⁺ (λ {x} ≊V → ≊.trans (I[-] x) ≊V) {xs = f ᵀ} ≋.refl) ⟩ map id (f ᵀ) ᵀ ≡⟨ ≡.cong (_ᵀ) (map-id (f ᵀ)) ⟩ f ᵀ ᵀ ≡⟨ f ᵀᵀ ⟩ f ∎ @@ -138,8 +139,8 @@ opaque ·-Iʳ : {f : Matrix n m} → f · I ≋ f ·-Iʳ {A} {B} {f} = begin f · I ≡⟨ ·-·′ f I ⟩ - map (f [_]) (I ᵀ) ᵀ ≈⟨ -ᵀ-cong (≋.reflexive (≡.cong (map (f [_])) Iᵀ)) ⟩ - map (f [_]) I ᵀ ≈⟨ -ᵀ-cong (map--[-]-I f) ⟩ + map (f [_]) (I ᵀ) ᵀ ≈⟨ ᵀ-cong (≋.reflexive (≡.cong (map (f [_])) Iᵀ)) ⟩ + map (f [_]) I ᵀ ≈⟨ ᵀ-cong (map--[-]-I f) ⟩ f ᵀ ᵀ ≡⟨ f ᵀᵀ ⟩ f ∎ where @@ -147,7 +148,7 @@ opaque opaque - unfolding 𝟎 + unfolding 𝟎 _≋_ ·-𝟎ʳ : (M : Matrix A B) → M · 𝟎 {C} ≋ 𝟎 ·-𝟎ʳ [] = ≋.refl diff --git a/Data/Matrix/Core.agda b/Data/Matrix/Core.agda index d97cb20..4ef57fb 100644 --- a/Data/Matrix/Core.agda +++ b/Data/Matrix/Core.agda @@ -9,18 +9,18 @@ import Data.Vec.Relation.Binary.Equality.Setoid as PW-≈ import Data.Vec.Relation.Binary.Pointwise.Inductive as PW import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Data.Matrix.Raw as Raw using (_∥_; _≑_; _∷ᵥ_; _∷ₕ_; headₕ; tailₕ; headᵥ; tailᵥ; _ᵀ) open import Data.Matrix.Vec using (transpose) open import Data.Nat using (ℕ; _+_) -open import Data.Vec as Vec using (Vec; map; zipWith; head; tail; replicate) +open import Data.Vec as Vec using (map; zipWith; head; tail; replicate) open import Data.Vec.Properties using (map-cong; map-id) -open import Data.Vector.Core S using (Vector; Vectorₛ; _++_; ⟨⟩; ⟨⟩-!; _≊_) +open import Data.Vector.Core S using (Vector; Vectorₛ; _≊_) -- ; _++_; ⟨⟩; ⟨⟩-!) open import Data.Vector.Vec using (zipWith-map; replicate-++) open import Function using (id) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) open Setoid S open ℕ -open Vec.Vec private variable @@ -31,111 +31,22 @@ private module PW-≊ {n} = PW-≈ (Vectorₛ n) +open Raw.FixedBase Carrier using (Matrix) public + opaque - -- Matrices over a setoid - Matrix : Rel ℕ c - Matrix n m = Vec (Vector n) m + unfolding Raw.PW -- Pointwise equality of matrices _≋_ : Rel (Matrix n m) (c ⊔ ℓ) - _≋_ {n} {m} A B = A PW-≊.≋ B + _≋_ = Raw.PW _≈_ + + infix 4 _≋_ -- Pointwise equivalence is an equivalence relation ≋-isEquiv : IsEquivalence (_≋_ {n} {m}) ≋-isEquiv {n} {m} = PW-≊.≋-isEquivalence m - mapRows : (Vector n → Vector m) → Matrix n p → Matrix m p - mapRows = map - - _∥_ : Matrix A C → Matrix B C → Matrix (A + B) C - _∥_ M N = zipWith _++_ M N - - infixr 7 _∥_ - - _≑_ : Matrix A B → Matrix A C → Matrix A (B + C) - _≑_ M N = M Vec.++ N - - infixr 6 _≑_ - - _∷ᵥ_ : Vector A → Matrix A B → Matrix A (suc B) - _∷ᵥ_ V M = V Vec.∷ M - - infixr 5 _∷ᵥ_ - - opaque - - unfolding Vector - - _∷ₕ_ : Vector B → Matrix A B → Matrix (suc A) B - _∷ₕ_ V M = zipWith _∷_ V M - - infixr 5 _∷ₕ_ - - ∷ₕ-cong : {V V′ : Vector B} {M M′ : Matrix A B} → V ≊ V′ → M ≋ M′ → V ∷ₕ M ≋ V′ ∷ₕ M′ - ∷ₕ-cong PW.[] PW.[] = PW.[] - ∷ₕ-cong (≈x PW.∷ ≊V) (≊M₀ PW.∷ ≋M) = (≈x PW.∷ ≊M₀) PW.∷ (∷ₕ-cong ≊V ≋M) - - headₕ : Matrix (suc A) B → Vector B - headₕ M = map Vec.head M - - tailₕ : Matrix (suc A) B → Matrix A B - tailₕ M = map Vec.tail M - - head-∷-tailₕ : (M : Matrix (suc A) B) → headₕ M ∷ₕ tailₕ M ≡ M - head-∷-tailₕ M = begin - zipWith _∷_ (map Vec.head M) (map Vec.tail M) ≡⟨ zipWith-map head tail _∷_ M ⟩ - map (λ x → head x ∷ tail x) M ≡⟨ map-cong (λ { (_ ∷ _) → ≡.refl }) M ⟩ - map id M ≡⟨ map-id M ⟩ - M ∎ - where - open ≡-Reasoning - - []ᵥ : Matrix 0 B - []ᵥ = replicate _ [] - - []ᵥ-! : (E : Matrix 0 B) → E ≡ []ᵥ - []ᵥ-! [] = ≡.refl - []ᵥ-! ([] ∷ E) = ≡.cong ([] ∷_) ([]ᵥ-! E) - - []ᵥ-≑ : []ᵥ {A} ≑ []ᵥ {B} ≡ []ᵥ - []ᵥ-≑ {A} {B} = replicate-++ A B [] - - []ᵥ-∥ : (M : Matrix A B) → []ᵥ ∥ M ≡ M - []ᵥ-∥ [] = ≡.refl - []ᵥ-∥ (M₀ ∷ M) = ≡.cong (M₀ ∷_) ([]ᵥ-∥ M) - - ∷ₕ-∥ : (V : Vector C) (M : Matrix A C) (N : Matrix B C) → V ∷ₕ (M ∥ N) ≡ (V ∷ₕ M) ∥ N - ∷ₕ-∥ [] [] [] = ≡.refl - ∷ₕ-∥ (x ∷ V) (M₀ ∷ M) (N₀ ∷ N) = ≡.cong ((x ∷ M₀ ++ N₀) ∷_) (∷ₕ-∥ V M N) - - ∷ₕ-≑ : (V : Vector A) (W : Vector B) (M : Matrix C A) (N : Matrix C B) → (V ++ W) ∷ₕ (M ≑ N) ≡ (V ∷ₕ M) ≑ (W ∷ₕ N) - ∷ₕ-≑ [] W [] N = ≡.refl - ∷ₕ-≑ (x ∷ V) W (M₀ ∷ M) N = ≡.cong ((x ∷ M₀) ∷_) (∷ₕ-≑ V W M N) - - headᵥ : Matrix A (suc B) → Vector A - headᵥ (V ∷ _) = V - - tailᵥ : Matrix A (suc B) → Matrix A B - tailᵥ (_ ∷ M) = M - - head-∷-tailᵥ : (M : Matrix A (suc B)) → headᵥ M ∷ᵥ tailᵥ M ≡ M - head-∷-tailᵥ (_ ∷ _) = ≡.refl - - []ₕ : Matrix A 0 - []ₕ = [] - - []ₕ-! : (E : Matrix A 0) → E ≡ []ₕ - []ₕ-! [] = ≡.refl - - []ₕ-≑ : (M : Matrix A B) → []ₕ ≑ M ≡ M - []ₕ-≑ _ = ≡.refl - - ∷ᵥ-≑ : (V : Vector A) (M : Matrix A B) (N : Matrix A C) → V ∷ᵥ (M ≑ N) ≡ (V ∷ᵥ M) ≑ N - ∷ᵥ-≑ V M N = ≡.refl - -infix 4 _≋_ - module ≋ {n} {m} = IsEquivalence (≋-isEquiv {n} {m}) Matrixₛ : ℕ → ℕ → Setoid c (c ⊔ ℓ) @@ -147,120 +58,51 @@ Matrixₛ n m = record opaque - unfolding Vector - - head′ : Vector (suc A) → Carrier - head′ = head - - head-cong : {V V′ : Vector (suc A)} → V ≊ V′ → head′ V ≈ head′ V′ - head-cong (≈x PW.∷ _) = ≈x - - tail′ : Vector (suc A) → Vector A - tail′ = tail - - tail-cong : {V V′ : Vector (suc A)} → V ≊ V′ → tail′ V ≊ tail′ V′ - tail-cong (_ PW.∷ ≊V) = ≊V - -opaque - - unfolding headₕ head′ - - ≋headₕ : {M M′ : Matrix (suc A) B} → M ≋ M′ → headₕ M ≊ headₕ M′ - ≋headₕ M≋M′ = PW.map⁺ head-cong M≋M′ - - ≋tailₕ : {M M′ : Matrix (suc A) B} → M ≋ M′ → tailₕ M ≋ tailₕ M′ - ≋tailₕ M≋M′ = PW.map⁺ tail-cong M≋M′ - -opaque - unfolding _≋_ _∥_ []ᵥ _∷ₕ_ - ∥-cong : {M M′ : Matrix A C} {N N′ : Matrix B C} → M ≋ M′ → N ≋ N′ → M ∥ N ≋ M′ ∥ N′ - ∥-cong {zero} {C} {B} {M} {M′} {N} {N′} ≋M ≋N - rewrite []ᵥ-! M - rewrite []ᵥ-! M′ = begin - ([]ᵥ ∥ N) ≡⟨ []ᵥ-∥ N ⟩ - N ≈⟨ ≋N ⟩ - N′ ≡⟨ []ᵥ-∥ N′ ⟨ - ([]ᵥ ∥ N′) ∎ - where - open ≈-Reasoning (Matrixₛ _ _) - ∥-cong {suc A} {C} {B} {M} {M′} {N} {N′} ≋M ≋N - rewrite ≡.sym (head-∷-tailₕ M) - using M₀ ← headₕ M - using M- ← tailₕ M - rewrite ≡.sym (head-∷-tailₕ M′) - using M₀′ ← headₕ M′ - using M-′ ← tailₕ M′ = begin - (M₀ ∷ₕ M-) ∥ N ≡⟨ ∷ₕ-∥ M₀ M- N ⟨ - M₀ ∷ₕ M- ∥ N ≈⟨ ∷ₕ-cong ≊M₀ (∥-cong ≋M- ≋N) ⟩ - M₀′ ∷ₕ M-′ ∥ N′ ≡⟨ ∷ₕ-∥ M₀′ M-′ N′ ⟩ - (M₀′ ∷ₕ M-′) ∥ N′ ∎ - where - ≊M₀ : M₀ ≊ M₀′ - ≊M₀ = begin - headₕ M ≡⟨ ≡.cong headₕ (head-∷-tailₕ M) ⟨ - headₕ (M₀ ∷ₕ M-) ≈⟨ ≋headₕ ≋M ⟩ - headₕ (M₀′ ∷ₕ M-′) ≡⟨ ≡.cong headₕ (head-∷-tailₕ M′) ⟩ - headₕ M′ ∎ - where - open ≈-Reasoning (Vectorₛ _) - ≋M- : M- ≋ M-′ - ≋M- = begin - tailₕ M ≡⟨ ≡.cong tailₕ (head-∷-tailₕ M) ⟨ - tailₕ (M₀ ∷ₕ M-) ≈⟨ ≋tailₕ ≋M ⟩ - tailₕ (M₀′ ∷ₕ M-′) ≡⟨ ≡.cong tailₕ (head-∷-tailₕ M′) ⟩ - tailₕ M′ ∎ - where - open ≈-Reasoning (Matrixₛ _ _) - open ≈-Reasoning (Matrixₛ _ _) - -opaque - unfolding _≑_ - ≑-cong : {M M′ : Matrix A B} {N N′ : Matrix A C} → M ≋ M′ → N ≋ N′ → M ≑ N ≋ M′ ≑ N′ - ≑-cong PW.[] ≋N = ≋N - ≑-cong (M₀≊M₀′ PW.∷ ≋M) ≋N = M₀≊M₀′ PW.∷ ≑-cong ≋M ≋N - -opaque - - unfolding Matrix - - _ᵀ : Matrix n m → Matrix m n - _ᵀ [] = []ᵥ - _ᵀ (M₀ ∷ M) = M₀ ∷ₕ M ᵀ - - infix 10 _ᵀ - - -ᵀ-cong : {M₁ M₂ : Matrix n m} → M₁ ≋ M₂ → M₁ ᵀ ≋ M₂ ᵀ - -ᵀ-cong PW.[] = ≋.refl - -ᵀ-cong (≊M₀ PW.∷ ≋M) = ∷ₕ-cong ≊M₀ (-ᵀ-cong ≋M) - - opaque - - unfolding []ᵥ []ₕ - - []ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A} - []ᵥ-ᵀ {zero} = ≡.refl - []ᵥ-ᵀ {suc A} = ≡.cong (zipWith _∷_ []) ([]ᵥ-ᵀ) - - opaque - - unfolding _∷ₕ_ Vector - - ∷ₕ-ᵀ : (V : Vector A) (M : Matrix B A) → (V ∷ₕ M) ᵀ ≡ V ∷ᵥ M ᵀ - ∷ₕ-ᵀ [] [] = ≡.refl - ∷ₕ-ᵀ (x ∷ V) (M₀ ∷ M) = ≡.cong ((x ∷ M₀) ∷ₕ_) (∷ₕ-ᵀ V M) - - ∷ᵥ-ᵀ : (V : Vector B) (M : Matrix B A) → (V ∷ᵥ M) ᵀ ≡ V ∷ₕ M ᵀ - ∷ᵥ-ᵀ V M = ≡.refl - - opaque - - _ᵀᵀ : (M : Matrix n m) → M ᵀ ᵀ ≡ M - _ᵀᵀ [] = []ᵥ-ᵀ - _ᵀᵀ (M₀ ∷ M) = begin - (M₀ ∷ₕ M ᵀ) ᵀ ≡⟨ ∷ₕ-ᵀ M₀ (M ᵀ) ⟩ - M₀ ∷ᵥ M ᵀ ᵀ ≡⟨ ≡.cong (M₀ ∷ᵥ_) (M ᵀᵀ) ⟩ - M₀ ∷ᵥ M ∎ - where - open ≡-Reasoning - - infix 10 _ᵀᵀ + unfolding _≋_ + + ∥-cong + : {M₁ M₂ : Matrix A C} + {N₁ N₂ : Matrix B C} + → M₁ ≋ M₂ + → N₁ ≋ N₂ + → M₁ ∥ N₁ ≋ M₂ ∥ N₂ + ∥-cong = Raw.Relation.R-∥ + + ≑-cong + : {M₁ M₂ : Matrix A B} + {N₁ N₂ : Matrix A C} + → M₁ ≋ M₂ + → N₁ ≋ N₂ + → M₁ ≑ N₁ ≋ M₂ ≑ N₂ + ≑-cong = Raw.Relation.R-≑ + + ∷ᵥ-cong + : {V₁ V₂ : Vector n} + {M₁ M₂ : Matrix n m} + → V₁ ≊ V₂ + → M₁ ≋ M₂ + → V₁ ∷ᵥ M₁ ≋ V₂ ∷ᵥ M₂ + ∷ᵥ-cong = Raw.Relation.R-∷ᵥ + + ∷ₕ-cong + : {V₁ V₂ : Vector n} + {M₁ M₂ : Matrix m n} + → V₁ ≊ V₂ + → M₁ ≋ M₂ + → V₁ ∷ₕ M₁ ≋ V₂ ∷ₕ M₂ + ∷ₕ-cong = Raw.Relation.R-∷ₕ + + headₕ-cong : {M₁ M₂ : Matrix (suc n) m} → M₁ ≋ M₂ → headₕ M₁ ≊ headₕ M₂ + headₕ-cong = Raw.Relation.R-headₕ + + tailₕ-cong : {M₁ M₂ : Matrix (suc n) m} → M₁ ≋ M₂ → tailₕ M₁ ≋ tailₕ M₂ + tailₕ-cong = Raw.Relation.R-tailₕ + + headᵥ-cong : {M₁ M₂ : Matrix n (suc m)} → M₁ ≋ M₂ → headᵥ M₁ ≊ headᵥ M₂ + headᵥ-cong = Raw.Relation.R-headᵥ + + tailᵥ-cong : {M₁ M₂ : Matrix n (suc m)} → M₁ ≋ M₂ → tailᵥ M₁ ≋ tailᵥ M₂ + tailᵥ-cong = Raw.Relation.R-tailᵥ + + ᵀ-cong : {M₁ M₂ : Matrix n m} → M₁ ≋ M₂ → M₁ ᵀ ≋ M₂ ᵀ + ᵀ-cong = Raw.Relation.R-ᵀ diff --git a/Data/Matrix/Dagger-2-Poset.agda b/Data/Matrix/Dagger-2-Poset.agda index cddf183..0cda1ee 100644 --- a/Data/Matrix/Dagger-2-Poset.agda +++ b/Data/Matrix/Dagger-2-Poset.agda @@ -16,10 +16,11 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Category.Dagger.2-Poset using (dagger-2-poset; Dagger-2-Poset) open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) open import Data.Matrix.Category R.semiring using (Mat; _·_; ·-Iˡ; ·-Iʳ; ·-resp-≋; ·-assoc; ∥-·-≑; ·-∥; ·-𝟎ˡ; ≑-·) -open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; _∥_; _≑_; _ᵀ; module ≋; ∥-cong; ≑-cong) +open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; module ≋; ∥-cong; ≑-cong) open import Data.Matrix.Monoid R.+-monoid using (𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ) -open import Data.Matrix.Transform R.semiring using (I; Iᵀ) +open import Data.Matrix.Raw using (_∥_; _≑_; _ᵀ) open import Data.Matrix.SemiadditiveDagger R using (∥-ᵀ; Mat-SemiadditiveDagger) +open import Data.Matrix.Transform R.semiring using (I; Iᵀ) open import Data.Nat using (ℕ) open import Data.Vec using (Vec) open import Data.Vector.Core R.setoid using (Vector; _≊_) @@ -33,7 +34,7 @@ private A B : ℕ opaque - unfolding _≊_ _⊕_ + unfolding _⊕_ ⊕-idem : (V : Vector A) → V ⊕ V ≊ V ⊕-idem [] = PW.[] ⊕-idem (v ∷ V) = +-idem v PW.∷ ⊕-idem V diff --git a/Data/Matrix/Endofunctor.agda b/Data/Matrix/Endofunctor.agda index 25703ce..ac3638f 100644 --- a/Data/Matrix/Endofunctor.agda +++ b/Data/Matrix/Endofunctor.agda @@ -6,13 +6,14 @@ open import Level using (Level; _⊔_) -- The endofunctor in setoids sending A to Matrix A n m for fixed n and m module Data.Matrix.Endofunctor (n m : ℕ) {c ℓ : Level} where -import Data.Vector.Endofunctor as Vector +import Data.Vector.Endofunctor.Setoid as Vector open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor using (Functor; _∘F_) +open import Data.Matrix.Raw as Raw using (map; map₂) open import Data.Matrix.Core as Core using (Matrix; Matrixₛ) open import Data.Vector.Core using (Vector) -open import Function using (_⟶ₛ_; _⟨$⟩_) +open import Function using (_⟶ₛ_; _⟨$⟩_; Func) open import Function.Construct.Composition using () renaming (function to compose) open import Function.Construct.Identity using () renaming (function to Id) open import Function.Construct.Setoid using (setoid) @@ -25,21 +26,26 @@ private module Vec∘Vec = Functor Vec∘Vec +open Func + opaque - unfolding Matrix Vector - map : {A B : Setoid c ℓ} → A ⟶ₛ B → Matrixₛ A n m ⟶ₛ Matrixₛ B n m - map = Vec∘Vec.₁ + + unfolding Core._≋_ + + mapₛ : {A B : Setoid c ℓ} → A ⟶ₛ B → Matrixₛ A n m ⟶ₛ Matrixₛ B n m + to (mapₛ f) = map (to f) + cong (mapₛ f) = map₂ (cong f) abstract opaque - unfolding map + unfolding mapₛ identity : {A : Setoid c ℓ} {M : Matrix A n m} (open Core A using (_≋_)) - → map (Id A) ⟨$⟩ M ≋ M - identity = Vec∘Vec.identity + → mapₛ (Id A) ⟨$⟩ M ≋ M + identity {A} = Vec∘Vec.identity {A} homomorphism : {X Y Z : Setoid c ℓ} @@ -47,8 +53,8 @@ abstract opaque {g : Y ⟶ₛ Z} {M : Matrix X n m} (open Core Z using (_≋_)) - → map (compose f g) ⟨$⟩ M ≋ map g ⟨$⟩ (map f ⟨$⟩ M) - homomorphism = Vec∘Vec.homomorphism + → mapₛ (compose f g) ⟨$⟩ M ≋ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ M) + homomorphism {f = f} {g} = Vec∘Vec.homomorphism {f = f} {g} F-resp-≈ : {A B : Setoid c ℓ} @@ -57,14 +63,14 @@ abstract opaque → (f ≈ g) → {M : Matrix A n m} (open Core B using (_≋_)) - → map f ⟨$⟩ M ≋ map g ⟨$⟩ M - F-resp-≈ = Vec∘Vec.F-resp-≈ + → mapₛ f ⟨$⟩ M ≋ mapₛ g ⟨$⟩ M + F-resp-≈ {f = f} {g} = Vec∘Vec.F-resp-≈ {f = f} {g} -- only a true endofunctor when c ≤ ℓ Mat : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) Mat = record { F₀ = λ A → Matrixₛ A n m - ; F₁ = map + ; F₁ = mapₛ ; identity = identity ; homomorphism = homomorphism ; F-resp-≈ = F-resp-≈ diff --git a/Data/Matrix/FreeSemimodule.agda b/Data/Matrix/FreeSemimodule.agda index ae5822f..77f2fe3 100644 --- a/Data/Matrix/FreeSemimodule.agda +++ b/Data/Matrix/FreeSemimodule.agda @@ -13,7 +13,7 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Categories.Functor using (Functor) open import Category.Instance.Semimodules {c} {ℓ} {c} {c ⊔ ℓ} R using (Semimodules; SemimoduleHomomorphism) open import Data.Matrix.Category R.semiring using (Mat; _·_; ·-[]) -open import Data.Matrix.Core R.setoid using (Matrix; module ≋; mapRows) +open import Data.Matrix.Core R.setoid using (Matrix; module ≋) open import Data.Matrix.Transform R.semiring using (I; _[_]; -[-]-cong; -[-]-cong₁; [_]_; -[⟨0⟩]; I[-]; -[⊕]) open import Data.Nat using (ℕ) open import Data.Vec using (map) diff --git a/Data/Matrix/Matrices.agda b/Data/Matrix/Matrices.agda new file mode 100644 index 0000000..008ec36 --- /dev/null +++ b/Data/Matrix/Matrices.agda @@ -0,0 +1,110 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; 0ℓ; _⊔_) + +-- Functor from category of rigs to the category of categories +module Data.Matrix.Matrices {c ℓ : Level} where + +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Algebra.Bundles using (Semiring) +open import Algebra.Morphism.Bundles using (SemiringHomomorphism) +open import Categories.Category.Instance.Cats using (Cats) +open import Categories.Functor using (Functor; _∘F_) renaming (id to idF) +open import Categories.Morphism.Properties using (id-iso) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) +open import Category.Instance.Rigs using (Rigs; compose) renaming (id to idRigHomo) +open import Data.Matrix.BaseChange using (ChangeBase) +open import Data.Matrix.BaseChange using (change) +open import Data.Matrix.Category as Cat using (Mat) +open import Data.Matrix.Core as Core using () +open import Data.Matrix.Endofunctor using (mapₛ; identity; homomorphism; F-resp-≈) +open import Data.Matrix.Transform as Transform using () +open import Data.Nat using (ℕ) +open import Relation.Binary.PropositionalEquality using (_≗_) + +open Semiring using (rawSemiring) +open SemiringHomomorphism using (⟦_⟧) + +≃-identity : {A : Semiring c ℓ} → ChangeBase A A (Category.Instance.Rigs.id A) ≃ idF +≃-identity {A} = niHelper record + { η = λ n → I {n} + ; η⁻¹ = λ n → I {n} + ; commute = commute + ; iso = λ n → id-iso (Mat A) + } + where + module A = Semiring A + open Core A.setoid + open Transform A + open Cat A hiding (Mat) + commute : {n m : ℕ} (M : Matrix n m) → I · change A A (idRigHomo A) M ≋ M · I + commute {n} {m} M = begin + I · change A A (idRigHomo A) M ≈⟨ ·-Iˡ ⟩ + change A A (idRigHomo A) M ≈⟨ identity n m ⟩ + M ≈⟨ ·-Iʳ ⟨ + M · I ∎ + where + open ≈-Reasoning (Matrixₛ n m) + +≃-homo + : {X Y Z : Semiring c ℓ} + {g : SemiringHomomorphism (rawSemiring Y) (rawSemiring Z)} + {f : SemiringHomomorphism (rawSemiring X) (rawSemiring Y)} + → ChangeBase X Z (compose X Y Z g f) ≃ ChangeBase Y Z g ∘F ChangeBase X Y f +≃-homo {X} {Y} {Z} {g} {f} = niHelper record + { η = λ n → I {n} + ; η⁻¹ = λ n → I {n} + ; commute = commute + ; iso = λ n → id-iso (Mat Z) + } + where + module Z = Semiring Z + module X = Semiring X + open Core Z.setoid using (_≋_; Matrixₛ) + open Core X.setoid using (Matrix) + open Transform Z + open Cat Z hiding (Mat) + commute : {n m : ℕ} (M : Matrix n m) → I · change X Z (compose X Y Z g f) M ≋ change Y Z g (change X Y f M) · I + commute {n} {m} M = begin + I · change X Z (compose X Y Z g f) M ≈⟨ ·-Iˡ ⟩ + change X Z (compose X Y Z g f) M ≈⟨ homomorphism n m ⟩ + change Y Z g (change X Y f M) ≈⟨ ·-Iʳ ⟨ + change Y Z g (change X Y f M) · I ∎ + where + open ≈-Reasoning (Matrixₛ n m) + +resp-≈ : {A B : Semiring c ℓ} + → {f g : SemiringHomomorphism (rawSemiring A) (rawSemiring B)} + → ⟦ f ⟧ ≗ ⟦ g ⟧ + → ChangeBase A B f ≃ ChangeBase A B g +resp-≈ {A} {B} {f} {g} f≗g = niHelper record + { η = λ n → I {n} + ; η⁻¹ = λ n → I {n} + ; commute = commute + ; iso = λ n → id-iso (Mat B) + } + where + module A = Semiring A + module B = Semiring B + open Core A.setoid using (Matrix) + open Core B.setoid using (_≋_; Matrixₛ) + open Transform B + open Cat B hiding (Mat) + commute : {n m : ℕ} (M : Matrix n m) → I · change A B f M ≋ change A B g M · I + commute {n} {m} M = begin + I · change A B f M ≈⟨ ·-Iˡ ⟩ + change A B f M ≈⟨ F-resp-≈ n m (λ {x} → B.reflexive (f≗g x)) ⟩ + change A B g M ≈⟨ ·-Iʳ ⟨ + change A B g M · I ∎ + where + open ≈-Reasoning (Matrixₛ n m) + +Matrices : Functor (Rigs {c} {ℓ}) (Cats 0ℓ c (c ⊔ ℓ)) +Matrices = record + { F₀ = Mat + ; F₁ = λ {R S} → ChangeBase R S + ; identity = ≃-identity + ; homomorphism = ≃-homo + ; F-resp-≈ = resp-≈ + } diff --git a/Data/Matrix/Monoid.agda b/Data/Matrix/Monoid.agda index b7638f6..93b449f 100644 --- a/Data/Matrix/Monoid.agda +++ b/Data/Matrix/Monoid.agda @@ -10,7 +10,8 @@ module M = Monoid M import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Data.Vec.Relation.Binary.Pointwise.Inductive as PW -open import Data.Matrix.Core M.setoid using (Matrix; _≋_; _ᵀ; _∷ₕ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥) +open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥) +open import Data.Matrix.Core M.setoid using (Matrix; _≋_) open import Data.Nat using (ℕ) open import Data.Vec using (Vec; replicate; zipWith) open import Data.Vec.Properties using (zipWith-replicate) @@ -72,7 +73,7 @@ opaque opaque - unfolding Matrix + unfolding _≋_ _[+]_ : Matrix A B → Matrix A B → Matrix A B _[+]_ = zipWith _⊕_ diff --git a/Data/Matrix/Raw.agda b/Data/Matrix/Raw.agda new file mode 100644 index 0000000..f2ad431 --- /dev/null +++ b/Data/Matrix/Raw.agda @@ -0,0 +1,320 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_) +open import Relation.Binary using (Rel; REL) + +module Data.Matrix.Raw where + +open import Data.Nat using (ℕ; _+_) +open import Data.Vec as Vec using (Vec; zipWith; head; tail; replicate) +open import Data.Vec using (_++_) +open import Data.Vec.Properties using (map-cong; map-id; map-++; map-∘; map-replicate) +open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW-Vec using (Pointwise; map⁺) +open import Data.Vector.Raw as Vector using (R-zipWith) +open import Data.Vector.Vec using (zipWith-map; replicate-++; map-zipWith; zipWith-map-map; zipWith-cong) +open import Function using (id; _∘_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) + +open ℕ +open Vec.Vec + +private + variable + n m p : ℕ + a ℓ ℓ₁ ℓ₂ : Level + A B C D E F : Set a + +open ≡-Reasoning + +module FixedBase (A : Set a) where + + opaque + + -- Matrices + Matrix : Rel ℕ a + Matrix n m = Vec (Vec A n) m + +open FixedBase public + +opaque + + unfolding Matrix + + PW : {a b : Level} {A : Set a} {B : Set b} (R : REL A B ℓ) → REL (Matrix A n m) (Matrix B n m) (a ⊔ b ⊔ ℓ) + PW R = Pointwise (Pointwise R) + + mapRows : (Vec A n → Vec A m) → Matrix A n p → Matrix A m p + mapRows = Vec.map + + map : (A → B) → Matrix A n m → Matrix B n m + map f = Vec.map (Vec.map f) + + _∥_ : Matrix A n p → Matrix A m p → Matrix A (n + m) p + _∥_ M N = zipWith _++_ M N + + infixr 7 _∥_ + + _≑_ : Matrix A n m → Matrix A n p → Matrix A n (m + p) + _≑_ M N = M ++ N + + infixr 6 _≑_ + + _∷ᵥ_ : Vec A n → Matrix A n m → Matrix A n (suc m) + _∷ᵥ_ V M = V Vec.∷ M + + infixr 5 _∷ᵥ_ + + _∷ₕ_ : Vec A m → Matrix A n m → Matrix A (suc n) m + _∷ₕ_ V M = zipWith _∷_ V M + + infixr 5 _∷ₕ_ + + headₕ : Matrix A (suc n) m → Vec A m + headₕ = Vec.map Vec.head + + tailₕ : Matrix A (suc n) m → Matrix A n m + tailₕ = Vec.map Vec.tail + + head-∷-tailₕ : (M : Matrix A (suc n) m) → headₕ M ∷ₕ tailₕ M ≡ M + head-∷-tailₕ M = begin + zipWith _∷_ (Vec.map Vec.head M) (Vec.map Vec.tail M) ≡⟨ zipWith-map head tail _∷_ M ⟩ + Vec.map (λ x → head x ∷ tail x) M ≡⟨ map-cong (λ { (_ ∷ _) → ≡.refl }) M ⟩ + Vec.map id M ≡⟨ map-id M ⟩ + M ∎ + + []ᵥ : Matrix A 0 m + []ᵥ = replicate _ [] + + []ᵥ-! : (E : Matrix A 0 m) → E ≡ []ᵥ + []ᵥ-! [] = ≡.refl + []ᵥ-! ([] ∷ E) = ≡.cong ([] ∷_) ([]ᵥ-! E) + + []ᵥ-≑ : []ᵥ {m = n} ≑ []ᵥ ≡ []ᵥ {A = A} {n + m} + []ᵥ-≑ {n = n} {m = m} = replicate-++ n m [] + + []ᵥ-∥ : (M : Matrix A n m) → []ᵥ ∥ M ≡ M + []ᵥ-∥ [] = ≡.refl + []ᵥ-∥ (M₀ ∷ M) = ≡.cong (M₀ ∷_) ([]ᵥ-∥ M) + + ∷ₕ-∥ : (V : Vec A p) (M : Matrix A n p) (N : Matrix A m p) → V ∷ₕ (M ∥ N) ≡ (V ∷ₕ M) ∥ N + ∷ₕ-∥ [] [] [] = ≡.refl + ∷ₕ-∥ (x ∷ V) (M₀ ∷ M) (N₀ ∷ N) = ≡.cong ((x ∷ M₀ ++ N₀) ∷_) (∷ₕ-∥ V M N) + + ∷ₕ-≑ : (V : Vec A n) (W : Vec A m) (M : Matrix A p n) (N : Matrix A p m) → (V ++ W) ∷ₕ (M ≑ N) ≡ (V ∷ₕ M) ≑ (W ∷ₕ N) + ∷ₕ-≑ [] W [] N = ≡.refl + ∷ₕ-≑ (x ∷ V) W (M₀ ∷ M) N = ≡.cong ((x ∷ M₀) ∷_) (∷ₕ-≑ V W M N) + + headᵥ : Matrix A n (suc m) → Vec A n + headᵥ = head + + tailᵥ : Matrix A n (suc m) → Matrix A n m + tailᵥ = tail + + head-∷-tailᵥ : (M : Matrix A n (suc m)) → headᵥ M ∷ᵥ tailᵥ M ≡ M + head-∷-tailᵥ (_ ∷ _) = ≡.refl + + []ₕ : Matrix A n 0 + []ₕ = [] + + []ₕ-! : (E : Matrix A n 0) → E ≡ []ₕ + []ₕ-! [] = ≡.refl + + []ₕ-≑ : (M : Matrix A n m) → []ₕ ≑ M ≡ M + []ₕ-≑ _ = ≡.refl + + ∷ᵥ-≑ : (V : Vec A n) (M : Matrix A n m) (N : Matrix A n p) → V ∷ᵥ (M ≑ N) ≡ (V ∷ᵥ M) ≑ N + ∷ᵥ-≑ V M N = ≡.refl + + _ᵀ : Matrix A n m → Matrix A m n + _ᵀ [] = []ᵥ + _ᵀ (M₀ ∷ M) = M₀ ∷ₕ M ᵀ + + infix 10 _ᵀ + + []ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A = A} {n} + []ᵥ-ᵀ {n = zero} = ≡.refl + []ᵥ-ᵀ {n = suc n} = ≡.cong (zipWith _∷_ []) ([]ᵥ-ᵀ) + + ∷ₕ-ᵀ : (V : Vec A n) (M : Matrix A m n) → (V ∷ₕ M) ᵀ ≡ V ∷ᵥ M ᵀ + ∷ₕ-ᵀ [] [] = ≡.refl + ∷ₕ-ᵀ (x ∷ V) (M₀ ∷ M) = ≡.cong ((x ∷ M₀) ∷ₕ_) (∷ₕ-ᵀ V M) + + ∷ᵥ-ᵀ : (V : Vec A m) (M : Matrix A m n) → (V ∷ᵥ M) ᵀ ≡ V ∷ₕ M ᵀ + ∷ᵥ-ᵀ V M = ≡.refl + + _ᵀᵀ : (M : Matrix A n m) → M ᵀ ᵀ ≡ M + _ᵀᵀ [] = []ᵥ-ᵀ + _ᵀᵀ (M₀ ∷ M) = begin + (M₀ ∷ₕ M ᵀ) ᵀ ≡⟨ ∷ₕ-ᵀ M₀ (M ᵀ) ⟩ + M₀ ∷ᵥ M ᵀ ᵀ ≡⟨ ≡.cong (M₀ ∷ᵥ_) (M ᵀᵀ) ⟩ + M₀ ∷ᵥ M ∎ + + infix 10 _ᵀᵀ + +open Pointwise + +module Natural (f : A → B) where + + open Vector.Natural + + opaque + + unfolding map + + α-∥ : (M : Matrix A n p) (N : Matrix A m p) → map f (M ∥ N) ≡ map f M ∥ map f N + α-∥ M N = begin + Vec.map (Vec.map f) (zipWith _++_ M N) ≡⟨ map-zipWith (Vec.map f) _++_ M N ⟩ + zipWith (λ x y → Vec.map f (x ++ y)) M N ≡⟨ zipWith-cong (map-++ f) M N ⟩ + zipWith (λ x y → Vec.map f x ++ Vec.map f y) M N ≡⟨ zipWith-map-map (Vec.map f) (Vec.map f) _++_ M N ⟩ + zipWith _++_ (Vec.map (Vec.map f) M) (Vec.map (Vec.map f) N) ∎ + + α-≑ : (M : Matrix A n m) (N : Matrix A n p) → map f (M ≑ N) ≡ map f M ≑ map f N + α-≑ = map-++ (Vec.map f) + + α-∷ᵥ : (V : Vec A n) (M : Matrix A n m) → map f (V ∷ᵥ M) ≡ Vec.map f V ∷ᵥ map f M + α-∷ᵥ _ _ = ≡.refl + + α-∷ₕ : (V : Vec A m) (M : Matrix A n m) → map f (V ∷ₕ M) ≡ Vec.map f V ∷ₕ map f M + α-∷ₕ V M = begin + Vec.map (Vec.map f) (zipWith _∷_ V M) ≡⟨ map-zipWith (Vec.map f) _∷_ V M ⟩ + zipWith (λ x y → f x ∷ Vec.map f y) V M ≡⟨ zipWith-map-map f (Vec.map f) _∷_ V M ⟩ + zipWith _∷_ (Vec.map f V) (Vec.map (Vec.map f) M) ∎ + + α-headₕ : (M : Matrix A (suc n) m) → Vec.map f (headₕ M) ≡ headₕ (map f M) + α-headₕ M = begin + Vec.map f (Vec.map head M) ≡⟨ map-∘ f head M ⟨ + Vec.map (f ∘ head) M ≡⟨ map-cong (α-head f) M ⟩ + Vec.map (head ∘ Vec.map f) M ≡⟨ map-∘ head (Vec.map f) M ⟩ + Vec.map head (Vec.map (Vec.map f) M) ∎ + + α-tailₕ : (M : Matrix A (suc n) m) → map f (tailₕ M) ≡ tailₕ (map f M) + α-tailₕ M = begin + Vec.map (Vec.map f) (Vec.map tail M) ≡⟨ map-∘ (Vec.map f) tail M ⟨ + Vec.map (Vec.map f ∘ tail) M ≡⟨ map-cong (α-tail f) M ⟩ + Vec.map (tail ∘ Vec.map f) M ≡⟨ map-∘ tail (Vec.map f) M ⟩ + Vec.map tail (Vec.map (Vec.map f) M) ∎ + + α-[]ᵥ : map f ([]ᵥ {m = m}) ≡ []ᵥ + α-[]ᵥ {m} = map-replicate (Vec.map f) [] m + + α-headᵥ : (M : Matrix A n (suc m)) → Vec.map f (headᵥ M) ≡ headᵥ (map f M) + α-headᵥ = α-head (Vec.map f) + + α-tailᵥ : (M : Matrix A n (suc m)) → map f (tailᵥ M) ≡ tailᵥ (map f M) + α-tailᵥ = α-tail (Vec.map f) + + α-[]ₕ : map f ([]ₕ {n = n}) ≡ []ₕ + α-[]ₕ = ≡.refl + + α-ᵀ : (M : Matrix A n m) → map f (M ᵀ) ≡ map f M ᵀ + α-ᵀ [] = α-[]ᵥ + α-ᵀ (V ∷ M) = begin + map f (V ∷ₕ M ᵀ) ≡⟨ α-∷ₕ V (M ᵀ) ⟩ + Vec.map f V ∷ₕ map f (M ᵀ) ≡⟨ ≡.cong (Vec.map f V ∷ₕ_) (α-ᵀ M) ⟩ + Vec.map f V ∷ₕ map f M ᵀ ∎ + +opaque + + unfolding PW + + -- TODO double functor + map₂ + : {R : REL A B ℓ} + {S : REL C D ℓ} + {f : A → C} + {g : B → D} + → (∀ {x y} → R x y → S (f x) (g y)) + → {M₁ : Matrix A m n} + {M₂ : Matrix B m n} + → PW R M₁ M₂ + → PW S (map f M₁) (map g M₂) + map₂ R⇒S = map⁺ (map⁺ R⇒S) + +module Relation {R : REL A B ℓ} where + + open Vector.Relation + + opaque + + unfolding PW + + R-∥ : {M₁ : Matrix A n p} + {M₂ : Matrix B n p} + {N₁ : Matrix A m p} + {N₂ : Matrix B m p} + → PW R M₁ M₂ + → PW R N₁ N₂ + → PW R (M₁ ∥ N₁) (M₂ ∥ N₂) + R-∥ = R-zipWith {R = Pointwise R} (R-++ {R = R}) + + R-≑ : {M₁ : Matrix A n m} + {M₂ : Matrix B n m} + {N₁ : Matrix A n p} + {N₂ : Matrix B n p} + → PW R M₁ M₂ + → PW R N₁ N₂ + → PW R (M₁ ≑ N₁) (M₂ ≑ N₂) + R-≑ = R-++ {R = Pointwise R} + + R-∷ᵥ + : {V₁ : Vec A n} + {V₂ : Vec B n} + {M₁ : Matrix A n m} + {M₂ : Matrix B n m} + → Pointwise R V₁ V₂ + → PW R M₁ M₂ + → PW R (V₁ ∷ᵥ M₁) (V₂ ∷ᵥ M₂) + R-∷ᵥ R-V R-M = R-V ∷ R-M + + R-∷ₕ + : {V₁ : Vec A n} + {V₂ : Vec B n} + {M₁ : Matrix A m n} + {M₂ : Matrix B m n} + → Pointwise R V₁ V₂ + → PW R M₁ M₂ + → PW R (V₁ ∷ₕ M₁) (V₂ ∷ₕ M₂) + R-∷ₕ [] [] = [] + R-∷ₕ (R-x ∷ R-V) (R-M₀ ∷ R-M) = (R-x ∷ R-M₀) ∷ R-∷ₕ R-V R-M + + R-headₕ + : {M₁ : Matrix A (suc n) m} + {M₂ : Matrix B (suc n) m} + → PW R M₁ M₂ + → Pointwise R (headₕ M₁) (headₕ M₂) + R-headₕ = map⁺ R-head + + R-tailₕ + : {M₁ : Matrix A (suc n) m} + {M₂ : Matrix B (suc n) m} + → PW R M₁ M₂ + → PW R (tailₕ M₁) (tailₕ M₂) + R-tailₕ = map⁺ R-tail + + R-[]ᵥ : PW R []ᵥ ([]ᵥ {m = m}) + R-[]ᵥ = R-replicate [] + + R-headᵥ + : {M₁ : Matrix A n (suc m)} + {M₂ : Matrix B n (suc m)} + → PW R M₁ M₂ + → Pointwise R (headᵥ M₁) (headᵥ M₂) + R-headᵥ = R-head + + R-tailᵥ + : {M₁ : Matrix A n (suc m)} + {M₂ : Matrix B n (suc m)} + → PW R M₁ M₂ + → PW R (tailᵥ M₁) (tailᵥ M₂) + R-tailᵥ = R-tail + + R-[]ₕ : PW R []ₕ ([]ₕ {n = n}) + R-[]ₕ = [] + + R-ᵀ + : {M₁ : Matrix A n m} + {M₂ : Matrix B n m} + → PW R M₁ M₂ + → PW R (M₁ ᵀ) (M₂ ᵀ) + R-ᵀ [] = R-[]ᵥ + R-ᵀ (R-V ∷ R-M) = R-∷ₕ R-V (R-ᵀ R-M) diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda index 220ff2e..ebc6592 100644 --- a/Data/Matrix/SemiadditiveDagger.agda +++ b/Data/Matrix/SemiadditiveDagger.agda @@ -18,15 +18,17 @@ open import Categories.Object.Initial using (Initial) open import Category.Dagger.Semiadditive using (DaggerCocartesianMonoidal; SemiadditiveDagger) open import Data.Matrix.Cast R.setoid using (cast₂; cast₂-∥; ∥-≑; ∥-≑⁴; ≑-sym-assoc) open import Data.Matrix.Category R.semiring using (Mat; _·_; ≑-·; ·-Iˡ; ·-Iʳ; ·-𝟎ˡ; ·-𝟎ʳ; ·-∥; ∥-·-≑) -open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _ᵀ; _ᵀᵀ; _≋_; module ≋; mapRows; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; ∥-cong; ≑-cong; -ᵀ-cong; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; []ᵥ-!) +open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; mapRows; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; []ᵥ-!) +open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; module ≋; ∥-cong; ≑-cong; ᵀ-cong) open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; 𝟎≑𝟎; 𝟎∥𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ) open import Data.Matrix.Transform R.semiring using (I; Iᵀ; [_]_; _[_]; -[-]ᵀ; [-]--cong; [-]-[]ᵥ; [⟨⟩]-[]ₕ) open import Data.Nat using (ℕ) open import Data.Product using (_,_; Σ-syntax) -open import Data.Vec using (Vec; map; replicate) +open import Data.Vec using (Vec; map; replicate; _++_) open import Data.Vec.Properties using (map-cong; map-const) open import Data.Vector.Bisemimodule R.semiring using (_∙_ ; ∙-cong) -open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; ⟨⟩; _++_; module ≊; _≊_) +open import Data.Vector.Raw using (⟨⟩) +open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; module ≊; _≊_) open import Data.Vector.Monoid R.+-monoid using () renaming (⟨ε⟩ to ⟨0⟩) open import Data.Vector.Vec using (replicate-++) open import Function using (_∘_) @@ -41,13 +43,13 @@ private A B C D E F : ℕ opaque - unfolding Vector _∙_ + unfolding _∙_ ∙-comm : (V W : Vector A) → V ∙ W ≈ W ∙ V ∙-comm [] [] = refl ∙-comm (x ∷ V) (w ∷ W) = +-cong (*-comm x w) (∙-comm V W) opaque - unfolding _[_] [_]_ _ᵀ []ᵥ ⟨⟩ _∷ₕ_ _≊_ _≋_ _∷ᵥ_ + unfolding _[_] [_]_ _ᵀ []ᵥ _∷ₕ_ _≋_ _∷ᵥ_ [-]-ᵀ : (M : Matrix A B) (V : Vector A) → M [ V ] ≊ [ V ] (M ᵀ) [-]-ᵀ [] V = ≊.sym (≊.reflexive ([-]-[]ᵥ V)) [-]-ᵀ (M₀ ∷ M) V = begin @@ -60,7 +62,7 @@ opaque open ≈-Reasoning (Vectorₛ _) opaque - unfolding []ᵥ mapRows ⟨⟩ _∷ₕ_ _∷ᵥ_ _ᵀ + unfolding []ᵥ mapRows _∷ₕ_ _∷ᵥ_ _ᵀ _≋_ ·-ᵀ : {A B C : ℕ} (M : Matrix A B) @@ -211,7 +213,7 @@ opaque → ((I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N) ᵀ ≋ (I ≑ 𝟎) · M ᵀ ∥ (𝟎 ≑ I) · N ᵀ ᵀ-resp-⊗ {M = M} {N = N} = begin - ((I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N) ᵀ ≈⟨ -ᵀ-cong (≋⊗ M N) ⟩ + ((I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N) ᵀ ≈⟨ ᵀ-cong (≋⊗ M N) ⟩ ((M ≑ 𝟎) ∥ (𝟎 ≑ N)) ᵀ ≡⟨ ≡.cong (_ᵀ) (∥-≑ M 𝟎 𝟎 N) ⟨ ((M ∥ 𝟎) ≑ (𝟎 ∥ N)) ᵀ ≡⟨ ≑-ᵀ (M ∥ 𝟎) (𝟎 ∥ N) ⟩ (M ∥ 𝟎) ᵀ ∥ (𝟎 ∥ N) ᵀ ≡⟨ ≡.cong₂ _∥_ (∥-ᵀ M 𝟎) (∥-ᵀ 𝟎 N) ⟩ @@ -311,7 +313,7 @@ Mat-DaggerCocartesian = record { _† = λ M → M ᵀ ; †-identity = ≋.reflexive Iᵀ ; †-homomorphism = λ {f = f} {g} → ·-ᵀ f g - ; †-resp-≈ = -ᵀ-cong + ; †-resp-≈ = ᵀ-cong ; †-involutive = ᵀ-involutive } ; λ≅† = ≋λᵀ @@ -344,7 +346,7 @@ p₂-i₂ = begin open ≈-Reasoning (Matrixₛ _ _) opaque - unfolding 𝟎 ⟨⟩ + unfolding 𝟎 mapRows []ᵥ·[]ₕ : []ᵥ · []ₕ ≡ 𝟎 {A} {B} []ᵥ·[]ₕ {A} {B} = begin map ([_] []ₕ) []ᵥ ≡⟨ map-cong (λ { [] → [⟨⟩]-[]ₕ }) []ᵥ ⟩ diff --git a/Data/Matrix/Transform.agda b/Data/Matrix/Transform.agda index 87b8020..9c9fb23 100644 --- a/Data/Matrix/Transform.agda +++ b/Data/Matrix/Transform.agda @@ -12,19 +12,25 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Data.Vec.Relation.Binary.Pointwise.Inductive as PW open import Data.Nat using (ℕ) -open import Data.Vec using (Vec; map; replicate; zipWith) +open import Data.Vec using (Vec; map; replicate; zipWith; _++_) open import Data.Vec.Properties using (map-id; map-const; map-∘; zipWith-replicate; zipWith-replicate₁; map-replicate; map-cong) open import Relation.Binary.PropositionalEquality as ≡ using (_≗_; _≡_; module ≡-Reasoning) open import Function using (id; _∘_) -open import Data.Matrix.Core R.setoid +open import Data.Matrix.Raw using - ( Matrix; Matrixₛ; _≋_; ≋-isEquiv; _ᵀ; _∷ₕ_; []ᵥ; []ₕ; []ᵥ-ᵀ; mapRows - ; _ᵀᵀ; []ᵥ-!; ∷ₕ-ᵀ; ∷ₕ-cong; module ≋; -ᵀ-cong; _∥_; []ᵥ-∥; headₕ; tailₕ; head-∷-tailₕ; ∷ₕ-∥ + ( _ᵀ; _∷ₕ_; []ᵥ; []ₕ; []ᵥ-ᵀ; mapRows + ; _ᵀᵀ; []ᵥ-!; ∷ₕ-ᵀ; _∥_; []ᵥ-∥; headₕ; tailₕ; head-∷-tailₕ; ∷ₕ-∥ ; _≑_; []ᵥ-≑; ∷ₕ-≑ ) +open import Data.Matrix.Core R.setoid + using + ( Matrix; Matrixₛ; _≋_; ≋-isEquiv + ; ∷ₕ-cong; module ≋; ᵀ-cong + ) open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; _[+]_) -open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; ⟨⟩; module ≊; _≊_; _++_; ⟨⟩-++) +open import Data.Vector.Raw using (⟨⟩; ⟨⟩-++) +open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; module ≊; _≊_) open import Data.Vector.Vec using (zipWith-map; map-zipWith; zipWith-map-map) open import Data.Vector.Monoid R.+-monoid using (_⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ) renaming (⟨ε⟩ to ⟨0⟩) open import Data.Vector.Bisemimodule R using (_∙_; ∙-cong; ∙-zeroˡ; ∙-zeroʳ; _⟨_⟩; *-∙ˡ; *-∙ʳ; ∙-distribˡ; ∙-distribʳ) @@ -40,11 +46,11 @@ private opaque - unfolding Matrix + unfolding _≋_ opaque - unfolding Vector + -- unfolding Vector _[_] : Matrix n m → Vector n → Vector m _[_] M V = map (_∙ V) M @@ -59,7 +65,7 @@ opaque -[-]-cong₁ {n} {m} {M} {M′} ≋M V = PW.map⁺ (λ ≊V → ∙-cong ≊V ≊.refl) ≋M [-]--cong : {x y : Vector m} {A B : Matrix n m} → x ≊ y → A ≋ B → [ x ] A ≊ [ y ] B - [-]--cong ≋V A≋B = PW.map⁺ (∙-cong ≋V) (-ᵀ-cong A≋B) + [-]--cong ≋V A≋B = PW.map⁺ (∙-cong ≋V) (ᵀ-cong A≋B) opaque @@ -85,7 +91,7 @@ opaque opaque - unfolding Matrix Vector + unfolding _≋_ -- The identity matrix I : Matrix n n @@ -137,7 +143,7 @@ opaque open ≈-Reasoning setoid opaque - unfolding Vector [_]_ I _∙_ ⟨0⟩ mapRows _ᵀ []ᵥ + unfolding [_]_ I _∙_ ⟨0⟩ mapRows _ᵀ []ᵥ [-]I : {n : ℕ} (V : Vector n) → [ V ] I ≊ V [-]I {zero} [] = ≊.refl [-]I {suc n} (x ∷ V) = begin @@ -155,7 +161,7 @@ opaque open ≈-Reasoning (Vectorₛ (suc n)) opaque - unfolding _≊_ I _[_] _∙_ _≋_ _∷ₕ_ ⟨0⟩ + unfolding I _[_] _∙_ _≋_ _∷ₕ_ ⟨0⟩ I[-] : {n : ℕ} (V : Vector n) → I [ V ] ≊ V I[-] {zero} [] = PW.[] I[-] {suc n} (x ∷ V) = hd PW.∷ tl @@ -223,7 +229,7 @@ opaque opaque - unfolding _++_ _∙_ + unfolding _∙_ ∙-++ : (W Y : Vector A) (X Z : Vector B) → (W ++ X) ∙ (Y ++ Z) ≈ W ∙ Y + X ∙ Z ∙-++ [] [] X Z = sym (+-identityˡ (X ∙ Z)) @@ -236,7 +242,7 @@ opaque opaque - unfolding _⊕_ ⟨⟩ [_]_ + unfolding _⊕_ [_]_ [++]-≑ : (V : Vector B) @@ -248,10 +254,10 @@ opaque [++]-≑ {B} {C} {zero} V W M N rewrite []ᵥ-! M rewrite []ᵥ-! N = begin - [ V ++ W ] ([]ᵥ {B} ≑ []ᵥ) ≡⟨ ≡.cong ([ V ++ W ]_) []ᵥ-≑ ⟩ - [ V ++ W ] []ᵥ ≡⟨ [-]-[]ᵥ (V ++ W) ⟩ - ⟨⟩ ⊕ ⟨⟩ ≡⟨ ≡.cong₂ _⊕_ ([-]-[]ᵥ V) ([-]-[]ᵥ W) ⟨ - [ V ] []ᵥ ⊕ [ W ] []ᵥ ∎ + [ V ++ W ] ([]ᵥ {m = B} ≑ []ᵥ) ≡⟨ ≡.cong ([ V ++ W ]_) ([]ᵥ-≑ {B}) ⟩ + [ V ++ W ] []ᵥ ≡⟨ [-]-[]ᵥ (V ++ W) ⟩ + ⟨⟩ ⊕ ⟨⟩ ≡⟨ ≡.cong₂ _⊕_ ([-]-[]ᵥ V) ([-]-[]ᵥ W) ⟨ + [ V ] []ᵥ ⊕ [ W ] []ᵥ ∎ where open ≈-Reasoning (Vectorₛ 0) [++]-≑ {B} {C} {suc A} V W M N @@ -272,13 +278,13 @@ opaque unfolding []ₕ []ᵥ [_]_ ⟨0⟩ _∙_ _ᵀ - [⟨⟩]-[]ₕ : [ ⟨⟩ ] ([]ₕ {A}) ≡ ⟨0⟩ {A} + [⟨⟩]-[]ₕ : [ ⟨⟩ ] ([]ₕ {n = A}) ≡ ⟨0⟩ {A} [⟨⟩]-[]ₕ {zero} = ≡.refl [⟨⟩]-[]ₕ {suc A} = ≡.cong (0# ∷_) [⟨⟩]-[]ₕ opaque - unfolding Vector ⟨⟩ ⟨0⟩ []ᵥ [_]_ _ᵀ _∷ₕ_ 𝟎 _≊_ + unfolding ⟨0⟩ []ᵥ [_]_ _ᵀ _∷ₕ_ 𝟎 [-]-𝟎 : (V : Vector A) → [ V ] (𝟎 {B}) ≊ ⟨0⟩ [-]-𝟎 {A} {zero} V = ≊.reflexive (≡.cong (map (V ∙_)) 𝟎ᵀ) @@ -292,7 +298,7 @@ opaque opaque - unfolding ⟨0⟩ ⟨⟩ [_]_ + unfolding ⟨0⟩ [_]_ [⟨0⟩]- : (M : Matrix A B) → [ ⟨0⟩ ] M ≊ ⟨0⟩ [⟨0⟩]- {zero} M rewrite []ᵥ-! M = ≊.reflexive ([-]-[]ᵥ ⟨0⟩) diff --git a/Data/Matrix/Vec.agda b/Data/Matrix/Vec.agda index e0312d4..b191052 100644 --- a/Data/Matrix/Vec.agda +++ b/Data/Matrix/Vec.agda @@ -2,10 +2,9 @@ module Data.Matrix.Vec where -open import Relation.Binary.PropositionalEquality using (_≡_) -open import Level using (Level) open import Data.Nat using (ℕ) open import Data.Vec using (Vec; replicate; zipWith) +open import Level using (Level) private variable diff --git a/Data/Vector/Bifunctor.agda b/Data/Vector/Bifunctor.agda new file mode 100644 index 0000000..51e8970 --- /dev/null +++ b/Data/Vector/Bifunctor.agda @@ -0,0 +1,57 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Data.Vector.Bifunctor {c : Level} where + +open import Categories.Category.Instance.Nat using (Natop) +open import Categories.Category.Instance.Sets using (Sets) +open import Categories.Functor.Bifunctor using (Bifunctor) +open import Function using (_∘_) +open import Data.Nat using (ℕ) +open import Data.Fin using (Fin) +open import Data.Product using (_,_) +open import Data.Vec using (Vec; map; tabulate; lookup) +open import Data.Vec.Properties using (map-id; map-∘; map-cong; tabulate∘lookup; lookup∘tabulate; tabulate-cong; lookup-map; tabulate-∘) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) + +naturality + : {A B : Set c} {f : A → B} {n m : ℕ} {g : Fin m → Fin n} (v : Vec A n) + → map f (tabulate (λ i → lookup v (g i))) ≡ tabulate (λ i → lookup (map f v) (g i)) +naturality {A} {B} {f} {n} {m} {g} v = begin + map f (tabulate (λ i → lookup v (g i))) ≡⟨ tabulate-∘ f (λ i → lookup v (g i)) ⟨ + tabulate (λ i → f (lookup v (g i))) ≡⟨ tabulate-cong (λ i → (lookup-map (g i) f v)) ⟨ + tabulate (λ i → lookup (map f v) (g i)) ∎ + where + open ≡-Reasoning + +bimap : {A B : Set c} {n m : ℕ} (f : A → B) (g : Fin m → Fin n) → Vec A n → Vec B m +bimap f g v = map f (tabulate (λ i → lookup v (g i))) + +Vec₂ : Bifunctor (Sets c) Natop (Sets c) +Vec₂ = record + { F₀ = λ (A , n) → Vec A n + ; F₁ = λ (f , g) v → bimap f g v + ; identity = λ v → ≡.trans (map-id (tabulate (λ i → lookup v i))) (tabulate∘lookup v) + ; homomorphism = λ {_ _ _} {(f , f′)} {(g , g′)} → homomorphism f g f′ g′ + ; F-resp-≈ = λ (f≗g , f′≗g′) v → ≡.trans (map-cong f≗g (tabulate (λ i → lookup v _))) (≡.cong (map _) (tabulate-cong (λ i → (≡.cong (lookup v) (f′≗g′ i))))) + } + where + homomorphism + : {X Y Z : Set c} + (f : X → Y) + (g : Y → Z) + {x y z : ℕ} + (f′ : Fin y → Fin x) + (g′ : Fin z → Fin y) + (v : Vec X x) + → bimap (g ∘ f) (f′ ∘ g′) v ≡ bimap g g′ (bimap f f′ v) + homomorphism f g f′ g′ v = begin + map (g ∘ f) (tabulate (λ i → lookup v (f′ (g′ i)))) ≡⟨ map-∘ g f (tabulate (λ i → lookup v (f′ (g′ i)))) ⟩ + map g (map f (tabulate (λ i → lookup v (f′ (g′ i))))) ≡⟨ ≡.cong (map g) (naturality v) ⟩ + map g (tabulate (λ i → lookup (map f v) (f′ (g′ i)))) ≡⟨ ≡.cong (map g) (tabulate-cong (λ i → (lookup∘tabulate (λ i₁ → lookup (map f v) (f′ i₁)) (g′ i)))) ⟨ + map g (tabulate (λ i → lookup (tabulate (λ i₁ → lookup (map f v) (f′ i₁))) (g′ i))) + ≡⟨ ≡.cong (map g) (tabulate-cong (λ i → ≡.cong (λ h → lookup h (g′ i)) (naturality v))) ⟨ + map g (tabulate (λ i → lookup (map f (tabulate (λ i₁ → lookup v (f′ i₁)))) (g′ i))) ∎ + where + open ≡-Reasoning diff --git a/Data/Vector/Bisemimodule.agda b/Data/Vector/Bisemimodule.agda index e38536a..4121b91 100644 --- a/Data/Vector/Bisemimodule.agda +++ b/Data/Vector/Bisemimodule.agda @@ -32,8 +32,6 @@ private opaque - unfolding Vector - -- Scaling a vector from the left _⟨_⟩ : Carrier → Vector n → Vector n _⟨_⟩ r = map (r *_) diff --git a/Data/Vector/Core.agda b/Data/Vector/Core.agda index a430f12..c002676 100644 --- a/Data/Vector/Core.agda +++ b/Data/Vector/Core.agda @@ -6,101 +6,104 @@ open import Relation.Binary using (Setoid; Rel; IsEquivalence) module Data.Vector.Core {c ℓ : Level} (S : Setoid c ℓ) where -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open Setoid S + import Data.Vec.Relation.Binary.Pointwise.Inductive as PW open import Categories.Category.Instance.Nat using (Natop) open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor using (Functor) open import Data.Fin using (Fin) -open import Data.Nat using (ℕ; _+_) -open import Data.Setoid using (∣_∣) -open import Data.Vec as Vec using (Vec; lookup; tabulate) +open import Data.Nat using (ℕ) +open import Data.Vec using (Vec; lookup; tabulate; head; tail; map; _++_; replicate; zipWith) open import Data.Vec.Properties using (tabulate∘lookup; lookup∘tabulate; tabulate-cong) open import Data.Vec.Relation.Binary.Equality.Setoid S using (_≋_; ≋-isEquivalence) +open import Data.Vector.Raw using (module Relation) open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) open Func -open Setoid S -open Fin -open Vec.Vec +open ℕ + +Vector : ℕ → Set c +Vector = Vec Carrier private variable - n A B C : ℕ - -opaque - - -- Vectors over the rig - Vector : ℕ → Set c - Vector = Vec ∣ S ∣ + n m A B C : ℕ - -- Pointwise equivalence of vectors - _≊_ : Rel (Vector n) (c ⊔ ℓ) - _≊_ A B = A ≋ B +-- Pointwise equivalence of vectors +_≊_ : Rel (Vector n) (c ⊔ ℓ) +_≊_ A B = A ≋ B - -- Pointwise equivalence is an equivalence relation - ≊-isEquiv : IsEquivalence (_≊_ {n}) - ≊-isEquiv {n} = ≋-isEquivalence n - - _++_ : Vector A → Vector B → Vector (A + B) - _++_ = Vec._++_ - - ⟨⟩ : Vector 0 - ⟨⟩ = [] - - ⟨⟩-! : (V : Vector 0) → V ≡ ⟨⟩ - ⟨⟩-! [] = ≡.refl +infix 4 _≊_ - ⟨⟩-++ : (V : Vector A) → ⟨⟩ ++ V ≡ V - ⟨⟩-++ V = ≡.refl +-- Pointwise equivalence is an equivalence relation +≊-isEquiv : IsEquivalence (_≊_ {n}) +≊-isEquiv {n} = ≋-isEquivalence n -- A setoid of vectors for every natural number Vectorₛ : ℕ → Setoid c (c ⊔ ℓ) Vectorₛ n = record - { Carrier = Vector n - ; _≈_ = _≊_ - ; isEquivalence = ≊-isEquiv + { Carrier = Vector n + ; _≈_ = _≊_ + ; isEquivalence = ≊-isEquiv } module ≊ {n} = Setoid (Vectorₛ n) -infix 4 _≊_ - -opaque - - unfolding Vector - - pull : (Fin B → Fin A) → Vectorₛ A ⟶ₛ Vectorₛ B - pull f .to v = tabulate (λ i → lookup v (f i)) - pull f .cong ≊v = PW.tabulate⁺ (λ i → PW.lookup ≊v (f i)) +pull : (Fin B → Fin A) → Vectorₛ A ⟶ₛ Vectorₛ B +pull f .to v = tabulate (λ i → lookup v (f i)) +pull f .cong ≊v = PW.tabulate⁺ (λ i → PW.lookup ≊v (f i)) - pull-id : {v : Vector n} → pull id ⟨$⟩ v ≊ v - pull-id {v} = ≊.reflexive (tabulate∘lookup v) +pull-id : {v : Vector n} → pull id ⟨$⟩ v ≊ v +pull-id {v} = ≊.reflexive (tabulate∘lookup v) - pull-∘ - : {f : Fin B → Fin A} - {g : Fin C → Fin B} - {v : Vector A} - → pull (f ∘ g) ⟨$⟩ v ≊ pull g ⟨$⟩ (pull f ⟨$⟩ v) - pull-∘ {f} {g} {v} = ≊.reflexive (≡.sym (tabulate-cong (λ i → lookup∘tabulate (lookup v ∘ f) (g i)))) +pull-∘ + : {f : Fin B → Fin A} + {g : Fin C → Fin B} + {v : Vector A} + → pull (f ∘ g) ⟨$⟩ v ≊ pull g ⟨$⟩ (pull f ⟨$⟩ v) +pull-∘ {f} {g} {v} = ≊.reflexive (≡.sym (tabulate-cong (λ i → lookup∘tabulate (lookup v ∘ f) (g i)))) - pull-cong - : {f g : Fin B → Fin A} - → f ≗ g - → {v : Vector A} - → pull f ⟨$⟩ v ≊ pull g ⟨$⟩ v - pull-cong f≗g {v} = ≊.reflexive (tabulate-cong (λ i → ≡.cong (lookup v) (f≗g i))) +pull-cong + : {f g : Fin B → Fin A} + → f ≗ g + → {v : Vector A} + → pull f ⟨$⟩ v ≊ pull g ⟨$⟩ v +pull-cong f≗g {v} = ≊.reflexive (tabulate-cong (λ i → ≡.cong (lookup v) (f≗g i))) -- Copying, deleting, and rearranging elements -- of a vector according to a function on indices -- gives a contravariant functor from Nat to Setoids Pull : Functor Natop (Setoids c (c ⊔ ℓ)) Pull = record - { F₀ = Vectorₛ - ; F₁ = pull - ; identity = pull-id - ; homomorphism = pull-∘ - ; F-resp-≈ = pull-cong - } + { F₀ = Vectorₛ + ; F₁ = pull + ; identity = pull-id + ; homomorphism = λ {f = f} {g v} → pull-∘ {f = f} {g} {v} + ; F-resp-≈ = pull-cong + } + +module Cong where + + open Relation {R = _≈_} + + head-cong : {V₁ V₂ : Vector (suc n)} → V₁ ≊ V₂ → head V₁ ≈ head V₂ + head-cong = R-head + + tail-cong : {V₁ V₂ : Vector (suc n)} → V₁ ≊ V₂ → tail V₁ ≊ tail V₂ + tail-cong = R-tail + + ++-cong + : {V₁ V₂ : Vector m} + {W₁ W₂ : Vector n} + → V₁ ≊ V₂ + → W₁ ≊ W₂ + → V₁ ++ W₁ ≊ V₂ ++ W₂ + ++-cong = R-++ + + replicate-cong : {n : ℕ} {x y : Carrier} → x ≈ y → replicate n x ≋ replicate n y + replicate-cong = R-replicate + +open Cong public diff --git a/Data/Vector/Endofunctor.agda b/Data/Vector/Endofunctor.agda deleted file mode 100644 index a9b2905..0000000 --- a/Data/Vector/Endofunctor.agda +++ /dev/null @@ -1,68 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Data.Nat using (ℕ) -open import Level using (Level; _⊔_) - --- The endofunctor in setoids sending A to Vector A n for a fixed n -module Data.Vector.Endofunctor (n : ℕ) {c ℓ : Level} where - -import Data.Vec as Vec - -open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Functor using (Functor) -open import Data.Vec.Properties using (map-id; map-∘) -open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺) -open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊) -open import Function using (Func; _⟶ₛ_; _⟨$⟩_) -open import Function.Construct.Composition using () renaming (function to compose) -open import Function.Construct.Identity using () renaming (function to Id) -open import Relation.Binary using (Setoid) - -open Func - -opaque - unfolding Vector - map : {c ℓ : Level} {A B : Setoid c ℓ} → A ⟶ₛ B → Vectorₛ A n ⟶ₛ Vectorₛ B n - map f .to = Vec.map (to f) - map f .cong = map⁺ (cong f) - -abstract opaque - - unfolding map - - identity - : {A : Setoid c ℓ} - {V : Vector A n} - (open Core A using (_≊_)) - → map (Id A) ⟨$⟩ V ≊ V - identity {A} {V} = ≊.reflexive A (map-id V) - - homomorphism - : {X Y Z : Setoid c ℓ} - {f : X ⟶ₛ Y} - {g : Y ⟶ₛ Z} - {V : Vector X n} - (open Core Z using (_≊_)) - → map (compose f g) ⟨$⟩ V ≊ map g ⟨$⟩ (map f ⟨$⟩ V) - homomorphism {_} {_} {Z} {f} {g} {V} = ≊.reflexive Z (map-∘ (to g) (to f) V) - - F-resp-≈ - : {A B : Setoid c ℓ} - {f g : A ⟶ₛ B} - → ({x : Setoid.Carrier A} → (B Setoid.≈ to f x) (to g x)) - → {V : Vector A n} - (open Core B using (_≊_)) - → map f ⟨$⟩ V ≊ map g ⟨$⟩ V - F-resp-≈ {A} {B} {_} {g} f≈g {V} = map⁺ (λ x≈y → B.trans f≈g (cong g x≈y)) (≊.refl A) - where - module B = Setoid B - --- only a true endofunctor when c ≤ ℓ -Vec : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) -Vec = record - { F₀ = λ A → Vectorₛ A n - ; F₁ = map - ; identity = identity - ; homomorphism = homomorphism - ; F-resp-≈ = F-resp-≈ - } diff --git a/Data/Vector/Endofunctor/Monoid.agda b/Data/Vector/Endofunctor/Monoid.agda new file mode 100644 index 0000000..217c754 --- /dev/null +++ b/Data/Vector/Endofunctor/Monoid.agda @@ -0,0 +1,106 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Nat using (ℕ) +open import Level using (Level; _⊔_) + +-- The endofunctor in monoids sending A to Vectorₘ A n for a fixed n +module Data.Vector.Endofunctor.Monoid (n : ℕ) {c ℓ : Level} where + +import Data.Vec as Vec +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Algebra using (Monoid) +open import Categories.Category using (Category; _[_∘_]; _[_≈_]) +open import Categories.Functor using (Functor) +open import Category.Instance.Monoids using (Monoids; MonoidHomomorphism; mk-⇒) +open import Data.Monoid using (toMonoid) +open import Data.Vec.Properties using (map-replicate) +open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺) +open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊; replicate-cong) +open import Data.Vector.Endofunctor.Setoid as Endo using (mapₛ; zipWith-cong) +open import Data.Vector.Monoid as Mon using (Vectorₘ; ⟨ε⟩) renaming (_⊕_ to _[_⊕_]) +open import Data.Vector.Vec using (map-zipWith; zipWith-map-map) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_) + +open Func +open MonoidHomomorphism + +private module _ {M N : Monoid c ℓ} (f : MonoidHomomorphism c ℓ M N) where + + private + module M = Monoid M + module N = Monoid N + + open Core N.setoid using (_≊_) + open ≈-Reasoning (Vectorₛ N.setoid n) + + opaque + unfolding _[_⊕_] + map-⊕ + : (W V : Vector M.setoid n) + → mapₛ n (func f) ⟨$⟩ (M [ W ⊕ V ]) + ≊ N [ mapₛ n (func f) ⟨$⟩ W ⊕ mapₛ n (func f) ⟨$⟩ V ] + map-⊕ W V = begin + Vec.map ⟦ f ⟧ (Vec.zipWith M._∙_ W V) ≡⟨ map-zipWith ⟦ f ⟧ M._∙_ W V ⟩ + Vec.zipWith (λ x y → ⟦ f ⟧ (x M.∙ y)) W V ≈⟨ zipWith-cong n N.setoid (homo f) W V ⟩ + Vec.zipWith (λ x y → ⟦ f ⟧ x N.∙ ⟦ f ⟧ y) W V ≡⟨ zipWith-map-map ⟦ f ⟧ ⟦ f ⟧ N._∙_ W V ⟩ + Vec.zipWith N._∙_ (Vec.map ⟦ f ⟧ W) (Vec.map ⟦ f ⟧ V) ∎ + + opaque + unfolding ⟨ε⟩ + map-⟨ε⟩ : mapₛ n (func f) ⟨$⟩ (Mon.⟨ε⟩ M) ≊ Mon.⟨ε⟩ N + map-⟨ε⟩ = begin + Vec.map (to (func f)) (Vec.replicate n M.ε) ≡⟨ map-replicate (to (func f)) M.ε n ⟩ + Vec.replicate n (func f ⟨$⟩ M.ε) ≈⟨ replicate-cong N.setoid (ε-homo f) ⟩ + Vec.replicate n N.ε ∎ + +mapₘ : {M N : Monoid c ℓ} → MonoidHomomorphism c ℓ M N → MonoidHomomorphism c (c ⊔ ℓ) (Vectorₘ M n) (Vectorₘ N n) +mapₘ {M} {N} f = mk-⇒ record + { ⟦_⟧ = to (mapₛ n (func f)) + ; isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = map⁺ (⟦⟧-cong f) + } + ; homo = map-⊕ f + } + ; ε-homo = map-⟨ε⟩ f + } + } + +open Category using (id) + +abstract + + identity + : {A : Monoid c ℓ} + → Monoids c (c ⊔ ℓ) [ mapₘ (id (Monoids c ℓ) {A}) ≈ id (Monoids c (c ⊔ ℓ)) ] + identity {A} V = Endo.identity n {c} {ℓ} {Monoid.setoid A} + + homomorphism + : {X Y Z : Monoid c ℓ} + {f : MonoidHomomorphism c ℓ X Y} + {g : MonoidHomomorphism c ℓ Y Z} + → Monoids c (c ⊔ ℓ) [ mapₘ (Monoids c ℓ [ g ∘ f ]) ≈ Monoids c (c ⊔ ℓ) [ mapₘ g ∘ mapₘ f ] ] + homomorphism {X} {Y} {Z} {f} {g} V = Endo.homomorphism n {c} {ℓ} {setoid X} {setoid Y} {setoid Z} {func f} {func g} {V} + where + open Monoid using (setoid) + + F-resp-≈ + : {A B : Monoid c ℓ} + {f g : MonoidHomomorphism c ℓ A B} + → Monoids c ℓ [ f ≈ g ] + → Monoids c (c ⊔ ℓ) [ mapₘ f ≈ mapₘ g ] + F-resp-≈ {A} {B} {f} {g} f≈g V = Endo.F-resp-≈ n {c} {ℓ} {setoid A} {setoid B} {func f} {func g} (λ {x} → f≈g x) + where + open Monoid using (setoid) + +-- only a true endofunctor when c ≤ ℓ +Vec : Functor (Monoids c ℓ) (Monoids c (c ⊔ ℓ)) +Vec = record + { F₀ = λ M → Vectorₘ M n + ; F₁ = mapₘ + ; identity = λ {M} → identity {M} + ; homomorphism = λ {f = f} {g} → homomorphism {f = f} {g} + ; F-resp-≈ = λ {f = f} {g} → F-resp-≈ {f = f} {g} + } diff --git a/Data/Vector/Endofunctor/Setoid.agda b/Data/Vector/Endofunctor/Setoid.agda new file mode 100644 index 0000000..09f8f69 --- /dev/null +++ b/Data/Vector/Endofunctor/Setoid.agda @@ -0,0 +1,81 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Nat using (ℕ) +open import Level using (Level; _⊔_) + +-- The endofunctor in setoids sending A to Vector A n for a fixed n +module Data.Vector.Endofunctor.Setoid (n : ℕ) {c ℓ : Level} where + +import Data.Vec as Vec + +open import Categories.Category using (_[_≈_]) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.Setoid using (∣_∣) +open import Data.Vec.Properties using (map-id; map-∘) +open import Data.Vec.Relation.Binary.Equality.Setoid using () renaming (_≋_ to _[_≋_]) +open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW using (map⁺; Pointwise) +open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊) +open import Data.Vector.Raw using (R-zipWith) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_) +open import Function.Construct.Composition using () renaming (function to compose) +open import Function.Construct.Identity using () renaming (function to Id) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open Func +open ℕ +open Vec.Vec +open Pointwise + +mapₛ : {A B : Setoid c ℓ} → A ⟶ₛ B → Vectorₛ A n ⟶ₛ Vectorₛ B n +mapₛ f .to = Vec.map (to f) +mapₛ f .cong = map⁺ (cong f) + +abstract + + identity + : {A : Setoid c ℓ} + {V : Vector A n} + (open Core A using (_≊_)) + → mapₛ (Id A) ⟨$⟩ V ≊ V + identity {A} {V} = ≊.reflexive A (map-id V) + + homomorphism + : {X Y Z : Setoid c ℓ} + {f : X ⟶ₛ Y} + {g : Y ⟶ₛ Z} + {V : Vector X n} + (open Core Z using (_≊_)) + → mapₛ (compose f g) ⟨$⟩ V ≊ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ V) + homomorphism {_} {_} {Z} {f} {g} {V} = ≊.reflexive Z (map-∘ (to g) (to f) V) + + F-resp-≈ + : {A B : Setoid c ℓ} + {f g : A ⟶ₛ B} + → Setoids c ℓ [ f ≈ g ] + → Setoids c (c ⊔ ℓ) [ mapₛ f ≈ mapₛ g ] + F-resp-≈ {A} {B} {_} {g} f≈g {V} = map⁺ (λ x≈y → B.trans f≈g (cong g x≈y)) (≊.refl A) + where + module B = Setoid B + +-- only a true endofunctor when c ≤ ℓ +Vec : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) +Vec = record + { F₀ = λ A → Vectorₛ A n + ; F₁ = mapₛ + ; identity = λ {A} → identity {A} + ; homomorphism = λ {f = f} {g} → homomorphism {f = f} {g} + ; F-resp-≈ = λ {f = f} {g} → F-resp-≈ {f = f} {g} + } + +zipWith-cong + : {A B : Set c} + (C : Setoid c ℓ) + (let module C = Setoid C) + {f g : A → B → ∣ C ∣} + → (∀ x y → f x y C.≈ g x y) + → (xs : Vec.Vec A n) + (ys : Vec.Vec B n) + → C [ Vec.zipWith f xs ys ≋ Vec.zipWith g xs ys ] +zipWith-cong C f≈g xs ys = R-zipWith {R = _≡_} {S = _≡_} (λ { ≡.refl ≡.refl → f≈g _ _}) (PW.refl ≡.refl) (PW.refl ≡.refl) diff --git a/Data/Vector/Monoid.agda b/Data/Vector/Monoid.agda index 5906bf9..da09de9 100644 --- a/Data/Vector/Monoid.agda +++ b/Data/Vector/Monoid.agda @@ -24,8 +24,6 @@ private opaque - unfolding Vector - -- Sum the elements of a vector sum : Vector n → M.Carrier sum = foldr′ _∙_ ε @@ -36,8 +34,6 @@ opaque opaque - unfolding Vector - -- Pointwise sum of two vectors _⊕_ : Vector n → Vector n → Vector n _⊕_ = zipWith _∙_ @@ -54,8 +50,6 @@ infixl 6 _⊕_ opaque - unfolding Vector - -- The identity vector ⟨ε⟩ : Vector n ⟨ε⟩ {n} = replicate n ε @@ -119,7 +113,7 @@ open ≡-Reasoning opaque - unfolding pull _⊕_ + unfolding _⊕_ pull-⊕ : {f : Fin A → Fin B} (V W : Vector B) → pull f ⟨$⟩ (V ⊕ W) ≡ (pull f ⟨$⟩ V) ⊕ (pull f ⟨$⟩ W) pull-⊕ {A} {B} {f} V W = begin @@ -132,7 +126,7 @@ opaque opaque - unfolding pull ⟨ε⟩ + unfolding ⟨ε⟩ pull-⟨ε⟩ : {f : Fin A → Fin B} → pull f ⟨$⟩ ⟨ε⟩ ≡ ⟨ε⟩ pull-⟨ε⟩ {f = f} = begin @@ -157,7 +151,7 @@ opaque {g : Fin C → Fin B} {v : Vector A} → arr (pullₘ (f ∘ g)) ⟨$⟩ v ≊ arr (pullₘ g) ⟨$⟩ (arr (pullₘ f) ⟨$⟩ v) - pullₘ-∘ = S.pull-∘ + pullₘ-∘ {f = f} {g} {v} = S.pull-∘ {f = f} {g} {v} pullₘ-cong : {f g : Fin B → Fin A} diff --git a/Data/Vector/Raw.agda b/Data/Vector/Raw.agda new file mode 100644 index 0000000..c333553 --- /dev/null +++ b/Data/Vector/Raw.agda @@ -0,0 +1,95 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Vector.Raw where + +open import Data.Nat using (ℕ; _+_) +open import Data.Vec using (Vec; head; tail; map; _++_; replicate; zipWith) +open import Data.Vec.Properties using (map-replicate) +open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise) +open import Level using (Level) +open import Relation.Binary using (REL) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +private + variable + n m : ℕ + a ℓ ℓ₁ ℓ₂ : Level + A B C D E F : Set a + +open ℕ +open Vec + +⟨⟩ : Vec A 0 +⟨⟩ = [] + +⟨⟩-! : (V : Vec A 0) → V ≡ ⟨⟩ +⟨⟩-! [] = ≡.refl + +⟨⟩-++ : {n : ℕ} (V : Vec A n) → ⟨⟩ ++ V ≡ V +⟨⟩-++ V = ≡.refl + +module Natural {n : ℕ} (f : A → B) where + + α-head : (V : Vec A (suc n)) → f (head V) ≡ head (map f V) + α-head (x ∷ _) = ≡.erefl (f x) + + α-tail : (V : Vec A (suc n)) → map f (tail V) ≡ tail (map f V) + α-tail (_ ∷ V) = ≡.erefl (map f V) + + α-replicate : {x : A} → map f (replicate n x) ≡ replicate n (f x) + α-replicate {x} = map-replicate f x n + +open Natural public + +open Pointwise + +module Relation {R : REL A B ℓ} where + + R-head + : {V₁ : Vec A (suc n)} + {V₂ : Vec B (suc n)} + → Pointwise R V₁ V₂ + → R (head V₁) (head V₂) + R-head (R-x ∷ _) = R-x + + R-tail + : {V₁ : Vec A (suc n)} + {V₂ : Vec B (suc n)} + → Pointwise R V₁ V₂ + → Pointwise R (tail V₁) (tail V₂) + R-tail (_ ∷ R-V) = R-V + + R-++ + : {R : REL A B ℓ} + {V₁ : Vec A m} + {V₂ : Vec B m} + {W₁ : Vec A n} + {W₂ : Vec B n} + → Pointwise R V₁ V₂ + → Pointwise R W₁ W₂ + → Pointwise R (V₁ ++ W₁) (V₂ ++ W₂) + R-++ [] R-W = R-W + R-++ (R-v ∷ R-V) R-W = R-v ∷ R-++ R-V R-W + + R-replicate : {x : A} {y : B} → R x y → Pointwise R (replicate n x) (replicate n y) + R-replicate {n = zero} _ = [] + R-replicate {n = suc n} xRy = xRy ∷ R-replicate xRy + +R-zipWith + : {W : Vec A n} + {X : Vec B n} + {Y : Vec C n} + {Z : Vec D n} + {R : REL A B ℓ₁} + {S : REL C D ℓ₂} + {T : REL E F ℓ} + {f : A → C → E} + {g : B → D → F} + → (∀ {w x y z} → R w x → S y z → T (f w y) (g x z)) + → Pointwise R W X + → Pointwise S Y Z + → Pointwise T (zipWith f W Y) (zipWith g X Z) +R-zipWith cong [] [] = [] +R-zipWith cong (wRx ∷ WRX) (ySz ∷ YSZ) = cong wRx ySz ∷ R-zipWith cong WRX YSZ + +open Relation public diff --git a/Data/Vector/Vec.agda b/Data/Vector/Vec.agda index 868571a..4367bdd 100644 --- a/Data/Vector/Vec.agda +++ b/Data/Vector/Vec.agda @@ -5,6 +5,8 @@ module Data.Vector.Vec where open import Data.Fin using (Fin) open import Data.Nat using (ℕ; _+_) open import Data.Vec using (Vec; tabulate; zipWith; replicate; map; _++_) +open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW using (Pointwise-≡⇒≡) +open import Data.Vector.Raw using (R-zipWith) open import Function using (_∘_) open import Level using (Level) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) @@ -71,3 +73,16 @@ zipWith-map-map → zipWith (λ x y → f x ⊕ g y) v w ≡ zipWith _⊕_ (map f v) (map g w) zipWith-map-map f g _⊕_ [] [] = ≡.refl zipWith-map-map f g _⊕_ (x ∷ v) (y ∷ w) = ≡.cong (f x ⊕ g y ∷_) (zipWith-map-map f g _⊕_ v w) + +zipWith-cong + : {f g : A → B → C} + → (∀ x y → f x y ≡ g x y) + → (xs : Vec A n) + (ys : Vec B n) + → zipWith f xs ys + ≡ zipWith g xs ys +zipWith-cong f≗g xs ys = + Pointwise-≡⇒≡ + (R-zipWith {R = _≡_} {S = _≡_} (λ { ≡.refl ≡.refl → f≗g _ _}) + (PW.refl ≡.refl) + (PW.refl ≡.refl)) |