集合的形式化 #7 关系 (1) 等价关系、偏序关系

    类型 A 到类型 B 的（二元）关系，指的是类型为 A -> B -> Prop 的对象。我们通常说函数是一种特殊的关系，这种说法在 ZFC 中是正确的，但在这里则是不准确的，因为二者的语法结构不同（函数的类型为 A -> option B）。

    对于关系 r : A -> B -> Prop，我们定义它的图像是所有满足 r x y 的 (x,y) 组成的集合。反过来，对于集合 S : 集合 (A * B)，我们定义它对应的关系为 fun x y => (x,y) ∈ S。

    如果一个类型为 A -> A -> Prop 的关系满足自反性、对称性、传递性，那么这个关系被称为等价关系。

    设【A : Type】【r : A -> A -> Prop】【r自反 : forall x : A, r x x】【r对称 : forall x y : A, r x y -> r y x】【r传递 : forall x y z : A, r x y -> r y z -> r x z】，那么有【@等价关系_of A r r自反 r对称 r传递 : 等价关系 A】。类型为 等价关系 A 的对象严格地说并不能被称为关系（因为关系应具有类型 A -> B -> Prop），它是由一个关系和这个关系满足自反性、对称性、传递性的证明项打包组合而成的项。在刚定义完“等价关系”后，对于 x : A ，y : A，r : 等价关系 A，“r x y”是语法错误，而“eq_rel r x y”则是符合语法规则的。在使用了 Coercion 指令后，Coq 在遇到“r x y”的表述时可以自动将其解析为“eq_rel r x y”以匹配类型，从而简化了表达。等价关系的基本性质如下：

    对于 R : 等价关系 A 和 a : A，我们定义其对应的等价类为所有满足 R x a 的 x 组成的集合。对于 R : 等价关系 A，我们定义 R 的等价类集为 R 的所有等价类的集合。具体定义与相关定理如下：

    对于等价类 S（即已知 S ∈ 等价类集 R），我们可以选出一个代表 x，使得 S 恰好为 x 对应的等价类（同时自然也有 x ∈ S）。

    等价类的一个重要应用是构造新的类型。对于 A : Type 和 R : 等价关系 A，我们可以构造出一个新的类型 T，使得 T 中的元素与 R 的等价类一一对应。对于 x : A，Btfr R x 表示 R 和 x 对应的等价类对应的 T 中的元素。对于 T 中的每一个元素，我们都能找到一个 x : A，使得 Btfr R x 恰好是这个元素。

    “等价类构造类型”在未来将被用于基数、整数、有理数、实数的构造。（注：以上代码中定义了两种“等价类构造类型”，同样是为了控制层级）

    除了等价关系以外，序关系也是常见的关系。对于关系 r : A -> A -> Prop 和集合 S : 集合 A，若 r 在 S 的范围内满足自反性、反对称性、传递性，则 r 被称为 S 上的偏序关系；若 r 在 S 的范围内满足反自反性、反对称性、传递性，则 r 被称为 S 上的严格偏序关系。

    容易证明偏序关系和严格偏序关系的以下基本性质：

    对于 S 上的偏序关系 r，(fun x y => r x y /\ x <> y) 符合 S 上的严格偏序关系的要求。以下代码中，对于 S : 集合 A 和 r : 偏序关系 S，strict_po r 表示的就是 r 自然对应的这个 S 上的严格偏序关系，它具有类型 严格偏序关系 S。

    对于全集上的偏序关系和严格偏序关系，以上性质可以得到简化。

    子集关系是偏序关系的一个常见实例。我们可以相应地定义真子集关系，它与子集偏序关系对应的严格偏序关系一致。

    对于一个偏序关系，我们可以定义它的最大值和最小值运算。

    对于 S : 集合 A，r : 偏序关系 S，T : 集合 A，类型为 A 的 x 被称为 T 的上界当且仅当 T 为 S 的子集且 x ∈ S 且对于任意的属于 T 的 y 都有 r y x；x 被称为 T 的下界当且仅当 T 为 S 的子集且 x ∈ S 且对于任意的属于 T 的 y 都有 r x y。

    上界集的最小值就是最小上界，下界集的最大值就是最大下界。

    对于 S : 集合 A，r : 偏序关系 S，T : 集合 A，可定义其极大元集和极小元集。注意“极大元”与“最大值”、“极小元”与“最小值”的差别。