Lean 教程(二) ｜ 函数式编程

发表于 更新于 阅读次数： 字数： 6.4k 时间 ≈ 23 分钟
学习 Lean 的途径很多，具体取决于你的背景和偏好，这些教程有偏重数学的也有偏重编程的。

教程定位

学习 Lean 的教程和途径很多，具体取决于个人知识背景和偏好。这些教程里，有偏重数学的也有偏重编程的。

快速上手

  1. 自然数游戏 NNG4，在线交互式 Lean 教程，重点是证明自然数基本运算的属性。 Lean Game Server 托管各种学习游戏，包括集合论、逻辑和 Robo（一个关于本科数学的故事）等。

  2. 快速上手的 Lean 初探教程，涵盖使用 Lean 证明的一些基本概念，也包括初级分析、抽象拓扑和数理逻辑的独立主题。

  3. 如果希望直接从源代码学习， Lean API 文档 不仅包括 Mathlib ，还包括 Std、 Batteries、Lake 和核心编译器，这是最接近现有综合参考手册的内容。

文档教程

  1. 数学导向的 Mathematics in Lean，以及节奏更缓的 The Mechanics of Proof

  2. 从类型论基础出发的 Theorem Proving in Lean，计算机科学导向的 The Hitchhiker’s Guide to Logical Verification

  3. 侧重将 Lean 作为编程语言的 Functional Programming in Lean 以及侧重元编程策略编写的 Metaprogramming in Lean

  4. 更关注 LEAN 本身而不仅是使用的 Reference manual

系列定位

教程系列从 LEAN 函数式编程切入，在文档基础上，加上个人的理解和精炼。主要参考 Theorem Proving in Lean，目前也有社区翻译版 fp-lean-zh。

该书面向的场景：使用 LEAN 作为证明助手的数学家在某些时候可能需要编写自己的证明自动化工具。随着工具变得越来越复杂，它们开始类似于函数式语言的程序，不过多数数学家都接受过 Python 和 Mathematica 等语言的培训。这本书可以帮助弥合差距，使更多的数学家能够编写可维护和易于理解的证明自动化工具。

本地安装 Lean 的方式参看上一篇，也可以通过 live.lean-lang.org 或 live.leanprover.cn 在线使用。

基础知识

交互方式

Python, Java, C# 这类语言通常提供一个 REPL(Read Eval Print Loop)用于交互式地执行命令；而 LEAN 语言服务器协议（LSP）的扩展版本，将交互功能集成到编辑器上（比如 vscode），用户在输入命令的同时，在编译器上获取反馈。

如果我们希望计算某个表达式的值，使用 #eval 命令：

1
2
#eval 1 + 2
#eval String.append "hello, " "lean!"

通过查看右侧面板，或者将鼠标光标放在 #eval 上，查看表达式取值。

20230910101410

为方便展示，我们用注释的形式将显示结果写在代码下方，LEAN 的注释格式有两种：单行注释 -- 和多行注释 /- ... -/。

边际效应

大多数语言都是命令式的(imperative)，程序由一系列执行语句组成，用于计算结果。此外，程序能访问到变量的内存，并在执行过程中修改变量的取值。因为这种可修改的特性，这些程序通常存在边际效应(side effects)，比如某个表达式的值可能会因为执行顺序的不同而不同。

关于边际效应，用几个例子讲讲我的理解。在下边的 Python 代码中，函数 f 依赖于变量 a，而变量 a 的修改会导致 f 执行结果变化：

1
2
3
4
5
6
a = 1
def f():
    return a
print(f()) # 1
a = 2
print(f()) # 2

类似地，在 C 数组中，如果我们修改了数组 a 的值，那么指向 a 的指针 b 的值也会发生变化：

1
2
3
4
int a[2] = {1, 2};
int* b = a;
a[1] = 3;
printf("%d\n", b[1]);

