------------------------------------------------------------------------ -- Vectors, defined using an inductive family ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} open import Equality module Vec.Data {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where open import Prelude 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 (_↠_; ↠-≡) ------------------------------------------------------------------------ -- The type -- Vectors. infixr 5 _∷_ data Vec {a} (A : Set a) : ℕ → Set a where [] : Vec A zero _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n) ------------------------------------------------------------------------ -- Some simple functions -- Finds the element at the given position. index : ∀ {n} {a} {A : Set a} → Vec A n → Fin n → A index (x ∷ _) fzero = x index (_ ∷ xs) (fsuc i) = index xs i -- Updates the element at the given position. infix 3 _[_≔_] _[_≔_] : ∀ {n} {a} {A : Set a} → Vec A n → Fin n → A → Vec A n _[_≔_] [] () _ _[_≔_] (x ∷ xs) fzero y = y ∷ xs _[_≔_] (x ∷ xs) (fsuc i) y = x ∷ (xs [ i ≔ y ]) -- 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 f [] = [] map 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 -- The head of the vector. head : ∀ {n a} {A : Set a} → Vec A (suc n) → A head (x ∷ _) = x -- The tail of the vector. tail : ∀ {n a} {A : Set a} → Vec A (suc n) → Vec A n tail (_ ∷ xs) = xs ------------------------------------------------------------------------ -- 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 [] = [] to-list (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) □