「型の理論」と証明支援システム -- COQの世界

33 %
67 %
Information about 「型の理論」と証明支援システム -- COQの世界
Technology

Published on March 6, 2014

Author: maruyama097

Source: slideshare.net

「型の理論」と証明支援システ ム -- Coqの世界 @maruyama097 丸山不二夫

Agenda     はじめに Part I : 「型の理論」をふりかえる Part II : Curry-Howard対応について Part III: Coq入門

はじめに  現在、HoTT(Homotopy Type Theory)と呼 ばれる新しい型の理論とそれを基礎付ける Univalent Theoryと呼ばれる新しい数学理論 が、熱い関心を集めている。  Univalent Theoryは、数学者のVladimir Voevodskyが、論理学者Per Martin-Löfの型 の理論を「再発見」したことに始まる。  この新しい分野は、21世紀の数学とコンピュ ータサイエンスの双方に、大きな影響を与え ていくだろう。

はじめに  「証明支援システム」は、人間の証明をコン ピュータが支援するシステムである。ただ見 方を変えれば、それは、コンピュータの証明 を人間が支援しているシステムだと考えるこ とも出来る。  コンピュータの進化が進んでいる方向の先に は知性を持つ機械の実現があると筆者は考え ている。「証明支援システム」での人間と機 械の、証明をめぐる双対的な「共生」は、そ れに至る一つの段階なのだと思う。

はじめに  小論は、HoTTを直接の対象とはしていない。 HoTTにいたる型の理論のオーバービューを与 え、Martin-Löfの型の理論に基づいた証明支 援システムCoqの初等的な紹介を行うことを 目的にしている。  おりしも、Coqは、今年2013年に、ACMの SIGPLANのProgramming Languages Software Awardを授賞した。  型の理論と証明支援システムに対する関心が 広がることを期待したい。

Part I 「型の理論」をふりかえる

Part I 「型の理論」をふりかえる  型の理論 ~1910 Russell 集合論の逆理と型の理論  計算可能性の原理 〜1930 Church 型のないラムダ計算  型を持つラムダ計算 Church 1940年  型付きラムダ計算と論理との対応 Curry-Howard  Dependent Type Theory Martin-Löf 1970~  Homotopy Type Theory Voevodsky

型の理論 ~1910 Russell 集合論の逆理と型の理論 型の理論の歴史は古い。それは、Russell による集合論のパラドックスの発見に端を 発する100年以上前の理論にさかのぼる。

Fregeの公理  Cantorの集合概念 「集合とは、我々の直観あるいは思考の明確 で異なった対象を一つの全体にした集まりで ある。 その対象は、集合の要素と呼ばれる。」  Fregeの定式化(Comprehension Axiom) ある述語ΦについてΦ(x)が成り立つ全ての要 素xを集めた集合yが存在する。

Russellの逆理  先のΦ(x)に、~(x∈x)を取ろう。 このΦによって定義される集合をRとすれば、 R={ x | ~(x∈x) } Rは、自分自身を要素として含まない全ての 要素からなる集合になる。  R∈Rだろうか? この時、Rは自分自身を要 素に含んでいるので、Rの要素ではない。だ から、R∈Rならば~(R∈R)となって矛盾する 。  それでは、~(R∈R)だろうか? この時、Rの 定義から、このRはRの要素でなければならな

Russellの矛盾の分析  Russellは、定義されるべきクラス自身を含ん だ、 全てのクラスからなるクラスを考える自己参 照的な定義、非述語的な定義(impredicative definition)が問題の原因だと考えた。  「全体は、その全体という言葉によってのみ 定義される要素を含んではいけない。ある全 体の全ての要素という言葉によってのみ定義 されうるものは、その全体の要素にはなり得 ない。」  Russellは、対象と述語に型(degreeとorder

Russellの型の理論  全ての個体は型 i を持つ。  述語 P(x1,x2,...xn)は、x1,x2,...xn がそれぞ れ持つ型 i1,i2,...inに応じて、型 (i1,i2,...in) を持つ。  ある型を持つ述語Pは、この型の階層構造の中 で、その型以下の型を持つ個体に対してのみ 適用出来る。  「全て」を表す全称記号は、その型以下の型 を持つ個体の上を走る。

集合論の逆理に対する もうひとつのアプローチ  Russellの型の理論とは、別のスタイルでの集 合論の逆理に対する対応が、Zermelo– Fraenkelの公理的集合論(ZF)では、行われ ている。  ZFでは、FregeのComprehension Axiomに かえて、次の公理が採用されている。

集合論の逆理の発見の波紋 数学・論理学の基礎に対する反省  集合論での逆理の発見は、Russellの型の理論 の導入、ZFによる集合論の公理化の動きとと もに、数学・論理学の基礎に対する反省を活 発なものにした。  疑われたのは次のような推論の正当性である 。~∀x~P(x) ==> ∃xP(x) 「ある述語Pが成り立たないと全てのxについ て言うことが否定できるなら、Pを満たすある xが存在する。」 ここでは、あるものの存在 が、存在しないと仮定すると矛盾することを 示すことで証明されている。

直観主義・構成主義の登場  こうした間接的な存在証明に疑いを持ち、こ うしたものを論理から排除しようという動き が20世紀の初頭から生まれてくる。それが、 直観主義・構成主義と呼ばれるものである。  この立場では、P(x)を満たすあるxの存在は 、P(a)が成り立つあるaを示すことで、始め て与えられることになる。  この立場は、その後の数学・論理学に深い影 響を与えた。現代のコンピュータ・サイエン スの基礎となっている型の理論も、後述する ように、この立場に立っている。

計算可能性の原理 〜1930年代 Church 型のないラムダ計算 「計算可能性」については、1930年代に Gödel, Turing, Church, Postらによる多 くの成果が集中している。Churchのラム ダ計算の理論は、TuringのTuringマシン とともに、現代のコンピュータの基礎理論 に大きな影響を与えた。

Church–Turing thesis  “一般帰納関数は、実効的に計算可能である” というこの経験的な事実は、Churchを次のよ うなテーゼの記述に導いた。 同じテーゼは、チューリングの計算機械の記 述のうちにも、暗黙のうちに含まれている。  “THESIS I. 全ての実効的に計算可能な関数 (実効的に決定可能な述語)は、一般帰納関 数である。 1943年 Kleene “Recursive Predicates and Quantifiers”

関数の表記としてのλ記法  t = x2+y としよう。このtを、 xの関数としてみることを λx.t で表し、 yの関数としてみることを λy.t で表わそう。  これは、普通の関数で考えると、 λx.t は、 f(x)=x2+y λy.t は、 g(y)=x2+y と表記することに相当する。  t = x2+y は、また、xとyの二つの変数の関 数とみることが出来る。これを λxy.t と表そ う。 λxy.t は、 h(x, y)=x2+y

抽象化としてのλ表記  λ記法を使うことによって、上記の f, g, h のよ うな関数の具体的な名前を使わなくても、関数 のある特徴を抽象的に示すことが出来る。 これをλによる抽象化と呼ぶ。  λによる抽象化の例      λx.(x2 + ax +b) :xの関数としてみた x2 + ax +b λa.(x2 + ax +b) :aの関数としてみた x2 + ax +b λb.(x2 + ax +b) :bの関数としてみた x2 + ax +b λxa.(x2 + ax +b) :xとaの関数としてみた x2 + ax +b λxab.(x2 + ax +b) :xとaとbの関数としてみた x2 + ax +b

関数の値の計算  関数の値の計算をλ表記で考えよう。  t = x2+y を xの関数とみた時、x=2の時のtの値は 4+y yの関数とみた時、y=1の時のtの値は x2+1 x,yの関数とみた時、x=2, y=1の時の値は、5  λで抽象化されたλx.t, λy.tが、例えば、x=2, y=1の時にとる値は、それぞれ、4+y, x2+1と いった関数を値として返す関数であることに注 意しよう。  λxy.tの時、二つの変数 x, yに値を与えると、 この関数は、はじめて具体的な値をとる。

λ式での値の適用  λ式 tに、ある値 sを適用することを、λ式 tの後 ろに、値 sを並べて、t sのように表す。  例えば、次のようになる。 λx.t 2 = λx.(x2+y) 2 = 22+y = 4+y λy.t 1 = λy.(x2+y) 1 = x2+1 λxy.t 2 1 = λxy.(x2+y) 2 1 = 22+1 = 5

変数への値の代入  関数 f(x) が、x = aの時にとる値は、f(x)の 中に現れる x に、x = aの値を代入すること で得ることが出来る。これは、通常、f(a)と 表わされる。  名前のないλ式 tでの変数 xへの値aの代入に よる関数の値の計算を、次のように表現する 。 t [x:=a]  もっとも単純なλ式である、x自体が変数であ る時、代入は次のようになる。 x [x:=a] = a

適用と代入  もう尐し、適用と代入の関係を見ておこう。  λ式 λx.tへの、aの適用 (λx.t) aとは、代入 t[x:= a]を計算することである。 (λx.t) a = t[x:=a]  先の例での値の適用の直観的な説明は、代入 を用いると、次のように考えることが出来る 。 λx.t 2 = λx.(x2+y) 2 = (x2+y) [x:=2] = 22+y = 4+y λy.t 1 = λy.(x2+y) 1 = (x2+y)[y:=1]=x2+1

λ式の形式的定義  これまでは関数とその引数、引数に具体的な 値が与えられた時の関数の値をベースに、λ式 とその値の計算を説明してきたが、ここでは 、λ式の形式的な定義を与えよう。(正確なも のではなく、簡略化したものであることに留 意) 1. 変数x,...はλ式である。 2. tがλ式で、xが変数であるなら、λxによる抽 象化λx.t はλ式である。(abstraction) 3. t, sがλ式であるなら、tへのsの適用 t s は、 λ式である。(application)

λ計算の形式的定義  次の三つのルールを利用して、λ式を(基本的に は単純なものに)変換することをλ計算という。 1. α-conversion: 抽象化に用いる変数の名前は、自由に変更出来 る。例えば、 λx.(x2+1) => λy.(y2+1) => λz.(z2+1) 2. β-reduction: 代入による計算ルール (λx.t) a => t[x:=a] 3. η-conversion: λx.(f x) => f xで抽象化されたf(x)は、fに等しいということ

β-reductionと代入ルール  実際のλ計算で、大きな役割を果たすのはβreductionである。その元になっている代入 ルールを尐し詳しく見ておこう。 1. x[x := N] ≡N 2. y[x := N] ≡ y, if x ≠ y 3. (M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N]) 4. (λx.M)[x := N] ≡ λx.M 5. (λy.M)[x := N] ≡ λy.(M[x := N]), if x ≠ y, provided y ∉ FV(N)

