open import 1Lab.Prelude

open import Data.Fin.Base

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πŸ”—

tabulate-lookup : (xs : Vec A n) β†’ tabulate (lookup xs) ≑ xs
tabulate-lookup []       = refl
tabulate-lookup (x ∷ xs) = ap (x ∷_) (tabulate-lookup xs)

lookup-tabulate : (xs : Fin n β†’ A) (i : Fin n) β†’ lookup (tabulate xs) i ≑ xs i
lookup-tabulate xs fzero = refl
lookup-tabulate xs (fsuc i) = lookup-tabulate (Ξ» x β†’ xs (fsuc x)) 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

module Lookup {β„“} {A : Type β„“} {n : Nat} = Equiv (lookup {A = A} {n} , lookup-is-equiv)

map-lookup : βˆ€ (f : A β†’ B) (xs : Vec A n) i β†’ lookup (Vec.map f xs) i ≑ f (lookup xs i)
map-lookup f (x ∷ xs) fzero    = refl
map-lookup f (x ∷ xs) (fsuc i) = map-lookup f xs i

map-id : (xs : Vec A n) β†’ Vec.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)
  β†’ Vec.map (Ξ» x β†’ g (f x)) xs ≑ Vec.map g (Vec.map f xs)
map-comp xs f g = Lookup.injective $ funext Ξ» i β†’
  lookup (Vec.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 (Vec.map f xs) i)           β‰‘Λ˜βŸ¨ map-lookup g (Vec.map f xs) i βŸ©β‰‘Λ˜
  lookup (Vec.map g (Vec.map f xs)) i   ∎