2. 依值类型论
依值类型论（Dependent type theory）是一种强大而富有表达力的语言，允许你表达复杂的数学断言， 编写复杂的硬件和软件规范，并以自然和统一的方式对这两者进行推理。 Lean 是基于一个被称为 构造演算（Calculus of Constructions） 的依值类型论的版本， 它拥有一个可数的非累积性宇宙（non-cumulative universe）的层次结构以及归纳类型（Inductive type）。 在本章结束时，你将学会一大部分。
2.1. 简单类型论
“类型论”得名于其中每个表达式都有一个关联的 类型。
例如，在一个给定的语境中，x + 0 可能表示一个自然数，f 可能表示一个定义在自然数上的函数。
对于那些喜欢精确定义的人来说，Lean 中的自然数是任意精度的无符号整数。
这里的一些例子展示了如何声明对象以及检查其类型。
/- 定义一些常数 -/
def m : Nat := 1 -- m 是自然数
def n : Nat := 0
def b1 : Bool := true -- b1 是布尔型
def b2 : Bool := false
/- 检查类型 -/
#check m#check n#check n + 0#check m * (n + 0)#check b1-- "&&" 是布尔与
#check b1 && b2-- 布尔或
#check b1 || b2-- 布尔 "真"
#check true/- 求值（Evaluate） -/
#eval 5 * 4#eval m + 2#eval b1 && b2
位于 /- 和 -/ 之间的文本组成了一个注释块，会被 Lean 忽略。
类似地，两条横线 -- 表示该行的其余部分包含也会被忽略的注释。
注释块可以嵌套，这样就可以“注释掉”一整块代码，这和许多编程语言都是一样的。
def 关键字声明工作环境中的新常量符号。在上面的例子中，def m : Nat := 1
定义了一个 Nat 类型的新常量 m，其值为 1。
#check 命令要求 Lean 报告它们的类型；在 Lean 中，用于向系统询问信息的辅助命令通常都以井号 (#) 开头。
#eval 命令让 Lean 计算给出的表达式。
你应该试试自己声明一些常量和检查一些表达式的类型。以这种方式声明新对象是试验系统的好方法。
简单类型论的强大之处在于，你可以从其他类型中构建新的类型。例如，如果 a 和 b 是类型，a -> b
表示从 a 到 b 的函数类型，a × b
表示由 a 元素与 b 元素配对构成的类型，也称为 笛卡尔积。注意
× 是一个 Unicode 符号。合理使用 Unicode 提高了易读性，所有现代编辑器都支持它。在
Lean 标准库中，你经常看到希腊字母表示类型，Unicode 符号 → 是 -> 的更紧凑版本。
#check Nat → Nat#check Nat -> Nat
#check Nat × Nat#check Prod Nat Nat
#check Nat → Nat → Nat#check Nat → (Nat → Nat)
#check Nat × Nat → Nat#check (Nat → Nat) → Nat#check Nat.succ#check (0, 1)#check Nat.add
#check Nat.succ 2#check Nat.add 3#check Nat.add 5 2#check (5, 9).1#check (5, 9).2
#eval Nat.succ 2#eval Nat.add 5 2#eval (5, 9).1#eval (5, 9).2同样，你应该自己尝试一些例子。
让我们看一些基本语法。你可以通过输入 \to 或者 \r 或者 \-> 来输入 Unicode 箭头 →。
你也可以使用 ASCII 替代符号 ->，所以表达式 Nat -> Nat 和 Nat → Nat
意思是一样的。这两个表达式都表示以一个自然数作为输入并返回一个自然数作为输出的函数类型。
Unicode 符号 × 是笛卡尔积，用 \times 输入。通常使用小写的希腊字母
如 α，β，和 γ 来表示类型变量。你可以
用 \a，\b，和 \g 来输入它们。
这里还有一些需要注意的事情。第一，函数 f 应用到值 x 上写为 f x（例如，Nat.succ 2）。
第二，当写类型表达式时，箭头是 右结合 的；例如，
Nat.add 的类型是 Nat → Nat → Nat，等价于
Nat → (Nat → Nat)。因此你可以
把 Nat.add 看作一个函数，它接受一个自然数并返回
另一个函数，该函数接受一个自然数并返回一个自然数。
在类型论中，这通常比把 Nat.add 写成接受一对自然数作为
输入并返回一个自然数作为输出的函数更方便。例如，它允许
你“部分应用”函数 Nat.add。上面的例子显示
Nat.add 3 具有类型 Nat → Nat，即 Nat.add 3 返回一个
“等待”第二个参数 n 的函数，然后
等价于写 Nat.add 3 n。
你已经看到，如果你有 m : Nat 和 n : Nat，那么
(m, n) 表示 m 和 n 的有序对，其类型为
Nat × Nat。这为你提供了一种创建自然数对的方法。
反过来，如果你有 p : Nat × Nat，那么你可以写
p.1 : Nat 和 p.2 : Nat。这为你提供了一种提取
其两个分量的方法。
2.2. 类型作为对象
Lean 的依值类型论扩展简单类型论的一种方式是，类型本身（像 Nat 和 Bool 这样的实体）是一等公民，也就是说它们本身也是
对象。为了做到这一点，它们中的每一个也必须有一个
类型。
#check Nat#check Bool#check Nat → Bool#check Nat × Bool#check Nat → Nat#check Nat × Nat → Nat#check Nat → Nat → Nat#check Nat → (Nat → Nat)#check Nat → Nat → Bool#check (Nat → Nat) → Nat
你可以看到上面的每个表达式都是类型为 Type 的对象。你也可以为类型声明新的常量：
def α : Type := Nat
def β : Type := Bool
def F : Type → Type := List
def G : Type → Type → Type := Prod
#check α#check F α#check F Nat#check G α#check G α β#check G α Nat
正如上面的例子所示，你已经看到了一个类型为
Type → Type → Type 的函数示例，即笛卡尔积 Prod：
def α : Type := Nat
def β : Type := Bool
#check Prod α β#check α × β
#check Prod Nat Nat#check Nat × Nat
这里有另一个例子：给定任意类型 α，类型 List α
表示类型为 α 的元素的列表类型。
既然 Lean 中的每个表达式都有一个类型，那么很自然地会问：
Type 本身有什么类型？
你实际上已经遇到了 Lean 类型系统中最微妙的方面之一。 Lean 的底层基础有一个无限的类型层次结构：
可以将 Type 0 想象成一个由“小”或“普通”类型组成的宇宙。
Type 1 则是一个更大的类型宇宙，它包含 Type 0
作为一个元素，而 Type 2 是一个更大的类型宇宙，
它包含 Type 1 作为一个元素。这个列表是无限的：
对于每个自然数 n 都有一个 Type n。Type 是
Type 0 的缩写：
下表可能有助于具体化所讨论的关系。 沿 x 轴的移动代表宇宙的变化，而沿 y 轴的移动 代表有时被称为“度”的变化。
sort |
|
|
|
| ... |
|---|---|---|---|---|---|
type |
|
| ... | ||
term |
|
| ... |
然而，有些操作需要在类型宇宙上具有 多态性。例如，List α 应该对任何类型
α 都有意义，无论 α 存在于哪个类型宇宙中。这解释了
函数 List 的类型签名：
这里 u 是一个遍历类型级别的变量。
#check 命令的输出意味着只要 α 具有类型 Type u，
List α 也具有类型 Type u。函数 Prod 具有
类似的多态性：
为了定义多态常量，Lean 允许你
使用 universe 命令显式声明宇宙变量：
你可以通过在定义 F 时提供宇宙参数来避免使用 universe 命令：
2.3. 函数抽象和求值
Lean 提供了一个 fun（或 λ）关键字，用于从表达式创建函数，如下所示：
在这个例子中，类型 Nat 可以被推断出来：
你可以通过传递所需的参数来计算 lambda 函数：
从另一个表达式创建函数的过程称为
lambda 抽象。假设你有变量 x : α 并且你可以
构造一个表达式 t : β，那么表达式 fun (x : α) => t，
或者等价地，λ (x : α) => t，是一个类型为 α → β 的对象。可以把
这看作是从 α 到 β 的函数，它将
任何值 x 映射到值 t。
这里还有一些例子
#check fun x : Nat => fun y : Bool => if not y then x + 1 else x + 2#check fun (x : Nat) (y : Bool) => if not y then x + 1 else x + 2#check fun x y => if not y then x + 1 else x + 2
Lean 将最后三个例子解释为相同的表达式；在
最后一个表达式中，Lean 从表达式 if not y then x + 1 else x + 2
推断出 x 和 y 的类型。
一些数学上常见的函数运算示例可以用 lambda 抽象来描述：
def f (n : Nat) : String := toString n
def g (s : String) : Bool := s.length > 0
#check fun x : Nat => x#check fun x : Nat => true#check fun x : Nat => g (f x)#check fun x => g (f x)
思考一下这些表达式的含义。表达式
fun x : Nat => x 表示 Nat 上的恒等函数，
表达式 fun x : Nat => true 表示总是返回 true 的常数函数，
而 fun x : Nat => g (f x) 表示 f 和 g 的复合。
通常，你可以省略类型注释，让 Lean 为你推断。因此，例如，你
可以写 fun x => g (f x) 而不是 fun x : Nat => g (f x)。
你可以将函数作为参数传递，通过给它们命名 f
和 g，你可以在实现中使用这些函数：
你也可以将类型作为参数传递：
例如，最后一个表达式表示一个函数，它接受
三个类型 α、β 和 γ，以及两个函数 g : β → γ
和 f : α → β，并返回 g 和 f 的复合。
（要理解这个函数的类型，需要理解 依值积，下面将对此进行解释。）
lambda 表达式的一般形式是 fun (x : α) => t，其中
变量 x 是一个“绑定变量”：它实际上是一个占位符，
其“作用域”不会超出表达式 t。例如，
表达式 fun (b : β) (x : α) => b 中的变量 b
与前面声明的常量 b 没有任何关系。事实上，
该表达式表示的函数与 fun (u : β) (z : α) => u 相同。
形式上，除了绑定变量的重命名之外都相同的表达式被称为 alpha 等价，并且被认为是“相同的”。Lean 识别这种等价性。
注意，将项 t : α → β 应用于项 s : α 会产生
表达式 t s : β。回到前面的例子，
为了清晰起见重命名绑定变量，请注意以下表达式的类型：
#check (fun x : Nat => x) 1#check (fun x : Nat => true) 1
def f (n : Nat) : String := toString n
def g (s : String) : Bool := s.length > 0
#check
(fun (α β γ : Type) (u : β → γ) (v : α → β) (x : α) => u (v x)) Nat String Bool g f 0
正如预期的那样，表达式 (fun x : Nat => x) 1 具有类型 Nat。
事实上，更进一步：将表达式 (fun x : Nat => x) 应用于
1 应该“返回”值 1。确实如此：
稍后你将看到这些项是如何求值的。现在，请注意 这是依值类型论的一个重要特征：每个项都有 计算行为，并支持 规范化 的概念。原则上， 归约为相同值的两个项被称为 定义相等。它们被 Lean 的类型检查器认为是“相同的”， 并且 Lean 尽最大努力识别和支持这些标识。
Lean 是一门完整的编程语言。它有一个编译器，可以
生成二进制可执行文件和一个交互式解释器。你可以
使用命令 #eval 来执行表达式，这是
测试函数的首选方法。
2.4. 定义
回想一下，def 关键字提供了声明新命名对象的一种重要方式。
如果你知道函数在其他编程语言中是如何工作的，这看起来可能会更熟悉。
名称 double 被定义为一个函数，它接受一个类型为 Nat 的输入参数 x，
调用的结果是 x + x，所以它返回类型 Nat。
然后你可以使用以下方式调用此函数：
在这种情况下，你可以将 def 视为一种命名的 fun。
以下产生相同的结果：
当 Lean 有足够的信息来推断类型时，你可以省略类型声明。 类型推断是 Lean 的重要组成部分：
def double :=
fun (x : Nat) => x + x
定义的一般形式是 def foo : α := bar，其中
α 是表达式 bar 返回的类型。Lean 通常可以
推断类型 α，但显式写出它通常是一个好主意。
这阐明了你的意图，如果定义的右侧没有匹配的类型，Lean 将标记错误。
右侧 bar 可以是任何表达式，不仅仅是 lambda。
所以 def 也可以用来简单地命名一个值，如下所示：
def pi := 3.141592654
def 可以接受多个输入参数。让我们创建一个
将两个自然数相加的函数：
参数列表可以像这样分开：
注意这里我们调用了 double 函数来创建 add 的第一个参数。
你可以在 def 中使用其他更有趣的表达式：
你大概能猜到这个函数会做什么。
你也可以定义一个接受另一个函数作为输入的函数。 下面的代码调用给定的函数两次，将第一次调用的输出传递给第二次：
现在稍微抽象一点，你也可以指定像类型参数一样的参数：
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
这意味着 compose 是一个接受任意两个函数作为输入参数的函数，
只要这些函数每个只接受一个输入。
类型代数 β → γ 和 α → β 意味着要求
第二个函数的输出类型必须与第一个函数的输入类型匹配，否则
这两个函数将无法组合。
compose 还接受一个类型为 α 的第 3 个参数，
它使用该参数来调用第二个函数（局部命名为 f），并将
该函数的结果（类型为 β）作为输入传递给
第一个函数（局部命名为 g）。第一个函数返回类型
γ，所以这也是 compose 函数的返回类型。
compose 也非常通用，因为它适用于任何类型
α β γ。这意味着 compose 几乎可以组合任何 2 个函数，
只要它们每个都接受一个参数，并且只要第二个函数的输出类型与第一个函数的输入类型匹配。例如：
2.5. 局部定义
Lean 还允许你使用 let 关键字引入“局部”定义。
表达式 let a := t1; t2 在定义上等于
将 t2 中出现的每个 a 替换为 t1 的结果。
#check let y := 2 + 2; y * y#eval let y := 2 + 2; y * y
def twice_double (x : Nat) : Nat :=
let y := x + x; y * y
#eval twice_double 2
这里，twice_double x 在定义上等于项 (x + x) * (x + x)。
你可以通过链接 let 语句来组合多个赋值：
当使用换行符时，可以省略 ;。
注意，表达式 let a := t1; t2 的含义与 (fun a => t2) t1 的含义非常相似，但两者并不相同。
在第一个表达式中，你应该将 t2 中出现的每个 a 视为 t1 的语法缩写。
在第二个表达式中，a 是一个变量，表达式 fun a => t2 必须独立于 a 的值而有意义。
let 构造是一种更强的缩写手段，有些形式为 let a := t1; t2 的表达式不能表示为 (fun a => t2) t1。
作为一个练习，试着理解为什么下面 foo 的定义可以通过类型检查，而 bar 的定义却不能。
def foo := let a := Nat; fun x : a => x + 2
/-
def bar := (fun a => fun x : a => x + 2) Nat
-/
2.6. 变量和小节
考虑下面这三个函数定义：
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
def doTwice (α : Type) (h : α → α) (x : α) : α :=
h (h x)
def doThrice (α : Type) (h : α → α) (x : α) : α :=
h (h (h x))
Lean 提供 variable 指令来让这些声明变得紧凑：
variable (α β γ : Type)
def compose (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
def doTwice (h : α → α) (x : α) : α :=
h (h x)
def doThrice (h : α → α) (x : α) : α :=
h (h (h x))
你可以声明任意类型的变量，不只是 Type 类型：
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)
def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))
#print compose#print doTwice#print doThrice输出结果表明所有三组定义具有完全相同的效果。
variable 命令指示 Lean 将声明的变量作为绑定变量插入定义中，这些定义通过名称引用它们。
Lean 足够聪明，它能找出定义中显式或隐式使用哪些变量。
因此在写定义时，你可以将 α、β、γ、g、f、h 和 x 视为固定的对象，
并让 Lean 自动抽象这些定义。
当以这种方式声明时，变量将一直保持存在，直到所处理的文件结束。
然而，有时需要限制变量的作用范围。Lean 提供了小节标记 section 来实现这个目的：
section useful
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)
def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))
end useful
当一个小节结束后，变量不再发挥作用。
你不需要缩进一个小节中的行。你也不需要命名一个小节，也就是说，你可以使用一个匿名的
section / end 对。但是，如果你确实命名了一个小节，你必须使用相同的名字关闭它。
小节也可以嵌套，这允许你逐步增加声明新变量。
2.7. 命名空间
Lean 可以让你把定义放进一个嵌套的、层次化的 命名空间（namespaces）里：
namespace Foo
def a : Nat := 5
def f (x : Nat) : Nat := x + 7
def fa : Nat := f a
def ffa : Nat := f (f a)
#check a #check f #check fa #check ffa #check Foo.faend Foo
-- #check a -- error
-- #check f -- error
#check Foo.a#check Foo.f#check Foo.fa#check Foo.ffa
open Foo
#check a#check f#check fa#check Foo.fa
当你声明你在命名空间 Foo 中工作时，你声明的每个标识符都有一个前缀 “Foo.” 的全名。
在命名空间中，可以通过较短的名称引用标识符，但是关闭命名空间后，必须使用较长的名称。
与 section 不同，命名空间需要一个名称。只有一个匿名命名空间在根级别上。
open 命令使你可以在当前使用较短的名称。通常，当你导入一个模块时，
你会想打开它包含的一个或多个命名空间，以访问短标识符。
但是，有时你希望将这些信息保留在一个完全限定的名称中，例如，当它们与你想要使用的另一个命名空间中的标识符冲突时。
因此，命名空间为你提供了一种在工作环境中管理名称的方法。
例如，Lean 把和列表相关的定义和定理都放在了命名空间 List 之中。
像小节一样，命名空间也是可以嵌套的：
namespace Foo
def a : Nat := 5
def f (x : Nat) : Nat := x + 7
def fa : Nat := f a
namespace Bar
def ffa : Nat := f (f a)
#check fa #check ffa end Bar
#check fa #check Bar.ffaend Foo
#check Foo.fa#check Foo.Bar.ffa
open Foo
#check fa#check Bar.ffa关闭的命名空间可以之后重新打开，甚至是在另一个文件里：
namespace Foo
def a : Nat := 5
def f (x : Nat) : Nat := x + 7
def fa : Nat := f a
end Foo
#check Foo.a#check Foo.f
namespace Foo
def ffa : Nat := f (f a)
end Foo
与小节一样，嵌套的名称空间必须按照打开的顺序关闭。命名空间和小节有不同的用途：
命名空间组织数据，小节声明变量，以便在定义中插入。
小节对于分隔 set_option 和 open 等命令的范围也很有用。
然而，在许多方面，namespace ... end 结构块和 section ... end 表现出来的特征是一样的。
尤其是你在命名空间中使用 variable 命令时，它的作用范围被限制在命名空间里。
类似地，如果你在命名空间中使用 open 命令，它的效果在命名空间关闭后消失。
2.8. 依值类型论“依赖”着什么？
def cons (α : Type) (a : α) (as : List α) : List α :=
List.cons a as
#check cons Nat#check cons Bool#check cons
回到列表的例子，你可以使用命令 #check 来
检查下列 List 函数的类型。@ 符号
以及圆括号和花括号之间的区别将在稍后解释。
universe u v
def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
⟨a, b⟩
def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a :=
Sigma.mk a b
def h1 (x : Nat) : Nat :=
(f Type (fun α => α) Nat x).2
#eval h1 5
def h2 (x : Nat) : Nat :=
(g Type (fun α => α) Nat x).2
#eval h2 5
上面的函数 f 和 g 表示相同的函数。
2.9. 隐参数
假设我们有一个列表的实现如下：
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst#check Lst.cons#check Lst.nil#check Lst.append
然后，你可以建立一个 Nat 列表如下：
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst.cons Nat 0 (Lst.nil Nat)
def as : Lst Nat := Lst.nil Nat
def bs : Lst Nat := Lst.cons Nat 5 (Lst.nil Nat)
#check Lst.append Nat as bs
这是依值类型论的一个主要特征：项包含大量
信息，而且通常可以从上下文推断出一些信息。
在 Lean 中，我们使用下划线 _ 来指定
系统应该自动填写信息。这就是所谓的“隐参数”。
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst
#check Lst.cons
#check Lst.nil
#check Lst.append
#check Lst.cons _ 0 (Lst.nil _)
def as : Lst Nat := Lst.nil _
def bs : Lst Nat := Lst.cons _ 5 (Lst.nil _)
#check Lst.append _ as bs然而，敲这么多下划线仍然很繁琐。当一个 函数接受一个通常可以从上下文推断出来的参数时， Lean 允许你指定该参数在默认情况下应该保持隐式。 这是通过将参数放入花括号来实现的，如下所示：
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons {α : Type u} (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil {α : Type u} : Lst α := List.nil
def Lst.append {α : Type u} (as bs : Lst α) : Lst α := List.append as bs
#check Lst.cons 0 Lst.nil
def as : Lst Nat := Lst.nil
def bs : Lst Nat := Lst.cons 5 Lst.nil
#check Lst.append as bs
唯一改变的是变量声明中 α : Type u 周围的花括号。我们也可以在函数
定义中使用这个技巧：
检查 ident 的类型需要将其用括号括起来，以避免显示其签名：
universe u
def ident {α : Type u} (x : α) := x
#check (ident)#check ident 1#check ident "hello"#check @ident
这使得 ident 的第一个参数是隐式的。从符号上讲，
这隐藏了类型的说明，使它看起来好像
ident 只是接受任何类型的参数。事实上，函数
id 在标准库中就是以这种方式定义的。我们在这里
选择一个非传统的名字只是为了避免名字的冲突。
variable 命令也可以用这种技巧来来把变量变成隐式的：
universe u
section
variable {α : Type u}
variable (x : α)
def ident := x
end
#check ident#check ident 4#check ident "hello"
此处定义的 ident 和上面那个效果是一样的。
Lean 有非常复杂的机制来实例化隐参数，
我们将看到它们可以用来推断函数类型、
谓词，甚至证明。实例化这些
“洞”或“占位符”的过程通常被称为
繁饰（Elaboration）。隐参数的存在意味着有时
可能没有足够的信息来精确地确定表达式的含义。
像 id 或 List.nil 这样的表达式被认为是 多态的，
因为它可以在不同的上下文中具有不同的含义。
Lean 中数字是重载的，但是当数字的类型不能
被推断时，Lean 默认假设它是一个自然数。因此，
下面的前两个 #check 命令中的表达式以同样的方式进行了
繁饰，而第三个 #check 命令
将 2 解释为整数。
注意，现在第一个 #check 命令给出了
标识符 id 的类型，没有插入任何占位符。而且，
输出表明第一个参数是隐式的。