ちょっと変わったλ式 1  λ式 Ω := (λx.xx) (λx.xx) を考えよう。 これを計算してみる。 (λx.xx) (λx.xx) = (λx.xx) (λy.yy) = xx[x:=λy.yy] = (λy.yy) (λy.yy) = (λx.xx) (λx.xx) となって、同じλ式が現れ、計算が終わらない 。

ちょっと変わったλ式 2  Y := λg.(λx.g (x x)) (λx.g (x x))とする。 このとき、Y gを計算してみよう。 Yg = λg.(λx.g (x x)) (λx.g (x x)) g = λf.(λx.f (x x)) (λx.f (x x)) g = (λx.g (x x)) (λx.g (x x)) = (λy.g (y y)) (λx.g (x x)) = g (y y)[y:=(λx.g (x x))] = g ((λx.g (x x)) (λx.g (x x))) =g(Yg) すなわち、Y g = g ( Y g )となって、Y gは 、gの不動点を与える。

型を持つラムダ計算 Church 1940年 現在のML, Haskellといった関数型言語は 、 このChurchの型を持つラムダ計算に基礎 をおいている。

ラムダ計算への型の導入  型σから型τへの関数は、型 σ → τ を持つ。  あるλ式 eが型τを持つことを、e : τ と表す。  α, β, ηの変換ルールは同じものとする この表記の下で、λ式の型の定義を次のように行 う。 1. 単純な変数 vi は型を持つ。 vi : τ 2. e1 : ( σ → τ )で、e2 : σ なら、 (e1 e2) : τ 3. x : σ で e : τ なら、(λxσ.e) : ( σ → τ )

型のないラムダ計算と 単純な型を持つラムダ計算の違い  先に見た型のないλ計算で成り立つ性質の大部 分は、型を持つλ計算でも成り立つ。  ただ、両者のあいだには違いもある。 型のないλ計算では、任意のλ式に対して任意 のλ式の適用を許していたが、型を持つλ計算 では、λ式の適用に型による制限が入っている 。  型を持つラムダ計算では、xσxσという適用は許 されない。許されるのは、xσ→τ xσという型を 持つλ式どうしの適用のみである。先の Ω := (λx.xx) (λx.xx) は、型を持つラムダ計算では

単純な型を持つラムダ計算の特徴  単純な型を持つラムダ計算は、こうした点で は、型を持たないラムダ計算より表現力が弱 いにもかかわらず、次のような重要な特徴を 持つ。  単純な型を持つラムダ計算では、変換による 計算は、必ず停止する。

型を持つラムダ計算での計算  あるオブジェクト aがある型 Aを持つとい う判断を、 a : A と表わそう。  型を持つラムダ計算の理論では、計算は、 次の形をしている。  関数 λx:A.b[x] を、型Aに属するオブジ ェクトaを適用して b[a]を得る。  計算の下で、全てのオブジェクトはユニー クな値を持つ。また、計算で等しいオブジ ェクトは、同一の値を持つ。

型を持つラムダ計算での 正規のオブジェクトとその値  ある型に属するオブジェクトは、型の計算 ルールによって、値が求まるなら、正規オ ブジェクトと呼ばれる。  例えば、1 + 1 は、自然数の型に属するが 正規ではない。2 は、正規のオブジェクト である。  ある型 A の正規オブジェクト v は、それ 以上計算ルールの適用がが出来ず、それ自 身を値として持つ。 この時、 v : A と書 く。

型、オブジェクト、値 オブジェクト a:A 計算 型 v:A 値 正規オブジェクト

Curry-Howard 型付きラムダ計算と論理との対 応 ラムダ計算に対する関心が、ふたたび活発 化するのは、20年近くたった1960年代か らだと思う。理由ははっきりしている。コ ンピュータが現実に動き出したからである 。この時期の代表的な成果は、Howardの Curry-Howard対応の研究である。

Curryの発見  既に1934年に、Curryは、型付を持つラムダ 計算と直観主義論理とのあいだに、対応関係 があることを発見していたという。  ここでは、型を持つラムダ計算の型に登場す る矢印 -> が、論理式で、「A ならば B」の 含意を意味する “A -> B” の中に出てくる矢 印 -> との間に、対応関係があることが大き な役割を果たす。 Curry, Haskell (1934), "Functionality in Combinatory Logic” http://www.ncbi.nlm.nih.gov/pmc/articles/PMC1076489/pdf/ pnas01751-0022.pdf

Howardによる発展  Howardは、このCurryの発見を、さらに 深く考えた。  1969年の彼の論文のタイトルが示すよう に、 論理式は型付きラムダ計算の型と見なすこ とが出来るのである。ただし、彼のこの論 文が公開されたのは、1980年になってか らのことらしい。 Howard,Williams (1980) "The formulae-as-types notion of construction” http://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf

“Propositions as Types” “Proofs as Terms”  Howardの洞察は、”Propositions as Types”, “Proofs as Terms” (これを、PAT というらしい)として、次にみるMartin-Löf の型の理論に大きな影響を与えた。  同時に、Curry-Howard対応は、型付きラム ダ計算をプログラムと見なせば、”Proof as Program”としても解釈出来る。  こうした観点は、今日のCoq等の証明支援言 語の理論的基礎になっている。

