整理机械证明

Alectryon（以希腊小鸡之神的名字命名）是用于编写将Coq代码和散文混合在一起的技术文档的工具的集合，这种风格有时称为识字编程。

Coq证明很难孤立地理解：与纸质证明不同，证明脚本仅记录要采取的步骤（在x上进行归纳，应用定理，…），而不记录这些步骤导致的状态（目标）。结果，如果没有诸如CoqIDE或Proof General之类的交互界面的帮助，纯文本脚本基本上是难以理解的。

如今，与读者共享证明而不强迫他们运行Coq的最常见方法是将Coq的输出手动复制到源代码注释中，这是一个繁琐，容易出错且脆弱的过程。证明中随附的任何文本也会嵌入到注释中，从而带来痛苦的编辑体验。

Alectryon的表现更好：它可以自动捕获Coq的输出并将其与校对脚本进行交织以生成交互式网页，并且它使您可以在同一文档的基于散文和面向代码的观点之间切换，从而可以使用自己喜欢的文本编辑模式编写散文和您最喜欢的Coq IDE来编写证明。

在下面，您可以看到三个示例：在第一个示例中，我要求Alectryon记录单个Check命令的结果。在第二个中，我记录了由Coq打印的错误消息。在第三篇中，我记录了一个简单的证明脚本-尝试将鼠标悬停或单击Coq句子。最后，我使用了隐藏的Show Proof命令来显示每种策略如何参与构造证明术语。

引理rev_rev {A}（l：list A）：List.rev（List.rev l）= l。证明。归纳法-（* l←[] *）cbn。反身性。 -（* l←_ :: :: _ *）cbn。重写rev_app_distr。重写IHl。 cbn。反身性。 Qed。

上下文（经典：forall A，A \ /〜A）。示例double_negation：（forall A，~~ A-> A）。证明。介绍notnot_A。破坏（经典A）为[_A | not_A]。 -（* A持有*）假设。 -（* A不持有*）elim（notnot_A not_A）。 Qed。

顺便说一句，我在SLE2020（11月16日）上在Alectryon上写了一篇学术论文（由于DOI链接仍无法解析，因此在我的网站上有预印本）。它具有大量出色的可视化效果和示例，比本简介要深入得多，而且重要的是它具有所有相关的工作，包括关于程序和声明式证明的大量内容。这篇博客文章，论文和演讲都是使用Alectryon构建的。

如果这是您第一次访问此博客，则可能需要先阅读有关浏览这些可视化内容的简短教程，然后再继续本文的其余部分。

通过将Coq源文件转换为网页，使读者可以在其浏览器中重现样张（“ Proviola”风格），从而更轻松地浏览Coq开发（即使这些开发不是用识字的风格编写）。作为一个演示，我记录了完整构建Flocq库的目标和响应。

编写包含Coq源代码和解释性散文的文档，或者从包含特殊指令的文本文件（Coq参考手册中使用的“ coqtex”和“ coqrst”样式）开始，或者从包含特殊注释的Coq文件（“ coqdoc”开始）样式，用于CPDT，软件基础等）。

Alectryon的论文，这篇博客文章以及我在SLE上的演讲都是前者的示例（它们以reStructuredText（一种类似于Markdown的标记语言）编写）；作为另一个示例，这是FRAP的一章和CPDT的一章，它们被手动转换为reStructuredText（将URL更改为.rst以查看源代码）。

不支持将文档的某些部分附加到特定的代码部分，例如定义，公理，变量等。正如我过去写的那样，我认为这是一项不同的工作（“文档字符串”），最好由以下人员处理Coq本身（类似于它如何跟踪定义的主体和位置）。 Alectryon还不像Coqdoc一样支持超链接Coq术语到其定义，但我计划最终实现这一点。

Alectryon的主要目的是记录Coq的输出并将它们与相应的输入进行交织以创建交互式网页：

定理rev_length：l：list nat，长度（rev l）=长度l。证明。介绍影片归纳l为[| n l'IHl']。 -（* l←[] *）自反性。 -（* l←_ :: _ *）简单。重写app_length。重写Nat.add_comm。简单重写IH'。反身性。 Qed。检查rev_length。

因为这是一个交互式网页，所以我们可以对输出进行各种后处理，例如使用MathJax使数学证明更具可读性：

