DProof: Procedual Proof to Declarative Proof

タクティック列からC-zarの証明を生成します。

インストール

Coq8.6にのみ対応しています。

1. coq_makefile -f _CoqProject -o Makefile

2. make

3. make install

使い方

原則coqtop以外では機能しません。

1. 任意の位置で Require Import dp.DProof.

2. 変換したいタクティック列の直前で DProof.

   • 例えば定理全体の場合 Goal コマンドの直後

   • メッセージなどはなし

3. 変換したいタクティック列の直後で DEnd.

   • 定理全体の場合 Qed コマンドの直後

   • C-zarの証明が表示される

その他

• ファイルに出力したい場合には DEnd の前に Set DProof File filename.

• DProof から DEnd までの間でエラーを起こした場合、変換時にもエラーが発生するため注意

論文

『定理証明支援系Coqにおける手続き的証明から可読性の高い宣言的証明への変換』 http://id.nii.ac.jp/1438/00008687