但在 LEAN 中，程序都是表达式，其取值是确定不变的。Haskell 和 LEAN 都具有这个特性，而且在 .hs 或 .lean 文件如果对一个变量做多次定义编译器会抛出错误。由于 Haskell 还支持交互式编程，我们用 Haskell 来解释这个特性：

1
2
3
4
5
6
7
ghci> a = 1
ghci> f x = x + a -- 定义函数 f(x) = x + a
ghci> f 2
3
ghci> a = 2 -- 修改变量的值
ghci> f 2
3

在最开始定义 f 的时候，不是将 a 放入函数体，而是放入 a 的值。所以修改 a 并不会影响 f，而且 f 每次执行的结果都是确定不变的。此外，像 a=1;a=2 这种变量重定义仅在 REPL 中有效，在 .hs 文件中仍然会报错。

类似地，LEAN 的判断语句也是一个表达式，而且 if 必须伴随 else，因为表达式取值必须是确定的，不存在 Null 取值。

1
2
3
4
#eval if 1 > 2 then 1 else 2
-- 2
#eval if false then "yes" else "no"
-- "no"

本节回顾：无边际效应，所有程序都是表达式，不允许对一个变量做多次定义或修改。

变量、函数和类型

类型在程序中有很多作用，比如

  1. 允许编译器决定变量在内存中的存储方式
  2. 帮助程序员向其他人传达意图，限定程序输入输出的规范
  3. 防止各种潜在错误，不匹配类型的数据运算
  4. 帮助 LEAN 编译器生成辅助代码

LEAN 的所有程序本质都是表达式，且表达式都有其类型。通常，编译器会进行自动推断来判读表达式类型，但也可以声明类型

1
2
3
4
5
6
#eval (1 + 2 : Nat) -- 自然数类型 Nat
-- 3
#eval 1 - 2 -- 自然数 0 是最小值
-- 0
#eval (1 - 2 : Int) -- 声明数据类型为 Int
-- -1

我们可以通过 #check 来检查类型。

1
2
3
4
5
6
#check 1 + 2
-- 1 + 2 : Nat
#check (1 - 2 : Int)
-- 1 - 2 : Int
#check "hello"
-- "hello" : String

在函数式编程语言中，函数是一等公民。这个特性在 Haskell 和 LEAN 语言上更加明显，它们甚至连定义格式也是完全一致的，变量就是函数的特殊情形。

LEAN 通过 def 关键字定义变量，其中赋值号用 := 而不是 =，后者被用于判断语句。

1
2
3
def x := 1 -- 定义 Nat 类型的变量 x
def y : Int := 1 - 2
def astr := "hello"

变量的定义格式为 def 变量名 : 类型 := 表达式，其中 类型 可以省略，编译器会自动推断。至于函数的定义格式，在 := 左边添加参数就得到了：

1
2
3
4
5
6
7
8
9
def f (x : Nat) := x + 1 -- 一参函数
def myplus (x y : Int) : Int := x + y -- 两参函数
#eval myplus 1 2
-- 3
def plusthree x y z := x + y + z
def maximum (n : Nat) (k : Nat) : Nat :=
  if n < k then
    k
  else n

函数的定义格式为 def 函数名 (x1 x2 ... : 类型) (y1 y2 ...: 类型) ... : 返回类型 := 表达式，由于编译器会自动推断，变量的类型也可以省略。

从这里不难看出，变量本质上就是零参数的函数。

此外 LEAN 的函数调用不需要加括号，f x y 等同于 f(x, y)，比如

1
2
#eval String.append "hello, " "lean!"
-- "hello, lean!"

同样地，我们可以用 #check 来检查函数类型，但需加上括号，否则返回的是函数签名(signature)。

1
2
3
4
5
6
#check f -- 返回函数签名
-- f (x : Nat) : Nat
#check (f)
-- f : Nat → Na
#check (myplus)
-- myplus : Int → Int → Int

