Isabelle Tutorial その27

Isabelle

ついに最終章です。

10. Case Study: Verifying a Security Protocol

最後の章は、セキュリティプロトコルをモデル化し、その正しさを証明します。Needham-Schroeder公開鍵プロトコルを例として、Isabelleを使ったプロトコルの検証方法を見ていきます。

10.1 The Needham-Schroeder Public-Key Protocol

このプロトコルは公開鍵暗号を使用します。アリスがボブにメッセージを送るにはボブの公開鍵で暗号化し、ボブの持っている秘密鍵のみがこの暗号文を正しく復号することができます。

Needham-Schroederプロトコルには三つの重要なメッセージがあります。

1. A \rightarrow B : \{|Na, A|\}_{Kb}
2. B \rightarrow A : \{|Na, Nb|\}_{Ka}
3. A \rightarrow B : \{|Nb|\}_{Kb}

最初のメッセージは、アリスが作成したノンス(Na)とアリスの名前(A)を、ボブの公開鍵(Kb)で暗号化したメッセージをアリスからボブへ送信することを意味します。二つ目はNaとボブが作成したノンス(Nb)をアリスの公開鍵(Ka)で暗号化したメッセージをボブからアリスへ送信することを意味します。最後はアリスからボブへ、Nbをボブの公開鍵で暗号化し送信することを意味します。

最初のメッセージを復号しNaを取り出せるのはボブのみなので、二つ目のメッセージによってアリスはボブが最初のメッセージを受け取り返信してきたことを確認できます。同様に、三つ目のメッセージによってボブはメッセージを送ったのがアリスであることを確認します。このプロトコルが、NaとNbをアリスとボブのみが共有することを保証すると思われていました。しかし、これが間違いであることをLoweが発見しました。もしアリスが他のエージェント(チャーリーとします)に対して通信を始めると、チャーリーはボブのふりをすることができます。

1. A \rightarrow C : \{|Na, A|\}_{Kc}
　　　　1'. C \rightarrow B : \{|Na, A|\}_{Kb}
2. B \rightarrow A : \{|Na, Nb|\}_{Ka}
3. A \rightarrow C : \{|Nb|\}_{Kc}
　　　　3'. C \rightarrow B : \{|Nb|\}_{Kb}

メッセージ1と3において、チャーリーはアリスからのメッセージを復号し、ボブの公開鍵で暗号化し直してからボブへ送信しています。これによってボブは通信相手がアリスであると思い込み、ノンスが漏れていることには気付きません。これが、マン・イン・ザ・ミドルと呼ばれる攻撃方法の典型的なパターンです。

Loweはまたこの問題に対する対策も提案しています。それは、メッセージ2にボブの名前を入れることです。

1. A \rightarrow B : \{|Na, A|\}_{Kb}
2. B \rightarrow A : \{|Na, Nb, B|\}_{Ka}
3. A \rightarrow B : \{|Nb|\}_{Kb}

もしチャーリーが同じように攻撃しても、アリスは\{|Na, Nb, C|\}_{Ka}を受け取るはずが\{|Na, Nb, B|\}_{Ka}を受け取ることになり、攻撃されていることに気付くことができます。以下では、このプロトコルの正しさを証明していきます。

Loweはこのような攻撃手段があることをモデル検査器を使用して見つけられることを示しました。以下で見るように、プロトコルの正しさを証明で確かめることもできます。無限の状態を扱うことができるため、証明の方がよりパワフルです。まずシステムの操作的意味を形式的に表し、その性質を帰納的に証明していきます。

10.2 Agents and Messages

データ型agentは定数Server、Friend、そしてSpyを定義します。Friendは複数いる可能性があるので、引数にnatを取ります。

datatype agent = Server | Friend nat | Spy

鍵は自然数で表わします。関数invKeyは公開鍵から秘密鍵へ、またはその逆へのマップ関数です。

types key = nat
consts invKey :: "key => key"

データ型msgはメッセージの形を定義します。メッセージはエージェント名、ノンス、鍵、及びそれらの暗号化と合成から成ります。

datatype msg = Agent agent |
               Nonce nat |
               Key key |
               MPair msg msg |
               Crypt key msg

{|X1, ..., Xn-1, Xn|}はMPair X1 ...(MPair Xn-1 Xn)の略記とします。

データ型の構成子は単射であることから、次の定理が得られます。

lemma "Crypt ka xa = Crypt kb xb ==> ka = kb & xa = xb"

暗号文を復号できる鍵は唯一であり、得られる平文も唯一です。現実には誤った鍵を使用して復号することもできますが、このモデルでは例えばチェックサムなどを使用して、間違った鍵による復号であることがわかると仮定します。

10.3 Modelling the Adversary

スパイもシステムの一部であり、モデルに含めなければなりません。スパイはネットワークを見張り、持っている鍵でメッセージを復号しようとします。そのために鍵とノンスを集め、新たなメッセージを作り、送信します。

二つの関数analzとsynthがこの振る舞いを形式化します。analz Hはスパイがメッセージの集合Hから得られる情報を表わします。

inductive_set
  analz :: "msg set => msg set"
  for H :: "msg set"
where
Inj [intro, simp]: "X : H ==> X : analz H" |
Fst:               "{|X, Y|} : analz H ==> X : analz H" |
Snd:               "{|X, Y|} : analz H ==> Y : analz H" |
Decrypt [dest]:    "[|Crypt K X : analz H; Key (invKey K) : analz H|] ==> X : analz H"

Decryptルールは、スパイが自分の持っている鍵のみで復号できることを示しています。規則帰納を用いて次の定理を証明することができます。

"G <= H ==> analz G <= analz H"　　　　(analz_mono)
"analz (analz H) = analz H"　　　　　　(analz_idem)

synth Hはメッセージの集合Hから作ることのできるメッセージの集合を表わします。よってスパイがHから偽造できるメッセージをsynth (analz H)で表わすことができます。

inductive_set
  synth :: "msg set => msg set"
  for H :: "msg set"
where
Inj [intro]:   "X : H ==> X : synth H" |
Agent [intro]: "Agent agent : synth H" |
MPair [intro]: "[|X : synth H; Y : synth H|] ==> {|X, Y|} : synth H" |
Crypt [intro]: "[|X : synth H; Key K : synth H|] ==> Crypt K X : synth H"

この集合にはすべてのエージェント名が含まれています。対して、鍵やノンスは推測できないと仮定しているので、Hに含まれていない限り使うことはできません。

