概要 https://coq-handson.peatix.com/
目次
I. Hello Coq!
-
Coqとのはじめての対話 ( ムービー pdf )
- 人間はCoqに何を伝えたか? ( ムービー pdf )
- Coqは人間に何を伝えたか? ( ムービー pdf )
II. 論理式の証明
-
論理式はどのような形をしているか?( ムービー pdf )
- 論理式の部分式への分解とサブゴール( ムービー pdf )
- 構成のルールと演繹のルール ( ムービー pdf )
- 「正しい」ことと「証明を持つ」こと ( ムービー pdf )
- 命題論理の演繹ルール ( ムービー pdf )
- Coqの返す「証明の状態」と演繹ルール ( ムービー pdf )
- tactic (1) サブゴールの形と演繹ルールの選択 ( ムービー pdf )
- tactic (2) 仮説部の形と演繹ルールの選択 ( ムービー pdf )
- 「否定」について ( ムービー pdf )