Dependent Type Theory Martin-Löf 1970年~ 現在の「型の理論」の基本が出来上がるの は、1980年代になってからである。その 中心人物は、Martin-Löfである。 現在のCoq, Agdaという証明支援システム は、彼のDependent Typeの理論に基礎 付けられている。

型の命題への拡張  Churchの単純な型を持つラムダ計算の体系は 、 基本的には、型A, 型Bに対して、型 A → Bで 表現される関数型の型しか持たない。  それに対して、Martin-Löfは、論理的な命題 にも、自然なスタイルで型を定義した。例え ば、Aが型であり、Bが型であれば、A∧Bも A→BもA∨Bも型であるというように。もちろ ん、それぞれは異なる型である。詳しくは後 述する。  ある aが型Aを持つ時、a : A で表す。

同一性への型の付与  Martin-Löf は、式 a = b にも型を与える。 a =A b : Id(A a b) 型 Id(A a b) を持つ式は、a と b は等しいと いう意味を持つ。  a =A b のAは、型Aの中での同一性であるこ とを表している。すなわち、a : A で b : Aで 、かつa = bの時にはじめて、a =A b は型 Id(A a b) を持つ。  ここでは式の同一性について述べたが、式の 同一性と型の同一性は、異なるものである。

型の理論の記述  Martin-Löfの型の理論は、次のことを示す、 四つの形式で記述される。 1. ある対象aが、型であること α : Type 2. ある表現式 aが、型 αの要素であること a:α 3. 二つの表現式が、同じ型の内部で、等しいこ と a=b:α 4. 二つの型が、等しいこと α = β : Type

Dependent Type  これまで、A∧B, A → B, A∨B といった、元 になる型 A, B を指定すると新しい型が決ま るといったスタイルで型を導入してきた。  これとは異なる次のようなスタイル、型Aそ のものではなく型Aに属する要素 a : Aに応じ て新しい型 B(a)が変化するような型の導入が 可能である。  例えば、実数R上のn次元のベクトル Vec(R,n)とn+1次元のベクトルVec(R,n+1) は、別の型を持つのだが、これは nに応じて 型が変わると考えることが出来る。

Dependent Type  こうした型をDependent Typeと呼び、次の ように表す。 Π(x:A).B(x)  Dependent Typeは、ある型Aの値aにディペ ンドして変化する型である。  先の例のベクトルの型は、次のように表され る。 Π(x:N).Vec(R,n) これは、全てのnについてVec(R,n)を考える ことに対応している。  型の理論では、全称記号は、Dependent

Dependent Typeと Polymorphism  Dependent Typeの例を、もう一つあげよう 。 n次元のベクトルは、自然数 N、整数 Z、実 数 R、複素数 C上でも定義出来る。 { N, Z, R, C } : T とする時、次のように定 義されるDependent Typeを考えよう。 Π( x : T)Vec(x,n)  これは、次元nは同じだが、定義された領域が 異なる別の型 Vec(N,n),Vec(Z,n),Vec(R,n), Vec(C,n)を 考えることに相当する。

Inductive Type  型の理論では、基本的な定数と関数から、新 しい型を帰納的に定義することが出来る。こ うした型をInductive Type(帰納的型)と呼 ぶ。  次は、そうした帰納的な定義の例である。 ここでは、自然数の型natが、ゼロを意味する 定数Oとsuccesser関数を表す関数Sで、帰納 的に定義されている。 Inductive nat : Type := | 0 : nat | S : nat -> nat.

関数型言語の基礎としての 型の理論  Martin-Löfの型の理論は、型を持つラムダ計 算の拡張として、ML, Haskell等の現在の関 数型言語に理論的基礎を与えた。  同時に、それは、Curry-Howard対応によっ て、Coq, Agda等の証明システムの理論的な 基礎をも与えることになった。

Homotopy Type Theory Voevodsky 現在進行中

新しい型の理論 HoTT  Homotopy Type Theory (HoTT) は、数学 者Voevodsky が中心となって構築した、新 しい型の理論である。  HoTTは、数学の一分野であるホモトピー論や ホモロジー代数と、論理学・計算機科学の一 分野である型の理論とのあいだに、深い結び つきがあるという発見に端を発している。  ここで取り上げられている型の理論は、 Martin-LöfのDependent Type Theoryであ る。

HoTTでの a : A の解釈  論理=数学的には、 a : A には、様々な解釈がある 。ここでは、他の解釈と比較して、HoTTでの a : A の解釈を見てみよう。 1. 集合論: Russellの立場 Aは集合であり、aはその要素である。 2. 構成主義: Kolmogorovの立場 Aは問題であり、aはその解決である 3. PAT: Curry & Howardの立場 Aは命題であり、aはその証明である。 4. HoTT: Voevodskyの立場 Aは空間であり、aはその点である。

HoTTでの同一性の解釈 空間Aの中で、 点aと点bをつな ぐ道がある時、 aとbは、同じも のと見なす。 道自体は、連続 的に変化しうる。 その同一性は、 homotopyが 与える

HoTTでのDependent Typeの解釈 (Ex)x∈B Bの値で、 パラメータ ー化されたE

Univalent TheoryとCoq  Voevodskyは、HoTTを武器に、Univalent Theoryという数学の新しい基礎付け・再構成 を始めている。興味深いのは、彼が、こうし た理論展開を、数学論文ではなく、Coqのプ ログラムの形でGitHubで公開していることで ある。 https://github.com/vladimirias/Foundati ons/  次の論文は、型の理論やHoTTにあまりなじみ のない一般の数学者向けの、Voevodskyの理 論 Coqライブラリーの解説である。

Part II “Proposition as Type” “Proof as Term” Curry-Howard 対応について

Part II “Proposition as Type”  Curry-Howard対応について  論理式の意味を考える  証明について考える  Propositions as Types and Proofs as Terms (PAT)  命題とその証明のルール  型とその要素のルール  QuantifierとEquality

Curry-Howard対応について

Curry-Howard対応について  Curry-Howard対応は、「型の理論」の最も 重要な発見の一つである。  Curry-Howard対応は、論理と型の理論との 間の、驚くべき対応関係を明らかにした。 すなわち、論理における命題は、型の理論の 型に対応し、論理における証明は、型の理論 でのある型の要素に対応する。  Curry-Howard対応は、“Proposition as Type” “Proof as Term” の頭文字をとって 、PATと呼ばれることがある。

型と命題、証明と要素の「双対性」  型の理論の、中心的な概念は、型と命題、 証明と要素の「双対性」である。  p が命題 P の証明であることを、p : P と表してみよう。  この「p が命題 P の証明である」という判 断を表す p : P は、「p は、型 P の要素 である」という判断を表していると見なす ことが出来るし、また、逆の見方も出来る のである。

型と命題、要素と証明の「双対性」 「p は、命題 P の証明である」 証明 命題 p:P 要素 型 「p は、型 P の要素である」

論理式の意味を考える Due to Per Martin-Lof “ON THE MEANINGS OF THE LOGICAL CONSTANTS AND THE JUSTIFICATIONS OF THE LOGICAL LAWS” http://docenti.lett.unisi.it/files/4/1/1/6/mar tinlof4.pdf

論理式の意味?       A∧B : AかつB A∨B : AまたはB A→B : AならばB ~A : Aではない ∀xP(x) : 全てのxについてP(x) ∃xP(x) : あるxが存在してP(x)

A の意味  「Aは真である。」  「私は「Aは真である」ことを知っている 。」 対象 行為 私は「Aは真である」ことを知って いる。 ただ、その前に、知っていることがある。

論理式の表現・構成についての 判断の構造 明証的な判断 判断 私は A が論理式である ことを知ってい る 表現 判断の形式

