Isabelle Tutorial その22
8. More about Types
この章ではより高度な型の扱い方を紹介します。
8.1 Pairs and Tuples
ペアやタプルは既に登場しましたが、ここではパターンマッチついて見てみます。
8.1.1 Pattern Matching with Tuples
変数を束縛するためのパターンとしてペアやタプルを使うことができます。例をいくつか示します。
% (x, y, z). x + y + z
let (x, y) = f z in (y, x)
case xs of [] => 0 | (x, y) # zs => x + y
ALL (x, y) : A. x = y
{(x, y, z). x = z}
UN (x, y) : A. {x + y}
ペアやタプルを使った抽象化は単なる略記なので、例えば% (x, y). x + yの代わりに% p. fst p + snd pと書くことができます。
% (x, y). tは内部的にはsplit (% x y. t)に変換されます。splitは型が('a => 'b => 'c) => 'a * 'b => 'cであり、定義は次の通りです。
split == %c p. c (fst p) (snd p) (split_def)
他の形の変数に対するパターンマッチも同様に変換されるので、ペアの場合に対する推論方法のみを見ていきます。
8.1.2 Theorem Proving
もっとも愚直な方法はsplit:による展開を手当たり次第に適用することです。
lemma "(% (x, y). x) p = fst p" by(simp add: split_def)
しかしこの方法は、上の例ではうまくいきますが、いつもうまくいくとは限りません。pを任意のペア(a, b)に置き換えられると、左辺と右辺はそれぞれ単純化ルールsplit f (a, b) = f a bとfst (a, b) = aで単純化できます。split f pの形を置き換えるには、split_splitを使用します。
lemma "(% (x, y). y) p = snd p" apply(split split_split)
1. ALL x y. p = (x, y) --> y = snd p
この残ったサブゴールは単純化で証明できます。
次の例を見てみます。
lemma "let (x, y) = p in fst p = x" apply(simp only: Let_def)
1. (%(x, y). fst p = x) p
ペアのletは、ペアのラムダ抽象に変換されます。ペアの集合の内包表現についても同様です。
lemma "p : {(x, y). x = y} --> fst p = snd p"
apply simp
1. split op = p --> fst p = snd p
split (op =)は% (x, y). x = yの省略形です。次の例も同じ手続きで証明できます。
lemma "p : {(x, y). x = y} ==> fst p = snd p"
ただし、splitが前提に現れているので、split_split_asmを使用しなければなりません。
splitがいつも解であるとは限りません。次の関数を考えます。
primrec swap :: "'a * 'b => 'b * 'a" where "swap (x, y) = (y, x)"
次の定理を証明してみます。
lemma "swap (swap p) = p"
simpでは証明が進みません。まずpをペアの形に変換しなければなりませんが、使えるsplitルールもありません。そこで、手動で変換します。
apply(case_tac p)
1. !!a b. p = (a, b) ==> swap (swap p) = p
*はデータ型なので、case_tacを使えます。残ったサブゴールは単純化のみで証明できます。case_tacによる分解は上の他の例でも使用でき、またこちらの方が簡単だったかもしれません。
別の方法として、split_paired_allを使用してメタ全称限量子によって限量化された変数を変換することができます。
lemma "!! p q. swap (swap p) = q --> p = q" apply(simp only: split_paired_all)
1. !!a b aa ba. swap (swap (a, b)) = (aa, ba) --> (a, b) = (aa, ba)
apply simp done
上の例では先にsplit_paired_allのみを適用し、その後にsimpを適用し直しています。今回の例では
apply(simp add: split_paired_all)
の1ステップで証明することもできますが、split_paired_allは他の関数と干渉してうまくいかない場合もあり、そのときには例のように二つのステップに分けなければなりません。
最後に、全称限量子と存在限量子に限量化された変数は自動的に変換されます。
lemma "ALL p. EX q. swap p = swap q" by simp
変換は、次の定理によって行われます。
(ALL x. ?P x) = (ALL a b. ?P (a, b)) (split_paired_All) (EX x. ?P x) = (EX a b. ?P (a, b)) (split_paired_Ex)
8.2 Records
n個のフィールドを持つレコードは基本的にはn組のタプルです。しかし、レコードの各フィールドは名前を持っているため、よりわかりやすくなっています。また各フィールドは型も決まっています。
8.2.1 Record Basics
レコード型はIsabelleのプリミティブな型ではなく、プリミティブな組型を基に作られています。recordは新しいレコード型を定義します。例を見てみます。
record point = Xcoord :: int Ycoord :: int
pointは二つのフィールドXcoordとYcoordを持ち、それらはともにint型です。point型の定数を定義してみます。
definition pt1 :: point where "pt1 == (| Xcoord = 999, Ycoord = 23 |)"
レコード型は直接それぞれのフィールドを書いて表わすこともでき、型名はその略記です。
definition pt2 :: "(| Xcoord :: int, Ycoord :: int |)" where "pt2 == (| Xcoord = -45, Ycoord = 97 |)"
それぞれのフィールドに対して、選択関数が同じ名前で定義されます。例えば、pをpoint型の変数とすると、Xcoord pはpのフィールドXcoordの値を表わします。フィールド選択関数は自動的に単純化されます。
lemma "Xcoord (| Xcoord = a, Ycoord = b |) = a" by simp
値の更新も定義されます。例えば、p (| Xcoord := 0 |)はXcoordの値が0、Ycoordの値がpと同じレコードを表わします。これも自動的に単純化されます。
lemma "(| Xcoord = a, Ycoord = b |)(| Xcoord := 0 |) = (| Xcoord = 0, Ycoord = b |)" by simp
フィールド名は定数として宣言されるため、変数名には使えなくなります。よって、フィールド名に単なるxやyといった名前は付けない方がよいでしょう。
8.2.2 Extensible Records and Generic Operations
pointを拡張して、色付きのポイント型(cpoint)を定義することができます。
datatype colour = Red | Green | Blue record cpoint = point + col :: colour
この新しい型の要素はXcoord、Ycoord、colの三つです。
definition cpt1 :: cpoint where "cpt1 == (| Xcoord = 999, Ycoord = 23, col = Green |)"
レコード型は、拡張されたフィールドを保持するための暗黙のフィールドmore :: 'aを持ちます。レコードの値が定義されたフィールドのみで表わされている場合、moreの値は空のタプル() :: unitです。レコードブラケットの中では、moreフィールドは"..."で参照できます。
lemma "Xcoord (| Xcoord = a, Ycoord = b, ... = p |) = a" by simp
moreフィールドを直接操作することもできますが、その場合は型名で修飾する必要があります。
lemma "point.more cpt1 = (| col = Green |)" by (simp add: cpt1_def)
拡張されたcolour部分はそれ自身がレコード(| col = Green |)になっていることがわかります。
pointの定義には二つの形があります。
point = (|Xcoord :: int, Ycoord :: int|) 'a point_scheme = (|Xcoord :: int, Ycoord :: int, ... :: 'a|)
pointが二つのフィールドのみを表わしているの対し、総称型'a point_schemeはこの二つのフィールドを元に拡張した型を表わしています。unit point_schemeはpointと同じであり、(|col :: colour|) point_schemeはcpointと同じです。
次に、Xcoordの値をゲット、セットする総称関数を定義してみます。
definition getX :: "'a point_scheme => int" where "getX r == Xcoord r" definition setX :: "'a point_scheme => int => 'a point_scheme" where "setX r a == r(| Xcoord := a |)"
型が'a point_schemeなので、point型だけでなく、cpointなどのpointを拡張した型に対してもこのメソッドを使うことができます。さらにXcoordの値のみを1増やす関数を次のようにも定義できます。
definition incX :: "'a point_scheme => 'a point_scheme" where "incX r == (| Xcoord = Xcoord r + 1, Ycoord = Ycoord r, ... = point.more r |)"
次の例のように、総称関数に関する総称的な定理を証明できます。
lemma "incX r = setX r (getX r + 1)" by (simp add: getX_def setX_def incX_def)
8.2.3 Record Equality
二つのレコードが等しいとは、対応するフィールドの値がすべて等しいことをいいます。レコードの同値関係は自動的に単純化されます。
lemma "(| Xcoord = a, Ycoord = b |) = (| Xcoord = a', Ycoord = b' |) =
(a = a' & b = b')"
by simp
次の証明も似ていますが、この場合Isabelleはrを'a point_schemeの任意のインスタンスと判断します。
lemma "r(| Xcoord := a, Ycoord := b |) = r(| Ycoord := b, Xcoord := a |)" by simp
同値性の証明は多くの場合単純化で証明できますが、うまくいかない場合もあります。次の例を見てみます。
lemma "r(| Xcoord := a |) = r(| Xcoord := a' |) ==> a = a'"
レコードの同値性の除去規則は自動的に適用されないため、simpでは証明が進みません。証明を進める方法の一つは、Xcoordを前提の両辺に適用することです。
apply(drule_tac f = Xcoord in arg_cong)
1. Xcoord (r(| Xcoord := a |)) = Xcoord (r(| Xcoord := a' |)) ==> a = a'
残りは単純化で完了します。
メソッドcasesを使って証明を進めることもできます。casesは、レコード変数を外延的な表現に置き換えるための等式を前提に追加します。
lemma "r(| Xcoord := a |) = r(| Xcoord := a' |) ==> a = a'" apply(cases r)
1. !!Xcoord Ycoord more.
[| r(| Xcoord := a |) = r(| Xcoord := a' |);
r = (| Xcoord = Xcoord, Ycoord = Ycoord, ... = more |) |]
==> a = a'
こちらも残りは単純化で完了します。
8.2.4 Extending and Truncating Records
レコード型を定義すると、同時にいくつかの関数が暗黙に定義されます。
- makeは引数にそれぞれのフィールドの値を取り、レコード値を返します。
- fieldsはそのレコード独自の値を引数に取り、そのフィールドのみのレコード値を返します。
- extendは拡張元のレコード型の値と、追加されたフィールドの値を引数に取り、拡張されたレコード型の値を返します。
- truncateは拡張されたレコード型の値を引数に取り、拡張元のレコード型の値を返します。
これらはレコード型名.defsに定義されています。例えば、pointに対する関数定義は次のようになっています。
point.make ?Xcoord ?Ycoord == (| Xcoord = ?Xcoord, Ycoord = ?Ycoord |) point.fields ?Xcoord ?Ycoord == (| Xcoord = ?Xcoord, Ycoord = ?Ycoord |) point.extend ?r ?more == (| Xcoord = Xcoord ?r, Ycoord = Ycoord ?r, ... = ?more |) point.truncate ?r == (| Xcoord = Xcoord ?r, Ycoord = Ycoord ?r |)
cpointの場合は次のようになります。
cpoint.make ?Xcoord ?Ycoord ?col == (| Xcoord = ?Xcoord, Ycoord = ?Ycoord, col = ?col |) cpoint.fields ?col == (| col = ?col |) cpoint.extend ?r ?more == (| Xcoord = Xcoord ?r, Ycoord = Ycoord ?r, col = col ?r, ... = ?more |) cpoint.truncate ?r == (| Xcoord = Xcoord ?r, Ycoord = Ycoord ?r, col = col ?r |)
例として、定数pt1を拡張してcpoint型の定数を定義します。
definition cpt2 :: cpoint where "cpt2 == point.extend pt1 (cpoint.fields Green)"
cpt1とcpt2が等しいことを証明してみます。
lemma "cpt1 = cpt2" apply(simp add: cpt1_def cpt2_def point.defs cpoint.defs)
1. Xcoord pt1 = 999 & Ycoord pt1 = 23
pt1の定義が足りないため、サブゴールが残りました。もちろんこれは次のようにして証明できます。
apply(simp add: pt1_def) done
Exercise 8.2.1
cpointにnat型のフィールドintensityを追加し、操作してみます。
record icpoint = cpoint + intensity :: nat definition icpt1 :: icpoint where "icpt1 == cpoint.extend cpt1 (icpoint.fields 100)" lemma "pt1 = point.truncate (cpoint.truncate icpt1)" apply(simp add: pt1_def cpt1_def icpt1_def point.defs cpoint.defs) done
Exercise 8.2.2
Javaを知らないのでパスします。