analzと同様にsynthも単調性を持ち、冪等律を満たします。さらに、次の定理も満たします。

"analz (synth H) = analz H Un synth H"　　　　(analz_synth)

次の例のように規則の反転を使用することで、synthに関する証明がしやすくなります。

inductive_cases Nonce_synth [elim!]: "Nonce n : synth H"

三つ目の演算子partsは正当性を表わすのに便利です。parts HはHに含まれるメッセージに含まれるすべての要素を表わします。定義はanalzに似ていますが、Cryptに対応する規則のみが異なります。

Crypt K X : parts H ==> X : parts H

partsを使って例えば、信頼できるエージェントの秘密鍵はどのメッセージにも含まれないといった、プロトコルに関する整礎な性質を表わすことができます。

10.4 Event Traces

システムの振る舞いはイベントトレースの集合で形式化します。最も重要なイベントSays A B XはAからBへXを送信することを表わします。トレースは単にイベントの列です。他のイベントには、メッセージの受信や情報の記憶などがあります。

通信の中で、新たなノンスを生成しなければなりません。これを形式化するために、used evsはトレースevsに含まれるすべての要素の集合とします。この関数は帰納的に定義でき、例えばイベントSaysの場合は次のようになります。

used (Says A B X # evs) = parts {X} Un used evs

関数knowsはエージェントの知識を形式化します。多くの場合はスパイの持っている知識を考慮すればよく、knows Spy evsはトレースevsからスパイが得られる情報の集合を表わします。イベントSaysに対して、スパイは送信されたメッセージを記憶します。

knows Spy (Says A B X # evs) = insert X (Knows Spy evs)

次のように、関数を組み合わせて他のメッセージ集合を表わすことができます。

  • analz (knows Spy evs)はevsから復号によってスパイが得られるすべてのメッセージを表わします。
  • synth (analz (knows Spy evs))はスパイが生成できるすべてのメッセージを表わします。

関数pubKはエージェントからその公開鍵への関数です。関数priKはエージェントからその秘密鍵への関数です。

consts pubK :: "agent => key"
abbreviation priK :: "agent => key"
where "priK x == invKey (pubK x)"

集合badは秘密鍵をスパイに知られているエージェントの集合とします。

公開鍵に関する二つの公理、異なるエージェントが同じ公開鍵を持つことはない、そして秘密鍵が公開鍵とは異なることを定義します。

axioms
  inj_pubK:      "inj pubK"
  priK_neq_pubK: "priK A ~= pubK B"

10.5 Modelling the Protocol

Loweによって修正されたNeedham-Schroeder公開鍵プロトコルを形式化します。プロトコルのそれぞれのステップは帰納的に定義されます。イベントトレースはevent list型とし、イベントトレースの集合ns_pubicを次のように帰納的に定義します。

inductive_set ns_public :: "event list set" where
Nil:  "[] : ns_public" |
Fake: "[|evsf : ns_public; X : synth (analz (knows Spy evsf))|]
       ==> Says Spy B X # evsf : ns_public" |
NS1:  "[|evs1 : ns_public; Nonce NA ~: used evs1|]
       ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) # evs1 : ns_public" |
NS2:  "[|evs2 : ns_public; Nonce NB ~: used evs2;
         Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2|]
       ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) # evs2 : ns_public" |
NS3:  "[|evs3 : ns_public;
         Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
         Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) set evs3|]
       ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"

ルールNilは空列が含まれることを定義します。Fakeは過去のメッセージを元に偽造したメッセージをスパイが送信できることを定義しています。最後の三つのルールはプロトコルが定義する正しいステップを表わしています。NS2において送信者がAではなくA'となっているのは、受信者Bはそのメッセージの送信者が誰であるか知らないためです。また、変数に単なるevsではなくevs1やevs2を使用しているのは、証明中のサブゴールを見やすくするためであり、本質的ではありません。

10.6 Proving Elementary Properties

機密性に関する典型的な例はX ~: analz (knows Spy evs)、つまりXがスパイに知られてはいないというものです。この証明はanalzについて解かなければならないことから、かなり困難です。これと比べると、Xがまったく現れないことの証明は簡単になります。この場合は、analzの代わりにpartsを使用します。

次の補題は、Aの秘密鍵がスパイに漏れる可能性があるのは、Aが集合badに含まれているとき、かつその時に限るということを表わしています。ここでpartsが使われているのは、暗号化されているかどうかに関わらず、Aの秘密鍵がメッセージに含まれているかという点にのみ注目しているからです。証明はプロトコルに関する他の証明と同様、メッセージトレースに関する帰納法を使用します。

lemma Spy_see_priK [simp]:
  "evs : ns_public
   ==> (Key (priK A) : parts (knows Spy evs)) = (A : bad)"
apply(erule ns_public.induct, simp_all)

帰納法によって五つのサブゴールに別れます。正当なメッセージに暗号鍵が含まれていないことは明らかであり、問題となるのはFakeのみです。単純化の結果次のサブゴールのみが残ります。

 1. !!evsf X.
      [|evsf : ns_public;
        (Key (priK A) : parts (knows Spy evsf)) = (A : bad);
        X : synth (analz (knows Spy evsf))|]
      ==> (Key (priK A) : parts (insert X (knows Spy evsf))) =
          (A : bad)

by blast

もしpriK AがXで拡張したトレースに含まれるならば、(1)元のトレースに含まれていたか、(2)スパイによって生成されたメッセージに含まれていたかのどちらかであり、どちらの場合も前提から証明することが可能です。

単一性は特定の要素がトレースの中に一度だけ現れることを示します。次の補題は、スパイに知られない限り、ノンスの値は唯一であることを示しています。証明は帰納法、単純化、そしてblastのみで可能です。最初にrev_mpを使用するのは、メタ前提に含まれる二つの仮定を含意の前提に移動して帰納法を適用するためです。

lemma no_nonce_NS1_NS2:
  "[|Crypt (pubK C) {|NA', Nonce NA, Agent D|} : parts (knows Spy evs);
     Crypt (pubK B) {|Nonce NA, Agent A|} : parts (knows Spy evs);
     evs : ns_public|]
   ==> Nonce NA : analz (knows Spy evs)"
apply(erule rev_mp, erule rev_mp)
apply(erule ns_public.induct, simp_all)
apply(blast intro: analz_insertI)+
done

次の補題は、ノンスNAが漏れていないならば、NAを含むメッセージ1は唯一であることを表わしています。証明の手順は上と同様です。

