diff options
Diffstat (limited to 'Data/Vector/Core.agda')
| -rw-r--r-- | Data/Vector/Core.agda | 129 |
1 files changed, 66 insertions, 63 deletions
diff --git a/Data/Vector/Core.agda b/Data/Vector/Core.agda index a430f12..c002676 100644 --- a/Data/Vector/Core.agda +++ b/Data/Vector/Core.agda @@ -6,101 +6,104 @@ 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 +open Setoid S + 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 as Vec using (Vec; lookup; tabulate) +open import Data.Nat using (ℕ) +open import Data.Vec using (Vec; lookup; tabulate; head; tail; map; _++_; replicate; zipWith) 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 Data.Vector.Raw using (module Relation) open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) open Func -open Setoid S -open Fin -open Vec.Vec +open ℕ + +Vector : ℕ → Set c +Vector = Vec Carrier private variable - n A B C : ℕ - -opaque - - -- Vectors over the rig - Vector : ℕ → Set c - Vector = Vec ∣ S ∣ + n m A B C : ℕ - -- Pointwise equivalence of vectors - _≊_ : Rel (Vector n) (c ⊔ ℓ) - _≊_ A B = A ≋ B +-- 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 - - _++_ : Vector A → Vector B → Vector (A + B) - _++_ = Vec._++_ - - ⟨⟩ : Vector 0 - ⟨⟩ = [] - - ⟨⟩-! : (V : Vector 0) → V ≡ ⟨⟩ - ⟨⟩-! [] = ≡.refl +infix 4 _≊_ - ⟨⟩-++ : (V : Vector A) → ⟨⟩ ++ V ≡ V - ⟨⟩-++ V = ≡.refl +-- 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 + { 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 : (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-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-∘ + : {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))) +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 - } + { F₀ = Vectorₛ + ; F₁ = pull + ; identity = pull-id + ; homomorphism = λ {f = f} {g v} → pull-∘ {f = f} {g} {v} + ; F-resp-≈ = pull-cong + } + +module Cong where + + open Relation {R = _≈_} + + head-cong : {V₁ V₂ : Vector (suc n)} → V₁ ≊ V₂ → head V₁ ≈ head V₂ + head-cong = R-head + + tail-cong : {V₁ V₂ : Vector (suc n)} → V₁ ≊ V₂ → tail V₁ ≊ tail V₂ + tail-cong = R-tail + + ++-cong + : {V₁ V₂ : Vector m} + {W₁ W₂ : Vector n} + → V₁ ≊ V₂ + → W₁ ≊ W₂ + → V₁ ++ W₁ ≊ V₂ ++ W₂ + ++-cong = R-++ + + replicate-cong : {n : ℕ} {x y : Carrier} → x ≈ y → replicate n x ≋ replicate n y + replicate-cong = R-replicate + +open Cong public |