\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}
\newcommand{\liff}{\leftrightarrow}
% 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 5}

\medskip

due 6pm Thursday, October 7, 2021
\end{center}

\medskip

\thispagestyle{fancy}

\subsection*{Problem 1 (3 points)}

Remember the definition of substitution for propositional formulas:
\begin{align*}
  A[B/p] &= B \quad \text{if $A$ is the variable $p$} \\
  A[B/p] &= A \quad \text{if $A$ is any other atomic formula} \\
  (\lnot A)[B/p] &= \lnot (A[B/p]) \\
  (A_0 \star A_1)[B/p] &= A_0[B/p] \star A_1[B/p] \quad \text{for any binary connective $\star$}
\end{align*}
Remember also that a \emph{truth assignment} $\tau$ is a function that assigns a truth value
$\top$ or $\bot$ to each variable. If $\tau$ is such a truth assignment, $p$ is a variable,
and $b$ is a truth value, $\tau[p \mapsto b]$ is the function defined by
\[
  (\tau[p \mapsto b])(q) =
     \begin{cases}
        b & \text{if $q$ is $p$} \\
        \tau(q) & \text{otherwise}
     \end{cases}
\]
In other words, $\tau[p \mapsto b]$ is the (possible) modification of $\tau$ that maps $p$ to
$b$ and leaves the rest of the assignment the same.

Prove that for any $A$, $B$, $p$, and $\tau$,
\[
  \tval{A[B/p]}_\tau = \tval{A}_{\tau[p \mapsto \tval{B}_\tau]}.
\]
In other words, we can evaluate $A[B/p]$ at $\tau$ by evaluating $B$ at $\tau$, and then evaluating
$A$ with $p$ replaced by that result.

\subsection*{Problem 2 (2 points)}

Use the previous problem to show that for any $A$, $B$, and $p$, if $A$ is valid, then
$A[B/p]$ is valid.

\subsection*{Problem 3 (3 points)}

Consider the formula $p_1 \liff p_2 \liff \cdots \liff p_n$. Convince yourself that this formula is true
if and only if an even number of variables are assigned the value \emph{false}.

Prove that the smallest CNF formula that is equivalent to this must have
at least $2^{n-1}$ clauses. 
(Hint: it suffices to show that any DNF formula equivalent to the negation, which says that an odd
number of variables are false, has to have at least $2^{n-1}$ cubes. Start by showing that in any
such DNF formula, each cube has to contain all the variables.)
%(Hint: first argue that each clause has to include all the variables either
%positively or negatively.)

\subsection*{Problem 4 (3 points)}

Write a function in Lean that implements substitution for propositional formulas, and test it on one or two examples.

% TODO: an alternative: write a function that turns a {\tt CnfForm} into a {\tt PropForm}.

\subsection*{Problem 5 (4 points)}

In class and in the textbook, we discuss a Lean function {\tt PropForm.eval} that
evaluates a propositional formula with respect to a truth assignment.
Define a similar function, {\tt CnfForm.eval}, that evaluates a formula in conjunctive
normal form. (Do it directly: don't translate it to a propositional formula.)

\subsection*{Problem 6 (4 points)}

In class and in the textbook, we define a Lean data type {\tt NnfForm} for NNF formulas,
and we define a function {\tt PropForm.toNnfForm} that converts a propositional formula
to one in NNF. Notice that the method we used to expand $\liff$ can lead to an exponential
increase in length.

Define a Lean data type {\tt EnnfForm} for \emph{extended} negation normal form formulas,
which adds the $\liff$ connective to ordinary NNF. Then define a function that translates any propositional
formula to an extended NNF formula.

\end{document}