Isabelle Tutorial その11

5.7 Interlude: the Basic Methods for Rules

次の規則を例として、メソッドの作用を詳しく見ていきます。

$\frac{P_{1} \, \cdots \, P_{n}}{Q}$

規則の名前をRとします。

メソッドruleはQとサブゴールを単一化し、P₁からP_nを新たなサブゴールとします。

メソッドeruleはQとサブゴールを単一化すると同時にP₁を前提の何れかと単一化し、P₂からP_nをn - 1個の新たなサブゴールとします。単一化した前提は除去されます。(rule R, assumption)は似ていますが、前提は除去されません。

メソッドdruleはP₁を前提の何れかと単一化し、これを除去します。得られるサブゴールはP₂からP_nのn - 1個と、元のゴールの前提からP₁とマッチした項を取り除きQを加えた、計n個です。

メソッドfruleはdruleと似ていますが、マッチした仮定を除去しません。

各メソッドに_tacを付けると、単一化を制限することができます。

rule_tac v₁ = t₁ and ... and  v_n = t_n in R

これはruleと同じように作用しますが、v₁ ... v_nは指定した項で置き換えられます。また、適用するサブゴールを指定できます。デフォルトでは最初のサブゴールに適用されますが、次のようにするとi番目に適用できます。

rule_tac [i] R

5.8 Unification and Substitution

単一化は二つの項が同じかどうかを求めます。最も単純なケースは二つの項が既に等しい場合です。また、スキーム変数を項で置き換えることによって等しくできる場合も、単一化に成功します。単一化に成功すると、規則や他のサブゴールに含まれる同じスキーム変数は同時に置換されます。

Proof Generalの設定によって、単一化のログを見ることができます。これによって、単一化に失敗した原因を確認できます。

Isabelleは高階の単一化を使用します。変数の束縛は正しく判断され、自由変数が束縛されることはありません。例えば% x. f(x, z)と% y. f(y, z)は束縛変数が異なっているのみのため、正しく単一化できます。しかし、% x. ?Pと% x. t xは?Pをt xで置き換えると自由変数xが束縛される可能性があるため、単一化に失敗します。

高階の単一化では関数変数をラムダ式に置き換えますが、これが組み合わせ爆発を起こす場合があります。例えば?h aとa + bを単一化しようとすると、?hは% x. a + bと% x. x + bの二つの可能性があります。?h aとa + a + bは組み合わせによって四つの可能性が生じます。このように、二つ目の項のaの出現回数によって組み合わせは指数関数的に増えていきます。

5.8.1 Substitution and the subst Method

明示的に項を置換することもできます。代表的な規則は、等しい項を置き換える次の規則です。

$\frac{s = t \,\, P[s/x]}{P[t/x]}$

P[t/x]はPに含まれるxをtで置き換えた結果を表わします。Isabelleには次の規則があります。

[|?t = ?s; ?P ?s|] ==> ?P ?t　　　　(ssubst)

メソッドsimpも同様に置換しますが、置換規則はより細かく指定できます。例を見てみます。

lemma "[|x = f x; odd(f x)|] ==> odd x"
by(erule ssubst)

simpを使用すると前提のx = f xから、xをf xに置き換え、さらにf (f x)、f (f (f x))と、無限ループになる可能性があります*1。置換規則を使うと置換が一度だけ行われます。残りはassumptionで証明可能なので、byを使用しています。

メソッドsubstも置換に使用します。次のサブゴールがあるとします。

 1. [|P x y z; Suc x < y|] ==> f z = x * y

ここで、*の交換法則を使用したいとします。

?m * ?n = ?n * ?m　　　　(mult_commute)

しかし、交換法則は無限に適用可能なため、次のステップは実行できません。

apply(simp add: mult_commute)

メソッドsubstは、mult_commuteを一度だけ適用します。

apply(subst mult_commute)

その結果、次のサブゴールが得られます。

 1. [|P x y z; Suc x < y|] ==> f z = y * x

メソッドsubstは前提を置換したり、サブゴールに複数の置換対象がある場合に置換する項を指定したりもできます。

5.8.2 Unification and Its Pitfalls

次の例を見てみます。

lemma "[| x = f x; triple (f x) (f x) x|] ==> triple x x x"
apply(erule ssubst)
back
back
back
back
apply assumption
done

デフォルトでは、全ての出現が置換されるため、最初のeruleの適用では次のサブゴールが得られます。

 1. triple (f x) (f x) x ==> triple (f x) (f x) (f x)

