10. 关系

正如集合为描述一个类型中对象的性质提供了便利语言，关系也为描述一个类型中对象对的性质提供了便利语言。这听起来也许枯燥而抽象，但这类性质在数学中处处出现：一个实数小于另一个实数；一个整数与另一个整数模 5 同余；一个集合是另一个集合的子集；一个函数是另一个函数的逆。

本章介绍关系本身可以具有的一些重要性质：它们可以是自反的、对称的、反对称的或传递的，也可以同时具有这些性质中的若干个。

10.1. 自反、对称、反对称、传递

10.1.1. 例

定义

类型 \(X\) 上的关系 \(\sim\) 称为自反的，如果对类型 \(X\) 的所有 \(x\)，都有 \(x\sim x\)。

问题

证明 \(\mathbb{N}\) 上的关系 \(|\) 是自反的。

解答

我们必须证明对所有自然数 \(x\)，都有 \(x\mid x\)。确实，设 \(x\) 为自然数，则 \(x=x\cdot 1\)。

example : Reflexive ((·:ℕ) ∣ ·) := by
  dsimp [Reflexive]
  intro x
  use 1
  ring

定义

类型 \(X\) 上的关系 \(\sim\) 称为对称的，如果对类型 \(X\) 的所有 \(x\) 和 \(y\)，若 \(x\sim y\)，则 \(y\sim x\)。

问题

证明 \(\mathbb{N}\) 上的关系 \(|\) 不是对称的。

解答

我们必须证明存在自然数 \(x\) 和 \(y\)，使得 \(x\mid y\) 且 \(y\not\mid x\)。确实，\(2=1\cdot 2\)，所以 \(1\mid 2\)；并且 \(2\cdot 0<1<2\cdot 1\)，所以 \(2\not\mid 1\)。

example : ¬ Symmetric ((·:ℕ) ∣ ·) := by
  dsimp [Symmetric]
  push_neg
  use 1, 2
  constructor
  · use 2
    numbers
  · apply Nat.not_dvd_of_exists_lt_and_lt
    use 0
    constructor
    · numbers
    · numbers

定义

类型 \(X\) 上的关系 \(\sim\) 称为反对称的，如果对类型 \(X\) 的所有 \(x\) 和 \(y\)，若 \(x\sim y\) 且 \(y\sim x\)，则 \(x=y\)。

问题

证明 \(\mathbb{N}\) 上的关系 \(|\) 是反对称的。

解答

我们先注意如下事实（\(\star\)）：若 \(m\) 和 \(n\) 是自然数，且 \(m=0\) 并且 \(m\mid n\)，则 \(m=n\)。确实，由 \(m\mid n\)，存在自然数 \(k\) 使得 \(n=mk\)，于是

\[\begin{split}m&=0\\ &=0\cdot k\\ &=mk\\ &=n.\end{split}\]

现在回到原问题。我们必须证明：对所有自然数 \(x\) 和 \(y\)，若 \(x\mid y\) 且 \(y\mid x\)，则 \(x=y\)。确实，设 \(x\) 和 \(y\) 为自然数，并假设 \(x\mid y\) 且 \(y\mid x\)。若 \(x=0\)，则由（\(\star\)）完成；若 \(y=0\)，同理完成。否则，\(x>0\)，所以由 \(y\mid x\) 可得 \(y\le x\)；并且 \(y>0\)，所以由 \(x\mid y\) 可得 \(x\le y\)。合并两者，得 \(x=y\)。

example : AntiSymmetric ((·:ℕ) ∣ ·) := by
  have H : ∀ {m n}, m = 0 → m ∣ n → m = n
  · intro m n h1 h2
    obtain ⟨k, hk⟩ := h2
    calc m = 0 := by rw [h1]
      _ = 0 * k := by ring
      _ = m * k := by rw [h1]
      _ = n := by rw [hk]
  dsimp [AntiSymmetric]
  intro x y h1 h2
  obtain hx | hx := Nat.eq_zero_or_pos x
  · apply H hx h1
  obtain hy | hy := Nat.eq_zero_or_pos y
  · have : y = x := by apply H hy h2
    rw [this]
  apply le_antisymm
  · apply Nat.le_of_dvd hy h1
  · apply Nat.le_of_dvd hx h2

