Coq Tutorial https://github.com/maruyama097/coq-tutorial

目次

I. Hello Coq!

1. Coqとのはじめての対話　( ムービー　pdf )
2. 人間はCoqに何を伝えたか？　( ムービー　pdf )
3. Coqは人間に何を伝えたか？　( ムービー　pdf )

II. 論理式の証明

1. 論理式はどのような形をしているか？( ムービー　pdf )
2. 論理式の部分式への分解とサブゴール( ムービー　pdf )
3. 構成のルールと演繹のルール　( ムービー　pdf )
4. 「正しい」ことと「証明を持つ」こと ( ムービー　pdf )
5. 命題論理の演繹ルール　( ムービー　pdf )
6. Coqの返す「証明の状態」と演繹ルール　( ムービー　pdf )
7. tactic (1) サブゴールの形と演繹ルールの選択   ( ムービー　pdf )
8. tactic (2) 仮説部の形と演繹ルールの選択  ( ムービー　pdf )
   
9. 「否定」について   ( ムービー　pdf )