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

「型の理論」と証明支援システ
ム
-- 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)

ちょっと変わったλ式１
 λ式 Ω := (λ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である。

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

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で置き換えたもの）になる。

（→F）
(A→B) は命題である
[x : A]

…

e:B
（→I）
(λx:A).e : (A→B)


q : (A→B)
a:A
（→E）
(q a) : B
((λ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が導ける。


（∨F）
(A∨B) は命題である
q:A
r:B
（∨I1）
（∨I2）
inl q : (A∨B)
inr r : (A∨B)
p : (A∨B) f : (A→C） g : （B→C
（∨E）
）
cases p f g : C

cases (inl q) g f → f q
cases (inr r) g f → g r

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

⊥ の証明のルール
（⊥F）

⊥は命題である
p:⊥
（⊥E）
abortA p : A

Assumption のルール
Aは命題である（AS）
x:A

型とその要素のルール

型とその要素のルール
システムの型は、どのような形をしているか
？

 Introduction / Eliminationルール
どのような表現が、型の要素となるか？
表現は、どのようにして単純な形に還元さ
れるのか？

∧ を含む要素の型のルール
 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である。

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

∧ を含む型のルール
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で置き換えたもの）になる。

→ を含む型のルール
A は型である
B は型である
（→F）
(A→B) は型である
[x : A]

…

e:B
（→I）
(λx:A).e : (A→B)

→ を含む型のルール

q : (A→B)
a:A
（→E）
(q a) : B
((λ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が導ける。

∨ のルール

A は型である
B は型である
（∨F）
(A∨B) は型である
q:A
r:B
（∨I1）
（∨I2）
inl q : (A∨B)
inr r : (A∨B)
p : (A∨B) f : (A→C） g : （B→C
（∨E）
）
cases p f g : C

∨ を含む型のルール
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の要素を求めることを表している。

⊥ の型のルール
（⊥F）

⊥は型である
p:⊥
（⊥E）
abortA p : A

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

Assumption のルール
Aは型である（AS）
x:A

∀ を含む命題の証明のルール
[x : A]

…
Aは命題である
Pは命題である
（∀F）
(∀x:A).P は命題である
[x : A]

…
p:P
(λx:A).p : (∀x:A) P

（∀I）

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

（∀E）

∃ を含む命題の証明のルール
[x : A]

…
Aは命題である
Pは命題である
（∃F）
(∃x:A).P は命題である
a:A
p : P[a/x]
(a,p) : (∃x:A) .P

（∃I）

∃ を含む命題の証明のルール

p : (∃x：A).P
p : (∃x：A).P
Fst p : A （∃E’1） Snd p : A （∃E’2）
Fst (p, q) = p
Snd (p, q) = q

等号＝A を含む型のルール
 I(A, a, b)  a =A b
Aは型である
a:A b:A
（IF）
I(A, a, b)は型である

a:A
r(a) : I(A, a, a)

（II）

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

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年のあいだに数百の論文誌に発表した
、膨大な量の「証明」の総和である。そのペ
ージ数は一万ページを超えると言われている
。（「全部を読んでる数学者は、１人もいな
い。」というのがジョークなのか本当なのか
、分からない。）

「四色問題」のコンピュータによる
解決
 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

型のチェックと定義
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が導かれるこ
とを表現している。

推論ルール
 ある判断の集まり Γ１ |- A1, Γ2 |- A2, ...
Γn |- Anから、別の判断 Γ |- Bが導かれる
時、それを推論ルールと呼び、次のように
表す。
Γ１ |- 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: A１→...
H: An→...
apply H
...
...
...
--------------------------- ... ----------A
A１
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.

1 subgoal:
P : Prop
Q : Prop
R : Prop
H:P→Q→R
H0 : P → Q
p:P
-----------------------R
apply H.

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:
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 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.

例１
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

H０ A->B を利用する。
Aをゴールに移す。

A : Prop
B : Prop
Γ２新しい仮定
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についての帰納法での証明
 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 なので
、これを左辺に代入すると、左辺＝右辺とな
る。

ただ、先の証明には、いくつかの前
提がある
 補題１ 0 x m = 0
 補題２ m x 0 = 0
 補題３ (n + 1) x m = n x m + m
 補題４ 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

補題１の証明
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.
という定義を考えよう。この時。コンストラクタ
０が、この式が成り立つことを示している。
先の証明で、simpl. auto. で証明したのも
同じことである。

lemma1 < reflexivity.
1 subgoal

n : nat
IHn : 0 * n = 0
============================
0*Sn=0
lemma1 < constructor.
No more subgoals.
lemma1 < Qed.
intros.
induction n.
simpl.
reflexivity.
constructor.
lemma1 is defined

補題2の証明
Coq < Lemma lemma2: forall n:nat, n * 0 = 0.
intros.
単純な式は、autoでも証明出来る。
auto with arith.
こちらは、もっとキチンとした書き方。
Qed.

補題３の証明
Coq < Lemma lemma3: forall n m:nat, S n * m = n * m + m.
1 subgoal

============================
forall n m : nat, S n * m = n * m + m
lemma3 < intros.
1 subgoal
n : nat
m : nat
============================
Sn*m=n*m+m

lemma3 < simpl.
1 subgoal
n : nat
m : nat
============================
m+n*m=n*m+m

plus_comm : forall n m : nat,
lemma3 < apply plus_comm. n + m = m + n
で。和の可換性を示す補題。
No more subgoals.
既に証明されたものとして、証明中で
利用出来る。

lemma3 < Qed.
intros.
simpl.
apply plus_comm.

lemma3 is defined

補題４の証明
Coq < Lemma lemma4: forall n m:nat, m * S n = m * n + m.
1 subgoal
============================
forall n m : nat, m * S n = m * n + m
lemma4 < intros.
1 subgoal
n : nat
m : nat
============================
m*Sn=m*n+m

lemma4 < symmetry.
1 subgoal
n : nat
m : nat
============================
m*n+m=m*Sn
lemma4 < apply mult_n_Sm.
No more subgoals.
lemma4 < Qed.
intros.
symmetry.
apply mult_n_Sm.
lemma4 is defined

mult_n_Sm : forall n m : nat,
n*m+n=n*Sm
を利用する。この補題は、意外と証明が
難しい。

証明に必要な情報を見つける

証明に必要な定理・補題を見つける
Search
 Coqは、証明に利用出来る定理・補題のデ
ータベースを持っている。
 Search コマンドを使うと、それらの名前
と型が検索出来る。
Coq < Search le.
le_S: forall n m : nat, n <= m -> n <= S m
le_n: forall n : nat, n <= n
plus_le_reg_l: forall n m p : nat, p + n <= p + m -> n <= m
plus_le_compat_r: forall n m p : nat, n <= m -> n + p <= m + p
plus_le_compat_l: forall n m p : nat, n <= m -> p + n <= p + m
plus_le_compat: forall n m p q : nat, n <= m -> p <= q -> n + p <= m + q
nth_le:
forall (P Q : nat -> Prop) (init l n : nat),
P_nth P Q init l n -> init <= l
......

文字列を使って検索する
SearchAbout
Coq < SearchAbout "comm".
Bool.orb_comm: forall b1 b2 : bool, (b1 || b2)%bool = (b2 || b1)%bool
Bool.andb_comm: forall b1 b2 : bool, (b1 && b2)%bool = (b2 && b1)%bool
Bool.xorb_comm: forall b b' : bool, xorb b b' = xorb b' b
app_comm_cons:
forall (A : Type) (x y : Datatypes.list A) (a : A),
a :: x ++ y = (a :: x) ++ y
and_comm: forall A B : Prop, A / B <-> B / A
or_comm: forall A B : Prop, A / B <-> B / A
Max.max_comm: forall n m : nat, max n m = max m n
Min.min_comm: forall n m : nat, min n m = min m n
mult_comm: forall n m : nat, n * m = m * n
plus_comm: forall n m : nat, n + m = m + n
Relation_Definitions.commut:
forall A : Type,
Relation_Definitions.relation A -> Relation_Definitions.relation A -> Prop
....
....l

パターンを使って検索する
SearchPattern
Coq < SearchPattern (_ + _ = _ + _).
plus_permute_2_in_4: forall n m p q :
nat, n + m + (p + q) = n + p + (m + q)
plus_permute: forall n m p : nat, n + (m + p) = m + (n + p)
plus_comm: forall n m : nat, n + m = m + n
plus_assoc_reverse: forall n m p : nat, n + m + p = n + (m + p)
plus_assoc: forall n m p : nat, n + (m + p) = n + m + p
plus_Snm_nSm: forall n m : nat, S n + m = n + S m
....
....

先の mult_n_Smは、次のような検索で
見つけることが出来る。
Coq < SearchPattern (_ + _ = _ * _).
mult_n_Sm: forall n m : nat, n * m + n = n * S m

二分木についての定理の証明

http://users.csc.calpoly.edu/~zwood/teaching/csc471/finalproj26/mma/

二分木の定義
Inductive natBinTree : Set :=
| Leaf : natBinTree
| Node (n:nat)(t1 t2 : natBinTree).

Definition t0 : natBinTree :=
Node 5 (Node 3 Leaf Leaf)
(Node 8 Leaf Leaf).

t0
５

3

8

Fixpoint tree_size (t:natBinTree): nat :=
match t with
| Leaf =>
| Node _ t1 t2 => 1 + tree_size t1
+ tree_size t2
end.
Require Import Max.
Fixpoint tree_height (t: natBinTree) : nat :=
match t with
| Leaf => 1
| Node _ t1 t2 => 1 + max (tree_height t1)
(tree_height t2)
end.

Compute tree_size t0.
= 7: nat
Compute tree_height t0.
= 3 : nat

t1

4

Definition t1 : natBinTree :=
Node 4 (Node 7 Leaf Leaf) 7
(Node 1 Leaf t0).
Compute tree_size t1.
= 13 : nat
Compute tree_height t1.
= 5 : nat

1
５

3

8

Require Import List.
Fixpoint labels (t: natBinTree) : list nat :=
match t with
| Leaf => nil
| Node n t1 t2 => labels t1 ++ (n :: labels t2)
end.
Compute labels (Node 9 t0 t0).
= 3 :: 5 :: 8 :: 9 :: 3 :: 5 :: 8 :: nil
: list nat

9

５
3

５
8

3

8

この時、次のことを証明しよう。
「木tのサイズが１でなければ、tを構成する部分木t1,t
が存在する。」
命題の形で表すと次のようになる。
forall t, tree_size t <> 1 ->
exists n:nat,
exists t1:natBinTree,
t = Node n t1 t2.
以下は、Coqでの証明である。

Coq < Lemma tree_decompose : forall t, tree_size t <> 1 ->
exists n:nat, exists t1:natBinTree,
t = Node n t1 t2.
============================
forall t : natBinTree,
tree_size t <> 1 ->
exists (n : nat) (t1 t2 : natBinTree), t = Node n t1 t2
tree_decompose < Proof.
tree_decompose < intros t H.
1 subgoal
t : natBinTree
H : tree_size t <> 1
============================
exists (n : nat) (t1 t2 : natBinTree), t = Node n t1 t2
tree_decompose < destruct t as [ | i t1 t2]

2 subgoals
H : tree_size Leaf <> 1
============================
exists (n : nat) (t1 t2 : natBinTree), Leaf = Node n t1 t2
subgoal 2 is:
exists (n : nat) (t3 t4 : natBinTree), Node i t1 t2 = Node n t3 t4

tree_decompose < destruct H.
2 subgoals
============================
tree_size Leaf = 1
subgoal 2 is:
tree_decompose < reflexivity.

1 subgoal
i : nat
t1 : natBinTree
t2 : natBinTree
H : tree_size (Node i t1 t2) <> 1
============================

tree_decompose < exists i.
1 subgoal
i : nat
t1 : natBinTree
t2 : natBinTree
============================
exists t3 t4 : natBinTree, Node i t1 t2 = Node i t3 t4

tree_decompose < exists t1.

1 subgoal
i : nat
t1 : natBinTree
t2 : natBinTree
============================
exists t3 : natBinTree, Node i t1 t2 = Node i t1 t3
tree_decompose < exists t2.
1 subgoal
i : nat
t1 : natBinTree
t2 : natBinTree
============================
Node i t1 t2 = Node i t1 t2
tree_decompose < reflexivity.
No more subgoals.

tree_decompose < Qed.
intros t H.
destruct t as [| i t1 t2].
destruct H.
reflexivity.
exists i.
exists t1.
exists t2.
reflexivity.
tree_decompose is defined
Coq <

Coqからのプログラムの抽出

Coq < Extraction Language Haskell.
Coq < Require Import List.
Coq < Print length.
length =
fun A : Type =>
fix length (l : Datatypes.list A) : nat :=
match l with
| Datatypes.nil => 0
| _ :: l' => S (length l')
end
: forall A : Type, Datatypes.list A -> nat
Argument A is implicit
Argument scopes are [type_scope list_scope]

Coq < Extraction length.
length :: (List a1) -> Nat
length l =
case l of {
Nil -> O;
Cons y l' -> S (length l')}

Coq < Print app.
app =
fun A : Type =>
fix app (l m : Datatypes.list A) {struct l} :
Datatypes.list A :=
match l with
| Datatypes.nil => m
| a :: l1 => a :: app l1 m
end
: forall A : Type,
Datatypes.list A -> Datatypes.list A ->
Datatypes.list A
Argument A is implicit
Argument scopes are [type_scope list_scope
list_scope]

Coq < Extraction app.
app :: (List a1) -> (List a1) -> List a1
app l m =
case l of {
Nil -> m;
Cons a l1 -> Cons a (app l1 m)}

Coq < Extraction Language Ocaml.
(** val length : 'a1 list -> nat **)
let rec length = function
| Nil -> O
| Cons (y, l') -> S (length l')
(** val app : 'a1 list -> 'a1 list -> 'a1 list **)
let rec app l m =
match l with
| Nil -> m
| Cons (a, l1) -> Cons (a, (app l1 m))

Coq < Extraction Language Scheme.
(define length (lambda (l)
(match l
((Nil) `(O))
((Cons y l~) `(S ,(length l~))))))
(define app (lambdas (l m)
(match l
((Nil) m)
((Cons a l1) `(Cons ,a ,(@ app l1 m))))))

あらためて、
p : P (証明 : 命題) を考える
証明の関数としての表現

証明の関数としての表現
Coq < Print S1.
S1 =
fun (A B : Prop) (H : A) (H0 : A -> B) => H0 H
: forall A B : Prop, A -> (A -> B) -> B
Argument scopes are [type_scope type_scope _ _]
Coq < Print S2.
S2 =
fun (P Q : Prop) (H : forall P0 : Prop, (P0 -> Q) -> Q)
(H0 : (P -> Q) -> P) =>
H0 (fun _ : P => H (P -> Q) (H P))
: forall P Q : Prop,
(forall P0 : Prop, (P0 -> Q) -> Q) -> ((P -> Q) -> P) -> P
Argument scopes are [type_scope type_scope _ _]

Coq < Print S3.
S3 =
fun (P Q R : Prop) (H : (P / Q) / ~ Q) (H0 : R) =>
conj H0
match H with
| conj (or_introl H3) _ => H3
| conj (or_intror H3) H2 =>
False_ind P
((fun H4 : Q =>
(fun H5 : ~ Q => (fun (H6 : ~ Q) (H7 : Q) =>
H6 H7) H5) H2 H4) H3)
end
: forall P Q R : Prop, (P / Q) / ~ Q -> R -> R / P
Argument scopes are [type_scope type_scope type_scope _ _]

Coq < Print lemma1.
lemma1 =
fun n : nat =>
nat_ind (fun n0 : nat => 0 * n0 = 0) eq_refl
(fun (n0 : nat) (_ : 0 * n0 = 0) => eq_refl) n
: forall n : nat, 0 * n = 0

Coq < Print lemma2.
lemma2 =
fun n : nat =>
nat_ind (fun n0 : nat => n0 * 0 = 0) eq_refl
(fun (n0 : nat) (IHn : n0 * 0 = 0) => IHn) n
: forall n : nat, n * 0 = 0

Argument scope is [nat_scope]

Coq < Print lemma3.
lemma3 =
fun n m : nat => plus_comm m (n * m)
: forall n m : nat, S n * m = n * m + m
Argument scopes are [nat_scope nat_scope]

Coq < Print lemma4.
lemma4 =
fun n m : nat => eq_sym (mult_n_Sm m n)
: forall n m : nat, m * S n = m * n + m

Coq < Print mult_n_Sm.
mult_n_Sm =
fun n m : nat =>
nat_ind (fun n0 : nat => n0 * m + n0 = n0 * S m) eq_refl
(fun (p : nat) (H : p * m + p = p * S m) =>
let n0 := p * S m in
match H in (_ = y) return (m + p * m + S p = S (m + y)) with
| eq_refl =>
eq_ind (S (m + p * m + p)) (fun n1 : nat => n1 = S (m + (p * m + p)))
(eq_S (m + p * m + p) (m + (p * m + p))
(nat_ind (fun n1 : nat => n1 + p * m + p = n1 + (p * m + p))
eq_refl
(fun (n1 : nat) (H0 : n1 + p * m + p = n1 + (p * m + p)) =>
f_equal S H0) m)) (m + p * m + S p)
(plus_n_Sm (m + p * m) p)
end) n
: forall n m : nat, n * m + n = n * S m

Argument scopes are [nat_scope nat_scope]

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

More Related Content

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