Local labels

Didier Rémy

January 31, 2006

Abstract

This package provides macros to generate numeric references and refer to them by name, much as equation numbers, except that numbers and names can be reset at any time. One typical use is to refer to facts beeing establish during a proof until completion of the proof and be able to do so in the next proof without any clash of names of labels.

The package also comes with a version for HeVeA.

1 Example

Theorem 1 Socrate is mortal.

\underline{Proof:} Socrate is a man (1). It is well-known that all man are mortal (2). Hence, by (1) and (2), Socrate is mortal.

Let me prove it another way:

\underline{Proof:} It is well-known that all man are mortal (1). Socrate is a man (2). Hence, by (1) and (2), Socrate is mortal.

Did you notice that fact (1) of first proof became fact (2) in the second proof?

2 Short manual

\locallabelreset

Reset numeric labels and names to refer to them

\llabel{⟨Name⟩}

Creates a new numeric label, binds it to ⟨Name⟩, and print the label as a binding occurrence.

This primitive may take a ⟨Gname⟩ as optional argument, so that the \ref{⟨Gname⟩} can be used to refer to this label in any context. Of course ⟨Gname⟩ is subject to overriding and name clashes exactly as all global labels do.

\lref{⟨Name⟩}

Prints numeric use occurrence of label ⟨Name⟩.

\lbind{⟨Name⟩}

This creates the label as \llabel, but does not print it. This can be used to skip one numeric value or to assign them in a controlled order. In this case, the next use of \llabel{⟨Name⟩} will print the name of the label as a binding occurrence.

If \llabel{⟨Name⟩} is repeated with the same name ⟨Name⟩ a warning will be issued.

Customization You may redefined the followuing macros to change the appearance of binding and use occurrences:

\LlabelTypeset{⟨Val⟩}

Typesets ⟨Val⟩ as a binding occurrence.

\LrefTypeset{⟨Val⟩}

Typesets ⟨Val⟩ as a use occurrence.

3 Code of the example

\begin{theorem}\label{socrate-mortal}Socrate is mortal.
\end{theorem}
\begin{proof}
Socrate is a man~\llabel[socrate-man]{sm}.  It is well-known that all man
are mortal~\llabel{mm}.  Hence, by~\lref {sm} and \lref {mm}, Socrate is
mortal.
\end{proof}
Did you hear what I said?
\begin{theorem}
Socrate is mortal.
\end{theorem}
Let me prove it another way:
\begin{proof}
\locallabelreset
It is well-known that all man are mortal~\llabel{mm}.  Socrate is a
man~\llabel {sm}.  Hence, by~\lref {mm} and \lref {sm}, Socrate is mortal.
\end{proof}
Actually, in the proof of Theorem~\ref{socrate-mortal},
claim \ref{socrate-man} is arguable.