Certified Programming with Dependent Types関係


※上記の広告は60日以上更新のないWIKIに表示されています。更新することで広告が下部へ移動します。

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が使用出来る。
ツールボックス

下から選んでください:

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