我见过很多功能上相互重叠的 Coq 策略。
例如，当您在假设中有确切的结论时，您可以使用assumption, apply, exact, trivial, 或者其他。destruct其他示例包括induction非归纳类型（？？）。
我的问题是：
是否存在完整的最小基本策略集（不包括auto等），从某种意义上说，该集可用于证明任何 Coq 可证明的关于自然数函数的定理？
理想情况下，这个最小完整集合中的策略是基本的，因此每个人只执行一个（或两个）功能，并且可以很容易地理解它的作用。
Coq 中的证明只是一个正确类型的术语。策略通过将较小的子术语组合成更复杂的子术语来帮助您构建这些术语。exact因此，正如康斯坦丁所说，最小的基本战术集只包含战术。
该refine策略允许您直接给出证明条件，但会产生子目标的漏洞。基本上任何策略都只是该refine策略的一个实例。
但是，如果您只想首先考虑一组最小的策略，我会考虑intro{s}, exists, reflexivity, symmetry, apply, rewrite, revert,destruct和induction。inversion也可能很快派上用场。