coq - Coq 中是否有一套最小的完整策略？

Question

我见过很多在功能上相互重叠的 Coq 策略。

例如，当您在假设中有确切的结论时，您可以使用 assumption , apply , exact , trivial ，也许还有其他人。其他示例包括 destruct和 induction对于非归纳类型(??)。

我的问题是:

是否有最小集 基本策略(不包括 auto 等)是完整的，因为这个集合可以用来证明任何关于自然数函数的 Coq 可证明定理？

这个最小的完整集合中的策略理想情况下是基本的，这样每个策略只执行一个(或两个)功能，并且可以很容易地理解它的作用。

Answer 1

Coq 中的证明只是一个正确类型的术语。策略通过将较小的子术语组合成更复杂的子术语来帮助您构建这些术语。因此，基本策略的最小集合将仅包含 exact战术，正如康斯坦丁提到的。
refine战术允许您直接给出证明条款，但会产生子目标的漏洞。基本上任何策略都只是 refine 的一个实例。战术。

但是，如果您只想首先考虑一组最少的策略，我会考虑 intro{s} , exists , reflexivity , symmetry , apply , rewrite , revert , destruct和 induction . inversion也可能很快派上用场。