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?