多参函数的类型是 Int → Int → Int，根据映射的右结合律，可以理解为 Int → (Int → Int)。也即，二参函数 myplus 由两个单参函数复合而来，其中第一个函数返回值是个单参函数。具体地，我们可以只传递一个参数，并查看返回结果

1
2
3
def addone := myplus 1
#eval addone 2
-- 3

这种多参转化为单参的方式称为柯里化(curring)，以数学家 Haskell Curry 命名。

和通常的语言相比，LEAN 有一个最不寻常的特性，它的类型也是一等公民。举个例子，假设你觉得 String 这个名字太长，那可以定义一个新的类型 Str 来代替它

1
2
3
4
5
6
def Str : Type := String -- 将 String 作为传入参数！！！
#check Str
-- Str : Type
def hello : Str := "hello"
#check hello
-- hello : Str

新类型 Str 赋值为 String，能沿用针对 String 的运算，比如

1
2
3
4
5
6
def connectString (str1 str2 : String) := str1 ++ str2
#check (connectString)
-- connectString : String → String → String
def aStr := connectString hello "lean"
#check aStr
-- aStr : String

尽管 connectString 传入参数要求 String 类型，但使用 Str 也是符合的。至于输出结果为 String 而不是 Str，这是 connectString 输出类型决定的。

新手在这里可能遇到一个错误：现在假设我们觉得用 Nat 表达自然数太简短，想用 NaturalNumber 来代替，那么定义

1
def NaturalNumber : Type := Nat

接着定义变量 a，这将产生错误

1
2
3
4
def a : NaturalNumber := 1
-- 错误信息 -- 
failed to synthesize instance
  OfNat NaturalNumber 1

这个错误源于 LEAN 的一个特殊机制：数字输入的重载特性。为了适应不同的类型需求，当我们在使用数字 1,2,3... 时，如果编译器能判断数字取什么类型有意义，这些数字 123... 才开始匹配转化为类型。

1
2
3
4
5
6
7
8
9
def a := 1
def b := -1
def c : Int := 1
#check a
-- a : Nat
#check b
-- b : Int
#check c
-- c : Int

输入 1 得到 Nat，输入 -1 得到 Int，通过指定类型 1 也可以得到 Int。

而当执行 1 : NaturalNumber 时，编译器并不知道 1 应该适应为什么类型，正确写法应当是

1
2
3
4
#eval ((1 : Nat) : NaturalNumber)
-- 1
#check ((1 : Nat) : NaturalNumber)
-- 1: NaturalNumber

通过添加括号来让 1 有意义，继而在转化为 NaturalNumber。或者我们再举一个例子，

1
2
3
4
5
6
#eval 1-2 -- 1 和 2 默认为 Nat，运算得 0
-- 0
#eval ((1 - 2) : Int) -- 编译器推断 1 和 2 为 Int，运算得 -1
-- -1
#eval (1 - 2 : Int) -- 与上边等价
-- -1

顺带一提，冒号 : 的优先级极低，经常要结合括号使用。

这个机制很奇怪。
Haskell 的处理方式很自然，通过参数化的 Num a => a 来表示数字类型，以此支持不同类型数值的运算。
LEAN 重载的规则里，1 本身没有类型，如果简单地理解为 Nat 类型，在运算 (1-2):Int 中会先得到 0:Nat，然后转化为 Int，这样就不对了。
可能整体学下来会有新的理解，附一段原话：
This error occurs because Lean allows number literals to be overloaded. When it makes sense to do so, natural number literals can be used for new types, just as if those types were built in to the system. This is part of Lean’s mission of making it convenient to represent mathematics, and different branches of mathematics use number notation for very different purposes. The specific feature that allows this overloading does not replace all defined names with their definitions before looking for overloading, which is what leads to the error message above.

在一些场景中，比如希望用简写 N 代替 Nat，可以用 abbrev 关键字，类似 C 语言的 #define。

1
2
abbrev N : Type := Nat
def a : N := 1