lemma unique_NA:
  "[|Crypt (pubK B)  {|Nonce NA, Agent A |} : parts (knows Spy evs);
     Crypt (pubK B') {|Nonce NA, Agent A'|} : parts (knows Spy evs);
     Nonce NA ~: analz (knows Spy evs); evs : ns_public|]
   ==> A=A' & B=B'"

10.7 Proving Secrecy Theorems

元のプロトコルで問題となっていた、ボブに関する機密性の確認が特に重要となります。ボブとアリスの情報に漏洩がないならば、ボブがアリスへメッセージ2を送ってもボブのノンスがスパイに漏れることはないことを示します。

theorem Spy_not_see_NB [dest]:
  "[|Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) : set evs;
    A ~: bad; B ~: bad; evs : ns_public|]
   ==> Nonce NB ~: analz (knows Spy evs)"

適用できる形に変形してから帰納法を適用し、単純化します。

apply(erule rev_mp, erule ns_public.induct, simp_all)

メッセージ1に関するサブゴールのみを詳細に見てみます。

 1. !!evs1 NAa Ba.
       [|A ~: bad; B ~: bad; evs1 : ns_public;
         Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
         : set evs1 -->
         Nonce NB ~: analz (knows Spy evs1);
         Nonce NAa ~: used evs1|]
       ==> Ba : bad -->
           Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
           : set evs1 -->
           NB ~= NAa

単純化の中で次の場合分けルールが使われています。これは、復号のための鍵を持っているかどうかで場合分けします。

analz (insert (Crypt K X) H) =
(if Key (invKey K) : analz H
 then insert (Crypt K X) (analz (insert X H))
 else insert (Crypt K X) (analz H))　　　　　　　　　(analz_Crypt_if)

このサブゴールは、最後のメッセージが次のようだった場合を考えています。

1. A' \rightarrow B' : \{|Na', A'|\}_{Kb'}

このメッセージによってNbが漏れるのは、Nb = Na'かつB'の秘密鍵が漏れている場合です。サブゴールの中では変数名としてNB、NAa、Baが使われています。Nb ~= Na'を証明するのは簡単です。前提Nonce NAa ~: used evs1からNAaが新しいノンスであり、既に使われているNBと異なることが導けます。

エージェントは同時に複数のエージェントと通信しなければならず、その同時に進行する通信の狭間に攻撃されることがよくあります。これがモデル検査においては状態爆発の原因となり、証明においては複雑さの原因となります。特にメッセージ2は多くの場合分けが必要になります。しかし今回の証明では、補題no_nonce_NS1_NS2とメソッドblastによってすべてのサブゴールが証明できます。

残りの定理の証明はそれほど難しくはありません。次は真正性、すなわちBがAにメッセージ2を送信し、その返事が返ってきたならば、確かにAからの応答であることを証明します。

theorem B_trust_NS3:
 "[|Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) : set evs;
    Says A' B (Crypt (pubK B) (Nonce NB)) : set evs;
    A ~: bad; B ~: bad; evs : ns_public|]
  ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs"

これも帰納法によって証明できます。

同様の前提から、AがノンスNAを使ってメッセージ1を送信したことも証明できます。この定理では、結論は次のようになります。

Says A B (Crypt (pubK B) {|Nonce NA, agent A|}) : set evs

ノンスNAの機密性と、メッセージ2を送信したのが確かにBであることも同様に証明できます。

この章での説明は以上です。現実のプロトコルは上で見た例より長く複雑ですが、プロトコル検証の流れは理解できたと思います。更なる詳細は参考文献*1 *2を参照してください。また、証明の全容はIsabelleのインストールディレクトリのsrc/HOL/Authを参照してください。

*1:Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85–128, 1998.

*2:Lawrence C. Paulson. Inductive analysis of the Internet protocol TLS. ACM Transactions on Information and System Security, 2(3):332–351, August 1999.

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が恒等関数であることを証明します。

続きを読む

Isabelle Tutorial その25

Isabelle

9. Advanced Simplification and Induction

9.1 Simplification

この節では、単純化に関してこれまで述べてこなかった部分を補足します。

9.1.1 Advanced Features

Congruence Rules.

P ==> QのQを単純化するのに前提Pを利用できます。==>ならば当然のように思えますが、他の演算子の場合も同様に文脈上の事実が使われます。文脈から得られる事実を使用するための規則を合同規則と言います。例えば次の規則は-->の合同規則です。

