機能が重複している Coq タクティックをたくさん見てきました。
たとえば、仮説に正確な結論がある場合はassumption、apply、exact、trivial、およびおそらく他のものを使用できます。他の例にはdestruct、induction非誘導型 (??) の と が含まれます。
私の質問は：
自然数の関数に関するCoq証明可能な定理を証明するためにこのセットを使用できるという意味で、完全な基本的な戦術の最小セット( などを除く)はありますか?auto
この最小限の完全なセットの戦術は、それぞれが 1 つ (または 2 つ) の機能のみを実行し、その機能を簡単に理解できるように、理想的には基本的なものです。
Coq での証明は、正しい型の項にすぎません。戦術は、小さなサブ用語をより複雑なサブ用語に組み合わせることで、これらの用語を構築するのに役立ちます。したがって、基本的な戦術の最小限のセットには、exactコンスタンティンが述べたように、戦術のみが含まれます。
戦術では、refine証明項を直接与えることができますが、サブゴールを生成する穴があります。基本的に、戦術は戦術の単なるインスタンスですrefine。
ただし、最初に最小限の戦術セットのみを検討したい場合はintro{s}、exists、reflexivity、symmetry、apply、rewrite、revert、destructおよびinduction. inversionすぐに役立つかもしれません。