LeiEq.md

十分钟魔法练习：莱布尼兹相等性

By 「玩火」

前置技能：构造演算

相等类型

相等关系可以作为一个命题，那么也可以作为一个类型，被称为相等类型（Identity type）。相等类型有多种编码形式，这里先介绍莱布尼兹（Leibniz）给出的定义：

x 和 y 相等，当且仅当他们的所有性质一样，也就是说对于所有 P 可以得到 P x 蕴含 P y

用构造演算表达就是：

Eq = (T: *) ⇒ (x: T) ⇒ (y: T) ⇒ 
     (P: T → *) → P x → P y

对于 Eq 类型，它拥有唯一的构造器用于构造出 x = x ，其类型为：

(T: *) → (x: T) → Eq T x x

自反性

相等类型的构造器的类型也是个命题，它指出对于任意的 x 都存在 x = x ，也就是相等的自反性（Reflexive），而构造器的实现就是对自反性的证明。为了证明自反性，可以观察一下展开了的构造器类型：

(T: *) → (x: T) → (P: T → *) → P x → P x

最终我们需要一个类型为 P x 的实例而在之前我们已经拿到了一个类型为 P x 的参数，直接作为函数结果即可：

Refl = (T: *) ⇒ (x: T) ⇒ 
       (P: T → *) ⇒ (Px: P x) ⇒ 
       Px

传递性

如果 x = y 并且 y = z 那么可以得到 x = z ，这就是相等的传递性（Transitivity），命题的类型是：

(T: *) → (x: T) → (y: T) → (z: T) →
Eq T x y → Eq T y z → Eq T x z

直接看可能比较难想出如何构造函数来证明传递性，还是可以按照如上方法展开类型：

(T: *) → (x: T) → (y: T) → (z: T) →
((P: T → *) → P x → P y) → ((P: T → *) → P y → P z) →
(P: T → *) → P x → P z

观察发现有参数类型为 P x 的实例，而通过类型为 (P: T → *) → P x → P y 的实例可以把它转换成类型为 P z 的实例，同样的方法还能继续转换成类型为 P z 的实例。于是就得到以下函数：

Trans = (T: *) ⇒ (x: T) ⇒ (y: T) ⇒ (z: T) ⇒
        (xEqy: Eq T x y) ⇒ (yEqz: Eq T y z) ⇒
        (P: T → *) ⇒ (Px: P x) ⇒ yEqz P (xEqy P Px)

对称性

相等是对称的，也就是说 x = y 一定能得到 y = x ，相等的对称性（Symmetry）用类型表示就是：

(T: *) → (x: T) → (y: T) → Eq T x y → Eq T y x

想要证明这个命题有一些难度，核心思想就是利用相等的定义来构造出合适的性质替换利用自反性构造出的实例等式两边的内容：

Sym = (T: *) ⇒ (x: T) ⇒ (y: T) ⇒
      (xEqy: Eq T x y) ⇒ 
      xEqy ((z: T) ⇒ Eq T z x) (Refl T x)

因为有了 xEqy 就可以把任意命题 Q x 变成 Q y，如果构造命题 Q = (z: T) ⇒ Eq T z x ，那么 Q x 就是 Eq T x x 也就是 Refl T x 构造出实例的类型，应用给 xEqy 就可以得到类型为 Q y 也就是 Eq T y x 的实例，也就是我们的目标。

合同性

如果 x = y 那么显然对于同一个函数 f 来说 f x = f y ，这就是相等的合同性（Congruence）也叫替换性（Substitution），用构造演算表示就是：

(A: *) → (B: *) → (f: A → B) → 
(x: A) → (y: A) → 
Eq A x y → Eq B (f x) (f y)

合同性的证明非常类似于对称性的证明，只需要构造一个命题 Q = (z: A) ⇒ P (f x) → P (f z) 即可：

Cong = (A: *) ⇒ (B: *) ⇒ (f: A → B) ⇒
       (x: A) ⇒ (y: A) ⇒
       (xEqy: Eq A x y) ⇒
       xEqy ((z: A) ⇒ Eq B (f x) (f z)) (Refl B (f x))