[| ?P = ?P'; ?P' ==> ?Q = ?Q' |] ==> (?P --> ?Q) = (?P' --> ?Q')　　　　(imp_cong)

限量子の合同規則は束縛変数に関する文脈情報を与えます。

[| ?A = ?B; !!x. x : ?B ==> ?P x = ?Q x |]
==> (ALL x:?A. ?P x) = (ALL x:?B. ?Q x)　　　　(ball_cong)

条件式の合同規則はthen節とelse節の単純化するための規則を与えます。

[| ?b = ?c; ?c ==> ?x = ?u; ~ ?c ==> ?y = ?v |]
==> (if ?b then ?x else ?y) = (if ?c then ?u else ?v)　　　　(if_cong)

条件式には次の合同規則もあり、こちらが条件式のデフォルトの合同規則になっています。

[| ?b = ?c; ?c ==> ?x = ?u; ~ ?c ==> ?y = ?v |]
==> (if ?b then ?x else ?y) = (if ?c then ?u else ?v)　　　　(if_weak_cong)

最初の項のみが単純化され、残りはそのままです。

独自の規則を合同規則にしたり無効にしたりするには、次のようにします。

declare theorem_name [cong]
declare theorem_name [cong del]

Permutative Rewrite Rules.

等式の右辺と左辺の変数が同じならば、並び替え規則と言います。もっとも一般的な並び替え規則はx + y = y + xのような交換律です。このような規則は無限に適用を続ける事ができますが、単純化では順序付き書換えと呼ばれる方法でこれを回避します。順序付きとは、項に対するある辞書式順序が小さくなる場合にのみルールが適用されることを言います。例えばb + aからa + bへは変換されますが、a + bの方が辞書式順序で小さいため、逆向きには書き換えられません。

並び替え規則は交換・結合律を満たす関数に対して効果的です。そのような関数を定義する場合、次のことに気を付けると良いでしょう。

  1. 結合律は左から右へ、つまりf(f(x, y), z) = f(x, f(y, z))の向きにします。
  2. 結合律(A)と交換律(C)に加えて左交換律(LC)、f(x, f(y, z)) = f(y, f(x, z))も定義します。

A、C、そしてLCによって次の例のように項が辞書式に並べ替えられます。

f(f(b, c), a) \overset{\text{A}}{\rightarrow} f(b, f(c, a)) \overset{\text{C}}{\rightarrow} f(b, f(a, c)) \overset{\text{LC}}{\rightarrow} f(a, f(b, c))

9.1.2 How the Simplifier Works

単純化はボトムアップに、つまり内側の項から先に行われます。また条件付きの場合は、条件が単純化によって証明できた場合にのみ適用されます。以下では更に特別な場合の単純化の振る舞いを説明します。

Higher-Order Patterns.

単純化ルールの左辺は高階パターンであることが求められており、スキーム変数の出現位置が制限されます。高階パターンの項はβ正規形であり、スキーム変数は?f x1 ... xnという形で出現します。もしスキーム変数が基本型ならば、引数の数は0です。よって、例えば?a + ?b + ?c = ?a + (?b + ?c)のようにすべてのスキーム変数の型が基本型であるような書換規則は、この制限を満たします。

もし左辺が高階パターンでない場合、それでも直接マッチする場合は規則が適用されます。例えば(?f ?x : range ?f) = Trueによってg a : range gからTrueに書き換えられますが、g(h b) : range (% x. g(h x))は失敗します。?f ?xを取り除き?y = ?f ?x ==> (?y : range ?f) = Trueとすることで改善しますが、完全な解決策とはなりません。

一方、右辺には制限がありません。

The Preprocessor.

定理を単純化ルールとして宣言すると、一つの等式から複数の等式に自動的に変形されます。例えばf x = g x & h x = k xは二つの単純化ルールf x = g xとh x = k xに分割されます。一般的に、入力された定理は次のように変形されます。

~P  |->  P = False
P --> Q  |->  P ==> Q
P & Q  |->  P, Q
ALL x. P x  |->  P ?x
ALL x : A. P x  |->  ?x : A ==> P ?x
if P then Q else R  |->  P ==> Q, ~P ==> R

これらの変形が終わった後、等式ではない項PはP = Trueに変形されます。例えば式

(p --> t = u & ~r) & s

は次の三つの式に変形されます。

p ==> t = u, p ==> r = False, s = True

Isabelle Tutorial その24

Isabelle

8.5 Introducing New Types

多くの場合は定義済みの型boolや=>とそれらの組み合わせで事が足りますが、稀にこれらでは表わせない高度な型が必要になる場合があります。そのような場合に必要となる型の導入方法を紹介します。

8.5.1 Declaring New Types

typedeclは詳細を定義する事なく新たな型の名前を宣言します。これは6.6の例で既に見ました。

typedecl my_new_type

関係する型に型パラメータを導入することで、typedeclによる型宣言は除去する事ができます。どちらを使っても本質的な違いはなく、違いは読みやすさのみです。

宣言した型にプロパティを付けたい場合は、公理として宣言する事ができます。

axioms just_one: "EX x::my_new_type. ALL y. x = y"

しかし、この方法は矛盾する公理を宣言する可能性があるため推奨はしません。

8.5.2 Defining New Types

より汎用的で安全な型の定義するにはtypedefを使います。datatypeを始めとする、他の型の定義手段はすべてtypedefに基づいています。簡単に言うと、既にある型の要素の部分集合を値とする新たな型を定義する事ができます。

例として、三つの値を持つ型を定義してみます。要素は自然数の最初の三つの値を使って表わします。

typedef three = "{0::nat, 1, 2}"

HOLの型は非空でなければならないため、少なくとも一つはその要素がある事を保証しなければなりません。typedefはこの制限の証明を要求してきます。今回の例の場合、この制限を満たす事は自明です。

 1. EX x. x : {0, 1, 2}

apply(rule_tac x = 0 in exI)
by simp

この型定義によって新たな型threeが導入されます。さらにその値は、集合{0, 1, 2}と1対1の関係です。これを表わすために、次の定数が同時に定義されます。

three :: nat set
Rep_three :: three => nat
Abs_three :: nat => three

また定数threeも定義されます。

three == {0, 1, 2}　　　　(three_def)

最後に、typedefはRep_threeが全射であり、Abs_threeとRep_threeが逆関係になっていることを明示します。

Rep_three ?x : three　　　　　　　　　　　　　　　　(Rep_three)
Abs_three (Rep_three ?x) = ?x　　　　　　　　　　　 (Rep_three_inverse)
?y : three ==> Rep_three (Abs_three ?y) = ?y　　　　(Abs_three_inverse)

次のステップは、この新しい型に対する基本的な関数を定義する事です。どのような関数を用意するかは定義する型に因りますが、次のような戦略をとると良いでしょう。

  • 他のすべての関数を表わすのに十分、かつできるだけ少ない基本関数のみを定義せよ。
  • 二つのレベルを行き来するために、AbsとRepを使って表わした型を表現するための関数を定義せよ。

今回の例では、threeの三つの要素それぞれに名前を定義すれば十分です。

definition A :: three where "A == Abs_three 0"
definition B :: three where "B == Abs_three 1"
definition C :: three where "C == Abs_three 2"

型threeを毎回natに変換していては大変です。そこでA、BそしてCのみで書かれたthreeに関する十分な定理を用意し、抽象レベルを上げる必要があります。簡単な例として、A、B、Cがすべて異なり、かつそれが型の要素のすべてである事を証明します。

Isabelleは予めいくつかの役立つ補題を用意しています。最初の二つはRep_threeとAbs_threeが単射である事を表わしています。

(Rep_three ?x = Rep_three ?y) = (?x = ?y)　　　　　　　　　　　　　　　　　　　　 (Rep_three_inject)
[| ?x : three; ?y : three |] ==> (Abs_three ?x = Abs_three ?y) = (?x = ?y)　　　　(Abs_three_inject)

次の定理はx::threeをAbs_three(y::nat)に、またyをRep_three xに置き換えます。

[| ?y : three; !!x. ?y = Rep_three x ==> ?P |] ==> ?P　　　　 (Rep_three_cases)
(!!y. [| ?x = Abs_three y; y : three |] ==> ?P) ==> ?P　　　　(Abs_three_cases)
[| ?y : three; !!x. ?P (Rep_three x) |] ==> ?P ?y　　　　　　 (Rep_three_induct)
(!!y. y : three ==> ?P (Abs_three y)) ==> ?P ?x　　　　　　　 (Abs_three_induct)

A、B、Cがすべて異なることの証明は、それぞれの定義を展開し、さらにAbs_threeが単射である事を用いて証明できます。

lemma "A ~= B & B ~= A & A ~= C & C ~= A & B ~= C & C ~= B"
by(simp add: Abs_three_inject A_def B_def C_def three_def)

A、B、Cが型の要素のすべてである事は、場合分けルールとして表わすのが良いでしょう。

lemma three_cases: "[| P A; P B; P C |] ==> P x"

証明は帰納法を使用して進めます。

apply(induct_tac x)

 1. !!y. [| P A; P B; P C; y : three |] ==> P (Abs_three y)

three_defによってy = 0 | y = 1 | y = 2が導かれ、場合分けするとそれぞれのサブゴールは自明になります。

apply(auto simp add: three_def A_def B_def C_def)
done

ところで、今回の例は次の一行で代用できます。

datatype better_three = A | B | C

実際、datatypeはおおよそ上の例と同じようなことを内部で行います。

Isabelle Tutorial その23

Isabelle

8.3 Type Classes

型クラスの概念はHaskellによって広まりました。型クラスは型とインタフェースの集合を定義し、そのクラスに属する型はインタフェースを実装しなければなりません。Isabelleが提供する型クラスも同様ですが、さらにプロパティ(型公理)を定めることができ、クラスに属する型はプロパティを満たさなければなりません。型tがクラスCに属することをt :: Cと書きます。また型クラスは継承することができ、DがCのサブクラスであることをD < Cと書きます。

8.3.1 Overloading

型クラスによって関数のオーバーロードが可能になります。従って定数をそれぞれの型に対して多重定義できます。

Overloading.

型クラスを使い、任意の型に対する加算演算子[+]を導入してみます。

class plus =
  fixes plus :: "'a => 'a => 'a" (infixl "[+]" 70)

これは、新しいクラスplusと同時に、定数plusの構文を定義します。またplusはクラス演算子でもあります。plusに属する型はその型変数に対して"'a :: plus"を制約として持ち、これはクラスplusに属する型は"'a"をインスタンス化した結果でなければならないことを意味します。インスタンス化の例を見てみます。

instantiation nat :: plus
begin

コマンドinstantiationはローカルスコープを開きます。ここでは、plusをnatでインスタンス化します。まず、natに対する関数plusを定義しなければなりません。

primrec plus_nat :: "nat => nat => nat" where
"(0::nat) [+] n = n" |
"Suc m [+] n = Suc (m [+] n)"

デフォルトでは、型tに対するクラス演算子fのローカル名はf_tとします。次に、型natがクラスplusのプロパティを満たしていることを証明しなければなりません。クラスplusにはプロパティがないので、証明は".."と書くだけで終わります。

instance ..

最後に、endで閉じて終わります。

end

以上で、Suc (m [+] 2)といった記述ができるようになりました。

次に、plusをplusのペアでインスタンス化してみます。

instantiation * :: (plus, plus) plus
begin
fun plus_prod :: "'a * 'b => 'a * 'b => 'a * 'b" where
"(x, y) [+] (w, z) = (x [+] w, y [+] z)"
instance ..
end
8.3.2 Axioms

クラスにプロパティを付けると、そのクラスに属する型の制約となります。

Semigroups.

plusのサブクラスとしてsemigroupsを定めます。

class semigroup = plus +
  assumes assoc: "(x [+] y) [+] z = x [+] (y [+] z)"

semigroupに属する型は[+]について結合律を満たさなければなりません。このクラスプロパティを使って、semigroupに属する型に対する定理を導出することができます。*1

lemma assoc_left: "(x::'a::semigroup) [+] (y [+] z) = (x [+] y) [+] z"
by (rule assoc[THEN sym])

このように証明された定理は、このクラスに属する型に対して自由に使うことができます。

インスタンス化の時には、クラスプロパティを満たすことを証明しなければなりません。

instantiation nat :: semigroup
begin
instance

証明はメソッドintro_classesで始めます。

  apply(intro_classes)
  apply(induct_tac x)
  by simp_all
end

ペアについても同様に証明してみます。

instantiation * :: (semigroup, semigroup) semigroup
begin
instance
  apply(intro_classes)
  apply(case_tac x, case_tac y, case_tac z)
  by (simp add: assoc)
end

ペアを構成するそれぞれの型がassocを満たすことから、ペアもまたassocを満たすことを証明できます。

Monoids.

semigroupを拡張してサブクラスmonoidlを定義します。monoidlは定数neutralを持ち、これは[+]に対する左単位元です。

class monoidl = semigroup +
  fixes neutral :: "'a" ("O")
  assumes neutl: "O [+] x = x"

上と同じく、natでインスタンス化します。natの[+]に対する単位元は0です。

instantiation nat :: monoidl
begin
definition neutral_nat_def: "O = (0::nat)"
instance
  apply(intro_classes)
  apply(subst neutral_nat_def)
  by simp
end

ペアも同様にインスタンス化できます。

instantiation * :: (monoidl, monoidl) monoidl
begin
definition neutral_prod_def: "O = (O, O)"
instance
  apply(intro_classes)
  apply(case_tac x)
  by (simp add: neutral_prod_def neutl)
end

完全なモノイドをモデル化するには、neutralが右単位元である必要があります。

class monoid = monoidl +
  assumes neutr : "x [+] O = x"

nat及びペアでのインスタンス化は省略します。

Groups.

最後にクラスgroupを作成します。

class group = monoidl +
  fixes inv :: "'a => 'a" (":- _" [81] 80)
  assumes invl: ":- x [+] x = O"

さらに、次の補題も証明しておきます。

lemma left_cancel: "((x::'a::group) [+] y = x [+] z) = (y = z)"
apply(rule iffI)
apply(subgoal_tac "(:- x [+] x) [+] y = (:- x [+] x) [+] z")
apply(simp add: invl neutl)
apply(simp add: assoc)
apply(simp)
done

このように定義したクラスgroupはmonoidでもあります。これを、groupがmonoidのサブクラスであることを証明して導入します。

instance group < monoid
apply(intro_classes)
apply(subgoal_tac "(:- x [+] x) [+] O = (:- x [+] x)")
apply(simp add: assoc left_cancel)
apply(simp add: invl neutl)
done

この証明結果がIsabelleの型システムにも伝わり、groupがmonoidのサブクラスであることが型クラスの継承関係に追加されます。

Inconsistencies.

互いに矛盾するプロパティをクラスに付加することもできます。しかし、既に見たようにインスタンス化するためにはその型変数がプロパティを満たすことを証明する必要があり、矛盾するプロパティは証明できません。

Syntactic Classes and Predefined Overloading.

上の例では最初に構文クラスであるplusを定義しましたが、操作とプロパティを同時に定めるsemigroupから始めることもできました。一般的には操作とそのプロパティを同時に定義する方が良いでしょう。しかし操作の構文が汎用的な場合は、上の例のように構文とそのプロパティを別のクラスで定義することによって、構文を使い回すことができます。

逆に構文を持たず、プロパティのみを定義するクラスも考えられます。例えば理論Finite_Setで定義されているクラスfiniteがあります。このクラスは有限集合"finite (UNIV :: 'a::finite set)"を定義しています。

8.4 Numbers

これまでは数値型に自然数型のnatを使用してきましたが、HOLには整数型intもあります。intは帰納法が使えませんが、所謂減算が使えます。よって減算を含む複雑な計算を解くにはnatよりもintの方が有利です。更には、有理数型rat、実数型real、複素数型complexもあります。Isabelleにサブタイプはなく、よって型は全て異なります。多くの算術演算子は多重定義されており、代数的な性質は型クラスを使って体系化されています。

多くの算術式はメソッドarithで証明することができます。また、算術式に関する多くの定理も用意されています。以下ではそれらの定理の一部を見ていきます。

8.4.1 Numeric Literals

定数0と1は全ての数値型に対して多重定義されています。他の値は数値リテラル、例えば2、-3、441223334678などで表わします。またIsabelleは加算や減算、乗算、整数型の除算や剰余算などは実際に計算します。

算術演算子が多重定義されているため、式の型に注意する必要があります。例えば次の証明はうまくいきません。

lemma "2 * m = m + m"

型を見てみると、'aとなっていることがわかると思います。型が定まらないため、証明が失敗します。例えば2::intのように型を指定すると、もちろん証明できます。

数値リテラルはパターンとして使うことができません。例えば次のような定義はエラーが返ります。

function h where
"h 3 = 2" |
"h i = i"

これを定義したい場合は、例えば次のようにします。

"h i = (if i = 3 then 2 else i)"
8.4.2 The Type of Natural Numbers, nat

natはこれまでに何度も使ってきました。natに関する多くの定理は理論NatとDividesで用意されています。

Literals.

1はnatでは次のように定義されています。

1 = Suc 0　　　　(One_nat_def)

これは単純化ルールなので、simpを使用すると自動的に置き換えられます。特に大きな値はリテラルで書いた方が明らかに読みやすいですが、多くの定理はSuc nの形にのみ適用できます。

次の二つの定理も単純化ルールです。

2 + ?n = Suc (Suc ?n)　　　　(add_2_eq_Suc)
?n + 2 = Suc (Suc ?n)　　　　(add_2_eq_Suc')

証明の中で例えば100をSuc 99に変形するのは簡単ではありません。よって予め0とSucのみで表わした方が良いでしょう。

Division.

natに対してdivとmodも定義されており、次の定理があります。

?m mod ?n = (if ?m < ?n then ?m else (?m - ?n) mod ?n)　　　　(mod_if)
?a div ?b * ?b + ?a mod ?b = ?a　　　　　　　　　　　　　　　 (mod_div_equality)

さらにいくつかの定理を紹介します。

?a * ?b div ?c = ?a * (?b div ?c) + ?a * (?b mod ?c) div ?c　　　　(div_mult1_eq)
?a * ?b mod ?c = ?a * (?b mod ?c) mod ?c　　　　　　　　　　　　　 (mod_mult_right_eq)
?a div (?b * ?c) = ?a div ?b div ?c　　　　　　　　　　　　　　　　(div_mult2_eq)
?a mod (?b * ?c) = ?b * (?a div ?b mod ?c) + ?a mod ?b　　　　　　 (mod_mult2_eq)
?c ~= 0 ==> ?c * ?a div (?c * ?b) = ?a div ?b　　　　　　　　　　　(div_mult_mult1)
?m mod ?n * ?k = ?m * ?k mod (?n * ?k)　　　　　　　　　　　　　　 (mod_mult_distrib)
?m <= ?n ==> ?m div ?k <= ?n div ?k　　　　　　　　　　　　　　　　(div_le_mono)

いくつかの定理は除数が0以外という制限が付いています。natにおける0による除算の結果は0です。

?a div 0 = 0 　　　　(div_by_0)
?a mod 0 = ?a　　　　(mod_by_0)

整除関係は標準的な形で、すべての数値型に対して多重定義されています。

(?b dvd ?a) = (EX k. ?a = ?b * k)　　　　(dvd_def)

さらに整除性について次の定理もあります。

[| ?m dvd ?n; ?n dvd ?m |] ==> ?m = ?n　　　　　　　 (dvd_antisym)
[| ?a dvd ?b; ?a dvd ?c |] ==> ?a dvd ?b + ?c　　　　(dvd_add)

Subtraction.

natではnがmより大きいならば、m - nは0になります。次の定理はn <= mという条件なしに成り立ちます。

(?m - ?n) * ?k = ?m * ?k - ?n * ?k　　　　(diff_mult_distrib)

減算は次の場合分けルールで除去することができます。

?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d))　　　　(nat_diff_split)

