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.