定义

类型 \(X\) 上的关系 \(\sim\) 称为传递的，如果对类型 \(X\) 的所有 \(x\)、\(y\)、\(z\)，若 \(x\sim y\) 且 \(y\sim z\)，则 \(x\sim z\)。

问题

证明 \(\mathbb{N}\) 上的关系 \(|\) 是传递的。

解答

我们必须证明对所有自然数 \(a\)、\(b\)、\(c\)，若 \(a\mid b\) 且 \(b\mid c\)，则 \(a\mid c\)。

确实，设 \(a\)、\(b\)、\(c\) 为具有这些性质的自然数。由于 \(a\mid b\)，存在自然数 \(k\) 使得 \(b=ak\)；由于 \(b\mid c\)，存在自然数 \(l\) 使得 \(c=bl\)。于是

\[\begin{split}c&=bl\\ &=(ak)l\\ &=a(kl),\end{split}\]

因此 \(a\mid c\)。

example : Transitive ((·:ℕ) ∣ ·) := by
  dsimp [Transitive]
  intro a b c hab hbc
  obtain ⟨k, hk⟩ := hab
  obtain ⟨l, hl⟩ := hbc
  use k * l
  calc c = b * l := by rw [hl]
    _ = (a * k) * l := by rw [hk]
    _ = a * (k * l) := by ring

10.1.2. 例

问题

判断 \(\mathbb{R}\) 上的关系 \(=\) 具有下列哪些性质：

自反；
对称；
反对称；
传递。

example : Reflexive ((·:ℝ) = ·) := by
  dsimp [Reflexive]
  intro x
  ring

example : Symmetric ((·:ℝ) = ·) := by
  dsimp [Symmetric]
  intro x y h
  rw [h]

example : AntiSymmetric ((·:ℝ) = ·) := by
  dsimp [AntiSymmetric]
  intro x y h1 h2
  rw [h1]

example : Transitive ((·:ℝ) = ·) := by
  dsimp [Transitive]
  intro x y z h1 h2
  rw [h1, h2]

10.1.3. 例

问题

判断 \(\mathbb{R}\) 上的关系 \(\sim\) 具有下列哪些性质，其中 \(x\sim y\) 定义为 \((x-y)^2\leq 1\)：

自反；
对称；
反对称；
传递。

local infix:50 "∼" => fun (x y : ℝ) ↦ (x - y) ^ 2 ≤ 1

example : Reflexive (· ∼ ·) := by
  dsimp [Reflexive]
  intro x
  calc (x - x) ^ 2 = 0 := by ring
    _ ≤ 1 := by numbers

example : Symmetric (· ∼ ·) := by
  dsimp [Symmetric]
  intro x y h
  calc (y - x) ^ 2 = (x - y) ^ 2 := by ring
    _ ≤ 1 := by rel [h]

example : ¬ AntiSymmetric (· ∼ ·) := by
  dsimp [AntiSymmetric]
  push_neg
  use 1, 1.1
  constructor
  · numbers
  constructor
  · numbers
  · numbers

example : ¬ Transitive (· ∼ ·) := by
  dsimp [Transitive]
  push_neg
  use 1, 1.9, 2.5
  constructor
  · numbers
  constructor
  · numbers
  · numbers

10.1.4. 例

考虑如下有限归纳类型 Hand。

inductive Hand
  | rock
  | paper
  | scissors

考虑 Hand 类型上的如下关系 \(\prec\)。

@[reducible] def r : Hand → Hand → Prop
  | rock, rock => False
  | rock, paper => True
  | rock, scissors => False
  | paper, rock => False
  | paper, paper => False
  | paper, scissors => True
  | scissors, rock => True
  | scissors, paper => False
  | scissors, scissors => False

