diff options
| -rw-r--r-- | Data/Mat/Category.agda | 434 | ||||
| -rw-r--r-- | Data/Mat/Util.agda | 130 |
2 files changed, 564 insertions, 0 deletions
diff --git a/Data/Mat/Category.agda b/Data/Mat/Category.agda new file mode 100644 index 0000000..2407d28 --- /dev/null +++ b/Data/Mat/Category.agda @@ -0,0 +1,434 @@ +{-# 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/Util.agda b/Data/Mat/Util.agda new file mode 100644 index 0000000..b7aedd2 --- /dev/null +++ b/Data/Mat/Util.agda @@ -0,0 +1,130 @@ +{-# 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 : ℕ) → transpose (replicate {A = Vec A zero} m []) ≡ [] +transpose-empty zero = ≡.refl +transpose-empty (suc m) = ≡.cong (zipWith _∷_ []) (transpose-empty m) + +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 +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) + +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₂) |