在幕后，一些定义会在重载解析期间被内部标记为可展开的，而另一些则不会标记。可展开的定义称为可约的（Reducible）。控制可约性对 Lean 的灵活性而言至关重要：完全展开所有的定义可能会产生非常大的类型，这对于机器处理和用户理解来说都很困难。使用 abbrev 生成的定义会被标记为可约定义。

本节回顾：

  1. Lean 的所有程序本质上都是表达式，都存在类型，可以通过 #check 来检查。
  2. 在函数式编程语言中，函数是一等公民。实际上，变量等同于零参数的函数。
  3. 一般地，函数定义格式为 def 函数名 (x1 x2 ... : 类型) (y1 y2 ...: 类型) ... : 返回类型 := 表达式，包括四个部分，函数名，输入参数类型，输出类型，表达式。由于编译器会自动推断，变量类型也可以省略。
  4. Lean 函数经常省略括号，比如 f x y 理解为 f(x, y) 或者从柯里化的角度理解为 (f x)(y) ，即通过两个单参数函数复合得。从类型上看，Lean 满足右结合率，比如 Int → Int → Int 理解为 Int → (Int → Int)。
  5. Lean 不仅函数是一等公民，甚至类型也是一等公民。
  6. abbrev 关键字可以为一些变量设置缩写，比如简写类型名称。

结构体

结构体常用于为表达复杂数据，LEAN 的结构体使用 structure 关键字定义：

1
2
3
4
structure Point where
    x : Float
    y : Float
deriving Repr

最后一行 deriving Repr 生成默认显示，方便 #eval 打印结果的输出，作用类似于 Python 的 __repl__ 方法。如果该行缺省在执行 #eval 时会报错。

结构体通过 {} 来构建，比如

1
2
3
4
5
def origin : Point := { x := 0, y := 0 }
#eval origin
-- { x := 0.000000, y := 0.000000 }
#eval origin.x
-- 0.000000

定义两点的加法函数

1
2
3
4
5
6
7
8
def addPoints (p1 : Point) (p2 : Point) : Point :=
  { x := p1.x + p2.x, y := p1.y + p2.y }
#eval addPoints { x := 1, y := 2 } { x := 3, y := 4 }
-- { x := 4.000000, y := 6.000000 }
#check { x := 0.0, y := 0.0 :Point} -- 声明类型
-- { x := 0.0, y := 0.0 } : Point
#check { x := 0.0, y := 0.0 } -- 报错，类型不明
-- invalid {...} notation, expected type is not known

最后一个例子报错，因为 LEAN 无法推断 {} 的数据类型，而第一处 #eval 不会报错，因为 LEAN 从 addPoints 函数推断了数据为 Point。

由于 LEAN 的变量不可变，如果要修改变量的某个字段，比如把点 {x:=1, y:=2} 的 x 取值为 0，只能创建新变量：

1
def zeroX (p:Point) : Point := { x := 0, y:= p.y }

但如果结构体的字段非常多，可以用 with 语法修改特定字段，把其他照抄：

1
def zeroX (p:Point) : Point := { p with x := 0 }

前边例子用 origin.x 获取字段 x 的值，这本质上是执行了一个函数 Point.x

1
2
3
4
5
6
7
8
9
#check Point.x -- 查看函数签名
-- Point.x (self : Point) : Float
#check (Point.x) -- 查看函数类型
-- Point.x : Point → Float
def p : Point := { x := 1, y := 2 }
#eval p.x
-- 1.000000
#eval Point.x p
-- 1.000000

这是 LEAN 针对 . 的一个语法，p.func 会执行 Point.func 函数，并以 p 作为匹配到的最左侧的参数。

举个例子，定义结构体上的函数 Point.modifyBoth：

1
2
3
4
5
def Point.modifyBoth (f : Float → Float) (p : Point) : Point :=
  { x:= f p.x, y := f p.y }
def f (x : Float) := x + 1
#eval p.modifyBoth f
-- { x := 2.000000, y := 3.000000 }

