■

assumption

この tactic は忘れてもよい。仮定の中に結論と一致しているものがある場合に使うと一発で証明が終わる。でも、auto を使えば同じことができる。

intro

この tactic はチュートリアルで普通に理解できる以上の機能はない。
結論が「forall x:T, U」の場合と「T->U」の場合にしか使わない。「U」が新しい結論になって、「x:T」が新たに仮定に追加される。それ以外の場合は「red」を勝手に実行してくれる。なので

Goal ~A.
intro.

とすれば、「not」を勝手に展開してくれて

H: A
======
False

となる。

intro ident

「intro」に引数を与えると、追加される仮定の名前を設定できる。チュートリアルに載ってるからみんな知ってるよね。

apply term

「apply」はゴールに辿り着くために最後に適用する仮定または定理を教えてあげる tactic。
適用できる定理は「forall」と「->」でゴールまでつながっている形で無ければならない。
例えばゴールが「A /\ B」のときは

th1: forall A B: Prop, A -> B -> A/\ B.

は適用できる定理であり、

apply th1.

とすれば、残った証明すべきことは「A」と「B」なので、ゴールはこの二つとなる。
ゴールに「forall」とか「->」含まれていてもよくて、「~A->~B」がゴールだとすると

th2: forall X Y: Prop, (X->Y)->~Y->~X

もうまくパターンマッチしてくれる。

パターンマッチングで決定できなかった変数は指定しなければならない。次の定理を適用することを考えよう

th3: forall (X: Set) (x y z: X), x = y -> y = z -> x = z.

証明したいのは

Goal 1+3 = 2+2.

だとする。どちらも「4」に等しいことを使って証明しよう

apply th3.

こうすると「1+3 = 2+2」が「x = z」とパターンマッチされて、「x = 1+3」と「z = 2+2」となる。
ついで、「X = nat」であることがわかる。しかし、「y」が何になるか分からないので、この apply はエラーになる。
「y」には「4」を指定したかったので、

apply th3 with 4.

とするか

apply th3 with (y := 4).

とすればよい。ここで上の形式は使いにくくて、この例で「X = nat」が決まることに気づかずに

apply th3 with nat 4.

なんて書いてしまうと、とんでもなく不親切なエラーメッセージが表示される。
下の形式だと、余分に指定した

apply th3 with (X := nat) (y := 4).

も通るので、初心者向きである。

もちろん

apply (th3 nat (1+3) 4 (2+2)).

のように全部自分で指定してもよい。