Isabelle Tutorial その19
7. Inductively Defined Sets
この章では集合の帰納的定義を紹介します。
7.1 The Set of Even Numbers
偶数の集合は、定数0と演算子+2からなる最小の集合として帰納的に定義できます。もちろん、整除関係(dvd)を使用しても定義できます。それぞれの方法で定義した集合が等しいことを証明してみます。
7.1.1 Making an Inductive Definition
inductive_setを使用して、偶数の集合evenを帰納的に定義できます。
inductive_set even :: "nat set" where zero[intro!]: "0 : even" | step[intro!]: "n : even ==> (Suc (Suc n)) : even"
最初の規則は0がevenに含まれること、二つ目はnがevenに含まれるならば、n + 2も含まれることを示しています。これはそのまま導入規則でもあります。Isabelleは定義と同時に導入規則、除去規則、帰納ルールなども生成します。以下はその中の二つの例です。
0 : even (even.zero) ?n : even ==> Suc (Suc ?n) : even (even.step)
導入規則にはオプションを付けることができます。今回はどちらの規則もsafeルールであることから、intro!を付けています。
7.1.2 Using Introduction Rules
2 * kが偶数であることを証明してみます。
lemma two_times_even [intro!]: "2 * k : even" apply(induct_tac k) apply auto done
最初のステップはkについての帰納法の適用です。サブゴールは次の二つになります。
1. 2 * 0 : even 2. !!n. 2 * n : even ==> 2 * Suc n : even
どちらも単純化するとevenの導入規則が使える形になり、証明が完了します。
最終的な目的はdvdを使って定義した偶数集合と帰納的に定義した集合が一致することを証明することであり、片方向は上の補題で証明できます。
lemma dvd_imp_even: "2 dvd n ==> n : even" by(auto simp add: dvd_def)
two_times_evenにはintro!オプションが付いているため、autoの中で自動的に使われています。
7.1.3 Rule Induction
evenの定義から、次の帰納ルールが生成されています。
[| ?x : even; ?P 0; !!n. [| n : even; ?P n |] ==> ?P (Suc (Suc n)) |] ==> ?P ?x (even.induct)
すべての偶数が?Pを満たすためには、?P 0が成り立つことと、演算Suc (Suc .)について閉じている必要があります。このような帰納法を規則帰納といいます。自然数を0とSucで帰納的に定義できることから、数学的帰納法も規則機能の一種です。
上の証明の逆方向を証明してみます。
lemma even_imp_dvd: "n : even ==> 2 dvd n"
帰納法で証明しますが、even.inductが除去規則の形をしているので、eruleを使用します。
apply(erule even.induct)
dvdを定義で展開し、一つ目のサブゴールは終了し、二つ目のみが残ります。
apply(simp_all add: dvd_def) apply clarify
1. !!n k. 2 * k : even ==> EX ka. Suc (Suc (2 * k)) = 2 * ka
kaをSuc kにすることで、証明が終わります。
apply(rule_tac x = "Suc k" in exI, simp)
最後に、二つの補題を繋げます。
lemma even_iff_dvd: "(n : even) = (2 dvd n)" by(blast intro: dvd_imp_even even_imp_dvd)
7.1.4 Generalization and Rule Induction
多くの場合、帰納法を適用する前にゴールを一般化する必要があります。ゴールの一般化は難しく、問題の形を大きく変えなければならないかもしれません。次の例は、帰納法で証明しようとしますがうまくいきません。
lemma "Suc (Suc n) : even ==> n : even" apply(erule even.induct) oops
帰納法を適用したとき、ゴールの結論はSuc (Suc n)というかたちではないため、結論はそのまま残ります。よってサブゴールは次のようになり、一つ目のサブゴールは証明できなくなります。
1. n : even 2. !!na. [| na : even; n : even |] ==> n : even
このような場合の対処方法の詳細は9.2.1で説明しますが、今回は加算を減算にすることで簡単に解決できます。
lemma even_imp_even_minus_2: "n : even ==> n - 2 : even" apply(erule even.induct) apply auto done
この補題を使って元の定理を証明できます。
lemma Suc_Suc_even_imp_even: "Suc (Suc n) : even ==> n : even" by(drule even_imp_even_minus_2, simp)
even.stepの逆を証明することができました。よって、次の等式も証明できます。
lemma [iff]: "((Suc (Suc n)) : even) = (n : even)" by(blast dest: Suc_Suc_even_imp_even)
7.1.5 Rule Inversion
帰納的定義の場合分けは、規則の反転と呼ばれます。Isabelle/HOLでこれがどのように働くか見ていきます。
もしaがevenの要素ならば、aは0、またはSuc (Suc n)の形をしており、nもevenの要素のどちらかです。次の場合分けルールがこれを表わしています。
[| ?a : even; ?a = 0 ==> ?P; !!n. [| ?a = Suc (Suc n); n : even |] ==> ?P |] ==> ?P (even.cases)
しかしこの規則はあまり便利とは言えません。例えばaがSuc (Suc n)の形をしているならば、場合分けの一つ目は意味がなく、二つ目があれば十分です。次の方法で、そのようなルールを作ることができます。
inductive_cases Suc_Suc_cases [elim!]: "Suc (Suc n) : even"
コマンドinductive_casesは与えたパターンに対する場合分けルールを生成します。Suc_Suc_casesは次のようになります。
[| Suc (Suc ?n) : even; ?n : even ==> ?P |] ==> ?P (Suc_Suc_cases)
even.casesがサブゴールを二つ作るのに対し、この規則をeruleで適用した場合はサブゴールを一つしか作りません。このような規則は、導入規則の結論にSucや#(cons)のようなデータ型の構築子が含まれている場合にうまく働きます。
inductive_casesにオプションを付けることもでき、上の例ではelim!を付けています。元の場合分けルールは無限ループを引き起こす可能性がありますが、Suc_Suc_casesはパターンマッチが制限されているため、その危険性がなくなっています。
inductive_casesを使って新しい定理を定義しなくとも、証明の中で使うことができます。
apply(ind_cases "Suc (Suc n) : even")
メソッドind_casesはinductive_casesと同じように与えたパターンに対する場合分けルールを作り、除去規則として適用します。
7.1.6 Mutually Inductive Definitions
データ型と同じように、集合を相互帰納的に定義することができます。例として偶数集合と奇数集合を定義します。
inductive_set Even :: "nat set" and
Odd :: "nat set" where
zero: "0 : Even" |
EvenI: "n : Odd ==> Suc n : Even" |
OddI: "n : Even ==> Suc n : Odd"
データ型のときと同じように、帰納法を使う場合は両方の集合について同時に証明しなければなりません。上の例の帰納ルールはEven_Odd.inductという名前が付いています。
全ての偶数が2で割り切れることを証明したい場合、次のようにゴールを一般化しなければなりません。
lemma "(m : Even --> 2 dvd m) & (n : Odd --> 2 dvd (Suc n))"
帰納法を使用しますが、Even_Odd.inductが導入規則の形をしているので、eruleではなくruleを使用します。
apply(rule Even_Odd.induct)
証明の続きは省略します。
7.1.7 Inductively Defined Predicates
集合の代わりに、nat上の述語を定義することもできます。
inductive evn :: "nat => bool" where zero: "evn 0" | step: "evn n ==> evn (Suc (Suc n))"
inductive_setの代わりにinductiveを使い、n : evenの代わりにevn nとしています。evenと同じ性質を持ちますが、集合演算子はもちろん使えません。
