はじめてのCoq

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

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

Hello Coq!

Coqとのはじめての対話 

ムービー pdf )

人間はCoqに何を伝えたか?

( ムービー pdf )

Coqは人間に何を伝えたか? 

( ムービー pdf )

論理式の証明

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

( ムービー pdf )

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

( ムービー pdf )

構成のルールと演繹のルール 

ムービー pdf )

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

ムービー pdf )

命題論理の演繹ルール 

ムービー pdf )

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

ムービー pdf )

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

 ( ムービー pdf )

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

ムービー pdf )

「否定」について 

 ( ムービー pdf )