derivations.tex

\documentclass{article}
\usepackage{mathpartir}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{ifxetex,ifluatex}
\usepackage{unicode-math}
\usepackage{booktabs}
\usepackage{minted}
\usepackage{float}
\usepackage{listings}
\usepackage{cite}
\usepackage[toc,page]{appendix}
\usepackage{xspace}
\usepackage{pdfpages}
\usepackage{lastpage}
\usepackage{fancyhdr}
\usepackage[a4paper,left=0.5cm,right=0.5cm,top=2.5cm,bottom=2.5cm]{geometry}
\usepackage[cm]{sfmath}
\usepackage{verbatim}


\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\idty}[0]{∀α.\ α → α}
\newcommand{\dblArr}[0]{⇒\mkern-9mu⇒}
\newcommand{\ahat}[0]{\hat{α}}
\newcommand{\subt}[0]{\mathbin{\mathtt{<:}}}

\newcommand{\Sub}[0]{\quad \textsc{[Sub]}}
\newcommand{\Var}[0]{\quad \textsc{[Var]}}
\newcommand{\arrE}[0]{\quad \textsc{[→E]}}
\newcommand{\id}[0]{\textsf{id}}

\begin{comment}

                                                  --------------------------- InstRSolve
                                                   Γ,^α ⊢ 1 =<: ^α ⊣ Γ,^α=1
                                               ------------------------------------- InstantiateR
                         Γ,^α ⊢ () ⇒ 1 ⊣ Γ,^α   Γ,^α ⊢ 1 <: α ⊣ Γ,^α=1
                         ------------------------------------------------------------ Sub
                                Γ,^α ⊢ () ⇐ ^α ⊣ Γ,^α=1
                         ------------------------------------- →App
                           Γ,^α ⊢ ^α → ^α ∙ () ⇒⇒ ^α ⊣ Γ,^α=1
                          ------------------------------------- ∀App
 Γ ⊢ id ⇒ ∀a. a → a ⊣ Γ     Γ ⊢ (∀a. a → a) ∙ () ⇒⇒ ^α ⊣ Γ,^α=1
 --------------------------------------------------------------- →E     ----------------------------------------------- <:Unit
 Γ ⊢ id () ⇒ ^α ⊣ Γ,^α=1                                                Γ,^α=1 ⊢ 1 <: 1 ⊣ Γ,^α=1
 ---------------------------------------------------------------------------------------------------------------------- Sub
 Γ ⊢ id () ⇐ 1 ⊣ Γ,^α=1
\end{comment}

\begin{document}


Let $Γ = ⋅, \id : \idty$
\section{Check $Γ ⊢ \id\ () ⇐ 1$}
\begin{mathpar}

\inferrule* [right=Sub] {
  \inferrule* [right=→E] {
    \inferrule* [right=Var] { }{Γ ⊢ x ⇒ \idty ⊣ Γ} \and
    \inferrule* [right=$∀$App] {
      \inferrule* [right=→App] {
        \inferrule* [right=Sub]
        { Γ,\ahat ⊢ () ⇒ 1 ⊣ Γ,\ahat \and T_3 }
        { Γ,\ahat ⊢ () ⇐ \ahat ⊢ Γ,\ahat=1 }
      } {Γ,\ahat ⊢ \ahat → \ahat ∙ () \dblArr \ahat ⊣ Γ,\ahat=1}
    } {Γ ⊢ (\idty) ∙ () \dblArr \ahat ⊣ Γ,\ahat=1}
  } {Γ ⊢ \id\ () ⇒ \ahat ⊣ Γ,\ahat=1} \and T_2
} {Γ ⊢ \id\ () ⇐ 1 ⊣ Γ,\ahat=1}

\\
T_2 = \inferrule* [right=\code{<:}Unit]
  { }
  { Γ,\ahat=1 ⊢ 1 \subt 1 ⊣ Γ,\ahat=1 }

\\
T_3 = \inferrule* [right=InstantiateR]
          { \inferrule* [right=InstRSolve]
            { }
            { Γ,\ahat ⊢ 1 =<: \ahat ⊣ Γ,\ahat=1 }
          }
          { Γ,\ahat ⊢ 1 \subt α ⊣ Γ,\ahat=1 }
\end{mathpar}
\end{document}