open import 1Lab.Prelude

open import Data.List.Base hiding (head ; tail ; lookup ; tabulate ; _++_)
open import Data.Fin.Base
open import Data.Irr

import Data.Vec.Base as Vec

open Vec

module Data.Vec.Properties where

private variable
  ℓ : Level
  A B C : Type ℓ
  n k : Nat
  xs ys zs : Vec A n

Properties of vectors🔗

In this module we show properties of vectors, including the equivalence between vectors of length $n$ and functions from Fin n.

tabulate-lookup : (xs : Vec A n) → tabulate (lookup xs) ≡ xs
tabulate-lookup v with vec-view v
... | []       = refl
... | (x ∷ xs) = ap (x ∷v_) (tabulate-lookup xs)

lookup-tabulate : (xs : Fin n → A) (i : Fin n) → lookup (tabulate xs) i ≡ xs i
lookup-tabulate xs i with fin-view i
... | zero  = refl
... | suc i = lookup-tabulate (xs ∘ fsuc) i

lookup-is-equiv : is-equiv (lookup {A = A} {n})
lookup-is-equiv = is-iso→is-equiv $
  iso tabulate (λ x → funext (lookup-tabulate x)) tabulate-lookup

Vec≃Fun : Vec A n ≃ (Fin n → A)
Vec≃Fun = lookup , lookup-is-equiv

module Lookup {ℓ} {A : Type ℓ} {n : Nat} = Equiv (Vec≃Fun {A = A} {n = n})

It follows from Vec≃Fun that Vec preserves h-Level.

Vec-is-hlevel
  : ∀ {A : Type ℓ} {n} m
  → is-hlevel A m
  → is-hlevel (Vec A n) m
Vec-is-hlevel m Ahl = Equiv→is-hlevel m Vec≃Fun (fun-is-hlevel m Ahl)

instance
  H-Level-Vec :
    ∀ {m} {A : Type ℓ} {n} → ⦃ H-Level A n ⦄
    → H-Level (Vec A m) n
  H-Level-Vec {n = n} .H-Level.has-hlevel = Vec-is-hlevel n (hlevel n)

unquoteDecl ap-vec = declare-record-path ap-vec (quote Vec)

We define the following for building paths between vectors:

Vec-path
  : ∀ {A : Type ℓ} {n} {v w : Vec A (suc n)}
  → (head v ≡ head w) → (tail v ≡ tail w)
  → v ≡ w
Vec-path {v = vec (x ∷ xs)} {w = vec (y ∷ ys)} p q = ap-vec $ ap₂ _∷_ p (ap Vec.lower q)
Vec-path {v = vec [] ⦃ l ⦄} with () ← recover l
Vec-path {w = vec [] ⦃ l ⦄} with () ← recover l

[]-unique : ∀ {A : Type ℓ} → is-contr (Vec A 0)
[]-unique {A = A} .centre = []v
[]-unique {A = A} .paths v with vec-view v
... | [] = refl

Functoriality🔗

Here we show the functoriality of Vec.map.

map-lookup : (f : A → B) (xs : Vec A n) → ∀ i → lookup (map f xs) i ≡ f (lookup xs i)
map-lookup f v i with vec-view v | fin-view i
... | (x ∷ xs) | zero  = refl
... | (x ∷ xs) | suc i = map-lookup f xs i

map-id : {A : Type ℓ} (xs : Vec A n) → map (λ x → x) xs ≡ xs
map-id xs = Lookup.injective₂ (funext λ i → map-lookup _ xs i) refl

map-comp
  : (xs : Vec A n) (f : A → B) (g : B → C)
  → map (λ x → g (f x)) xs ≡ map g (map f xs)
map-comp xs f g = Lookup.injective $ funext λ i →
  lookup (map (λ x → g (f x)) xs) i ≡⟨ map-lookup (λ x → g (f x)) xs i ⟩≡
  g (f (lookup xs i))               ≡˘⟨ ap g (map-lookup f xs i) ⟩≡˘
  g (lookup (map f xs) i)           ≡˘⟨ map-lookup g (map f xs) i ⟩≡˘
  lookup (map g (map f xs)) i       ∎