Isabelle Tutorial その26

Isabelle

9.2 Advanced Induction Techniques

この節では、証明したい式が帰納法に適した形になっていない場合にどうすべきか、そして帰納法のための新たな定理をどのように導出し使うかということを見ていきます。

9.2.1 Massaging the Proposition

証明したい式が帰納法の適用に適した形になっていない場合があります。次の自明に思える式を証明してみます。

lemma "xs ~= [] ==> hd(rev xs) = last xs"
apply(induct_tac xs)

帰納法を適用すると、次のワーニングが出ます。

### Induction variable occurs also among premises: xs

さらにサブゴールは次の形になり、証明が進まなくなります。

 1. xs ~= [] ==> hd (rev []) = last []

ワーニングは、帰納法を使用する変数が==>の前提に含まれていることを指摘しています。このような場合は、7.2節で述べた通り、==>を-->に変え、証明後に元の形に戻すためにrule_formatオプションを追加します。

lemma hd_rev[rule_format]: "xs ~= [] --> hd(rev xs) = last xs"
apply(induct_tac xs)

 1. [] ~= [] --> hd (rev []) = last []

帰納変数を含む複数の前提A1, ..., Anがある場合、次のようにします。

A1 --> ... --> An --> C

変数ではなく項に対して帰納法を適用したい場合、ゴールを次のような形に変形します。

ALL y1 ... yn. x = t --> C

y1 ... ynはtに含まれる自由変数であり、xは新たに導入した変数です。このように変形し、xに対して帰納法を適用することができます。

9.2.2 Beyond Structural and Recursion Induction

より一般化した帰納ルールを使用しなければうまくいかない場合があります。例を通して見てみます。

nat上の構造的帰納法は数学的帰納法として知られています。これとは別に、完全帰納法というものがあります。これは、m < nを満たすすべてのmについてP(m)が成り立つとき、P(n)も成り立つというものです。Isabelleには次の定理として定義されています。

(!!n. ALL m ?P n) ==> ?P ?n　　　　(nat_less_induct)

次の関数の性質を証明してみます。

consts f :: "nat => nat"
axioms f_ax: "f(f(n)) < f(Suc(n))"

f n上の帰納法を使用して、fの公理からn <= f nを証明できます。上で説明した通り、ゴールは次のように変形しておきます。

lemma f_incr_lem: "ALL i. k = f i --> i <= f i"

次のようにして、nat_less_inductをkに対して適用します。

apply(induct_tac k rule: nat_less_induct)

 1. !!n. ALL m i <= f i ==> ALL i. n = f i --> i <= f i

ALL iを除去し、iについて場合分けします。i = 0は自明です。

apply(rule allI)
apply(case_tac i)
apply(simp)

 1. !!n i nat.
       [| ALL m i <= f i; i = Suc nat |]
       ==> n = f i --> i <= f i

残ったサブゴールは、次のステップで証明できます。

by(blast intro!: f_ax Suc_leI intro: le_less_trans)

ここでは、次の二つの補題が使われています。

?m < ?n ==> Suc ?m <= ?n　　　　　　　　　 (Suc_leI)
[| ?x <= ?y; ?y < ?z |] ==> ?x < ?z　　　　(le_less_trans)

求めたかった定理は次のようにして得られます。

lemmas f_incr = f_incr_lem[rule_format, OF refl]

最後のreflは前提の?k = f ?iを取り除きます。

Exercise 9.2.1

fの公理と補題から、fが恒等関数であることを証明します。

lemma f_ax': "f n < f (Suc n)"
apply(blast intro: le_less_trans f_incr f_ax)
done

