Lean Acc关系

介绍

在 Lean 中，Acc 关系是一个用于定义归纳和递归的重要工具。它代表“可访问性”（Accessibility），用于描述一个关系是否满足某种归纳性质。通过 Acc 关系，我们可以确保递归定义在逻辑上是合理的，从而避免无限递归等问题。

Acc 关系的核心思想是：如果一个元素 x 在某种关系下没有无限递减的序列，那么 x 是可访问的。换句话说，Acc 关系帮助我们证明递归定义在某种关系下是良基的（well-founded）。

在 Lean 中，Acc 关系通常与某种二元关系 r 一起使用。给定一个类型 α 和一个二元关系 r : α → α → Prop，Acc r x 表示元素 x 在关系 r 下是可访问的。

inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop
| intro (x : α) (h : ∀ y, r y x → Acc r y) : Acc r x

这里，Acc.intro 构造器表示：如果对于所有 y，只要 r y x 成立，那么 y 也是可访问的，那么 x 就是可访问的。

Acc 关系的一个重要应用是帮助我们定义递归函数。通过 Acc，我们可以确保递归调用总是在“更小”的元素上进行，从而避免无限递归。

以下是一个简单的例子，展示了如何使用 Acc 关系定义一个递归函数来计算自然数的阶乘：

def factorial : ℕ → ℕ
| 0       := 1
| (n + 1) := (n + 1) * factorial n

在这个定义中，Lean 会自动为我们处理递归的终止性。然而，如果我们想要手动证明递归的终止性，可以使用 Acc 关系。

假设我们有一个关系 r，并且我们想要定义一个递归函数 f，使得每次递归调用都是在 r 下“更小”的元素上进行的。我们可以使用 Acc 关系来证明递归的终止性。

def f {α : Type} (r : α → α → Prop) (h : ∀ x, Acc r x) (x : α) : ℕ :=
  Acc.rec_on (h x) (λ x _ ih, 1 + (ih (λ y hy, hy)))

在这个例子中，f 函数接受一个关系 r 和一个证明 h，该证明表明对于所有 x，x 在关系 r 下是可访问的。然后，f 使用 Acc.rec_on 来定义递归行为。

Acc 关系是 Lean 中用于处理归纳与递归的重要工具。它帮助我们确保递归定义在逻辑上是合理的，并且可以避免无限递归等问题。通过理解 Acc 关系，我们可以更好地掌握 Lean 中的归纳与递归技巧。

提示

如果你对 Acc 关系还有疑问，建议阅读 Lean 官方文档中关于归纳与递归的部分，或者参考相关的教程和示例代码。