\input{latex-macros/handout-preamble.tex}
\inhandout{
\decideaboutsolutions
\usesimpleproblems
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Problem starts here
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{problem}
\PTAGfilename{CP0303_recursively_defined_sets}
\PTAGhistory{S09_cp5m}
%\PTAGkeyword{recursive data types}  %not sure best way to implement multiple keywords yet
%\PTAGkeyword{structural induction}
%
Here is a simple recursive definition of the set, $E$, of even integers:
\begin{definition*}
\textbf{Base case}: $ 0 \in E$.

\textbf{Constructor cases}:
    If $n \in E$, then so are $n+2$ and $-n$.
\end{definition*}
Provide similar simple recursive definitions of the following sets:

\bparts

\item The set $S \eqdef \set{ 2^k 3^m 5^n \suchthat k,m,n \in
\naturals}$.

\solution{We can define the set $S$ recursively as follows:

\begin{itemize}
\item $1 \in S$
\item If $n \in S$, then $2n$, $3n$, and $5n$ are in $S$.
\end{itemize}
}

\item  The set $T \eqdef \set{2^k 3^{2k+m} 5^{m+n} \suchthat k,m,n \in
\naturals}$.

\solution{We can define the set $T$ recursively as follows:

\begin{itemize}
\item $1 \in T$
\item If $n \in S$, then $18n$, $15n$, and $5n$ are in $T$.
\end{itemize}
}

\item The set $L \eqdef \set{ (a, b) \in \integers^2 \suchthat 3
  \divides (a-b)}$.

\solution{We can define a set $L' = L$ recursively as follows:

\begin{itemize}
\item $(0, 0), (1,1), (2,2) \in L'$
\item If $(a, b) \in L'$, then $(a + 3, b)$, $(a - 3, b)$, $(a, b +3)$, and
$(a, b -3)$ are in $L'$.
\end{itemize}

Lots of other definitions are also possible.}
\eparts

Let $L'$ be the set defined by the recursive definition you gave for $L$
in the previous part.  Now if you did it right, then $L'=L$, but maybe you
made a mistake.  So let's check that you got the definition right.

\bparts
\ppart Prove by structural induction on your definition of $L'$ that
\[
L' \subseteq L.
\]

\solution{
For the $L'$ defined above, a straightforward structural induction shows
that if $(c,d) \in L'$, then $(c,d) \in L$.  Namely, each of the base
cases in the definition of $L'$ are in $L$ since $3 \divides 0$.  For the
constructor cases, we may assume $(a,b) \in L$, that is $3 \divides
(a-b)$, and must prove that $(a\pm 3,b) \in L$ and $(a,b \pm 3) \in L$.
In the first the case, we must show that $3 \divides ((a\pm 3)-b)$.  But
this follows immediately because $((a\pm 3)-b) = (a-b)\pm 3$ and 3 divides
both $(a-b)$ and 3.  The other constructor case $(a,b\pm 3)$ follows in
exactly the same way.  So we conclude by structural induction on the
definition of $L'$ that $L' \subseteq L$.}

\ppart \emph{Optional: come back to this part only if you finish all the
  remaining problems.}  Confirm that you got the definition right by
proving that
\[
L \subseteq L'.
\]

\solution{Conversely, we must show that $L \subseteq L'$.  So suppose
  $(c,d) \in L$, that is, $3 \divides (c-d)$.  This means that $c = r+3k$
  and $d=r +3j$ for some $r \in \set{0,1,2}$ and $j,k \in \integers$.
  Then starting from base case $(r,r) \in L'$, we can apply the $(a \pm
  3,b)$ constructor rule $\abs{k}$ times to conclude that $(c,r) \in L'$,
  and then apply the $(a ,b \pm 3)$ rule $\abs{j}$ times to conclude that
  $(c,d) \in L'$.  This implies that $L \subseteq L'$, which completes the
  proof that $L = L'$.} 

\ppart \emph{Optional: come back to this part only if you finish all the
  remaining problems.}  Give an \emph{unambiguous} recursive definition of
$L$.

\solution{This is tricky.  Here is an attempt:

  \textbf{base cases}: $(0, 0), (1,1), (2,2), (-1,-1), (-2,-2), (-3,-3)
  (1, -2), (2, -1), (-1, 2), (-2, 1) \in L$

Now the idea is to constrain the constructors so the two coordinates have
absolute values that increase differing by at most 1, then one coordinate only
can continue to grow in absolute value.  Let
\[
\sg(x) \eqdef \begin{cases}
              1 \text{ if } x \geq 0,\\
             -1 \text{ if } x < 0.
              \end{cases}
\]

\textbf{constructors}: if $(a,b) \in L'$, then

\begin{itemize}

\item if $\abs{\abs{a} - \abs{b}} \leq 1 $, then $(a+3\sg(a),b+3\sg(b)),
  (a+3\sg(a),b), (a,b+3\sg(b)) \in L'$,

\item if $\abs{a} > \abs{b}+1$, then $(a+3\sg(a),b) \in L'$,

\item if $\abs{b} > \abs{a} + 1$, then $(a,b+3\sg(b)) \in L'$.

\end{itemize}
}

\eparts
\end{problem}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Problem ends here
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{latex-macros/handout-postamble.tex}