Coq定理的高速计算

Question

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

我了解“异步和并行的证明处理”，但是我想我的代码具有固有的弊端，因此我想对证明/证明样式的最佳实践获得一些参考或建议。例如：

1. 尝试使用定义而不是定理，

2. 使用编译器。使用并行处理。使用更好的硬件。

3. 不要使用占位符，填写每个参数，例如（@functionname var1 ... varn）

4. 用分号（;）代替句点（。）

5. 使用“部分”中的“定义”代替“ set（f：= term）”要快得多。在证明中。（可能是因为每个“设置”都有额外的打印时间。甚至要检查是否为空。）

如何加快Coq？（如果我在上面的项目中有错误，请说。它们是根据我的实践得出的。）

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

Answer 1

圣杯是分析您的代码并优化热点。在勒柯克> = 8.6，你可以Set Ltac Profiling.和Reset Ltac Profile.和Show Ltac Profile.对个人资料的战术。如果您coqc使用-time参数进行调用，您将获得逐行计时信息。有点sed技巧可以为您分类信息：

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

在Coq> = 8.8中，您可以Set NativeCompute Profiling分析本机计算（例如Eval native_compute in (slow program here)）。这将产生可perf report在GNU / Linux上可视化的痕迹。有关更多信息，请参见此错误报告。

如果遇到其他瓶颈，您要么必须擅长猜测，要么说服开发人员添加更多性能分析工具，分析正在运行的coq二进制文件，或者说服开发人员值得花时间为您分析代码。（当速度变慢指向Coq中的效率错误时，有时我可以让Pierre-MariePédrot来分析我的代码。）

一种有用的做法是始终在每次提交时都对代码进行概要分析。在Coq> = 8.7中，有Makefiletarget make-pretty-timed-before，make-pretty-timed-after和，print-pretty-timed-diff用于获得存储库两个状态之间每个文件编译时间差异的排序表。你可以得到每行信息有make TIMING=before，make TIMING=after，make all.timing.diff。

您可能也有兴趣查看Coq中实施绩效类别理论库的经验（此处有更多媒体），并且可能还有介绍该论文的幻灯片（pdf）（带有演示者注释的pptx）。

虽然您提到的大多数内容都无关紧要，但Coq在许多地方可能会变慢。依次检查您的：

1. Theorem并且Definition是同义词，唯一的区别是Definition支持:=和Theorem不支持。
2. 没有针对Coq的优化编译器，尽管更好的硬件，更多的RAM，更快的CPU绝对有帮助。和并行处理一样。在这一点上，文件级并行性往往比证明级并行性更好。我倾向于尽可能多地分割文件，具有细粒度的导入，以便库加载时间不是问题，并使用make -j。
3. 充实每一个论点比帮助更有可能受到伤害。您将承担额外的统一成本，尤其是当您要填充参数的术语很大时。通过填写参数来完成的工作是将evar创建与统一进行交易。统一通常比较慢。但是，如果您有任何漏洞被规范结构解析，类型类解析填补，或者需要其他回溯和展开操作或刷新Universe变量，则将其填充可以大大加快操作速度。
4. 我认为证明脚本中的分号和句点之间的区别仅在交互模式下才有意义（在coqtop / CoqIDE / ProofGeneral / etc中，运行时不重要make）。让我知道您是否进行测试，否则发现其他问题。
5. 这是事实，对印刷和其他事物都有影响。该set本身不会因打印速度慢，而是因为它试图找到术语中所有出现的你的目标（愣神，最多有所下降（β-丝毫的事实？我不记得），而不是直到句法平等），并用新的假设取代它们。如果您不需要这种行为，请使用pose而不是set。此外，较大的上下文变量可能会降低取决于上下文大小的策略，这就是为什么Definition在各节中更快的原因。

关于我遇到的事情的其他想法：

• 选择好的抽象障碍，并认真地尊重它们。每当您打破抽象障碍时，您都会付出汗水和眼泪。（挑选好的抽象障碍非常困难。通常，我通过复制现有的数学抽象或已发表的论文来做到这一点。在某种意义上，我设法在过去的五年中完全从头开始产生了一个好的抽象障碍。事后看来，障碍可以用“洞察力”来描述，即“在编写类似C的代码时，每个函数都将一个元组作为参数，并返回一个元组作为结果。”）
• 如果您要进行反射证明，请选择好的算法。如果您使用一元自然数，或者您的算法具有指数运行时间，则证明速度会很慢。
• 在Coq <8.7中，evar-map规范化会在很大程度上产生大量开销。（支持Pierre-Marie通过其EConstr分支解决此问题。）
• 慢速End Section（有时是慢速Defined）通常是由重新哈希处理问题引起的。要解决此问题，请双手合十祈祷。（或成为一名Coq开发人员并修复Coq。）
• 保护性检查器在检查fix具有大身体的裸露物体时非常慢（也许仅在存在β-碘-ζ-还原酶的情况下？）。解决方法是将主体提取到单独的定义中。例如，而不是写作

定点长度A（ls：列表A）：nat：=
  与ls匹配
  | 零=> 0
  | 缺点_ xs => S（长度_ xs）
  结束。

你可以写

定义length_step
             （长度：全部A，列表A-> nat）
             A（ls：清单A）
    ：nat
    ：=匹配ls与
       | 零=> 0
       | 缺点_ xs => S（长度_ xs）
       结束。
定点长度A（ls：列表A）：nat
  ：= length_step长度A ls。

• 请注意，Coq将自由地（有时会不一致）内联let x := ... in ...语句，这很容易导致指数定义的内部化时间。
• 进行规范化时，规范结构快速但难以阅读，Ltac慢约2倍，类型类分辨率又可以慢2倍（或可以与Ltac规范化相同的速度）。希望Ltac2完成后情况会更好。
• simpl 总体来说很慢

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