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

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

• Anarchy Proof

という読者投稿型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に変える