ebproof 証明木: 副条件の重複

Question

私は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*}

しかし、副条件が周囲の要素と重なるという問題があります。推論が 1 つしかない場合は、\vspace{...}証明ツリーの前後に配置できますが、別の推論がある場合 (つまり、より大きなツリーの一部である場合)、これは機能しません (\vspace{...}証明ツリー環境内では無視されます)。

(これを生成するコード:)

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

Answer 1

2つの可能性があると思います。

\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|}} では、ボトムライン（深さ、つまりベースラインより下にあるもの）に役立つ「トップストラット」は無視されます。

フル ストラットは中央のラインに便利です。高さも深さも無視されません。

2 番目のディスプレイでは、より短い支柱が使用されていますが、考え方は同じです。