blog | Ma Jia-Jun （马家骏）

本文要讲清楚 Lean 中的定义相等和命题相等这两个概念。在这个过程中，我们也会解释其他相关概念。

相等命题的定义

inductive Eq : α → α → Prop where
  | refl (a : α) : Eq a a

Eq a b 记作 a = b，表示同一类型 α 中两个项相等的命题，称为命题相等（propositional equality）。唯一的构造子 Eq.refl 给出自反性的证明：对每个 a : α，都有 Eq.refl a : a = a。 ¹

rfl 的定义

def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a

花括号中的参数称为隐式参数，Lean 可以根据上下文推断它们，调用时通常不必填写。 rfl 的定义体就是 Eq.refl a，只是把 a 也设成了隐式参数。在 := rfl 中，Lean 根据目标推断 a。

内核检查证明项的类型时，按定义展开、计算等转换规则识别相同的表达式。这种关系叫定义相等（definitional equality）。如果目标 Eq t s 与某个 Eq a a 定义相等， Eq.refl a 就能作为该目标的证明。例如，1 + 2 和 2 + 1 都归约为 $3$ ，目标 1 + 2 = 2 + 1 因而与 3 = 3 定义相等：

import Init

example : 1 + 2 = 2 + 1 := rfl

这里的 example 让 Lean 检查冒号后的命题与 := 后的证明是否匹配。 rfl 在这里构造的是一个 Eq 证明；定义相等使它的类型与目标匹配。 ²

归纳类型与递归器

归纳类型 A 的定义列出了构造子，也就列出了定义函数时要处理的各种情形。 Lean 同时生成递归器（recursor）A.rec，让我们按这些情形定义函数。

先考虑单独定义的归纳类型 A : Type u，其构造子都返回 A。我们要定义的函数可以具有下面的类型：

F : (a : A) → motive a

这里 motive: A → Sort v 是函数的目标类型族，motive a 是函数在 a 处的返回类型。我们要为每个 a 给出一个值 F a : motive a。这样的函数称为依赖函数，因为返回类型可以随输入变化。若结果总属于同一个类型 β，取 motive := fun _ ↦ β，就得到普通函数 A → β。若 motive a 是命题，F a 就是这个命题的证明。

使用 A.rec 定义 F，需要提供两部分内容：

motive：说明每个输入 a 所需的结果类型 motive a。
每个构造子对应的分支：说明输入由这个构造子构成时，F 的值怎样给出。若构造子含有递归子项，分支还可以使用 F 处理那些子项所得的结果。

递归器把这些分支组成所需的函数，并规定它在各个构造子上的计算方式。它规定怎样使用归纳类型中的项得到结果，因此也称为消去原则。当函数的结果是证明时，这也给出了归纳证明的方法。 ³

下面的递归器把 motive 写在花括号里，同样作为隐式参数。这是因为 Lean 通常可以从后面参数的类型推断出 motive，不必每次都写出来。

PUnit：只有一个元素的类型

只有一个元素的类型称为单元素类型（singleton type）。 Core 中的 PUnit 就是这样的归纳类型： ⁴

inductive PUnit : Sort u where
  | unit : PUnit

PUnit 只有一个元素 PUnit.unit。给定目标类型族 motive : PUnit.u → Sort v，我们要定义函数：

F : (x : PUnit.{u}) → motive x

PUnit.rec 的完整类型是：

PUnit.rec :
  ∀ {motive : PUnit.{u} → Sort v}
    (unitCase : motive PUnit.unit.{u})
    (x : PUnit.{u}),
    motive x

由于 PUnit 只有一个元素，我们只需给出 motive PUnit.unit 中的一个元素 unitCase。 PUnit.rec 就用这个值作为 F PUnit.unit，给出所求的函数。

等式消去：Eq.rec

Eq.rec 的完整类型是：

Eq.rec :
  ∀ {α : Sort u} {a : α}
    {motive : (b : α) → (h : a = b) → Sort v}
    (reflCase : motive a (Eq.refl a))
    {b : α} (h : a = b),
    motive b h

先固定类型 α : Sort u 和左端 a : α，再让右端 b 变化。等式证明 h : a = b 是递归器要处理的输入， motive b h 则是所求函数在这一输入处的返回类型，或此时要证明的命题。

Eq 只有 refl 这一个构造子。因此，我们只须给出：

reflCase : motive a (Eq.refl a)

再给定任意 b 和证明 h : a = b，Eq.rec 就返回一个 motive b h 中的结果。

用 Eq.rec 证明 congrArg

congrArg 说的是：对相等的两个项应用同一个函数，结果仍然相等。 f a 这样的表达式称为函数应用（function application，简称 app）。定理的完整陈述是：

congrArg : ∀ {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β),
  a₁ = a₂ → f a₁ = f a₂

这里 f : α → β 的结果类型是固定的 β，所以两个应用项具有同一个类型。

