はじめてのCoq

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

概要 https://coq-handson.peatix.com/

目次

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 )