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