はじめてのCoq

なぜ、開発は人間によって担われているのか? (pdf

参考資料

MaruLabo Hands on はじめてのCoq

Coqのインストール 

平原ゼミ Coq スタートアップセミナー を利用ください

Hands on のソース

Github https://github.com/maruyama097/coq-tutorial

Hello Coq!

Hello Coq! (1) — Coqとのはじめての対話 (pdf)

Hello Coq! (2) — 人間はCoqに何を伝えたか? (pdf)

Hello Coq! (3) — Coqは人間に何を伝えたか? (pdf)

論理式の証明

論理式はどのような形をしているか?( pdf )

論理式の部分式への分解とサブゴール ( pdf )

構成のルールと演繹のルール ( ムービー pdf )

「正しい」ことと「証明を持つ」こと (  pdf )

命題論理の演繹ルール ( pdf )

Coqの返す「証明の状態」と演繹ルール ( pdf )

tactic (1) サブゴールの形と演繹ルールの選択   ( pdf )

tactic (2) 仮説部の形と演繹ルールの選択  ( pdf )

「否定」について   ( pdf )