☰

哪些软件包/实践与编写结构化推导相关？（类似于 Dijkstra 的计算证明风格）

tag-icon • tag-icon math-mode packages equations theorems
哪些软件包/实践与编写结构化推导相关？（类似于 Dijkstra 的计算证明风格）

有谁知道有什么软件包可以支持这种风格的证明书写？

“结构化派生”语法的一个非平凡示例，取自 Ralph-Johan Back 的论文

我唯一发现的是：tex-ewd，一组在 CTAN 上专门为 Dijkstra 编写的纯 TeX 宏；以及LyX 仅适用于 Windows 的版本已扩展支持结构化派生。（遗憾的是 LyX-SD 仅限于 Windows，因为我猜用 LyX 编写证明会很棒）

如果没有任何现成的包并且我必须自己动手，那么是否有足够相似的包以便我可以学习“正确的方法”来制作 LaTeX 的结构化派生包？

我首先向您表示“感谢”:) 对于任何帮助我都会非常感激。

如果您需要更多信息来提供帮助（或者即使我只是引起了您的兴趣），这里有一些很好的资源：

答案1

我很想使用一系列itemize和enumerate环境，使用enumitem包来帮助格式化

在此处输入图片描述

在下面的代码中，我使用了包resume提供的功能enumitem来帮助保持环境的编号，enumerate而无需对任何数字进行硬编码。

我还使用了该命令的可选参数\item，例如可以使用

\item[$\Vdash$]

如果你打算经常使用它，你可以把它变成\newcommand

\documentclass{article}
\usepackage{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{enumitem}

% global settings for enumerate environment
\setlist[enumerate]{label*=(\arabic*),leftmargin=0mm}

% itemize environment, when at nested depths 2, 3, 4
\setlist[itemize,2]{label=\textbullet,leftmargin=1cm}
\setlist[itemize,3]{label=\textbullet,leftmargin=1cm}
\setlist[itemize,4]{label=\textbullet,leftmargin=1cm}

\begin{document}
\begin{itemize}
    \item Show that $f$ is continuous at $x_0$, when
        \begin{enumerate}
            \item\label{item:range} $f(x)=\sqrt{x}$ when $x\geq 0$, and
            \item\label{item:pos} $x_0>0$
        \end{enumerate}
    \item[$\Vdash$] $f$ is continuous at $x_0$
    \item[$\equiv$] $\{\text{definition of continuity}\}$

            $(\forall\epsilon>0\cdot \exists\delta>0\cdot\forall x\geq 0\cdot |x-x_0|<\delta\Rightarrow|f(x)-f(x_0)|<\epsilon)$
    \item[$\equiv$] $\{\text{choose arbitrary }\epsilon \text{generilization rule}\}$
    \begin{itemize}
        \item Show that $(\exists\delta>0\cdot\forall x\geq 0\cdot |x-x_0|<\delta\Rightarrow |f(x)-f(x_0)|<\epsilon)$, when
        \begin{enumerate}[resume]
            \item $\epsilon>0$
        \end{enumerate}
        \item[$\Vdash$] $\{\text{find a suitable value for } \delta\text{ witness rule}\}$
        \begin{itemize}
            \item Show that $\delta>0\wedge(\forall x\geq 0\cdot|x-x_0|<\delta\Rightarrow|f(x)-f(x_0)|<\epsilon)$, when
            \begin{enumerate}[resume]
                \item $\delta=?$ $\sharp$ $\delta=\epsilon\cdot\sqrt{x_0}$
            \end{enumerate}
            \item[$\Vdash$] $\{\text{show the two conjuncts separately, use generalization rule for second conjunct}\}$
            \begin{itemize}
                \item Show that $|f(x)-f(x_0)|<\epsilon$, when
                \begin{enumerate}[resume]
                    \item\label{item:xnonneg} $x\geq 0$, and
                    \item $|x-x_0|<\delta$
                \end{enumerate}
                \item[$\Vdash$] $|f(x)-f(x_0)|$
                \item[$=$] $\{$assumption \ref{item:range}, $f(x)$ and $f(x_0)$ are defined by assumptions \ref{item:xnonneg} and \ref{item:range}$\}$
                \item[] $|\sqrt{x}-\sqrt{x_0}|$
                \item[$=$] $\{$extend with conjugate value for $\sqrt{x}-\sqrt{x_0}$, i.e., with $\sqrt{x}+\sqrt{x_0}>0$$\}$
                \item[] $\dfrac{|x-x_0|}{\sqrt{x}+\sqrt{x_0}}$
                \item[$\leq$] $\{$make divisor smaller, $\sqrt{x}\geq 0$ $\}$
            \end{itemize}
        \end{itemize}
    \end{itemize}
\end{itemize}
\end{document}

答案2

您可能对 Leslie Lamport 编写的软件包感兴趣，pf2，用于产生结构化证明看起来与 Dijkstra 使用的风格非常相似。该包只是一个.sty文件，似乎没有托管在 CTAN 上，但您可以在这里找到它：http://lamport.azurewebsites.net/latex/latex.html。

itemize此包提供的样式将类似于下面这两列之一（您可以自由更改编号和缩进的样式）。我认为经过一些调整后，您可能能够实现所需的美感。好吧，可以说比使用一堆嵌套的和更轻松enumerate。

<code>pf2.sty</code> 中的结构化证明

编辑：经过一番谷歌搜索，我没有找到一种轻松创建嵌套列表的优雅方法。Markdown + KaTeX（或 MathJax）和 LaTeX 转换pandoc可能接近这一点，但您只能获得 Markdown 环境中支持的一组有限的 LaTeX 命令。

答案3

Fokkinga 于 2015 年 1 月发布了这样一个包，它被称为计算。

它以某种方式遵循了 eqnarray 的方法（文档中如此说）。因此分数和大运算符会变得拥挤。除此之外，它还不错。

相关内容