![用于序列微积分证明的自定义环境](https://linux22.com/image/435932/%E7%94%A8%E4%BA%8E%E5%BA%8F%E5%88%97%E5%BE%AE%E7%A7%AF%E5%88%86%E8%AF%81%E6%98%8E%E7%9A%84%E8%87%AA%E5%AE%9A%E4%B9%89%E7%8E%AF%E5%A2%83.png)
我正在使用该软件包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}
我现在想改变的是:
- 环境默认居中,但可以通过可选参数更改对齐方式
- 缩短命令名称:分别为
\Axiom
become\ax
、\RightLabel
become\rlab
、\LeftLabel
\llab
、\UnaryInf
、\BinaryInf
、\TrinaryInf
和\QuaternaryInf
become 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 新手,担心这个项目太大,我一个人无法完成。有谁能帮我吗?
答案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}