論理式の正しさについての 判断の構造 明証的な判断 判断 私は A が真である ことを知っている 論理式 判断の形式

判断と命題  判断の概念は、常に、命題の概念に先立つ 。  判断における論理的帰結の概念は、命題に おける含意より先に、説明されなければな らない。

証明とは何か?  証明とは、判断を明証なものにするもの。  証明すること=知ること=理解して把握す ること  知るようになる=知識を得ること  証明と知識は、同じもの

証明について考える Due to Per Martin-Lof “Intuitionistic Type Theory” Bibliopolis 1980

証明の解釈  Kolmogorovは、命題 a → bの証明に、「命 題 aの証明を命題 bの証明に変換する方法を 構築すること」という解釈を与えた。  このことは、a → bの証明を、aの証明からb の証明への関数と見ることが出来るというこ とを意味する。  このことは、同時に、命題をその証明と同一 視出来ることを示唆する。  型はこうした証明の集まりを表現し、そうし た証明の一つは、対応する型の、一つの項と 見なすことが出来る。

命題の証明は、何から構成されるか ?      ⊥ A∧B A∨B A→B (∀x)B(x) なし Aの証明とBの証明の両方 Aの証明、あるいは、Bの証明 Aの証明からBの証明を導く方法 任意のaに対してB(a)の証明を与 える方法  (∃x)B(x) あるaに対するB(a)の証明

命題の証明は、何から構成されるか ? 形式的に  ⊥  A∧B  A∨B  A→B  (∀x)B(x)  (∃x)B(x) none Aの証明であるaと、 Bの証明であるbのペア(a,b) Aの証明であるi(a)、あるいは、 Bの証明であるj(b) Aの証明であるaに対して、 Bの証明b(a)を与える(λx)b(x) 任意のaに対して Bの証明b(a)を与える(λx)b(x) あるaと、B(a)の証明であるbのペア (a,b)

Propositions as Types and Proofs as Terms (PAT) Due to Simon Thompson “Type Theory & Functional Programming” 1999

Curry-Howardの対応関係を どう証明するか?  ここでは、Simon Thompsonのやり方に従 う。  まず、p : P が 「p が命題 P の証明である」 という判断を表すとして、そうした判断が従 うべきルールを形式的に記述する。  ついで、p : P が 「p が型 P の要素である」 という判断を表すとして、そうした判断が従 うべきルールを形式的に記述する。  そうすると、前者と後者の形式的記述が、そ の解釈は別にして、まったく同じものである ことが分かる。

命題とその証明のルール

命題とその証明のルール  Formationルール システムの証明は、どのような形をしている か?  Introduction / Eliminationルール どのような表現が、命題の証明になるか?  Computationルール 表現は、どのようにして単純な形に還元さ れるのか?

∧ を含む命題の証明のルール  Aが命題であり、Bが命題であれば、A∧Bは命 題になる。  pが命題Aの証明であり、かつ、qが命題Bの証 明であれば、p,qのペア(p、q)は、命題 A∧Bの証明である。  rが命題A∧Bの証明であれば、ペアrの第一項 fst rは、命題Aの証明であり、ペアrの第二項 snd rは命題Bの証明である。  ペア(p、q)について、fst(p,q)=pであり、 snd(p,q)=qである。

∧ を含む命題の証明のルール  Formationルール A は命題である B は命題である (∧F) (A∧B) は命題である  Introductionルール p:A q:B (∧I) (p,q) : (A∧B)  Eliminationルール r : (A∧B) (∧E ) r : (A∧B) 1 (∧E2) fst r : A snd r : B

∧ を含む命題の証明のルール  Computationルール fst (p,q) → p snd (p,q) → q

→ を含む命題の証明のルール  Aが命題であり、Bが命題であれば、A→Bは 命題になる。  xが命題Aの証明だと仮定して、eが命題Bの証 明だとしよう。この時、命題A→Bの証明は、 x:Aであるxの関数としてみたe、 (λx:A).eで ある。  qが命題A→Bの証明で、aが命題Aの証明だと すれば、関数qにaを適用した(q a)は、命題B の証明である。  この時、((λx:A).e) a = e[a/x] (eの中 のxを全てaで置き換えたもの) になる。

→ を含む命題の証明のルール  Formationルール A は命題である B は命題である (→F) (A→B) は命題である  Introductionルール [x : A] … e:B (→I) (λx:A).e : (A→B)

→ を含む命題の証明のルール  Eliminationルール q : (A→B) a:A (→E) (q a) : B  Computationルール ((λx:A).e) a → e[a/x]

∨ を含む命題の証明のルール  Aが命題であり、Bが命題であれば、A∨Bは命 題になる。  qが命題Aの証明であれば、qは命題A∨Bの証 明を、rが命題Bの証明であれば、rも命題A∨B の証明を与えるように見える。  ここで、qに「qは∨で結ばれた命題の左の式 の証明である」という情報を付け加えたもの を、inl qとし、同様に、rに「rは∨で結ばれた 命題の右の式の証明である」という情報を付 け加えたものを、inr rと表すことにしよう。

∨ を含む命題の証明のルール  その上で、qが命題Aの証明であれば、inl qが 命題A∨Bの証明を、rがBの証明であれば、inr rが命題A∨Bの証明を与えると考える。  このことは、命題A∨Bが証明されるのは、命 題Aまたは命題Bのどちらかが証明される場合 に限ることになる。  例えば、命題A∨~Aが証明されるのは、命題A または命題~Aのどちらかが証明された場合だ けということになる。この体系では、一般に 「排中律」はなりたたない。

∨ を含む命題の証明のルール  今、pが命題A∨Bの証明で、fが命題A→Cの証 明で、gが命題B→Cの証明とした時、命題C の証明がどのような形になるか考えよう。  pが命題A∨Bの命題Aの証明であるか(inl p) 命題A∨Bの命題Bの証明であるか(inr p)の場 合に応じて、命題Cの証明の形は変わる。  前者の場合、pは命題Aの証明であるので、 f:A→Cと組み合わせれば、命題Cが導ける。 後者の場合、pは命題Bの証明であるので、 g:B→Cと組み合わせれば、命題Cが導ける。

∨ を含む命題の証明のルール  Formationルール A は命題である B は命題である (∨F) (A∨B) は命題である  Introductionルール q:A r:B (∨I1) (∨I2) inl q : (A∨B) inr r : (A∨B)  Eliminationルール p : (A∨B) f : (A→C) g : (B→C (∨E) ) cases p f g : C

∨ を含む命題の証明のルール  Computationルール cases (inl q) g f → f q cases (inr r) g f → g r

⊥ の証明のルール  ⊥は、矛盾を表す。  矛盾を導く証明のルールは、存在しない。  もし、pが矛盾の証明なら、どんな命題も証明 可能になる。

⊥ の証明のルール  Formationルール (⊥F) ⊥は命題である  Eliminationルール p:⊥ (⊥E) abortA p : A

Assumption のルール  Formationルール Aは命題である(AS) x:A

型とその要素のルール

型とその要素のルール  Formationルール システムの型は、どのような形をしているか ?  Introduction / Eliminationルール どのような表現が、型の要素となるか?  Computationルール 表現は、どのようにして単純な形に還元さ れるのか?

∧ を含む要素の型のルール  Aが型であり、Bが型であれば、A∧Bは型にな る。  pが型Aの要素であり、かつ、qが型Bの要素で あれば、p,qのペア(p、q)は、型A∧Bの要 素である。  rが型A∧Bの要素であれば、ペアrの第一項 fst rは、型Aの要素であり、ペアrの第二項snd r は型Bの要素である。  ペア(p、q)について、fst(p,q)=pであり、 snd(p,q)=qである。

∧ を含む型のルール  Formationルール A は型である B は型である (∧F) (A∧B) は型である  Introductionルール p:A q:B (∧I) (p,q) : (A∧B)  Eliminationルール r : (A∧B) (∧E ) r : (A∧B) 1 (∧E2) fst r : A snd r : B

