\subsection{Exercises}

\begin{comment}
\begin{code}
module Exercise1 where

{- The library is in the Library directory.

   To make the system find it do
     M-x customize-group
     agda2
     Add the Library directory (full path) to the Agda2 Include Dirs option
     Click Save for Future Sessions (or Set for Current Session, whichever you prefer)
-}

open import Data.Bool
open import Data.Vec
open import Data.List
open import Data.Nat
open import Data.Fin
open import Data.Function
open import Logic.Id
\end{code}
\end{comment}

\NewExercise{Matrix transposition}

We can model an $n × m$ matrix as a vector of vectors:
%
\begin{code}
Matrix : Set -> Nat -> Nat -> Set
Matrix A n m = Vec (Vec A n) m
\end{code}
%
The goal of this exercise is to define the transposition of such a matrix.

\Exercise{Define a function to compute a vector containing $n$ copies of an element $x$.}

\begin{code}
vec : {n : Nat}{A : Set} -> A -> Vec A n
vec {n} x = {! !}
\end{code}

\Exercise{Define point-wise application of a vector of functions to a vector of arguments.}

\begin{code}
infixl 90 _$_
_$_ : {n : Nat}{A B : Set} -> Vec (A -> B) n -> Vec A n -> Vec B n
fs $ xs = {! !}
\end{code}

\Exercise{Define matrix transposition in terms of these two functions.}

\begin{code}
transpose : forall {A n m} -> Matrix A n m -> Matrix A m n
transpose xss = {! !}
\end{code}

\NewExercise{Vector lookup}

Remember {\tt tabulate} and {\tt \_!\_} from Section~\ref{Families}. Prove that they are indeed each other's inverses.

\Exercise{This direction should be relatively easy.}
\begin{code}
lem-!-tab : forall {A n} (f : Fin n -> A)(i : Fin n) ->
            tabulate f ! i == f i
lem-!-tab f i = {! !}
\end{code}

\Exercise{This direction might be trickier.}
\begin{code}
lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs
lem-tab-! xs = {! !}
\end{code}

\NewExercise{Sublists}

Remember the representation of sublists from Section~\ref{Families}:

\begin{code}
data _⊆_ {A : Set} : List A -> List A -> Set where
  stop : [] ⊆ []
  drop : forall {x xs ys} -> xs ⊆ ys ->      xs ⊆ x :: ys
  keep : forall {x xs ys} -> xs ⊆ ys -> x :: xs ⊆ x :: ys
\end{code}

\Exercise{Prove the reflexivity and transitivity of {\tt \_⊆\_}:}

\begin{code}
⊆-refl : {A : Set}{xs : List A} -> xs ⊆ xs
⊆-refl {xs = xs} = {! !}

⊆-trans : {A : Set}{xs ys zs : List A} ->
          xs ⊆ ys -> ys ⊆ zs -> xs ⊆ zs
⊆-trans p q = {! !}
\end{code}

Instead of defining the sublist relation we can define the type of
sublists of a given list as follows:

\begin{code}
infixr 30 _::_
data SubList {A : Set} : List A -> Set where
  []   : SubList []
  _::_ : forall x {xs} -> SubList xs -> SubList (x :: xs)
  skip : forall {x xs} -> SubList xs -> SubList (x :: xs)
\end{code}

\Exercise{Define a function to extract the list corresponding to a sublist.}

\begin{code}
forget : {A : Set}{xs : List A} -> SubList xs -> List A
forget s = {! !}
\end{code}

\Exercise{Now, prove that a {\tt SubList} is a sublist in the sense of {\tt \_⊆\_}.}

\begin{code}
lem-forget : {A : Set}{xs : List A}(zs : SubList xs) ->
             forget zs ⊆ xs
lem-forget zs = {! !}
\end{code}

\Exercise{Give an alternative definition of filter which satisfies the
sublist property by construction.}

\begin{code}
filter' : {A : Set} -> (A -> Bool) -> (xs : List A) -> SubList xs
filter' p xs = {! !}
\end{code}

\Exercise{Define the complement of a sublist}

\begin{code}
complement : {A : Set}{xs : List A} -> SubList xs -> SubList xs
complement zs = {! !}
\end{code}

\Exercise{Compute all sublists of a given list}

\begin{code}
sublists : {A : Set}(xs : List A) -> List (SubList xs)
sublists xs = {! !}
\end{code}