「はじめてのCoq」

Github 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 )

Appendix 11/28マルレク紹介

  1. なぜ、開発は人間によって担われているのか? ( ムービー pdf )

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

論理式の証明 (6) — Coqの返す「証明の状態」と演繹ルール

論理式の証明 (5) — 命題論理の演繹ルール

論理式の証明 (4) — 「正しい」ことと「証明を持つ」こと

論理式の証明 (3) — 構成のルールと演繹のルール

論理式の証明 (2) — 論理式の部分式への分解とサブゴール

論理式の証明 (1) — 論理式はどのような形をしているか?

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

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

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