\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\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{\G}{\Gamma}
\newtheorem{lemma}{Lemma}
\newcommand{\seq}{\longrightarrow}

\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 3: Quantifiers and Metatheorems}
\author{Carlo Angiuli \texttt{(cangiuli@cs)}}
\date{Out: Thursday, September 20, 2012 \\
      Due: Thursday, September 27, 2012 (before class)}

\begin{document}
\maketitle

In this assignment, you will prove propositions with quantifiers ($\forall$ and
$\exists$), and prove metatheorems about natural deduction and sequent calculus.

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 hw03 <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 hw03
\end{verbatim}
If you have trouble running either of these commands, email Carlo.

The written portion of your work (Sections~\ref{sec:weak},~\ref{sec:unprove})
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}

For quantifiers, you'll need a little bit of new syntax:
\begin{itemize}
\item $\forall x:\tau.A$ is written \verb|!x:t.A|

\item $\exists x:\tau.A$ is written \verb|?x:t.A|
\item The existential elimination rule requires a hypothetical with two 
  assumptions.  These are written by separating the assumptions with a
  comma.  For example:
\begin{verbatim}
proof exp : (?x:t.A(x)) => ?x:t.A(x) =
begin
[(?x:t.A(x));
 [a:t , A(a);
  ?x:t.A(x)];
 ?x:t.A(x)];
(?x:t.A(x)) => ?x:t.A(x);
end;
\end{verbatim}

\end{itemize}

\begin{task}[15 points]
Prove the following theorems using Tutch.

\begin{verbatim}
proof weak : (!x:t. P(x) => (?y:t. P(y)));
proof dm : ~(?x:t.P(x)) => (!x:t.~P(x));
proof emp : (!x:t. P(x) => Q(x)) => (?x:t. P(x)) => (?x:t. Q(x));
proof compose : (!x:t. P(x) => Q(x)) => (!x:t. Q(x) => R(x))
                  => (!x:t. P(x) => R(x));
proof deor : ((?x:t. P(x)) | (?x:t. Q(x))) => (?x:t. P(x) | Q(x));
\end{verbatim}
\end{task}

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

\section{Weakening (13 points)}
\label{sec:weak}

The weakening lemma states that typing judgments hold in the presence of
additional variables. Formally:

\begin{lemma}[Weakening]
If $\G\vdash M:B$ and $x\not\in\G$, then $\G,x:A\vdash M:B$.
\end{lemma}

We can prove weakening by structural induction on the typing derivation
$\G\vdash M:B$, in a similar fashion to the proof of the substitution lemma
presented in lecture.

\begin{task}[13 points]
Prove weakening for the $\pimp$ fragment of our logic. That is, show the cases
of the proof where the last rule to be applied is:
\begin{itemize}
\item The hypothesis (variable) rule
\item $\pimp I$
\item $\pimp E$
\end{itemize}
\end{task}

\section{Sequent Calculus (12 points)}
\label{sec:unprove}

\begin{task}[3 points]
Assuming $A$ and $B$ are atomic propositions, give a sequent calculus derivation
of:
\[ \cdot\seq (A\lor \lnot A)\pimp (((A\pimp B)\pimp A)\pimp A) \]
\end{task}

We claimed in lecture that it is much easier to demonstrate unprovability (and
related results) in sequent calculus than natural deduction.

\begin{task}[3 points]
Assuming $A$ is an atomic proposition, show there is \emph{no} proof of:
\[ \cdot\seq (\lnot A)\pimp A \]
\end{task}

\begin{task}[3 points]
Assuming $A$ and $B$ are (distinct) atomic propositions, show there is \emph{no}
proof of:
\[ \cdot\seq (A\lor B)\pimp (A\land B) \]
\end{task}

\begin{task}[3 points]
Assuming $A$ is an atomic proposition, show there is \emph{exactly one} proof
of:
\[ \cdot\seq A\pimp A \]
\end{task}

\end{document}