例えばこの定理を次のように使用できます。

lemma "(n - 2) * (n + 2) = n * n - (4::nat)"
apply(simp split: nat_diff_split, clarify)

 1. !!d. [| n < 2; n * n = 4 + d |] ==> d = 0

n < 2から0か1のどちらかです。

apply(subgoal_tac "n = 0 | n = 1", force, arith)
done
8.4.3 The Type of Integers, int

帰納法はありませんが、intを含む証明はnatに似ており、多くの定理が用意されています。

絶対値を返す関数absは、intを始め負数を持つ全ての型に対して多重定義されています。absを含む式はメソッドarithで証明できます。

lemma "abs (x + y) <= abs x + abs (y::int)"
by arith

剰余の正負は除数に依存します。

0 < ?b ==> 0 <= ?a mod ?b　　　　(pos_mod_sign)
0 < ?b ==> ?a mod ?b < ?b　　　　(pos_mod_bound)
?b < 0 ==> ?a mod ?b <= 0　　　　(neg_mod_sign)
?b < 0 ==> ?b < ?a mod ?b　　　　(neg_mod_bound)

更に次の定理が用意されています。

(?a + ?b) div ?c = ?a div ?c + ?b div ?c + (?a mod ?c + ?b mod ?c) div ?c　　　　(zdiv_zadd1_eq)
(?a + ?b) mod ?c = (?a mod ?c + ?b mod ?c) mod ?c　　　　　　　　　　　　　　　　(mod_add_eq)
?a * ?b div ?c = ?a * (?b div ?c) + ?a * (?b mod ?c) div ?c　　　　　　　　　　　(zdiv_zmult1_eq)
?a * ?b mod ?c = ?a * (?b mod ?c) mod ?c　　　　　　　　　　　　　　　　　　　　 (zmod_zmult1_eq)
0 < ?c ==> ?a div (?b * ?c) = ?a div ?b div ?c　　　　　　　　　　　　　　　　　 (zdiv_zmult2_eq)
0 < ?c ==> ?a mod (?b * ?c) = ?b * (?a div ?b mod ?c) + ?a mod ?b　　　　　　　　(zmod_zmult2_eq)