∧ を含む型のルール  Computationルール fst (p,q) → p snd (p,q) → q

∧ を含む要素の型のルール  型として見ると、A∧Bは、二つの型の直積で ある。  fst, sndは、直積から直積を構成する要素へ の射影演算子である。  通常のプログラム言語からみれば、A∧Bは、 「レコード型」と見ることが出来る。

→ を含む要素の型のルール  Aが型であり、Bが型であれば、A→Bは型に なる。  xが型Aの要素だと仮定して、eが型Bの要素だ としよう。この時、型A→Bの要素は、x:Aで あるxの関数としてみたe、 (λx:A).eである 。  qが型A→Bの要素で、aが型Aの要素だとすれ ば、関数qにaを適用した(q a)は、型Bの要素 である。  この時、((λx:A).e) a = e[a/x] (eの中 のxを全てaで置き換えたもの) になる。

→ を含む型のルール  Formationルール A は型である B は型である (→F) (A→B) は型である  Introductionルール [x : A] … e:B (→I) (λx:A).e : (A→B)

→ を含む型のルール  Eliminationルール q : (A→B) a:A (→E) (q a) : B  Computationルール ((λx:A).e) a → e[a/x]

→ を含む要素の型のルール  型A→Bの要素は、型Aから型Bヘの関数であ る。  Introductionルールは、ドメインに x:Aとい う制限を加えた、λ計算のλ abstractionであ る。  Eliminationルールは、λ計算の関数の適用( application)の型を与える。  Computationルールは、λ計算のβ還元規則で ある。

∨ を含む型の要素のルール  Aが型であり、Bが型であれば、A∨Bは型にな る。  qが型Aの要素であれば、qは型A∨Bの要素を 、rが型Bの要素であれば、rも型A∨Bの要素を 与えるように見える。  ここで、qに「qは∨で結ばれた型の左の型の 型である」という情報を付け加えたものを、 inl qとし、同様に、rに「rは∨で結ばれた型の 右の型の要素である」という情報を付け加え たものを、inr rと表すことにしよう。

∨ を含む型の要素のルール  その上で、qが型Aの要素であれば、inl qが型 A∨Bの要素を、rが型Bの証明であれば、inr r が型A∨Bの要素を与えると考える。  このことは、型A∨Bが要素を持つのは、型Aま たは型Bのどちらかが要素を持つ場合に限る ことになる。  例えば、型A∨~Aが要素を持つのは、型Aまた は型~Aのどちらかが要素を持つ場合だけとい うことになる。この体系では、一般に「排中 律」はなりたたない。

∨ を含む型の要素のルール  今、pが型A∨Bの要素で、fが型A→Cの要素で 、gが型B→Cの要素とした時、型Cの要素が どのような形になるか考えよう。  pが型A∨Bの型Aの要素であるか(inl p) 型A∨Bの型Bの要素であるか(inr p)の場合に 応じて、型Cの要素の形は変わる。  前者の場合、pは型Aの要素であるので、 f:A→Cと組み合わせれば、型Cが導ける。 後者の場合、pは型Bの要素であるので、 g:B→Cと組み合わせれば、型Cが導ける。

∨ のルール  Formationルール A は型である B は型である (∨F) (A∨B) は型である  Introductionルール q:A r:B (∨I1) (∨I2) inl q : (A∨B) inr r : (A∨B)  Eliminationルール p : (A∨B) f : (A→C) g : (B→C (∨E) ) cases p f g : C

∨ を含む型のルール  Computationルール cases (inl q) g f → f q cases (inr r) g f → g r

∨ を含む型のルール  型A∨Bは、型Aと型Bの直和である。  通常のプログラム言語では、値に名前のタグ がつけられたレコード型と考えてよい。  Eliminationルールは、その名前による場合分 けに相当する。  Computationルールは、pにAのタグがつい ていれば、f p を計算してCの要素を求め、p にBのタグがついていれば、 g pを計算して、 Cの要素を求めることを表している。

⊥ の型のルール  Formationルール (⊥F) ⊥は型である  Eliminationルール p:⊥ (⊥E) abortA p : A

⊥ の型のルール  このルールは、もしpが空である型の要素であ れば、プログラムは中断すべきことを表して いる。

Assumption のルール  Formationルール Aは型である (AS) x:A

QuantifierとEquality

∀ を含む命題の証明のルール  Formationルール [x : A] … Aは命題である Pは命題である (∀F) (∀x:A).P は命題である  Introductionルール [x : A] … p:P (λx:A).p : (∀x:A) P (∀I)

∀ を含む命題の証明のルール  Eliminationルール a:A f : (∀x:A) P f a : P[a/x]  Computationルール ((λx : A) . p) a = p[a/x] (∀E)

∃ を含む命題の証明のルール  Formationルール [x : A] … Aは命題である Pは命題である (∃F) (∃x:A).P は命題である  Introductionルール a:A p : P[a/x] (a,p) : (∃x:A) .P (∃I)

∃ を含む命題の証明のルール  Eliminationルール p : (∃x:A).P p : (∃x:A).P Fst p : A (∃E’1) Snd p : A (∃E’2)  Computationルール Fst (p, q) = p Snd (p, q) = q

等号 =A を含む型のルール  I(A, a, b)  a =A b  Formationルール Aは型である a:A b:A (IF) I(A, a, b)は型である  Introductionルール a:A r(a) : I(A, a, a) (II)

等号 =A を含む型のルール  Eliminationルール c : I(A, a, b) d : C(a, a, r(a)) (IE) J(c, d) : C(a, b, c)  Computationルール J(r(a)、d) = d

Part III Coq入門

Part III Coq入門  数学の証明とコンピュータ  Coqとはどんな言語か?  関数型プログラム言語としてのCoq  ListをCoqでプログラムする  証明支援システムとしてのCoq      基本的なtacticについて tacticを使って見る n x m = m x n を証明する 証明に必要な情報を見つける 二分木についての定理の証明  Coqからのプログラムの抽出  あらためて、p : P (証明 : 命題) を考える

数学の証明とコンピュータ

誤っていた「証明」  「フェルマーの定理」は、最終的には、1995 年のAndrew Wilesの論文によって証明され たが、フェルマー自身は、この定理を証明出 来たと信じていた。それが、誤った「証明」 であったのは確かである。  Wiles自身も、95年の論文以前に一度、「証 明した」とする発表を行うが、誤りが見つか り、それを撤回している。  世紀の難問である「リーマン予想」は、何度 か「証明」が発表されている。今までのとこ ろ、それは誤って「証明」だった。

正しいことの判定が難しい証明  Grigory Perelmanは、2002年から2003年 にかけて arXiv に投稿した論文で、「三次元 のポアンカレ予想」を解いたと主張した。  arXivは、学会の論文誌とは異なり、掲載の可 否を決める査読が基本的にないので、発表の 時点では、彼の論文以外に、彼の証明が正し いという裏付けはなかった。  彼の証明の検証は、複数の数学者のグループ で取り組まれ、最終的に彼の証明の正しさが 「検証」されたのは、2006年のことだった。

非常に膨大な証明  「有限単純群の分類問題」は、Daniel Gorensteinをリーダーとする数学者の集団に よって解決され、20世紀の数学の大きな成果 の一つと呼ばれている。  ただ、その「証明」は、100人以上の数学者 が、50年のあいだに数百の論文誌に発表した 、膨大な量の「証明」の総和である。そのペ ージ数は一万ページを超えると言われている 。(「全部を読んでる数学者は、1人もいな い。」というのがジョークなのか本当なのか 、分からない。)

