在Coq中编写Ltac时，`match`是否比`rewrite`更快？

这是个非常务实的问题——毕竟在大型策略的内部循环里，哪怕一点点性能差异累积起来都会影响整体速度。我来分享下实际使用和测试中的观察：

核心差异：rewrite的失败开销 vs match的匹配开销 #

• rewrite的失败路径成本：当rewrite尝试应用引理却失败时，它背后做了不少工作：先是尝试匹配引理结论与目标（或指定假设），匹配失败后还要回溯、清理临时状态，这些操作都有一定开销。尤其是引理结构复杂、目标子项繁多时，这个失败成本会被放大。
• 手写match的提前过滤：如果先用match goal精准匹配出符合条件的目标/假设结构，再调用rewrite，相当于提前把肯定会失败的情况过滤掉了。这种情况下rewrite只会在大概率成功的场景下执行，自然能减少不必要的无效操作开销。

什么时候差异最明显？ #

• 高频失败场景：如果内部循环里rewrite的失败率极高（比如90%以上的调用都会失败），手写match提前过滤的性能提升会非常显著。我曾在处理复杂归纳结构的策略中，把盲调rewrite改成先match匹配，整体速度提升了30%左右。
• 简单场景例外：如果rewrite用的是极简单的引理（比如trivial的x = x等式），或者目标结构非常单一，那rewrite的失败开销其实很小。这时候match自身的模式匹配开销，可能和rewrite的失败开销持平，甚至反而更慢。

实际测试建议 #

Coq的性能会受很多细节影响（比如引理定义方式、目标复杂度、Coq版本），所以最靠谱的方式是自己做小测试：

• 写两个版本的策略：一个盲调rewrite，一个先match再调用rewrite
• 用Time命令分别运行两个策略，对比执行时间
• 如果是循环执行的策略，尽量让它跑足够多次，这样性能差异会更直观

注意：新版本Coq的优化 #

值得一提的是，Coq 8.15+版本对rewrite的失败路径做了不少优化，比如更快的模式匹配回溯逻辑。如果用的是较新的Coq版本，rewrite的失败开销可能比旧版本小很多，这时候两者的性能差异会被缩小。

内容的提问来源于stack exchange，提问作者Joachim Breitner