\documentclass{article}
\usepackage{graphicx}
\usepackage[colorlinks=true,urlcolor=blue,linkcolor=blue,citecolor=blue]{hyperref}%
\usepackage{fancyhdr}
\usepackage[margin=35mm]{geometry}
\usepackage{amsmath}

\newcommand{\fn}[1]{\mathrm{#1}}
\newcommand{\append}{\mathbin{+\mkern-10mu+}}
\newcommand{\cons}{\mathbin{::}}

\pagestyle{fancy}
\fancyhf{}
\renewcommand{\headrulewidth}{0pt}

\lhead{\sf Logic and Mechanized Reasoning}
\rhead{\sf Fall 2021}


\begin{document}

\bigskip

\begin{center}
{\Large Assignment 3}

\medskip

due Thursday, September 16, 2021
\end{center}

\medskip

\thispagestyle{fancy}

\noindent Remember that homework is due at 6pm on the due date.

\subsection*{Problem 1 (3 points)}

Use structural induction to prove that for every $\ell$ we have
\begin{align*}
  \fn{length}(\fn{reverse}(\ell)) = \fn{length}(\ell).
\end{align*}

\noindent
You can use either the definition of $\fn{reverse}$ of $\fn{reverse'}$ from the textbook.

\subsection*{Problem 2 (3 points)}

In class we defined $\fn{size}(t)$ and $\fn{depth}(t)$ for any (extended) binary tree $t$.
Using those definitions, prove by structural recursion that for any tree $t$, we have
$\fn{size}(t) \le 2^{\fn{depth}(t)} - 1$.

\subsection*{Problem 3 (3 points)}

Recall the {\sf MU} puzzle by Douglas Hofstadter from the textbook and the lecture. 
It concerns strings consisting of the letters {\sf M}, {\sf I}, and {\sf U}.
Starting with the string {\sf MI}, we are allowed to apply any of the following rules:

\begin{enumerate}
\item Replace {\sf xI} by {\sf xIU}, that is, add a {\sf U} to the end of any string that ends with {\sf I}.
\item Replace {\sf Mx} by {\sf Mxx}, that is, double the string after the initial {\sf M}.
\item Replace {\sf xIIIy} by {\sf xUy}, that is, replace any three consecutive {\sf I}s with a {\sf U}.
\item Replace {\sf xUUy} by {\sf xy}, that is, delete any consecutive pair of {\sf U}s.
\end{enumerate}

\noindent 
Prove that you can produce any string {\sf MI...I}, that is, {\sf M} followed by only {\sf I}s, if the number
of {\sf I}s is not $0 \pmod 3$ when starting with string {\sf MI}.

\subsection*{Problem 4 (3 points)}

Using operations on {\sf List}, write a Lean function that for every $n$ returns
   the list of all the divisors of $n$ that are less than $n$.

\subsection*{Problem 5 (3 points)}

A natural number $n$ is \emph{perfect} if it is equal to the sum of the divisors less
   than $n$. Write a Lean function (with return type {\sf Bool}) that determines
   whether a number $n$ is perfect. Use it to find all the perfect numbers less
   than 1,000.

\subsection*{Problem 6 (3 points)}

Define a recursive function $\fn{sublists}(\ell)$ in Lean that,
for every list $\ell$, returns a list of all the sublists of $\ell$.
For example, given the list $[1, 2, 3]$, it should compute the list
\[
      [ [], [1], [2], [3], [1,2], [1,3], [2, 3], [1, 2, 3] ].
\]
The elements need not be listed in that same order.

\end{document}