lemma f_less_imp_less[rule_format]: "ALL n. f m < f n --> m < n"
apply(induct_tac m)
apply(clarify)
apply(case_tac n, simp, simp)
apply(blast intro!: Suc_lessI f_ax' less_imp_le intro: less_le_trans)
done

theorem "f n = n"
apply(rule antisym)
apply(subst less_Suc_eq_le[THEN sym])
apply(blast intro: f_less_imp_less f_ax)
apply(rule f_incr)
done

メソッドinduct_tacは、結論が?P ?x1 ... ?xnの形をしている任意のルールrを適用できます。適用するには次のようにします。

apply(induct_tac y1 ... yn rule: r)

ここでy1 ... ynはゴールの結論に含まれる変数です。

よく利用する帰納ルールに、リストの長さに対する帰納ルールlength_inductがあります。

(!!xs. ALL ys. length ys < length xs --> ?P ys ==> ?P xs) ==> ?P ?xs　　　　(length_induct)

これは、次のmeasure_inductの特別な場合です。

(!!x. ALL y. ?f y < ?f x --> ?P y ==> ?P x) ==> ?P ?a　　　　(measure_induct)

fはnatに関する任意の関数です。

9.2.3 Derivation of New Induction Schemas

帰納ルールも普通の定理なので、新たに作ることができます。nat_less_inductを作りながらその方法を見ていきます。まず次のように一般化した形で証明します。

lemma induct_lem: "(!!n::nat. ALL m < n. P m ==> P n) ==> ALL m < n. P m"
apply(induct_tac n)

基底ケースはblastで証明できます。帰納ケースは二つの場合に分けて考えます。m < nの場合は帰納法の仮定から真であり、m = nの場合も前提と帰納法の仮定から真であることがわかります。

apply(blast)
by(blast elim: less_SucE)

除去規則less_SucEは場合分けルールとして使えます。

[| ?m < Suc ?n; ?m < ?n ==> ?P; ?m = ?n ==> ?P |] ==> ?P　　　　(less_SucE)

この補題に対して、nをSuc nで、mをnでインスタンス化し、n < Suc nを取り除くとnat_less_inductになります。これは、補題を前提に追加すると自動的に計算されます。

theorem nat_less_induct: "(!!n::nat. ALL m < n. P m ==> P n) ==> P n"
by(insert induct_lem, blast)

HOLにはすべての帰納法の元となる整礎帰納法が用意されています。例えばnat_less_inductはwf_inductのrをnat上の<としたものです。

9.2.4 CTL Revisited

この節では、上で述べた帰納法の原則とヒューリスティクスのデモを見ていきます。また、帰納的定義が証明をどのように簡単にするかも見ていきます。

6.6.2でCTLを使用したモデル検査器の正当性を見ました。その中から、AF_lemma2をよりシンプルに証明してみます。

Aに含まれない状態のみからなるパスをA-avoidingパスと呼ぶことにします。すると、AF_lemma2は次を意味します。すなわち、sから始まる無限のA-avoidingパスが無いならば、sはlfp(af A)の要素です。まず、sから始まるA-avoidingパスで到達可能な状態の集合を帰納的に定義します。

inductive_set
  Avoid :: "state => state set => state set"
  for s :: "state" and A :: "state set"
where
"s : Avoid s A" |
"[| t : Avoid s A; t ~: A; (t,u) : M |] ==> u : Avoid s A"

無限のA-avoidingパスfについて、f 0 : Avoid s Aならば、sから始まる無限のA-avoidingパスが存在します。これを証明しますが、ゴールは帰納法を適用するために少し変形します。

lemma ex_infinite_path[rule_format]:
  "t : Avoid s A ==>
   ALL f : Paths t. (ALL i. f i ~: A) --> (EX p : Paths s. ALL i. p i ~: A)"
apply(erule Avoid.induct)
apply(blast)
apply(clarify)
apply(drule_tac x="% i. case i of 0 => t | Suc i => f i" in bspec)
apply(simp_all add: Paths_def split: nat.split)
done

基底ケース(t = s)は自明であり、blastで証明できます。帰納ケースの前提には、uから始まる無限のA-avoidingパスがあり、またtからuへの遷移もあります。よって、tからuへの遷移を付け加えたパスでゴールをインスタンス化すれば証明ができます。

次に、sから始まる無限のA-avoidingパスが無いならば、sはlfp(af A)のようであることを証明しますが、ゴールを一般化し、sからAまでのすべての状態tについてこれが成り立つことを証明します。

lemma Avoid_in_lfp[rule_format(no_asm)]:
  "ALL p : Paths s. EX i. p i : A ==> t : Avoid s A --> t : lfp(af A)"

証明はtからAまでの「距離」に関する帰納法を使用します。tがAに含まれているならばゴールは自明です。tがAに含まれず、tから先の状態がすべてlfp(af A)に含まれているならば、tがlfp(af A)に含まれていることもすぐに言えそうです。

以上の考え方を元に、Avoid s A - Aに制限したM、

{(y, x). (x, y) : M & x : Avoid s A & x ~: A}

に関する整礎帰納法で証明します。無限のA-avoidingパスが存在しないならば、この関係が整礎であることを導けます。まずはこれを仮定として加えて、証明を進めます。

apply(subgoal_tac "wf{(y, x). (x, y) : M & x : Avoid s A & x ~: A}")
apply(erule_tac a = t in wf_induct)
apply(clarsimp)

 1. !!x. [| ALL p:Paths s. EX i. p i : A;
            ALL y. (x, y) : M & x ~: A --> y : Avoid s A --> y : lfp (af A);
            x : Avoid s A |]
         ==> x : lfp (af A)
 2. ALL p:Paths s. EX i. p i : A
    ==> wf {(y, x). (x, y) : M & x : Avoid s A & x ~: A}

結論のlfpを展開すると、tがAに含まれている、またはtから辿れるすべての状態がlfp(af A)に含まれているのどちらかになります。もしt ~: Aならば、二つ目の仮定からtから辿れるすべての状態がlfp(af A)に含まれていることが導けます。これを次のように証明します。

apply(subst lfp_unfold[OF mono_af])
apply(simp (no_asm) add: af_def)
apply(blast intro: Avoid.intros)

メインゴールの証明が終わったので、追加したサブゴールの証明に入ります。こちらは対偶を証明し、定理wf_iff_no_infinite_down_chainを使用します。

wf ?r = (~ (EX f. ALL i. (f (Suc i), f i) : ?r))　　　　(wf_iff_no_infinite_down_chain)

apply(erule contrapos_pp)
apply(simp add: wf_iff_no_infinite_down_chain)
apply(erule exE)
apply(rule ex_infinite_path)
apply(auto simp add: Paths_def)
done

rule_formatの(no_asm)は、定理の変更を結論のみにし、前提を変形しないことを指示します。

この補題から、AF_lemma2は簡単に導くことができます。

theorem AF_lemma2: "{s. ALL p : Paths s. EX i. p i : A} <= lfp(af A)"
by(auto elim: Avoid_in_lfp intro: Avoid.intros)