下準備
- Coq IDEをインストールする。
- 英語版のサイトから[sf.tar.gz」をダウンロードし解凍する。
- 英語版サイトのトップページにDownloadボタンがあります。
- 解凍先のディレクトリパスが全角文字を含んでいると、Coqはファイルの読み込みに失敗します。半角文字だけのディレクトリに解凍するようにしてください。
学習
- まずCoq IDEにBasics.vを読み込む。
- 日本語の解説を読みながら、Coq IDEでCtrl+Alt+↓を押し、1行1行実行してコンテキストの動きを観察する。
Pierce先生も文中で何度も書いていますが、大切なことほど、文を読んだだけでは理解できません。必ずCoq IDEで例題を実際に実行し、コンテキストの変化を観察してください。Coq IDEではCtrl+Alt+↑とすることで、実行済みの行を1行戻すことができます。Ctrl+Alt+カーソル上下を何度も繰り返して、ある行を実行することでコンテキストのどこがどう変わったかを確認しながら実行することがとても大切です。
練習問題
- 練習問題では、(* FILL IN HERE *) となっているところに解答を書き実行する。
- 証明できたらAdmitted.をQed.に書き換えて次の問題に取り組む。
