{-# OPTIONS --without-K --safe #-}
open import Equality
module Vec
{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 (id; _∘_)
open import List eq using (length)
open import Surjection eq using (_↠_; ↠-≡)
private
variable
a b c : Level
A B : Set a
f g : A → B
n : ℕ
Vec : Set a → ℕ → Set a
Vec A zero = ↑ _ ⊤
Vec A (suc n) = A × Vec A n
index : Vec A n → Fin n → A
index {n = suc _} (x , _) fzero = x
index {n = suc _} (_ , xs) (fsuc i) = index xs i
infix 3 _[_≔_]
_[_≔_] : Vec A n → Fin n → A → Vec A n
_[_≔_] {n = zero} _ () _
_[_≔_] {n = suc _} (x , xs) fzero y = y , xs
_[_≔_] {n = suc _} (x , xs) (fsuc i) y = x , (xs [ i ≔ y ])
map : (A → B) → Vec A n → Vec B n
map {n = zero} f _ = _
map {n = suc _} f (x , xs) = f x , map f xs
replicate : A → Vec A n
replicate {n = zero} _ = _
replicate {n = suc _} x = x , replicate x
head : Vec A (suc n) → A
head = proj₁
tail : Vec A (suc n) → Vec A n
tail = proj₂
to-list : Vec A n → List A
to-list {n = zero} _ = []
to-list {n = suc n} (x , xs) = x ∷ to-list xs
from-list : (xs : List A) → Vec A (length xs)
from-list [] = _
from-list (x ∷ xs) = x , from-list xs
∃Vec↔List : ∃ (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) □
map-id :
{A : Set a} {xs : Vec A n} → map id xs ≡ xs
map-id {n = zero} = refl _
map-id {n = suc n} = cong (_ ,_) map-id
map-∘ :
{A : Set a} {B : Set b} {C : Set c} {f : B → C} {g : A → B}
{xs : Vec A n} →
map (f ∘ g) xs ≡ map f (map g xs)
map-∘ {n = zero} = refl _
map-∘ {n = suc n} = cong (_ ,_) map-∘
map-cong :
∀ {n} {xs : Vec A n} →
(∀ x → f x ≡ g x) → map f xs ≡ map g xs
map-cong {n = zero} _ = refl _
map-cong {n = suc n} hyp = cong₂ _,_ (hyp _) (map-cong hyp)