From 71cdd278bb008bb4375e8d5b2b6b00e3d5bf393a Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 28 Mar 2026 22:23:16 -0500 Subject: Begin separating vector concepts from matrices --- Data/Vector/CommutativeMonoid.agda | 40 +++++++++ Data/Vector/Core.agda | 94 ++++++++++++++++++++ Data/Vector/Monoid.agda | 175 +++++++++++++++++++++++++++++++++++++ Data/Vector/Vec.agda | 33 +++++++ 4 files changed, 342 insertions(+) create mode 100644 Data/Vector/CommutativeMonoid.agda create mode 100644 Data/Vector/Core.agda create mode 100644 Data/Vector/Monoid.agda create mode 100644 Data/Vector/Vec.agda diff --git a/Data/Vector/CommutativeMonoid.agda b/Data/Vector/CommutativeMonoid.agda new file mode 100644 index 0000000..c7b4a73 --- /dev/null +++ b/Data/Vector/CommutativeMonoid.agda @@ -0,0 +1,40 @@ +{-# OPTIONS --without-K --safe #-} + +open import Algebra using (Monoid; CommutativeMonoid) +open import Level using (Level; _⊔_) + +module Data.Vector.CommutativeMonoid {c ℓ : Level} (CM : CommutativeMonoid c ℓ) where + +module CM = CommutativeMonoid CM + +import Data.Vec.Relation.Binary.Pointwise.Inductive as PW + +open import Data.Vector.Core CM.setoid using (Vector; _≊_; module ≊) +open import Data.Vector.Monoid CM.monoid as M using (_⊕_) +open import Data.Nat using (ℕ) +open import Data.Vec using (Vec) + +open CM +open Vec + +private + variable + n : ℕ + +opaque + + unfolding _⊕_ + + ⊕-comm : (V W : Vector n) → V ⊕ W ≊ W ⊕ V + ⊕-comm [] [] = ≊.refl + ⊕-comm (v ∷ V) (w ∷ W) = comm v w PW.∷ ⊕-comm V W + +-- A commutative monoid of vectors for each natural number +Vectorₘ : ℕ → CommutativeMonoid c (c ⊔ ℓ) +Vectorₘ n = record + { Monoid (M.Vectorₘ n) + ; isCommutativeMonoid = record + { Monoid (M.Vectorₘ n) + ; comm = ⊕-comm + } + } diff --git a/Data/Vector/Core.agda b/Data/Vector/Core.agda new file mode 100644 index 0000000..974f672 --- /dev/null +++ b/Data/Vector/Core.agda @@ -0,0 +1,94 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --hidden-argument-puns #-} + +open import Level using (Level; _⊔_) +open import Relation.Binary using (Setoid; Rel; IsEquivalence) + +module Data.Vector.Core {c ℓ : Level} (S : Setoid c ℓ) where + +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Data.Vec.Relation.Binary.Pointwise.Inductive as PW + +open import Categories.Category.Instance.Nat using (Natop) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.Fin using (Fin) +open import Data.Nat using (ℕ) +open import Data.Setoid using (∣_∣) +open import Data.Vec using (Vec; lookup; tabulate) +open import Data.Vec.Properties using (tabulate∘lookup; lookup∘tabulate; tabulate-cong) +open import Data.Vec.Relation.Binary.Equality.Setoid S using (_≋_; ≋-isEquivalence) +open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) + +open Func +open Setoid S +open Vec +open Fin + +private + variable + n A B C : ℕ + +opaque + + -- Vectors over the rig + Vector : ℕ → Set c + Vector = Vec ∣ S ∣ + + -- Pointwise equivalence of vectors + _≊_ : Rel (Vector n) (c ⊔ ℓ) + _≊_ A B = A ≋ B + + -- Pointwise equivalence is an equivalence relation + ≊-isEquiv : IsEquivalence (_≊_ {n}) + ≊-isEquiv {n} = ≋-isEquivalence n + +-- A setoid of vectors for every natural number +Vectorₛ : ℕ → Setoid c (c ⊔ ℓ) +Vectorₛ n = record + { Carrier = Vector n + ; _≈_ = _≊_ + ; isEquivalence = ≊-isEquiv + } + +module ≊ {n} = Setoid (Vectorₛ n) + +infix 4 _≊_ + +opaque + + unfolding Vector + + pull : (Fin B → Fin A) → Vectorₛ A ⟶ₛ Vectorₛ B + pull f .to v = tabulate (λ i → lookup v (f i)) + pull f .cong ≊v = PW.tabulate⁺ (λ i → PW.lookup ≊v (f i)) + + pull-id : {v : Vector n} → pull id ⟨$⟩ v ≊ v + pull-id {v} = ≊.reflexive (tabulate∘lookup v) + + pull-∘ + : {f : Fin B → Fin A} + {g : Fin C → Fin B} + {v : Vector A} + → pull (f ∘ g) ⟨$⟩ v ≊ pull g ⟨$⟩ (pull f ⟨$⟩ v) + pull-∘ {f} {g} {v} = ≊.reflexive (≡.sym (tabulate-cong (λ i → lookup∘tabulate (lookup v ∘ f) (g i)))) + + pull-cong + : {f g : Fin B → Fin A} + → f ≗ g + → {v : Vector A} + → pull f ⟨$⟩ v ≊ pull g ⟨$⟩ v + pull-cong f≗g {v} = ≊.reflexive (tabulate-cong (λ i → ≡.cong (lookup v) (f≗g i))) + +-- Copying, deleting, and rearranging elements +-- of a vector according to a function on indices +-- gives a contravariant functor from Nat to Setoids +Pull : Functor Natop (Setoids c (c ⊔ ℓ)) +Pull = record + { F₀ = Vectorₛ + ; F₁ = pull + ; identity = pull-id + ; homomorphism = pull-∘ + ; F-resp-≈ = pull-cong + } diff --git a/Data/Vector/Monoid.agda b/Data/Vector/Monoid.agda new file mode 100644 index 0000000..5906bf9 --- /dev/null +++ b/Data/Vector/Monoid.agda @@ -0,0 +1,175 @@ +{-# OPTIONS --without-K --safe #-} + +open import Algebra using (Monoid) +open import Level using (Level; _⊔_) + +module Data.Vector.Monoid {c ℓ : Level} (M : Monoid c ℓ) where + +module M = Monoid M + +import Data.Vec.Relation.Binary.Pointwise.Inductive as PW +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Data.Nat using (ℕ) +open import Data.Product using (_,_) +open import Data.Vec using (Vec; foldr′; zipWith; replicate) +open import Data.Vector.Core M.setoid as S using (Vector; _≊_; module ≊; pull; Vectorₛ) + +open M +open Vec + +private + variable + n A B C : ℕ + +opaque + + unfolding Vector + + -- Sum the elements of a vector + sum : Vector n → M.Carrier + sum = foldr′ _∙_ ε + + sum-cong : {V V′ : Vector n} → V ≊ V′ → sum V ≈ sum V′ + sum-cong PW.[] = refl + sum-cong (≈x PW.∷ ≊V) = ∙-cong ≈x (sum-cong ≊V) + +opaque + + unfolding Vector + + -- Pointwise sum of two vectors + _⊕_ : Vector n → Vector n → Vector n + _⊕_ = zipWith _∙_ + + ⊕-cong : {V₁ V₂ W₁ W₂ : Vector n} → V₁ ≊ V₂ → W₁ ≊ W₂ → V₁ ⊕ W₁ ≊ V₂ ⊕ W₂ + ⊕-cong PW.[] PW.[] = PW.[] + ⊕-cong (≈v PW.∷ ≊V) (≈w PW.∷ ≊W) = ∙-cong ≈v ≈w PW.∷ ⊕-cong ≊V ≊W + + ⊕-assoc : (x y z : Vector n) → x ⊕ y ⊕ z ≊ x ⊕ (y ⊕ z) + ⊕-assoc [] [] [] = PW.[] + ⊕-assoc (x₀ ∷ x) (y₀ ∷ y) (z₀ ∷ z) = assoc x₀ y₀ z₀ PW.∷ ⊕-assoc x y z + +infixl 6 _⊕_ + +opaque + + unfolding Vector + + -- The identity vector + ⟨ε⟩ : Vector n + ⟨ε⟩ {n} = replicate n ε + +opaque + + unfolding _⊕_ ⟨ε⟩ + + ⊕-identityˡ : (V : Vector n) → ⟨ε⟩ ⊕ V ≊ V + ⊕-identityˡ [] = PW.[] + ⊕-identityˡ (x ∷ V) = identityˡ x PW.∷ ⊕-identityˡ V + + ⊕-identityʳ : (V : Vector n) → V ⊕ ⟨ε⟩ ≊ V + ⊕-identityʳ [] = PW.[] + ⊕-identityʳ (x ∷ V) = identityʳ x PW.∷ ⊕-identityʳ V + +-- A monoid of vectors for each natural number +Vectorₘ : ℕ → Monoid c (c ⊔ ℓ) +Vectorₘ n = record + { Carrier = Vector n + ; _≈_ = _≊_ + ; _∙_ = _⊕_ + ; ε = ⟨ε⟩ + ; isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = ≊.isEquivalence + ; ∙-cong = ⊕-cong + } + ; assoc = ⊕-assoc + } + ; identity = ⊕-identityˡ , ⊕-identityʳ + } + } + +open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×; ×-monoidal′) + +open import Categories.Category.Construction.Monoids Setoids-×.monoidal using (Monoids) +open import Categories.Category.Instance.Nat using (Natop) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Categories.Object.Monoid Setoids-×.monoidal as Obj using (Monoid⇒) +open import Data.Fin using (Fin) +open import Data.Monoid using (module FromMonoid) +open import Data.Monoid {c} {c ⊔ ℓ} using (fromMonoid) +open import Data.Vec using (tabulate; lookup) +open import Data.Vec.Properties using (tabulate-cong; lookup-zipWith; lookup-replicate) +open import Data.Vector.Vec using (zipWith-tabulate; replicate-tabulate) +open import Function using (Func; _⟨$⟩_; _∘_; id) +open import Relation.Binary.PropositionalEquality as ≡ using (module ≡-Reasoning; _≡_; _≗_) + +open Functor +open Monoid⇒ + +Vector′ : ℕ → Obj.Monoid +Vector′ n = fromMonoid (Vectorₘ n) + +open ℕ +open Fin +open ≡-Reasoning + +opaque + + unfolding pull _⊕_ + + pull-⊕ : {f : Fin A → Fin B} (V W : Vector B) → pull f ⟨$⟩ (V ⊕ W) ≡ (pull f ⟨$⟩ V) ⊕ (pull f ⟨$⟩ W) + pull-⊕ {A} {B} {f} V W = begin + tabulate (λ i → lookup (zipWith _∙_ V W) (f i)) + ≡⟨ tabulate-cong (λ i → lookup-zipWith _∙_ (f i) V W) ⟩ + tabulate (λ i → lookup V (f i) ∙ lookup W (f i)) + ≡⟨ zipWith-tabulate _∙_ (lookup V ∘ f) (lookup W ∘ f) ⟨ + zipWith _∙_ (tabulate (lookup V ∘ f)) (tabulate (lookup W ∘ f)) + ∎ + +opaque + + unfolding pull ⟨ε⟩ + + pull-⟨ε⟩ : {f : Fin A → Fin B} → pull f ⟨$⟩ ⟨ε⟩ ≡ ⟨ε⟩ + pull-⟨ε⟩ {f = f} = begin + tabulate (λ i → lookup (replicate _ ε) (f i)) ≡⟨ tabulate-cong (λ i → lookup-replicate (f i) ε) ⟩ + tabulate (λ _ → ε) ≡⟨ replicate-tabulate ε ⟨ + replicate _ ε ∎ + +opaque + + unfolding FromMonoid.μ + + pullₘ : (Fin A → Fin B) → Monoid⇒ (Vector′ B) (Vector′ A) + pullₘ f .arr = S.pull f + pullₘ f .preserves-μ {V , W} = ≊.reflexive (pull-⊕ V W) + pullₘ f .preserves-η = ≊.reflexive pull-⟨ε⟩ + + pullₘ-id : {V : Vector n} → arr (pullₘ id) ⟨$⟩ V ≊ V + pullₘ-id = S.pull-id + + pullₘ-∘ + : {f : Fin B → Fin A} + {g : Fin C → Fin B} + {v : Vector A} + → arr (pullₘ (f ∘ g)) ⟨$⟩ v ≊ arr (pullₘ g) ⟨$⟩ (arr (pullₘ f) ⟨$⟩ v) + pullₘ-∘ = S.pull-∘ + + pullₘ-cong + : {f g : Fin B → Fin A} + → f ≗ g + → {v : Vector A} + → arr (pullₘ f) ⟨$⟩ v ≊ arr (pullₘ g) ⟨$⟩ v + pullₘ-cong = S.pull-cong + +-- Contravariant functor from Nat to Monoids +Pullₘ : Functor Natop Monoids +Pullₘ .F₀ = Vector′ +Pullₘ .F₁ = pullₘ +Pullₘ .identity = pullₘ-id +Pullₘ .homomorphism = pullₘ-∘ +Pullₘ .F-resp-≈ = pullₘ-cong 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) -- cgit v1.2.3