enumerating lines of bussproofs

Question

EDIT: see below the original question

Having got a great task of re-TeX-ing, i.e. transforming a PDF original of a lost LaTeX source back into LaTeX, I've got the recommendation to use bussproof.sty to recreate a bunch of proofs. https://github.com/leanprover/logic_and_proof/blob/master/bussproofs.sty https://www.math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/BussGuide2_Smith2012.pdf

So far so good - it works nicely (generally spoken). However, as many of these proofs are pretty lengthy, there is need for reference to single lines of each proof. That's why it's neccessary to enumerate each line, preferrably with numbers left-aligned (see the original), automatically increasing, and with the possibility of starting from a certain number (not always from 1.) as some of the proofs have to be continued after a bigger portion of text - with something similar to \begin{enumerate}[label=\roman*.,start=3] or ...[resume]. The normal labelling for each line should be possible to be able to refer to. I cannot use the bussproof labels for enumeration as a workaround because they are in the height of inference lines and are just next to the line (left or right aligned). This is what I could manage so far (without enumeration): A very short code example:

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

Does anybody have an idea how to set the left-aligned enumeration within these proofs?

---

EDIT: using the nice solution given by Alan Munn, some other problems occur:

It's still a bit of rocket science for me as I am not familiar with tikz and related packages, but I guess that the most magic happens there...
The first tests with your solution lead me to the following observations:
(1) Wrong order of line enumeration: The busproofs are kind of too smart, because as soon as proofs get more complicated, some axioms have to be specified on quite distant lines (compared to a simple straight-forward hierarchy). I include one of the simple (!) examples that already shows that the lines 1 and 2 are not in the correct order any more (blame it on the 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.

I doubt that there is a simple solution to the mismatch of the order in which bussproofs puts the single axiom (and other) lines and the resulting line numbers. I have to see if I can "sell" this solution for the future readers of the document, hoping that they are not too irritated by the wrong order and pay more attention to a reference of the line in question as such and not the actual number of that line. (2) If after the beginning of a prooftree there is no \Numbersfalse included, then at least on \lnum is needed (e.g. starting the 1st axiom), otherwise TeXstudio issues an error message "Package pgf Error: No shape named n0 is known. \end{profftree}". No big deal, just make sure that there is either a \Numbersfalse or at least one \lnum included.

(3) EDIT: partly solved: after adding % at the end of \lnum definition lines, it works for \Numberstrue, but the extra space is now visible for \Numbersfalse. Some extra space is created at the beginning of each proof line that starts with \lnum: if you pay attention to e.g. the line that includes an A, you'll notice that it is somewhat shifted to the right instead of being centered (the same for B, D and J). Can this be re-adjusted somewhere?

(4) As I need a dot after the left-aligned numbers (e.g. "1." instead of "1", like in the original), I tried to find the right place (as a best guess) within that tikzpicture construct. It seems to be working when added after the at..., just after the \z, so making it to ... {\z.};. I suspect that this adds even more extra white space to (3).

(5) EDIT: "Overprinting" occurs because of side effects of \ResumeProof; it is not so clearly visible in the short sample document.
I suspect that that "tikz magic" always counts from 1 (\foreach \z in {1,...,\theprooflinecount}), making all the unnecessary lines "overprinted" (=visible)... Is it somehow possible to limit the output of the lines in question only (highly probably >1, i.e. for the resumed proof for the lines e.g. 6. and 7.)?
While experimenting with the dot addition problem (4) I noticed that this suspicious boldface-looking numbering of the second example proof "dissolves" in doubling the numbers - I cannot reproduce this revealing behaviour. Effects are (almost in)visible in the second proof; overprinting comes from the invocation of of \lnum after \ResumeProof, producing output with all the left-aligned line numbers which are smaller then the resumed line number (but otherwise these are empty lines)

(6) Defining a label within an axiom (or other bussproof constructs) works nicely :-) That's why I added a sentence referencing to it.

Answer 1

I can't think of a way to do this completely automatically because of the way bussproofs is written: it has no concept of 'line' that can be used since everything is built (very cleverly) using TeX boxes.

But here's a solution that uses TikZ to place the numbers and a semi-manual numbering command. It's semi-manual in the sense that the first element of each line needs to contain an explicit \lnum command to number that line. This technique requires two compilations to get the placement correct, so don't be alarmed if the first run puts the numbers in strange place.

I've also added a \ResumeProof macro to start the numbering from the end of the previous proof, and a \LastProof macro that references to a line number in the immediately preceding proof. This of course could be modified in various ways.

Since it's useful to be able to turn on and off the numbering (especially when you are figuring out which elements to number) I've created a conditional to turn numbering on and off, either globally or locally.

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