\documentclass{article}
\usepackage{graphicx}
\usepackage[colorlinks=true,urlcolor=blue,linkcolor=blue,citecolor=blue]{hyperref}%
\usepackage{fancyhdr}
\usepackage[margin=35mm]{geometry}
\usepackage{amsmath}
\usepackage{stmaryrd}   % for the tval symbol
\usepackage{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{trees}
\newcommand{\fn}[1]{\mathrm{#1}}
\newcommand{\append}{\mathbin{+\mkern-10mu+}}
\newcommand{\cons}{\mathbin{::}}
\newcommand{\tval}[1]{\llbracket #1 \rrbracket}
% If you don't have the stmaryrd package, the following substitute will do.
%\newcommand{\tval}[1]{[\![ #1 ]\!]}

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

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


\begin{document}

\bigskip

\begin{center}
{\Large Assignment 4}

\medskip

due 6pm Thursday, September 23, 2021
\end{center}

\medskip

\thispagestyle{fancy}


\subsection*{Problem 1 (3 points)}

Consider a variation of the Towers of Hanoi puzzle where we assume the pegs
$A$, $B$, and $C$ are in a row, and we are only allowed to transfer a disk to
an \emph{adjacent} peg, which is to say, moves from $A$ to $C$ or vice-versa
are ruled out. Convince yourself that the following algorithm works:

\medskip

\begin{algorithmic}
  \Procedure{hanoiAdj}{$n, A, B, C$}
  \If {$n = 0$}
    \State \textbf{return}
  \Else
    \State move $n - 1$ disks from $A$ to $C$
    \State move the last disk from $A$ to $B$
    \State move $n - 1$ disks from $C$ to $A$
    \State move the last disk from $B$ to $C$
    \State move $n - 1$ disks from $A$ to $C$
  \EndIf
  \EndProcedure
\end{algorithmic}

\medskip

\noindent
Write a Lean program to output the list of moves required to move $n$ disks.
(For an extra challenge, try to figure out how many steps it takes.)

\subsection*{Problem 2 (4 points)}

A binary tree with nodes labeled from a datatype $\alpha$ is just what it sounds like.
For example, the following is a binary tree with nodes labeled by natural numbers:
\begin{center}
    \begin{tikzpicture}
    \node [circle,draw]{5} [level distance=10mm,sibling distance=25mm]
    child { node [circle,draw]{7} [level distance=10mm ,sibling distance=15mm]
      child[missing] {}
      child {node [circle,draw]{3}}}
    child {node [circle,draw] {6} [level distance=10mm ,sibling distance=15mm]
      child {node [circle,draw] {4}}
      child {node [circle,draw]{2}}
    };
    \end{tikzpicture}
\end{center}
As in the textbook, by ``binary tree'' we really mean ``extended binary tree,''
which means that we count the empty tree.

\medskip

\noindent
Do the following:
\begin{enumerate}
    \item Define a datatype $\mathsf{LBinTree} \; \alpha$ in Lean.
      It should be similar to $\mathsf{BinTree}$, as defined in the textbook,
      but the node constructor should include the label, like the $\mathsf{cons}$
      constructor for $\mathsf{List}$.
    \item Define $\mathsf{myTree} \; : \; \mathsf{LBinTree} \; \mathsf{Nat}$
      corresponding to the example above.
    \item Define a function $\mathsf{addNodes} \; : \;
      \mathsf{LBinTree} \; \mathsf{Nat} \to \mathsf{LBinTree} \; \mathsf{Nat}$
      that adds up the nodes of a tree with labels from $\mathsf{Nat}$.
      On the example above, it should return 27.
    \item Define a function $\mathsf{toListInorder}$ that creates a list with an
      \emph{inorder} traversal (left subtree first, then the node, then the right subtree).
      On the example above, it should return $[7, 3, 5, 4, 6, 2]$.
\end{enumerate}

\subsection*{Problem 3 (3 points)}

Write a Lean procedure $\mathsf{pascal}$ which, on input $n$, outputs
the first $n$ rows of Pascal's triangle. We adopt the convention that
the row numbers start with $0$, so the row numbered $n$ should have $n + 1$ entries,
$\binom{n}{0}, \binom{n}{1}, \ldots, \binom{n}{n}$.
For example, on input $6$, the program should output the following:
\begin{verbatim}
    0: 1
    1: 1 1
    2: 1 2 1
    3: 1 3 3 1
    4: 1 4 6 4 1
    6: 1 5 10 10 5 1
\end{verbatim}

\subsection*{Problem 4 (3 points)}

Use the definition of ``$A$ is a subformula of $B$'' in Section 4.1 to prove
that if $A$, $B$, and $C$ are any propositional formulas,
$A$ is a subformula of $B$, and $B$ is a subformula of $C$,
then $A$ is a subformula of $C$.

\medskip

\noindent (Hint. This is tricky. Remember that, by definition,
``$A$ is a subformula of $B$'' means $A \in \fn{subformulas}(B)$.
Show by induction $C$ that for every $A$ and $B$,
if $A$ is a subformula of $B$ and $B$ is a subformula of $C$,
then $A$ is a subformula of $C$.)

\subsection*{Problem 5 (2 points)}

Prove the following carefully, using the semantic definitions in Section 4.2:
let $\Gamma$ and $\Gamma'$ be sets of propositional formulas and let $A$ be a propositional formula.
If $\Gamma \models A$ and $\Gamma' \supseteq \Gamma$, then $\Gamma' \models A$.

\subsection*{Problem 6 (2 points)}

Prove the following carefully: $\{ A \to B, A \} \models B$.

\subsection*{Problem 7 (2 points)}

Use an algebraic calculation to prove $(A \to B) \land A \equiv A \land B$,
using the equivalences in Section 4.3 and the
equivalence $U \to V \equiv \lnot U \lor V$.

\subsection*{Problem 8 (2 points)}

Use an algebraic calculation to prove $(A \to B) \lor \lnot A \equiv A \to B$.
You can carry out multiple applications of associativity and commutativity of $\lor$
in one step.

\end{document}