本页旨在解释 Idris 中用于证明命题等式（propositional equality）的一些技术。

证明命题等式（Propositional Equality）

我们已经看到，定义等式（definitional equality）可以通过 Refl 证明，因为它们总是归约为可以直接比较的值。

然而，对于命题等式（propositional equality），我们使用的是符号变量，这些变量并不总是能够归约。

以之前的例子为例：

plusReducesR : (n : Nat) -> plus n Z = n

在这种情况下，plus n Z 并不会归约为 n。即使等式两边可以被证明相等，我们也无法直接用 Refl 作为证明。

如果模式匹配无法覆盖所有 n 的情况，那么我们需要对 n 的所有可能取值进行匹配。在本例中

plusReducesR : (n : Nat) -> plus n Z = n
plusReducesR Z = Refl
plusReducesR (S k)
    = let rec = plusReducesR k in
          rewrite rec in Refl

我们无法用 Refl 来证明对所有 n 都有 plus n 0 = n。相反，我们需要对每种情况分别证明。例如，在第二行中，类型检查器会将 Z 代入被匹配的类型，并相应地化简类型。

替换（Replace）

这实现了"不可分辨同一性（indiscernability of identicals）"原则：如果两个项相等，那么它们具有相同的性质。换句话说，如果 x=y，那么我们可以在任何表达式中用 y 替换 x。在我们的证明中，可以这样表达：

如果 x=y，则 prop x = prop y

其中 prop 是表示性质的纯函数。在下方示例中，prop 是某个变量上的表达式，类型类似于：prop: n -> Type

因此，如果 n 是一个自然数变量，那么 prop 可以是类似 \n => 2*n + 3 的表达式。

要在我们的证明中使用这一点，prelude（前置库）中提供了如下函数：

||| Perform substitution in a term according to some equality.
replace : forall x, y, prop . (0 rule : x = y) -> prop x -> prop y
replace Refl prf = prf

如果我们给出一个等式（x=y）以及 x 的某个性质的证明（prop x），那么就能得到 y 的该性质的证明（prop y）。因此，在下例中，如果我们提供 p1 x``（即 ``x=2 的证明）和等式 x=y，就能得到 y=2 的证明。

p1: Nat -> Type
p1 n = (n=2)

testReplace: (x=y) -> (p1 x) -> (p1 y)
testReplace a b = replace a b

重写（Rewrite）

在实际使用中，replace 有时较难使用，因为通常隐式参数 prop 对机器来说难以推断。因此 Idris 提供了高级语法，能够自动计算性质并应用 replace。

示例：同样地，如果我们提供 p1 x``（即 ``x=2 的证明）和等式 y=x，就能得到 y=2 的证明。

p1: Nat -> Type
p1 x = (x=2)

testRewrite: (y=x) -> (p1 x) -> (p1 y)
testRewrite a b = rewrite a in b

我们可以这样理解 rewrite 的工作方式：

以等式 x=y 和性质 prop : x -> Type 开始

在 prop 中查找 x

将 prop 中所有出现的 x 替换为 y。

也就是说，我们在做替换操作。

注意，这里我们需要提供反向等式，即 y=x 而不是 x=y。这是因为 rewrite 会将等式左边替换为右边，并且这种替换发生在*返回类型*中。因此，在返回类型 y=2 中，我们需要应用 y=x，以便与参数 x=2 的类型匹配。

对称性与传递性（Symmetry and Transitivity）

除了"自反性（reflexivity）"，等式还遵循"对称性（symmetry）"和"传递性（transitivity）"，这些也包含在 prelude 中：

||| Symmetry of propositional equality
sym : forall x, y . (0 rule : x = y) -> y = x
sym Refl = Refl

||| Transitivity of propositional equality
trans : forall a, b, c . (0 l : a = b) -> (0 r : b = c) -> a = c
trans Refl Refl = Refl

异类等式（Heterogeneous Equality）

prelude 中同样包含：

||| Explicit heterogeneous ("John Major") equality. Use this when Idris
||| incorrectly chooses homogeneous equality for `(=)`.
||| @ a the type of the left side
||| @ b the type of the right side
||| @ x the left side
||| @ y the right side
(~=~) : (x : a) -> (y : b) -> Type
(~=~) x y = (x = y)