From b795c34f2b7451a6cfde086b1944cca49de02605 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 27 Mar 2026 16:09:59 -0500 Subject: Add dagger structure for commutative rig matrices --- Data/Mat/Cocartesian.agda | 71 +++++++++++++++++++++++++++++++++++------------ 1 file changed, 53 insertions(+), 18 deletions(-) (limited to 'Data/Mat/Cocartesian.agda') diff --git a/Data/Mat/Cocartesian.agda b/Data/Mat/Cocartesian.agda index 44e6d1c..5ea92b3 100644 --- a/Data/Mat/Cocartesian.agda +++ b/Data/Mat/Cocartesian.agda @@ -11,7 +11,7 @@ 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ʳ + ; _ᵀ; mapRows; _·_; _∙_; _ᵀᵀ; _⊕_; ·-identityʳ; ∙-zerosʳ; ∙-zerosˡ ) renaming ([_]_ to [_]′_) @@ -22,7 +22,7 @@ open import Data.Mat.Util using (replicate-++; zipWith-map; transpose-zipWith; z 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-id) +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) @@ -141,8 +141,8 @@ opaque opaque unfolding []ᵥ - []-ᵀ : []ᵥ ᵀ ≡ []ₕ {A} - []-ᵀ = []ₕ ᵀᵀ + []ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A} + []ᵥ-ᵀ = []ₕ ᵀᵀ opaque unfolding []ₕ @@ -228,7 +228,7 @@ opaque unfolding []ₕ [_]′_ _ᵀ []ᵥ ⟨⟩ [-]-[]ᵥ : (V : Vector A) → [ V ]′ []ᵥ ≡ ⟨⟩ [-]-[]ᵥ [] = ≡.refl - [-]-[]ᵥ (x ∷ V) = ≡.cong (map ((x ∷ V) ∙_)) []-ᵀ + [-]-[]ᵥ (x ∷ V) = ≡.cong (map ((x ∷ V) ∙_)) []ᵥ-ᵀ opaque unfolding [_]′_ _ᵀ _∷ᵥ_ _∷′_ @@ -242,7 +242,7 @@ opaque (M : Matrix A C) (N : Matrix B C) → [ V ]′ (M ∥ N) ≡ ([ V ]′ M) +++ ([ V ]′ N) -[-]--∥ {C} {zero} V M N rewrite ([]ᵥ-! M) = begin +[-]--∥ {C} {zero} V M N rewrite []ᵥ-! M = begin [ V ]′ ([]ᵥ ∥ N) ≡⟨ ≡.cong ([ V ]′_) ([]ᵥ-∥ N) ⟩ [ V ]′ N ≡⟨ ⟨⟩-+++ ([ V ]′ N) ⟨ ⟨⟩ +++ ([ V ]′ N) ≡⟨ ≡.cong (_+++ ([ V ]′ N)) ([-]-[]ᵥ V) ⟨ @@ -250,7 +250,7 @@ opaque where open ≡-Reasoning [-]--∥ {C} {suc A} V M N - rewrite (≡.sym (head-∷-tailₕ M)) + rewrite ≡.sym (head-∷-tailₕ M) using M₀ ← headₕ M using M ← tailₕ M = begin [ V ]′ ((M₀ ∷ₕ M) ∥ N) ≡⟨ ≡.cong ([ V ]′_) (∷ₕ-∥ M₀ M N) ⟨ @@ -263,7 +263,7 @@ opaque open ≡-Reasoning opaque - unfolding Matrix _∥_ mapRows _+++_ + unfolding _∥_ mapRows _+++_ ·-∥ : (M : Matrix C D) (N : Matrix A C) @@ -272,6 +272,15 @@ opaque ·-∥ {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 @@ -314,8 +323,8 @@ opaque → [ V +++ W ]′ (M ≑ N) ≊ [ V ]′ M ⊕ [ W ]′ N [+++]-≑ {B} {C} {zero} V W M N - rewrite ([]ᵥ-! M) - rewrite ([]ᵥ-! N) = begin + rewrite []ᵥ-! M + rewrite []ᵥ-! N = begin [ V +++ W ]′ ([]ᵥ {B} ≑ []ᵥ) ≡⟨ ≡.cong ([ V +++ W ]′_) []ᵥ-≑ ⟩ [ V +++ W ]′ []ᵥ ≡⟨ [-]-[]ᵥ (V +++ W) ⟩ ⟨⟩ ≡⟨ ⟨⟩-⊕ ⟨ @@ -324,8 +333,8 @@ opaque where open ≈-Reasoning (≊-setoid 0) [+++]-≑ {B} {C} {suc A} V W M N - rewrite (≡.sym (head-∷-tailₕ M)) - rewrite (≡.sym (head-∷-tailₕ N)) + rewrite ≡.sym (head-∷-tailₕ M) + rewrite ≡.sym (head-∷-tailₕ N) using M₀ ← headₕ M using M ← tailₕ M using N₀ ← headₕ N @@ -414,6 +423,26 @@ opaque 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 @@ -441,7 +470,7 @@ opaque 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′)) + rewrite ≡.sym (head-∷-tailₕ M′) using M₀ ← headₕ M′ using M ← tailₕ M′ with split-∥ A M @@ -498,8 +527,8 @@ 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 + rewrite []ᵥ-! M + rewrite []ᵥ-! M′ = begin ([]ᵥ ∥ N) ≡⟨ []ᵥ-∥ N ⟩ N ≈⟨ ≋N ⟩ N′ ≡⟨ []ᵥ-∥ N′ ⟨ @@ -507,10 +536,10 @@ opaque where open ≈-Reasoning (≋-setoid _ _) ∥-cong {suc A} {C} {B} {M} {M′} {N} {N′} ≋M ≋N - rewrite (≡.sym (head-∷-tailₕ M)) + rewrite ≡.sym (head-∷-tailₕ M) using M₀ ← headₕ M using M- ← tailₕ M - rewrite (≡.sym (head-∷-tailₕ M′)) + rewrite ≡.sym (head-∷-tailₕ M′) using M₀′ ← headₕ M′ using M-′ ← tailₕ M′ = begin (M₀ ∷ₕ M-) ∥ N ≡⟨ ∷ₕ-∥ M₀ M- N ⟨ @@ -536,6 +565,12 @@ opaque 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 @@ -547,7 +582,7 @@ opaque → 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 + 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₂) ∎ -- cgit v1.2.3