diff options
Diffstat (limited to 'Data/Matrix/Category.agda')
| -rw-r--r-- | Data/Matrix/Category.agda | 28 |
1 files changed, 21 insertions, 7 deletions
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 _≋_ |