这里定义了 Point.modifyBoth 函数，其接受两个参数，且第二参为最左侧的 Point 类型参数。执行 p.modifyBoth f 等同于调用 Point.modifyBoth f p。

除了定义 Point 时的字段 x, y，结构体默认还定义了构造子 Point.mk，用于构造 Point 类型的数据。比如

1
def p' : Point := Point.mk 1 2 -- 通过构造器构造

如果我们希望改用其他名称，可以在一开始定义结构体 Point 时，加上一行

1
2
3
4
5
structure Point where
  mymaker ::
  x : Float
  y : Float
deriving Repr

此时可以通过 Point.mymaker 1 2 来定义 Point 类型数据。

这部分知识和 Python 的面向对象编程有点类似，p.xxx 是以 p 作为 self 参数去执行调用方法。

本节回顾：

  1. 结构体通过 structure 结构体名 where (x1 : 类型1) ... deriving Repr 的方式定义，使用 {} 进行初始化。
  2. 在拷贝数据时，可用 with 方法，比如 {p with x:=1}。
  3. 用 . 方法访问结构体内容，p.func 本质上执行了 Point.func ，并以 p 作为匹配到的最左侧的参数。

数据类型，模式和递归

这节开始，考察抽象的理解能力。

数据类型

前边介绍了结构体，多个独立的数据块组合成一个连贯的整体，作为全新的类型。这种将一组值组合在一起的类型（如结构体）称为积类型（Product Type）。然而，许多领域的概念不能自然地表示为结构体，例如计算器的二元运算符，加法、减法和乘法。结构体无法提供一种简单的方法来编码多项选择。

结构体是跟踪固定字段集的绝佳方式，但许多应用程序需要可能包含任意数量元素的数据。大多数经典的数据结构（例如树和列表）具有递归结构，其列表的尾部本身是一个列表，或者二叉树的左右分支本身是二叉树。在计算器中，加法表达式中的加数本身可能是乘法表达式。

允许选择的类型称为和类型（Sum Type），而可以包含自身实例的类型称为递归类型（Recursive Datatype）。递归和类型称为归纳类型（Inductive Datatype），因为可以用数学归纳法来证明有关它们的陈述。在编程时，归纳类型通过模式匹配和递归函数来转化。

许多内置类型是标准库中的归纳类型。例如，Bool 就是一个归纳类型：

1
2
3
inductive Bool where
  | false : Bool
  | true : Bool

第一行定义新类型（Bool）的名称，而其余各行分别描述了一个构造子。

与结构体的构造子一样，归纳类型的构造子用于产生该类型的元素。与结构体不同，归纳类型可以有多个构造子。这里有两个构造子，true 和 false，并且都不接受任何参数。这些构造子保存在类型同名的命名空间，例如 Bool.true 和 Bool.false。在 Lean 标准库中，true 和 false 从此命名空间中重新导出，以便可以单独编写它们。

举个例子：

1
2
3
4
5
6
7
8
inductive Demo where
  | a : Demo
  | b : Demo

#check a -- 变量未定义
#check Demo.a -- Demo 类型
open Demo -- 打开命名空间
#check a

和抽象类型不同，比如

1
2
3
abstract type Bool end
struct True <: Bool end
struct False <: Bool end

在面向对象的示例中，True 和 False 都是比 Bool 更具体的类型，而 Lean 定义仅引入了新类型 Bool。

归纳数据类型 Nat 的定义如下：

1
2
3
inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

在这里，构造子 zero 表示 0 属于 Nat，而构造子 succ 表示 (n : Nat) 的后继也属于 Nat。通过这两个构造子，我们能表达整个自然数集。

同样地，为了表达 Nat，在其他语言中需要定义三个类型：

1
2
3
4
5
6
7
8
abstract type Nat end
struct Zero <: Nat end
struct Succ <: Nat
  n ::Nat
end
zero = Zero()
one = Succ(zero)
...

