Árvores de prova ebproof: sobreposição de condições laterais

Árvores de prova ebproof: sobreposição de condições laterais

Estou usando o ebproofpacote para criar árvores de derivação para regras de inferência. Estas regras têm premissas acima do julgamento e condições secundárias à esquerda:

Exemplo de prova renderizada

Para gerar isso, eu 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*}

No entanto, estou tendo um problema em que as condições laterais se sobrepõem aos elementos circundantes. Onde há uma única inferência, posso simplesmente colocar \vspace{...}antes e depois da árvore de prova, mas onde há outra inferência (ou seja, como parte de uma árvore maior), isso não funciona ( \vspace{...}é ignorado dentro do ambiente da árvore de prova).

Sobreposição de condições laterais em inferências empilhadas

(Código para gerar isso:)

    \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 uma maneira limpa de fazer com que ele tenha a quantidade correta de espaço? Usar o arrayambiente é um pouco complicado, mas foi a única maneira de adicionar quebras de linha ao parâmetro do rótulo esquerdo em \infer. Como alternativa, existem outros pacotes que fornecem essa sintaxe de maneira mais limpa?


Isso não é relevante para o problema, mas se você quiser copiar exatamente esses trechos de código em seu próprio documento, aqui está a definição de \triple:\newcommand{\triple}[3]{ \{#1\}\ \texttt{#2}\ \{#3\}}

Responder1

Vejo duas possibilidades.

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

insira a descrição da imagem aqui

Os espaços adicionais são obtidos com um hack, na verdade.

Com \smash[t]{\vphantom{\bigg|}}insiro a parte inferior de a \bigg|(sem imprimir o símbolo), pois \smash[t]{...}tem o cuidado de desconsiderar a altura do símbolo. Isso é útil para a linha superior, então eu chamo de “suporte inferior”.

Da mesma forma com `\smash[b]{\vphantom{\bigg|}}, um “suporte superior” útil para a linha inferior (a profundidade, ou seja, o que está abaixo da linha de base) é desconsiderado.

A escora completa é útil para a linha média: nem a altura nem a profundidade são desconsideradas.

No segundo display é utilizado um suporte mais curto, mas a ideia é a mesma.

informação relacionada