Martin Escardo, 15th December 2019, 9th Feb 2021.

Vectors with a different type for each entry (vec), usual vectors
(Vec) and lists (List) in our spartan MLTT.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module MLTT.SpartanList where

open import MLTT.Spartan
open import Fin.Type

vec : (n : β„•) β†’ (Fin n β†’ 𝓀 Μ‡ ) β†’ 𝓀 Μ‡
vec 0        X = πŸ™
vec (succ n) X = X 𝟎 Γ— vec n (X ∘ suc)

Vec : 𝓀 Μ‡ β†’ β„• β†’ 𝓀 Μ‡
Vec X n = vec n (Ξ» _ β†’ X)

List : 𝓀 Μ‡ β†’ 𝓀 Μ‡
List X = Ξ£ n κž‰ β„• , Vec X n

length : {X : 𝓀 Μ‡ } β†’ List X β†’ β„•
length = pr₁

pattern [] = (0 , ⋆)

_∷_ : {X : 𝓀 Μ‡ } β†’ X β†’ List X β†’ List X
x ∷ (n , s) = succ n , x , s

[_] : {X : 𝓀 Μ‡ } β†’ X β†’ List X
[ x ] = x ∷ []

\end{code}

Our list encoding satisfies Martin-LΓΆf's rules for lists:

\begin{code}

List-induction : {X : 𝓀 Μ‡ } (P : List X β†’ π“₯ Μ‡ )
               β†’ P []
               β†’ ((x : X) (xs : List X) β†’ P xs β†’ P (x ∷ xs))
               β†’ (xs : List X) β†’ P xs
List-induction {𝓀} {π“₯} {X} P p f = h
 where
  h : (xs : List X) β†’ P xs
  h []               = p
  h (succ n , x , s) = f x (n , s) (h (n , s))

\end{code}

With the computation rules holding definitionally, as required:

\begin{code}

List-induction-[] : {X : 𝓀 Μ‡ } (P : List X β†’ π“₯ Μ‡ )
               β†’ (p : P [])
               β†’ (f : (x : X) (xs : List X) β†’ P xs β†’ P (x ∷ xs))
               β†’ List-induction P p f [] ＝ p
List-induction-[] {𝓀} {π“₯} {X} P p f = refl

List-induction-∷ : {X : 𝓀 Μ‡ } (P : List X β†’ π“₯ Μ‡ )
               β†’ (p : P [])
               β†’ (f : (x : X) (xs : List X) β†’ P xs β†’ P (x ∷ xs))
               β†’ (x : X)
               β†’ (xs : List X)
               β†’ List-induction P p f (x ∷ xs) ＝ f x xs (List-induction P p f xs)
List-induction-∷ {𝓀} {π“₯} {X} P p f x xs = refl

pattern ⟨⟩       = ⋆
pattern _::_ x xs = (x , xs)

hd : {n : β„•} {X : Fin (succ n) β†’ 𝓀 Μ‡ } β†’ vec (succ n) X β†’ X 𝟎
hd (x :: xs) = x

tl : {n : β„•} {X : Fin (succ n) β†’ 𝓀 Μ‡ } β†’ vec (succ n) X β†’ vec n (X ∘ suc)
tl (x :: xs) = xs

index : (n : β„•) {X : Fin n β†’ 𝓀 Μ‡ } β†’ vec n X β†’ (i : Fin n) β†’ X i
index 0        xs        i       = 𝟘-elim i
index (succ n) (x :: xs) 𝟎       = x
index (succ n) (x :: xs) (suc i) = index n xs i

_!!_ : {n : β„•} {X : 𝓀 Μ‡ } β†’ Vec X n β†’ (i : Fin n) β†’ X
_!!_ {𝓀} {n} = index n

\end{code}

An isomorphic copy of vec n X.

\begin{code}

vec' : (n : β„•) β†’ (Fin n β†’ 𝓀 Μ‡ ) β†’ 𝓀 Μ‡
vec' n X = (i : Fin n) β†’ X i

Vec' : β„• β†’ 𝓀 Μ‡ β†’ 𝓀 Μ‡
Vec' n X = vec' n (Ξ» _ β†’ X)

hd' : {n : β„•} {X : Fin (succ n) β†’ 𝓀 Μ‡ } β†’ vec' (succ n) X β†’ X 𝟎
hd' xs = xs 𝟎

tl' : {n : β„•} {X : Fin (succ n) β†’ 𝓀 Μ‡ } β†’ vec' (succ n) X β†’ vec' n (X ∘ suc)
tl' xs = Ξ» i β†’ xs (suc i)


