# 2020-01-17 `FinVec`

```
module FinVec where

open import Data.Product
open import Data.Nat using ( ℕ ; zero ; suc ; _<_ ; z≤n ; s≤s )

open import Function using ( _∘_ )

open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; cong )
```

## Prototypical Finite Types: `Fin`

The type `Fin n` can be seen as an inductive implementation
of the set of all natural numbers less than `n`.
Informally:

  Fin 0 = {}
  Fin 1 = { 0 }
  Fin 2 = { 0 , 1 }

```
data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc : {n : ℕ} → Fin n → Fin (suc n)
```

  suc (zero : Fin 1) : Fin 2

```
toℕ : {n : ℕ} → Fin n → ℕ
toℕ zero = 0
toℕ (suc i) = suc (toℕ i)
```

For each `n`, the function `toℕ {n}` is injective:
```
suc-injective : {m n : ℕ} → ℕ.suc m ≡ suc n → m ≡ n
suc-injective = {!!}

toℕ-injective : {n : ℕ} {i j : Fin n} → toℕ i ≡ toℕ j → i ≡ j
toℕ-injective = {!!}
```

But since `toℕ {n}` is not surjective, we cannot define a full inverse:

  fromℕ : {n : ℕ} → (m : ℕ) → Fin n -- cannot be injective because of pigeon-hole

  toℕ-fromℕ : {n : ℕ} (m : ℕ) → toℕ (fromℕ m) ≡ m   -- cannot be made to hold

Since the range of the function `toℕ {n}` contains exactly the
natural numbers that are smaller than `n`,
the restriction to these makes it possible to define an inverse function for `toℕ {n}`:
```
fromℕ : {n : ℕ} → (m : ℕ) → m < n → Fin n
fromℕ = {!!}
```

If we defined this correctly, we can now show the inverse properties:
```
toℕ-bound : {n : ℕ} (i : Fin n) → toℕ i < n
toℕ-bound = {!!}

fromℕ-toℕ : {n : ℕ} (i : Fin n) → fromℕ (toℕ i) {!!} ≡ i
fromℕ-toℕ = {!!}

toℕ-fromℕ : {n : ℕ} (m : ℕ) (m<n : m < n) → toℕ (fromℕ m m<n) ≡ m
toℕ-fromℕ = {!!}
```


## Known-length “Vectors”

An elemet of the type `Vec A n` is a vector of `n` elements of type `A`.

```
data Vec (A : Set) : ℕ → Set where
  [] : Vec A zero
  _∷_ : A → {n :  ℕ} → Vec A n → Vec A (suc n)
```

```
vmap : {A B : Set} → (A → B) → {n : ℕ} → (Vec A n → Vec B n)
vmap f [] = []
vmap f (x ∷ xs) = f x ∷ vmap f xs
```

```
_!_ : {A : Set} {n : ℕ} → Vec A n → (Fin n → A)
[] ! ()
(x ∷ xs) ! zero = x
(x ∷ xs) ! suc i = xs ! i
```

The parentheses in the type of `_!_` emphasis that we can
think of `_!_ {A} {n}` as a function
that turns vectors of type `Vec A n`
into functions of type `Fin n → A`.
This has an inverse:

```
tabulate : {A : Set} {n : ℕ} → (Fin n → A) → Vec A n
tabulate = {!!}
```

If we defined this correctly, we can prove the inverse properties:

```
tabulate-! : {A : Set} {n : ℕ} → (xs : Vec A n) → tabulate (_!_ xs) ≡ xs
tabulate-! = {!!}


!-tabulate : {A : Set} {n : ℕ} → (f : Fin n → A) → (i : Fin n) → tabulate f ! i ≡ f i
!-tabulate = {!!}
```