最後の二つはnatの場合とは異なり、cが正数でなければなりません。また、定理名に現れるzは整数の集合を表わす記号\mathbb{Z}からきています。

もし値域に上限あるいは下限があるならば、整数に対しても帰納法が使えます。値域の範囲によって、次の四つの帰納ルールがあります。

[| ?k <= ?i; ?P ?k; !!i. [| ?k <= i; ?P i |] ==> ?P (i + 1) |] ==> ?P ?i　　　　　(int_ge_induct)
[| ?k < ?i; ?P (?k + 1); !!i. [| ?k < i; ?P i |] ==> ?P (i + 1) |] ==> ?P ?i　　　(int_gr_induct)
[| ?i <= ?k; ?P ?k; !!i. [| i <= ?k; ?P i |] ==> ?P (i - 1) |] ==> ?P ?i　　　　　(int_le_induct)
[| ?i < ?k; ?P (?k - 1); !!i. [| i < ?k; ?P i |] ==> ?P (i - 1) |] ==> ?P ?i　　　(int_less_induct)
8.4.4 The Types of Rational, Real and Complex Numbers

rat、real、complexは理論HOL-Complesに定義されており、これを使用するためにはMainではなくComplex_Mainをimportsする必要があります。

これらの型にはdivではなく、除算演算子/が定義されています。有理数と実数は稠密性を持っており、二つの異なる値の間には別の値が存在します。