⟨⟩' : {X : Fin 0 β†’ 𝓀 Μ‡ } β†’ vec' 0 X
⟨⟩' = Ξ» i β†’ unique-from-𝟘 i


_::'_ : {n : β„•} {X : Fin (succ n) β†’ 𝓀 Μ‡ }
     β†’ X 𝟎 β†’ vec' n (X ∘ suc) β†’ vec' (succ n) X
(x ::' xs) 𝟎       = x
(x ::' xs) (suc i) = xs i


xedni : (n : β„•) {X : Fin n β†’ 𝓀 Μ‡ } β†’ ((i : Fin n) β†’ X i) β†’ vec n X
xedni 0        xs' = ⟨⟩
xedni (succ n) xs' = hd' xs' :: xedni n (tl' xs')


vecΞ· : (n : β„•) {X : Fin n β†’ 𝓀 Μ‡ } β†’ xedni n {X} ∘ index n {X} ∼ id
vecη zero     ⟨⟩       = refl
vecΞ· (succ n) (x :: xs) = ap (x ::_) (vecΞ· n xs)

open import UF.FunExt
open import UF.Base
open import UF.Equiv

module _ {𝓀} (fe : funext 𝓀₀ 𝓀) where

 vecΞ΅ : (n : β„•) {X : Fin n β†’ 𝓀 Μ‡ } β†’ index n {X} ∘ xedni n {X} ∼ id
 vecΞ΅ 0        xs' = dfunext fe (Ξ» i β†’ 𝟘-elim i)
 vecΞ΅ (succ n) xs' = dfunext fe h
  where
   h : (i : Fin (succ n)) β†’ index (succ n) (xs' 𝟎 :: xedni n (tl' xs')) i ＝ xs' i
   h 𝟎       = refl
   h (suc i) = happly (vecΞ΅ n (tl' xs')) i


 vec-≃ : (n : β„•) {X : Fin n β†’ 𝓀 Μ‡ } β†’ vec n X ≃ vec' n X
 vec-≃ n {X} = qinveq (index n) (xedni n {X} , vecΞ· n , vecΞ΅ n)

\end{code}

9th Feb 2021. More operations on vectors. The stuff on
vectors should be eventually moved to another module.

\begin{code}

⟨_⟩ : {X : 𝓀 Μ‡ } β†’ X β†’ Vec X 1
⟨ x ⟩ = x :: ⟨⟩

_βˆ”_ : β„• β†’ β„• β†’ β„•
zero   βˆ” n = n
succ m βˆ” n = succ (m βˆ” n)

append : {X : 𝓀 Μ‡ } (m n : β„•) β†’ Vec X m β†’ Vec X n β†’ Vec X (m βˆ” n)
append zero     n ⟨⟩      t = t
append (succ m) n (x :: s) t = x :: append m n s t

_++_ : {X : 𝓀 Μ‡ } {m n : β„•} β†’ Vec X m β†’ Vec X n β†’ Vec X (m βˆ” n)
_++_ = append _ _

plus-1-is-succ : (n : β„•) β†’ n βˆ” 1 ＝ succ n
plus-1-is-succ zero     = refl
plus-1-is-succ (succ n) = ap succ (plus-1-is-succ n)

rev' : {X : 𝓀 Μ‡ } (n : β„•) β†’ Vec X n β†’ Vec X n
rev' zero     ⟨⟩      = ⟨⟩
rev' (succ n) (x :: s) = Ξ³
 where
  IH : Vec _ (n βˆ” 1)
  IH = rev' n s ++ ⟨ x ⟩

  Ξ³ : Vec _ (succ n)
  Ξ³ = transport (Vec _) (plus-1-is-succ n) IH

rev : {X : 𝓀 Μ‡ } {n : β„•} β†’ Vec X n β†’ Vec X n
rev = rev' _

_+ₐ_ : β„• β†’ β„• β†’ β„•
zero   +ₐ n = n
succ m +ₐ n = m +ₐ succ n

rev-append : {X : 𝓀 Μ‡ } (m n : β„•) β†’ Vec X m β†’ Vec X n β†’ Vec X (m +ₐ n)
rev-append zero     n ⟨⟩       t = t
rev-append (succ m) n (x :: s) t = rev-append m (succ n) s (x :: t)

revₐ : {X : 𝓀 Μ‡ } (m : β„•) β†’ Vec X m β†’ Vec X (m +ₐ zero)
revₐ n s = rev-append n zero s ⟨⟩

\end{code}