编辑：请参阅下面的原始问题
我接到了一项关于重新 TeX 的伟大任务，即将丢失的 LaTeX 源的 PDF 原件转换回 LaTeX，我得到了建议使用它bussproof.sty来重新创建一堆证明。https://github.com/leanprover/logic_and_proof/blob/master/bussproofs.sty
https://www.math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/BussGuide2_Smith2012.pdf
到目前为止一切顺利 - 效果很好（一般来说）。但是，由于许多证明都相当冗长，因此需要引用每个证明的单行。
这就是为什么有必要枚举每行，最好是数字左对齐（见原文），自动增加，并且可以从某个数字开始（不一定从 1 开始），因为有些证明必须在更大的文本部分之后继续 - 类似于\begin{enumerate}[label=\roman*.,start=3]或...[resume]。每行的正常标签应该可以参考。我不能使用 bussproof 标签进行枚举作为解决方法，因为它们位于推理线的高度，并且就在行旁边（左对齐或右对齐）。这是我到目前为止可以管理的（没有枚举）：
一个非常简短的代码示例：
\documentclass[11pt]{article}
\usepackage{bussproofs}
\begin{document}
no enumeration of single lines of the proof :(
\begin{prooftree}
\Axiom$\Gamma\left[\langle\mbox{A}\rangle\right] \fCenter\ \Rightarrow \mbox{C}$
\RightLabel{($\ast$)}
\UnaryInf$\Gamma\left[\mbox{A}\right] \fCenter\ \Rightarrow \mbox{C}$
\end{prooftree}
\end{document}
有人知道如何在这些证明中设置左对齐枚举吗？
编辑：使用 Alan Munn 给出的很好的解决方案，出现了一些其他问题：
对于我来说这仍然有点火箭科学，因为我不熟悉tikz和相关的软件包，但我猜最神奇的事情发生在那里......
使用您的解决方案进行的第一次测试让我得出以下观察结果：
（1）错误的顺序行枚举：有点busproofs太聪明了，因为一旦证明变得更加复杂，一些公理必须在相当远的行上指定（与简单直接的层次结构相比）。我包括一个简单的（！）示例，它已经显示行 1 和 2 不再处于正确的顺序（归咎于bussproofs！）。
\def\ciOneL{$\circ_{1l}$}
\def\ciTwo{$\circ_2$}
\begin{prooftree}
% switch to \Numberstrue automatically as soon as the first \lnum is used
\AxiomC{\lnum v$_1$ $\Rightarrow$ tv$/_2$vp} % 2. line left
\AxiomC{\lnum v$_2$ $\Rightarrow$ tv} % 1. line mid
\AxiomC{np$_3$ $\Rightarrow$ np} % 1. line right
\RightLabel{\scriptsize{[$/_{1l}$E]}}
\BinaryInfC{v$_2$ \ciOneL\ np$_3$ $\Rightarrow$ vp} % 2. line mid
\RightLabel{\scriptsize{[$/_2$E]}}
\BinaryInfC{\lnum (v$_1$ \ciTwo\ (v$_2$ \ciOneL\ np$_3$)) $\Rightarrow$ tv} % 3. line left
\AxiomC{np$_2$ $\Rightarrow$ np} % 3. line right
\RightLabel{\scriptsize{[$/_{1l}$E]}}
\BinaryInfC{\lnum ((v$_1$ \ciTwo\ (v$_2$ \ciOneL\ np$_3$)) \ciOneL\ np$_2$) $\Rightarrow$ vp \label{proofline:correct-word-order}} % 4. line (mid)
\RightLabel{\scriptsize{[MP]}}
\UnaryInfC{\lnum ((v$_1$ \ciOneL\ np$_2$) \ciTwo\ (v$_2$ \ciOneL\ np$_3$)) $\Rightarrow$ vp} % 5. line (mid)
\end{prooftree}
Applying MP in line \ref{proofline:correct-word-order} yields the correct word order.
我怀疑是否有一个简单的解决方案来解决bussproofs单个公理（和其他）行的放置顺序与结果行号不一致的问题。我必须看看我是否可以将这个解决方案“推销”给文档的未来读者，希望他们不会因为错误的顺序而太恼火，并更多地关注相关行的引用，而不是该行的实际编号。
(2) 如果在 prooftree 开始后没有\Numbersfalse包含任何内容，则至少\lnum需要一个（例如，开始第一个公理），否则TeXstudio会发出错误消息“Package pgf 错误：没有已知的名为 n0 的形状。\end{profftree}”。没什么大不了的，只要确保包含一个\Numbersfalse或至少一个即可\lnum。
（3）编辑：部分解决：%在定义行末尾添加后\lnum，它适用于\Numberstrue，但现在可以看到额外的空间\Numbersfalse。一些额外空间在每个以 开头的证明行的开头创建\lnum：如果您注意例如包含 A 的行，您会注意到它稍微向右移动而不是居中（B、D 和 J 也是如此）。可以在某处重新调整吗？
（4）因为我需要一个点在左对齐的数字之后（例如，用“1.”代替“1”，就像原来的一样），我尝试在该tikzpicture结构中找到正确的位置（作为最佳猜测）。在 之后添加时，它似乎有效at...，就在 之后\z，因此将其改为... {\z.};。我怀疑这会给 (3) 增加更多额外的空白。
（5）编辑： “套印”是由于的副作用而发生的\ResumeProof；在短样本文档中它不是那么清晰可见。
我怀疑那个“tikz魔法”总是从1（\foreach \z in {1,...,\theprooflinecount}），使所有不必要的线条“叠印”（=可见）... 是否有可能以某种方式限制仅输出有问题的线条（很可能> 1，即对于线条的恢复校样，例如 6. 和 7.）？
在试验点加法问题 (4) 时，我注意到这个可疑的粗体字第二个示例证明的编号在数字加倍时“消失”——我无法重现这种揭示行为。效果在第二次校样中（几乎）可见；套印来自于对 of \lnumafter的调用\ResumeProof，产生输出，其中所有左对齐的行号都小于恢复的行号（但除此之外，这些都是空行）
(6) 在公理（或其他bussproof构造）中定义标签效果很好:-) 这就是我添加引用它的句子的原因。
答案1
由于书写方式的原因，我无法想到一种完全自动地执行此操作的方法bussproofs：它没有可以使用的“线”的概念，因为一切都是使用 TeX 框（非常巧妙地）构建的。
但这里有一个解决方案，它使用 TikZ 来放置数字和半手动编号命令。它是半手动的，因为每行的第一个元素需要包含一个明确的\lnum命令来编号该行。此技术需要两次编译才能正确放置，因此如果第一次运行将数字放在奇怪的位置，请不要惊慌。
我还添加了一个\ResumeProof宏，用于从上一个证明的末尾开始编号，以及一个\LastProof引用紧接在前一个证明中的行号的宏。当然，这可以通过各种方式进行修改。
因为能够打开和关闭编号很有用（特别是当您确定要编号的元素时），所以我创建了一个条件来打开和关闭编号，无论是全局还是本地。
\documentclass{article}
\usepackage{bussproofs}
\newcounter{prooflinecount}
\newcounter{LastNum}
\newcounter{proofnum}
\newlength{\linenumindent}
\setlength{\linenumindent}{0pt}
\usepackage{tikz}
\usepackage{tikzpagenodes}
\usepackage{etoolbox}
\usetikzlibrary{calc}
% command to number a line
\newcommand{\lnum}{%
\refstepcounter{prooflinecount}%
\label{\theproofnum-\theprooflinecount}%
\tikz[remember picture]{\coordinate (n\theprooflinecount);}}
% conditional to number or not
\newif\ifNumbers
\Numberstrue% turn numbering on by default
% main command to number a proof
\newcommand{\NumberProof}{%
\ifNumbers%
\begin{tikzpicture}[remember picture, overlay]
\foreach \z in {\FirstNum,...,\theprooflinecount}{
\path let \p1 = (current page text area.west),
\p2 = (n\z)
in
node[inner sep=0pt,
outer sep=0pt,
baseline,
align=right,
text width=2.5em]
at ($(\x1,\y2)+(\linenumindent,2.5pt)$) {\z.};}
\end{tikzpicture}%
\fi%
\setcounter{LastNum}{\value{prooflinecount}}%
}
% Some referencing commands
\newcommand{\LastNum}{}
\newcommand{\FirstNum}{}
\newcommand{\ResumeProof}{\setcounter{prooflinecount}{\value{LastNum}}\def\FirstNum{\theLastNum}}
\newcommand{\LastProof}[1]{\ref{\theproofnum-#1}}
%
% Set up autonumbering
\AtBeginEnvironment{prooftree}{\refstepcounter{proofnum}\setcounter{prooflinecount}{0}\def\FirstNum{1}}
\AtEndEnvironment{prooftree}{\NumberProof}
\begin{document}
\begin{prooftree}
\Axiom$\lnum\Gamma\left[\langle\mbox{A}\rangle\right] \fCenter\ \Rightarrow \mbox{C}$
\RightLabel{($\ast$)}
\UnaryInf$\lnum\Gamma\left[\mbox{A}\right] \fCenter\ \Rightarrow \mbox{C}$
\end{prooftree}
\begin{prooftree}
\AxiomC{\lnum A}
\UnaryInfC{\lnum B}
\AxiomC{C}
\BinaryInfC{\lnum D}
\AxiomC{E}
\AxiomC{F}
\BinaryInfC{G}
\UnaryInfC{H}
\BinaryInfC{\lnum J}
\end{prooftree}
As we can see in line \LastProof{3} the lines are referencible. We can also resume a proof by using the \verb|\ResumeProof| command:
\begin{prooftree}
\ResumeProof
\AxiomC{\lnum A}
\UnaryInfC{\lnum B}
\AxiomC{C}
\BinaryInfC{\lnum D}
\AxiomC{E}
\AxiomC{F}
\BinaryInfC{G}
\UnaryInfC{H}
\BinaryInfC{\lnum J}
\end{prooftree}
We can use \verb|\Numbersfalse| to turn off the numbering while we're figuring out which elements to number or use \verb|\Numberstrue| to selectively turn on numbering.
\begin{prooftree}
\Numbersfalse
\AxiomC{A}
\UnaryInfC{B}
\AxiomC{C}
\BinaryInfC{D}
\AxiomC{E}
\AxiomC{F}
\BinaryInfC{G}
\UnaryInfC{H}
\BinaryInfC{J}
\end{prooftree}
% More complex example
\def\ciOneL{$\circ_{1l}$}
\def\ciTwo{$\circ_2$}
To get the line number ordering correct you need to understand the proof structure to know where to place the initial \verb|\lnum| command. Here's a more complex example.
\begin{prooftree}
% switch to \Numberstrue automatically as soon as the first \lnum is used
\AxiomC{ v$_1$ $\Rightarrow$ tv$/_2$vp} % 2. line left
\AxiomC{\lnum v$_2$ $\Rightarrow$ tv} % 1. line mid
\AxiomC{np$_3$ $\Rightarrow$ np} % 1. line right
\RightLabel{\scriptsize{[$/_{1l}$E]}}
\BinaryInfC{\lnum v$_2$ \ciOneL\ np$_3$ $\Rightarrow$ vp} % 2. line mid
\RightLabel{\scriptsize{[$/_2$E]}}
\BinaryInfC{\lnum (v$_1$ \ciTwo\ (v$_2$ \ciOneL\ np$_3$)) $\Rightarrow$ tv} % 3. line left
\AxiomC{np$_2$ $\Rightarrow$ np} % 3. line right
\RightLabel{\scriptsize{[$/_{1l}$E]}}
\BinaryInfC{\lnum ((v$_1$ \ciTwo\ (v$_2$ \ciOneL\ np$_3$)) \ciOneL\ np$_2$) $\Rightarrow$ vp \label{proofline:correct-word-order}} % 4. line (mid)
\RightLabel{\scriptsize{[MP]}}
\UnaryInfC{\lnum ((v$_1$ \ciOneL\ np$_2$) \ciTwo\ (v$_2$ \ciOneL\ np$_3$)) $\Rightarrow$ vp} % 5. line (mid)
\end{prooftree}
\begin{prooftree}
% switch to \Numberstrue automatically as soon as the first \lnum is used
\Numbersfalse
\AxiomC{ v$_1$ $\Rightarrow$ tv$/_2$vp} % 2. line left
\AxiomC{\lnum v$_2$ $\Rightarrow$ tv} % 1. line mid
\AxiomC{np$_3$ $\Rightarrow$ np} % 1. line right
\RightLabel{\scriptsize{[$/_{1l}$E]}}
\BinaryInfC{\lnum v$_2$ \ciOneL\ np$_3$ $\Rightarrow$ vp} % 2. line mid
\RightLabel{\scriptsize{[$/_2$E]}}
\BinaryInfC{\lnum (v$_1$ \ciTwo\ (v$_2$ \ciOneL\ np$_3$)) $\Rightarrow$ tv} % 3. line left
\AxiomC{np$_2$ $\Rightarrow$ np} % 3. line right
\RightLabel{\scriptsize{[$/_{1l}$E]}}
\BinaryInfC{\lnum ((v$_1$ \ciTwo\ (v$_2$ \ciOneL\ np$_3$)) \ciOneL\ np$_2$) $\Rightarrow$ vp \label{proofline:correct-word-order}} % 4. line (mid)
\RightLabel{\scriptsize{[MP]}}
\UnaryInfC{\lnum ((v$_1$ \ciOneL\ np$_2$) \ciTwo\ (v$_2$ \ciOneL\ np$_3$)) $\Rightarrow$ vp} % 5. line (mid)
\end{prooftree}
\end{document}
