Coq による定理証明入門 ∗髙橋 真2023 年 4 月 26 日
この資料は定理証明支援系 Coq を利用して定理証明の初歩を分かりやすく解説する*1 ことを目的としています．

∗ この講義資料は JSPS 科研費 26560089 の助成を受けた研究の過程で得られたものです．
*1 ただし，プログラミング言語としての特徴については扱わないので，Coq の全体像については参考文献「ソフトウェアの基礎」[1] を参照してほしい．

目次
1

Coq

1

1.1

Coq とは . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1

1.2

Coq のインストール . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1

1.3

CoqIDE のウインドウ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1

1.4

基本的な枠組み2. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

論理式の証明2

2.1

命題論理 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2

2.2

述語論理 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

2集合の基本的性質の証明

3

20

3.1

ライブラリ Ensembles を利用した集合の性質の証明 . . . . . . . . . . . . . . 20

3.2

ライブラリーの作成と読み込み . . . . . . . . . . . . . . . . . . . . . . . . . 29

3.3

集合族 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
写像の性質の証明

4

33

4.1

像と逆像の定義. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

4.2

像の性質の証明. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

4.3

逆像の性質の証明 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
関係

5

38

5.1

同値関係 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

5.2

同値類 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
集合

A

44

A.1

部分集合と集合の相等A.2

空集合 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

A.3

集合の演算

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

B

集合族

45

C

写像

46

C.1

像 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46

C.2

逆像 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
関係

D
D.1

47

同値類 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

2017 年 11 月 4 日作成
2017 年 11 月 10 日修正2017 年 11 月 15 日修正（集合族と同値関係の追加）
2020 年 8 月 11 日修正（タクティクスと証明の見直しによる修正）2020 年 8 月 13 日修正（追加の修正）
2021 年 5 月 24 日修正（フォント指定のミスの修正）
2023 年 4 月 26 日修正（誤字の修正）

1 Coq
1.1 Coq とは
Coq はフランスの INRIA で開発されている定理証明支援系である．Coq の公式ページには以下のように記載されている．

Coq is a formal proof management system. It provides a formal language to write
mathematical deﬁnitions, executable algorithms and theorems together with anenvironment for semi-interactive development of machine-checked proofs. Typicalapplications include the certiﬁcation of properties of programming languages (e.g.
the CompCert compiler certiﬁcation project, or the Bedrock veriﬁed low-level programming library), the formalization of mathematics (e.g. the full formalizationof the Feit-Thompson theorem or homotopy type theory) and teaching.

1.2 Coq のインストール
Coq は https://github.com/coq/coq/releases よりダウンロードできる．Windows
OS や Mac OS X の場合はバイナリをダウンロードする．Linux 系の OS の場合は，パッケージ管理ツールを利用してインストールする．Coq のライセンスは GNU LGPL ライセンスである．

1.3 CoqIDE のウインドウ
Coq はコマンドラインでも実行可能であるが，ここでは CoqIDE を用いて説明する．
CoqIDE を起動すると 3 ペインのウインドウが開く．

1

左側が編集で，右上は仮定とゴールの表示，右下は情報を表示する．

1.4 基本的な枠組み
Coq を使用する場合，基本的なライブラリーは読み込まれているが，必要に応じて外部ラ
イブラリーを読み込むことができる（2.1.9 参照）．古典論理のライブラリーを読み込まない
限り，Coq で証明できるのは直観主義論理で証明できるもののみになる．Section 宣言は使
わなくてもよいが，局所的な変数を使う場合は必要になる．Section を宣言する場合は，

Section h セクション名 i.
のようにセクション名の後にピリオドをつける．Section の終わりは，

