Custom environment for sequent calculus proofs

Question

I'm using the package bussproofs to typeset sequent calculus proofs with LaTeX. Whilst I'm more than satisfied with the results, writing the code is cumbersome. Thus, I'd like to define a custom environment to make my life a little easier. Normally, I would write code like this:

\documentclass{article}
\usepackage{bussproofs}
\usepackage{amsmath}
\begin{document}
\begin{center}
    \begin{prooftree}
\def\fCenter{\mbox{\Large$\Rightarrow$}}
\Axiom$\alpha  \ \fCenter\ \alpha$
\Axiom$\beta   \ \fCenter\ \beta$
\RightLabel{FEA}
\BinaryInf$\alpha \to \beta, \alpha \ \fCenter\  \beta$
\RightLabel{UEA}
\UnaryInf$ (\alpha \to \beta) \land \alpha, \alpha \  \fCenter\ \beta$
\RightLabel{UEA}
\UnaryInf$ (\alpha \to \beta) \land \alpha, (\alpha \to \beta )\land \alpha \  \fCenter\ \beta$
\RightLabel{Contract}
\UnaryInf$ (\alpha \to \beta) \land \alpha \  \fCenter\ \beta$
\RightLabel{FES}
\UnaryInf$\  \fCenter\  (\alpha \to \beta) \land \alpha \to \beta$
\end{prooftree}
\end{center}
\end{document}

What I'd like to change now is this:

• the environment is centered by default but the alignment can be changed by an optional argument
• shorten the command names: \Axiom becomes \ax, \RightLabel becomes \rlab, \LeftLabel \llab, \UnaryInf, \BinaryInf, \TrinaryInf, \QuaternaryInf and \QuinaryInf become \inf1 to \inf5, respectively
• \ax and the inference commands take the respective sequent as a mandatory argument; this argument is in math-mode by default so you don't need dollar signs
• instead of \ \fCenter\, => is used to denote the alignment and automatically prints \Rightarrow (as defined in the very first line of the environment).

In the end, the proof displayed above should look something like this:

\documentclass{article}
\usepackage{bussproofs}
\usepackage{amsmath}
\begin{document}
\begin{scproof}
  \ax{\alpha => \alpha}
  \ax{\beta  => \beta}
  \rlab{FEA}
  \inf2{\alpha \to \beta, \alpha => \beta}
  \rlab{UEA}
  \inf1{(\alpha \to \beta) \land \alpha, \alpha => \beta}
  \rlab{UEA}
  \inf1{(\alpha \to \beta) \land \alpha, (\alpha \to \beta) \land \alpha => \beta}
  \rlab{Contract}
  \inf1{(\alpha \to \beta) \land \alpha => \beta}
  \rlab{FES}
  \inf1{=> (\alpha \to \beta) \land \alpha \to \beta}
\end{scproof}
\end{document}

I'm new to LaTeX and afraid this is too big of a project to handle on my own. Is there someone who can help me out?

Answer 1

Here's an implementation as you desire.

I'd never do \mbox{\Large$\Rightarrow$} with additional spaces around, so I used \implies.

\documentclass{article}
\usepackage{bussproofs}
\usepackage{amsmath}

\makeatletter
\newcommand{\vitus@ax}[1]{\vitus@@ax$#1$}
\def\vitus@@ax$#1=>#2${\Axiom$#1\fCenter#2$}
\newcommand\vitus@inf[2]{\vitus@@inf{#1}$#2$}
\def\vitus@@inf#1$#2=>#3${%
  \ifcase#1\or
  \expandafter\UnaryInf\or
  \expandafter\BinaryInf\or
  \expandafter\TernaryInf\or
  \expandafter\QuaternaryInf\or
  \expandafter\QuinaryInf\fi
  $#2\fCenter#3$%
}
\newenvironment{scproof}
 {% make the new user interface
  \let\ax\vitus@ax
  \let\inf\vitus@inf
  \let\rlab\RightLabel
  \def\fCenter{\implies}%
  % start the prooftree
  \prooftree
 }
 {\endprooftree}
\makeatother

\begin{document}

\begin{prooftree}
\def\fCenter{\implies}
\Axiom$\alpha  \fCenter\alpha$
\Axiom$\beta   \fCenter\beta$
\RightLabel{FEA}
\BinaryInf$\alpha \to \beta, \alpha \fCenter \beta$
\RightLabel{UEA}
\UnaryInf$ (\alpha \to \beta) \land \alpha, \alpha  \fCenter\beta$
\RightLabel{UEA}
\UnaryInf$ (\alpha \to \beta) \land \alpha, (\alpha \to \beta )\land \alpha  \fCenter\beta$
\RightLabel{Contract}
\UnaryInf$ (\alpha \to \beta) \land \alpha  \fCenter\beta$
\RightLabel{FES}
\UnaryInf$ \fCenter (\alpha \to \beta) \land \alpha \to \beta$
\end{prooftree}

\begin{scproof}
  \ax{\alpha => \alpha}
  \ax{\beta  => \beta}
  \rlab{FEA}
  \inf2{\alpha \to \beta, \alpha => \beta}
  \rlab{UEA}
  \inf1{(\alpha \to \beta) \land \alpha, \alpha => \beta}
  \rlab{UEA}
  \inf1{(\alpha \to \beta) \land \alpha, (\alpha \to \beta) \land \alpha => \beta}
  \rlab{Contract}
  \inf1{(\alpha \to \beta) \land \alpha => \beta}
  \rlab{FES}
  \inf1{=> (\alpha \to \beta) \land \alpha \to \beta}
\end{scproof}

\end{document}