Isabelle Tutorial その13

5.12 Proving Theorems Using the blast Method

Isabelleのclassical reasonerは自動証明のためのツールの一つであり、その中でも最も重要なメソッドがblastです。

述語論理の例から見ていきます。次の例はAndrew's challengeと呼ばれ、自動証明が難しいとされる定理です。しかし、blastはこれを解くことができます。

lemma "((EX x. ALL y. p(x) = p(y)) = ((EX x. q(x)) = (ALL y. p(y)))) =
       ((EX x. ALL y. q(x) = q(y)) = ((EX x. p(x)) = (ALL y. q(y))))"
by blast

blastは集合にも使えます。次の定理もblastで解くことができます。

lemma "(UN i : I. A(i)) Int (UN j : J. B(j)) =
       (UN i : I. UN j : J. A(i) Int B(j))"
by blast

新しいルールを追加することで、classical reasonerを強化していくことができます。そのためには、導入、除去、破壊の各ルールを理解する必要があります。さらに、safeとunsafeを区別する必要があります。情報を失うことなく適用できるルールをsafeルールといい、情報を失ってしまうルールをunsafeルールといいます。情報を失うため、unsafeルールは適用を間違うと証明が失敗する可能性があります。classical reasonerは自動証明に失敗すると、最後に適用したunsafeルールまでバックトラックし、別の道を探します。

論理的同値にオプションiffを付けることでも、classical reasonerや単純化に新しいルールを追加できます。例として、リストの結合を見てみます。二つのリストを結合した結果が空リストであることと、それぞれのリストが空リストであることは同値です。次の定理を証明することで、classical reasonerと単純化の新しいルール追加されます。

lemma [iff]: "(xs @ ys = []) = (xs = [] & ys = [])"
apply(induct_tac xs)
apply(simp_all)
done

P = Qという定理にiffを付けると、導入規則Q => Pと破壊規則P => Qの二つのルールが作られます。どちらもsafeルールであり、ルールに含まれるPをQに置き換えます。また、単純化も同様にPをQに置き換えます。単純化とclassical reasonerの違いは、単純化は可能な限り置き換えを繰り返すだけなのに対し、classical reasonerは証明に失敗した場合はバックトラックし、別の道を探すところです。

5.13 Other Classical Reasoning Methods

メソッドclarifyはゴールを複数に分割することなく、safeルールだけを適用します。例えば次の正しくない補題を証明してみます。

lemma "(ALL x. P x) & (EX x. Q x) --> (ALL x. P x & Q x)"
apply clarify

メソッドblastを使用した場合は単に失敗するだけですが、clarifyを使用した場合は次のサブゴールが残ります。

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

前提のQ xaと結論のQ xは変数が異なるため、証明に失敗します。このように、clarifyを使用すると証明がうまくいかない理由のヒントが得られます。

メソッドclarsimpはclarifyとsimpを同時に使用するメソッドです。こちらはsimpによってゴールが複数に分割される場合があります。

メソッドforceはclassical reasonerと単純化を一つのサブゴールにのみ適用します。証明に失敗した場合は単に失敗するのみで、ゴールを変形することはありません。autoもclassical reasonerと単純化の両方を使用しますが、こちらは全てのサブゴールに適用されます。また、証明に失敗した場合も途中経過がサブゴールとして残ります。よってautoは非常に多くの新しいサブゴールに変形してしまう可能性があります。またforceはautoよりも深く証明しようと試みるため、終了するまで時間がかかる場合もあります。

メソッドblastが組み込みのfirst-order reasonerを使用して証明しようとするのに対して、fastとbestは標準的なIsabelleの推論を使用します。これによって証明が遅くなりますが、Isabelle固有の規則を使えるようになります。例えば、SOMEの導入規則をもう一度見てみます。

?P ?x = (SOME x. ?P x)　　　　(someI)

次の補題を証明してみます。

lemma "[|Q a; P a|] ==> P (SOME x. P x & Q x) & Q (SOME x. P x & Q x)"
apply(rule someI)

someIを使用すると次のサブゴールが残ります。

 1. [| Q a; P a |] ==> P ?x & Q ?x

ここから先の証明は明らかです。この定理を1ステップで証明するにはどうしたらよいでしょうか。blastは高階の単一化ができないためうまくいきません。このような場合はfastを使用します。

apply(fast intro!: someI)

bestも同様に働きますが、fastが深さ優先探索で証明できる経路を探すのに対し、bestは最良優先探索で証明しようとします。

5.14 Finding More Theorems

パターンマッチや名前で定理を探す他に、証明しようとしているゴールに適用できるルールを探す方法があります。

introは導入規則として適用できる定理を検索します。例えば次のゴール

 1. A & B

に対してintroとして定理を検索すると、==> ?P & ?Qで終わる定理を探すことができます。

検索条件は単に並べて組み合わせることができます。例えば

"_ @ _" intro

は現在のゴールに適用可能な、関数@に関係する導入規則を検索します。

elimとdestは同様にそれぞれ現在のゴールに適用可能な除去規則と破壊規則を検索します。