08 December, 2010

[Coq] Coq Advent Calender : intro (8 of 25)

 Coq でよく使われる tactic の8つ目は intro です。基本的には前に説明したintrosと同じで、introsと違って一度に1つしかintro出来ないのが違います。
 あと、introsと違ってintroの場合は、~Pの形のゴールを、Pという仮定と、Falseというゴールに変形出来ます。~PP->Falseなのですが、intros.では~P~Pのままです。

 intro.を使った例です。

Coq < Lemma Sample_of_intro : forall P, ~~~P -> ~P.
1 subgoal

============================
forall P : Prop, ~ ~ ~ P -> ~ P

Sample_of_intro < intro P.
1 subgoal

P : Prop
============================
~ ~ ~ P -> ~ P

Sample_of_intro < intro nnnp.
1 subgoal

P : Prop
nnnp : ~ ~ ~ P
============================
~ P

Sample_of_intro < intro p.
1 subgoal

P : Prop
nnnp : ~ ~ ~ P
p : P
============================
False

Sample_of_intro < elim nnnp.
1 subgoal

P : Prop
nnnp : ~ ~ ~ P
p : P
============================
~ ~ P

Sample_of_intro < intro np.
1 subgoal

P : Prop
nnnp : ~ ~ ~ P
p : P
np : ~ P
============================
False

Sample_of_intro < elim np.
1 subgoal

P : Prop
nnnp : ~ ~ ~ P
p : P
np : ~ P
============================
P

Sample_of_intro < exact p.
Proof completed.

Sample_of_intro < Qed.

No comments: