用于序列微积分证明的自定义环境

Question

我正在使用该软件包bussproofs用 LaTeX 排版连续微积分证明。虽然我对结果非常满意，但编写代码却很麻烦。因此，我想定义一个自定义环境，让我的生活更轻松一些。通常，我会编写如下代码：

\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}

我现在想改变的是：

• 环境默认居中，但可以通过可选参数更改对齐方式
• 缩短命令名称：分别为\Axiombecome \ax、\RightLabelbecome \rlab、\LeftLabel \llab、\UnaryInf、\BinaryInf、\TrinaryInf和\QuaternaryInfbecome to \QuinaryInf。\inf1\inf5
• \ax推理命令将相应的序列作为强制参数；此参数默认处于数学模式，因此不需要美元符号
• 而不是\ \fCenter\，=>用于表示对齐并自动打印\Rightarrow（如环境第一行所定义）。

最后，上面显示的证明应该是这样的：

\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}

我是 LaTeX 新手，担心这个项目太大，我一个人无法完成。有谁能帮我吗？

Answer 1

这是您所期望的实现。

我从来不会\mbox{\Large$\Rightarrow$}在周围留有额外的空格，因此我使用了\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}