dependent-type - 为 Lean 中的自然数定义前置函数（pred 0 = 0）

Question

我正在学习精益证明助手。https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html中的一个练习是为自然数定义前置函数。有人可以帮我吗？

Answer 1

您可能熟悉 Lean 或某些函数式编程语言中的模式匹配，所以这里有一个使用这种机制的解决方案：

open nat

definition pred : ℕ → ℕ
| zero     := zero
| (succ n) := n

另一种方法是使用这样的递归：

def pred (n : ℕ) : ℕ :=
  nat.rec_on n 0 (λ p _, p)

在这里，0如果参数为零，我们返回的(λ p _, p)是一个匿名函数，它接受两个参数：递归调用的前任 ( p)和结果。匿名函数忽略第二个参数并返回前一个参数。npred p