「四色問題」のコンピュータによる 解決  1974年、 イリノイ大学のKenneth Appelと Wolfgang Hakenは、当時の最先端のコンピ ュータを使って、「四色問題」を解いた。  コンピュータの稼働時間は、1200時間に及び 、夜間の空き時間しか利用が認められなかっ たので半年がかりの計算だったと言う。  コンピュータが人手にはあまる膨大な計算を 行ったのは事実だが、当時、その計算の正し さの検証しようのないことを理由に、こうし た「証明」を疑問視する声も一部にはあった 。

「四色問題」「Feit-Thompsonの 定理」のCoqによる証明  2004年、Georges Gonthierは、Coqを使っ て「四色問題」を解いた。  Georges Gonthierは、また、2013年、有限 群分類の重要な定理である、「FeitThompsonの定理」のCoqによる形式的証明 を与えた。  15,000の定義、4,300の定理、17万行のソ ースからなるこの証明を、彼はチーム作業で 、6年かけて完成させた。

Univalent TheoryでのCoqの利用  先にも見たように、Voevodskyは、 Univalent Theoryという数学理論を、Coqの プログラムの形で、GitHubで公開している。 https://github.com/vladimirias/Foundati ons/

Coqとはどんな言語か?

Coq言語の開発  Coqの開発は、Thierry Coquand とGérard Huetによって1984年から、INRIA(Institut National de Recherche en Informatique et en Automatique フランス国立情報学自 動制御研究所)で開始された。その後、 Christine Paulin-Mohringが加わり、40人以 上の協力者がいる。  最初の公式のリリースは、拡張された素朴な 帰納タイプのCoC 4.10で1989年。1991年 には、Coqと改名された。

 それ以来、ユーザーのコミュニティは増大を 続けており、豊かな型付き言語として、また 、インタラクティブな定理証明システムとし て、Coqのコンセプトのオリジナリティとそ の様々な特徴に魅了されている。  今年2013年には、ACMのSIGPLANの Programming Languages Software Awardを授賞した。

Award 授賞理由  Coq証明支援システムは、 機械でチェックさ れた形式的推論に対して、豊かなインタラク ティブな開発環境を与えている。  Coqは、プログラム言語とシステムの研究に 深いインパクトを与え、その基礎へのアプロ ーチをそれまで全く予想もされなかった規模 と確実さのレベルへと拡大し、そして、それ らを現実のプログラミング言語とツールにま で押し広げた。

 Coqは、プログラム言語研究のコミュニティ で研究ツールとして広く受け入れられている 。そのことは、SIGPLANのカンファレンスの 論文成果の多くが、Coqで開発され検証され ていることをみても明らかである。  Coqは、また、急速に、多くの有力な大学の 提供する講座で、プログラミング言語の基礎 を教える為の主要なツールの一つとして選ば れている。そして、それをサポートする多く の書籍が登場しようとしている。

 最後だが重要なことは、こうした成功が、 Coqがそれに基づいている、非常に豊かな表 現力を備えた基本的な論理である、 dependent type theoryに対する関心の幅広 い波が、急速に広がるのを助けていることで ある。  ソフトウェア・システムとしてCoqは、20年 以上にわたって開発が継続してきた。これは 、本当に印象的な、研究ドリブンの開発とそ の維持の偉業である。Coqチームは開発を続 け、新しいリリースの度に、表現力でも利用

 一言で言って、Coqは、数学・セマンティッ クス・プログラムの検証の、形式的な正確性 の保証の新しい時代への移行の中で、本質的 に重要な役割を果たしているのである。

Coqのインストールと起動  Coqは、次のサイトから入手出来る。 http://coq.inria.fr/  コマンドラインから、coqtopと打ち込む とCoqが起動する。  coqideで、IDE環境を利用することが出来 る。

関数型プログラム言語としての Coq

型のチェックと定義 Coq < Check 2 + 3. 2 + 3 : nat Coq < Check 2. 2 : nat Coq < Check (2 + 3) + 3. (2 + 3) + 3 : nat Coq < Definition three := 3. three is defined

型のチェックと定義 Coq < Definition add3 (x : nat) := x + 3. add3 is defined Coq < Check add3. add3 : nat -> nat Coq < Check add3 + 3. Error the term "add3" has type "nat -> nat" while it is expected to have type "nat” Coq < Check add3 2. add3 2 : nat

値の計算 Coq < Compute add3 2. = 5 : nat Coq < Definition s3 (x y z : nat) := x + y + z. s3 is defined Coq < Check s3. s3 : nat -> nat -> nat -> nat Coq < Compute s3 1 2 3 =6 : nat

関数の定義と引数 Coq < Definition rep2 (f : nat -> nat)(x:nat) := f (f x). rep2 is defined Coq < Check rep2. rep2 : (nat -> nat) -> nat -> nat Coq < Definition rep2on3 (f : nat -> nat) := rep2 f 3. rep2on3 is defined Coq < Check rep2on3. rep2on3 : (nat -> nat) -> nat

無名関数の定義 Coq < Check fun (x : nat) => x + 3. fun x : nat => x + 3 : nat -> nat Coq < Compute (fun x:nat => x+3) 4. = 7 : nat Coq < Check rep2on3 (fun (x : nat) => x + 3). rep2on3 (fun x : nat => x + 3) : nat Coq < Compute rep2on3 (fun (x : nat) => x + 3) . = 9 : nat

帰納的データ型の定義の例 bool型の定義 (enumerated type) Inductive bool : Set := | true : bool | false : bool. 自然数型の定義 (recursive type) Inductive nat : Set := | O : nat | S : nat -> nat.

帰納的データ型の定義の例 List型の定義 (recursive type) Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A. 二分木型の定義 (recursive type) Inductive natBinTree : Set := | Leaf : natBinTree | Node (n:nat)(t1 t2 : natBinTree).

パターン・マッチングによる定義 bool値の否定の定義 Definition negb b := match b with | true => false | false => true end.

パターン・マッチングによる定義 Definition tail (A : Type) (l:list A) := match l with | x::tl => tl | nil => nil end. Definition isempty (A : Type) (l : list A) := match l with | nil => true | _ :: _ => false end.

パターン・マッチングによる定義 Definition has_two_elts (A : Type) (l : list A) := match l with | _ :: _ :: nil => true | _ => false end. Definition andb b1 b2 := match b1, b2 with | true, true => true | _, _ => false end.

リカーシブな定義 Fixpoint plus n m := match n with | O => m | S n' => S (plus n' m) end. Notation : n + m for plus n m 1+1 = S(O+1)=S(1)=S(S(O))

リカーシブな定義 Fixpoint minus n m := match n, m with | S n', S m' => minus n' m' | _, _ => n end. Notation : n - m for minus n m 3-2=2-1=1-0=1 2-3=1-2=0-1=0

リカーシブな定義 Fixpoint mult (n m :nat) : nat := match n with | 0 => 0 | S p => m + mult p m end. Notation : n * m for mult n m 3*2=2+2*2=2+2+2*1=2+2+2+2*0

ListをCoqでプログラムする

list型の定義 listの基本的な定義は、次のものである。 Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A. ここで、listは、A : Type なる任意の型に対して 定義されていることに注意しよう。(Polymorphism) constructor consに対して次の記法を導入する。 infix “::” := cons (at level 60, ....)

listについての基本的な関数 length lengthは、listの長さを返す。 Definition length (A : Type) : list A -> nat := fix length l := match l with | nil => O | _ :: l' => S (length l') end. 再帰的な関数の定義には、fixpoint を使うが、 定義の本体に再帰的な定義が現れる場合は、 fix を使う。

