Coqには最小限の戦術がありますか？

Question

私は、機能において互いに重なり合っているCoqの戦術をたくさん見てきました。例えば

、あなたは仮説の正確な結論を持っているとき、あなたはassumption、apply、exact、trivial、そしておそらく他の人を使用することができます。その他の例には、非誘導型（??）の場合はdestructとinductionが含まれます。

私の質問は次のとおりです。

は、このセットは任意のコックを証明するために使用することができますという意味で、完了です基本戦術（つまりautoを除外し、そのような）の最小限セットがあります自然数の関数に関する証明可能な定理？

この最小完全セットの戦術は理想的には基本的なものであり、それぞれが1つ（または2つ）の機能のみを実行し、その機能を容易に理解することができます。

Answer 1

Coqの証明は、正しいタイプの用語に過ぎません。戦術は、より小さなサブ用語をより複雑なものに組み合わせることによって、これらの用語を構築するのに役立ちます。したがって、基本的な戦術の最小限のセットは、コンスタンチンが述べたように、exactの戦術しか含んでいません。

refineの戦術では、証明の言葉を直接与えることができますが、サブゴールを生成する穴があります。基本的にどんな戦術も、refine戦術の例です。

あなたが最初の戦術の唯一の最小セットを考慮したい場合は、私がintro{s}、exists、reflexivity、symmetry、apply、rewrite、revert、destructとinductionを検討します。 inversionもすぐに便利になるかもしれません。