\documentclass[11pt]{article}

\usepackage[margin=1.6in]{geometry}
\usepackage{proof}
\usepackage{amsmath,amsthm,amssymb}
\usepackage[colorlinks=true,linkcolor=black,urlcolor=black]{hyperref}

% font{
\usepackage{pxfonts}
%% fix sans serif
\renewcommand\sfdefault{cmss}
\DeclareMathAlphabet{\mathsf}{OT1}{cmss}{m}{n}
\SetMathAlphabet{\mathsf}{bold}{OT1}{cmss}{b}{n}
% }font

\theoremstyle{definition}
\newtheorem{task}{Task}

\newcommand\amp{\mathop{\&}}
\newcommand\anglepair[1]{\ensuremath{\langle\!\langle#1\rangle\!\rangle}}

\newcommand\pimp{\mathop{\supset}}
\newcommand\pand{\mathop{\wedge}}
\newcommand\por{\mathop{\vee}}
\newcommand\ptrue{\top}
\newcommand\pfalse{\bot}
\newcommand\pforall[3]{\forall #1{:}#2.\, #3}
\newcommand\pexists[3]{\exists #1{:}#2.\, #3}

\newcommand\tabort[1]{\mathsf{abort}\;#1}
\newcommand\tlam[3]{\lambda #1{:}#2.\,#3}
\newcommand\tinl[1]{\mathsf{in_1}\;M}
\newcommand\tinr[1]{\mathsf{in_2}\;M}
\newcommand\tcase[5]{\mathsf{case}(#1, #2.#3, #4.#5)}
\newcommand\tunit{\langle\rangle}
\newcommand\tpair[2]{\langle #1, #2 \rangle}
\newcommand\tfst[1]{\pi_1 #1}
\newcommand\tsnd[1]{\pi_2 #1}

\newcommand\true{\;\textit{true}}
\newcommand\ddd{\raisebox{0.2em}[1.3em]{$\vdots$}}
\newcommand\com{\raisebox{0.3em}{$\ ,\ \ $}}
\newcommand\hyp[2]{\infer[#1]{#2}{}}

\newcommand{\lred}{\mathrel{\raisebox{0.5em}{$\Longrightarrow_R$}}}
\newcommand{\lexp}{\mathrel{\raisebox{0.5em}{$\Longrightarrow_E$}}}

\newcommand{\jsub}[3]{[#1/#2]\;#3}

\newcommand{\DD}{\mathcal{D}}
\newcommand{\EE}{\mathcal{E}}
\newcommand{\FF}{\mathcal{F}}

\newcommand\tutchGuideURL{http://www.andrew.cmu.edu/course/15-317/software/tutch/doc/html/tutch_ovr.html}
\newcommand\tutchProofTermsURL{http://www.andrew.cmu.edu/course/15-317/software/tutch/doc/html/tutch_4.html\#SEC18}
\newcommand\tutchProofTermsRefURL{http://www.andrew.cmu.edu/course/15-317/software/tutch/doc/html/tutch_9.html\#SEC28}

\title{Constructive Logic (15-317), Fall 2012 \\
       Assignment 2: Proof Terms and Substitution}
\author{Carlo Angiuli \texttt{(cangiuli@cs)}}
\date{Out: Friday, September 14, 2012 \\
      Due: Thursday, September 20, 2012 (before class)}

\begin{document}
\maketitle

In this assignment, you will write proof terms and demonstrate your
understanding of substitution. The Tutch portion of your work
(Section~\ref{sec:tutch}) should be submitted electronically using the command
\begin{verbatim}
  $ /afs/andrew/course/15/317/bin/submit -r hw02 <files...>
\end{verbatim}
from any Andrew server.  You may check the status of your submission by
running the command
\begin{verbatim}
  $ /afs/andrew/course/15/317/bin/status hw02
\end{verbatim}
If you have trouble running either of these commands, email Carlo.

The written portion of your work (Sections \ref{sec:sub}, \ref{sec:uses}, and
\ref{sec:and}) should be submitted at the beginning of class. If you are
familiar with \LaTeX, you are encouraged to use this document as a template for
typesetting your solutions, but you may alternatively write your solutions
\textit{neatly} by hand.

\section{Tutch Proofs (15 points)}
\label{sec:tutch}

To give a proof term in Tutch, declare it with \texttt{term} rather than 
\texttt{proof}:
\begin{verbatim}
  term andComm : A & B => B & A =
    fn u => (snd u, fst u);
\end{verbatim}
For more examples, see \href{\tutchProofTermsURL}{Chapter~4} of the 
\href{\tutchGuideURL}{\textit{Tutch User's Guide}}.  The proof terms are 
very similar to the ones given in lecture (even more similar to ML) and are
summarized in \href{\tutchProofTermsRefURL}{Section~A.2.1} of the \textit{Guide}.

\begin{task}[15 pts]
  Prove the following theorems using Tutch:
\begin{verbatim}
term absurdity : (A & ~A) => B;
term demorgan : ~(A | B) => ~A & ~B;
term uncurry : (A => B => C) => (A & B => C);
term lemDne : (A | ~A) => (~~A => A);
term poe : (A | B) => ~A => B;
\end{verbatim}
\end{task}

On Andrew machines, you can check your progress against the requirements
file \texttt{/afs/andrew/course/15/317/req/hw02.req} by running the command
\begin{verbatim}
  $ /afs/andrew/course/15/317/bin/tutch -r hw02 <files...>
\end{verbatim}

\section{Substitution (6 points)}
\label{sec:sub}

Recall the definition of substitution given in lecture. To see how they
operate on particular terms, we can expand the definition iteratively until
no substitutions need be applied. Here is an example:
\begin{eqnarray*}
&& \jsub{(\tlam{x}{A}{x})}{f}{(f\;z)} \\
&=& (\jsub{(\tlam{x}{A}{x})}{f}{f})~(\jsub{\tlam{x}{A}{x}}{f}{z}) \\
&=& (\tlam{x}{A}{x})~z
\end{eqnarray*}

\begin{task}[6 points]
Show the step-by-step unpacking of the following substitutions, taking care
to avoid variable capture:
\begin{enumerate}
\item $\jsub{(f~y)}{x}{(\tlam{f}{A \pimp B}{(f~x)})}$
\item $\jsub{(f~y)}{x}{(x~(\tlam{x}{A}{y}))}$
\item $\jsub{(f~y)}{x}{(x~(\tlam{y}{A}{(f~y~x)}))}$
\end{enumerate}
\end{task}

\section{Verification and Uses (9 points)}
\label{sec:uses}

In this set of tasks, we will investigate how replacing the $\true$ judgment
with the $\uparrow$ and $\downarrow$ judgments affects the structure of proofs.
Assume $A$ and $B$ are atomic propositions.

\begin{task}[3 points]
Give \textit{two} different natural deduction proofs of $(A\pimp B)\pimp (A\pimp
B)\true$. How many natural deduction proofs of this judgment exist? Explain.
\end{task}

\begin{task}[3 points]
Give a natural deduction proof of $A\pimp A\true$. How many natural deduction
proofs of this judgment exist? Explain.
\end{task}

\begin{task}[3 points]
Give a proof of $A\pimp A\uparrow$. How many proofs of this judgment exist?
Explain.
\end{task}

\section{$\amp$er's Game (10 points)}
\label{sec:and}

\subsection{Uses and verifications}
Recall the $\amp$ connective defined in Homework 1:
\[
\infer[\amp I]
  {A\amp B\true}
  {A\true & B\true}
\qquad
\infer[\amp E_1]
  {C\true}
  {A\amp B\true & \deduce[\ddd]{C\true}{[A\true]}}
\qquad
\infer[\amp E_2]
  {C\true}
  {A\amp B\true & \deduce[\ddd]{C\true}{[B\true]}}
\]

\begin{task}[3 points]
Give use and verification rules corresponding to these introduction and
elimination rules. There may be more than one right answer.
\end{task}

\subsection{Proof terms}
Consider the following proof term assignment for the $\amp$ connective:
\[
\infer[\amp I]
  {\anglepair{M,N} : A\amp B}
  {M:A & N:B}
\qquad
\infer[\amp E_1]
  {p_1(M,x.N) : C}
  {M:A\amp B & \deduce[\ddd]{N:C}{[x:A]}}
\qquad
\infer[\amp E_2]
  {p_2(M,x.N) : C}
  {M:A\amp B & \deduce[\ddd]{N:C}{[x:B]}}
\]

\begin{task}[4 points]
Show all the local reduction(s) and expansion(s) for these rules in proof term
notation. Be sure to indicate which are reductions and which are expansions. You
do not need to include derivations for the proof terms.
\end{task}

\begin{task}[3 points]
Expand the definition of substitution given in lecture to the $\amp$ proof
terms.
\end{task}

\end{document}