listについての基本的な関数 app app(++)は、二つのlistを結合(append)する。 Definition app (A : Type) : list A -> list A -> list A := fix app l m := match l with | nil => m | a :: l1 => a :: app l1 m end. Infix "++" := app (right associativity, ....

listについての基本的な関数 map mapは、listの各要素に関数を適用する。 Fixpoint map A B (f : A -> B)(l : list A) : list B := match l with | nil => nil | a::l' => f a :: map f l' end. Compute map (fun n => n * n)(1::2::3::4::5::nil). 1::4::9::16::25::nil : list nat

listについての基本的な関数 reverse reverseは、listの要素を逆順にする。 Fixpoint naive_reverse (A:Type)(l: list A) : list A := match l with | nil => nil | a::l' => naive_reverse l' ++ (a::nil) end. Compute naive_reverse (1::2::3::4::5::6::nil). = 6 :: 5 :: 4 :: 3 :: 2 :: 1 :: nil : list nat

証明支援システムとしてのCoq

判断 Γ |- A  いくつかの命題の集りΓ を仮定すれば、あ る命題Aが結論として導かれるという判断 を次のように表現しよう。 Γ |- A  例えば、次の表現は、命題 P / Q と命題 〜Q から、命題 R → R ∧ Pが導かれるこ とを表現している。

推論ルール  ある判断の集まり Γ1 |- A1, Γ2 |- A2, ... Γn |- Anから、別の判断 Γ |- Bが導かれる 時、それを推論ルールと呼び、次のように 表す。 Γ1 |- A1 Γ2 |- A2 ... Γn |- An Γ |- B  例えば、次の表現は、一つの推論ルールで ある。

推論ルールの二つの解釈  この推論ルールには、次のような二つの解 釈が可能である。  前向きの解釈 Aが成り立つことが言え、Bが成り立つこ とが言えれば、A∧Bが成り立つことが言え る。  後ろ向きの解釈 A∧Bが成り立つことが言える為には、Aが 成り立つことが言え、Bが成り立つことが 言えなければならない。

Coqでの証明のスタイル  Coqでは、推論ルールの後ろ向きの解釈で 証明を進める。  すなわち、証明すべき命題(これをGoalと 呼ぶ)を成り立たせる為に必要な命題(こ れをSub Goalと呼ぶ)にさかのぼって証 明を進める。  あるGoalの全てのSub Goalが証明出来れ ば、これ以上のSub Goalが存在しなくな った時に証明が終わる。

Coqでの演繹ルールの適用 tactic  GoalからSub Goalの導出は、与えられた推 論ルールの(後ろ向きの)適用に基づくのだ が、Coqでは、その操作をtacticを適用する という。  tacticには、いろいろな種類があり、それぞ れのtacticsが、Coqのインタラクティブな証 明支援システムの中で、証明を進める為のコ マンドとして機能する。  Coqでの証明とは、あるGoalに対して、全て のSub Goalがなくなるような、一連のtactic コマンドを与えることである。

様々なタイプのtacticコマンド  Coqには、非常に沢山のtacticコマンドがある。 例えば、つぎのようなタイプのtacticがある。  論理的な(命題論理、一階の述語論理等の)推 論ルール、あるいはそれらのルールの組み合わ せに対応した基本的なtactic (intro, elim等) 。  システムの中で既に証明されている補題・定理 を利用するtactic (apply等)。  a=b という等式を代入してGoal を書き換え るtactic (rewrite 等)。

基本的なtacticについて

tactic assumption  現在のゴールが次のような形をしているとき 、tactic assumption を用いる。 ... H:A ... ----------A  exact H, trivial tacticを使ってもいい。  このtacticは、次の推論規則に対応している 。

tactic intro  現在のゴールが A→Bの形をしている時、 tactic introは次のように働く。 ... ... ... ----------A→B intro H ... H:A ... ----------B  これは、次の推論規則に対応している。

tactic apply  現在の仮定とゴールが次のような形をしてい るとき、tactic apply を用いる。 ... ... H: B→ A H: B→ A apply H ... ... --------------------A B  対応する推論規則は、次になる。

tactic apply  より一般に、apply Hはn個のサブゴールを生 み出す。 ... ... ... H: A1→A2→...An→ A H: A1→... H: An→... apply H ... ... ... --------------------------- ... ----------A A1 An  対応する推論規則は。

introとapplyのサンプル Section Propositional_Logic. Variables P Q R : Prop. Lemma imp_dist : (P → (Q → R)) → (P → Q) → P → R. Proof. 1 subgoal P : Prop Q : Prop R : Prop -----------------------(P → Q → R) → (P → Q) → P → R intros H H0 p.

introとapplyのサンプル 1 subgoal: P : Prop Q : Prop R : Prop H:P→Q→R H0 : P → Q p:P -----------------------R apply H.

introとapplyのサンプル 2 subgoals: P : Prop Q : Prop R : Prop H:P→Q→R H0 : P → Q p:P -----------------------P subgoal 2 is: Q assumption.

1 subgoal: introとapplyのサンプル P : Prop Q : Prop R : Prop T : Prop H:P→Q→R H0 : P → Q p:P -----------------------Q apply H0;assumption. Proof completed Qed. imp dist is dened

tactic split  現在のゴールが A∧Bの形をしている時、 tactic splitは次のように、二つのサブゴール ... ... ... を作る。 ... ... ... split ... ... ... --------------------------------A∧B A B  対応する推論規則は。

tactic destruct  現在の仮定とゴールが次のような形をしてい るとき、tactic destruct を用いる。 ... ... H1: A destruct H H: A∧B H2: B as [H1 H2] ... ... --------------------C C  対応する推論規則。

destructとsplitのサンプル Lemma and_comm : P ∧ Q → Q ∧ P. Proof. intro H. 1 subgoal P : Prop Q : Prop H:P∧Q -----------------------Q∧P

destructとsplitのサンプル Lemma and_comm : P ∧ Q → Q ∧ P. Proof. intro H. 1 subgoal P : Prop Q : Prop H:P∧Q -----------------------Q∧P

destruct H as [H1 H2]. 1 subgoal P : Prop Q destructとsplitのサンプル : Prop H1 : P H2 : Q -----------------------Q∧P split. 2 subgoals P : Prop Q : Prop H1 : P H2 : Q -----------------------Q subgoal 2 is: P

tactic left, right  現在のゴールが、A∨Bのような形をしている とき、tactic left あるいrightを用いる。 ... ... ... ... left ... ... --------------------A∨B A  対応する推論規則は、次になる。

tactic destruct  現在の仮定が A∨Bの形をしている時、tactic destructは、二つのサブゴールを作る。 ... destruct H A∨B as [H1 H2] ... ------------C  対応する推論規則は。 ... H1: A ... ----------C ... H2: B ... ----------C

left, right, destructのサンプル Lemma or_comm : P ∨ Q → Q ∨ P. Proof. intros. P : Prop Q : Prop H:P∨Q -----------------------Q∨P

destruct H as [H0 | H0]. two subgoals P : Prop Q : Prop H:P∨Q H0 : P -----------------------Q∨P subgoal 2 is : Q∨P right; assumption. left; assumption. Qed.

tacticを使って見る

例1 A -> (A->B) ->B の証明 Coq < Lemma S1 : forall A B :Prop, A ->(A->B) ->B. 1 subgoal ============================ forall A B : Prop, A -> (A -> B) -> B Goalから、forallを消す。 S1 < intros. →の前提部分を仮説に移す。 1 subgoal introsは、複数のintroを同時に適用する。 A : Prop B : Prop Γ1 新しい仮定 H:A H0 : A -> B ============================ B 新しいゴール

S1 < apply H0. 1 subgoal H0 A->B を利用する。 Aをゴールに移す。 A : Prop B : Prop Γ2 新しい仮定 H:A H0 : A -> B ============================ A 新しいゴール S1 < assumption. 仮定には、既にAが含まれている No more subgoals. S1 < Qed. 証明終わり intros. apply H0. assumption. S1 is defined

例3 (P / Q) / ~Q) -> ( R -> R /P)の証明 Coq < Lemma S3: forall P Q R : Prop, (P / Q) / ~Q -> ( R -> R /P). 1 subgoal ============================ forall P Q R : Prop, (P / Q) / ~ Q -> R -> R / P S3 < intros. 1 subgoal Goalから、forallを消す。 →の前提部分を仮説に移す。 P : Prop Q : Prop R : Prop Γ1 新しい仮定 H : (P / Q) / ~ Q H0 : R ============================ R / P 新しいゴール

