以特定风格输入派生词

Question

我该如何输入这样的推导，在假设周围加上方框，并用垂直线从左侧“延续”这些方框？

Answer 1

类似这样的内容？我定义了一个环境prooftabular，它有tabular三个左对齐的列，其中的新命令\proofitem会自动增加计数器并显示数字。我还定义了一个命令\assumption，将这些假设写在下面带有垂直线的框中。它需要两个参数：垂直线应跨越的行数（不包括带有框的行），以及假定处于数学模式的框的内容。

\documentclass{article}
\usepackage{amsmath, amssymb}
\newlength{\rowdepth}
\setlength{\rowdepth}{3.5pt}
\newlength{\rowtotalheight}
\setlength{\rowtotalheight}{14pt}
\newcommand*{\vertrule}[1]{%
    \smash{\rule[\dimexpr-\rowdepth-#1\rowtotalheight]{.4pt}{#1\rowtotalheight}}%
}
\newcommand*{\assumption}[2]{%
    \makebox[0pt][l]{\vertrule{#1}}\(\boxed{#2}\)%
}
\newcounter{prooftabenumi}
\renewcommand*{\theprooftabenumi}{(\arabic{prooftabenumi})}
\newcommand*{\proofitem}{%
    \refstepcounter{prooftabenumi}%
    \theprooftabenumi%
}
\newenvironment{prooftabular}{%
    \setcounter{prooftabenumi}{0}
    \begin{tabular}{@{\rule[-\rowdepth]{0pt}{\rowtotalheight}}lll}
}{%
    \end{tabular}
}
\begin{document}
\begin{prooftabular}
    \proofitem\label{sort}
        & \(* : \square\) & (\emph{sort}) \\
        & \assumption{5}{A : *} & \\
    \proofitem\label{var}
        & \quad \(A : *\) & (\emph{var}) on \ref{sort} \\
    \proofitem\label{weak1}
        & \quad \(* : \square\) & (\emph{weak}) on \ref{sort} and \ref{sort} \\
        & \quad \assumption{1}{x : A} & \\
    \proofitem\label{weak2}
        & \qquad \(* : \square\) & (\emph{weak}) on \ref{weak1} and \ref{var} \\
    \proofitem
        & \quad \(A \to * : \square\) & (\emph{form}) on \ref{var} and \ref{weak2}
\end{prooftabular}
\end{document}

它似乎运行良好，但如果行太长，并且缩进不能自动调整到低于假设值（因此是\quads），布局就会中断。我怀疑可能有一个包已经编码了这样的环境，而且可能以更好的方式，但我不知道。

Answer 2

flagderiv旨在排版此类证明。由于我不是计算机科学家，因此我不熟悉该软件包或您的语法，因此毫无疑问，以下内容可以进行微调以获得良好的效果。例如，我怀疑这\lbox是一个很好的语义名称，但我不确定该符号是否以其通常的含义用于我所熟悉的逻辑中，因此我犹豫是否要相应地命名它。（我会将此符号用作表示必要的一元运算符或作为证明结束指示符，但两者似乎都不适合这里。）此外，flagderiv提供了很多选项来配置证明的外观，如果这些是您需要的证明类型，这将值得进一步探索。

\documentclass{article}
\usepackage{flagderiv}
\usepackage{amssymb}
\newcommand*{\limp}{\ensuremath{\mathbin{\rightarrow}}}
\newcommand*{\lbox}{\ensuremath{\mathbin{\square}}}
\NewDocumentCommand \jrule {m} {(\emph{#1})}
\NewDocumentCommand \jruleon {mm} {\jrule{#1} on \ref{#2}}
\begin{document}
\begin{flagderiv}
  \step{sort}{*:\lbox}{\jrule{sort}}
  \assume*{}{A:*}{}
    \step{var-a}{A:*}{\jruleon{var}{sort}}
    \step{weak-a}{*:\lbox}{\jruleon{weak}{sort} and \ref{sort}}
    \assume*{}{x:A}{}
      \step{weak-x}{*:\lbox}{\jruleon{weak}{weak-a} and \ref{var-a}}
    \done
    \step{conc}{A \limp *:\lbox}{\jruleon{form}{var-a} and \ref{weak-x}}
  \done
\end{flagderiv}

\end{document}

对于有两条引用线的情况，创建另一个可能也是有意义的\jrule...。这留给读者练习，因为这里有意义的东西不仅取决于语义，还取决于个人偏好。

Answer 3

我怀疑Tikz 包将会很有帮助。

对于其他数学符号，你可以简单地使用 TeX 编辑器中可用的命令。$A \rightarrow * : $ \square例如

正如问题（5）中所述。

但请注意符号使用的包（即 \usepackage{xxx}）。