現代数学概説Ⅰ
1章 $1 例題4 以下a)b)c)を示せ。
a) M ∪ (M ∩ N)=M, M ∩ (M ∪ N) = M.
b) M ⊆ N <-> M = M ∩ N <-> N = M ∪ N.
c) M ⊆ M' <-> M ∪ N ⊆ M' ∪ N, M ∩ N ⊆ M' ∩ N.
-----
coq 証明
- a)
Theorem math_1_1_exp_4a1: forall (M N:Ensemble M),
M ∪ (M ∩ N) = M.
Proof.
intros M N.
apply Extensionality_Ensembles.
unfold Same_set.
split.
- unfold Included.
intros x H.
+ destruct H as [x1| x2 Hmn].
apply H.
+ destruct Hmn as [x Hm Hn].
apply Hm.
- unfold Included.
intros x H.
+ apply Union_introl.
apply H.
Qed.
Theorem math_1_1_exp_4a2: forall (M N:Ensemble M),
M ∩ (M ∪ N) = M.
Proof.
intros M N.
apply Extensionality_Ensembles.
unfold Same_set.
split.
- unfold Included.
intros x H.
destruct H as [m Hm Hmn].
apply Hm.
- unfold Included.
intros x H.
apply Intersection_intro.
apply H.
apply Union_introl.
apply H.
Qed.
- b)
Theorem math_1_1_exp_4b': forall (M N:Ensemble M),
M ⊆ N <-> M = M ∩ N <-> N = M ∪ N.
Proof.
(*" -- なぜか出来ない? -- "*)
Admitted.
- c)
Theorem math_1_1_exp_4c1: forall (M M' N:Ensemble M),
M ⊆ M' -> M ∪ N ⊆ M' ∪ N.
Proof.
intros M M' N.
intros H.
apply math_1_1_8.
split.
- unfold Included in H.
unfold Included.
intros x H1.
apply H in H1.
apply Union_introl.
apply H1.
- apply math_1_1_7_2.
Qed.
Theorem math_1_1_exp_4c2: forall (M M' N:Ensemble M),
M ⊆ M' -> M ∩ N ⊆ M' ∩ N.
Proof.
intros M M' N.
intros H.
apply math_1_1_8'.
split.
- unfold Included in H.
unfold Included.
intros x H1.
apply H.
destruct H1 as [x1 Hm Hn].
apply Hm.
- apply math_1_1_7'_2.
Qed.
----------------------
証明中の math_1_1_xxは、現代数学概説1章にある定理(xx)のcoq証明。
これを最大限生かしたい所だけど上手くゆきません。。汗）
俺のcoq技もこの程度か。
例題4 b)がcoqで解けない。。原因不明。。
中学生でも解ける問題だが、coq(ver-8.13.2)でダメでした。
注）一般の集合演算なのでinduction使えません。
肝の部分は
apply Extensionality_Ensembles.
でしょうか、いわゆる「外延性公理」で"="が出てくる部分でapplyすると、それなりに分解してくれる。
使用したライブラリは
Ensembles.v
coqインストールホルダーを漁ると出てくよ。
参考にした文献は、大学の講義資料
http://herb.h.kobe-u.ac.jp/snap/coq.pdf
４年前に次の仕事の種探そうと、数学基礎の本を読み始めて。。外延性公理がある事を初めて知った。(彌永昌吉・集合と位相 p16)
集合は中学校から出てくるが、外延性公理を教えてもらった記憶がない！
俺は、集合、多重集合の違いが分からなくて悩んでいた。。数十年も。。汗）
＊＊ ミカンが入っている幾つかの籠がある。
傷があるミカンが入っている、入っている個数が違う。。
でもミカンが入っていれば、同じ集合として扱う。。
中学生でも十分に分かると思うが。＊＊
今思えば、中学で選別するポイントの一つで、頭がの特別よろしい人は難なく通過でき、お金のある人は家庭教師等より教えて貰って通過。普通の人は？？のまま落ちこぼれる。。だったのかなと感じます。
