☰

ebproof Доказательство Деревья: Боковые условия перекрываются

tag-icon • tag-icon white-space overlap ebproof
ebproof Доказательство Деревья: Боковые условия перекрываются

Я использую ebproofпакет для создания деревьев вывода для правил вывода. Эти правила имеют посылки над суждением и побочные условия слева:

Пример предоставленного доказательства

Для его создания я использую:

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

Однако у меня возникла проблема, когда боковые условия перекрываются окружающими элементами. Там, где есть один вывод, я могу просто поставить \vspace{...}до и после prooftree, но там, где есть другой вывод (т. е. как часть большего дерева), это не работает ( \vspace{...}игнорируется внутри среды prooftree).

Перекрывающиеся побочные условия в многоуровневых выводах

(Код для генерации этого:)

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

Есть ли чистый способ сделать так, чтобы у него было правильное количество места? Использование среды arrayнемного хакерское, но это был единственный способ, которым я мог добавить переносы строк в параметр left-label в \infer. Или есть ли другие пакеты, которые предоставляют этот синтаксис более чистым способом?

Это не имеет отношения к проблеме, но если вы хотите в точности скопировать эти фрагменты кода в свой документ, вот определение \triple:\newcommand{\triple}[3]{ \{#1\}\ \texttt{#2}\ \{#3\}}

решение1

Я вижу две возможности.

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

введите описание изображения здесь

На самом деле, дополнительные места можно получить с помощью взлома.

С помощью \smash[t]{\vphantom{\bigg|}}я вставляю нижнюю часть a \bigg|(не печатая символ), потому что \smash[t]{...}это позволяет не учитывать высоту символа. Это полезно для верхней строки, поэтому я называю это «нижней распоркой».

Аналогично с `\smash[b]{\vphantom{\bigg|}}, «верхняя распорка», полезная для нижней линии (глубины, то есть того, что находится ниже базовой линии), игнорируется.

Полная распорка полезна для средней линии: ни высота, ни глубина не игнорируются.

Во втором варианте используется более короткая стойка, но идея та же.

Связанный контент