Begin separating vector concepts from matrices

1 files changed, 33 insertions, 0 deletions

diff --git a/Data/Vector/Vec.agda b/Data/Vector/Vec.agda
new file mode 100644
index 0000000..ae87737
--- /dev/null
+++ b/Data/Vector/Vec.agda
@@ -0,0 +1,33 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Vector.Vec where
+
+open import Data.Fin using (Fin)
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec; tabulate; zipWith; replicate)
+open import Function using (_∘_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+open Vec
+open ℕ
+open Fin
+
+zipWith-tabulate
+    : {a : Level}
+      {A : Set a}
+      {n : ℕ}
+      (_⊕_ : A → A → A)
+      (f g : Fin n → A)
+    → 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))
+
+replicate-tabulate
+    : {a : Level}
+      {A : Set a}
+      {n : ℕ}
+      (x : A)
+    → replicate n x ≡ tabulate (λ _ → x)
+replicate-tabulate {n = zero} x = ≡.refl
+replicate-tabulate {n = suc n} x = ≡.cong (x ∷_) (replicate-tabulate x)