End h セクション名 i.
とする．また，書いた内容を反映させるためには，式の評価を行なう必要がある．単純な式の評価はメニューバーの下矢印をクリックする．あるいは Navigation メニュで Forward を選択してもよい．戻るにはメニューの上向き矢印（BackWard）を使う．他に全てを一度に評価したり (End)，先頭に戻したり (Start)，指定された場所まで評価を行う (Go to）ことができる．キーボードショートカットを使うのが便利である．キーボードショートカットで使用する Modiﬁer キーは，Edit->Preferences->Shortcuts で変更できる．

2 論理式の証明
2.1 命題論理
Coq では，すべての変数は型をもっている．例えば，Prop は命題の型を表していて，
A:Prop のように表し，変数 A が型 Prop をもつことを表す．
論理式を証明するときは，証明する論理式の前に，Goal, Theorem, Lemma などを書く．
証明した論理式を後で参照する必要のない場合は Goal でよいが，あとでその事実を証明に利用するのであれば，Theorem や Lemma にする．Theorem と Lemma に違いはなく，どちらにするかは気持ちの問題である．証明する論理式には名前を付ける*2 ．そのセクションで共通に使う変数は，Variable で宣言する．

Variable A B C:Prop.
命題 A, B に対し，A → (B → A) が成り立つことを証明する場合，

Lemma HA1:A->(B->A).
とする．論理結合子の → は Coq では，ハイフン-と大小記号>で表す．HA1 が論理式

A->(B->A) につけた名前*3 である．これらを評価すると Coq は proof-editing モードに入り，右上のペインに仮定とゴールが現れる．

*2 とりあえず定理証明する際に参照するための区別と考えればよいが，詳細は参考文献 [1], [2] を参照してほしい．
*3 この論理式は，ヒルベルトによる形式式的体系の公理の一つなので HA1 と名前をつけている．

2

証明を始める場合，Proof. を付けるが，付けなくてもよい．証明を終えたら（Coq が No

more subgoals. となったら）Qed. で終える．これで上記であれば，HA1 として，A->(B->A)が利用できる．

2.1.1 ゴールが含意の場合
実際に A->(B->A) を証明してみる．LJ の推論規則*4 の 右→ は，A, Γ ` B

(右→)
Γ`A→B
であるから， ` A → (B → A) を示すには，A ` B → A を示せば良い．このように A を仮定に入れて，ゴールを B → A に変更するには，intro タクティック*5 を用いる．intro. として評価するとそのように仮定とゴールが変換されることがわかる．

もう一度，intro を行うと，A, B ` A となり，ゴールと同じ仮定ができる．なお，評価した
タクティックの次は空白を入れる．入れないと先頭が赤字で表示され次の評価ができない．

ゴールと同じ仮定がある場合，LJ では始式から構造に関する推論規則で導かれるが，

Coq では trivial あるいは assumption を用いる．trivial. を評価すると No more
subgoals. となり証明が終了する．

*4 LJ あるいは LK については，参考文献 [3] を参照してほしい．Γ を論理式の列とするとき，Γ ⊢ X の直観的な意味は Γ を仮定すると X が導くことができることである．
*5 タクティックについては [4] を参照してほしい。

3

最後に Qed. で Lemma HA1 が登録される．

上記では，intro を 2 回続けたが，これは intros で 1 回で行うことができる．ただし，intros は単なる intro の繰り返しではない．2.1.6 で説明する．なお，intro を行うとCoq が自動的に仮定に入る論理式に名前をつけるが，H, H0 のように機械的な番号付になるので，自分で名前を付けたければ，intro K. のように指定できる．

仮定が多く出てくる場合は，このようにして名前を制御した方がよいが，このテキストでは記載を簡単にするため一部を除いて特に指定はしないで証明を進める．
今挙げた例のように Coq では，Γ ` A → B を証明するには，A, Γ ` B を証明すればよいというように，LJ の推論規則（あるいは LJ で許容される推論規則）を元にタクティックを用いてゴール変換を行いながら推論を進める．なお，基本はゴール変換による証明である
が，仮定を書き換えた方が良い場合もあるので，適宜ゴール変換と仮定の書換を交えて証明をすすめる．
以下，いくつかの例を用いながら，タクティックの説明をする．タクティックの名前を忘れた場合は，メニューの Tactics を見て探してほしい

2.1.2 ゴールが論理積のとき
Lemma Iand:A->(B->A/\B).
を証明しようとして，intros を行うとゴールが論理積 A/\B になる．なお，論理結合子の∧ は Coq では，スラッシュ/とバックスラッシュ\*6 で表す．

*6 日本語キーボードでは\は￥キーをタイプする．

4

ゴールが論理積 X ∧ Y の形のときは，split でゴールを X と Y の 2 つのゴールに分割
しそれぞれ証明する．これは，推論規則でいうと

Γ`A

Γ`B

Γ`A∧B

に対応している．今の例では，split で分割後，trivial で証明が終了する．

注意：ここでは説明のために intros してから，split したが，split の定義は intros をした後に apply conj を適用するものなので，最初の intros は不要でいきなり split を適用してもよい．

2.1.3 仮定に論理積があるとき
Lemma And1:A/\B -> Aを証明しようとして，intro を行うと，仮定に論理積 A/\B が入る．

仮定が論理積 X ∧ Y の形のときは，destruct あるいは inversion で仮定を分割する．
仮定にタクティックを適用する場合は，どの仮定に適用するか指定する．ここでの使い方での destruct と inversion の違いは，destruct が元の論理積が仮定に残らないのに対し，

inversion は元の論理積を仮定に残したままにすることである．

5

いずれにせよ，仮定にゴールと同じ論理式があるので，trivial で証明ができる．

これは推論規則として考えると，

Γ, A, B ` C
Γ, A ∧ B ` Cに対応している．

2.1.4 ゴールが論理和のとき
Lemma Or1:A-> A\/ Bを証明しようとして，intro を行うと，ゴールが論理和 A\/B になる．論理結合子の論理和∨ は Coq ではバックスラッシュとスラッシュである．

ゴールが論理和 X ∨ Y のときは，LJ では背理法が使えないので，証明できる論理式が Xであるか Y であるかを left, right で指定する必要がある．ここでは，A が仮定にあるので，left を選択する．

推論規則としては，

Γ`A
Γ`A∨B

6

Γ`B
Γ`A∨B
に対応している．背理法でないと証明できない場合については，2.1.9 で扱う．
注意：split のときと同様に，left はそもそも intros の後に apply or introl を適用するので，最初の intro は不要で，最初から left で証明できる．

2.1.5 仮定に論理和があるとき
Lemma EMDN:A\/˜A->(˜˜A -> A)を証明しようとして，intro を行うと，仮定に論理和 A\/˜A が入る．論理結合子の否定 ¬は，Coq ではチルダ˜で表す．

仮定が論理和 X ∨ Y の形のときは，destruct あるいは inversion で仮定を分離し，X の場合でも Y の場合でもいずれの場合でも証明できることを示す．推論規則では

Γ, A ` C
Γ, B ` C
Γ, A ∨ B ` Cに対応している．

この例では，A\/ ˜A を destruct あるいは inversion することでゴールが 2 つでき，Aを仮定する場合は trivial，˜A を仮定する場合は˜˜A が仮定にあり仮定が矛盾するので，

contradiction で証明できる．

7

2.1.6 ゴールが否定形のとき
Lemma Cont:(A->B)->(˜B -> ˜ A)を証明しようとして，intros を行うと，ゴールが否定形˜A になる．

Coq では，¬A は A → ⊥（Coq では ⊥ は False）の省略系である．従って，intro を使うことができる．

最初に適用した intros では， ˜A には適用されていなくて，明示的に intro を使う*7 ことで，A を仮定に入れることができている．仮定の˜B は B-> False であるから，False を示
すには，B を示せばよいことがわかる．推論規則としては，

Γ`XΓ, Y ` Y
Γ, X→Y ` Yに対応している．（上式右は明らかに成り立つので，上式左のみを示せばよい．
）これは apply
タクティックを使う．

再度，apply タクティックを使えば証明が終了する．

*7 このことからわかるように intros は intro の単なる繰り返しではない．

8

2.1.7 仮定に X と X → Y があるとき
Lemma HA2:(A->B)->((A->˜B)->˜A)を証明しようとして，intros を行い，続けて intro を行うと，仮定に A, A->B, A->˜B が入る．

仮定に X と X → Y があるとき，仮定を Y にすることができる．X を Y に書き換える
場合と X → Y を Y に書き換える場合でタクティックが異なる．specialize を用いて

specialize(H H1) とすると，仮定 H:A->B が B に変わる．

H:A->B を A から B への写像と考えて，H1:A の H1 を A の元だと考えると，H(H1) は B の元になるが，この H(H1) を (H H1) と表して，それを実際に計算させるのが specialize になっていると考えられる．

specialize ではなく，apply H in H1 とすると，仮定 H1:A が B に変わる．

今の場合，仮定 H1:A を書き換えると，論理式 A が消えて H0:A->˜B への適用ができなくな
る*8 ため，前者の specialize を用いることにする．specialize を H と H0 に続けて適用
すると，仮定に B と˜B が入り矛盾するので証明が終わる．

*8 後で説明する generalize と intro を使用して A のコピーを残しておけば apply でも証明はできる．

9注意：この例題では仮定を書き換える説明のために specialize を使った証明をしたが，absurd を用いる方が自然である．absurd は LJ で許容される推論規則Γ`AΓ ` ¬AΓ`⊥に対応している．absurd B. を適用すると，B と˜B の 2 つのゴールが生成され，仮定をapply することで証明が終わる．

2.1.8 同値式のとき
A ↔ B は (A → B) ∧ (B → A) の略記であるから、それに準じてタクティックを適用する．例えば、ゴールにある場合は split、仮定にある場合は destruct あるいは inversionを使う．
演習問題 1. 次の論理式が証明可能であることを Coq で示せ．

1. (A → (B → C)) → ((A → B) → (A → C))
2. ¬(A ∧ B) → (A → ¬B)
3. ((A ∧ B) → C) → (A → (B → C))
4. (B → A) → ((C → A) → ((B ∨ C) → A))
5. (¬A ∧ ¬B ↔ ¬(A ∨ B)
6. (¬A ∨ ¬B) → ¬(A ∧ B)

10

2.1.9 古典論理
ここまでは排中律 A ∨ ¬A を必要としない論理式を証明してきた．Coq では，特に仮定を置かない限り，直観主義論理 LJ で証明可能なものしか証明できない．排中律も証明することはできない．実際，排中律を証明しようとしても，ゴールが論理和の形であるから，left
か right しかタクティックが使えない．従って，排中律を仮定するしか，古典論理は扱えない．
古典論理を扱うために必要／便利な公理・定理を集めたライブラリーが Classical である．
ライブラリーを読み込むには次のように宣言する*9 ．

Require Import Classical.
このライブラリーでは，次のように公理，Lemma が扱われている．
Axiom classic : forall P:Prop, P \/ ~ P.
Lemma NNPP : forall p:Prop, ~ ~ p -> p.
Lemma Peirce : forall P:Prop, ((P -> False) -> P) -> P.
Lemma not_imply_elim : forall P Q:Prop, ~ (P -> Q) -> P.
Lemma not_imply_elim2 : forall P Q:Prop, ~ (P -> Q) -> ~ Q.
Lemma imply_to_or : forall P Q:Prop, (P -> Q) -> ~ P \/ Q.
Lemma imply_to_and : forall P Q:Prop, ~ (P -> Q) -> P /\ ~ Q.
Lemma or_to_imply : forall P Q:Prop, ~ P \/ Q -> P -> Q.
Lemma not_and_or : forall P Q:Prop, ~ (P /\ Q) -> ~ P \/ ~ Q.
Lemma or_not_and : forall P Q:Prop, ~ P \/ ~ Q -> ~ (P /\ Q).
Lemma not_or_and : forall P Q:Prop, ~ (P \/ Q) -> ~ P /\ ~ Q.
Lemma and_not_or : forall P Q:Prop, ~ P /\ ~ Q -> ~ (P \/ Q).
Lemma imply_and_or : forall P Q:Prop, (P -> Q) -> P \/ Q -> Q.
Lemma imply_and_or2 : forall P Q R:Prop, (P -> Q) -> P \/ R -> Q \/ R.

従って，このライブラリーを読み込むとこれらの Lemma を利用して証明することができる．
例えば，(˜B-> ˜A)->(A->B) は古典論理でないと証明できない論理式であるが，これを証明してみよう．intros を適用するとゴールが B になるが，このままでは適用できる仮定がない．

そこで，Classical の Lemma NNPP をゴールに適用する．apply NNPP. とすると Coq が今のゴール B に合わせて NNPP を適用する．

*9 Section 内でライブラリーを読み込むことは現在は推奨されていない．必要なライブラリーは Section 開

始前に宣言する．ここでは説明の都合上途中で宣言している．

11

ゴールが˜˜B になったので intro が適用でき，2.1.6 で使用した specialize または absurdを用いて証明ができる．

あるいは，Γ ` ¬AA, Γ ` ⊥は LJ で許容される推論規則だが，これに対応するタクティックである generalize を使うこともできる．

A->False は˜A のことなので，後は仮定の H を apply すれば証明できる．

ライブラリーの Lemma を使うもう一つの例として Peirce の論理式*10 ((A → B) → A) →A を証明してみよう．

*10 Classical の中にも Peirce という名前の Lemma があるが，それはこの論理式の特別の形で通常こちらをPeirce の論理式とよぶ．

12

intro をすると，仮定が (A->B)->A で結論が A になる．すぐに仮定を適用してゴールを
A->B にすると，証明できる形にはならない．古典論理でないと証明できない論理式なのでClassical の公理か Lemma の適用が必要である．証明の方法はいろいろあるが，ここでは，imply_to_or:forall P Q : Prop, (P -> Q) -> ~ P \/ Q. を仮定 H に利用してみる．タクティックの書き方は apply imply_to_or in H. である．

仮定が論理和に変わったので，destruct で分割する．仮定˜(A->B) は，imply_to_and が使えそうである．

演習問題 2. 次の論理式が古典論理で証明可能であることを Coq で示せ．

1. ¬(A ∧ B) → ¬A ∨ ¬B
2. ((A → ¬A) → B) → ((A → B) → B)
3. (¬B → ¬A) → ((¬B → A) → B
4. (A → B) ∨ (B → A)

（ヒント：最初に NNPP を使う．）

最 後 に End PropositionalLogic. で Section を 閉 じ る ．Section か ら 抜 け る と 、Section 内で変数として仮定されていたものが forall の形で Section 内の定義に自動的に付加される．次にメニューの File->Save でファイルを保存する．拡張子は.v にする．

Section を閉じると、Section 内で Variable として仮定されていたものに対して，その Section 外で，任意の論理式にあてはめて使用することができる．例えば，次のように

Section PropositionalLogic を閉じた後に，次のような Lemma を示すことができる．

13

apply (HA1 (X->Y) Z) は，Section PropositionalLogic で定義した HA1 の A として X->Y，B として Z を当てはめて適用することを示している．ただし，これは同一ファイル
内で行なっているのでそのまま使えているが，他のファイルの場合はコンパイルしてから，
その.vo ファイルを読み込む必要がある．詳しくは 3.2 で説明する．

2.2 述語論理
述語論理を Coq で扱うには，述語を定義する必要がある．述語は対象領域の要素が与えられると真偽が定まる命題になることを踏まえ，次のように宣言する．

ここで、A は対象領域を表しているが、どのような型に対しても適用できるように Type 型にしる．また、P,Q は A 上の 1 変数述語、R は A 上の２変数述語、t は A の要素としている．

2.2.1 仮定が全称論理式のとき
Lemma all imply:(forall x:A, P x)-> P tを証明しようとして，intro を行うと，仮定に全称論理式 forall x:A, P x が入る．

14

仮定が全称論理式の場合、任意の項に対して成り立つことが仮定できる．推論規則としては

Γ, P [t/x] ` CΓ, ∀xP ` Cに対応している．この例の場合は仮定 H を t に対して適用するため、apply (H t) とする．

2.2.2 ゴールが存在論理式のとき
Lemma imply exists:P t->(exists x:A,P x)を証明しようとして，intro を行うと，ゴールが存在論理式 exists x:A,P x になる．

ゴールが存在論理式の場合、古典論理でない限り、存在論理式をみたす項 t（witness とよぶ）を明示しなければならない．この例の場合は、witness として t を選択すればよいので、

exists t として t を適用する．

2.2.3 ゴールが全称論理式のとき
Lemma alpha all:(forall x:A, P x)-> forall y:A,P yを証明しようとして，intro を行うと，ゴールが全称論理式 forall y:A, P y になる．

15

ゴールが全称論理式の場合は、intro を行う．推論規則としては

Γ ` P [a/t]Γ, ` ∀xP（ただし、a は下式には現れない変数）に対応する．この推論規則では自由変数 a に変数条件があるが，Coq では intro を適用す
ると、自動的にそれまでに自由変数として使われていない新しい変数が用意される． 今の場
合 y は自由変数として使われていないので y がそのまま使われる*11 ．

後は、仮定 H を apply を適用して証明が終わる．

最後のところで使用した apply H. の代わりに，specialize (H y) と仮定を書き換えても証明できる．

ここで証明した ∀xP (x) → ∀yP (y) は，束縛変数を書き換えてもよいことを表す．このように束縛変数を書き換えることを α 変換とよぶ．

2.2.4 仮定が存在論理式のとき
Lemma all not not ex:(forall x:A, ˜P x)-> ˜exists x:A,P xを証明しようとして，intro を続けて行うと，仮定に存在論理式 exists x:A, P x が入る．

*11 言語で変数記号を自由変数と束縛変数に分ける場合もあるが，Coq では分けていないので注意する．

16

仮定が存在論理式の場合は destruct を行う．推論規則としては

Γ, P [a/x] ` CΓ, ∃xP ` C（ただし、a は下式には現れない）に対応する．Coq では destruct を適用すると、自動的にそれまでに自由変数として使われていない新しい変数が用意される．この例の場合 x は自由変数として使われていないので xがそのまま使われる．

後は仮定 H と x に apply を適用すると，ゴールが P x になり，trivial で証明が終わる．

ここでも最後のところで使用した apply (H x). の代わりに，specialize (H x) と仮定を書き換えても矛盾する論理式が仮定に現れるので contradiction で証明できる．

2.2.5 タクティックのカスタマイズ
既存のタクティックを自分用に改変したり、新たに作成することができる．ここでは長い
名前のタクティックを自分用の短い名前で定義し直す方法を述べる．タクティックは Ltacという Vernacular コマンドを用いて定義する．例えば、

17とすると、現在のゴールに対して、ok とすると、trivial や contradiction を適用する．
なお、セミコロンはタクティックの逐次適用になる．従って、ok を適用すると trivial を試した後で contradiction を行う．
演習問題 3. 次の論理式が証明可能であることを Coq で示せ．

1. ¬(∃xP ) → ∀x(¬P )2. ∃x(¬P ) → ¬(∀xP )3. ∀x(P ∧ Q) ↔ (∀xP ) ∧ (∀xQ)（ヒント：仮定に入った forall x, P x/\Q x を x:A
に対して destruct するには，destruct (H x) のように書く必要がある．destructではなく，specialize で仮定を書き換えることでもできる．

4. ∃x(P ∨ Q) ↔ (∃xP ) ∨ (∃xQ)
5. ∃x∀yR(x, y) → ∀y∃xR(x, y)2.2.6 古典論理でないと証明できない例
論理式 ¬(∀xP ) → ∃x(¬P ) は、証明に古典論理のライブラリー Classical が必要である．

証明を始める前に，上記の Lemma の記述で補足をする．これまで変数には型を付けてきたが，exists x の x には型が付いていない．これは Coq が x が P の引数になっていることから，型を推論して決定しているからである．実際，右のペインを見てみると変数には型がついているのがわかる．

intro を適用した時点で、ゴールに exists で適用できる項（変数）はなく、また仮定にある否定もはずすことができない．そこで Classical にある二重否定の除去 NNPP を用いて、ゴールに二重否定をつけ、intro で仮定に入れることにする．

18

これで仮定 H を適用することが可能になる．

ここで intro を行うと、また適用できるタクティックがなくなるので再度 NNPP を適用してintro を行う．

最後に仮定 H0 をゴールに適用すると、最初に適用できなかった exists が使える形になっていることがわかる．

二重否定の除去 NNPP の後に，intro を行うことは，背理法で証明することに相当する．
これは，LK で許容される推論規則¬A, Γ ` ⊥
Γ`Aに対応する．次のようにタクティック hairihou を定義しておくと，通常の証明と同じ感覚
で背理法を利用することができる．

演習問題 4. 次の論理式が証明可能であることを Coq で示せ．

1. ¬¬∃xP → ∃x(¬¬P )2. ¬∃x(¬P ) → ∀xP
3. ∃xA ↔ ¬∀x¬A19

4. ∃x(P (x) ↔ ∀yP (y))
演習問題 5. セクションを閉じて，ファイルを保存せよ．
最後にこれまで紹介してこなかった強力なタクティックの intuition について説明する．

intuition はライブラリの Tauto で定義されていて，Coq を起動すると自動的に読み込まれる．intuition はゴールや仮定からの推論が「明らか」なときに使えるタクティックで，これまでいろいろなタクティックを説明するためにあえて使ってこなかったが，命題論理のところで扱った例の多く（特に LJ で証明できるもの）は，intuition. だけで証明できた
り，証明が短縮できる．intuition がどのように定義されているかを説明しないが，自分で新たにタクティックを定義しようとする場合，よい参考になる．

3 集合の基本的性質の証明
3.1 ライブラリ Ensembles を利用した集合の性質の証明
3.1.1 ライブラリ Ensembles
Coq を用いて数学的な主張を証明するための例としてここでは集合のかんたんな性質を証明して行くことにする．集合を Coq でどのように扱うかであるが，（Coq には Set という型があるが）Library の Ensembles を使うことにする．Ensembles.v は Coq のインストー
ルフォルダ内にある．

Ensembles では次のように集合（Ensemble）を定義している．
Variable U : Type.
Definition Ensemble := U -> Prop.
U が全体集合で，その部分集合を Ensemble と定義していると考えることができる．
Ensemble は，この定義だと前節の述語論理での述語の扱いと変わらないが，これは U 上の述語とその述語をみたす元の集合の関係

R(a) ↔ a ∈ {x ∈ U | R(x)}(*)

を考えれば，同じ扱いでよいことがわかる．次は集合の要素関係 ∈ の定義である．

Definition In (A:Ensemble) (x:U) : Prop := A x.
これも上記の (*) を考えればこの定義でよいことがわかる．次は集合の包含関係の定義である．

Definition Included (B C:Ensemble) :Prop :=

forall x:U, In B x -> In C x.
これは通常の包含関係の定義である．次は全体集合と空集合の定義である．

20

Inductive Full set :Ensemble :=Full intro :Inductive Empty set :forall x:U, In Full set x.

Ensemble :=.

ここで Inductive は，対象を帰納的に定義する場合の用語である．Full set の定義にある Full intro はこの集合のコンストラクタ（この集合の元は何であるかを示すもの）で，Full set に関わる事実を証明する際に，この名前を用いて apply Full intro のように使うことができる．一方，Empty set には何も書かれていない．これはコンストラクタがない（つまり何もないから空である）ことを表している．
空集合と全体集合を Inductive ではなく Definition で定義すると次のようにできる．
この二つの定義の同等性は後で証明する．

Definition Full set :Ensemble := fun x:U=>True.

Definition Empty set :Ensemble := fun x:U=>False.

fun x:A=>y は写像の対応関係でよく使われる x 7→ y を表している．従って，Definition
による定義は，Ensemble の型である U->Prop が，U から Prop への写像であると考えると自然な定義である．Inductive で定義した場合と Definition で定義した場合で証明で使うタクティックが変わるが，説明は具体的な証明の中で行う．
集合に関する演算の和集合 (union)∪，共通部分 (intersection)∩ は次のように Inductiveに定義する．

Inductive Union (B C:Ensemble) :Ensemble :=| Union introl :forall x:U, In B x -> In (Union B C) x

| Union intror :forall x:U, In C x -> In (Union B C) x.

Inductive Intersection (B C:Ensemble) :Ensemble :=Intersection intro :forall x:U, In B x -> In C x -> In (Intersection B C) x.
集合 B と C の和集合の元は，B の元であるか C の元のいずれかであることと定義され，共通部分は B の元かつ C の元であることと定義されている．ライブラリ Ensembles で定義されている他の演算の定義については，集合の基本的な性質を証明しながら説明する．

3.1.2 基本的性質の証明
ここで証明する集合の性質は，集合と写像に関する授業資料*12 から抜粋したもので，付録に掲載をしている．定理や問題番号はそれに沿っているので適宜参照してほしい．なお，この先 Unicode の記号を利用するため，メニューの Edit->Preferences を選び，Files の Filecharset encoding が UTF-8 になっているか確認し，UTF-8 でない場合は UTF-8 を選択する必要がある．（選択後 OK をクリックする．）*12 http://herb.h.kobe-u.ac.jp/nst/

21

最初に Ensembles をインポートする．背理法を使うことがあるので，Classical もインポートする．また，論理のところで定義した 2 つのタクティックも使えるようにする．また，集合の型を Ensemble と書くのは面倒なので，略記を用意する．

Coq で証明するときに見やすいように，最初に Notation で略記を定義する．2 項演算を定義するときは，結合の強さと結合の順序を定義する必要がある．ここでは複合命題を表現するときに，仮定やゴールの表示でカッコを省略せずそのまま表示するようにするためにす
べて no associativity で指定しておく．また，この後，証明する命題の主張を簡潔にするため，使用する変数も定義する．

集合の元であるかないかを示すには排中律が必要になる．

22

x が集合 A の元であるかどうかで場合分けするには，この in or not が必要になる*13 ．
Coq の章の述語論理のところで述べたように，Coq が型を推論できる部分は表現を簡潔にするために上記のように型を省略することにする．以下，付録にある集合や写像の性質を Coq
を用いて証明をしていく．
命題 A.1 A ⊆ B かつ B ⊆ C ならば A ⊆ C.
最 初 に 部 分 集 合 の 包 含 関 係 Included を 定 義 に 従 っ て 分 解 す る ．こ れ は unfold

Included を行う．

次に intros. を行う．これで現在の状況はである．あとは，destruct H を行い分解された仮定を使えば証明が終了する．

Included の分解はよく行うので，タクティックとして定義する．

定理 A.2 空集合は任意の集合の部分集合である．すなわち，任意の集合 A に対し，∅ ⊆ Aが成り立つ．
証明は，intro.

bubun.

destruct H. で終わる．

*13 この資料で使用するのは．問題 A.8 の証明のところである．

23

ここで扱う集合は全体集合の部分集合であるのでそれも示示す．

証明で注意すべき点は，intro;bubun. を行った後，Full set の定義のコンストラクタである Full intro を使うことである．apply Full intro とすると，結論が一気に証明できる．なお，split は intros した後に，ただ一つのコンストラクタを適用することなので，
この Lemma は split とするとすぐに証明が終わる．

今後集合の同等性を示すことが多くなるが，それには外延性の定理を用いる．

Axiom Extensionality Ensembles :forall A B:Ensemble, Same set A B -> A = B.
ここで，Same set の定義は，Definition Same set (B C:Ensemble) :Prop :=

Included B C /\ Included C B.
であるから，通常の外延性定理 ∀A, B[A ⊆ B ∧ B ⊆ A → A = B] である．ゴールに入る/\を分解することまで含め，次のようにタクティック seteq を定義する．今後集合の同等性を示す場合は最初にこの seteq を使用する．

定理 A.3 集合 A, B, C に対し，次の関係式が成り立つ．

1. A∪A = A
2. A∪B = B∪A
3. A∪(B∪C) = (A∪B)∪C
4. A ⊆ A∪B, B ⊆ A∪B
5. A, B ⊆ C → A∪B ⊆ C
証明で注意することは和集合のコンストラクタ Union introl と Union intror の使い

24

方だけであるが，left や right は intros した後にそれぞれコンストラクタの 1 と 2 を適用するものなので，left と right を使用するほうが簡単である．より一般的には，n 番目のコンストラクタを適用する constructor n を用いて，constructor 1 や constructor

2 でも構わない．証明を後で見直す時に，Union introl と Union intror と書いてある方が見やすいということだけである．

seteq の後最初のゴールは簡単で 2 つ目のゴールの証明で bubun を適用すると次のようになる．

ここで apply Union introl あるいは left を適用する*14 ．するとゴールが x ∈ A に変換されて証明ができる．

A.3 の 3 の証明では，仮定に∪がある場合は destruct で分解される（\/と同じ）こととUnion introl と Union intror の使い分けに気をつける．

演習問題 6. 定理 A.3 の 4 と 5 及び問題 A.4 の左から右を証明せよ．
問題 A.4 の右から左を示すときに，タクティックの新しい使い方が必要になる．intro を行うと次の状況になる．

ここで仮定に対して，destruct H を適用すると，ゴールが A ⊆ A ∪ B に変わる．これは，仮定 H を利用してゴールの B を A ∪ B に書き換えたことになる．明示的に等式を利用し*14 この場合は apply

Union intror あるいは right でも良い．

25

て書き換えるタクティックは rewrite である．rewrite は仮定にある等式の左式を右式に置き換えるが，今回のように右式を左式に置き換えるには rewrite <-を用いる．rewrite

H ではなく，rewrite <- H とするとゴールが確かに変わる．

あとは定理 A.3 の 4 の最初の式を用いれば良い．（以下の証明では，定理 A.3 の 4 の最初の式の命題の名前を bubun unionl としている．

定理 A.5 集合 A, B, C に対し，次の関係式が成り立つ．

1. A∩A = A
2. A∩B = B∩A
3. A∩(B∩C) = (A∩B)∩C
4. A∩B ⊆ A, A∩B ⊆ B
5. C ⊆ A, B → C ⊆ A∩B
6. A ⊆ B ↔ A∩B = A
証明は，使うタクティックが Intersection intro であることを除けば，和集合と同じようにできる．この場合も split がコンストラクタの 1 を適用するものなので，apply

Intersection intro よりも split を使用する方が簡単である．
演習問題 7. 定理 A.5 を証明せよ．

Ensembles では，Disjoint は次のように定義されている．
Inductive Disjoint (B C:Ensemble) :Prop :=Disjoint intro :forall x:U, ˜In (Intersection B C) x) -> Disjoint B C.
すなわち，B ∩ C に元がないときに，Disjoint B C と定義している．よって，Disjoint
ならば共通部分は空集合になるが，それを示すのが次の Lemma である．

26

specialize で仮定を書き換えるのは論理のところで行ったのと同じである．ここでもapply Disjoint intro ではなく split を使うことができる．rewrite H in H0 は等式H を用いて，仮定 H1 を書き換えるときの書き方である．
演習問題 8. 定理 A.6 と問題 A.7 の左から右を証明せよ．
次に問題 A.7 の右から左を証明する．

この時点で仮定とゴールを見ると，，仮定 H0 より x ∈ A ∪ B が成り立ち，さらに仮定 H
より x ∈ B ∩ C となり x0 ∈ B が証明できることがわかる．しかし，これを実現するためには，x ∈ A ∪ B が仮定にないといけない．このような証明の途中に必要な事実を入れるにはassert あるいは cut を用いる．
assert (x ∈ (A ∪ B)).
を評価すると，ゴールが x ∈ A ∪ B になる．

証明が終了するとこれが仮定に入る．

27

後はこれまでと同様に証明を行えばよい．cut の場合は，証明の順序が逆になる．cut (x∈ (A ∪ B)). とすると，さきに，これを用いて証明するモードになり，終わると x ∈ A ∪B を証明するモードに入る．
いずれを用いても，後は仮定に入れた x ∈ (A ∪ B) により証明ができる．

差集合 Seminus は Definition で次のように定義されていて，和集合や共通部分のようなコンストラクタがないため，unfold を多用する必要がある．

Definition Setminus (B C:Ensemble) :Ensemble :=fun x:U => In B x /\˜In C x.
コンストラクタの代わりになる Lemma を証明しておくと便利である．差集合の記号は以下のように定義する．

差集合についてもこれまでの同様に証明ができるがこの節の最初に説明したように

in or not を使う必要のあるものがいくつかある．その一つが問題 A.8 の (A − B) ∪ (A ∩B) = A である．
この問題は A ⊆ (A − B) ∪ (A ∩ B) を示す時に，x ∈ B の場合と x ∈/ B の場合に分けて証明する必要が出てくる．

28

このときのゴールは x ∈ (A \ B) ∪ (A ∩ B) であるが，仮定に B に関する情報がないため，和集合のどちらに入るか決定することができない．そこでdestruct (in or not B x)とすることで x ∈ B の場合と˜(x ∈ B) の場合に分けることができて証明が完成する．

ここで前に言及した Full set と Empty set を Inductive と Definition で定義したものの同等性を示しておく．具体的には次の 2 つの Lemma になる．証明は特に難しいことはない．これらにより，Full set U は，fun x:U => True であり，Empty set は fun x:U=> False であることがわかる．

演習問題 9. 付録 A の残りの定理と問題を証明しなさい．
最後に Section を終了する．

End SetTheory.
集合に関してここまで証明したものを Shugo.v として保存する．

3.2 ライブラリーの作成と読み込み
3.2.1 ライブラリーの作成
自分で定理を証明したものをライブラリーとして作成するには，ファイル（.v ファイル）を開いた状態でメニューの Compile から Compile buﬀer を選ぶ．これで同じディレクトリ
に.vo ファイル（と.glob ファイル）が生成される．ライブラリを読み込むときに使用するの29

はこの.vo ファイルである．
前節で作成した Shugo.v を Compile して，新しいライブラリを作成する．作成したライ
ブラリを読み込んだときに，新たに作成したタクティックと集合演算の記法がそのまま使えるように，Shugo.v の End SetTheory の後に以下のものを記述した後に Compile を行い，ライブラリを作成する．

Ltac ok:=trivial;contradiction.
Ltac hairihou:=apply NNPP;intro.
Ltac seteq:=apply Extensionality Ensembles;unfold Same set;split.
Ltac bubun:=unfold Included;intros.
Notation "x ∈ A":=(InA x)(at level 50,no associativity).

Notation "A ⊆ B":=(Included
Notation "A ∪ B" :=(Union

A B)(at level 100,no associativity).
A B)(at level 80, no associativity).

Notation "A ∩ B":=(Intersection
Notation "A \ B":=(Setminus
Notation ø :=(Empty set).

Notation Ω:=(Full set).

A B)(at level 80, no associativity).

A B)(at level 60, no associativity).

3.2.2 ライブラリの読み込み作成したライブラリを読み込むには，ライブラリーの置かれているフォルダーを LoadPath
で指定してから，Require Import を用いる．例えば，hogehoge.vo を置いたフォルダの絶対パスを PATH とするとき，hogehoge を読み込むには

Add LoadPath "PATH".
Require Import hogehoge.
とする．

3.3 集合族
自分で作成したライブラリーの利用の演習も兼ねて，集合族のかんたんな性質を証明する．
まず最初に必要なライブラリー Shugo を読み込む．Windows 10 の場合はのように書く．ここでは C:\Users\makoto\Documents\coq にライブラリーがおかれていることにしている．Mac OS X の場合は30のように書く．ここでは/Users/makoto/Desktop/Coq にライブラリーがおかれていることにしている．
一般に集合 Λ の元 λ に対して，集合 Fλ が決められているとき，{Fλλ ∈ Λ} を Λ を添

字の集合とする集合族とよぶ．添字の集合は空ではないと仮定する．
ここでは，集合族の Coq における定義を次のように考えることにする．

集合族 {Fλλ ∈ Λ} に対し，Fλ のいずれかの元となるようなものの全体，すなわちS∃λ ∈ Λ[a ∈ Fλ ] をみたす a の全体を {Fλ λ ∈ Λ} の和集合とよび， {Fλ λ ∈ Λ} あるい[はFλ で表す．また，集合族 {Fλ λ ∈ Λ} に対し，Fλ のすべてに共通な元の全体，すなλ∈Λ

わち ∀λ ∈ Λ[a ∈ Fλ ] をみたす a の全体を {Fλ

\

あるいは

T
λ ∈ Λ} の共通部分とよび， {Fλ λ ∈ Λ}

Fλ で表す．

λ∈Λ

このことを踏まえ，集合族の和集合と共通部分の Coq における定義を次のようにする．

集合族については次の定理 B.1, B.2 が成り立ちますが，これを Coq で確かめてみる．
定理 B.1 集合族 {Fλ1. Fλ0 ⊆2.

\[

λ ∈ Λ} と集合族の構成元 Fλ0 に対し，次が成立する．

Fλ(λ0 ∈ Λ)Fλ ⊆ Fλ0(λ0 ∈ Λ)λ∈Λλ∈Λ

定理 B.2 集合族 {Fλ

1.

\
λ∈Λ

Fλ ⊆

\

λ ∈ Λ},{Gλ λ ∈ Λ} に対し，次が成立する．
Gλ ↔ ∀λ ∈ Λ[Fλ ⊆ Gλ ]

λ∈Λ

31

2.

[
λ∈Λ

Fλ ⊆

[

Gλ ↔ ∀λ ∈ Λ[Fλ ⊆ Gλ ]λ∈Λ

この証明は，和集合と共通部分のコンストラクタ unionf intro と interf intro を使
うところに注意をすれば特に難しいことはない．

次に，定理 B.3 を確かめてみる．
定理 B.3 集合族 {Fλλ ∈ Λ} と集合 A に対し，次が成立する．
A∪(\Fλ ) =λ∈Λ\(A ∪ Fλ )λ∈Λ

この定理を Coq で表現するためには，集合族 {A ∪ Fλ }λ∈Λ を定義する必要がある．この定義は，Definition で行う．各 λ ∈ Λ に対して，A ∪ Fλ を対応させることに注意する．

証明中で UFam を定義に従って書き換えるとき，ゴールにある場合は unfold UFam. とし，仮定 H にある場合は unfold UFam in H. とする．
定理 B.3 を証明する際に，問題となる箇所は次の部分である．

32

ゴールは和集合なので，どちらに入るか決めないといけないが，この時点の仮定ではどちらに入るか決めることはできない．そこで in or not を用いて，x ∈ X の場合と x ∈/Xの場合分けを行う．後は特に難しいところはない．

演習問題 10. 問題 B.4 を示せ．ただし，集合族 {A ∩ Fλ }λ∈Λ は次のように定義する．証明
中で IFam を書き換えるは，UFam と同様に unfold を使用する．

また，添字集合が空でないことを明示するために，以下の宣言をする．

最後にファイルをファイル名を Family.v にしてコンパイルせよ．コンパイルしたファイ
ルは，同値関係のところで Import する．

4 写像の性質の証明
ここで証明する写像の性質は，集合と同様 http://herb.h.kobe-u.ac.jp/nst/から抜粋したもので，付録 C に掲載をしているものである．

4.1 像と逆像の定義
集合族の性質の証明と同様に，ライブラリをインポートする．

写像は定義域と値域の集合を型としては区別する必要があるため，次のように UShugo とVShugo を定義する．Set Implicit Arguments を宣言すると，型が推論できるような引数
33

を省略することができる．

f : A → B と C ⊆ A, D ⊆ B に対し，f による C の像 f (C) と f による D の逆像
f −1 (D) は次のように定義される．
f (C) = {f (a) | a ∈ C}, f −1 (D) = {a ∈ A | f (a) ∈ D}
よって，Coq では次のように定義するのが自然である．

4.2 像の性質の証明
まず最初に x ∈ X ならば f (x) ∈ f (X) であることを示す．証明は直線的にできる．

定理 C.3 f : U −→ V とする．A, B ⊆ U とするとき，次の関係が成り立つ．

1. A ⊆ B → f (A) ⊆ f (B)
2. f (A ∪ B) = f (A) ∪ f (B)
3. f (A ∩ B) ⊆ f (A) ∩ f (B)
順に証明すると次のようになる．いずれも集合で証明したときに用いたことと像のコンス

34

トラクタから証明ができる．証明中では像のコンストラクタを直接適用しているのではなくsplit で代用している．特に共通部分に関わるところでは，像のコンストラクタを使うところと共通部分のコンストラクタを使うところをどちらも split で代用しているので，どちらを使用しているのか注意せよ．

4.3 逆像の性質の証明
次に逆像に関することを証明してみる．まず最初に，x ∈ f −1 (Y ) ↔ f (x) ∈ Y を示す．
証明は逆像のコンストラクタを用いることで容易にできる．ここでも逆像のコンストラクタを指定する代わりに split で代用している．

次に，f −1 (Y ) = f −1 (f (U ) ∩ Y ) を示す．

定理 C.6 f : U −→ V とする．C, D ⊆ U とするとき，次の関係が成り立つ．

1. C ⊆ D → f −1 (C) ⊆ f −1 (D)352. f −1 (C ∪ D) = f −1 (C) ∪ f −1 (D)
3. f −1 (C ∩ D) = f −1 (C) ∩ f −1 (D)
1. の証明では，特に難しいところはない．

2. は集合の同等性を証明するので，これまで同様にすすめるととなる．ここで，f (x) ∈ C ∪ D ↔ f (x) ∈ C ∨ f (x) ∈ D を使うために仮定 H を使いたい
が，そのまま destruct H とすると，f (x) の情報も失われてしまう．

そこで destruct ではなく inversion H. とする．そうすると，f (x) の情報も保存されるので証明が進む．

destruct を使う場合は，一旦 y = f (x) とおいて，変数 y にしてから destruct することにする．そのために使うのが remember タクティックである．remember (f x) as y と36

することで，仮定に Heqy:y = f x が追加され，destruct H. の後に rewrite すると，

仮定が実質 f x ∈ C と f x ∈ D に場合分けされる．

しかし，このようなことをしなくても，inversion で簡単にできる．
後は，同様に証明をすすめることできる．

3. も同様にできる．

演習問題 11. 問題 C.7 を示せ．なお，U, V を集合として扱う場合は，(Full set U),(Full set V) とすることに注意せよ．

37

5 関係
この章では関係を扱う．ここで証明する関係の性質は，集合と同様授業資料*15 から抜粋したもので，付録 D に掲載をしているものである．集合と集合族に関する概念を必要とするのでライブラリ Shugo, Family を読み込む．

5.1 同値関係
2 項関係 R は，次の条件 R1,R2,R3 を満たすとき，それぞれ反射的 (reﬂexive)，対称的(symmetric)，推移的 (transitive) であるという．
R1: ∀a ∈ A[aRa]R2: ∀a, b ∈ A[aRb → bRa]
R3: ∀a, b, c ∈ A[aRb ∧ bRc → aRc]
Coq でも次のように定義する．

反射的，対称的かつ推移的である関係を同値関係 (equivalence relation) とよぶ．

*15 http://herb.h.kobe-u.ac.jp/nst/

38

5.2 同値類
R を A 上の同値関係とする．任意の a ∈ A に対し，a と同値な関係にある A の元全体を[a] で表すことにする．すなわち，[a] := {b ∈ A aRb}
とおく．[a] の形の集合を同値類 (equivalence class) とよび，a をその同値類の代表元とよぶ．代表元の取り方は，一意的には決まらない．Coq で同値類を定義するためには，最初に同値関係を決めておく必要がある．そのために Hypothesis を用いる．

これにより，これ以降 R は同値関係として仮定される．Coq で仮定にある同値関係を反射
的，対称的，推移的のそれぞれの関係にわけるタクティック eqrel を次のように定義する．

ここで，destruct equiv as [ref symtran] は，Equivalent relation R を destruct
したときに，最初の仮定 Reflexive R に ref というラベルをつけ，残りの Symmetric R/\Transitive R に symtran といラベルをつけることを表す．さらに destruct symtranas [sym tran] により，対称律と推移律の式に sym と tran のラベルがつけられることになる．
その上で，同値類を次のように定義する．

xRx であるから，x ∈ [x] となるがこれを最初に確認する

eqrel で同値関係の性質を 3 つにわける．

39

同値類のコンストラクタ eqclass intro でゴールを変換する．

反射律 ref を用いれば証明終了である．

次に xRy ならば [x] ⊆ [y] を示す．

結論と仮定の H と H0 を見ると，推移律を適用できそうであるが，推移律を適用するには仮定 H の変数の順序を入れ替える必要があるので，sym を用いる．

40

これで推移律が適用できるので証明が終わる．

tran に引数を与えているのは，どの順で適用するか指示する必要があるからである．
tran に引数が必要な理由は，Transitive の定義がで，apply tran を行うときの仮定とゴールの状況が Γ, R y x, R x y0 ` R y y0 だったからである．そこで，仮定にある H0:R x y0 を intro の逆の操作を行う revert を使い revert

H0 とすると，tran を適用できる形になり apply tran. で証明ができる．

定理 D.1 A 上の同値関係 R の同値類に関して次が成り立つ．

41

1. ∀a, a′ ∈ A(aRa′ → [a] = [a′ ])2. ∀a, a′ ∈ A(¬(aRa′ ) → [a] ∩ [a′ ] = ∅)[3.
[a] = Aa∈A

1. は演習問題とする．2. を証明する．

ここで absurd (R x y) として，∼R x y と R x y のいずれも導かれることを示す．∼R x

y は明らかで，R x y は H1 を revert してから，tran を apply して証明ができる．あるいは，specialize で仮定を書き換えて矛盾を出す方針でも構わない．

3. の証明には，Family.v で定義した集合族の和集合を用いる．3. の左辺はここでの定義に従えば，集合族 {[x] | x : U } の和集合であるから，最初にこの集合族を次のように定義する．

これを踏まえて，証明すべき命題と証明は次のようにできる．

演習問題 12. 定理 D.1 の 1. を示せ．

42

参考文献
[1] Software Foundations, B. C. Pierce, C. Casinghino, M. Greenberg,
V. Sjŏberg, B. Yorgey, Vol.1, Vol. 2, Vol.3,
https://softwarefoundations.cis.upenn.edu（2020 年 6 月 5 日閲覧）
（日本語訳）ソフトウェアの基礎, 梅村晃広、片山功士、水野洋樹、大橋台地、増子萌、今井宜洋訳，http://proofcafe.org/sf/（2020 年 6 月 5 日閲覧）

[2] An experiment in modernizing Coq’s manual.
http://web.mit.edu/cpitcla/www/coq-rst/index.html（2020 年 6 月 5 日閲覧）
[3] 情報科学における論理, 小野寛晰著, 日本評論社[4] Tactic Index ― Coq 8.12.0 documentation,
https://coq.inria.fr/refman/coq-tacindex.html, (2020 年 8 月 11 日閲覧)

43

付録A

集合

A.1

部分集合と集合の相等

A.1.1

部分集合

命題 A.1. A ⊆ B かつ B ⊆ C ならば A ⊆ C

A.1.2

集合の相等

A ⊆ B かつ B ⊆ A ならば，∀x[x ∈ A ↔ x ∈ B] が成り立つから外延性の公理より，
A = B である．

A.2

空集合

定理 A.2. 空集合は任意の集合の部分集合である．すなわち，任意の集合 A に対し，∅ ⊆ Aが成り立つ．

A.3

集合の演算

A.3.1

和集合

定理 A.3. 集合 A, B, C に対し，次の関係式が成り立つ．

1. A∪A = A
2. A∪B = B∪A
3. A∪(B∪C) = (A∪B)∪C
4. A ⊆ A∪B, B ⊆ A∪B
5. A, B ⊆ C → A∪B ⊆ C
問題 A.4. A ⊆ B ↔ A∪B = B を示せ．

A.3.2

共通部分

定理 A.5. 集合 A, B, C に対し，次の関係式が成り立つ．

1. A∩A = A
2. A∩B = B∩A
3. A∩(B∩C) = (A∩B)∩C
4. A∩B ⊆ A, A∩B ⊆ B
5. C ⊆ A, B → C ⊆ A∩B
6. A ⊆ B ↔ A∩B = A
44

A∩B = ∅ のとき，A と B は 互いに素 (mutually disjoint) であるとよばれる．
A.3.3

和集合と共通部分の関係

定理 A.6. 集合 A, B, C に対し，次の関係式が成り立つ．

1. A∪(B∩C) = (A∪B)∩(A∪C)
2. A∩(B∪C) = (A∩B)∪(A∩C)
3. A∪(A∩B) = A,A∩(A∪B) = A

問題 A.7. A ⊆ B ⊆ C ↔ A ∪ B = B ∩ C を示せ．

A.3.4

差集合

定義より A − B ⊆ A, (A − B) ∩ B = ∅ が常に成り立つ．
問題 A.8. (A − B) ∪ (A ∩ B) = A を示せ．
命題 A.9. A ⊆ C かつ D ⊆ B ならば A − B ⊆ C − D
問題 A.10. A ⊆ B ↔ A − B = ∅ であることを示せ．
問題 A.11. A − (A − B) = A ∩ B を示せ．
問題 A.12. A, B ⊆ C とする．A ∩ B = ∅ ↔ A ⊆ C − B を示せ．
問題 A.13. (A − C) ⊆ (A − B) ∪ (B − C) を示せ．
定理 A.14 (ド・モルガンの法則). 集合 A, B, C に対し，次の関係式が成り立つ．

1. A − (B∪C) = (A − B)∩(A − C)
2. A − (B∩C) = (A − B)∪(A − C)問題 A.15. 次を示せ．

1. (A∪B) − C = (A − C)∪(B − C)
2. (A∩B) − C = (A − C)∩(B − C)
3. (A∩C) − B = (A − B)∩C
4. (A∪C) − B ⊆ (A − B)∪C

付録B

集合族

定理 B.1. 集合族 {Fλλ ∈ Λ} と集合族の構成元 Fλ0 に対し，次が成立する．

45

1. Fλ0 ⊆
2.

\

[

Fλ

(λ0 ∈ Λ)Fλ ⊆ Fλ0(λ0 ∈ Λ)λ∈Λλ∈Λ

定理 B.2. 集合族 {Fλ

1.

\
[

Fλ ⊆

λ∈Λ

2.

\
[

λ ∈ Λ},{Gλ λ ∈ Λ} に対し，次が成立する．

Gλ ↔ ∀λ ∈ Λ[Fλ ⊆ Gλ ]

λ∈Λ

Fλ ⊆

λ∈Λ

Gλ ↔ ∀λ ∈ Λ[Fλ ⊆ Gλ ]λ∈Λ

定理 B.3. 集合族 {Fλλ ∈ Λ} と集合 A に対し，次が成立する．
A∪(\Fλ ) =λ∈Λ\(A ∪ Fλ )λ∈Λ

問題 B.4. 集合族 {Fλλ ∈ Λ} と集合 A に対し，次が成り立つことを示せ．
[[
1. A ∪ (Fλ ) =(A ∪ Fλ )\λ∈Λ

2. A ∩ ([Fλ ) =λ∈Λ

3. A ∩ ([(A ∩ Fλ )λ∈ΛFλ ) =

λ∈Λ

付録C

\

λ∈Λ

(A ∩ Fλ )

λ∈Λ

写像

C.1 像
命題 C.1. f : U −→ V, X ⊆ U とする．x ∈ X ならば f (x) ∈ f (X) である．
命題 C.2. f : U −→ V, X ⊆ U とする．y ∈ f (X) であるための必要十分条件は ∃x ∈X[y = f (x)] である．
定理 C.3. f : U −→ V とする．A, B ⊆ U とするとき，次の関係が成り立つ．

1. A ⊆ B → f (A) ⊆ f (B)
2. f (A ∪ B) = f (A) ∪ f (B)
3. f (A ∩ B) ⊆ f (A) ∩ f (B)C.2 逆像命題 C.4. f : U −→ V, Y ⊆ V とする．∀x ∈ U [x ∈ f −1 (Y ) ↔ f (x) ∈ Y ] である．
命題 C.5. f : U −→ V, Y ⊆ V とする．f −1 (Y ) = f −1 (Y ∩ f (U )) である．

46

定理 C.6. f : U −→ V とする．C, D ⊆ U とするとき，次の関係が成り立つ．

1. C ⊆ D → f −1 (C) ⊆ f −1 (D)
2. f −1 (C ∪ D) = f −1 (C) ∪ f −1 (D)
3. f −1 (C ∩ D) = f −1 (C) ∩ f −1 (D)問題 C.7. f : U −→ V とする．C, D ⊆ V とするとき，次の関係が成り立つことを示せ．

1. f −1 (V − C) = U − f −1 (C)
2. f (f −1 (C)) = C ∩ f (U )3. C ∩ f (U ) ⊆ D ∩ f (U ) ↔ f −1 (C) ⊆ f −1 (D)

付録D

関係

D.1 同値類
定理 D.1. A 上の同値関係 R の同値類に関して次が成り立つ．

1. ∀a, a′ ∈ A(aRa′ → [a] = [a′ ])2. ∀a, a′ ∈ A(¬(aRa′ ) → [a] ∩ [a′ ] = ∅)[3.
[a] = Aa∈A

問題 D.2. 定理 C.1 の 1. の逆を示しなさい．

47