\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}