这样会定义比 Lean 中等价的项更多的类型。此外，这个示例突出显示了 Lean 构造子更像是抽象类的子类，而不是像 C# 或 Java 中的构造函数。

注：Lean 构造子对应于 JavaScript 或 TypeScript 中的对象，这些对象包含一个标识内容的标记。

模式匹配

在很多语言中，这类数据首先会使用 instance-of 运算符来检查接收了哪个子类，然后读取给定子类中可用的字段值。instance-of 会检查确定要运行哪个代码，以确保此代码所需的数据可用，而数据由字段本身提供。在 Lean 中，这两个目的均由模式匹配（Pattern Matching）实现。

使用模式匹配的函数示例是 isZero，这是一个当其参数为 Nat.zero 时返回 true 的函数，否则返回 false。

def isZero (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => false
match 表达式为函数参数 n 提供了解构。若 n 由 Nat.zero 构建，则采用模式匹配的第一分支，结果为 true。若 n 由 Nat.succ 构建，则采用第二分支，结果为 false。

isZero Nat.zero 的逐步求值过程如下：

isZero Nat.zero
===>
match Nat.zero with
| Nat.zero => true
| Nat.succ k => false
===>
true
isZero 5 的求值过程类似：

isZero 5
===>
isZero (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))))
===>
match Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))) with
| Nat.zero => true
| Nat.succ k => false
===>
false
isZero 中模式的第二分支中的 k 并非装饰性符号。它使 succ 的参数 Nat 可见，并提供了名称。然后可以使用该较小的数字计算表达式的最终结果。

正如某个数字 n
的后继比 n
大 1（即 n+1
），某个数字的前驱比它小 1。如果 pred 是一个查找 Nat 前驱的函数，那么以下示例应该能得到预期的结果：

#eval pred 5

4

#eval pred 839

838
由于 Nat 无法表示负数，因此 0 有点令人费解。在使用 Nat 时，会产生负数的运算符通常会被重新定义为产生 0 本身：

#eval pred 0

0
要查找 Nat 的前驱，第一步是检查它是使用哪个构造子创建的。如果是 Nat.zero，则结果为 Nat.zero。如果是 Nat.succ，则使用名称 k 引用其下的 Nat。而这个 Nat 即是所需的前驱，因此 Nat.succ 分支的结果是 k。

def pred (n : Nat) : Nat :=
match n with
| Nat.zero => Nat.zero
| Nat.succ k => k
将此函数应用于 5 会产生以下步骤：

pred 5
===>
pred (Nat.succ 4)
===>
match Nat.succ 4 with
| Nat.zero => Nat.zero
| Nat.succ k => k
===>
4
模式匹配不仅可以用于和类型，还可用于结构体。例如，一个从 Point3D 中提取第三维度的函数可以写成如下：

def depth (p : Point3D) : Float :=
match p with
| { x:= h, y := w, z := d } => d
在这种情况下，直接使用 z 访问器会简单得多，但结构体模式有时是编写函数的最简单方法。

递归函数

引用正在定义的名称的定义称为递归定义（Recursive Definition）。归纳数据类型允许是递归的，事实上，Nat 就是这样的数据类型的一个例子，因为 succ 需要另一个 Nat。递归数据类型可以表示任意大的数据，仅受可用内存等技术因素限制。就像不可能在数据类型定义中为每个自然数编写一个构造器一样，也不可能为每个可能性编写一个模式匹配用例。

递归数据类型与递归函数可以很好地互补。一个简单的Nat 递归函数是检查其参数是否是偶数。在这种情况下，zero 是偶数。像这样的代码的非递归分支称为 基本情况（Base Case）。奇数的后继是偶数，偶数的后继是奇数。这意味着使用 succ 构建的数字当且仅当其参数不是偶数时才是偶数。