local infix:50 " ≺ " => r

问题

判断关系 \(\prec\) 具有下列哪些性质：

自反；
对称；
反对称；
传递。

example : ¬ Reflexive (· ≺ ·) := by
  dsimp [Reflexive]
  push_neg
  use rock
  exhaust

example : ¬ Symmetric (· ≺ ·) := by
  dsimp [Symmetric]
  push_neg
  use rock, paper
  exhaust

example : AntiSymmetric (· ≺ ·) := by
  dsimp [AntiSymmetric]
  intro x y
  cases x <;> cases y <;> exhaust

example : ¬ Transitive (· ≺ ·) := by
  dsimp [Transitive]
  push_neg
  use rock, paper, scissors
  exhaust

10.1.5. 练习

证明 \(\mathbb{R}\) 上的关系 \(<\) 不是对称的。

example : ¬ Symmetric ((·:ℝ) < ·) := by
  sorry

证明 \(\mathbb{Z}\) 上如下定义的关系 \(\sim\) 不是反对称的：\(x\sim y\) 当且仅当 \(x\equiv y \mod 2\)。

local infix:50 "∼" => fun (x y : ℤ) ↦ x ≡ y [ZMOD 2]

example : ¬ AntiSymmetric (· ∼ ·) := by
  sorry

考虑如下有限归纳类型 Little，以及 Little 类型上的如下关系 \(\sim\)。判断关系 \(\sim\) 具有下列哪些性质：自反；对称；反对称；传递。

自反；
对称；
反对称；
传递。

section
inductive Little
  | meg
  | jo
  | beth
  | amy
  deriving DecidableEq

open Little

@[reducible] def s : Little → Little → Prop
  | meg, meg => True
  | meg, jo => True
  | meg, beth => True
  | meg, amy => True
  | jo, meg => True
  | jo, jo => True
  | jo, beth => True
  | jo, amy => False
  | beth, meg => True
  | beth, jo => True
  | beth, beth => False
  | beth, amy => True
  | amy, meg => True
  | amy, jo => False
  | amy, beth => True
  | amy, amy => True

local infix:50 " ∼ " => s

example : Reflexive (· ∼ ·) := by
  sorry

example : ¬ Reflexive (· ∼ ·) := by
  sorry

example : Symmetric (· ∼ ·) := by
  sorry

example : ¬ Symmetric (· ∼ ·) := by
  sorry

example : AntiSymmetric (· ∼ ·) := by
  sorry

example : ¬ AntiSymmetric (· ∼ ·) := by
  sorry

example : Transitive (· ∼ ·) := by
  sorry

example : ¬ Transitive (· ∼ ·) := by
  sorry

判断 \(\mathbb{Z}\) 上如下定义的关系 \(\sim\) 具有哪些性质：\(x\sim y\) 当且仅当 \(y\equiv x+1\mod 5\)：自反；对称；反对称；传递。并把这个关系的一段代表性部分画成有向图。

自反；
对称；
反对称；
传递。

local infix:50 "∼" => fun (x y : ℤ) ↦ y ≡ x + 1 [ZMOD 5]

example : Reflexive (· ∼ ·) := by
  sorry

example : ¬ Reflexive (· ∼ ·) := by
  sorry

example : Symmetric (· ∼ ·) := by
  sorry

example : ¬ Symmetric (· ∼ ·) := by
  sorry

example : AntiSymmetric (· ∼ ·) := by
  sorry

example : ¬ AntiSymmetric (· ∼ ·) := by
  sorry

example : Transitive (· ∼ ·) := by
  sorry

example : ¬ Transitive (· ∼ ·) := by
  sorry

判断 \(\mathbb{Z}\) 上如下定义的关系 \(\sim\) 具有哪些性质：\(x\sim y\) 当且仅当 \(x+y\equiv 0\mod 3\)：自反；对称；反对称；传递。并把这个关系的一段代表性部分画成有向图。

自反；
对称；
反对称；
传递。

local infix:50 "∼" => fun (x y : ℤ) ↦ x + y ≡ 0 [ZMOD 3]

example : Reflexive (· ∼ ·) := by
  sorry

example : ¬ Reflexive (· ∼ ·) := by
  sorry

example : Symmetric (· ∼ ·) := by
  sorry

example : ¬ Symmetric (· ∼ ·) := by
  sorry

example : AntiSymmetric (· ∼ ·) := by
  sorry

example : ¬ AntiSymmetric (· ∼ ·) := by
  sorry

example : Transitive (· ∼ ·) := by
  sorry

example : ¬ Transitive (· ∼ ·) := by
  sorry

判断 \(\mathcal{P}(\mathbb{N})\)，即自然数集合的类型，上的关系 \(\subseteq\) 具有哪些性质：自反；对称；反对称；传递。并把这个关系的一段代表性部分画成有向图。

自反；
对称；
反对称；
传递。

example : Reflexive ((· : Set ℕ) ⊆ ·) := by
  sorry

example : ¬ Reflexive ((· : Set ℕ) ⊆ ·) := by
  sorry

example : Symmetric ((· : Set ℕ) ⊆ ·) := by
  sorry

example : ¬ Symmetric ((· : Set ℕ) ⊆ ·) := by
  sorry

example : AntiSymmetric ((· : Set ℕ) ⊆ ·) := by
  sorry

example : ¬ AntiSymmetric ((· : Set ℕ) ⊆ ·) := by
  sorry

example : Transitive ((· : Set ℕ) ⊆ ·) := by
  sorry

example : ¬ Transitive ((· : Set ℕ) ⊆ ·) := by
  sorry

判断 \(\mathbb{R}^2\) 上如下定义的关系 \(\prec\) 具有哪些性质：\((x_1,y_1)\prec(x_2,y_2)\) 当且仅当 \(x_1\le x_2\) 且 \(y_1\le y_2\)：自反；对称；反对称；传递。

自反；
对称；
反对称；
传递。

local infix:50 "≺" => fun ((x1, y1) : ℝ × ℝ) (x2, y2) ↦ (x1 ≤ x2 ∧ y1 ≤ y2)

example : Reflexive (· ≺ ·) := by
  sorry

example : ¬ Reflexive (· ≺ ·) := by
  sorry

example : Symmetric (· ≺ ·) := by
  sorry

example : ¬ Symmetric (· ≺ ·) := by
  sorry

example : AntiSymmetric (· ≺ ·) := by
  sorry

example : ¬ AntiSymmetric (· ≺ ·) := by
  sorry

example : Transitive (· ≺ ·) := by
  sorry

example : ¬ Transitive (· ≺ ·) := by
  sorry

10.2. 等价关系

10.2.1. 例

定义

一个关系称为等价关系，如果它是自反的、对称的且传递的。

问题

设 \(n\) 为整数。证明 \(\mathbb{Z}\) 上如下定义的关系 \(\sim\) 是等价关系：\(x\sim y\) 当且仅当 \(x\equiv y\mod n\)。

解答

由例 3.3.10，关系 \(\sim\) 是自反的。

由第 3.3 节的两道练习，关系 \(\sim\) 是对称的且传递的。

variable (n : ℤ)

local infix:50 "∼" => fun (x y : ℤ) ↦ x ≡ y [ZMOD n]

example : Reflexive (· ∼ ·) := by
  dsimp [Reflexive]
  apply Int.ModEq.refl

example : Symmetric (· ∼ ·) := by
  dsimp [Symmetric]
  apply Int.ModEq.symm

example : Transitive (· ∼ ·) := by
  dsimp [Transitive]
  apply Int.ModEq.trans

我们画出这个关系的一部分有向图，例如取 \(n=3\)。

