------------------------------------------------------------------------ -- Vectors ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} open import Equality module Vec {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where open import Prelude hiding (tail) open import Bijection eq using (_↔_) open Derived-definitions-and-properties eq open import Function-universe eq hiding (_∘_) open import List eq using (length) open import Surjection eq using (_↠_; ↠-≡) ------------------------------------------------------------------------ -- Some simple functions -- Finds the element at the given position. index : ∀ {n} {a} {A : Set a} → Fin n → Vec A n → A index {zero} () _ index {suc _} fzero (x , _) = x index {suc _} (fsuc i) (_ , xs) = index i xs -- Applies the function to every element in the vector. map : ∀ {n a b} {A : Set a} {B : Set b} → (A → B) → Vec A n → Vec B n map {zero} f _ = _ map {suc _} f (x , xs) = f x , map f xs -- Constructs a vector containing a certain number of copies of the -- given element. replicate : ∀ {n a} {A : Set a} → A → Vec A n replicate {zero} _ = _ replicate {suc _} x = x , replicate x ------------------------------------------------------------------------ -- Conversions to and from lists -- Vectors can be converted to lists. to-list : ∀ {n} {a} {A : Set a} → Vec A n → List A to-list {zero} _ = [] to-list {suc n} (x , xs) = x ∷ to-list xs -- Lists can be converted to vectors. from-list : ∀ {a} {A : Set a} (xs : List A) → Vec A (length xs) from-list [] = _ from-list (x ∷ xs) = x , from-list xs -- ∃ (Vec A) is isomorphic to List A. ∃Vec↔List : ∀ {a} {A : Set a} → ∃ (Vec A) ↔ List A ∃Vec↔List {A = A} = record { surjection = record { logical-equivalence = record { to = to-list ∘ proj₂ ; from = λ xs → length xs , from-list xs } ; right-inverse-of = to∘from } ; left-inverse-of = uncurry from∘to } where to∘from : (xs : List A) → to-list (from-list xs) ≡ xs to∘from [] = refl _ to∘from (x ∷ xs) = cong (x ∷_) (to∘from xs) tail : A → ∃ (Vec A) ↠ ∃ (Vec A) tail y = record { logical-equivalence = record { to = λ where (suc n , _ , xs) → n , xs xs@(zero , _) → xs ; from = Σ-map suc (y ,_) } ; right-inverse-of = refl } from∘to : ∀ n (xs : Vec A n) → (length (to-list xs) , from-list (to-list xs)) ≡ (n , xs) from∘to zero _ = refl _ from∘to (suc n) (x , xs) = $⟨ from∘to n xs ⟩ (length (to-list xs) , from-list (to-list xs)) ≡ (n , xs) ↝⟨ _↠_.from $ ↠-≡ (tail x) ⟩□ (length (to-list (x , xs)) , from-list (to-list (x , xs))) ≡ (suc n , x , xs) □