[Coq] Coq Advent Calender : apply (1 of 25)

　技術的 Advent Calender という概念を知らなかったのですが、面白そうなので遅ればせながら始めてみました。という訳で12/1から開始出来なかったのはご容赦下さい。
　先日のCoq Party絡みで集計されたCoqでよく使われるtacticのリストの順に、そのtacticが使われている証明例を書いてみます。

　最初は apply です。
　「この仮定（下記の例では pq）を使うとゴール（下記の例では Q）が出て来る」という時に、apply pq とすると、ゴール Q が変化します。学校で習う普通の証明の順序と違って、Coqの証明はゴールを一歩一歩、仮定に戻して行きます。その時使うのが apply です。

Coq < Lemma Sample_of_apply : forall P Q:Prop, P -> (P->Q) -> Q.
1 subgoal
  
  ============================
   forall P Q : Prop, P -> (P -> Q) -> Q

Sample_of_apply < intros P Q p pq.
1 subgoal
  
  P : Prop
  Q : Prop
  p : P
  pq : P -> Q
  ============================
   Q

Sample_of_apply < apply pq.
1 subgoal
  
  P : Prop
  Q : Prop
  p : P
  pq : P -> Q
  ============================
   P

Sample_of_apply < exact p.  
Proof completed.

Sample_of_apply < Qed.
intros P Q p pq.
apply pq.
exact p.

Sample_of_apply is defined

Coq <