Isabelle Tutorial その15

5.17 Managing Large Proof

長くなりがちな証明のステップを短くする方法を見ていきます。

5.17.1 Tacticals, or Control Structures

長い証明の中には、規則性が現れることがあります。プラス記号(+)を使用して、ステップを繰り返すことができます。例えば、次の証明を見てみます。

lemma "[|P --> Q; Q --> R; R --> S; P|] ==> S"
apply(drule mp, assumption)
apply(drule mp, assumption)
apply(drule mp, assumption)
apply(assumption)
done

同じコマンドが三回続いています。これを、次のように証明できます。

lemma "[|P --> Q; Q --> R; R --> S; P|] ==> S"
by(drule mp, assumption)+

byを使用しているのは最後のassumptionが必要なためです。+は適用が可能なだけ繰り返し適用します。

縦棒(|)で二つのメソッドを区切ると、まず左のメソッドが適用され、適用できなかった場合に右のメソッドが適用されます。これは、繰り返しとともに使用すると便利です。次の証明では、assumptionが必要な場合と、x + 1 < 5からx < 5を推論するためにarithが必要な場合があります。そこで、次のように証明します。

lemma "[|Q --> R; P --> Q; x < 5 --> P; Suc x < 5|] ==> R"
by(drule mp, (assumption|arith))+

はてな(?)はメソッドを0または一回適用します。(m+)?とするとmを0回以上繰り返します。

5.17.2 Subgoal Numbering

サブゴールの数が非常に多くなる場合があります。Isabelleはデフォルトではサブゴールを10個までしか表示しません。コマンドprはこの数を変更します。

pr 2
 1. subgoal1
 2. subgoal2
A total of 6 subgoals...

多くのメソッドは最初のサブゴールに適用されます。他のサブゴールに注目したい場合、コマンドdeferまたはpreferを使用します。コマンドdeferは最初のサブゴールを後ろにまわします。コマンドpreferは指定した数字のサブゴールを先頭にまわします。これにより、難しいサブゴールを後回しにしたり、証明可能かどうか疑わしいサブゴールを先に確認したりすることができます。

Exercise 5.17.1

次の証明の中で?と+がどのように使われているか説明します。

lemma "[|P & Q --> R; P --> Q; P|] ==> R"
by(drule mp, (intro conjI)?, assumption)+

証明のステップを分けてみます。

lemma "[|P & Q --> R; P --> Q; P|] ==> R"
apply(drule mp, assumption)
apply(drule mp, intro conjI, assumption)
apply(assumption)
apply(assumption)
done

1ステップ目と2ステップ目は、intro conjIの部分が異なっています。そこで、intro conjIに?を付けて0または一回適用することにし、更に全体を+にすることで繰り返し適用します。残りのassumptionはbyが自動的に実行します。

5.18 Proving the Correctness of Euclid's Algorithm

gcdが最大公約数を返すことを証明してみます。gcdの定義と単純化規則は3.5.3で定義したものを使用します。

まず、次の補題を証明します。

lemma gcd_dvd_both: "(gcd m n dvd m) & (gcd m n dvd n)"
apply(induct_tac m n rule: gcd.induct)

帰納ケースにおいてお互いに参照し合うため、論理積の左右両方を同時に証明する必要があります。サブゴールは次のようになります。

 1. !!m n. (n ~= 0 ==> gcd n (m mod n) dvd n & gcd n (m mod n) dvd m mod n)
           ==> gcd m n dvd m & gcd m n dvd n

前提から、n = 0かどうかで場合分けすると良さそうです。

apply(case_tac "n = 0")
apply(simp_all)

 1. !!m n. [| gcd n (m mod n) dvd n & gcd n (m mod n) dvd m mod n; 0 < n |]
           ==> gcd n (m mod n) dvd m

このサブゴールを証明するために、次の定理を利用します。

[|?k dvd (?m mod ?n); ?k dvd ?n|] ==> ?k dvd ?m　　　　(dvd_mod_imp_dvd)

この定理は導入規則としても使用できますが、ここでは破壊規則として使用してみます。サブゴールは次のステップで証明が完了します。

apply(blast dest: dvd_mod_imp_dvd)

論理積の左右それぞれを定理とするために分割します。

lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2]

gcdが公約数であることは証明できましたので、それが最大であることを証明します。

lemma gcd_greatest [rule_format]: "k dvd m --> k dvd n --> k dvd gcd m n"

ゴールはHOLの含意を使用していますが、これは証明に帰納法を使用するためです。オプションrule_formatは、証明後に-->を==>に変換します。また、全称限量子を取り除き一般的な推論規則の形に変形もします。これは、THENを使用してmpとspecを必要なだけ適用したのと同じことです。今回の場合は次のように書くのと同じです。

lemma gcd_greatest [THEN mp, THEN mp]: "k dvd m --> k dvd n --> k dvd gcd m n"

証明の最初のステップは先ほどと同じように、帰納法の適用と場合分けです。サブゴールは次のようになります。

 1. !!m n. [| n ~= 0 ==> k dvd n --> k dvd m mod n --> k dvd gcd n (m mod n);
              n = 0 |]
           ==> k dvd m --> k dvd n --> k dvd gcd m n
 2. !!m n. [| n ~= 0 ==> k dvd n --> k dvd m mod n --> k dvd gcd n (m mod n);
              n ~= 0 |]
           ==> k dvd m --> k dvd n --> k dvd gcd m n

一つ目のサブゴールは単純化で証明できます。二つ目のサブゴールには、次の定理を使用します。

[|?f dvd ?m; ?f dvd ?n|] ==> ?f dvd ?m mod ?n　　　　(dvd_mod)

よって次のコマンドで証明が完了します。

apply(simp_all add: dvd_mod)

最後に、これまでの定理を論理的同値でまとめます。

theorem gcd_greatest_iff [iff]: "(k dvd gcd m n) = (k dvd m & k dvd n)"
by(blast intro!: gcd_greatest intro: dvd_trans)

gcd_greatestを導入規則として使用しています。intro!は指定したルールがsafeルールであることを示しており、そのルールはより積極的に利用されます。!がない場合はunsafeルールとして使用されます。dvd_transは整除関係の推移律です。

[|?m dvd ?n; ?n dvd ?p|] ==> ?m dvd ?p　　　　(dvd_trans)

さらにこの証明の中では、gcd_dvd1とgcd_dvd2が暗黙のうちに使用されています。