diff options
Diffstat (limited to 'Data/Vector')
| -rw-r--r-- | Data/Vector/Bifunctor.agda | 57 | ||||
| -rw-r--r-- | Data/Vector/Bisemimodule.agda | 2 | ||||
| -rw-r--r-- | Data/Vector/Core.agda | 129 | ||||
| -rw-r--r-- | Data/Vector/Endofunctor.agda | 68 | ||||
| -rw-r--r-- | Data/Vector/Endofunctor/Monoid.agda | 106 | ||||
| -rw-r--r-- | Data/Vector/Endofunctor/Setoid.agda | 81 | ||||
| -rw-r--r-- | Data/Vector/Monoid.agda | 12 | ||||
| -rw-r--r-- | Data/Vector/Raw.agda | 95 | ||||
| -rw-r--r-- | Data/Vector/Vec.agda | 15 |
9 files changed, 423 insertions, 142 deletions
diff --git a/Data/Vector/Bifunctor.agda b/Data/Vector/Bifunctor.agda new file mode 100644 index 0000000..51e8970 --- /dev/null +++ b/Data/Vector/Bifunctor.agda @@ -0,0 +1,57 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Data.Vector.Bifunctor {c : Level} where + +open import Categories.Category.Instance.Nat using (Natop) +open import Categories.Category.Instance.Sets using (Sets) +open import Categories.Functor.Bifunctor using (Bifunctor) +open import Function using (_∘_) +open import Data.Nat using (ℕ) +open import Data.Fin using (Fin) +open import Data.Product using (_,_) +open import Data.Vec using (Vec; map; tabulate; lookup) +open import Data.Vec.Properties using (map-id; map-∘; map-cong; tabulate∘lookup; lookup∘tabulate; tabulate-cong; lookup-map; tabulate-∘) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) + +naturality + : {A B : Set c} {f : A → B} {n m : ℕ} {g : Fin m → Fin n} (v : Vec A n) + → map f (tabulate (λ i → lookup v (g i))) ≡ tabulate (λ i → lookup (map f v) (g i)) +naturality {A} {B} {f} {n} {m} {g} v = begin + map f (tabulate (λ i → lookup v (g i))) ≡⟨ tabulate-∘ f (λ i → lookup v (g i)) ⟨ + tabulate (λ i → f (lookup v (g i))) ≡⟨ tabulate-cong (λ i → (lookup-map (g i) f v)) ⟨ + tabulate (λ i → lookup (map f v) (g i)) ∎ + where + open ≡-Reasoning + +bimap : {A B : Set c} {n m : ℕ} (f : A → B) (g : Fin m → Fin n) → Vec A n → Vec B m +bimap f g v = map f (tabulate (λ i → lookup v (g i))) + +Vec₂ : Bifunctor (Sets c) Natop (Sets c) +Vec₂ = record + { F₀ = λ (A , n) → Vec A n + ; F₁ = λ (f , g) v → bimap f g v + ; identity = λ v → ≡.trans (map-id (tabulate (λ i → lookup v i))) (tabulate∘lookup v) + ; homomorphism = λ {_ _ _} {(f , f′)} {(g , g′)} → homomorphism f g f′ g′ + ; F-resp-≈ = λ (f≗g , f′≗g′) v → ≡.trans (map-cong f≗g (tabulate (λ i → lookup v _))) (≡.cong (map _) (tabulate-cong (λ i → (≡.cong (lookup v) (f′≗g′ i))))) + } + where + homomorphism + : {X Y Z : Set c} + (f : X → Y) + (g : Y → Z) + {x y z : ℕ} + (f′ : Fin y → Fin x) + (g′ : Fin z → Fin y) + (v : Vec X x) + → bimap (g ∘ f) (f′ ∘ g′) v ≡ bimap g g′ (bimap f f′ v) + homomorphism f g f′ g′ v = begin + map (g ∘ f) (tabulate (λ i → lookup v (f′ (g′ i)))) ≡⟨ map-∘ g f (tabulate (λ i → lookup v (f′ (g′ i)))) ⟩ + map g (map f (tabulate (λ i → lookup v (f′ (g′ i))))) ≡⟨ ≡.cong (map g) (naturality v) ⟩ + map g (tabulate (λ i → lookup (map f v) (f′ (g′ i)))) ≡⟨ ≡.cong (map g) (tabulate-cong (λ i → (lookup∘tabulate (λ i₁ → lookup (map f v) (f′ i₁)) (g′ i)))) ⟨ + map g (tabulate (λ i → lookup (tabulate (λ i₁ → lookup (map f v) (f′ i₁))) (g′ i))) + ≡⟨ ≡.cong (map g) (tabulate-cong (λ i → ≡.cong (λ h → lookup h (g′ i)) (naturality v))) ⟨ + map g (tabulate (λ i → lookup (map f (tabulate (λ i₁ → lookup v (f′ i₁)))) (g′ i))) ∎ + where + open ≡-Reasoning diff --git a/Data/Vector/Bisemimodule.agda b/Data/Vector/Bisemimodule.agda index e38536a..4121b91 100644 --- a/Data/Vector/Bisemimodule.agda +++ b/Data/Vector/Bisemimodule.agda @@ -32,8 +32,6 @@ private opaque - unfolding Vector - -- Scaling a vector from the left _⟨_⟩ : Carrier → Vector n → Vector n _⟨_⟩ r = map (r *_) 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 diff --git a/Data/Vector/Endofunctor.agda b/Data/Vector/Endofunctor.agda deleted file mode 100644 index a9b2905..0000000 --- a/Data/Vector/Endofunctor.agda +++ /dev/null @@ -1,68 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Data.Nat using (ℕ) -open import Level using (Level; _⊔_) - --- The endofunctor in setoids sending A to Vector A n for a fixed n -module Data.Vector.Endofunctor (n : ℕ) {c ℓ : Level} where - -import Data.Vec as Vec - -open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Functor using (Functor) -open import Data.Vec.Properties using (map-id; map-∘) -open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺) -open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊) -open import Function using (Func; _⟶ₛ_; _⟨$⟩_) -open import Function.Construct.Composition using () renaming (function to compose) -open import Function.Construct.Identity using () renaming (function to Id) -open import Relation.Binary using (Setoid) - -open Func - -opaque - unfolding Vector - map : {c ℓ : Level} {A B : Setoid c ℓ} → A ⟶ₛ B → Vectorₛ A n ⟶ₛ Vectorₛ B n - map f .to = Vec.map (to f) - map f .cong = map⁺ (cong f) - -abstract opaque - - unfolding map - - identity - : {A : Setoid c ℓ} - {V : Vector A n} - (open Core A using (_≊_)) - → map (Id A) ⟨$⟩ V ≊ V - identity {A} {V} = ≊.reflexive A (map-id V) - - homomorphism - : {X Y Z : Setoid c ℓ} - {f : X ⟶ₛ Y} - {g : Y ⟶ₛ Z} - {V : Vector X n} - (open Core Z using (_≊_)) - → map (compose f g) ⟨$⟩ V ≊ map g ⟨$⟩ (map f ⟨$⟩ V) - homomorphism {_} {_} {Z} {f} {g} {V} = ≊.reflexive Z (map-∘ (to g) (to f) V) - - F-resp-≈ - : {A B : Setoid c ℓ} - {f g : A ⟶ₛ B} - → ({x : Setoid.Carrier A} → (B Setoid.≈ to f x) (to g x)) - → {V : Vector A n} - (open Core B using (_≊_)) - → map f ⟨$⟩ V ≊ map g ⟨$⟩ V - F-resp-≈ {A} {B} {_} {g} f≈g {V} = map⁺ (λ x≈y → B.trans f≈g (cong g x≈y)) (≊.refl A) - where - module B = Setoid B - --- only a true endofunctor when c ≤ ℓ -Vec : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) -Vec = record - { F₀ = λ A → Vectorₛ A n - ; F₁ = map - ; identity = identity - ; homomorphism = homomorphism - ; F-resp-≈ = F-resp-≈ - } diff --git a/Data/Vector/Endofunctor/Monoid.agda b/Data/Vector/Endofunctor/Monoid.agda new file mode 100644 index 0000000..217c754 --- /dev/null +++ b/Data/Vector/Endofunctor/Monoid.agda @@ -0,0 +1,106 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Nat using (ℕ) +open import Level using (Level; _⊔_) + +-- The endofunctor in monoids sending A to Vectorₘ A n for a fixed n +module Data.Vector.Endofunctor.Monoid (n : ℕ) {c ℓ : Level} where + +import Data.Vec as Vec +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Algebra using (Monoid) +open import Categories.Category using (Category; _[_∘_]; _[_≈_]) +open import Categories.Functor using (Functor) +open import Category.Instance.Monoids using (Monoids; MonoidHomomorphism; mk-⇒) +open import Data.Monoid using (toMonoid) +open import Data.Vec.Properties using (map-replicate) +open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺) +open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊; replicate-cong) +open import Data.Vector.Endofunctor.Setoid as Endo using (mapₛ; zipWith-cong) +open import Data.Vector.Monoid as Mon using (Vectorₘ; ⟨ε⟩) renaming (_⊕_ to _[_⊕_]) +open import Data.Vector.Vec using (map-zipWith; zipWith-map-map) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_) + +open Func +open MonoidHomomorphism + +private module _ {M N : Monoid c ℓ} (f : MonoidHomomorphism c ℓ M N) where + + private + module M = Monoid M + module N = Monoid N + + open Core N.setoid using (_≊_) + open ≈-Reasoning (Vectorₛ N.setoid n) + + opaque + unfolding _[_⊕_] + map-⊕ + : (W V : Vector M.setoid n) + → mapₛ n (func f) ⟨$⟩ (M [ W ⊕ V ]) + ≊ N [ mapₛ n (func f) ⟨$⟩ W ⊕ mapₛ n (func f) ⟨$⟩ V ] + map-⊕ W V = begin + Vec.map ⟦ f ⟧ (Vec.zipWith M._∙_ W V) ≡⟨ map-zipWith ⟦ f ⟧ M._∙_ W V ⟩ + Vec.zipWith (λ x y → ⟦ f ⟧ (x M.∙ y)) W V ≈⟨ zipWith-cong n N.setoid (homo f) W V ⟩ + Vec.zipWith (λ x y → ⟦ f ⟧ x N.∙ ⟦ f ⟧ y) W V ≡⟨ zipWith-map-map ⟦ f ⟧ ⟦ f ⟧ N._∙_ W V ⟩ + Vec.zipWith N._∙_ (Vec.map ⟦ f ⟧ W) (Vec.map ⟦ f ⟧ V) ∎ + + opaque + unfolding ⟨ε⟩ + map-⟨ε⟩ : mapₛ n (func f) ⟨$⟩ (Mon.⟨ε⟩ M) ≊ Mon.⟨ε⟩ N + map-⟨ε⟩ = begin + Vec.map (to (func f)) (Vec.replicate n M.ε) ≡⟨ map-replicate (to (func f)) M.ε n ⟩ + Vec.replicate n (func f ⟨$⟩ M.ε) ≈⟨ replicate-cong N.setoid (ε-homo f) ⟩ + Vec.replicate n N.ε ∎ + +mapₘ : {M N : Monoid c ℓ} → MonoidHomomorphism c ℓ M N → MonoidHomomorphism c (c ⊔ ℓ) (Vectorₘ M n) (Vectorₘ N n) +mapₘ {M} {N} f = mk-⇒ record + { ⟦_⟧ = to (mapₛ n (func f)) + ; isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = map⁺ (⟦⟧-cong f) + } + ; homo = map-⊕ f + } + ; ε-homo = map-⟨ε⟩ f + } + } + +open Category using (id) + +abstract + + identity + : {A : Monoid c ℓ} + → Monoids c (c ⊔ ℓ) [ mapₘ (id (Monoids c ℓ) {A}) ≈ id (Monoids c (c ⊔ ℓ)) ] + identity {A} V = Endo.identity n {c} {ℓ} {Monoid.setoid A} + + homomorphism + : {X Y Z : Monoid c ℓ} + {f : MonoidHomomorphism c ℓ X Y} + {g : MonoidHomomorphism c ℓ Y Z} + → Monoids c (c ⊔ ℓ) [ mapₘ (Monoids c ℓ [ g ∘ f ]) ≈ Monoids c (c ⊔ ℓ) [ mapₘ g ∘ mapₘ f ] ] + homomorphism {X} {Y} {Z} {f} {g} V = Endo.homomorphism n {c} {ℓ} {setoid X} {setoid Y} {setoid Z} {func f} {func g} {V} + where + open Monoid using (setoid) + + F-resp-≈ + : {A B : Monoid c ℓ} + {f g : MonoidHomomorphism c ℓ A B} + → Monoids c ℓ [ f ≈ g ] + → Monoids c (c ⊔ ℓ) [ mapₘ f ≈ mapₘ g ] + F-resp-≈ {A} {B} {f} {g} f≈g V = Endo.F-resp-≈ n {c} {ℓ} {setoid A} {setoid B} {func f} {func g} (λ {x} → f≈g x) + where + open Monoid using (setoid) + +-- only a true endofunctor when c ≤ ℓ +Vec : Functor (Monoids c ℓ) (Monoids c (c ⊔ ℓ)) +Vec = record + { F₀ = λ M → Vectorₘ M n + ; F₁ = mapₘ + ; identity = λ {M} → identity {M} + ; homomorphism = λ {f = f} {g} → homomorphism {f = f} {g} + ; F-resp-≈ = λ {f = f} {g} → F-resp-≈ {f = f} {g} + } diff --git a/Data/Vector/Endofunctor/Setoid.agda b/Data/Vector/Endofunctor/Setoid.agda new file mode 100644 index 0000000..09f8f69 --- /dev/null +++ b/Data/Vector/Endofunctor/Setoid.agda @@ -0,0 +1,81 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Nat using (ℕ) +open import Level using (Level; _⊔_) + +-- The endofunctor in setoids sending A to Vector A n for a fixed n +module Data.Vector.Endofunctor.Setoid (n : ℕ) {c ℓ : Level} where + +import Data.Vec as Vec + +open import Categories.Category using (_[_≈_]) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.Setoid using (∣_∣) +open import Data.Vec.Properties using (map-id; map-∘) +open import Data.Vec.Relation.Binary.Equality.Setoid using () renaming (_≋_ to _[_≋_]) +open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW using (map⁺; Pointwise) +open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊) +open import Data.Vector.Raw using (R-zipWith) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_) +open import Function.Construct.Composition using () renaming (function to compose) +open import Function.Construct.Identity using () renaming (function to Id) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open Func +open ℕ +open Vec.Vec +open Pointwise + +mapₛ : {A B : Setoid c ℓ} → A ⟶ₛ B → Vectorₛ A n ⟶ₛ Vectorₛ B n +mapₛ f .to = Vec.map (to f) +mapₛ f .cong = map⁺ (cong f) + +abstract + + identity + : {A : Setoid c ℓ} + {V : Vector A n} + (open Core A using (_≊_)) + → mapₛ (Id A) ⟨$⟩ V ≊ V + identity {A} {V} = ≊.reflexive A (map-id V) + + homomorphism + : {X Y Z : Setoid c ℓ} + {f : X ⟶ₛ Y} + {g : Y ⟶ₛ Z} + {V : Vector X n} + (open Core Z using (_≊_)) + → mapₛ (compose f g) ⟨$⟩ V ≊ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ V) + homomorphism {_} {_} {Z} {f} {g} {V} = ≊.reflexive Z (map-∘ (to g) (to f) V) + + F-resp-≈ + : {A B : Setoid c ℓ} + {f g : A ⟶ₛ B} + → Setoids c ℓ [ f ≈ g ] + → Setoids c (c ⊔ ℓ) [ mapₛ f ≈ mapₛ g ] + F-resp-≈ {A} {B} {_} {g} f≈g {V} = map⁺ (λ x≈y → B.trans f≈g (cong g x≈y)) (≊.refl A) + where + module B = Setoid B + +-- only a true endofunctor when c ≤ ℓ +Vec : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) +Vec = record + { F₀ = λ A → Vectorₛ A n + ; F₁ = mapₛ + ; identity = λ {A} → identity {A} + ; homomorphism = λ {f = f} {g} → homomorphism {f = f} {g} + ; F-resp-≈ = λ {f = f} {g} → F-resp-≈ {f = f} {g} + } + +zipWith-cong + : {A B : Set c} + (C : Setoid c ℓ) + (let module C = Setoid C) + {f g : A → B → ∣ C ∣} + → (∀ x y → f x y C.≈ g x y) + → (xs : Vec.Vec A n) + (ys : Vec.Vec B n) + → C [ Vec.zipWith f xs ys ≋ Vec.zipWith g xs ys ] +zipWith-cong C f≈g xs ys = R-zipWith {R = _≡_} {S = _≡_} (λ { ≡.refl ≡.refl → f≈g _ _}) (PW.refl ≡.refl) (PW.refl ≡.refl) diff --git a/Data/Vector/Monoid.agda b/Data/Vector/Monoid.agda index 5906bf9..da09de9 100644 --- a/Data/Vector/Monoid.agda +++ b/Data/Vector/Monoid.agda @@ -24,8 +24,6 @@ private opaque - unfolding Vector - -- Sum the elements of a vector sum : Vector n → M.Carrier sum = foldr′ _∙_ ε @@ -36,8 +34,6 @@ opaque opaque - unfolding Vector - -- Pointwise sum of two vectors _⊕_ : Vector n → Vector n → Vector n _⊕_ = zipWith _∙_ @@ -54,8 +50,6 @@ infixl 6 _⊕_ opaque - unfolding Vector - -- The identity vector ⟨ε⟩ : Vector n ⟨ε⟩ {n} = replicate n ε @@ -119,7 +113,7 @@ open ≡-Reasoning opaque - unfolding pull _⊕_ + unfolding _⊕_ 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 @@ -132,7 +126,7 @@ opaque opaque - unfolding pull ⟨ε⟩ + unfolding ⟨ε⟩ pull-⟨ε⟩ : {f : Fin A → Fin B} → pull f ⟨$⟩ ⟨ε⟩ ≡ ⟨ε⟩ pull-⟨ε⟩ {f = f} = begin @@ -157,7 +151,7 @@ opaque {g : Fin C → Fin B} {v : Vector A} → arr (pullₘ (f ∘ g)) ⟨$⟩ v ≊ arr (pullₘ g) ⟨$⟩ (arr (pullₘ f) ⟨$⟩ v) - pullₘ-∘ = S.pull-∘ + pullₘ-∘ {f = f} {g} {v} = S.pull-∘ {f = f} {g} {v} pullₘ-cong : {f g : Fin B → Fin A} diff --git a/Data/Vector/Raw.agda b/Data/Vector/Raw.agda new file mode 100644 index 0000000..c333553 --- /dev/null +++ b/Data/Vector/Raw.agda @@ -0,0 +1,95 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Vector.Raw where + +open import Data.Nat using (ℕ; _+_) +open import Data.Vec using (Vec; head; tail; map; _++_; replicate; zipWith) +open import Data.Vec.Properties using (map-replicate) +open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise) +open import Level using (Level) +open import Relation.Binary using (REL) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +private + variable + n m : ℕ + a ℓ ℓ₁ ℓ₂ : Level + A B C D E F : Set a + +open ℕ +open Vec + +⟨⟩ : Vec A 0 +⟨⟩ = [] + +⟨⟩-! : (V : Vec A 0) → V ≡ ⟨⟩ +⟨⟩-! [] = ≡.refl + +⟨⟩-++ : {n : ℕ} (V : Vec A n) → ⟨⟩ ++ V ≡ V +⟨⟩-++ V = ≡.refl + +module Natural {n : ℕ} (f : A → B) where + + α-head : (V : Vec A (suc n)) → f (head V) ≡ head (map f V) + α-head (x ∷ _) = ≡.erefl (f x) + + α-tail : (V : Vec A (suc n)) → map f (tail V) ≡ tail (map f V) + α-tail (_ ∷ V) = ≡.erefl (map f V) + + α-replicate : {x : A} → map f (replicate n x) ≡ replicate n (f x) + α-replicate {x} = map-replicate f x n + +open Natural public + +open Pointwise + +module Relation {R : REL A B ℓ} where + + R-head + : {V₁ : Vec A (suc n)} + {V₂ : Vec B (suc n)} + → Pointwise R V₁ V₂ + → R (head V₁) (head V₂) + R-head (R-x ∷ _) = R-x + + R-tail + : {V₁ : Vec A (suc n)} + {V₂ : Vec B (suc n)} + → Pointwise R V₁ V₂ + → Pointwise R (tail V₁) (tail V₂) + R-tail (_ ∷ R-V) = R-V + + R-++ + : {R : REL A B ℓ} + {V₁ : Vec A m} + {V₂ : Vec B m} + {W₁ : Vec A n} + {W₂ : Vec B n} + → Pointwise R V₁ V₂ + → Pointwise R W₁ W₂ + → Pointwise R (V₁ ++ W₁) (V₂ ++ W₂) + R-++ [] R-W = R-W + R-++ (R-v ∷ R-V) R-W = R-v ∷ R-++ R-V R-W + + R-replicate : {x : A} {y : B} → R x y → Pointwise R (replicate n x) (replicate n y) + R-replicate {n = zero} _ = [] + R-replicate {n = suc n} xRy = xRy ∷ R-replicate xRy + +R-zipWith + : {W : Vec A n} + {X : Vec B n} + {Y : Vec C n} + {Z : Vec D n} + {R : REL A B ℓ₁} + {S : REL C D ℓ₂} + {T : REL E F ℓ} + {f : A → C → E} + {g : B → D → F} + → (∀ {w x y z} → R w x → S y z → T (f w y) (g x z)) + → Pointwise R W X + → Pointwise S Y Z + → Pointwise T (zipWith f W Y) (zipWith g X Z) +R-zipWith cong [] [] = [] +R-zipWith cong (wRx ∷ WRX) (ySz ∷ YSZ) = cong wRx ySz ∷ R-zipWith cong WRX YSZ + +open Relation public diff --git a/Data/Vector/Vec.agda b/Data/Vector/Vec.agda index 868571a..4367bdd 100644 --- a/Data/Vector/Vec.agda +++ b/Data/Vector/Vec.agda @@ -5,6 +5,8 @@ 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; map; _++_) +open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW using (Pointwise-≡⇒≡) +open import Data.Vector.Raw using (R-zipWith) open import Function using (_∘_) open import Level using (Level) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) @@ -71,3 +73,16 @@ zipWith-map-map → zipWith (λ x y → f x ⊕ g y) v w ≡ zipWith _⊕_ (map f v) (map g w) zipWith-map-map f g _⊕_ [] [] = ≡.refl zipWith-map-map f g _⊕_ (x ∷ v) (y ∷ w) = ≡.cong (f x ⊕ g y ∷_) (zipWith-map-map f g _⊕_ v w) + +zipWith-cong + : {f g : A → B → C} + → (∀ x y → f x y ≡ g x y) + → (xs : Vec A n) + (ys : Vec B n) + → zipWith f xs ys + ≡ zipWith g xs ys +zipWith-cong f≗g xs ys = + Pointwise-≡⇒≡ + (R-zipWith {R = _≡_} {S = _≡_} (λ { ≡.refl ≡.refl → f≗g _ _}) + (PW.refl ≡.refl) + (PW.refl ≡.refl)) |