本文是系列文章的第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
。