\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}
\newcommand{\D}{\Delta}
\newtheorem{lemma}{Lemma}
\newcommand{\seq}{\longrightarrow}
\newcommand{\nat}{\textsf{nat}}
\newcommand{\even}{\textsf{even}}
\newcommand{\odd}{\textsf{odd}}
\newcommand{\s}{\textsf{s}}

\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 4: Sequent Calculus and Natural Numbers}
\author{Carlo Angiuli \texttt{(cangiuli@cs)}}
\date{Out: Thursday, September 27, 2012 \\
      Due: Thursday, October 4, 2012 (before class)}

\begin{document}
\maketitle

In this assignment, you will prove metatheorems about sequent calculus, and
propositions about natural numbers.

\section{Contraction (20 points)}
\label{sec:contr}

The contraction lemma for sequent calculus states that two equal propositions on
the left of a sequent can be replaced by a single instance:

\begin{lemma}[Contraction]
If $\D,A,A\seq D$, then $\D,A\seq D$.
\end{lemma}

We can prove contraction by structural induction on the derivation
$\D,A,A\seq D$, in a similar fashion to the proofs of the substitution and
weakening lemmas for natural deduction.

\begin{task}[20 points]
Prove contraction for the $\pimp,\land$ fragment of sequent calculus. That is,
show the cases of the proof where the last rule to be applied is:
\begin{itemize}
\item $\mathsf{init}$
\item $\pimp R$
\item $\pimp L$
\item $\land R$
\item $\land L_1$
\end{itemize}
You don't need to show the $\land L_2$ case, because it is very similar to the
$\land L_1$ case.
\end{task}

\section{Derivability and Admissibility (10 points)}
\label{sec:deriv}

\begin{task}[10 points]
For each of the following sequent calculus rules, state whether or not it is
derivable, and whether or not it is admissible. Explain.

\[
\infer[(1)]
  {\D,A\seq D}
  {\D,A,A\seq D}
\qquad
\infer[(2)]
  {\D,A\land B\seq A}
  {A\textit{ atomic}}
\]

\[
\infer[(3)]
  {\D,A,A\pimp B\seq B}
  {}
\qquad
\infer[(4)]
  {\D\seq C}
  {\D\seq A & \D,A\seq C}
\]
\end{task}

\section{Natural numbers (10 points)}
\label{sec:nat}

In recitation, we saw how to define the natural numbers as a data type, and
prove theorems quantified over them. We also defined the $\even$ and $\odd$
predicates on natural numbers:
\[
\infer{\even(0)}{}
\qquad
\infer{\even(\s(n))\true}{n:\nat & \odd(n)\true}
\qquad
\infer{\odd(\s(n))\true}{n:\nat & \even(n)\true}
\]

\begin{task}[5 points]
Derive the following judgment:
\[ \forall n:\nat.(\even(n)\pimp\even(\s(\s(n))))\true \]
\end{task}

\begin{task}[5 points]
Derive the following judgment:
\[ \forall n:\nat.(\even(n)\lor\even(\s(n)))\true \]
\end{task}

\end{document}