いくつかのtacticについて

ではいくつかのtacticについて、その簡単な使い方を説明しようと思います。 また、当然Coq上で実際に使うわけですから、λ式や型の表記はCoqの表記で 書こうと思います。

applyについて

head typeとfinal type

まず次のような型を考えます。

1. 　　　　ｆｏｒａｌｌ　（ｖ_１：Ａ_１） 　．．．　（ｖ_ｎ：Ａ_ｎ），　Ｂ

ただし、Ｂはｆｏｒａｌｌでは始まらない型とします。このとき、

2. 　　　　ｆｏｒａｌｌ　（ｖ_ｋ：Ａ_ｋ） 　．．．　（ｖ_ｎ：Ａ_ｎ），　Ｂ　　　 （ｋ＝１，．．．，ｎ）

をｒａｎｋ　ｋのhead typeと言います。そして、Ｂをfinal typeと言うのです。 Ｂはｒａｎｋ　ｎ＋１のhead typeと言うこともあります。

自由変数に、同じ型の式を代入したものをinstanceと言いますが、 subgoalが、仮定Ｈのhead typeのinstanceのとき、apply H.で証明をさかのぼる ことができます。

apply命令で証明をさかのぼる様子を具体例で見てみましょう。まずはすでに 見たOrtoAndでの例です。それは、

でした。 仮定のH : A \/ B -> C （画面上のH : A \/ B -> C） ですが、これは略記せずに 書けば、
H : (forall x:A \/ B, C) です。 よって、C はH のｒａｎｋ　２のhead typeのinstance （C の中に変数x はないので、変数x に何かを代入してもしなくても同じ）なので、apply H.を適用できるわけ です。証明をさかのぼる様子は既に説明した通りです。

次の例です。とても単純な例も見ておきましょう。次の定理をCoqで実行して 証明してみてください。

Section ML.
Variable D : Set.
Variable P : D -> Prop.
Variable a : D.
Theorem exam1 : (forall x:D, P x) -> P a.
Proof.
 intro H.
 apply H.
Qed.
End ML.

apply H.の実行部分だけ以下に表示します。

P a は、 H : (forall x : D, P x) のｒａｎｋ　２のhead typeのinstanceです。この場合は、 apply H.を適用するだけで証明は終了しました。

少し複雑（そう）な例も見ましょう。次の定理をCoqで実行して 証明してみてください。

Section ML.
Variable D : Set.
Variable A : Prop.
Variable B C : D -> D -> Prop.
Theorem exam2 : forall a b:D, A -> B a b -> 
(A -> forall x y:D, B x y -> C x y) -> C a b.
Proof.
 intros a b.
 intros Ha Hb H.
 apply H.
 assumption.
 assumption.
Qed.
End ML.

applyの実行部分だけ以下に表示します。

ここでapplyを適用している仮定 H は

3. 　　　　 H : A -> forall x y : D, B x y -> C x y

ですが、これを略記せずに書くと

4. 　　　　 H : forall p : A, forall x y : D, forall q : B x y, C x y

となります。よって、 C a b は H のfinal typeのinstanceになります。この C a b にapply H.が適用される様子を考えて見ましょう。おそらく、 H のfinal typeの C x y とsubgoalの C a b をくらべて、 x が a 、 y が b になればよいと判断し、その上で残った型 A 、 D 、 B a b のうち、 A と B a b が新しいsubgoalになっています。apply H.適用前のsubgoalが C a b でしたから、 a : D および b : D は、型とその型を取る式が完全に定まるので、 D は新しいsubgoalにしなくて良かったのだと思います。

論理式の形から

今度は視点を変えて説明しましょう。実際の証明の場面では、仮定やsubgoalにある （型である）論理式をみて適用するtacticを決めるわけなので、その論理式の 形で分けて説明することにします。

論理式が P -> Q の形のとき

• P -> Q が仮定にあるとき。
  仮定は H : P -> Q であるとする。このときsubgoalが Q であれば、apply H.が適用できる。適用後はsubgoalが P になる。
• P -> Q がsubgoalのとき。
  H をそれまで使用されていない変数とする。このときintro H.が適用できる。 適用後は仮定に H : P が増え、subgoalは Q となる。

論理式が forall x : P, Q(x) の形のとき
ここで Q(x) というのは、自由変数として文字 x を含んだ型のことを表している。

• forall x : P, Q(x) が仮定にあるとき。
  仮定は H : forall x : P, Q(x) であるとする。このとき a : P なる式 a があって、subgoalが Q(a) （ Q(x) におけるすべての自由な x に a を代入したもの）であれば、apply H.が適用できる。この場合はこれで 証明が完了する。
• forall x : P, Q(x) がsubgoalのとき。
  y をそれまで自由には使用されていない変数とする。このときintro y.が 適用できる。適用後は仮定に y : P が増え、subgoalは Q(y) となる。

論理式が P /\ Q の形のとき

• P /\ Q が仮定にあるとき。
  仮定は H : P /\ Q であるとする。このときelim H.が適用できる。elim H.適用前の subgoalが R であれば、適用後はsubgoalが P -> Q -> R になる。この後は例えばintro H0.そしてintro H1.と続ければ、仮定に H0 : P と H1 : Q が増え、subgoalは R となる。これで、最初の仮定 H : P /\ Q を、 H0 : P と H1 : Q に分離できることになる。
• P /\ Q がsubgoalのとき。
  split.が適用できる。 適用後はsubgoalが P と Q の2つになる。 subgoalが複数に分かれた場合、画面に表示されたsubgoalのうち、 一番上のsubgoalが以降の操作対象となる。また、操作対象でないsubgoal の方の仮定は表示されない。

