はじめに

Coq で集合を扱う標準ライブラリEnsemblesの再開発を行います。 勉強のため auto.を使わないで証明を行います。

集合論

Section Ensembles.

  (* ここにコードを書く *)

End Ensembles.

集合とは

1 変数の述語を用いて集合論を定義する。

Variable U : Type.
Definition Ensemble := U -> Prop.

U は述語の変数の型であり、Ensemble は U を受け取って命題を返す 1 変数の述語である。 今回は Ensemble を集合とする。

∈ を定義

元 a が集合 A に含まれるということは、変数 a と 1 変数の述語 A について A(a)ということである。

例): 「ソクラテスが人間という集合に含まれる。」は、「ソクラテスが人間ある。」ということである。

Definition In (A : Ensemble) (a : U) : Prop := A a.
Notation "a ∈ A" := (In A a) (at level 55,no associativity).
Notation "a ∉ A" := (~ In A a) (at level 55,no associativity).

Notation を定義すると楽しくなってきますね。

排中律を示す。 その前に

Require Import Classical.

を Section の一番最初に追加しましょう。 (Coq は直観論理なので Classical を Import しないと排中律を示すことが出来ない。)

Lemma excluded_middle : forall A : Ensemble , forall a : U, (a ∈ A) \/ (a ∉ A).
Proof.
  unfold In.
  intros.
  apply classic.
Qed.

unfold は定義を展開する Tactic である。

⊆ を定義

A ⊆ B は任意の A の元は B に含まれることである。

Definition Include (A : Ensemble) (B : Ensemble) : Prop := forall a : U, a ∈ A -> a ∈ B.
Notation "A ⊆ B" := (Include A B) (at level 54, no associativity).

⊆ の反射律と推移律を示す。

Lemma reflexive : forall A : Ensemble, A ⊆ A.
Proof.
  unfold Include.
  intros.
  trivial.
Qed.

Lemma transitive : forall A B C : Ensemble, A ⊆ B /\ B ⊆ C -> A ⊆ C.
Proof.
  unfold Include.
  intros.
  destruct H.
  specialize (H a).
  specialize (H1 a).
  apply H1.
  apply H.
  trivial.
Qed.

auto.を使うと楽に証明できる。

≡ を定義

「A ≡ B」は「A ⊆ B かつ B ⊆ A」ということである。

Definition Same_set (A : Ensemble) (B : Ensemble) : Prop := A ⊆ B /\ B ⊆ A.
Notation "A ≡ B" := (Same_set A B) (at level 57, no associativity).

空集合と全体集合を定義

空集合は元が一つもないので、どんな変数を取っても False を返し、

全体集合はすべてが元であるから、どんな変数を取っても True を返す。

Definition Empty_set : Ensemble := fun a : U => False.
Notation "∅" := Empty_set.

Definition Full_set : Ensemble := fun a : U => True.
Notation Ω := Full_set.

空集合は任意の集合の部分集合であり、全体集合は任意の集合を部分集合にもつことを示す。

Lemma empty_subset : forall A : Ensemble, ∅ ⊆ A.
Proof.
  unfold Include.
  intros.
  contradiction.
Qed.

Lemma subset_full : forall A : Ensemble, A ⊆ Ω.
Proof.
  unfold Include.
  intros.
  unfold Full_set.
  unfold In.
  trivial.
Qed.

仮定に False があるとき任意の命題を示すことができる。 仮定に False があったら contradiction.を用いる。

感想

  • ラッセルのパラドックスは型をつけると回避できるとかどっかで聞いたけどよくわからない。
  • Coq で公理的集合論をやりたかったけどどうやれば良いのかよくわからない。