?x < ?y ==> EX z>?x. z < ?y　　　　(dense)

また実数は完備性を持ちますが、有理数は持ちません。完備性の形式化は理論RCompleteに書かれています。

分数を/で表わすことができ、単純化で自動的に約分されます。

 1. P ((3 / 4) * (8 / 15))

apply simp

 1. P (2 / 5)

2 * 10^6のように指数表現で表わすこともでき、これも単純化で実数に変換されます。

8.4.5 The Numeric Type Classes

Isabelle/HOLは型クラスを使用して数値に関する理論を体系付けています。いくつかの型クラスと定理を紹介します。

  • semiringとordered_semiring: 半環は演算子+と*、それらの結合律、さらにそれぞれの単位元となる0と1を与えます。演算子はまた一般的な分配則を満たし、さらに加算(+)は交換律を満たします。順序半環は半環を継承し、更に線形順序を与えます。natは順序半環に属します。
  • ringとordered_ring: 環は半環を継承し、単項のマイナス(加法に対する逆元)と減算(-)を与えます。順序環には関数absが定義されています。intは順序環に属します。
  • fieldとordered_field: 体は環を継承し、逆数を与えます。順序体は順序環を元にします。complexは体に、realは順序体に属します。
  • division_by_zeroはinverse 0 = 0とa / 0 = 0を満たすすべての型を含みます。このクラスはIsabelleの標準的な数値型をすべて含みますが、体の基本的な定理はこの性質に依存することなく証明されています。

0除算を含まない環であるクラスring_no_zero_divisorsは吸収律を満たし、次の定理があります。

