diff options
Diffstat (limited to 'Data/Matrix')
| -rw-r--r-- | Data/Matrix/BaseChange.agda | 2 | ||||
| -rw-r--r-- | Data/Matrix/Cast.agda | 4 | ||||
| -rw-r--r-- | Data/Matrix/Category.agda | 28 | ||||
| -rw-r--r-- | Data/Matrix/Convert.agda | 18 | ||||
| -rw-r--r-- | Data/Matrix/Core.agda | 3 | ||||
| -rw-r--r-- | Data/Matrix/Dagger-2-Poset.agda | 7 | ||||
| -rw-r--r-- | Data/Matrix/Monoid.agda | 6 | ||||
| -rw-r--r-- | Data/Matrix/Raw.agda | 269 | ||||
| -rw-r--r-- | Data/Matrix/Semiadditive.agda | 108 | ||||
| -rw-r--r-- | Data/Matrix/SemiadditiveDagger.agda | 8 | ||||
| -rw-r--r-- | Data/Matrix/Transform.agda | 168 |
11 files changed, 376 insertions, 245 deletions
diff --git a/Data/Matrix/BaseChange.agda b/Data/Matrix/BaseChange.agda index 2135c13..04b9f9c 100644 --- a/Data/Matrix/BaseChange.agda +++ b/Data/Matrix/BaseChange.agda @@ -95,7 +95,7 @@ resp = cong (Mat.₁ func) ⟨ε⟩-homo {A} = MonoidHomomorphism.ε-homo (MonEndo.mapₘ A (mk-⇒ +-monoidHomomorphism)) opaque - unfolding I _ᵀ _∷ₕ_ Endo.mapₛ + 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 diff --git a/Data/Matrix/Cast.agda b/Data/Matrix/Cast.agda index 43c50c8..a0fa92f 100644 --- a/Data/Matrix/Cast.agda +++ b/Data/Matrix/Cast.agda @@ -7,7 +7,7 @@ module Data.Matrix.Cast {c ℓ : Level} (S : Setoid c ℓ) where module S = Setoid S -open import Data.Matrix.Raw using (_∥_; _≑_; _∷ₕ_; []ᵥ; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥; head-∷-tailₕ; headₕ; tailₕ) +open import Data.Matrix.Raw as 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) @@ -25,7 +25,7 @@ private opaque - unfolding Matrix + unfolding Raw.Matrix cast₁ : .(A ≡ B) → Matrix A C → Matrix B C cast₁ eq = map (castVec eq) diff --git a/Data/Matrix/Category.agda b/Data/Matrix/Category.agda index b4b0f23..717926a 100644 --- a/Data/Matrix/Category.agda +++ b/Data/Matrix/Category.agda @@ -12,7 +12,7 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Categories.Category using (Category) open import Categories.Category.Helper using (categoryHelper) -open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; _ᵀᵀ; _∥_; _≑_; mapRows) +open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; _ᵀᵀ; _∥_; _≑_; mapₕ; mapᵥ; ∷ᵥⁿ; ∷ₕⁿ; columns-∷ₕⁿ; ∷ᵥⁿ-ᵀ) 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⟩]-) @@ -32,23 +32,24 @@ open ℕ private variable n m p : ℕ - A B C D : ℕ + A B C D E : ℕ -- matrix multiplication _·_ : Matrix m p → Matrix n m → Matrix n p -_·_ A B = mapRows ([_] B) A +_·_ A B = ∷ᵥⁿ (mapₕ ([_] B) A) -- alternative form _·′_ : Matrix m p → Matrix n m → Matrix n p -_·′_ A B = mapRows (A [_]) (B ᵀ) ᵀ +_·′_ A B = ∷ₕⁿ (mapᵥ (A [_]) B) infixr 9 _·_ _·′_ ·-·′ : (A : Matrix m p) (B : Matrix n m) → A · B ≡ A ·′ B ·-·′ A B = begin - mapRows ([_] B) A ≡⟨ mapRows ([_] B) A ᵀᵀ ⟨ - mapRows ([_] B) A ᵀ ᵀ ≡⟨ ≡.cong (_ᵀ) (-[-]ᵀ A B) ⟨ - mapRows (A [_]) (B ᵀ) ᵀ ∎ + ∷ᵥⁿ (mapₕ ([_] B) A) ≡⟨ ≡.cong ∷ᵥⁿ (columns-∷ₕⁿ (mapₕ ([_] B) A)) ⟨ + ∷ₕⁿ (mapₕ ([_] B) A) ᵀ ≡⟨ ≡.cong _ᵀ (-[-]ᵀ A B) ⟨ + ∷ᵥⁿ (mapᵥ (A [_]) B) ᵀ ≡⟨ ∷ᵥⁿ-ᵀ (mapᵥ (A [_]) B) ⟩ + ∷ₕⁿ (mapᵥ (A [_]) B) ∎ where open ≡-Reasoning @@ -111,6 +112,19 @@ opaque where open ≈-Reasoning (Matrixₛ A B) +≑-·-∥ + : (W : Matrix A B) + (X : Matrix A C) + (Y : Matrix D A) + (Z : Matrix E A) + → (W ≑ X) · (Y ∥ Z) ≡ (W · Y) ∥ (W · Z) ≑ (X · Y) ∥ (X · Z) +≑-·-∥ W X Y Z = begin + (W ≑ X) · (Y ∥ Z) ≡⟨ ≑-· W X (Y ∥ Z) ⟩ + W · (Y ∥ Z) ≑ X · (Y ∥ Z) ≡⟨ ≡.cong₂ _≑_ (·-∥ W Y Z) (·-∥ X Y Z) ⟩ + W · Y ∥ W · Z ≑ X · Y ∥ X · Z ∎ + where + open ≡-Reasoning + opaque unfolding _≋_ diff --git a/Data/Matrix/Convert.agda b/Data/Matrix/Convert.agda index 8b140c0..1f577f0 100644 --- a/Data/Matrix/Convert.agda +++ b/Data/Matrix/Convert.agda @@ -16,7 +16,7 @@ open import Data.Matrix.Category R using (_·_) open import Data.Matrix.Core setoid using (_≋_) renaming (Matrix to Mat) open import Data.Matrix.Functional R as Functional using (Matrix; identity) open import Data.Matrix.Monoid +-monoid using (_[+]_) -open import Data.Matrix.Raw using (_∷ₕ_; _∷ᵥ_; _ᵀ) +open import Data.Matrix.Raw as Raw using (_∷ₕ_; _∷ᵥ_; _ᵀ) open import Data.Matrix.Transform R using (I; [_]_) open import Data.Nat using (ℕ) open import Data.Vec.Functional using (Vector; head; tail) @@ -33,7 +33,7 @@ open ≡-Reasoning opaque - unfolding Mat + unfolding Raw.Matrix tabulate : {n m : ℕ} → Matrix n m → Mat n m tabulate M = Vec.tabulate (λ j → Vec.tabulate (λ i → M i j)) @@ -65,14 +65,12 @@ opaque Vec.replicate n 0# ∷ₕ (tabulate (λ i j → identity i j)) ≡⟨ ≡.cong₂ _∷ₕ_ ≡.refl tabulate-I ⟩ ⟨ε⟩ ∷ₕ I ∎ - opaque - unfolding _ᵀ - tabulate-flip : {n m : ℕ} (M : Matrix n m) → tabulate (flip M) ≡ tabulate M ᵀ - tabulate-flip {n} {zero} M = ≡.sym (replicate-tabulate []) - tabulate-flip {n} {suc m} M = begin - Vec.tabulate (λ j → head (M j) ∷ Vec.tabulate (λ x → M j (Fin.suc x))) ≡⟨ zipWith-tabulate _∷_ (λ j → M j Fin.zero) _ ⟨ - Vec.tabulate (λ i → head (M i)) ∷ₕ (tabulate (λ j i → M i (Fin.suc j))) ≡⟨ ≡.cong (Vec.tabulate (λ i → head (M i)) ∷ₕ_) (tabulate-flip (λ i → tail (M i))) ⟩ - Vec.tabulate (λ i → head (M i)) ∷ₕ (tabulate (λ i j → M i (Fin.suc j))) ᵀ ∎ + tabulate-flip : {n m : ℕ} (M : Matrix n m) → tabulate (flip M) ≡ tabulate M ᵀ + tabulate-flip {n} {zero} M = ≡.sym (replicate-tabulate []) + tabulate-flip {n} {suc m} M = begin + Vec.tabulate (λ j → head (M j) ∷ Vec.tabulate (λ x → M j (Fin.suc x))) ≡⟨ zipWith-tabulate _∷_ (λ j → M j Fin.zero) _ ⟨ + Vec.tabulate (λ i → head (M i)) ∷ₕ (tabulate (λ j i → M i (Fin.suc j))) ≡⟨ ≡.cong (Vec.tabulate (λ i → head (M i)) ∷ₕ_) (tabulate-flip (λ i → tail (M i))) ⟩ + Vec.tabulate (λ i → head (M i)) ∷ₕ (tabulate (λ i j → M i (Fin.suc j))) ᵀ ∎ opaque unfolding _∙_ diff --git a/Data/Matrix/Core.agda b/Data/Matrix/Core.agda index 4ef57fb..fef4274 100644 --- a/Data/Matrix/Core.agda +++ b/Data/Matrix/Core.agda @@ -31,7 +31,8 @@ private module PW-≊ {n} = PW-≈ (Vectorₛ n) -open Raw.FixedBase Carrier using (Matrix) public +Matrix : ℕ → ℕ → Set c +Matrix = Raw.Matrix Carrier opaque diff --git a/Data/Matrix/Dagger-2-Poset.agda b/Data/Matrix/Dagger-2-Poset.agda index aff22d7..1b7b07f 100644 --- a/Data/Matrix/Dagger-2-Poset.agda +++ b/Data/Matrix/Dagger-2-Poset.agda @@ -13,7 +13,7 @@ module Data.Matrix.Dagger-2-Poset import Data.Vec.Relation.Binary.Pointwise.Inductive as PW import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open import Category.Dagger.2-Poset using (dagger-2-poset; Dagger-2-Poset) +open import Category.Dagger.2-Poset using (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) @@ -59,7 +59,6 @@ opaque where open ≈-Reasoning (Matrixₛ _ _) - idem : (M : Matrix A B) → (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (M · (𝟎 ∥ I))) · (I ≑ I) ≋ M idem M = begin (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (M · (𝟎 ∥ I))) · (I ≑ I) ≈⟨ +-[+] M M ⟩ @@ -74,5 +73,7 @@ Mat-IdempotentSemiadditiveDagger = record ; idempotent = idem _ } +open IdempotentSemiadditiveDagger Mat-IdempotentSemiadditiveDagger + Mat-Dagger-2-Poset : Dagger-2-Poset -Mat-Dagger-2-Poset = dagger-2-poset Mat-IdempotentSemiadditiveDagger +Mat-Dagger-2-Poset = dagger-2-poset diff --git a/Data/Matrix/Monoid.agda b/Data/Matrix/Monoid.agda index f614dc6..719d78a 100644 --- a/Data/Matrix/Monoid.agda +++ b/Data/Matrix/Monoid.agda @@ -10,7 +10,7 @@ module M = Monoid M import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Data.Vec.Relation.Binary.Pointwise.Inductive as PW -open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; _∷ᵥ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥) +open import Data.Matrix.Raw as Raw using (_ᵀ; _∷ₕ_; _∷ᵥ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥) open import Data.Matrix.Core M.setoid using (Matrix; _≋_) open import Data.Nat using (ℕ) open import Data.Vec using (Vec; replicate; zipWith) @@ -28,14 +28,14 @@ private opaque - unfolding Matrix + unfolding Raw.Matrix 𝟎 : Matrix A B 𝟎 {A} {B} = replicate B ⟨ε⟩ opaque - unfolding _ᵀ []ᵥ ⟨ε⟩ + unfolding []ᵥ ⟨ε⟩ 𝟎ᵀ : 𝟎 ᵀ ≡ 𝟎 {A} {B} 𝟎ᵀ {zero} = ≡.refl diff --git a/Data/Matrix/Raw.agda b/Data/Matrix/Raw.agda index ecd5e9f..73a4b8c 100644 --- a/Data/Matrix/Raw.agda +++ b/Data/Matrix/Raw.agda @@ -5,14 +5,14 @@ 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.Nat using (ℕ; _+_; _*_) +open import Data.Vec as Vec using (Vec; zipWith; head; tail; replicate; concat; foldr) open import Data.Vec using (_++_) -open import Data.Vec.Properties using (map-cong; map-id; map-++; map-∘; map-replicate) +open import Data.Vec.Properties using (map-cong; map-id; map-++; map-∘; map-const; map-replicate; zipWith-map₂; zipWith-++; zipWith-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 Function using (id; _∘_; const) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) open ℕ @@ -20,61 +20,138 @@ open Vec.Vec private variable - n m p : ℕ + n m p q : ℕ 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 + -- Matrices + Matrix : Set a → Rel ℕ a + Matrix A n m = Vec (Vec A n) m + -- Pointwise relation on matrices 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 - + -- Apply a function to every element map : (A → B) → Matrix A n m → Matrix B n m map f = Vec.map (Vec.map f) + -- Lift a square in the double category of sets and relations to matrices + 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) + + -- Juxtapose matrices horizontally _∥_ : Matrix A n p → Matrix A m p → Matrix A (n + m) p _∥_ M N = zipWith _++_ M N infixr 7 _∥_ + -- Juxtapose matrices verically _≑_ : Matrix A n m → Matrix A n p → Matrix A n (m + p) - _≑_ M N = M ++ N + _≑_ = _++_ infixr 6 _≑_ + -- Append a column on the left + _∷ₕ_ : Vec A m → Matrix A n m → Matrix A (suc n) m + _∷ₕ_ = zipWith _∷_ + + infixr 5 _∷ₕ_ + + -- Append a row to the top _∷ᵥ_ : 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 + -- A matrix of width 0 + []ᵥ : Matrix A 0 m + []ᵥ = replicate _ [] - infixr 5 _∷ₕ_ + -- A matrix of height 0 + []ₕ : Matrix A n 0 + []ₕ = [] + -- The first column of a matrix headₕ : Matrix A (suc n) m → Vec A m headₕ = Vec.map Vec.head + -- The first row of a matrix + headᵥ : Matrix A n (suc m) → Vec A n + headᵥ = head + + -- All but the first column of a matrix tailₕ : Matrix A (suc n) m → Matrix A n m tailₕ = Vec.map Vec.tail + -- All but the first row of a matrix + tailᵥ : Matrix A n (suc m) → Matrix A n m + tailᵥ = tail + + -- View a matrix as a vector of rows + rows : Matrix A n m → Vec (Vec A n) m + rows = id + + -- View a matrix as a vector of columns + columns : Matrix A n m → Vec (Vec A m) n + columns {A = A} {n} = foldr (λ i → Vec (Vec A i) n) _∷ₕ_ []ᵥ + + -- Intepret a vector of rows as a matrix + ∷ᵥⁿ : Vec (Vec A n) m → Matrix A n m + ∷ᵥⁿ = id + + -- Interpret a vector of columns as a matrix + ∷ₕⁿ : Vec (Vec A m) n → Matrix A n m + ∷ₕⁿ = columns + +-- Transpose +_ᵀ : Matrix A n m → Matrix A m n +_ᵀ = ∷ᵥⁿ ∘ columns + +infix 10 _ᵀ + +-- Apply a function to each row +mapₕ : (Vec A n → B) → Matrix A n m → Vec B m +mapₕ f M = Vec.map f (rows M) + +-- Apply a function to each column +mapᵥ : (Vec A m → B) → Matrix A n m → Vec B n +mapᵥ f M = Vec.map f (columns M) + +-- Horizontally flatten a vector of same-height matrices +∥ⁿ : Vec (Matrix A n m) p → Matrix A (p * n) m +∥ⁿ [] = []ᵥ +∥ⁿ (M ∷ Ms) = M ∥ ∥ⁿ Ms + +-- Vertically flatten a vector of same-width matrices +≑ⁿ : Vec (Matrix A n m) p → Matrix A n (p * m) +≑ⁿ [] = []ₕ +≑ⁿ (M ∷ Ms) = M ≑ ≑ⁿ Ms + +-- Flatten a matrix of matrices +join : Matrix (Matrix A p q) n m → Matrix A (n * p) (m * q) +join M = ≑ⁿ (mapₕ ∥ⁿ M) + +opaque + + unfolding Matrix + + head-∷-tailᵥ : (M : Matrix A n (suc m)) → headᵥ M ∷ᵥ tailᵥ M ≡ M + head-∷-tailᵥ (_ ∷ _) = ≡.refl + 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 ⟩ @@ -82,9 +159,6 @@ opaque Vec.map id M ≡⟨ map-id M ⟩ M ∎ - []ᵥ : Matrix A 0 m - []ᵥ = replicate _ [] - []ᵥ-! : (E : Matrix A 0 m) → E ≡ []ᵥ []ᵥ-! [] = ≡.refl []ᵥ-! ([] ∷ E) = ≡.cong ([] ∷_) ([]ᵥ-! E) @@ -107,18 +181,6 @@ opaque ∷ᵥ-∥ : (V : Vec A n) (W : Vec A m) (M : Matrix A n p) (N : Matrix A m p) → (V ++ W) ∷ᵥ (M ∥ N) ≡ (V ∷ᵥ M) ∥ (W ∷ᵥ N) ∷ᵥ-∥ {_} {A} {n} {m} {p} V W M N = ≡.refl - 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 @@ -128,19 +190,51 @@ opaque ∷ᵥ-≑ : (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 ᵀ + ≑-∥ + : (M : Matrix A n m) + (N : Matrix A p m) + (P : Matrix A n q) + (Q : Matrix A p q) + → M ∥ N ≑ P ∥ Q ≡ (M ≑ P) ∥ (N ≑ Q) + ≑-∥ M N P Q = begin + zipWith _++_ M N ++ zipWith _++_ P Q ≡⟨ zipWith-++ _++_ M P N Q ⟨ + zipWith _++_ (M ++ P) (N ++ Q) ∎ + + columns-∷ₕ : (V : Vec A n) (M : Matrix A m n) → columns (V ∷ₕ M) ≡ V ∷ columns M + columns-∷ₕ {A = A} {n} {m} [] [] = ≡.refl + columns-∷ₕ {A = A} {n} {m} (x ∷ V) (M₀ ∷ M) = begin + (x ∷ M₀) ∷ₕ (columns (V ∷ₕ M)) ≡⟨ ≡.cong ((x ∷ M₀) ∷ₕ_) (columns-∷ₕ V M) ⟩ + (x ∷ V) ∷ columns (M₀ ∷ M) ∎ + + columns-∥ : (M : Matrix A m p) (N : Matrix A n p) → columns (M ∥ N) ≡ columns M ++ columns N + columns-∥ {m = m} {n = n} [] [] = ≡.sym (replicate-++ m n []) + columns-∥ (M₀ ∷ M) (N₀ ∷ N) = begin + zipWith _∷_ (M₀ ++ N₀) (columns (M ∥ N)) ≡⟨ ≡.cong (zipWith _∷_ (M₀ ++ N₀)) (columns-∥ M N) ⟩ + zipWith _∷_ (M₀ ++ N₀) (columns M ++ columns N) ≡⟨ zipWith-++ _∷_ M₀ N₀ (columns M) (columns N) ⟩ + zipWith _∷_ M₀ (columns M) ++ zipWith _∷_ N₀ (columns N) ∎ + + columns-≑ : (M : Matrix A m n) (N : Matrix A m p) → columns (M ≑ N) ≡ zipWith _++_ (columns M) (columns N) + columns-≑ [] N = ≡.sym ([]ᵥ-∥ (columns N)) + columns-≑ (V ∷ M) N = begin + zipWith _∷_ V (columns (M ++ N)) ≡⟨ ≡.cong (zipWith _∷_ V) (columns-≑ M N) ⟩ + zipWith _∷_ V (zipWith _++_ (columns M) (columns N)) ≡⟨ ∷ₕ-∥ V (M ᵀ) (N ᵀ) ⟩ + zipWith _++_ (zipWith _∷_ V (columns M)) (columns N) ∎ + +join-[]ᵥ : join ([]ᵥ {a} {Matrix A m p} {n}) ≡ []ᵥ +join-[]ᵥ = []ᵥ-! (join []ᵥ) + +join-[]ₕ : join ([]ₕ {a} {Matrix A m p} {n}) ≡ []ₕ +join-[]ₕ = []ₕ-! (join []ₕ) + +[]ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A = A} {n} +[]ᵥ-ᵀ = []ₕ-! ([]ᵥ ᵀ) - infix 10 _ᵀ +opaque - []ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A = A} {n} - []ᵥ-ᵀ {n = zero} = ≡.refl - []ᵥ-ᵀ {n = suc n} = ≡.cong (zipWith _∷_ []) ([]ᵥ-ᵀ) + unfolding Matrix ∷ₕ-ᵀ : (V : Vec A n) (M : Matrix A m n) → (V ∷ₕ M) ᵀ ≡ V ∷ᵥ M ᵀ - ∷ₕ-ᵀ [] [] = ≡.refl - ∷ₕ-ᵀ (x ∷ V) (M₀ ∷ M) = ≡.cong ((x ∷ M₀) ∷ₕ_) (∷ₕ-ᵀ V M) + ∷ₕ-ᵀ V M = columns-∷ₕ V M ∷ᵥ-ᵀ : (V : Vec A m) (M : Matrix A m n) → (V ∷ᵥ M) ᵀ ≡ V ∷ₕ M ᵀ ∷ᵥ-ᵀ V M = ≡.refl @@ -154,6 +248,68 @@ opaque infix 10 _ᵀᵀ + ≑ⁿ-∥ : (Ms : Vec (Matrix A n p) q) (Ns : Vec (Matrix A m p) q) → ≑ⁿ (zipWith _∥_ Ms Ns) ≡ ≑ⁿ Ms ∥ ≑ⁿ Ns + ≑ⁿ-∥ {n = n} [] [] = ≡.sym ([]ₕ-! ([]ₕ {n = n} ∥ []ₕ)) + ≑ⁿ-∥ (M ∷ Ms) (N ∷ Ns) = begin + M ∥ N ≑ ≑ⁿ (zipWith _∥_ Ms Ns) ≡⟨ ≡.cong (M ∥ N ≑_) (≑ⁿ-∥ Ms Ns) ⟩ + M ∥ N ≑ ≑ⁿ Ms ∥ ≑ⁿ Ns ≡⟨ ≑-∥ M N (≑ⁿ Ms) (≑ⁿ Ns) ⟩ + (M ≑ ≑ⁿ Ms) ∥ (N ≑ ≑ⁿ Ns) ∎ + + join-∷ₕ : (V : Vec (Matrix A n m) q) (M : Matrix (Matrix A n m) p q) → join (V ∷ₕ M) ≡ ≑ⁿ V ∥ join M + join-∷ₕ V M = begin + ≑ⁿ (mapₕ ∥ⁿ (V ∷ₕ M)) ≡⟨ ≡.cong ≑ⁿ (map-zipWith ∥ⁿ _∷_ V M) ⟩ + ≑ⁿ (zipWith (λ x y → x ∥ ∥ⁿ y) V M) ≡⟨ ≡.cong ≑ⁿ (zipWith-map₂ _∥_ ∥ⁿ V M) ⟨ + ≑ⁿ (zipWith _∥_ V (mapₕ ∥ⁿ M)) ≡⟨ ≑ⁿ-∥ V (mapₕ ∥ⁿ M) ⟩ + ≑ⁿ V ∥ ≑ⁿ (mapₕ ∥ⁿ M) ∎ + + join-∷ᵥ : (V : Vec (Matrix A n m) p) (M : Matrix (Matrix A n m) p q) → join (V ∷ᵥ M) ≡ ∥ⁿ V ≑ join M + join-∷ᵥ V M = ≡.refl + + ≑ⁿ-∷ₕ : (Vs : Vec (Vec A m) p) (Ms : Vec (Matrix A n m) p) → ≑ⁿ (zipWith _∷ₕ_ Vs Ms) ≡ concat Vs ∷ₕ ≑ⁿ Ms + ≑ⁿ-∷ₕ [] [] = ≡.sym ([]ₕ-! ([] ∷ₕ []ₕ)) + ≑ⁿ-∷ₕ (V ∷ Vs) (M ∷ Ms) = begin + (V ∷ₕ M) ≑ ≑ⁿ (zipWith _∷ₕ_ Vs Ms) ≡⟨ ≡.cong ((V ∷ₕ M) ≑_) (≑ⁿ-∷ₕ Vs Ms) ⟩ + (V ∷ₕ M) ≑ (concat Vs ∷ₕ ≑ⁿ Ms) ≡⟨ ∷ₕ-≑ V (concat Vs) M (≑ⁿ Ms) ⟨ + (V ++ concat Vs) ∷ₕ (M ≑ ≑ⁿ Ms) ∎ + + replicate-∷ₕ : (V : Vec A m) (M : Matrix A n m) → replicate p (V ∷ₕ M) ≡ zipWith _∷ₕ_ (replicate p V) (replicate p M) + replicate-∷ₕ V M = ≡.sym (zipWith-replicate _∷ₕ_ V M) + + ≑ⁿ-replicate : (p : ℕ) (M : Matrix A n m) → ≑ⁿ (replicate p M) ≡ ∷ₕⁿ (mapᵥ (concat ∘ replicate p) M) + ≑ⁿ-replicate {n = zero} p M = ≡.trans ([]ᵥ-! (≑ⁿ (replicate p M))) (≡.sym ([]ᵥ-! (∷ₕⁿ (mapᵥ (concat ∘ replicate p) M)))) + ≑ⁿ-replicate {n = suc n} p M = begin + ≑ⁿ (replicate p M) ≡⟨ ≡.cong (≑ⁿ ∘ replicate p) (head-∷-tailₕ M) ⟨ + ≑ⁿ (replicate p (headₕ M ∷ₕ tailₕ M)) ≡⟨ ≡.cong ≑ⁿ (replicate-∷ₕ {p = p} (headₕ M) (tailₕ M)) ⟩ + ≑ⁿ (zipWith _∷ₕ_ (replicate p (headₕ M)) (replicate p (tailₕ M))) ≡⟨ ≑ⁿ-∷ₕ (replicate p (headₕ M)) (replicate p (tailₕ M)) ⟩ + concat (replicate p (headₕ M)) ∷ₕ (≑ⁿ (replicate p (tailₕ M))) ≡⟨ ≡.cong (concat (replicate p (headₕ M)) ∷ₕ_) (≑ⁿ-replicate p (tailₕ M)) ⟩ + concat (replicate p (headₕ M)) ∷ₕ ∷ₕⁿ (mapᵥ (concat ∘ replicate p) (tailₕ M)) ≡⟨ ≡.cong (∷ₕⁿ ∘ Vec.map (concat ∘ replicate p)) (∷ₕ-ᵀ (headₕ M) (tailₕ M)) ⟨ + ∷ₕⁿ (mapᵥ (concat ∘ replicate p) (headₕ M ∷ₕ tailₕ M)) ≡⟨ ≡.cong (∷ₕⁿ ∘ mapᵥ (concat ∘ replicate p)) (head-∷-tailₕ M) ⟩ + ∷ₕⁿ (mapᵥ (concat ∘ replicate p) M) ∎ + + ∥ⁿ-replicate : (p : ℕ) (M : Matrix A n m) → ∥ⁿ (replicate p M) ≡ ∷ᵥⁿ (mapₕ (concat ∘ replicate p) M) + ∥ⁿ-replicate zero M = ≡.sym (map-const M []) + ∥ⁿ-replicate (suc p) M = begin + zipWith _++_ M (∥ⁿ (replicate p M)) ≡⟨ ≡.cong (zipWith _++_ M) (∥ⁿ-replicate p M) ⟩ + zipWith _++_ M (Vec.map (concat ∘ replicate p) M) ≡⟨ ≡.cong (λ h → zipWith _++_ h (Vec.map (concat ∘ replicate p) M)) (map-id M) ⟨ + zipWith _++_ (Vec.map id M) (Vec.map (concat ∘ replicate p) M) ≡⟨ zipWith-map id (concat ∘ replicate p) _++_ M ⟩ + Vec.map (λ V → V ++ concat (replicate p V)) M ∎ + +opaque + + unfolding ∷ₕⁿ + + columns-∷ₕⁿ : (Vs : Vec (Vec A n) m) → columns (∷ₕⁿ Vs) ≡ Vs + columns-∷ₕⁿ Vs = Vs ᵀᵀ + + ∷ₕⁿ-columns : (M : Matrix A n m) → ∷ₕⁿ (columns M) ≡ M + ∷ₕⁿ-columns M = M ᵀᵀ + + ∷ᵥⁿ-rows : (M : Matrix A n m) → ∷ᵥⁿ (rows M) ≡ M + ∷ᵥⁿ-rows M = ≡.refl + + ∷ᵥⁿ-ᵀ : (Vs : Vec (Vec A n) m) → ∷ᵥⁿ Vs ᵀ ≡ ∷ₕⁿ Vs + ∷ᵥⁿ-ᵀ Vs = ≡.refl + open Pointwise module Natural (f : A → B) where @@ -162,7 +318,7 @@ module Natural (f : A → B) where opaque - unfolding map + unfolding Matrix α-∥ : (M : Matrix A n p) (N : Matrix A m p) → map f (M ∥ N) ≡ map f M ∥ map f N α-∥ M N = begin @@ -216,23 +372,6 @@ module Natural (f : A → B) where 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 diff --git a/Data/Matrix/Semiadditive.agda b/Data/Matrix/Semiadditive.agda index f91dfd7..babbdfa 100644 --- a/Data/Matrix/Semiadditive.agda +++ b/Data/Matrix/Semiadditive.agda @@ -24,7 +24,7 @@ open import Category.Semiadditive using (Semiadditive) open import Data.Matrix.Category R using (Mat; _·_; ≑-·; ·-Iˡ; ·-Iʳ; ·-𝟎ˡ; ·-𝟎ʳ; ·-∥; ∥-·-≑; ·-resp-≋; ·-assoc) 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.Raw using (_ᵀ; _ᵀᵀ; mapRows; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!) +open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; mapₕ; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!) open import Data.Matrix.Transform R using (I; Iᵀ; [_]_; _[_]; -[-]ᵀ; [-]--cong; [-]-[]ᵥ; [⟨⟩]-[]ₕ) open import Data.Nat using (ℕ) open import Data.Product using (_,_; Σ-syntax) @@ -66,7 +66,7 @@ inj₂ {A} {C} {B} M N = begin opaque - unfolding Matrix _∷ᵥ_ + unfolding _∷ᵥ_ split-∥ : (A : ℕ) (M : Matrix (A ℕ.+ B) C) → Σ[ M₁ ∈ Matrix A C ] Σ[ M₂ ∈ Matrix B C ] M₁ ∥ M₂ ≡ M split-∥ zero M = []ᵥ , M , []ᵥ-∥ M @@ -158,61 +158,57 @@ isProduct {A} {B} = record ; unique = λ eq₁ eq₂ → ≑-uniq _ _ _ eq₁ eq₂ } -opaque - - unfolding Matrix +π₁∘i₁ : (I {A} ∥ 𝟎 {B}) · (I ≑ 𝟎) ≋ I +π₁∘i₁ {A} = begin + (I ∥ 𝟎) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ I 𝟎 I 𝟎 ⟩ + (I · I) [+] (𝟎 · 𝟎) ≈⟨ [+]-cong ·-Iˡ (·-𝟎ˡ 𝟎) ⟩ + I [+] 𝟎 ≈⟨ [+]-𝟎ʳ I ⟩ + I ∎ + where + open ≈-Reasoning (Matrixₛ A A) + +π₂∘i₂ : (𝟎 {A} {B} ∥ I) · (𝟎 ≑ I) ≋ I +π₂∘i₂ {A} {B} = begin + (𝟎 ∥ I) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ 𝟎 I 𝟎 I ⟩ + (𝟎 · 𝟎) [+] (I · I) ≈⟨ [+]-cong (·-𝟎ˡ 𝟎) ·-Iˡ ⟩ + 𝟎 [+] I ≈⟨ [+]-𝟎ˡ I ⟩ + I ∎ + where + open ≈-Reasoning (Matrixₛ B B) + +π₁∘i₂ : (I {A} ∥ 𝟎 {B}) · (𝟎 ≑ I) ≋ 𝟎 {B} {A} +π₁∘i₂ {A} {B} = begin + (I ∥ 𝟎) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ I 𝟎 𝟎 I ⟩ + (I · 𝟎) [+] (𝟎 · I) ≈⟨ [+]-cong (·-𝟎ʳ I) (·-𝟎ˡ I) ⟩ + 𝟎 [+] 𝟎 ≈⟨ [+]-𝟎ʳ 𝟎 ⟩ + 𝟎 ∎ + where + open ≈-Reasoning (Matrixₛ B A) + +π₂∘i₁ : (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎) ≋ 𝟎 {A} {B} +π₂∘i₁ {A} {B} = begin + (𝟎 ∥ I) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ 𝟎 I I 𝟎 ⟩ + (𝟎 · I) [+] (I · 𝟎) ≈⟨ [+]-cong (·-𝟎ˡ I) (·-𝟎ʳ I) ⟩ + 𝟎 [+] 𝟎 ≈⟨ [+]-𝟎ʳ 𝟎 ⟩ + 𝟎 ∎ + where + open ≈-Reasoning (Matrixₛ A B) - π₁∘i₁ : (I {A} ∥ 𝟎 {B}) · (I ≑ 𝟎) ≋ I - π₁∘i₁ {A} = begin - (I ∥ 𝟎) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ I 𝟎 I 𝟎 ⟩ - (I · I) [+] (𝟎 · 𝟎) ≈⟨ [+]-cong ·-Iˡ (·-𝟎ˡ 𝟎) ⟩ - I [+] 𝟎 ≈⟨ [+]-𝟎ʳ I ⟩ - I ∎ - where - open ≈-Reasoning (Matrixₛ A A) - - π₂∘i₂ : (𝟎 {A} {B} ∥ I) · (𝟎 ≑ I) ≋ I - π₂∘i₂ {A} {B} = begin - (𝟎 ∥ I) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ 𝟎 I 𝟎 I ⟩ - (𝟎 · 𝟎) [+] (I · I) ≈⟨ [+]-cong (·-𝟎ˡ 𝟎) ·-Iˡ ⟩ - 𝟎 [+] I ≈⟨ [+]-𝟎ˡ I ⟩ - I ∎ - where - open ≈-Reasoning (Matrixₛ B B) - - π₁∘i₂ : (I {A} ∥ 𝟎 {B}) · (𝟎 ≑ I) ≋ 𝟎 {B} {A} - π₁∘i₂ {A} {B} = begin - (I ∥ 𝟎) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ I 𝟎 𝟎 I ⟩ - (I · 𝟎) [+] (𝟎 · I) ≈⟨ [+]-cong (·-𝟎ʳ I) (·-𝟎ˡ I) ⟩ - 𝟎 [+] 𝟎 ≈⟨ [+]-𝟎ʳ 𝟎 ⟩ - 𝟎 ∎ - where - open ≈-Reasoning (Matrixₛ B A) - - π₂∘i₁ : (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎) ≋ 𝟎 {A} {B} - π₂∘i₁ {A} {B} = begin - (𝟎 ∥ I) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ 𝟎 I I 𝟎 ⟩ - (𝟎 · I) [+] (I · 𝟎) ≈⟨ [+]-cong (·-𝟎ˡ I) (·-𝟎ʳ I) ⟩ - 𝟎 [+] 𝟎 ≈⟨ [+]-𝟎ʳ 𝟎 ⟩ - 𝟎 ∎ - where - open ≈-Reasoning (Matrixₛ A B) - - permute - : (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) - ≋ (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎 {B} {A}) - permute {A} {B} = begin - (I ≑ 𝟎) · (I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) ≈⟨ ·-resp-≋ ≋.refl ·-assoc ⟨ - (I ≑ 𝟎) · ((I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I)) · (𝟎 {A} {B} ∥ I) ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ π₁∘i₂ ≋.refl) ⟩ - (I ≑ 𝟎) · 𝟎 {B} {A} · (𝟎 {A} {B} ∥ I) ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ (𝟎 ∥ I)) ⟩ - (I ≑ 𝟎 {A} {B}) · 𝟎 ≈⟨ ·-𝟎ʳ (I ≑ 𝟎) ⟩ - 𝟎 ≈⟨ ·-𝟎ʳ (𝟎 ≑ I) ⟨ - (𝟎 {B} {A} ≑ I) · 𝟎 ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ (I ∥ 𝟎)) ⟨ - (𝟎 ≑ I) · 𝟎 {A} {B} · (I ∥ 𝟎 {B} {A}) ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ π₂∘i₁ ≋.refl) ⟨ - (𝟎 {B} {A} ≑ I) · ((𝟎 ∥ I) · (I ≑ 𝟎 {A} {B})) · (I ∥ 𝟎 {B} {A}) ≈⟨ ·-resp-≋ ≋.refl ·-assoc ⟩ - (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎) ∎ - where - open ≈-Reasoning (Matrixₛ (A ℕ.+ B) (A ℕ.+ B)) +permute + : (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) + ≋ (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎 {B} {A}) +permute {A} {B} = begin + (I ≑ 𝟎) · (I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) ≈⟨ ·-resp-≋ ≋.refl ·-assoc ⟨ + (I ≑ 𝟎) · ((I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I)) · (𝟎 {A} {B} ∥ I) ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ π₁∘i₂ ≋.refl) ⟩ + (I ≑ 𝟎) · 𝟎 {B} {A} · (𝟎 {A} {B} ∥ I) ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ (𝟎 ∥ I)) ⟩ + (I ≑ 𝟎 {A} {B}) · 𝟎 ≈⟨ ·-𝟎ʳ (I ≑ 𝟎) ⟩ + 𝟎 ≈⟨ ·-𝟎ʳ (𝟎 ≑ I) ⟨ + (𝟎 {B} {A} ≑ I) · 𝟎 ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ (I ∥ 𝟎)) ⟨ + (𝟎 ≑ I) · 𝟎 {A} {B} · (I ∥ 𝟎 {B} {A}) ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ π₂∘i₁ ≋.refl) ⟨ + (𝟎 {B} {A} ≑ I) · ((𝟎 ∥ I) · (I ≑ 𝟎 {A} {B})) · (I ∥ 𝟎 {B} {A}) ≈⟨ ·-resp-≋ ≋.refl ·-assoc ⟩ + (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎) ∎ + where + open ≈-Reasoning (Matrixₛ (A ℕ.+ B) (A ℕ.+ B)) biproduct : Biproduct Mat A B biproduct {A} {B} = record diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda index 017f05f..7ebc5da 100644 --- a/Data/Matrix/SemiadditiveDagger.agda +++ b/Data/Matrix/SemiadditiveDagger.agda @@ -26,7 +26,7 @@ open import Category.Semiadditive using (Semiadditive) 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; ᵀ-cong) open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; 𝟎≑𝟎; 𝟎∥𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ) -open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; mapRows; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!) +open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!) open import Data.Matrix.Semiadditive R.semiring using (Mat-Semiadditive) open import Data.Matrix.Transform R.semiring using (I; Iᵀ; [_]_; _[_]; -[-]ᵀ; [-]--cong; [-]-[]ᵥ; [⟨⟩]-[]ₕ) open import Data.Nat using (ℕ) @@ -56,7 +56,7 @@ opaque ∙-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 @@ -69,7 +69,7 @@ opaque open ≈-Reasoning (Vectorₛ _) opaque - unfolding []ᵥ mapRows _∷ₕ_ _∷ᵥ_ _ᵀ _≋_ + unfolding []ᵥ _∷ₕ_ _∷ᵥ_ _≋_ ·-ᵀ : {A B C : ℕ} (M : Matrix A B) @@ -95,7 +95,7 @@ opaque ᵀ-involutive M = ≋.reflexive (M ᵀᵀ) opaque - unfolding Matrix _∥_ _ᵀ _≑_ _∷ₕ_ + unfolding _∥_ _≑_ _∷ₕ_ ∥-ᵀ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) ᵀ ≡ M ᵀ ≑ N ᵀ ∥-ᵀ {A} {zero} {B} [] [] = ≡.sym (replicate-++ A B []) ∥-ᵀ (M₀ ∷ M) (N₀ ∷ N) = begin diff --git a/Data/Matrix/Transform.agda b/Data/Matrix/Transform.agda index f536aaf..9f87cbb 100644 --- a/Data/Matrix/Transform.agda +++ b/Data/Matrix/Transform.agda @@ -13,15 +13,15 @@ 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.Properties using (map-id; map-const; map-∘; zipWith-replicate; zipWith-replicate₁; map-replicate; map-cong) +open import Data.Vec.Properties using (map-id; map-const; map-∘; zipWith-replicate; zipWith-replicate₁; map-replicate; map-++; map-cong) open import Relation.Binary.PropositionalEquality as ≡ using (_≗_; _≡_; module ≡-Reasoning) open import Function using (id; _∘_) open import Data.Matrix.Raw using - ( _ᵀ; _∷ₕ_; []ᵥ; []ₕ; []ᵥ-ᵀ; mapRows + ( _ᵀ; _∷ₕ_; []ᵥ; []ₕ; []ᵥ-ᵀ; mapₕ; mapᵥ; ∷ₕⁿ; ∷ᵥⁿ; columns ; _ᵀᵀ; []ᵥ-!; ∷ₕ-ᵀ; _∥_; []ᵥ-∥; headₕ; tailₕ; head-∷-tailₕ; ∷ₕ-∥ - ; _≑_; []ᵥ-≑; ∷ₕ-≑; []ₕ-≑; []ₕ-!; ∷ᵥ-∥ + ; _≑_; []ᵥ-≑; ∷ₕ-≑; []ₕ-≑; []ₕ-!; ∷ᵥ-∥; columns-≑ ) open import Data.Matrix.Core R.setoid using @@ -30,11 +30,12 @@ open import Data.Matrix.Core R.setoid ) open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; _[+]_) renaming (⟨ε⟩∷ᵥ𝟎 to ⟨0⟩∷ᵥ𝟎; ⟨ε⟩∷ₕ𝟎 to ⟨0⟩∷ₕ𝟎) open import Data.Matrix.Cast R.setoid using (∥-≑) -open import Data.Vector.Raw using (⟨⟩; ⟨⟩-++) +open import Data.Vector.Raw using (⟨⟩; ⟨⟩-++; ⟨⟩-!) open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; module ≊; _≊_) +open import Data.Vector.Endofunctor.Setoid using (zipWith-cong) 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⟩; ⟨ε⟩-++ to ⟨0⟩-++) -open import Data.Vector.Bisemimodule R using (_∙_; ∙-cong; ∙-zeroˡ; ∙-zeroʳ; _⟨_⟩; *-∙ˡ; *-∙ʳ; ∙-distribˡ; ∙-distribʳ) +open import Data.Vector.Bisemimodule R using (_∙_; ∙-cong; ∙-zeroˡ; ∙-zeroʳ; _⟨_⟩; *-∙ˡ; ∙-distribˡ; ∙-distribʳ) open Vec open ℕ @@ -51,13 +52,11 @@ opaque opaque - -- unfolding Vector - _[_] : Matrix n m → Vector n → Vector m - _[_] M V = map (_∙ V) M + _[_] M V = mapₕ (_∙ V) M [_]_ : Vector m → Matrix n m → Vector n - [_]_ V M = map (V ∙_) (M ᵀ) + [_]_ V = mapᵥ (V ∙_) -[-]-cong : {x y : Vector n} (A : Matrix n m) → x ≊ y → A [ x ] ≊ A [ y ] -[-]-cong {x = x} {y} A ≋V = PW.map⁺ (λ ≋w → ∙-cong ≋w ≋V) {xs = A} ≋.refl @@ -68,17 +67,12 @@ opaque [-]--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) - opaque - - unfolding _ᵀ []ᵥ - - [-]-[]ᵥ : (V : Vector A) → [ V ] []ᵥ ≡ ⟨⟩ - [-]-[]ᵥ [] = ≡.refl - [-]-[]ᵥ (x ∷ V) = ≡.cong (map ((x ∷ V) ∙_)) []ᵥ-ᵀ + [-]-[]ᵥ : (V : Vector A) → [ V ] []ᵥ ≡ ⟨⟩ + [-]-[]ᵥ V = ⟨⟩-! ([ V ] []ᵥ) opaque - unfolding []ᵥ _ᵀ ⟨0⟩ _∙_ + unfolding []ᵥ ⟨0⟩ _∙_ [-]-[]ₕ : (V : Vector 0) → [ V ] []ₕ ≡ ⟨0⟩ {n} [-]-[]ₕ {zero} [] = ≡.refl @@ -101,7 +95,7 @@ opaque opaque - unfolding _ᵀ _∷ₕ_ + unfolding _∷ₕ_ Iᵀ : I ᵀ ≡ I {n} Iᵀ {zero} = ≡.sym ([]ᵥ-! []) @@ -141,18 +135,18 @@ opaque open ≡-Reasoning opaque - unfolding mapRows _ᵀ _[_] [_]_ []ᵥ - -[-]ᵀ : (A : Matrix m p) (B : Matrix n m) → mapRows (A [_]) (B ᵀ) ≡ (mapRows ([_] B) A) ᵀ - -[-]ᵀ [] B = map-const (B ᵀ) [] + unfolding _[_] [_]_ []ᵥ + -[-]ᵀ : (A : Matrix m p) (B : Matrix n m) → ∷ᵥⁿ (mapᵥ (A [_]) B) ≡ ∷ₕⁿ (mapₕ ([_] B) A) + -[-]ᵀ [] B = map-const (columns B) [] -[-]ᵀ (A₀ ∷ A) B = begin - map (λ V → A₀ ∙ V ∷ map (_∙ V) A) (B ᵀ) ≡⟨ zipWith-map (A₀ ∙_) (A [_]) _∷_ (B ᵀ) ⟨ - [ A₀ ] B ∷ₕ (map (A [_]) (B ᵀ)) ≡⟨ ≡.cong ([ A₀ ] B ∷ₕ_) (-[-]ᵀ A B) ⟩ - [ A₀ ] B ∷ₕ ((map ([_] B) A) ᵀ) ∎ + map (λ V → A₀ ∙ V ∷ map (_∙ V) A) (columns B) ≡⟨ zipWith-map (A₀ ∙_) (A [_]) _∷_ (columns B) ⟨ + [ A₀ ] B ∷ₕ (map (A [_]) (columns B)) ≡⟨ ≡.cong ([ A₀ ] B ∷ₕ_) (-[-]ᵀ A B) ⟩ + [ A₀ ] B ∷ₕ ∷ₕⁿ ((map ([_] B) A)) ∎ where open ≡-Reasoning opaque - unfolding [_]_ _[_] _ᵀ []ₕ _∙_ _∷ₕ_ _⟨_⟩ + unfolding [_]_ _[_] []ₕ _∙_ _∷ₕ_ _⟨_⟩ []-∙ : (V : Vector m) (M : Matrix n m) (W : Vector n) → [ V ] M ∙ W ≈ V ∙ M [ W ] []-∙ {n = n} [] M@[] W = begin @@ -172,7 +166,7 @@ opaque open ≈-Reasoning setoid opaque - unfolding [_]_ I _∙_ ⟨0⟩ mapRows _ᵀ []ᵥ + unfolding [_]_ I _∙_ ⟨0⟩ []ᵥ [-]I : {n : ℕ} (V : Vector n) → [ V ] I ≊ V [-]I {zero} [] = ≊.refl [-]I {suc n} (x ∷ V) = begin @@ -215,8 +209,8 @@ opaque open ≈-Reasoning (Vectorₛ n) opaque - unfolding mapRows _[_] _ᵀ _∷ₕ_ I - map--[-]-I : (M : Matrix n m) → mapRows (M [_]) I ≋ M ᵀ + unfolding _[_] _∷ₕ_ I + map--[-]-I : (M : Matrix n m) → ∷ᵥⁿ (mapₕ (M [_]) I) ≋ M ᵀ map--[-]-I {n} {m} [] = ≋.reflexive (map-const I []) map--[-]-I {n} {suc m} (M₀ ∷ M) = begin map ((M₀ ∷ M) [_]) I ≡⟨⟩ @@ -257,14 +251,13 @@ opaque open ≡-Reasoning opaque - unfolding Matrix _[_] + unfolding _[_] ≑--[-] : (V : Vector A) (M : Matrix A B) (N : Matrix A C) → (M ≑ N) [ V ] ≡ M [ V ] ++ N [ V ] - ≑--[-] {A} {zero} {C} V [] N = ≡.refl - ≑--[-] {A} {suc B} {C} V (M₀ ∷ M) N = ≡.cong (M₀ ∙ V ∷_) (≑--[-] V M N) + ≑--[-] V M N = map-++ (_∙ V) M N opaque @@ -281,54 +274,41 @@ opaque opaque - unfolding _⊕_ [_]_ + unfolding _⊕_ - [++]-≑ - : (V : Vector B) - (W : Vector C) - (M : Matrix A B) - (N : Matrix A C) - → [ V ++ W ] (M ≑ N) - ≊ [ V ] M ⊕ [ W ] N - [++]-≑ {B} {C} {zero} V W M N - rewrite []ᵥ-! M - rewrite []ᵥ-! N = begin - [ 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 - rewrite ≡.sym (head-∷-tailₕ M) - rewrite ≡.sym (head-∷-tailₕ N) - using M₀ ← headₕ M - using M ← tailₕ M - using N₀ ← headₕ N - using N ← tailₕ N = begin - [ V ++ W ] ((M₀ ∷ₕ M) ≑ (N₀ ∷ₕ N)) ≡⟨ ≡.cong ([ V ++ W ]_) (∷ₕ-≑ M₀ N₀ M N) ⟨ - [ V ++ W ] ((M₀ ++ N₀) ∷ₕ (M ≑ N)) ≡⟨ ≡.cong (map ((V ++ W) ∙_)) (∷ₕ-ᵀ (M₀ ++ N₀) (M ≑ N)) ⟩ - (V ++ W) ∙ (M₀ ++ N₀) ∷ ([ V ++ W ] (M ≑ N)) ≈⟨ ∙-++ V M₀ W N₀ PW.∷ [++]-≑ V W M N ⟩ - (V ∙ M₀ ∷ [ V ] M) ⊕ (W ∙ N₀ ∷ [ W ] N) ≡⟨ ≡.cong₂ (λ h₁ h₂ → map (V ∙_) h₁ ⊕ map (W ∙_) h₂) (∷ₕ-ᵀ M₀ M) (∷ₕ-ᵀ N₀ N) ⟨ - ([ V ] (M₀ ∷ₕ M)) ⊕ ([ W ] (N₀ ∷ₕ N)) ∎ - where - open ≈-Reasoning (Vectorₛ (suc A)) + opaque + unfolding [_]_ + [++]-≑ + : (V : Vector B) + (W : Vector C) + (M : Matrix A B) + (N : Matrix A C) + → [ V ++ W ] (M ≑ N) + ≊ [ V ] M ⊕ [ W ] N + [++]-≑ {A = A} V W M N = begin + map ((V ++ W) ∙_) (columns (M ++ N)) ≡⟨ ≡.cong (map ((V ++ W) ∙_)) (columns-≑ M N) ⟩ + map ((V ++ W) ∙_) (zipWith _++_ (columns M) (columns N)) ≡⟨ map-zipWith ((V ++ W) ∙_) _++_ (columns M) (columns N) ⟩ + zipWith (λ x y → (V ++ W) ∙ (x ++ y)) (columns M) (columns N) ≈⟨ zipWith-cong A R.setoid (λ x y → ∙-++ V x W y) (columns M) (columns N) ⟩ + zipWith (λ x y → V ∙ x + W ∙ y) (columns M) (columns N) ≡⟨ zipWith-map-map (V ∙_) (W ∙_) _+_ (columns M) (columns N) ⟩ + zipWith _+_ (map (V ∙_) (columns M)) (map (W ∙_) (columns N)) ∎ + where + open ≈-Reasoning (Vectorₛ A) -opaque - unfolding Matrix _[_] _⊕_ - ∥-[++] - : (V : Vector A) - (W : Vector B) - (M : Matrix A C) - (N : Matrix B C) - → (M ∥ N) [ V ++ W ] - ≊ M [ V ] ⊕ N [ W ] - ∥-[++] {A} {B} {zero} V W [] [] = PW.[] - ∥-[++] {A} {B} {suc C} V W (M₀ ∷ M) (N₀ ∷ N) = ∙-++ M₀ V N₀ W PW.∷ ∥-[++] V W M N + opaque + unfolding _[_] + ∥-[++] + : (V : Vector A) + (W : Vector B) + (M : Matrix A C) + (N : Matrix B C) + → (M ∥ N) [ V ++ W ] + ≊ M [ V ] ⊕ N [ W ] + ∥-[++] {A} {B} {zero} V W [] [] = PW.[] + ∥-[++] {A} {B} {suc C} V W (M₀ ∷ M) (N₀ ∷ N) = ∙-++ M₀ V N₀ W PW.∷ ∥-[++] V W M N opaque - unfolding []ₕ []ᵥ [_]_ ⟨0⟩ _∙_ _ᵀ + unfolding []ₕ []ᵥ [_]_ ⟨0⟩ _∙_ [⟨⟩]-[]ₕ : [ ⟨⟩ ] ([]ₕ {n = A}) ≡ ⟨0⟩ {A} [⟨⟩]-[]ₕ {zero} = ≡.refl @@ -336,7 +316,7 @@ opaque opaque - unfolding ⟨0⟩ []ᵥ [_]_ _ᵀ _∷ₕ_ 𝟎 + unfolding ⟨0⟩ []ᵥ [_]_ _∷ₕ_ 𝟎 [-]-𝟎 : (V : Vector A) → [ V ] (𝟎 {B}) ≊ ⟨0⟩ [-]-𝟎 {A} {zero} V = ≊.reflexive (≡.cong (map (V ∙_)) 𝟎ᵀ) @@ -349,29 +329,31 @@ opaque open ≈-Reasoning (Vectorₛ (suc B)) opaque - unfolding Matrix _[_] ⟨0⟩ 𝟎 + unfolding _[_] ⟨0⟩ 𝟎 𝟎-[-] : (V : Vector A) → (𝟎 {A} {B}) [ V ] ≊ ⟨0⟩ 𝟎-[-] {A} {zero} V = PW.[] 𝟎-[-] {A} {suc B} V = ∙-zeroˡ V PW.∷ 𝟎-[-] V opaque - unfolding ⟨0⟩ [_]_ + unfolding ⟨0⟩ - [⟨0⟩]- : (M : Matrix A B) → [ ⟨0⟩ ] M ≊ ⟨0⟩ - [⟨0⟩]- {zero} M rewrite []ᵥ-! M = ≊.reflexive ([-]-[]ᵥ ⟨0⟩) - [⟨0⟩]- {suc A} M - rewrite ≡.sym (head-∷-tailₕ M) - using M₀ ← headₕ M - using M ← tailₕ M = begin - [ ⟨0⟩ ] (M₀ ∷ₕ M) ≡⟨ ≡.cong (map (⟨0⟩ ∙_)) (∷ₕ-ᵀ M₀ M) ⟩ - ⟨0⟩ ∙ M₀ ∷ [ ⟨0⟩ ] M ≈⟨ ∙-zeroˡ M₀ PW.∷ [⟨0⟩]- M ⟩ - 0# ∷ ⟨0⟩ ∎ - where - open ≈-Reasoning (Vectorₛ _) + opaque + unfolding [_]_ + [⟨0⟩]- : (M : Matrix A B) → [ ⟨0⟩ ] M ≊ ⟨0⟩ + [⟨0⟩]- {zero} M rewrite []ᵥ-! M = ≊.reflexive ([-]-[]ᵥ ⟨0⟩) + [⟨0⟩]- {suc A} M + rewrite ≡.sym (head-∷-tailₕ M) + using M₀ ← headₕ M + using M ← tailₕ M = begin + [ ⟨0⟩ ] (M₀ ∷ₕ M) ≡⟨ ≡.cong (map (⟨0⟩ ∙_)) (∷ₕ-ᵀ M₀ M) ⟩ + ⟨0⟩ ∙ M₀ ∷ [ ⟨0⟩ ] M ≈⟨ ∙-zeroˡ M₀ PW.∷ [⟨0⟩]- M ⟩ + 0# ∷ ⟨0⟩ ∎ + where + open ≈-Reasoning (Vectorₛ _) -opaque - unfolding _[_] ⟨0⟩ - -[⟨0⟩] : (M : Matrix A B) → M [ ⟨0⟩ ] ≊ ⟨0⟩ - -[⟨0⟩] {A} {B} [] = PW.[] - -[⟨0⟩] {A} {B} (M₀ ∷ M) = ∙-zeroʳ M₀ PW.∷ -[⟨0⟩] M + opaque + unfolding _[_] + -[⟨0⟩] : (M : Matrix A B) → M [ ⟨0⟩ ] ≊ ⟨0⟩ + -[⟨0⟩] {A} {B} [] = PW.[] + -[⟨0⟩] {A} {B} (M₀ ∷ M) = ∙-zeroʳ M₀ PW.∷ -[⟨0⟩] M |