

\documentclass[11pt]{article}
\usepackage[nostamp]{coursetemplate}

\begin{document}

\input{cs54header.tex}

\begin{header}
\psheader{12 - groupwork}{5}{11:59PM}{Thursday}
\end{header}

\newcommand{\ins}[2]{\ensuremath{\mathtt{insert}\,#1\,#2}}
\newcommand{\len}[1]{\ensuremath{\mathtt{length}\,#1}}
\newcommand{\map}[2]{\ensuremath{\mathtt{map}\,#1\,#2}}
\newcommand{\filter}[2]{\ensuremath{\mathtt{filter}\,#1\,#2}}

\begin{verbatim}
insert x [] = [x]
insert x (y:l)
  | x <= y = x:y:l
  | otherwise = y:(insert x l)

map _f [] = []
map f (x:l) = x:(map f l)

filter _f [] = []
filter f (x:l)
  | f x = x : (filter f l)
  | otherwise = filter f l

length [] = 0
length (_:l) = 1 + length l
\end{verbatim}

\begin{enumerate}
  \item \problem{1}{FilterLength} Prove by induction that for all lists l and functions f, \(\len{(\filter{f}{l})} \le \len{l}\).
  \item \problem{1}{InsertLength} Prove by induction that for all lists l and elements x, \(\len{(\ins{x}{l})} = \len{l}+1\).
  \item \problem{1}{FilterCollapse} Prove by induction that for all lists l and functions f: \(\filter{f}{(\filter{f}{l})} = \filter{f}{l}\).
  \item \problem{1}{MapFilterSwap} Prove by induction that for all lists l and functions a, b: \(\map{a}{(\filter{b}{l})} = \filter{b}{(\map{a}{l})}\).
  \item \problem{1}{MapInverse} Prove by induction that for all lists l and functions a, b, if b is a's inverse (in other words, if \(\forall x, b\,(a\,x) = x\)) then \(\map{b}{(\map{a}{l})} = l\).

\end{enumerate}
\end{document}
