1章 $1 例題4 以下c)を示せ。
c) M ⊆ M' ⇒ M ∪ N ⊆ M' ∪ N 、M ∩ N ⊆ M' ∩ N.
上記をcoq/SSReflectで解いてみる。
問題自体は中学生程度で見りゃ分かるだろう程度です。
でも、coqを使用すると大学教授クラスでも納得する証明ができる・・と思う。
------------------
Theorem math_1_1_exp_4_c: forall (M M' N:Ensemble M),
M ⊆ M' -> M ∪ N ⊆ M' ∪ N /\ M ∩ N ⊆ M' ∩ N.
Proof.
intros M M' N.
split.
** 今日はここまで。。(1年半サボってたので解き方を脳内よりほぼ消失した。)
下に張り付けた画像を見るとcoq/SSReflect形式化は正しいようだ。
取りあえず証明できました。
使った補題2個。。
Theorem math_1_1_exp_4_c: forall (M M' N:Ensemble M),
M ⊆ M' -> M ∪ N ⊆ M' ∪ N /\ M ∩ N ⊆ M' ∩ N.
Proof.
intros M M' N.
split.
- apply math_1_1_exp_4c1.
apply H.
- apply math_1_1_exp_4c2.
apply H.
Qed.
補題２個
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.
Theorem math_1_1_8: forall(S M N:Ensemble M),
M ⊆ S /\ N ⊆ S -> (M ∪ N) ⊆ S.
Proof.
intros S M N.
intros H.
destruct H as [Hnm Hsm].
unfold Included in Hnm.
unfold Included in Hsm.
unfold Included.
intros x Hx.
destruct Hx as [x1 H1| x2 H2].
apply Hnm.
apply H1.
apply Hsm.
apply H2.
Qed.
Theorem math_1_1_8': forall(S M N:Ensemble M),
S ⊆ M /\ S ⊆ N -> S ⊆ (M ∩ N).
Proof.
intros S M N.
intros H.
destruct H as [Hsm Hsn].
unfold Included in Hsm.
unfold Included in Hsn.
unfold Included.
intros x Hx.
apply Intersection_intro.
apply Hsm.
apply Hx.
apply Hsn.
apply Hx.
Qed.
Theorem math_1_1_7'_2: forall(M N:Ensemble M),
(M ∩ N) ⊆ N.
Proof.
intros M N.
unfold Included.
intros x H.
destruct H as [x Hm Hn].
apply Hn.
Qed.
Theorem math_1_1_7_2: forall(M N:Ensemble M),
N ⊆ (M ∪ N).
Proof.
intros M N.
unfold Included.
intros x Hn.
(* right. *)
apply Union_intror.
apply Hn.
Qed.
今日はここまで。