(?a * ?b = (0::?'a)) = (?a = (0::?'a) | ?b = (0::?'a))　　　　(mult_eq_0_iff)
(?a * ?c = ?b * ?c) = (?c = (0::?'a) | ?a = ?b)　　　　　　　 (mult_cancel_right)

ProofGeneralのメニュー Isabelle > Settings > Show Sorts で型クラスを表示することができます。定理mult_cancel_leftを型クラスを付けて示してみます。

((?c::?'a::ring_no_zero_divisors) * (?a::?'a::ring_no_zero_divisors) =
 ?c * (?b::?'a::ring_no_zero_divisors)) =
(?c = (0::?'a::ring_no_zero_divisors) | ?a = ?b)　　　　　　　　　　　　　　　(mult_cancel_left)

Simplifying with the AC-Laws.

加算に関する交換則と結合則を示します。

?a + ?b + ?c = ?a + (?b + ?c)　　　　　(add_assoc)
?a + ?b = ?b + ?a　　　　　　　　　　　(add_commute)
?a + (?b + ?c) = ?b + (?a + ?c)　　　　(add_left_commute)

add_acでこれらすべての定理を参照することができます。乗算に関しては同様にmult_acがあります。これらは半環で証明されており、よってすべての数値型がこの性質を持ちます。

Division Laws for Fields.

次に除算演算子に関するルールを見てみます。次の定理は、乗算と除算を使って表わされた有理式の単純化ルールです。

?a * (?b / ?c) = ?a * ?b / ?c　　　　(times_divide_eq_right)
?b / ?c * ?a = ?b * ?a / ?c　　　　　(times_divide_eq_left)
?a / (?b / ?c) = ?a * ?c / ?b　　　　(divide_divide_eq_right)
?a / ?b / ?c = ?a / (?b * ?c)　　　　(divide_divide_eq_left)

次の定理を使用し、符号を商から取り出すことができます。

- (?a / ?b) = - ?a / ?b　　　　(minus_divide_left)
- (?a / ?b) = ?a / - ?b　　　　(minus_divide_right)

分配則もありますが、これは単純化ルールではありません。

(?a + ?b) / ?c = ?a / ?c + ?b / ?c　　　　(add_divide_distrib)

Absolute Value.

関数absはint、rat、realを含むすべての順序環に定義されています。いくつかの定理を示します。

abs (?a * ?b) = abs ?a * abs ?b　　　　　　　　 (abs_mult)
(abs ?a <= ?b) = (?a <= ?b & - ?a <= ?b)　　　　(abs_le_iff)
abs (?a + ?b) <= abs ?a + abs ?b　　　　　　　　(abs_triangle_ineq)

Raising to a Power.

クラスordered_idomは環を元にし、さらに指数表現を原始帰納を使用して定義しています。理論Powerに含まれるいくつかの定理を示します。

?a ^ (?m + ?n) = ?a ^ ?m * ?a ^ ?n　　　　(power_add)
?a ^ (?m * ?n) = (?a ^ ?m) ^ ?n　　　　　 (power_mult)
abs (?a ^ ?n) = abs ?a ^ ?n　　　　　　　 (power_abs)

*1:チュートリアルの中ではこの節の証明をstructured Isar proofsを使用していますが、これまで通りの方法で証明していきます。

Isabelle Tutorial その22

Isabelle

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を追加し、操作してみます。

続きを読む

Isabelle Tutorial その21

Isabelle

7.4 Case Study: A Context Free Grammer

ここでは、HopcroftとUllmanによる文脈自由文法の例*1を取り上げます。生成規則は次のようになっており、これはaとbの数が同じ文字列を生成します。

S \rightarrow \epsilon | bA | aB
A \rightarrow aS | bAA
B \rightarrow bS | aBB

まず、アルファベットを定義します。

datatype alpha = a | b

便宜上、次の定理を証明しておきます。

lemma [simp]: "(x ~= a) = (x = b) & (x ~= b) = (x = a)"
by(case_tac x, auto)

生成規則は相互帰納で定義します。

inductive_set S :: "alpha list set" and
              A :: "alpha list set" and
              B :: "alpha list set"
where
"[] : S" |
"w : A ==> b#w : S" |
"w : B ==> a#w : S" |
"w : S ==> a#w : A" |
"[| v : A; w : A |] ==> b#v@w : A" |
"w : S ==> b#w : B" |
"[| v : B; w : B |] ==> a#v@w : B"

Sに含まれる文字列は、aとbの数が同じであることを証明します。相互帰納で定義しているので、Aに含まれる文字列はaの数がbよりも一つ多いこと、Bに含まれる文字列はbの数がaよりも一つ多いことを同時に証明します。

lemma correctness:
"(w : S --> size[x<-w. x=a] = size[x<-w. x=b]) &
 (w : A --> size[x<-w. x=a] = size[x<-w. x=b] + 1) &
 (w : B --> size[x<-w. x=b] = size[x<-w. x=a] + 1)"
by(rule S_A_B.induct, auto)

上の補題の中でリスト上の関数filterを使用しており、[x<-xs. P x]はfilter P xsと同じです。驚くかもしれませんが、証明はS_A_Bに関する規則帰納とautoだけで完了します。

健全性の証明は簡単ですが、完全性、aとbの数が同じ文字列は全てSに含まれていることの証明は複雑です。この証明には次の補題、aの数がbより二つ多い文字列は、aの数がbより一つ多い二つの文字列に分けることができるということを必要とします。これは、次のように考えます。すなわち、左端からaとbの数の差を数えていくと、最初は0、最後は2になり、その途中の1になる箇所で分けることができます。形式的には、次の定理を利用します。

[| ALL i<?n. abs (?f (i + 1) - ?f i) <= 1; ?f 0 <= ?k; ?k <= ?f ?n |]
==> EX i<=?n. ?f i = ?k　　　　　　　　　　　　　　　　　　　(nat0_intermed_int_val)

まず、左から右へ一つ動くごとに、aとbの数の差が一つずつ変わることを証明します。ただし、aとbに関する汎用的なプロパティPについての定理として証明します。

lemma step1: "ALL i < size w.
  abs((int(size[x<-take (i + 1) w. P x]) - int(size[x<-take (i + 1) w. ~P x]))
      - (int(size[x<-take i w. P x]) - int(size[x<-take i w. ~P x]))) <= 1"
apply(induct_tac w)
apply(auto simp add: abs_if take_Cons split: nat.split)
done

intは自然数から整数へ変換する関数であり、差を計算するために必要です。takeはリストに関する関数として定義されており、take i xsはxsの先頭から長さi分だけ取り出す関数です。またdrop i xsはxsの先頭から長さi分だけ取り出した残りを返す関数です。

先ほどの補題の証明に移ります。

lemma part1:
"size[x<-w. P x] = size[x<-w. ~P x] + 2 ==>
 EX i <= size w. size[x<-take i w. P x] = size[x<-take i w. ~P x] + 1"
apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "1"])
by force

part1はプレフィックスtake i wに関する補題ですので、サフィックスdrop i wに関しても証明します。

lemma part2:
"[| size[x<-take i w @ drop i w. P x] =
    size[x<-take i w @ drop i w. ~P x] + 2;
    size[x<-take i w. P x] = size[x<-take i w. ~P x] + 1|]
 ==> size[x<-drop i w. P x] = size[x<-drop i w. ~P x] + 1"
by(simp del: append_take_drop_id)

append_take_drop_idは次のような定理です。

take ?n ?xs @ drop ?n ?xs = ?xs　　　　(append_take_drop_id)

これを使用すると証明がうまくいかないので、無効にしています。代わりに次の定理が使われ、証明がうまくいきます。

filter ?P (?xs @ ?ys) = filter ?P ?xs @ filter ?P ?ys　　　　(filter_append)

以降の証明では、明らかな場合を自動的に証明させるため、次のルールを単純化規則として宣言しておきます。

declare S_A_B.intros[simp]

完全性の証明は手順のみを示し、詳細は省略します。

theorem completeness:
"(size[x<-w. x=a] = size[x<-w. x=b] --> w : S) &
 (size[x<-w. x=a] = size[x<-w. x=b] + 1 --> w : A) &
 (size[x<-w. x=b] = size[x<-w. x=a] + 1 --> w : B)"
apply(induct_tac w rule: length_induct)
apply(rename_tac w)
apply(case_tac w)
apply(simp_all)
apply(rename_tac v)
apply(rule conjI)
apply(clarify)
apply(frule part1[of "% x. x=a", simplified])
apply(clarify)
apply(drule part2[of "% x. x=a", simplified])
apply(assumption)
apply(rule_tac n1 = i and t = v in subst[OF append_take_drop_id])
apply(rule S_A_B.intros)
apply(force simp add: min_less_iff_disj)
apply(force split add: nat_diff_split)
apply(clarify)
apply(frule part1[of "% x. x=b", simplified])
apply(clarify)
apply(drule part2[of "% x. x=b", simplified])
apply(assumption)
apply(rule_tac n1 = i and t = v in subst[OF append_take_drop_id])
apply(rule S_A_B.intros)
apply(force simp add: min_less_iff_disj)
apply(force split add: nat_diff_split)
done

*1:John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.