私はCoqを学んでおり、学んでいる本（CPDT）は証明に多用autoされています。
私は学んでいるので、内部で何autoが行われているのかを正確に確認することが役立つかもしれないと思います（早い段階で魔法が少ないほど良い）。証明を計算するために使用している戦術やテクニックを正確に表示するように強制する方法はありますか？
そうでない場合、正確に何をするのかを詳しく説明する場所はありautoますか？
質問する
1988 次
1 に答える
18
ボンネットの下で何が起こっているかを一目で確認する方法は複数あります。
TLDR: 戦術の前に置くか、戦術を呼び出す前後にinfo使用して違いを見つけます。Show Proof.
特定の戦術の呼び出しが何を行っているかを確認するには、 is の前に を付けてinfo、実行した特定の証明手順を示すことができます。
(これは Coq 8.4 では壊れている可能性がありますinfo_。いくつかの戦術のバージョンが提供されているようです。必要に応じてエラー メッセージを読んでください。)
これはおそらく初心者レベルで必要なものであり、すでに非常に簡潔になっている可能性があります。
プルーフ内で現在何が起こっているかを確認する別の方法は、コマンドを使用することShow Proof.です。現在作成されている穴のある用語が表示され、現在の目標のそれぞれがどの穴を埋める必要があるかが示されます。
induction特にorなどのタクティックを使用する場合、これはおそらくより高度です。inversion構築される用語はかなり複雑になり、誘導スキームまたは依存パターン マッチングの基本的な性質を理解する必要があるためです (CPDT が教えてくれるはずです)。すぐに）。
Qed.(または) で証明を終えたら、where isDefined.を使用して構築された用語を調べるように依頼することもできます。定理/用語の名前です。Print term.term
多くの場合、これは大きくて醜い用語であり、関連する用語を読むにはある程度のトレーニングが必要です。特に、用語が強力な戦術 ( 、 など) を使用して作成された場合、omegaおそらくcrush読めなくなります。基本的には、興味のある用語の特定の場所をスキャンするためだけに使用します。10 行を超える長さの場合は、そのような粗雑な形式で読む必要さえありません。:)
Set Printing All.以前のすべてで、 Coqがすべての展開された明示的なバージョンを出力するように、事前に使用できます。さらに冗長ですが、暗黙的なパラメーターの値が何であるか疑問に思う場合に役立ちます。
頭の中で思いつくのはこれだけですが、他にもあるかもしれません。
戦術が何をするかについては、通常の最良の答えはドキュメントにあります:
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
于 2013-02-17T04:48:23.837 に答える