S3 < split. 2 subgoals ゴールのR∧Pを、二つの サブゴールに分割する P : Prop Q : Prop Γ1 仮定 R : Prop H : (P / Q) / ~ Q H0 : R ============================ 新しいゴール R subgoal 2 is: もう一つの新しいゴール。 P 仮定部分は表示されていない S3 < assumption. ゴールのRは、既に仮定に含まれている。 これで、一つのゴールの証明は終わり、 証明すべきゴールは、一つになった。

1 subgoal P : Prop Q : Prop Γ1 仮定 R : Prop H : (P / Q) / ~ Q H0 : R ============================ 新しいゴール P S3 < destruct H. 仮定のHを分割する。仮定中の∧の destructは、仮定を変更する。 1 subgoal P : Prop Q : Prop R : Prop Γ2 新しい仮定 H : P / Q H1 : ~ Q H0 : R ============================ 新しいゴール P

仮定のHを分割する。仮定中の∨の S3 < destruct H. destructは、仮定を変更するとともに 2 subgoals ゴールを枝分かれさせる。 P : Prop Q : Prop R : Prop Γ3 新しい仮定 H:P H1 : ~ Q H0 : R ============================ 新しいゴール P subgoal 2 is: P S3 < assumption. ゴールのPは、既に仮定に含まれている。 これで、一つのゴールの証明は終わり、 証明すべきゴールは、一つになった。

1 subgoal P : Prop Q : Prop R : Prop Γ4 新しい仮定 H:Q H1 : ~ Q H0 : R ============================ 新しいゴール P S3 < absurd Q. Qについての仮定は矛盾している。 Qか〜Qのどちらかが正しい

2 subgoals P : Prop Q : Prop R : Prop Γ4 新しい仮定 H:Q H1 : ~ Q H0 : R ============================ 新しいゴール ~Q subgoal 2 is: Q S3 < assumption. ゴールの〜Qは、既に仮定に含まれている。 これで、一つのゴールの証明は終わり、 証明すべきゴールは、一つになった。

1 subgoal P : Prop Q : Prop R : Prop Γ4 新しい仮定 H:Q H1 : ~ Q H0 : R ============================ Q 新しいゴール S3 < assumption. No more subgoals. ゴールのQは、既に仮定に含まれている。

S3 < Qed. intros. split. assumption. destruct H. destruct H. assumption. absurd Q. assumption. assumption. S3 is defined

n x m = m x n を証明する

n x m = m x nの nについての帰納法での証明  n=0 の時 0xm=mx0 0 = 0 となり、成り立つ。  n x m = m x n が成り立つと仮定して、 (n + 1) x m = m x (n + 1) を証明する。 左辺 = n x m + m 右辺 = m x n + m 帰納法の仮定より、n x m = m x n なので 、これを左辺に代入すると、左辺=右辺とな る。

ただ、先の証明には、いくつかの前 提がある  補題1 0 x m = 0  補題2 m x 0 = 0  補題3 (n + 1) x m = n x m + m  補題4 m x (n +1) = m x n + m これらの補題を使って  定理 n x m = m x n を証明する。

次の補題が証明されたとしよう  Lemma lemma1: forall n:nat, 0 * n = 0.  Lemma lemma2 : forall n:nat, n * 0 = 0.  Lemma lemma3: forall n m:nat, S n * m = n * m + m.  Lemma lemma4: forall n m:nat, m * S n = m * n + m.

この時、定理の証明は次のように進 む Coq < Theorem Mult_Commute : forall n m:nat, n * m = m * n. 1 subgoal ============================ forall n m : nat, n * m = m * n Mult_Commute < intros. 1 subgoal forallを消す。 n : nat m : nat ============================ n*m=m*n

Mult_Commute < induction n. nについての帰納法で証明する。 2 subgoals m : nat ============================ 0*m=m*0 n = 0の場合。 subgoal 2 is: Sn*m=m*Sn Mult_Commute < simpl. 2 subgoals nで成り立つと仮定して、n+1で 成り立つことを示す。 0 * m = 0 は、定義からすぐに 言えるので、単純化する。 m : nat ============================ 0=m*0 subgoal 2 is: Sn*m=m*Sn Mult_Commute < auto. 単純な式は、autoでも証明出来る。

1 subgoal n : nat m : nat IHn : n * m = m * n ============================ Sn*m=m*Sn Mult_Commute < rewrite lemma4. 1 subgoal lemma4 : m * S n = m * n + m を 使って、ゴールを書き換える。 n : nat m : nat IHn : n * m = m * n ============================ Sn*m=m*n+m

Mult_Commute < rewrite lemma3. 1 subgoal lemma3 : (S n) * m = n * m + m を 使って、ゴールを書き換える。 n : nat m : nat IHn : n * m = m * n ============================ n*m+m=m*n+m Mult_Commute < rewrite IHn. 1 subgoal IHn : n * m = m * n を 使って、ゴールを書き換える。 n : nat m : nat IHn : n * m = m * n ============================ m*n+m=m*n+m Mult_Commute < reflexivity. No more subgoals. 左辺と右辺は等しい

Mult_Commute < Qed. intros. induction n. simpl. auto. rewrite lemma4. rewrite lemma3. rewrite IHn. reflexivity. Mult_Commute is defined

補題1の証明 Coq < Lemma lemma1: forall n:nat, 0 * n = 0. 1 subgoal ============================ forall n : nat, 0 * n = 0 lemma1 < intros. 1 subgoal n : nat ============================ 0*n=0

lemma1 < induction n. 2 subgoals ============================ 0*0=0 subgoal 2 is: 0*Sn=0 lemma1 < simpl. 2 subgoals ============================ 0=0 subgoal 2 is: 0*Sn=0

lemma1 < reflexivity. 1 subgoal n : nat IHn : 0 * n = 0 ============================ 0*Sn=0 Fixpoint mult (n m :nat) : nat := lemma1 < constructor. No more subgoals. lemma1 < Qed. intros. induction n. simpl. reflexivity. constructor. lemma1 is defined match n with | 0 => 0 | S p => m + mult p m end. という定義を考えよう。この時。コンストラクタ 0が、この式が成り立つことを示している。 先の証明で、simpl. auto. で証明したのも 同じことである。

lemma1 < induction n. 2 subgoals ============================ 0*0=0 subgoal 2 is: 0*Sn=0 lemma1 &l

Add a comment

Related presentations

Related pages

プログラム利用時のすべてのユース ... - Qiita

facebook 『「型の理論」と証明支援システム —— Coqの世界 ... maruyama097 『「型の理論」と証明支援システム ...
Read more

『マルレク第七回テーマ:「型の理論」と証明支援システム -- COQの世界 』に行ってきました - yuumi3のお仕事日記

感想. 万年Haskell弱者である私には、なぜHaskellerが 型 型 型 型 いうのかが理解出来なかったのですが、今回学んだ ...
Read more

マルレク第七回テーマ:「型の理論」と証明支援システム -- Coqの世界

マルレク第七回テーマ:「型の理論」と証明支援システム -- Coqの世界 マルレク開催概要. 日時:12月16日(月) 19:00 ...
Read more

マルゼミ第七回テーマ:「型の理論」と証明支援システム -- Coqの世界

マルゼミ第七回テーマ:「型の理論」と証明支援システム -- Coqの世界 ... 型の理論」と証明支援システム ...
Read more

Maruyama-office - 丸山事務所(デジタルらいふ)

... の世界で、 丸山不二夫が重要と ... の理論」と証明支援システム --- coq ... 型の理論」と証明支援システム ...
Read more

後半第5回 「前回のつづき(証明支援システム)と 論理プログラミング」

計算の理論 後半第5回 「前回のつづき(証明支援システム)と ... 型検査. 論理の世界. 命題. 証明.
Read more