Isabelle Tutorial その7
3.2 Induction Heuristics
この節では、帰納法を使った証明のヒューリスティクスを説明します。最初は既に出てきたヒューリスティクスです。
次は二つ以上の引数を取る関数の証明についてです。
このヒューリスティクスは例えば2.3節の証明で使いました。
ゴールが固有的な場合、帰納ケースの前提が弱すぎて証明できない場合があります。そこでキーとなるヒューリスティクスは、帰納法を使う前にゴールを一般化することです。例を使って見ていきます。
関数revは効率が悪いので、累積変数を導入し線形時間で計算可能な関数を作成します。
primrec itrev :: "'a list => 'a list => 'a list" where "itrev [] ys = ys" | "itrev (x#xs) ys = itrev xs (x#ys)"
itrevがrevと同じ振る舞いをすることを確かめるために、次の補題を証明します。
lemma "itrev xs [] = rev xs" apply(induct_tac xs, simp_all)
しかし、証明は完了せず、帰納ケースが次のように残ります。
1. !!a list.
itrev list [] = rev list ==> itrev list (a # []) = rev list @ a # []
引数[]が固定されているため、前提が弱すぎて証明できません。この例から次のヒューリスティクスが出てきます。
定数を変数に置き換え、ゴールを一般化せよ。
今回の場合は、左辺の[]を変数に置き換えただけではうまくいきません。証明すべき補題は以下になります。
lemma "itrev xs ys = rev xs @ ys"
今回は次のようなサブゴールが残ります。
1. !!a list.
itrev list ys = rev list @ ys ==> itrev list (a # ys) = rev list @ a # ys
まだ前提が弱いため証明ができません。問題は変数ysが固定されていることであり、よって全称限量子を導入します。
lemma "ALL ys. itrev xs ys = rev xs @ ys"
この補題は帰納法ですぐに証明することができます。以上のことから、次のヒューリスティクスが出てきます。
(帰納法を適用する変数を除く)全ての自由変数を全称限量し、ゴールを一般化せよ。
これによってゴールの妥当性に影響を与えることなく、上の例のような問題を回避できます。しかし、いつでもこのヒューリスティクスを使えばよいわけではありません。全性限量子が必要ではない場合もありますし、証明を複雑にしてしまいます。多くの場合、再帰呼び出しによって変わる変数を全称限量するとよいでしょう。
最後のヒューリスティクスです。
等式の右辺は左辺よりも単純にせよ。
どちらが単純か簡単にはわからない場合もあります。しかし、証明がうまくできないときに、左右を入れ替えて試してみるとよいかもしれません。
Exercise 3.2.1
次の関数を定義します。
primrec add :: "nat => nat => nat" where "add m 0 = m" | "add m (Suc n) = add (Suc m) n"
add m n = m + nを証明します。
lemma "ALL m. add m n = m + n" apply(induct_tac n, simp_all) done
Exercise 3.2.2
問題2.5.1で作成した関数flattenを、累積変数を導入し線形時間で計算可能な関数に変更し、振る舞いが変わっていないことを証明します。
primrec itflatten :: "'a tree => 'a list => 'a list" where "itflatten Tip xs = xs" | "itflatten (Node lt v rt) xs = itflatten lt (v # itflatten rt xs)" lemma "ALL xs. itflatten t xs = (flatten t) @ xs" apply(induct_tac t, simp_all) done