これは前提とは一致しません。コマンドbackを使用すると、置換する箇所が次々と変わり、四回目の適用で前提と同じになります。

次のようにapplyを使用しても証明できます。

lemma "[| x = f x; triple (f x) (f x) x|] ==> triple x x x"
apply(erule ssubst, assumption)
done

最初のerule ssubstでは前提と一致しないことを既に見ました。従ってassumptionは失敗します。コマンドapplyは失敗すると自動的にバックトラックし、二つ目のメソッド(assumption)が成功するまで一つ目のメソッド(erule ssubst)の適用方法を変え、成功する道がないか探します。コマンドbyでも同様に証明できます。

lemma "[| x = f x; triple (f x) (f x) x|] ==> triple x x x"
by(erule ssubst)

さらに、tacを使用して単一化を制限する方法もあります。

lemma "[| x = f x; triple (f x) (f x) x|] ==> triple x x x"
by(erule_tac P = "% u. triple u u x" in ssubst)

置換結果が前提と一致するためバックトラックの必要がなくなり、また制限されているためそもそもバックトラックできなくなります。

オプションofを使用する方法もありますが、この方法は後ほど紹介します。

5.9 Quantifiers

全称限量から見ていきます。全称限量子の導入規則は一般的に次のように表記されます。

$\frac{P}{\forall x. P}$

さらに、xが前提に出現してはならないという条件が自然言語で書かれます。メタ論理と呼ばれるIsabelleの形式手法ではこのような条件の記載を無くすため、任意の値であるということを示すための限量子(!!)を導入しています。既に登場している==>もメタ論理の作用素です。残るメタ論理の作用素は==のみであり、これは定数定義に使用しています。

5.9.1 The Universal Introduction Rule

Isabelleでの全称限量子の導入規則は次のようになっています。

(!!x. ?P x) ==> ALL x. ?P x　　　　(allI)

この規則の使い方を例で見ていきます。

lemma "ALL x. P x --> P x"
apply(rule allI)
by(rule impI)

最初のステップはallIを適用しています。

 1. !!x. P x --> P x

高階論理の全称限量子が、メタ論理の全称限量子に置き換えられています。よってゴールは任意のxについてP x --> P xを証明することになります。後は含意の導入規則を適用し、assumptionで証明が完了します。

5.9.2 The Universal Elimination Rule

次に全称限量子の除去規則を見ます。一般的には次のように表記されます。

$\frac{\forall x. P}{P[t/x]}$

結論はxをtで置き換えたPです。Isabelleでは置換を関数で表わします。

ALL x. ?P x ==> ?P ?x　　　　(spec)

この破壊規則は全称限量子を取り除き、束縛変数xをスキーム変数?xに置き換えます。

次の形の除去規則もあります。

[|ALL x. ?P x; ?P ?x ==> ?R|] ==> ?R　　　　(allE)

drule specとerule allEは同じ効果をもたらします。

全称限量子の除去規則を、全称限量子のスコープを減らす規則の導出を例にしながら見ていきます。

$\frac{\forall x. P \rightarrow Q}{P \rightarrow \forall x. Q}$

この規則には、Pには自由変数xが含まれないという条件が付きます。Isabelleでは、Pが引数にxを取っていなければ、xには依存していないとみなされます。従って上の規則をIsabelleでは次のように書きます。

lemma "(ALL x. P --> Q x) ==> P --> (ALL x. Q x)"

まず、impIとallIを適用します。

apply(rule impI, rule allI)

すると、次のサブゴールが残ります。

 1. !!x. [| ALL x. P --> Q x; P |] ==> Q x

前提に全称限量があるので、druleを使って除去規則を適用します。

apply(drule spec)

サブゴールは次のようになります。

 1. !!x. [| P; P --> Q (?x2 x) |] ==> Q x

全称限量子が取り除かれ、束縛変数xが?x2 xに置き換わっています。これは、xに依存した項に置き換えられるスキーム変数を表わしています*2。前提に含意があるので、次にmpを使用します。

apply(drule mp, assumption)

 1. !!x. [| P; Q (?x2 x) |] ==> Q x

残るサブゴールはこのようになり、?x2 xは単純にxとすることで結論と一致します。従ってこのサブゴールはassumptionで完了します。

5.9.3 The Existential Quantifier

存在限量子の導入規則はexI、除去規則はexEです。

?P ?x ==> EX x. ?P x　　　　　　　　　　　　　　(exI)
[|EX x. ?P x; !!x. ?P x ==> ?Q |] ==> ?Q　　　　(exE)

