证明包的推断命令中的量化

Question

我正在尝试使用 proof 包的 infer 命令编写这个推理规则：

为此我使用以下命令：

$\infer{s = s'}{%
        R \subseteq A^{\omega} \times A^{\omega}
        & R \; s \; s'
        & \forall s_1, s_2. \infer{\text{head}(s_1) = \text{head}(s_2) \land R(\text{tail}(s_1), \text{tail}(s_2))}{%
            R \; s_1 \; s_2
        }
    }$

然而，在较低层次上，所有量化表现为：

我怎样才能像上面那样把它放在中间？

Answer 1

我建议一个\qinfer命令：

\documentclass{article}

\usepackage{proof,amsmath}

\newcommand{\func}[1]{\mathrm{#1}}

\newcommand{\qinfer}[3]{%
  \sbox0{\infer{#2}{#3}}%
  \raisebox{\dimexpr(\ht0-1ex)/2}{$#1\;$}%
  \box0
}

\begin{document}

\[
  \infer{s = s'}{%
    R \subseteq A^{\omega} \times A^{\omega}
    & R \; s \; s'
    &
      \qinfer{\forall s_1,s_2}
             {\func{head}(s_1) = \func{head}(s_2) \land R(\func{tail}(s_1), \func{tail}(s_2))}
             {R \; s_1 \; s_2}
  }
\]

\end{document}

我还修复\text了\mathrm，这是这里使用的正确命令（如果不是\operatorname）。

Answer 2

推理规则的名称可以作为可选参数添加至\infer：

\infer[label]{conclusion}{premises}

然而，标签被添加向右。

\documentclass{article}
\usepackage{proof}
\usepackage{amsmath}
\begin{document}
$\infer{s = s'}{%
   R \subseteq A^{\omega} \times A^{\omega}
 & R \; s \; s'
 & \infer[\forall s_1, s_2]{%
     \text{head}(s_1) = \text{head}(s_2)
     \land R(\text{tail}(s_1), \text{tail}(s_2))%
   }{%
     R \; s_1 \; s_2
   }
 }$
\end{document}

Answer 3

您可以使用以下方法将其提升到位\raisebox{<len>}{<stuff>}：

\documentclass{article}

\usepackage{proof,amsmath}

\begin{document}

\[
  \infer{s = s'}{%
    R \subseteq A^{\omega} \times A^{\omega}
    & R \; s \; s'
    & \raisebox{.6\baselineskip}{$\forall s_1, s_2$~}
      \infer{\text{head}(s_1) = \text{head}(s_2) \land R(\text{tail}(s_1), \text{tail}(s_2))}{%
        R \; s_1 \; s_2
      }
  }
\]

\end{document}