Coqの "Verbose" auto

Question

私はCoqと私が学んでいる本を学んでいます。（CPDT）はautoを証明に使っています。

私は学んでいるから、autoがフードの下で何をしているのかを正確に見ることが役立つかもしれないと思います。プルーフを計算するためにどのような戦術や技法を使用するかを正確に表示する方法はありますか？

もしそうでない場合は、正確にautoの詳細が記載されていますか？

Answer 1

フードの中で起こっていることを一目で分かる方法はいくつかあります。

TLDR：戦術の前にinfoを置くか、または戦術を呼び出す前後にShow Proof.を使用してください。

---

特定の戦術呼び出しが行ってきたかを見るために、あなたは前に付けることができ、特定の証明はそれが取った手順を示すためになるように、infoです。

（これは、Coqの8.4で壊れている可能性があります、私はあなたがする必要がある場合、エラーメッセージを読んで、彼らはいくつかの戦術のinfo_のバージョンを提供していることがわかります。）

これは、あなたが初心者レベルで何をしたい、おそらく、それはすでにかなり簡潔にすることができます。

---

現在、証明内で行われていることを確認する別の方法は、コマンドShow Proof.を使用することです。それはあなたが穴を持つ現在構築された用語を表示し、あなたの現在のゴールのどれが満たされるべき穴を表示します。

inductionやのような戦術を使用する場合、これはもっと進んでいる可能性があります。構築する用語がかなり複雑になり、誘導方式や依存パターンマッチングの基本的な性質を理解する必要があります（CPDTはすぐにあなたに教えるべきです）。

---

あなたがQed.（またはDefined.）との証明を完了したら、あなたはまた、termが定理/用語の名前ですPrint term.を使用してビルドされた用語を見て頼むことができます。

これはしばしば大きくて醜い用語であり、関連する用語についてこれを読むことができるようにするには、いくつかの訓練が必要です。特に、強力な戦術（例えばomega,crushなど）を使用してこの用語が構築されていると、おそらく判読できなくなる可能性があります。あなたは基本的にそれを使用して興味のある用語の特定の場所をスキャンするだけです。もしそれが10行以上であれば、そのような粗い形式でそれを読んでも気にしないでください！以前のすべてで:)

---

コックはすべての展開、明示的なバージョンを出力するように、あなたは、事前にSet Printing All.使用することができます。さらに冗長ですが、暗黙的なパラメータの値が何であるか不思議に思うときに役立ちます。

これは私が頭の上で考えることができるすべてですが、もっとあるかもしれません。

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic155

基本的には、autoは、使用するデータベースに応じて、（提供されたすべてのヒントを使用しようとします：戦術は、いつもの最良の答えがマニュアルに記載されていているん何のためとして

---

）、あなたの目標を解決するために、それらを（あなたが指定できる）深さまで組み合わせることができます。既定では、データベースはcoreで、深さは5です。その上

詳細情報はここで見つけることができます：

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#Hints-databases