論理式が P \/ Q の形のとき

• P \/ Q が仮定にあるとき。
  仮定は H : P \/ Q であるとする。このときelim H.が適用できる。elim H.適用前の subgoalが R であれば、適用後はsubgoalが P -> R と Q -> R の2つになる。これは、仮定の H : P \/ Q を、 P と Q で場合わけしていることになる。この後、最初のsubgoalが P -> R だとすると、新しい変数H0を用いてintro H0.とすれば、仮定に H0 : P が増え、subgoalは R となる。これで、場合わけにおける P の場合の証明をさかのぼることとなる。
• P \/ Q がsubgoalのとき。
  left.およびright.が適用できる。left.適用後はsubgoalが P になる。right.適用後はsubgoalが Q になる。Coqは証明をさかのぼっているということを忘れないこと。 この命令は、 P 、 Q のいずれかを捨てる命令である。

論理式が exists x : P, Q の形のとき

• exists x : P, Q が仮定にあるとき。
  仮定は H : exists x : P, Q であるとする。 このときelim H.が適用できる。elim H.適用前の subgoalが R であれば、適用後はsubgoalが forall x : P, Q -> R になる。これは、 forall x : P, (Q -> R) の略記であることに注意。この後、y,H0をどちらも新しい変数として intros y H0.を適用すれば、仮定に y : P 及び H0 : Q が増え、subgoalは R となる。これは、「 H : exists x : P, Q で存在が仮定されている x を y とおいて、仮定 Q[x:=y] （ Q におけるすべての自由な x に y を代入したもの）のもとで R を証明する」ということである。
• exists x : P, Q がsubgoalのとき。
  a : P なる式 a があれば、exists a.を適用することができる。このときsubgoalは Q[x:=a] になる。

論理式が ~ P の形のとき
「 ~ P 」は 「 P の否定」のことですが、Coqでは「 P -> False 」の略記です。 False は定項です。意味は「成立しない命題」と思っておけば大丈夫です。 とりあえずは False の定義は気にしなくてもいいと思います。

• ~ P が仮定にあるとき。
  仮定は H : ~ P であるとする。このときelim H.が適用できる。elim H.適用前のsubgoalは 消去され、subgoalは P になる。 P -> ~ P -> Q なる恒真式を知っていれば、この推論が妥当であることはわかると思う。
• ~ P がsubgoalのとき。
  上記にも書いたように、 ~ P は P -> False の略記なので、上記の「 P -> Q がsubgoalのとき。」に準じた処理ができる。つまり、 H をそれまで使用されていない変数とする。このときintro H.が適用できる。 適用後は仮定に H : P が増え、subgoalは False となる。

論理式が a = b の形のとき

• a = b が仮定にあるとき。
  仮定は H : a = b であるとする。このときrewrite H.が適用できる。 rewrite H.は、subgoalの形が P a ならば、新しいsubgoalを P b にする。 subgoalの形が P a でないならば、subgoalの中にある自由な a をすべて b に置き換える。 subgoalの中に a がないときはエラーになる。 型があうなら、仮定は H : forall x y : A, a = b のような 形でもよい。同じ例で、rewrite <- H.とすると、 a, b が逆転して subgoalの中にある b をすべて a に置き換える。 H : a = b をつかって、他の仮定である H0 の中の a をすべて b に置き換え たいなら、rewrite H in H0.とすればよい。 a, b の逆転も同様。 さらに、subgoalにおける自由な a のうち、左から2番目の a のみ b に置き換えたい なら、rewrite H.を適用する直前にpattern a at 2.を実行しておけばよい。
• a = b がsubgoalのとき。
  a と b が同じ文字列であり、つまりsubgoalが a = a となっているのであれば、reflexivity.で証明を終わらせることができる。 そうでない場合は、symmetry.とすると、新しいsubgoalが b = a となる。transitivity c.を実行すると、subgoalは a = c と c = b の2つになる。

以上簡潔に表にすると

その他

tacticの区切り記号「；」について

複数のtacticを記号「；」で区切って並べることができるのですが、 ただ並べるのとはちょっと違います。具体的には ここの定理Syllogeqの証明の解説を読んで ください。（定理Syllogeqの証明の中に出てくるSyllogは、定理Syllogeqのすぐ 上で証明されている定理です。）

applyにつけるwithについて

apply命令は、subgoalをhead typeとするような仮定を適用するわけですが、 そのとき、仮定の中の束縛変数を何にするかCoqが判断できないときがあります。 これも、具体的には ここの定理Syllogeqの証明の解説を読んで ください。（定理Syllogeqの証明の中に出てくるSyllogは、定理Syllogeqのすぐ 上で証明されている定理です。）

withを使わずに束縛変数を指定する方法について

withをつかってもapply命令がうまくいかないこともありました。そこで、withを 使わない方法も紹介しておこうと思います。上記のwithの解説に続けて、 ここで具体的に説明してあります。

unfoldについて

いわゆる「定義に戻れ」をしなくてはならないときもあります。その命令 がunfoldです。具体的な説明はAndABABの証明 にあります。

exists vへの注意

証明中にexists v.命令を実行するときは、仮定の中にvなるλ式がなくては なりません。あるいは、仮定の中にある式からvを作ることができてもいいようです。 具体例はDm_nexの証明 を見てください。

cut命令

「->」（ならば）に関する証明のさかのぼり方の一種です。これは、subgoalが Bのとき、cut A.命令を実行すると、subgoalがAとA -> Bの2つになります。つまり、 「Bを証明するには、AとA -> Bの2つを証明すればよい」という考えに基づく さかのぼり方です。証明の具体例はAllandの証明 を見てください。

もどる