Coq中是否有一套最基本的战术？ [英] Is there a minimal complete set of tactics in Coq?

问题描述

我已经看到许多Coq策略在功能上相互重叠。

I have seen a lot of Coq tactics that are overlapping each other in function.

例如，当您在假设中有确切结论时，可以使用假设，应用，精确，简单，甚至其他。其他示例包括 destruct 和 induction 用于非归纳类型（??）。

For example, when you have the exact conclusion in the hypothesis, you can use assumption, apply, exact, trivial, and maybe others. Other examples include destruct and induction for non-inductive types(??).

我的问题是：

是否存在基本策略的 minimum 组（即不包括完整的 auto 及其类似的东西），就这个意义而言，该集合可用于证明任何有关自然数函数的Coq可证明定理？

Is there a minimal set of basic tactics (that excludes auto, and its like) that is complete, in the sense that this set can be used to prove any Coq-provable theorems about functions of natural numbers?

此最小组合中的策略在理想情况下将是基本的，因此每个策略仅执行一个（或两个）功能，并且一个人可以轻松了解其功能。

The tactics in this minimal complete set would be ideally basic, so that each perform one (or two) function only and one can easily understand what it does.

推荐答案

Coq中的证明只是正确类型的术语。通过将较小的子术语组合为更复杂的子术语，策略可以帮助您构建这些术语。因此，正如康斯坦丁所提到的那样，最少的基本策略集仅包含精确策略。

A proof in Coq is just a term of the correct type. Tactics help you build these term by combining smaller sub-terms into more complex ones. Therefore, the minimal set of basic tactics would only contain the exact tactic, as Konstantin mentioned.

优化策略可让您直接给出证明条款，但带有会产生子目标的漏洞。基本上，任何策略只是 refine 策略的一个实例。

The refine tactics allows you to directly give proof terms, but with holes that will generated sub-goals. Basically any tactic is just an instance of the refine tactic.

但是，如果您只想先考虑一个最少的策略集，我会考虑简介{s} ，存在，自反性，对称，应用，重写 ，还原，销毁和归纳。 反转也可能会很快派上用场。

However, if you want to first consider only a minimal set of tactics, I would consider intro{s}, exists, reflexivity, symmetry, apply, rewrite, revert, destruct and induction. inversion might come in handy rather quickly too.

这篇关于Coq中是否有一套最基本的战术？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！