diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-22 14:52:16 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-22 14:52:16 -0500 |
| commit | f7091746dcae0aacd0fc8c8971d6dc5a748e7bc5 (patch) | |
| tree | 9966acfbd9584af65d1f20f99e051bdc94ecd63b /Data/Matrix/Convert.agda | |
| parent | 9a65579633967a0c02b912e6baa3e575a02b868f (diff) | |
Add more matrix operations
Diffstat (limited to 'Data/Matrix/Convert.agda')
| -rw-r--r-- | Data/Matrix/Convert.agda | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/Data/Matrix/Convert.agda b/Data/Matrix/Convert.agda index 8b140c0..1f577f0 100644 --- a/Data/Matrix/Convert.agda +++ b/Data/Matrix/Convert.agda @@ -16,7 +16,7 @@ open import Data.Matrix.Category R using (_·_) open import Data.Matrix.Core setoid using (_≋_) renaming (Matrix to Mat) open import Data.Matrix.Functional R as Functional using (Matrix; identity) open import Data.Matrix.Monoid +-monoid using (_[+]_) -open import Data.Matrix.Raw using (_∷ₕ_; _∷ᵥ_; _ᵀ) +open import Data.Matrix.Raw as Raw using (_∷ₕ_; _∷ᵥ_; _ᵀ) open import Data.Matrix.Transform R using (I; [_]_) open import Data.Nat using (ℕ) open import Data.Vec.Functional using (Vector; head; tail) @@ -33,7 +33,7 @@ open ≡-Reasoning opaque - unfolding Mat + unfolding Raw.Matrix tabulate : {n m : ℕ} → Matrix n m → Mat n m tabulate M = Vec.tabulate (λ j → Vec.tabulate (λ i → M i j)) @@ -65,14 +65,12 @@ opaque Vec.replicate n 0# ∷ₕ (tabulate (λ i j → identity i j)) ≡⟨ ≡.cong₂ _∷ₕ_ ≡.refl tabulate-I ⟩ ⟨ε⟩ ∷ₕ I ∎ - opaque - unfolding _ᵀ - tabulate-flip : {n m : ℕ} (M : Matrix n m) → tabulate (flip M) ≡ tabulate M ᵀ - tabulate-flip {n} {zero} M = ≡.sym (replicate-tabulate []) - tabulate-flip {n} {suc m} M = begin - Vec.tabulate (λ j → head (M j) ∷ Vec.tabulate (λ x → M j (Fin.suc x))) ≡⟨ zipWith-tabulate _∷_ (λ j → M j Fin.zero) _ ⟨ - Vec.tabulate (λ i → head (M i)) ∷ₕ (tabulate (λ j i → M i (Fin.suc j))) ≡⟨ ≡.cong (Vec.tabulate (λ i → head (M i)) ∷ₕ_) (tabulate-flip (λ i → tail (M i))) ⟩ - Vec.tabulate (λ i → head (M i)) ∷ₕ (tabulate (λ i j → M i (Fin.suc j))) ᵀ ∎ + tabulate-flip : {n m : ℕ} (M : Matrix n m) → tabulate (flip M) ≡ tabulate M ᵀ + tabulate-flip {n} {zero} M = ≡.sym (replicate-tabulate []) + tabulate-flip {n} {suc m} M = begin + Vec.tabulate (λ j → head (M j) ∷ Vec.tabulate (λ x → M j (Fin.suc x))) ≡⟨ zipWith-tabulate _∷_ (λ j → M j Fin.zero) _ ⟨ + Vec.tabulate (λ i → head (M i)) ∷ₕ (tabulate (λ j i → M i (Fin.suc j))) ≡⟨ ≡.cong (Vec.tabulate (λ i → head (M i)) ∷ₕ_) (tabulate-flip (λ i → tail (M i))) ⟩ + Vec.tabulate (λ i → head (M i)) ∷ₕ (tabulate (λ i j → M i (Fin.suc j))) ᵀ ∎ opaque unfolding _∙_ |