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が使用出来る。
最終更新:2010年05月18日 23:11