Certified Programming with Dependent Types関係

Certified Programming with Dependent Types (CPDT)を読む為の前提


この教科書は、オリジナルなtacticのcrushというのを導入して、色々自動証明をさせています。なので、crush出来る様にしておかないと、教科書の証明を写経できません。crushを使う方法ですが、

  • Coqをインストールしておくのは当然。
  • CPDTの付属ファイルを入手する。詳しくはCPDT 1.6章を読むべきだが
    • http://adam.chlipala.net/cpdt/cpdt.tgz をダウンロードする。
    • 適当なディレクトリ (~/cpdt/とか)で展開し、makeする。
    • Coq起動時に、coqtop -I ~/cpdt/src とオプションでソースディレクトリを指定。
    • Coq内で、Require Import Tactics. と Tactics.v を読み込んでおく。
    • こうすると、crushというtacticが使用出来る。

タグ:

+ タグ編集
  • タグ:

このサイトはreCAPTCHAによって保護されており、Googleの プライバシーポリシー利用規約 が適用されます。

最終更新:2010年05月18日 23:11
ツールボックス

下から選んでください:

新しいページを作成する
ヘルプ / FAQ もご覧ください。