自定义待证明语句的命令

Question

我已经为证明目标创建了一个代码：

\centering{zz:\,$\{P,\,P \lif Q,\,Q \lif  R\}\,\sststile{AL}{}\,R$`

输出如下所示：

现在我想定义一个自定义命令，它为这种代码提供了非常通用的配方。它应该具有以下形式：

\zz{formulas before the turnstile |- formula after the turnstile}[first argument of sststile, optional]

所以在我的例子中，它应该是：

\zz{P,P \lif Q, Q \lif R|- R}[AL]

该命令应该适用于旋转门前的任意数量的公式，用逗号分隔它们并在它们之间添加额外的空格。此外，如果我写|=而不是|-它应该产生双旋转门\sdtstile。我该怎么做？我期待您的回答！

以下是我使用的代码：

\documentclass[a4paper,ngerman, abstracton, leqno]{scrartcl} 
\usepackage{amsmath} 
\usepackage{amssymb} 
\usepackage{amsthm} 
\usepackage{turnstile}
\usepackage[LGRgreek]{mathastext} % removes italics from mathfont

\newcommand{\lif}{\rightarrow}

\begin{document}
\centering{zz:\,$\{P,\,P \lif Q,\,Q \lif  R\}\,\sststile{AL}{}\,R$}
\end{document}

Answer 1

首先，\centering它似乎不像你想象的那样有效。我\[...\]曾经用过。

\documentclass{article}
\usepackage{amsmath}
\usepackage{turnstile}

\usepackage{lipsum} % just for mock text

\newcommand{\lif}{\rightarrow}

\ExplSyntaxOn

\NewDocumentCommand{\zz}{mO{}}
 {
  \vitus_zz_start:nn { #1 } { #2 }
 }

\cs_new_protected:Nn \vitus_zz_start:nn
 {
  \regex_match:nnTF { \| \- } { #1 }
   {
    \vitus_zz_do:nnnn { |- } { \sststile } { #1 } { #2 }
   }
   {
    \vitus_zz_do:nnnn { |= } { \sdtstile } { #1 } { #2 }
   }
 }

\cs_new_protected:Nn \vitus_zz_do:nnnn
 {
  \[
  \mathrm{zz{:}\;}
  \seq_set_split:Nnn \l_tmpa_seq { #1 } { #3 }
  \seq_item:Nn \l_tmpa_seq { 1 }
  #2{#4}{}
  \seq_item:Nn \l_tmpa_seq { 2 }
  \]
 }

\ExplSyntaxOff

\begin{document}

\lipsum[1][1-3]
\zz{P,P \lif Q, Q \lif R |- R}[AL]
\lipsum[2][1-3]
\zz{P,P \lif Q, Q \lif R |- R}
\lipsum[1][1-3]
\zz{P,P \lif Q, Q \lif R |= R}[AL]
\lipsum[2][1-3]
\zz{P,P \lif Q, Q \lif R |= R}
\lipsum[2][1-3]

\end{document}

吸收参数并分析第一个（强制）参数以查看其是否包含|-。如果包含，则\sststile使用，否则使用\sdtstile。接下来，根据前面的分析，将参数拆分为或|-，|=并形成线。