图形有些杂乱，但仍勉强可以看出一个模式：这些数形成团，例如 … -5、-2、1、4、7、… 全都彼此相连，并且不与其他数相连。我们为这种有向图引入如下视觉简写：当节点被赋予不同颜色时，它表示这样一个有向图：同一颜色的所有节点彼此双向连接（包括与自身相连），且不与其他颜色的节点相连。

10.2.2. 例

问题

证明 \(\mathbb{Z}\) 上由 \(a\sim b\) 当且仅当 \(a^2=b^2\) 定义的关系 \(\sim\) 是等价关系。

解答

对所有整数 \(x\)，有 \(x^2=x^2\)，所以 \(x\sim x\)。因此关系 \(\sim\) 是自反的。

对所有整数 \(x\) 和 \(y\)，若 \(x\sim y\)，则 \(x^2=y^2\)，所以 \(y^2=x^2\)，从而 \(y\sim x\)。因此关系 \(\sim\) 是对称的。

对所有整数 \(x\)、\(y\)、\(z\)，若 \(x\sim y\) 且 \(y\sim z\)，则 \(x^2=y^2\) 且 \(y^2=z^2\)，所以

\[\begin{split}x^2&=y^2\\ &=z^2,\end{split}\]

因此 \(x\sim z\)。所以关系 \(\sim\) 是传递的。

local infix:50 "∼" => fun (x y : ℤ) ↦ x ^ 2 = y ^ 2

example : Reflexive (· ∼ ·) := by
  dsimp [Reflexive]
  intro x
  ring

example : Symmetric (· ∼ ·) := by
  dsimp [Symmetric]
  intro x y hxy
  rw [hxy]

example : Transitive (· ∼ ·) := by
  dsimp [Transitive]
  intro x y z hxy hyz
  calc x ^ 2 = y ^ 2 := by rw [hxy]
    _ = z ^ 2 := by rw [hyz]

如果你尝试为这个关系画出有向图，会看到它具有与前一个关系相同的“团”行为。画出有向图后，再画出多色“团”版本。

10.2.3. 例

你大概已经猜到，对任意等价关系，都可以用这种方式一致地着色。我们把这一点数学化。

设 \(r\) 为类型 \(\alpha\) 上的一个关系，用中缀记号 \(\sim\) 表示。

定义

对 \(\alpha\) 中的 \(a\)，\(a\) 的等价类（记为 \([a]\)）定义为 \(\{b:\alpha\mid a\sim b\}\)。

定理

若关系 \(r\) 是对称的且传递的，则对所有 \(a_1\) 和 \(a_2\)，若 \(a_1\sim a_2\)，则 \([a_1]=[a_2]\)。

证明

我们必须证明对 \(\alpha\) 中所有 \(b\)，有 \(a_1\sim b\) 当且仅当 \(a_2\sim b\)。

首先，假设 \(a_1\sim b\)。由于 \(a_1\sim a_2\)，由对称性得 \(a_2\sim a_1\)，再由传递性得 \(a_2\sim a_1\sim b\)。

反过来，假设 \(a_2\sim b\)。由于 \(a_1\sim a_2\)，由传递性得 \(a_1\sim a_2\sim b\)。

notation:arg "⦍" a "⦐" => { b | a ∼ b }

theorem EquivalenceClass.eq_of_rel (h_symm : @Symmetric α r) (h_trans : @Transitive α r)
    {a1 a2 : α} (ha : a1 ∼ a2) :
    ⦍a1⦐ = ⦍a2⦐ := by
  ext b
  dsimp
  constructor
  · intro ha1b
    apply h_trans (y := a1)
    · apply h_symm ha
    · apply ha1b
  · intro ha2b
    apply h_trans ha ha2b

定理

若关系 \(r\) 是自反的，则每个 \(a\) 都属于自己的等价类：\(a\in [a]\)。

证明

我们必须证明对所有 \(a\)，都有 \(a\sim a\)，而这正是自反性的定义。

theorem EquivalenceClass.mem_self (h_refl : @Reflexive α r) (a : α) :
    a ∈ { b : α | a ∼ b } := by
  dsimp
  apply h_refl

10.2.4. 例

考虑 \(\mathbb{Z}\) 上的关系 \(=\)。由例 10.1.2，它是等价关系。

练习：画出这个关系，方法是沿直线画出底层类型 \(\mathbb{Z}\) 的一部分，然后用不同颜色标出各个等价类。

10.2.5. 例

问题

证明 \(\mathbb{Z}\times\mathbb{N}\) 上由 \((a,b)\sim(c,d)\) 当且仅当 \(a(d+1)=c(b+1)\) 定义的关系 \(\sim\) 是等价关系。

解答

对 \(\mathbb{Z}\times\mathbb{N}\) 中所有 \((a,b)\)，有 \(a(b+1)=a(b+1)\)，所以 \((a,b)\sim(a,b)\)。因此 \(\sim\) 是自反的。

对 \(\mathbb{Z}\times\mathbb{N}\) 中所有 \((a,b)\) 和 \((c,d)\)，若 \((a,b)\sim(c,d)\)，则 \(a(d+1)=c(b+1)\)，所以 \(c(b+1)=a(d+1)\)，从而 \((c,d)\sim(a,b)\)。因此 \(\sim\) 是对称的。

对 \(\mathbb{Z}\times\mathbb{N}\) 中所有 \((a,b)\)、\((c,d)\)、\((e,f)\)，若 \((a,b)\sim(c,d)\) 且 \((c,d)\sim(e,f)\)，则 \(a(d+1)=c(b+1)\) 且 \(c(f+1)=e(d+1)\)。我们将证明 \(a(f+1)=e(b+1)\)，这将推出 \((a,b)\sim(e,f)\)，从而证明 \(\sim\) 的传递性。

由于 \(d+1>0\)，只需证明 \((d+1)\left[a(f+1)\right]=(d+1)\left[e(b+1)\right]\)。记 \(B:=b+1\)、\(D:=d+1\)、\(F:=f+1\)；于是我们已知 \(aD=cB\) 且 \(cF=eD\)，并需要证明 \(D(aF)=D(eB)\)。

确实，

\[\begin{split}D (a F) &= (a D) F \\ & = (c B) F \\ & = (c F) B \\ & = (e D) B \\ & = D (e B).\end{split}\]

local infix:50 "∼" => fun ((a, b) : ℤ × ℕ) (c, d) ↦ a * (d + 1) = c * (b + 1)

example : Reflexive (· ∼ ·) := by
  dsimp [Reflexive]
  intro (a, b)
  dsimp

example : Symmetric (· ∼ ·) := by
  dsimp [Symmetric]
  intro (a, b) (c, d) h
  dsimp at *
  rw [h]

example : Transitive (· ∼ ·) := by
  dsimp [Transitive]
  intro (a, b) (c, d) (e, f) h1 h2
  dsimp at *
  set B := (b:ℤ) + 1
  set D := (d:ℤ) + 1
  set F := (f:ℤ) + 1
  have :=
  calc D * (a * F) = (a * D) * F := by ring
    _ = (c * B) * F := by rw [h1]
    _ = (c * F) * B := by ring
    _ = (e * D) * B := by rw [h2]
    _ = D * (e * B) := by ring
  cancel D at this

现在画出关系 \(\sim\)：在平面中画出底层类型 \(\mathbb{Z}\times\mathbb{N}\) 的一部分，然后用不同颜色标出各个等价类。

10.2.6. 例

定理

在 0 层类型的类型上定义关系 \(\sim\)：\(\alpha\sim\beta\) 当且仅当存在一个双射函数 \(f:\alpha\to\beta\)。这个关系是等价关系。

local infix:50 "∼" => fun (α β : Type) ↦ ∃ f : α → β, Bijective f

example : Reflexive (· ∼ ·) := by
  dsimp [Reflexive]
  intro α
  use id
  rw [bijective_iff_exists_inverse]
  use id
  constructor
  · rfl
  · rfl

