diff options
| -rw-r--r-- | Data/Mat/Category.agda | 434 | ||||
| -rw-r--r-- | Data/Mat/Cocartesian.agda | 623 | ||||
| -rw-r--r-- | Data/Mat/Dagger-2-Poset.agda | 79 | ||||
| -rw-r--r-- | Data/Mat/SemiadditiveDagger.agda | 503 | ||||
| -rw-r--r-- | Data/Mat/Util.agda | 134 | ||||
| -rw-r--r-- | Data/Matrix/Cast.agda | 162 | ||||
| -rw-r--r-- | Data/Matrix/Category.agda | 177 | ||||
| -rw-r--r-- | Data/Matrix/Core.agda | 266 | ||||
| -rw-r--r-- | Data/Matrix/Dagger-2-Poset.agda | 72 | ||||
| -rw-r--r-- | Data/Matrix/Monoid.agda | 93 | ||||
| -rw-r--r-- | Data/Matrix/SemiadditiveDagger.agda | 389 | ||||
| -rw-r--r-- | Data/Matrix/Transform.agda | 298 | ||||
| -rw-r--r-- | Data/Matrix/Vec.agda | 20 | ||||
| -rw-r--r-- | Data/Vector/Bisemimodule.agda | 16 | ||||
| -rw-r--r-- | Data/Vector/Core.agda | 20 | ||||
| -rw-r--r-- | Data/Vector/Vec.agda | 56 |
16 files changed, 1549 insertions, 1793 deletions
diff --git a/Data/Mat/Category.agda b/Data/Mat/Category.agda deleted file mode 100644 index 2407d28..0000000 --- a/Data/Mat/Category.agda +++ /dev/null @@ -1,434 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Algebra.Bundles using (Semiring) -open import Level using (Level; 0ℓ; _⊔_) - -module Data.Mat.Category {c ℓ : Level} (Rig : Semiring c ℓ) where - -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -import Data.Vec.Relation.Binary.Equality.Setoid as PW - -open import Categories.Category using (Category) -open import Categories.Category.Helper using (categoryHelper) -open import Data.Nat using (ℕ) -open import Data.Vec using (Vec; zipWith; foldr; foldr′; map; replicate) -open import Data.Mat.Util - using - ( foldr-cong ; zipWith-cong ; transpose ; transpose-involutive ; map-replicate - ; zipWith-map ; map-zipWith ; zipWith-map-map ; transpose-zipWith ; transpose-cong - ) -open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise) -open import Data.Vec.Properties using (map-id; map-∘; map-cong; zipWith-replicate₁) -open import Relation.Binary using (Rel; IsEquivalence; Setoid) -open import Relation.Binary.PropositionalEquality as ≡ using (_≗_; _≡_; module ≡-Reasoning) -open import Function using (_∘_; id) - -open Vec -open ℕ - -open Semiring Rig renaming (Carrier to R) -module V = PW setoid - -private - variable - n m o p : ℕ - -opaque - -- Vectors over the rig - Vector : ℕ → Set c - Vector = Vec R - -opaque - -- N by M matrices over the rig - Matrix : Rel ℕ c - Matrix n m = Vec (Vector n) m - -opaque - - unfolding Vector - - -- Pointwise equality of vectors - _≊_ : Rel (Vector n) (c ⊔ ℓ) - _≊_ {n} A B = A V.≋ B - - ≊-setoid : ℕ → Setoid c (c ⊔ ℓ) - ≊-setoid n = record - { Carrier = Vector n - ; _≈_ = _≊_ {n} - ; isEquivalence = record - { refl = V.≋-refl - ; sym = V.≋-sym - ; trans = V.≋-trans - } - } - -module ≊ {n} = Setoid (≊-setoid n) - -infix 4 _≊_ - -module M {n} = PW (≊-setoid n) - -opaque - - unfolding Matrix ≊-setoid - - -- Pointwise equality of matrices - _≋_ : Rel (Matrix n m) (c ⊔ ℓ) - _≋_ {n} {m} A B = A M.≋ B - - ≋-setoid : ℕ → ℕ → Setoid c (c ⊔ ℓ) - ≋-setoid n m = record - { Carrier = Matrix n m - ; _≈_ = _≋_ {n} {m} - ; isEquivalence = record - { refl = M.≋-refl - ; sym = M.≋-sym - ; trans = M.≋-trans - } - } - - ≋-isEquivalence : IsEquivalence (_≋_ {n} {m}) - ≋-isEquivalence {n} {m} = Setoid.isEquivalence (≋-setoid n m) - -module ≋ {n} {m} = Setoid (≋-setoid n m) - -infix 4 _≋_ - -opaque - unfolding Vector - -- Sum the elements of a vector - sum : Vector n → R - sum = foldr′ _+_ 0# - -opaque - unfolding sum _≊_ - sum-cong : {x y : Vector n} → x ≊ y → sum x ≈ sum y - sum-cong = foldr-cong {A = setoid} (λ _ → setoid) +-cong refl - -opaque - unfolding sum - -- Dot product of two vectors - _∙_ : Vector n → Vector n → R - _∙_ v w = sum (zipWith _*_ v w) - -infix 8 _∙_ - -opaque - unfolding Vector - -- Pointwise sum of two vectors - _⊕_ : Vector n → Vector n → Vector n - _⊕_ = zipWith _+_ - -infixl 6 _⊕_ - -opaque - unfolding Vector - -- Scaling a vector - _⟨_⟩ : R → Vector n → Vector n - _⟨_⟩ r = map (r *_) - -infix 9 _⟨_⟩ - -opaque - unfolding _∙_ _≊_ - ∙-cong : {v₁ v₂ w₁ w₂ : Vector n} → v₁ ≊ v₂ → w₁ ≊ w₂ → v₁ ∙ w₁ ≈ v₂ ∙ w₂ - ∙-cong {n} ≋v ≋w = sum-cong (zipWith-cong *-cong ≋v ≋w) - -opaque - unfolding Vector - -- The zero vector - zeros : Vector n - zeros {n} = replicate n 0# - -opaque - unfolding Matrix Vector - -- The identity matrix - I : Matrix n n - I {zero} = [] - I {suc n} = (1# ∷ zeros) ∷ map (0# ∷_) I - -opaque - unfolding Matrix Vector - _[_] : Matrix n m → Vector n → Vector m - _[_] M V = map (_∙ V) M - -opaque - unfolding Matrix Vector - [_]_ : Vector m → Matrix n m → Vector n - [_]_ V M = map (V ∙_) (transpose M) - -opaque - unfolding Matrix - mapRows : (Vector n → Vector m) → Matrix n p → Matrix m p - mapRows = map - -opaque - unfolding Matrix Vector - _ᵀ : Matrix n m → Matrix m n - _ᵀ = transpose - -infix 10 _ᵀ - -opaque - unfolding _ᵀ - _ᵀᵀ : (M : Matrix n m) → M ᵀ ᵀ ≡ M - _ᵀᵀ M = transpose-involutive M - -infix 10 _ᵀᵀ - -opaque - unfolding mapRows _ᵀ _[_] [_]_ - -[-]ᵀ : (A : Matrix m o) (B : Matrix n m) → mapRows (A [_]) (B ᵀ) ≡ (mapRows ([_] B) A) ᵀ - -[-]ᵀ [] B = map-replicate [] (transpose B) - -[-]ᵀ (A₀ ∷ A) B = begin - map (λ V → A₀ ∙ V ∷ map (_∙ V) A) (B ᵀ) ≡⟨ zipWith-map (A₀ ∙_) (A [_]) _∷_ (B ᵀ) ⟨ - zipWith _∷_ ([ A₀ ] B) (map (A [_]) (B ᵀ)) ≡⟨ ≡.cong (zipWith _∷_ ([ A₀ ] B)) (-[-]ᵀ A B) ⟩ - zipWith _∷_ ([ A₀ ] B) (transpose (map ([_] B) A)) ∎ - where - open ≡-Reasoning - --- matrix multiplication -_·_ : {n m o : ℕ} → Matrix m o → Matrix n m → Matrix n o -_·_ A B = mapRows ([_] B) A - --- alternative form -_·′_ : Matrix m o → Matrix n m → Matrix n o -_·′_ A B = (mapRows (A [_]) (B ᵀ)) ᵀ - -infixr 9 _·_ _·′_ - -·-·′ : (A : Matrix m o) (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 ᵀ) ᵀ ∎ - where - open ≡-Reasoning - -opaque - unfolding _∙_ zeros - - ∙-zerosˡ : (V : Vector n) → zeros ∙ V ≈ 0# - ∙-zerosˡ [] = refl - ∙-zerosˡ (x ∷ V) = begin - 0# * x + zeros ∙ V ≈⟨ +-congʳ (zeroˡ x) ⟩ - 0# + zeros ∙ V ≈⟨ +-identityˡ (zeros ∙ V) ⟩ - zeros ∙ V ≈⟨ ∙-zerosˡ V ⟩ - 0# ∎ - where - open ≈-Reasoning setoid - - ∙-zerosʳ : (V : Vector n) → V ∙ zeros ≈ 0# - ∙-zerosʳ [] = refl - ∙-zerosʳ (x ∷ V) = begin - x * 0# + V ∙ zeros ≈⟨ +-congʳ (zeroʳ x) ⟩ - 0# + V ∙ zeros ≈⟨ +-identityˡ (V ∙ zeros) ⟩ - V ∙ zeros ≈⟨ ∙-zerosʳ V ⟩ - 0# ∎ - where - open ≈-Reasoning setoid - -opaque - unfolding _∙_ _⊕_ - ∙-distribʳ : (A B C : Vector n) → (A ⊕ B) ∙ C ≈ A ∙ C + B ∙ C - ∙-distribʳ [] [] [] = sym (+-identityˡ 0#) - ∙-distribʳ (a ∷ A) (b ∷ B) (c ∷ C) = begin - (a + b) * c + (zipWith _+_ A B ∙ C) ≈⟨ +-congˡ (∙-distribʳ A B C) ⟩ - (a + b) * c + (A ∙ C + B ∙ C) ≈⟨ +-congʳ (distribʳ c a b) ⟩ - a * c + b * c + (A ∙ C + B ∙ C) ≈⟨ +-assoc _ _ _ ⟩ - a * c + (b * c + (A ∙ C + B ∙ C)) ≈⟨ +-congˡ (+-assoc _ _ _) ⟨ - a * c + (b * c + A ∙ C + B ∙ C) ≈⟨ +-congˡ (+-congʳ (+-comm _ _)) ⟩ - a * c + (A ∙ C + b * c + B ∙ C) ≈⟨ +-congˡ (+-assoc _ _ _) ⟩ - a * c + (A ∙ C + (b * c + B ∙ C)) ≈⟨ +-assoc _ _ _ ⟨ - a * c + A ∙ C + (b * c + B ∙ C) ∎ - where - open ≈-Reasoning setoid - -opaque - unfolding _⟨_⟩ _∙_ - *-∙ˡ : (r : R) (A B : Vector n) → r * A ∙ B ≈ r ⟨ A ⟩ ∙ B - *-∙ˡ r [] [] = zeroʳ r - *-∙ˡ r (a ∷ A) (b ∷ B) = begin - r * (a * b + A ∙ B) ≈⟨ distribˡ r (a * b) (A ∙ B) ⟩ - r * (a * b) + r * A ∙ B ≈⟨ +-congʳ (*-assoc r a b) ⟨ - r * a * b + r * A ∙ B ≈⟨ +-congˡ (*-∙ˡ r A B )⟩ - r * a * b + map (r *_) A ∙ B ∎ - where - open ≈-Reasoning setoid - -module _ where - - open ≈-Reasoning setoid - - opaque - unfolding [_]_ _[_] zeros _∙_ _≋_ _ᵀ _⊕_ _⟨_⟩ - - []-∙ : (V : Vector m) (M : Matrix n m) (W : Vector n) → [ V ] M ∙ W ≈ V ∙ M [ W ] - []-∙ {n = n} [] M@[] W = begin - map (zeros ∙_) (M ᵀ) ∙ W ≈⟨ ∙-cong (PW.map⁺ (λ {x} _ → ∙-zerosˡ x) {xs = M ᵀ} ≋.refl) ≊.refl ⟩ - map (λ _ → 0#) (M ᵀ) ∙ W ≡⟨ ≡.cong (_∙ W) (map-replicate 0# (M ᵀ)) ⟩ - zeros ∙ W ≈⟨ ∙-zerosˡ W ⟩ - 0# ∎ - []-∙ (V₀ ∷ V) (M₀ ∷ M) W = begin - [ V₀ ∷ V ] (M₀ ∷ M) ∙ W ≡⟨ ≡.cong (_∙ W) (map-zipWith ((V₀ ∷ V) ∙_) _∷_ M₀ (M ᵀ)) ⟩ - (zipWith (λ x y → V₀ * x + V ∙ y) M₀ (M ᵀ)) ∙ W ≡⟨ ≡.cong (_∙ W) (zipWith-map-map (V₀ *_) (V ∙_) _+_ M₀ (M ᵀ)) ⟩ - (V₀ ⟨ M₀ ⟩ ⊕ [ V ] M) ∙ W ≈⟨ ∙-distribʳ (map (V₀ *_) M₀) ([ V ] M) W ⟩ - V₀ ⟨ M₀ ⟩ ∙ W + [ V ] M ∙ W ≈⟨ +-congʳ (*-∙ˡ V₀ M₀ W) ⟨ - V₀ * (M₀ ∙ W) + ([ V ] M) ∙ W ≈⟨ +-congˡ ([]-∙ V M W) ⟩ - (V₀ ∷ V) ∙ (M₀ ∷ M) [ W ] ∎ - -opaque - unfolding _≊_ _[_] - -[-]-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} M.≋-refl - -opaque - unfolding _≊_ [_]_ _ᵀ _≋_ - [-]--cong : {x y : Vector m} {A B : Matrix n m} → x ≊ y → A ≋ B → [ x ] A ≊ [ y ] B - [-]--cong {x = x} {y} ≋V A≋B = PW.map⁺ (λ ≋w → ∙-cong ≋V ≋w) (transpose-cong setoid A≋B) - -opaque - unfolding mapRows _[_] _≊_ - ·-[] : {A B C : ℕ} (M : Matrix A B) (N : Matrix B C) (V : Vector A) → (N · M) [ V ] ≊ N [ M [ V ] ] - ·-[] {A} {B} {zero} M [] V = PW.[] - ·-[] {A} {B} {suc C} M (N₀ ∷ N) V = []-∙ N₀ M V PW.∷ ·-[] M N V - -opaque - unfolding [_]_ _ᵀ mapRows _≋_ - []-· : {A B C : ℕ} (V : Vector C) (M : Matrix A B) (N : Matrix B C) → [ V ] (N · M) ≊ [ [ V ] N ] M - []-· {A} {B} {C} V M N = begin - [ V ] (map ([_] M) N) ≡⟨ ≡.cong (map (V ∙_)) (-[-]ᵀ N M) ⟨ - map (V ∙_) (map (N [_]) (M ᵀ)) ≡⟨ map-∘ (V ∙_) (N [_]) (M ᵀ) ⟨ - map ((V ∙_) ∘ (N [_])) (M ᵀ) ≈⟨ PW.map⁺ (λ {W} ≋W → trans ([]-∙ V N W) (∙-cong ≊.refl (-[-]-cong N ≋W))) {xs = M ᵀ} ≋.refl ⟨ - map ([ V ] N ∙_) (M ᵀ) ∎ - where - open ≈-Reasoning (≊-setoid A) - -opaque - unfolding mapRows _≋_ _ᵀ - ·-assoc : {A B C D : ℕ} {f : Matrix A B} {g : Matrix B C} {h : Matrix C D} → (h · g) · f ≋ h · g · f - ·-assoc {A} {B} {C} {D} {f} {g} {h} = begin - map ([_] f) (map ([_] g) h) ≡⟨ map-∘ ([_] f) ([_] g) h ⟨ - map (λ v → [ [ v ] g ] f) h ≈⟨ PW.map⁺ (λ {x} x≊y → ≊.trans ([]-· x f g) ([-]--cong ([-]--cong x≊y ≋.refl) ≋.refl)) {xs = h} M.≋-refl ⟨ - map (λ v → [ v ] (g · f)) h ∎ - where - open ≈-Reasoning (≋-setoid A D) - -opaque - unfolding _≋_ _ᵀ _≊_ ≊-setoid I zeros - transpose-I : I ᵀ ≡ I {n} - transpose-I {zero} = ≡.refl - transpose-I {suc n} = begin - zipWith _∷_ (1# ∷ zeros) ((map (0# ∷_) I) ᵀ) ≡⟨ ≡.cong (zipWith _∷_ (1# ∷ zeros) ∘ (_ᵀ)) (zipWith-replicate₁ _∷_ 0# I) ⟨ - zipWith _∷_ (1# ∷ zeros) ((zipWith _∷_ zeros I) ᵀ) ≡⟨ ≡.cong (zipWith _∷_ (1# ∷ zeros)) (transpose-zipWith zeros I) ⟩ - (1# ∷ zeros) ∷ zipWith _∷_ zeros (I ᵀ) ≡⟨ ≡.cong ((1# ∷ zeros) ∷_) (zipWith-replicate₁ _∷_ 0# (I ᵀ)) ⟩ - (1# ∷ zeros) ∷ map (0# ∷_) (I ᵀ) ≡⟨ ≡.cong (((1# ∷ zeros) ∷_) ∘ map (0# ∷_)) (transpose-I) ⟩ - (1# ∷ zeros) ∷ map (0# ∷_) I ∎ - where - open ≡-Reasoning - -opaque - unfolding Vector [_]_ I ≊-setoid _∙_ zeros ≋-setoid mapRows _ᵀ - [-]I : {n : ℕ} (V : Vector n) → [ V ] I ≊ V - [-]I {zero} [] = ≊.refl - [-]I {suc n} (x ∷ V) = begin - map ((x ∷ V) ∙_) (zipWith _∷_ (1# ∷ zeros) (map (0# ∷_ ) I ᵀ)) ≡⟨ ≡.cong (map ((x ∷ V) ∙_) ∘ zipWith _∷_ (1# ∷ zeros) ∘ _ᵀ) (zipWith-replicate₁ _∷_ 0# I) ⟨ - map ((x ∷ V) ∙_) (zipWith _∷_ (1# ∷ zeros) (zipWith _∷_ zeros I ᵀ)) ≡⟨ ≡.cong (map ((x ∷ V) ∙_) ∘ zipWith _∷_ (1# ∷ zeros)) (transpose-zipWith zeros I) ⟩ - map ((x ∷ V) ∙_) (zipWith _∷_ (1# ∷ zeros) (zeros ∷ I ᵀ)) ≡⟨ ≡.cong (map ((x ∷ V) ∙_) ∘ zipWith _∷_ (1# ∷ zeros) ∘ (zeros ∷_)) transpose-I ⟩ - map ((x ∷ V) ∙_) (zipWith _∷_ (1# ∷ zeros) (zeros ∷ I)) ≡⟨⟩ - map ((x ∷ V) ∙_) ((1# ∷ zeros) ∷ zipWith _∷_ zeros I) ≡⟨ ≡.cong (map ((x ∷ V) ∙_) ∘ ((1# ∷ zeros) ∷_)) (zipWith-replicate₁ _∷_ 0# I) ⟩ - map ((x ∷ V) ∙_) ((1# ∷ zeros) ∷ map (0# ∷_) I) ≡⟨⟩ - (x ∷ V) ∙ (1# ∷ zeros) ∷ map ((x ∷ V) ∙_) ((map (0# ∷_) I)) ≡⟨⟩ - x * 1# + V ∙ zeros ∷ map ((x ∷ V) ∙_) (map (0# ∷_) I) ≈⟨ +-congʳ (*-identityʳ x) PW.∷ ≊.refl ⟩ - x + V ∙ zeros ∷ map ((x ∷ V) ∙_) (map (0# ∷_) I) ≈⟨ +-congˡ (∙-zerosʳ V) PW.∷ ≊.refl ⟩ - x + 0# ∷ map ((x ∷ V) ∙_) (map (0# ∷_) I) ≈⟨ +-identityʳ x PW.∷ ≊.refl ⟩ - x ∷ map ((x ∷ V) ∙_) (map (0# ∷_) I) ≡⟨ ≡.cong (x ∷_) (map-∘ ((x ∷ V) ∙_) (0# ∷_) I) ⟨ - x ∷ map (λ u → (x ∷ V) ∙ (0# ∷ u)) I ≡⟨⟩ - x ∷ map (λ u → x * 0# + V ∙ u) I ≈⟨ refl PW.∷ PW.map⁺ (λ ≋V → trans (+-congʳ (zeroʳ x)) (+-congˡ (∙-cong {v₁ = V} ≊.refl ≋V))) {xs = I} ≋.refl ⟩ - x ∷ map (λ u → 0# + V ∙ u) I ≈⟨ refl PW.∷ PW.map⁺ (λ {z} ≋V → trans (+-identityˡ (V ∙ z)) (∙-cong {v₁ = V} ≊.refl ≋V)) {xs = I} ≋.refl ⟩ - x ∷ map (V ∙_) I ≡⟨ ≡.cong (λ y → x ∷ map (V ∙_) y) transpose-I ⟨ - x ∷ map (V ∙_) (I ᵀ) ≈⟨ refl PW.∷ ([-]I V) ⟩ - x ∷ V ∎ - where - open ≈-Reasoning (≊-setoid (suc n)) - -opaque - unfolding Vector _≊_ I _[_] _∙_ _≋_ - transform-with-I : {n : ℕ} (V : Vector n) → I [ V ] ≊ V - transform-with-I {zero} [] = PW.[] - transform-with-I {suc n} (x ∷ V) = hd PW.∷ tl - where - hd : (1# ∷ zeros) ∙ (x ∷ V) ≈ x - hd = begin - 1# * x + zeros ∙ V ≈⟨ +-congʳ (*-identityˡ x) ⟩ - x + zeros ∙ V ≈⟨ +-congˡ (∙-zerosˡ V) ⟩ - x + 0# ≈⟨ +-identityʳ x ⟩ - x ∎ - where - open ≈-Reasoning setoid - tl : map (_∙ (x ∷ V)) (map (0# ∷_ ) I) ≊ V - tl = begin - map (_∙ (x ∷ V)) (map (0# ∷_) I) ≡⟨ map-∘ (_∙ (x ∷ V)) (0# ∷_) I ⟨ - map (λ t → 0# * x + t ∙ V) I ≈⟨ PW.map⁺ (λ ≋X → trans (+-congʳ (zeroˡ x)) (+-congˡ (∙-cong ≋X ≊.refl))) {xs = I} ≋.refl ⟩ - map (λ t → 0# + t ∙ V) I ≈⟨ PW.map⁺ (λ {t} ≋X → trans (+-identityˡ (t ∙ V)) (∙-cong ≋X ≊.refl)) {xs = I} ≋.refl ⟩ - map (_∙ V) I ≈⟨ transform-with-I V ⟩ - V ∎ - where - open ≈-Reasoning (≊-setoid n) - -opaque - unfolding mapRows _[_] _ᵀ _≋_ _≊_ [_]_ - map--[-]-I : (M : Matrix n m) → mapRows (M [_]) I ≋ M ᵀ - map--[-]-I {n} {m} [] = ≋.reflexive (map-replicate [] I) - map--[-]-I {n} {suc m} (M₀ ∷ M) = begin - map ((M₀ ∷ M) [_]) I ≡⟨⟩ - map (λ V → M₀ ∙ V ∷ M [ V ]) I ≡⟨ zipWith-map (M₀ ∙_) (M [_]) _∷_ I ⟨ - zipWith _∷_ (map (M₀ ∙_) I) (map (M [_]) I) ≈⟨ zipWith-cong PW._∷_ (≊.reflexive (≡.sym (≡.cong (map (M₀ ∙_)) (transpose-I)))) (map--[-]-I M) ⟩ - zipWith _∷_ ([ M₀ ] I) (M ᵀ) ≈⟨ zipWith-cong PW._∷_ ([-]I M₀) ≋.refl ⟩ - zipWith _∷_ M₀ (M ᵀ) ∎ - where - open ≈-Reasoning (≋-setoid (suc m) n) - -opaque - unfolding mapRows ≋-setoid _ᵀ - ·-identityˡ : {f : Matrix n m} → I · f ≋ f - ·-identityˡ {A} {B} {f} = begin - I · f ≡⟨ ·-·′ I f ⟩ - map (I [_]) (f ᵀ) ᵀ ≈⟨ transpose-cong setoid (PW.map⁺ (λ {x} ≊V → ≊.trans (transform-with-I x) ≊V) {xs = f ᵀ} ≋.refl) ⟩ - map id (f ᵀ) ᵀ ≡⟨ ≡.cong (_ᵀ) (map-id (f ᵀ)) ⟩ - f ᵀ ᵀ ≡⟨ f ᵀᵀ ⟩ - f ∎ - where - open ≈-Reasoning (≋-setoid A B) - -opaque - unfolding _≋_ mapRows ≊-setoid ≋-setoid _≊_ _ᵀ - ·-identityʳ : {f : Matrix n m} → f · I ≋ f - ·-identityʳ {A} {B} {f} = begin - f · I ≡⟨ ·-·′ f I ⟩ - map (f [_]) (I ᵀ) ᵀ ≈⟨ transpose-cong setoid (≋.reflexive (≡.cong (map (f [_])) transpose-I)) ⟩ - map (f [_]) I ᵀ ≈⟨ transpose-cong setoid (map--[-]-I f) ⟩ - f ᵀ ᵀ ≡⟨ f ᵀᵀ ⟩ - f ∎ - where - open ≈-Reasoning (≋-setoid A B) - -opaque - unfolding _ᵀ _≋_ mapRows - ·-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 - --- The category of matrices over a rig -Mat : Category 0ℓ c (c ⊔ ℓ) -Mat = categoryHelper record - { Obj = ℕ - ; _⇒_ = Matrix - ; _≈_ = _≋_ - ; id = I - ; _∘_ = _·_ - ; assoc = λ {A B C D f g h} → ·-assoc {f = f} {g} {h} - ; identityˡ = ·-identityˡ - ; identityʳ = ·-identityʳ - ; equiv = ≋-isEquivalence - ; ∘-resp-≈ = ·-resp-≋ - } diff --git a/Data/Mat/Cocartesian.agda b/Data/Mat/Cocartesian.agda deleted file mode 100644 index 5ea92b3..0000000 --- a/Data/Mat/Cocartesian.agda +++ /dev/null @@ -1,623 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Algebra.Bundles using (Semiring) -open import Level using (Level) - -module Data.Mat.Cocartesian {c ℓ : Level} (Rig : Semiring c ℓ) where - -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -import Data.Vec.Relation.Binary.Pointwise.Inductive as PW - -open import Data.Mat.Category Rig - using - ( Mat; Matrix; Vector; zeros; I; _≊_; module ≊; ≊-setoid; _≋_; module ≋; ≋-setoid - ; _ᵀ; mapRows; _·_; _∙_; _ᵀᵀ; _⊕_; ·-identityʳ; ∙-zerosʳ; ∙-zerosˡ - ) - renaming ([_]_ to [_]′_) - -open import Categories.Category.Cocartesian Mat using (Cocartesian) -open import Categories.Object.Coproduct Mat using (Coproduct) -open import Categories.Object.Initial Mat using (Initial) -open import Data.Mat.Util using (replicate-++; zipWith-map; transpose-zipWith; zipWith-cong) -open import Data.Nat as ℕ using (ℕ) -open import Data.Product using (_,_; Σ-syntax) -open import Data.Vec using (Vec; map; zipWith; replicate; _++_; head; tail) -open import Data.Vec.Properties using (zipWith-replicate; map-cong; map-const; map-id) -open import Function using (id; _∘_) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) - -open Semiring Rig renaming (Carrier to R) -open Vec -open ℕ.ℕ - -private - variable - A B C D : ℕ - A₁ A₂ B₁ B₂ : ℕ - -opaque - unfolding Vector - _+++_ : Vector A → Vector B → Vector (A ℕ.+ B) - _+++_ = _++_ - -opaque - unfolding Matrix Vector - _∥_ : Matrix A C → Matrix B C → Matrix (A ℕ.+ B) C - _∥_ M N = zipWith _++_ M N - -opaque - unfolding Matrix - [_] : Vector A → Matrix A 1 - [_] V = V ∷ [] - -opaque - unfolding Matrix Vector - ⟦_⟧ : R → Matrix 1 1 - ⟦_⟧ x = [ x ∷ [] ] - -[_]ᵀ : Vector A → Matrix 1 A -[_]ᵀ V = [ V ] ᵀ - -opaque - unfolding Vector - ⟨⟩ : Vector 0 - ⟨⟩ = [] - -opaque - unfolding Vector - _∷′_ : R → Vector A → Vector (suc A) - _∷′_ = _∷_ - -infixr 5 _∷′_ - -infixr 7 _∥_ - -opaque - unfolding Matrix - _≑_ : Matrix A B → Matrix A C → Matrix A (B ℕ.+ C) - _≑_ M N = M ++ N - -infixr 6 _≑_ - -opaque - unfolding Matrix - _∷ᵥ_ : Vector A → Matrix A B → Matrix A (suc B) - _∷ᵥ_ V M = V ∷ M - -infixr 5 _∷ᵥ_ - -opaque - unfolding Matrix Vector - _∷ₕ_ : Vector B → Matrix A B → Matrix (suc A) B - _∷ₕ_ V M = zipWith _∷_ V M - -infixr 5 _∷ₕ_ - -opaque - unfolding Matrix - headᵥ : Matrix A (suc B) → Vector A - headᵥ (V ∷ _) = V - -opaque - unfolding Matrix - tailᵥ : Matrix A (suc B) → Matrix A B - tailᵥ (_ ∷ M) = M - -opaque - unfolding Matrix Vector - headₕ : Matrix (suc A) B → Vector B - headₕ M = map head M - -opaque - unfolding Matrix Vector - tailₕ : Matrix (suc A) B → Matrix A B - tailₕ M = map tail M - -opaque - unfolding _∷ᵥ_ headᵥ tailᵥ - head-∷-tailᵥ : (M : Matrix A (suc B)) → headᵥ M ∷ᵥ tailᵥ M ≡ M - head-∷-tailᵥ (_ ∷ _) = ≡.refl - -opaque - unfolding _∷ₕ_ headₕ tailₕ - head-∷-tailₕ : (M : Matrix (suc A) B) → headₕ M ∷ₕ tailₕ M ≡ M - head-∷-tailₕ M = begin - zipWith _∷_ (map head M) (map 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 - -opaque - unfolding Matrix - []ₕ : Matrix A 0 - []ₕ = [] - -opaque - unfolding []ₕ _ᵀ - []ᵥ : Matrix 0 B - []ᵥ = []ₕ ᵀ - -opaque - unfolding []ᵥ - []ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A} - []ᵥ-ᵀ = []ₕ ᵀᵀ - -opaque - unfolding []ₕ - []ₕ-! : (E : Matrix A 0) → E ≡ []ₕ - []ₕ-! [] = ≡.refl - -opaque - unfolding []ᵥ - []ᵥ-! : (E : Matrix 0 B) → E ≡ []ᵥ - []ᵥ-! [] = ≡.refl - []ᵥ-! ([] ∷ E) = ≡.cong ([] ∷_) ([]ᵥ-! E) - -opaque - unfolding Matrix Vector - _∷[_,_]_ : R → Vector B → Vector A → Matrix A B → Matrix (suc A) (suc B) - _∷[_,_]_ v C R M = (v ∷ R) ∷ᵥ (C ∷ₕ M) - -opaque - unfolding Matrix - 𝟎 : Matrix A B - 𝟎 {A} {B} = replicate B zeros - -opaque - unfolding 𝟎 _ᵀ zeros _∷ₕ_ _∥_ - 𝟎ᵀ : 𝟎 ᵀ ≡ 𝟎 {A} {B} - 𝟎ᵀ {zero} = ≡.refl - 𝟎ᵀ {suc A} = begin - zeros ∷ₕ (𝟎 ᵀ) ≡⟨ ≡.cong (zeros ∷ₕ_) 𝟎ᵀ ⟩ - zeros ∷ₕ 𝟎 ≡⟨ zipWith-replicate _∷_ 0# zeros ⟩ - 𝟎 ∎ - where - open ≡-Reasoning - -opaque - unfolding _∥_ []ᵥ - []ᵥ-∥ : (M : Matrix A B) → []ᵥ ∥ M ≡ M - []ᵥ-∥ [] = ≡.refl - []ᵥ-∥ (M₀ ∷ M) = ≡.cong (M₀ ∷_) ([]ᵥ-∥ M) - -opaque - unfolding _≑_ []ₕ - []ₕ-≑ : (M : Matrix A B) → []ₕ ≑ M ≡ M - []ₕ-≑ _ = ≡.refl - -opaque - unfolding _∷ₕ_ _ᵀ _∷ᵥ_ - ∷ₕ-ᵀ : (V : Vector A) (M : Matrix B A) → (V ∷ₕ M) ᵀ ≡ V ∷ᵥ M ᵀ - ∷ₕ-ᵀ = transpose-zipWith - -opaque - unfolding _∷ₕ_ _ᵀ _∷ᵥ_ - ∷ᵥ-ᵀ : (V : Vector B) (M : Matrix B A) → (V ∷ᵥ M) ᵀ ≡ V ∷ₕ M ᵀ - ∷ᵥ-ᵀ V M = ≡.refl - -opaque - unfolding _∷ₕ_ _∥_ - ∷ₕ-∥ : (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) - -opaque - unfolding _∷ᵥ_ _≑_ - ∷ᵥ-≑ : (V : Vector A) (M : Matrix A B) (N : Matrix A C) → V ∷ᵥ (M ≑ N) ≡ (V ∷ᵥ M) ≑ N - ∷ᵥ-≑ V M N = ≡.refl - -opaque - unfolding zeros [_]′_ Matrix _∙_ - [-]- : (V : Vector 0) (E : Matrix A 0) → [ V ]′ E ≡ zeros - [-]- {zero} _ [] = ≡.refl - [-]- {suc A} [] [] = ≡.cong (0# ∷_) ([-]- [] []) - -opaque - unfolding ⟨⟩ _+++_ - ⟨⟩-+++ : (V : Vector A) → ⟨⟩ +++ V ≡ V - ⟨⟩-+++ V = ≡.refl - -opaque - unfolding _∷′_ _+++_ - ∷-+++ : (x : R) (M : Vector A) (N : Vector B) → (x ∷′ M) +++ N ≡ x ∷′ (M +++ N) - ∷-+++ x M N = ≡.refl - -opaque - unfolding []ₕ [_]′_ _ᵀ []ᵥ ⟨⟩ - [-]-[]ᵥ : (V : Vector A) → [ V ]′ []ᵥ ≡ ⟨⟩ - [-]-[]ᵥ [] = ≡.refl - [-]-[]ᵥ (x ∷ V) = ≡.cong (map ((x ∷ V) ∙_)) []ᵥ-ᵀ - -opaque - unfolding [_]′_ _ᵀ _∷ᵥ_ _∷′_ - [-]-∷ₕ : (V M₀ : Vector B) (M : Matrix A B) → [ V ]′ (M₀ ∷ₕ M) ≡ V ∙ M₀ ∷′ ([ V ]′ M) - [-]-∷ₕ V M₀ M = ≡.cong (map (V ∙_)) (∷ₕ-ᵀ M₀ M) - where - open ≡-Reasoning - -[-]--∥ - : (V : Vector C) - (M : Matrix A C) - (N : Matrix B C) - → [ V ]′ (M ∥ N) ≡ ([ V ]′ M) +++ ([ V ]′ N) -[-]--∥ {C} {zero} V M N rewrite []ᵥ-! M = begin - [ V ]′ ([]ᵥ ∥ N) ≡⟨ ≡.cong ([ V ]′_) ([]ᵥ-∥ N) ⟩ - [ V ]′ N ≡⟨ ⟨⟩-+++ ([ V ]′ N) ⟨ - ⟨⟩ +++ ([ V ]′ N) ≡⟨ ≡.cong (_+++ ([ V ]′ N)) ([-]-[]ᵥ V) ⟨ - ([ V ]′ []ᵥ) +++ ([ V ]′ N) ∎ - where - open ≡-Reasoning -[-]--∥ {C} {suc A} V M N - rewrite ≡.sym (head-∷-tailₕ M) - using M₀ ← headₕ M - using M ← tailₕ M = begin - [ V ]′ ((M₀ ∷ₕ M) ∥ N) ≡⟨ ≡.cong ([ V ]′_) (∷ₕ-∥ M₀ M N) ⟨ - [ V ]′ (M₀ ∷ₕ (M ∥ N)) ≡⟨ [-]-∷ₕ V M₀ (M ∥ N) ⟩ - V ∙ M₀ ∷′ ([ V ]′ (M ∥ N)) ≡⟨ ≡.cong (V ∙ M₀ ∷′_) ([-]--∥ V M N) ⟩ - V ∙ M₀ ∷′ (([ V ]′ M) +++ ([ V ]′ N)) ≡⟨ ∷-+++ (V ∙ M₀) ([ V ]′ M) ([ V ]′ N) ⟨ - (V ∙ M₀ ∷′ [ V ]′ M) +++ ([ V ]′ N) ≡⟨ ≡.cong (_+++ ([ V ]′ N)) ([-]-∷ₕ V M₀ M) ⟨ - ([ V ]′ (M₀ ∷ₕ M)) +++ ([ V ]′ N) ∎ - where - open ≡-Reasoning - -opaque - unfolding _∥_ mapRows _+++_ - ·-∥ - : (M : Matrix C D) - (N : Matrix A C) - (P : Matrix B C) - → M · (N ∥ P) ≡ M · N ∥ M · P - ·-∥ {C} {D} {A} {B} [] N P = ≡.refl - ·-∥ {C} {D} {A} {B} (M₀ ∷ M) N P = ≡.cong₂ _∷_ ([-]--∥ M₀ N P) (·-∥ M N P) - -opaque - unfolding _≑_ mapRows - ≑-· : (M : Matrix B C) - (N : Matrix B D) - (P : Matrix A B) - → (M ≑ N) · P ≡ (M · P) ≑ (N · P) - ≑-· [] N P = ≡.refl - ≑-· (M₀ ∷ M) N P = ≡.cong ([ M₀ ]′ P ∷_) (≑-· M N P) - -opaque - unfolding Matrix - _[+]_ : Matrix A B → Matrix A B → Matrix A B - _[+]_ = zipWith _⊕_ - -opaque - unfolding _+++_ _≑_ _∷ₕ_ - ∷ₕ-≑ : (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) - -opaque - unfolding _+++_ _∙_ - ∙-+++ : (W Y : Vector A) (X Z : Vector B) → (W +++ X) ∙ (Y +++ Z) ≈ W ∙ Y + X ∙ Z - ∙-+++ [] [] X Z = sym (+-identityˡ (X ∙ Z)) - ∙-+++ (w ∷ W) (y ∷ Y) X Z = begin - w * y + (W ++ X) ∙ (Y ++ Z) ≈⟨ +-congˡ (∙-+++ W Y X Z) ⟩ - w * y + (W ∙ Y + X ∙ Z) ≈⟨ +-assoc _ _ _ ⟨ - (w * y + W ∙ Y) + X ∙ Z ∎ - where - open ≈-Reasoning setoid - -opaque - unfolding []ᵥ _≑_ - []ᵥ-≑ : []ᵥ {A} ≑ []ᵥ {B} ≡ []ᵥ - []ᵥ-≑ {A} {B} = replicate-++ A B [] - -opaque - unfolding _⊕_ ⟨⟩ - ⟨⟩-⊕ : ⟨⟩ ⊕ ⟨⟩ ≡ ⟨⟩ - ⟨⟩-⊕ = ≡.refl - -opaque - unfolding ≊-setoid _∷′_ _⊕_ - [+++]-≑ - : (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 ]′ ([]ᵥ {B} ≑ []ᵥ) ≡⟨ ≡.cong ([ V +++ W ]′_) []ᵥ-≑ ⟩ - [ V +++ W ]′ []ᵥ ≡⟨ [-]-[]ᵥ (V +++ W) ⟩ - ⟨⟩ ≡⟨ ⟨⟩-⊕ ⟨ - ⟨⟩ ⊕ ⟨⟩ ≡⟨ ≡.cong₂ _⊕_ ([-]-[]ᵥ V) ([-]-[]ᵥ W) ⟨ - [ V ]′ []ᵥ ⊕ [ W ]′ []ᵥ ∎ - where - open ≈-Reasoning (≊-setoid 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)) ≡⟨ [-]-∷ₕ (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₂ _⊕_ ([-]-∷ₕ V M₀ M) ([-]-∷ₕ W N₀ N) ⟨ - ([ V ]′ (M₀ ∷ₕ M)) ⊕ ([ W ]′ (N₀ ∷ₕ N)) ∎ - where - open ≈-Reasoning (≊-setoid (suc A)) - -opaque - unfolding _∥_ _+++_ mapRows _[+]_ ≋-setoid - ∥-·-≑ - : (W : Matrix A C) - (X : Matrix B C) - (Y : Matrix D A) - (Z : Matrix D B) - → (W ∥ X) · (Y ≑ Z) ≋ (W · Y) [+] (X · Z) - ∥-·-≑ [] [] Y Z = PW.[] - ∥-·-≑ {A} {C} {B} {D} (W₀ ∷ W) (X₀ ∷ X) Y Z = [+++]-≑ W₀ X₀ Y Z PW.∷ ∥-·-≑ W X Y Z - where - open ≈-Reasoning (≋-setoid A B) - -opaque - unfolding _⊕_ _≊_ - ⊕-cong : {V V′ W W′ : Vector A} → V ≊ V′ → W ≊ W′ → V ⊕ W ≊ V′ ⊕ W′ - ⊕-cong = zipWith-cong +-cong - -opaque - unfolding _[+]_ _≋_ - [+]-cong : {M M′ N N′ : Matrix A B} → M ≋ M′ → N ≋ N′ → M [+] N ≋ M′ [+] N′ - [+]-cong = zipWith-cong ⊕-cong - -opaque - unfolding ⟨⟩ []ₕ [_]′_ zeros _∙_ - [⟨⟩]-[]ₕ : [ ⟨⟩ ]′ ([]ₕ {A}) ≡ zeros {A} - [⟨⟩]-[]ₕ {zero} = ≡.refl - [⟨⟩]-[]ₕ {suc A} = ≡.cong (0# ∷_) [⟨⟩]-[]ₕ - -opaque - unfolding Vector ⟨⟩ zeros []ᵥ [_]′_ _ᵀ _∷ₕ_ 𝟎 _≊_ - [-]-𝟎 : (V : Vector A) → [ V ]′ (𝟎 {B}) ≊ zeros - [-]-𝟎 {A} {zero} V = ≊.reflexive (≡.cong (map (V ∙_)) 𝟎ᵀ) - [-]-𝟎 {A} {suc B} V = begin - map (V ∙_) (𝟎 ᵀ) ≡⟨ ≡.cong (map (V ∙_)) 𝟎ᵀ ⟩ - V ∙ zeros ∷ map (V ∙_) 𝟎 ≡⟨ ≡.cong ((V ∙ zeros ∷_) ∘ map (V ∙_)) 𝟎ᵀ ⟨ - V ∙ zeros ∷ [ V ]′ 𝟎 ≈⟨ ∙-zerosʳ V PW.∷ ([-]-𝟎 V) ⟩ - 0# ∷ zeros ∎ - where - open ≈-Reasoning (≊-setoid (suc B)) - -opaque - unfolding _⊕_ zeros _≊_ - ⊕-zerosʳ : (V : Vector A) → V ⊕ zeros ≊ V - ⊕-zerosʳ [] = PW.[] - ⊕-zerosʳ (x ∷ V) = +-identityʳ x PW.∷ ⊕-zerosʳ V - -opaque - unfolding _⊕_ zeros _≊_ - ⊕-zerosˡ : (V : Vector A) → zeros ⊕ V ≊ V - ⊕-zerosˡ [] = PW.[] - ⊕-zerosˡ (x ∷ V) = +-identityˡ x PW.∷ ⊕-zerosˡ V - -opaque - unfolding Matrix _[+]_ _≋_ 𝟎 - [+]-𝟎ʳ : (M : Matrix A B) → M [+] 𝟎 ≋ M - [+]-𝟎ʳ [] = PW.[] - [+]-𝟎ʳ (M₀ ∷ M) = ⊕-zerosʳ M₀ PW.∷ [+]-𝟎ʳ M - -opaque - unfolding Matrix _[+]_ _≋_ 𝟎 - [+]-𝟎ˡ : (M : Matrix A B) → 𝟎 [+] M ≋ M - [+]-𝟎ˡ [] = PW.[] - [+]-𝟎ˡ (M₀ ∷ M) = ⊕-zerosˡ M₀ PW.∷ [+]-𝟎ˡ M - - -opaque - unfolding ≋-setoid mapRows 𝟎 - ·-𝟎ʳ : (M : Matrix A B) → M · 𝟎 {C} ≋ 𝟎 - ·-𝟎ʳ [] = ≋.refl - ·-𝟎ʳ (M₀ ∷ M) = begin - [ M₀ ]′ 𝟎 ∷ M · 𝟎 ≈⟨ [-]-𝟎 M₀ PW.∷ ·-𝟎ʳ M ⟩ - zeros ∷ 𝟎 ∎ - where - open ≈-Reasoning (≋-setoid _ _) - -opaque - unfolding Matrix zeros ≊-setoid _∷′_ ⟨⟩ - [zeros]- : (M : Matrix A B) → [ zeros ]′ M ≊ zeros - [zeros]- {zero} M rewrite []ᵥ-! M = ≊.reflexive ([-]-[]ᵥ zeros) - [zeros]- {suc A} M - rewrite ≡.sym (head-∷-tailₕ M) - using M₀ ← headₕ M - using M ← tailₕ M = begin - [ zeros ]′ (M₀ ∷ₕ M) ≡⟨ [-]-∷ₕ zeros M₀ M ⟩ - zeros ∙ M₀ ∷ [ zeros ]′ M ≈⟨ ∙-zerosˡ M₀ PW.∷ [zeros]- M ⟩ - 0# ∷ zeros ∎ - where - open ≈-Reasoning (≊-setoid _) - -opaque - unfolding ≋-setoid mapRows 𝟎 _ᵀ []ᵥ - ·-𝟎ˡ : (M : Matrix A B) → 𝟎 {B} {C} · M ≋ 𝟎 - ·-𝟎ˡ {A} {B} {zero} M = PW.[] - ·-𝟎ˡ {A} {B} {suc C} M = [zeros]- M PW.∷ ·-𝟎ˡ M - -opaque - unfolding ≋-setoid - inj₁ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (I ≑ 𝟎) ≋ M - inj₁ {A} {C} M N = begin - (M ∥ N) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ M N I 𝟎 ⟩ - (M · I) [+] (N · 𝟎) ≈⟨ [+]-cong ·-identityʳ (·-𝟎ʳ N) ⟩ - M [+] 𝟎 ≈⟨ [+]-𝟎ʳ M ⟩ - M ∎ - where - open ≈-Reasoning (≋-setoid A C) - -opaque - unfolding ≋-setoid - inj₂ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (𝟎 ≑ I) ≋ N - inj₂ {A} {C} {B} M N = begin - (M ∥ N) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ M N 𝟎 I ⟩ - (M · 𝟎) [+] (N · I) ≈⟨ [+]-cong (·-𝟎ʳ M) ·-identityʳ ⟩ - 𝟎 [+] N ≈⟨ [+]-𝟎ˡ N ⟩ - N ∎ - where - open ≈-Reasoning (≋-setoid B C) - -opaque - unfolding Matrix - split-∥ : (A : ℕ) → (M : Matrix (A ℕ.+ B) C) → Σ[ M₁ ∈ Matrix A C ] Σ[ M₂ ∈ Matrix B C ] M₁ ∥ M₂ ≡ M - split-∥ zero M = []ᵥ , M , []ᵥ-∥ M - split-∥ (suc A) M′ - rewrite ≡.sym (head-∷-tailₕ M′) - using M₀ ← headₕ M′ - using M ← tailₕ M′ - with split-∥ A M - ... | M₁ , M₂ , M₁∥M₂≡M = M₀ ∷ₕ M₁ , M₂ , (begin - (M₀ ∷ₕ M₁) ∥ M₂ ≡⟨ ∷ₕ-∥ M₀ M₁ M₂ ⟨ - M₀ ∷ₕ M₁ ∥ M₂ ≡⟨ ≡.cong (M₀ ∷ₕ_) M₁∥M₂≡M ⟩ - M₀ ∷ₕ M ∎) - where - open ≡-Reasoning - -opaque - unfolding _≋_ _∷ₕ_ - ∷ₕ-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) - -opaque - unfolding Vector - head′ : Vector (suc A) → R - head′ = head - -opaque - unfolding Vector - tail′ : Vector (suc A) → Vector A - tail′ = tail - -opaque - unfolding _≊_ head′ - head-cong : {V V′ : Vector (suc A)} → V ≊ V′ → head′ V ≈ head′ V′ - head-cong (≈x PW.∷ _) = ≈x - -opaque - unfolding _≊_ 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′ - -opaque - unfolding _≋_ tailₕ tail′ - ≋tailₕ : {M M′ : Matrix (suc A) B} → M ≋ M′ → tailₕ M ≋ tailₕ M′ - ≋tailₕ M≋M′ = PW.map⁺ tail-cong M≋M′ - -opaque - unfolding _≋_ _≊_ _∷ₕ_ - _≋∷ₕ_ : {V V′ : Vector B} → V ≊ V′ → {M M′ : Matrix A B} → M ≋ M′ → V ∷ₕ M ≋ V′ ∷ₕ M′ - _≋∷ₕ_ PW.[] PW.[] = PW.[] - _≋∷ₕ_ (≈x PW.∷ ≊V) (≊M₀ PW.∷ ≋M) = (≈x PW.∷ ≊M₀) PW.∷ (≊V ≋∷ₕ ≋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 (≋-setoid _ _) - ∥-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 (≊-setoid _) - ≋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 (≋-setoid _ _) - open ≈-Reasoning (≋-setoid _ _) - -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 ≋-setoid - uniq - : (H : Matrix (A ℕ.+ B) C) - (M : Matrix A C) - (N : Matrix B C) - → H · (I ≑ 𝟎) ≋ M - → H · (𝟎 ≑ I) ≋ N - → M ∥ N ≋ H - uniq {A} {B} {C} H M N eq₁ eq₂ - with (H₁ , H₂ , H₁∥H₂≡H) ← split-∥ A H - rewrite ≡.sym H₁∥H₂≡H = begin - M ∥ N ≈⟨ ∥-cong eq₁ eq₂ ⟨ - (H₁ ∥ H₂) · (I {A} ≑ 𝟎) ∥ (H₁ ∥ H₂) · (𝟎 ≑ I) ≈⟨ ∥-cong (inj₁ H₁ H₂) (inj₂ H₁ H₂) ⟩ - (H₁ ∥ H₂) ∎ - where - open ≈-Reasoning (≋-setoid (A ℕ.+ B) C) - -coproduct : Coproduct A B -coproduct {A} {B} = record - { A+B = A ℕ.+ B - ; i₁ = I ≑ 𝟎 - ; i₂ = 𝟎 ≑ I - ; [_,_] = _∥_ - ; inject₁ = λ {a} {b} {c} → inj₁ b c - ; inject₂ = λ {a} {b} {c} → inj₂ b c - ; unique = λ eq₁ eq₂ → uniq _ _ _ eq₁ eq₂ - } - -opaque - unfolding _≋_ - !-unique : (E : Matrix 0 B) → []ᵥ ≋ E - !-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E)) - -initial : Initial -initial = record - { ⊥ = 0 - ; ⊥-is-initial = record - { ! = []ᵥ - ; !-unique = !-unique - } - } - -Mat-Cocartesian : Cocartesian -Mat-Cocartesian = record - { initial = initial - ; coproducts = record - { coproduct = coproduct - } - } diff --git a/Data/Mat/Dagger-2-Poset.agda b/Data/Mat/Dagger-2-Poset.agda deleted file mode 100644 index cb939d1..0000000 --- a/Data/Mat/Dagger-2-Poset.agda +++ /dev/null @@ -1,79 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Algebra using (Idempotent; CommutativeSemiring) -open import Level using (Level) - -module Data.Mat.Dagger-2-Poset - {c ℓ : Level} - (Rig : CommutativeSemiring c ℓ) - (let module Rig = CommutativeSemiring Rig) - (+-idem : Idempotent Rig._≈_ Rig._+_) - where - -import Data.Vec.Relation.Binary.Pointwise.Inductive as PW -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning - -open import Data.Mat.Util using (transpose-cong; replicate-++) -open import Data.Mat.Category Rig.semiring - using - ( Mat; _ᵀ; transpose-I; I; _≋_; module ≋; _≊_; Matrix; Vector - ; ≋-setoid; _·_; ·-identityˡ; ·-identityʳ; ·-resp-≋; ·-assoc; _⊕_ - ) -open import Data.Mat.Cocartesian Rig.semiring - using - ( 𝟎 ; _∥_; _≑_; ∥-cong; ≑-cong; ≑-·; ·-𝟎ˡ; ·-∥; ∥-·-≑ - ; _[+]_; [+]-cong; [+]-𝟎ʳ; [+]-𝟎ˡ - ) -open import Data.Mat.SemiadditiveDagger Rig using (∥-ᵀ; Mat-SemiadditiveDagger) -open import Category.Dagger.Semiadditive Mat using (IdempotentSemiadditiveDagger) -open import Category.Dagger.2-Poset using (dagger-2-poset; Dagger-2-Poset) -open import Data.Nat using (ℕ) -open import Data.Vec using (Vec) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) - -open Vec - -private - variable - A B : ℕ - -opaque - unfolding _≊_ _⊕_ - ⊕-idem : (V : Vector A) → V ⊕ V ≊ V - ⊕-idem [] = PW.[] - ⊕-idem (v ∷ V) = +-idem v PW.∷ ⊕-idem V - -opaque - unfolding _≋_ _[+]_ - [+]-idem : (M : Matrix A B) → M [+] M ≋ M - [+]-idem [] = PW.[] - [+]-idem (M₀ ∷ M) = ⊕-idem M₀ PW.∷ [+]-idem M - -opaque - unfolding ≋-setoid - idem : (M : Matrix A B) → (I ∥ I) · (((I ≑ 𝟎) · M) ∥ ((𝟎 ≑ I) · M)) · (I ∥ I) ᵀ ≋ M - idem M = begin - (I ∥ I) · (((I ≑ 𝟎) · M) ∥ ((𝟎 ≑ I) · M)) · (I ∥ I) ᵀ ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · (h₁ ∥ h₂) · (I ∥ I) ᵀ) (≑-· I 𝟎 M) (≑-· 𝟎 I M) ⟩ - (I ∥ I) · ((I · M ≑ 𝟎 · M) ∥ (𝟎 · M ≑ I · M)) · (I ∥ I) ᵀ ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ (∥-cong (≑-cong ·-identityˡ (·-𝟎ˡ M)) (≑-cong (·-𝟎ˡ M) ·-identityˡ)) ≋.refl) ⟩ - (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ∥ I) ᵀ ≡⟨ ≡.cong (λ h → (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · h) (∥-ᵀ I I) ⟩ - (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ᵀ ≑ I ᵀ) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (h₁ ≑ h₂)) transpose-I transpose-I ⟩ - (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ≑ I) ≈⟨ ·-assoc ⟨ - ((I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M))) · (I ≑ I) ≡⟨ ≡.cong (_· (I ≑ I)) (·-∥ (I ∥ I) (M ≑ 𝟎) (𝟎 ≑ M)) ⟩ - (((I ∥ I) · (M ≑ 𝟎)) ∥ ((I ∥ I) · (𝟎 ≑ M))) · (I ≑ I) ≈⟨ ∥-·-≑ ((I ∥ I) · (M ≑ 𝟎)) ((I ∥ I) · (𝟎 ≑ M)) I I ⟩ - (((I ∥ I) · (M ≑ 𝟎)) · I) [+] (((I ∥ I) · (𝟎 ≑ M)) · I) ≈⟨ [+]-cong ·-identityʳ ·-identityʳ ⟩ - ((I ∥ I) · (M ≑ 𝟎)) [+] ((I ∥ I) · (𝟎 ≑ M)) ≈⟨ [+]-cong (∥-·-≑ I I M 𝟎) (∥-·-≑ I I 𝟎 M) ⟩ - ((I · M) [+] (I · 𝟎)) [+] ((I · 𝟎) [+] (I · M)) ≈⟨ [+]-cong ([+]-cong ·-identityˡ ·-identityˡ) ([+]-cong ·-identityˡ ·-identityˡ) ⟩ - (M [+] 𝟎) [+] (𝟎 [+] M) ≈⟨ [+]-cong ([+]-𝟎ʳ M) ([+]-𝟎ˡ M) ⟩ - M [+] M ≈⟨ [+]-idem M ⟩ - M ∎ - where - open ≈-Reasoning (≋-setoid _ _) - -Mat-IdempotentSemiadditiveDagger : IdempotentSemiadditiveDagger -Mat-IdempotentSemiadditiveDagger = record - { semiadditiveDagger = Mat-SemiadditiveDagger - ; idempotent = idem _ - } - -Mat-Dagger-2-Poset : Dagger-2-Poset -Mat-Dagger-2-Poset = dagger-2-poset Mat-IdempotentSemiadditiveDagger diff --git a/Data/Mat/SemiadditiveDagger.agda b/Data/Mat/SemiadditiveDagger.agda deleted file mode 100644 index 65aeee6..0000000 --- a/Data/Mat/SemiadditiveDagger.agda +++ /dev/null @@ -1,503 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Algebra.Bundles using (CommutativeSemiring) -open import Level using (Level) - -module Data.Mat.SemiadditiveDagger {c ℓ : Level} (Rig : CommutativeSemiring c ℓ) where - -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -import Data.Nat.Properties as ℕ-Props - -module Rig = CommutativeSemiring Rig - -open import Data.Mat.Util using (transpose-cong; replicate-++) -open import Data.Mat.Category Rig.semiring - using - ( Mat; _ᵀ; transpose-I; I; _≋_; module ≋; _≊_; module ≊; Matrix; Vector - ; [_]_; _[_]; _·_; ≋-setoid; ≊-setoid; mapRows; zeros; _∙_ - ; ∙-cong; _ᵀᵀ; -[-]ᵀ - ; [-]--cong - ; ·-identityˡ - ; ·-identityʳ - ) -open import Data.Mat.Cocartesian Rig.semiring - using - ( Mat-Cocartesian; []ᵥ; []ₕ; [-]-[]ᵥ; ⟨⟩; _∷ₕ_; ∷ₕ-cong; _∷ᵥ_ - ; [-]-∷ₕ; _∷′_; ∷ₕ-ᵀ; ∷ᵥ-ᵀ; 𝟎; _∥_; _≑_; []ᵥ-∥; []ₕ-≑; []ₕ-! - ; _+++_; ∷ₕ-≑; []ᵥ-ᵀ; ∥-cong; ≑-cong; ≑-·; ·-𝟎ʳ; ·-𝟎ˡ; 𝟎ᵀ; ·-∥ - ; headₕ; tailₕ; head-∷-tailₕ; [⟨⟩]-[]ₕ - ; ∷ₕ-∥; []ᵥ-!; _[+]_; ∥-·-≑; [+]-cong; [+]-𝟎ʳ; [+]-𝟎ˡ - ) - -open import Category.Dagger.Semiadditive Mat using (DaggerCocartesianMonoidal; SemiadditiveDagger) -open import Data.Nat as ℕ using (ℕ) -open import Data.Vec using (Vec; map; replicate) -open import Function using (_∘_) -open import Data.Vec.Properties using (map-cong; map-const) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) - -open ℕ.ℕ -open Vec -open Rig renaming (Carrier to R) - -private - variable - A B C D E F : ℕ - -opaque - unfolding _≋_ - Iᵀ : I ᵀ ≋ I {A} - Iᵀ = ≋.reflexive transpose-I - -import Data.Vec.Relation.Binary.Pointwise.Inductive as PW - -opaque - unfolding Vector _∙_ - ∙-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 _[_] [_]_ _ᵀ []ᵥ ⟨⟩ _∷ₕ_ _≊_ _≋_ _∷ᵥ_ - [-]-ᵀ : (M : Matrix A B) (V : Vector A) → M [ V ] ≊ [ V ] (M ᵀ) - [-]-ᵀ [] V = ≊.sym (≊.reflexive ([-]-[]ᵥ V)) - [-]-ᵀ (M₀ ∷ M) V = begin - M₀ ∙ V ∷ map (_∙ V) M ≈⟨ ∙-comm M₀ V PW.∷ (PW.map⁺ (λ {x} ≊V → trans (∙-comm x V) (∙-cong ≊.refl ≊V)) ≋.refl) ⟩ - V ∙ M₀ ∷ map (V ∙_) M ≡⟨⟩ - map (V ∙_) (M₀ ∷ᵥ M) ≡⟨ ≡.cong (map (V ∙_) ∘ (M₀ ∷ᵥ_)) (M ᵀᵀ) ⟨ - map (V ∙_) (M₀ ∷ᵥ M ᵀ ᵀ) ≡⟨ ≡.cong (map (V ∙_)) (∷ₕ-ᵀ M₀ (M ᵀ)) ⟨ - map (V ∙_) ((M₀ ∷ₕ (M ᵀ)) ᵀ) ∎ - where - open ≈-Reasoning (≊-setoid _) - -opaque - unfolding ≋-setoid []ᵥ mapRows ⟨⟩ _∷ₕ_ _∷ᵥ_ - ·-ᵀ - : {A B C : ℕ} - (M : Matrix A B) - (N : Matrix B C) - → (N · M) ᵀ ≋ M ᵀ · N ᵀ - ·-ᵀ {A} {B} {zero} M [] = begin - []ᵥ ≡⟨ map-const (M ᵀ) ⟨⟩ ⟨ - map (λ _ → ⟨⟩) (M ᵀ) ≡⟨ map-cong [-]-[]ᵥ (M ᵀ) ⟨ - map ([_] []ᵥ) (M ᵀ) ∎ - where - open ≈-Reasoning (≋-setoid 0 A) - ·-ᵀ {A} {B} {suc C} M (N₀ ∷ N) = begin - map ([_] M) (N₀ ∷ᵥ N) ᵀ ≡⟨ -[-]ᵀ (N₀ ∷ᵥ N) M ⟨ - map ((N₀ ∷ᵥ N) [_]) (M ᵀ) ≈⟨ PW.map⁺ (λ {V} ≋V → ≊.trans ([-]-ᵀ (N₀ ∷ᵥ N) V) ([-]--cong {A = (N₀ ∷ᵥ N) ᵀ} ≋V ≋.refl)) ≋.refl ⟩ - map ([_] ((N₀ ∷ᵥ N) ᵀ)) (M ᵀ) ≡⟨ map-cong (λ V → ≡.cong ([ V ]_) (∷ᵥ-ᵀ N₀ N)) (M ᵀ) ⟩ - map ([_] (N₀ ∷ₕ N ᵀ)) (M ᵀ) ∎ - where - open ≈-Reasoning (≋-setoid (suc C) A) - -opaque - unfolding _ᵀ _≋_ - ᵀ-cong : {M M′ : Matrix A B} → M ≋ M′ → M ᵀ ≋ M′ ᵀ - ᵀ-cong ≋M = transpose-cong setoid ≋M - -opaque - unfolding _≋_ - ᵀ-involutive : (M : Matrix A B) → (M ᵀ) ᵀ ≋ M - ᵀ-involutive M = ≋.reflexive (M ᵀᵀ) - -opaque - unfolding _≋_ - ≋λᵀ : ([]ᵥ ∥ I) ᵀ ≋ 𝟎 ≑ I {A} - ≋λᵀ = begin - ([]ᵥ ∥ I) ᵀ ≡⟨ ≡.cong (_ᵀ) ([]ᵥ-∥ I) ⟩ - I ᵀ ≈⟨ Iᵀ ⟩ - I ≡⟨ []ₕ-≑ I ⟨ - []ₕ ≑ I ≡⟨ ≡.cong (_≑ I) ([]ₕ-! 𝟎) ⟨ - 𝟎 ≑ I ∎ - where - open ≈-Reasoning (≋-setoid _ _) - -opaque - unfolding Matrix _∥_ _ᵀ _≑_ _+++_ _∷ₕ_ - ∥-ᵀ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) ᵀ ≡ M ᵀ ≑ N ᵀ - ∥-ᵀ {A} {zero} {B} [] [] = ≡.sym (replicate-++ A B []) - ∥-ᵀ (M₀ ∷ M) (N₀ ∷ N) = begin - (M₀ +++ N₀) ∷ₕ ((M ∥ N) ᵀ) ≡⟨ ≡.cong ((M₀ +++ N₀) ∷ₕ_) (∥-ᵀ M N) ⟩ - (M₀ +++ N₀) ∷ₕ (M ᵀ ≑ N ᵀ) ≡⟨ ∷ₕ-≑ M₀ N₀ (M ᵀ) (N ᵀ) ⟩ - (M₀ ∷ₕ M ᵀ) ≑ (N₀ ∷ₕ N ᵀ) ∎ - where - open ≡-Reasoning - -≑-ᵀ : (M : Matrix A B) (N : Matrix A C) → (M ≑ N) ᵀ ≡ M ᵀ ∥ N ᵀ -≑-ᵀ M N = begin - (M ≑ N) ᵀ ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ≑ h₂) ᵀ) (M ᵀᵀ) (N ᵀᵀ) ⟨ - (M ᵀ ᵀ ≑ N ᵀ ᵀ ) ᵀ ≡⟨ ≡.cong (_ᵀ) (∥-ᵀ (M ᵀ) (N ᵀ)) ⟨ - (M ᵀ ∥ N ᵀ ) ᵀ ᵀ ≡⟨ (M ᵀ ∥ N ᵀ ) ᵀᵀ ⟩ - M ᵀ ∥ N ᵀ ∎ - where - open ≡-Reasoning - -opaque - unfolding _≋_ - ≋ρᵀ : (I ∥ []ᵥ) ᵀ ≋ I {A} ≑ 𝟎 - ≋ρᵀ {A} = begin - (I ∥ []ᵥ) ᵀ ≡⟨ ∥-ᵀ I []ᵥ ⟩ - I ᵀ ≑ []ᵥ ᵀ ≡⟨ ≡.cong (I ᵀ ≑_) []ᵥ-ᵀ ⟩ - I ᵀ ≑ []ₕ ≡⟨ ≡.cong (_≑ []ₕ) transpose-I ⟩ - I ≑ []ₕ ≡⟨ ≡.cong (I ≑_) ([]ₕ-! 𝟎) ⟨ - I ≑ 𝟎 ∎ - where - open ≈-Reasoning (≋-setoid _ _) - -open import Data.Vec using () renaming (cast to castVec) -open import Data.Vec.Properties using (++-assoc-eqFree) renaming (cast-is-id to castVec-is-id) - -opaque - unfolding Matrix Vector - 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₂ (ℕ-Props.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 (ℕ-Props.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 (ℕ-Props.suc-injective eq₁) (ℕ-Props.suc-injective eq₂) M) - -opaque - unfolding _∥_ cast₁ - ∥-assoc - : (X : Matrix A D) - (Y : Matrix B D) - (Z : Matrix C D) - → cast₁ (ℕ-Props.+-assoc A B C) ((X ∥ Y) ∥ Z) ≡ X ∥ Y ∥ Z - ∥-assoc [] [] [] = cast₁-is-id ≡.refl [] - ∥-assoc (X₀ ∷ X) (Y₀ ∷ Y) (Z₀ ∷ Z) = ≡.cong₂ _∷_ (++-assoc-eqFree X₀ Y₀ Z₀) (∥-assoc X Y Z) - -opaque - unfolding _≑_ cast₂ - ≑-assoc - : (X : Matrix A B) - (Y : Matrix A C) - (Z : Matrix A D) - → cast₂ (ℕ-Props.+-assoc B C D) ((X ≑ Y) ≑ Z) ≡ X ≑ Y ≑ Z - ≑-assoc [] Y Z = cast₂-is-id ≡.refl (Y ≑ Z) - ≑-assoc (X₀ ∷ X) Y Z = ≡.cong (X₀ ∷_) (≑-assoc X Y Z) - -≑-sym-assoc - : (X : Matrix A B) - (Y : Matrix A C) - (Z : Matrix A D) - → cast₂ (≡.sym (ℕ-Props.+-assoc B C D)) (X ≑ Y ≑ Z) ≡ (X ≑ Y) ≑ Z -≑-sym-assoc {A} {B} {C} {D} X Y Z = begin - cast₂ _ (X ≑ Y ≑ Z) ≡⟨ ≡.cong (cast₂ _) (≑-assoc X Y Z) ⟨ - cast₂ _ (cast₂ assoc ((X ≑ Y) ≑ Z)) ≡⟨ cast₂-trans assoc (≡.sym assoc) ((X ≑ Y) ≑ Z) ⟩ - cast₂ _ ((X ≑ Y) ≑ Z) ≡⟨ cast₂-is-id _ ((X ≑ Y) ≑ Z) ⟩ - (X ≑ Y) ≑ Z ∎ - where - open ≡-Reasoning - assoc : B ℕ.+ C ℕ.+ D ≡ B ℕ.+ (C ℕ.+ D) - assoc = ℕ-Props.+-assoc B C D - -opaque - unfolding _∥_ _≑_ _+++_ - ∥-≑ : {A₁ B₁ A₂ B₂ : ℕ} - (W : Matrix A₁ B₁) - (X : Matrix A₂ B₁) - (Y : Matrix A₁ B₂) - (Z : Matrix A₂ B₂) - → W ∥ X ≑ Y ∥ Z ≡ (W ≑ Y) ∥ (X ≑ Z) - ∥-≑ {A₁} {ℕ.zero} {A₂} {B₂} [] [] Y Z = ≡.refl - ∥-≑ {A₁} {suc B₁} {A₂} {B₂} (W₀ ∷ W) (X₀ ∷ X) Y Z = ≡.cong ((W₀ +++ X₀) ∷_) (∥-≑ W X Y Z) - -∥-≑⁴ - : (R : Matrix A D) - (S : Matrix B D) - (T : Matrix C D) - (U : Matrix A E) - (V : Matrix B E) - (W : Matrix C E) - (X : Matrix A F) - (Y : Matrix B F) - (Z : Matrix C F) - → (R ∥ S ∥ T) ≑ - (U ∥ V ∥ W) ≑ - (X ∥ Y ∥ Z) - ≡ (R ≑ U ≑ X) ∥ - (S ≑ V ≑ Y) ∥ - (T ≑ W ≑ Z) -∥-≑⁴ R S T U V W X Y Z = begin - R ∥ S ∥ T ≑ U ∥ V ∥ W ≑ X ∥ Y ∥ Z ≡⟨ ≡.cong (R ∥ S ∥ T ≑_) (∥-≑ U (V ∥ W) X (Y ∥ Z)) ⟩ - R ∥ S ∥ T ≑ (U ≑ X) ∥ (V ∥ W ≑ Y ∥ Z) ≡⟨ ≡.cong (λ h → (R ∥ S ∥ T ≑ (U ≑ X) ∥ h)) (∥-≑ V W Y Z) ⟩ - R ∥ S ∥ T ≑ (U ≑ X) ∥ (V ≑ Y) ∥ (W ≑ Z) ≡⟨ ∥-≑ R (S ∥ T) (U ≑ X) ((V ≑ Y) ∥ (W ≑ Z)) ⟩ - (R ≑ (U ≑ X)) ∥ ((S ∥ T) ≑ ((V ≑ Y) ∥ (W ≑ Z))) ≡⟨ ≡.cong ((R ≑ U ≑ X) ∥_) (∥-≑ S T (V ≑ Y) (W ≑ Z)) ⟩ - (R ≑ U ≑ X) ∥ (S ≑ V ≑ Y) ∥ (T ≑ W ≑ Z) ∎ - where - open ≡-Reasoning - -opaque - unfolding Vector - cast : .(A ≡ B) → Vector A → Vector B - cast = castVec - -opaque - unfolding cast cast₂ _∷ₕ_ - cast₂-∷ₕ : .(eq : B ≡ C) (V : Vector B) (M : Matrix A B) → cast eq V ∷ₕ cast₂ eq M ≡ cast₂ eq (V ∷ₕ M) - cast₂-∷ₕ {zero} {zero} {A} _ [] [] = ≡.sym (cast₂-is-id ≡.refl ([] ∷ₕ [])) - cast₂-∷ₕ {suc B} {suc C} {A} eq (x ∷ V) (M₀ ∷ M) = ≡.cong ((x ∷ M₀) ∷_) (cast₂-∷ₕ _ V M) - -opaque - unfolding []ᵥ cast₂ - cast₂-[]ᵥ : .(eq : A ≡ B) → cast₂ eq []ᵥ ≡ []ᵥ - cast₂-[]ᵥ {zero} {zero} _ = ≡.refl - cast₂-[]ᵥ {suc A} {suc B} eq = ≡.cong ([] ∷_) (cast₂-[]ᵥ (ℕ-Props.suc-injective eq)) - -cast₂-∥ : .(eq : C ≡ D) (M : Matrix A C) (N : Matrix B C) → cast₂ eq M ∥ cast₂ eq N ≡ cast₂ eq (M ∥ N) -cast₂-∥ {C} {D} {zero} {B} eq M N - rewrite ([]ᵥ-! M) = begin - cast₂ _ []ᵥ ∥ cast₂ _ N ≡⟨ ≡.cong (_∥ cast₂ _ N) (cast₂-[]ᵥ _) ⟩ - []ᵥ ∥ cast₂ _ N ≡⟨ []ᵥ-∥ (cast₂ _ N) ⟩ - cast₂ _ N ≡⟨ ≡.cong (cast₂ _) ([]ᵥ-∥ N) ⟨ - cast₂ _ ([]ᵥ ∥ N) ∎ - where - open ≡-Reasoning -cast₂-∥ {C} {D} {suc A} {B} eq M N - rewrite ≡.sym (head-∷-tailₕ M) - using M₀ ← headₕ M - using M ← tailₕ M = begin - cast₂ _ (M₀ ∷ₕ M) ∥ (cast₂ _ N) ≡⟨ ≡.cong (_∥ (cast₂ eq N)) (cast₂-∷ₕ eq M₀ M) ⟨ - (cast _ M₀ ∷ₕ cast₂ _ M) ∥ (cast₂ _ N) ≡⟨ ∷ₕ-∥ (cast _ M₀) (cast₂ _ M) (cast₂ _ N) ⟨ - cast _ M₀ ∷ₕ (cast₂ _ M ∥ cast₂ _ N) ≡⟨ ≡.cong (cast eq M₀ ∷ₕ_) (cast₂-∥ _ M N) ⟩ - cast _ M₀ ∷ₕ cast₂ _ (M ∥ N) ≡⟨ cast₂-∷ₕ eq M₀ (M ∥ N) ⟩ - cast₂ _ (M₀ ∷ₕ (M ∥ N)) ≡⟨ ≡.cong (cast₂ eq) (∷ₕ-∥ M₀ M N) ⟩ - cast₂ _ ((M₀ ∷ₕ M) ∥ N) ∎ - where - open ≡-Reasoning - -opaque - unfolding 𝟎 _≑_ - 𝟎≑𝟎 : 𝟎 {A} {B} ≑ 𝟎 {A} {C} ≡ 𝟎 - 𝟎≑𝟎 {B = zero} = ≡.refl - 𝟎≑𝟎 {B = suc B} = ≡.cong (zeros ∷_) (𝟎≑𝟎 {B = B}) - -opaque - unfolding _∷ₕ_ 𝟎 zeros - zeros∷ₕ𝟎 : zeros ∷ₕ 𝟎 {A} {B} ≡ 𝟎 - zeros∷ₕ𝟎 {A} {zero} = ≡.refl - zeros∷ₕ𝟎 {A} {suc B} = ≡.cong (zeros ∷_) zeros∷ₕ𝟎 - -𝟎∥𝟎 : 𝟎 {A} {C} ∥ 𝟎 {B} {C} ≡ 𝟎 -𝟎∥𝟎 {zero} {C} rewrite []ᵥ-! (𝟎 {0} {C}) = []ᵥ-∥ 𝟎 -𝟎∥𝟎 {suc A} {C} {B} = begin - 𝟎 ∥ 𝟎 ≡⟨ ≡.cong (_∥ 𝟎) (zeros∷ₕ𝟎 {A} {C}) ⟨ - (zeros ∷ₕ 𝟎 {A}) ∥ 𝟎 ≡⟨ ∷ₕ-∥ zeros 𝟎 𝟎 ⟨ - zeros ∷ₕ 𝟎 {A} ∥ 𝟎 ≡⟨ ≡.cong (zeros ∷ₕ_) 𝟎∥𝟎 ⟩ - zeros ∷ₕ 𝟎 ≡⟨ zeros∷ₕ𝟎 ⟩ - 𝟎 ∎ - where - open ≡-Reasoning - -opaque - unfolding _≋_ - ≋αᵀ : (((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎)) ∥ (𝟎 {_} {A} ≑ I {B ℕ.+ C}) · (𝟎 ≑ I {C})) ᵀ - ≋ (I {A ℕ.+ B} ≑ 𝟎) · (I {A} ≑ 𝟎) ∥ (I {A ℕ.+ B} ≑ 𝟎) · (𝟎 ≑ I {B}) ∥ (𝟎 ≑ I {C}) - ≋αᵀ {A} {B} {C} = begin - (((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ - ≡⟨ ∥-ᵀ ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ⟩ - ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ - ≡⟨ ≡.cong (_≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (∥-ᵀ (I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C}))) ⟩ - ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ - ≡⟨ ≡.cong (λ h → (h ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (≑-ᵀ I 𝟎) ⟩ - (I {A} ᵀ ∥ 𝟎 {A} {B ℕ.+ C} ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ - ≡⟨ ≡.cong (λ h → (h ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (≡.cong₂ _∥_ Iᵀ′ 𝟎ᵀ) ⟩ - (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ - ≈⟨ ≑-cong (≑-cong ≋.refl (·-ᵀ (I ≑ 𝟎) (𝟎 ≑ I))) (·-ᵀ (𝟎 ≑ I) (𝟎 ≑ I)) ⟩ - (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ≑ 𝟎 {B} {C}) ᵀ · (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) ᵀ) ≑ (𝟎 {C} {B} ≑ I {C}) ᵀ · (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) ᵀ - ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ (λ h₁ h₂ → I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ h₁ · h₂) (≑-ᵀ I 𝟎) (≑-ᵀ 𝟎 I)) (≡.cong₂ _·_ (≑-ᵀ 𝟎 I) (≑-ᵀ 𝟎 I)) ⟩ - (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ᵀ ∥ 𝟎 {B} {C} ᵀ) · (𝟎 {B ℕ.+ C} {A} ᵀ ∥ I {B ℕ.+ C} ᵀ)) ≑ (𝟎 {C} {B} ᵀ ∥ I {C} ᵀ) · (𝟎 {B ℕ.+ C} {A} ᵀ ∥ I {B ℕ.+ C} ᵀ) - ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ (λ h₁ h₂ → I {A} ∥ 𝟎 ≑ h₁ · h₂) (≡.cong₂ _∥_ Iᵀ′ 𝟎ᵀ) (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ′)) (≡.cong₂ _·_ (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ′) (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ′)) ⟩ - (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ∥ 𝟎 {C} {B}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C}) - ≡⟨ ≡.cong (λ h → (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ h) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})) (·-∥ (I ∥ 𝟎) 𝟎 I) ⟩ - (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ∥ 𝟎 {C} {B}) · 𝟎 {A} {B ℕ.+ C} ∥ (I {B} ∥ 𝟎 {C} {B}) · I {B ℕ.+ C}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C}) - ≈⟨ ≑-cong (≑-cong ≋.refl (∥-cong (·-𝟎ʳ (I ∥ 𝟎)) ·-identityʳ)) ≋.refl ⟩ - (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C}) - ≡⟨ ≡.cong ((I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑_) (·-∥ (𝟎 ∥ I) 𝟎 I) ⟩ - (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B} {C} ∥ I {C}) · I {B ℕ.+ C} - ≈⟨ ≑-cong ≋.refl (∥-cong (·-𝟎ʳ (𝟎 ∥ I)) ·-identityʳ) ⟩ - (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ 𝟎 {A} {C} ∥ 𝟎 {B} {C} ∥ I {C} - ≡⟨ ≡.cong (λ h → (I {A} ∥ h ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ 𝟎 {A} {C} ∥ 𝟎 {B} {C} ∥ I {C}) 𝟎∥𝟎 ⟨ - (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ I {B} ∥ 𝟎 {C}) ≑ 𝟎 {A} ∥ 𝟎 {B} ∥ I {C} - ≡⟨ ≑-sym-assoc (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C}) (𝟎 {A} ∥ I {B} ∥ 𝟎 {C}) (𝟎 {A} ∥ 𝟎 {B} ∥ I {C}) ⟨ - cast₂ _ (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ I {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ 𝟎 {B} ∥ I {C}) - ≡⟨ ≡.cong (cast₂ _) (∥-≑⁴ I 𝟎 𝟎 𝟎 I 𝟎 𝟎 𝟎 I) ⟩ - cast₂ (≡.sym assoc) ((I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥ (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C}))) - ≡⟨ cast₂-∥ (≡.sym assoc) ((I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C}))) ((𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C}))) ⟨ - (cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C}))) ∥ cast₂ (≡.sym assoc) ((𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C}))) - ≡⟨ ≡.cong (cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥_) (cast₂-∥ (≡.sym assoc) (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) (𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})) ⟨ - cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥ cast₂ (≡.sym assoc) (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ cast₂ (≡.sym assoc) (𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C}) - ≡⟨ ≡.cong₂ _∥_ (≑-sym-assoc I 𝟎 𝟎) (≡.cong₂ _∥_ (≑-sym-assoc 𝟎 I 𝟎) (≑-sym-assoc 𝟎 𝟎 I)) ⟩ - ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B}) ≑ I {C}) - ≡⟨ ≡.cong (λ h → ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ (h ≑ I {C})) 𝟎≑𝟎 ⟩ - ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) - ≈⟨ ∥-cong ≋.refl (∥-cong (≑-cong ·-identityˡ (·-𝟎ˡ (𝟎 ≑ I))) ≋.refl) ⟨ - ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ (((I {A ℕ.+ B} · (𝟎 {B} {A} ≑ I {B})) ≑ (𝟎 {A ℕ.+ B} {C} · (𝟎 {B} {A} ≑ I {B})))) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) - ≡⟨ ≡.cong (λ h → ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ h ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})) (≑-· I 𝟎 (𝟎 ≑ I)) ⟨ - ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) - ≈⟨ ∥-cong (≑-cong ·-identityˡ (·-𝟎ˡ (I ≑ 𝟎))) ≋.refl ⟨ - ((I {A ℕ.+ B} · (I {A} ≑ 𝟎 {A} {B})) ≑ (𝟎 {A ℕ.+ B} {C} · (I {A} ≑ 𝟎 {A} {B}))) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) - ≡⟨ ≡.cong (λ h → h ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})) (≑-· I 𝟎 (I ≑ 𝟎)) ⟨ - (I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (I {A} ≑ 𝟎 {A} {B}) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) ∎ - where - assoc : A ℕ.+ B ℕ.+ C ≡ A ℕ.+ (B ℕ.+ C) - assoc = ℕ-Props.+-assoc A B C - Iᵀ′ : {A : ℕ} → I ᵀ ≡ I {A} - Iᵀ′ = transpose-I - open ≈-Reasoning (≋-setoid _ _) - -opaque - unfolding ≋-setoid - ≋σᵀ : ((𝟎 ≑ I {A}) ∥ (I {B} ≑ 𝟎)) ᵀ ≋ (𝟎 ≑ I {B}) ∥ (I {A} ≑ 𝟎) - ≋σᵀ {A} {B} = begin - ((𝟎 ≑ I) ∥ (I ≑ 𝟎)) ᵀ ≡⟨ ∥-ᵀ (𝟎 ≑ I) (I ≑ 𝟎) ⟩ - (𝟎 ≑ I {A}) ᵀ ≑ (I ≑ 𝟎) ᵀ ≡⟨ ≡.cong₂ _≑_ (≑-ᵀ 𝟎 I) (≑-ᵀ I 𝟎) ⟩ - 𝟎 ᵀ ∥ (I {A}) ᵀ ≑ I ᵀ ∥ 𝟎 ᵀ ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ _∥_ 𝟎ᵀ transpose-I) (≡.cong₂ _∥_ transpose-I 𝟎ᵀ) ⟩ - 𝟎 ∥ I {A} ≑ I ∥ 𝟎 ≡⟨ ∥-≑ 𝟎 I I 𝟎 ⟩ - (𝟎 ≑ I {B}) ∥ (I ≑ 𝟎) ∎ - where - open ≈-Reasoning (≋-setoid _ _) - -opaque - unfolding ≋-setoid - ≋⊗ : (M : Matrix A B) - (N : Matrix C D) - → (I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N - ≋ (M ≑ 𝟎) ∥ (𝟎 ≑ N) - ≋⊗ M N = begin - (I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N ≡⟨ ≡.cong₂ _∥_ (≑-· I 𝟎 M) (≑-· 𝟎 I N) ⟩ - (I · M ≑ 𝟎 · M) ∥ (𝟎 · N ≑ I · N) ≈⟨ ∥-cong (≑-cong ·-identityˡ (·-𝟎ˡ M)) (≑-cong (·-𝟎ˡ N) ·-identityˡ) ⟩ - (M ≑ 𝟎) ∥ (𝟎 ≑ N) ∎ - where - open ≈-Reasoning (≋-setoid _ _) - -opaque - unfolding ≋-setoid - ᵀ-resp-⊗ - : {M : Matrix A B} - {N : Matrix C D} - → ((I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N) ᵀ - ≋ (I ≑ 𝟎) · M ᵀ ∥ (𝟎 ≑ I) · N ᵀ - ᵀ-resp-⊗ {M = M} {N = N} = begin - ((I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N) ᵀ ≈⟨ ᵀ-cong (≋⊗ M N) ⟩ - ((M ≑ 𝟎) ∥ (𝟎 ≑ N)) ᵀ ≡⟨ ≡.cong (_ᵀ) (∥-≑ M 𝟎 𝟎 N) ⟨ - ((M ∥ 𝟎) ≑ (𝟎 ∥ N)) ᵀ ≡⟨ ≑-ᵀ (M ∥ 𝟎) (𝟎 ∥ N) ⟩ - (M ∥ 𝟎) ᵀ ∥ (𝟎 ∥ N) ᵀ ≡⟨ ≡.cong₂ _∥_ (∥-ᵀ M 𝟎) (∥-ᵀ 𝟎 N) ⟩ - (M ᵀ ≑ 𝟎 ᵀ) ∥ (𝟎 ᵀ ≑ N ᵀ) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (M ᵀ ≑ h₁) ∥ (h₂ ≑ N ᵀ)) 𝟎ᵀ 𝟎ᵀ ⟩ - (M ᵀ ≑ 𝟎) ∥ (𝟎 ≑ N ᵀ) ≈⟨ ≋⊗ (M ᵀ) (N ᵀ) ⟨ - (I ≑ 𝟎) · M ᵀ ∥ (𝟎 ≑ I) · N ᵀ ∎ - where - open ≈-Reasoning (≋-setoid _ _) - -Mat-DaggerCocartesian : DaggerCocartesianMonoidal -Mat-DaggerCocartesian = record - { cocartesian = Mat-Cocartesian - ; dagger = record - { _† = λ M → M ᵀ - ; †-identity = Iᵀ - ; †-homomorphism = λ {f = f} {g} → ·-ᵀ f g - ; †-resp-≈ = ᵀ-cong - ; †-involutive = ᵀ-involutive - } - ; λ≅† = ≋λᵀ - ; ρ≅† = ≋ρᵀ - ; α≅† = ≋αᵀ - ; σ≅† = ≋σᵀ - ; †-resp-⊗ = ᵀ-resp-⊗ - } - -opaque - unfolding ≋-setoid - p₁-i₁ : (I ≑ 𝟎) ᵀ · (I ≑ 𝟎 {A} {B}) ≋ I - p₁-i₁ = begin - (I ≑ 𝟎) ᵀ · (I ≑ 𝟎) ≡⟨ ≡.cong (_· (I ≑ 𝟎)) (≑-ᵀ I 𝟎) ⟩ - (I ᵀ ∥ 𝟎 ᵀ) · (I ≑ 𝟎) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (I ≑ 𝟎)) transpose-I 𝟎ᵀ ⟩ - (I ∥ 𝟎) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ I 𝟎 I 𝟎 ⟩ - (I · I) [+] (𝟎 · 𝟎) ≈⟨ [+]-cong ·-identityˡ (·-𝟎ˡ 𝟎) ⟩ - I [+] 𝟎 ≈⟨ [+]-𝟎ʳ I ⟩ - I ∎ - where - open ≈-Reasoning (≋-setoid _ _) - -opaque - unfolding ≋-setoid - p₂-i₂ : (𝟎 {A} {B} ≑ I) ᵀ · (𝟎 ≑ I) ≋ I - p₂-i₂ = begin - (𝟎 ≑ I) ᵀ · (𝟎 ≑ I) ≡⟨ ≡.cong (_· (𝟎 ≑ I)) (≑-ᵀ 𝟎 I) ⟩ - (𝟎 ᵀ ∥ I ᵀ) · (𝟎 ≑ I) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (𝟎 ≑ I)) 𝟎ᵀ transpose-I ⟩ - (𝟎 ∥ I) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ 𝟎 I 𝟎 I ⟩ - (𝟎 · 𝟎) [+] (I · I) ≈⟨ [+]-cong (·-𝟎ˡ 𝟎) ·-identityˡ ⟩ - 𝟎 [+] I ≈⟨ [+]-𝟎ˡ I ⟩ - I ∎ - where - open ≈-Reasoning (≋-setoid _ _) - -opaque - unfolding 𝟎 mapRows ⟨⟩ - []ᵥ·[]ₕ : []ᵥ · []ₕ ≡ 𝟎 {A} {B} - []ᵥ·[]ₕ {A} {B} = begin - map ([_] []ₕ) []ᵥ ≡⟨ map-cong (λ { [] → [⟨⟩]-[]ₕ }) []ᵥ ⟩ - map (λ _ → zeros) []ᵥ ≡⟨ map-const []ᵥ zeros ⟩ - replicate B zeros ∎ - where - open ≡-Reasoning - -opaque - unfolding ≋-setoid - p₂-i₁ : (𝟎 {A} ≑ I) ᵀ · (I ≑ 𝟎 {B}) ≋ []ᵥ · []ᵥ ᵀ - p₂-i₁ = begin - (𝟎 ≑ I) ᵀ · (I ≑ 𝟎) ≡⟨ ≡.cong (_· (I ≑ 𝟎)) (≑-ᵀ 𝟎 I) ⟩ - (𝟎 ᵀ ∥ I ᵀ) · (I ≑ 𝟎) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (I ≑ 𝟎)) 𝟎ᵀ transpose-I ⟩ - (𝟎 ∥ I) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ 𝟎 I I 𝟎 ⟩ - (𝟎 · I) [+] (I · 𝟎) ≈⟨ [+]-cong (·-𝟎ˡ I) (·-𝟎ʳ I) ⟩ - 𝟎 [+] 𝟎 ≈⟨ [+]-𝟎ˡ 𝟎 ⟩ - 𝟎 ≡⟨ []ᵥ·[]ₕ ⟨ - []ᵥ · []ₕ ≡⟨ ≡.cong ([]ᵥ ·_) []ᵥ-ᵀ ⟨ - []ᵥ · []ᵥ ᵀ ∎ - where - open ≈-Reasoning (≋-setoid _ _) - -opaque - unfolding ≋-setoid - p₁-i₂ : (I ≑ 𝟎 {A}) ᵀ · (𝟎 {B} ≑ I) ≋ []ᵥ · []ᵥ ᵀ - p₁-i₂ = begin - (I ≑ 𝟎) ᵀ · (𝟎 ≑ I) ≡⟨ ≡.cong (_· (𝟎 ≑ I)) (≑-ᵀ I 𝟎) ⟩ - (I ᵀ ∥ 𝟎 ᵀ) · (𝟎 ≑ I) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (𝟎 ≑ I)) transpose-I 𝟎ᵀ ⟩ - (I ∥ 𝟎) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ I 𝟎 𝟎 I ⟩ - (I · 𝟎) [+] (𝟎 · I) ≈⟨ [+]-cong (·-𝟎ʳ I) (·-𝟎ˡ I) ⟩ - 𝟎 [+] 𝟎 ≈⟨ [+]-𝟎ˡ 𝟎 ⟩ - 𝟎 ≡⟨ []ᵥ·[]ₕ ⟨ - []ᵥ · []ₕ ≡⟨ ≡.cong ([]ᵥ ·_) []ᵥ-ᵀ ⟨ - []ᵥ · []ᵥ ᵀ ∎ - where - open ≈-Reasoning (≋-setoid _ _) - -Mat-SemiadditiveDagger : SemiadditiveDagger -Mat-SemiadditiveDagger = record - { daggerCocartesianMonoidal = Mat-DaggerCocartesian - ; p₁-i₁ = p₁-i₁ - ; p₂-i₂ = p₂-i₂ - ; p₂-i₁ = p₂-i₁ - ; p₁-i₂ = p₁-i₂ - } diff --git a/Data/Mat/Util.agda b/Data/Mat/Util.agda deleted file mode 100644 index 4570b44..0000000 --- a/Data/Mat/Util.agda +++ /dev/null @@ -1,134 +0,0 @@ -{-# OPTIONS --without-K --safe #-} -{-# OPTIONS --hidden-argument-puns #-} - -module Data.Mat.Util where - -import Data.Vec.Relation.Binary.Equality.Setoid as ≋ -import Data.Vec.Relation.Binary.Pointwise.Inductive as PW -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning - -open import Data.Nat using (ℕ; _+_) -open import Data.Setoid using (∣_∣) -open import Data.Vec using (Vec; zipWith; foldr; map; replicate; _++_) -open import Level using (Level) -open import Relation.Binary using (Rel; Setoid; Monotonic₂) -open import Relation.Binary.PropositionalEquality as ≡ using (_≗_; _≡_; module ≡-Reasoning) - -open ℕ -open Vec - -private - variable - n m o p : ℕ - ℓ : Level - A B C D E : Set ℓ - -transpose : Vec (Vec A n) m → Vec (Vec A m) n -transpose [] = replicate _ [] -transpose (row ∷ mat) = zipWith _∷_ row (transpose mat) - -transpose-empty : (m : ℕ) (E : Vec (Vec A 0) m) → transpose E ≡ [] -transpose-empty zero [] = ≡.refl -transpose-empty (suc m) ([] ∷ E) = ≡.cong (zipWith _∷_ []) (transpose-empty m E) - -transpose-zipWith : (V : Vec A m) (M : Vec (Vec A n) m) → transpose (zipWith _∷_ V M) ≡ V ∷ transpose M -transpose-zipWith [] [] = ≡.refl -transpose-zipWith (x ∷ V) (M₀ ∷ M) = ≡.cong (zipWith _∷_ (x ∷ M₀)) (transpose-zipWith V M) - -transpose-involutive : (M : Vec (Vec A n) m) → transpose (transpose M) ≡ M -transpose-involutive {n} [] = transpose-empty n (replicate n []) -transpose-involutive (V ∷ M) = begin - transpose (zipWith _∷_ V (transpose M)) ≡⟨ transpose-zipWith V (transpose M) ⟩ - V ∷ transpose (transpose M) ≡⟨ ≡.cong (V ∷_) (transpose-involutive M) ⟩ - V ∷ M ∎ - where - open ≡.≡-Reasoning - -map-replicate : (x : A) (v : Vec B n) → map (λ _ → x) v ≡ replicate n x -map-replicate x [] = ≡.refl -map-replicate x (y ∷ v) = ≡.cong (x ∷_) (map-replicate x v) - -replicate-++ : (n m : ℕ) (x : A) → replicate n x ++ replicate m x ≡ replicate (n + m) x -replicate-++ zero _ x = ≡.refl -replicate-++ (suc n) m x = ≡.cong (x ∷_) (replicate-++ n m x) - -zipWith-map-map - : (f : A → C) - (g : B → D) - (_⊕_ : C → D → E) - (v : Vec A n) - (w : Vec B n) - → 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-map - : (f : A → B) - (g : A → C) - (_⊕_ : B → C → D) - (v : Vec A n) - → zipWith _⊕_ (map f v) (map g v) ≡ map (λ x → f x ⊕ g x) v -zipWith-map f g _⊕_ [] = ≡.refl -zipWith-map f g _⊕_ (x ∷ v) = ≡.cong (f x ⊕ g x ∷_) (zipWith-map f g _⊕_ v) - -map-zipWith - : (f : C → D) - (_⊕_ : A → B → C) - (v : Vec A n) - (w : Vec B n) - → map f (zipWith _⊕_ v w) ≡ zipWith (λ x y → f (x ⊕ y)) v w -map-zipWith f _⊕_ [] [] = ≡.refl -map-zipWith f _⊕_ (x ∷ v) (y ∷ w) = ≡.cong (f (x ⊕ y) ∷_) (map-zipWith f _⊕_ v w) - -module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : Setoid c₁ ℓ₁} (B : ℕ → Setoid c₂ ℓ₂) where - - private - module A = Setoid A - module B {n : ℕ} = Setoid (B n) - module V = ≋ A - - foldr-cong - : {f g : {k : ℕ} → ∣ A ∣ → ∣ B k ∣ → ∣ B (suc k) ∣} - → ({k : ℕ} {w x : ∣ A ∣} {y z : ∣ B k ∣} → w A.≈ x → y B.≈ z → f w y B.≈ g x z) - → {d e : ∣ B zero ∣} - → d B.≈ e - → {n : ℕ} - {xs ys : Vec ∣ A ∣ n} - → (xs V.≋ ys) - → foldr (λ k → ∣ B k ∣) f d xs B.≈ foldr (λ k → ∣ B k ∣) g e ys - foldr-cong _ d≈e PW.[] = d≈e - foldr-cong cong d≈e (≈v₀ PW.∷ ≋v) = cong ≈v₀ (foldr-cong cong d≈e ≋v) - -module _ - {a b c ℓ₁ ℓ₂ ℓ₃ : Level} - {A : Set a} {B : Set b} {C : Set c} - {f : A → B → C} - {_∼₁_ : Rel A ℓ₁} - {_∼₂_ : Rel B ℓ₂} - {_∼₃_ : Rel C ℓ₃} - where - zipWith-cong - : {n : ℕ} - {ws xs : Vec A n} - {ys zs : Vec B n} - → Monotonic₂ _∼₁_ _∼₂_ _∼₃_ f - → PW.Pointwise _∼₁_ ws xs - → PW.Pointwise _∼₂_ ys zs - → PW.Pointwise _∼₃_ (zipWith f ws ys) (zipWith f xs zs) - zipWith-cong cong PW.[] PW.[] = PW.[] - zipWith-cong cong (x∼y PW.∷ xs) (a∼b PW.∷ ys) = cong x∼y a∼b PW.∷ zipWith-cong cong xs ys - -module _ {c ℓ : Level} (A : Setoid c ℓ) where - - private - module A = Setoid A - module V = ≋ A - module M {n} = ≋ (V.≋-setoid n) - - transpose-cong - : {n m : ℕ} - → {M₁ M₂ : Vec (Vec ∣ A ∣ n) m} - → M₁ M.≋ M₂ - → transpose M₁ M.≋ transpose M₂ - transpose-cong PW.[] = M.≋-refl - transpose-cong (R₁≋R₂ PW.∷ M₁≋M₂) = zipWith-cong PW._∷_ R₁≋R₂ (transpose-cong M₁≋M₂) diff --git a/Data/Matrix/Cast.agda b/Data/Matrix/Cast.agda new file mode 100644 index 0000000..a171c7a --- /dev/null +++ b/Data/Matrix/Cast.agda @@ -0,0 +1,162 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_) +open import Relation.Binary using (Setoid) + +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.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.Properties using (++-assoc-eqFree) renaming (cast-is-id to castVec-is-id) +open import Data.Vector.Core S using (Vector; _++_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) + +open Vec +open ℕ + +private + variable + A B C D E F : ℕ + +opaque + unfolding Matrix Vector + 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) + +opaque + unfolding _∥_ cast₁ + ∥-assoc + : (X : Matrix A D) + (Y : Matrix B D) + (Z : Matrix C D) + → cast₁ (+-assoc A B C) ((X ∥ Y) ∥ Z) ≡ X ∥ Y ∥ Z + ∥-assoc [] [] [] = cast₁-is-id ≡.refl [] + ∥-assoc (X₀ ∷ X) (Y₀ ∷ Y) (Z₀ ∷ Z) = ≡.cong₂ _∷_ (++-assoc-eqFree X₀ Y₀ Z₀) (∥-assoc X Y Z) + +opaque + unfolding _≑_ cast₂ + ≑-assoc + : (X : Matrix A B) + (Y : Matrix A C) + (Z : Matrix A D) + → cast₂ (+-assoc B C D) ((X ≑ Y) ≑ Z) ≡ X ≑ Y ≑ Z + ≑-assoc [] Y Z = cast₂-is-id ≡.refl (Y ≑ Z) + ≑-assoc (X₀ ∷ X) Y Z = ≡.cong (X₀ ∷_) (≑-assoc X Y Z) + +≑-sym-assoc + : (X : Matrix A B) + (Y : Matrix A C) + (Z : Matrix A D) + → cast₂ (≡.sym (+-assoc B C D)) (X ≑ Y ≑ Z) ≡ (X ≑ Y) ≑ Z +≑-sym-assoc {A} {B} {C} {D} X Y Z = begin + cast₂ _ (X ≑ Y ≑ Z) ≡⟨ ≡.cong (cast₂ _) (≑-assoc X Y Z) ⟨ + cast₂ _ (cast₂ assoc ((X ≑ Y) ≑ Z)) ≡⟨ cast₂-trans assoc (≡.sym assoc) ((X ≑ Y) ≑ Z) ⟩ + cast₂ _ ((X ≑ Y) ≑ Z) ≡⟨ cast₂-is-id _ ((X ≑ Y) ≑ Z) ⟩ + (X ≑ Y) ≑ Z ∎ + where + open ≡-Reasoning + assoc : B + C + D ≡ B + (C + D) + assoc = +-assoc B C D + +opaque + unfolding _∥_ _≑_ + ∥-≑ : {A₁ B₁ A₂ B₂ : ℕ} + (W : Matrix A₁ B₁) + (X : Matrix A₂ B₁) + (Y : Matrix A₁ B₂) + (Z : Matrix A₂ B₂) + → W ∥ X ≑ Y ∥ Z ≡ (W ≑ Y) ∥ (X ≑ Z) + ∥-≑ {A₁} {ℕ.zero} {A₂} {B₂} [] [] Y Z = ≡.refl + ∥-≑ {A₁} {suc B₁} {A₂} {B₂} (W₀ ∷ W) (X₀ ∷ X) Y Z = ≡.cong ((W₀ ++ X₀) ∷_) (∥-≑ W X Y Z) + +∥-≑⁴ + : (R : Matrix A D) + (S : Matrix B D) + (T : Matrix C D) + (U : Matrix A E) + (V : Matrix B E) + (W : Matrix C E) + (X : Matrix A F) + (Y : Matrix B F) + (Z : Matrix C F) + → (R ∥ S ∥ T) ≑ + (U ∥ V ∥ W) ≑ + (X ∥ Y ∥ Z) + ≡ (R ≑ U ≑ X) ∥ + (S ≑ V ≑ Y) ∥ + (T ≑ W ≑ Z) +∥-≑⁴ R S T U V W X Y Z = begin + R ∥ S ∥ T ≑ U ∥ V ∥ W ≑ X ∥ Y ∥ Z ≡⟨ ≡.cong (R ∥ S ∥ T ≑_) (∥-≑ U (V ∥ W) X (Y ∥ Z)) ⟩ + R ∥ S ∥ T ≑ (U ≑ X) ∥ (V ∥ W ≑ Y ∥ Z) ≡⟨ ≡.cong (λ h → (R ∥ S ∥ T ≑ (U ≑ X) ∥ h)) (∥-≑ V W Y Z) ⟩ + R ∥ S ∥ T ≑ (U ≑ X) ∥ (V ≑ Y) ∥ (W ≑ Z) ≡⟨ ∥-≑ R (S ∥ T) (U ≑ X) ((V ≑ Y) ∥ (W ≑ Z)) ⟩ + (R ≑ (U ≑ X)) ∥ ((S ∥ T) ≑ ((V ≑ Y) ∥ (W ≑ Z))) ≡⟨ ≡.cong ((R ≑ U ≑ X) ∥_) (∥-≑ S T (V ≑ Y) (W ≑ Z)) ⟩ + (R ≑ U ≑ X) ∥ (S ≑ V ≑ Y) ∥ (T ≑ W ≑ Z) ∎ + where + open ≡-Reasoning + +opaque + unfolding Vector + cast : .(A ≡ B) → Vector A → Vector B + cast = castVec + +opaque + unfolding cast cast₂ _∷ₕ_ + cast₂-∷ₕ : .(eq : B ≡ C) (V : Vector B) (M : Matrix A B) → cast eq V ∷ₕ cast₂ eq M ≡ cast₂ eq (V ∷ₕ M) + cast₂-∷ₕ {zero} {zero} {A} _ [] [] = ≡.sym (cast₂-is-id ≡.refl ([] ∷ₕ [])) + cast₂-∷ₕ {suc B} {suc C} {A} eq (x ∷ V) (M₀ ∷ M) = ≡.cong ((x ∷ M₀) ∷_) (cast₂-∷ₕ _ V M) + +opaque + unfolding []ᵥ cast₂ + cast₂-[]ᵥ : .(eq : A ≡ B) → cast₂ eq []ᵥ ≡ []ᵥ + cast₂-[]ᵥ {zero} {zero} _ = ≡.refl + cast₂-[]ᵥ {suc A} {suc B} eq = ≡.cong ([] ∷_) (cast₂-[]ᵥ (suc-injective eq)) + +cast₂-∥ : .(eq : C ≡ D) (M : Matrix A C) (N : Matrix B C) → cast₂ eq M ∥ cast₂ eq N ≡ cast₂ eq (M ∥ N) +cast₂-∥ {C} {D} {zero} {B} eq M N + rewrite ([]ᵥ-! M) = begin + cast₂ _ []ᵥ ∥ cast₂ _ N ≡⟨ ≡.cong (_∥ cast₂ _ N) (cast₂-[]ᵥ _) ⟩ + []ᵥ ∥ cast₂ _ N ≡⟨ []ᵥ-∥ (cast₂ _ N) ⟩ + cast₂ _ N ≡⟨ ≡.cong (cast₂ _) ([]ᵥ-∥ N) ⟨ + cast₂ _ ([]ᵥ ∥ N) ∎ + where + open ≡-Reasoning +cast₂-∥ {C} {D} {suc A} {B} eq M N + rewrite ≡.sym (head-∷-tailₕ M) + using M₀ ← headₕ M + using M ← tailₕ M = begin + cast₂ _ (M₀ ∷ₕ M) ∥ (cast₂ _ N) ≡⟨ ≡.cong (_∥ (cast₂ eq N)) (cast₂-∷ₕ eq M₀ M) ⟨ + (cast _ M₀ ∷ₕ cast₂ _ M) ∥ (cast₂ _ N) ≡⟨ ∷ₕ-∥ (cast _ M₀) (cast₂ _ M) (cast₂ _ N) ⟨ + cast _ M₀ ∷ₕ (cast₂ _ M ∥ cast₂ _ N) ≡⟨ ≡.cong (cast eq M₀ ∷ₕ_) (cast₂-∥ _ M N) ⟩ + cast _ M₀ ∷ₕ cast₂ _ (M ∥ N) ≡⟨ cast₂-∷ₕ eq M₀ (M ∥ N) ⟩ + cast₂ _ (M₀ ∷ₕ (M ∥ N)) ≡⟨ ≡.cong (cast₂ eq) (∷ₕ-∥ M₀ M N) ⟩ + cast₂ _ ((M₀ ∷ₕ M) ∥ N) ∎ + where + open ≡-Reasoning diff --git a/Data/Matrix/Category.agda b/Data/Matrix/Category.agda new file mode 100644 index 0000000..5a33440 --- /dev/null +++ b/Data/Matrix/Category.agda @@ -0,0 +1,177 @@ +{-# OPTIONS --without-K --safe #-} + +open import Algebra using (Semiring) +open import Level using (Level; 0ℓ; _⊔_) + +module Data.Matrix.Category {c ℓ : Level} (R : Semiring c ℓ) where + +module R = Semiring R + +import Data.Vec.Relation.Binary.Pointwise.Inductive as PW +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.Monoid R.+-monoid using (𝟎; _[+]_) +open import Data.Matrix.Transform R using ([_]_; _[_]; -[-]-cong; [-]--cong; -[-]ᵀ; []-∙; [-]--∥; [++]-≑; I; Iᵀ; I[-]; map--[-]-I; [-]-𝟎; [⟨0⟩]-) +open import Data.Nat using (ℕ) +open import Data.Vec using (Vec; map) +open import Data.Vec.Properties using (map-id; map-∘) +open import Data.Vector.Bisemimodule R using (_∙_; ∙-cong) +open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; module ≊; _≊_) +open import Data.Vector.Monoid R.+-monoid using () renaming (⟨ε⟩ to ⟨0⟩) +open import Function using (id) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) + +open R +open Vec +open ℕ + +private + variable + n m p : ℕ + A B C D : ℕ + +-- matrix multiplication +_·_ : Matrix m p → Matrix n m → Matrix n p +_·_ A B = mapRows ([_] B) A + +-- alternative form +_·′_ : Matrix m p → Matrix n m → Matrix n p +_·′_ A B = mapRows (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 ᵀ) ᵀ ∎ + where + open ≡-Reasoning + +opaque + + unfolding _[_] + + ·-[] : {A B C : ℕ} (M : Matrix A B) (N : Matrix B C) (V : Vector A) → (N · M) [ V ] ≊ N [ M [ V ] ] + ·-[] {A} {B} {zero} M [] V = PW.[] + ·-[] {A} {B} {suc C} M (N₀ ∷ N) V = []-∙ N₀ M V PW.∷ ·-[] M N V + +opaque + + unfolding [_]_ + + []-· : {A B C : ℕ} (V : Vector C) (M : Matrix A B) (N : Matrix B C) → [ V ] (N · M) ≊ [ [ V ] N ] M + []-· {A} {B} {C} V M N = begin + [ V ] (map ([_] M) N) ≡⟨ ≡.cong (map (V ∙_)) (-[-]ᵀ N M) ⟨ + map (V ∙_) (map (N [_]) (M ᵀ)) ≡⟨ map-∘ (V ∙_) (N [_]) (M ᵀ) ⟨ + map (λ h → V ∙ N [ h ]) (M ᵀ) ≈⟨ PW.map⁺ (λ {W} ≋W → trans ([]-∙ V N W) (∙-cong ≊.refl (-[-]-cong N ≋W))) {xs = M ᵀ} ≋.refl ⟨ + map ([ V ] N ∙_) (M ᵀ) ∎ + where + open ≈-Reasoning (Vectorₛ A) + +opaque + + unfolding _∥_ + + ·-∥ + : (M : Matrix C D) + (N : Matrix A C) + (P : Matrix B C) + → M · (N ∥ P) ≡ M · N ∥ M · P + ·-∥ {C} {D} {A} {B} [] N P = ≡.refl + ·-∥ {C} {D} {A} {B} (M₀ ∷ M) N P = ≡.cong₂ _∷_ ([-]--∥ M₀ N P) (·-∥ M N P) + +opaque + + unfolding _≑_ + + ≑-· : (M : Matrix B C) + (N : Matrix B D) + (P : Matrix A B) + → (M ≑ N) · P ≡ (M · P) ≑ (N · P) + ≑-· [] N P = ≡.refl + ≑-· (M₀ ∷ M) N P = ≡.cong ([ M₀ ] P ∷_) (≑-· M N P) + +opaque + + unfolding _[+]_ + + ∥-·-≑ + : (W : Matrix A C) + (X : Matrix B C) + (Y : Matrix D A) + (Z : Matrix D B) + → (W ∥ X) · (Y ≑ Z) ≋ (W · Y) [+] (X · Z) + ∥-·-≑ [] [] Y Z = PW.[] + ∥-·-≑ {A} {C} {B} {D} (W₀ ∷ W) (X₀ ∷ X) Y Z = [++]-≑ W₀ X₀ Y Z PW.∷ ∥-·-≑ W X Y Z + where + open ≈-Reasoning (Matrixₛ A B) + +opaque + + unfolding Matrix + + ·-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 + + ·-assoc : {A B C D : ℕ} {f : Matrix A B} {g : Matrix B C} {h : Matrix C D} → (h · g) · f ≋ h · g · f + ·-assoc {A} {B} {C} {D} {f} {g} {h} = begin + map ([_] f) (map ([_] g) h) ≡⟨ map-∘ ([_] f) ([_] g) h ⟨ + map (λ v → [ [ v ] g ] f) h ≈⟨ PW.map⁺ (λ {x} x≊y → ≊.trans ([]-· x f g) ([-]--cong ([-]--cong x≊y ≋.refl) ≋.refl)) {xs = h} ≋.refl ⟨ + map (λ v → [ v ] (g · f)) h ∎ + where + open ≈-Reasoning (Matrixₛ A D) + + ·-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 id (f ᵀ) ᵀ ≡⟨ ≡.cong (_ᵀ) (map-id (f ᵀ)) ⟩ + f ᵀ ᵀ ≡⟨ f ᵀᵀ ⟩ + f ∎ + where + open ≈-Reasoning (Matrixₛ A B) + + ·-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) ⟩ + f ᵀ ᵀ ≡⟨ f ᵀᵀ ⟩ + f ∎ + where + open ≈-Reasoning (Matrixₛ A B) + +opaque + + unfolding 𝟎 + + ·-𝟎ʳ : (M : Matrix A B) → M · 𝟎 {C} ≋ 𝟎 + ·-𝟎ʳ [] = ≋.refl + ·-𝟎ʳ (M₀ ∷ M) = begin + [ M₀ ] 𝟎 ∷ M · 𝟎 ≈⟨ [-]-𝟎 M₀ PW.∷ ·-𝟎ʳ M ⟩ + ⟨0⟩ ∷ 𝟎 ∎ + where + open ≈-Reasoning (Matrixₛ _ _) + + ·-𝟎ˡ : (M : Matrix A B) → 𝟎 {B} {C} · M ≋ 𝟎 + ·-𝟎ˡ {A} {B} {zero} M = PW.[] + ·-𝟎ˡ {A} {B} {suc C} M = [⟨0⟩]- M PW.∷ ·-𝟎ˡ M + +-- The category of matrices over a rig +Mat : Category 0ℓ c (c ⊔ ℓ) +Mat = categoryHelper record + { Obj = ℕ + ; _⇒_ = Matrix + ; _≈_ = _≋_ + ; id = I + ; _∘_ = _·_ + ; assoc = λ {A B C D f g h} → ·-assoc {f = f} {g} {h} + ; identityˡ = ·-Iˡ + ; identityʳ = ·-Iʳ + ; equiv = ≋-isEquiv + ; ∘-resp-≈ = ·-resp-≋ + } diff --git a/Data/Matrix/Core.agda b/Data/Matrix/Core.agda new file mode 100644 index 0000000..d97cb20 --- /dev/null +++ b/Data/Matrix/Core.agda @@ -0,0 +1,266 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_) +open import Relation.Binary using (Setoid; Rel; IsEquivalence) + +module Data.Matrix.Core {c ℓ : Level} (S : Setoid c ℓ) where + +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.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.Properties using (map-cong; map-id) +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 + n m p : ℕ + A B C : ℕ + +private + + module PW-≊ {n} = PW-≈ (Vectorₛ n) + +opaque + + -- Matrices over a setoid + Matrix : Rel ℕ c + Matrix n m = Vec (Vector n) m + + -- Pointwise equality of matrices + _≋_ : Rel (Matrix n m) (c ⊔ ℓ) + _≋_ {n} {m} A B = A PW-≊.≋ B + + -- 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 ⊔ ℓ) +Matrixₛ n m = record + { Carrier = Matrix n m + ; _≈_ = _≋_ {n} {m} + ; isEquivalence = ≋-isEquiv + } + +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 _ᵀᵀ diff --git a/Data/Matrix/Dagger-2-Poset.agda b/Data/Matrix/Dagger-2-Poset.agda new file mode 100644 index 0000000..cddf183 --- /dev/null +++ b/Data/Matrix/Dagger-2-Poset.agda @@ -0,0 +1,72 @@ +{-# OPTIONS --without-K --safe #-} + +open import Algebra using (Idempotent; CommutativeSemiring) +open import Level using (Level) + +module Data.Matrix.Dagger-2-Poset + {c ℓ : Level} + (R : CommutativeSemiring c ℓ) + (let module R = CommutativeSemiring R) + (+-idem : Idempotent R._≈_ R._+_) + where + +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.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.Monoid R.+-monoid using (𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ) +open import Data.Matrix.Transform R.semiring using (I; Iᵀ) +open import Data.Matrix.SemiadditiveDagger R using (∥-ᵀ; Mat-SemiadditiveDagger) +open import Data.Nat using (ℕ) +open import Data.Vec using (Vec) +open import Data.Vector.Core R.setoid using (Vector; _≊_) +open import Data.Vector.Monoid R.+-monoid using (_⊕_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open Vec + +private + variable + A B : ℕ + +opaque + unfolding _≊_ _⊕_ + ⊕-idem : (V : Vector A) → V ⊕ V ≊ V + ⊕-idem [] = PW.[] + ⊕-idem (v ∷ V) = +-idem v PW.∷ ⊕-idem V + +opaque + unfolding _≋_ _[+]_ + [+]-idem : (M : Matrix A B) → M [+] M ≋ M + [+]-idem [] = PW.[] + [+]-idem (M₀ ∷ M) = ⊕-idem M₀ PW.∷ [+]-idem M + +idem : (M : Matrix A B) → (I ∥ I) · (((I ≑ 𝟎) · M) ∥ ((𝟎 ≑ I) · M)) · (I ∥ I) ᵀ ≋ M +idem M = begin + (I ∥ I) · (((I ≑ 𝟎) · M) ∥ ((𝟎 ≑ I) · M)) · (I ∥ I) ᵀ ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · (h₁ ∥ h₂) · (I ∥ I) ᵀ) (≑-· I 𝟎 M) (≑-· 𝟎 I M) ⟩ + (I ∥ I) · ((I · M ≑ 𝟎 · M) ∥ (𝟎 · M ≑ I · M)) · (I ∥ I) ᵀ ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ (∥-cong (≑-cong ·-Iˡ (·-𝟎ˡ M)) (≑-cong (·-𝟎ˡ M) ·-Iˡ)) ≋.refl) ⟩ + (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ∥ I) ᵀ ≡⟨ ≡.cong (λ h → (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · h) (∥-ᵀ I I) ⟩ + (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ᵀ ≑ I ᵀ) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (h₁ ≑ h₂)) Iᵀ Iᵀ ⟩ + (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ≑ I) ≈⟨ ·-assoc ⟨ + ((I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M))) · (I ≑ I) ≡⟨ ≡.cong (_· (I ≑ I)) (·-∥ (I ∥ I) (M ≑ 𝟎) (𝟎 ≑ M)) ⟩ + (((I ∥ I) · (M ≑ 𝟎)) ∥ ((I ∥ I) · (𝟎 ≑ M))) · (I ≑ I) ≈⟨ ∥-·-≑ ((I ∥ I) · (M ≑ 𝟎)) ((I ∥ I) · (𝟎 ≑ M)) I I ⟩ + (((I ∥ I) · (M ≑ 𝟎)) · I) [+] (((I ∥ I) · (𝟎 ≑ M)) · I) ≈⟨ [+]-cong ·-Iʳ ·-Iʳ ⟩ + ((I ∥ I) · (M ≑ 𝟎)) [+] ((I ∥ I) · (𝟎 ≑ M)) ≈⟨ [+]-cong (∥-·-≑ I I M 𝟎) (∥-·-≑ I I 𝟎 M) ⟩ + ((I · M) [+] (I · 𝟎)) [+] ((I · 𝟎) [+] (I · M)) ≈⟨ [+]-cong ([+]-cong ·-Iˡ ·-Iˡ) ([+]-cong ·-Iˡ ·-Iˡ) ⟩ + (M [+] 𝟎) [+] (𝟎 [+] M) ≈⟨ [+]-cong ([+]-𝟎ʳ M) ([+]-𝟎ˡ M) ⟩ + M [+] M ≈⟨ [+]-idem M ⟩ + M ∎ + where + open ≈-Reasoning (Matrixₛ _ _) + +Mat-IdempotentSemiadditiveDagger : IdempotentSemiadditiveDagger Mat +Mat-IdempotentSemiadditiveDagger = record + { semiadditiveDagger = Mat-SemiadditiveDagger + ; idempotent = idem _ + } + +Mat-Dagger-2-Poset : Dagger-2-Poset +Mat-Dagger-2-Poset = dagger-2-poset Mat-IdempotentSemiadditiveDagger diff --git a/Data/Matrix/Monoid.agda b/Data/Matrix/Monoid.agda new file mode 100644 index 0000000..b7638f6 --- /dev/null +++ b/Data/Matrix/Monoid.agda @@ -0,0 +1,93 @@ +{-# OPTIONS --without-K --safe #-} + +open import Algebra using (Monoid) +open import Level using (Level) + +module Data.Matrix.Monoid {c ℓ : Level} (M : Monoid c ℓ) where + +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.Nat using (ℕ) +open import Data.Vec using (Vec; replicate; zipWith) +open import Data.Vec.Properties using (zipWith-replicate) +open import Data.Vector.Monoid M using (_⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ; ⟨ε⟩) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) + +open M +open Vec +open ℕ + +private + variable + A B C : ℕ + +opaque + + unfolding Matrix + + 𝟎 : Matrix A B + 𝟎 {A} {B} = replicate B ⟨ε⟩ + + opaque + + unfolding _ᵀ []ᵥ ⟨ε⟩ + + 𝟎ᵀ : 𝟎 ᵀ ≡ 𝟎 {A} {B} + 𝟎ᵀ {zero} = ≡.refl + 𝟎ᵀ {suc A} = let open ≡-Reasoning in begin + ⟨ε⟩ ∷ₕ (𝟎 ᵀ) ≡⟨ ≡.cong (⟨ε⟩ ∷ₕ_) 𝟎ᵀ ⟩ + ⟨ε⟩ ∷ₕ 𝟎 ≡⟨ zipWith-replicate _∷_ ε ⟨ε⟩ ⟩ + 𝟎 ∎ + + opaque + + unfolding _≑_ + + 𝟎≑𝟎 : 𝟎 {A} {B} ≑ 𝟎 {A} {C} ≡ 𝟎 + 𝟎≑𝟎 {B = zero} = ≡.refl + 𝟎≑𝟎 {B = suc B} = ≡.cong (⟨ε⟩ ∷_) (𝟎≑𝟎 {B = B}) + + opaque + + unfolding _∷ₕ_ ⟨ε⟩ + + ⟨ε⟩∷ₕ𝟎 : ⟨ε⟩ ∷ₕ 𝟎 {A} {B} ≡ 𝟎 + ⟨ε⟩∷ₕ𝟎 {A} {zero} = ≡.refl + ⟨ε⟩∷ₕ𝟎 {A} {suc B} = ≡.cong (⟨ε⟩ ∷_) ⟨ε⟩∷ₕ𝟎 + +𝟎∥𝟎 : 𝟎 {A} {C} ∥ 𝟎 {B} {C} ≡ 𝟎 +𝟎∥𝟎 {zero} {C} rewrite []ᵥ-! (𝟎 {0} {C}) = []ᵥ-∥ 𝟎 +𝟎∥𝟎 {suc A} {C} {B} = begin + 𝟎 ∥ 𝟎 ≡⟨ ≡.cong (_∥ 𝟎) (⟨ε⟩∷ₕ𝟎 {A} {C}) ⟨ + (⟨ε⟩ ∷ₕ 𝟎 {A}) ∥ 𝟎 ≡⟨ ∷ₕ-∥ ⟨ε⟩ 𝟎 𝟎 ⟨ + ⟨ε⟩ ∷ₕ 𝟎 {A} ∥ 𝟎 ≡⟨ ≡.cong (⟨ε⟩ ∷ₕ_) 𝟎∥𝟎 ⟩ + ⟨ε⟩ ∷ₕ 𝟎 ≡⟨ ⟨ε⟩∷ₕ𝟎 ⟩ + 𝟎 ∎ + where + open ≡-Reasoning + +opaque + + unfolding Matrix + + _[+]_ : Matrix A B → Matrix A B → Matrix A B + _[+]_ = zipWith _⊕_ + + [+]-cong : {M M′ N N′ : Matrix A B} → M ≋ M′ → N ≋ N′ → M [+] N ≋ M′ [+] N′ + [+]-cong = PW.zipWith-cong ⊕-cong + + opaque + + unfolding 𝟎 + + [+]-𝟎ˡ : (M : Matrix A B) → 𝟎 [+] M ≋ M + [+]-𝟎ˡ [] = PW.[] + [+]-𝟎ˡ (M₀ ∷ M) = ⊕-identityˡ M₀ PW.∷ [+]-𝟎ˡ M + + [+]-𝟎ʳ : (M : Matrix A B) → M [+] 𝟎 ≋ M + [+]-𝟎ʳ [] = PW.[] + [+]-𝟎ʳ (M₀ ∷ M) = ⊕-identityʳ M₀ PW.∷ [+]-𝟎ʳ M diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda new file mode 100644 index 0000000..220ff2e --- /dev/null +++ b/Data/Matrix/SemiadditiveDagger.agda @@ -0,0 +1,389 @@ +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Bundles using (CommutativeSemiring) +open import Level using (Level) + +module Data.Matrix.SemiadditiveDagger {c ℓ : Level} (R : CommutativeSemiring c ℓ) where + +module R = CommutativeSemiring R + +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Data.Vec.Relation.Binary.Pointwise.Inductive as PW +import Data.Nat.Properties as ℕ-Props +import Data.Nat as ℕ + +open import Categories.Category.Cocartesian using (Cocartesian) +open import Categories.Object.Coproduct using (Coproduct) +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.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.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.Monoid R.+-monoid using () renaming (⟨ε⟩ to ⟨0⟩) +open import Data.Vector.Vec using (replicate-++) +open import Function using (_∘_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) + +open R +open Vec +open ℕ.ℕ + +private + variable + A B C D E F : ℕ + +opaque + unfolding Vector _∙_ + ∙-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 _[_] [_]_ _ᵀ []ᵥ ⟨⟩ _∷ₕ_ _≊_ _≋_ _∷ᵥ_ + [-]-ᵀ : (M : Matrix A B) (V : Vector A) → M [ V ] ≊ [ V ] (M ᵀ) + [-]-ᵀ [] V = ≊.sym (≊.reflexive ([-]-[]ᵥ V)) + [-]-ᵀ (M₀ ∷ M) V = begin + M₀ ∙ V ∷ map (_∙ V) M ≈⟨ ∙-comm M₀ V PW.∷ (PW.map⁺ (λ {x} ≊V → trans (∙-comm x V) (∙-cong ≊.refl ≊V)) ≋.refl) ⟩ + V ∙ M₀ ∷ map (V ∙_) M ≡⟨⟩ + map (V ∙_) (M₀ ∷ᵥ M) ≡⟨ ≡.cong (map (V ∙_) ∘ (M₀ ∷ᵥ_)) (M ᵀᵀ) ⟨ + map (V ∙_) (M₀ ∷ᵥ M ᵀ ᵀ) ≡⟨ ≡.cong (map (V ∙_)) (∷ₕ-ᵀ M₀ (M ᵀ)) ⟨ + map (V ∙_) ((M₀ ∷ₕ (M ᵀ)) ᵀ) ∎ + where + open ≈-Reasoning (Vectorₛ _) + +opaque + unfolding []ᵥ mapRows ⟨⟩ _∷ₕ_ _∷ᵥ_ _ᵀ + ·-ᵀ + : {A B C : ℕ} + (M : Matrix A B) + (N : Matrix B C) + → (N · M) ᵀ ≋ M ᵀ · N ᵀ + ·-ᵀ {A} {B} {zero} M [] = begin + []ᵥ ≡⟨ map-const (M ᵀ) ⟨⟩ ⟨ + map (λ _ → ⟨⟩) (M ᵀ) ≡⟨ map-cong [-]-[]ᵥ (M ᵀ) ⟨ + map ([_] []ᵥ) (M ᵀ) ∎ + where + open ≈-Reasoning (Matrixₛ 0 A) + ·-ᵀ {A} {B} {suc C} M (N₀ ∷ N) = begin + map ([_] M) (N₀ ∷ N) ᵀ ≡⟨ -[-]ᵀ (N₀ ∷ N) M ⟨ + map ((N₀ ∷ N) [_]) (M ᵀ) ≈⟨ PW.map⁺ (λ {V} ≋V → ≊.trans ([-]-ᵀ (N₀ ∷ N) V) ([-]--cong {A = (N₀ ∷ᵥ N) ᵀ} ≋V ≋.refl)) ≋.refl ⟩ + map ([_] ((N₀ ∷ N) ᵀ)) (M ᵀ) ≡⟨ map-cong (λ V → ≡.cong ([ V ]_) (∷ᵥ-ᵀ N₀ N)) (M ᵀ) ⟩ + map ([_] (N₀ ∷ₕ N ᵀ)) (M ᵀ) ∎ + where + open ≈-Reasoning (Matrixₛ (suc C) A) + +opaque + unfolding _≋_ + ᵀ-involutive : (M : Matrix A B) → (M ᵀ) ᵀ ≋ M + ᵀ-involutive M = ≋.reflexive (M ᵀᵀ) + +opaque + unfolding _≋_ + ≋λᵀ : ([]ᵥ ∥ I) ᵀ ≋ 𝟎 ≑ I {A} + ≋λᵀ = begin + ([]ᵥ ∥ I) ᵀ ≡⟨ ≡.cong (_ᵀ) ([]ᵥ-∥ I) ⟩ + I ᵀ ≡⟨ Iᵀ ⟩ + I ≡⟨ []ₕ-≑ I ⟨ + []ₕ ≑ I ≡⟨ ≡.cong (_≑ I) ([]ₕ-! 𝟎) ⟨ + 𝟎 ≑ I ∎ + where + open ≈-Reasoning (Matrixₛ _ _) + +opaque + unfolding Matrix _∥_ _ᵀ _≑_ _∷ₕ_ + ∥-ᵀ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) ᵀ ≡ M ᵀ ≑ N ᵀ + ∥-ᵀ {A} {zero} {B} [] [] = ≡.sym (replicate-++ A B []) + ∥-ᵀ (M₀ ∷ M) (N₀ ∷ N) = begin + (M₀ ++ N₀) ∷ₕ ((M ∥ N) ᵀ) ≡⟨ ≡.cong ((M₀ ++ N₀) ∷ₕ_) (∥-ᵀ M N) ⟩ + (M₀ ++ N₀) ∷ₕ (M ᵀ ≑ N ᵀ) ≡⟨ ∷ₕ-≑ M₀ N₀ (M ᵀ) (N ᵀ) ⟩ + (M₀ ∷ₕ M ᵀ) ≑ (N₀ ∷ₕ N ᵀ) ∎ + where + open ≡-Reasoning + +≑-ᵀ : (M : Matrix A B) (N : Matrix A C) → (M ≑ N) ᵀ ≡ M ᵀ ∥ N ᵀ +≑-ᵀ M N = begin + (M ≑ N) ᵀ ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ≑ h₂) ᵀ) (M ᵀᵀ) (N ᵀᵀ) ⟨ + (M ᵀ ᵀ ≑ N ᵀ ᵀ ) ᵀ ≡⟨ ≡.cong (_ᵀ) (∥-ᵀ (M ᵀ) (N ᵀ)) ⟨ + (M ᵀ ∥ N ᵀ ) ᵀ ᵀ ≡⟨ (M ᵀ ∥ N ᵀ ) ᵀᵀ ⟩ + M ᵀ ∥ N ᵀ ∎ + where + open ≡-Reasoning + +opaque + unfolding _≋_ + ≋ρᵀ : (I ∥ []ᵥ) ᵀ ≋ I {A} ≑ 𝟎 + ≋ρᵀ {A} = begin + (I ∥ []ᵥ) ᵀ ≡⟨ ∥-ᵀ I []ᵥ ⟩ + I ᵀ ≑ []ᵥ ᵀ ≡⟨ ≡.cong (I ᵀ ≑_) []ᵥ-ᵀ ⟩ + I ᵀ ≑ []ₕ ≡⟨ ≡.cong (_≑ []ₕ) Iᵀ ⟩ + I ≑ []ₕ ≡⟨ ≡.cong (I ≑_) ([]ₕ-! 𝟎) ⟨ + I ≑ 𝟎 ∎ + where + open ≈-Reasoning (Matrixₛ _ _) + +opaque + unfolding _≋_ + ≋αᵀ : (((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎)) ∥ (𝟎 {_} {A} ≑ I {B ℕ.+ C}) · (𝟎 ≑ I {C})) ᵀ + ≋ (I {A ℕ.+ B} ≑ 𝟎) · (I {A} ≑ 𝟎) ∥ (I {A ℕ.+ B} ≑ 𝟎) · (𝟎 ≑ I {B}) ∥ (𝟎 ≑ I {C}) + ≋αᵀ {A} {B} {C} = begin + (((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ + ≡⟨ ∥-ᵀ ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ⟩ + ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ + ≡⟨ ≡.cong (_≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (∥-ᵀ (I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C}))) ⟩ + ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ + ≡⟨ ≡.cong (λ h → (h ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (≑-ᵀ I 𝟎) ⟩ + (I {A} ᵀ ∥ 𝟎 {A} {B ℕ.+ C} ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ + ≡⟨ ≡.cong (λ h → (h ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (≡.cong₂ _∥_ Iᵀ 𝟎ᵀ) ⟩ + (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ + ≈⟨ ≑-cong (≑-cong ≋.refl (·-ᵀ (I ≑ 𝟎) (𝟎 ≑ I))) (·-ᵀ (𝟎 ≑ I) (𝟎 ≑ I)) ⟩ + (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ≑ 𝟎 {B} {C}) ᵀ · (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) ᵀ) ≑ (𝟎 {C} {B} ≑ I {C}) ᵀ · (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) ᵀ + ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ (λ h₁ h₂ → I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ h₁ · h₂) (≑-ᵀ I 𝟎) (≑-ᵀ 𝟎 I)) (≡.cong₂ _·_ (≑-ᵀ 𝟎 I) (≑-ᵀ 𝟎 I)) ⟩ + (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ᵀ ∥ 𝟎 {B} {C} ᵀ) · (𝟎 {B ℕ.+ C} {A} ᵀ ∥ I {B ℕ.+ C} ᵀ)) ≑ (𝟎 {C} {B} ᵀ ∥ I {C} ᵀ) · (𝟎 {B ℕ.+ C} {A} ᵀ ∥ I {B ℕ.+ C} ᵀ) + ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ (λ h₁ h₂ → I {A} ∥ 𝟎 ≑ h₁ · h₂) (≡.cong₂ _∥_ Iᵀ 𝟎ᵀ) (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ)) (≡.cong₂ _·_ (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ) (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ)) ⟩ + (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ∥ 𝟎 {C} {B}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C}) + ≡⟨ ≡.cong (λ h → (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ h) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})) (·-∥ (I ∥ 𝟎) 𝟎 I) ⟩ + (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ∥ 𝟎 {C} {B}) · 𝟎 {A} {B ℕ.+ C} ∥ (I {B} ∥ 𝟎 {C} {B}) · I {B ℕ.+ C}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C}) + ≈⟨ ≑-cong (≑-cong ≋.refl (∥-cong (·-𝟎ʳ (I ∥ 𝟎)) ·-Iʳ)) (≋.refl {x = (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})}) ⟩ + (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C}) + ≡⟨ ≡.cong ((I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑_) (·-∥ (𝟎 ∥ I) 𝟎 I) ⟩ + (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B} {C} ∥ I {C}) · I {B ℕ.+ C} + ≈⟨ ≑-cong ≋.refl (∥-cong (·-𝟎ʳ (𝟎 ∥ I)) ·-Iʳ) ⟩ + (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ 𝟎 {A} {C} ∥ 𝟎 {B} {C} ∥ I {C} + ≡⟨ ≡.cong (λ h → (I {A} ∥ h ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ 𝟎 {A} {C} ∥ 𝟎 {B} {C} ∥ I {C}) 𝟎∥𝟎 ⟨ + (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ I {B} ∥ 𝟎 {C}) ≑ 𝟎 {A} ∥ 𝟎 {B} ∥ I {C} + ≡⟨ ≑-sym-assoc (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C}) (𝟎 {A} ∥ I {B} ∥ 𝟎 {C}) (𝟎 {A} ∥ 𝟎 {B} ∥ I {C}) ⟨ + cast₂ _ (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ I {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ 𝟎 {B} ∥ I {C}) + ≡⟨ ≡.cong (cast₂ _) (∥-≑⁴ I 𝟎 𝟎 𝟎 I 𝟎 𝟎 𝟎 I) ⟩ + cast₂ (≡.sym assoc) ((I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥ (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C}))) + ≡⟨ cast₂-∥ (≡.sym assoc) ((I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C}))) ((𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C}))) ⟨ + (cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C}))) ∥ cast₂ (≡.sym assoc) ((𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C}))) + ≡⟨ ≡.cong (cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥_) (cast₂-∥ (≡.sym assoc) (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) (𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})) ⟨ + cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥ cast₂ (≡.sym assoc) (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ cast₂ (≡.sym assoc) (𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C}) + ≡⟨ ≡.cong₂ _∥_ (≑-sym-assoc I 𝟎 𝟎) (≡.cong₂ _∥_ (≑-sym-assoc 𝟎 I 𝟎) (≑-sym-assoc 𝟎 𝟎 I)) ⟩ + ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B}) ≑ I {C}) + ≡⟨ ≡.cong (λ h → ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ (h ≑ I {C})) 𝟎≑𝟎 ⟩ + ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) + ≈⟨ ∥-cong ≋.refl (∥-cong (≑-cong ·-Iˡ (·-𝟎ˡ (𝟎 ≑ I))) ≋.refl) ⟨ + ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ (((I {A ℕ.+ B} · (𝟎 {B} {A} ≑ I {B})) ≑ (𝟎 {A ℕ.+ B} {C} · (𝟎 {B} {A} ≑ I {B})))) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) + ≡⟨ ≡.cong (λ h → ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ h ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})) (≑-· I 𝟎 (𝟎 ≑ I)) ⟨ + ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) + ≈⟨ ∥-cong (≑-cong ·-Iˡ (·-𝟎ˡ (I ≑ 𝟎))) ≋.refl ⟨ + ((I {A ℕ.+ B} · (I {A} ≑ 𝟎 {A} {B})) ≑ (𝟎 {A ℕ.+ B} {C} · (I {A} ≑ 𝟎 {A} {B}))) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) + ≡⟨ ≡.cong (λ h → h ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})) (≑-· I 𝟎 (I ≑ 𝟎)) ⟨ + (I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (I {A} ≑ 𝟎 {A} {B}) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) ∎ + where + assoc : A ℕ.+ B ℕ.+ C ≡ A ℕ.+ (B ℕ.+ C) + assoc = ℕ-Props.+-assoc A B C + open ≈-Reasoning (Matrixₛ _ _) + +≋σᵀ : ((𝟎 ≑ I {A}) ∥ (I {B} ≑ 𝟎)) ᵀ ≋ (𝟎 ≑ I {B}) ∥ (I {A} ≑ 𝟎) +≋σᵀ {A} {B} = begin + ((𝟎 ≑ I) ∥ (I ≑ 𝟎)) ᵀ ≡⟨ ∥-ᵀ (𝟎 ≑ I) (I ≑ 𝟎) ⟩ + (𝟎 ≑ I {A}) ᵀ ≑ (I ≑ 𝟎) ᵀ ≡⟨ ≡.cong₂ _≑_ (≑-ᵀ 𝟎 I) (≑-ᵀ I 𝟎) ⟩ + 𝟎 ᵀ ∥ (I {A}) ᵀ ≑ I ᵀ ∥ 𝟎 ᵀ ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ) (≡.cong₂ _∥_ Iᵀ 𝟎ᵀ) ⟩ + 𝟎 ∥ I {A} ≑ I ∥ 𝟎 ≡⟨ ∥-≑ 𝟎 I I 𝟎 ⟩ + (𝟎 ≑ I {B}) ∥ (I ≑ 𝟎) ∎ + where + open ≈-Reasoning (Matrixₛ _ _) + +≋⊗ : (M : Matrix A B) + (N : Matrix C D) + → (I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N + ≋ (M ≑ 𝟎) ∥ (𝟎 ≑ N) +≋⊗ M N = begin + (I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N ≡⟨ ≡.cong₂ _∥_ (≑-· I 𝟎 M) (≑-· 𝟎 I N) ⟩ + (I · M ≑ 𝟎 · M) ∥ (𝟎 · N ≑ I · N) ≈⟨ ∥-cong (≑-cong ·-Iˡ (·-𝟎ˡ M)) (≑-cong (·-𝟎ˡ N) ·-Iˡ) ⟩ + (M ≑ 𝟎) ∥ (𝟎 ≑ N) ∎ + where + open ≈-Reasoning (Matrixₛ _ _) + +ᵀ-resp-⊗ + : {M : Matrix A B} + {N : Matrix C D} + → ((I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N) ᵀ + ≋ (I ≑ 𝟎) · M ᵀ ∥ (𝟎 ≑ I) · N ᵀ +ᵀ-resp-⊗ {M = M} {N = N} = begin + ((I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N) ᵀ ≈⟨ -ᵀ-cong (≋⊗ M N) ⟩ + ((M ≑ 𝟎) ∥ (𝟎 ≑ N)) ᵀ ≡⟨ ≡.cong (_ᵀ) (∥-≑ M 𝟎 𝟎 N) ⟨ + ((M ∥ 𝟎) ≑ (𝟎 ∥ N)) ᵀ ≡⟨ ≑-ᵀ (M ∥ 𝟎) (𝟎 ∥ N) ⟩ + (M ∥ 𝟎) ᵀ ∥ (𝟎 ∥ N) ᵀ ≡⟨ ≡.cong₂ _∥_ (∥-ᵀ M 𝟎) (∥-ᵀ 𝟎 N) ⟩ + (M ᵀ ≑ 𝟎 ᵀ) ∥ (𝟎 ᵀ ≑ N ᵀ) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (M ᵀ ≑ h₁) ∥ (h₂ ≑ N ᵀ)) 𝟎ᵀ 𝟎ᵀ ⟩ + (M ᵀ ≑ 𝟎) ∥ (𝟎 ≑ N ᵀ) ≈⟨ ≋⊗ (M ᵀ) (N ᵀ) ⟨ + (I ≑ 𝟎) · M ᵀ ∥ (𝟎 ≑ I) · N ᵀ ∎ + where + open ≈-Reasoning (Matrixₛ _ _) + +inj₁ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (I ≑ 𝟎) ≋ M +inj₁ {A} {C} M N = begin + (M ∥ N) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ M N I 𝟎 ⟩ + (M · I) [+] (N · 𝟎) ≈⟨ [+]-cong ·-Iʳ (·-𝟎ʳ N) ⟩ + M [+] 𝟎 ≈⟨ [+]-𝟎ʳ M ⟩ + M ∎ + where + open ≈-Reasoning (Matrixₛ A C) + +inj₂ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (𝟎 ≑ I) ≋ N +inj₂ {A} {C} {B} M N = begin + (M ∥ N) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ M N 𝟎 I ⟩ + (M · 𝟎) [+] (N · I) ≈⟨ [+]-cong (·-𝟎ʳ M) ·-Iʳ ⟩ + 𝟎 [+] N ≈⟨ [+]-𝟎ˡ N ⟩ + N ∎ + where + open ≈-Reasoning (Matrixₛ B C) + +opaque + unfolding Matrix + split-∥ : (A : ℕ) → (M : Matrix (A ℕ.+ B) C) → Σ[ M₁ ∈ Matrix A C ] Σ[ M₂ ∈ Matrix B C ] M₁ ∥ M₂ ≡ M + split-∥ zero M = []ᵥ , M , []ᵥ-∥ M + split-∥ (suc A) M′ + rewrite ≡.sym (head-∷-tailₕ M′) + using M₀ ← headₕ M′ + using M ← tailₕ M′ + with split-∥ A M + ... | M₁ , M₂ , M₁∥M₂≡M = M₀ ∷ₕ M₁ , M₂ , (begin + (M₀ ∷ₕ M₁) ∥ M₂ ≡⟨ ∷ₕ-∥ M₀ M₁ M₂ ⟨ + M₀ ∷ₕ M₁ ∥ M₂ ≡⟨ ≡.cong (M₀ ∷ₕ_) M₁∥M₂≡M ⟩ + M₀ ∷ₕ M ∎) + where + open ≡-Reasoning + +uniq + : (H : Matrix (A ℕ.+ B) C) + (M : Matrix A C) + (N : Matrix B C) + → H · (I ≑ 𝟎) ≋ M + → H · (𝟎 ≑ I) ≋ N + → M ∥ N ≋ H +uniq {A} {B} {C} H M N eq₁ eq₂ + with (H₁ , H₂ , H₁∥H₂≡H) ← split-∥ A H + rewrite ≡.sym H₁∥H₂≡H = begin + M ∥ N ≈⟨ ∥-cong eq₁ eq₂ ⟨ + (H₁ ∥ H₂) · (I {A} ≑ 𝟎) ∥ (H₁ ∥ H₂) · (𝟎 ≑ I) ≈⟨ ∥-cong (inj₁ H₁ H₂) (inj₂ H₁ H₂) ⟩ + (H₁ ∥ H₂) ∎ + where + open ≈-Reasoning (Matrixₛ (A ℕ.+ B) C) + +coproduct : Coproduct Mat A B +coproduct {A} {B} = record + { A+B = A ℕ.+ B + ; i₁ = I ≑ 𝟎 + ; i₂ = 𝟎 ≑ I + ; [_,_] = _∥_ + ; inject₁ = λ {a} {b} {c} → inj₁ b c + ; inject₂ = λ {a} {b} {c} → inj₂ b c + ; unique = λ eq₁ eq₂ → uniq _ _ _ eq₁ eq₂ + } + +opaque + unfolding _≋_ + !-unique : (E : Matrix 0 B) → []ᵥ ≋ E + !-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E)) + +initial : Initial Mat +initial = record + { ⊥ = 0 + ; ⊥-is-initial = record + { ! = []ᵥ + ; !-unique = !-unique + } + } + +Mat-Cocartesian : Cocartesian Mat +Mat-Cocartesian = record + { initial = initial + ; coproducts = record + { coproduct = coproduct + } + } + +Mat-DaggerCocartesian : DaggerCocartesianMonoidal Mat +Mat-DaggerCocartesian = record + { cocartesian = Mat-Cocartesian + ; dagger = record + { _† = λ M → M ᵀ + ; †-identity = ≋.reflexive Iᵀ + ; †-homomorphism = λ {f = f} {g} → ·-ᵀ f g + ; †-resp-≈ = -ᵀ-cong + ; †-involutive = ᵀ-involutive + } + ; λ≅† = ≋λᵀ + ; ρ≅† = ≋ρᵀ + ; α≅† = ≋αᵀ + ; σ≅† = ≋σᵀ + ; †-resp-⊗ = ᵀ-resp-⊗ + } + +p₁-i₁ : (I ≑ 𝟎) ᵀ · (I ≑ 𝟎 {A} {B}) ≋ I +p₁-i₁ = begin + (I ≑ 𝟎) ᵀ · (I ≑ 𝟎) ≡⟨ ≡.cong (_· (I ≑ 𝟎)) (≑-ᵀ I 𝟎) ⟩ + (I ᵀ ∥ 𝟎 ᵀ) · (I ≑ 𝟎) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (I ≑ 𝟎)) Iᵀ 𝟎ᵀ ⟩ + (I ∥ 𝟎) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ I 𝟎 I 𝟎 ⟩ + (I · I) [+] (𝟎 · 𝟎) ≈⟨ [+]-cong ·-Iˡ (·-𝟎ˡ 𝟎) ⟩ + I [+] 𝟎 ≈⟨ [+]-𝟎ʳ I ⟩ + I ∎ + where + open ≈-Reasoning (Matrixₛ _ _) + +p₂-i₂ : (𝟎 {A} {B} ≑ I) ᵀ · (𝟎 ≑ I) ≋ I +p₂-i₂ = begin + (𝟎 ≑ I) ᵀ · (𝟎 ≑ I) ≡⟨ ≡.cong (_· (𝟎 ≑ I)) (≑-ᵀ 𝟎 I) ⟩ + (𝟎 ᵀ ∥ I ᵀ) · (𝟎 ≑ I) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (𝟎 ≑ I)) 𝟎ᵀ Iᵀ ⟩ + (𝟎 ∥ I) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ 𝟎 I 𝟎 I ⟩ + (𝟎 · 𝟎) [+] (I · I) ≈⟨ [+]-cong (·-𝟎ˡ 𝟎) ·-Iˡ ⟩ + 𝟎 [+] I ≈⟨ [+]-𝟎ˡ I ⟩ + I ∎ + where + open ≈-Reasoning (Matrixₛ _ _) + +opaque + unfolding 𝟎 ⟨⟩ + []ᵥ·[]ₕ : []ᵥ · []ₕ ≡ 𝟎 {A} {B} + []ᵥ·[]ₕ {A} {B} = begin + map ([_] []ₕ) []ᵥ ≡⟨ map-cong (λ { [] → [⟨⟩]-[]ₕ }) []ᵥ ⟩ + map (λ _ → ⟨0⟩) []ᵥ ≡⟨ map-const []ᵥ ⟨0⟩ ⟩ + 𝟎 ∎ + where + open ≡-Reasoning + +p₂-i₁ : (𝟎 {A} ≑ I) ᵀ · (I ≑ 𝟎 {B}) ≋ []ᵥ · []ᵥ ᵀ +p₂-i₁ = begin + (𝟎 ≑ I) ᵀ · (I ≑ 𝟎) ≡⟨ ≡.cong (_· (I ≑ 𝟎)) (≑-ᵀ 𝟎 I) ⟩ + (𝟎 ᵀ ∥ I ᵀ) · (I ≑ 𝟎) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (I ≑ 𝟎)) 𝟎ᵀ Iᵀ ⟩ + (𝟎 ∥ I) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ 𝟎 I I 𝟎 ⟩ + (𝟎 · I) [+] (I · 𝟎) ≈⟨ [+]-cong (·-𝟎ˡ I) (·-𝟎ʳ I) ⟩ + 𝟎 [+] 𝟎 ≈⟨ [+]-𝟎ˡ 𝟎 ⟩ + 𝟎 ≡⟨ []ᵥ·[]ₕ ⟨ + []ᵥ · []ₕ ≡⟨ ≡.cong ([]ᵥ ·_) []ᵥ-ᵀ ⟨ + []ᵥ · []ᵥ ᵀ ∎ + where + open ≈-Reasoning (Matrixₛ _ _) + +p₁-i₂ : (I ≑ 𝟎 {A}) ᵀ · (𝟎 {B} ≑ I) ≋ []ᵥ · []ᵥ ᵀ +p₁-i₂ = begin + (I ≑ 𝟎) ᵀ · (𝟎 ≑ I) ≡⟨ ≡.cong (_· (𝟎 ≑ I)) (≑-ᵀ I 𝟎) ⟩ + (I ᵀ ∥ 𝟎 ᵀ) · (𝟎 ≑ I) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (𝟎 ≑ I)) Iᵀ 𝟎ᵀ ⟩ + (I ∥ 𝟎) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ I 𝟎 𝟎 I ⟩ + (I · 𝟎) [+] (𝟎 · I) ≈⟨ [+]-cong (·-𝟎ʳ I) (·-𝟎ˡ I) ⟩ + 𝟎 [+] 𝟎 ≈⟨ [+]-𝟎ˡ 𝟎 ⟩ + 𝟎 ≡⟨ []ᵥ·[]ₕ ⟨ + []ᵥ · []ₕ ≡⟨ ≡.cong ([]ᵥ ·_) []ᵥ-ᵀ ⟨ + []ᵥ · []ᵥ ᵀ ∎ + where + open ≈-Reasoning (Matrixₛ _ _) + +Mat-SemiadditiveDagger : SemiadditiveDagger Mat +Mat-SemiadditiveDagger = record + { daggerCocartesianMonoidal = Mat-DaggerCocartesian + ; p₁-i₁ = p₁-i₁ + ; p₂-i₂ = p₂-i₂ + ; p₂-i₁ = p₂-i₁ + ; p₁-i₂ = p₁-i₂ + } diff --git a/Data/Matrix/Transform.agda b/Data/Matrix/Transform.agda new file mode 100644 index 0000000..671725f --- /dev/null +++ b/Data/Matrix/Transform.agda @@ -0,0 +1,298 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; 0ℓ; _⊔_) +open import Relation.Binary using (Setoid; Rel; IsEquivalence) +open import Algebra using (Semiring) + +module Data.Matrix.Transform {c ℓ : Level} (R : Semiring c ℓ) where + +module R = Semiring R + +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.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 + using + ( Matrix; Matrixₛ; _≋_; ≋-isEquiv; _ᵀ; _∷ₕ_; []ᵥ; []ₕ; []ᵥ-ᵀ; mapRows + ; _ᵀᵀ; []ᵥ-!; ∷ₕ-ᵀ; ∷ₕ-cong; module ≋; -ᵀ-cong; _∥_; []ᵥ-∥; headₕ; tailₕ; head-∷-tailₕ; ∷ₕ-∥ + ; _≑_; []ᵥ-≑; ∷ₕ-≑ + ) +open import Data.Matrix.Monoid R.+-monoid 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ʳ) + +open Vec +open ℕ +open R + +private + variable + n m p : ℕ + A B C D : ℕ + +opaque + + unfolding Matrix + + opaque + + unfolding Vector + + _[_] : Matrix n m → Vector n → Vector m + _[_] M V = map (_∙ V) M + + [_]_ : Vector m → Matrix n m → Vector n + [_]_ V M = map (V ∙_) (M ᵀ) + + -[-]-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 + + [-]--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) ∙_)) []ᵥ-ᵀ + + opaque + + unfolding []ᵥ _ᵀ ⟨0⟩ _∙_ + + [-]-[]ₕ : (V : Vector 0) → [ V ] []ₕ ≡ ⟨0⟩ {n} + [-]-[]ₕ {zero} [] = ≡.refl + [-]-[]ₕ {suc A} [] = ≡.cong (0# ∷_) ([-]-[]ₕ []) + +opaque + + unfolding Matrix Vector + + -- The identity matrix + I : Matrix n n + I {zero} = [] + I {suc n} = (1# ∷ ⟨0⟩) ∷ ⟨0⟩ ∷ₕ I + + opaque + + unfolding _ᵀ _∷ₕ_ + + Iᵀ : I ᵀ ≡ I {n} + Iᵀ {zero} = ≡.sym ([]ᵥ-! []) + Iᵀ {suc n} = begin + (1# ∷ ⟨0⟩) ∷ₕ ((⟨0⟩ ∷ₕ I) ᵀ) ≡⟨ ≡.cong ((1# ∷ ⟨0⟩) ∷ₕ_) (∷ₕ-ᵀ ⟨0⟩ I) ⟩ + (1# ∷ ⟨0⟩) ∷ (⟨0⟩ ∷ₕ (I ᵀ)) ≡⟨ ≡.cong (λ h → (1# ∷ ⟨0⟩) ∷ (⟨0⟩ ∷ₕ h)) Iᵀ ⟩ + (1# ∷ ⟨0⟩) ∷ (⟨0⟩ ∷ₕ I) ∎ + where + open ≡-Reasoning + +opaque + unfolding mapRows _ᵀ _[_] [_]_ []ᵥ + -[-]ᵀ : (A : Matrix m p) (B : Matrix n m) → mapRows (A [_]) (B ᵀ) ≡ (mapRows ([_] B) A) ᵀ + -[-]ᵀ [] B = map-const (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) ᵀ) ∎ + where + open ≡-Reasoning + +opaque + unfolding [_]_ _[_] _ᵀ []ₕ _∙_ _∷ₕ_ _⟨_⟩ + + []-∙ : (V : Vector m) (M : Matrix n m) (W : Vector n) → [ V ] M ∙ W ≈ V ∙ M [ W ] + []-∙ {n = n} [] M@[] W = begin + [ [] ] []ₕ ∙ W ≡⟨ ≡.cong (_∙ W) ([-]-[]ₕ []) ⟩ + ⟨0⟩ ∙ W ≈⟨ ∙-zeroˡ W ⟩ + 0# ∎ + where + open ≈-Reasoning setoid + []-∙ (V₀ ∷ V) (M₀ ∷ M) W = begin + [ V₀ ∷ V ] (M₀ ∷ M) ∙ W ≡⟨ ≡.cong (_∙ W) (map-zipWith ((V₀ ∷ V) ∙_) _∷_ M₀ (M ᵀ)) ⟩ + (zipWith (λ x y → V₀ * x + V ∙ y) M₀ (M ᵀ)) ∙ W ≡⟨ ≡.cong (_∙ W) (zipWith-map-map (V₀ *_) (V ∙_) _+_ M₀ (M ᵀ)) ⟩ + (V₀ ⟨ M₀ ⟩ ⊕ [ V ] M) ∙ W ≈⟨ ∙-distribʳ (V₀ ⟨ M₀ ⟩) ([ V ] M) W ⟩ + V₀ ⟨ M₀ ⟩ ∙ W + [ V ] M ∙ W ≈⟨ +-congʳ (*-∙ˡ V₀ M₀ W) ⟨ + V₀ * (M₀ ∙ W) + ([ V ] M) ∙ W ≈⟨ +-congˡ ([]-∙ V M W) ⟩ + (V₀ ∷ V) ∙ (M₀ ∷ M) [ W ] ∎ + where + open ≈-Reasoning setoid + +opaque + unfolding Vector [_]_ I _∙_ ⟨0⟩ mapRows _ᵀ []ᵥ + [-]I : {n : ℕ} (V : Vector n) → [ V ] I ≊ V + [-]I {zero} [] = ≊.refl + [-]I {suc n} (x ∷ V) = begin + map ((x ∷ V) ∙_) ((1# ∷ ⟨0⟩) ∷ₕ (⟨0⟩ ∷ₕ I) ᵀ) ≡⟨ ≡.cong (λ h → map ((x ∷ V) ∙_) ((1# ∷ ⟨0⟩) ∷ₕ h)) (∷ₕ-ᵀ ⟨0⟩ I) ⟩ + x * 1# + V ∙ ⟨0⟩ ∷ map ((x ∷ V) ∙_) (⟨0⟩ ∷ₕ I ᵀ) ≈⟨ +-congʳ (*-identityʳ x) PW.∷ ≊.refl ⟩ + x + V ∙ ⟨0⟩ ∷ map ((x ∷ V) ∙_) (⟨0⟩ ∷ₕ I ᵀ) ≈⟨ +-congˡ (∙-zeroʳ V) PW.∷ ≊.refl ⟩ + x + 0# ∷ map ((x ∷ V) ∙_) (⟨0⟩ ∷ₕ I ᵀ) ≈⟨ +-identityʳ x PW.∷ ≊.refl ⟩ + x ∷ map ((x ∷ V) ∙_) (⟨0⟩ ∷ₕ I ᵀ) ≡⟨ ≡.cong (λ h → x ∷ map ((x ∷ V) ∙_) h) (zipWith-replicate₁ _∷_ 0# (I ᵀ)) ⟩ + x ∷ map ((x ∷ V) ∙_) (map (0# ∷_) (I ᵀ)) ≡⟨ ≡.cong (x ∷_) (map-∘ ((x ∷ V) ∙_) (0# ∷_) (I ᵀ)) ⟨ + x ∷ map (λ y → x * 0# + V ∙ y) (I ᵀ) ≈⟨ refl PW.∷ PW.map⁺ (λ ≊V → trans (+-congʳ (zeroʳ x)) (+-congˡ (∙-cong {v₁ = V} ≊.refl ≊V))) ≋.refl ⟩ + x ∷ map (λ y → 0# + V ∙ y) (I ᵀ) ≈⟨ refl PW.∷ PW.map⁺ (λ ≊V → trans (+-identityˡ (V ∙ _)) (∙-cong {v₁ = V} ≊.refl ≊V)) ≋.refl ⟩ + x ∷ map (V ∙_) (I ᵀ) ≈⟨ refl PW.∷ ([-]I V) ⟩ + x ∷ V ∎ + where + open ≈-Reasoning (Vectorₛ (suc n)) + +opaque + unfolding _≊_ I _[_] _∙_ _≋_ _∷ₕ_ ⟨0⟩ + I[-] : {n : ℕ} (V : Vector n) → I [ V ] ≊ V + I[-] {zero} [] = PW.[] + I[-] {suc n} (x ∷ V) = hd PW.∷ tl + where + hd : (1# ∷ ⟨0⟩) ∙ (x ∷ V) ≈ x + hd = begin + 1# * x + ⟨0⟩ ∙ V ≈⟨ +-congʳ (*-identityˡ x) ⟩ + x + ⟨0⟩ ∙ V ≈⟨ +-congˡ (∙-zeroˡ V) ⟩ + x + 0# ≈⟨ +-identityʳ x ⟩ + x ∎ + where + open ≈-Reasoning setoid + tl : map (_∙ (x ∷ V)) (⟨0⟩ ∷ₕ I) ≊ V + tl = begin + map (_∙ (x ∷ V)) (⟨0⟩ ∷ₕ I) ≡⟨ ≡.cong (map (_∙ (x ∷ V))) (zipWith-replicate₁ _∷_ 0# I) ⟩ + map (_∙ (x ∷ V)) (map (0# ∷_) I) ≡⟨ map-∘ (_∙ (x ∷ V)) (0# ∷_) I ⟨ + map (λ t → 0# * x + t ∙ V) I ≈⟨ PW.map⁺ (λ ≋X → trans (+-congʳ (zeroˡ x)) (+-congˡ (∙-cong ≋X ≊.refl))) {xs = I} ≋.refl ⟩ + map (λ t → 0# + t ∙ V) I ≈⟨ PW.map⁺ (λ {t} ≋X → trans (+-identityˡ (t ∙ V)) (∙-cong ≋X ≊.refl)) {xs = I} ≋.refl ⟩ + map (_∙ V) I ≈⟨ I[-] V ⟩ + V ∎ + where + open ≈-Reasoning (Vectorₛ n) + +opaque + unfolding mapRows _[_] _ᵀ _∷ₕ_ I + map--[-]-I : (M : Matrix n m) → mapRows (M [_]) I ≋ M ᵀ + map--[-]-I {n} {m} [] = ≋.reflexive (map-const I []) + map--[-]-I {n} {suc m} (M₀ ∷ M) = begin + map ((M₀ ∷ M) [_]) I ≡⟨⟩ + map (λ V → M₀ ∙ V ∷ M [ V ]) I ≡⟨ zipWith-map (M₀ ∙_) (M [_]) _∷_ I ⟨ + map (M₀ ∙_) I ∷ₕ (map (M [_]) I) ≈⟨ ∷ₕ-cong (≊.reflexive (≡.sym (≡.cong (map (M₀ ∙_)) Iᵀ))) (map--[-]-I M) ⟩ + [ M₀ ] I ∷ₕ (M ᵀ) ≈⟨ ∷ₕ-cong ([-]I M₀) ≋.refl ⟩ + M₀ ∷ₕ (M ᵀ) ∎ + where + open ≈-Reasoning (Matrixₛ (suc m) n) + +opaque + + unfolding [_]_ + + [-]--∥ + : (V : Vector C) + (M : Matrix A C) + (N : Matrix B C) + → [ V ] (M ∥ N) ≡ ([ V ] M) ++ ([ V ] N) + [-]--∥ {C} {zero} V M N rewrite []ᵥ-! M = begin + [ V ] ([]ᵥ ∥ N) ≡⟨ ≡.cong ([ V ]_) ([]ᵥ-∥ N) ⟩ + [ V ] N ≡⟨ ⟨⟩-++ ([ V ] N) ⟨ + ⟨⟩ ++ ([ V ] N) ≡⟨ ≡.cong (_++ ([ V ] N)) ([-]-[]ᵥ V) ⟨ + ([ V ] []ᵥ) ++ ([ V ] N) ∎ + where + open ≡-Reasoning + [-]--∥ {C} {suc A} V M N + rewrite ≡.sym (head-∷-tailₕ M) + using M₀ ← headₕ M + using M ← tailₕ M = begin + [ V ] ((M₀ ∷ₕ M) ∥ N) ≡⟨ ≡.cong ([ V ]_) (∷ₕ-∥ M₀ M N) ⟨ + [ V ] (M₀ ∷ₕ (M ∥ N)) ≡⟨ ≡.cong (map (V ∙_)) (∷ₕ-ᵀ M₀ (M ∥ N)) ⟩ + V ∙ M₀ ∷ ([ V ] (M ∥ N)) ≡⟨ ≡.cong (V ∙ M₀ ∷_) ([-]--∥ V M N) ⟩ + V ∙ M₀ ∷ (([ V ] M) ++ ([ V ] N)) ≡⟨⟩ + (V ∙ M₀ ∷ map (V ∙_ ) (M ᵀ)) ++ ([ V ] N) ≡⟨ ≡.cong (λ h → map (V ∙_) h ++ ([ V ] N)) (∷ₕ-ᵀ M₀ M) ⟨ + ([ V ] (M₀ ∷ₕ M)) ++ ([ V ] N) ∎ + where + open ≡-Reasoning + +opaque + + unfolding _++_ _∙_ + + ∙-++ : (W Y : Vector A) (X Z : Vector B) → (W ++ X) ∙ (Y ++ Z) ≈ W ∙ Y + X ∙ Z + ∙-++ [] [] X Z = sym (+-identityˡ (X ∙ Z)) + ∙-++ (w ∷ W) (y ∷ Y) X Z = begin + w * y + (W ++ X) ∙ (Y ++ Z) ≈⟨ +-congˡ (∙-++ W Y X Z) ⟩ + w * y + (W ∙ Y + X ∙ Z) ≈⟨ +-assoc _ _ _ ⟨ + (w * y + W ∙ Y) + X ∙ Z ∎ + where + open ≈-Reasoning setoid + +opaque + + 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 ] ([]ᵥ {B} ≑ []ᵥ) ≡⟨ ≡.cong ([ V ++ W ]_) []ᵥ-≑ ⟩ + [ 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 []ₕ []ᵥ [_]_ ⟨0⟩ _∙_ _ᵀ + + [⟨⟩]-[]ₕ : [ ⟨⟩ ] ([]ₕ {A}) ≡ ⟨0⟩ {A} + [⟨⟩]-[]ₕ {zero} = ≡.refl + [⟨⟩]-[]ₕ {suc A} = ≡.cong (0# ∷_) [⟨⟩]-[]ₕ + +opaque + + unfolding Vector ⟨⟩ ⟨0⟩ []ᵥ [_]_ _ᵀ _∷ₕ_ 𝟎 _≊_ + + [-]-𝟎 : (V : Vector A) → [ V ] (𝟎 {B}) ≊ ⟨0⟩ + [-]-𝟎 {A} {zero} V = ≊.reflexive (≡.cong (map (V ∙_)) 𝟎ᵀ) + [-]-𝟎 {A} {suc B} V = begin + map (V ∙_) (𝟎 ᵀ) ≡⟨ ≡.cong (map (V ∙_)) 𝟎ᵀ ⟩ + V ∙ ⟨0⟩ ∷ map (V ∙_) 𝟎 ≡⟨ ≡.cong ((V ∙ ⟨0⟩ ∷_) ∘ map (V ∙_)) 𝟎ᵀ ⟨ + V ∙ ⟨0⟩ ∷ [ V ] 𝟎 ≈⟨ ∙-zeroʳ V PW.∷ ([-]-𝟎 V) ⟩ + 0# ∷ ⟨0⟩ ∎ + where + open ≈-Reasoning (Vectorₛ (suc B)) + +opaque + + 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ₛ _) diff --git a/Data/Matrix/Vec.agda b/Data/Matrix/Vec.agda new file mode 100644 index 0000000..e0312d4 --- /dev/null +++ b/Data/Matrix/Vec.agda @@ -0,0 +1,20 @@ +{-# OPTIONS --without-K --safe #-} + +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) + +private + variable + a : Level + A : Set a + n m : ℕ + +open Vec + +transpose : Vec (Vec A n) m → Vec (Vec A m) n +transpose [] = replicate _ [] +transpose (row ∷ mat) = zipWith _∷_ row (transpose mat) diff --git a/Data/Vector/Bisemimodule.agda b/Data/Vector/Bisemimodule.agda index d895459..e38536a 100644 --- a/Data/Vector/Bisemimodule.agda +++ b/Data/Vector/Bisemimodule.agda @@ -136,19 +136,19 @@ opaque unfolding _∙_ ⟨ε⟩ - ∙-identityˡ : (V : Vector n) → ⟨ε⟩ ∙ V ≈ 0# - ∙-identityˡ [] = refl - ∙-identityˡ (x ∷ V) = begin + ∙-zeroˡ : (V : Vector n) → ⟨ε⟩ ∙ V ≈ 0# + ∙-zeroˡ [] = refl + ∙-zeroˡ (x ∷ V) = begin 0# * x + ⟨ε⟩ ∙ V ≈⟨ +-congʳ (zeroˡ x) ⟩ - 0# + ⟨ε⟩ ∙ V ≈⟨ +-congˡ (∙-identityˡ V) ⟩ + 0# + ⟨ε⟩ ∙ V ≈⟨ +-congˡ (∙-zeroˡ V) ⟩ 0# + 0# ≈⟨ +-identityˡ 0# ⟩ 0# ∎ - ∙-identityʳ : (V : Vector n) → V ∙ ⟨ε⟩ ≈ 0# - ∙-identityʳ [] = refl - ∙-identityʳ (x ∷ V) = begin + ∙-zeroʳ : (V : Vector n) → V ∙ ⟨ε⟩ ≈ 0# + ∙-zeroʳ [] = refl + ∙-zeroʳ (x ∷ V) = begin x * 0# + V ∙ ⟨ε⟩ ≈⟨ +-congʳ (zeroʳ x) ⟩ - 0# + V ∙ ⟨ε⟩ ≈⟨ +-congˡ (∙-identityʳ V) ⟩ + 0# + V ∙ ⟨ε⟩ ≈⟨ +-congˡ (∙-zeroʳ V) ⟩ 0# + 0# ≈⟨ +-identityˡ 0# ⟩ 0# ∎ diff --git a/Data/Vector/Core.agda b/Data/Vector/Core.agda index 974f672..a430f12 100644 --- a/Data/Vector/Core.agda +++ b/Data/Vector/Core.agda @@ -13,18 +13,18 @@ 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.Nat using (ℕ; _+_) open import Data.Setoid using (∣_∣) -open import Data.Vec using (Vec; lookup; tabulate) +open import Data.Vec as Vec using (Vec; lookup; tabulate) 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 Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_) -open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) open Func open Setoid S -open Vec open Fin +open Vec.Vec private variable @@ -44,6 +44,18 @@ opaque ≊-isEquiv : IsEquivalence (_≊_ {n}) ≊-isEquiv {n} = ≋-isEquivalence n + _++_ : Vector A → Vector B → Vector (A + B) + _++_ = Vec._++_ + + ⟨⟩ : Vector 0 + ⟨⟩ = [] + + ⟨⟩-! : (V : Vector 0) → V ≡ ⟨⟩ + ⟨⟩-! [] = ≡.refl + + ⟨⟩-++ : (V : Vector A) → ⟨⟩ ++ V ≡ V + ⟨⟩-++ V = ≡.refl + -- A setoid of vectors for every natural number Vectorₛ : ℕ → Setoid c (c ⊔ ℓ) Vectorₛ n = record diff --git a/Data/Vector/Vec.agda b/Data/Vector/Vec.agda index ae87737..868571a 100644 --- a/Data/Vector/Vec.agda +++ b/Data/Vector/Vec.agda @@ -3,8 +3,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) +open import Data.Nat using (ℕ; _+_) +open import Data.Vec using (Vec; tabulate; zipWith; replicate; map; _++_) open import Function using (_∘_) open import Level using (Level) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) @@ -13,10 +13,18 @@ open Vec open ℕ open Fin +private + variable + a b c d e : Level + A : Set a + B : Set b + C : Set c + D : Set d + E : Set e + n : ℕ + zipWith-tabulate - : {a : Level} - {A : Set a} - {n : ℕ} + : {n : ℕ} (_⊕_ : A → A → A) (f g : Fin n → A) → zipWith _⊕_ (tabulate f) (tabulate g) ≡ tabulate (λ i → f i ⊕ g i) @@ -24,10 +32,42 @@ zipWith-tabulate {n = zero} _⊕_ f g = ≡.refl zipWith-tabulate {n = suc n} _⊕_ f g = ≡.cong (f zero ⊕ g zero ∷_) (zipWith-tabulate _⊕_ (f ∘ suc) (g ∘ suc)) replicate-tabulate - : {a : Level} - {A : Set a} - {n : ℕ} + : {n : ℕ} (x : A) → replicate n x ≡ tabulate (λ _ → x) replicate-tabulate {n = zero} x = ≡.refl replicate-tabulate {n = suc n} x = ≡.cong (x ∷_) (replicate-tabulate x) + +zipWith-map + : {n : ℕ} + (f : A → B) + (g : A → C) + (_⊕_ : B → C → D) + (v : Vec A n) + → zipWith _⊕_ (map f v) (map g v) ≡ map (λ x → f x ⊕ g x) v +zipWith-map f g _⊕_ [] = ≡.refl +zipWith-map f g _⊕_ (x ∷ v) = ≡.cong (f x ⊕ g x ∷_) (zipWith-map f g _⊕_ v) + +replicate-++ : (n m : ℕ) (x : A) → replicate n x ++ replicate m x ≡ replicate (n + m) x +replicate-++ zero _ x = ≡.refl +replicate-++ (suc n) m x = ≡.cong (x ∷_) (replicate-++ n m x) + +map-zipWith + : (f : C → D) + (_⊕_ : A → B → C) + {n : ℕ} + (v : Vec A n) + (w : Vec B n) + → map f (zipWith _⊕_ v w) ≡ zipWith (λ x y → f (x ⊕ y)) v w +map-zipWith f _⊕_ [] [] = ≡.refl +map-zipWith f _⊕_ (x ∷ v) (y ∷ w) = ≡.cong (f (x ⊕ y) ∷_) (map-zipWith f _⊕_ v w) + +zipWith-map-map + : (f : A → C) + (g : B → D) + (_⊕_ : C → D → E) + (v : Vec A n) + (w : Vec B n) + → 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) |