Isabelle Tutorial その10

5. The Rules of the Game

この章ではIsabelleを使った証明のコンセプトとテクニックを紹介します。

5.1 Natural Deducation

Isabelleでは、証明は推論規則によって構成されます。もっとも有名な推論規則の一つがmodus ponensです。

$\frac{P \rightarrow Q \,\, P}{Q}$

Isabelleでは自然演繹を使用します。Isabelleは適用可能な規則を探索することで、自動的に証明しようとします。自動証明がうまくいかない場合は、後述する方法で推論規則を適用し証明を手動で進めます。

5.2 Introduction Rules

ある論理記号について、導入規則はその記号が含まれた式を推論するのに使用します。例えば論理積の導入規則は、もしPとQが言えるならば、P ∧ Qが言えることを示しています。

$\frac{P \,\, Q}{P \wedge Q}$

結論に論理積が導入されているのがわかります。多くの場合、Isabelleの証明は後ろ向きに行います。よってこの規則を使うのは、サブゴールに含まれている論理積を削除したいときです。

Isabelleの記法では、論理積の導入規則は次のように書きます。

[|?P; ?Q|] ==> ?P & ?Q　　　　(conjI)

conjIはこの規則の名前です。規則の前提は矢印の左に、結論は右に書きます。また、全体が複数ある場合は[| |]で囲みます。?はスキーマ変数であることを示しており、規則を使用するときに任意の式と置き換えられます。この規則を適用しようとすると、Isabelleは?P & ?Qとゴールを単一化しようとし、成功すると?Pと?Qそれぞれに束縛された式が新たな二つのサブゴールとなります。例で見ていきます。

lemma conj_rule: "[|P; Q|] ==> P & (Q & P)"
apply(rule conjI)
apply assumption
apply(rule conjI)
apply assumption
apply assumption

まず、最も外側にある論理積を取り除くため、論理積の導入規則をメソッドruleを使用して適用します。すると、次のサブゴールが得られます。

 1. [| P; Q |] ==> P
 2. [| P; Q |] ==> Q & P

論理積の左側と右側がそれぞれサブゴールとして残ります。サブゴール1は前提から直ちに導けます。このような場合、メソッドassumptionを使用します。サブゴール2には再び論理積の導入規則を適用します。

 1. [| P; Q |] ==> Q
 2. [| P; Q |] ==> P

残った二つのサブゴールもassumptionで証明できます。

5.3 Elimination Rules

除去規則は導入規則とは逆に働きます。論理積の場合、除去規則は二つあります。

$\frac{P \wedge Q}{P} \,\,\, \frac{P \wedge Q}{Q}$

次は論理和を考えます。論理和の導入規則は二つあります。

$\frac{P}{P \vee Q} \,\,\, \frac{Q}{P \vee Q}$

論理和の除去規則は少し複雑です。P ∨ QからRを証明したいとします。もし、Pを真と仮定してRを証明でき、さらにQを真と仮定した場合もRを証明可能ならば、P ∨ QからRを推論できます。論理和の除去規則は次の形をしています。

$\frac { \begin{array}&[P]&[Q]\\&\vdots&\vdots\\P \vee Q&R&R\end{array} }{ R }$

仮定の[P]と[Q]の括弧は、それぞれの副証明のローカルな前提であることを示しています。Isabelleの記法では次のように書きます。

[|?P | ?Q; ?P ==> ?R; ?Q ==> ?R|] ==> ?R　　　　(disjE)

論理和の除去規則の適用は、場合分けのように働きます。例で見ていきます。

lemma disj_swap: "P | Q ==> Q | P"
apply(erule disjE)
apply(rule disjI2)
apply assumption
apply(rule disjI1)
apply assumption

まず、論理和の除去規則をメソッドeruleを使用して適用します。eruleはruleと同じようにゴールと規則それぞれの結論を単一化します。さらに規則の前提の最初の項を、ゴールの前提の何れかと単一化します。単一化に成功すると、規則の残りの前提が、サブゴールとして残ります。単一化しなかったゴールの前提も、それぞれのサブゴールの前提に加えられます。例の場合、次のサブゴールが残ります。

 1. P ==> Q | P
 2. Q ==> Q | P

サブゴール1にはdisjI2を使用することで、結論をPにすることができ、assumptionで証明が完了します。サブゴール2もdisjI1を使用して同様に証明します。

5.4 Destruction Rules: Some Examples

論理積に関する次の証明を見ていきます。

lemma conj_swap: "P & Q ==> Q & P"
apply(rule conjI)
apply(drule conjunct2)
apply assumption
apply(drule conjunct1)
apply assumption

conjunct1とconjunct2は論理積の除去規則であり、それぞれ論理積の左側及び右側を残します。このような規則は前提を破壊し一部分のみを残すため、破壊規則とも呼ばれます。

最初のステップは論理積の導入規則を適用しており、次の二つのサブゴールが残ります。

 1. P & Q ==> Q
 2. P & Q ==> P

メソッドdruleは規則の前提をゴールの前提と単一化し、規則の結論を新たな前提とします。よって今回の場合は、前提がP & QからQのみに置き換えられます。

 1. Q ==> Q
 2. P & Q ==> P

あとはassumptionで証明できます。サブゴール2も同様です。

rule、erule、druleのどれを使用するかは任意です。メソッドはルールをどのように使用するかを指定するだけであり、導入規則はruleを使わなければならないといった決まりはありません。

