From 2846fa72d97003006aa57306b0c71bb422e53dca Mon Sep 17 00:00:00 2001 From: Oling Cat Date: Sun, 23 Jun 2024 03:48:24 +0800 Subject: [PATCH] fix bold --- axioms_and_computation.md | 24 ++++++++++++------------ dependent_type_theory.md | 8 ++++---- induction_and_recursion.md | 12 ++++++------ inductive_types.md | 18 +++++++++--------- interacting_with_lean.md | 18 +++++++++--------- introduction.md | 20 ++++++++++---------- propositions_and_proofs.md | 4 ++-- structures_and_records.md | 6 +++--- tactics.md | 4 ++-- title_page.md | 2 +- type_classes.md | 28 ++++++++++++++-------------- 11 files changed, 72 insertions(+), 72 deletions(-) diff --git a/axioms_and_computation.md b/axioms_and_computation.md index c9d6fd6..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 世纪，数学论证复杂性的提升推动了数学家发展新的推理风格， 抑制算法信息并调用数学对象，从而抽象掉了对象被表征的细节。 目标是在不陷入繁重的计算细节的情况下获得强大的「概念」理解， -但这可能导致数学定理在直接计算的解读上干脆就是 **错误** 的。 +但这可能导致数学定理在直接计算的解读上干脆就是 **错误** 的。 -当前的研究计划包括关于**观测类型论（Observational Type Theory）** -和**立方类型论（Cubical Type Theory）**的研究，旨在扩展类型理论， +当前的研究计划包括关于 **观测类型论（Observational Type Theory）** +和 **立方类型论（Cubical Type Theory）** 的研究，旨在扩展类型理论， 以便允许对涉及函数外延、商，等等的强制转换进行归约。 但解决方案并不明朗，而 Lean 的底层演算法则对此类归约也不支持。 @@ -724,7 +724,7 @@ was an equivalence relation to start with, then for all ``a`` and 当然，当 ``r`` 是等价关系时，商集的结构是最常用的。给定上面的 ``r``， 如果我们根据法则 ``r' a b`` 当且仅当 ``Quot.mk r a = Quot.mk r b`` 定义 ``r'``， 那么显然 ``r'`` 就是一个等价关系。事实上，``r'`` 是函数 ``a ↦ quot.mk r a`` -的**核（Kernel）**。公理 ``Quot.sound`` 表明 ``r a b`` 蕴含 ``r' a b``。 +的 **核（Kernel）** 。公理 ``Quot.sound`` 表明 ``r a b`` 蕴含 ``r' a b``。 使用 ``Quot.lift`` 和 ``Quot.ind``，我们可以证明 ``r'`` 是包含 ``r`` 的最小的等价关系， 意思就是，如果 ``r''`` 是包含 ``r`` 的任意等价关系，则 ``r' a b`` 蕴含 ``r'' a b``。 特别地，如果 ``r`` 开始就是一个等价关系，那么对任意 ``a`` 和 ``b``，我们都有 @@ -736,7 +736,7 @@ notion of a *setoid*, which is simply a type with an associated equivalence relation: --> -为支持这种通用使用案例，标准库定义了 **广集（Setoid）** 的概念， +为支持这种通用使用案例，标准库定义了 **广集（Setoid）** 的概念， 它只是一个带有与之关联的等价关系的类型： ```lean @@ -829,7 +829,7 @@ the relevant equivalence relation: --> 回顾一下标准库中的 ``α × β`` 代表类型 ``α`` 和 ``β`` 的笛卡尔积。 -为了说明商的用法，让我们将类型为 ``α`` 的元素构成的**无序对（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 diff --git a/dependent_type_theory.md b/dependent_type_theory.md index d3221db..5e9b9cc 100644 --- a/dependent_type_theory.md +++ b/dependent_type_theory.md @@ -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 @@ -488,7 +488,7 @@ any value ``x`` to the value ``t``. Here are some more examples --> -从另一个表达式创建函数的过程称为**lambda 抽象**。假设你有一个变量 ``x : α`` 和一个表达式 ``t : β``，那么表达式 ``fun (x : α) => t`` 或者 ``λ (x : α) => t`` 是一个类型为 ``α → β`` 的对象。这个从 ``α`` 到 ``β`` 的函数把任意 ``x`` 映射到 ``t``。 +从另一个表达式创建函数的过程称为 **lambda 抽象** 。假设你有一个变量 ``x : α`` 和一个表达式 ``t : β``，那么表达式 ``fun (x : α) => t`` 或者 ``λ (x : α) => t`` 是一个类型为 ``α → β`` 的对象。这个从 ``α`` 到 ``β`` 的函数把任意 ``x`` 映射到 ``t``。 这有些例子： @@ -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 : β``。回到前面的例子，为清晰起见给绑定变量重命名，注意以下表达式的类型: @@ -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`` 所需的类型: diff --git a/induction_and_recursion.md b/induction_and_recursion.md index 6b8e8f8..a05cbcc 100644 --- a/induction_and_recursion.md +++ b/induction_and_recursion.md @@ -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 也可以处理更复杂的模式匹配形式，其中从属类型的参数对各种情况构成了额外的约束。这种 **依值模式匹配** 的例子在[依值模式匹配](#依值模式匹配)一节中考虑。 -如前所述，参数 ``{n : Nat}`` 是模式匹配的一部分，因为它不能在整个定义中保持固定。在以前的 Lean 版本中，用户经常发现必须包含这些额外的判别符是很麻烦的。因此，Lean 4 实现了一个新特性，**判别精炼（discriminant refinement）**，它自动为我们包含了这些额外的判别。 +如前所述，参数 ``{n : Nat}`` 是模式匹配的一部分，因为它不能在整个定义中保持固定。在以前的 Lean 版本中，用户经常发现必须包含这些额外的判别符是很麻烦的。因此，Lean 4 实现了一个新特性， **判别精炼（discriminant refinement）** ，它自动为我们包含了这些额外的判别。 ```lean # inductive Vector (α : Type u) : Nat → Type u diff --git a/inductive_types.md b/inductive_types.md index 8e52c1f..0396225 100644 --- a/inductive_types.md +++ b/inductive_types.md @@ -167,7 +167,7 @@ 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`` 到自然数的函数： @@ -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 := @@ -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`类似，但大前提发生在小前提之前。 @@ -1790,7 +1790,7 @@ An inductive family is an indexed family of types defined by a simultaneous induction of the following form: --> -我们几乎已经完成了对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 @@ -1987,9 +1987,9 @@ inductive types is of the form 我们已经通过例子描述了归纳类型和它们的语法。本节为那些对公理基础感兴趣的人提供额外的信息。 -我们已经看到，归纳类型的构造子需要**参量**（parameter，与argument都有「参数」译义，为区别此处译为参量）——即在整个归纳构造过程中保持固定的参数——和**索引**，即同时在构造中的类型类的参数。每个构造子都应该有一个类型，其中的参数类型是由先前定义的类型、参量和索引类型以及当前正在定义的归纳族建立起来的。要求是，如果后者存在，它只**严格正向**出现。这意味着它所出现的构造子的任何参数都是一个依值箭头类型，其中定义中的归纳类型只作为结果类型出现，其中的索引是以常量和先前的参数来给出。 +我们已经看到，归纳类型的构造子需要 **参量** （parameter，与argument都有「参数」译义，为区别此处译为参量）——即在整个归纳构造过程中保持固定的参数——和 **索引** ，即同时在构造中的类型类的参数。每个构造子都应该有一个类型，其中的参数类型是由先前定义的类型、参量和索引类型以及当前正在定义的归纳族建立起来的。要求是，如果后者存在，它只 **严格正向** 出现。这意味着它所出现的构造子的任何参数都是一个依值箭头类型，其中定义中的归纳类型只作为结果类型出现，其中的索引是以常量和先前的参数来给出。 -既然一个归纳类型对于某些 ``u`` 来说存在于在 ``Sort u`` 中，那么我们有理由问**哪些**宇宙层次的 ``u`` 可以被实例化。归纳类型类 ``C`` 的定义中的每个构造子 ``c`` 的形式为 +既然一个归纳类型对于某些 ``u`` 来说存在于在 ``Sort u`` 中，那么我们有理由问 **哪些** 宇宙层次的 ``u`` 可以被实例化。归纳类型类 ``C`` 的定义中的每个构造子 ``c`` 的形式为 ``` c : (a : α) → (b : β[a]) → C a p[a,b] @@ -2081,7 +2081,7 @@ where each one refers to the other(s). 我们现在考虑两个经常有用的归纳类型的推广，Lean 通过「编译」它们来支持上述更原始的归纳类型种类。换句话说，Lean 解析了更一般的定义，在此基础上定义了辅助的归纳类型，然后使用辅助类型来定义我们真正想要的类型。下一章将介绍Lean 的方程编译器，它需要有效地利用这些类型。尽管如此，在这里描述这些声明还是有意义的，因为它们是普通归纳定义的直接变形。 -首先，Lean 支持**相互定义**的归纳类型。这个想法是，我们可以同时定义两个（或更多）归纳类型，其中每个类型都指代其他类型。 +首先，Lean 支持 **相互定义** 的归纳类型。这个想法是，我们可以同时定义两个（或更多）归纳类型，其中每个类型都指代其他类型。 ```lean mutual @@ -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`` 的构造子。 -导入文件 ``Bar/Baz/Blah.olean``，其中的描述是相对于Lean**搜索路径**解释的。关于如何确定搜索路径的信息可以在[文档](https://lean-lang.org/documentation/)中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。 +导入文件 ``Bar/Baz/Blah.olean``，其中的描述是相对于Lean **搜索路径** 解释的。关于如何确定搜索路径的信息可以在[文档](https://lean-lang.org/documentation/)中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。 导入是传递性的。换句话说，如果你导入了 ``Foo``，并且 ``Foo`` 导入了 ``Bar``，那么你也可以访问 ``Bar`` 的内容，而不需要明确导入它。 @@ -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 @@ -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 设置选项的机制，它并 **不** 遵循这种模式：选项 **只能** 在局部设置，也就是说，它们的范围总是限制在当前小节或当前文件中。 -事实证明，第一个代码块中的所有命令实际上都是命令**宏**，翻译成更通用的 `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 @@ -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) @@ -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 @@ -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 : α) : γ := diff --git a/introduction.md b/introduction.md index 7e4b07e..e8031ac 100644 --- a/introduction.md +++ b/introduction.md @@ -23,7 +23,7 @@ lengthy computation, in which case verifying the truth of the theorem requires v it is supposed to do. --> -**形式验证（Formal Verification）**是指使用逻辑和计算方法来验证用精确的数学术语表达的命题。 + **形式验证（Formal Verification）** 是指使用逻辑和计算方法来验证用精确的数学术语表达的命题。 这包括普通的数学定理，以及硬件或软件、网络协议、机械和混合系统中的形式命题。 在实践中，验证数学命题和验证系统的正确性之间很类似：形式验证用数学术语描述硬件和软件系统， 在此基础上验证其命题的正确性，这就像定理证明的过程。相反，一个数学定理的证明可能需要冗长的计算， @@ -51,11 +51,11 @@ mathematical bounds, or finding mathematical objects. A calculation can be viewe too, help establish mathematical claims. --> -**自动定理证明（Automated theorem proving）**着眼于「寻找」证明。归结（Resolution）定理证明器、 -**表格法（tableau）**定理证明器、**快速可满足性求解器（Fast satisfiability solvers）** + **自动定理证明（Automated theorem proving）** 着眼于「寻找」证明。归结（Resolution）定理证明器、 + **表格法（tableau）** 定理证明器、 **快速可满足性求解器（Fast satisfiability solvers）** 等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法； 还有些系统为特定的语言和问题提供搜索和决策程序， -例如整数或实数上的线性或非线性表达式；像**SMT（Satisfiability modulo theories）** +例如整数或实数上的线性或非线性表达式；像 **SMT（Satisfiability modulo theories）** 这样的架构将通用的搜索方法与特定领域的程序相结合； 计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段， 这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。 @@ -72,7 +72,7 @@ allows you to obtain deeper and more complex proofs. --> 自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有 bug， -而且很难保证它们所提供的结果是正确的。相比之下，**交互式定理证明器（Interactive theorem proving）** +而且很难保证它们所提供的结果是正确的。相比之下， **交互式定理证明器（Interactive theorem proving）** 侧重于「验证」证明，要求每个命题都有合适的公理基础的证明来支持。 这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明， 一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的「证明对象」， @@ -86,7 +86,7 @@ axiomatic proofs. The goal is to support both mathematical reasoning and reasoni claims in both domains. --> -**Lean 定理证明器**旨在融合交互式和自动定理证明， + **Lean 定理证明器** 旨在融合交互式和自动定理证明， 它将自动化工具和方法置于一个支持用户交互和构建完整公理化证明的框架中。 它的目标是支持数学推理和复杂系统的推理，并验证这两个领域的命题。 @@ -101,7 +101,7 @@ aspects of the system will make an appearance here. Lean 的底层逻辑有一个计算的解释，与此同时 Lean 可以被视为一种编程语言。 更重要的是，它可以被看作是一个编写具有精确语义的程序的系统， -以及对程序所表示的计算功能进行推理。Lean 中也有机制使它能够作为它自己的**元编程语言**， +以及对程序所表示的计算功能进行推理。Lean 中也有机制使它能够作为它自己的 **元编程语言** ， 这意味着你可以使用 Lean 本身实现自动化和扩展 Lean 的功能。 Lean 的这些方面将在本教程的配套教程 [Lean 4函数式编程](https://www.leanprover.cn/fp-lean-zh/)中进行探讨，本书只介绍计算方面。 @@ -160,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 不仅可以定义数学对象和表达依值类型论的数学断言，而且还可以作为一种语言来编写证明。 -稍后我们将看到，构造逻辑中**有**某些情况允许「排中律」和「双重否定消除律」等，而 Lean 支持在这种情况下使用经典推理，而不依赖于排中律。 +稍后我们将看到，构造逻辑中 **有** 某些情况允许「排中律」和「双重否定消除律」等，而 Lean 支持在这种情况下使用经典推理，而不依赖于排中律。 Lean 中使用的公理的完整列表见[公理与计算](./axioms_and_computation.md)。 diff --git a/structures_and_records.md b/structures_and_records.md index 500fa98..d7641cc 100644 --- a/structures_and_records.md +++ b/structures_and_records.md @@ -36,7 +36,7 @@ for defining instances of a given structure. 我们已经看到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 为定义给定结构体的实例提供了方便的符号。 @@ -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 a34f8b0..bd609a4 100644 --- a/tactics.md +++ b/tactics.md @@ -29,7 +29,7 @@ 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 相区分。 @@ -1222,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 := 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