Estoy usando el ebproofpaquete para crear árboles de derivación para reglas de inferencia. Estas reglas tienen premisas encima del juicio y condiciones laterales a la izquierda:
Para generar esto, uso:
\begin{prooftree*}
\hypo{\Gamma \vdash \triple{P'}{S}{Q'}}
\infer[left label=
$\begin{array}{r}
Q' \geq 0 \\
P \geq P' \\
Q \leq Q'
\end{array}$]
1[\textsc{(While)}]
{ \Gamma \vdash \triple{P}{while $e$ do $S$}{Q} }
\end{prooftree*}
Sin embargo, tengo un problema por el cual las condiciones laterales se superponen con los elementos circundantes. Cuando hay una única inferencia, puedo ponerla \vspace{...}antes y después del árbol de prueba, pero cuando hay otra inferencia (es decir, como parte de un árbol más grande), esto no funciona ( \vspace{...}se ignora dentro del entorno del árbol de prueba).
(Código para generar esto :)
\begin{prooftree}
\hypo{\Gamma \vdash \triple{P}{$S_1$}{Q_1}}
\hypo{\Gamma \vdash \triple{P}{$S_2$}{Q_2}}
\infer[left label={
$\begin{array}{r}
Q' \leq Q_1 \\
Q' \leq Q_2
\end{array}$}]
2[\textsc{(B-Cond)}]
{ \Gamma \vdash \triple{P}{if $e$ then $S_1$ else $S_2$}{Q} }
\infer
[left label={$
\begin{array}{r}
P \geq Q' \\
Q \leq Q'
\end{array}
$}]
1[\textsc{(B-Conseq)}]
{\Gamma \vdash \triple{P}{if $e$ then $S_1$ else $S_2$}{Q}}
\end{prooftree}
¿Existe una manera limpia de hacer que tenga la cantidad correcta de espacio? Usar el arrayentorno es un poco complicado, pero era la única forma en que podía agregar saltos de línea al parámetro de etiqueta izquierda en \infer. Alternativamente, ¿existen otros paquetes que proporcionen esta sintaxis de una manera más limpia?
Esto no es relevante para el problema, pero si desea copiar exactamente estos fragmentos de código en su propio documento, aquí está la definición de \triple:\newcommand{\triple}[3]{ \{#1\}\ \texttt{#2}\ \{#3\}}
Respuesta1
Veo dos posibilidades.
\documentclass{article}
\usepackage{amsmath}
\usepackage{ebproof}
\newcommand{\triple}[3]{\{#1\}\ \texttt{#2}\ \{#3\}}
\newcommand{\bstrutb}{\smash[t]{\vphantom{\bigg|}}}
\newcommand{\bstrutt}{\smash[b]{\vphantom{\bigg|}}}
\newcommand{\bstrut}{\vphantom{\bigg|}}
\begin{document}
\section{Spacing the lines}
\begin{prooftree}
\hypo{\bstrutb \Gamma \vdash \triple{P}{$S_1$}{Q_1}}
\hypo{\Gamma \vdash \triple{P}{$S_2$}{Q_2}}
\infer[left label={
$\begin{array}{@{}r@{}}
Q' \leq Q_1 \\
Q' \leq Q_2
\end{array}$}]
2[\textsc{(B-Cond)}]
{\bstrut \Gamma \vdash \triple{P}{if $e$ then $S_1$ else $S_2$}{Q} }
\infer
[left label={
$\begin{array}{@{}r@{}}
P \geq Q' \\
Q \leq Q'
\end{array}$}]
1[\textsc{(B-Conseq)}]
{\bstrutt \Gamma \vdash \triple{P}{if $e$ then $S_1$ else $S_2$}{Q}}
\end{prooftree}
\section{Reducing the size, with some more space}
\begin{prooftree}
\hypo{\Gamma \vdash \triple{P}{$S_1$}{Q_1}}
\hypo{\Gamma \vdash \triple{P}{$S_2$}{Q_2}}
\infer[left label={
$\substack{
Q' \leq Q_1 \\
Q' \leq Q_2
}$}]
2[\textsc{(B-Cond)}]
{\vphantom{\Big|}\Gamma \vdash \triple{P}{if $e$ then $S_1$ else $S_2$}{Q} }
\infer
[left label={
$\substack{
P \geq Q' \\
Q \leq Q'
}$}]
1[\textsc{(B-Conseq)}]
{\Gamma \vdash \triple{P}{if $e$ then $S_1$ else $S_2$}{Q}}
\end{prooftree}
\end{document}
Los espacios adicionales se obtienen con un truco, de hecho.
Con \smash[t]{\vphantom{\bigg|}}inserto la parte inferior de a \bigg|(sin imprimir el símbolo), porque \smash[t]{...}se encarga de ignorar la altura del símbolo. Esto es útil para la línea superior, por eso lo llamo “puntal inferior”.
De manera similar con `\smash[b]{\vphantom{\bigg|}}, se ignora un “puntal superior” útil para la línea inferior (la profundidad, es decir, lo que está debajo de la línea de base).
El puntal completo es útil para la línea media: no se desprecia ni la altura ni la profundidad.
En la segunda pantalla se utiliza un puntal más corto, pero la idea es la misma.