5

I'm using the mathpartir package by Didier Remy for typesetting inference rules. I like the visual style of the rules, but the package doesn't integrate with the standard \label-\ref cross-referencing mechanism. For example, after I typeset the modus ponens rule:

\documentclass{article}
\usepackage{mathpartir}

\begin{document}
\begin{mathpar}
  \inferrule[ABC]{
    A \\
    A \Longrightarrow B
  }{
    B
  }{{\Longrightarrow}E}
\end{mathpar}
\end{document}

I would like to be able to reference it later using \ref, and get ${\Longrightarrow}E$ rendered. Questions:

  1. Can I make this work with mathpartir, and how? Also, a general pointer to how \label and \ref work under the hood might be useful - as I don't have all too many rules, I'd also be happy with a hacky solution.

  2. Do you know any alternative packages capable of this?

1
  • 2
    Welcome! Generally, \label writes the value of a counter to the .aux file and \ref uses the value of that counter to create a cross-reference. Since your rules aren't numbered, I'm not entirely sure how you think this might work. There are packages which allow you to pull in the name of something instead e.g. of a section, so I guess you'd need something like that. But the standard cross-referencing system does numbers and just numbers as far as I know. (They may get formatted as letters, say e.g. A, B, C rather than 1, 2, 3 but they are still values of a counter.)
    – cfr
    Nov 24, 2016 at 22:41

1 Answer 1

9

The default cross-referencing system relies on cross-referenced items being numbered. \label{} writes the value of the currently applicable counter to the .auz file, along with the tag given as its argument. \ref{} uses that tag to retrieve the value of the counter. The counter may be formatted as something other than a number e.g. A, B, C rather than 1, 2, 3, but it is still a number underneath.

Since the inference rules aren't numbered, this obviously does not apply. Moreover, even if they were numbered, \ref{} would return the value of a counter and not something like -> E.

However, the package nameref, which is part of the hyperref package, extends the standard cross-referencing system so that the names of items such as sections can be retrieved from the .aux file using \nameref{}. It does this by redefining \label{} to write additional information to the .aux file.

We can use this framework to redefine \inferrule so that a subsequent \label{} will write the required information to the .aux file. By default the -> E is not an argument passed to \inferrule at all - it just comes next. So we will need to redefine \inferrule to accept an additional argument, preferably an optional one. We then need to set \@currentlabelname to the value of this argument, if present, so that \label{} knows what to write to the .aux file.

I've used xparse to handle the redefinition.

We start by saving the current definition of \inferrule. We don't need this, but the user might.

\let\originferrule\inferrule

Now we overwrite the definition to accept a final, optional argument. So the new syntax will be \inferrule*[]{}{}[] rather than \inferrule*[]{}{}.

\DeclareDocumentCommand \inferrule { s O {} m m o }{%

Do we want the starred form or not?

  \IfBooleanTF{#1}%
  {%

All we do is pass arguments 2,3 and 4 to the relevant internal macro - either starred ...

    \mpr@inferstar[#2]{#3}{#4}%
  }{%

or not ...

    \mpr@inferrule[#2]{#3}{#4}%
  }%

Now we test if the user used an optional argument or not. If not, there's nothing to do.

  \IfValueT{#5}%
  {%

Otherwise, we add a little space,

    \quad

typeset the argument

    #5%

and pass the argument to another macro (which we define in a minute).

    \my@name@inferrule{#5}%
  }%

And that's it.

}

Now for the final macro. This just sets \@currentlabelname to the relevant value, wrapping it in an \ensuremath{} to avoid errors if the name contains symbols etc.

\NewDocumentCommand \my@name@inferrule { m }{%
  \def\@currentlabelname{\ensuremath{#1}}%
}

Then we can write

\begin{mathpar}
  \inferrule[Modus Ponens]{
    A \\
    A \Longrightarrow B
  }{
    B
  }[\Longrightarrow E]\label{infrule:mp}
\end{mathpar}
Applying \nameref{infrule:mp}, we see that \dots

to produce

refer to inference rule by name

Complete code:

\documentclass{article}
\usepackage{mathpartir,xparse}
\usepackage{nameref}

\makeatletter
\let\originferrule\inferrule
\DeclareDocumentCommand \inferrule { s O {} m m o }{%
  \IfBooleanTF{#1}%
  {%
    \mpr@inferstar[#2]{#3}{#4}%
  }{%
    \mpr@inferrule[#2]{#3}{#4}%
  }%
  \IfValueT{#5}%
  {%
    \quad
    #5%
    \my@name@inferrule{#5}%
  }%
}
\NewDocumentCommand \my@name@inferrule { m }{%
  \def\@currentlabelname{\ensuremath{#1}}%
}
\makeatother

\begin{document}
\begin{mathpar}
  \inferrule[Modus Ponens]{
    A \\
    A \Longrightarrow B
  }{
    B
  }[\Longrightarrow E]\label{infrule:mp}
\end{mathpar}
Applying \nameref{infrule:mp}, we see that \dots
\end{document}
3
  • Just... wow! Thank you for that detailed explanation!
    – oggy
    Nov 25, 2016 at 12:29
  • Impressive and very detailed explanation, thanks!
    – Niols
    May 31, 2017 at 10:55
  • When I use this with the starred version of inferrule (simply replacing \inferrule with \inferrule* in your MWE), I get an error (Use of \mpr@inferstar doesn't match its definition.). Any idea how to solve this? Apr 26, 2021 at 8:51

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .