Isabelle Tutorial その4
やっと証明に入りました。
2.3 An Introductory Proof
証明の大まかな流れを追ってみます。
Main Goal.
リストにrevを二回適用すると元に戻ることを証明します。
theorem rev_rev [simp]: "rev (rev xs) = xs"
theoremは新しい定理"rev (rev xs) = xs"を証明します。定理にはrev_revという名前を付けています。[simp]はこの定理を後から単純化ルールとして使うことを示しています。これは、単純化の際にrev (rev xs)をxsに置き換えることを意味します。定理名と単純化の属性はオプションです。
これを入力すると、Isabelleは次を返します。
1. rev (rev xs) = xs
証明中は、証明すべき残りのサブゴールが示されます。もちろん最初は単にメインゴールが示されます。
再帰関数に関する証明は一般的に帰納法を使って証明します。今回は変数xsに関する帰納法で証明します。
apply(induct_tac xs)
複数のサブゴールがある場合、最初のサブゴールに適用されます。適用すると、基底ケース(Nil)と帰納ケース(Cons)の二つのサブゴールが得られます。
1. rev (rev []) = [] 2. ∧a list. rev (rev list) = list ==> rev (rev (a # list)) = a # list
帰納ケースは典型的なサブゴールの形になっています。
i. ∧変数1 ... 変数n. 前提 ==> 結論
∧変数1 ... 変数n.の部分はとりあえず、このサブゴールのローカルな束縛変数と考えれば良いです。複数の前提がある場合は[| 前提1 ; 前提2 ; ... 前提n |]と書かれます。
両方のサブゴールの自動証明を試みます。
apply(auto)
autoは全てのサブゴールの自動証明を試みます。今回の場合、サブゴール1の証明は完了し、サブゴール2は次のサブゴールが残ります。
1. ∧a list. rev (rev list) = list ==> rev (rev list @ a # []) = a # list
このサブゴールから、補題が必要であることがわかります。
First Lemmas.
oopsで証明を中断するか、もしくはUndoで証明前の状態に戻り、次の補題の証明を行います。
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
lemmaとtheoremは単にそれが補題なのか定理なのかを示しており、全く同じ意味なのでどちらを使っても構いません。
今回の場合は変数が二つありますが、@の定義からxsを展開します。
apply(induct_tac xs) apply(auto)
次のサブゴールが残ります。
1. rev ys = rev ys @ []
また別の補題が必要そうです。
Second Lemma.
lemma app_Nil2 [simp]: "xs @ [] = xs" apply(induct_tac xs) apply(auto)
全てのサブゴールの証明が終わると、IsabelleはNo subgoals!を返します。
xs @ [] = xs No subgoals!
証明は次のようにして終了します。
done
doneの後は、定理と名前が結びつけられ参照可能となります。
最初の補題に戻って証明をやり直してみます。
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" apply(induct_tac xs) apply(auto)
app_Nil2が自動的に使われ、先ほどより証明が進みますが、次のサブゴールが残ります。
1. ∧a list. rev (list @ ys) = rev ys @ rev list ==>
(rev ys @ rev list) @ a # [] = rev ys @ rev list @ a # []
結論部分から、@の結合性に関するルールが足りないことがわかります。
Third Lemma.
@の結合法則を証明します。
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" apply(induct_tac xs) apply(auto) done
これで最初の補題も証明可能になりました。
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" apply(induct_tac xs) apply(auto) done
最後に、大本の定理の証明に戻ります。
theorem rev_rev [simp]: "rev (rev xs) = xs" apply(induct_tac xs) apply(auto) done
証明できました。理論ファイルの最後はendで終えます。endでIsabelleのプロセスが終了することがわかると思います。
今回の補題には全て[simp]が付いていましたが、これを付けるかどうかは注意が必要です。自動証明の中でsimpルールが適用可能であれば左辺を右辺に変換していくので、変換のループがあると最悪の場合自動証明が無限ループになります。[simp]を付けなかった場合の証明の方法はこのあと登場します。
2.4 Some Helpful Commands
コマンドには証明を進めるためのコマンドと、補助的なコマンドがあります。証明を進める基本的なコマンドはapply(method)という形をしており、methodにはinduct_tacやautoがあります。
補助コマンドを幾つか紹介します。
- defer - 先頭のサブゴールを後回しにします。
- prefer n - n番目のサブゴールを先頭にします。
- thm 定理名 - 定理を表示します。
- term 文字列 - 型チェックし、現在のコンテキストにおける項として表示します。
- typ 文字列 - 現在のコンテキストにおける型として表示します。
2.5 Datatype
2.5.1 Lists
リストは計算機における基本的なデータ型です。HOLにはListという理論が定義されており、その中にはhd(head)、tl(tail)、map、filterなどの関数も定義されています。また、[x1, ..., xn]はx1 # ... # xn # []の省略形です。
2.5.2 The General Format
データ型の定義は次の形をしています。
datatype (型変数1, ..., 型変数n) 型名 = 構成子1 型1 1 ... 型1 k1 | ... | 構成子m 型m 1 ... 型m km
構成子は大文字で始めるのが一般的です。
[] ~= x # xs(~は否定です)や(x # xs = y # ys) = (x = y & xs = ys)などの規則は、証明中の単純化のときに自動的に適用されます。これは原始再帰関数の定義でも同じです。
一部の例外を除くデータ型には関数sizeが定義されます。例えばリストの場合、sizeはリストの長さを返します。一般的には次の規則に従います。
- 引数を取らない構成子の場合は0。
- 引数を取る構成子の場合は、それぞれの引数のsizeの和に1を足した値。
sizeはそれぞれのデータ型に定義されている、つまりオーバーロードされています。リストの場合は、lengthという名前も付けられており、こちらはオーバーロードされていません。
2.5.3 Primitive Recursion
データ型上の関数は再帰関数、特に原始再帰関数で定義されることが多いです。つまり、再帰方程式は次の形をしていなければなりません。
f x1 ... (C y1 ... yk) ... xn = r
Cは構成子です。rはf ... yi ...という形をしていなければなりません。これから、Isabelleはfが停止性を満たしていることを判断できます。構成子毎に多くとも1つの再帰方程式を定義することができ、その順番は任意です。
Exercise 2.5.1
二分木を定義します。
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"
サブツリーを再帰的に入れ替える関数mirrorを定義し、mirror (mirror t) = tを証明します。
primrec mirror :: "'a tree => 'a tree" where "mirror Tip = Tip" | "mirror (Node lt v rt) = Node (mirror rt) v (mirror lt)" lemma "mirror_mirror: "mirror (mirror t) = t" apply(induct_tac t) apply(auto) done
二分木を通りがけ順でリストに変換する関数flattenを定義し、flatten (mirror t) = rev (flatten t)を証明します。
primrec flatten :: "'a tree => 'a list" where "flatten Tip = []" | "flatten (Node lt v rt) = (flatten lt) @ (v # flatten rt)" lemma "flatten (mirror t) = rev (flatten t)" apply(induct_tac t) apply(auto) done
2.5.4 Case Expressions
次の例のように、データ型にcase式を使うこともできます。
case xs of [] => [] | y # ys => y
case式のパターン部分には関数型プログラムのように、データ型の構成子、変数、_(ワイルドカード)を使うことができます。
2.5.5 Structural Induction and Case Distinction
induct_tacによる展開は行き過ぎになる場合、case_tacによる場合分けが有効な場合があります。
lemma "(case xs of [] => [] | y # ys => xs) = xs" apply(case_tac xs)
xsについて場合分けされ、二つのサブゴールが示されます。
1. xs= [] ==> (case xs of [] => [] | y # ys => xs) = xs 2. ∧a list. xs = a # list ==> (case xs of [] => [] | y # ys => xs) = xs
帰納法は前提に現れていない、自由変数または∧束縛変数にのみ適用できます。対して、case_tacは任意の項(変数とは限らない)に適用できます。ただし、∧以外で束縛されている変数を含んではなりません。
2.5.6 Case Study: Boolean Expressions
ブール式とその操作をどのようにモデル化し、Isabelleでどのように構成するか見ていきます。
Modelling Boolean Expressions.
ブール式は変数、定数、否定、論理積から構成することにします。
datatype boolex = Cosnt bool | Var nat | Neg boolex | And boolex boolex
例えばP0 ∧ ¬P1はAnd (Var 0) (Neg (Var 1))となります。
The Value of a Boolean Expression.
ブール式の値は変数に依存するため、評価するにはnat => bool型の関数が環境として必要になります。評価関数を次のように定義します。
primrec "value" :: "boolex => (nat => bool) => bool" where "value (Const b) env = b" | "value (Var x) env = env x" | "value (Neg b) env = (~ value b env)" | "value (And b c) env = (value b env & value c env)"
関数名valueが"で括られているのは、コマンドvalueと区別するためです。
If-Expressions.
別の表現方法として、いわゆるif式があります。if式を定数(CIF)、変数(VIF)、条件文(IF)から定義します。
datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
if式の評価関数を定義します。
primrec valif :: "ifex => (nat => bool) => bool" where "valif (CIF b) env = b" | "valif (VIF x) env = env x" | "valif (IF b t e) env = (if valif b env then valif t env else valif e env)"
Converting Boolean and If-Expressions.
boolexは一般的な論理式に近い表現であり、一方ifexは手続き的です。boolexからifexへの変換関数が定義できます。
primrec bool2if :: "boolex => ifex" where "bool2if (Const b) = CIF b" | "bool2if (Var x) = VIF x" | "bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)" | "bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)"
bool2ifが値を保存していることを証明します。
lemma "valif (bool2if b) env = value b env" apply(induct_tac b) apply(auto) done
bool2ifを使ってboolexからifexへ変換しても、値が変わらないことが証明できました。
次に、if式を正規化してみます。正規形とは、IFの第一引数が変数または定数のみで、別のIFではないこととします。サブ関数とともに、正規化関数を次のように定義できます。
primrec normif :: "ifex => ifex => ifex => ifex" where "normif (CIF b) t e = IF (CIF b) t e" | "normif (VIF x) t e = IF (VIF x) t e" | "normif (IF b t e) u f = normif b (normif t u f) (normif e u f)" primrec norm :: "ifex => ifex" where "norm (CIF b) = CIF b" | "norm (VIF x) = VIF x" | "norm (IF b t e) = normif b (norm t) (norm e)"
この定義は少し複雑ですが、Isabelleを使って値が変わっていないことを証明できます。
theorem "valif (norm b) env = valif b env"
これを証明するためには、次の補題が必要です。
lemma [simp]: "ALL t e. valif (normif b t e) env = valif (IF b t e) env"
次に、normが正しく正規化しているか確認します。そのために、正規化しているかどうか確認する関数を定義します。
primrec normal :: "ifex => bool" where "normal (CIF b) = True" | "normal (VIF x) = True" | "normal (IF b t e) = (normal t & normal e & (case b of CIF b => True | VIF x => True | IF x y z => False))"
これでnormal (norm b)を証明できれば、正しく正規化できていることがわかります。これを証明するには、次の補題が必要です。
lemma [simp]: "ALL t e. normal (normif b t e) = (normal t & normal e)"
メインゴールを自動証明した結果残ったサブゴールが、必要な補題のヒントとなります。補題に全称限量子が必要な理由は3.2節で説明します。
Exercise 2.5.2
正規化の定義を、IFの第一引数は変数でなければならないと変更してみます。
primrec normal :: "ifex => bool" where "normal (CIF b) = True" | "normal (VIF x) = True" | "normal (IF b t e) = (normal t & normal e & (case b of CIF b => False | VIF x => True | IF x y z => False))" primrec normif :: "ifex => ifex => ifex => ifex" where "normif (CIF b) t e = (if b then t else e)" | "normif (VIF x) t e = IF (VIF x) t e" | "normif (IF b t e) u f = normif b (normif t u f) (normif e u f)" primrec norm :: "ifex => ifex" where "norm (CIF b) = CIF b" | "norm (VIF x) = VIF x" | "norm (IF b t e) = normif b (norm t) (norm e)" lemma [simp]: "ALL t e. valif (normif b t e) env = valif (IF b t e) env" apply(induct_tac b) apply(auto) done theorem "valif (norm b) env = valif b env" apply(induct_tac b) apply(auto) done lemma [simp]: "ALL t e. (normal t & normal e) --> normal (normif b t e)" apply(induct_tac b) apply(auto) done theorem "normal (norm b)" apply(induct_tac b) apply(auto) done
-->は含意です。
