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

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