From 4dce82c8ce85857d94d174c9cd51f9ae11d78830 Mon Sep 17 00:00:00 2001 From: Oling Cat Date: Sun, 23 Jun 2024 03:41:47 +0800 Subject: [PATCH] format spaces --- axioms_and_computation.md | 32 +++--- custom.js | 4 +- dependent_type_theory.md | 46 ++++---- induction_and_recursion.md | 54 +++++----- inductive_types.md | 210 ++++++++++++++++++------------------ interacting_with_lean.md | 52 ++++----- introduction.md | 75 ++++++++++--- propositions_and_proofs.md | 46 ++++---- quantifiers_and_equality.md | 18 ++-- structures_and_records.md | 38 +++---- tactics.md | 27 ++--- title_page.md | 2 +- type_classes.md | 28 ++--- 13 files changed, 341 insertions(+), 291 deletions(-) diff --git a/axioms_and_computation.md b/axioms_and_computation.md index 466d6ef..34d9028 100644 --- a/axioms_and_computation.md +++ b/axioms_and_computation.md @@ -59,8 +59,8 @@ computation. This also blocks evaluation in the kernel, but it is compatible with compilation to bytecode. --> -Lean 的标准库定义了一个公理：**命题外延性（Propositional Extensionality）**。 -以及一个**商（Qoutient）**结构，它蕴含了函数外延性的公理。 +Lean 的标准库定义了一个公理： **命题外延性（Propositional Extensionality）** 。 +以及一个 **商（Qoutient）** 结构，它蕴含了函数外延性的公理。 这些扩展被用来发展如集合与有限集这些理论。我们在后面会看到， 这些定理的使用会阻碍 Lean 内核中的求值，因此 ``Nat`` 类型的封闭项不再求值为数值。 但是 Lean 在对其虚拟机器求值器进行字节码编译时会擦除类型和命题信息， @@ -163,7 +163,7 @@ computational reading. 然而在 19 世纪，数学论证复杂性的提升推动了数学家发展新的推理风格， 抑制算法信息并调用数学对象，从而抽象掉了对象被表征的细节。 目标是在不陷入繁重的计算细节的情况下获得强大的「概念」理解， -但这可能导致数学定理在直接计算的解读上干脆就是 **错误** 的。 +但这可能导致数学定理在直接计算的解读上干脆就是 **错误** 的。 在通过了证明无关的 ``Prop`` 之后，可以认为使用排中律 ``p ∨ ¬p`` 是合法的， -其中 ``p``是任何命题。当然，这也可能根据 CIC 的规则阻止计算， +其中 ``p`` 是任何命题。当然，这也可能根据 CIC 的规则阻止计算， 但它不会阻止字节码求值，如上所述。仅在 :numref:`choice` 中讨论过的选择原则才能完全消除理论中与证明无关的部分和与数据相关部分之间的区别。 @@ -516,8 +516,8 @@ quotients, and more. But the solutions are not so clear cut, and the rules of Lean's underlying calculus do not sanction such reductions. --> -当前的研究计划包括关于**观测类型论（Observational Type Theory）** -和**立方类型论（Cubical Type Theory）**的研究，旨在扩展类型理论， +当前的研究计划包括关于 **观测类型论（Observational Type Theory）** +和 **立方类型论（Cubical Type Theory）** 的研究，旨在扩展类型理论， 以便允许对涉及函数外延、商，等等的强制转换进行归约。 但解决方案并不明朗，而 Lean 的底层演算法则对此类归约也不支持。 @@ -678,7 +678,7 @@ They are, like inductively defined types and the associated constructors and recursors, viewed as part of the logical framework. --> -和归纳定义的类型以及相关的构造器和递归器一样，它们也被视为逻辑框架的一部分。 +和归纳定义的类型以及相关的构造子和递归器一样，它们也被视为逻辑框架的一部分。 -为支持这种通用使用案例，标准库定义了 **广集（Setoid）** 的概念， +为支持这种通用使用案例，标准库定义了 **广集（Setoid）** 的概念， 它只是一个带有与之关联的等价关系的类型： ```lean @@ -818,7 +818,7 @@ the quotient correspond exactly to the equivalence classes of elements in ``α``. --> -结合``Quotient.sound``，这意味着商的各个元素精确对应于 ``α``中各元素的等价类。 +结合 ``Quotient.sound``，这意味着商的各个元素精确对应于 ``α`` 中各元素的等价类。 回顾一下标准库中的 ``α × β`` 代表类型 ``α`` 和 ``β`` 的笛卡尔积。 -为了说明商的用法，让我们将类型为 ``α`` 的元素构成的**无序对（Unordered Pair）**的类型定义为 +为了说明商的用法，让我们将类型为 ``α`` 的元素构成的 **无序对（Unordered Pair）** 的类型定义为 ``α × α`` 类型的商。首先，我们定义相关的等价关系： ```lean @@ -1178,7 +1178,7 @@ subtypes as follows: --> 这可以在 ``Classical`` 命名空间中找到，所以定理的全名是 ``Classical.choice``。 -选择公理等价于**非限定摹状词（Indefinite Description）**原理，可通过子类型表示如下： +选择公理等价于 **非限定摹状词（Indefinite Description）** 原理，可通过子类型表示如下： ```lean # namespace Hidden @@ -1254,7 +1254,7 @@ definition is conventionally known as *Hilbert's epsilon function*: --> 假设环境类型 ``α`` 非空，``strongIndefiniteDescription p`` 产生一个满足 ``p`` -的元素 ``α``（如果存在的话）。该定义的数据部分通常被称为 **希尔伯特 ε 函数**： +的元素 ``α``（如果存在的话）。该定义的数据部分通常被称为 **希尔伯特 ε 函数** ： ```lean # open Classical @@ -1304,7 +1304,7 @@ sketch the proof that is found in the standard library. First, we import the necessary axioms, and define two predicates ``U`` and ``V``: --> -首先，我们导入必要的公理，并定义两个谓词``U``和``V``： +首先，我们导入必要的公理，并定义两个谓词 ``U`` 和 ``V``： ```lean # namespace Hidden diff --git a/custom.js b/custom.js index 2c800e7..80f4100 100644 --- a/custom.js +++ b/custom.js @@ -1,5 +1,5 @@ -const newline = /(?<=[，。、：；」）])\n(?!\n)/g; -const space = /\s+(<.+?>\p{Script=Han}.+?<\/.+?>)\s+/g +const newline = /(?<=[，。、：；」）])\n(?!\n)/gu; +const space = /\s*(<.+?>\p{Script=Han}.+?<\/.+?>)\s*/gu; const paras = document.querySelectorAll("#content > main > p"); for (const p of paras) { p.innerHTML = p.innerHTML.replace(newline, ""); diff --git a/dependent_type_theory.md b/dependent_type_theory.md index 16b411e..5e9b9cc 100644 --- a/dependent_type_theory.md +++ b/dependent_type_theory.md @@ -15,7 +15,7 @@ hierarchy of non-cumulative universes and inductive types. By the end of this chapter, you will understand much of what this means. --> -依值类型论（Dependent type theory）是一种强大而富有表达力的语言，允许你表达复杂的数学断言，编写复杂的硬件和软件规范，并以自然和统一的方式对这两者进行推理。Lean是基于一个被称为构造演算（Calculus of Constructions）的依值类型论的版本，它拥有一个可数的非累积性宇宙（non-cumulative universe）的层次结构以及归纳类型（Inductive type）。在本章结束时，你将学会一大部分。 +依值类型论（Dependent type theory）是一种强大而富有表达力的语言，允许你表达复杂的数学断言，编写复杂的硬件和软件规范，并以自然和统一的方式对这两者进行推理。Lean 是基于一个被称为构造演算（Calculus of Constructions）的依值类型论的版本，它拥有一个可数的非累积性宇宙（non-cumulative universe）的层次结构以及归纳类型（Inductive type）。在本章结束时，你将学会一大部分。 -「类型论」得名于其中每个表达式都有一个*类型*。举例：在一个给定的语境中，``x + 0`` 可能表示一个自然数，``f`` 可能表示一个定义在自然数上的函数。Lean中的自然数是任意精度的无符号整数。 +「类型论」得名于其中每个表达式都有一个*类型*。举例：在一个给定的语境中，``x + 0`` 可能表示一个自然数，``f`` 可能表示一个定义在自然数上的函数。Lean 中的自然数是任意精度的无符号整数。 -Lean所依据的依值类型论对简单类型论的其中一项升级是，类型本身（如 ``Nat`` 和 ``Bool`` 这些东西）也是对象，因此也具有类型。 +Lean 所依据的依值类型论对简单类型论的其中一项升级是，类型本身（如 ``Nat`` 和 ``Bool`` 这些东西）也是对象，因此也具有类型。 ```lean #check Nat -- Type @@ -347,7 +347,7 @@ Lean's typing system. Lean's underlying foundation has an infinite hierarchy of types: --> -实际上，这是 Lean 系统的一个最微妙的方面：Lean的底层基础有无限的类型层次： +实际上，这是 Lean 系统的一个最微妙的方面：Lean 的底层基础有无限的类型层次： ```lean #check Type -- Type 1 @@ -396,7 +396,7 @@ universes. For example, ``List α`` should make sense for any type type signature of the function ``List``: --> -然而，有些操作需要在类型宇宙上具有**多态**（polymorphic）。例如，``List α`` 应该对任何类型的 ``α`` 都有意义，无论 ``α`` 存在于哪种类型的宇宙中。所以函数 ``List`` 有如下的类型： +然而，有些操作需要在类型宇宙上具有 **多态（Polymorphic）** 。例如，``List α`` 应该对任何类型的 ``α`` 都有意义，无论 ``α`` 存在于哪种类型的宇宙中。所以函数 ``List`` 有如下的类型： ```lean #check List -- List.{u} (α : Type u) : Type u @@ -449,7 +449,7 @@ def F.{u} (α : Type u) : Type u := Prod α α ## 函数抽象和求值 -Lean提供 `fun` (或 `λ`)关键字用于从给定表达式创建函数，如下所示： +Lean 提供 `fun` (或 `λ`)关键字用于从给定表达式创建函数，如下所示： -从另一个表达式创建函数的过程称为**lambda 抽象**。假设你有一个变量 ``x : α`` 和一个表达式 ``t : β``，那么表达式 ``fun (x : α) => t`` 或者 ``λ (x : α) => t`` 是一个类型为 ``α → β`` 的对象。这个从 ``α`` 到 ``β`` 的函数把任意 ``x`` 映射到 ``t``。 +从另一个表达式创建函数的过程称为 **lambda 抽象** 。假设你有一个变量 ``x : α`` 和一个表达式 ``t : β``，那么表达式 ``fun (x : α) => t`` 或者 ``λ (x : α) => t`` 是一个类型为 ``α → β`` 的对象。这个从 ``α`` 到 ``β`` 的函数把任意 ``x`` 映射到 ``t``。 这有些例子： @@ -507,7 +507,7 @@ Some mathematically common examples of operations of functions can be described in terms of lambda abstraction: --> -Lean将这三个例子解释为相同的表达式；在最后一个表达式中，Lean可以从表达式`if not y then x + 1 else x + 2`推断 ``x`` 和 ``y`` 的类型。 +Lean 将这三个例子解释为相同的表达式；在最后一个表达式中，Lean 可以从表达式`if not y then x + 1 else x + 2`推断 ``x`` 和 ``y`` 的类型。 一些数学上常见的函数运算的例子可以用 lambda 抽象的项来描述: @@ -578,7 +578,7 @@ following expressions: 这个表达式表示一个接受三个类型 ``α``，``β`` 和 ``γ`` 和两个函数 ``g : β → γ`` 和 ``f : α → β``，并返回的 ``g`` 和 ``f`` 的复合的函数。(理解这个函数的类型需要理解依值积类型，下面将对此进行解释。) -lambda表达式的一般形式是 ``fun x : α => t``，其中变量 ``x`` 是一个**绑定变量**（bound variable）：它实际上是一个占位符，其「作用域」没有扩展到表达式 ``t`` 之外。例如，表达式 ``fun (b : β) (x : α) => b`` 中的变量 ``b`` 与前面声明的常量 ``b`` 没有任何关系。事实上，这个表达式表示的函数与 ``fun (u : β) (z : α) => u`` 是一样的。形式上，可以通过给绑定变量重命名来使形式相同的表达式被看作是**alpha等价**的，也就是被认为是「一样的」。Lean认识这种等价性。 +lambda表达式的一般形式是 ``fun x : α => t``，其中变量 ``x`` 是一个 **绑定变量（Bound Variable）** ：它实际上是一个占位符，其「作用域」没有扩展到表达式 ``t`` 之外。例如，表达式 ``fun (b : β) (x : α) => b`` 中的变量 ``b`` 与前面声明的常量 ``b`` 没有任何关系。事实上，这个表达式表示的函数与 ``fun (u : β) (z : α) => u`` 是一样的。形式上，可以通过给绑定变量重命名来使形式相同的表达式被看作是 **alpha等价** 的，也就是被认为是「一样的」。Lean 认识这种等价性。 注意到项 ``t : α → β`` 应用到项 ``s : α`` 上导出了表达式 ``t s : β``。回到前面的例子，为清晰起见给绑定变量重命名，注意以下表达式的类型: @@ -624,7 +624,7 @@ preferred way of testing your functions. 稍后你将看到这些项是如何计算的。现在，请注意这是依值类型论的一个重要特征：每个项都有一个计算行为，并支持「标准化」的概念。从原则上讲，两个可以化约为相同形式的项被称为「定义等价」。它们被 Lean 的类型检查器认为是「相同的」，并且 Lean 尽其所能地识别和支持这些识别结果。 -Lean是个完备的编程语言。它有一个生成二进制可执行文件的编译器，和一个交互式解释器。你可以用`#eval`命令执行表达式，这也是测试你的函数的好办法。 +Lean 是个完备的编程语言。它有一个生成二进制可执行文件的编译器，和一个交互式解释器。你可以用`#eval`命令执行表达式，这也是测试你的函数的好办法。 -定义的一般形式是 ``def foo : α := bar``，其中 ``α`` 是表达式 ``bar`` 返回的类型。Lean通常可以推断类型 ``α``，但是精确写出它可以澄清你的意图，并且如果定义的右侧没有匹配你的类型，Lean将标记一个错误。 +定义的一般形式是 ``def foo : α := bar``，其中 ``α`` 是表达式 ``bar`` 返回的类型。Lean 通常可以推断类型 ``α``，但是精确写出它可以澄清你的意图，并且如果定义的右侧没有匹配你的类型，Lean 将标记一个错误。 `bar` 可以是任何一个表达式，不只是一个 lambda 表达式。因此 `def` 也可以用于给一些值命名，例如： @@ -857,7 +857,7 @@ definitionally equal to the result of replacing every occurrence of ``a`` in ``t2`` by ``t1``. --> -Lean还允许你使用 ``let`` 关键字来引入「局部定义」。表达式 ``let a := t1; t2`` 定义等价于把 ``t2`` 中所有的 ``a`` 替换成 ``t1`` 的结果。 +Lean 还允许你使用 ``let`` 关键字来引入「局部定义」。表达式 ``let a := t1; t2`` 定义等价于把 ``t2`` 中所有的 ``a`` 替换成 ``t1`` 的结果。 ```lean #check let y := 2 + 2; y * y -- Nat @@ -947,7 +947,7 @@ Lean provides you with the ``variable`` command to make such declarations look more compact: --> -Lean提供 ``variable`` 指令来让这些声明变得紧凑： +Lean 提供 ``variable`` 指令来让这些声明变得紧凑： ```lean variable (α β γ : Type) @@ -1002,9 +1002,9 @@ a ``section``: 输出结果表明所有三组定义具有完全相同的效果。 -``variable`` 命令指示 Lean 将声明的变量作为绑定变量插入定义中，这些定义通过名称引用它们。Lean足够聪明，它能找出定义中显式或隐式使用哪些变量。因此在写定义时，你可以将 ``α``、``β``、``γ``、``g``、``f``、``h`` 和 ``x`` 视为固定的对象，并让 Lean 自动抽象这些定义。 +``variable`` 命令指示 Lean 将声明的变量作为绑定变量插入定义中，这些定义通过名称引用它们。Lean 足够聪明，它能找出定义中显式或隐式使用哪些变量。因此在写定义时，你可以将 ``α``、``β``、``γ``、``g``、``f``、``h`` 和 ``x`` 视为固定的对象，并让 Lean 自动抽象这些定义。 -当以这种方式声明时，变量将一直保持存在，直到所处理的文件结束。然而，有时需要限制变量的作用范围。Lean提供了小节标记 ``section`` 来实现这个目的： +当以这种方式声明时，变量将一直保持存在，直到所处理的文件结束。然而，有时需要限制变量的作用范围。Lean 提供了小节标记 ``section`` 来实现这个目的： ```lean section useful @@ -1044,7 +1044,7 @@ Lean provides you with the ability to group definitions into nested, hierarchical *namespaces*: --> -Lean可以让你把定义放进一个「命名空间」（``namespace``）里，并且命名空间也是层次化的： +Lean 可以让你把定义放进一个「命名空间」（``namespace``）里，并且命名空间也是层次化的： ```lean namespace Foo @@ -1100,7 +1100,7 @@ a namespace ``List``. ``open`` 命令使你可以在当前使用较短的名称。通常，当你导入一个模块时，你会想打开它包含的一个或多个命名空间，以访问短标识符。但是，有时你希望将这些信息保留在一个完全限定的名称中，例如，当它们与你想要使用的另一个命名空间中的标识符冲突时。因此，命名空间为你提供了一种在工作环境中管理名称的方法。 -例如，Lean把和列表相关的定义和定理都放在了命名空间 ``List`` 之中。 +例如，Lean 把和列表相关的定义和定理都放在了命名空间 ``List`` 之中。 ```lean #check List.nil @@ -1268,7 +1268,7 @@ explained momentarily. 注意到 ``(a : α) → β`` 对于任意表达式 ``β : Type`` 都有意义。当 ``β`` 的值依赖于 ``a``（例如，在前一段的表达式 ``β a``），``(a : α) → β`` 表示一个依值函数类型。当 ``β`` 的值不依赖于 ``a``，``(a : α) → β`` 与类型 ``α → β`` 无异。实际上，在依值类型论（以及Lean）中，``α → β`` 表达的意思就是当 ``β`` 的值不依赖于 ``a`` 时的 ``(a : α) → β``。【注】 -> 译者注：在依值类型论的数学符号体系中，依值类型是用 ``Π`` 符号来表达的，在Lean 3中还使用这种表达，例如 ``Π x : α, β x``。Lean 4抛弃了这种不友好的写法。``(x : α) → β x`` 这种写法在引入「构造器」之后意义会更明朗一些（见下一个注释），对于来自数学背景的读者可以把它类比于 ``forall x : α, β x`` 这种写法（这也是合法的 Lean 语句），关于前一种符号在[量词与等价](./quantifiers_and_equality.md)一章中有更详细的说明。同时，依值类型有着更丰富的引入动机，推荐读者寻找一些拓展读物。 +> 译者注：在依值类型论的数学符号体系中，依值类型是用 ``Π`` 符号来表达的，在Lean 3中还使用这种表达，例如 ``Π x : α, β x``。Lean 4抛弃了这种不友好的写法。``(x : α) → β x`` 这种写法在引入「构造子」之后意义会更明朗一些（见下一个注释），对于来自数学背景的读者可以把它类比于 ``forall x : α, β x`` 这种写法（这也是合法的 Lean 语句），关于前一种符号在[量词与等价](./quantifiers_and_equality.md)一章中有更详细的说明。同时，依值类型有着更丰富的引入动机，推荐读者寻找一些拓展读物。 回到列表的例子，你可以使用`#check`命令来检查下列的 `List` 函数。``@`` 符号以及圆括号和花括号之间的区别将在后面解释。 @@ -1385,9 +1385,9 @@ that the system should fill in the information automatically. This is known as an "implicit argument." --> -由于构造器对类型是多态的【注】，我们需要重复插入类型 ``Nat`` 作为一个参数。但是这个信息是多余的：我们可以推断表达式 ``Lst.cons Nat 5 (Lst.nil Nat)`` 中参数 ``α`` 的类型，这是通过第二个参数 ``5`` 的类型是 ``Nat`` 来实现的。类似地，我们可以推断 ``Lst.nil Nat`` 中参数的类型，这是通过它作为函数 ``Lst.cons`` 的一个参数，且这个函数在这个位置需要接收的是一个具有 ``Lst α`` 类型的参数来实现的。 +由于构造子对类型是多态的【注】，我们需要重复插入类型 ``Nat`` 作为一个参数。但是这个信息是多余的：我们可以推断表达式 ``Lst.cons Nat 5 (Lst.nil Nat)`` 中参数 ``α`` 的类型，这是通过第二个参数 ``5`` 的类型是 ``Nat`` 来实现的。类似地，我们可以推断 ``Lst.nil Nat`` 中参数的类型，这是通过它作为函数 ``Lst.cons`` 的一个参数，且这个函数在这个位置需要接收的是一个具有 ``Lst α`` 类型的参数来实现的。 -> 译者注：「构造器」（Constructor）的概念前文未加解释，对类型论不熟悉的读者可能会困惑。它指的是一种「依值类型的类型」，也可以看作「类型的构造器」，例如 ``λ α : α -> α`` 甚至可看成 ``⋆ -> ⋆``。当给 ``α`` 或者 ``⋆`` 赋予一个具体的类型时，这个表达式就成为了一个类型。前文中 ``(x : α) → β x`` 中的 ``β`` 就可以看成一个构造器，``(x : α)`` 就是传进的类型参数。原句「构造器对类型是多态的」意为给构造器中放入不同类型时它会变成不同类型。 +> 译者注：「构造子」（Constructor）的概念前文未加解释，对类型论不熟悉的读者可能会困惑。它指的是一种「依值类型的类型」，也可以看作「类型的构造子」，例如 ``λ α : α -> α`` 甚至可看成 ``⋆ -> ⋆``。当给 ``α`` 或者 ``⋆`` 赋予一个具体的类型时，这个表达式就成为了一个类型。前文中 ``(x : α) → β x`` 中的 ``β`` 就可以看成一个构造子，``(x : α)`` 就是传进的类型参数。原句「构造子对类型是多态的」意为给构造子中放入不同类型时它会变成不同类型。 这是依值类型论的一个主要特征：项包含大量信息，而且通常可以从上下文推断出一些信息。在 Lean 中，我们使用下划线 ``_`` 来指定系统应该自动填写信息。这就是所谓的「隐参数」。 @@ -1417,7 +1417,7 @@ default, be left implicit. This is done by putting the arguments in curly braces, as follows: --> -然而，敲这么多下划线仍然很无聊。当一个函数接受一个通常可以从上下文推断出来的参数时，Lean允许你指定该参数在默认情况下应该保持隐式。这是通过将参数放入花括号来实现的，如下所示: +然而，敲这么多下划线仍然很无聊。当一个函数接受一个通常可以从上下文推断出来的参数时，Lean 允许你指定该参数在默认情况下应该保持隐式。这是通过将参数放入花括号来实现的，如下所示: ```lean universe u @@ -1506,7 +1506,7 @@ used to specify the desired types of the expressions ``id`` and 此处定义的 ``ident`` 和上面那个效果是一样的。 -Lean有非常复杂的机制来实例化隐参数，我们将看到它们可以用来推断函数类型、谓词，甚至证明。实例化这些「洞」或「占位符」的过程通常被称为**繁饰**（Elaboration）。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像 ``id`` 或 ``List.nil`` 这样的表达式被认为是「多态的」，因为它可以在不同的上下文中具有不同的含义。 +Lean 有非常复杂的机制来实例化隐参数，我们将看到它们可以用来推断函数类型、谓词，甚至证明。实例化这些「洞」或「占位符」的过程通常被称为 **繁饰（Elaboration）** 。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像 ``id`` 或 ``List.nil`` 这样的表达式被认为是「多态的」，因为它可以在不同的上下文中具有不同的含义。 可以通过写 ``(e : T)`` 来指定表达式 ``e`` 的类型 ``T``。这就指导 Lean 的繁饰器在试图解决隐式参数时使用值 ``T`` 作为 ``e`` 的类型。在下面的第二个例子中，这种机制用于指定表达式 ``id`` 和 ``List.nil`` 所需的类型: @@ -1526,7 +1526,7 @@ elaborated in the same way, whereas the third ``#check`` command interprets ``2`` as an integer. --> -Lean中数字是重载的，但是当数字的类型不能被推断时，Lean默认假设它是一个自然数。因此，下面的前两个 ``#check`` 命令中的表达式以同样的方式进行了繁饰，而第三个 ``#check`` 命令将 ``2`` 解释为整数。 +Lean 中数字是重载的，但是当数字的类型不能被推断时，Lean 默认假设它是一个自然数。因此，下面的前两个 ``#check`` 命令中的表达式以同样的方式进行了繁饰，而第三个 ``#check`` 命令将 ``2`` 解释为整数。 ```lean #check 2 -- Nat diff --git a/induction_and_recursion.md b/induction_and_recursion.md index d657208..a05cbcc 100644 --- a/induction_and_recursion.md +++ b/induction_and_recursion.md @@ -24,7 +24,7 @@ of the trusted code base; its output consists of terms that are checked independently by the kernel. --> -在上一章中，我们看到归纳定义提供了在 Lean 中引入新类型的强大手段。此外，构造器和递归器提供了在这些类型上定义函数的唯一手段。命题即类型的对应关系，意味着归纳法是证明的基本方法。 +在上一章中，我们看到归纳定义提供了在 Lean 中引入新类型的强大手段。此外，构造子和递归器提供了在这些类型上定义函数的唯一手段。命题即类型的对应关系，意味着归纳法是证明的基本方法。 Lean 提供了定义递归函数、执行模式匹配和编写归纳证明的自然方法。它允许你通过指定它应该满足的方程来定义一个函数，它允许你通过指定如何处理可能出现的各种情况来证明一个定理。在它内部，这些描述被「方程编译器」程序「编译」成原始递归器。方程编译器不是可信代码库的一部分；它的输出包括由内核独立检查的项。 @@ -52,7 +52,7 @@ a function from the natural numbers to an arbitrary type by specifying a value in each of those cases: --> -对示意图模式的解释是编译过程的第一步。我们已经看到，`casesOn` 递归器可以通过分情况讨论来定义函数和证明定理，根据归纳定义类型所涉及的构造器。但是复杂的定义可能会使用几个嵌套的 ``casesOn`` 应用，而且可能很难阅读和理解。模式匹配提供了一种更方便的方法，并且为函数式编程语言的用户所熟悉。 +对示意图模式的解释是编译过程的第一步。我们已经看到，`casesOn` 递归器可以通过分情况讨论来定义函数和证明定理，根据归纳定义类型所涉及的构造子。但是复杂的定义可能会使用几个嵌套的 ``casesOn`` 应用，而且可能很难阅读和理解。模式匹配提供了一种更方便的方法，并且为函数式编程语言的用户所熟悉。 考虑一下自然数的归纳定义类型。每个自然数要么是 ``zero``，要么是 ``succ x``，因此你可以通过在每个情况下指定一个值来定义一个从自然数到任意类型的函数： @@ -117,7 +117,7 @@ and ``succ`` are exposed. Pattern matching works with any inductive type, such as products and option types: --> -因为加法和零符号已经被赋予 `[matchPattern]` 属性，它们可以被用于模式匹配。Lean 简单地将这些表达式规范化，直到显示构造器 ``zero`` 和 ``succ``。 +因为加法和零符号已经被赋予 `[matchPattern]` 属性，它们可以被用于模式匹配。Lean 简单地将这些表达式规范化，直到显示构造子 ``zero`` 和 ``succ``。 模式匹配适用于任何归纳类型，如乘积和 Option 类型： @@ -177,7 +177,7 @@ constructors, as in the following examples. 这样解决带逻辑连接词的命题就很紧凑。 -在所有这些例子中，模式匹配被用来进行单一情况的区分。更有趣的是，模式可以涉及嵌套的构造器，如下面的例子。 +在所有这些例子中，模式匹配被用来进行单一情况的区分。更有趣的是，模式可以涉及嵌套的构造子，如下面的例子。 ```lean def sub2 : Nat → Nat @@ -322,7 +322,7 @@ is a parameter and occurs before the colon to indicate it does not participate i Lean also allows parameters to occur after ``:``, but it cannot pattern match on them. --> -还要注意的是，当定义中不需要一个参数的值时，你可以用下划线来代替。这个下划线被称为**通配符模式**，或**匿名变量**。与方程编译器之外的用法不同，这里的下划线并**不**表示一个隐参数。使用下划线表示通配符在函数式编程语言中是很常见的，所以 Lean 采用了这种符号。[通配符和重叠模式](#通配符和重叠模式)一节阐述了通配符的概念，而[不可访问模式](#不可访问模式)一节解释了你如何在模式中使用隐参数。 +还要注意的是，当定义中不需要一个参数的值时，你可以用下划线来代替。这个下划线被称为 **通配符模式** ，或 **匿名变量** 。与方程编译器之外的用法不同，这里的下划线 **并不** 表示一个隐参数。使用下划线表示通配符在函数式编程语言中是很常见的，所以 Lean 采用了这种符号。[通配符和重叠模式](#通配符和重叠模式)一节阐述了通配符的概念，而[不可访问模式](#不可访问模式)一节解释了你如何在模式中使用隐参数。 正如[归纳类型](./inductive_types.md)一章中所描述的，归纳数据类型可以依赖于参数。下面的例子使用模式匹配定义了 ``tail`` 函数。参数 ``α : Type`` 是一个参数，出现在冒号之前，表示它不参与模式匹配。Lean 也允许参数出现在 ``:`` 之后，但它不能对其进行模式匹配。 @@ -350,7 +350,7 @@ considered in the [Section Dependent Pattern Matching](#dependent-pattern-matchi 尽管参数 ``α`` 在这两个例子中的位置不同，但在这两种情况下，它的处理方式是一样的，即它不参与情况分割。 -Lean也可以处理更复杂的模式匹配形式，其中从属类型的参数对各种情况构成了额外的约束。这种**依值模式匹配**的例子在[依值模式匹配](#依值模式匹配)一节中考虑。 +Lean 也可以处理更复杂的模式匹配形式，其中从属类型的参数对各种情况构成了额外的约束。这种 **依值模式匹配** 的例子在[依值模式匹配](#依值模式匹配)一节中考虑。 -在第二种表述中，模式是重叠的；例如，一对参数 ``0 0`` 符合所有三种情况。但是Lean通过使用第一个适用的方程来处理这种模糊性，所以在这个例子中，最终结果是一样的。特别是，以下方程在定义上是成立的： +在第二种表述中，模式是重叠的；例如，一对参数 ``0 0`` 符合所有三种情况。但是Lean 通过使用第一个适用的方程来处理这种模糊性，所以在这个例子中，最终结果是一样的。特别是，以下方程在定义上是成立的： ```lean # def foo : Nat → Nat → Nat @@ -411,7 +411,7 @@ example : foo (m+1) (n+1) = 2 := rfl Since the values of ``m`` and ``n`` are not needed, we can just as well use wildcard patterns instead. --> -由于不需要``m``和``n``的值，我们也可以用通配符模式代替。 +由于不需要 ``m`` 和 ``n`` 的值，我们也可以用通配符模式代替。 ```lean def foo : Nat → Nat → Nat @@ -444,7 +444,7 @@ both approaches. 你可以检查这个 ``foo`` 的定义是否满足与之前相同的定义特性。 -一些函数式编程语言支持**不完整的模式**。在这些语言中，解释器对不完整的情况产生一个异常或返回一个任意的值。我们可以使用 ``Inhabited`` （含元素的）类型类来模拟任意值的方法。粗略的说，``Inhabited α`` 的一个元素是对 ``α`` 拥有一个元素的见证；在[类型类](./type_classes.md)中，我们将看到 Lean 可以被告知合适的基础类型是含元素的，并且可以自动推断出其他构造类型是含元素的。在此基础上，标准库提供了一个任意元素``arbitrary``，任何含元素的类型。 +一些函数式编程语言支持 **不完整的模式** 。在这些语言中，解释器对不完整的情况产生一个异常或返回一个任意的值。我们可以使用 ``Inhabited`` （含元素的）类型类来模拟任意值的方法。粗略的说，``Inhabited α`` 的一个元素是对 ``α`` 拥有一个元素的见证；在[类型类](./type_classes.md)中，我们将看到 Lean 可以被告知合适的基础类型是含元素的，并且可以自动推断出其他构造类型是含元素的。在此基础上，标准库提供了一个任意元素 ``arbitrary``，任何含元素的类型。 我们还可以使用类型`Option α`来模拟不完整的模式。我们的想法是对所提供的模式返回`some a`，而对不完整的情况使用`none`。下面的例子演示了这两种方法。 @@ -593,9 +593,9 @@ recursion from the last chapter, now defined using the equation compiler: --> -这里 `(a : α)` 是一个参数序列，`(b : β)` 是进行模式匹配的参数序列，`γ` 是任何类型，它可以取决于 `a` 和 `b `。每一行应该包含相同数量的模式，对应于 `β` 的每个元素。正如我们所看到的，模式要么是一个变量，要么是应用于其他模式的构造器，要么是一个正规化为该形式的表达式（其中非构造器用 ``[matchPattern]`` 属性标记）。构造器的出现会提示情况拆分，构造器的参数由给定的变量表示。在[依值模式匹配](#依值模式匹配)一节中，我们将看到有时有必要在模式中包含明确的项，这些项需要进行表达式类型检查，尽管它们在模式匹配中没有起到作用。由于这个原因，这些被称为「不可访问的模式」。但是在[依值模式匹配](#依值模式匹配)一节之前，我们将不需要使用这种不可访问的模式。 +这里 `(a : α)` 是一个参数序列，`(b : β)` 是进行模式匹配的参数序列，`γ` 是任何类型，它可以取决于 `a` 和 `b `。每一行应该包含相同数量的模式，对应于 `β` 的每个元素。正如我们所看到的，模式要么是一个变量，要么是应用于其他模式的构造子，要么是一个正规化为该形式的表达式（其中非构造子用 ``[matchPattern]`` 属性标记）。构造子的出现会提示情况拆分，构造子的参数由给定的变量表示。在[依值模式匹配](#依值模式匹配)一节中，我们将看到有时有必要在模式中包含明确的项，这些项需要进行表达式类型检查，尽管它们在模式匹配中没有起到作用。由于这个原因，这些被称为「不可访问的模式」。但是在[依值模式匹配](#依值模式匹配)一节之前，我们将不需要使用这种不可访问的模式。 -正如我们在上一节所看到的，项 `t₁,...,tₙ` 可以利用任何一个参数 `a`，以及在相应模式中引入的任何一个变量。使得递归和归纳成为可能的是，它们也可以涉及对 ``foo`` 的递归调用。在本节中，我们将处理**结构性递归**，其中 `foo` 的参数出现在 `:=` 的右侧，是左侧模式的子项。我们的想法是，它们在结构上更小，因此在归纳类型中出现在更早的阶段。下面是上一章的一些结构递归的例子，现在用方程编译器来定义。 +正如我们在上一节所看到的，项 `t₁,...,tₙ` 可以利用任何一个参数 `a`，以及在相应模式中引入的任何一个变量。使得递归和归纳成为可能的是，它们也可以涉及对 ``foo`` 的递归调用。在本节中，我们将处理 **结构性递归** ，其中 `foo` 的参数出现在 `:=` 的右侧，是左侧模式的子项。我们的想法是，它们在结构上更小，因此在归纳类型中出现在更早的阶段。下面是上一章的一些结构递归的例子，现在用方程编译器来定义。 ```lean open Nat @@ -633,7 +633,7 @@ proofs of `zero_add` work: ``zero_add`` 的证明清楚地表明，归纳证明实际上是 Lean 中的一种递归形式。 -上面的例子表明，``add``的定义方程具有定义意义，`` mul``也是如此。方程编译器试图确保在任何可能的情况下都是这样，就像直接的结构归纳法一样。然而，在其他情况下，约简只在命题上成立，也就是说，它们是必须明确应用的方程定理。方程编译器在内部生成这样的定理。用户不能直接使用它们;相反，``simp``策略被配置为在必要时使用它们。因此，对`zero_add`的以下两种证明都成立： +上面的例子表明，``add`` 的定义方程具有定义意义，`` mul`` 也是如此。方程编译器试图确保在任何可能的情况下都是这样，就像直接的结构归纳法一样。然而，在其他情况下，约简只在命题上成立，也就是说，它们是必须明确应用的方程定理。方程编译器在内部生成这样的定理。用户不能直接使用它们;相反，``simp`` 策略被配置为在必要时使用它们。因此，对`zero_add`的以下两种证明都成立： ```lean open Nat @@ -742,9 +742,9 @@ type. You can get a sense of how it works by looking at the types of ``Nat.below`` and ``Nat.brecOn``: --> -在这两种情况下，Lean都会生成辅助函数 ``fibFast.loop``。 +在这两种情况下，Lean 都会生成辅助函数 ``fibFast.loop``。 -为了处理结构递归，方程编译器使用**值过程**（course-of-values）递归，使用由每个归纳定义类型自动生成的常量 `below` 和 `brecOn`。你可以通过查看 ``Nat.below`` 和 ``Nat.brecOn`` 的类型来了解它是如何工作的。 +为了处理结构递归，方程编译器使用 **值过程** （course-of-values）递归，使用由每个归纳定义类型自动生成的常量 `below` 和 `brecOn`。你可以通过查看 ``Nat.below`` 和 ``Nat.brecOn`` 的类型来了解它是如何工作的。 ```lean variable (C : Nat → Type u) @@ -847,7 +847,7 @@ Local recursive declarations You can define local recursive declarations using the `let rec` keyword. --> -可以使用``let rec``关键字定义局域递归声明。 +可以使用 ``let rec`` 关键字定义局域递归声明。 ```lean def replicate (n : Nat) (a : α) : List α := @@ -870,7 +870,7 @@ at `let rec loop`. You can also use `let rec` in tactic mode and for creating proofs by induction. --> -Lean为每个 ``let rec`` 创建一个辅助声明。在上面的例子中，它对于出现在 ``replicate`` 的 ``let rec loop`` 创建了声明 ``replication.loop``。请注意，Lean 通过添加 ``let rec`` 声明中出现的任何局部变量作为附加参数来「关闭」声明。例如，局部变量 ``a`` 出现在 ``let rec`` 循环中。 +Lean 为每个 ``let rec`` 创建一个辅助声明。在上面的例子中，它对于出现在 ``replicate`` 的 ``let rec loop`` 创建了声明 ``replication.loop``。请注意，Lean 通过添加 ``let rec`` 声明中出现的任何局部变量作为附加参数来「关闭」声明。例如，局部变量 ``a`` 出现在 ``let rec`` 循环中。 你也可以在策略证明模式中使用 ``let rec``，并通过归纳来创建证明。 @@ -894,7 +894,7 @@ You can also introduce auxiliary recursive declarations using `where` clause aft Lean converts them into a `let rec`. --> -还可以在定义后使用 ``where`` 子句引入辅助递归声明。Lean将它们转换为 ``let rec``。 +还可以在定义后使用 ``where`` 子句引入辅助递归声明。Lean 将它们转换为 ``let rec``。 ```lean def replicate (n : Nat) (a : α) : List α := @@ -1007,7 +1007,7 @@ founded orders from others, for example, using lexicographic order. Here is essentially the definition of division on the natural numbers that is found in the standard library. --> -这里有一大堆字，但我们熟悉第一块：类型 ``α``，关系 ``r``和假设 ``h``，即 ``r`` 是有良基的。变量' ``C`` 代表递归定义的动机：对于每个元素 ``x : α``，我们想构造一个 ``C x`` 的元素。函数 ``F`` 提供了这样做的归纳方法：它告诉我们如何构造一个元素 ``C x``，给定 ``C y`` 的元素对于 ``x`` 的每个 ``y``。 +这里有一大堆字，但我们熟悉第一块：类型 ``α``，关系 ``r`` 和假设 ``h``，即 ``r`` 是有良基的。变量' ``C`` 代表递归定义的动机：对于每个元素 ``x : α``，我们想构造一个 ``C x`` 的元素。函数 ``F`` 提供了这样做的归纳方法：它告诉我们如何构造一个元素 ``C x``，给定 ``C y`` 的元素对于 ``x`` 的每个 ``y``。 注意 ``WellFounded.fix`` 和归纳法原理一样有效。它说如果 ``≺`` 是良基的，而你想要证明 ``∀ x, C x``，那么只要证明对于任意的 ``x``，如果我们有 ``∀ y ≺ x, C y``，那么我们就有 ``C x`` 就足够了。 @@ -1046,7 +1046,7 @@ The elaborator is designed to make definitions like this more convenient. It accepts the following: --> -这个定义有点难以理解。这里递归在 ``x``上， ``div.F x f : Nat → Nat`` 为固定的 ``x`` 返回「除以 ``y``」函数。你要记住 ``div.F`` 的第二个参数 ``f`` 是递归的具体实现，这个函数对所有小于 ``x`` 的自然数 ``x₁`` 返回「除以 ``y``」函数。 +这个定义有点难以理解。这里递归在 ``x`` 上， ``div.F x f : Nat → Nat`` 为固定的 ``x`` 返回「除以 ``y``」函数。你要记住 ``div.F`` 的第二个参数 ``f`` 是递归的具体实现，这个函数对所有小于 ``x`` 的自然数 ``x₁`` 返回「除以 ``y``」函数。 繁饰器（Elaborator）可以使这样的定义更加方便。它接受下列内容: @@ -1153,7 +1153,7 @@ Note that a lexicographic order is used in the example above because the instanc `WellFoundedRelation (α × β)` uses a lexicographic order. Lean also defines the instance --> -注意，在上面的例子中使用了字典序，因为实例 `WellFoundedRelation (α × β)` 使用了字典序。Lean还定义了实例 +注意，在上面的例子中使用了字典序，因为实例 `WellFoundedRelation (α × β)` 使用了字典序。Lean 还定义了实例 ```lean instance (priority := low) [SizeOf α] : WellFoundedRelation α := @@ -1305,7 +1305,7 @@ Summary: - 如果没有 `termination_by`，良基关系（可能）可以这样被导出：选择一个参数，然后使用类型类解析为该参数的类型合成一个良基关系。 - 如果指定了 `termination_by`，它将函数的参数映射为类型 `α`，并再次使用类型类解析。 回想一下，`β × γ` 的默认实例是基于 `β` 和 `γ`的良基关系的字典序。 -- +- - `Nat` 的默认良基关系实例是 `<`。 - 默认情况下，策略 `decreasing_tactic` 用于显示递归应用小于选择的良基关系。如果 `decreasing_tactic` 失败，错误信息包括剩余目标 `... |- G`。注意，`decreasing_tactic` 使用 `assumption`。所以，你可以用 `have` 表达式来证明目标 `G`。你也可以使用 `decreasing_by` 来提供你自己的策略。 @@ -1365,7 +1365,7 @@ end The constructors, ``even_zero``, ``even_succ``, and ``odd_succ`` provide positive means for showing that a number is even or odd. We need to use the fact that the inductive type is generated by these constructors to know that zero is not odd, and that the latter two implications reverse. As usual, the constructors are kept in a namespace that is named after the type being defined, and the command ``open Even Odd`` allows us to access them more conveniently. --> -构造器``even_zero``、``even_succ`` 和 ``odd_succ`` 提供了显示数字是偶数还是奇数的积极方法。我们需要利用归纳类型是由这些构造器生成的这一事实来知道零不是奇数，并且后两个含义是相反的。像往常一样，构造器保存在以定义的类型命名的命名空间中，并且命令 ``open Even Odd`` 允许我们更方便地访问它们。 +构造子 ``even_zero``、``even_succ`` 和 ``odd_succ`` 提供了显示数字是偶数还是奇数的积极方法。我们需要利用归纳类型是由这些构造子生成的这一事实来知道零不是奇数，并且后两个含义是相反的。像往常一样，构造子保存在以定义的类型命名的命名空间中，并且命令 ``open Even Odd`` 允许我们更方便地访问它们。 ```lean # mutual @@ -1565,7 +1565,7 @@ equations, and the equation compiler generates all the boilerplate code automatically for us. Here are a number of similar examples: --> -在 ``nil`` 的情况下，``m`` 被实例化为 ``0``，``noConfusion`` 利用了 ``0 = succ n`` 不能出现的事实。否则，``v`` 的形式为 ``a :: w``，我们可以简单地将 ``w``从长度 ``m`` 的向量转换为长度 ``n``的向量后返回 ``w``。 +在 ``nil`` 的情况下，``m`` 被实例化为 ``0``，``noConfusion`` 利用了 ``0 = succ n`` 不能出现的事实。否则，``v`` 的形式为 ``a :: w``，我们可以简单地将 ``w`` 从长度 ``m`` 的向量转换为长度 ``n`` 的向量后返回 ``w``。 定义 ``tail`` 的困难在于维持索引之间的关系。 ``tailAux`` 中的假设 ``e : m = n + 1`` 用于传达 ``n`` 与与小前提相关的索引之间的关系。此外，``zero = n + 1`` 的情况是不可达的，而放弃这种情况的规范方法是使用 ``noConfusion``。 @@ -1659,9 +1659,9 @@ define the function ``inverse`` below, we *have to* mark ``f a`` inaccessible. --> -有时候，依值匹配模式中的参数对定义来说并不是必需的，但是必须包含它来适当地确定表达式的类型。Lean 允许用户将这些子项标记为「不可访问」以进行模式匹配。例如，当左侧出现的项既不是变量也不是构造器应用时，这些注解是必不可少的，因为它们不适合用于模式匹配的目标。我们可以将这种不可访问的模式视为模式的「不关心」组件。你可以通过写 ``.(t)`` 来声明子项不可访问。如果不可访问的模式可以被推断出来，你也可以写 ``_``。 +有时候，依值匹配模式中的参数对定义来说并不是必需的，但是必须包含它来适当地确定表达式的类型。Lean 允许用户将这些子项标记为「不可访问」以进行模式匹配。例如，当左侧出现的项既不是变量也不是构造子应用时，这些注解是必不可少的，因为它们不适合用于模式匹配的目标。我们可以将这种不可访问的模式视为模式的「不关心」组件。你可以通过写 ``.(t)`` 来声明子项不可访问。如果不可访问的模式可以被推断出来，你也可以写 ``_``。 -下面的例子中，我们声明了一个归纳类型，它定义了「在 ``f`` 的像中」的属性。您可以将 ``ImageOf f b`` 类型的元素视为 ``b`` 位于 ``f`` 的像中的证据，构造器``imf`` 用于构建此类证据。然后，我们可以定义任何函数 ``f`` 的「逆」，逆函数将 ``f`` 的像中的任何元素赋给映射到它的元素。类型规则迫使我们为第一个参数写 ``f a``，但是这个项既不是变量也不是构造器应用，并且在模式匹配定义中没有作用。为了定义下面的函数 ``inverse``，我们必须将 ``f a`` 标记为不可访问。 +下面的例子中，我们声明了一个归纳类型，它定义了「在 ``f`` 的像中」的属性。您可以将 ``ImageOf f b`` 类型的元素视为 ``b`` 位于 ``f`` 的像中的证据，构造子 ``imf`` 用于构建此类证据。然后，我们可以定义任何函数 ``f`` 的「逆」，逆函数将 ``f`` 的像中的任何元素赋给映射到它的元素。类型规则迫使我们为第一个参数写 ``f a``，但是这个项既不是变量也不是构造子应用，并且在模式匹配定义中没有作用。为了定义下面的函数 ``inverse``，我们必须将 ``f a`` 标记为不可访问。 ```lean inductive ImageOf {α β : Type u} (f : α → β) : β → Type u where @@ -1770,7 +1770,7 @@ implements a new feature, *discriminant refinement*, which includes these extra discriminants automatically for us. --> -如前所述，参数 ``{n : Nat}`` 是模式匹配的一部分，因为它不能在整个定义中保持固定。在以前的 Lean 版本中，用户经常发现必须包含这些额外的判别符是很麻烦的。因此，Lean 4 实现了一个新特性，**判别精炼**（discriminant refinement），它自动为我们包含了这些额外的判别。 +如前所述，参数 ``{n : Nat}`` 是模式匹配的一部分，因为它不能在整个定义中保持固定。在以前的 Lean 版本中，用户经常发现必须包含这些额外的判别符是很麻烦的。因此，Lean 4 实现了一个新特性， **判别精炼（discriminant refinement）** ，它自动为我们包含了这些额外的判别。 ```lean # inductive Vector (α : Type u) : Nat → Type u @@ -2089,7 +2089,7 @@ Write a function that evaluates such an expression, evaluating each ``var n`` to 此处 ``sampleExpr`` 表示 ``(v₀ * 7) + (2 * v₁)``。 -写一个函数来计算这些表达式，对每个``var n``赋值``v n``. +写一个函数来计算这些表达式，对每个 ``var n`` 赋值 ``v n``. -我们已经看到Lean的形式基础包括基本类型，``Prop, Type 0, Type 1, Type 2, ...``，并允许形成依值函数类型，``(x : α) → β``。在例子中，我们还使用了额外的类型，如``Bool``、``Nat``和``Int``，以及类型构造器，如``List``和乘积``×``。事实上，在Lean的库中，除了宇宙之外的每一个具体类型和除了依值箭头之外的每一个类型构造器都是一个被称为*归纳类型*的类型构造的一般类别的实例。值得注意的是，仅用类型宇宙、依值箭头类型和归纳类型就可以构建一个内涵丰富的数学大厦；其他一切都源于这些。 +我们已经看到Lean 的形式基础包括基本类型，``Prop, Type 0, Type 1, Type 2, ...``，并允许形成依值函数类型，``(x : α) → β``。在例子中，我们还使用了额外的类型，如 ``Bool``、``Nat`` 和 ``Int``，以及类型构造子，如 ``List`` 和乘积 ``×``。事实上，在Lean 的库中，除了宇宙之外的每一个具体类型和除了依值箭头之外的每一个类型构造子都是一个被称为*归纳类型*的类型构造的一般类别的实例。值得注意的是，仅用类型宇宙、依值箭头类型和归纳类型就可以构建一个内涵丰富的数学大厦；其他一切都源于这些。 -直观地说，一个归纳类型是由一个指定的构造器列表建立起来的。在Lean中，指定这种类型的语法如下： +直观地说，一个归纳类型是由一个指定的构造子列表建立起来的。在Lean 中，指定这种类型的语法如下： ``` inductive Foo where @@ -75,15 +75,15 @@ some basic examples of inductive types, and work our way up to more elaborate and complex examples. --> -我们的直觉是，每个构造器都指定了一种建立新的对象``Foo``的方法，可能是由以前构造的值构成。``Foo``类型只不过是由以这种方式构建的对象组成。归纳式声明中的第一个字符也可以用逗号而不是``|``来分隔构造器。 +我们的直觉是，每个构造子都指定了一种建立新的对象 ``Foo`` 的方法，可能是由以前构造的值构成。``Foo`` 类型只不过是由以这种方式构建的对象组成。归纳式声明中的第一个字符也可以用逗号而不是 ``|`` 来分隔构造子。 -我们将在下面看到，构造器的参数可以包括``Foo``类型的对象，但要遵守一定的「正向性」约束，即保证``Foo``的元素是自下而上构建的。粗略地说，每个`...`可以是由``Foo``和以前定义的类型构建的任何箭头类型，其中``Foo``如果出现，也只是作为依值箭头类型的「目标」。 +我们将在下面看到，构造子的参数可以包括 ``Foo`` 类型的对象，但要遵守一定的「正向性」约束，即保证 ``Foo`` 的元素是自下而上构建的。粗略地说，每个`...`可以是由 ``Foo`` 和以前定义的类型构建的任何箭头类型，其中 ``Foo`` 如果出现，也只是作为依值箭头类型的「目标」。 我们将提供一些归纳类型的例子。我们还把上述方案稍微扩展，即相互定义的归纳类型，以及所谓的*归纳族*。 -就像逻辑连接词一样，每个归纳类型都有引入规则，说明如何构造该类型的一个元素；还有消去规则，说明如何在另一个构造中「使用」该类型的一个元素。其实逻辑连接词也是归纳类型结构的例子。你已经看到了归纳类型的引入规则：它们只是在类型的定义中指定的构造器。消去规则提供了类型上的递归原则，其中也包括作为一种特殊情况的归纳原则。 +就像逻辑连接词一样，每个归纳类型都有引入规则，说明如何构造该类型的一个元素；还有消去规则，说明如何在另一个构造中「使用」该类型的一个元素。其实逻辑连接词也是归纳类型结构的例子。你已经看到了归纳类型的引入规则：它们只是在类型的定义中指定的构造子。消去规则提供了类型上的递归原则，其中也包括作为一种特殊情况的归纳原则。 -在下一章中，我们将介绍Lean的函数定义包，它提供了更方便的方法来定义归纳类型上的函数并进行归纳证明。但是由于归纳类型的概念是如此的基本，我们觉得从低级的、实践的理解开始是很重要的。我们将从归纳类型的一些基本例子开始，然后逐步上升到更详细和复杂的例子。 +在下一章中，我们将介绍Lean 的函数定义包，它提供了更方便的方法来定义归纳类型上的函数并进行归纳证明。但是由于归纳类型的概念是如此的基本，我们觉得从低级的、实践的理解开始是很重要的。我们将从归纳类型的一些基本例子开始，然后逐步上升到更详细和复杂的例子。 -``inductive``命令创建了一个新类型``Weekday``。构造器都在``Weekday``命名空间中。 +``inductive`` 命令创建了一个新类型 ``Weekday``。构造子都在 ``Weekday`` 命名空间中。 ```lean # inductive Weekday where @@ -167,9 +167,9 @@ We will use the `match` expression to define a function from ``Weekday`` to the natural numbers: --> -把``sunday``、``monday``、... 、``saturday``看作是``Weekday``的不同元素，没有其他有区别的属性。消去规则``Weekday.rec``，与``Weekday``类型及其构造器一起定义。它也被称为**递归器**（Recursor），它是使该类型「归纳」的原因：它允许我们通过给每个构造器分配相应的值来定义`Weekday`的函数。直观的说，归纳类型是由构造器详尽地生成的，除了它们构造的元素外，没有其他元素。 +把 ``sunday``、``monday``、... 、``saturday`` 看作是 ``Weekday`` 的不同元素，没有其他有区别的属性。消去规则 ``Weekday.rec``，与 ``Weekday`` 类型及其构造子一起定义。它也被称为 **递归器（Recursor）** ，它是使该类型「归纳」的原因：它允许我们通过给每个构造子分配相应的值来定义`Weekday`的函数。直观的说，归纳类型是由构造子详尽地生成的，除了它们构造的元素外，没有其他元素。 -我们将使用`match`表达式来定义一个从``Weekday``到自然数的函数： +我们将使用`match`表达式来定义一个从 ``Weekday`` 到自然数的函数： ```lean # inductive Weekday where @@ -253,9 +253,9 @@ Lean to generate a function that converts `Weekday` objects into text. This function is used by the `#eval` command to display `Weekday` objects. --> -> 译者注：此处详细解释一下递归器`rec`。递归器作为归纳类型的消去规则，用于构造归纳类型到其他类型的函数。从最朴素的集合论直觉上讲，枚举类型的函数只需要规定每个元素的对应，也就是`match`的方式，但是要注意，`match`并不像其他Lean关键字那样是一种简单的语法声明，它实际上是一种功能，而这并不是类型论自带的功能。因此`match`需要一个类型论实现，也就是递归器。现在我们通过`#check @Weekday.rec`命令的输出来看递归器是如何工作的。首先回忆`@`是显式参数的意思。递归器是一个复杂的函数，输入的信息有1）motive：一个「目的」函数，表明想要拿当前类型构造什么类型。这个输出类型足够一般所以在u上；2）motive函数对所有枚举元素的输出值(这里就显得它非常「递归」)。这两点是准备工作，下面是这个函数的实际工作：输入一个具体的属于这个枚举类型的项`t`，输出结果`motive t`。下文在非枚举类型中，会直接用到这些递归器，届时可以更清晰地看到它们如何被使用。 +> 译者注：此处详细解释一下递归器`rec`。递归器作为归纳类型的消去规则，用于构造归纳类型到其他类型的函数。从最朴素的集合论直觉上讲，枚举类型的函数只需要规定每个元素的对应，也就是`match`的方式，但是要注意，`match`并不像其他Lean 关键字那样是一种简单的语法声明，它实际上是一种功能，而这并不是类型论自带的功能。因此`match`需要一个类型论实现，也就是递归器。现在我们通过`#check @Weekday.rec`命令的输出来看递归器是如何工作的。首先回忆`@`是显式参数的意思。递归器是一个复杂的函数，输入的信息有1）motive：一个「目的」函数，表明想要拿当前类型构造什么类型。这个输出类型足够一般所以在u上；2）motive函数对所有枚举元素的输出值(这里就显得它非常「递归」)。这两点是准备工作，下面是这个函数的实际工作：输入一个具体的属于这个枚举类型的项`t`，输出结果`motive t`。下文在非枚举类型中，会直接用到这些递归器，届时可以更清晰地看到它们如何被使用。 -当声明一个归纳数据类型时，你可以使用`deriving Repr`来指示Lean生成一个函数，将`Weekday`对象转换为文本。这个函数被`#eval`命令用来显示`Weekday`对象。 +当声明一个归纳数据类型时，你可以使用`deriving Repr`来指示Lean 生成一个函数，将`Weekday`对象转换为文本。这个函数被`#eval`命令用来显示`Weekday`对象。 ```lean inductive Weekday where @@ -282,9 +282,9 @@ then allowed to use the shorter name when we open the namespace. We can define functions from ``Weekday`` to ``Weekday``: --> -将与某一结构相关的定义和定理归入同名的命名空间通常很有用。例如，我们可以将``numberOfDay``函数放在``Weekday``命名空间中。然后当我们打开命名空间时，我们就可以使用较短的名称。 +将与某一结构相关的定义和定理归入同名的命名空间通常很有用。例如，我们可以将 ``numberOfDay`` 函数放在 ``Weekday`` 命名空间中。然后当我们打开命名空间时，我们就可以使用较短的名称。 -我们可以定义从``Weekday``到``Weekday``的函数： +我们可以定义从 ``Weekday`` 到 ``Weekday`` 的函数： ```lean # inductive Weekday where @@ -332,7 +332,7 @@ for any Weekday ``d``? You can use `match` to provide a proof of the claim for e constructor: --> -我们如何证明``next (previous d) = d``对于任何Weekday``d``的一般定理？你可以使用`match`来为每个构造器提供一个证明： +我们如何证明 ``next (previous d) = d`` 对于任何Weekday``d`` 的一般定理？你可以使用`match`来为每个构造子提供一个证明： ```lean # inductive Weekday where @@ -429,9 +429,9 @@ enumerated type. 下面的[归纳类型的策略](#归纳类型的策略)一节将介绍额外的策略，这些策略是专门为利用归纳类型而设计。 -命题即类型的对应原则下，我们可以使用``match``来证明定理和定义函数。换句话说，逐情况证明是一种逐情况定义的另一表现形式，其中被「定义」的是一个证明而不是一段数据。 +命题即类型的对应原则下，我们可以使用 ``match`` 来证明定理和定义函数。换句话说，逐情况证明是一种逐情况定义的另一表现形式，其中被「定义」的是一个证明而不是一段数据。 -Lean库中的`Bool`类型是一个枚举类型的实例。 +Lean 库中的`Bool`类型是一个枚举类型的实例。 ```lean # namespace Hidden @@ -455,9 +455,9 @@ suggest defining boolean operations ``and``, ``or``, ``not`` on the binary operation like ``and`` using `match`: --> -（为了运行这个例子，我们把它们放在一个叫做``Hidden``的命名空间中，这样像``Bool``这样的名字就不会和标准库中的 ``Bool``冲突。这是必要的，因为这些类型是Lean「启动工作」的一部分，在系统启动时被自动导入）。 +（为了运行这个例子，我们把它们放在一个叫做 ``Hidden`` 的命名空间中，这样像 ``Bool`` 这样的名字就不会和标准库中的 ``Bool`` 冲突。这是必要的，因为这些类型是Lean「启动工作」的一部分，在系统启动时被自动导入）。 -作为一个练习，你应该思考这些类型的引入和消去规则的作用。作为进一步的练习，我们建议在``Bool``类型上定义布尔运算 ``and``、``or``、``not``，并验证其共性。提示，你可以使用`match`来定义像`and`这样的二元运算： +作为一个练习，你应该思考这些类型的引入和消去规则的作用。作为进一步的练习，我们建议在 ``Bool`` 类型上定义布尔运算 ``and``、``or``、``not``，并验证其共性。提示，你可以使用`match`来定义像`and`这样的二元运算： ```lean # namespace Hidden @@ -472,14 +472,14 @@ def and (a b : Bool) : Bool := Similarly, most identities can be proved by introducing suitable `match`, and then using ``rfl``. --> -同样地，大多数等式可以通过引入合适的`match`，然后使用``rfl``来证明。 +同样地，大多数等式可以通过引入合适的`match`，然后使用 ``rfl`` 来证明。 -带参数的构造器 +带参数的构造子 --------------------------- -枚举类型是归纳类型的一种非常特殊的情况，其中构造器根本不需要参数。一般来说，「构造」可以依赖于数据，然后在构造参数中表示。考虑一下库中的乘积类型和求和类型的定义: +枚举类型是归纳类型的一种非常特殊的情况，其中构造子根本不需要参数。一般来说，「构造」可以依赖于数据，然后在构造参数中表示。考虑一下库中的乘积类型和求和类型的定义: ```lean # namespace Hidden @@ -514,7 +514,7 @@ library defines notation ``α × β`` for ``Prod α β`` and ``(a, b)`` for ``Prod.mk a b``. --> -思考一下这些例子中发生了什么。乘积类型有一个构造器``Prod.mk``，它需要两个参数。要在``Prod α β``上定义一个函数，我们可以假设输入的形式是``Prod.mk a b``，而我们必须指定输出，用``a``和``b``来表示。我们可以用它来定义``Prod``的两个投影。标准库定义的符号``α × β``表示``Prod α β``，``(a, b)``表示``Prod.mk a b``。 +思考一下这些例子中发生了什么。乘积类型有一个构造子 ``Prod.mk``，它需要两个参数。要在 ``Prod α β`` 上定义一个函数，我们可以假设输入的形式是 ``Prod.mk a b``，而我们必须指定输出，用 ``a`` 和 ``b`` 来表示。我们可以用它来定义 ``Prod`` 的两个投影。标准库定义的符号 ``α × β`` 表示 ``Prod α β``，``(a, b)`` 表示 ``Prod.mk a b``。 ```lean # namespace Hidden @@ -540,7 +540,7 @@ Here is another example where we use the recursor `Prod.casesOn` instead of `match`. --> -函数``fst``接收一个对``p``。``match``将`p`解释为一个对``Prod.mk a b``。还记得在[依值类型论](./dependent_type_theory.md)中，为了给这些定义以最大的通用性，我们允许类型``α``和``β``属于任何宇宙。 +函数 ``fst`` 接收一个对 ``p``。``match`` 将`p`解释为一个对 ``Prod.mk a b``。还记得在[依值类型论](./dependent_type_theory.md)中，为了给这些定义以最大的通用性，我们允许类型 ``α`` 和 ``β`` 属于任何宇宙。 下面是另一个例子，我们用递归器`Prod.casesOn`代替`match`。 @@ -572,7 +572,7 @@ output value in terms of ``b``. 参数`motive`是用来指定你要构造的对象的类型，它是一个依值的函数，`_`是被自动推断出的类型，此处即`Bool × Nat`。函数`cond`是一个布尔条件：`cond b t1 t2`，如果`b`为真，返回`t1`，否则返回`t2`。函数`prod_example`接收一个由布尔值`b`和一个数字`n`组成的对，并根据`b`为真或假返回`2 * n`或`2 * n + 1`。 -相比之下，求和类型有*两个*构造器`inl`和`inr`（表示「从左引入」和「从右引入」），每个都需要**一个**（显式的）参数。要在``Sum α β``上定义一个函数，我们必须处理两种情况：要么输入的形式是``inl a``，由此必须依据``a``指定一个输出值；要么输入的形式是``inr b``，由此必须依据``b``指定一个输出值。 +相比之下，求和类型有*两个*构造子`inl`和`inr`（表示「从左引入」和「从右引入」），每个都需要 **一个** （显式的）参数。要在 ``Sum α β`` 上定义一个函数，我们必须处理两种情况：要么输入的形式是 ``inl a``，由此必须依据 ``a`` 指定一个输出值；要么输入的形式是 ``inr b``，由此必须依据 ``b`` 指定一个输出值。 ```lean def sum_example (s : Sum Nat Nat) : Nat := @@ -613,15 +613,15 @@ As with function definitions, Lean's inductive definition syntax will let you put named arguments to the constructors before the colon: --> -这个例子与前面的例子类似，但现在输入到`sum_example`的内容隐含了`inl n`或`inr n`的形式。在第一种情况下，函数返回``2 * n``，第二种情况下，它返回``2 * n + 1``。 +这个例子与前面的例子类似，但现在输入到`sum_example`的内容隐含了`inl n`或`inr n`的形式。在第一种情况下，函数返回 ``2 * n``，第二种情况下，它返回 ``2 * n + 1``。 -注意，乘积类型取决于参数`α β : Type`，这些参数是构造器和`Prod`的参数。Lean会检测这些参数何时可以从构造器的参数或返回类型中推断出来，并在这种情况下使其隐式。 +注意，乘积类型取决于参数`α β : Type`，这些参数是构造子和`Prod`的参数。Lean 会检测这些参数何时可以从构造子的参数或返回类型中推断出来，并在这种情况下使其隐式。 -在[定义自然数](#定义自然数)一节中，我们将看到当归纳类型的构造器从归纳类型本身获取参数时会发生什么。本节考虑的例子暂时不是这样：每个构造器只依赖于先前指定的类型。 +在[定义自然数](#定义自然数)一节中，我们将看到当归纳类型的构造子从归纳类型本身获取参数时会发生什么。本节考虑的例子暂时不是这样：每个构造子只依赖于先前指定的类型。 -一个有多个构造器的类型是析取的：``Sum α β``的一个元素要么是``inl a``的形式，要么是``inl b``的形式。一个有多个参数的构造器引入了合取信息：从``Prod.mk a b``的元素``Prod α β``中我们可以提取``a``*和*``b``。一个任意的归纳类型可以包括这两个特征：拥有任意数量的构造器，每个构造器都需要任意数量的参数。 +一个有多个构造子的类型是析取的：``Sum α β`` 的一个元素要么是 ``inl a`` 的形式，要么是 ``inl b`` 的形式。一个有多个参数的构造子引入了合取信息：从 ``Prod.mk a b`` 的元素 ``Prod α β`` 中我们可以提取 ``a``*和*``b``。一个任意的归纳类型可以包括这两个特征：拥有任意数量的构造子，每个构造子都需要任意数量的参数。 -和函数定义一样，Lean的归纳定义语法可以让你把构造器的命名参数放在冒号之前： +和函数定义一样，Lean 的归纳定义语法可以让你把构造子的命名参数放在冒号之前： ```lean # namespace Hidden @@ -648,7 +648,7 @@ well as its projections, at the same time. 这些定义的结果与本节前面给出的定义基本相同。 -像``Prod``这样只有一个构造器的类型是纯粹的合取型：构造器只是将参数列表打包成一块数据，基本上是一个元组，后续参数的类型可以取决于初始参数的类型。我们也可以把这样的类型看作是一个「记录」或「结构体」。在Lean中，关键词``structure``可以用来同时定义这样一个归纳类型以及它的投影。 +像 ``Prod`` 这样只有一个构造子的类型是纯粹的合取型：构造子只是将参数列表打包成一块数据，基本上是一个元组，后续参数的类型可以取决于初始参数的类型。我们也可以把这样的类型看作是一个「记录」或「结构体」。在Lean 中，关键词 ``structure`` 可以用来同时定义这样一个归纳类型以及它的投影。 ```lean # namespace Hidden @@ -668,9 +668,9 @@ example, the following defines a record to store a color as a triple of RGB values: --> -这个例子同时引入了归纳类型``Prod``，它的构造器``mk``，通常的消去器（``rec``和``recOn``），以及投影``fst``和``snd``。 +这个例子同时引入了归纳类型 ``Prod``，它的构造子 ``mk``，通常的消去器（``rec`` 和 ``recOn``），以及投影 ``fst`` 和 ``snd``。 -如果你没有命名构造器，Lean使用`mk`作为默认值。例如，下面定义了一个记录，将一个颜色存储为RGB值的三元组： +如果你没有命名构造子，Lean 使用`mk`作为默认值。例如，下面定义了一个记录，将一个颜色存储为RGB值的三元组： ```lean structure Color where @@ -689,7 +689,7 @@ shown, and the projection ``Color.red`` returns the red component. You can avoid the parentheses if you add a line break between each field. --> -``yellow``的定义形成了有三个值的记录，而投影``Color.red``则返回红色成分。 +``yellow`` 的定义形成了有三个值的记录，而投影 ``Color.red`` 则返回红色成分。 如果你在每个字段之间加一个换行符，就可以不用括号。 @@ -708,7 +708,7 @@ working with them. Here, for example, is the definition of a semigroup: --> -``structure``命令对于定义代数结构特别有用，Lean提供了大量的基础设施来支持对它们的处理。例如，这里是一个半群的定义： +``structure`` 命令对于定义代数结构特别有用，Lean 提供了大量的基础设施来支持对它们的处理。例如，这里是一个半群的定义： ```lean structure Semigroup where @@ -776,11 +776,11 @@ types is inhabited, and that the type of functions to an inhabited type is inhabited. --> -在依值类型论的语义中，没有内置的部分函数的概念。一个函数类型``α → β``或一个依值函数类型``(a : α) → β``的每个元素都被假定为在每个输入端有一个值。``Option``类型提供了一种表示部分函数的方法。`Option β`的一个元素要么是`none`，要么是`some b`的形式，用于某个值`b : β`。因此我们可以认为`α → Option β`类型的元素`f`是一个从`α`到`β`的部分函数：对于每一个`a : α`，`f a`要么返回`none`，表示`f a`是「未定义」，要么返回`some b`。 +在依值类型论的语义中，没有内置的部分函数的概念。一个函数类型 ``α → β`` 或一个依值函数类型 ``(a : α) → β`` 的每个元素都被假定为在每个输入端有一个值。``Option`` 类型提供了一种表示部分函数的方法。`Option β`的一个元素要么是`none`，要么是`some b`的形式，用于某个值`b : β`。因此我们可以认为`α → Option β`类型的元素`f`是一个从`α`到`β`的部分函数：对于每一个`a : α`，`f a`要么返回`none`，表示`f a`是「未定义」，要么返回`some b`。 -`Inhabited α`的一个元素只是证明了`α`有一个元素的事实。稍后，我们将看到``Inhabited``是Lean中*类型类*的一个例子：Lean可以被告知合适的基础类型是含有元素的，并且可以在此基础上自动推断出其他构造类型是含有元素的。 +`Inhabited α`的一个元素只是证明了`α`有一个元素的事实。稍后，我们将看到 ``Inhabited`` 是Lean 中*类型类*的一个例子：Lean 可以被告知合适的基础类型是含有元素的，并且可以在此基础上自动推断出其他构造类型是含有元素的。 -作为练习，我们鼓励你建立一个从``α``到``β``和``β``到``γ``的部分函数的组合概念，并证明其行为符合预期。我们也鼓励你证明``Bool``和``Nat``是含有元素的，两个含有元素的类型的乘积是含有元素的，以及到一个含有元素的类型的函数类型是含有元素的。 +作为练习，我们鼓励你建立一个从 ``α`` 到 ``β`` 和 ``β`` 到 ``γ`` 的部分函数的组合概念，并证明其行为符合预期。我们也鼓励你证明 ``Bool`` 和 ``Nat`` 是含有元素的，两个含有元素的类型的乘积是含有元素的，以及到一个含有元素的类型的函数类型是含有元素的。 -你应该想一想这些是如何产生你已经看到的引入和消去规则的。有一些规则规定了归纳类型的消去器可以去消去什么，或者说，哪些类型可以成为递归器的目标。粗略地说，``Prop``中的归纳类型的特点是，只能消去成``Prop``中的其他类型。这与以下理解是一致的：如果``p : Prop``，一个元素``hp : p``不携带任何数据。然而，这个规则有一个小的例外，我们将在[归纳族](#归纳族)一节中讨论。 +你应该想一想这些是如何产生你已经看到的引入和消去规则的。有一些规则规定了归纳类型的消去器可以去消去什么，或者说，哪些类型可以成为递归器的目标。粗略地说，``Prop`` 中的归纳类型的特点是，只能消去成 ``Prop`` 中的其他类型。这与以下理解是一致的：如果 ``p : Prop``，一个元素 ``hp : p`` 不携带任何数据。然而，这个规则有一个小的例外，我们将在[归纳族](#归纳族)一节中讨论。 甚至存在量词也是归纳式定义的： @@ -854,9 +854,9 @@ This is a good place to mention another inductive type, denoted ``∃ x : α, P`` and ``Σ x : α, P``. --> -请记住，符号``∃ x : α, p``是``Exists (fun x : α => p)``的语法糖。 +请记住，符号 ``∃ x : α, p`` 是 ``Exists (fun x : α => p)`` 的语法糖。 -`False`, `True`, `And`和`Or`的定义与`Empty`, `Unit`, `Prod`和`Sum`的定义完全类似。不同的是，第一组产生的是`Prop`的元素，第二组产生的是`Type u`的元素，适用于某些`u`。类似地，``∃ x : α, p``是``Σ x : α, p``的``Prop``值的变体。 +`False`, `True`, `And`和`Or`的定义与`Empty`, `Unit`, `Prod`和`Sum`的定义完全类似。不同的是，第一组产生的是`Prop`的元素，第二组产生的是`Type u`的元素，适用于某些`u`。类似地，``∃ x : α, p`` 是 ``Σ x : α, p`` 的 ``Prop`` 值的变体。 这里可以提到另一个归纳类型，表示为`{x : α // p}`，它有点像`∃ x : α, P`和`Σ x : α, P`之间的混合。 @@ -871,7 +871,7 @@ inductive Subtype {α : Type u} (p : α → Prop) where In fact, in Lean, ``Subtype`` is defined using the structure command: --> -事实上，在Lean中，``Subtype``是用结构体命令定义的。 +事实上，在Lean 中，``Subtype`` 是用结构体命令定义的。 ```lean # namespace Hidden @@ -887,7 +887,7 @@ It is modeled after subset notation in set theory: the idea is that ``{x : α // denotes the collection of elements of ``α`` that have property ``p``. --> -符号`{x : α // p x}`是``Subtype (fun x : α => p x)``的语法糖。它仿照集合理论中的子集表示法：`{x : α // p x}`表示具有属性`p`的`α`元素的集合。 +符号`{x : α // p x}`是 ``Subtype (fun x : α => p x)`` 的语法糖。它仿照集合理论中的子集表示法：`{x : α // p x}`表示具有属性`p`的`α`元素的集合。 -到目前为止，我们所看到的归纳定义的类型都是「无趣的」：构造器打包数据并将其插入到一个类型中，而相应的递归器则解压数据并对其进行操作。当构造器作用于被定义的类型中的元素时，事情就变得更加有趣了。一个典型的例子是自然数``Nat``类型： +到目前为止，我们所看到的归纳定义的类型都是「无趣的」：构造子打包数据并将其插入到一个类型中，而相应的递归器则解压数据并对其进行操作。当构造子作用于被定义的类型中的元素时，事情就变得更加有趣了。一个典型的例子是自然数 ``Nat`` 类型： ```lean # namespace Hidden @@ -938,9 +938,9 @@ next argument to the recursor specifies a value for ``f (succ n)`` in terms of ``n`` and ``f n``. If we check the type of the recursor, --> -有两个构造器，我们从``zero : Nat``开始；它不需要参数，所以我们一开始就有了它。相反，构造器`succ`只能应用于先前构造的`Nat`。将其应用于``zero``，得到``succ zero : Nat``。再次应用它可以得到`succ (succ zero) : Nat`，依此类推。直观地说，`Nat`是具有这些构造器的「最小」类型，这意味着它是通过从`zero`开始并重复应用`succ`这样无穷无尽地（并且自由地）生成的。 +有两个构造子，我们从 ``zero : Nat`` 开始；它不需要参数，所以我们一开始就有了它。相反，构造子`succ`只能应用于先前构造的`Nat`。将其应用于 ``zero``，得到 ``succ zero : Nat``。再次应用它可以得到`succ (succ zero) : Nat`，依此类推。直观地说，`Nat`是具有这些构造子的「最小」类型，这意味着它是通过从`zero`开始并重复应用`succ`这样无穷无尽地（并且自由地）生成的。 -和以前一样，``Nat``的递归器被设计用来定义一个从``Nat``到任何域的依值函数`f`，也就是一个`(n : nat) → motive n`的元素`f`，其中`motive : Nat → Sort u`。它必须处理两种情况：一种是输入为``zero``的情况，另一种是输入为 ``succ n``的情况，其中``n : Nat``。在第一种情况下，我们只需指定一个适当类型的目标值，就像以前一样。但是在第二种情况下，递归器可以假设在`n`处的`f`的值已经被计算过了。因此，递归器的下一个参数是以`n`和`f n`来指定`f (succ n)`的值。 +和以前一样，``Nat`` 的递归器被设计用来定义一个从 ``Nat`` 到任何域的依值函数`f`，也就是一个`(n : nat) → motive n`的元素`f`，其中`motive : Nat → Sort u`。它必须处理两种情况：一种是输入为 ``zero`` 的情况，另一种是输入为 ``succ n`` 的情况，其中 ``n : Nat``。在第一种情况下，我们只需指定一个适当类型的目标值，就像以前一样。但是在第二种情况下，递归器可以假设在`n`处的`f`的值已经被计算过了。因此，递归器的下一个参数是以`n`和`f n`来指定`f (succ n)`的值。 如果我们检查递归器的类型： @@ -977,7 +977,7 @@ Finally, the ``t : Nat``, is the input to the function. It is also known as the The `Nat.recOn` is similar to `Nat.rec` but the major premise occurs before the minor premises. --> -隐参数``motive``，是被定义的函数的陪域。在类型论中，通常说``motive``是消去/递归的**目的**，因为它描述了我们希望构建的对象类型。接下来的两个参数指定了如何计算零和后继的情况，如上所述。它们也被称为小前提``minor premises``。最后，``t : Nat``，是函数的输入。它也被称为大前提``major premise``。 +隐参数 ``motive``，是被定义的函数的陪域。在类型论中，通常说 ``motive`` 是消去/递归的 **目的** ，因为它描述了我们希望构建的对象类型。接下来的两个参数指定了如何计算零和后继的情况，如上所述。它们也被称为小前提 ``minor premises``。最后，``t : Nat``，是函数的输入。它也被称为大前提 ``major premise``。 `Nat.recOn`与`Nat.rec`类似，但大前提发生在小前提之前。 @@ -998,7 +998,7 @@ successor step, assuming the value ``add m n`` is already determined, we define ``add m (succ n)`` to be ``succ (add m n)``. --> -例如，考虑自然数上的加法函数``add m n``。固定`m`，我们可以通过递归来定义`n`的加法。在基本情况下，我们将`add m zero`设为`m`。在后续步骤中，假设`add m n`的值已经确定，我们将`add m (succ n)`定义为`succ (add m n)`。 +例如，考虑自然数上的加法函数 ``add m n``。固定`m`，我们可以通过递归来定义`n`的加法。在基本情况下，我们将`add m zero`设为`m`。在后续步骤中，假设`add m n`的值已经确定，我们将`add m (succ n)`定义为`succ (add m n)`。 ```lean # namespace Hidden @@ -1024,7 +1024,7 @@ then go on to define familiar notation in that namespace. The two defining equations for addition now hold definitionally: --> -将这些定义放入一个命名空间``Nat``是很有用的。然后我们可以继续在这个命名空间中定义熟悉的符号。现在加法的两个定义方程是成立的： +将这些定义放入一个命名空间 ``Nat`` 是很有用的。然后我们可以继续在这个命名空间中定义熟悉的符号。现在加法的两个定义方程是成立的： ```lean # namespace Hidden @@ -1061,9 +1061,9 @@ pattern of an inductive proof: to prove ``∀ n, motive n``, first prove ``motiv and then, for arbitrary ``n``, assume ``ih : motive n`` and prove ``motive (succ n)``. --> -我们将在[类型类](./type_classes.md)一章中解释``instance``命令如何工作。我们以后的例子将使用Lean自己的自然数版本。 +我们将在[类型类](./type_classes.md)一章中解释 ``instance`` 命令如何工作。我们以后的例子将使用Lean 自己的自然数版本。 -然而，证明像``zero + m = m``这样的事实，需要用归纳法证明。如上所述，归纳原则只是递归原则的一个特例，其中陪域``motive n``是``Prop``的一个元素。它代表了熟悉的归纳证明模式：要证明``∀ n, motive n``，首先要证明``motive 0``，然后对于任意的``n``，假设``ih : motive n``并证明``motive (succ n)``。 +然而，证明像 ``zero + m = m`` 这样的事实，需要用归纳法证明。如上所述，归纳原则只是递归原则的一个特例，其中陪域 ``motive n`` 是 ``Prop`` 的一个元素。它代表了熟悉的归纳证明模式：要证明 ``∀ n, motive n``，首先要证明 ``motive 0``，然后对于任意的 ``n``，假设 ``ih : motive n`` 并证明 ``motive (succ n)``。 ```lean # namespace Hidden @@ -1088,7 +1088,7 @@ a proof, it is really the induction principle in disguise. The like these. In this case, each can be used to reduce the proof to: --> -请注意，当``Nat.recOn``在证明中使用时，它实际上是变相的归纳原则。``rewrite``和``simp``策略在这样的证明中往往非常有效。在这种情况下，证明可以化简成： +请注意，当 ``Nat.recOn`` 在证明中使用时，它实际上是变相的归纳原则。``rewrite`` 和 ``simp`` 策略在这样的证明中往往非常有效。在这种情况下，证明可以化简成： ```lean # namespace Hidden @@ -1109,7 +1109,7 @@ The hardest part is figuring out which variable to do the induction on. Since ad ``k`` is a good guess, and once we make that choice the proof almost writes itself: --> -另一个例子，让我们证明加法结合律，``∀ m n k, m + n + k = m + (n + k)``。(我们定义的符号`+`是向左结合的，所以`m + n + k`实际上是`(m + n) + k`。) 最难的部分是确定在哪个变量上做归纳。由于加法是由第二个参数的递归定义的，``k``是一个很好的猜测，一旦我们做出这个选择，证明几乎是顺理成章的： +另一个例子，让我们证明加法结合律，``∀ m n k, m + n + k = m + (n + k)``。(我们定义的符号`+`是向左结合的，所以`m + n + k`实际上是`(m + n) + k`。) 最难的部分是确定在哪个变量上做归纳。由于加法是由第二个参数的递归定义的，``k`` 是一个很好的猜测，一旦我们做出这个选择，证明几乎是顺理成章的： ```lean # namespace Hidden @@ -1165,7 +1165,7 @@ At this point, we see that we need another supporting fact, namely, that ``succ You can prove this by induction on ``m``: --> -在这一点上，我们看到我们需要另一个事实，即``succ (n + m) = succ n + m``。你可以通过对``m``的归纳来证明这一点： +在这一点上，我们看到我们需要另一个事实，即 ``succ (n + m) = succ n + m``。你可以通过对 ``m`` 的归纳来证明这一点： ```lean open Nat @@ -1185,7 +1185,7 @@ theorem succ_add (n m : Nat) : succ n + m = succ (n + m) := You can then replace the ``sorry`` in the previous proof with ``succ_add``. Yet again, the proofs can be compressed: --> -然后你可以用``succ_add``代替前面证明中的``sorry``。然而，证明可以再次压缩： +然后你可以用 ``succ_add`` 代替前面证明中的 ``sorry``。然而，证明可以再次压缩： ```lean # namespace Hidden @@ -1216,7 +1216,7 @@ any type, ``α``, the type ``List α`` of lists of elements of ``α`` is defined in the library. --> -让我们再考虑一些归纳定义类型的例子。对于任何类型``α``，在库中定义了``α``的元素列表``List α``类型。 +让我们再考虑一些归纳定义类型的例子。对于任何类型 ``α``，在库中定义了 ``α`` 的元素列表 ``List α`` 类型。 ```lean # namespace Hidden @@ -1251,7 +1251,7 @@ and the remainder, ``t``, is known as the "tail." As an exercise, prove the following: --> -一个``α``类型的元素列表，要么是空列表``nil``，要么是一个元素``h : α``，后面是一个列表``t : List α``。第一个元素`h`，通常被称为列表的「头」，最后一个`t`，被称为「尾」。 +一个 ``α`` 类型的元素列表，要么是空列表 ``nil``，要么是一个元素 ``h : α``，后面是一个列表 ``t : List α``。第一个元素`h`，通常被称为列表的「头」，最后一个`t`，被称为「尾」。 作为一个练习，请证明以下内容： @@ -1287,7 +1287,7 @@ and prove that it behaves as expected (for example, ``length (append as bs) = le For another example, we can define the type of binary trees: --> -还可以尝试定义函数``length : {α : Type u} → List α → Nat``，返回一个列表的长度，并证明它的行为符合我们的期望（例如，``length (append as bs) = length as + length bs``）。 +还可以尝试定义函数 ``length : {α : Type u} → List α → Nat``，返回一个列表的长度，并证明它的行为符合我们的期望（例如，``length (append as bs) = length as + length bs``）。 另一个例子，我们可以定义二叉树的类型： @@ -1343,9 +1343,9 @@ applied to an element ``x`` in the local context. It then reduces the goal to cases in which ``x`` is replaced by each of the constructions. --> -归纳类型在Lean中有最根本的重要性，因此设计了一些方便使用的策略，这里讲几种。 +归纳类型在Lean 中有最根本的重要性，因此设计了一些方便使用的策略，这里讲几种。 -``cases``策略适用于归纳定义类型的元素，正如其名称所示：它根据每个可能的构造器分解元素。在其最基本的形式中，它被应用于局部环境中的元素`x`。然后，它将目标还原为``x``被每个构成体所取代的情况。 +``cases`` 策略适用于归纳定义类型的元素，正如其名称所示：它根据每个可能的构造子分解元素。在其最基本的形式中，它被应用于局部环境中的元素`x`。然后，它将目标还原为 ``x`` 被每个构成体所取代的情况。 ```lean example (p : Nat → Prop) (hz : p 0) (hs : ∀ n, p (Nat.succ n)) : ∀ n, p n := by @@ -1367,7 +1367,7 @@ below, notice that the hypothesis ``h : n ≠ 0`` becomes ``h : 0 ≠ 0`` in the first branch, and ``h : succ m ≠ 0`` in the second. --> -还有一些额外的修饰功能。首先，``cases``允许你使用``with``子句来选择每个选项的名称。例如在下一个例子中，我们为``succ``的参数选择`m`这个名字，这样第二个情况就指的是`succ m`。更重要的是，cases策略将检测局部环境中任何依赖于目标变量的项目。它将这些元素还原，进行拆分，并重新引入它们。在下面的例子中，注意假设`h : n ≠ 0`在第一个分支中变成`h : 0 ≠ 0`，在第二个分支中变成`h : succ m ≠ 0`。 +还有一些额外的修饰功能。首先，``cases`` 允许你使用 ``with`` 子句来选择每个选项的名称。例如在下一个例子中，我们为 ``succ`` 的参数选择`m`这个名字，这样第二个情况就指的是`succ m`。更重要的是，cases策略将检测局部环境中任何依赖于目标变量的项目。它将这些元素还原，进行拆分，并重新引入它们。在下面的例子中，注意假设`h : n ≠ 0`在第一个分支中变成`h : 0 ≠ 0`，在第二个分支中变成`h : succ m ≠ 0`。 ```lean open Nat @@ -1386,7 +1386,7 @@ example (n : Nat) (h : n ≠ 0) : succ (pred n) = n := by Notice that ``cases`` can be used to produce data as well as prove propositions. --> -``cases``可以用来产生数据，也可以用来证明命题。 +``cases`` 可以用来产生数据，也可以用来证明命题。 ```lean def f (n : Nat) : Nat := by @@ -1420,7 +1420,7 @@ example : f myTuple = 7 := Here is an example of multiple constructors with arguments. --> -下面是一个带有参数的多个构造器的例子。 +下面是一个带有参数的多个构造子的例子。 ```lean inductive Foo where @@ -1438,7 +1438,7 @@ The alternatives for each constructor don't need to be solved in the order the constructors were declared. --> -每个构造器的备选项不需要按照构造器的声明顺序来求解。 +每个构造子的备选项不需要按照构造子的声明顺序来求解。 ```lean # inductive Foo where @@ -1456,7 +1456,7 @@ Lean also provides a complementary ``case`` tactic, which allows you to focus on assign variable names. --> -`with`的语法对于编写结构化证明很方便。Lean还提供了一个补充的`case`策略，它允许你专注于目标分配变量名。 +`with`的语法对于编写结构化证明很方便。Lean 还提供了一个补充的`case`策略，它允许你专注于目标分配变量名。 ```lean # inductive Foo where @@ -1472,7 +1472,7 @@ def silly (x : Foo) : Nat := by The ``case`` tactic is clever, in that it will match the constructor to the appropriate goal. For example, we can fill the goals above in the opposite order: --> -``case``策略很聪明，它将把构造器与适当的目标相匹配。例如，我们可以按照相反的顺序填充上面的目标： +``case`` 策略很聪明，它将把构造子与适当的目标相匹配。例如，我们可以按照相反的顺序填充上面的目标： ```lean # inductive Foo where @@ -1491,7 +1491,7 @@ the expression, introduce the resulting universally quantified variable, and case on that. --> -你也可以使用``cases``伴随一个任意的表达式。假设该表达式出现在目标中，cases策略将概括该表达式，引入由此产生的全称变量，并对其进行处理。 +你也可以使用 ``cases`` 伴随一个任意的表达式。假设该表达式出现在目标中，cases策略将概括该表达式，引入由此产生的全称变量，并对其进行处理。 ```lean open Nat @@ -1509,7 +1509,7 @@ zero or the successor of some number." The result is functionally equivalent to the following: --> -可以认为这是在说「把``m + 3 * k``是零或者某个数字的后继的情况拆开」。其结果在功能上等同于以下： +可以认为这是在说「把 ``m + 3 * k`` 是零或者某个数字的后继的情况拆开」。其结果在功能上等同于以下： ```lean open Nat @@ -1535,9 +1535,9 @@ If the expression you case on does not appear in the goal, the the context. Here is an example: --> -注意，表达式``m + 3 * k``被``generalize``删除了；重要的只是它的形式是``0``还是``succ a``。这种形式的``cases``*不会*恢复任何同时提到方程中的表达式的假设（在本例中是`m + 3 * k`）。如果这样的术语出现在一个假设中，而你也想对其进行概括，你需要明确地恢复``revert``它。 +注意，表达式 ``m + 3 * k`` 被 ``generalize`` 删除了；重要的只是它的形式是 ``0`` 还是 ``succ a``。这种形式的 ``cases``*不会*恢复任何同时提到方程中的表达式的假设（在本例中是`m + 3 * k`）。如果这样的术语出现在一个假设中，而你也想对其进行概括，你需要明确地恢复 ``revert`` 它。 -如果你所涉及的表达式没有出现在目标中，``cases``策略使用``have``来把表达式的类型放到上下文中。下面是一个例子： +如果你所涉及的表达式没有出现在目标中，``cases`` 策略使用 ``have`` 来把表达式的类型放到上下文中。下面是一个例子： ```lean example (p : Prop) (m n : Nat) @@ -1555,7 +1555,7 @@ in the second we have the hypothesis ``hge : m ≥ n``. The proof above is functionally equivalent to the following: --> -定理``Nat.lt_or_ge m n``说``m < n ∨ m ≥ n``，很自然地认为上面的证明是在这两种情况下的分割。在第一个分支中，我们有假设``h₁ : m < n``，在第二个分支中，我们有假设``h₂ : m ≥ n``。上面的证明在功能上等同于以下： +定理 ``Nat.lt_or_ge m n`` 说 ``m < n ∨ m ≥ n``，很自然地认为上面的证明是在这两种情况下的分割。在第一个分支中，我们有假设 ``h₁ : m < n``，在第二个分支中，我们有假设 ``h₂ : m ≥ n``。上面的证明在功能上等同于以下： ```lean example (p : Prop) (m n : Nat) @@ -1574,7 +1574,7 @@ Here is another example, where we use the decidability of equality on the natural numbers to split on the cases ``m = n`` and ``m ≠ n``. --> -在前两行之后，我们有``h : m < n ∨ m ≥ n``作为假设，我们只需在此基础上做cases。 +在前两行之后，我们有 ``h : m < n ∨ m ≥ n`` 作为假设，我们只需在此基础上做cases。 下面是另一个例子，我们利用自然数相等的可判定性，对`m = n`和`m ≠ n`的情况进行拆分。 @@ -1600,9 +1600,9 @@ induction. The syntax is similar to that of ``cases``, except that the argument can only be a term in the local context. Here is an example: --> -如果你``open Classical``，你可以对任何命题使用排中律。但是使用[类型类](./type_classes.md)推理，Lean实际上可以找到相关的决策程序，这意味着你可以在可计算函数中使用情况拆分。 +如果你 ``open Classical``，你可以对任何命题使用排中律。但是使用[类型类](./type_classes.md)推理，Lean 实际上可以找到相关的决策程序，这意味着你可以在可计算函数中使用情况拆分。 -正如``cases``项可以用来进行分情况证明，``induction``项可以用来进行归纳证明。其语法与`cases`相似，只是参数只能是局部上下文中的一个项。下面是一个例子： +正如 ``cases`` 项可以用来进行分情况证明，``induction`` 项可以用来进行归纳证明。其语法与`cases`相似，只是参数只能是局部上下文中的一个项。下面是一个例子： ```lean # namespace Hidden @@ -1617,7 +1617,7 @@ theorem zero_add (n : Nat) : 0 + n = n := by As with ``cases``, we can use the ``case`` tactic instead of `with`. --> -和``cases``一样，我们可以使用``case``代替`with`。 +和 ``cases`` 一样，我们可以使用 ``case`` 代替`with`。 ```lean # namespace Hidden @@ -1728,7 +1728,7 @@ disjoint ranges. The ``injection`` tactic is designed to make use of this fact: --> -我们用最后一个策略来结束本节，这个策略旨在促进归纳类型的工作，即``injection``注入策略。归纳类型的元素是自由生成的，也就是说，构造器是注入式的，并且有不相交的作用范围。``injection``策略是为了利用这一事实： +我们用最后一个策略来结束本节，这个策略旨在促进归纳类型的工作，即 ``injection`` 注入策略。归纳类型的元素是自由生成的，也就是说，构造子是注入式的，并且有不相交的作用范围。``injection`` 策略是为了利用这一事实： ```lean open Nat @@ -1748,9 +1748,9 @@ The ``injection`` tactic also detects contradictions that arise when different c are set equal to one another, and uses them to close the goal. --> -该策略的第一个实例在上下文中加入了``h' : succ m = succ n``，第二个实例加入了``h'' : m = n``。 +该策略的第一个实例在上下文中加入了 ``h' : succ m = succ n``，第二个实例加入了 ``h'' : m = n``。 -``injection``策略还可以检测不同构造器被设置为相等时产生的矛盾，并使用它们来关闭目标。 +``injection`` 策略还可以检测不同构造子被设置为相等时产生的矛盾，并使用它们来关闭目标。 ```lean open Nat @@ -1769,7 +1769,7 @@ example (h : 7 = 4) : False := by As the second example shows, the ``contradiction`` tactic also detects contradictions of this form. --> -如第二个例子所示，``contradiction``策略也能检测出这种形式的矛盾。 +如第二个例子所示，``contradiction`` 策略也能检测出这种形式的矛盾。 -我们几乎已经完成了对Lean所接受的全部归纳定义的描述。到目前为止，你已经看到Lean允许你用任何数量的递归构造器引入归纳类型。事实上，一个归纳定义可以引入一个有索引的归纳类型的**族**（Family）。 +我们几乎已经完成了对Lean 所接受的全部归纳定义的描述。到目前为止，你已经看到Lean 允许你用任何数量的递归构造子引入归纳类型。事实上，一个归纳定义可以引入一个有索引的归纳类型的 **族（Family）** 。 归纳族是一个由以下形式的同时归纳定义的有索引的家族： @@ -1812,7 +1812,7 @@ definition of ``Vector α n``, the type of vectors of elements of ``α`` of length ``n``: --> -与普通的归纳定义不同，它构造了某个``Sort u``的元素，更一般的版本构造了一个函数``... → Sort u``，其中``...``表示一串参数类型，也称为**索引**。然后，每个构造器都会构造一个家族中某个成员的元素。一个例子是``Vector α n``的定义，它是长度为``n``的``α``元素的向量的类型： +与普通的归纳定义不同，它构造了某个 ``Sort u`` 的元素，更一般的版本构造了一个函数 ``... → Sort u``，其中 ``...`` 表示一串参数类型，也称为 **索引** 。然后，每个构造子都会构造一个家族中某个成员的元素。一个例子是 ``Vector α n`` 的定义，它是长度为 ``n`` 的 ``α`` 元素的向量的类型： ```lean # namespace Hidden @@ -1830,9 +1830,9 @@ element of one member of the family to build an element of another. A more exotic example is given by the definition of the equality type in Lean: --> -注意，``cons``构造器接收``Vector α n``的一个元素，并返回``Vector α (n+1)``的一个元素，从而使用家族中的一个成员的元素来构建另一个成员的元素。 +注意，``cons`` 构造子接收 ``Vector α n`` 的一个元素，并返回 ``Vector α (n+1)`` 的一个元素，从而使用家族中的一个成员的元素来构建另一个成员的元素。 -一个更奇特的例子是由Lean中相等类型的定义： +一个更奇特的例子是由Lean 中相等类型的定义： ```lean # namespace Hidden @@ -1852,7 +1852,7 @@ Note that ``Eq a a`` is the only inhabited type in the family of types ``Eq a x``. The elimination principle generated by Lean is as follows: --> -对于每个固定的``α : Sort u``和``a : α``，这个定义构造了一个``Eq a x``的类型类，由``x : α``索引。然而，只有一个构造器`refl`，它是`Eq a a`的一个元素，构造器后面的大括号告诉Lean要把`refl`的参数明确化。直观地说，在`x`是`a`的情况下，构建`Eq a x`证明的唯一方法是使用自反性。请注意，`Eq a a`是`Eq a x`这个类型家族中唯一的类型。由Lean产生的消去规则如下： +对于每个固定的 ``α : Sort u`` 和 ``a : α``，这个定义构造了一个 ``Eq a x`` 的类型类，由 ``x : α`` 索引。然而，只有一个构造子`refl`，它是`Eq a a`的一个元素，构造子后面的大括号告诉Lean 要把`refl`的参数明确化。直观地说，在`x`是`a`的情况下，构建`Eq a x`证明的唯一方法是使用自反性。请注意，`Eq a a`是`Eq a x`这个类型家族中唯一的类型。由Lean 产生的消去规则如下： ```lean universe u v @@ -1869,7 +1869,7 @@ definition of equality is atypical, however; see the discussion in [Section Axio The recursor ``Eq.rec`` is also used to define substitution: --> -一个显著的事实是，所有关于相等的基本公理都来自构造器`refl`和消去器`Eq.rec`。然而，相等的定义是不典型的，见[公理化细节](#公理化细节)一节的讨论。 +一个显著的事实是，所有关于相等的基本公理都来自构造子`refl`和消去器`Eq.rec`。然而，相等的定义是不典型的，见[公理化细节](#公理化细节)一节的讨论。 递归器`Eq.rec`也被用来定义代换： @@ -1899,7 +1899,7 @@ Actually, Lean compiles the `match` expressions using a definition based on `Eq.rec`. --> -实际上，Lean使用基于`Eq.rec`的定义来编译`match`表达式。 +实际上，Lean 使用基于`Eq.rec`的定义来编译`match`表达式。 ```lean # namespace Hidden @@ -1927,7 +1927,7 @@ In the following example, we prove ``symm`` and leave as exercises the theorems 使用递归器或`match`与`h₁ : a = b`，我们可以假设`a`和`b`相同，在这种情况下，`p b`和`p a`相同。 -证明``Eq``的对称和传递性并不难。在下面的例子中，我们证明`symm`，并留下`trans`和`congr` （congruence）定理作为练习。 +证明 ``Eq`` 的对称和传递性并不难。在下面的例子中，我们证明`symm`，并留下`trans`和`congr` （congruence）定理作为练习。 ```lean # namespace Hidden @@ -1950,7 +1950,7 @@ inductive definitions, for example, the principles of supported by Lean. --> -在类型论文献中，有对归纳定义的进一步推广，例如，「归纳-递归」和「归纳-归纳」的原则。这些东西Lean暂不支持。 +在类型论文献中，有对归纳定义的进一步推广，例如，「归纳-递归」和「归纳-归纳」的原则。这些东西Lean 暂不支持。 -其中`a`是一列数据类型的参量，`b`是一列构造器的参数，`p[a, b]`是索引，用于确定构造所处的归纳族的元素。（请注意，这种描述有些误导，因为构造器的参数可以以任何顺序出现，只要依赖关系是合理的）。对``C``的宇宙层级的约束分为两种情况，取决于归纳类型是否被指定落在``Prop``（即``Sort 0``）。 +其中`a`是一列数据类型的参量，`b`是一列构造子的参数，`p[a, b]`是索引，用于确定构造所处的归纳族的元素。（请注意，这种描述有些误导，因为构造子的参数可以以任何顺序出现，只要依赖关系是合理的）。对 ``C`` 的宇宙层级的约束分为两种情况，取决于归纳类型是否被指定落在 ``Prop``（即 ``Sort 0``）。 -我们首先考虑归纳类型*不*指定落在``Prop``的情况。那么宇宙等级`u'`被限制为满足以下条件： +我们首先考虑归纳类型*不*指定落在 ``Prop`` 的情况。那么宇宙等级`u'`被限制为满足以下条件： -> 对于上面的每个构造器`c`，以及序列`β[a]`中的每个`βk[a]`，如果`βk[a] : Sort v`，我们有`u`≥`v`。 +> 对于上面的每个构造子`c`，以及序列`β[a]`中的每个`βk[a]`，如果`βk[a] : Sort v`，我们有`u`≥`v`。 -换句话说，宇宙等级``u``被要求至少与代表构造器参数的每个类型的宇宙等级一样大。 +换句话说，宇宙等级 ``u`` 被要求至少与代表构造子参数的每个类型的宇宙等级一样大。 -当归纳类型被指定落在``Prop``中时，对构造器参数的宇宙等级没有任何限制。但是这些宇宙等级对消去规则有影响。一般来说，对于``Prop``中的归纳类型，消去规则的motive被要求在``Prop``中。 +当归纳类型被指定落在 ``Prop`` 中时，对构造子参数的宇宙等级没有任何限制。但是这些宇宙等级对消去规则有影响。一般来说，对于 ``Prop`` 中的归纳类型，消去规则的motive被要求在 ``Prop`` 中。 -这最后一条规则有一个例外：当只有一个构造器，并且每个构造器参数都在`Prop`中或者是一个索引时，我们可以从一个归纳定义的`Prop`中消除到一个任意的`Sort`。直观的说，在这种情况下，消除并不利用任何信息，而这些信息并不是由参数类型被栖息这一简单的事实所提供的。这种特殊情况被称为*单子消除*（singleton elimination）。 +这最后一条规则有一个例外：当只有一个构造子，并且每个构造子参数都在`Prop`中或者是一个索引时，我们可以从一个归纳定义的`Prop`中消除到一个任意的`Sort`。直观的说，在这种情况下，消除并不利用任何信息，而这些信息并不是由参数类型被栖息这一简单的事实所提供的。这种特殊情况被称为*单子消除*（singleton elimination）。 -我们已经在`Eq.rec`的应用中看到了单子消除的作用，这是归纳定义的相等类型的消去器。我们可以使用一个元素``h : Eq a b``来将一个元素``t' : p a``转换为``p b``，即使``p a``和``p b``是任意类型，因为转换并不产生新的数据；它只是重新解释了我们已经有的数据。单子消除法也用于异质等价和良基的递归，这将在[归纳和递归](./induction_and_recursion.md)一章中讨论。 +我们已经在`Eq.rec`的应用中看到了单子消除的作用，这是归纳定义的相等类型的消去器。我们可以使用一个元素 ``h : Eq a b`` 来将一个元素 ``t' : p a`` 转换为 ``p b``，即使 ``p a`` 和 ``p b`` 是任意类型，因为转换并不产生新的数据；它只是重新解释了我们已经有的数据。单子消除法也用于异质等价和良基的递归，这将在[归纳和递归](./induction_and_recursion.md)一章中讨论。 -我们现在考虑两个经常有用的归纳类型的推广，Lean通过「编译」它们来支持上述更原始的归纳类型种类。换句话说，Lean解析了更一般的定义，在此基础上定义了辅助的归纳类型，然后使用辅助类型来定义我们真正想要的类型。下一章将介绍Lean的方程编译器，它需要有效地利用这些类型。尽管如此，在这里描述这些声明还是有意义的，因为它们是普通归纳定义的直接变形。 +我们现在考虑两个经常有用的归纳类型的推广，Lean 通过「编译」它们来支持上述更原始的归纳类型种类。换句话说，Lean 解析了更一般的定义，在此基础上定义了辅助的归纳类型，然后使用辅助类型来定义我们真正想要的类型。下一章将介绍Lean 的方程编译器，它需要有效地利用这些类型。尽管如此，在这里描述这些声明还是有意义的，因为它们是普通归纳定义的直接变形。 -首先，Lean支持**相互定义**的归纳类型。这个想法是，我们可以同时定义两个（或更多）归纳类型，其中每个类型都指代其他类型。 +首先，Lean 支持 **相互定义** 的归纳类型。这个想法是，我们可以同时定义两个（或更多）归纳类型，其中每个类型都指代其他类型。 ```lean mutual @@ -2136,11 +2136,11 @@ results back and forth along this isomorphism is tedious. In fact, Lean allows us to define the inductive type we really want: --> -有了这个定义，我们可以通过给出一个``α``的元素和一个子树列表（可能是空的）来构造``Tree α``的元素。子树列表由`TreeList α`类型表示，它被定义为空列表`nil`，或者是一棵树的`cons`和`TreeList α`的一个元素。 +有了这个定义，我们可以通过给出一个 ``α`` 的元素和一个子树列表（可能是空的）来构造 ``Tree α`` 的元素。子树列表由`TreeList α`类型表示，它被定义为空列表`nil`，或者是一棵树的`cons`和`TreeList α`的一个元素。 -然而，这个定义在工作中是不方便的。如果子树的列表是由``List (Tree α)``类型给出的，那就更好了，尤其是Lean的库中包含了一些处理列表的函数和定理。我们可以证明``TreeList α``类型与``List (Tree α)``是*同构*的，但是沿着这个同构关系来回翻译结果是很乏味的。 +然而，这个定义在工作中是不方便的。如果子树的列表是由 ``List (Tree α)`` 类型给出的，那就更好了，尤其是Lean 的库中包含了一些处理列表的函数和定理。我们可以证明 ``TreeList α`` 类型与 ``List (Tree α)`` 是*同构*的，但是沿着这个同构关系来回翻译结果是很乏味的。 -事实上，Lean允许我们定义我们真正想要的归纳类型： +事实上，Lean 允许我们定义我们真正想要的归纳类型： ```lean inductive Tree (α : Type u) where @@ -2157,7 +2157,7 @@ isomorphism between ``TreeList α`` and ``List (Tree α)`` in its kernel, and defines the constructors for ``Tree`` in terms of the isomorphism. --> -这就是所谓的**嵌套**归纳类型。它不属于上一节给出的归纳类型的严格规范，因为`Tree`不是严格意义上出现在`mk`的参数中，而是嵌套在`List`类型构造器中。然后Lean在其内核中自动建立了``TreeList α``和``List (Tree α)``之间的同构关系，并根据同构关系定义了``Tree``的构造器。 +这就是所谓的 **嵌套** 归纳类型。它不属于上一节给出的归纳类型的严格规范，因为`Tree`不是严格意义上出现在`mk`的参数中，而是嵌套在`List`类型构造子中。然后Lean 在其内核中自动建立了 ``TreeList α`` 和 ``List (Tree α)`` 之间的同构关系，并根据同构关系定义了 ``Tree`` 的构造子。 -Lean的前端的目标是解释用户的输入，构建形式化的表达式，并检查它们是否形式良好和类型正确。Lean还支持使用各种编辑器，这些编辑器提供持续的检查和反馈。更多信息可以在Lean[文档](https://lean-lang.org/documentation/)上找到。 +Lean 的前端的目标是解释用户的输入，构建形式化的表达式，并检查它们是否形式良好和类型正确。Lean 还支持使用各种编辑器，这些编辑器提供持续的检查和反馈。更多信息可以在Lean[文档](https://lean-lang.org/documentation/)上找到。 -Lean的标准库中的定义和定理分布在多个文件中。用户也可能希望使用额外的库，或在多个文件中开发自己的项目。当 Lean 启动时，它会自动导入库中 `Init` 文件夹的内容，其中包括一些基本定义和结构。因此，我们在这里介绍的大多数例子都是「开箱即用」的。 +Lean 的标准库中的定义和定理分布在多个文件中。用户也可能希望使用额外的库，或在多个文件中开发自己的项目。当 Lean 启动时，它会自动导入库中 `Init` 文件夹的内容，其中包括一些基本定义和结构。因此，我们在这里介绍的大多数例子都是「开箱即用」的。 然而，如果你想使用其他文件，需要通过文件开头的`import'语句手动导入。命令 @@ -74,7 +74,7 @@ Importing is transitive. In other words, if you import ``Foo`` and ``Foo`` impor then you also have access to the contents of ``Bar``, and do not need to import it explicitly. --> -导入文件 ``Bar/Baz/Blah.olean``，其中的描述是相对于Lean**搜索路径**解释的。关于如何确定搜索路径的信息可以在[文档](https://lean-lang.org/documentation/)中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。 +导入文件 ``Bar/Baz/Blah.olean``，其中的描述是相对于 Lean **搜索路径** 解释的。关于如何确定搜索路径的信息可以在[文档](https://lean-lang.org/documentation/)中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。 导入是传递性的。换句话说，如果你导入了 ``Foo``，并且 ``Foo`` 导入了 ``Bar``，那么你也可以访问 ``Bar`` 的内容，而不需要明确导入它。 @@ -96,7 +96,7 @@ necessary. Remember that the point of the `variable` command is to declare variables for use in theorems, as in the following example: --> -Lean提供了各种分段机制来帮助构造理论。你在[变量和小节](./dependent_type_theory.md#变量和小节)中看到，``section`` 命令不仅可以将理论中的元素组合在一起，还可以在必要时声明变量，作为定理和定义的参数插入。请记住，`variable` 命令的意义在于声明变量，以便在定理中使用，如下面的例子： +Lean 提供了各种分段机制来帮助构造理论。你在[变量和小节](./dependent_type_theory.md#变量和小节)中看到，``section`` 命令不仅可以将理论中的元素组合在一起，还可以在必要时声明变量，作为定理和定义的参数插入。请记住，`variable` 命令的意义在于声明变量，以便在定理中使用，如下面的例子： ```lean section @@ -130,7 +130,7 @@ Note that ``double`` does *not* have ``y`` as argument. Variables are only included in declarations where they are actually used. --> -``double`` 的定义不需要声明 ``x`` 作为参数；Lean检测到这种依赖关系并自动插入。同样，Lean检测到 ``x`` 在 ``t1`` 和 ``t2`` 中的出现，也会自动插入。注意，double**没有**``y`` 作为参数。变量只包括在实际使用的声明中。 +``double`` 的定义不需要声明 ``x`` 作为参数；Lean 检测到这种依赖关系并自动插入。同样，Lean 检测到 ``x`` 在 ``t1`` 和 ``t2`` 中的出现，也会自动插入。注意，double **没有** ``y`` 作为参数。变量只包括在实际使用的声明中。 -在 Lean 中，标识符是由层次化的*名称*给出的，如 ``Foo.Bar.baz``。我们在[命名空间](./dependent_type_theory.md#命名空间)一节中看到，Lean提供了处理分层名称的机制。命令 ``namespace foo`` 导致 ``foo`` 被添加到每个定义和定理的名称中，直到遇到 ``end foo``。命令 ``open foo`` 然后为以 `foo` 开头的定义和定理创建临时的**别名**。 +在 Lean 中，标识符是由层次化的*名称*给出的，如 ``Foo.Bar.baz``。我们在[命名空间](./dependent_type_theory.md#命名空间)一节中看到，Lean 提供了处理分层名称的机制。命令 ``namespace foo`` 导致 ``foo`` 被添加到每个定义和定理的名称中，直到遇到 ``end foo``。命令 ``open foo`` 然后为以 `foo` 开头的定义和定理创建临时的 **别名** 。 ```lean namespace Foo @@ -194,7 +194,7 @@ by giving the full name. To that end, the string ``_root_`` is an explicit description of the empty prefix. --> -尽管定理和定义的名称必须是唯一的，但标识它们的别名却不是。当我们打开一个命名空间时，一个标识符可能是模糊的。Lean试图使用类型信息来消除上下文中的含义，但你总是可以通过给出全名来消除歧义。为此，字符串 ``_root_`` 是对空前缀的明确表述。 +尽管定理和定义的名称必须是唯一的，但标识它们的别名却不是。当我们打开一个命名空间时，一个标识符可能是模糊的。Lean 试图使用类型信息来消除上下文中的含义，但你总是可以通过给出全名来消除歧义。为此，字符串 ``_root_`` 是对空前缀的明确表述。 ```lean def String.add (a b : String) : String := @@ -266,7 +266,7 @@ open Nat hiding succ gcd creates aliases for everything in the ``Nat`` namespace *except* the identifiers listed. --> -给 ``Nat`` 命名空间中**除了**被列出的标识符都创建了别名。命令 +给 ``Nat`` 命名空间中 **除了** 被列出的标识符都创建了别名。命令 ```lean open Nat renaming mul → times, add → plus @@ -442,7 +442,7 @@ their scope is always restricted to the current section or current file. --> -在下面的[符号](#符号)一节中，我们将讨论 Lean 定义符号的机制，并看到它们也支持 ``local`` 修饰符。然而，在[设置选项](#设置选项)一节中，我们将讨论 Lean 设置选项的机制，它并**不**遵循这种模式：选项**只能**在局部设置，也就是说，它们的范围总是限制在当前小节或当前文件中。 +在下面的[符号](#符号)一节中，我们将讨论 Lean 定义符号的机制，并看到它们也支持 ``local`` 修饰符。然而，在[设置选项](#设置选项)一节中，我们将讨论 Lean 设置选项的机制，它并 **不** 遵循这种模式：选项 **只能** 在局部设置，也就是说，它们的范围总是限制在当前小节或当前文件中。 -Lean中的标识符可以包括任何字母数字字符，包括希腊字母（除了∀、Σ和λ，它们在依值类型论中有特殊的含义）。它们还可以包括下标，可以通过输入 ``\_``，然后再输入所需的下标字符。 +Lean 中的标识符可以包括任何字母数字字符，包括希腊字母（除了∀、Σ和λ，它们在依值类型论中有特殊的含义）。它们还可以包括下标，可以通过输入 ``\_``，然后再输入所需的下标字符。 -Lean的解析器是可扩展的，也就是说，我们可以定义新的符号。 +Lean 的解析器是可扩展的，也就是说，我们可以定义新的符号。 -Lean的语法可以由用户在各个层面进行扩展和定制，从基本的「mixfix」符号到自定义的繁饰器。事实上，所有内置的语法都是使用对用户开放的相同机制和 API 进行解析和处理的。 在本节中，我们将描述和解释各种扩展点。 +Lean 的语法可以由用户在各个层面进行扩展和定制，从基本的「mixfix」符号到自定义的繁饰器。事实上，所有内置的语法都是使用对用户开放的相同机制和 API 进行解析和处理的。 在本节中，我们将描述和解释各种扩展点。 -虽然在编程语言中引入新的符号是一个相对罕见的功能，有时甚至因为它有可能使代码变得模糊不清而被人诟病，但它是形式化的一个宝贵工具，可以在代码中简洁地表达各自领域的既定惯例和符号。 除了基本的符号之外，Lean的能力是将普通的样板代码分解成（良好的）宏，并嵌入整个定制的特定领域语言（DSL，domain specific language），对子问题进行高效和可读的文本编码，这对程序员和证明工程师都有很大的好处。 +虽然在编程语言中引入新的符号是一个相对罕见的功能，有时甚至因为它有可能使代码变得模糊不清而被人诟病，但它是形式化的一个宝贵工具，可以在代码中简洁地表达各自领域的既定惯例和符号。 除了基本的符号之外，Lean 的能力是将普通的样板代码分解成（良好的）宏，并嵌入整个定制的特定领域语言（DSL，domain specific language），对子问题进行高效和可读的文本编码，这对程序员和证明工程师都有很大的好处。 -事实证明，第一个代码块中的所有命令实际上都是命令**宏**，翻译成更通用的 `notation` 命令。我们将在下面学习如何编写这种宏。 `notation` 命令不接受单一的记号，而是接受一个混合的记号序列和有优先级的命名项占位符，这些占位符可以在`=>`的右侧被引用，并将被在该位置解析的相应项所取代。 优先级为 `p` 的占位符在该处只接受优先级至少为 `p` 的记号。因此，字符串`a + b + c`不能被解析为等同于`a + (b + c)`，因为 `infixl` 符号的右侧操作数的优先级比该符号本身大。 相反，`infixr` 重用了符号右侧操作数的优先级，所以`a ^ b ^ c` *可以*被解析为`a ^ (b ^ c)`。 注意，如果我们直接使用 `notation` 来引入一个 infix 符号，如 +事实证明，第一个代码块中的所有命令实际上都是命令 **宏** ，翻译成更通用的 `notation` 命令。我们将在下面学习如何编写这种宏。 `notation` 命令不接受单一的记号，而是接受一个混合的记号序列和有优先级的命名项占位符，这些占位符可以在`=>`的右侧被引用，并将被在该位置解析的相应项所取代。 优先级为 `p` 的占位符在该处只接受优先级至少为 `p` 的记号。因此，字符串`a + b + c`不能被解析为等同于`a + (b + c)`，因为 `infixl` 符号的右侧操作数的优先级比该符号本身大。 相反，`infixr` 重用了符号右侧操作数的优先级，所以`a ^ b ^ c` *可以*被解析为`a ^ (b ^ c)`。 注意，如果我们直接使用 `notation` 来引入一个 infix 符号，如 ```lean # set_option quotPrecheck false @@ -718,7 +718,7 @@ As mentioned above, the `notation` command allows us to define arbitrary *mixfix* syntax freely mixing tokens and placeholders. --> -在上文没有充分确定结合规则的情况下，Lean的解析器将默认为右结合。 更确切地说，Lean的解析器在存在模糊语法的情况下遵循一个局部的*最长解析*规则：当解析`a ~`中`a ~ b ~ c`的右侧时，它将继续尽可能长的解析（在当前的上下文允许的情况下），不在 `b` 之后停止，而是同时解析`~ c`。因此该术语等同于`a ~ (b ~ c)`。 +在上文没有充分确定结合规则的情况下，Lean 的解析器将默认为右结合。 更确切地说，Lean 的解析器在存在模糊语法的情况下遵循一个局部的*最长解析*规则：当解析`a ~`中`a ~ b ~ c`的右侧时，它将继续尽可能长的解析（在当前的上下文允许的情况下），不在 `b` 之后停止，而是同时解析`~ c`。因此该术语等同于`a ~ (b ~ c)`。 如上所述，`notation` 命令允许我们定义任意的*mixfix*语法，自由地混合记号和占位符。 @@ -766,7 +766,7 @@ any natural number as an integer, when needed. Lean has mechanisms to detect and insert *coercions* of this sort. --> -在 Lean 中，自然数的类型 ``Nat``，与整数的类型 ``Int`` 不同。但是有一个函数 ``Int.ofNat`` 将自然数嵌入整数中，这意味着我们可以在需要时将任何自然数视为整数。Lean有机制来检测和插入这种**强制转换**。 +在 Lean 中，自然数的类型 ``Nat``，与整数的类型 ``Int`` 不同。但是有一个函数 ``Int.ofNat`` 将自然数嵌入整数中，这意味着我们可以在需要时将任何自然数视为整数。Lean 有机制来检测和插入这种 **强制转换** 。 ```lean variable (m n : Nat) @@ -798,7 +798,7 @@ prints the type of the symbol, and its definition. If it is a constant or an axiom, Lean indicates that fact, and shows the type. --> -有很多方法可以让你查询 Lean 的当前状态以及当前上下文中可用的对象和定理的信息。你已经看到了两个最常见的方法，`#check`和`#eval`。请记住，`#check`经常与`@`操作符一起使用，它使定理或定义的所有参数显式化。此外，你可以使用`#print`命令来获得任何标识符的信息。如果标识符表示一个定义或定理，Lean会打印出符号的类型，以及它的定义。如果它是一个常数或公理，Lean会指出它并显示其类型。 +有很多方法可以让你查询 Lean 的当前状态以及当前上下文中可用的对象和定理的信息。你已经看到了两个最常见的方法，`#check`和`#eval`。请记住，`#check`经常与`@`操作符一起使用，它使定理或定义的所有参数显式化。此外，你可以使用`#print`命令来获得任何标识符的信息。如果标识符表示一个定义或定理，Lean 会打印出符号的类型，以及它的定义。如果它是一个常数或公理，Lean 会指出它并显示其类型。 -Lean维护着一些内部变量，用户可以通过设置这些变量来控制其行为。语法如下： +Lean 维护着一些内部变量，用户可以通过设置这些变量来控制其行为。语法如下： ``` set_option @@ -869,7 +869,7 @@ set_option One very useful family of options controls the way Lean's *pretty- printer* displays terms. The following options take an input of true or false: --> -有一系列非常有用的选项可以控制 Lean 的**美观打印**显示项的方式。下列选项的输入值为真或假： +有一系列非常有用的选项可以控制 Lean 的 **美观打印** 显示项的方式。下列选项的输入值为真或假： ``` pp.explicit : display implicit arguments @@ -902,7 +902,7 @@ error message. Too much information can be overwhelming, though, and Lean's defaults are generally sufficient for ordinary interactions. --> -命令 ``set_option pp.all true`` 一次性执行这些设置，而 ``set_option pp.all false`` 则恢复到之前的值。当你调试一个证明，或试图理解一个神秘的错误信息时，漂亮地打印额外的信息往往是非常有用的。不过太多的信息可能会让人不知所措，Lean的默认值一般来说对普通的交互是足够的。 +命令 ``set_option pp.all true`` 一次性执行这些设置，而 ``set_option pp.all false`` 则恢复到之前的值。当你调试一个证明，或试图理解一个神秘的错误信息时，漂亮地打印额外的信息往往是非常有用的。不过太多的信息可能会让人不知所措，Lean 的默认值一般来说对普通的交互是足够的。 -Lean中的标识符可以被组织到分层的命名空间中。例如，命名空间 ``Nat`` 中名为 ``le_of_succ_le_succ`` 的定理有全称 ``Nat.le_of_succ_le_succ``，但较短的名称可由命令 ``open Nat`` 提供（对于未标记为 `protected` 的名称）。我们将在[归纳类型](./inductive_types.md)和[结构体和记录](./structures_and_records.md)中看到，在 Lean 中定义结构体和归纳数据类型会产生相关操作，这些操作存储在与被定义类型同名的命名空间。例如，乘积类型带有以下操作： +Lean 中的标识符可以被组织到分层的命名空间中。例如，命名空间 ``Nat`` 中名为 ``le_of_succ_le_succ`` 的定理有全称 ``Nat.le_of_succ_le_succ``，但较短的名称可由命令 ``open Nat`` 提供（对于未标记为 `protected` 的名称）。我们将在[归纳类型](./inductive_types.md)和[结构体和记录](./structures_and_records.md)中看到，在 Lean 中定义结构体和归纳数据类型会产生相关操作，这些操作存储在与被定义类型同名的命名空间。例如，乘积类型带有以下操作： ```lean #check @Prod.mk @@ -1095,7 +1095,7 @@ any unbound identifier is automatically added as an implicit argument *if* it is greek letter. With this feature we can write `compose` as --> -Lean 4支持一个名为**自动约束隐参数**的新特性。它使诸如 `compose` 这样的函数在编写时更加方便。当 Lean 处理一个声明的头时，**如果**它是一个小写字母或希腊字母，任何未约束的标识符都会被自动添加为隐式参数。有了这个特性，我们可以把 `compose` 写成 +Lean 4支持一个名为 **自动约束隐参数** 的新特性。它使诸如 `compose` 这样的函数在编写时更加方便。当 Lean 处理一个声明的头时， **如果** 它是一个小写字母或希腊字母，任何未约束的标识符都会被自动添加为隐式参数。有了这个特性，我们可以把 `compose` 写成 ```lean def compose (g : β → γ) (f : α → β) (x : α) : γ := @@ -1113,7 +1113,7 @@ we realize some users may feel uncomfortable with it. Thus, you can disable it u the command `set_option autoImplicit false`. --> -请注意，Lean使用 `Sort` 而不是 `Type` 推断出了一个更通用的类型。 +请注意，Lean 使用 `Sort` 而不是 `Type` 推断出了一个更通用的类型。 虽然我们很喜欢这个功能，并且在实现 Lean 时广泛使用，但我们意识到有些用户可能会对它感到不舒服。因此，你可以使用`set_option autoBoundImplicitLocal false`命令将其禁用。 diff --git a/introduction.md b/introduction.md index 4078c02..e8031ac 100644 --- a/introduction.md +++ b/introduction.md @@ -23,7 +23,11 @@ lengthy computation, in which case verifying the truth of the theorem requires v it is supposed to do. --> -**形式验证**（Formal verification）是指使用逻辑和计算方法来验证用精确的数学术语表达的命题。这包括普通的数学定理，以及硬件或软件、网络协议、机械和混合系统中的形式命题。在实践中，验证数学命题和验证系统的正确性之间很类似：形式验证用数学术语描述硬件和软件系统，在此基础上验证其命题的正确性，这就像定理证明的过程。相反，一个数学定理的证明可能需要冗长的计算，在这种情况下，验证定理的真实性需要验证计算过程是否出错。 + **形式验证（Formal Verification）** 是指使用逻辑和计算方法来验证用精确的数学术语表达的命题。 +这包括普通的数学定理，以及硬件或软件、网络协议、机械和混合系统中的形式命题。 +在实践中，验证数学命题和验证系统的正确性之间很类似：形式验证用数学术语描述硬件和软件系统， +在此基础上验证其命题的正确性，这就像定理证明的过程。相反，一个数学定理的证明可能需要冗长的计算， +在这种情况下，验证定理的真实性需要验证计算过程是否出错。 -二十世纪的逻辑学发展表明，绝大多数传统证明方法可以化为若干基础系统中的一小套公理和规则。有了这种简化，计算机能以两种方式帮助建立命题：1）它可以帮助寻找一个证明，2）可以帮助验证一个所谓的证明是正确的。 +二十世纪的逻辑学发展表明，绝大多数传统证明方法可以化为若干基础系统中的一小套公理和规则。 +有了这种简化，计算机能以两种方式帮助建立命题：1）它可以帮助寻找一个证明， +2）可以帮助验证一个所谓的证明是正确的。 -**自动定理证明**（Automated theorem proving）着眼于「寻找」证明。归结（Resolution）定理证明器、表格法（tableau）定理证明器、快速可满足性求解器（Fast satisfiability solvers）等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法；还有些系统为特定的语言和问题提供搜索和决策程序，例如整数或实数上的线性或非线性表达式；像SMT（Satisfiability modulo theories）这样的架构将通用的搜索方法与特定领域的程序相结合；计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段，这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。 + **自动定理证明（Automated theorem proving）** 着眼于「寻找」证明。归结（Resolution）定理证明器、 + **表格法（tableau）** 定理证明器、 **快速可满足性求解器（Fast satisfiability solvers）** +等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法； +还有些系统为特定的语言和问题提供搜索和决策程序， +例如整数或实数上的线性或非线性表达式；像 **SMT（Satisfiability modulo theories）** +这样的架构将通用的搜索方法与特定领域的程序相结合； +计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段， +这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。 -自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有bug，而且很难保证它们所提供的结果是正确的。相比之下，**交互式定理证明器**（Interactive theorem proving）侧重于「验证」证明，要求每个命题都有合适的公理基础的证明来支持。这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明，一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的「证明对象」，可以传给其他系统并独立检查。构建这样的证明通常需要用户更多的输入和交互，但它可以让你获得更深入、更复杂的证明。 +自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有 bug， +而且很难保证它们所提供的结果是正确的。相比之下， **交互式定理证明器（Interactive theorem proving）** +侧重于「验证」证明，要求每个命题都有合适的公理基础的证明来支持。 +这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明， +一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的「证明对象」， +可以传给其他系统并独立检查。构建这样的证明通常需要用户更多的输入和交互， +但它可以让你获得更深入、更复杂的证明。 -**Lean 定理证明器**旨在融合交互式和自动定理证明，它将自动化工具和方法置于一个支持用户交互和构建完整公理化证明的框架中。它的目标是支持数学推理和复杂系统的推理，并验证这两个领域的命题。 + **Lean 定理证明器** 旨在融合交互式和自动定理证明， +它将自动化工具和方法置于一个支持用户交互和构建完整公理化证明的框架中。 +它的目标是支持数学推理和复杂系统的推理，并验证这两个领域的命题。 -Lean的底层逻辑有一个计算的解释，与此同时 Lean 可以被视为一种编程语言。更重要的是，它可以被看作是一个编写具有精确语义的程序的系统，以及对程序所表示的计算功能进行推理。Lean中也有机制使它能够作为它自己的**元编程语言**，这意味着你可以使用 Lean 本身实现自动化和扩展 Lean 的功能。Lean的这些方面将在本教程的配套教程[Lean 4函数式编程](https://www.leanprover.cn/fp-lean-zh/)中进行探讨，本书只介绍计算方面。 +Lean 的底层逻辑有一个计算的解释，与此同时 Lean 可以被视为一种编程语言。 +更重要的是，它可以被看作是一个编写具有精确语义的程序的系统， +以及对程序所表示的计算功能进行推理。Lean 中也有机制使它能够作为它自己的 **元编程语言** ， +这意味着你可以使用 Lean 本身实现自动化和扩展 Lean 的功能。 +Lean 的这些方面将在本教程的配套教程 +[Lean 4函数式编程](https://www.leanprover.cn/fp-lean-zh/)中进行探讨，本书只介绍计算方面。 -*Lean* 项目由微软 Redmond 研究院的Leonardo de Moura在2013年发起，这是个长期项目，自动化方法的潜力会在未来逐步被挖掘。Lean是在[Apache 2.0 license](LICENSE)下发布的，这是一个允许他人自由使用和扩展代码和数学库的许可性开源许可证。 +*Lean* 项目由微软 Redmond 研究院的 Leonardo de Moura 在 2013 年发起，这是个长期项目， +自动化方法的潜力会在未来逐步被挖掘。Lean 是在 [Apache 2.0 许可协议](LICENSE) 下发布的， +这是一个允许他人自由使用和扩展代码和数学库的许可性开源许可证。 -通常有两种办法来运行Lean。第一个是[网页版本](https://live.lean-lang.org/)：由 Javascript 编写，包含标准定义和定理库，编辑器会下载到你的浏览器上运行。这是个方便快捷的办法。 +通常有两种办法来运行Lean。第一个是[网页版本](https://live.lean-lang.org/)： +由 JavaScript 编写，包含标准定义和定理库，编辑器会下载到你的浏览器上运行。 +这是个方便快捷的办法。 -第二种是本地版本：本地版本远快于网页版本，并且非常灵活。Visual Studio Code和 Emacs 扩展模块给编写和调试证明提供了有力支撑，因此更适合正式使用。源代码和安装方法见[https://github.com/leanprover/lean4/](https://github.com/leanprover/lean4/). +第二种是本地版本：本地版本远快于网页版本，并且非常灵活。Visual Studio Code +和 Emacs 扩展模块给编写和调试证明提供了有力支撑，因此更适合正式使用。 +源代码和安装方法见[https://github.com/leanprover/lean4/](https://github.com/leanprover/lean4/). 本教程介绍的是 Lean 的当前版本：Lean 4。 @@ -128,7 +160,7 @@ mathematical assertions in dependent type theory, but it also can be used as a l --> -本书的目的是教你在 Lean 中编写和验证证明，并且不太需要针对 Lean 的基础知识。首先，你将学习 Lean 所基于的逻辑系统，它是**依值类型论**（Dependent type theory）的一个版本，足以证明几乎所有传统的数学定理，并且有足够的表达能力自然地表示数学定理。更具体地说，Lean是基于具有归纳类型（Inductive type）的构造演算（Calculus of Construction）系统的类型论版本。Lean不仅可以定义数学对象和表达依值类型论的数学断言，而且还可以作为一种语言来编写证明。 +本书的目的是教你在 Lean 中编写和验证证明，并且不太需要针对 Lean 的基础知识。首先，你将学习 Lean 所基于的逻辑系统，它是 **依值类型论（Dependent type theory）** 的一个版本，足以证明几乎所有传统的数学定理，并且有足够的表达能力自然地表示数学定理。更具体地说，Lean 是基于具有归纳类型（Inductive type）的构造演算（Calculus of Construction）系统的类型论版本。Lean 不仅可以定义数学对象和表达依值类型论的数学断言，而且还可以作为一种语言来编写证明。 -由于完全深入细节的公理证明十分复杂，定理证明的难点在于让计算机尽可能多地填补证明细节。你将通过[依值类型论](dependent_type_theory.md)语言来学习各种方法实现自动证明，例如项重写，以及 Lean 中的项和表达式的自动简化方法。同样，**繁饰**（Elaboration）和**类型推断**（Type inference）的方法，可以用来支持灵活的代数推理。 +由于完全深入细节的公理证明十分复杂，定理证明的难点在于让计算机尽可能多地填补证明细节。 +你将通过[依值类型论](dependent_type_theory.md)语言来学习各种方法实现自动证明，例如项重写， +以及 Lean 中的项和表达式的自动简化方法。同样， **繁饰（Elaboration）** +和 **类型推断（Type inference）** 的方法，可以用来支持灵活的代数推理。 -如果你在[VS Code](https://code.visualstudio.com/)中阅读本书，你会看到一个按钮，上面写着「try it!」按下按钮将示例复制到编辑器中，并带有足够的周围上下文，以使代码正确编译。您可以在编辑器中输入内容并修改示例，Lean将在您输入时检查结果并不断提供反馈。我们建议您在阅读后面的章节时，自己运行示例并试验代码。你可以通过使用「Lean 4: Open Documentation View」命令在VS Code中打开本书。 +如果你在 [VS Code](https://code.visualstudio.com/) 中阅读本书，你会看到一个按钮， +上面写着「try it!」按下按钮将示例复制到编辑器中，并带有足够的周围上下文，以使代码正确编译。 +您可以在编辑器中输入内容并修改示例，Lean 将在您输入时检查结果并不断提供反馈。 +我们建议您在阅读后面的章节时，自己运行示例并试验代码。你可以通过使用 +「Lean 4: Open Documentation View」命令在 VS Code 中打开本书。 致谢 --------------- + + +本教程是一项开放源代码项目，在 Github 上维护。许多人为此做出了贡献，提供了 +更正、建议、示例和文本。我们要感谢 Ulrik Buchholz、Kevin Buzzard、Mario Carneiro、 +Nathan Carter、Eduardo Cavazos、Amine Chaieb、Joe Corneli、William DeMeo、 +Marcus Klaas de Vries、Ben Dyer、Gabriel Ebner、Anthony Hart、Simon Hudon、Sean Leather、 +Assia Mahboubi、Gihan Marasingha、Patrick Massot、Christopher John Mazey、 +Sebastian Ullrich、Floris van Doorn、Daniel Velleman、Théo Zimmerman、Paul Chisholm、Chris Lovett +以及 Siddhartha Gadgil 对本文做出的贡献。有关我们杰出的贡献者的最新名单， +请参见 [Lean 证明器](https://github.com/leanprover/)和 [Lean 社区](https://github.com/leanprover-community/)。 diff --git a/propositions_and_proofs.md b/propositions_and_proofs.md index 487dfc0..a538ca5 100644 --- a/propositions_and_proofs.md +++ b/propositions_and_proofs.md @@ -38,7 +38,7 @@ from others. 证明在依值类型论语言中定义的对象的断言（assertion）的一种策略是在定义语言之上分层断言语言和证明语言。但是，没有理由以这种方式重复使用多种语言：依值类型论是灵活和富有表现力的，我们也没有理由不能在同一个总框架中表示断言和证明。 -例如，我们可引入一种新类型 ``Prop``，来表示命题，然后引入用其他命题构造新命题的构造器。 +例如，我们可引入一种新类型 ``Prop``，来表示命题，然后引入用其他命题构造新命题的构造子。 ```lean # def Implies (p q : Prop) : Prop := p → q @@ -209,9 +209,9 @@ verify that it is well-formed and has the correct type. 可以做一些简化。首先，我们可以通过将 ``Proof p`` 和 ``p`` 本身合并来避免重复地写 ``Proof`` 这个词。换句话说，只要我们有 ``p : Prop``，我们就可以把 ``p`` 解释为一种类型，也就是它的证明类型。然后我们可以把 ``t : p`` 读作 ``t`` 是 ``p`` 的证明。 -此外，我们可以在 ``Implies p q`` 和 ``p → q`` 之间来回切换。换句话说，命题 ``p`` 和 ``q`` 之间的含义对应于一个函数，它将 ``p`` 的任何元素接受为 ``q`` 的一个元素。因此，引入连接词 ``Implies`` 是完全多余的：我们可以使用依值类型论中常见的函数空间构造器 ``p → q`` 作为我们的蕴含概念。 +此外，我们可以在 ``Implies p q`` 和 ``p → q`` 之间来回切换。换句话说，命题 ``p`` 和 ``q`` 之间的含义对应于一个函数，它将 ``p`` 的任何元素接受为 ``q`` 的一个元素。因此，引入连接词 ``Implies`` 是完全多余的：我们可以使用依值类型论中常见的函数空间构造子 ``p → q`` 作为我们的蕴含概念。 -这是在构造演算（Calculus of Constructions）中遵循的方法，因此在 Lean 中也是如此。自然演绎证明系统中的蕴含规则与控制函数抽象（abstraction）和应用（application）的规则完全一致，这是*Curry-Howard同构*的一个实例，有时也被称为*命题即类型*。事实上，类型 ``Prop`` 是上一章描述的类型层次结构的最底部 ``Sort 0`` 的语法糖。此外，``Type u`` 也只是 ``Sort (u+1)`` 的语法糖。``Prop`` 有一些特殊的特性，但像其他类型宇宙一样，它在箭头构造器下是封闭的:如果我们有 ``p q : Prop``，那么 ``p → q : Prop``。 +这是在构造演算（Calculus of Constructions）中遵循的方法，因此在 Lean 中也是如此。自然演绎证明系统中的蕴含规则与控制函数抽象（abstraction）和应用（application）的规则完全一致，这是*Curry-Howard同构*的一个实例，有时也被称为*命题即类型*。事实上，类型 ``Prop`` 是上一章描述的类型层次结构的最底部 ``Sort 0`` 的语法糖。此外，``Type u`` 也只是 ``Sort (u+1)`` 的语法糖。``Prop`` 有一些特殊的特性，但像其他类型宇宙一样，它在箭头构造子下是封闭的:如果我们有 ``p q : Prop``，那么 ``p → q : Prop``。 至少有两种将命题作为类型来思考的方法。对于那些对逻辑和数学中的构造主义者来说，这是对命题含义的忠实诠释：命题 ``p`` 代表了一种数据类型，即构成证明的数据类型的说明。``p`` 的证明就是正确类型的对象 ``t : p``。 @@ -223,7 +223,7 @@ verify that it is well-formed and has the correct type. 在下面的论述中，我们将在这两种说话方式之间来回切换，有时说一个表达式「构造」或「产生」或「返回」一个命题的证明，有时则简单地说它「是」这样一个证明。这类似于计算机科学家偶尔会模糊语法和语义之间的区别，有时说一个程序「计算」某个函数，有时又说该程序「是」该函数。 -为了用依值类型论的语言正式表达一个数学断言，我们需要展示一个项 ``p : Prop``。为了*证明*该断言，我们需要展示一个项 ``t : p``。Lean的任务，作为一个证明助手，是帮助我们构造这样一个项 ``t``，并验证它的格式是否良好，类型是否正确。 +为了用依值类型论的语言正式表达一个数学断言，我们需要展示一个项 ``p : Prop``。为了*证明*该断言，我们需要展示一个项 ``t : p``。Lean 的任务，作为一个证明助手，是帮助我们构造这样一个项 ``t``，并验证它的格式是否良好，类型是否正确。 -注意，lambda抽象 ``hp : p`` 和 ``hq : q`` 可以被视为 ``t1`` 的证明中的临时假设。Lean还允许我们通过 ``show`` 语句明确指定最后一个项 ``hp`` 的类型。 +注意，lambda抽象 ``hp : p`` 和 ``hq : q`` 可以被视为 ``t1`` 的证明中的临时假设。Lean 还允许我们通过 ``show`` 语句明确指定最后一个项 ``hp`` 的类型。 ```lean # variable {p : Prop} @@ -417,7 +417,7 @@ If ``p`` and ``q`` have been declared as variables, Lean will generalize them for us automatically: --> -如果 ``p`` 和 ``q`` 被声明为变量，Lean会自动为我们推广它们： +如果 ``p`` 和 ``q`` 被声明为变量，Lean 会自动为我们推广它们： ```lean variable {p q : Prop} @@ -452,7 +452,7 @@ different pairs of propositions, to obtain different instances of the general theorem. --> -Lean检测到证明使用 ``hp``，并自动添加 ``hp : p`` 作为前提。在所有情况下，命令 ``#print t1`` 仍然会产生 ``∀ p q : Prop, p → q → p``。这个类型也可以写成 ``∀ (p q : Prop) (hp : p) (hq :q), p``，因为箭头仅仅表示一个箭头类型，其中目标不依赖于约束变量。 +Lean 检测到证明使用 ``hp``，并自动添加 ``hp : p`` 作为前提。在所有情况下，命令 ``#print t1`` 仍然会产生 ``∀ p q : Prop, p → q → p``。这个类型也可以写成 ``∀ (p q : Prop) (hp : p) (hq :q), p``，因为箭头仅仅表示一个箭头类型，其中目标不依赖于约束变量。 当我们以这种方式推广 ``t1`` 时，我们就可以将它应用于不同的命题对，从而得到一般定理的不同实例。 @@ -525,7 +525,7 @@ Lean defines all the standard logical connectives and notation. The propositiona They all take values in ``Prop``. --> -Lean定义了所有标准的逻辑连接词和符号。命题连接词有以下表示法: +Lean 定义了所有标准的逻辑连接词和符号。命题连接词有以下表示法: | Ascii | Unicode | 编辑器缩写 | 定义 | |------------|-----------|--------------------------|--------| @@ -653,9 +653,9 @@ inductive type and can be inferred from the context. In particular, we can often write ``⟨hp, hq⟩`` instead of ``And.intro hp hq``: --> -请注意，引入和消去与笛卡尔积的配对和投影操作类似。区别在于，给定 ``hp : p`` 和 ``hq : q``，``And.intro hp hq`` 具有类型 ``p ∧ q : Prop``，而 ``Prod hp hq`` 具有类型 ``p × q : Type``。``∧`` 和 ``×`` 之间的相似性是Curry-Howard同构的另一个例子，但与蕴涵和函数空间构造器不同，在 Lean 中 ``∧`` 和 ``×`` 是分开处理的。然而，通过类比，我们刚刚构造的证明类似于交换一对中的元素的函数。 +请注意，引入和消去与笛卡尔积的配对和投影操作类似。区别在于，给定 ``hp : p`` 和 ``hq : q``，``And.intro hp hq`` 具有类型 ``p ∧ q : Prop``，而 ``Prod hp hq`` 具有类型 ``p × q : Type``。``∧`` 和 ``×`` 之间的相似性是Curry-Howard同构的另一个例子，但与蕴涵和函数空间构造子不同，在 Lean 中 ``∧`` 和 ``×`` 是分开处理的。然而，通过类比，我们刚刚构造的证明类似于交换一对中的元素的函数。 -我们将在[结构体和记录](./structures_and_records.md)一章中看到 Lean 中的某些类型是*Structures*，也就是说，该类型是用单个规范的*构造器*定义的，该构造器从一系列合适的参数构建该类型的一个元素。对于每一组 ``p q : Prop``， ``p ∧ q`` 就是一个例子:构造一个元素的规范方法是将 ``And.intro`` 应用于合适的参数 ``hp : p`` 和 ``hq : q``。Lean允许我们使用*匿名构造器*表示法 ``⟨arg1, arg2, ...⟩`` 在此类情况下，当相关类型是归纳类型并可以从上下文推断时。特别地，我们经常可以写入 ``⟨hp, hq⟩``，而不是 ``And.intro hp hq``: +我们将在[结构体和记录](./structures_and_records.md)一章中看到 Lean 中的某些类型是*Structures*，也就是说，该类型是用单个规范的*构造子*定义的，该构造子从一系列合适的参数构建该类型的一个元素。对于每一组 ``p q : Prop``， ``p ∧ q`` 就是一个例子:构造一个元素的规范方法是将 ``And.intro`` 应用于合适的参数 ``hp : p`` 和 ``hq : q``。Lean 允许我们使用*匿名构造子*表示法 ``⟨arg1, arg2, ...⟩`` 在此类情况下，当相关类型是归纳类型并可以从上下文推断时。特别地，我们经常可以写入 ``⟨hp, hq⟩``，而不是 ``And.intro hp hq``: ```lean variable (p q : Prop) @@ -677,7 +677,7 @@ thing: 尖括号可以用 ``\<`` 和 ``\>`` 打出来。 -Lean提供了另一个有用的语法小工具。给定一个归纳类型 ``Foo`` 的表达式 ``e``(可能应用于一些参数)，符号 ``e.bar`` 是 ``Foo.bar e`` 的缩写。这为访问函数提供了一种方便的方式，而无需打开名称空间。例如，下面两个表达的意思是相同的： +Lean 提供了另一个有用的语法小工具。给定一个归纳类型 ``Foo`` 的表达式 ``e``(可能应用于一些参数)，符号 ``e.bar`` 是 ``Foo.bar e`` 的缩写。这为访问函数提供了一种方便的方式，而无需打开名称空间。例如，下面两个表达的意思是相同的： ```lean variable (xs : List Nat) @@ -715,7 +715,7 @@ these two proofs are equivalent: 在简洁和含混不清之间有一条微妙的界限，以这种方式省略信息有时会使证明更难阅读。但对于像上面这样简单的结构，当 ``h`` 的类型和结构的目标很突出时，符号是干净和有效的。 -像 ``And.`` 这样的迭代结构是很常见的。Lean还允许你将嵌套的构造函数向右结合，这样这两个证明是等价的: +像 ``And.`` 这样的迭代结构是很常见的。Lean 还允许你将嵌套的构造函数向右结合，这样这两个证明是等价的: ```lean variable (p q : Prop) @@ -785,7 +785,7 @@ shorthand for ``Or.intro_right _`` and ``Or.intro_left _``. Thus the proof term above could be written more concisely: --> -在大多数情况下，``Or.intro_right`` 和 ``Or.intro_left`` 的第一个参数可以由 Lean 自动推断出来。因此，Lean提供了 ``Or.inr`` 和 ``Or.inl`` 作为 ``Or.intro_right _`` 和 ``Or.intro_left _`` 的缩写。因此，上面的证明项可以写得更简洁: +在大多数情况下，``Or.intro_right`` 和 ``Or.intro_left`` 的第一个参数可以由 Lean 自动推断出来。因此，Lean 提供了 ``Or.inr`` 和 ``Or.inl`` 作为 ``Or.intro_right _`` 和 ``Or.intro_left _`` 的缩写。因此，上面的证明项可以写得更简洁: ```lean variable (p q r : Prop) @@ -805,9 +805,9 @@ constructor notation. But we can still write ``h.elim`` instead of ``Or.elim h``: --> -Lean的完整表达式中有足够的信息来推断 ``hp`` 和 ``hq`` 的类型。但是在较长的版本中使用类型注释可以使证明更具可读性，并有助于捕获和调试错误。 +Lean 的完整表达式中有足够的信息来推断 ``hp`` 和 ``hq`` 的类型。但是在较长的版本中使用类型注释可以使证明更具可读性，并有助于捕获和调试错误。 -因为 ``Or`` 有两个构造器，所以不能使用匿名构造器表示法。但我们仍然可以写 ``h.elim`` 而不是 ``Or.elim h``，不过你需要注意这些缩写是增强还是降低了可读性： +因为 ``Or`` 有两个构造子，所以不能使用匿名构造子表示法。但我们仍然可以写 ``h.elim`` 而不是 ``Or.elim h``，不过你需要注意这些缩写是增强还是降低了可读性： ```lean variable (p q r : Prop) @@ -936,7 +936,7 @@ can also use ``.`` notation with ``mp`` and ``mpr``. The previous examples can therefore be written concisely as follows: --> -我们可以用匿名构造器表示法来，从正反两个方向的证明，来构建 ``p ↔ q`` 的证明。我们也可以使用 ``.`` 符号连接 ``mp`` 和 ``mpr``。因此，前面的例子可以简写如下： +我们可以用匿名构造子表示法来，从正反两个方向的证明，来构建 ``p ↔ q`` 的证明。我们也可以使用 ``.`` 符号连接 ``mp`` 和 ``mpr``。因此，前面的例子可以简写如下： ```lean variable (p q : Prop) @@ -989,7 +989,7 @@ the previous proof. 在内部，表达式 ``have h : p := s; t`` 产生项 ``(fun (h : p) => t) s``。换句话说，``s`` 是 ``p`` 的证明，``t`` 是假设 ``h : p`` 的期望结论的证明，并且这两个是由 lambda 抽象和应用组合在一起的。这个简单的方法在构建长证明时非常有用，因为我们可以使用中间的 ``have`` 作为通向最终目标的垫脚石。 -Lean还支持从目标向后推理的结构化方法，它模仿了普通数学文献中「足以说明某某」（suffices to show）的构造。下一个例子简单地排列了前面证明中的最后两行。 +Lean 还支持从目标向后推理的结构化方法，它模仿了普通数学文献中「足以说明某某」（suffices to show）的构造。下一个例子简单地排列了前面证明中的最后两行。 ```lean variable (p q : Prop) @@ -1136,9 +1136,9 @@ reasoning are discussed in [Axioms and Computation](./axioms_and_computation.md) --> -稍后我们将看到，构造逻辑中**有**某些情况允许「排中律」和「双重否定消除律」等，而 Lean 支持在这种情况下使用经典推理，而不依赖于排中律。 +稍后我们将看到，构造逻辑中 **有** 某些情况允许「排中律」和「双重否定消除律」等，而 Lean 支持在这种情况下使用经典推理，而不依赖于排中律。 -Lean中使用的公理的完整列表见[公理与计算](./axioms_and_computation.md)。 +Lean 中使用的公理的完整列表见[公理与计算](./axioms_and_computation.md)。 -Lean的标准库包含了许多命题逻辑的有效语句的证明，你可以自由地在自己的证明中使用这些证明。下面的列表包括一些常见的逻辑等价式。 +Lean 的标准库包含了许多命题逻辑的有效语句的证明，你可以自由地在自己的证明中使用这些证明。下面的列表包括一些常见的逻辑等价式。 -``sorry`` 标识符神奇地生成任何东西的证明，或者提供任何数据类型的对象。当然，作为一种证明方法，它是不可靠的——例如，你可以使用它来证明 ``False``——并且当文件使用或导入依赖于它的定理时，Lean会产生严重的警告。但它对于增量地构建长证明非常有用。从上到下写证明，用 ``sorry`` 来填子证明。确保 Lean 接受所有的 ``sorry``；如果不是，则有一些错误需要纠正。然后返回，用实际的证据替换每个 ``sorry``，直到做完。 +``sorry`` 标识符神奇地生成任何东西的证明，或者提供任何数据类型的对象。当然，作为一种证明方法，它是不可靠的——例如，你可以使用它来证明 ``False``——并且当文件使用或导入依赖于它的定理时，Lean 会产生严重的警告。但它对于增量地构建长证明非常有用。从上到下写证明，用 ``sorry`` 来填子证明。确保 Lean 接受所有的 ``sorry``；如果不是，则有一些错误需要纠正。然后返回，用实际的证据替换每个 ``sorry``，直到做完。 -有另一个有用的技巧。你可以使用下划线 ``_`` 作为占位符，而不是 ``sorry``。回想一下，这告诉 Lean 该参数是隐式的，应该自动填充。如果 Lean 尝试这样做并失败了，它将返回一条错误消息「不知道如何合成占位符」（Don't know how to synthesize placeholder），然后是它所期望的项的类型，以及上下文中可用的所有对象和假设。换句话说，对于每个未解决的占位符，Lean报告在那一点上需要填充的子目标。然后，你可以通过递增填充这些占位符来构造一个证明。 +有另一个有用的技巧。你可以使用下划线 ``_`` 作为占位符，而不是 ``sorry``。回想一下，这告诉 Lean 该参数是隐式的，应该自动填充。如果 Lean 尝试这样做并失败了，它将返回一条错误消息「不知道如何合成占位符」（Don't know how to synthesize placeholder），然后是它所期望的项的类型，以及上下文中可用的所有对象和假设。换句话说，对于每个未解决的占位符，Lean 报告在那一点上需要填充的子目标。然后，你可以通过递增填充这些占位符来构造一个证明。 这里有两个简单的证明例子作为参考。 diff --git a/quantifiers_and_equality.md b/quantifiers_and_equality.md index 6764648..74b3223 100644 --- a/quantifiers_and_equality.md +++ b/quantifiers_and_equality.md @@ -402,7 +402,7 @@ example : f a = g b := congr h₂ h₁ Lean's library contains a large number of common identities, such as these: --> -Lean的库包含大量通用的等式，例如： +Lean 的库包含大量通用的等式，例如： ```lean variable (a b c : Nat) @@ -467,7 +467,7 @@ chapter. 注意，``Eq.subst`` 的第二个隐式参数提供了将要发生代换的表达式上下文，其类型为 ``α → Prop``。因此，推断这个谓词需要一个*高阶合一*（higher-order unification）的实例。一般来说，确定高阶合一器是否存在的问题是无法确定的，而 Lean 充其量只能提供不完美的和近似的解决方案。因此，``Eq.subst`` 并不总是做你想要它做的事。宏 ``h ▸ e`` 使用了更有效的启发式方法来计算这个隐参数，并且在不能应用 ``Eq.subst`` 的情况下通常会成功。 -因为等式推理是如此普遍和重要，Lean提供了许多机制来更有效地执行它。下一节将提供允许你以更自然和清晰的方式编写计算式证明的语法。但更重要的是，等式推理是由项重写器、简化器和其他种类的自动化方法支持的。术语重写器和简化器将在下一节中简要描述，然后在下一章中更详细地描述。 +因为等式推理是如此普遍和重要，Lean 提供了许多机制来更有效地执行它。下一节将提供允许你以更自然和清晰的方式编写计算式证明的语法。但更重要的是，等式推理是由项重写器、简化器和其他种类的自动化方法支持的。术语重写器和简化器将在下一节中简要描述，然后在下一章中更详细地描述。 -当类型可从上下文中推断时，我们可以使用匿名构造器表示法 ``⟨t, h⟩`` 替换 ``Exists.intro t h``。 +当类型可从上下文中推断时，我们可以使用匿名构造子表示法 ``⟨t, h⟩`` 替换 ``Exists.intro t h``。 ```lean example : ∃ x : Nat, x > 0 := @@ -810,7 +810,7 @@ following example, in which we set the option ``pp.explicit`` to true to ask Lean's pretty-printer to show the implicit arguments. --> -注意 ``Exists.intro`` 有隐参数：Lean必须在结论 ``∃ x, p x`` 中推断谓词 ``p : α → Prop``。这不是一件小事。例如，如果我们有 ``hg : g 0 0 = 0`` 和 ``Exists.intro 0 hg``，有许多可能的值的谓词 ``p``，对应定理 ``∃ x, g x x = x``，``∃ x, g x x = 0``，``∃ x, g x 0 = x``，等等。Lean使用上下文来推断哪个是合适的。下面的例子说明了这一点，在这个例子中，我们设置了选项 ``pp.explicit`` 为true，要求 Lean 打印隐参数。 +注意 ``Exists.intro`` 有隐参数：Lean 必须在结论 ``∃ x, p x`` 中推断谓词 ``p : α → Prop``。这不是一件小事。例如，如果我们有 ``hg : g 0 0 = 0`` 和 ``Exists.intro 0 hg``，有许多可能的值的谓词 ``p``，对应定理 ``∃ x, g x x = x``，``∃ x, g x x = 0``，``∃ x, g x 0 = x``，等等。Lean 使用上下文来推断哪个是合适的。下面的例子说明了这一点，在这个例子中，我们设置了选项 ``pp.explicit`` 为true，要求 Lean 打印隐参数。 -把存在消去规则和析取消去规则作个比较可能会带来一些启发。命题 ``∃ x : α, p x`` 可以看成一个对所有 ``α`` 中的元素 ``a`` 所组成的命题 ``p a`` 的大型析取。注意到匿名构造器 ``⟨w, hw.right, hw.left⟩`` 是嵌套的构造器 ``⟨w, ⟨hw.right, hw.left⟩⟩`` 的缩写。 +把存在消去规则和析取消去规则作个比较可能会带来一些启发。命题 ``∃ x : α, p x`` 可以看成一个对所有 ``α`` 中的元素 ``a`` 所组成的命题 ``p a`` 的大型析取。注意到匿名构造子 ``⟨w, hw.right, hw.left⟩`` 是嵌套的构造子 ``⟨w, ⟨hw.right, hw.left⟩⟩`` 的缩写。 存在式命题类型很像依值类型一节所述的 sigma 类型。给定 ``a : α`` 和 ``h : p a`` 时，项 ``Exists.intro a h`` 具有类型 ``(∃ x : α, p x) : Prop``，而 ``Sigma.mk a h`` 具有类型 ``(Σ x : α, p x) : Type``。``∃`` 和 ``Σ`` 之间的相似性是Curry-Howard同构的另一例子。 -Lean提供一个更加方便的消去存在量词的途径，那就是通过 ``match`` 表达式。 +Lean 提供一个更加方便的消去存在量词的途径，那就是通过 ``match`` 表达式。 ```lean variable (α : Type) (p q : α → Prop) @@ -941,7 +941,7 @@ example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := Lean also provides a pattern-matching ``let`` expression: --> -Lean还提供了一个模式匹配的 ``let`` 表达式： +Lean 还提供了一个模式匹配的 ``let`` 表达式： ```lean # variable (α : Type) (p q : α → Prop) @@ -956,7 +956,7 @@ construct above. Lean will even allow us to use an implicit ``match`` in the ``fun`` expression: --> -这实际上是上面的 ``match`` 结构的替代表示法。Lean甚至允许我们在 ``fun`` 表达式中使用隐含的 ``match``： +这实际上是上面的 ``match`` 结构的替代表示法。Lean 甚至允许我们在 ``fun`` 表达式中使用隐含的 ``match``： ```lean @@ -996,7 +996,7 @@ statement, anonymous constructors, and the ``rewrite`` tactic, we can write this proof concisely as follows: --> -使用本章描述的各种小工具——``match`` 语句、匿名构造器和 ``rewrite`` 策略，我们可以简洁地写出如下证明： +使用本章描述的各种小工具——``match`` 语句、匿名构造子和 ``rewrite`` 策略，我们可以简洁地写出如下证明： ```lean # def is_even (a : Nat) := ∃ b, a = 2 * b diff --git a/structures_and_records.md b/structures_and_records.md index 1be567a..d7641cc 100644 --- a/structures_and_records.md +++ b/structures_and_records.md @@ -34,11 +34,11 @@ previously defined ones. Moreover, Lean provides convenient notation for defining instances of a given structure. --> -我们已经看到Lean的基本系统包括归纳类型。此外，显然仅基于类型宇宙、依赖箭头类型和归纳类型，就有可能构建一个坚实的数学大厦；其他的一切都是由此而来。Lean标准库包含许多归纳类型的实例(例如，``Nat``，``Prod``，``List``)，甚至逻辑连接词也是使用归纳类型定义的。 +我们已经看到Lean 的基本系统包括归纳类型。此外，显然仅基于类型宇宙、依赖箭头类型和归纳类型，就有可能构建一个坚实的数学大厦；其他的一切都是由此而来。Lean 标准库包含许多归纳类型的实例(例如，``Nat``，``Prod``，``List``)，甚至逻辑连接词也是使用归纳类型定义的。 -回忆一下，只包含一个构造器的非递归归纳类型被称为**结构体**（structure）或**记录**（record）。乘积类型是一种结构体，依值乘积(Sigma)类型也是如此。一般来说，每当我们定义一个结构体``S``时，我们通常定义*投影*（projection）函数来「析构」（destruct）``S``的每个实例并检索存储在其字段中的值。``prod.pr1``和``prod.pr2``，分别返回乘积对中的第一个和第二个元素的函数，就是这种投影的例子。 +回忆一下，只包含一个构造子的非递归归纳类型被称为 **结构体（structure）** 或 **记录（record）** 。乘积类型是一种结构体，依值乘积(Sigma)类型也是如此。一般来说，每当我们定义一个结构体 ``S`` 时，我们通常定义*投影*（projection）函数来「析构」（destruct）``S`` 的每个实例并检索存储在其字段中的值。``prod.pr1`` 和 ``prod.pr2``，分别返回乘积对中的第一个和第二个元素的函数，就是这种投影的例子。 -在编写程序或形式化数学时，定义包含许多字段的结构体是很常见的。Lean中可用``structure``命令实现此过程。当我们使用这个命令定义一个结构体时，Lean会自动生成所有的投影函数。``structure``命令还允许我们根据以前定义的结构体定义新的结构体。此外，Lean为定义给定结构体的实例提供了方便的符号。 +在编写程序或形式化数学时，定义包含许多字段的结构体是很常见的。Lean 中可用 ``structure`` 命令实现此过程。当我们使用这个命令定义一个结构体时，Lean 会自动生成所有的投影函数。``structure`` 命令还允许我们根据以前定义的结构体定义新的结构体。此外，Lean 为定义给定结构体的实例提供了方便的符号。 -结构体命令本质上是定义归纳数据类型的「前端」。每个``structure``声明都会引入一个同名的命名空间。一般形式如下: +结构体命令本质上是定义归纳数据类型的「前端」。每个 ``structure`` 声明都会引入一个同名的命名空间。一般形式如下: ``` structure where @@ -81,7 +81,7 @@ theorems. Here are some of the constructions generated for the declaration above. --> -类型``Point``的值是使用``Point.mk a b``创建的，并且点``p``的字段可以使用``Point.x p``和``Point.y p``。结构体命令还生成有用的递归器和定理。下面是为上述声明生成的一些结构体方法。 +类型 ``Point`` 的值是使用 ``Point.mk a b`` 创建的，并且点 ``p`` 的字段可以使用 ``Point.x p`` 和 ``Point.y p``。结构体命令还生成有用的递归器和定理。下面是为上述声明生成的一些结构体方法。 -如果没有提供构造器名称，则默认的构造函数名为``mk``。如果在每个字段之间添加换行符，也可以避免字段名周围的括号。 +如果没有提供构造子名称，则默认的构造函数名为 ``mk``。如果在每个字段之间添加换行符，也可以避免字段名周围的括号。 ```lean structure Point (α : Type u) where @@ -131,7 +131,7 @@ constructions. As usual, you can avoid the prefix ``Point`` by using the command ``open Point``. --> -下面是一些使用生成的结构的简单定理和表达式。像往常一样，您可以通过使用命令``open Point``来避免前缀``Point``。 +下面是一些使用生成的结构的简单定理和表达式。像往常一样，您可以通过使用命令 ``open Point`` 来避免前缀 ``Point``。 ```lean # structure Point (α : Type u) where @@ -155,7 +155,7 @@ Given ``p : Point Nat``, the dot notation ``p.x`` is shorthand for of a structure. --> -给定``p : Point Nat``，符号``p.x``是``Point.x p``的缩写。这提供了一种方便的方式来访问结构体的字段。 +给定 ``p : Point Nat``，符号 ``p.x`` 是 ``Point.x p`` 的缩写。这提供了一种方便的方式来访问结构体的字段。 ```lean # structure Point (α : Type u) where @@ -178,7 +178,7 @@ has type ``Point``, the expression ``p.foo`` is interpreted as shorthand for ``Point.add p q`` in the example below. --> -点记号不仅方便于访问记录的投影，而且也方便于应用同名命名空间中定义的函数。回想一下[合取](./propositions_and_proofs.md#_conjunction)一节，如果``p``具有``Point``类型，那么表达式``p.foo``被解释为``Point.foo p``，假设``foo``的第一个非隐式参数具有类型``Point``，表达式``p.add q``因此是``Point.add p q``的缩写。可见下面的例子。 +点记号不仅方便于访问记录的投影，而且也方便于应用同名命名空间中定义的函数。回想一下[合取](./propositions_and_proofs.md#_conjunction)一节，如果 ``p`` 具有 ``Point`` 类型，那么表达式 ``p.foo`` 被解释为 ``Point.foo p``，假设 ``foo`` 的第一个非隐式参数具有类型 ``Point``，表达式 ``p.add q`` 因此是 ``Point.add p q`` 的缩写。可见下面的例子。 ```lean structure Point (α : Type u) where @@ -207,9 +207,9 @@ Lean will insert ``p`` at the first argument to ``Point.foo`` of type below, ``p.smul 3`` is interpreted as ``Point.smul 3 p``. --> -在下一章中，您将学习如何定义一个像``add``这样的函数，这样它就可以通用地为``Point α``的元素工作，而不仅仅是``Point Nat``，只要假设``α``有一个关联的加法操作。 +在下一章中，您将学习如何定义一个像 ``add`` 这样的函数，这样它就可以通用地为 ``Point α`` 的元素工作，而不仅仅是 ``Point Nat``，只要假设 ``α`` 有一个关联的加法操作。 -更一般地，给定一个表达式``p.foo x y z``其中`p : Point`，Lean会把``p``以``Point``为类型插入到``Point.foo``的第一个参数。例如，下面是标量乘法的定义，``p.smul 3``被解释为``Point.smul 3 p``。 +更一般地，给定一个表达式 ``p.foo x y z`` 其中`p : Point`，Lean 会把 ``p`` 以 ``Point`` 为类型插入到 ``Point.foo`` 的第一个参数。例如，下面是标量乘法的定义，``p.smul 3`` 被解释为 ``Point.smul 3 p``。 ```lean # structure Point (α : Type u) where @@ -229,7 +229,7 @@ It is common to use a similar trick with the ``List.map`` function, which takes a list as its second non-implicit argument: --> -对``List.map``函数使用类似的技巧很常用。它接受一个列表作为它的第二个非隐式参数: +对 ``List.map`` 函数使用类似的技巧很常用。它接受一个列表作为它的第二个非隐式参数: ```lean #check @List.map @@ -244,7 +244,7 @@ def f : Nat → Nat := fun x => x * x Here ``xs.map f`` is interpreted as ``List.map f xs``. --> -此处``xs.map f``被解释为``List.map f xs``。 +此处 ``xs.map f`` 被解释为 ``List.map f xs``。 -我们一直在使用构造器创建结构体类型的元素。对于包含许多字段的结构，这通常是不方便的，因为我们必须记住字段定义的顺序。因此，Lean为定义结构体类型的元素提供了以下替代符号。 +我们一直在使用构造子创建结构体类型的元素。对于包含许多字段的结构，这通常是不方便的，因为我们必须记住字段定义的顺序。因此，Lean 为定义结构体类型的元素提供了以下替代符号。 ``` { ( := )* : structure-type } @@ -278,7 +278,7 @@ specified does not matter, so all the expressions below define the same point. --> -只要可以从期望的类型推断出结构体的名称，后缀``: structure-type``就可以省略。例如，我们使用这种表示法来定义「Point」。字段的指定顺序无关紧要，因此下面的所有表达式定义相同的Point。 +只要可以从期望的类型推断出结构体的名称，后缀 ``: structure-type`` 就可以省略。例如，我们使用这种表示法来定义「Point」。字段的指定顺序无关紧要，因此下面的所有表达式定义相同的Point。 ```lean structure Point (α : Type u) where @@ -299,7 +299,7 @@ the unspecified fields cannot be inferred, Lean flags an error indicating the corresponding placeholder could not be synthesized. --> -如果一个字段的值没有指定，Lean会尝试推断它。如果不能推断出未指定的字段，Lean会标记一个错误，表明相应的占位符无法合成。 +如果一个字段的值没有指定，Lean 会尝试推断它。如果不能推断出未指定的字段，Lean 会标记一个错误，表明相应的占位符无法合成。 ```lean structure MyStruct where @@ -323,7 +323,7 @@ field. Lean raises an error if any of the field names remain unspecified after all the objects are visited. --> -**记录更新**（Record update）是另一个常见的操作，相当于通过修改旧记录中的一个或多个字段的值来创建一个新的记录对象。通过在字段赋值之前添加注释``s with``，Lean允许您指定记录规范中未赋值的字段，该字段应从之前定义的结构对象``s``中获取。如果提供了多个记录对象，那么将按顺序访问它们，直到Lean找到一个包含未指定字段的记录对象。如果在访问了所有对象之后仍未指定任何字段名，Lean将引发错误。 + **记录更新（Record update）** 是另一个常见的操作，相当于通过修改旧记录中的一个或多个字段的值来创建一个新的记录对象。通过在字段赋值之前添加注释 ``s with``，Lean 允许您指定记录规范中未赋值的字段，该字段应从之前定义的结构对象 ``s`` 中获取。如果提供了多个记录对象，那么将按顺序访问它们，直到Lean 找到一个包含未指定字段的记录对象。如果在访问了所有对象之后仍未指定任何字段名，Lean 将引发错误。 ```lean structure Point (α : Type u) where @@ -366,7 +366,7 @@ We can *extend* existing structures by adding new fields. This feature allows us to simulate a form of *inheritance*. --> -我们可以通过添加新的字段来**扩展**现有的结构体。这个特性允许我们模拟一种形式的**继承**。 +我们可以通过添加新的字段来 **扩展** 现有的结构体。这个特性允许我们模拟一种形式的 **继承** 。 ```lean structure Point (α : Type u) where diff --git a/tactics.md b/tactics.md index 9b6ea4c..bd609a4 100644 --- a/tactics.md +++ b/tactics.md @@ -29,9 +29,10 @@ write. Moreover, tactics offer a gateway to using Lean's automation, since automated procedures are themselves tactics. --> -在本章中，我们描述了另一种构建证明的方法，即使用**策略**（Tactic）。 一个证明项代表一个数学证明；策略是描述如何建立这样一个证明的命令或指令。你可以在数学证明开始时非正式地说：「为了证明条件的必要性，展开定义，应用前面的定理，并进行简化。」就像这些指令告诉读者如何构建证明一样，策略告诉 Lean 如何构建证明。它们自然而然地支持增量式的证明书写，在这种写作方式中，你将分解一个证明，并一步步地实现目标。 +在本章中，我们描述了另一种构建证明的方法，即使用 **策略（Tactic）** 。 一个证明项代表一个数学证明；策略是描述如何建立这样一个证明的命令或指令。你可以在数学证明开始时非正式地说：「为了证明条件的必要性，展开定义，应用前面的定理，并进行简化。」就像这些指令告诉读者如何构建证明一样，策略告诉 Lean 如何构建证明。它们自然而然地支持增量式的证明书写，在这种写作方式中，你将分解一个证明，并一步步地实现目标。 -> 译者注：tactic 和 strategy 都有策略的意思，其中 tactic 侧重细节，如排兵布阵，strategy面向整体，如大规模战略。试译 strategy 为「要略」，与 tactic 相区分。 +> 译者注：tactic 和 strategy 都有策略的意思，其中 tactic 侧重细节，如排兵布阵， +> strategy 面向整体，如大规模战略。试译 strategy 为「要略」，与 tactic 相区分。 我们将把由策略序列组成的证明描述为「策略式」证明，前几章的证明我们称为「项式」证明。每种风格都有自己的优点和缺点。例如，策略式证明可能更难读，因为它们要求读者预测或猜测每条指令的结果。但它们一般更短，更容易写。此外，策略提供了一个使用 Lean 自动化的途径，因为自动化程序本身就是策略。 @@ -80,9 +81,9 @@ separated by semicolons or line breaks. You can prove the theorem above in that way: --> -事实上，如果你把上面的例子中的「sorry」换成下划线，Lean会报告说，正是这个目标没有得到解决。 +事实上，如果你把上面的例子中的「sorry」换成下划线，Lean 会报告说，正是这个目标没有得到解决。 -通常情况下，你会通过写一个明确的项来满足这样的目标。但在任何需要项的地方，Lean允许我们插入一个 ``by `` 块，其中 ```` 是一串命令，用分号或换行符分开。你可以用下面这种方式来证明上面的定理： +通常情况下，你会通过写一个明确的项来满足这样的目标。但在任何需要项的地方，Lean 允许我们插入一个 ``by `` 块，其中 ```` 是一串命令，用分号或换行符分开。你可以用下面这种方式来证明上面的定理： ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := @@ -262,9 +263,9 @@ the "bullet" notation ``. `` (or ``· ``) for structuring proof. --> -注意，Lean将其他目标隐藏在 ``case`` 块内。我们说它「专注」于选定的目标。 此外，如果所选目标在 ``case`` 块的末尾没有完全解决，Lean会标记一个错误。 +注意，Lean 将其他目标隐藏在 ``case`` 块内。我们说它「专注」于选定的目标。 此外，如果所选目标在 ``case`` 块的末尾没有完全解决，Lean 会标记一个错误。 -对于简单的子目标，可能不值得使用其标签来选择一个子目标，但你可能仍然想要结构化证明。Lean还提供了「子弹」符号 ``. `` 或 ``· ``。 +对于简单的子目标，可能不值得使用其标签来选择一个子目标，但你可能仍然想要结构化证明。Lean 还提供了「子弹」符号 ``. `` 或 ``· ``。 ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by @@ -779,7 +780,7 @@ constructor for conjunction, ``And.intro``. With these tactics, an example from the previous section can be rewritten as follows: --> -在这个例子中，应用 ``cases`` 策略后只有一个目标，``h : p ∧ q`` 被一对假设取代，``hp : p`` 和 ``hq : q``。``constructor`` 策略应用了唯一一个合取构造器 ``And.intro``。有了这些策略，上一节的一个例子可以改写如下。 +在这个例子中，应用 ``cases`` 策略后只有一个目标，``h : p ∧ q`` 被一对假设取代，``hp : p`` 和 ``hq : q``。``constructor`` 策略应用了唯一一个合取构造子 ``And.intro``。有了这些策略，上一节的一个例子可以改写如下。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -808,7 +809,7 @@ always applies the first applicable constructor of an inductively defined type. For example, you can use ``cases`` and ``constructor`` with an existential quantifier: --> -你将在[归纳类型](./inductive_types.md)一章中看到，这些策略是相当通用的。``cases`` 策略可以用来分解递归定义类型的任何元素；``constructor`` 总是应用递归定义类型的第一个适用构造器。例如，你可以使用 ``cases`` 和 ``constructor`` 与一个存在量词： +你将在[归纳类型](./inductive_types.md)一章中看到，这些策略是相当通用的。``cases`` 策略可以用来分解递归定义类型的任何元素；``constructor`` 总是应用递归定义类型的第一个适用构造子。例如，你可以使用 ``cases`` 和 ``constructor`` 与一个存在量词： ```lean example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := by @@ -970,7 +971,7 @@ block. The following is a somewhat toy example: 策略通常提供了建立证明的有效方法，但一长串指令会掩盖论证的结构。在这一节中，我们将描述一些有助于为策略式证明提供结构的方法，使这种证明更易读，更稳健。 -Lean的证明写作语法的一个优点是，它可以混合项式和策略式证明，并在两者之间自由转换。例如，策略 ``apply`` 和 ``exact`` 可以传入任意的项，你可以用 ``have``，``show`` 等等来写这些项。反之，当写一个任意的 Lean 项时，你总是可以通过插入一个 ``by`` 块来调用策略模式。下面是一个简易例子： +Lean 的证明写作语法的一个优点是，它可以混合项式和策略式证明，并在两者之间自由转换。例如，策略 ``apply`` 和 ``exact`` 可以传入任意的项，你可以用 ``have``，``show`` 等等来写这些项。反之，当写一个任意的 Lean 项时，你总是可以通过插入一个 ``by`` 块来调用策略模式。下面是一个简易例子： ```lean example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by @@ -1116,7 +1117,7 @@ auxiliary facts. It is the tactic analogue of a ``let`` in a proof term. --> -Lean还有一个 ``let`` 策略，与 ``have`` 策略类似，但用于引入局部定义而不是辅助事实。它是证明项中 ``let`` 的策略版。 +Lean 还有一个 ``let`` 策略，与 ``have`` 策略类似，但用于引入局部定义而不是辅助事实。它是证明项中 ``let`` 的策略版。 ```lean example : ∃ x, x + 2 = 8 := by @@ -1141,7 +1142,7 @@ define tactic blocks using curly braces and semicolons. 和 ``have`` 一样，你可以通过写 ``let a := 3 * 2`` 来保留类型为隐式。``let`` 和 ``have`` 的区别在于，``let`` 在上下文中引入了一个局部定义，因此局部声明的定义可以在证明中展开。 -我们使用了`.`来创建嵌套的策略块。 在一个嵌套块中，Lean专注于第一个目标，如果在该块结束时还没有完全解决，就会产生一个错误。这对于表明一个策略所引入的多个子目标的单独证明是有帮助的。符号 ``.`` 是对空格敏感的，并且依靠缩进来检测策略块是否结束。另外，你也可以用大括号和分号来定义策略块。 +我们使用了`.`来创建嵌套的策略块。 在一个嵌套块中，Lean 专注于第一个目标，如果在该块结束时还没有完全解决，就会产生一个错误。这对于表明一个策略所引入的多个子目标的单独证明是有帮助的。符号 ``.`` 是对空格敏感的，并且依靠缩进来检测策略块是否结束。另外，你也可以用大括号和分号来定义策略块。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -1221,7 +1222,7 @@ Tactic Combinators ones. A sequencing combinator is already implicit in the ``by`` block: --> -**策略组合器**是由旧策略形成新策略的操作。``by`` 隐含了一个序列组合器： + **策略组合器** 是由旧策略形成新策略的操作。``by`` 隐含了一个序列组合器： ```lean example (p q : Prop) (hp : p) : p ∨ q := @@ -1559,7 +1560,7 @@ number of identities in Lean's library have been tagged with the rewrite subterms in an expression. --> -``rewrite`` 被设计为操纵目标的手术刀，而简化器提供了一种更强大的自动化形式。Lean库中的一些特性已经被标记为`[simp]`属性，`simp` 策略使用它们来反复重写表达式中的子项。 +``rewrite`` 被设计为操纵目标的手术刀，而简化器提供了一种更强大的自动化形式。Lean 库中的一些特性已经被标记为`[simp]`属性，`simp` 策略使用它们来反复重写表达式中的子项。 ```lean example (x y z : Nat) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by diff --git a/title_page.md b/title_page.md index c53b672..b95f71a 100644 --- a/title_page.md +++ b/title_page.md @@ -6,7 +6,7 @@ 作者：*Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, 以及来自 Lean 社区的贡献者* -**[Lean-zh 项目组](https://github.com/Lean-zh) 译** + **[Lean-zh 项目组](https://github.com/Lean-zh) 译** -将 **类型类（Type Class）** 作为一种原则性方法引入， -是为了在函数式编程语言中支持 **特设多态（Ad-hoc Polymorphism）**。 +将 **类型类（Type Class）** 作为一种原则性方法引入， +是为了在函数式编程语言中支持 **特设多态（Ad-hoc Polymorphism）** 。 我们首先观察到，如果函数简单地接受特定类型的实现作为参数， 然后在其余参数上调用该实现，则很容易实现特设多态函数（如加法）。 例如，假设我们在 Lean 中声明一个结构体来保存加法的实现： @@ -97,7 +97,7 @@ i.e. that it should be synthesized using typeclass resolution. This version of Similarly, we can register instances by: --> -其中方括号表示类型为 `Add a` 的参数是 **实例隐式的**， +其中方括号表示类型为 `Add a` 的参数是 **实例隐式的** ， 即，它应该使用类型类求解合成。这个版本的 `add` 是 Haskell 项 `add :: Add a => a -> a -> a` 的 Lean 类比。 同样，我们可以通过以下方式注册实例： @@ -203,7 +203,7 @@ Let us start with the first step of the program above, declaring an appropriate 例如，我们可能希望当 ``xs`` 为 ``List a`` 类型时 ``head xs`` 表达式的类型为 ``a``。 类似地，许多定理在类型不为空的附加假设下成立。例如，如果 ``a`` 是一个类型， 则 ``exists x : a, x = x`` 仅在 ``a`` 不为空时为真。标准库定义了一个类型类 -``Inhabited``，它能够让类型类推理来推断**可居（Inhabited）**类型类的「默认」元素。 +``Inhabited``，它能够让类型类推理来推断 **可居（Inhabited）** 类型类的「默认」元素。 让我们从上述程序的第一步开始，声明一个适当的类： ```lean @@ -467,7 +467,7 @@ You can input the raw natural number `2` using the macro `nat_lit 2`. Lean 会将项 `(2 : Nat)` 和 `(2 : Rational)` 分别繁饰（Elaborate）为： `OfNat.ofNat Nat 2 (instOfNatNat 2)` 和 `OfNat.ofNat Rational 2 (instOfNatRational 2)`。 -我们将繁饰的项中出现的数字 `2` 称为 **原始** 自然数。 +我们将繁饰的项中出现的数字 `2` 称为 **原始** 自然数。 你可以使用宏 `nat_lit 2` 来输入原始自然数 `2`。 ```lean @@ -478,7 +478,7 @@ Lean 会将项 `(2 : Nat)` 和 `(2 : Rational)` 分别繁饰（Elaborate）为 Raw natural numbers are *not* polymorphic. --> -原始自然数 **不是** 多态的。 +原始自然数 **不是** 多态的。 `OfNat` 实例对数值进行了参数化，因此你可以定义特定数字的实例。 -第二个参数通常是变量，如上例所示，或者是一个 **原始** 自然数。 +第二个参数通常是变量，如上例所示，或者是一个 **原始** 自然数。 ```lean class Monoid (α : Type u) where @@ -528,10 +528,10 @@ In the following example, we use output parameters to define a *heterogeneous* p multiplication. --> -你可以将类型类 `Inhabited` 的参数视为类型类合成器的 **输入** 值。 +你可以将类型类 `Inhabited` 的参数视为类型类合成器的 **输入** 值。 当类型类有多个参数时，可以将其中一些标记为输出参数。 即使这些参数有缺失部分，Lean 也会开始类型类合成。 -在下面的示例中，我们使用输出参数定义一个 **异质（Heterogeneous）** 的多态乘法。 +在下面的示例中，我们使用输出参数定义一个 **异质（Heterogeneous）** 的多态乘法。 ```lean # namespace Ex @@ -638,7 +638,7 @@ this kind of situation. We can achieve exactly that using *default instances*. 实例 `HMul` 没有被 Lean 合成，因为没有提供 `y` 的类型。 然而，在这种情况下，自然应该认为 `y` 和 `x` 的类型应该相同。 -我们可以使用 **默认实例** 来实现这一点。 +我们可以使用 **默认实例** 来实现这一点。 ```lean # namespace Ex @@ -985,7 +985,7 @@ connectives: --> 如果没有经典逻辑，我们就不能证明每个命题都是可判定的。 -但我们可以证明**某些**命题是可判定的。 +但我们可以证明 **某些** 命题是可判定的。 例如，我们可以证明基本运算（比如自然数和整数上的等式和比较）的可判定性。 此外，命题连词下的可判定性被保留了下来： @@ -1276,7 +1276,7 @@ is done: --> 你可以按对类型类实例进行尝试的顺序来更改这些实例， -方法是为它们分配一个**优先级**。在声明实例时， +方法是为它们分配一个 **优先级** 。在声明实例时， 它将被分配一个默认优先级值。在定义实例时，你可以分配其他的优先级。 以下示例说明了如何执行此操作： @@ -1442,7 +1442,7 @@ Lean 也会在有需要的时候构造链式（非依赖的）强制转换。事 Let us now consider the second kind of coercion. By the *class of sorts*, we mean the collection of universes ``Type u``. A coercion of the second kind is of the form: --> -现在我们来考查第二种强制转换。**种类类（Class of Sort）**是指宇宙 ``Type u`` 的集合。 +现在我们来考查第二种强制转换。 **种类类（Class of Sort）** 是指宇宙 ``Type u`` 的集合。 第二种强制转换的形式如下： ``` @@ -1520,7 +1520,7 @@ It is the coercion that makes it possible to write ``(a b c : S)``. Note that, w By the *class of function types*, we mean the collection of Pi types ``(z : B) → C``. The third kind of coercion has the form: --> -**函数类型的类**，是指 Π 类型集合 ``(z : B) → C``。第三种强制转换形式为： + **函数类型的类** ，是指 Π 类型集合 ``(z : B) → C``。第三种强制转换形式为： ``` c : (x1 : A1) → ... → (xn : An) → (y : F x1 ... xn) → (z : B) → C