example {α : Sort u} {β : Sort v} {a₁ a₂ : α}
    (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂ :=
  Eq.rec (motive := fun x _ ↦ f a₁ = f x) (Eq.refl (f a₁)) h

这里的 motive 表示：右端为 x 时，要证明 f a₁ = f x；下划线表示不使用等式证明本身。在自反情形下，目标变成 f a₁ = f a₁，由 Eq.refl (f a₁) 证明。最后将 h : a₁ = a₂ 交给 Eq.rec，便得到 f a₁ = f a₂ 的证明。

对类型进行等式替换

如果你打开 Lean 的标准库会发现congrArg并不是用上面的方法证明的，而是用 ▸ 记号：

theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β)
    (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
  h ▸ rfl

h ▸ e 是 Lean 的等式替换记号，替换发生在类型中的参数位置。在安装了 Lean 4 扩展的 VS Code 中，输入 \t，再按 Tab，就得到 ▸。 ⁵ 把程序确定的类型族记作 P。沿 h : a = b 正向替换时，程序从 e : P a 构造 h ▸ e : P b。这里 e 可以是证明，也可以是数据。

负责 h ▸ e 的精化程序是 Lean.Elab.Term.elabSubst。给定 h : a = b，它从类型中确定替换位置，构造通过类型检查的目标类型族，再按 Eq.rec 的等式消去规则构造结果，交给内核检查。 ⁶

例如，Lean 核心库的 Vector α n 表示由 n 个 α 类型的元素组成的向量，长度 n 是类型的一部分。 ⁷ 某个函数要求输入 Vector α m，而我们手中有 v : Vector α n 和长度相等的证明 h : n = m，就可以这样转换类型：

example {α : Type} {n m : Nat} (h : n = m) (v : Vector α n) : Vector α m :=
  h ▸ v

这里替换的是类型 Vector α n 中的长度参数 n，结果的类型是 Vector α m；向量中的元素及其顺序保持不变。

Nat.zero_add 的证明

自然数的两种构造形式是零和后继 Nat.succ n，后者就是 n + 1。自然数递归器 Nat.rec 的完整类型是：

Nat.rec :
  ∀ {motive : Nat → Sort u}
    (zeroCase : motive 0)
    (succCase : (n : Nat) → motive n → motive (Nat.succ n))
    (n : Nat),
    motive n

它让我们按零和后继两种情形定义函数：先给出零处的值，再说明怎样利用 n 及 n 处的结果，得到 Nat.succ n 处的结果。如果 motive 是命题族，后继分支收到的 motive n 就是归纳假设。

我们要证明命题相等 0 + n = n，其中 n : Nat 是任意自然数。

Nat.add 按第二个参数递归，定义如下： ⁸

def Nat.add : Nat → Nat → Nat
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (Nat.add a b)

由第二个分支，0 + Nat.succ n 定义相等于 Nat.succ (0 + n)。

当 n 是任意变量时，0 + n 与 n 并不定义相等。直接用 rfl 证明会失败：

example (n : Nat) : 0 + n = n := by rfl

Lean 报错：

Tactic `rfl` failed: The left-hand side
  0 + n
is not definitionally equal to the right-hand side
  n

此时第二个参数 n 尚未确定是零还是后继，无法按上述分支继续计算。

对 n 使用 Nat.rec，可以把库中证明的两个分支写成下面的显式递归器形式： ⁹

theorem Nat.zero_add : ∀ (n : Nat), 0 + n = n :=
  Nat.rec (motive := fun n ↦ 0 + n = n)
    rfl
    (fun n ih ↦ congrArg Nat.succ ih)

这里的 motive 是 fun n ↦ 0 + n = n，所以零处要证明 0 + 0 = 0，由 rfl 完成。后继分支中的 ih 是归纳假设 0 + n = n。 congrArg Nat.succ ih 在等式两边应用后继函数，得到 Nat.succ (0 + n) = Nat.succ n 的证明。由上面的加法定义，这个证明的类型与后继目标 0 + Nat.succ n = Nat.succ n 定义相等，因而完成证明。

引自 Lean 4.35.0 的 Eq 定义，省略说明注释。↩︎
这里引用的是证明项 rfl 的定义，省略了 match_pattern 属性，见 Prelude.lean。 by rfl 调用同名策略；本文的等式例子中，它同样依靠自反性和定义相等。↩︎
递归器的类型与计算规则见 Lean Language Reference：Recursor Types 与 Reduction。本文的声明、接口和输出均按 Lean 4.35.0 核对。↩︎
引自 Lean 4.35.0 的 PUnit 定义，省略说明注释。↩︎
扩展的缩写表将 t 映射为 ▸；Tab 用于确认 Unicode 输入。↩︎
实现见 Lean 4.35.0 的 elabSubst。↩︎
见 Lean 4.35.0 的 Vector 定义。↩︎
见 Lean 4.35.0 的 Nat.add，这里省略命名和编译注解。↩︎
Lean 4.35.0 中的原定理以递归方程书写，见 Nat.zero_add。↩︎

Ma Jia-Jun （马家骏）

Tag Archives: blog

Lean 中的相等：定义相等与命题相等