概要 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 )
