定义精益自然数的前驱函数（pred 0 = 0）

Question

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

Answer 1

你可能熟悉的精益模式匹配或一些功能的编程语言，所以这里是使用这种机制的解决方案：

open nat 

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

这样做的另一种方法是使用recursor像这样：

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

这里，0就是我们返回如果参数是零，(λ p _, p)是匿名函数有两个参数：的前身（p）和递归调用pred p的结果。匿名函数忽略第二个参数并返回前一个参数。