我见过很多 Coq 策略，它们在功能上是相互重叠的。
例如，当你在假设中得到确切的结论时，你可以使用assumption, apply, exact, trivial，也许还有其他人。其他例子包括destruct and induction对于无感类型（??）。
我的问题是：
有没有minimal set of basic战术（不包括auto等）是完整的，从这个意义上说，这个集合可以用来证明任何关于自然数函数的 Coq 可证明的定理？
理想情况下，这套最小的完整策略中的策略是基本的，因此每个策略仅执行一种（或两种）功能，并且人们可以轻松理解它的作用。
Coq 中的证明只是正确类型的术语。策略通过将较小的子术语组合成更复杂的子术语来帮助您构建这些术语。因此，最基本的基本策略集只包含exact正如康斯坦丁提到的那样。
The refine策略允许你直接给出证明项，但存在会产生子目标的漏洞。基本上任何策略都只是一个例子refine tactic.
但是，如果您只想首先考虑一组最小的策略，我会考虑intro{s}, exists, reflexivity, symmetry, apply, rewrite, revert, destruct and induction. inversion可能也会很快派上用场。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
