Coq定理的高速计算

Question

即使在非常简单的情况下，我也必须等到 Coq 完成计算。

我知道 "Asynchronous and Parallel Proof Processing"，但我想我的代码有内在缺陷，所以我想获得一些关于 guidelines/best 校样样式实践的参考或建议。例如：

尝试使用定义而不是定理，
使用编译器。使用并行处理。使用更好的硬件。
不要使用占位符，填写每个参数，例如 (@functionname var1 ... varn)
分号(;)而不是句号(.)
在部分中使用定义比在证明中使用 "set (f:=term)." 快得多。（可能是因为每 "set" 得到额外的时间来打印。甚至检查空。）

如何加速 Coq？（如有错误请指出，以上是我的实践所得。）

计算的最关键阶段是什么以及如何使用它们？

Answer 1

圣杯是分析您的代码并优化热点。在 Coq >= 8.6 中，您可以 Set Ltac Profiling. 和 Reset Ltac Profile. 和 Show Ltac Profile. 来分析策略。如果你用 -time 参数调用 coqc，你会得到逐行的计时信息；一点 sed 技巧可以为您整理信息：

coqc -time foo.v | sed s'/^\(.*\) \([0-9\.]\+ secs.*\)$/ /g' | sort -h

在 Coq >= 8.8 中，您可以 Set NativeCompute Profiling 分析原生计算（例如 Eval native_compute in (slow program here)）。这会产生您可以在 GNU/Linux 上使用 perf report 可视化的痕迹。有关详细信息，请参阅 this bug report。

如果遇到其他瓶颈，您要么必须善于猜测，说服开发人员添加更多分析工具，分析运行ning coq 二进制文件，要么说服开发人员值得他们花时间为您分析您的代码。（当缓慢指向 Coq 中的效率错误时，有时我可以让 Pierre-Marie Pédrot 分析我的代码。）

一个有用的做法是始终在每次提交时分析您的代码。在 Coq >= 8.7 中，有 Makefile 个目标 make-pretty-timed-before、make-pretty-timed-after 和 print-pretty-timed-diff 来获得很好的排序表，其中列出了你的回购协议的两个状态之间的每个文件的编译时间差异.您可以使用 make TIMING=before、make TIMING=after、make all.timing.diff.

获取每行信息

您可能也有兴趣查看 Experience Implementing a Performant Category-Theory Library in Coq (more media here), and perhaps also the slide deck for the presentation of that paper (pdf) (pptx with presenter notes)。

Coq 在很多地方都可能很慢，尽管你提到的大部分事情都是无关紧要的。按顺序浏览您的：

Theorem和Definition是同义词，唯一的区别是Definition支持:=而Theorem不支持
没有针对 Coq 的优化编译器，尽管更好的硬件、更多的 RAM、更快的 CPU 肯定有帮助。并行处理也是如此。在这一点上，文件级并行性往往比证明级并行性更好。我倾向于尽可能多地拆分我的文件，进行细粒度的导入，这样库加载时间就不是问题，并使用 make -j.
填满每一个论点更可能是伤害而不是帮助。您会产生额外的统一成本，尤其是当您用来填充参数的术语很大时。您通过填写参数所做的真实事情是用 evar 的创建与统一进行交易。统一通常较慢。但是，如果您有任何漏洞需要通过规范结构解析、类型类解析来填充，或者需要其他回溯和展开内容或刷新宇宙变量，填充它们可以大大加快速度。
我认为证明脚本中分号和句点之间的区别只在交互模式下很重要（在 coqtop/CoqIDE/ProofGeneral/etc 中，而不是在运行宁 make 中）。如果您测试它并发现其他情况，请告诉我。
这是非常正确的，对印刷和其他方面都有影响。 set 本身不会因为打印而变慢，而是因为它试图在您的目标中找到该术语的所有出现（愚蠢的是，减少了一些（beta-iota？我不能召回），而不是句法相等），并用新的假设替换它们。如果您不需要此行为，请使用 pose 而不是 set。此外，大的上下文变量可以减慢取决于上下文大小的策略，这就是为什么 Definition 在部分中更快。

关于我运行的其他想法：

选择好的抽象障碍，虔诚地尊重它们。每次打破抽象障碍，你都会付出汗水和泪水的代价。（选择好的抽象障碍是非常困难的。通常我通过复制现有的数学抽象或发表的论文来做到这一点。我已经设法完全从头开始生成一个好的抽象障碍，在某种意义上，在过去五年中恰好一次。抽象事后看来，障碍可以用 "insight" 来描述 "when writing C-like code, every function takes one tuple as an argument and returns one tuple as a result.")
如果您要进行反思性证明，请选择好的算法。如果你使用一元自然数，或者你的算法有指数运行ning 时间，你的证明会很慢。
在 Coq < 8.7 中，evar-map 规范化会导致大量开销。（支持 Pierre-Marie 用他的 EConstr 分支解决这个问题。）
缓慢 End Section（有时 Defineds 缓慢）通常是由重新散列问题引起的。要解决这个问题，请祈祷。（或者成为 Coq 开发人员并修复 Coq。）
防护检查器在检查具有大体的 fixes 时非常慢（也许只有在存在 beta-iota-zeta reduxes 的情况下？）。解决方法是将正文提取到单独的定义中。例如，而不是写

Fixpoint length A (ls : list A) : nat :=
  match ls with
  | nil => 0
  | cons _ xs => S (length _ xs)
  end.

你可以写

Definition length_step
             (length : forall A, list A -> nat)
             A (ls : list A)
    : nat
    := match ls with
       | nil => 0
       | cons _ xs => S (length _ xs)
       end.
Fixpoint length A (ls : list A) : nat
  := length_step length A ls.

请注意，Coq 会自由地（有时不一致地）内联 let x := ... in ... 语句，这很容易导致指数定义内化时间。
进行具体化时，规范结构速度很快但难以阅读，Ltac 大约慢 2 倍，类型类解析可能再次慢 2 倍（或者可以与 Ltac 具体化的速度相同）。希望 Ltac2 完成后情况会更好。
simpl 在大范围内非常慢

稍后我可能会回来添加更多内容（并随时在评论中提出建议供我添加），但这是一个半体面的开始。

Coq定理的高速计算

High-speed calculation of Coq's theorems

profiling

coq