\（\ newcommand {\ ccQ} {\ mathbb {Q}} \\）\（\ newcommand {\ ccNat} {\ mathbb {N}} \）\（\ newcommand {\ ccSucc} [1] {\ mathrm {S } \：＃1} \）\（\ newcommand {\ ccFrac} [2] {\ frac {＃1} {＃2}} \\）\（\ newcommand {\ ccPow} [2] {{＃1} ^ {＃2}} \）\（\ newcommand {\ ccNot} [1] {{\\ lnot＃1}} \）\（\ newcommand {\ ccEvar} [1] {\ textit {\ texttt {＃1}} } \）\（\ newcommand {\ ccForall} [2] {\ forall \：＃1。\;＃2} \）\（\ newcommand {\ ccNsum} [3] {\ sum _ {＃1 = 0} ^ {＃2}＃3} \）

引理高斯（Lemma Gauss）：∀n，2 *（nsum n（fun i => i））= n *（n +1）。证明。感应n cbn [nsum]。 -（* n←0 *）自反性。 -（* n←S _ *）重写Mult.mult_plus_distr_l。重写IHn。环。 Qed。

…或使用浏览器对矢量图形的本机支持，将以布尔值列表形式编码的生命游戏板渲染为小图像：

定义滑翔机：= [[0; 1; 0; 0; 0]; [0; 0; 1; 0; 0]; [1; 1; 1; 0; 0]; [0; 0; 0; 0; 0]; [0; 0; 0; 0; 0]]。计算9（iter conway_life滑翔机）。

…或使用图形库绘制可视化效果，以使其更清晰地显示使用Coq.MSets.MSetRBT构建红黑树时发生的情况。

定义build_trees（leaves：list nat）：= List.fold_left（fun trs n => RBT.add n（hd RBT.empty trs）:: trs）leaves [] |> List.rev。计算build_trees [1; 2; 3; 4; 5]。计算build_trees [2; 1; 4; 3; 6]。

这些可视化真的有用吗？您将成为法官：这是带有纯文本输出的红黑树示例的外观：

计算build_trees [1; 2; 3; 4; 5]。计算build_trees [2; 1; 4; 3; 6]。

即使您不使用Alectryon的识字编程功能，这些网页也具有方便浏览之外的另一个优势：因为它们同时记录了您的代码和Coq的响应，所以它们可以永久记录您的发展，免受Bitrot侵害并适合存档。

除了从独立的Coq文件生成网页之外，Alectryon还可以帮助您编写文档，博客文章以及各种其他融合证明和散文的文档。 Alectryon的扫盲模块实现了从Coq到reStructuredText以及从reStructuredText到Coq的翻译，这使您可以在同一文档的两个独立视图之间进行切换：一个最适合编辑代码，另一个最适合编辑reST散文。具体而言，Alectryon知道如何在以下两者之间进行转换：

============================写作决策程序================== ============这里是归纳类型：.. coq ::归纳偶数：nat-> Prop：= | EvenO：偶数O |偶数S：forall n，偶数n->偶数（S（S n））。 .. note ::它有两个构造函数：.. coq ::展开Check EvenO。检查EvenS。

（* | ============================写作决策程序=============== ===============这是一个归纳类型：| *）归纳偶数：nat-> Prop：= | EvenO：偶数O | EvenS：forall n，偶数n->偶数（S（S n））。 （* | ..注意：:它具有两个构造函数：| *）检查EvenO。检查EvenS。

因为这些转换（基本上）是彼此相反的，所以您不必选择这两种样式中的一种并坚持使用（或更糟的是，要维护同一文档的两个副本，来回复制粘贴的片段）。取而代之的是，您可以在使用自己喜欢的Coq IDE编辑注释中的散文，同时使用自己喜欢的reStructuredText编辑器来编写散文的同时自由地使用它来编写代码和证明。

选择reStructuredText作为注释的标记语言的原因是，其设计时考虑了可扩展性，这使我可以将Alectryon插入reStructuredText的标准Docutils和Sphinx编译管道中（Sphinx是Haskell，Agda，Coq和使用Python编写）。这是此博客的撰写方式，实际上，如果您想了解它的外观，则可以下载源。这也是我制作SLE2020幻灯片的方式（按p查看演示者的注释），也是我撰写SLE2020论文的方式。

一个小的Emacs软件包（alectryon.el），使您可以在Coq和reST之间快速切换。下面的屏幕快照演示了此功能：左侧是coq模式的Software Foundations编辑摘录的Coq视图。右边是第一个模式缓冲区中同一摘录的reST视图。转换是透明的，因此编辑任一视图都会更新磁盘上的同一.v文件。请注意高亮显示了在两侧都显示reStructuredText警告：

Alectryon的语法突出显示是使用Pygments完成的，但它使用了更新的Coq语法，其中包含直接从参考手册中提取的关键字和命令的数据库（最终，这部分应在上游合并，数据库生成工具应合并到Coq参考手册；有时我会写一篇单独的博客文章。

