[Coq] Coq Advent Calender : assert (7 of 25)

　Coq でよく使われる tactic の７つ目は assert です。

　１つ目のapplyのところで書いた様に、Coqの証明は最初にゴールがあって、それを仮定と逆に戻して行く格好になっています。しかし証明する人間は仮定からゴールを考える方が楽な場合、つまり証明途中で適当な補題を作りたくなる場合があります。
　補題はある程度汎用性があるならば、予め切り出して証明しておいた方が良いと思いますが、使い捨て的な補題は assert を使うと、証明内証明みたいに作る事ができます。例えば下記の例で、

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

Sample_of_assert < intros P Q pp qq.
1 subgoal
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  ============================
   P /\ Q

　ここまで証明した段階で、forall X, X /\ X -> Xという補題があれば、ppからPを、qqからQを取り出せて便利そうだと考えました。そこでassertを使います。すると現在の証明課題より先に、まずこの補題が証明課題になります。

Sample_of_assert < assert(H: forall X, X /\ X -> X).
2 subgoals
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  ============================
   forall X : Prop, X /\ X -> X

subgoal 2 is:
 P /\ Q

Sample_of_assert < intros X xx.
2 subgoals
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  X : Prop
  xx : X /\ X
  ============================
   X

subgoal 2 is:
 P /\ Q

Sample_of_assert < destruct xx as [x _].
2 subgoals
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  X : Prop
  x : X
  ============================
   X

subgoal 2 is:
 P /\ Q

Sample_of_assert < exact x.
1 subgoal
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  H : forall X : Prop, X /\ X -> X
  ============================
   P /\ Q

　assertで設定した補題 H の証明が終わると、以後は仮定 H としてそれを使う事が出来ます。

Sample_of_assert < split.
2 subgoals
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  H : forall X : Prop, X /\ X -> X
  ============================
   P

subgoal 2 is:
 Q

Sample_of_assert < apply (H P).
2 subgoals
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  H : forall X : Prop, X /\ X -> X
  ============================
   P /\ P

subgoal 2 is:
 Q

Sample_of_assert < exact pp. 
1 subgoal
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  H : forall X : Prop, X /\ X -> X
  ============================
   Q

Sample_of_assert < apply (H Q).
1 subgoal
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  H : forall X : Prop, X /\ X -> X
  ============================
   Q /\ Q

Sample_of_assert < exact qq.
Proof completed.

Sample_of_assert < Qed.