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

\begin{document}

\input{cs54header.tex}

\begin{header}
\psheader{- Week 07}{22}{10:00pm}{Sunday}
\end{header}

\begin{itemize}
\item As before, you are welcome to discuss the problems with your
  classmates, the TAs, and myself.  You must write up your solutions
  on your own (or with your partner).  You should never be looking at
  someone else's solution (not even written up on a whiteboard!) nor
  should you show anyone else in the class your solution.  This also
  means that if you're working on a whiteboard, you should erase
  your work when you're done.
\item Solutions to the written component must be typeset using
  \LaTeX\; and uploaded to Gradescope as a pdf.  The \LaTeX\; source
  is available on the course webpage and you are encouraged to modify
  that file by adding your solutions after each question.  When
  you upload your pdf to Gradescope you will be asked to identify the
  pages for each problem.  It's ok if you give the same page for more
  than one problem.
\end{itemize}

\vspace*{.1cm}

\begin{enumerate}
\item \problem{10}{Proofs by induction}
  \begin{enumerate}
  \item Use a proof by induction to show that $\sum_{i=0}^n i^2 =
    \frac{n(n+1)(2n+1)}{6}$ for all integers $n \geq 0$.
  \item Use a proof by induction to show that for all $n \in
    \mathbb{Z}^+$, $3 | (n^3+2n)$.
  \item Use a proof by induction to show that $2^m > m$ for all $m \in
    \mathbb{Z}^+$.
  \end{enumerate}
    
\item \problem{12}{Proofs about programs}
  Consider the following Haskell code:
  \begin{verbatim}
plus 0 b = b
plus a b = (plus (a-1) b) + 1

mult 0 _b = 0
mult a b = (mult (a-1) b) + b
  \end{verbatim}
  Recall from class that we can rewrite a term like \verb|plus (a+1) b| into \verb|(plus ((a+1)-1) b) + 1| ``by the definition of plus''.  Also recall that it's fine to use what we know about \verb|+| and \verb|-|.  For example, we proved this theorem together:
  \newcommand{\hplus}[2]{\mathtt{plus}\,#1\,#2}
  \newcommand{\hmult}[2]{\mathtt{mult}\,#1\,#2}

  Theorem: \(\forall a \in \mathbb{N},~\hplus~ a~ 0 = a\)

  Proof: By induction on a.
  \begin{itemize}
  \item (\(a=0\)). \(\hplus{0}{0} = 0\) by the definition of plus.
  \item (\(a=a'+1\)).  IH: \(\hplus{a'}{0} = a'\).  We want to show that \(\hplus{(a'+1)}{0} = a'+1\).

    First, by the definition of plus, \(\hplus{(a'+1)}{0} = \hplus{((a'+1)-1)}{0}+1\), i.e. \(\hplus{a'}{0}+1\).

    By the IH, \(\hplus{a'}{0} = a'\), so we have \(a' + 1 = a' + 1\), which is what we were trying to prove.
  \end{itemize}
  
  \begin{enumerate}
  \item Prove \textit{mult0}: \(\forall a \in \mathbb{N}, \hmult{a}{0} = \hmult{0}{a}\).
  \item Prove \textit{mult\_b)}:\(\forall a \in \mathbb{N}\,b \in \mathbb{N}, \hmult{a}{b} + a = \hmult{a}{(b+1)}\).
  \item Use the above theorems to prove \textit{mult\_comm}: \(\forall a \in \mathbb{N}\,b \in \mathbb{N}, \hmult{a}{b} = \hmult{b}{a}\).
  \end{enumerate}
\end{enumerate}

\end{document}