破壊規則はdisjEのような規則と比べると単純ですが、使いづらい面もあります。例えば論理積の破壊規則は式の半分を失ってしまうため、両方が必要な場合は使用できません。そのような場合には、他の除去規則を使用します。例えば論理積には次の除去規則もあります。

[|?P & ?Q; [|?P; ?Q|] ==> ?R|] ==> ?R　　　　(conjE)

Exercise 5.4.1

conjEを使用して先ほどの証明をより短くします。

lemma conj_swap: "P & Q ==> Q & P"
apply(erule conjE)
apply(erule conjI)
apply assumption

5.5 Implication

前述のmodus ponensは破壊規則です。

[|?P --> ?Q; ?P|] ==> ?Q　　　　(mp)

またこれに対する導入規則はimpIです。

(?P ==> ?Q) ==> ?P --> ?Q　　　　(impI)

含意に関する証明の例を見ていきます。

lemma imp_uncurry: "P --> (Q --> R) ==> P & Q --> R"
apply(rule impI)
apply(erule conjE)
apply(drule mp)
apply assumption
apply(drule mp)
apply assumption
apply assumption

まず含意の導入規則を使用し、次のサブゴールが残ります。

 1. [| P --> Q --> R; P & Q |] ==> R

次に論理積の除去規則を使用し、論理積の左右を分解します。

 1. [| P --> Q --> R; P; Q |] ==> R

次に前提のP --> (Q --> R)について考えます。これには、二回のmodus ponensの適用(drule mp)が必要です。残ったサブゴールはassumptionで終了できます。

記号==>と-->はどちらも含意を意味しますが、異なる点があります。==>は推論規則を表わし、Isabelleの推論機構はこれを特別に扱います。一方-->は高階論理に含まれる多くの論理結合子の中の一つとして扱われます。-->は高階論理の式の中で使用し、==>は定理の前提と結論を分けるのに使用しなければなりません。

コマンドbyは、applyと同じようにメソッドを適用し、残りのサブゴールを全てassumptionで証明しようとします。さらに、証明が終了するとdoneも自動的に行います。例えば先ほどの証明は次のように短くできます。

lemma imp_uncurry: "P --> (Q --> R) ==> P & Q --> R"
apply(rule impI)
apply(erule conjE)
apply(drule mp)
apply assumption
by(drule mp)

5.6 Negation

否定の導入規則は、もしPから矛盾が導かれるなら、¬Pを推論できることを示しています。また除去規則は、Pと¬Pからはどんな式も導けることを示しています。

(?P ==> False) ==> ~?P　　　　(notI)
[|~?P; ?P|] ==> ?R　　　　　　(notE)

古典論理はPを証明しようとする際に¬Pを前提とすることができます。

(~?P ==> ?P) ==> ?P　　　　(classical)

P --> Qと¬Q --> ¬Pは論理的に等しく、お互いを対偶といいます。対偶に関する次の四つの規則があり、それぞれ否定の位置が異なります。

[|?Q; ~?P ==> ~?Q|] ==> ?P　　　　(contrapos_pp)
[|?Q; ?P ==> ~?Q|] ==> ~?P　　　　(contrapos_pn)
[|~?Q; ~?P ==> ?Q|] ==> ?P　　　　(contrapos_np)
[|~?Q; ?P ==> ?Q|] ==> ~?P　　　　(contrapos_np)

これらの規則は主にeruleで使われ、仮定と結論を対偶で入れ替えます。特にcontrapos_npは仮定にある否定の項を結論に移動することができ便利です。例で見てみます。

lemma "[|~(P --> Q); ~(R --> Q)|] ==> R"
apply(erule_tac Q="R --> Q" in contrapos_np)
apply(intro impI)
by(erule notE)

二つの仮定がありますが、contrapos_npを適用したいのは二つ目です。メソッドerule_tacは単一化を制限し、マッチする項を決めることができます。この場合、contrapos_npの?QをR --> Qに指定することで、二つ目の項とマッチさせています。この結果、次のサブゴールが得られます。

 1. [| ~ (P --> Q); ~ R |] ==> R --> Q

元の結論Rが否定されて前提となり、前提の~(R --> Q)の否定が取れて結論になっています。次に含意の導入規則を適用します。メソッドintroは導入規則を繰り返し適用しようとします。

 1. [| ~ (P --> Q); ~ R; R |] ==> Q

前提に矛盾が含まれていることから、否定の除去ルールを使用します。もし単純に使用すると一つ目の項とマッチしてしまい証明が完了しません。コマンドbyは、証明完了しなかった場合にバックトラックし、別の項とマッチすることで証明ができないか探索します。従ってbyを使用することで証明が完了します。

次に、新たな論理和の導入規則を示します。

(~?Q ==> ?P) ==> ?P | ?Q　　　　(disjCI)

この導入規則はdisjI1やdisjI2と異なり、論理和の左右ともに残すことができます。例で見てみます。

lemma "(P | Q) & R ==> P | (Q & R)"
apply(rule disjCI)
apply(elim conjE disjE)
apply assumption
by(erule contrapos_np, rule conjI)

まずdisjCIを使用します。得られたサブゴールには~(Q & R)が前提に含まれています。

 1. [| (P | Q) & R; ~ (Q & R) |] ==> P

メソッドelimは除去規則を繰り返し適用します。一つ目のサブゴールはassumptionで証明が完了し、次のサブゴールが残ります。

 1. [| ~ (Q & R); R; Q |] ==> P

前提のQ & Rを結論に移動させる必要があります。そこでcontrapos_npを使用し、次に論理積の導入規則を適用しています。残りはassumptionのみで証明が完了します。そこでこれをbyを使用して1ステップで行っています。