From 8836bd79943359b9b6e7ff146834ccf55a9980f8 Mon Sep 17 00:00:00 2001 From: Oling Cat Date: Tue, 18 Jun 2024 22:43:44 +0800 Subject: [PATCH] Format spaces --- SUMMARY.md | 1 - dependent_type_theory.md | 170 ++++++++++++++--------------- interacting_with_lean.md | 112 +++++++++---------- introduction.md | 18 ++-- propositions_and_proofs.md | 152 +++++++++++++------------- quantifiers_and_equality.md | 134 ++++++++++++----------- tactics.md | 209 ++++++++++++++++++------------------ type_classes.md | 4 +- 8 files changed, 398 insertions(+), 402 deletions(-) diff --git a/SUMMARY.md b/SUMMARY.md index fa71aa9..eef366d 100644 --- a/SUMMARY.md +++ b/SUMMARY.md @@ -15,7 +15,6 @@ - [Type Classes](./type_classes.md) - [The Conversion Tactic Mode](./conv.md) - [Axioms and Computation](./axioms_and_computation.md) - --> # Lean 4 定理证明 diff --git a/dependent_type_theory.md b/dependent_type_theory.md index b99a9df..265f663 100644 --- a/dependent_type_theory.md +++ b/dependent_type_theory.md @@ -31,7 +31,7 @@ numbers. For those who like precise definitions, a Lean natural number is an arbitrary-precision unsigned integer. --> -“类型论”得名于其中每个表达式都有一个*类型*。举例：在一个给定的语境中，``x + 0``可能表示一个自然数，``f``可能表示一个定义在自然数上的函数。Lean中的自然数是任意精度的无符号整数。 +「类型论」得名于其中每个表达式都有一个*类型*。举例：在一个给定的语境中，``x + 0`` 可能表示一个自然数，``f`` 可能表示一个定义在自然数上的函数。Lean中的自然数是任意精度的无符号整数。 -位于``/-``和``-/``之间的文本组成了一个注释块，会被Lean的编译器忽略。类似地，两条横线`--`后面也是注释。注释块可以嵌套，这样就可以“注释掉”一整块代码，这和任何程序语言都是一样的。 +位于 ``/-`` 和 ``-/`` 之间的文本组成了一个注释块，会被 Lean 的编译器忽略。类似地，两条横线`--`后面也是注释。注释块可以嵌套，这样就可以「注释掉」一整块代码，这和任何程序语言都是一样的。 -``def``关键字声明工作环境中的新常量符号。在上面的例子中，`def m : Nat := 1`定义了一个`Nat`类型的新常量`m`，其值为`1`。``#check``命令要求Lean给出它的类型，用于向系统询问信息的辅助命令都以井号(#)开头。`#eval`命令让Lean计算给出的表达式。你应该试试自己声明一些常量和检查一些表达式的类型。 +``def`` 关键字声明工作环境中的新常量符号。在上面的例子中，`def m : Nat := 1`定义了一个 `Nat` 类型的新常量 `m`，其值为 `1`。``#check`` 命令要求 Lean 给出它的类型，用于向系统询问信息的辅助命令都以井号(#)开头。`#eval`命令让 Lean 计算给出的表达式。你应该试试自己声明一些常量和检查一些表达式的类型。 -简单类型论的强大之处在于，你可以从其他类型中构建新的类型。例如，如果``a``和``b``是类型，``a -> b``表示从``a``到``b``的函数类型，``a × b``表示由``a``元素与``b``元素配对构成的类型，也称为*笛卡尔积*。注意`×`是一个Unicode符号，可以使用``\times``或简写``\tim``来输入。合理使用Unicode提高了易读性，所有现代编辑器都支持它。在Lean标准库中，你经常看到希腊字母表示类型，Unicode符号`→`是`->`的更紧凑版本。 +简单类型论的强大之处在于，你可以从其他类型中构建新的类型。例如，如果 ``a`` 和 ``b`` 是类型，``a -> b`` 表示从 ``a`` 到 ``b`` 的函数类型，``a × b`` 表示由 ``a`` 元素与 ``b`` 元素配对构成的类型，也称为*笛卡尔积*。注意`×`是一个 Unicode 符号，可以使用 ``\times`` 或简写 ``\tim`` 来输入。合理使用 Unicode 提高了易读性，所有现代编辑器都支持它。在 Lean 标准库中，你经常看到希腊字母表示类型，Unicode符号`→`是`->`的更紧凑版本。 -> 注：取一个类型为``Nat × Nat → Nat``的函数，然后“重定义”它，让它变成``Nat → Nat → Nat``类型，这个过程被称作*柯里化*（currying）。 +> 注：取一个类型为 ``Nat × Nat → Nat`` 的函数，然后「重定义」它，让它变成 ``Nat → Nat → Nat`` 类型，这个过程被称作*柯里化*（currying）。 -如果你有``m : Nat``和``n : Nat``，那么``(m, n)``表示``m``和``n``组成的有序对，其类型为``Nat × Nat``。这个方法可以制造自然数对。反过来，如果你有``p : Nat × Nat``，之后你可以写``p.1 : Nat``和``p.2 : Nat``。这个方法用于提取它的两个组件。 +如果你有 ``m : Nat`` 和 ``n : Nat``，那么 ``(m, n)`` 表示 ``m`` 和 ``n`` 组成的有序对，其类型为 ``Nat × Nat``。这个方法可以制造自然数对。反过来，如果你有 ``p : Nat × Nat``，之后你可以写 ``p.1 : Nat`` 和 ``p.2 : Nat``。这个方法用于提取它的两个组件。 -Lean所依据的依值类型论对简单类型论的其中一项升级是，类型本身（如``Nat``和``Bool``这些东西）也是对象，因此也具有类型。 +Lean所依据的依值类型论对简单类型论的其中一项升级是，类型本身（如 ``Nat`` 和 ``Bool`` 这些东西）也是对象，因此也具有类型。 ```lean #check Nat -- Type @@ -282,7 +282,7 @@ You can see that each one of the expressions above is an object of type ``Type``. You can also declare new constants for types: --> -上面的每个表达式都是类型为``Type``的对象。你也可以为类型声明新的常量: +上面的每个表达式都是类型为 ``Type`` 的对象。你也可以为类型声明新的常量: ```lean def α : Type := Nat @@ -303,7 +303,7 @@ As the example above suggests, you have already seen an example of a function of ``Type → Type → Type``, namely, the Cartesian product `Prod`: --> -正如上面所示，你已经看到了一个类型为``Type → Type → Type``的函数例子，即笛卡尔积 `Prod`： +正如上面所示，你已经看到了一个类型为 ``Type → Type → Type`` 的函数例子，即笛卡尔积 `Prod`： ```lean def α : Type := Nat @@ -321,7 +321,7 @@ Here is another example: given any type ``α``, the type ``List α`` denotes the type of lists of elements of type ``α``. --> -这里有另一个例子：给出任意类型``α``，那么类型``List α``是类型为``α``的元素的列表的类型。 +这里有另一个例子：给出任意类型 ``α``，那么类型 ``List α`` 是类型为 ``α`` 的元素的列表的类型。 ```lean def α : Type := Nat @@ -335,7 +335,7 @@ Given that every expression in Lean has a type, it is natural to ask: what type does ``Type`` itself have? --> -看起来Lean中任何表达式都有一个类型，因此你可能会想到：``Type``自己的类型是什么？ +看起来 Lean 中任何表达式都有一个类型，因此你可能会想到：``Type`` 自己的类型是什么？ ```lean #check Type -- Type 1 @@ -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 @@ -366,7 +366,7 @@ that there is a ``Type n`` for every natural number ``n``. ``Type`` is an abbreviation for ``Type 0``: --> -可以将``Type 0``看作是一个由“小”或“普通”类型组成的宇宙。然后，``Type 1``是一个更大的类型范围，其中包含``Type 0``作为一个元素，而``Type 2``是一个更大的类型范围，其中包含``Type 1``作为一个元素。这个列表是不确定的，所以对于每个自然数``n``都有一个``Type n``。``Type``是``Type 0``的缩写： +可以将 ``Type 0`` 看作是一个由「小」或「普通」类型组成的宇宙。然后，``Type 1`` 是一个更大的类型范围，其中包含 ``Type 0`` 作为一个元素，而 ``Type 2`` 是一个更大的类型范围，其中包含 ``Type 1`` 作为一个元素。这个列表是不确定的，所以对于每个自然数 ``n`` 都有一个 ``Type n``。``Type`` 是 ``Type 0`` 的缩写： ```lean #check Type @@ -380,7 +380,7 @@ along the y-axis represents a change in what is sometimes referred to as "degree". --> -下表可能有助于具体说明所讨论的关系。行方向代表宇宙的变化，列方向代表有时被称为“度”的变化。 +下表可能有助于具体说明所讨论的关系。行方向代表宇宙的变化，列方向代表有时被称为「度」的变化。 | | | | | | | |:------:|:-------------:|:-------------:|:---------------:|:----------------------:|:---:| @@ -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 @@ -409,7 +409,7 @@ Here ``u`` is a variable ranging over type levels. The output of the similarly polymorphic: --> -这里``u``是一个遍取类型级别的变量。``#check``命令的输出意味着当``α``有类型``Type n``时，``List α``也有类型``Type n``。函数``Prod``具有类似的多态性： +这里 ``u`` 是一个遍取类型级别的变量。``#check`` 命令的输出意味着当 ``α`` 有类型 ``Type n`` 时，``List α`` 也有类型 ``Type n``。函数 ``Prod`` 具有类似的多态性： ```lean #check Prod -- Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v) @@ -434,7 +434,7 @@ def F (α : Type u) : Type u := Prod α α You can avoid the universe command by providing the universe parameters when defining F. --> -可以通过在定义F时提供universe参数来避免使用`universe`命令： +可以通过在定义 F 时提供 universe 参数来避免使用 `universe` 命令： ```lean def F.{u} (α : Type u) : Type u := Prod α α @@ -471,7 +471,7 @@ Lean提供 `fun` (或 `λ`)关键字用于从给定表达式创建函数，如 You can evaluate a lambda function by passing the required parameters: --> -你可以通过传递所需的参数来计算lambda函数： +你可以通过传递所需的参数来计算 lambda 函数： ```lean #eval (λ x : Nat => x + 5) 10 -- 15 @@ -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``。 这有些例子： @@ -507,9 +507,9 @@ 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抽象的项来描述: +一些数学上常见的函数运算的例子可以用 lambda 抽象的项来描述: ```lean def f (n : Nat) : String := toString n @@ -534,9 +534,9 @@ You can pass functions as parameters and by giving them names `f` and `g` you can then use those functions in the implementation: --> -看看这些表达式的意思。表达式``fun x : Nat => x``代表``Nat``上的恒等函数，表达式``fun x : Nat => true``表示一个永远输出``true``的常值函数，表达式``fun x : Nat => g (f x)``表示``f``和``g``的复合。一般来说，你可以省略类型注释，让Lean自己推断它。因此你可以写``fun x => g (f x)``来代替``fun x : Nat => g (f x)``。 +看看这些表达式的意思。表达式 ``fun x : Nat => x`` 代表 ``Nat`` 上的恒等函数，表达式 ``fun x : Nat => true`` 表示一个永远输出 ``true`` 的常值函数，表达式 ``fun x : Nat => g (f x)`` 表示 ``f`` 和 ``g`` 的复合。一般来说，你可以省略类型注释，让 Lean 自己推断它。因此你可以写 ``fun x => g (f x)`` 来代替 ``fun x : Nat => g (f x)``。 -你可以以函数作为参数，通过给它们命名`f`和`g`，你可以在实现中使用这些函数： +你可以以函数作为参数，通过给它们命名 `f` 和 `g`，你可以在实现中使用这些函数： ```lean #check fun (g : String → Bool) (f : Nat → String) (x : Nat) => g (f x) @@ -576,11 +576,11 @@ renaming bound variables for clarity, notice the types of the following expressions: --> -这个表达式表示一个接受三个类型``α``，``β``和``γ``和两个函数``g : β → γ``和``f : α → β``，并返回的``g``和``f``的复合的函数。(理解这个函数的类型需要理解依值积类型，下面将对此进行解释。) +这个表达式表示一个接受三个类型 ``α``，``β`` 和 ``γ`` 和两个函数 ``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 : β``。回到前面的例子，为清晰起见给绑定变量重命名，注意以下表达式的类型: +注意到项 ``t : α → β`` 应用到项 ``s : α`` 上导出了表达式 ``t s : β``。回到前面的例子，为清晰起见给绑定变量重命名，注意以下表达式的类型: ```lean #check (fun x : Nat => x) 1 -- Nat @@ -600,7 +600,7 @@ In fact, more should be true: applying the expression ``(fun x : Nat => x)`` to ``1`` should "return" the value ``1``. And, indeed, it does: --> -表达式``(fun x : Nat => x) 1``的类型是``Nat``。实际上，应用``(fun x : Nat => x)``到``1``上返回的值是``1``。 +表达式 ``(fun x : Nat => x) 1`` 的类型是 ``Nat``。实际上，应用 ``(fun x : Nat => x)`` 到 ``1`` 上返回的值是 ``1``。 ```lean #eval (fun x : Nat => x) 1 -- 1 @@ -622,7 +622,7 @@ use the command `#eval` to execute expressions, and it is the preferred way of testing your functions. --> -稍后你将看到这些项是如何计算的。现在，请注意这是依值类型论的一个重要特征：每个项都有一个计算行为，并支持“标准化”的概念。从原则上讲，两个可以化约为相同形式的项被称为“定义等价”。它们被Lean的类型检查器认为是“相同的”，并且Lean尽其所能地识别和支持这些识别结果。 +稍后你将看到这些项是如何计算的。现在，请注意这是依值类型论的一个重要特征：每个项都有一个计算行为，并支持「标准化」的概念。从原则上讲，两个可以化约为相同形式的项被称为「定义等价」。它们被 Lean 的类型检查器认为是「相同的」，并且 Lean 尽其所能地识别和支持这些识别结果。 Lean是个完备的编程语言。它有一个生成二进制可执行文件的编译器，和一个交互式解释器。你可以用`#eval`命令执行表达式，这也是测试你的函数的好办法。 @@ -643,8 +643,8 @@ treats all foreign functions as opaque constants. You will learn later that there are some other differences between the two commands. --> -> 注意到`#eval`和`#reduce`*不是*等价的。`#eval`命令首先把Lean表达式编译成中间表示（intermediate representation, IR）然后用一个解释器来执行这个IR。某些内建类型（例如，`Nat`、`String`、`Array`）在IR中有更有效率的表示。IR支持使用对Lean不透明的外部函数。 -> ``#reduce``命令建立在一个规约引擎上，类似于在Lean的可信内核中使用的那个，它是负责检查和验证表达式和证明正确性的那一部分。它的效率不如``#eval``，且将所有外部函数视为不透明的常量。之后你将了解到这两个命令之间还有其他一些差异。 +> 注意到`#eval`和`#reduce`*不是*等价的。`#eval`命令首先把 Lean 表达式编译成中间表示（intermediate representation, IR）然后用一个解释器来执行这个IR。某些内建类型（例如，`Nat`、`String`、`Array`）在 IR 中有更有效率的表示。IR支持使用对 Lean 不透明的外部函数。 +> ``#reduce`` 命令建立在一个规约引擎上，类似于在 Lean 的可信内核中使用的那个，它是负责检查和验证表达式和证明正确性的那一部分。它的效率不如 ``#eval``，且将所有外部函数视为不透明的常量。之后你将了解到这两个命令之间还有其他一些差异。 -``def``关键字提供了一个声明新对象的重要方式。 +``def`` 关键字提供了一个声明新对象的重要方式。 ```lean def double (x : Nat) : Nat := @@ -672,7 +672,7 @@ result of the call is `x + x`, so it is returning type `Nat`. You can then invoke this function using: --> -这很类似其他编程语言中的函数。名字`double`被定义为一个函数，它接受一个类型为`Nat`的输入参数`x`，其结果是`x + x`，因此它返回类型`Nat`。然后你可以调用这个函数: +这很类似其他编程语言中的函数。名字 `double` 被定义为一个函数，它接受一个类型为 `Nat` 的输入参数 `x`，其结果是`x + x`，因此它返回类型 `Nat`。然后你可以调用这个函数: ```lean # def double (x : Nat) : Nat := @@ -685,7 +685,7 @@ In this case you can think of `def` as a kind of named `lambda`. The following yields the same result: --> -在这种情况下你可以把`def`想成一种`lambda`。下面给出了相同的结果： +在这种情况下你可以把 `def` 想成一种 `lambda`。下面给出了相同的结果： ```lean def double : Nat → Nat := @@ -699,7 +699,7 @@ You can omit the type declarations when Lean has enough information to infer it. Type inference is an important part of Lean: --> -当Lean有足够的信息来推断时，你可以省略类型声明。类型推断是Lean的重要组成部分: +当 Lean 有足够的信息来推断时，你可以省略类型声明。类型推断是 Lean 的重要组成部分: ```lean def double := @@ -718,9 +718,9 @@ The right hand side `bar` can be any expression, not just a lambda. So `def` can also be used to simply name a value like this: --> -定义的一般形式是``def foo : α := bar``，其中``α``是表达式``bar``返回的类型。Lean通常可以推断类型``α``，但是精确写出它可以澄清你的意图，并且如果定义的右侧没有匹配你的类型，Lean将标记一个错误。 +定义的一般形式是 ``def foo : α := bar``，其中 ``α`` 是表达式 ``bar`` 返回的类型。Lean通常可以推断类型 ``α``，但是精确写出它可以澄清你的意图，并且如果定义的右侧没有匹配你的类型，Lean将标记一个错误。 -`bar`可以是任何一个表达式，不只是一个lambda表达式。因此`def`也可以用于给一些值命名，例如： +`bar` 可以是任何一个表达式，不只是一个 lambda 表达式。因此 `def` 也可以用于给一些值命名，例如： ```lean @@ -732,7 +732,7 @@ def pi := 3.141592654 that adds two natural numbers: --> -`def`可以接受多个输入参数。比如定义两自然数之和： +`def` 可以接受多个输入参数。比如定义两自然数之和： ```lean def add (x y : Nat) := @@ -763,9 +763,9 @@ parameter to `add`. You can use other more interesting expressions inside a `def`: --> -注意到这里我们使用了`double`函数来创建`add`函数的第一个参数。 +注意到这里我们使用了 `double` 函数来创建 `add` 函数的第一个参数。 -你还可以在`def`中写一些更有趣的表达式： +你还可以在 `def` 中写一些更有趣的表达式： ```lean def greater (x y : Nat) := @@ -826,11 +826,11 @@ so long as they each take one parameter, and so long as the type of output of the second matches the input of the first. For example: --> -这句代码的意思是：函数`compose`首先接受任何两个函数作为参数，这其中两个函数各自接受一个输入。类型`β → γ`和`α → β`意思是要求第二个函数的输出类型必须与第一个函数的输入类型匹配，否则这两个函数将无法复合。 +这句代码的意思是：函数 `compose` 首先接受任何两个函数作为参数，这其中两个函数各自接受一个输入。类型`β → γ`和`α → β`意思是要求第二个函数的输出类型必须与第一个函数的输入类型匹配，否则这两个函数将无法复合。 -`compose`再接受一个类型为`α`的参数作为第二个函数（这里叫做`f`）的输入，通过这个函数之后的返回结果类型为`β`，再作为第一个函数（这里叫做`g`）的输入。第一个函数返回类型为`γ`，这就是`compose`函数最终返回的类型。 +`compose` 再接受一个类型为`compose` 再参数作为第二个函数（这里叫做 `f`）的输入，通过这个函数之后的返回结果类型为`β`，再作为第一个函数（这里叫做 `g`）的输入。第一个函数返回类型为`γ`，这就是 `compose` 函数最终返回的类型。 -`compose`可以在任意的类型`α β γ`上使用，它可以复合任意两个函数，只要前一个的输出类型是后一个的输入类型。举例： +`compose` 可以在任意的类型`α β γ`上使用，它可以复合任意两个函数，只要前一个的输出类型是后一个的输入类型。举例： ```lean # def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ := @@ -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 @@ -875,9 +875,9 @@ Here, ``twice_double x`` is definitionally equal to the term ``(x + x) * (x + x) You can combine multiple assignments by chaining ``let`` statements: --> -这里``twice_double x``定义等价于``(x + x) * (x + x)``。 +这里 ``twice_double x`` 定义等价于 ``(x + x) * (x + x)``。 -你可以连续使用多个``let``命令来进行多次替换： +你可以连续使用多个 ``let`` 命令来进行多次替换： ```lean #check let y := 2 + 2; let z := y + y; z * z -- Nat @@ -888,7 +888,7 @@ You can combine multiple assignments by chaining ``let`` statements: The ``;`` can be omitted when a line break is used. --> -换行可以省略分号``;``。 +换行可以省略分号 ``;``。 ```lean def t (x : Nat) : Nat := @@ -910,7 +910,7 @@ why the definition of ``foo`` below type checks, but the definition of ``bar`` does not. --> -表达式``let a := t1; t2``的意思很类似``(fun a => t2) t1``，但是这两者并不一样。前者中你要把``t2``中每一个``a``的实例考虑成``t1``的一个缩写。后者中``a``是一个变量，表达式``fun a => t2``不依赖于``a``的取值而可以单独具有意义。作为一个对照，考虑为什么下面的``foo``定义是合法的，但``bar``不行（因为在确定了``x``所属的``a``是什么之前，是无法让它``+ 2``的）。 +表达式 ``let a := t1; t2`` 的意思很类似 ``(fun a => t2) t1``，但是这两者并不一样。前者中你要把 ``t2`` 中每一个 ``a`` 的实例考虑成 ``t1`` 的一个缩写。后者中 ``a`` 是一个变量，表达式 ``fun a => t2`` 不依赖于 ``a`` 的取值而可以单独具有意义。作为一个对照，考虑为什么下面的 ``foo`` 定义是合法的，但 ``bar`` 不行（因为在确定了 ``x`` 所属的 ``a`` 是什么之前，是无法让它 ``+ 2`` 的）。 ```lean def foo := let a := Nat; fun x : a => x + 2 @@ -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) @@ -966,7 +966,7 @@ def doThrice (h : α → α) (x : α) : α := You can declare variables of any type, not just ``Type`` itself: --> -你可以声明任意类型的变量，不只是``Type``类型： +你可以声明任意类型的变量，不只是 ``Type`` 类型： ```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 @@ -1031,7 +1031,7 @@ which allows you to declare new variables incrementally. 当一个小节结束后，变量不再发挥作用。 -你不需要缩进一个小节中的行。你也不需要命名一个小节，也就是说，你可以使用一个匿名的``section`` /``end``对。但是，如果你确实命名了一个小节，你必须使用相同的名字关闭它。小节也可以嵌套，这允许你逐步增加声明新变量。 +你不需要缩进一个小节中的行。你也不需要命名一个小节，也就是说，你可以使用一个匿名的 ``section`` /``end`` 对。但是，如果你确实命名了一个小节，你必须使用相同的名字关闭它。小节也可以嵌套，这允许你逐步增加声明新变量。 -Lean可以让你把定义放进一个“命名空间”（``namespace``）里，并且命名空间也是层次化的： +Lean可以让你把定义放进一个「命名空间」（``namespace``）里，并且命名空间也是层次化的： ```lean namespace Foo @@ -1096,11 +1096,11 @@ For example, Lean groups definitions and theorems involving lists into a namespace ``List``. --> -当你声明你在命名空间``Foo``中工作时，你声明的每个标识符都有一个前缀``Foo.``。在打开的命名空间中，可以通过较短的名称引用标识符，但是关闭命名空间后，必须使用较长的名称。与`section`不同，命名空间需要一个名称。只有一个匿名命名空间在根级别上。 +当你声明你在命名空间 ``Foo`` 中工作时，你声明的每个标识符都有一个前缀 ``Foo.``。在打开的命名空间中，可以通过较短的名称引用标识符，但是关闭命名空间后，必须使用较长的名称。与 `section` 不同，命名空间需要一个名称。只有一个匿名命名空间在根级别上。 -``open``命令使你可以在当前使用较短的名称。通常，当你导入一个模块时，你会想打开它包含的一个或多个命名空间，以访问短标识符。但是，有时你希望将这些信息保留在一个完全限定的名称中，例如，当它们与你想要使用的另一个命名空间中的标识符冲突时。因此，命名空间为你提供了一种在工作环境中管理名称的方法。 +``open`` 命令使你可以在当前使用较短的名称。通常，当你导入一个模块时，你会想打开它包含的一个或多个命名空间，以访问短标识符。但是，有时你希望将这些信息保留在一个完全限定的名称中，例如，当它们与你想要使用的另一个命名空间中的标识符冲突时。因此，命名空间为你提供了一种在工作环境中管理名称的方法。 -例如，Lean把和列表相关的定义和定理都放在了命名空间``List``之中。 +例如，Lean把和列表相关的定义和定理都放在了命名空间 ``List`` 之中。 ```lean #check List.nil @@ -1111,7 +1111,7 @@ a namespace ``List``. The command ``open List`` allows you to use the shorter names: --> -``open List``命令允许你使用短一点的名字： +``open List`` 命令允许你使用短一点的名字： ```lean open List @@ -1186,15 +1186,15 @@ namespace. Similarly, if you use an ``open`` command within a namespace, its effects disappear when the namespace is closed. --> -与小节一样，嵌套的名称空间必须按照打开的顺序关闭。命名空间和小节有不同的用途：命名空间组织数据，小节声明变量，以便在定义中插入。小节对于分隔``set_option``和``open``等命令的范围也很有用。 +与小节一样，嵌套的名称空间必须按照打开的顺序关闭。命名空间和小节有不同的用途：命名空间组织数据，小节声明变量，以便在定义中插入。小节对于分隔 ``set_option`` 和 ``open`` 等命令的范围也很有用。 -然而，在许多方面，``namespace ... end``结构块和``section ... end``表现出来的特征是一样的。尤其是你在命名空间中使用``variable``命令时，它的作用范围被限制在命名空间里。类似地，如果你在命名空间中使用``open``命令，它的效果在命名空间关闭后消失。 +然而，在许多方面，``namespace ... end`` 结构块和 ``section ... end`` 表现出来的特征是一样的。尤其是你在命名空间中使用 ``variable`` 命令时，它的作用范围被限制在命名空间里。类似地，如果你在命名空间中使用 ``open`` 命令，它的效果在命名空间关闭后消失。 -## 依值类型论“依赖”着什么? +## 依值类型论「依赖」着什么? -简单地说，类型可以依赖于参数。你已经看到了一个很好的例子：类型``List α``依赖于参数``α``，而这种依赖性是区分``List Nat``和``List Bool``的关键。另一个例子，考虑类型``Vector α n``，即长度为``n``的``α``元素的向量类型。这个类型取决于*两个*参数：向量中元素的类型``α : Type``和向量的长度``n : Nat``。 +简单地说，类型可以依赖于参数。你已经看到了一个很好的例子：类型 ``List α`` 依赖于参数 ``α``，而这种依赖性是区分 ``List Nat`` 和 ``List Bool`` 的关键。另一个例子，考虑类型 ``Vector α n``，即长度为 ``n`` 的 ``α`` 元素的向量类型。这个类型取决于*两个*参数：向量中元素的类型 ``α : Type`` 和向量的长度 ``n : Nat``。 -假设你希望编写一个函数``cons``，它在列表的开头插入一个新元素。``cons``应该有什么类型？这样的函数是*多态的*（polymorphic）：你期望``Nat``，``Bool``或任意类型``α``的``cons``函数表现相同的方式。因此，将类型作为``cons``的第一个参数是有意义的，因此对于任何类型``α``，``cons α``是类型``α``列表的插入函数。换句话说，对于每个``α``，``cons α``是将元素``a : α``插入列表``as : List α``的函数，并返回一个新的列表，因此有``cons α a as : List α``。 +假设你希望编写一个函数 ``cons``，它在列表的开头插入一个新元素。``cons`` 应该有什么类型？这样的函数是*多态的*（polymorphic）：你期望 ``Nat``，``Bool`` 或任意类型 ``α`` 的 ``cons`` 函数表现相同的方式。因此，将类型作为 ``cons`` 的第一个参数是有意义的，因此对于任何类型 ``α``，``cons α`` 是类型 ``α`` 列表的插入函数。换句话说，对于每个 ``α``，``cons α`` 是将元素 ``a : α`` 插入列表 ``as : List α`` 的函数，并返回一个新的列表，因此有 ``cons α a as : List α``。 -很明显，``cons α``具有类型``α → List α → List α``，但是``cons``具有什么类型？如果我们假设是``Type → α → list α → list α``，那么问题在于，这个类型表达式没有意义：``α``没有任何的所指，但它实际上指的是某个类型``Type``。换句话说，*假设*``α : Type``是函数的首个参数，之后的两个参数的类型是``α``和``List α``，它们依赖于首个参数``α``。 +很明显，``cons α`` 具有类型 ``α → List α → List α``，但是 ``cons`` 具有什么类型？如果我们假设是 ``Type → α → list α → list α``，那么问题在于，这个类型表达式没有意义：``α`` 没有任何的所指，但它实际上指的是某个类型 ``Type``。换句话说，*假设*``α : Type`` 是函数的首个参数，之后的两个参数的类型是 ``α`` 和 ``List α``，它们依赖于首个参数 ``α``。 ```lean def cons (α : Type) (a : α) (as : List α) : List α := @@ -1264,13 +1264,13 @@ and the difference between the round and curly braces will be explained momentarily. --> -这就是*依值函数类型*，或者*依值箭头类型*的一个例子。给定``α : Type``和``β : α → Type``，把``β``考虑成``α``之上的类型族，也就是说，对于每个``a : α``都有类型``β a``。在这种情况下，类型``(a : α) → β a``表示的是具有如下性质的函数``f``的类型：对于每个``a : α``，``f a``是``β a``的一个元素。换句话说，``f``返回值的类型取决于其输入。 +这就是*依值函数类型*，或者*依值箭头类型*的一个例子。给定 ``α : Type`` 和 ``β : α → Type``，把 ``β`` 考虑成 ``α`` 之上的类型族，也就是说，对于每个 ``a : α`` 都有类型 ``β a``。在这种情况下，类型 ``(a : α) → β a`` 表示的是具有如下性质的函数 ``f`` 的类型：对于每个 ``a : α``，``f a`` 是 ``β a`` 的一个元素。换句话说，``f`` 返回值的类型取决于其输入。 -注意到``(a : α) → β``对于任意表达式``β : Type``都有意义。当``β``的值依赖于``a``（例如，在前一段的表达式``β a``），``(a : α) → β``表示一个依值函数类型。当``β``的值不依赖于``a``，``(a : α) → β``与类型``α → β``无异。实际上，在依值类型论（以及Lean）中，``α → β``表达的意思就是当``β``的值不依赖于``a``时的``(a : α) → β``。【注】 +注意到 ``(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`函数。``@``符号以及圆括号和花括号之间的区别将在后面解释。 +回到列表的例子，你可以使用`#check`命令来检查下列的 `List` 函数。``@`` 符号以及圆括号和花括号之间的区别将在后面解释。 ```lean #check @List.cons -- {α : Type u_1} → α → List α → List α @@ -1290,7 +1290,7 @@ dependent pair. The `⟨` and `⟩` characters may be typed with `\langle` and `\rangle` or `\<` and `\>`, respectively. --> -就像依值函数类型``(a : α) → β a``通过允许``β``依赖``α``从而推广了函数类型``α → β``，依值笛卡尔积类型``(a : α) × β a``同样推广了笛卡尔积``α × β``。依值积类型又称为*sigma*类型，可写成`Σ a : α, β a`。你可以用`⟨a, b⟩`或者`Sigma.mk a b`来创建依值对。 `⟨`和`⟩`符号可以用`\langle`和`\rangle`或者`\<`和`\>`来输入. +就像依值函数类型 ``(a : α) → β a`` 通过允许 ``β`` 依赖 ``α`` 从而推广了函数类型 ``α → β``，依值笛卡尔积类型 ``(a : α) × β a`` 同样推广了笛卡尔积 ``α × β``。依值积类型又称为*sigma*类型，可写成`Σ a : α, β a`。你可以用`⟨a, b⟩`或者`Sigma.mk a b`来创建依值对。 `⟨`和`⟩`符号可以用`\langle`和`\rangle`或者`\<`和`\>`来输入. ```lean universe u v @@ -1316,7 +1316,7 @@ def h2 (x : Nat) : Nat := The functions `f` and `g` above denote the same function. --> -函数`f`和`g`表达的是同样的函数。 +函数 `f` 和 `g` 表达的是同样的函数。 -由于构造器对类型是多态的【注】，我们需要重复插入类型``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中，我们使用下划线``_``来指定系统应该自动填写信息。这就是所谓的“隐参数”。 +这是依值类型论的一个主要特征：项包含大量信息，而且通常可以从上下文推断出一些信息。在 Lean 中，我们使用下划线 ``_`` 来指定系统应该自动填写信息。这就是所谓的「隐参数」。 ```lean # universe u @@ -1441,7 +1441,7 @@ declaration of the variables. We can also use this device in function definitions: --> -唯一改变的是变量声明中``α : Type u``周围的花括号。我们也可以在函数定义中使用这个技巧： +唯一改变的是变量声明中 ``α : Type u`` 周围的花括号。我们也可以在函数定义中使用这个技巧： ```lean universe u @@ -1464,9 +1464,9 @@ Variables can also be specified as implicit when they are declared with the ``variable`` command: --> -这使得``ident``的第一个参数是隐式的。从符号上讲，这隐藏了类型的说明，使它看起来好像``ident``只是接受任何类型的参数。事实上，函数``id``在标准库中就是以这种方式定义的。我们在这里选择一个非传统的名字只是为了避免名字的冲突。 +这使得 ``ident`` 的第一个参数是隐式的。从符号上讲，这隐藏了类型的说明，使它看起来好像 ``ident`` 只是接受任何类型的参数。事实上，函数 ``id`` 在标准库中就是以这种方式定义的。我们在这里选择一个非传统的名字只是为了避免名字的冲突。 -``variable``命令也可以用这种技巧来来把变量变成隐式的： +``variable`` 命令也可以用这种技巧来来把变量变成隐式的： ```lean universe u @@ -1504,11 +1504,11 @@ used to specify the desired types of the expressions ``id`` and ``List.nil``: --> -此处定义的``ident``和上面那个效果是一样的。 +此处定义的 ``ident`` 和上面那个效果是一样的。 -Lean有非常复杂的机制来实例化隐参数，我们将看到它们可以用来推断函数类型、谓词，甚至证明。实例化这些“洞”或“占位符”的过程通常被称为**繁饰**（Elaboration）。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像``id``或``List.nil``这样的表达式被认为是“多态的”，因为它可以在不同的上下文中具有不同的含义。 +Lean有非常复杂的机制来实例化隐参数，我们将看到它们可以用来推断函数类型、谓词，甚至证明。实例化这些「洞」或「占位符」的过程通常被称为**繁饰**（Elaboration）。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像 ``id`` 或 ``List.nil`` 这样的表达式被认为是「多态的」，因为它可以在不同的上下文中具有不同的含义。 -可以通过写``(e : T)``来指定表达式``e``的类型``T``。这就指导Lean的繁饰器在试图解决隐式参数时使用值``T``作为``e``的类型。在下面的第二个例子中，这种机制用于指定表达式``id``和``List.nil``所需的类型: +可以通过写 ``(e : T)`` 来指定表达式 ``e`` 的类型 ``T``。这就指导 Lean 的繁饰器在试图解决隐式参数时使用值 ``T`` 作为 ``e`` 的类型。在下面的第二个例子中，这种机制用于指定表达式 ``id`` 和 ``List.nil`` 所需的类型: ```lean #check List.nil -- List ?m @@ -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 @@ -1542,7 +1542,7 @@ notation ``@foo`` denotes the same function with all the arguments made explicit. --> -然而，有时我们可能会发现自己处于这样一种情况：我们已经声明了函数的参数是隐式的，但现在想显式地提供参数。如果``foo``是有隐参数的函数，符号``@foo``表示所有参数都是显式的该函数。 +然而，有时我们可能会发现自己处于这样一种情况：我们已经声明了函数的参数是隐式的，但现在想显式地提供参数。如果 ``foo`` 是有隐参数的函数，符号 ``@foo`` 表示所有参数都是显式的该函数。 ```lean #check @id -- {α : Sort u_1} → α → α @@ -1553,4 +1553,4 @@ made explicit. #check @id Bool true -- Bool ``` -第一个``#check``命令给出了标识符的类型``id``，没有插入任何占位符。而且，输出表明第一个参数是隐式的。 +第一个 ``#check`` 命令给出了标识符的类型 ``id``，没有插入任何占位符。而且，输出表明第一个参数是隐式的。 diff --git a/interacting_with_lean.md b/interacting_with_lean.md index e33ca70..20e25ac 100644 --- a/interacting_with_lean.md +++ b/interacting_with_lean.md @@ -3,7 +3,7 @@ Interacting with Lean ===================== --> -与Lean交互 +与 Lean 交互 ===================== -你现在已经熟悉了依值类型论的基本原理，它既是一种定义数学对象的语言，也是一种构造证明的语言。现在你缺少一个定义新数据类型的机制。下一章介绍*归纳数据类型*的概念来帮你完成这个目标。但首先，在这一章中，我们从类型论的机制中抽身出来，探索与Lean交互的一些实用性问题。 +你现在已经熟悉了依值类型论的基本原理，它既是一种定义数学对象的语言，也是一种构造证明的语言。现在你缺少一个定义新数据类型的机制。下一章介绍*归纳数据类型*的概念来帮你完成这个目标。但首先，在这一章中，我们从类型论的机制中抽身出来，探索与 Lean 交互的一些实用性问题。 -并非所有的知识都能马上对你有用。可以略过这一节，然后在必要时再回到这一节以了解Lean的特性。 +并非所有的知识都能马上对你有用。可以略过这一节，然后在必要时再回到这一节以了解 Lean 的特性。 -导入文件``Bar/Baz/Blah.olean``，其中的描述是相对于Lean**搜索路径**解释的。关于如何确定搜索路径的信息可以在[文档](https://lean-lang.org/documentation/)中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。 +导入文件 ``Bar/Baz/Blah.olean``，其中的描述是相对于Lean**搜索路径**解释的。关于如何确定搜索路径的信息可以在[文档](https://lean-lang.org/documentation/)中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。 -导入是传递性的。换句话说，如果你导入了 ``Foo``，并且``Foo``导入了``Bar``，那么你也可以访问``Bar``的内容，而不需要明确导入它。 +导入是传递性的。换句话说，如果你导入了 ``Foo``，并且 ``Foo`` 导入了 ``Bar``，那么你也可以访问 ``Bar`` 的内容，而不需要明确导入它。 -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 := @@ -221,7 +221,7 @@ open String We can prevent the shorter alias from being created by using the ``protected`` keyword: --> -我们可以通过使用``protected``关键字来阻止创建较短的别名： +我们可以通过使用 ``protected`` 关键字来阻止创建较短的别名： ```lean protected def Foo.bar : Nat := 1 @@ -241,7 +241,7 @@ The ``open`` command admits variations. The command 这通常用于像`Nat.rec`和`Nat.recOn`这样的名称，以防止普通名称的重载。 -``open``命令允许变量。命令 +``open`` 命令允许变量。命令 ```lean open Nat (succ zero gcd) @@ -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 @@ -279,7 +279,7 @@ creates aliases renaming ``Nat.mul`` to ``times`` and ``Nat.add`` to ``plus``. It is sometimes useful to ``export`` aliases from one namespace to another, or to the top level. The command --> -将`Nat.mul`更名为`times`，`Nat.add`更名为`plus`。 +将`Nat.mul`更名为 `times`，`Nat.add`更名为 `plus`。 有时，将别名从一个命名空间导出到另一个命名空间，或者导出到上一层是很有用的。命令 @@ -294,7 +294,7 @@ available. If this command is used outside a namespace, the aliases are exported to the top level. --> -在当前命名空间中为``succ``、``add``和``sub``创建别名，这样无论何时命名空间被打开，这些别名都可以使用。如果这个命令在名字空间之外使用，那么这些别名会被输出到上一层。 +在当前命名空间中为 ``succ``、``add`` 和 ``sub`` 创建别名，这样无论何时命名空间被打开，这些别名都可以使用。如果这个命令在名字空间之外使用，那么这些别名会被输出到上一层。 -Lean的主要功能是把用户的输入翻译成形式化的表达式，由内核检查其正确性，然后存储在环境中供以后使用。但是有些命令对环境有其他的影响，或者给环境中的对象分配属性，定义符号，或者声明类型族的实例，如[类型族](./type_classes.md)一章所述。这些命令大多具有全局效应，也就是说，它们不仅在当前文件中保持有效，而且在任何导入它的文件中也保持有效。然而，这类命令通常支持``local``修饰符，这表明它们只在当前``section``或``namespace``关闭前或当前文件结束前有效。 +Lean的主要功能是把用户的输入翻译成形式化的表达式，由内核检查其正确性，然后存储在环境中供以后使用。但是有些命令对环境有其他的影响，或者给环境中的对象分配属性，定义符号，或者声明类型族的实例，如[类型族](./type_classes.md)一章所述。这些命令大多具有全局效应，也就是说，它们不仅在当前文件中保持有效，而且在任何导入它的文件中也保持有效。然而，这类命令通常支持 ``local`` 修饰符，这表明它们只在当前 ``section`` 或 ``namespace`` 关闭前或当前文件结束前有效。 在[简化](./tactics.md#简化)一节中，我们看到可以用`[simp]`属性来注释定理，这使它们可以被简化器使用。下面的例子定义了列表的前缀关系，证明了这种关系是自反的，并为该定理分配了`[simp]`属性。 @@ -346,7 +346,7 @@ The simplifier then proves ``isPrefix [1, 2, 3] [1, 2, 3]`` by rewriting it to ` One can also assign the attribute any time after the definition takes place: --> -然后简化器通过将其改写为``True``来证明``isPrefix [1, 2, 3] [1, 2, 3]``。 +然后简化器通过将其改写为 ``True`` 来证明 ``isPrefix [1, 2, 3] [1, 2, 3]``。 你也可以在做出定义后的任何时候分配属性： @@ -365,7 +365,7 @@ imports the one in which the declaration occurs. Adding the ``local`` modifier restricts the scope: --> -在所有这些情况下，该属性在任何导入该声明的文件中仍然有效。添加``local``修饰符可以限制范围： +在所有这些情况下，该属性在任何导入该声明的文件中仍然有效。添加 ``local`` 修饰符可以限制范围： ```lean # def isPrefix (l₁ : List α) (l₂ : List α) : Prop := @@ -394,7 +394,7 @@ be explained in [Chapter Type Classes](./type_classes.md), works by assigning an ``[instance]`` attribute to the associated definition. --> -另一个例子，我们可以使用`instance`命令来给`isPrefix`关系分配符号`≤`。该命令将在[类型族](./type_classes.md)中解释，它的工作原理是给相关定义分配一个`[instance]`属性。 +另一个例子，我们可以使用 `instance` 命令来给 `isPrefix` 关系分配符号`≤`。该命令将在[类型族](./type_classes.md)中解释，它的工作原理是给相关定义分配一个`[instance]`属性。 ```lean def isPrefix (l₁ : List α) (l₂ : List α) : Prop := @@ -442,7 +442,7 @@ their scope is always restricted to the current section or current file. --> -在下面的[符号](#符号)一节中，我们将讨论Lean定义符号的机制，并看到它们也支持``local``修饰符。然而，在[设置选项](#设置选项)一节中，我们将讨论Lean设置选项的机制，它并**不**遵循这种模式：选项**只能**在局部设置，也就是说，它们的范围总是限制在当前小节或当前文件中。 +在下面的[符号](#符号)一节中，我们将讨论 Lean 定义符号的机制，并看到它们也支持 ``local`` 修饰符。然而，在[设置选项](#设置选项)一节中，我们将讨论 Lean 设置选项的机制，它并**不**遵循这种模式：选项**只能**在局部设置，也就是说，它们的范围总是限制在当前小节或当前文件中。 -在[隐参数](./dependent_type_theory.md#隐参数)一节中，我们看到，如果Lean将术语``t``的类型显示为``{x : α} → β x``，那么大括号表示``x``被标记为``t``的*隐参数*。这意味着每当你写``t``时，就会插入一个占位符，或者说“洞”，这样``t``就会被``@t _``取代。如果你不希望这种情况发生，你必须写``@t``来代替。 +在[隐参数](./dependent_type_theory.md#隐参数)一节中，我们看到，如果 Lean 将术语 ``t`` 的类型显示为 ``{x : α} → β x``，那么大括号表示 ``x`` 被标记为 ``t`` 的*隐参数*。这意味着每当你写 ``t`` 时，就会插入一个占位符，或者说「洞」，这样 ``t`` 就会被 ``@t _`` 取代。如果你不希望这种情况发生，你必须写 ``@t`` 来代替。 -请注意，隐参数是急于插入的。假设我们定义一个函数``f (x : Nat) {y : Nat} (z : Nat)``。那么，当我们写表达式`f 7`时，没有进一步的参数，它会被解析为`f 7 _`。Lean提供了一个较弱的注释，``{{y : ℕ}}``，它指定了一个占位符只应在后一个显式参数之前添加。这个注释也可以写成``⦃y : Nat⦄``，其中的unicode括号输入方式为``\{{``和``\}}``。有了这个注释，表达式`f 7`将被解析为原样，而`f 7 3`将被解析为``f 7 _ 3``，就像使用强注释一样。 +请注意，隐参数是急于插入的。假设我们定义一个函数 ``f (x : Nat) {y : Nat} (z : Nat)``。那么，当我们写表达式`f 7`时，没有进一步的参数，它会被解析为`f 7 _`。Lean提供了一个较弱的注释，``{{y : ℕ}}``，它指定了一个占位符只应在后一个显式参数之前添加。这个注释也可以写成 ``⦃y : Nat⦄``，其中的 unicode 括号输入方式为 ``\{{`` 和 ``\}}``。有了这个注释，表达式`f 7`将被解析为原样，而`f 7 3`将被解析为 ``f 7 _ 3``，就像使用强注释一样。 为了说明这种区别，请看下面的例子，它表明一个自反的欧几里得关系既是对称的又是传递的。 @@ -531,7 +531,7 @@ otherwise too many implicit arguments are inserted. The problem goes away if we use weak implicit arguments: --> -这些结果被分解成几个小步骤。``th1``表明自反和欧氏的关系是对称的，``th2``表明对称和欧氏的关系是传递的。然后``th3``结合这两个结果。但是请注意，我们必须手动禁用`th1`、`th2`和`euclr`中的隐参数，否则会插入太多的隐参数。如果我们使用弱隐式参数，这个问题就会消失： +这些结果被分解成几个小步骤。``th1`` 表明自反和欧氏的关系是对称的，``th2`` 表明对称和欧氏的关系是传递的。然后 ``th3`` 结合这两个结果。但是请注意，我们必须手动禁用 `th1`、`th2` 和 `euclr` 中的隐参数，否则会插入太多的隐参数。如果我们使用弱隐式参数，这个问题就会消失： ```lean def reflexive {α : Type u} (r : α → α → Prop) : Prop := @@ -577,7 +577,7 @@ brackets, ``[`` and ``]``. These are used for type classes, as explained in [Chapter Type Classes](./type_classes.md). --> -还有第三种隐式参数，用方括号表示，``[``和``]``。这些是用于类型族的，在[类型族](./type_classes.md)中解释。 +还有第三种隐式参数，用方括号表示，``[`` 和 ``]``。这些是用于类型族的，在[类型族](./type_classes.md)中解释。 -Lean中的标识符可以包括任何字母数字字符，包括希腊字母（除了∀、Σ和λ，它们在依值类型论中有特殊的含义）。它们还可以包括下标，可以通过输入``\_``，然后再输入所需的下标字符。 +Lean中的标识符可以包括任何字母数字字符，包括希腊字母（除了∀、Σ和λ，它们在依值类型论中有特殊的含义）。它们还可以包括下标，可以通过输入 ``\_``，然后再输入所需的下标字符。 Lean的解析器是可扩展的，也就是说，我们可以定义新的符号。 -Lean的语法可以由用户在各个层面进行扩展和定制，从基本的“mixfix”符号到自定义的繁饰器。事实上，所有内置的语法都是使用对用户开放的相同机制和API进行解析和处理的。 在本节中，我们将描述和解释各种扩展点。 +Lean的语法可以由用户在各个层面进行扩展和定制，从基本的「mixfix」符号到自定义的繁饰器。事实上，所有内置的语法都是使用对用户开放的相同机制和 API 进行解析和处理的。 在本节中，我们将描述和解释各种扩展点。 虽然在编程语言中引入新的符号是一个相对罕见的功能，有时甚至因为它有可能使代码变得模糊不清而被人诟病，但它是形式化的一个宝贵工具，可以在代码中简洁地表达各自领域的既定惯例和符号。 除了基本的符号之外，Lean的能力是将普通的样板代码分解成（良好的）宏，并嵌入整个定制的特定领域语言（DSL，domain specific language），对子问题进行高效和可读的文本编码，这对程序员和证明工程师都有很大的好处。 @@ -668,9 +668,9 @@ can make this more precise by looking at the commands the above unfold to: 语法： -运算符种类（其“结合方式”） : 解析优先级 " 新的或现有的符号 " => 这个符号应该翻译成的函数 +运算符种类（其「结合方式」） : 解析优先级 " 新的或现有的符号 " => 这个符号应该翻译成的函数 -优先级是一个自然数，描述一个运算符与它的参数结合的“紧密程度”，编码操作的顺序。我们可以通过查看上述展开的命令来使之更加精确： +优先级是一个自然数，描述一个运算符与它的参数结合的「紧密程度」，编码操作的顺序。我们可以通过查看上述展开的命令来使之更加精确： ```lean notation:65 lhs:65 " + " rhs:66 => HAdd.hAdd lhs rhs @@ -698,7 +698,7 @@ operand, so `a ^ b ^ c` *can* be parsed as `a ^ (b ^ c)`. Note that if we used `notation` directly to introduce an infix notation like --> -事实证明，第一个代码块中的所有命令实际上都是命令**宏**，翻译成更通用的`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,9 +718,9 @@ 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*语法，自由地混合记号和占位符。 +如上所述，`notation` 命令允许我们定义任意的*mixfix*语法，自由地混合记号和占位符。 ```lean # set_option quotPrecheck false @@ -733,7 +733,7 @@ Placeholders without precedence default to `0`, i.e. they accept notations of an If two notations overlap, we again apply the longest parse rule: --> -没有优先级的占位符默认为`0`，也就是说，它们接受任何优先级的符号来代替它们。如果两个记号重叠，我们再次应用最长解析规则： +没有优先级的占位符默认为 `0`，也就是说，它们接受任何优先级的符号来代替它们。如果两个记号重叠，我们再次应用最长解析规则： ```lean notation:65 a " + " b:66 " + " c:66 => a + b - c @@ -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 的**美观打印**显示项的方式。下列选项的输入值为真或假： ``` 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，你将不可避免地需要使用库中的定义和定理。回想一下，文件开头的``import``命令会从其他文件中导入之前编译的结果，而且导入是传递的；如果你导入了``Foo``，``Foo``又导入了``Bar``，那么``Bar``的定义和定理也可以被你利用。但是打开一个命名空间的行为，提供了更短的名字，并没有延续下去。在每个文件中，你需要打开你想使用的命名空间。 +为了有效地使用Lean，你将不可避免地需要使用库中的定义和定理。回想一下，文件开头的 ``import`` 命令会从其他文件中导入之前编译的结果，而且导入是传递的；如果你导入了 ``Foo``，``Foo`` 又导入了 ``Bar``，那么 ``Bar`` 的定义和定理也可以被你利用。但是打开一个命名空间的行为，提供了更短的名字，并没有延续下去。在每个文件中，你需要打开你想使用的命名空间。 -一般来说，你必须熟悉库和它的内容，这样你就知道有哪些定理、定义、符号和资源可供你使用。下面我们将看到Lean的编辑器模式也可以帮助你找到你需要的东西，但直接研究库的内容往往是不可避免的。Lean的标准库在GitHub上。 +一般来说，你必须熟悉库和它的内容，这样你就知道有哪些定理、定义、符号和资源可供你使用。下面我们将看到 Lean 的编辑器模式也可以帮助你找到你需要的东西，但直接研究库的内容往往是不可避免的。Lean的标准库在 GitHub 上。 - [https://github.com/leanprover/lean4/tree/master/src/Init](https://github.com/leanprover/lean4/tree/master/src/Init) @@ -988,9 +988,9 @@ we rely on descriptive names where the different components are separated by `_`s. Often the name of theorem simply describes the conclusion: --> -你可以使用GitHub的浏览器界面查看这些目录和文件的内容。如果你在自己的电脑上安装了Lean，你可以在``lean``文件夹中找到这个库，用你的文件管理器探索它。每个文件顶部的注释标题提供了额外的信息。 +你可以使用 GitHub 的浏览器界面查看这些目录和文件的内容。如果你在自己的电脑上安装了Lean，你可以在 ``lean`` 文件夹中找到这个库，用你的文件管理器探索它。每个文件顶部的注释标题提供了额外的信息。 -Lean库的开发者遵循一般的命名准则，以便于猜测你所需要的定理的名称，或者在支持Lean模式的编辑器中用Tab自动补全来找到它，这将在下一节讨论。标识符一般是``camelCase``，而类型是`CamelCase`。对于定理的名称，我们依靠描述性的名称，其中不同的组成部分用`_`分开。通常情况下，定理的名称只是描述结论。 +Lean库的开发者遵循一般的命名准则，以便于猜测你所需要的定理的名称，或者在支持 Lean 模式的编辑器中用 Tab 自动补全来找到它，这将在下一节讨论。标识符一般是 ``camelCase``，而类型是 `CamelCase`。对于定理的名称，我们依靠描述性的名称，其中不同的组成部分用 `_` 分开。通常情况下，定理的名称只是描述结论。 ```lean #check Nat.succ_ne_zero @@ -1012,7 +1012,7 @@ a namespace with the same name as the type under definition. For example, the product type comes with the following operations: --> -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 @@ -1034,7 +1034,7 @@ also instances of inductive types, and so we tend to use dot notation for them as well: --> -第一个用于构建一个对，而接下来的两个，``Prod.fst``和``Prod.snd``，投影两个元素。最后一个，``Prod.rec``，提供了另一种机制，用两个元素的函数来定义乘积上的函数。像``Prod.rec``这样的名字是*受保护*的，这意味着即使``Prod``名字空间是打开的，也必须使用全名。 +第一个用于构建一个对，而接下来的两个，``Prod.fst`` 和 ``Prod.snd``，投影两个元素。最后一个，``Prod.rec``，提供了另一种机制，用两个元素的函数来定义乘积上的函数。像 ``Prod.rec`` 这样的名字是*受保护*的，这意味着即使 ``Prod`` 名字空间是打开的，也必须使用全名。 由于命题即类型的对应原则，逻辑连接词也是归纳类型的实例，因此我们也倾向于对它们使用点符号： @@ -1066,7 +1066,7 @@ However, functions such as `compose` are still quite verbose to define. Note tha polymorphic `compose` is even more verbose than the one previously defined. --> -在上一节中，我们已经展示了隐参数是如何使函数更方便使用的。然而，像`compose`这样的函数在定义时仍然相当冗长。宇宙多态的`compose`比之前定义的函数还要啰嗦。 +在上一节中，我们已经展示了隐参数是如何使函数更方便使用的。然而，像 `compose` 这样的函数在定义时仍然相当冗长。宇宙多态的 `compose` 比之前定义的函数还要啰嗦。 ```lean universe u v w @@ -1079,7 +1079,7 @@ def compose {α : Type u} {β : Type v} {γ : Type w} You can avoid the `universe` command by providing the universe parameters when defining `compose`. --> -你可以通过在定义`compose`时提供宇宙参数来避免使用`universe`命令。 +你可以通过在定义 `compose` 时提供宇宙参数来避免使用 `universe` 命令。 ```lean def compose.{u, v, w} @@ -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,9 +1113,9 @@ 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`命令将其禁用。 +虽然我们很喜欢这个功能，并且在实现 Lean 时广泛使用，但我们意识到有些用户可能会对它感到不舒服。因此，你可以使用`set_option autoBoundImplicitLocal false`命令将其禁用。 -在Lean 3 stdlib中，我们发现了许多[例子](https://github.com/leanprover/lean/blob/master/library/init/category/reader.lean#L39)包含丑陋的`@`+`_`惯用法。当我们的预期类型是一个带有隐参数的函数类型，而我们有一个常量（例子中的`reader_t.pure`）也需要隐参数时，就会经常使用这个惯用法。在Lean 4中，繁饰器自动引入了lambda来消除隐参数。我们仍在探索这一功能并分析其影响，但到目前为止的结果是非常积极的。下面是上面链接中使用Lean 4隐式lambda的例子。 +在Lean 3 stdlib中，我们发现了许多[例子](https://github.com/leanprover/lean/blob/master/library/init/category/reader.lean#L39)包含丑陋的`@`+`_` 惯用法。当我们的预期类型是一个带有隐参数的函数类型，而我们有一个常量（例子中的`reader_t.pure`）也需要隐参数时，就会经常使用这个惯用法。在Lean 4中，繁饰器自动引入了 lambda 来消除隐参数。我们仍在探索这一功能并分析其影响，但到目前为止的结果是非常积极的。下面是上面链接中使用Lean 4隐式 lambda 的例子。 ```lean # variable (ρ : Type) (m : Type → Type) [Monad m] @@ -1164,7 +1164,7 @@ a lambda expression with `{}` or `[]` binder annotations. Here are few examples --> -用户可以通过使用`@`或用包含`{}`或`[]`的约束标记编写的lambda表达式来禁用隐式lambda功能。下面是几个例子 +用户可以通过使用`@`或用包含`{}`或`[]`的约束标记编写的 lambda 表达式来禁用隐式 lambda 功能。下面是几个例子 -在Lean 3中，我们可以通过使用小括号从infix运算符中创建简单的函数。例如，`(+1)`是`fun x, x + 1`的语法糖。在Lean 4中，我们用`·`作为占位符来扩展这个符号。这里有几个例子： +在Lean 3中，我们可以通过使用小括号从 infix 运算符中创建简单的函数。例如，`(+1)`是`fun x, x + 1`的语法糖。在Lean 4中，我们用`·`作为占位符来扩展这个符号。这里有几个例子： ```lean # namespace ex3 @@ -1260,7 +1260,7 @@ As in Lean 3, the notation is activated using parentheses, and the lambda abstra The collection is interrupted by nested parentheses. In the following example, two different lambda expressions are created. --> -如同在Lean 3中，符号是用圆括号激活的，lambda抽象是通过收集嵌套的`·`创建的。这个集合被嵌套的小括号打断。在下面的例子中创建了两个不同的lambda表达式。 +如同在Lean 3中，符号是用圆括号激活的，lambda抽象是通过收集嵌套的`·`创建的。这个集合被嵌套的小括号打断。在下面的例子中创建了两个不同的 lambda 表达式。 ```lean #check (Prod.mk · (· + 1)) @@ -1285,7 +1285,7 @@ infer it. Named arguments also improve the readability of your code by identifying what each argument represents. --> -被命名参数使你可以通过用参数的名称而不是参数列表中的位置来指定参数。 如果你不记得参数的顺序但知道它们的名字，你可以以任何顺序传入参数。当Lean未能推断出一个隐参数时，你也可以提供该参数的值。被命名参数还可以通过识别每个参数所代表的内容来提高你的代码的可读性。 +被命名参数使你可以通过用参数的名称而不是参数列表中的位置来指定参数。 如果你不记得参数的顺序但知道它们的名字，你可以以任何顺序传入参数。当 Lean 未能推断出一个隐参数时，你也可以提供该参数的值。被命名参数还可以通过识别每个参数所代表的内容来提高你的代码的可读性。 ```lean def sum (xs : List Nat) := @@ -1345,7 +1345,7 @@ You can use `..` to provide missing explicit arguments as `_`. This feature combined with named arguments is useful for writing patterns. Here is an example: --> -你可以使用`..`来提供缺少的显式参数作为`_`。这个功能与被命名参数相结合，对编写模式很有用。下面是一个例子： +你可以使用`..`来提供缺少的显式参数作为 `_`。这个功能与被命名参数相结合，对编写模式很有用。下面是一个例子： ```lean inductive Term where @@ -1368,7 +1368,7 @@ Ellipses are also useful when explicit arguments can be automatically inferred by Lean, and we want to avoid a sequence of `_`s. --> -当显式参数可以由Lean自动推断时，省略号也很有用，而我们想避免一连串的`_`。 +当显式参数可以由 Lean 自动推断时，省略号也很有用，而我们想避免一连串的 `_`。 ```lean example (f : Nat → Nat) (a b c : Nat) : f (a + b + c) = f (a + (b + c)) := diff --git a/introduction.md b/introduction.md index 9548104..279b5fc 100644 --- a/introduction.md +++ b/introduction.md @@ -74,7 +74,7 @@ aspects of Lean are described in the free online book, [Functional Programming i aspects of the system will make an appearance here. --> -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](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。 +本教程介绍的是 Lean 的当前版本：Lean 4。 -本书的目的是教你在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）的方法，可以用来支持灵活的代数推理。 -最后，你会学到Lean的一些特性，包括与系统交流的语言，和Lean提供的对复杂理论和数据的管理机制。 +最后，你会学到 Lean 的一些特性，包括与系统交流的语言，和 Lean 提供的对复杂理论和数据的管理机制。 在本书中你会见到类似下面这样的代码： @@ -164,7 +164,7 @@ that follow. You can open this book on VS Code by using the command "Lean 4: Ope --> -如果你在[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中打开本书。 致谢 --------------- diff --git a/propositions_and_proofs.md b/propositions_and_proofs.md index 099aa39..487dfc0 100644 --- a/propositions_and_proofs.md +++ b/propositions_and_proofs.md @@ -13,7 +13,7 @@ mathematical assertions and proofs in the language of dependent type theory as well. --> -前一章你已经看到了在Lean中定义对象和函数的一些方法。在本章中，我们还将开始解释如何用依值类型论的语言来编写数学命题和证明。 +前一章你已经看到了在 Lean 中定义对象和函数的一些方法。在本章中，我们还将开始解释如何用依值类型论的语言来编写数学命题和证明。 -对每个元素``p : Prop``，可以引入另一个类型``Proof p``，作为``p``的证明的类型。“公理”是这个类型中的常值。 +对每个元素 ``p : Prop``，可以引入另一个类型 ``Proof p``，作为 ``p`` 的证明的类型。「公理」是这个类型中的常值。 ```lean # def Implies (p q : Prop) : Prop := p → q @@ -85,7 +85,7 @@ We could represent this as follows: 然而，除了公理之外，我们还需要从旧证明中建立新证明的规则。例如，在许多命题逻辑的证明系统中，我们有肯定前件式（modus ponens）推理规则: -> 如果能证明``Implies p q``和``p``，则能证明``q``。 +> 如果能证明 ``Implies p q`` 和 ``p``，则能证明 ``q``。 我们可以如下地表示它： @@ -106,7 +106,7 @@ We could render this as follows: 命题逻辑的自然演绎系统通常也依赖于以下规则： -> 当假设``p``成立时，如果我们能证明``q``. 则我们能证明``Implies p q``. +> 当假设 ``p`` 成立时，如果我们能证明 ``q``. 则我们能证明 ``Implies p q``. 我们可以如下地表示它： @@ -205,32 +205,32 @@ proof assistant, is to help us to construct such a term, ``t``, and to verify that it is well-formed and has the correct type. --> -这个功能让我们可以合理地搭建断言和证明。确定表达式``t``是``p``的证明，只需检查``t``具有类型``Proof p``。 +这个功能让我们可以合理地搭建断言和证明。确定表达式 ``t`` 是 ``p`` 的证明，只需检查 ``t`` 具有类型 ``Proof p``。 -可以做一些简化。首先，我们可以通过将``Proof p``和``p``本身合并来避免重复地写``Proof``这个词。换句话说，只要我们有``p : Prop``，我们就可以把``p``解释为一种类型，也就是它的证明类型。然后我们可以把``t : p``读作``t``是``p``的证明。 +可以做一些简化。首先，我们可以通过将 ``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``。 +至少有两种将命题作为类型来思考的方法。对于那些对逻辑和数学中的构造主义者来说，这是对命题含义的忠实诠释：命题 ``p`` 代表了一种数据类型，即构成证明的数据类型的说明。``p`` 的证明就是正确类型的对象 ``t : p``。 -非构造主义者可以把它看作是一种简单的编码技巧。对于每个命题``p``，我们关联一个类型，如果``p``为假，则该类型为空，如果``p``为真，则有且只有一个元素，比如``*``。在后一种情况中，让我们说(与之相关的类型)``p``被*占据*（inhabited）。恰好，函数应用和抽象的规则可以方便地帮助我们跟踪``Prop``的哪些元素是被占据的。所以构造一个元素``t : p``告诉我们``p``确实是正确的。你可以把``p``的占据者想象成“``p``为真”的事实。对``p → q``的证明使用“``p``是真的”这个事实来得到“``q``是真的”这个事实。 +非构造主义者可以把它看作是一种简单的编码技巧。对于每个命题 ``p``，我们关联一个类型，如果 ``p`` 为假，则该类型为空，如果 ``p`` 为真，则有且只有一个元素，比如 ``*``。在后一种情况中，让我们说(与之相关的类型)``p`` 被*占据*（inhabited）。恰好，函数应用和抽象的规则可以方便地帮助我们跟踪 ``Prop`` 的哪些元素是被占据的。所以构造一个元素 ``t : p`` 告诉我们 ``p`` 确实是正确的。你可以把 ``p`` 的占据者想象成「``p`` 为真」的事实。对 ``p → q`` 的证明使用「``p`` 是真的」这个事实来得到「``q`` 是真的」这个事实。 -事实上，如果``p : Prop``是任何命题，那么Lean的内核将任意两个元素``t1 t2 : p``看作定义相等，就像它把``(fun x => t) s``和``t[s/x]``看作定义等价。这就是所谓的“证明无关性”（proof irrelevance）。这意味着，即使我们可以把证明``t : p``当作依值类型论语言中的普通对象，它们除了``p``是真的这一事实之外，没有其他信息。 +事实上，如果 ``p : Prop`` 是任何命题，那么 Lean 的内核将任意两个元素 ``t1 t2 : p`` 看作定义相等，就像它把 ``(fun x => t) s`` 和 ``t[s/x]`` 看作定义等价。这就是所谓的「证明无关性」（proof irrelevance）。这意味着，即使我们可以把证明 ``t : p`` 当作依值类型论语言中的普通对象，它们除了 ``p`` 是真的这一事实之外，没有其他信息。 -我们所建议的思考“命题即类型”范式的两种方式在一个根本性的方面有所不同。从构造的角度看，证明是抽象的数学对象，它被依值类型论中的合适表达式所*表示*。相反，如果我们从上述编码技巧的角度考虑，那么表达式本身并不表示任何有趣的东西。相反，是我们可以写下它们并检查它们是否有良好的类型这一事实确保了有关命题是真的。换句话说，表达式*本身*就是证明。 +我们所建议的思考「命题即类型」范式的两种方式在一个根本性的方面有所不同。从构造的角度看，证明是抽象的数学对象，它被依值类型论中的合适表达式所*表示*。相反，如果我们从上述编码技巧的角度考虑，那么表达式本身并不表示任何有趣的东西。相反，是我们可以写下它们并检查它们是否有良好的类型这一事实确保了有关命题是真的。换句话说，表达式*本身*就是证明。 -在下面的论述中，我们将在这两种说话方式之间来回切换，有时说一个表达式“构造”或“产生”或“返回”一个命题的证明，有时则简单地说它“是”这样一个证明。这类似于计算机科学家偶尔会模糊语法和语义之间的区别，有时说一个程序“计算”某个函数，有时又说该程序“是”该函数。 +在下面的论述中，我们将在这两种说话方式之间来回切换，有时说一个表达式「构造」或「产生」或「返回」一个命题的证明，有时则简单地说它「是」这样一个证明。这类似于计算机科学家偶尔会模糊语法和语义之间的区别，有时说一个程序「计算」某个函数，有时又说该程序「是」该函数。 -为了用依值类型论的语言正式表达一个数学断言，我们需要展示一个项``p : Prop``。为了*证明*该断言，我们需要展示一个项``t : p``。Lean的任务，作为一个证明助手，是帮助我们构造这样一个项``t``，并验证它的格式是否良好，类型是否正确。 +为了用依值类型论的语言正式表达一个数学断言，我们需要展示一个项 ``p : Prop``。为了*证明*该断言，我们需要展示一个项 ``t : p``。Lean的任务，作为一个证明助手，是帮助我们构造这样一个项 ``t``，并验证它的格式是否良好，类型是否正确。 -## 以“命题即类型”的方式工作 +## 以「命题即类型」的方式工作 -在“命题即类型”范式中，只涉及``→``的定理可以通过lambda抽象和应用来证明。在Lean中，``theorem``命令引入了一个新的定理： +在「命题即类型」范式中，只涉及 ``→`` 的定理可以通过 lambda 抽象和应用来证明。在 Lean 中，``theorem`` 命令引入了一个新的定理： ```lean variable {p : Prop} @@ -282,13 +282,13 @@ As with definitions, the ``#print`` command will show you the proof of a theorem. --> -这与上一章中常量函数的定义完全相同，唯一的区别是参数是``Prop``的元素，而不是``Type``的元素。直观地说，我们对``p → q → p``的证明假设``p``和``q``为真，并使用第一个假设(平凡地)建立结论``p``为真。 +这与上一章中常量函数的定义完全相同，唯一的区别是参数是 ``Prop`` 的元素，而不是 ``Type`` 的元素。直观地说，我们对 ``p → q → p`` 的证明假设 ``p`` 和 ``q`` 为真，并使用第一个假设(平凡地)建立结论 ``p`` 为真。 -请注意，``theorem``命令实际上是``def``命令的一个翻版：在命题和类型对应下，证明定理``p → q → p``实际上与定义关联类型的元素是一样的。对于内核类型检查器，这两者之间没有区别。 +请注意，``theorem`` 命令实际上是 ``def`` 命令的一个翻版：在命题和类型对应下，证明定理 ``p → q → p`` 实际上与定义关联类型的元素是一样的。对于内核类型检查器，这两者之间没有区别。 -然而，定义和定理之间有一些实用的区别。正常情况下，永远没有必要展开一个定理的“定义”；通过证明无关性，该定理的任何两个证明在定义上都是相等的。一旦一个定理的证明完成，通常我们只需要知道该证明的存在；证明是什么并不重要。鉴于这一事实，Lean将证明标记为*不可还原*（irreducible），作为对解析器（更确切地说，是**繁饰器**）的提示，在处理文件时一般不需要展开它。事实上，Lean通常能够并行地处理和检查证明，因为评估一个证明的正确性不需要知道另一个证明的细节。 +然而，定义和定理之间有一些实用的区别。正常情况下，永远没有必要展开一个定理的「定义」；通过证明无关性，该定理的任何两个证明在定义上都是相等的。一旦一个定理的证明完成，通常我们只需要知道该证明的存在；证明是什么并不重要。鉴于这一事实，Lean将证明标记为*不可还原*（irreducible），作为对解析器（更确切地说，是**繁饰器**）的提示，在处理文件时一般不需要展开它。事实上，Lean通常能够并行地处理和检查证明，因为评估一个证明的正确性不需要知道另一个证明的细节。 -和定义一样，``#print``命令可以展示一个定理的证明。 +和定义一样，``#print`` 命令可以展示一个定理的证明。 ```lean # variable {p : Prop} @@ -305,7 +305,7 @@ allows us to specify the type of the final term ``hp``, explicitly, with a ``show`` statement. --> -注意，lambda抽象``hp : p``和``hq : q``可以被视为``t1``的证明中的临时假设。Lean还允许我们通过``show``语句明确指定最后一个项``hp``的类型。 +注意，lambda抽象 ``hp : p`` 和 ``hq : q`` 可以被视为 ``t1`` 的证明中的临时假设。Lean还允许我们通过 ``show`` 语句明确指定最后一个项 ``hp`` 的类型。 ```lean # variable {p : Prop} @@ -326,9 +326,9 @@ As with ordinary definitions, we can move the lambda-abstracted variables to the left of the colon: --> -添加这些额外的信息可以提高证明的清晰度，并有助于在编写证明时发现错误。``show``命令只是注释类型，而且在内部，我们看到的所有关于``t1``的表示都产生了相同的项。 +添加这些额外的信息可以提高证明的清晰度，并有助于在编写证明时发现错误。``show`` 命令只是注释类型，而且在内部，我们看到的所有关于 ``t1`` 的表示都产生了相同的项。 -与普通定义一样，我们可以将lambda抽象的变量移到冒号的左边： +与普通定义一样，我们可以将 lambda 抽象的变量移到冒号的左边： ```lean # variable {p : Prop} @@ -342,7 +342,7 @@ theorem t1 (hp : p) (hq : q) : p := hp Now we can apply the theorem ``t1`` just as a function application. --> -现在我们可以把定理``t1``作为一个函数应用。 +现在我们可以把定理 ``t1`` 作为一个函数应用。 ```lean # variable {p : Prop} @@ -361,7 +361,7 @@ example, we can use it to postulate the empty type `False` has an element. --> -这里，``axiom``声明假定存在给定类型的元素，因此可能会破坏逻辑一致性。例如，我们可以使用它来假设空类型`False`有一个元素： +这里，``axiom`` 声明假定存在给定类型的元素，因此可能会破坏逻辑一致性。例如，我们可以使用它来假设空类型 `False` 有一个元素： -声明“公理”``hp : p``等同于声明``p``为真，正如``hp``所证明的那样。应用定理``t1 : p → q → p``到事实``hp : p``（也就是``p``为真）得到定理``t1 hp : q → p``。 +声明「公理」``hp : p`` 等同于声明 ``p`` 为真，正如 ``hp`` 所证明的那样。应用定理 ``t1 : p → q → p`` 到事实 ``hp : p``（也就是 ``p`` 为真）得到定理 ``t1 hp : q → p``。 -回想一下，我们也可以这样写定理``t1``: +回想一下，我们也可以这样写定理 ``t1``: ```lean theorem t1 {p q : Prop} (hp : p) (hq : q) : p := hp @@ -405,7 +405,7 @@ this as the assertion "for every pair of propositions ``p q``, we have of the colon: --> -``t1``的类型现在是``∀ {p q : Prop}, p → q → p``。我们可以把它理解为“对于每一对命题``p q``，我们都有``p → q → p``”。例如，我们可以将所有参数移到冒号的右边： +``t1`` 的类型现在是 ``∀ {p q : Prop}, p → q → p``。我们可以把它理解为「对于每一对命题 ``p q``，我们都有 ``p → q → p``」。例如，我们可以将所有参数移到冒号的右边： ```lean theorem t1 : ∀ {p q : Prop}, p → q → p := @@ -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} @@ -430,7 +430,7 @@ In fact, by the propositions-as-types correspondence, we can declare the assumption ``hp`` that ``p`` holds, as another variable: --> -事实上，通过命题即类型的对应关系，我们可以声明假设``hp``为``p``，作为另一个变量: +事实上，通过命题即类型的对应关系，我们可以声明假设 ``hp`` 为 ``p``，作为另一个变量: ```lean variable {p q : Prop} @@ -452,9 +452,9 @@ 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``时，我们就可以将它应用于不同的命题对，从而得到一般定理的不同实例。 +当我们以这种方式推广 ``t1`` 时，我们就可以将它应用于不同的命题对，从而得到一般定理的不同实例。 ```lean theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp @@ -478,7 +478,7 @@ As another example, let us consider the composition function discussed in the last chapter, now with propositions instead of types. --> -同样，使用命题即类型对应，类型为``r → s``的变量``h``可以看作是``r → s``存在的假设或前提。 +同样，使用命题即类型对应，类型为 ``r → s`` 的变量 ``h`` 可以看作是 ``r → s`` 存在的假设或前提。 作为另一个例子，让我们考虑上一章讨论的组合函数，现在用命题代替类型。 @@ -498,9 +498,9 @@ entered as ``\0``, ``\1``, ``\2``, ..., for hypotheses, as we did in this example. --> -作为一个命题逻辑定理，``t2``是什么意思？ +作为一个命题逻辑定理，``t2`` 是什么意思？ -注意，数字unicode下标输入方式为``\0``，``\1``，``\2``，...。 +注意，数字 unicode 下标输入方式为 ``\0``，``\1``，``\2``，...。 -操作符的优先级如下：``¬ > ∧ > ∨ > → > ↔``。举例：``a ∧ b → c ∨ d ∧ e``意为``(a ∧ b) → (c ∨ (d ∧ e))``。``→``等二元关系是右结合的。所以如果我们有``p q r : Prop``，表达式``p → q → r``读作“如果``p``，那么如果``q``，那么``r``”。这是``p ∧ q → r``的柯里化形式。 +操作符的优先级如下：``¬ > ∧ > ∨ > → > ↔``。举例：``a ∧ b → c ∨ d ∧ e`` 意为 ``(a ∧ b) → (c ∨ (d ∧ e))``。``→`` 等二元关系是右结合的。所以如果我们有 ``p q r : Prop``，表达式 ``p → q → r`` 读作「如果 ``p``，那么如果 ``q``，那么 ``r``」。这是 ``p ∧ q → r`` 的柯里化形式。 -在上一章中，我们观察到lambda抽象可以被看作是``→``的“引入规则”，展示了如何“引入”或建立一个蕴含。应用可以看作是一个“消去规则”，展示了如何在证明中“消去”或使用一个蕴含。其他的命题连接词在Lean的库``Prelude.core``文件中定义。(参见[导入文件](./interacting_with_lean.md#_importing_files)以获得关于库层次结构的更多信息)，并且每个连接都带有其规范引入和消去规则。 +在上一章中，我们观察到 lambda 抽象可以被看作是 ``→`` 的「引入规则」，展示了如何「引入」或建立一个蕴含。应用可以看作是一个「消去规则」，展示了如何在证明中「消去」或使用一个蕴含。其他的命题连接词在 Lean 的库 ``Prelude.core`` 文件中定义。(参见[导入文件](./interacting_with_lean.md#_importing_files)以获得关于库层次结构的更多信息)，并且每个连接都带有其规范引入和消去规则。 -表达式``And.intro h1 h2``是``p ∧ q``的证明，它使用了``h1 : p``和``h2 : q``的证明。通常把``And.intro``称为*合取引入*规则。下面的例子我们使用``And.intro``来创建``p → q → p ∧ q``的证明。 +表达式 ``And.intro h1 h2`` 是 ``p ∧ q`` 的证明，它使用了 ``h1 : p`` 和 ``h2 : q`` 的证明。通常把 ``And.intro`` 称为*合取引入*规则。下面的例子我们使用 ``And.intro`` 来创建 ``p → q → p ∧ q`` 的证明。 ```lean variable (p q : Prop) @@ -606,9 +606,9 @@ The expression ``And.left h`` creates a proof of ``p`` from a proof are commonly known as the left and right *and-elimination* rules. --> -``example``命令声明了一个没有名字也不会永久保存的定理。本质上，它只是检查给定项是否具有指定的类型。它便于说明，我们将经常使用它。 +``example`` 命令声明了一个没有名字也不会永久保存的定理。本质上，它只是检查给定项是否具有指定的类型。它便于说明，我们将经常使用它。 -表达式``And.left h``从``h : p ∧ q``建立了一个``p``的证明。类似地，``And.right h``是``q``的证明。它们常被称为左或右*合取消去*规则。 +表达式 ``And.left h`` 从 ``h : p ∧ q`` 建立了一个 ``p`` 的证明。类似地，``And.right h`` 是 ``q`` 的证明。它们常被称为左或右*合取消去*规则。 ```lean variable (p q : Prop) @@ -621,7 +621,7 @@ example (h : p ∧ q) : q := And.right h We can now prove ``p ∧ q → q ∧ p`` with the following proof term. --> -我们现在可以证明``p ∧ q → q ∧ p``： +我们现在可以证明 ``p ∧ q → q ∧ p``： ```lean variable (p q : Prop) @@ -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) @@ -675,9 +675,9 @@ a namespace. For example, the following two expressions mean the same thing: --> -尖括号可以用``\<``和``\>``打出来。 +尖括号可以用 ``\<`` 和 ``\>`` 打出来。 -Lean提供了另一个有用的语法小工具。给定一个归纳类型``Foo``的表达式``e``(可能应用于一些参数)，符号``e.bar``是``Foo.bar e``的缩写。这为访问函数提供了一种方便的方式，而无需打开名称空间。例如，下面两个表达的意思是相同的： +Lean提供了另一个有用的语法小工具。给定一个归纳类型 ``Foo`` 的表达式 ``e``(可能应用于一些参数)，符号 ``e.bar`` 是 ``Foo.bar e`` 的缩写。这为访问函数提供了一种方便的方式，而无需打开名称空间。例如，下面两个表达的意思是相同的： ```lean variable (xs : List Nat) @@ -692,7 +692,7 @@ As a result, given ``h : p ∧ q``, we can write ``h.left`` for rewrite the sample proof above conveniently as follows: --> -给定``h : p ∧ q``，我们可以写``h.left``来表示``And.left h``以及``h.right``来表示``And.right h``。因此我们可以简写上面的证明如下： +给定 ``h : p ∧ q``，我们可以写 ``h.left`` 来表示 ``And.left h`` 以及 ``h.right`` 来表示 ``And.right h``。因此我们可以简写上面的证明如下： ```lean variable (p q : Prop) @@ -713,9 +713,9 @@ to flatten nested constructors that associate to the right, so that these two proofs are equivalent: --> -在简洁和含混不清之间有一条微妙的界限，以这种方式省略信息有时会使证明更难阅读。但对于像上面这样简单的结构，当``h``的类型和结构的目标很突出时，符号是干净和有效的。 +在简洁和含混不清之间有一条微妙的界限，以这种方式省略信息有时会使证明更难阅读。但对于像上面这样简单的结构，当 ``h`` 的类型和结构的目标很突出时，符号是干净和有效的。 -像``And.``这样的迭代结构是很常见的。Lean还允许你将嵌套的构造函数向右结合，这样这两个证明是等价的: +像 ``And.`` 这样的迭代结构是很常见的。Lean还允许你将嵌套的构造函数向右结合，这样这两个证明是等价的: ```lean variable (p q : Prop) @@ -746,7 +746,7 @@ proof for ``p ∨ q`` using a proof ``hq : q``. These are the left and right *or-introduction* rules. --> -表达式``Or.intro_left q hp``从证明``hp : p``建立了``p ∨ q``的证明。类似地，``Or.intro_right p hq``从证明``hq : q``建立了``p ∨ q``的证明。这是左右析取（“或”）引入规则。 +表达式 ``Or.intro_left q hp`` 从证明 ``hp : p`` 建立了 ``p ∨ q`` 的证明。类似地，``Or.intro_right p hq`` 从证明 ``hq : q`` 建立了 ``p ∨ q`` 的证明。这是左右析取（「或」）引入规则。 ```lean variable (p q : Prop) @@ -764,7 +764,7 @@ takes three arguments, ``hpq : p ∨ q``, ``hpr : p → r`` and ``Or.elim`` to prove ``p ∨ q → q ∨ p``. --> -析取消去规则稍微复杂一点。这个想法是，我们可以从``p ∨ q``证明``r``，通过从``p``证明``r``，且从``q``证明``r``。换句话说，它是一种逐情况证明。在表达式``Or.elim hpq hpr hqr``中，``Or.elim``接受三个论证，``hpq : p ∨ q``，``hpr : p → r``和``hqr : q → r``，生成``r``的证明。在下面的例子中，我们使用``Or.elim``证明``p ∨ q → q ∨ p``。 +析取消去规则稍微复杂一点。这个想法是，我们可以从 ``p ∨ q`` 证明 ``r``，通过从 ``p`` 证明 ``r``，且从 ``q`` 证明 ``r``。换句话说，它是一种逐情况证明。在表达式 ``Or.elim hpq hpr hqr`` 中，``Or.elim`` 接受三个论证，``hpq : p ∨ q``，``hpr : p → r`` 和 ``hqr : q → r``，生成 ``r`` 的证明。在下面的例子中，我们使用 ``Or.elim`` 证明 ``p ∨ q → q ∨ p``。 ```lean variable (p q r : 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) @@ -836,7 +836,7 @@ proof of ``(p → q) → ¬q → ¬p``. (The symbol ``¬`` is produced by typing ``\not`` or ``\neg``.) --> -否定``¬p``真正的定义是``p → False``，所以我们通过从``p``导出一个矛盾来获得``¬p``。类似地，表达式``hnp hp``从``hp : p``和``hnp : ¬p``产生一个``False``的证明。下一个例子用所有这些规则来证明``(p → q) → ¬q → ¬p``。（``¬``符号可以由``\not``或者``\neg``来写出。） +否定 ``¬p`` 真正的定义是 ``p → False``，所以我们通过从 ``p`` 导出一个矛盾来获得 ``¬p``。类似地，表达式 ``hnp hp`` 从 ``hp : p`` 和 ``hnp : ¬p`` 产生一个 ``False`` 的证明。下一个例子用所有这些规则来证明 ``(p → q) → ¬q → ¬p``。（``¬`` 符号可以由 ``\not`` 或者 ``\neg`` 来写出。） ```lean variable (p q : Prop) @@ -853,7 +853,7 @@ contradiction. This rule is sometimes called *ex falso* (short for *ex falso sequitur quodlibet*), or the *principle of explosion*. --> -连接词``False``只有一个消去规则``False.elim``，它表达了一个事实，即矛盾能导出一切。这个规则有时被称为*ex falso* 【*ex falso sequitur quodlibet*（无稽之谈）的缩写】，或*爆炸原理*。 +连接词 ``False`` 只有一个消去规则 ``False.elim``，它表达了一个事实，即矛盾能导出一切。这个规则有时被称为*ex falso* 【*ex falso sequitur quodlibet*（无稽之谈）的缩写】，或*爆炸原理*。 ```lean variable (p q : Prop) @@ -868,7 +868,7 @@ pattern, deriving an arbitrary fact from contradictory hypotheses, is quite common, and is represented by ``absurd``. --> -假命题导出任意的事实``q``，是``False.elim``的一个隐参数，而且是自动推断出来的。这种从相互矛盾的假设中推导出任意事实的模式很常见，用``absurd``来表示。 +假命题导出任意的事实 ``q``，是 ``False.elim`` 的一个隐参数，而且是自动推断出来的。这种从相互矛盾的假设中推导出任意事实的模式很常见，用 ``absurd`` 来表示。 ```lean variable (p q : Prop) @@ -880,7 +880,7 @@ example (hp : p) (hnp : ¬p) : q := absurd hp hnp Here, for example, is a proof of ``¬p → q → (q → p) → r``: --> -证明``¬p → q → (q → p) → r``： +证明 ``¬p → q → (q → p) → r``： ```lean variable (p q r : Prop) @@ -895,7 +895,7 @@ has only an introduction rule, ``True.intro : true``. In other words, ``True`` is simply true, and has a canonical proof, ``True.intro``. --> -顺便说一句，就像``False``只有一个消去规则，``True``只有一个引入规则``True.intro : true``。换句话说，``True``就是真，并且有一个标准证明``True.intro``。 +顺便说一句，就像 ``False`` 只有一个消去规则，``True`` 只有一个引入规则 ``True.intro : true``。换句话说，``True`` 就是真，并且有一个标准证明 ``True.intro``。 -表达式``Iff.intro h1 h2``从``h1 : p → q``和``h2 : q → p``生成了``p ↔ q``的证明。表达式``Iff.mp h``从``h : p ↔ q``生成了``p → q``的证明。表达式``Iff.mpr h``从``h : p ↔ q``生成了``q → p``的证明。下面是``p ∧ q ↔ q ∧ p``的证明： +表达式 ``Iff.intro h1 h2`` 从 ``h1 : p → q`` 和 ``h2 : q → p`` 生成了 ``p ↔ q`` 的证明。表达式 ``Iff.mp h`` 从 ``h : p ↔ q`` 生成了 ``p → q`` 的证明。表达式 ``Iff.mpr h`` 从 ``h : p ↔ q`` 生成了 ``q → p`` 的证明。下面是 ``p ∧ q ↔ q ∧ p`` 的证明： ```lean variable (p q : 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) @@ -961,7 +961,7 @@ introduces an auxiliary subgoal in a proof. Here is a small example, adapted from the last section: --> -这里介绍Lean提供的另一种帮助构造长证明的方法，即``have``结构，它在证明中引入了一个辅助的子目标。下面是一个小例子，改编自上一节: +这里介绍 Lean 提供的另一种帮助构造长证明的方法，即 ``have`` 结构，它在证明中引入了一个辅助的子目标。下面是一个小例子，改编自上一节: ```lean variable (p q : Prop) @@ -987,9 +987,9 @@ mathematics. The next example simply permutes the last two lines in the previous proof. --> -在内部，表达式``have h : p := s; t``产生项``(fun (h : p) => t) s``。换句话说，``s``是``p``的证明，``t``是假设``h : p``的期望结论的证明，并且这两个是由lambda抽象和应用组合在一起的。这个简单的方法在构建长证明时非常有用，因为我们可以使用中间的``have``作为通向最终目标的垫脚石。 +在内部，表达式 ``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) @@ -1007,7 +1007,7 @@ goal of ``q ∧ p`` with the additional hypothesis ``hq : q``. Finally, we have to show ``q``. --> -``suffices hq : q``给出了两条目标。第一，我们需要证明，通过利用附加假设``hq : q``证明原目标``q ∧ p``，这样足以证明``q``，第二，我们需要证明``q``。 +``suffices hq : q`` 给出了两条目标。第一，我们需要证明，通过利用附加假设 ``hq : q`` 证明原目标 ``q ∧ p``，这样足以证明 ``q``，第二，我们需要证明 ``q``。 -到目前为止，我们看到的引入和消去规则都是构造主义的，也就是说，它们反映了基于命题即类型对应的逻辑连接词的计算理解。普通经典逻辑在此基础上加上了排中律``p ∨ ¬p``（excluded middle, em）。要使用这个原则，你必须打开经典逻辑命名空间。 +到目前为止，我们看到的引入和消去规则都是构造主义的，也就是说，它们反映了基于命题即类型对应的逻辑连接词的计算理解。普通经典逻辑在此基础上加上了排中律 ``p ∨ ¬p``（excluded middle, em）。要使用这个原则，你必须打开经典逻辑命名空间。 ```lean open Classical @@ -1044,7 +1044,7 @@ One consequence of the law of the excluded middle is the principle of double-negation elimination: --> -从直觉上看，构造主义的“或”非常强：断言``p ∨ q``等于知道哪个是真实情况。如果``RH``代表黎曼猜想，经典数学家愿意断言``RH ∨ ¬RH``，即使我们还不能断言析取式的任何一端。 +从直觉上看，构造主义的「或」非常强：断言 ``p ∨ q`` 等于知道哪个是真实情况。如果 ``RH`` 代表黎曼猜想，经典数学家愿意断言 ``RH ∨ ¬RH``，即使我们还不能断言析取式的任何一端。 排中律的一个结果是双重否定消去规则（double-negation elimination, dne）: @@ -1071,9 +1071,9 @@ proof that can be justified by appeal to ``em``. For example, one can carry out a proof by cases: --> -双重否定消去规则给出了一种证明任何命题``p``的方法：通过假设``¬p``来推导出``false``，相当于证明了``p``。换句话说，双重否定消除允许反证法，这在构造主义逻辑中通常是不可能的。作为练习，你可以试着证明相反的情况，也就是说，证明``em``可以由``dne``证明。 +双重否定消去规则给出了一种证明任何命题 ``p`` 的方法：通过假设 ``¬p`` 来推导出 ``false``，相当于证明了 ``p``。换句话说，双重否定消除允许反证法，这在构造主义逻辑中通常是不可能的。作为练习，你可以试着证明相反的情况，也就是说，证明 ``em`` 可以由 ``dne`` 证明。 -经典公理还可以通过使用``em``让你获得额外的证明模式。例如，我们可以逐情况进行证明: +经典公理还可以通过使用 ``em`` 让你获得额外的证明模式。例如，我们可以逐情况进行证明: ```lean open Classical @@ -1109,7 +1109,7 @@ standpoint, knowing that ``p`` and ``q`` are not both true does not necessarily tell you which one is false: --> -如果你不习惯构造主义，你可能需要一些时间来了解经典推理在哪里使用。在下面的例子中，它是必要的，因为从一个构造主义的观点来看，知道``p``和``q``不同时真并不一定告诉你哪一个是假的： +如果你不习惯构造主义，你可能需要一些时间来了解经典推理在哪里使用。在下面的例子中，它是必要的，因为从一个构造主义的观点来看，知道 ``p`` 和 ``q`` 不同时真并不一定告诉你哪一个是假的： ```lean # open Classical @@ -1136,7 +1136,7 @@ reasoning are discussed in [Axioms and Computation](./axioms_and_computation.md) --> -稍后我们将看到，构造逻辑中**有**某些情况允许“排中律”和“双重否定消除律”等，而Lean支持在这种情况下使用经典推理，而不依赖于排中律。 +稍后我们将看到，构造逻辑中**有**某些情况允许「排中律」和「双重否定消除律」等，而 Lean 支持在这种情况下使用经典推理，而不依赖于排中律。 Lean中使用的公理的完整列表见[公理与计算](./axioms_and_computation.md)。 @@ -1241,9 +1241,9 @@ For reference, here are two sample proofs of validities taken from the list above. --> -``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报告在那一点上需要填充的子目标。然后，你可以通过递增填充这些占位符来构造一个证明。 这里有两个简单的证明例子作为参考。 @@ -1328,7 +1328,7 @@ Exercises Prove the following identities, replacing the "sorry" placeholders with actual proofs. --> -证明以下等式，用真实证明取代“sorry”占位符。 +证明以下等式，用真实证明取代「sorry」占位符。 -最后，证明``¬(p ↔ ¬p)``且不使用经典逻辑。 +最后，证明 ``¬(p ↔ ¬p)`` 且不使用经典逻辑。 diff --git a/quantifiers_and_equality.md b/quantifiers_and_equality.md index 8d23c95..5d8756d 100644 --- a/quantifiers_and_equality.md +++ b/quantifiers_and_equality.md @@ -72,29 +72,29 @@ depend on ``x``. Here is an example of how the propositions-as-types correspondence gets put into practice. --> -如果``α``是任何类型，我们可以将``α``上的一元谓词``p``作为``α → Prop``类型的对象。在这种情况下，给定``x : α``， ``p x``表示断言``p``在``x``上成立。类似地，一个对象``r : α → α → Prop``表示``α``上的二元关系：给定``x y : α``，``r x y``表示断言``x``与``y``相关。 +如果 ``α`` 是任何类型，我们可以将 ``α`` 上的一元谓词 ``p`` 作为 ``α → Prop`` 类型的对象。在这种情况下，给定 ``x : α``， ``p x`` 表示断言 ``p`` 在 ``x`` 上成立。类似地，一个对象 ``r : α → α → Prop`` 表示 ``α`` 上的二元关系：给定 ``x y : α``，``r x y`` 表示断言 ``x`` 与 ``y`` 相关。 -全称量词``∀ x : α, p x``表示，对于每一个``x : α``，``p x``成立。与命题连接词一样，在自然演绎系统中，“forall”有引入和消去规则。非正式地，引入规则是： +全称量词 ``∀ x : α, p x`` 表示，对于每一个 ``x : α``，``p x`` 成立。与命题连接词一样，在自然演绎系统中，「forall」有引入和消去规则。非正式地，引入规则是： -> 给定``p x``的证明，在``x : α``是任意的情况下，我们得到``∀ x : α, p x``的证明。 +> 给定 ``p x`` 的证明，在 ``x : α`` 是任意的情况下，我们得到 ``∀ x : α, p x`` 的证明。 消去规则是： -> 给定``∀ x : α, p x``的证明和任何项``t : α``，我们得到``p t``的证明。 +> 给定 ``∀ x : α, p x`` 的证明和任何项 ``t : α``，我们得到 ``p t`` 的证明。 与蕴含的情况一样，命题即类型。回想依值箭头类型的引入规则: -> 给定类型为``β x``的项``t``，在``x : α``是任意的情况下，我们有``(fun x : α => t) : (x : α) → β x``。 +> 给定类型为 ``β x`` 的项 ``t``，在 ``x : α`` 是任意的情况下，我们有 ``(fun x : α => t) : (x : α) → β x``。 消去规则： -> 给定项``s : (x : α) → β x``和任何项``t : α``，我们有``s t : β t``。 +> 给定项 ``s : (x : α) → β x`` 和任何项 ``t : α``，我们有 ``s t : β t``。 -在``p x``具有``Prop``类型的情况下，如果我们用``∀ x : α, p x``替换``(x : α) → β x``，就得到构建涉及全称量词的证明的规则。 +在 ``p x`` 具有 ``Prop`` 类型的情况下，如果我们用 ``∀ x : α, p x`` 替换 ``(x : α) → β x``，就得到构建涉及全称量词的证明的规则。 -因此，构造演算用全称表达式来识别依值箭头类型。如果``p``是任何表达式，``∀ x : α, p``不过是``(x : α) → p``的替代符号，在``p``是命题的情况下，前者比后者更自然。通常，表达式``p``取决于``x : α``。回想一下，在普通函数空间中，我们可以将``α → β``解释为``(x : α) → β``的特殊情况，其中``β``不依赖于``x``。类似地，我们可以把命题之间的蕴涵``p → q``看作是``∀ x : p, q``的特殊情况，其中``q``不依赖于``x``。 +因此，构造演算用全称表达式来识别依值箭头类型。如果 ``p`` 是任何表达式，``∀ x : α, p`` 不过是 ``(x : α) → p`` 的替代符号，在 ``p`` 是命题的情况下，前者比后者更自然。通常，表达式 ``p`` 取决于 ``x : α``。回想一下，在普通函数空间中，我们可以将 ``α → β`` 解释为 ``(x : α) → β`` 的特殊情况，其中 ``β`` 不依赖于 ``x``。类似地，我们可以把命题之间的蕴涵 ``p → q`` 看作是 ``∀ x : p, q`` 的特殊情况，其中 ``q`` 不依赖于 ``x``。 -下面是一个例子，说明了如何运用命题即类型对应规则。``∀``可以用``\forall``输入，也可以用前两个字母简写``\fo``。 +下面是一个例子，说明了如何运用命题即类型对应规则。``∀`` 可以用 ``\forall`` 输入，也可以用前两个字母简写 ``\fo``。 ```lean example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ y : α, p y := @@ -120,9 +120,9 @@ conclusion, and instantiated it by a different variable, ``z``, in the proof: --> -作为一种符号约定，我们给予全称量词尽可能最宽的优先级范围，因此上面例子中的假设中，需要用括号将``x``上的量词限制起来。证明``∀ y : α, p y``的标准方法是取任意的``y``，然后证明``p y``。这是引入规则。现在，给定``h``有类型``∀ x : α, p x ∧ q x``，表达式``h y``有类型``p y ∧ q y``。这是消去规则。取合取的左侧得到想要的结论``p y``。 +作为一种符号约定，我们给予全称量词尽可能最宽的优先级范围，因此上面例子中的假设中，需要用括号将 ``x`` 上的量词限制起来。证明 ``∀ y : α, p y`` 的标准方法是取任意的 ``y``，然后证明 ``p y``。这是引入规则。现在，给定 ``h`` 有类型 ``∀ x : α, p x ∧ q x``，表达式 ``h y`` 有类型 ``p y ∧ q y``。这是消去规则。取合取的左侧得到想要的结论 ``p y``。 -只有约束变量名称不同的表达式被认为是等价的。因此，例如，我们可以在假设和结论中使用相同的变量``x``，并在证明中用不同的变量``z``实例化它: +只有约束变量名称不同的表达式被认为是等价的。因此，例如，我们可以在假设和结论中使用相同的变量 ``x``，并在证明中用不同的变量 ``z`` 实例化它: ```lean example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ x : α, p x := @@ -135,7 +135,7 @@ example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ x : As another example, here is how we can express the fact that a relation, ``r``, is transitive: --> -再举一个例子，下面是关系``r``的传递性： +再举一个例子，下面是关系 ``r`` 的传递性： ```lean variable (α : Type) (r : α → α → Prop) @@ -162,8 +162,7 @@ In situations like this, it can be tedious to supply the arguments is common to make these arguments implicit: --> - -当我们在值``a b c``上实例化``trans_r``时，我们最终得到``r a b → r b c → r a c``的证明。将此应用于“假设”``hab : r a b``，我们得到了``r b c → r a c``的一个证明。最后将它应用到假设``hbc``中，得到结论``r a c``的证明。 +当我们在值 ``a b c`` 上实例化 ``trans_r`` 时，我们最终得到 ``r a b → r b c → r a c`` 的证明。将此应用于「假设」``hab : r a b``，我们得到了 ``r b c → r a c`` 的一个证明。最后将它应用到假设 ``hbc`` 中，得到结论 ``r a c`` 的证明。 ```lean variable (α : Type) (r : α → α → Prop) @@ -188,7 +187,7 @@ that the implicit arguments are unspecified in this case. Here is an example of how we can carry out elementary reasoning with an equivalence relation: --> -优点是我们可以简单地写``trans_r hab hbc``作为``r a c``的证明。一个缺点是Lean没有足够的信息来推断表达式``trans_r``和``trans_r hab``中的参数类型。第一个``#check``命令的输出是``r ?m.1 ?m.2 → r ?m.2 ?m.3 → r ?m.1 ?m.3``，表示在本例中隐式参数未指定。 +优点是我们可以简单地写 ``trans_r hab hbc`` 作为 ``r a c`` 的证明。一个缺点是 Lean 没有足够的信息来推断表达式 ``trans_r`` 和 ``trans_r hab`` 中的参数类型。第一个 ``#check`` 命令的输出是 ``r ?m.1 ?m.2 → r ?m.2 ?m.3 → r ?m.1 ?m.3``，表示在本例中隐式参数未指定。 下面是一个用等价关系进行基本推理的例子: @@ -241,11 +240,11 @@ considered problematic. 为了习惯使用全称量词，你应该尝试本节末尾的一些练习。 -依值箭头类型的类型规则，特别是全称量词，体现了``Prop``命题类型与其他对象的类型的不同。假设我们有``α : Sort i``和``β : Sort j``，其中表达式``β``可能依赖于变量``x : α``。那么``(x : α) → β``是``Sort (imax i j)``的一个元素，其中``imax i j``是``i``和``j``在``j``不为0时的最大值，否则为0。 +依值箭头类型的类型规则，特别是全称量词，体现了 ``Prop`` 命题类型与其他对象的类型的不同。假设我们有 ``α : Sort i`` 和 ``β : Sort j``，其中表达式 ``β`` 可能依赖于变量 ``x : α``。那么 ``(x : α) → β`` 是 ``Sort (imax i j)`` 的一个元素，其中 ``imax i j`` 是 ``i`` 和 ``j`` 在 ``j`` 不为0时的最大值，否则为0。 -其想法如下。如果``j``不是``0``，然后``(x : α) → β``是``Sort (max i j)``类型的一个元素。换句话说，从``α``到``β``的一类依值函数存在于指数为``i``和``j``最大值的宇宙中。然而，假设``β``属于``Sort 0``，即``Prop``的一个元素。在这种情况下，``(x : α) → β``也是``Sort 0``的一个元素，无论``α``生活在哪种类型的宇宙中。换句话说，如果``β``是一个依赖于``α``的命题，那么``∀ x : α, β``又是一个命题。这反映出``Prop``作为一种命题类型而不是数据类型，这也使得``Prop``具有“非直谓性”（impredicative）。 +其想法如下。如果 ``j`` 不是 ``0``，然后 ``(x : α) → β`` 是 ``Sort (max i j)`` 类型的一个元素。换句话说，从 ``α`` 到 ``β`` 的一类依值函数存在于指数为 ``i`` 和 ``j`` 最大值的宇宙中。然而，假设 ``β`` 属于 ``Sort 0``，即 ``Prop`` 的一个元素。在这种情况下，``(x : α) → β`` 也是 ``Sort 0`` 的一个元素，无论 ``α`` 生活在哪种类型的宇宙中。换句话说，如果 ``β`` 是一个依赖于 ``α`` 的命题，那么 ``∀ x : α, β`` 又是一个命题。这反映出 ``Prop`` 作为一种命题类型而不是数据类型，这也使得 ``Prop`` 具有「非直谓性」（impredicative）。 -“直谓性”一词起源于20世纪初的数学基础发展，当时逻辑学家如庞加莱和罗素将集合论的悖论归咎于“恶性循环”：当我们通过量化一个集合来定义一个属性时，这个集合包含了被定义的属性。注意，如果``α``是任何类型，我们可以在``α``上形成所有谓词的类型``α → Prop``(``α``的“幂”类型)。Prop的非直谓性意味着我们可以通过``α → Prop``形成量化命题。特别是，我们可以通过量化所有关于``α``的谓词来定义``α``上的谓词，这正是曾经被认为有问题的循环类型。 +「直谓性」一词起源于20世纪初的数学基础发展，当时逻辑学家如庞加莱和罗素将集合论的悖论归咎于「恶性循环」：当我们通过量化一个集合来定义一个属性时，这个集合包含了被定义的属性。注意，如果 ``α`` 是任何类型，我们可以在 ``α`` 上形成所有谓词的类型 ``α → Prop``(``α`` 的「幂」类型)。Prop的非直谓性意味着我们可以通过 ``α → Prop`` 形成量化命题。特别是，我们可以通过量化所有关于 ``α`` 的谓词来定义 ``α`` 上的谓词，这正是曾经被认为有问题的循环类型。 -现在让我们来看看在Lean库中定义的最基本的关系之一，即等价关系。在[归纳类型](inductive_types.md)一章中，我们将解释如何从Lean的逻辑框架中定义等价。在这里我们解释如何使用它。 +现在让我们来看看在 Lean 库中定义的最基本的关系之一，即等价关系。在[归纳类型](inductive_types.md)一章中，我们将解释如何从 Lean 的逻辑框架中定义等价。在这里我们解释如何使用它。 等价关系的基本性质：反身性、对称性、传递性。 - ```lean #check Eq.refl -- Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a #check Eq.symm -- Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a @@ -280,7 +278,7 @@ We can make the output easier to read by telling Lean not to insert the implicit arguments (which are displayed here as metavariables). --> -通过告诉Lean不要插入隐参数(在这里显示为元变量)可以使输出更容易阅读。 +通过告诉 Lean 不要插入隐参数(在这里显示为元变量)可以使输出更容易阅读。 ```lean universe u @@ -296,7 +294,7 @@ The inscription ``.{u}`` tells Lean to instantiate the constants at the universe Thus, for example, we can specialize the example from the previous section to the equality relation: --> -``.{u}``告诉Lean实例化宇宙``u``上的常量。 +``.{u}`` 告诉 Lean 实例化宇宙 ``u`` 上的常量。 因此，我们可以将上一节中的示例具体化为等价关系: @@ -342,7 +340,7 @@ example : 2 + 3 = 5 := Eq.refl _ This feature of the framework is so important that the library defines a notation ``rfl`` for ``Eq.refl _``: --> -这个特性非常重要，以至于库中为``Eq.refl _``专门定义了一个符号``rfl``： +这个特性非常重要，以至于库中为 ``Eq.refl _`` 专门定义了一个符号 ``rfl``： ```lean # variable (α β : Type) @@ -360,7 +358,7 @@ can construct a proof for ``p b`` using substitution: ``Eq.subst h1 h2``. --> -然而，等价不仅仅是一种关系。它有一个重要的性质，即每个断言都遵从等价性，即我们可以在不改变真值的情况下对表达式做等价代换。也就是说，给定``h1 : a = b``和``h2 : p a``，我们可以构造一个证明``p b``，只需要使用代换``Eq.subst h1 h2``。 +然而，等价不仅仅是一种关系。它有一个重要的性质，即每个断言都遵从等价性，即我们可以在不改变真值的情况下对表达式做等价代换。也就是说，给定 ``h1 : a = b`` 和 ``h2 : p a``，我们可以构造一个证明 ``p b``，只需要使用代换 ``Eq.subst h1 h2``。 ```lean example (α : Type) (a b : α) (p : α → Prop) @@ -384,9 +382,9 @@ used to replace the term that is being applied, and ``congr`` can be used to replace both at once. --> -第二个例子中的三角形是建立在``Eq.subst``和``Eq.symm``之上的宏，它可以通过``\t``来输入。 +第二个例子中的三角形是建立在 ``Eq.subst`` 和 ``Eq.symm`` 之上的宏，它可以通过 ``\t`` 来输入。 -规则``Eq.subst``定义了一些辅助规则，用来执行更显式的替换。它们是为处理应用型项，即形式为``s t``的项而设计的。这些辅助规则是，使用``congrArg``来替换参数，使用``congrFun``来替换正在应用的项，并且可以同时使用``congr``来替换两者。 +规则 ``Eq.subst`` 定义了一些辅助规则，用来执行更显式的替换。它们是为处理应用型项，即形式为 ``s t`` 的项而设计的。这些辅助规则是，使用 ``congrArg`` 来替换参数，使用 ``congrFun`` 来替换正在应用的项，并且可以同时使用 ``congr`` 来替换两者。 ```lean variable (α : Type) @@ -432,7 +430,7 @@ Here is an example of a calculation in the natural numbers that uses substitution combined with associativity and distributivity. --> -``Nat.mul_add``和``Nat.add_mul``是``Nat.left_distrib``和``Nat.right_distrib``的代称。上面的属性是为自然数类型``Nat``声明的。 +``Nat.mul_add`` 和 ``Nat.add_mul`` 是 ``Nat.left_distrib`` 和 ``Nat.right_distrib`` 的代称。上面的属性是为自然数类型 ``Nat`` 声明的。 这是一个使用代换以及结合律、交换律和分配律的自然数计算的例子。 @@ -467,7 +465,7 @@ briefly in the next section, and then in greater detail in the next chapter. --> -注意，``Eq.subst``的第二个隐式参数提供了将要发生代换的表达式上下文，其类型为``α → Prop``。因此，推断这个谓词需要一个*高阶合一*（higher-order unification）的实例。一般来说，确定高阶合一器是否存在的问题是无法确定的，而Lean充其量只能提供不完美的和近似的解决方案。因此，``Eq.subst``并不总是做你想要它做的事。宏``h ▸ e``使用了更有效的启发式方法来计算这个隐参数，并且在不能应用``Eq.subst``的情况下通常会成功。 +注意，``Eq.subst`` 的第二个隐式参数提供了将要发生代换的表达式上下文，其类型为 ``α → Prop``。因此，推断这个谓词需要一个*高阶合一*（higher-order unification）的实例。一般来说，确定高阶合一器是否存在的问题是无法确定的，而 Lean 充其量只能提供不完美的和近似的解决方案。因此，``Eq.subst`` 并不总是做你想要它做的事。宏 ``h ▸ e`` 使用了更有效的启发式方法来计算这个隐参数，并且在不能应用 ``Eq.subst`` 的情况下通常会成功。 因为等式推理是如此普遍和重要，Lean提供了许多机制来更有效地执行它。下一节将提供允许你以更自然和清晰的方式编写计算式证明的语法。但更重要的是，等式推理是由项重写器、简化器和其他种类的自动化方法支持的。术语重写器和简化器将在下一节中简要描述，然后在下一章中更详细地描述。 @@ -486,7 +484,7 @@ equality. In Lean, a calculational proof starts with the keyword ``calc``, and has the following syntax: --> -一个计算式证明是指一串使用诸如等式的传递性等基本规则得到的中间结果。在Lean中，计算式证明从关键字``calc``开始，语法如下： +一个计算式证明是指一串使用诸如等式的传递性等基本规则得到的中间结果。在 Lean 中，计算式证明从关键字 ``calc`` 开始，语法如下： ``` calc @@ -504,12 +502,12 @@ We can also use `_` in the first relation (right after ``_0``) which is useful to align the sequence of relation/proof pairs: --> -`calc`下的每一行使用相同的缩进。每个``_i``是``_{i-1} op_i _i``的证明。 +`calc` 下的每一行使用相同的缩进。每个 ``_i`` 是 ``_{i-1} op_i _i`` 的证明。 -我们也可以在第一个关系中使用`_`(就在``_0``之后)，这对于对齐关系/证明对的序列很有用: +我们也可以在第一个关系中使用 `_`(就在 ``_0`` 之后)，这对于对齐关系/证明对的序列很有用: ``` -calc _0 +calc _0 '_' 'op_1' _1 ':=' _1 '_' 'op_2' _2 ':=' _2 ... @@ -546,7 +544,7 @@ the abbreviation ``rw`` for rewrite, the proof above could be written as follows: --> -这种写证明的风格在与`simp`和`rewrite`策略（Tactic）结合使用时最为有效，这些策略将在下一章详细讨论。例如，用缩写`rw`表示重写，上面的证明可以写成如下。 +这种写证明的风格在与 `simp` 和 `rewrite` 策略（Tactic）结合使用时最为有效，这些策略将在下一章详细讨论。例如，用缩写 `rw` 表示重写，上面的证明可以写成如下。 ```lean # variable (a b c d e : Nat) @@ -573,7 +571,7 @@ Rewrites can be applied sequentially, so that the proof above can be shortened to this: --> -本质上，``rw``策略使用一个给定的等式(它可以是一个假设、一个定理名称或一个复杂的项)来“重写”目标。如果这样做将目标简化为一种等式``t = t``，那么该策略将使用反身性来证明这一点。 +本质上，``rw`` 策略使用一个给定的等式(它可以是一个假设、一个定理名称或一个复杂的项)来「重写」目标。如果这样做将目标简化为一种等式 ``t = t``，那么该策略将使用反身性来证明这一点。 重写可以一次应用一系列，因此上面的证明可以缩写为： @@ -614,7 +612,7 @@ the system, and applies commutativity wisely to avoid looping. As a result, we can also prove the theorem as follows: --> -相反，``simp``策略通过在项中以任意顺序在任何适用的地方重复应用给定的等式来重写目标。它还使用了之前声明给系统的其他规则，并明智地应用交换性以避免循环。因此，我们也可以如下证明定理: +相反，``simp`` 策略通过在项中以任意顺序在任何适用的地方重复应用给定的等式来重写目标。它还使用了之前声明给系统的其他规则，并明智地应用交换性以避免循环。因此，我们也可以如下证明定理: ```lean # variable (a b c d e : Nat) @@ -633,9 +631,9 @@ The ``calc`` command can be configured for any relation that supports some form of transitivity. It can even combine different relations. --> -我们将在下一章讨论``rw``和``simp``的变体。 +我们将在下一章讨论 ``rw`` 和 ``simp`` 的变体。 -``calc``命令可以配置为任何支持某种形式的传递性的关系式。它甚至可以结合不同的关系式。 +``calc`` 命令可以配置为任何支持某种形式的传递性的关系式。它甚至可以结合不同的关系式。 ```lean example (a b c d : Nat) (h1 : a = b) (h2 : b ≤ c) (h3 : c + 1 < d) : a < d := @@ -652,7 +650,7 @@ of the `Trans` type class. Type classes are introduced later, but the following small example demonstrates how to extend the `calc` notation using new `Trans` instances. --> -你可以通过添加`Trans`类型族（Type class）的新实例来“教给”`calc`新的传递性定理。稍后将介绍类型族，但下面的小示例将演示如何使用新的`Trans`实例扩展`calc`表示法。 +你可以通过添加 `Trans` 类型族（Type class）的新实例来「教给」`calc` 新的传递性定理。稍后将介绍类型族，但下面的小示例将演示如何使用新的 `Trans` 实例扩展 `calc` 表示法。 ```lean def divides (x y : Nat) : Prop := @@ -692,14 +690,14 @@ unicode to make sure we do not overload the ASCII `|` used in the `match .. with` expression. --> -上面的例子也清楚地表明，即使关系式没有中缀符号，也可以使用`calc`。最后，我们注意到上面例子中的竖线`∣`是unicode。我们使用unicode来确保我们不会重载在`match .. with`表达式中使用的ASCII`|`。 +上面的例子也清楚地表明，即使关系式没有中缀符号，也可以使用 `calc`。最后，我们注意到上面例子中的竖线`∣`是unicode。我们使用 unicode 来确保我们不会重载在`match .. with`表达式中使用的ASCII`|`。 -使用``calc``，我们可以以一种更自然、更清晰的方式写出上一节的证明。 +使用 ``calc``，我们可以以一种更自然、更清晰的方式写出上一节的证明。 ```lean example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := @@ -716,7 +714,7 @@ first expression is taking this much space, using `_` in the first relation naturally aligns all relations: --> -这里值得考虑另一种`calc`表示法。当第一个表达式占用这么多空间时，在第一个关系中使用`_`自然会对齐所有关系式: +这里值得考虑另一种 `calc` 表示法。当第一个表达式占用这么多空间时，在第一个关系中使用 `_` 自然会对齐所有关系式: ```lean example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := @@ -734,7 +732,7 @@ use the ascii equivalent, ``<-``.) If brevity is what we are after, both ``rw`` and ``simp`` can do the job on their own: --> -``Nat.add_assoc``之前的左箭头指挥重写以相反的方向使用等式。(你可以输入``\l``或ascii码``<-``。)如果追求简洁，``rw``和``simp``可以一次性完成这项工作: +``Nat.add_assoc`` 之前的左箭头指挥重写以相反的方向使用等式。(你可以输入 ``\l`` 或 ascii 码 ``<-``。)如果追求简洁，``rw`` 和 ``simp`` 可以一次性完成这项工作: ```lean example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := @@ -763,9 +761,9 @@ straightforward: to prove ``∃ x : α, p x``, it suffices to provide a suitable term ``t`` and a proof of ``p t``. Here are some examples: --> -存在量词可以写成``exists x : α, p x``或``∃ x : α, p x``。这两个写法实际上在Lean的库中的定义为一个更冗长的表达式，``Exists (fun x : α => p x)``。 +存在量词可以写成 ``exists x : α, p x`` 或 ``∃ x : α, p x``。这两个写法实际上在 Lean 的库中的定义为一个更冗长的表达式，``Exists (fun x : α => p x)``。 -存在量词也有一个引入规则和一个消去规则。引入规则很简单：要证明``∃ x : α, p x``，只需提供一个合适的项``t``和对``p t``的证明即可。``∃``用``\exists``或简写``\ex``输入，下面是一些例子: +存在量词也有一个引入规则和一个消去规则。引入规则很简单：要证明 ``∃ x : α, p x``，只需提供一个合适的项 ``t`` 和对 ``p t`` 的证明即可。``∃`` 用 ``\exists`` 或简写 ``\ex`` 输入，下面是一些例子: ```lean example : ∃ x : Nat, x > 0 := @@ -786,7 +784,7 @@ We can use the anonymous constructor notation ``⟨t, h⟩`` for ``Exists.intro t h``, when the type is clear from the context. --> -当类型可从上下文中推断时，我们可以使用匿名构造器表示法``⟨t, h⟩``替换``Exists.intro t h``。 +当类型可从上下文中推断时，我们可以使用匿名构造器表示法 ``⟨t, h⟩`` 替换 ``Exists.intro t h``。 ```lean example : ∃ x : Nat, x > 0 := @@ -812,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 打印隐参数。 -我们可以将``Exists.intro``视为信息隐藏操作，因为它将断言的具体实例隐藏起来变成了存在量词。存在消去规则``Exists.elim``执行相反的操作。它允许我们从``∃ x : α, p x``证明一个命题``q``，通过证明对于任意值``w``时``p w``都能推出``q``。粗略地说，既然我们知道有一个``x``满足``p x``，我们可以给它起个名字，比如``w``。如果``q``没有提到``w``，那么表明``p w``能推出``q``就等同于表明``q``从任何这样的``x``的存在而推得。下面是一个例子: +我们可以将 ``Exists.intro`` 视为信息隐藏操作，因为它将断言的具体实例隐藏起来变成了存在量词。存在消去规则 ``Exists.elim`` 执行相反的操作。它允许我们从 ``∃ x : α, p x`` 证明一个命题 ``q``，通过证明对于任意值 ``w`` 时 ``p w`` 都能推出 ``q``。粗略地说，既然我们知道有一个 ``x`` 满足 ``p x``，我们可以给它起个名字，比如 ``w``。如果 ``q`` 没有提到 ``w``，那么表明 ``p w`` 能推出 ``q`` 就等同于表明 ``q`` 从任何这样的 ``x`` 的存在而推得。下面是一个例子: ```lean variable (α : Type) (p q : α → Prop) @@ -892,11 +890,11 @@ Lean provides a more convenient way to eliminate from an existential quantifier with the ``match`` expression: --> -把存在消去规则和析取消去规则作个比较可能会带来一些启发。命题``∃ 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同构的另一例子。 +存在式命题类型很像依值类型一节所述的 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) @@ -917,7 +915,7 @@ to prove the proposition. We can annotate the types used in the match for greater clarity: --> -``match``表达式是Lean功能定义系统的一部分，它提供了复杂功能的方便且丰富的表达方式。再一次，正是Curry-Howard同构让我们能够采用这种机制来编写证明。``match``语句将存在断言“析构”到组件``w``和``hw``中，然后可以在语句体中使用它们来证明命题。我们可以对match中使用的类型进行注释，以提高清晰度： +``match`` 表达式是 Lean 功能定义系统的一部分，它提供了复杂功能的方便且丰富的表达方式。再一次，正是Curry-Howard同构让我们能够采用这种机制来编写证明。``match`` 语句将存在断言「析构」到组件 ``w`` 和 ``hw`` 中，然后可以在语句体中使用它们来证明命题。我们可以对 match 中使用的类型进行注释，以提高清晰度： ```lean # variable (α : Type) (p q : α → Prop) @@ -930,7 +928,7 @@ example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := We can even use the match statement to decompose the conjunction at the same time: --> -我们甚至可以同时使用match语句来分解合取： +我们甚至可以同时使用 match 语句来分解合取： ```lean # variable (α : Type) (p q : α → Prop) @@ -943,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) @@ -958,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 @@ -977,7 +975,7 @@ and then we show that the sum of two even numbers is an even number. 我们将在[归纳和递归](./induction_and_recursion.md)一章看到所有这些变体都是更一般的模式匹配构造的实例。 -在下面的例子中，我们将``even a``定义为``∃ b, a = 2 * b``，然后我们证明两个偶数的和是偶数。 +在下面的例子中，我们将 ``even a`` 定义为 ``∃ b, a = 2 * b``，然后我们证明两个偶数的和是偶数。 ```lean @@ -998,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 @@ -1016,7 +1014,7 @@ not the case that every ``x`` satisfies ``¬ p`` is not the same as having a particular ``x`` that satisfies ``p``. --> -就像构造主义的“或”比古典的“或”强，同样，构造的“存在”也比古典的“存在”强。例如，下面的推论需要经典推理，因为从构造的角度来看，知道并不是每一个``x``都满足``¬ p``，并不等于有一个特定的``x``满足``p``。 +就像构造主义的「或」比古典的「或」强，同样，构造的「存在」也比古典的「存在」强。例如，下面的推论需要经典推理，因为从构造的角度来看，知道并不是每一个 ``x`` 都满足 ``¬ p``，并不等于有一个特定的 ``x`` 满足 ``p``。 ```lean open Classical @@ -1070,7 +1068,7 @@ assumption that there is at least one element ``a`` of type ``α``. Here are solutions to two of the more difficult ones: --> -注意，第二个例子和最后两个例子要求假设至少有一个类型为``α``的元素``a``。 +注意，第二个例子和最后两个例子要求假设至少有一个类型为 ``α`` 的元素 ``a``。 以下是两个比较困难的问题的解： @@ -1131,9 +1129,9 @@ auxiliary goal without having to label it. We can refer to the last expression introduced in this way using the keyword ``this``: --> -我们已经看到像``fun``、``have``和``show``这样的关键字使得写出反映非正式数学证明结构的正式证明项成为可能。在本节中，我们将讨论证明语言的一些通常很方便的附加特性。 +我们已经看到像 ``fun``、``have`` 和 ``show`` 这样的关键字使得写出反映非正式数学证明结构的正式证明项成为可能。在本节中，我们将讨论证明语言的一些通常很方便的附加特性。 -首先，我们可以使用匿名的``have``表达式来引入一个辅助目标，而不需要标注它。我们可以使用关键字``this``'来引用最后一个以这种方式引入的表达式: +首先，我们可以使用匿名的 ``have`` 表达式来引入一个辅助目标，而不需要标注它。我们可以使用关键字 ``this``'来引用最后一个以这种方式引入的表达式: ```lean variable (f : Nat → Nat) @@ -1155,7 +1153,7 @@ the proof by writing ``by assumption``: 通常证明从一个事实转移到另一个事实，所以这可以有效地消除杂乱的大量标签。 -当目标可以推断出来时，我们也可以让Lean写``by assumption``来填写证明： +当目标可以推断出来时，我们也可以让 Lean 写 ``by assumption`` 来填写证明： ```lean # variable (f : Nat → Nat) @@ -1180,9 +1178,9 @@ symbols can also be used as French quotation marks. In fact, the notation is defined in Lean as follows: --> -这告诉Lean使用``assumption``策略，反过来，通过在局部上下文中找到合适的假设来证明目标。我们将在下一章学习更多关于``assumption``策略的内容。 +这告诉 Lean 使用 ``assumption`` 策略，反过来，通过在局部上下文中找到合适的假设来证明目标。我们将在下一章学习更多关于 ``assumption`` 策略的内容。 -我们也可以通过写``‹p›``的形式要求Lean填写证明，其中``p``是我们希望Lean在上下文中找到的证明命题。你可以分别使用``\f<``和``\f>``输入这些角引号。字母“f”表示“French”，因为unicode符号也可以用作法语引号。事实上，这个符号在Lean中定义如下: +我们也可以通过写 ``‹p›`` 的形式要求 Lean 填写证明，其中 ``p`` 是我们希望 Lean 在上下文中找到的证明命题。你可以分别使用 ``\f<`` 和 ``\f>`` 输入这些角引号。字母「f」表示「French」，因为 unicode 符号也可以用作法语引号。事实上，这个符号在 Lean 中定义如下: ```lean notation "‹" p "›" => show p by assumption @@ -1195,7 +1193,7 @@ explicitly. It also makes proofs more readable. Here is a more elaborate example: --> -这种方法比使用``by assumption``更稳健，因为需要推断的假设类型是显式给出的。它还使证明更具可读性。这里有一个更详细的例子: +这种方法比使用 ``by assumption`` 更稳健，因为需要推断的假设类型是显式给出的。它还使证明更具可读性。这里有一个更详细的例子: ```lean variable (f : Nat → Nat) @@ -1216,7 +1214,7 @@ introduced anonymously. Its use is also not limited to propositions, though using it for data is somewhat odd: --> -你可以这样使用法语引号来指代上下文中的“任何东西”，而不仅仅是匿名引入的东西。它的使用也不局限于命题，尽管将它用于数据有点奇怪： +你可以这样使用法语引号来指代上下文中的「任何东西」，而不仅仅是匿名引入的东西。它的使用也不局限于命题，尽管将它用于数据有点奇怪： ```lean example (n : Nat) : Nat := ‹Nat› @@ -1226,7 +1224,7 @@ example (n : Nat) : Nat := ‹Nat› Later, we show how you can extend the proof language using the Lean macro system. --> -稍后，我们将展示如何使用Lean中的宏系统扩展证明语言。 +稍后，我们将展示如何使用 Lean 中的宏系统扩展证明语言。 -3. 考虑“理发师悖论”：在一个小镇里，这里有一个（男性）理发师给所有不为自己刮胡子的人刮胡子。证明这里存在矛盾： +3. 考虑「理发师悖论」：在一个小镇里，这里有一个（男性）理发师给所有不为自己刮胡子的人刮胡子。证明这里存在矛盾： ```lean variable (men : Type) (barber : men) @@ -1301,7 +1299,7 @@ example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := sorry other statements, if necessary. --> -4. 如果没有任何参数，类型``Prop``的表达式只是一个断言。填入下面``prime``和``Fermat_prime``的定义，并构造每个给定的断言。例如，通过断言每个自然数``n``都有一个大于``n``的质数，你可以说有无限多个质数。哥德巴赫弱猜想指出，每一个大于5的奇数都是三个素数的和。如果有必要，请查阅费马素数的定义或其他任何资料。 +4. 如果没有任何参数，类型 ``Prop`` 的表达式只是一个断言。填入下面 ``prime`` 和 ``Fermat_prime`` 的定义，并构造每个给定的断言。例如，通过断言每个自然数 ``n`` 都有一个大于 ``n`` 的质数，你可以说有无限多个质数。哥德巴赫弱猜想指出，每一个大于5的奇数都是三个素数的和。如果有必要，请查阅费马素数的定义或其他任何资料。 ```lean def even (n : Nat) : Prop := sorry diff --git a/tactics.md b/tactics.md index 93c7b1e..9b6ea4c 100644 --- a/tactics.md +++ b/tactics.md @@ -29,11 +29,11 @@ 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自动化的途径，因为自动化程序本身就是策略。 +我们将把由策略序列组成的证明描述为「策略式」证明，前几章的证明我们称为「项式」证明。每种风格都有自己的优点和缺点。例如，策略式证明可能更难读，因为它们要求读者预测或猜测每条指令的结果。但它们一般更短，更容易写。此外，策略提供了一个使用 Lean 自动化的途径，因为自动化程序本身就是策略。 -从概念上讲，陈述一个定理或引入一个``have``的声明会产生一个目标，即构造一个具有预期类型的项的目标。例如, 下面创建的目标是构建一个类型为``p ∧ q ∧ p``的项，条件有常量``p q : Prop``，``hp : p``和``hq : q``。 +从概念上讲，陈述一个定理或引入一个 ``have`` 的声明会产生一个目标，即构造一个具有预期类型的项的目标。例如, 下面创建的目标是构建一个类型为 ``p ∧ q ∧ p`` 的项，条件有常量 ``p q : Prop``，``hp : p`` 和 ``hq : q``。 ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := @@ -80,10 +80,9 @@ separated by semicolons or line breaks. You can prove the theorem above in that way: --> -事实上，如果你把上面的例子中的“sorry”换成下划线，Lean会报告说，正是这个目标没有得到解决。 - -通常情况下，你会通过写一个明确的项来满足这样的目标。但在任何需要项的地方，Lean允许我们插入一个``by ``块，其中````是一串命令，用分号或换行符分开。你可以用下面这种方式来证明上面的定理： +事实上，如果你把上面的例子中的「sorry」换成下划线，Lean会报告说，正是这个目标没有得到解决。 +通常情况下，你会通过写一个明确的项来满足这样的目标。但在任何需要项的地方，Lean允许我们插入一个 ``by `` 块，其中 ```` 是一串命令，用分号或换行符分开。你可以用下面这种方式来证明上面的定理： ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := @@ -99,7 +98,7 @@ We often put the ``by`` keyword on the preceding line, and write the example above as: --> -我们经常将``by``关键字放在前一行，并将上面的例子写为 +我们经常将 ``by`` 关键字放在前一行，并将上面的例子写为 ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by @@ -119,7 +118,7 @@ them. In the example above, the command ``apply And.intro`` yields two subgoals: --> -``apply``策略应用于一个表达式，被视为表示一个有零或多个参数的函数。它将结论与当前目标中的表达式统一起来，并为剩余的参数创建新的目标，只要后面的参数不依赖于它们。在上面的例子中，命令``apply And.intro``产生了两个子目标： +``apply`` 策略应用于一个表达式，被视为表示一个有零或多个参数的函数。它将结论与当前目标中的表达式统一起来，并为剩余的参数创建新的目标，只要后面的参数不依赖于它们。在上面的例子中，命令 ``apply And.intro`` 产生了两个子目标： ``` case left @@ -148,7 +147,7 @@ this case, however, ``apply`` would work just as well. You can see the resulting proof term with the ``#print`` command: --> -第一个目标是通过``exact hp``命令来实现的。``exact``命令只是``apply``的一个变体，它表示所给的表达式应该准确地填充目标。在策略证明中使用它很有益，因为它如果失败那么表明出了问题。它也比``apply``更稳健，因为繁饰器在处理被应用的表达式时，会考虑到目标所预期的类型。然而，在这种情况下，``apply``也可以很好地工作。 +第一个目标是通过 ``exact hp`` 命令来实现的。``exact`` 命令只是 ``apply`` 的一个变体，它表示所给的表达式应该准确地填充目标。在策略证明中使用它很有益，因为它如果失败那么表明出了问题。它也比 ``apply`` 更稳健，因为繁饰器在处理被应用的表达式时，会考虑到目标所预期的类型。然而，在这种情况下，``apply`` 也可以很好地工作。 你可以用`#print`命令查看所产生的证明项。 @@ -178,7 +177,7 @@ identifiers. The following is a shorter version of the preceding proof: --> -你可以循序渐进地写一个策略脚本。在VS Code中，你可以通过按`Ctrl-Shift-Enter`打开一个窗口来显示信息，然后只要光标在策略块中，该窗口就会显示当前的目标。在Emacs中，你可以通过按`C-c C-g`看到任何一行末尾的目标，或者通过把光标放在最后一个策略的第一个字符之后，看到一个不完整的证明中的剩余目标。如果证明是不完整的，标记``by``会被装饰成一条红色的斜线，错误信息中包含剩余的目标。 +你可以循序渐进地写一个策略脚本。在VS Code中，你可以通过按`Ctrl-Shift-Enter`打开一个窗口来显示信息，然后只要光标在策略块中，该窗口就会显示当前的目标。在 Emacs 中，你可以通过按`C-c C-g`看到任何一行末尾的目标，或者通过把光标放在最后一个策略的第一个字符之后，看到一个不完整的证明中的剩余目标。如果证明是不完整的，标记 ``by`` 会被装饰成一条红色的斜线，错误信息中包含剩余的目标。 策略命令可以接受复合表达式，而不仅仅是单一标识符。下面是前面证明的一个简短版本。 @@ -222,7 +221,7 @@ notation ``case => ``. The following is a structured version of our first tactic proof in this chapter. --> -可能产生多个子目标的策略通常对子目标进行标记。例如，``apply And.intro``策略将第一个目标标记为``left``，将第二个目标标记为``right``。在``apply``策略的情况下，标签是从``And.intro``声明中使用的参数名称推断出来的。你可以使用符号``case => ``来结构化你的策略。下面是本章中第一个策略证明的结构化版本。 +可能产生多个子目标的策略通常对子目标进行标记。例如，``apply And.intro`` 策略将第一个目标标记为 ``left``，将第二个目标标记为 ``right``。在 ``apply`` 策略的情况下，标签是从 ``And.intro`` 声明中使用的参数名称推断出来的。你可以使用符号 ``case => `` 来结构化你的策略。下面是本章中第一个策略证明的结构化版本。 ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by @@ -239,7 +238,7 @@ You can solve the subgoal ``right`` before ``left`` using the ``case`` notation: --> -使用``case``标记，你也可以在``left``之前先解决子目标``right``： +使用 ``case`` 标记，你也可以在 ``left`` 之前先解决子目标 ``right``： ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by @@ -263,9 +262,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 @@ -291,7 +290,7 @@ of an identity from propositional logic that we proved in a previous chapter, now proved using tactics. --> -除了``apply``和``exact``之外，另一个有用的策略是``intro``，它引入了一个假设。下面是我们在前一章中证明的命题逻辑中的一个等价性的例子，现在用策略来证明。 +除了 ``apply`` 和 ``exact`` 之外，另一个有用的策略是 ``intro``，它引入了一个假设。下面是我们在前一章中证明的命题逻辑中的一个等价性的例子，现在用策略来证明。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -326,7 +325,7 @@ example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by The ``intro`` command can more generally be used to introduce a variable of any type: --> -``intro``命令可以更普遍地用于引入任何类型的变量。 +``intro`` 命令可以更普遍地用于引入任何类型的变量。 ```lean example (α : Type) : α → α := by @@ -358,7 +357,7 @@ form ``fun x => e``). As with lambda abstraction notation, the ``intro`` tactic allows us to use an implicit ``match``. --> -由于``apply``策略是一个用于交互式构造函数应用的命令，``intro``策略是一个用于交互式构造函数抽象的命令（即``fun x => e``形式的项）。 与lambda抽象符号一样，``intro``策略允许我们使用隐式的``match``。 +由于 ``apply`` 策略是一个用于交互式构造函数应用的命令，``intro`` 策略是一个用于交互式构造函数抽象的命令（即 ``fun x => e`` 形式的项）。 与 lambda 抽象符号一样，``intro`` 策略允许我们使用隐式的 ``match``。 ```lean example (α : Type) (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by @@ -370,7 +369,7 @@ example (α : Type) (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x You can also provide multiple alternatives like in the ``match`` expression. --> -就像``match``表达式一样，你也可以提供多个选项。 +就像 ``match`` 表达式一样，你也可以提供多个选项。 ```lean example (α : Type) (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := by @@ -389,9 +388,9 @@ the current goal, and if there is one matching the conclusion, it applies it. --> -``intros``策略可以在没有任何参数的情况下使用，在这种情况下，它选择名字并尽可能多地引入变量。稍后你会看到一个例子。 +``intros`` 策略可以在没有任何参数的情况下使用，在这种情况下，它选择名字并尽可能多地引入变量。稍后你会看到一个例子。 -``assumption``策略在当前目标的背景下查看假设，如果有一个与结论相匹配的假设，它就会应用这个假设。 +``assumption`` 策略在当前目标的背景下查看假设，如果有一个与结论相匹配的假设，它就会应用这个假设。 -下面的例子使用``intros``命令来自动引入三个变量和两个假设： +下面的例子使用 ``intros`` 命令来自动引入三个变量和两个假设： ```lean example : ∀ a b c : Nat, a = b → a = c → c = b := by @@ -456,7 +455,7 @@ ensure your tactic proofs do not rely on automatically generated names, and are However, you can use the combinator ``unhygienic`` to disable this restriction. --> -请注意，由Lean自动生成的名称在默认情况下是不可访问的。其动机是为了确保你的策略证明不依赖于自动生成的名字，并因此而更加强大。然而，你可以使用组合器``unhygienic``来禁用这一限制。 +请注意，由 Lean 自动生成的名称在默认情况下是不可访问的。其动机是为了确保你的策略证明不依赖于自动生成的名字，并因此而更加强大。然而，你可以使用组合器 ``unhygienic`` 来禁用这一限制。 ```lean example : ∀ a b c : Nat, a = b → a = c → c = b := by unhygienic @@ -473,7 +472,7 @@ In the following example, the tactic ``rename_i h1 _ h2`` renames two of the las your context. --> -你也可以使用``rename_i``策略来重命名你的上下文中最近的不能访问的名字。在下面的例子中，策略``rename_i h1 _ h2``在你的上下文中重命名了三个假设中的两个。 +你也可以使用 ``rename_i`` 策略来重命名你的上下文中最近的不能访问的名字。在下面的例子中，策略 ``rename_i h1 _ h2`` 在你的上下文中重命名了三个假设中的两个。 ```lean example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := by @@ -489,7 +488,7 @@ example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := by The ``rfl`` tactic is syntactic sugar for ``exact rfl``. --> -``rfl``策略是``exact rfl``的语法糖。 +``rfl`` 策略是 ``exact rfl`` 的语法糖。 ```lean example (y : Nat) : (fun x : Nat => 0) y = 0 := @@ -500,7 +499,7 @@ example (y : Nat) : (fun x : Nat => 0) y = 0 := The ``repeat`` combinator can be used to apply a tactic several times. --> -``repeat``组合器可以多次使用一个策略。 +``repeat`` 组合器可以多次使用一个策略。 ```lean example : ∀ a b c : Nat, a = b → a = c → c = b := by @@ -515,7 +514,7 @@ Another tactic that is sometimes useful is the ``revert`` tactic, which is, in a sense, an inverse to ``intro``. --> -另一个有时很有用的策略是还原``revert``策略，从某种意义上说，它是对``intro``的逆。 +另一个有时很有用的策略是还原 ``revert`` 策略，从某种意义上说，它是对 ``intro`` 的逆。 ```lean example (x : Nat) : x = x := by @@ -549,7 +548,7 @@ context that depend on it. For example, reverting ``x`` in the example above brings ``h`` along with it: --> -但是`revert`更聪明，因为它不仅会还原上下文中的一个元素，还会还原上下文中所有依赖它的后续元素。例如，在上面的例子中，还原`x`会带来`h`。 +但是 `revert` 更聪明，因为它不仅会还原上下文中的一个元素，还会还原上下文中所有依赖它的后续元素。例如，在上面的例子中，还原 `x` 会带来 `h`。 ```lean example (x y : Nat) (h : x = y) : y = x := by @@ -582,7 +581,7 @@ expression in the goal by a fresh variable using the ``generalize`` tactic. --> -你只能``revert``局部环境中的一个元素，也就是一个局部变量或假设。但是你可以使用泛化``generalize``策略将目标中的任意表达式替换为新的变量。 +你只能 ``revert`` 局部环境中的一个元素，也就是一个局部变量或假设。但是你可以使用泛化 ``generalize`` 策略将目标中的任意表达式替换为新的变量。 ```lean example : 3 = 3 := by @@ -603,7 +602,7 @@ every generalization preserves the validity of the goal. Here, ``rfl`` with one that is not provable: --> -上述符号的记忆法是，你通过将``3``设定为任意变量``x``来泛化目标。要注意：不是每一个泛化都能保留目标的有效性。这里，`generalize`用一个无法证明的目标取代了一个可以用``rfl``证明的目标。 +上述符号的记忆法是，你通过将 ``3`` 设定为任意变量 ``x`` 来泛化目标。要注意：不是每一个泛化都能保留目标的有效性。这里，`generalize` 用一个无法证明的目标取代了一个可以用 ``rfl`` 证明的目标。 ```lean example : 2 + 3 = 5 := by @@ -622,7 +621,7 @@ label, and ``generalize`` uses it to store the assignment in the local context: --> -在这个例子中，``admit``策略是``sorry``证明项的类似物。它关闭了当前的目标，产生了通常的警告：使用了``sorry``。为了保持之前目标的有效性，`generalize`策略允许我们记录`3`已经被`x`所取代的事实。你所需要做的就是提供一个标签，`generalize`使用它来存储局部上下文中的赋值。 +在这个例子中，``admit`` 策略是 ``sorry`` 证明项的类似物。它关闭了当前的目标，产生了通常的警告：使用了 ``sorry``。为了保持之前目标的有效性，`generalize` 策略允许我们记录 `3` 已经被 `x` 所取代的事实。你所需要做的就是提供一个标签，`generalize` 使用它来存储局部上下文中的赋值。 ```lean example : 2 + 3 = 5 := by @@ -636,7 +635,7 @@ Here the ``rewrite`` tactic, abbreviated ``rw``, uses ``h`` to replace ``x`` by ``3`` again. The ``rewrite`` tactic will be discussed below. --> -这里``rewrite``策略，缩写为``rw``，用``h``把``x``用``3``换了回来。``rewrite``策略下文将继续讨论。 +这里 ``rewrite`` 策略，缩写为 ``rw``，用 ``h`` 把 ``x`` 用 ``3`` 换了回来。``rewrite`` 策略下文将继续讨论。 -一些额外的策略对于建构和析构命题以及数据很有用。例如，当应用于形式为``p ∨ q``的目标时，你可以使用``apply Or.inl``和``apply Or.inr``等策略。 反之，``cases``策略可以用来分解一个析取。 +一些额外的策略对于建构和析构命题以及数据很有用。例如，当应用于形式为 ``p ∨ q`` 的目标时，你可以使用 ``apply Or.inl`` 和 ``apply Or.inr`` 等策略。 反之，``cases`` 策略可以用来分解一个析取。 ```lean example (p q : Prop) : p ∨ q → q ∨ p := by @@ -669,7 +668,7 @@ Note that the syntax is similar to the one used in `match` expressions. The new subgoals can be solved in any order. --> -注意，该语法与`match`表达式中使用的语法相似。新的子目标可以按任何顺序解决。 +注意，该语法与 `match` 表达式中使用的语法相似。新的子目标可以按任何顺序解决。 ```lean example (p q : Prop) : p ∨ q → q ∨ p := by @@ -684,7 +683,7 @@ You can also use a (unstructured) ``cases`` without the ``with`` and a tactic for each alternative. --> -你也可以使用一个（非结构化的）`cases`，而不使用`with`，并为每个备选情况制定一个策略。 +你也可以使用一个（非结构化的）`cases`，而不使用 `with`，并为每个备选情况制定一个策略。 ```lean example (p q : Prop) : p ∨ q → q ∨ p := by @@ -701,7 +700,7 @@ The (unstructured) ``cases`` is particularly useful when you can close several subgoals using the same tactic. --> -（非结构化的）`cases`在你可以用同一个策略来解决子任务时格外有用。 +（非结构化的）`cases` 在你可以用同一个策略来解决子任务时格外有用。 ```lean example (p : Prop) : p ∨ p → p := by @@ -715,7 +714,7 @@ You can also use the combinator ``tac1 <;> tac2`` to apply ``tac2`` to each subgoal produced by tactic ``tac1``. --> -你也可以使用组合器``tac1 <;> tac2``，将``tac2``应用于策略``tac1``产生的每个子目标。 +你也可以使用组合器 ``tac1 <;> tac2``，将 ``tac2`` 应用于策略 ``tac1`` 产生的每个子目标。 ```lean example (p : Prop) : p ∨ p → p := by @@ -727,7 +726,7 @@ example (p : Prop) : p ∨ p → p := by You can combine the unstructured ``cases`` tactic with the ``case`` and ``.`` notation. --> -你可以与``.``符号相结合使用非结构化的``cases``策略。 +你可以与 ``.`` 符号相结合使用非结构化的 ``cases`` 策略。 ```lean example (p q : Prop) : p ∨ q → q ∨ p := by @@ -763,7 +762,7 @@ The ``cases`` tactic can also be used to decompose a conjunction. --> -``cases``策略也被用来分解一个析取。 +``cases`` 策略也被用来分解一个析取。 ```lean example (p q : Prop) : p ∧ q → q ∧ p := by @@ -780,7 +779,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 @@ -809,7 +808,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 @@ -828,7 +827,7 @@ to specify a witness to the existential quantifier explicitly, you can use the ``exists`` tactic instead: --> -在这里，``constructor``策略将存在性断言的第一个组成部分，即``x``的值，保留为隐式的。它是由一个元变量表示的，这个元变量以后应该被实例化。在前面的例子中，元变量的正确值是由策略``exact px``决定的，因为``px``的类型是``p x``。如果你想明确指定存在量词的存在者，你可以使用`exists`策略来代替。 +在这里，``constructor`` 策略将存在性断言的第一个组成部分，即 ``x`` 的值，保留为隐式的。它是由一个元变量表示的，这个元变量以后应该被实例化。在前面的例子中，元变量的正确值是由策略 ``exact px`` 决定的，因为 ``px`` 的类型是 ``p x``。如果你想明确指定存在量词的存在者，你可以使用 `exists` 策略来代替。 ```lean example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := by @@ -881,7 +880,7 @@ for conjunction and disjunction. The ``cases`` tactic will also do a case distinction on a natural number: --> -在我们为变量选择的名称之前，它们的定义与有关合取和析取的类似命题的证明是相同的。``cases``策略也会对自然数进行逐情况区分： +在我们为变量选择的名称之前，它们的定义与有关合取和析取的类似命题的证明是相同的。``cases`` 策略也会对自然数进行逐情况区分： ```lean open Nat @@ -898,9 +897,9 @@ the [Tactics for Inductive Types](./inductive_types.md#tactics-for-inductive-typ The ``contradiction`` tactic searches for a contradiction among the hypotheses of the current goal: --> -``cases``策略伙同``induction``策略将在[归纳类型的策略](./inductive_types.md#_tactics_for_inductive_types)一节中详述。 +``cases`` 策略伙同 ``induction`` 策略将在[归纳类型的策略](./inductive_types.md#_tactics_for_inductive_types)一节中详述。 -``contradiction``策略搜索当前目标的假设中的矛盾： +``contradiction`` 策略搜索当前目标的假设中的矛盾： ```lean example (p q : Prop) : p ∧ ¬ p → q := by @@ -913,7 +912,7 @@ example (p q : Prop) : p ∧ ¬ p → q := by You can also use ``match`` in tactic blocks. --> -你也可以在策略块中使用``match``： +你也可以在策略块中使用 ``match``： ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -932,7 +931,7 @@ example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by You can "combine" ``intro h`` with ``match h ...`` and write the previous examples as follows --> -你可以将``intro h``与``match h ...``结合起来，然后上例就可以如下地写出： +你可以将 ``intro h`` 与 ``match h ...`` 结合起来，然后上例就可以如下地写出： ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -971,7 +970,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 @@ -1011,7 +1010,7 @@ goal that is about to be solved, while remaining in tactic mode. --> -事实上，有一个``show``策略，它类似于证明项中的``show``表达式。它只是简单地声明即将被解决的目标的类型，同时保持策略模式。 +事实上，有一个 ``show`` 策略，它类似于证明项中的 ``show`` 表达式。它只是简单地声明即将被解决的目标的类型，同时保持策略模式。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -1038,7 +1037,7 @@ example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by The ``show`` tactic can actually be used to rewrite a goal to something definitionally equivalent: --> -``show``策略其实可以被用来重写一些定义等价的目标： +``show`` 策略其实可以被用来重写一些定义等价的目标： ```lean example (n : Nat) : n + 1 = Nat.succ n := by @@ -1050,7 +1049,7 @@ example (n : Nat) : n + 1 = Nat.succ n := by There is also a ``have`` tactic, which introduces a new subgoal, just as when writing proof terms: --> -还有一个``have``策略，它引入了一个新的子目标，就像写证明项时一样。 +还有一个 ``have`` 策略，它引入了一个新的子目标，就像写证明项时一样。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by @@ -1072,7 +1071,7 @@ As with proof terms, you can omit the label in the ``have`` tactic, in which case, the default label ``this`` is used: --> -与证明项一样，你可以省略``have``策略中的标签，在这种情况下，将使用默认标签``this``： +与证明项一样，你可以省略 ``have`` 策略中的标签，在这种情况下，将使用默认标签 ``this``： ```lean example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by @@ -1096,7 +1095,7 @@ notation, you can even omit both the type and the label, in which case the new fact is introduced with the label ``this``. --> -``have``策略中的类型可以省略，所以你可以写``have hp := h.left``和``have hqr := h.right``。 事实上，使用这种符号，你甚至可以省略类型和标签，在这种情况下，新的事实是用标签``this``引入的。 +``have`` 策略中的类型可以省略，所以你可以写 ``have hp := h.left`` 和 ``have hqr := h.right``。 事实上，使用这种符号，你甚至可以省略类型和标签，在这种情况下，新的事实是用标签 ``this`` 引入的。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by @@ -1117,7 +1116,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 @@ -1140,9 +1139,9 @@ to detect whether the tactic block ends. Alternatively, you can define tactic blocks using curly braces and semicolons. --> -和``have``一样，你可以通过写``let a := 3 * 2``来保留类型为隐式。``let``和``have``的区别在于，``let``在上下文中引入了一个局部定义，因此局部声明的定义可以在证明中展开。 +和 ``have`` 一样，你可以通过写 ``let a := 3 * 2`` 来保留类型为隐式。``let`` 和 ``have`` 的区别在于，``let`` 在上下文中引入了一个局部定义，因此局部声明的定义可以在证明中展开。 -我们使用了`.`来创建嵌套的策略块。 在一个嵌套块中，Lean专注于第一个目标，如果在该块结束时还没有完全解决，就会产生一个错误。这对于表明一个策略所引入的多个子目标的单独证明是有帮助的。符号``.``是对空格敏感的，并且依靠缩进来检测策略块是否结束。另外，你也可以用大括号和分号来定义策略块。 +我们使用了`.`来创建嵌套的策略块。 在一个嵌套块中，Lean专注于第一个目标，如果在该块结束时还没有完全解决，就会产生一个错误。这对于表明一个策略所引入的多个子目标的单独证明是有帮助的。符号 ``.`` 是对空格敏感的，并且依靠缩进来检测策略块是否结束。另外，你也可以用大括号和分号来定义策略块。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -1171,7 +1170,7 @@ theorem ``foo`` to a single goal produces four subgoals, one would expect the proof to look like this: --> -使用缩进来构造证明很有用：每次一个策略留下一个以上的子目标时，我们通过将它们封装在块中并缩进来分隔剩下的子目标。因此，如果将定理``foo``应用于一个目标产生了四个子目标，那么我们就可以期待这样的证明： +使用缩进来构造证明很有用：每次一个策略留下一个以上的子目标时，我们通过将它们封装在块中并缩进来分隔剩下的子目标。因此，如果将定理 ``foo`` 应用于一个目标产生了四个子目标，那么我们就可以期待这样的证明： ``` apply foo @@ -1222,7 +1221,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 := @@ -1238,7 +1237,7 @@ In ``t₁ <;> t₂``, the ``<;>`` operator provides a *parallel* version of the ``t₁`` is applied to the current goal, and then ``t₂`` is applied to *all* the resulting subgoals: --> -这里，`apply Or.inl; assumption`在功能上等同于一个单独的策略，它首先应用`apply Or.inl`，然后应用`assumption`。 +这里，`apply Or.inl; assumption`在功能上等同于一个单独的策略，它首先应用`apply Or.inl`，然后应用 `assumption`。 在`t₁ <;> t₂`中，`<;>`操作符提供了一个*并行*的序列操作。`t₁`被应用于当前目标，然后`t₂`被应用于*所有*产生的子目标： @@ -1257,7 +1256,7 @@ The ``first | t₁ | t₂ | ... | tₙ`` applies each `tᵢ` until one succeeds, 当所产生的目标能够以统一的方式完成时，或者，至少，当有可能以统一的方式在所有的目标上取得进展时，这就特别有用。 -``first | t₁ | t₂ | ... | tₙ``应用每个`tᵢ`，直到其中一个成功，否则就失败： +``first | t₁ | t₂ | ... | tₙ`` 应用每$1 $2，直到其中一个成功，否则就失败： ```lean example (p q : Prop) (hp : p) : p ∨ q := by @@ -1305,7 +1304,7 @@ succeeds. 该策略试图通过假设立即解决左边的析取项；如果失败，它就试图关注右边的析取项；如果不成功，它就调用假设策略。 -毫无疑问，策略可能会失败。事实上，正是这种“失败”状态导致`first`组合器回溯并尝试下一个策略。``try``组合器建立了一个总是成功的策略，尽管可能是以一种平凡的方式：``try t``执行``t``并报告成功，即使``t``失败。它等同于``first | t | skip``，其中``skip``是一个什么都不做的策略（并且成功地做到了“什么都不做”）。在下一个例子中，第二个`constructor`在右边的合取项``q ∧ r``上成功了（注意，合取和析取是右结合的），但在第一个合取项上失败。`try`策略保证了序列组合的成功。 +毫无疑问，策略可能会失败。事实上，正是这种「失败」状态导致 `first` 组合器回溯并尝试下一个策略。``try`` 组合器建立了一个总是成功的策略，尽管可能是以一种平凡的方式：``try t`` 执行 ``t`` 并报告成功，即使 ``t`` 失败。它等同于 ``first | t | skip``，其中 ``skip`` 是一个什么都不做的策略（并且成功地做到了「什么都不做」）。在下一个例子中，第二个 `constructor` 在右边的合取项 ``q ∧ r`` 上成功了（注意，合取和析取是右结合的），但在第一个合取项上失败。`try` 策略保证了序列组合的成功。 ```lean example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by @@ -1321,9 +1320,9 @@ to multiple goals, but there are other ways to do this. For example, ``all_goals t`` applies ``t`` to all open goals: --> -小心：``repeat (try t)``将永远循环，因为内部策略永远不会失败。 +小心：``repeat (try t)`` 将永远循环，因为内部策略永远不会失败。 -在一个证明中，往往有多个目标未完成。并行序列是一种布置方式，以便将一个策略应用于多个目标，但也有其他的方式可以做到这一点。例如，`all_goals t`将`t`应用于所有未完成的目标： +在一个证明中，往往有多个目标未完成。并行序列是一种布置方式，以便将一个策略应用于多个目标，但也有其他的方式可以做到这一点。例如，`all_goals t`将 `t` 应用于所有未完成的目标： ```lean example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by @@ -1338,7 +1337,7 @@ It is similar to ``all_goals``, except it succeeds if its argument succeeds on at least one goal. --> -在这种情况下，``any_goals``策略提供了一个更稳健的解决方案。它与``all_goals``类似，只是除非它的参数至少在一个目标上成功，否则就会失败。 +在这种情况下，``any_goals`` 策略提供了一个更稳健的解决方案。它与 ``all_goals`` 类似，只是除非它的参数至少在一个目标上成功，否则就会失败。 ```lean example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by @@ -1352,7 +1351,7 @@ The first tactic in the ``by`` block below repeatedly splits conjunctions: --> -下面``by``块中的第一个策略是反复拆分合取： +下面 ``by`` 块中的第一个策略是反复拆分合取： ```lean example (p q r : Prop) (hp : p) (hq : q) (hr : r) : @@ -1380,7 +1379,7 @@ ordinarily only effects the current goal, ``focus (all_goals t)`` has the same effect as ``t``. --> -组合器``focus t``确保``t``只影响当前的目标，暂时将其他目标从作用范围中隐藏。因此，如果`t`通常只影响当前目标，`focus (all_goals t)`与`t`具有相同的效果。 +组合器 ``focus t`` 确保 ``t`` 只影响当前的目标，暂时将其他目标从作用范围中隐藏。因此，如果 `t` 通常只影响当前目标，`focus (all_goals t)`与 `t` 具有相同的效果。 -在[计算式证明](./quantifiers_and_equality.md#计算式证明)一节中简要介绍了``rewrite``策略（简称``rw``）和 ``simp``策略。在本节和下一节中，我们将更详细地讨论它们。 +在[计算式证明](./quantifiers_and_equality.md#计算式证明)一节中简要介绍了 ``rewrite`` 策略（简称 ``rw``）和 ``simp`` 策略。在本节和下一节中，我们将更详细地讨论它们。 -``rewrite``策略提供了一种基本的机制，可以将替换应用于目标和假设，在处理等式时非常方便。该策略的最基本形式是``rewrite [t]``，其中``t``是一个类型断定为等式的项。例如，`t`可以是上下文中的一个假设`h : x = y`；可以是一个一般的法则，如`add_comm : ∀ x y, x + y = y + x`，在这个法则中，重写策略试图找到`x`和`y`的合适实例；或者可以是任何断言具体或一般等式的复合项。在下面的例子中，我们使用这种基本形式，用一个假设重写目标。 +``rewrite`` 策略提供了一种基本的机制，可以将替换应用于目标和假设，在处理等式时非常方便。该策略的最基本形式是 ``rewrite [t]``，其中 ``t`` 是一个类型断定为等式的项。例如，`t` 可以是上下文中的一个假设`h : x = y`；可以是一个一般的法则，如`add_comm : ∀ x y, x + y = y + x`，在这个法则中，重写策略试图找到 `x` 和 `y` 的合适实例；或者可以是任何断言具体或一般等式的复合项。在下面的例子中，我们使用这种基本形式，用一个假设重写目标。 -在上面的例子中，第一次使用``rw``将目标``f k = 0``中的``k``替换成``0``。然后，第二次用``0``替换``f 0``。该策略自动关闭任何形式的目标`t = t`。下面是一个使用复合表达式进行重写的例子。 +在上面的例子中，第一次使用 ``rw`` 将目标 ``f k = 0`` 中的 ``k`` 替换成 ``0``。然后，第二次用 ``0`` 替换 ``f 0``。该策略自动关闭任何形式的目标`t = t`。下面是一个使用复合表达式进行重写的例子。 ```lean example (x y : Nat) (p : Nat → Prop) (q : Prop) (h : q → x = y) @@ -1447,7 +1446,7 @@ Multiple rewrites can be combined using the notation ``rw [t_1, ..., t_n]``, which is just shorthand for ``rw [t_1]; ...; rw [t_n]``. The previous example can be written as follows: --> -这里，``h hq``建立了等式``x = y``。``h hq``周围的括号是不必要的，但为了清楚起见，还是加上了括号。 +这里，``h hq`` 建立了等式 ``x = y``。``h hq`` 周围的括号是不必要的，但为了清楚起见，还是加上了括号。 多个重写可以使用符号`rw [t_1, ..., t_n]`来组合，这只是`rw t_1; ...; rw t_n`的缩写。前面的例子可以写成如下： @@ -1463,7 +1462,7 @@ right-hand side. The notation ``←t`` can be used to instruct the tactic to use the equality ``t`` in the reverse direction. --> -默认情况下，``rw``正向使用一个等式，用一个表达式匹配左边的等式，然后用右边的等式替换它。符号``←t``可以用来指示策略在反方向上使用等式``t``。 +默认情况下，``rw`` 正向使用一个等式，用一个表达式匹配左边的等式，然后用右边的等式替换它。符号 ``←t`` 可以用来指示策略在反方向上使用等式 ``t``。 ```lean example (f : Nat → Nat) (a b : Nat) (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := by @@ -1482,9 +1481,9 @@ you want, you can use additional arguments to specify the appropriate subterm. --> -在这个例子中，项``←h₁``指示重写器用``a``替换``b``。在编辑器中，你可以用``\l``输入反箭头。你也可以使用ascii替代品``<-``。 +在这个例子中，项 ``←h₁`` 指示重写器用 ``a`` 替换 ``b``。在编辑器中，你可以用 ``\l`` 输入反箭头。你也可以使用 ascii 替代品 ``<-``。 -有时一个等式的左侧可以匹配模式中的多个子项，在这种情况下，``rw``策略会在遍历项时选择它发现的第一个匹配。如果这不是你想要的，你可以使用附加参数来指定适当的子项。 +有时一个等式的左侧可以匹配模式中的多个子项，在这种情况下，``rw`` 策略会在遍历项时选择它发现的第一个匹配。如果这不是你想要的，你可以使用附加参数来指定适当的子项。 ```lean example (a b c : Nat) : a + b + c = a + c + b := by @@ -1513,9 +1512,9 @@ By default, the ``rewrite`` tactic affects only the goal. The notation ``rw [t] at h`` applies the rewrite ``t`` at hypothesis ``h``. --> -在上面的第一个例子中，第一步将``a + b + c``重写为``a + (b + c)``。然后，接下来对项``b + c``使用交换律；如果不指定参数，该策略将把``a + (b + c)``重写为``(b + c) + a``。最后一步以相反的方向应用结合律，将`a + (c + b)`改写为``a + c + b``。接下来的两个例子则是应用结合律将两边的小括号移到右边，然后将``b``和``c``调换。注意最后一个例子通过指定``Nat.add_comm``的第二个参数来指定重写应该在右侧进行。 +在上面的第一个例子中，第一步将 ``a + b + c`` 重写为 ``a + (b + c)``。然后，接下来对项 ``b + c`` 使用交换律；如果不指定参数，该策略将把 ``a + (b + c)`` 重写为 ``(b + c) + a``。最后一步以相反的方向应用结合律，将`a + (c + b)`改写为 ``a + c + b``。接下来的两个例子则是应用结合律将两边的小括号移到右边，然后将 ``b`` 和 ``c`` 调换。注意最后一个例子通过指定 ``Nat.add_comm`` 的第二个参数来指定重写应该在右侧进行。 -默认情况下，``rewrite``策略只影响目标。符号``rw [t] at h``在假设``h``处应用重写``t``。 +默认情况下，``rewrite`` 策略只影响目标。符号 ``rw [t] at h`` 在假设 ``h`` 处应用重写 ``t``。 ```lean example (f : Nat → Nat) (a : Nat) (h : a + 0 = 0) : f a = f 0 := by @@ -1531,9 +1530,9 @@ The ``rewrite`` tactic is not restricted to propositions. In the following example, we use ``rw [h] at t`` to rewrite the hypothesis ``t : Tuple α n`` to ``t : Tuple α 0``. --> -第一步，``rw [Nat.add_zero] at h``将假设``a + 0 = 0``改写为``a = 0``。然后，新的假设`a = 0`被用来把目标重写为`f 0 = f 0`。 +第一步，``rw [Nat.add_zero] at h`` 将假设 ``a + 0 = 0`` 改写为 ``a = 0``。然后，新的假设`a = 0`被用来把目标重写为`f 0 = f 0`。 -``rewrite``策略不限于命题。在下面的例子中，我们用`rw [h] at t`来重写假设`t : Tuple α n`为`t : Tuple α 0`。 +``rewrite`` 策略不限于命题。在下面的例子中，我们用`rw [h] at t`来重写假设`t : Tuple α n`为`t : Tuple α 0`。 ```lean def Tuple (α : Type) (n : Nat) := @@ -1560,7 +1559,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 @@ -1581,7 +1580,7 @@ finishes it off. Here are some more examples with lists: --> -在第一个例子中，目标中等式的左侧被简化，使用涉及0和1的通常的同义词，将目标简化为`x * y = x * y'`。此时`simp'`应用反身性（rfl）来完成它。在第二个例子中，`simp`将目标化简为`p (x * y)`，这时假设`h`完成了它。下面是一些关于列表的例子。 +在第一个例子中，目标中等式的左侧被简化，使用涉及0和1的通常的同义词，将目标简化为`x * y = x * y'`。此时`simp'`应用反身性（rfl）来完成它。在第二个例子中，`simp` 将目标化简为`p (x * y)`，这时假设 `h` 完成了它。下面是一些关于列表的例子。 ```lean open List @@ -1599,7 +1598,7 @@ example (xs ys : List α) As with ``rw``, you can use the keyword ``at`` to simplify a hypothesis: --> -就像``rw``，你也可以用关键字``at``来简化一个假设： +就像 ``rw``，你也可以用关键字 ``at`` 来简化一个假设： ```lean example (x y z : Nat) (p : Nat → Prop) @@ -1611,7 +1610,7 @@ example (x y z : Nat) (p : Nat → Prop) Moreover, you can use a "wildcard" asterisk to simplify all the hypotheses and the goal: --> -此外，你可以使用一个“通配符”星号来简化所有的假设和目标： +此外，你可以使用一个「通配符」星号来简化所有的假设和目标： ```lean attribute [local simp] Nat.mul_comm Nat.mul_assoc Nat.mul_left_comm @@ -1648,7 +1647,7 @@ associativity and commutativity are then rewritten to the same canonical form. --> -上例中前两行的意思是，对于具有交换律和结合律的运算（如自然数的加法和乘法），简化器使用这两个定律来重写表达式，同时还使用*左交换律*。在乘法的情况下，左交换律表达如下：``x * (y * z) = y * (x * z)``。`local`修饰符告诉简化器在当前文件（或小节或命名空间，视情况而定）中使用这些规则。交换律和左交换律是有一个问题是，重复应用其中一个会导致循环。但是简化器检测到了对其参数进行置换的特性，并使用了一种被称为*有序重写*的技术。这意味着系统保持着项的内部次序，只有在这样做会降低次序的情况下才会应用等式。对于上面提到的三个等式，其效果是表达式中的所有小括号都被结合到右边，并且表达式以一种规范的（尽管有些随意）方式排序。两个在交换律和结合律上等价的表达式然后被改写成相同的规范形式。 +上例中前两行的意思是，对于具有交换律和结合律的运算（如自然数的加法和乘法），简化器使用这两个定律来重写表达式，同时还使用*左交换律*。在乘法的情况下，左交换律表达如下：``x * (y * z) = y * (x * z)``。`local` 修饰符告诉简化器在当前文件（或小节或命名空间，视情况而定）中使用这些规则。交换律和左交换律是有一个问题是，重复应用其中一个会导致循环。但是简化器检测到了对其参数进行置换的特性，并使用了一种被称为*有序重写*的技术。这意味着系统保持着项的内部次序，只有在这样做会降低次序的情况下才会应用等式。对于上面提到的三个等式，其效果是表达式中的所有小括号都被结合到右边，并且表达式以一种规范的（尽管有些随意）方式排序。两个在交换律和结合律上等价的表达式然后被改写成相同的规范形式。 ```lean # attribute [local simp] Nat.mul_comm Nat.mul_assoc Nat.mul_left_comm @@ -1671,7 +1670,7 @@ added to the collection of identities that are used to simplify a term. --> -与``rewrite``一样，你可以向``simp``提供一个要使用的事实列表，包括一般引理、局部假设、要展开的定义和复合表达式。`simp`策略也能识别`rewrite`的`←t`语法。在任何情况下，额外的规则都会被添加到用于简化项的等式集合中。 +与 ``rewrite`` 一样，你可以向 ``simp`` 提供一个要使用的事实列表，包括一般引理、局部假设、要展开的定义和复合表达式。`simp` 策略也能识别 `rewrite` 的`←t`语法。在任何情况下，额外的规则都会被添加到用于简化项的等式集合中。 ```lean def f (m n : Nat) : Nat := @@ -1697,7 +1696,7 @@ To use all the hypotheses present in the local context when simplifying, we can use the wildcard symbol, ``*``: --> -为了在简化时使用局部环境中存在的所有假设，我们可以使用通配符``*``： +为了在简化时使用局部环境中存在的所有假设，我们可以使用通配符 ``*``： ```lean example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by @@ -1723,7 +1722,7 @@ q`` to ``true``, which it then proves trivially. Iterating such rewrites produces nontrivial propositional reasoning. --> -简化器也会进行命题重写。例如，使用假设``p``，它把``p ∧ q``改写为``q``，把``p ∨ q``改写为``true``，然后以普通方式证明。迭代这样的重写，会生成非平凡的命题推理。 +简化器也会进行命题重写。例如，使用假设 ``p``，它把 ``p ∧ q`` 改写为 ``q``，把 ``p ∨ q`` 改写为 ``true``，然后以普通方式证明。迭代这样的重写，会生成非平凡的命题推理。 ```lean example (p q : Prop) (hp : p) : p ∧ q ↔ q := by @@ -1769,7 +1768,7 @@ Then for any list ``xs``, ``reverse (mk_symm xs)`` is equal to ``mk_symm xs``, which can easily be proved by unfolding the definition: --> -那么对于任何列表``xs``，``reverse (mk_symm xs)``等于``mk_symm xs``，这可以通过展开定义轻松证明： +那么对于任何列表 ``xs``，``reverse (mk_symm xs)`` 等于 ``mk_symm xs``，这可以通过展开定义轻松证明： ```lean # def mk_symm (xs : List α) := @@ -1808,7 +1807,7 @@ achieve that by marking it as a simplification rule when the theorem is defined: --> -但是使用`reverse_mk_symm`通常是正确的，如果用户不需要明确地调用它，那就更好了。你可以通过在定义该定理时将其标记为简化规则来实现这一点： +但是使用 `reverse_mk_symm` 通常是正确的，如果用户不需要明确地调用它，那就更好了。你可以通过在定义该定理时将其标记为简化规则来实现这一点： ```lean # def mk_symm (xs : List α) := @@ -1832,7 +1831,7 @@ The notation ``@[simp]`` declares ``reverse_mk_symm`` to have the ``[simp]`` attribute, and can be spelled out more explicitly: --> -符号``@[simp]``声明``reverse_mk_symm``具有``[simp]``属性，可以更明确地说明： +符号 ``@[simp]`` 声明 ``reverse_mk_symm`` 具有 ``[simp]`` 属性，可以更明确地说明： ```lean # def mk_symm (xs : List α) := @@ -1886,7 +1885,7 @@ attribute is assigned. As we will discuss further in current file or section using the ``local`` modifier: --> -然而，一旦属性被应用，就没有办法永久地删除它；它将在任何导入该属性的文件中持续存在。正如我们将在[属性](./interacting_with_lean.md#属性)一章中进一步讨论的那样，我们可以使用``local``修饰符将属性的范围限制在当前文件或章节中： +然而，一旦属性被应用，就没有办法永久地删除它；它将在任何导入该属性的文件中持续存在。正如我们将在[属性](./interacting_with_lean.md#属性)一章中进一步讨论的那样，我们可以使用 ``local`` 修饰符将属性的范围限制在当前文件或章节中： ```lean # def mk_symm (xs : List α) := @@ -1927,11 +1926,11 @@ rules. In the examples below, the minus sign and ``only`` are used to block the application of ``reverse_mk_symm``. --> -在该部分之外，简化器将不再默认使用``reverse_mk_symm``。 +在该部分之外，简化器将不再默认使用 ``reverse_mk_symm``。 -请注意，我们讨论过的各种`simp`选项----给出一个明确的规则列表，并使用`at`指定位置----可以合并，但它们的排列顺序是严格的。你可以在编辑器中看到正确的顺序，把光标放在``simp``标识符上，查看与之相关的文档。 +请注意，我们讨论过的各种 `simp` 选项----给出一个明确的规则列表，并使用 `at` 指定位置----可以合并，但它们的排列顺序是严格的。你可以在编辑器中看到正确的顺序，把光标放在 ``simp`` 标识符上，查看与之相关的文档。 -有两个额外的修饰符是有用的。默认情况下，``simp``包括所有被标记为``[simp]``属性的定理。写`simp only`排除了这些默认值，允许你使用一个更明确的规则列表。在下面的例子中，减号和``only``被用来阻止``reverse_mk_symm``的应用： +有两个额外的修饰符是有用的。默认情况下，``simp`` 包括所有被标记为 ``[simp]`` 属性的定理。写`simp only`排除了这些默认值，允许你使用一个更明确的规则列表。在下面的例子中，减号和 ``only`` 被用来阻止 ``reverse_mk_symm`` 的应用： ```lean def mk_symm (xs : List α) := @@ -1960,7 +1959,7 @@ example (xs ys : List Nat) (p : List Nat → Prop) The `simp` tactic has many configuration options. For example, we can enable contextual simplifications as follows. --> -`simp`策略有很多配置选项，例如，我们可以启用语境简化： +`simp` 策略有很多配置选项，例如，我们可以启用语境简化： ```lean example : if x = 0 then y + x = y else x ≠ 0 := by @@ -1972,7 +1971,7 @@ when `contextual := true`, `simp` uses the fact that `x = 0` when simplifying `y `x ≠ 0` when simplifying the other branch. Here is another example. --> -当`contextual := true`，`simp`简化`y + x = y`时会使用`x = 0`，同时会用`x ≠ 0`来简化另一侧。另一个例子： +当`contextual := true`，`simp` 简化`y + x = y`时会使用`x = 0`，同时会用`x ≠ 0`来简化另一侧。另一个例子： ```lean example : ∀ (x : Nat) (h : x = 0), y + x = y := by @@ -1984,7 +1983,7 @@ Another useful configuration option is `arith := true` which enables arithmetica that `simp_arith` is a shorthand for `simp (config := { arith := true })`. --> -另一个有用的配置是`arith := true`，它会简化算术表达式。因为这太常用了所以用`simp_arith`作为`simp (config := { arith := true })`的缩写。 +另一个有用的配置是`arith := true`，它会简化算术表达式。因为这太常用了所以用 `simp_arith` 作为`simp (config := { arith := true })`的缩写。 ```lean example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by @@ -2004,8 +2003,8 @@ The ``split`` tactic is useful for breaking nested `if-then-else` and `match` ex For a `match` expression with `n` cases, the `split` tactic generates at most `n` subgoals. Here is an example. --> -``split``策略对于在多情形分支结构中打破嵌套的`if-then-else`和`match`表达式很有用。 -对于包含`n`种情形的`match`表达式，`split`策略最多生成`n`个子目标。例子： +``split`` 策略对于在多情形分支结构中打破嵌套的`if-then-else`和 `match` 表达式很有用。 +对于包含 `n` 种情形的 `match` 表达式，`split` 策略最多生成 `n` 个子目标。例子： ```lean def f (x y z : Nat) : Nat := @@ -2048,9 +2047,9 @@ and then for each generated goal it tries `contradiction`, and then `rfl` if `co Like `simp`, we can apply `split` to a particular hypothesis. --> -策略`split <;> first | contradiction | rfl`首先应用`split`策略，接着对每个生成出的目标尝试`contradiction`，如果失败那么最后`rfl`。 +策略`split <;> first | contradiction | rfl`首先应用 `split` 策略，接着对每个生成出的目标尝试 `contradiction`，如果失败那么最后 `rfl`。 -类似`simp`，我们对一个特定的假设也可以使用`split`。 +类似 `simp`，我们对一个特定的假设也可以使用 `split`。 ```lean def g (xs ys : List Nat) : Nat := @@ -2078,7 +2077,7 @@ be done when `triv` is used. You can provide different expansions, and the tacti interpreter will try all of them until one succeeds. --> -在下面的例子中，我们使用`syntax`命令定义符号`triv`。然后，我们使用`macro_rules`命令来指定使用`triv`时应该做什么。你可以提供不同的扩展，策略解释器将尝试所有的扩展，直到有一个成功。 +在下面的例子中，我们使用 `syntax` 命令定义符号 `triv`。然后，我们使用 `macro_rules` 命令来指定使用 `triv` 时应该做什么。你可以提供不同的扩展，策略解释器将尝试所有的扩展，直到有一个成功。 -1. 用策略式证明重做[命题与证明](./propositions_and_proofs.md)和[量词与等价](./quantifiers_and_equality.md)两章的练习。适当使用``rw``和``simp``。 +1. 用策略式证明重做[命题与证明](./propositions_and_proofs.md)和[量词与等价](./quantifiers_and_equality.md)两章的练习。适当使用 ``rw`` 和 ``simp``。 2. 用策略组合器给下面的例子用一行写一个证明： ```lean diff --git a/type_classes.md b/type_classes.md index 9ab0f6d..b7cc015 100644 --- a/type_classes.md +++ b/type_classes.md @@ -1120,7 +1120,7 @@ prove a target ``p``. By the previous observations, ``decide p`` 将根据定义化简未为布尔值 ``true``。在假设 ``decide p = true`` 成立的情况下，``of_decide_eq_true`` 会生成 ``p`` 的证明。 策略 ``decide`` 将所有这些组合在一起以证明目标 ``p``。根据前面的观察， -只要推断出的决策过程拥有足够的信息，可以根据定义将 ``c``求值为 ``isTrue`` 的情况， +只要推断出的决策过程拥有足够的信息，可以根据定义将 ``c`` 求值为 ``isTrue`` 的情况， 那么 ``decide`` 就会成功。 最基本的强制转换将一种类型的元素映射到另一种类型。 -例如，从``Nat``到``Int``的强制转换允许我们将任何元素 ``n : Nat`` 视作元素 ``Int``。 +例如，从 ``Nat`` 到 ``Int`` 的强制转换允许我们将任何元素 ``n : Nat`` 视作元素 ``Int``。 但一些强制转换依赖于参数；例如，对于任何类型 ``α``，我们可以将任何元素 ``as : List α`` 视为 ``Set α`` 的元素，即，列表中出现的元素组成的集合。 相应的强制转换被定义在 ``List α`` 的「类型族（Type Family）」上，由 ``α`` 参数化。