ひとり勉強会

ひとり楽しく勉強会

[Coq] forall と -> : まとめ (1.6)

というわけで、Coq入門編その一、forall と -> だけ使った定理の証明、をお届けしました。気が向いたら「and, or, not を使った定理の証明」「exists を使った定理の証明」「帰納法」「forallと->と依存型について本気出して考えてみた」… の順番で続きます。入門記事を書くのはいいけれど、面白い練習問題が提供できないとつまらないよなーむずかしいなー、と思って長年躊躇していたのですが、最近

という読者投稿型Coqの問題集サイトができて、面白い練習問題はここを見ろ!と言えるようになったので、まあいいかなという気分になりました。

今日のまとめ。少なくとも最初のうちは、ゴールにforallや->がいたら何も考えずintros。

intro
「"A -> B" を証明しろ」という状態を、「"A" が成り立つものと仮定して "B" を証明しろ」に変える。forallも同様に仮定に移す
intros
introをできるかぎり繰り返す
"->"な仮定を使ったゴール変形。
apply H
H:A->B で、ゴールがB なら、ゴールをAに変える
手書き証明。
exact t
現在のゴールの型をもつ値/証明 t を直書きする
自動証明。
assumption
exactな仮定があるとき自動で探してそれを使う
auto
Coqさんは賢い
仮定変形系。
assert (X := t).
証明tで証明できた事実を新しい仮定Xとして増やす
specialize (A B).
仮定AをA Bに変える
apply A in B.
仮定BをA Bに変える