diff options
Diffstat (limited to 'Data/Matrix')
| -rw-r--r-- | Data/Matrix/Dagger-2-Poset.agda | 33 | ||||
| -rw-r--r-- | Data/Matrix/Functional.agda | 5 |
2 files changed, 25 insertions, 13 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 |