Alectryon的设计是非常模块化的，因此，如果您要将其用于其他目的，则仅使用其中的某些部分就很容易。特别是，它的核心是一个简单的API，该API可以获取一系列代码段，并通过SerAPI将其输入到Coq，并记录目标和消息。此功能在命令行（以json作为输入并产生json作为输出）以及Python模块中公开：

>>>从alectryon.core导入注释>>>注释（[[示例xyz（H：False）：正确。（* ... *）精确I. Qed。 （句子=“示例xyz（H：False）：是。”，响应= []，目标= [CoqGoal（名称='2'，结论='真实'，假设= [CoqHypothesis（名称='H'，身体= None，type ='False'）]）））），CoqText（string ='（* ... *）'），CoqSentence（句子='exact I.'，响应= []，目标= []）， CoqText（字符串=''），CoqSentence（句子='Qed。'，响应= []，目标= []）]，[CoqSentence（句子='Print xyz。'，响应= ['xyz = fun _：False =>我\ n：错误->正确']，目标= []）]

Alectryon使用JSON缓存来加快连续运行的速度，但是即使性能不是问题，缓存也可以为嵌入式Coq片段提供一种非常有用的回归测试形式。没有这样的测试，很容易对库中看似无害的更改以微妙的方式破坏其文档。例如，您可能具有以下片段：

如果将plus重命名为Nat.add并添加一个兼容标记，这将是您的文档默默地变成的，没有错误或警告让您意识到出了问题：

这是参考手册中的一个常见问题，我们实施了变通方法来捕获最糟糕的情况（更改导致片段摘要打印错误而不是成功执行）。但是，如果您将Alectryon的缓存签入源代码管理中，则以下内容将非常清楚地显示出来：

“ contents”：“ Print plus。”，“ messages”：[{“ _type”：“ message”，-“ contents”：“ plus = \ nfix plus（nm：nat）{struct n}：nat：=…” +“目录”：“符号加：= Nat.add”}

所有这些功能都通过Alectryon的README文件中记录的命令行界面公开。这个项目已经开发了一年多，但是仍然有很多困难，所以请期待错误，并报告他们！

入门Alectryon的最简单方法是非常像coqdoc一样使用它，但是在以（* |和| *）分隔的特殊注释中使用reStructuredText语法，例如在这个假设的even.v文档中：

（* | =======标题=======散文。*强调*; **重点强调**;``code'';`coq code`;`link `__。 | *）归纳偶数：nat->道具：= | EvenO：偶数O | EvenS：forall n，偶数n->偶数（S（S n））。

…然后可以使用../alectryon.py --frontend coq + rst --backend网页even.v -o even.html将其编译成静态网页。

这就是我为FRAP和CPDT做的。对于软件基础和Flocq，我使用了一个兼容层，该层结合了Alectryon来呈现代码和coqdoc来呈现散文：

Alectryon非​​常容易与支持Sphinx或Docutils的平台和工具集成，例如Pelican，readthedocs，Nikola等。（从长远来看，我希望将Coq的参考手册迁移到Alectryon。目前，它使用的是coqrst，这是该版本的先前版本我几年前写的Alectryon是基于coqtop而不是SerAPI的。

import alectryon import alectryon.docutils from alectryon.html import ASSETS＃注册“ .. coq ::”指令alectryon。 docutils。 register（）＃复制Alectryon的样式表alectryon_assets = path。 relpath（ASSETS.PATH，PATH）STATIC_PATHS。 append（alectryon_assets）EXTRA_PATH_METADATA [alectryon_assets] = {'path'：'static / alectryon /'}＃复制自定义的Pygments主题，该主题与pth的主题/颜料有很好的对比（“ tango_subtle.css”，“ tango_subtle.min.css ”）：EXTRA_PATH_METADATA [path。 join（alectryon_assets，pth）] = \ {'path'：path。加入（'theme / pygments /'，pth）}

尽管使用alectryon.sphinx.register（）代替，但对于Sphinx也需要类似的步骤。我听说正在进行与其他博客平台集成的工作。

reStructuredText的选择有些随意，因此这不是Alectryon的硬性依赖。将其与其他输入语言（例如LaTeX，Markdown等）结合起来应该相对简单一些-我只是没有时间来做。甚至还有一种输出模式，它将Coq片段作为输入并为每个片段生成单独的HTML代码段，从而使集成更加容易。有关更多信息，请参见Alectryon的自述文件。

例如，我为Coqdoc制作了一个兼容垫片，该垫片使用Alectryon来呈现Coq代码，响应和目标，但是调用coqdoc来呈现（**…**）注释的内容。在发行版的文件cli.py中查找coqdoc，以了解其工作原理。

在reStructuredText文档中，.. coq ::块中的代码在编译时执行；目标和响应与代码一起记录和显示。这是一个例子：

显示所有目标和响应归纳式偶数：nat-> Prop：= | EvenO：偶数O |偶数S：forall n，偶数n->偶数（S（S n））。 Fixpoint even（n：nat）：bool：=用|匹配n 0 => true | 1 =>假| S（S n）=>连n个结尾。引理even_Even：forall n，偶数n = true->偶数n。修复IHn 1.将n破坏为[| [| ]]。全部：简单。全部：简介。 -（*基本情况：0 *）构造函数。 -（*基本情况：1 *）区分。 -（*归纳式：[S（S _）] *）构造函数。汽车。 Qed。

Coq片段旁边的小气泡（例如：）表明它产生了输出：您可以将鼠标悬停，单击或点击该片段以显示相应的目标和消息。

如上所述，在文档的开头添加了一个特殊的“显示所有目标和响应”复选框。可以通过添加显式..alectryon-toggle ::指令来调整其位置。

这些功能不需要JavaScript（仅是现代CSS实现）。可选地，可以使用一个小的Javascript库来启用键盘导航，从而显着提高可访问性。您可以在此页面上按Ctrl +↑或Ctrl +↓进行尝试。

引理some_not_none：全部{A：类型}（a：A），有的a = None-> False。进度介绍。更改（将a与| a _ => False | None => True匹配）。在*中将（Some _）设置为s。透明体。与|匹配目标[H：？x = _ |-context [？x]] =>重写H结束。首先[确切的我]。显示证明。已定义。评估计算some_not_none。

指令参数和特殊注释可用于自定义Coq块的显示。 Alectryon的文档提供了详细信息，但以下是一些示例：

.. coq ::展开目标True / \ True。 （* .fold *）分割。 -（* .fold *）idtac“你好”。 （* .no-goals *）适用I.-自动。 Qed。

当然，如果要隐藏输入但显示一些输出（如.no-input，.messages或.goals），则需要添加.unfold，因为显示输出的常用方法是（点击输入）将不可用。

默认的alectryon.css样式表支持两种显示模式：proviola样式（两个窗口并排，一侧显示代码，另一侧显示目标），以及该Blog的样式（当窗口较大时，目标显示在每个片段的旁边）足够，并低于输入线）。两种模式都支持单击输入行以在其下方显示输出。您可以通过以下方式选择一种模式

在Alectryon中，绝大多数处理时间都花费在解析和解析S表达式上。我本人亲自编写了Alectryon的s-exp解析器，以最大程度地减少依赖关系，并使它相当快地运行，但是，如果您是Python速度极客，那么您肯定应该看看（我想知道cython是否对您有所帮助-我不确定它有多好在字节串操作）。希望一旦SerAPI支持JSON，此问题（以及相应的代码）将消失。

默认的HTML后端无需JavaScript就可以使用-仅使用CSS。它将状态存储在复选框中：每条输入行都是一个隐藏复选框的标签，该复选框的状态通过条件CSS规则控制输出的可见性。整个文档范围内的切换以相同的方式工作，覆盖所有单独的复选框。您可以在地址栏中输入javascript：document.querySelector（“ link [href $ = \” alectryon.css \“]”）。remove（）来查看没有样式的页面（所有响应，目标和复选框都将是显示，那么您当然会失去互动性）。

Coq中的块注释相对复杂：解析器不仅需要跟踪嵌套的注释，还需要跟踪嵌套的字符串，这是我们从OCaml继承的奇数（必须正确匹配注释中的字符串定界符，并且忽略其中的注释标记）。这样做的目的是使注释更加健壮，以便将有效代码段包装在（*…*）中将始终有效。例如，以下是有效的OCaml代码：

在（*中让a =“ x *）y”在*）中使a =“ x *）y”

…虽然您可能会从语法突出显示的残缺中猜到，但是没有多少工具能够正确处理此问题–它会很高兴地破坏Emacs的tuareg模式，Pygments等。

但是，整个问题在Coq中尚无定论，因为*）是相当普遍的令牌，并且不被禁止（与OCaml不同）：

单行注释很好地解决了这个问题。我已经看到在OCaml和Coq中使用（*）的建议，但是（1）键入非常不愉快，（2）它会破坏当前支持OCaml的每个编辑器，并且（3）它没有自然变体（（（*是常规注释，而（**是coqdoc注释；（*）的识字变体是什么？不是（**），因为那是