Include missing properties

3 files changed, 28 insertions, 15 deletions

diff --git a/Data/Matrix/Dagger-2-Poset.agda b/Data/Matrix/Dagger-2-Poset.agda
index 0cda1ee..400be2e 100644
--- a/Data/Matrix/Dagger-2-Poset.agda
+++ b/Data/Matrix/Dagger-2-Poset.agda
@@ -45,21 +45,28 @@ opaque
   [+]-idem [] = PW.[]
   [+]-idem (M₀ ∷ M) = ⊕-idem M₀ PW.∷ [+]-idem M
 
++-[+] : (M N : Matrix A B) → (I ∥ I) · (((I ≑ 𝟎) · M) ∥ ((𝟎 ≑ I) · N)) · (I ∥ I) ᵀ ≋ M [+] N
++-[+] M N = begin
+    (I ∥ I) · (((I ≑ 𝟎) · M) ∥ ((𝟎 ≑ I) · N)) · (I ∥ I) ᵀ     ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · (h₁ ∥ h₂) · (I ∥ I) ᵀ) (≑-· I 𝟎 M) (≑-· 𝟎 I N) ⟩
+    (I ∥ I) · ((I · M ≑ 𝟎 · M) ∥ (𝟎 · N ≑ I · N)) · (I ∥ I) ᵀ ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ (∥-cong (≑-cong ·-Iˡ (·-𝟎ˡ M)) (≑-cong (·-𝟎ˡ N) ·-Iˡ)) ≋.refl) ⟩
+    (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ N)) · (I ∥ I) ᵀ                 ≡⟨ ≡.cong (λ h → (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ N)) · h) (∥-ᵀ I I) ⟩
+    (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ N)) · (I ᵀ ≑ I ᵀ)               ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ N)) · (h₁ ≑ h₂)) Iᵀ Iᵀ ⟩
+    (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ N)) · (I ≑ I)                   ≈⟨ ·-assoc ⟨
+    ((I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ N))) · (I ≑ I)                 ≡⟨ ≡.cong (_· (I ≑ I)) (·-∥ (I ∥ I) (M ≑ 𝟎) (𝟎 ≑ N)) ⟩
+    (((I ∥ I) · (M ≑ 𝟎)) ∥ ((I ∥ I) · (𝟎 ≑ N))) · (I ≑ I)     ≈⟨ ∥-·-≑ ((I ∥ I) · (M ≑ 𝟎)) ((I ∥ I) · (𝟎 ≑ N)) I I ⟩
+    (((I ∥ I) · (M ≑ 𝟎)) · I) [+] (((I ∥ I) · (𝟎 ≑ N)) · I)   ≈⟨ [+]-cong ·-Iʳ ·-Iʳ ⟩
+    ((I ∥ I) · (M ≑ 𝟎)) [+] ((I ∥ I) · (𝟎 ≑ N))               ≈⟨ [+]-cong (∥-·-≑ I I M 𝟎) (∥-·-≑ I I 𝟎 N) ⟩
+    ((I · M) [+] (I · 𝟎)) [+] ((I · 𝟎) [+] (I · N))           ≈⟨ [+]-cong ([+]-cong ·-Iˡ ·-Iˡ) ([+]-cong ·-Iˡ ·-Iˡ) ⟩
+    (M [+] 𝟎) [+] (𝟎 [+] N)                                   ≈⟨ [+]-cong ([+]-𝟎ʳ M) ([+]-𝟎ˡ N) ⟩
+    M [+] N                                                   ∎
+  where
+    open ≈-Reasoning (Matrixₛ _ _)
+
 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 ∎
+    (I ∥ I) · (((I ≑ 𝟎) · M) ∥ ((𝟎 ≑ I) · M)) · (I ∥ I) ᵀ ≈⟨ +-[+] M M ⟩
+    M [+] M                                               ≈⟨ [+]-idem M ⟩
+    M                                                     ∎
   where
     open ≈-Reasoning (Matrixₛ _ _)
 
diff --git a/Data/Matrix/Functional.agda b/Data/Matrix/Functional.agda
index 2f9a85d..bbfd53c 100644
--- a/Data/Matrix/Functional.agda
+++ b/Data/Matrix/Functional.agda
@@ -10,6 +10,7 @@ open import Data.Fin using (Fin; _≟_)
 open import Data.Nat using (ℕ)
 open import Data.Vec.Functional using (Vector; head; tail)
 open import Function using (flip)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 open import Relation.Nullary.Decidable using (⌊_⌋)
 
 open Semiring R
@@ -22,6 +23,10 @@ sum : {n : ℕ} → Vector Carrier n → Carrier
 sum {zero} _ = 0#
 sum {suc n} v = head v + sum (tail v)
 
+sum-cong : {n : ℕ} {V W : Vector Carrier n} → V ≗ W → sum V ≡ sum W
+sum-cong {zero} V≗W = ≡.refl
+sum-cong {suc n} {V} {W} V≗W = ≡.cong₂ _+_ (V≗W Fin.zero) (sum-cong (λ i → V≗W (Fin.suc i)))
+
 _⟨*⟩_ : {n : ℕ} → Vector Carrier n → Vector Carrier n → Vector Carrier n
 _⟨*⟩_ v w i = v i * w i
 
diff --git a/Data/Vector/Vec.agda b/Data/Vector/Vec.agda
index 4367bdd..74ab0cc 100644
--- a/Data/Vector/Vec.agda
+++ b/Data/Vector/Vec.agda
@@ -27,8 +27,9 @@ private
 
 zipWith-tabulate
     : {n : ℕ}
-      (_⊕_ : A → A → A)
-      (f g : Fin n → A)
+      (_⊕_ : A → B → C)
+      (f : Fin n → A)
+      (g : Fin n → B)
     → zipWith _⊕_ (tabulate f) (tabulate g) ≡ tabulate (λ i → f i ⊕ g i)
 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))