forall と -> (1.2)

いくつか細かい捕捉。

intro

introsと同じひっぺがし作業を１回だけやる

単数形にすると「1回だけやる」意味になります。introsだとやれるまでやってしまうので、今回の例だと4個全部はがしちゃいますが

Theorem Modus_ponens:
 forall (P: Prop),
   forall (Q: Prop),
     (P -> Q) -> P -> Q.
Proof.
intro.
intro.
intro.

3回だけで止めると

P: Prop
Q: Prop
H: P -> Q
------------------------------------------------
P -> Q

こうなるので、ここで exact H. という証明もありです。apply とか要らない分簡単かも。

intro X

X という名前をつけつつintroでひっぺがす

intros X1 X2 ... Xn

X1 X2 ... という名前をつけつつn個introsでひっぺがす

単にintroとかintrosとか打つと、Coqが適当に"H"やら"H0"と名前をつけてくれますが、自分で命名もできます。たぶん可読性のためにはこっちの方が良いです。

Theorem Modus_ponens:
 forall (P: Prop), forall (Q: Prop), (P -> Q) -> P -> Q.
Proof.
intros P Q P_naraba_Q.
exact P_naraba_Q.
Qed.

他にも、intro/intros にはいくつか賢いオプション指定ができるので、詳しくはマニュアル参照のこと。

assumption

仮定にあるどれかがゴールそのまんまだからそれでお願い！という証明

Theorem Modus_ponens:
 forall (P: Prop), forall (Q: Prop), (P -> Q) -> P -> Q.
Proof.
 intros.
 apply H.
 assumption.  (* exact H0. の代わり *)
Qed.

実は、"exact H" や "exact H0" のように名前を指定しなくても、そのくらい自動で探してこいよ！というとCoqさんちゃんと見つけてくれます。賢いですね。

賢いと言えば

auto

Coqさんならできる！頑張れよ！もっと熱くなれよ！！

Theorem Modus_ponens:
 forall (P: Prop), forall (Q: Prop), (P -> Q) -> P -> Q.
Proof.
 auto.
Qed.

実はCoqさん十分賢いのでこの程度の証明は、auto. って書くと勝手に全部やってくれるんですが、それだとあんまりCoq入門にならないので、この記事ではできるだけautoを使わないようにします。