Exercise 5.9.1

次の補題を証明します。

$\exists x. P \wedge Q(x) \Rightarrow P \wedge (\exists x. Q(x))$

lemma "EX x. P & Q x ==> P & (EX x. Q x)"
apply(erule exE, erule conjE)
apply(rule conjI, assumption)
by(rule exI)

5.9.4 Renaming an Assumption: rename_tac

allIを適用すると限量化された変数は新しい束縛変数になります。この時、問題がなければ変数名はそのままですが、他の変数とぶつかる場合は別の新しい名前になります。

lemma "x < y ==> ALL x y. P x (f y)"
apply(intro allI)

 1. !!xa ya. x < y ==> P xa (f ya)

xとyが使われているため、それぞれxaとyaに変わりました。この変数名を任意の名前に変えられます。

apply(rename_tac v w)

 1. !!v w. x < y ==> P v (f w)

rename_tacはメタ全称限量子によって限量化されている変数を、右から順に指定された名前に変更します。Isabelleによって自動生成される名前は変わる可能性があり、名前を直接参照すると問題が生じる場合があります。そのような場合は予めrename_tacで名前を変更しておくと良いでしょう。

5.9.5 Reusing an Assumption: frule

druleはマッチした前提を除去しますが、除去したくない場合もあります。そのような場合はfruleを使用します。次の例を見てみます。

lemma "[|ALL x. P x --> P (h x); P a|] ==> P (h (h a))"

まずspecをfruleで適用します。

apply(frule spec)

 1. [| ALL x. P x --> P (h x); P a; P ?x --> P (h ?x) |] ==> P (h (h a))

単一化した前提も残っていることがわかります。もしdruleを使用すると、証明は進めなくなります。次にmpを使用します。

apply(drule mp, assumption)

 1. [| ALL x. P x --> P (h x); P a; P (h a) |] ==> P (h (h a))

P (h a)を作ることで少し証明が進みました。再びspecを使用しますが、今度はdruleでも大丈夫です。

apply(drule spec)

 1. [| P a; P (h a); P ?x2 --> P (h ?x2) |] ==> P (h (h a))

更にmpを使用しますが、drule mpとしてしまうとP aとP ?x2がマッチしうまくいきません。そこでbyを使用するか、または

apply(drule mp, assumption, assumption)

とすることでメソッドが完了する道を見つけるまでバックトラックするため、証明が完了します。

5.9.6 Instantiating a Quantifier Explicitly

specによってALL x. P xから任意のtに関するP tを導出する例を見ました。多くの場合単一化によってtは正しく置き換えられますが、予め指定したい場合もあります。そのようなときはtacを使用します。5.9.5と同じ証明が、次のサブゴールまで進んだとします。

 1. [| ALL x. P x --> P (h x); P a; P (h a) |] ==> P (h (h a))

ここでspecを適用する際に、予めh aを指定します。

apply(drule_tac x="h a" in spec)

サブゴールは次のようになります。

 1. [| P a; P (h a); P (h a) --> P (h (h a)) |] ==> P (h (h a))

ここでmpを使用するとマッチする項は一つしかないため、バックトラックすることなく証明することができます。

存在限量子の場合も同様です。次の例では、整除性に関する次の定理を使用します。

?m dvd ?n == EX k. ?n = ?m * k　　　　(dvd_def)

自然数の乗算は整除性に対して単調であることを証明します。

lemma mult_dvd_mono: "[|i dvd m; j dvd n|] ==> i * j dvd (m * n::nat)"
apply(simp add:dvd_def)

定義を展開すると、次のサブゴールが残ります。

 1. [| EX k. m = i * k; EX k. n = j * k |] ==> EX k. m * n = i * j * k

次に、二つのEXを除去します。

apply(elim exE)

 1. !!k ka. [| m = i * k; n = j * ka |] ==> EX k. m * n = i * j * k

結論のkがk * kaならば証明できそうです。exIを使用しますが、kaはIsabelleが導入した名前ですので、5.9.4の理由によりまず名前を変更します。

apply(rename_tac l)

 1. !!k l. [| m = i * k; n = j * l |] ==> EX k. m * n = i * j * k

改めてexIを使用します。

apply(rule_tac x = "k * l" in exI)

 1. !!k l. [| m = i * k; n = j * l |] ==> m * n = i * j * (k * l)

残りはsimpで証明できます。

*1:実際には、今回の例ではメソッドsimpを使用しても証明できます

*2:形式的には、関数?x2に引数xが適用されたと考えます