現代数学概説Ⅰ
1章 $1 例題4 以下b)を示せ。
b) M ⊆ N <-> M = M ∩ N <-> N = M ∪ N.
------------------------------------------------------------------
Theorem math_1_1_exp_4b_ab: forall (M N:Ensemble M),
M ⊆ N <-> M = M ∩ N.
Proof.
intros M N.
unfold iff.
split.
- intros H.
apply math_1_1_exp_4b_2.
apply H.
- intros H.
apply math_1_1_exp_4b_3.
apply H.
Qed.
Theorem math_1_1_exp_4b_ac: forall (M N:Ensemble M),
M ⊆ N <-> N = M ∪ N.
Proof.
intros M N.
unfold iff.
split.
- intros H.
apply Extensionality_Ensembles.
unfold Same_set.
split.
unfold Included.
intros x H1.
apply Union_intror.
apply H1.
apply math_1_1_8.
split.
apply H.
unfold Included.
intros x H1.
apply H1.
- intros H.
unfold Included.
intros x H1.
rewrite H.
apply Union_introl.
apply H1.
Qed.
Theorem math_1_1_exp_4b_bc: forall (M N:Ensemble M),
M = M ∩ N <-> N = M ∪ N.
Proof.
intros M N.
unfold iff.
split.
- intros H.
apply math_1_1_exp_4b_1.
apply H.
- intros H.
apply Extensionality_Ensembles.
unfold Same_set.
split.
+ unfold Included.
intros x H1.
apply Intersection_intro.
apply H1.
rewrite H.
apply Union_introl.
apply H1.
+ unfold Included.
intros x H1.
destruct H1 as [x Hm Hn].
apply Hm.
Qed.
Lemma math_1_1_exp_4b_1: forall (M N:Ensemble M),
M = M ∩ N -> N = M ∪ N.
Proof.
intros M N.
intros H.
apply Extensionality_Ensembles.
unfold Same_set.
split.
- unfold Included.
intros x H1.
apply Union_intror.
apply H1.
- unfold Included.
intros x Hmn.
destruct Hmn as [x1 H1 | x1 H2].
rewrite H in H1.
destruct H1 as [x1 H1 H2].
apply H2.
apply H2.
Qed.
Lemma math_1_1_exp_4b_2: forall (M N:Ensemble M),
M ⊆ N -> M = M ∩ N.
Proof.
intros M N.
intros H.
apply Extensionality_Ensembles.
unfold Same_set.
split.
- unfold Included.
unfold Included in H.
intros x H1.
apply Intersection_intro.
apply H1.
apply H in H1.
apply H1.
- unfold Included.
intros x H1.
destruct H1 as [x2 H2 H3].
apply H2.
Qed.
Lemma math_1_1_exp_4b_3: forall (M N:Ensemble M),
M = M ∩ N -> M ⊆ N.
Proof.
intros M N.
intros H.
- rewrite H.
unfold Included.
intros x H1.
destruct H1 as [x Hm Hn].
apply Hn.
Qed.
-----------------------------------------
A <-> B <-> C
の形をそのままcoqで解くと、仮定に上げる式が複雑でよく分からなくなる。
結局 A <-> B , A <-> C, B <-> Cに分解して解いた。
(A <-> B /\ A <-> C /\ B <-> C) == (A <-> B <-> C).
は解いてません。。メンドクサソウ。。汗）
補題は３つ作ったけど、整理できてないので汚いコードになってます。。
