■

Coqでの証明はtacticと呼ばれるコマンドを並べて次々に実行ことによって行われる。
このtacticの語彙が多いほど証明の記述は楽になる。
しかし、語彙を増やすようなドキュメントはオンラインに見つからないので、書きやすいところから書いてみる。

exact term

「exact」は最もプリミティブなtacticで、現在のゴールの証明を直接記述する。
直接記述する形式は Print コマンドを使えば知ることができる。

Variables A B C:Prop.
Lemma ex1: (A->B->C)->(A->B)->A->C.
auto.
Qed.

このように簡単な定理を証明したとして、証明の内容を Print コマンドを使って表示すると

Print ex1.
ex1 = 
fun (H : A -> B -> C) (H0 : A -> B) (H1 : A) => H H1 (H0 H1)
     : (A -> B -> C) -> (A -> B) -> A -> C

となり、この中で証明にあたる部分は

fun (H : A -> B -> C) (H0 : A -> B) (H1 : A) => H H1 (H0 H1)

である。まったく同じ定理を証明しようと思ったら、

Lemma ex2: (A->B->C)->(A->B)->A->C.
exact (fun X Y Z => X Z (Y Z)).
Qed.

のように同じ関数を記述すればよい。型は指定しなくても勝手に推論してくれる。

定理の証明を行ったら毎回 Print を実行して、どのような証明が行われたかを確認するとよい。
初めて見る関数に出会えたり、より簡単な証明を思いついたりできる。
慣れてくれば「->」しかでてこない定理は exact でも簡単に証明できる。

否定がまじってる場合も同様である。否定の定義は

not A := A -> False.

であるから、これを展開すれば同様にできる。結論に False が現れる場合は仮定のどこかに False が入っていなければ証明できない。最も単純な場合は

Lemma ex3: A -> ~A -> False.

は「A である」と「A ではない」を仮定して結論「False」を導きたいので、仮定に入っている「False」を探すことになる。
否定の定義を思い出すと証明したいことは

A -> (A -> False) -> False.

なので、一発で証明できて

exact (fun isA notA => notA isA).

となる。
「notA isA」が False になるのは覚えておくべき基本事項。

もっと複雑な例

Lemma ex4: (A -> B) -> (~B -> ~A).

こういう場合は、括弧と優先順位からintros したときにどこまでが仮定になるのかを考えて、「A->B」と「~B」と「A」が仮定で「False」が結論であることに気づけば、「A->B」と「A」から「B」を導いて、「~B」とぶつけてやれば「False」が得られることが分かるので、

exact (fun AimplB notB isA => notB (AimplB isA)).

で証明できる。