example : Symmetric (· ∼ ·) := by
  dsimp [Symmetric]
  intro α β h
  obtain ⟨f, hf⟩ := h
  rw [bijective_iff_exists_inverse] at hf
  obtain ⟨g, hfg1, hfg2⟩ := hf
  use g
  rw [bijective_iff_exists_inverse]
  use f
  constructor
  · apply hfg2
  · apply hfg1

example : Transitive (· ∼ ·) := by
  dsimp [Transitive]
  intro α β γ h1 h2
  obtain ⟨f1, hf1a, hf1b⟩ := h1
  obtain ⟨f2, hf2a, hf2b⟩ := h2
  use f2 ∘ f1
  constructor
  · apply Injective.comp
    · apply hf2a
    · apply hf1a
  · apply Surjective.comp
    · apply hf2b
    · apply hf1b

10.2.7. 练习

考虑 \(\mathbb{Z}\) 上的关系 \(\sim\)，定义为：\(a\sim b\) 当且仅当存在正整数 \(m\) 和 \(n\)，使得 \(am=bn\)。证明 \(\sim\) 是等价关系。画出关系 \(\sim\)：沿直线画出底层类型 \(\mathbb{Z}\) 的一部分，然后用不同颜色标出各个等价类。
- 证明 \(\sim\) 是等价关系。
- 画出关系 \(\sim\)：沿直线画出底层类型 \(\mathbb{Z}\) 的一部分，然后用不同颜色标出各个等价类。
```
local infix:50 "∼" => fun (a b : ℤ) ↦ ∃ m n, m > 0 ∧ n > 0 ∧ a * m = b * n

example : Reflexive (· ∼ ·) := by
  sorry

example : Symmetric (· ∼ ·) := by
  sorry

example : Transitive (· ∼ ·) := by
  sorry
```
考虑 \(\mathbb{N}^2\) 上的关系 \(\sim\)，定义为：\((a,b)\sim(c,d)\) 当且仅当 \(a+d=b+c\)。证明 \(\sim\) 是等价关系。画出关系 \(\sim\)：在平面中画出底层类型 \(\mathbb{N}^2\) 的一部分，然后用不同颜色标出各个等价类。
- 证明 \(\sim\) 是等价关系。
- 画出关系 \(\sim\)：在平面中画出底层类型 \(\mathbb{N}^2\) 的一部分，然后用不同颜色标出各个等价类。
```
local infix:50 "∼" => fun ((a, b) : ℕ × ℕ) (c, d) ↦ a + d = b + c

example : Reflexive (· ∼ ·) := by
  sorry

example : Symmetric (· ∼ ·) := by
  sorry

example : Transitive (· ∼ ·) := by
  sorry
```
考虑 \(\mathbb{Z}^2\) 上的关系 \(\sim\)，定义为：\((a,b)\sim(c,d)\) 当且仅当存在正整数 \(m\) 和 \(n\)，满足 \(mb(b^2-3a^2)=nd(d^2-3c^2)\)。证明 \(\sim\) 是等价关系。画出关系 \(\sim\)：在平面中画出底层类型 \(\mathbb{Z}^2\) 的一部分，然后用不同颜色标出各个等价类。
- 证明 \(\sim\) 是等价关系。
- 画出关系 \(\sim\)：在平面中画出底层类型 \(\mathbb{Z}^2\) 的一部分，然后用不同颜色标出各个等价类。
```
local infix:50 "∼" => fun ((a, b) : ℤ × ℤ) (c, d) ↦
  ∃ m n, m > 0 ∧ n > 0 ∧ m * b * (b ^ 2 - 3 * a ^ 2) = n * d * (d ^ 2 - 3 * c ^ 2)

example : Reflexive (· ∼ ·) := by
  sorry

example : Symmetric (· ∼ ·) := by
  sorry

example : Transitive (· ∼ ·) := by
  sorry
```