Coqで集合論（集合の定義）

●概要

Coqによる集合論の形式化の紹介です。本稿では、部分集合の定義と軽い証明をお見せしようと思います。

●前提知識

集合論をなんとなく知ってて、CoqでのProp型の扱いが分かってれば、理解できると思います。以下、私が参考にした本・サイトです。

・ソフトウェアの基礎

前提知識なしでも読めるCoqのチュートリアル。

・Coq/SSReflect/MathCompによる定理証明

集合論の形式化を参照。

・集合位相入門（松坂）

集合論の各種定義を参照。

●集合の定義

Definition sets (M : Type):= M -> Prop.
Notation "[ M ]" := (sets M).

任意の型Mに対して、m : Mが集合に含まれるか判別する関数を、M型を母集合とする集合sets Mとして定義しています。

直感的に、関数を集合と見るのは違和感があると思います。「単なる型を集合とみなすと部分集合が扱えないから、都合が良いように集合を定義した」みたいな感じで、これがCoqでの集合なんだと思ってください。定義ってのは得てして便宜的なものです。

あと、 ここでのNotationに深い意味はないです。気分です。

●∈の定義

Definition member {M : Type }(A : [M]) (a : M) := A a.
Notation "a ∈ A" := (member A a) (at level 11).

集合の型(M -> Prop)から、A aがa ∈ Aを意味するのが分かると思います。つまり、集合Aに含まれるか判別する関数をaに適応した、って感じです。そのまんまですね。

●⊂ の定義

Definition sub {M : Type}(A B : [M]) :=
 forall x, x ∈ A -> x ∈ B.
Notation "A ⊂ B" := (sub A B) (at level 11).

ようやく数学らしくなってきたので、それっぽく書くなら、

 任意のｘに対して「x ∈ A ならば x ∈ B」が成り立つ時、AはBの部分集合であると言う。

って感じでしょうか。教科書的な定義通りに形式化できてるのが分かると思います。

●定理証明の例

A ⊂ B かつ B ⊂ C ならば A ⊂ C

という命題の証明です。

Theorem sub_trans {M : Type} (A B C : [M]) :
 A ⊂ B -> B ⊂ C -> A ⊂ C.
Proof.
 rewrite /sub /member.
 intros AB BC x Ax.
 apply BC.
 apply AB.
 apply Ax.
Qed.

簡潔ですね。日本語を使って厳密な証明をしようとすれば、便利さが実感できると思います。教科書的に言えば「読者への課題とする」といったお気持ちです。

●おわりに

本当は、写像にまつわる定理証明を載せてドヤ散らかすつもりでした。ただ、理解してくれる人が少ないのも寂しいので、教科書の順番通り記事にしてこうと思った次第です。次回記事を書くなら、和集合と積集合についてだと思います。

かしこ。