[Coq] Coq Advent Calender : intros (5 of 25)

　Coq でよく使われる tactic の５つ目は intros です。

　実は過去４回の記事でも毎回 intros を使用していました。forall とかで定義された変数や -> の左の式とかを仮定に持って行く為に使います。introの複数形なので、introを必要な回数繰り返してもOKです。
　intros. だけでも勝手に適当に名前（仮定は通常 H? みたいな名前）を付けてくれますが、判りやすさを考えると自分で適切な名前を付けた方が良いと思います。

Coq < Lemma Sample_of_intros : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C.
1 subgoal
  
  ============================
   forall A B C : Prop, (A -> B -> C) -> (A -> B) -> A -> C

Sample_of_intros < intros A B C abc ab a.
1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  abc : A -> B -> C
  ab : A -> B
  a : A
  ============================
   C

Sample_of_intros < apply abc.
2 subgoals
  
  A : Prop
  B : Prop
  C : Prop
  abc : A -> B -> C
  ab : A -> B
  a : A
  ============================
   A

subgoal 2 is:
 B

Sample_of_intros < exact a.   
1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  abc : A -> B -> C
  ab : A -> B
  a : A
  ============================
   B

Sample_of_intros < apply ab; exact a.
Proof completed.

Sample_of_intros < Qed.
intros A B C abc ab a.
apply abc.
 exact a.
 
 apply ab; exact a.
 
Sample_of_intros is defined

Coq <