我见过很多功能上相互重叠的 Coq 策略。
例如，当你在假设中有确切的结论时，你可以使用assumption、apply、exact、trivial，也许还有其他。其他示例包括用于非归纳类型的 destruct 和 induction (??)。
我的问题是：
是否有一套最小基本战术（不包括auto等）是完整的，从某种意义上说，这套战术可用于证明任何关于自然数函数的 Coq 可证明定理？
这个最小的完整集合中的策略在理想情况下应该是基本的，因此每个人只执行一个（或两个）功能，并且可以很容易地理解它的作用。
【问题讨论】：
exact 策略足以证明任何目标。如果您不想一次构建该术语，可以使用refine。
标签： coq coq-tactic
Coq 中的证明只是类型正确的术语。策略通过将较小的子术语组合成更复杂的子术语来帮助您构建这些术语。因此，正如 Konstantin 所提到的，最小的基本策略集将仅包含 exact 策略。
refine 策略允许您直接给出证明条件，但存在会产生子目标的漏洞。基本上任何策略都只是refine 策略的一个实例。
但是，如果您只想首先考虑一组最少的策略，我会考虑intro{s}、exists、reflexivity、symmetry、apply、rewrite、revert、@ 987654331@ 和induction。 inversion 也可能很快派上用场。
【讨论】：
reflexivity 只是 apply eq_refl 如果你不使用 setoids，对称也是一个应用程序；存在是constructor，而它也只是apply。你经常使用revert吗？另一方面，rewrite 和 simpl 可能会很好地添加到此列表中。
rewrite，它只是应用了具有正确形状的引理。正如我所说，一切都下降到refine（直接写证明项）。但我承认，rewrite 应该在列表中。我经常使用 revert，因为我对依赖类型做了很多归纳，这很有帮助。
reverting，确实 :) rewrite 确实通常只是一个归纳原理的应用，但我几乎从不使用它。
reflexivity 只是起初有点像apply eq_refl，如果不成功，它有几个后备，比如setoid_rewrite 和one_constructor（一种非公开的策略，它如果目标是单构造子归纳类型，则尝试找到证明项）。例如。 reflexivity 解决了像 True 这样的目标。