Hatena::ブログ(Diary)

caeruiro

2010-06-20

Isabelle Tutorial その27

ついに最終章です。

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を取り出せるのはボブのみなので、二つ目のメッセージによってアリスはボブが最初のメッセージを受け取り返信してきたことを確認できます。同様に、三つ目のメッセージによってボブはメッセージを送ったのがアリスであることを確認します。このプロトコルが、NaNbアリスとボブのみが共有することを保証すると思われていました。しかし、これが間違いであることを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は定数ServerFriend、そして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

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

二つの関数analzsynthがこの振る舞いを形式化します。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 HHに含まれるメッセージに含まれるすべての要素を表わします。定義はanalzに似ていますが、Cryptに対応する規則のみが異なります。

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

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


10.4 Event Traces

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

通信の中で、新たなノンスを生成しなければなりません。これを形式化するために、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ではなくevs1evs2を使用しているのは、証明中のサブゴールを見やすくするためであり、本質的ではありません。


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 AXで拡張したトレースに含まれるならば、(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'秘密鍵が漏れている場合です。サブゴールの中では変数名としてNBNAaBaが使われています。Nb ~= Na'を証明するのは簡単です。前提Nonce NAa ~: used evs1からNAaが新しいノンスであり、既に使われているNBと異なることが導けます。

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

残りの定理の証明はそれほど難しくはありません。次は真正性、すなわちBAにメッセージ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.

2010-06-06

Isabelle Tutorial その26

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 ... yntに含まれる自由変数であり、xは新たに導入した変数です。このように変形し、xに対して帰納法を適用することができます。

9.2.2 Beyond Structural and Recursion Induction

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

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

(!!n. ALL m<n. ?P 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_inductkに対して適用します。

apply(induct_tac k rule: nat_less_induct)
 1. !!n. ALL m<n. ALL i. m = f i --> 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<n. ALL i. m = f i --> 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が恒等関数であることを証明します。

続きを読む

2010-05-23

Isabelle Tutorial その25

9. Advanced Simplification and Induction

9.1 Simplification

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

9.1.1 Advanced Features

Congruence Rules.

P ==> QQを単純化するのに前提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 xh 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

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

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

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

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

2010-05-17

Isabelle Tutorial その24

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_threeRep_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)

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

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

今回の例では、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に変換していては大変です。そこでABそしてCのみで書かれたthreeに関する十分な定理を用意し、抽象レベルを上げる必要があります。簡単な例として、ABCがすべて異なり、かつそれが型の要素のすべてである事を証明します。

Isabelleは予めいくつかの役立つ補題を用意しています。最初の二つはRep_threeAbs_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::threeAbs_three(y::nat)に、またyRep_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)

ABCがすべて異なることの証明は、それぞれの定義を展開し、さらに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)

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

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はおおよそ上の例と同じようなことを内部で行います。

2010-05-16

Isabelle Tutorial その23

8.3 Type Classes

型クラスの概念はHaskellによって広まりました。型クラスは型とインタフェースの集合を定義し、そのクラスに属する型はインタフェースを実装しなければなりません。Isabelleが提供する型クラスも同様ですが、さらにプロパティ(型公理)を定めることができ、クラスに属する型はプロパティを満たさなければなりません。型tがクラスCに属することをt :: Cと書きます。また型クラスは継承することができ、DCサブクラスであることを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はローカルスコープを開きます。ここでは、plusnatインスタンス化します。まず、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)といった記述ができるようになりました。

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

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

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

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の型システムにも伝わり、groupmonoidサブクラスであることが型クラスの継承関係に追加されます。

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

定数01は全ての数値型に対して多重定義されています。他の値は数値リテラル、例えば2-3441223334678などで表わします。また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に関する多くの定理は理論NatDividesで用意されています。

Literals.

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

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')

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

Division.

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

?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ではnmより大きいならば、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

ratrealcomplexは理論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は型クラスを使用して数値に関する理論を体系付けています。いくつかの型クラスと定理を紹介します。

  • semiringordered_semiring: 半環は演算子+*、それらの結合律、さらにそれぞれの単位元となる01を与えます。演算子はまた一般的な分配則を満たし、さらに加算(+)は交換律を満たします。順序半環は半環を継承し、更に線形順序を与えます。natは順序半環に属します。
  • ringordered_ring: 環は半環を継承し、単項のマイナス(加法に対する逆元)と減算(-)を与えます。順序環には関数absが定義されています。intは順序環に属します。
  • fieldordered_field: 体は環を継承し、逆数を与えます。順序体は順序環を元にします。complexは体に、realは順序体に属します。
  • division_by_zeroinverse 0 = 0a / 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.

関数absintratrealを含むすべての順序環に定義されています。いくつかの定理を示します。

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を使用していますが、これまで通りの方法で証明していきます。