\documentclass{article}

% Language setting
% Replace `english' with e.g. `spanish' to change the document language
\usepackage[english]{babel}

% Set page size and margins
% Replace `letterpaper' with`a4paper' for UK/EU standard size
\usepackage[letterpaper,top=1in,bottom=1in,left=1in,right=1in]{geometry}

% Useful packages
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{enumerate}
\usepackage{graphicx}
\usepackage{mathpartir}
\usepackage[colorlinks=true, allcolors=blue]{hyperref}

\title{CS 599 A1: Assignment 3}
\author{YOUR NAME, BU ID}
\date{}

\newcommand{\lc}{$\lambda$-calculus}

\newcommand{\m}[1]{\mathsf{#1}}
\newcommand{\pt}{\; \m{true}}
\newcommand{\mi}[1]{\mathit{#1}}
\newcommand{\mb}[1]{\mathbf{#1}}
\newcommand{\mt}[1]{\mathtt{#1}}
\newcommand{\elam}[2]{\lambda{#1}.\,{#2}}
\newcommand{\eapp}[2]{#1 \; #2}
\newcommand{\step}{\mapsto}
\newcommand{\val}[1]{#1 \; \m{value}}
\newcommand{\eval}{\Downarrow}
\newcommand{\num}[1]{\overline{#1}}
\newcommand{\numf}[1]{\underline{#1}}
\newcommand{\eif}[3]{\m{if} \; #1 \; \m{then} \; #2 \; \m{else} \; #3}
\newcommand{\multval}[1]{#1 \; \m{mult{-}value}}
\newcommand{\closed}[1]{#1 \; \m{closed}}
\newcommand{\tint}{\m{int}}
\newcommand{\tbool}{\m{bool}}
\newcommand{\elet}[3]{\m{let} \; #1 = #2 \; \m{in} \; #3}
\newcommand{\G}{\Gamma}
\newcommand{\R}[1]{\textcolor{red}{#1}}
\newcommand{\tfloat}{\m{float}}
\newcommand{\emptybox}{\boxed{\textcolor{white}{QWERTY}}}
\newcommand{\mstep}{\step^{*}}
\newcommand{\zero}{\m{zero}}
\renewcommand{\succ}[1]{\m{succ}(#1)}
\newcommand{\semi}{\,;\,}
\newcommand{\natrec}[5]{\m{natrec}(#1 \semi #2 \semi #3.\, #4. \, #5)}
\newcommand{\tnat}{\m{nat}}
\newcommand{\Red}{\m{Red}}
\newcommand{\natred}[1]{#1 \downarrow}
\newcommand{\issubst}{\Vdash}
\newcommand{\ift}{\m{int{-}or{-}float}}
\newcommand{\ecase}[3]{\m{case} \; #1 \; (#2 \Rightarrow #3)}
\newcommand{\ecaselr}[3]{\m{case} \; #1 \; (\m{inl} \Rightarrow #2 \mid \m{inr} \Rightarrow #3)}
\newcommand{\case}[2]{\m{case} \; #1 \; (#2)}
\newcommand{\erecv}[2]{#2 \leftarrow \m{recv} \; #1}
\newcommand{\esend}[2]{\m{send} \; #1 \; #2}
\newcommand{\esendl}[2]{#1.#2}
\newcommand{\ewait}[1]{\m{wait} \; #1}
\newcommand{\eclose}[1]{\m{close} \; #1}
\newcommand{\fwd}[2]{#1 \leftrightarrow #2}
\newcommand{\espawn}[3]{#1 \leftarrow #2 \; #3}
\newcommand{\ichoice}[1]{\oplus\{#1\}}
\newcommand{\echoice}[1]{\&\{#1\}}
\newcommand{\with}{\,\&\,}
\newcommand{\one}{\mathbf{1}}
\newcommand{\tensor}{\otimes}
\newcommand{\lolli}{\multimap}
\newcommand{\config}{\mathcal{C}}
\newcommand{\dc}{\mathcal{D}}
\newcommand{\D}{\Delta}
\newcommand{\T}{\Theta}
\newcommand{\poised}[1]{#1 \; \m{poised}}
\newcommand{\proc}[2]{\m{proc}(#1, #2)}
\newcommand{\msg}[2]{\m{msg}(#1, #2)}
\newcommand{\fresh}[1]{(#1 \; \m{fresh})}
\newcommand{\up}{\,\uparrow^{\m{S}}_{\m{L}}}
\newcommand{\down}{\,\downarrow^{\m{S}}_{\m{L}}}

\newcommand{\cons}{\mathcal{C}}
\newcommand{\vars}{\mathcal{V}}
\newcommand{\proves}{\vDash}

\newcommand{\tforall}[1]{\forall #1. \, }
\newcommand{\texists}[1]{\exists #1. \, }
\newcommand{\tassertop}{{?}}  % -fp was: ?
\newcommand{\tassumeop}{{!}}  % -fp was: !
\newcommand{\tassert}[1]{\tassertop\{#1\}. \,} % -fp was: \; \tassertop
\newcommand{\tassume}[1]{\tassumeop\{#1\}. \,} % -fp was: \; \tassumeop

\newcommand{\esendn}[2]{\m{send} \; #1 \; \{#2\}}
\newcommand{\erecvn}[2]{\{#2\} \leftarrow \m{recv} \; #1}
\newcommand{\eassume}[2]{\m{assume} \; #1 \; \{#2\}}
\newcommand{\eassert}[2]{\m{assert} \; #1 \; \{#2\}}
\newcommand{\eimposs}{\m{impossible}}

\newcommand{\epair}[2]{\langle #1, #2 \rangle}
\newcommand{\letpair}[4]{\m{let} \; \langle #1, #2 \rangle = #3 \; \m{in} \; #4}
\newcommand{\inl}[1]{\m{inl}(#1)}
\newcommand{\inr}[1]{\m{inr}(#1)}
\newcommand{\match}[5]{\m{match} \; #1 \; \m{with} \; \{\,\m{inl}(#2) \to #3 \mid \m{inr}(#4) \to #5\,\}}
\newcommand{\letapp}[4]{\m{let} \; #1 = #2 \; #3 \; \m{in} \; #4}

\newcommand{\limpl}{\supset}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Real}{\mathbb{R}}
\newcommand{\seq}{\Longrightarrow}

\newtheorem{problem}{Problem}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}
\newenvironment{solution}{\textbf{Solution.}}{}

\makeatletter
\def\arcr{\@arraycr}
\makeatother


\begin{document}
\maketitle

\begin{problem}[Mandatory; No LLM; 60 pts]
For the following sequents, either provide a proof using rules of sequent calculus
or explain why none exists.
\begin{enumerate}[(i)]
    \item $(A \limpl (B \limpl C)) \seq (A \land B) \limpl C$
    \item $A \seq \neg \neg A$
    \item $(\neg A \lor \neg B) \seq \neg (A \land B)$
    \item $(A \land (B \lor C)) \seq (A \land B) \lor (A \land C)$
    \item $A \limpl B \seq \neg B \limpl \neg A$
    \item $(A \limpl B) \limpl B \seq \neg \neg A \limpl B$
\end{enumerate}
\end{problem}

\begin{solution}
    YOUR SOLUTION GOES HERE
\end{solution}


\begin{problem}[Mandatory; No LLM; 20 pts]
Provide sequent calculus rules for universal and existential quantification. In particular, provide:
\begin{enumerate}[(i)]
    \item Right rule for $\G \seq \forall x. A(x)$.
    \item Left rule for $\G, \forall x. A(x) \seq C$.
    \item Right rule for $\G \seq \exists x. A(x)$.
    \item Left rule for $\G, \exists x. A(x) \seq C$.
\end{enumerate}
\end{problem}

\begin{solution}
    YOUR SOLUTION GOES HERE
\end{solution}

\begin{problem}[Mandatory; No LLMs; 20 pts]
~
\begin{itemize}
    \item The introduction rules for lists are defined as follows:
    \begin{mathpar}
        \inferrule*[right=ListI$_n$]
        { }
        {\m{nil} : \tau \; \m{list}}
        \and
        \inferrule*[right=ListI$_c$]
        {x : \tau \and \ell : \tau \; \m{list}}
        {\m{cons}(x, \ell) : \tau \; \m{list}}
    \end{mathpar}
    Design the corresponding elimination rule for lists.

    \item The introduction rules for trees are defined as follows:
    \begin{mathpar}
        \inferrule*[right=TreeI$_l$]
        { }
        {\m{leaf} : \tau \; \m{tree}}
        \and
        \inferrule*[right=TreeI$_n$]
        {x : \tau \and \ell : \tau \; \m{tree} \and r : \tau \; \m{tree}}
        {\m{node}(x, \ell, r) : \tau \; \m{tree}}
    \end{mathpar}
    Design the corresponding elimination rule for trees.
\end{itemize}
\end{problem}

\begin{solution}
    YOUR SOLUTION GOES HERE
\end{solution}


\end{document}