def even (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => not (even k)
这种思维模式对于在Nat 上编写递归函数是非常典型的。首先，确定对 zero 做什么。然后，确定如何将任意 Nat 的结果转换为其后继的结果，并将此转换应用于递归调用的结果。此模式称为 结构化递归（Structural Recursion）。

不同于许多语言，Lean 默认确保每个递归函数最终都会到达基本情况。从编程角度来看，这排除了意外的无限循环。但此特性在证明定理时尤为重要，而无限循环会产生重大的困难。由此产生的一个结果是，Lean 不会接受尝试对原始数字递归调用自身的 even 版本：

def evenLoops (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => not (evenLoops n)
错误消息的主要部分是 Lean 无法确定递归函数是否最终会到达基本情况（因为它不会）。

fail to show termination for
evenLoops
with errors
structural recursion cannot be used

well-founded recursion cannot be used, ‘evenLoops’ does not take any (non-fixed) arguments
尽管加法需要两个参数，但只需要检查其中一个参数。要将零加到数字 n
上，只需返回 n
。要将 k
的后继加到 n
上，则需要得到将 k
加到 n
的结果的后继。

def plus (n : Nat) (k : Nat) : Nat :=
match k with
| Nat.zero => n
| Nat.succ k’ => Nat.succ (plus n k’)
在 plus 的定义中，选择名称 k’ 表示它与参数 k 相关联，但并不相同。例如，展开 plus 3 2 的求值过程会产生以下步骤：

plus 3 2
===>
plus 3 (Nat.succ (Nat.succ Nat.zero))
===>
match Nat.succ (Nat.succ Nat.zero) with
| Nat.zero => 3
| Nat.succ k’ => Nat.succ (plus 3 k’)
===>
Nat.succ (plus 3 (Nat.succ Nat.zero))
===>
Nat.succ (match Nat.succ Nat.zero with
| Nat.zero => 3
| Nat.succ k’ => Nat.succ (plus 3 k’))
===>
Nat.succ (Nat.succ (plus 3 Nat.zero))
===>
Nat.succ (Nat.succ (match Nat.zero with
| Nat.zero => 3
| Nat.succ k’ => Nat.succ (plus 3 k’)))
===>
Nat.succ (Nat.succ 3)
===>
5
考虑加法的一种方法是 n+k
将 Nat.succ 应用于 n
k
次。类似地，乘法 n×k
将 n
加到自身 k
次，而减法 n−k
将 n
的前驱求得 k
次。

def times (n : Nat) (k : Nat) : Nat :=
match k with
| Nat.zero => Nat.zero
| Nat.succ k’ => plus n (times n k’)

def minus (n : Nat) (k : Nat) : Nat :=
match k with
| Nat.zero => n
| Nat.succ k’ => pred (minus n k’)
并非每个函数都可以轻松地使用结构化递归来编写。将加法理解为迭代的 Nat.succ，将乘法理解为迭代的加法，将减法理解为迭代的前驱，这表明除法可以实现为迭代的减法。在这种情况下，如果分子小于分母，则结果为零。否则，结果是将分子减去分母除以再除以分母所得的后继。

def div (n : Nat) (k : Nat) : Nat :=
if n < k then
0
else Nat.succ (div (n - k) k)
只要第二个参数不为 0，这个程序就会终止，因为它始终朝着基本情况前进。然而，它不是结构化递归，因为它不遵循「为零找到一个结果，然后将较小的 Nat 的结果转换为其后继的结果」的模式。特别是，该函数的递归调用，应用于另一个函数调用的结果，而非输入构造子的参数。因此，Lean 会拒绝它，并显示以下消息：

fail to show termination for
div
with errors
argument #1 was not used for structural recursion
failed to eliminate recursive application
div (n - k) k

argument #2 was not used for structural recursion
failed to eliminate recursive application
div (n - k) k

structural recursion cannot be used

failed to prove termination, use termination_by to specify a well-founded relation
此消息表示 div 需要手动证明停机。这个主题在最后一章中进行了探讨。

多态