本文是系列文章的第8篇。上一篇：ocau：如何用Coq形式化集合論？（7：自然數良序，強歸納原理）
前幾講稍微抄了點近路。我們在講完公理之後就馬不停蹄地進入自然數一直講到了強歸納法。但遺憾的是，目前的工具還不足以建立自然數算術，因為需要遞迴定理。而它又建立在集合論函式的概念之上，而這又依賴於有序對和笛卡爾積。從這講開始我們回到傳統教科書的順序，從交集講起。
交集
集合A的交集是被A中的每個集合所共有的那些元素所組成的集合。我們已經知道⋃ A是把A中的每個集合裡的元素拿出來放到一起所組成的集合，因此它包含了A的交集。要得到A的交集，只需用分離公理，從⋃ A中分離出那些被A的每個集合所共有的元素就行了。
（* Definition/Intersect。v *）
Definition
交集
：=
λ
A
，
{
x
∊
⋃
A
|
∀
a
∈
A
，
x
∈
a
}。
Notation
“⋂ X”
：=
（
交集
X
）
（
at
level
9
，
right
associativity
）
：
集合域
。
可以證明如下引理，它們佐證了以上對“交集”的定義符合直觀。注意它們涉及到集合A的“非空”性，請思考為什麼。
（* Definition/Intersect。v *）
Lemma
交集介入
：
∀
x
A
，
非空
A
→
（
∀
a
∈
A
，
x
∈
a
）
→
x
∈
⋂
A
。
Proof
。
intros
x
A
［
y
Hy
］
Hx
。
apply
分離介入
；
auto
。
eapply
並集介入
；
eauto
。
Qed
。
Lemma
交集除去
：
∀
A
，
∀
x
∈
⋂
A
，
非空
A
∧
∀
a
∈
A
，
x
∈
a
。
Proof
。
intros
。
apply
分離除去
in
H
as
［
H1
H2
］。
split
；
auto
。
apply
並集除去
in
H1
as
［
y
［
Hy
_］］。
now
exists
y
。
Qed
。
結合包含的定義，可以證明
（* Definition/Intersect。v *）
Lemma
交得子集
：
∀
A
，
∀
a
∈
A
，
⋂
A
⊆
a
。
Proof
。
intros
。
eapply
交集除去
；
eauto
。
Qed
。
Lemma
交集反轉包含關係
：
∀
A
B
，
非空
A
→
A
⊆
B
→
⋂
B
⊆
⋂
A
。
Proof
。
intros
。
apply
交集除去
in
H1
as
［［
b
Hb
］
H1
］。
eapply
交集介入
；
auto
。
Qed
。
Lemma
所有元素都是子集則交集也是子集
：
∀
A
B
，
（
∀
a
∈
A
，
a
⊆
B
）
→
⋂
A
⊆
B
。
Proof
。
intros
。
apply
交集除去
in
H0
as
［［
a
Ha
］
H0
］。
eapply
H
；
eauto
。
Qed
。
請回顧關於並集的命題“並得父集”，“並集保持包含關係”，“所有元素都是子集則並集也是子集”，對比它們與上面的命題有何異同。
結合空集的定義，可以證明
（* Definition/Intersect。v *）
Lemma
空集之交
：
⋂
∅
=
∅
。
Proof
。
外延
。
2
：
空集歸謬
。
apply
交集除去
in
H
as
［
H
_］。
exfalso
。
apply
空集非非空
。
apply
H
。
Qed
。
結合單集的定義，可以證明
（* Definition/Intersect。v *）
Lemma
單集之交
：
∀
x
，
⋂
{
x
，}
=
x
。
Proof
with
auto
。
intros
。
外延
。
-
apply
交集除去
in
H
as
［_
H
］。
apply
H
。。。
-
apply
交集介入
。
exists
x
。。。
intros
y
Hy
。
apply
單集除去
in
Hy
；
subst
。。。
Qed
。
二元交
二元交有兩種定義方式。一種是仿照二元並的定義，將A與B的二元交定義為⋂ {A， B}，但是這依賴於並集公理。我們這裡採取另一種方式，它的形式更簡單一些，只依賴於分離公理。
（* Definition/BinaryIntersect。v *）
Definition
二元交
：=
λ
A
B
，
{
x
∊
A
|
x
∈
B
}。
Notation
“A ∩ B”
：=
（
二元交
A
B
）
（
at
level
49
）
：
集合域
。
Lemma
二元交介入
：
∀
x
A
B
，
x
∈
A
→
x
∈
B
→
x
∈
A
∩
B
。
Proof
。
intros
。
now
apply
分離介入
。
Qed
。
Global
Hint
Resolve
二元交介入
：
core
。
Lemma
二元交除去
：
∀
x
A
B
，
x
∈
A
∩
B
→
x
∈
A
∧
x
∈
B
。
Proof
。
intros
。
now
apply
分離除去
in
H
。
Qed
。
Lemma
二元交外介入
：
∀
x
A
B
，
x
∉
A
∨
x
∉
B
→
x
∉
A
∩
B
。
Proof
。
intros
。
firstorder
using
二元交除去
。
Qed
。
Lemma
二元交外除去
：
∀
x
A
B
，
x
∉
A
∩
B
→
x
∉
A
∨
x
∉
B
。
Proof
。
intros
。
排中
（
x
∈
A
）；
auto
。
Qed
。
我們把二元交的其他結論放到下一節。
集合初等代數
本節是對二元並，二元交以及補集運算的一個小結。我們在第3篇講過關於二元並的運算律。為了方便對比，這裡再次列出，但省略證明過程。
（* Definition/BinaryUnion。v *）
Lemma
二元並冪等律
：
∀
A
，
A
∪
A
=
A
。
Lemma
二元並交換律
：
∀
A
B
，
A
∪
B
=
B
∪
A
。
Lemma
二元並結合律
：
∀
A
B
C
，
（
A
∪
B
）
∪
C
=
A
∪
（
B
∪
C
）。
Lemma
二元並保持包含關係
：
∀
A
B
C
，
A
⊆
B
→
A
∪
C
⊆
B
∪
C
。
Lemma
二元並吸收子集
：
∀
A
B
，
A
⊆
B
→
A
∪
B
=
B
。
（* 么元 *）
Lemma
左並空集
：
∀
A
，
∅
∪
A
=
A
。
Lemma
右並空集
：
∀
A
，
A
∪
∅
=
A
。
（* 零元 *）
Lemma
左並全集
：
∀
A
S
，
A
⊆
S
→
S
∪
A
=
S
。
Lemma
右並全集
：
∀
A
S
，
A
⊆
S
→
A
∪
S
=
S
。
Lemma
二元並的並等於並的二元並
：
∀
A
B
，
⋃
（
A
∪
B
）
=
（
⋃
A
）
∪
（
⋃
B
）。
下面給出二元交的版本，請注意對比它們的異同。
（* Definition/BinaryIntersect。v *）
Lemma
二元交冪等律
：
∀
A
，
A
∩
A
=
A
。
Proof
。
intros
。
外延
；
auto
。
apply
二元交除去
in
H
as
［］
；
auto
。
Qed
。
Lemma
二元交交換律
：
∀
A
B
，
A
∩
B
=
B
∩
A
。
Proof
。
intros
。
外延
；
apply
二元交除去
in
H
as
［］
；
auto
。
Qed
。
Lemma
二元交結合律
：
∀
A
B
C
，
（
A
∩
B
）
∩
C
=
A
∩
（
B
∩
C
）。
Proof
。
intros
。
外延
；
apply
二元交除去
in
H
as
［］
。
apply
二元交除去
in
H
as
［］
；
auto
。
apply
二元交除去
in
H0
as
［］
；
auto
。
Qed
。
Lemma
二元交保持包含關係
：
∀
A
B
C
，
A
⊆
B
→
A
∩
C
⊆
B
∩
C
。
Proof
。
intros
。
apply
二元交除去
in
H0
as
［］
；
auto
。
Qed
。
Lemma
二元交拒斥父集
：
∀
A
B
，
A
⊆
B
→
A
∩
B
=
A
。
Proof
。
intros
。
外延
；
auto
。
apply
二元交除去
in
H0
as
［］
；
auto
。
Qed
。
（* 零元 *）
Lemma
左交空集
：
∀
A
，
∅
∩
A
=
∅
。
Proof
。
intros
。
apply
二元交拒斥父集
。
apply
空集是任意集合的子集
。
Qed
。
Lemma
右交空集
：
∀
A
，
A
∩
∅
=
∅
。
Proof
。
intros
。
rewrite
二元交交換律
。
apply
左交空集
。
Qed
。
（* 么元 *）
Lemma
左交全集
：
∀
A
S
，
A
⊆
S
→
S
∩
A
=
A
。
Proof
。
intros
。
外延
；
auto
。
now
apply
二元交除去
in
H0
as
［］
。
Qed
。
Lemma
右交全集
：
∀
A
S
，
A
⊆
S
→
A
∩
S
=
A
。
Proof
。
intros
。
rewrite
二元交交換律
。
now
apply
左交全集
。
Qed
。
Lemma
二元並的交等於交的二元交
：
∀
A
B
，
非空
A
→
非空
B
→
⋂
（
A
∪
B
）
=
（
⋂
A
）
∩
（
⋂
B
）。
Proof
with
auto
。
intros
。
外延
。
-
apply
交集除去
in
H1
as
［_
H1
］。
apply
二元交介入
；
apply
交集介入
；
auto
。
-
apply
二元交除去
in
H1
as
［
H1
H2
］。
apply
交集介入
。
+
destruct
H
as
［
a
Ha
］。
exists
a
；
auto
。
+
intros
a
Ha
。
apply
二元併除去
in
Ha
as
［］
。
*
apply
交集除去
in
H1
as
［_
H1
］；
auto
。
*
apply
交集除去
in
H2
as
［_
H2
］；
auto
。
Qed
。
結合二元並和二元交，可以證明如下吸收律和分配律。
（* Theory/BasicAlgebraOfSet。v *）
Lemma
並交吸收律
：
∀
A
B
，
A
∪
（
A
∩
B
）
=
A
。
Proof
with
auto
。
intros
。
外延
。。。
apply
二元併除去
in
H
as
［］
。。。
apply
二元交除去
in
H
as
［］
。。。
Qed
。
Lemma
交併吸收律
：
∀
A
B
，
A
∩
（
A
∪
B
）
=
A
。
Proof
with
auto
。
intros
。
外延
。。。
apply
二元交除去
in
H
as
［］
。。。
Qed
。
Lemma
交併分配律
：
∀
A
B
C
，
（
A
∩
B
）
∪
C
=
（
A
∪
C
）
∩
（
B
∪
C
）。
Proof
with
auto
。
intros
。
外延
。
-
apply
二元併除去
in
H
as
［］
。。。
apply
二元交除去
in
H
as
［］
。。。
-
apply
二元交除去
in
H
as
［］
；
apply
二元併除去
in
H
as
［］
；
apply
二元併除去
in
H0
as
［］
。。。
Qed
。
Lemma
並交分配律
：
∀
A
B
C
，
（
A
∪
B
）
∩
C
=
（
A
∩
C
）
∪
（
B
∩
C
）。
Proof
with
auto
。
intros
。
外延
。
-
apply
二元交除去
in
H
as
［］
。
apply
二元併除去
in
H
as
［］
。。。
-
apply
二元併除去
in
H
as
［］
；
apply
二元交除去
in
H
as
［］
。。。
Qed
。
對於補集，我們有類似的。
（* Definition/Complement。v *）
Lemma
補集反轉包含關係
：
∀
A
B
C
，
A
⊆
B
→
C
-
B
⊆
C
-
A
。
Proof
。
intros
。
apply
分離除去
in
H0
as
［
Hx
Hx‘
］。
apply
分離介入
；
auto
。
Qed
。
（* 右么元 *）
Lemma
空集之補
：
∀
A
，
A
-
∅
=
A
。
Proof
。
intros
。
外延
。
-
now
apply
分離之父集
in
H
。
-
apply
分離介入
。
apply
H
。
intros
H0
。
空集歸謬
。
Qed
。
（* 左零元 *）
Lemma
補自空集
：
∀
A
，
∅
-
A
=
∅
。
Proof
。
intros
。
外延
。
-
apply
分離之父集
in
H
。
空集歸謬
。
-
空集歸謬
。
Qed
。
補集運算對於二元並和二元交也有分配律。
（* Theory/BasicAlgebraOfSet。v *）
Lemma
並補分配律
：
∀
A
B
C
，
（
A
∪
B
）
-
C
=
（
A
-
C
）
∪
（
B
-
C
）。
Proof
。
intros
。
外延
。
-
apply
分離除去
in
H
as
［
Hx
Hx’
］。
apply
二元併除去
in
Hx
as
［］
。
+
apply
左並介入
。
now
apply
分離介入
。
+
apply
右並介入
。
now
apply
分離介入
。
-
apply
二元併除去
in
H
as
［］
；
apply
分離除去
in
H
as
［
Hx
Hx‘
］；
apply
分離介入
；
auto
。
Qed
。
Lemma
交補分配律
：
∀
A
B
C
，
（
A
∩
B
）
-
C
=
（
A
-
C
）
∩
（
B
-
C
）。
Proof
。
intros
。
外延
。
-
apply
分離除去
in
H
as
［
Hx
Hx’
］。
apply
二元交除去
in
Hx
as
［］
。
apply
二元交介入
；
now
apply
分離介入
。
-
apply
二元交除去
in
H
as
［］
。
apply
分離除去
in
H
as
［
HxA
HxC
］。
apply
分離之父集
in
H0
。
apply
分離介入
；
auto
。
Qed
。
Corollary
交補分配律_簡化
：
∀
A
B
C
，
（
A
∩
B
）
-
C
=
A
∩
（
B
-
C
）。
Proof
。
intros
。
rewrite
交補分配律
。
外延
。
-
apply
二元交除去
in
H
as
［］
。
apply
分離之父集
in
H
。
apply
二元交介入
；
auto
。
-
apply
二元交除去
in
H
as
［
H1
H2
］。
apply
分離除去
in
H2
as
［
Hx
Hx‘
］。
apply
二元交介入
；
apply
分離介入
；
auto
。
Qed
。
補集運算對於二元並和二元交有德摩根律。
（* Theory/BasicAlgebraOfSet。v *）
Lemma
補並德摩根律
：
∀
A
B
C
，
C
-
（
A
∪
B
）
=
（
C
-
A
）
∩
（
C
-
B
）。
Proof
。
intros
。
外延
。
-
apply
分離除去
in
H
as
［
Hx
Hx’
］。
apply
二元交介入
；
apply
分離介入
；
auto
。
-
apply
二元交除去
in
H
as
［
H1
H2
］。
apply
分離除去
in
H1
as
［
Hx
Hx‘
］。
apply
分離之條件
in
H2
。
apply
分離介入
；
auto
。
now
apply
二元並外介入
。
Qed
。
Lemma
補交德摩根律
：
∀
A
B
C
，
C
-
（
A
∩
B
）
=
（
C
-
A
）
∪
（
C
-
B
）。
Proof
。
intros
。
外延
。
-
apply
分離除去
in
H
as
［
Hx
Hx’
］。
apply
二元交外除去
in
Hx‘
as
［］
。
+
apply
左並介入
。
now
apply
分離介入
。
+
apply
右並介入
。
now
apply
分離介入
。
-
apply
二元併除去
in
H
as
［］
；
apply
分離除去
in
H
as
［
Hx
Hx’
］；
apply
分離介入
；
auto
；
apply
二元交外介入
；
auto
。
Qed
。
還有一些常用引理。
（* Theory/BasicAlgebraOfSet。v *）
Lemma
先補再並等於沒補
：
∀
A
B
，
A
∪
（
B
-
A
）
=
A
∪
B
。
Proof
with
auto
。
intros
。
外延
。
-
apply
二元併除去
in
H
as
［］
。。。
apply
分離之父集
in
H
。。。
-
apply
二元併除去
in
H
as
［］
。。。
排中
（
x
∈
A
）。。。
apply
右並介入
。
apply
分離介入
。。。
Qed
。
Lemma
先並再補等於沒並
：
∀
A
B
，
（
A
∪
B
）
-
A
=
B
-
A
。
Proof
with
auto
。
intros
。
外延
；
apply
分離除去
in
H
as
［］
。
-
apply
二元併除去
in
H
as
［］
。
exfalso
。。。
apply
分離介入
。。。
-
apply
分離介入
。。。
Qed
。
Lemma
並自身之補得全集
：
∀
A
S
，
A
⊆
S
→
A
∪
（
S
-
A
）
=
S
。
Proof
with
auto
。
intros
。
rewrite
先補再並等於沒補
。
外延
。。。
apply
二元併除去
in
H0
as
［］
；
auto
。
Qed
。
Lemma
交自身之補得空集
：
∀
A
S
，
A
∩
（
S
-
A
）
=
∅
。
Proof
。
intros
。
apply
空集介入
。
intros
x
H
。
apply
二元交除去
in
H
as
［
H1
H2
］。
now
apply
分離之條件
in
H2
。
Qed
。
最後再補充2條關於補集的引理。它們可以使後面習題的證明更簡單。
（* Definition/Complement。v *）
Lemma
補集外介入
：
∀
A
B
x
，
x
∉
A
∨
x
∈
B
→
x
∉
A
-
B
。
Proof
。
intros
*
［］
；
intros
H1
。
-
apply
H
。
now
apply
分離之父集
in
H1
。
-
now
apply
分離之條件
in
H1
。
Qed
。
Lemma
補集外除去
：
∀
A
B
x
，
x
∉
A
-
B
→
x
∉
A
∨
x
∈
B
。
Proof
。
intros
。
排中
（
x
∈
B
）。
auto
。
left
。
intros
H1
。
apply
H
。
now
apply
分離介入
。
Qed
。
提示：
intros
後接*可以匯入所有全稱量化的變數，但不會匯入前提。
綜合練習
證明下面的命題。要求使用分號語法和
auto
使證明儘可能地短。
（* Example/Ch8。v *）
（* 我們可以加入一些只在當前檔案起作用的Hint *）
Local
Hint
Resolve
二元並外介入
：
core
。
Local
Hint
Resolve
二元交外介入
：
core
。
Local
Hint
Resolve
補集外介入
：
core
。
Example
練習8_1
：
∀
A
B
，
（
A
∩
B
）
∪
（
A
-
B
）
=
A
。
Admitted
。
Example
練習8_2
：
∀
A
B
，
（
A
∩
B
）
∪
（
B
-
A
）
=
B
。
Admitted
。
Example
練習8_3
：
∀
A
B
，
A
-
（
A
∩
B
）
=
A
-
B
。
Admitted
。
Example
練習8_4
：
∀
A
B
，
A
-
（
A
-
B
）
=
A
∩
B
。
Admitted
。
Example
練習8_5
：
∀
A
B
C
，
（
A
∪
B
）
-
C
=
（
A
-
C
）
∪
（
B
-
C
）。
Admitted
。
Example
練習8_6
：
∀
A
B
C
，
A
-
（
B
-
C
）
=
（
A
-
B
）
∪
（
A
∩
C
）。
Admitted
。
Example
練習8_7
：
∀
A
B
C
，
（
A
-
B
）
-
C
=
A
-
（
B
∪
C
）。
Admitted
。
Example
練習8_8
：
∀
A
B
C
，
A
⊆
C
∧
B
⊆
C
↔
A
∪
B
⊆
C
。
Admitted
。
Example
練習8_9
：
∀
A
B
C
，
C
⊆
A
∧
C
⊆
B
↔
C
⊆
A
∩
B
。
Admitted
。
Example
練習8_10
：
∀
A
B
C
，
（
A
∩
B
）
-
（
A
∩
C
）
=
（
A
∩
B
）
-
C
。
Admitted
。
Example
練習8_11
：
∀
A
B
C
，
（（
A
∪
B
∪
C
）
∩
（
A
∪
B
））
-
（（
A
∪
（
B
-
C
））
∩
A
）
=
B
-
A
。
Proof
。
（* 提示：可以用“二元交交換律”，“交併吸收律”等rewrite，而不需要外延 *）
Admitted
。
