CoqでZFC公理系において2つのペアが等しいときその対応する要素もそれぞれ等しいことを証明する。(1)
mathlogでの投稿は初めてとなります。今回はCoqでZFC公理系の外延性の公理とペアの公理を記述したうえで、2つのペアが等しいときその対応する要素もそれぞれ等しいことを証明します。この命題を記号で書くと以下のようになります。
$$ \forall x \ y \ z \ w \ ((x, y) = (z,w) \rightarrow x = z \land y = z) $$
ここでは2つの集合$x, y$からなる集合を$\{x, y\} $、2つの集合のペアを$(x,y) $と表し区別します。
外延性の公理とペアの公理
Coqで外延性の公理とペアの公理を記述したものは以下のようになります。（命題の名称は適当につけています。この他にも命題を記述していますので番号が飛ぶのはそのためです。)
Axiom is_in : Set -> (Set -> Prop).
Axiom p1 : forall x y : Set, (forall z : Set, is_in z x <-> is_in z y) <-> x = y.
Axiom pair_set : Set -> (Set -> Set).
Axiom p7 : forall x y : Set, forall w : Set, is_in w (pair_set x y) <-> (w = x \/ w = y).
is_inは含有記号$\in$に、(pair_set x y) は$\{x,y\}$に相当します。
今回は先の命題の証明のために以下の補題を証明します。
補題1
$$ \forall x \ y \ (\{x,x\} = \{x,y\} \rightarrow x= y) $$
この命題をCoqで記述したもの及びその証明は以下のようになります。
Theorem p16_2 : forall x y : Set, (pair_set x x) = (pair_set x y) <-> x = y.
Proof.
intros.
split.
intros.
assert (is_in y (pair_set x x)).
rewrite H.
apply p7.
right.
reflexivity.
assert (y = x -> x = y).
intros.
rewrite H1.
reflexivity.
apply H1.
assert (y = x \/ y = x -> y = x).
intros.
destruct H2.
apply H2.
apply H2.
apply H2.
apply p7.
apply H0.
intros.
rewrite <- H.
reflexivity.
Qed.