Isabelle Tutorial その6
3. More Functional Programming
3.1 Simplification
単純化はIsabelle及び他の多くのシステムにおいて重要な定理証明ツールです。今節では単純化について述べていきます。
3.1.1 What is Simplification?
簡単に言うと、単純化とは等式の左辺から右辺への変換を繰り返すことです。例えば、@のルールを使った単純化のステップを示します。
(0#1#[]) @ [] → 0#((1#[]) @ []) → 0#(1#([] @ [])) → 0#1#[]
これは項書換えと見ることもでき、その場合等式は書換規則と見ることができます。
既に見たように単純化を用いて算術式を証明することもできますが、この場合は項書換え以上のことが行われています。ただしこれについてこのチュートリアルでは取り上げません。
3.1.2 Simplification Rules
定理に[simp]属性を付けると、単純化の際に自動的に使われます。また、datatypeとprimrecは幾つかの単純化ルールを陰に作ります。
単純化の属性は有効/無効を切り替えることができます。
declare 定理名[simp] declare 定理名[simp del]
3.1.3 The simp Method
simpメソッドにはオプションを付けることができます。詳細は後述します。simpは先頭のサブゴールにのみ適用されます。全てのサブゴールに適用したい場合は、simp_allを使用します。
3.1.4 Adding and Deleting Simplification Rules
simpメソッドを適用するときにオプションを付けることで、使用するルールを変更することができます。
add: 追加する定理名のリスト del: 削除する定理名のリスト only: 使用する定理名のリスト
ある定理のみを使用し、それ以外を使用したくない場合はonlyを使用します。例えば二つの分配法則を加えて単純化したい場合、次のようにします。
apply(simp add: mod_mult_distrib add_mult_ditrib)
3.1.5 Assumptions
デフォルトでは、ゴールの前提も単純化の対象となります。しかし、これが問題を引き起こす場合もあります。
lemma "ALL x. f x = g (f (g x)) ==> f [] = f [] @ []"
この定理にsimpメソッドを適用すると、無限ループに陥り応答が返ってきません。これを回避するには、前提を単純化の対象から外します。
apply(simp (no_asm)) done
(no_asm)は前提を全く無視します。(no_asm_simp)は前提を単純化しませんが、結論の単純化には使用します。(no_asm_use)は前提を単純化しますが、他の前提や結論の単純化には使用しません。
3.1.6 Rewriting with Definitions
2.7.2で説明した定数定義は単純化に使用することができますが、自動で適用されません。例を示します*1。
lemma "xor A (~A)"
次のようにして、xorを定義で展開できます。
apply(simp only: xor_def)
次の結果が得られます。
1. A & ~ ~ A | ~ A & ~ A
これはすぐに証明できます。一回のコマンドで証明するには、次のようにします。
apply(simp add: xor_def)
関数fをf x y == tと定義した場合、fをその定義で置き換えるには二つの引数が必要です。しかしf == % x y. tと定義すると、全てのfを定義で置き換えることができます。
単に定義で置き換えたい場合は、メソッドunfoldも使えます。例えば次のように使えます。
apply(unfold xor_def)
unfoldは全てのサブゴールに適用されます。
3.1.7 Simplifying let-Expressions
let式を展開するには、Let_defを使用します。以下に例を示します。
lemma "(let xs = [] in xs @ ys @ xs) = ys" apply(simp add: Let_def) done
3.1.8 Conditional Simplification Rules
これまでは等式のみを扱ってきましたが、単純化には次の例のような条件付きの等式も使えます。
lemma hd_Cons_tl[simp]: "xs ~= [] ==> hd xs # tl xs = xs" apply(case_tac xs, simp, simp) done
メソッドは","で区切って並べることができます。hd_Cons_tlが単純化ルールなので、次の補題をsimpのみで証明することができます。
lemma "xs ~= [] ==> hd (rev xs) # tl (rev xs) = rev xs"
3.1.9 Automatic Case Splits
ゴールがif式を含んでいる場合、通常場合分けで証明します。
lemma "ALL xs. if xs = [] then rev xs = [] else rev xs ~= []"
メソッドsplitで場合分けすることができます。
apply(split split_if)
split_ifはif式を場合分けする定理です。ただしこれは、単純化の際に自動的に行われます。
この考え方はcase式にも適用できます。リスト上のcase式を単純化してみます。
lemma "(case xs of [] => zs | y # ys => y # (ys @ zs)) = xs @ zs" apply(split list.split)
再帰的データ型の場合に無限ループになる可能性があるため、case式の場合分けは自動的には行われません。代わりに、場合分けルールをsplitオプションで指定することができます。上の補題は次の一手で証明できます。
apply(simp split: list.split)
また、split delオプションで削除することもできます。
apply(simp split del: split_if)
さらに、自動適用の有効/無効を切り替えることもできます。
declare list.split [split] declare list.split [split del]
全てのデータ型tについて、場合分けルールt.splitがあります。
上の方法では、結論のみ場合分けされます。前提も場合分けしたい場合は、split_if_asmやt.split_asmを使用します。また前提と結論の両方を場合分けしたい場合は、if_splitsやt.splitsを使用します。
if式を単純化した場合、条件部のみが単純化され、then節とelse節は単純化されません。then節及びelse節は場合分けされた後にのみ単純化できます。これはcase式についても同様です。
3.1.10 Tracing
Proof Generalのオプションを使用すると、単純化のトレースログを見ることができます。トレースログから証明のヒントが得られるかもしれません。
3.1.11 Finding Theorems
Proof GeneralのFindボタンを使用して、定理を検索することができます。検索にはパターンマッチが使えます。例をいくつか示します。
length "_ # _ = _ # _" "_ + _" "_ * (_ - (_::nat))"
"_"はワイルドカードです。最後の例のように、オーバーロードされた演算子に対して型を指定することで検索結果を絞ることができます。
単純化に使用される書換規則を検索する場合は、パターンにsimp:を追加します。
simp: "_ * (_ + _)"
名前で検索することもできます。以下は、commという文字列を含む名前の定理を検索します。
name: comm
検索パターンを否定することもできます。例えばListに関する定理を検索範囲から外したい場合は次のようにします。
-name: List
複数のパターンを組み合わせたい場合は、スペースで区切って並べます。
*1:xorの定義は前述の通りです。
