format spaces

Lean-zh · Jun 22, 2024 · bec69ac · bec69ac
1 parent bd5fda9
commit bec69ac
Show file tree

Hide file tree

Showing 10 changed files with 300 additions and 250 deletions.
diff --git a/axioms_and_computation.md b/axioms_and_computation.md
@@ -247,7 +247,7 @@ the theory.
 -->
 
 在通过了证明无关的 ``Prop`` 之后，可以认为使用排中律 ``p ∨ ¬p`` 是合法的，
-其中 ``p``是任何命题。当然，这也可能根据 CIC 的规则阻止计算，
+其中 ``p`` 是任何命题。当然，这也可能根据 CIC 的规则阻止计算，
 但它不会阻止字节码求值，如上所述。仅在 :numref:`choice`
 中讨论过的选择原则才能完全消除理论中与证明无关的部分和与数据相关部分之间的区别。
 
@@ -678,7 +678,7 @@ They are, like inductively defined types and the associated
 constructors and recursors, viewed as part of the logical framework.
 -->
 
-和归纳定义的类型以及相关的构造器和递归器一样，它们也被视为逻辑框架的一部分。
+和归纳定义的类型以及相关的构造子和递归器一样，它们也被视为逻辑框架的一部分。
 
 <!--
 What makes the ``Quot`` construction into a bona fide quotient is the
@@ -818,7 +818,7 @@ the quotient correspond exactly to the equivalence classes of elements
 in ``α``.
 -->
 
-结合``Quotient.sound``，这意味着商的各个元素精确对应于 ``α``中各元素的等价类。
+结合 ``Quotient.sound``，这意味着商的各个元素精确对应于 ``α`` 中各元素的等价类。
 
 <!--
 Recall that in the standard library, ``α × β`` represents the
@@ -1304,7 +1304,7 @@ sketch the proof that is found in the standard library.
 First, we import the necessary axioms, and define two predicates ``U`` and ``V``:
 -->
 
-首先，我们导入必要的公理，并定义两个谓词``U``和``V``：
+首先，我们导入必要的公理，并定义两个谓词 ``U`` 和 ``V``：
 
 ```lean
 # namespace Hidden

diff --git a/dependent_type_theory.md b/dependent_type_theory.md
diff --git a/induction_and_recursion.md b/induction_and_recursion.md
diff --git a/inductive_types.md b/inductive_types.md
diff --git a/interacting_with_lean.md b/interacting_with_lean.md
diff --git a/introduction.md b/introduction.md
@@ -23,7 +23,11 @@ lengthy computation, in which case verifying the truth of the theorem requires v
 it is supposed to do.
 -->
 
-**形式验证**（Formal verification）是指使用逻辑和计算方法来验证用精确的数学术语表达的命题。这包括普通的数学定理，以及硬件或软件、网络协议、机械和混合系统中的形式命题。在实践中，验证数学命题和验证系统的正确性之间很类似：形式验证用数学术语描述硬件和软件系统，在此基础上验证其命题的正确性，这就像定理证明的过程。相反，一个数学定理的证明可能需要冗长的计算，在这种情况下，验证定理的真实性需要验证计算过程是否出错。
+**形式验证（Formal Verification）**是指使用逻辑和计算方法来验证用精确的数学术语表达的命题。
+这包括普通的数学定理，以及硬件或软件、网络协议、机械和混合系统中的形式命题。
+在实践中，验证数学命题和验证系统的正确性之间很类似：形式验证用数学术语描述硬件和软件系统，
+在此基础上验证其命题的正确性，这就像定理证明的过程。相反，一个数学定理的证明可能需要冗长的计算，
+在这种情况下，验证定理的真实性需要验证计算过程是否出错。
 
 <!--
 The gold standard for supporting a mathematical claim is to provide a proof, and twentieth-century developments in logic
@@ -32,7 +36,9 @@ foundational systems. With this reduction, there are two ways that a computer ca
 find a proof in the first place, and it can help verify that a purported proof is correct.
 -->
 
-二十世纪的逻辑学发展表明，绝大多数传统证明方法可以化为若干基础系统中的一小套公理和规则。有了这种简化，计算机能以两种方式帮助建立命题：1）它可以帮助寻找一个证明，2）可以帮助验证一个所谓的证明是正确的。
+二十世纪的逻辑学发展表明，绝大多数传统证明方法可以化为若干基础系统中的一小套公理和规则。
+有了这种简化，计算机能以两种方式帮助建立命题：1）它可以帮助寻找一个证明，
+2）可以帮助验证一个所谓的证明是正确的。
 
 <!--
 *Automated theorem proving* focuses on the "finding" aspect. Resolution theorem provers, tableau theorem provers, fast
@@ -45,7 +51,14 @@ mathematical bounds, or finding mathematical objects. A calculation can be viewe
 too, help establish mathematical claims.
 -->
 
-**自动定理证明**（Automated theorem proving）着眼于「寻找」证明。归结（Resolution）定理证明器、表格法（tableau）定理证明器、快速可满足性求解器（Fast satisfiability solvers）等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法；还有些系统为特定的语言和问题提供搜索和决策程序，例如整数或实数上的线性或非线性表达式；像SMT（Satisfiability modulo theories）这样的架构将通用的搜索方法与特定领域的程序相结合；计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段，这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。
+**自动定理证明（Automated theorem proving）**着眼于「寻找」证明。归结（Resolution）定理证明器、
+**表格法（tableau）**定理证明器、**快速可满足性求解器（Fast satisfiability solvers）**
+等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法；
+还有些系统为特定的语言和问题提供搜索和决策程序，
+例如整数或实数上的线性或非线性表达式；像**SMT（Satisfiability modulo theories）**
+这样的架构将通用的搜索方法与特定领域的程序相结合；
+计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段，
+这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。
 
 <!--
 Automated reasoning systems strive for power and efficiency, often at the expense of guaranteed soundness. Such systems
@@ -58,7 +71,13 @@ checked independently. Constructing such proofs typically requires much more inp
 allows you to obtain deeper and more complex proofs.
 -->
 
-自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有bug，而且很难保证它们所提供的结果是正确的。相比之下，**交互式定理证明器**（Interactive theorem proving）侧重于「验证」证明，要求每个命题都有合适的公理基础的证明来支持。这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明，一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的「证明对象」，可以传给其他系统并独立检查。构建这样的证明通常需要用户更多的输入和交互，但它可以让你获得更深入、更复杂的证明。
+自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有 bug，
+而且很难保证它们所提供的结果是正确的。相比之下，**交互式定理证明器（Interactive theorem proving）**
+侧重于「验证」证明，要求每个命题都有合适的公理基础的证明来支持。
+这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明，
+一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的「证明对象」，
+可以传给其他系统并独立检查。构建这样的证明通常需要用户更多的输入和交互，
+但它可以让你获得更深入、更复杂的证明。
 
 <!--
 The *Lean Theorem Prover* aims to bridge the gap between interactive and automated theorem proving, by situating
@@ -67,7 +86,9 @@ axiomatic proofs. The goal is to support both mathematical reasoning and reasoni
 claims in both domains.
 -->
 
-**Lean 定理证明器**旨在融合交互式和自动定理证明，它将自动化工具和方法置于一个支持用户交互和构建完整公理化证明的框架中。它的目标是支持数学推理和复杂系统的推理，并验证这两个领域的命题。
+**Lean 定理证明器**旨在融合交互式和自动定理证明，
+它将自动化工具和方法置于一个支持用户交互和构建完整公理化证明的框架中。
+它的目标是支持数学推理和复杂系统的推理，并验证这两个领域的命题。
 
 <!--
 Lean's underlying logic has a computational interpretation, and Lean can be viewed equally well as a programming
@@ -78,7 +99,12 @@ 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/)中进行探讨，本书只介绍计算方面。
 
 <!--
 About Lean
@@ -94,7 +120,9 @@ effort, and much of the potential for automation will be realized only gradually
 mathematical libraries freely.
 -->
 
-*Lean* 项目由微软 Redmond 研究院的Leonardo de Moura在2013年发起，这是个长期项目，自动化方法的潜力会在未来逐步被挖掘。Lean是在[Apache 2.0 license](LICENSE)下发布的，这是一个允许他人自由使用和扩展代码和数学库的许可性开源许可证。
+*Lean* 项目由微软 Redmond 研究院的 Leonardo de Moura 在 2013 年发起，这是个长期项目，
+自动化方法的潜力会在未来逐步被挖掘。Lean 是在 [Apache 2.0 许可协议](LICENSE) 下发布的，
+这是一个允许他人自由使用和扩展代码和数学库的许可性开源许可证。
 
 
 <!--
@@ -105,9 +133,13 @@ To install Lean in your computer consider using the [Quickstart](https://github.
 This tutorial describes the current version of Lean, known as Lean 4.
 -->
 
-通常有两种办法来运行Lean。第一个是[网页版本](https://live.lean-lang.org/)：由 Javascript 编写，包含标准定义和定理库，编辑器会下载到你的浏览器上运行。这是个方便快捷的办法。
+通常有两种办法来运行Lean。第一个是[网页版本](https://live.lean-lang.org/)：
+由 JavaScript 编写，包含标准定义和定理库，编辑器会下载到你的浏览器上运行。
+这是个方便快捷的办法。
 
-第二种是本地版本：本地版本远快于网页版本，并且非常灵活。Visual Studio Code和 Emacs 扩展模块给编写和调试证明提供了有力支撑，因此更适合正式使用。源代码和安装方法见[https://github.com/leanprover/lean4/](https://github.com/leanprover/lean4/).
+第二种是本地版本：本地版本远快于网页版本，并且非常灵活。Visual Studio Code
+和 Emacs 扩展模块给编写和调试证明提供了有力支撑，因此更适合正式使用。
+源代码和安装方法见[https://github.com/leanprover/lean4/](https://github.com/leanprover/lean4/).
 
 本教程介绍的是 Lean 的当前版本：Lean 4。
 
@@ -128,7 +160,7 @@ mathematical assertions in dependent type theory, but it also can be used as a l
 -->
 
 
-本书的目的是教你在 Lean 中编写和验证证明，并且不太需要针对 Lean 的基础知识。首先，你将学习 Lean 所基于的逻辑系统，它是**依值类型论**（Dependent type theory）的一个版本，足以证明几乎所有传统的数学定理，并且有足够的表达能力自然地表示数学定理。更具体地说，Lean是基于具有归纳类型（Inductive type）的构造演算（Calculus of Construction）系统的类型论版本。Lean不仅可以定义数学对象和表达依值类型论的数学断言，而且还可以作为一种语言来编写证明。
+本书的目的是教你在 Lean 中编写和验证证明，并且不太需要针对 Lean 的基础知识。首先，你将学习 Lean 所基于的逻辑系统，它是**依值类型论（Dependent type theory）**的一个版本，足以证明几乎所有传统的数学定理，并且有足够的表达能力自然地表示数学定理。更具体地说，Lean 是基于具有归纳类型（Inductive type）的构造演算（Calculus of Construction）系统的类型论版本。Lean 不仅可以定义数学对象和表达依值类型论的数学断言，而且还可以作为一种语言来编写证明。
 
 <!--
 Because fully detailed axiomatic proofs are so complicated, the challenge of theorem proving is to have the computer
@@ -138,7 +170,10 @@ expressions automatically. Similarly, methods of *elaboration* and *type inferen
 flexible forms of algebraic reasoning.
 -->
 
-由于完全深入细节的公理证明十分复杂，定理证明的难点在于让计算机尽可能多地填补证明细节。你将通过[依值类型论](dependent_type_theory.md)语言来学习各种方法实现自动证明，例如项重写，以及 Lean 中的项和表达式的自动简化方法。同样，**繁饰**（Elaboration）和**类型推断**（Type inference）的方法，可以用来支持灵活的代数推理。
+由于完全深入细节的公理证明十分复杂，定理证明的难点在于让计算机尽可能多地填补证明细节。
+你将通过[依值类型论](dependent_type_theory.md)语言来学习各种方法实现自动证明，例如项重写，
+以及 Lean 中的项和表达式的自动简化方法。同样，**繁饰（Elaboration）**
+和**类型推断（Type inference）**的方法，可以用来支持灵活的代数推理。
 
 
 <!--
@@ -165,17 +200,31 @@ If you are reading the book inside of [VS Code](https://code.visualstudio.com/),
 things into the editor and modify the examples, and Lean will check the results and provide feedback continuously as you
 type. We recommend running the examples and experimenting with the code on your own as you work through the chapters
 that follow. You can open this book on VS Code by using the command "Lean 4: Open Documentation View".
-
 -->
 
-如果你在[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 中打开本书。
 
 致谢
 ---------------
 
+<!--
 This tutorial is an open access project maintained on Github. Many people have contributed to the effort, providing
 corrections, suggestions, examples, and text. We are grateful to Ulrik Buchholz, Kevin Buzzard, Mario Carneiro, Nathan
 Carter, Eduardo Cavazos, Amine Chaieb, Joe Corneli, William DeMeo, Marcus Klaas de Vries, Ben Dyer, Gabriel Ebner,
 Anthony Hart, Simon Hudon, Sean Leather, Assia Mahboubi, Gihan Marasingha, Patrick Massot, Christopher John Mazey,
 Sebastian Ullrich, Floris van Doorn, Daniel Velleman, Théo Zimmerman, Paul Chisholm, Chris Lovett, and Siddhartha Gadgil for their contributions.  Please see [lean prover](https://github.com/leanprover/) and [lean community](https://github.com/leanprover-community/) for an up to date list
 of our amazing contributors.
+-->
+
+本教程是一项开放源代码项目，在 Github 上维护。许多人为此做出了贡献，提供了
+更正、建议、示例和文本。我们要感谢 Ulrik Buchholz、Kevin Buzzard、Mario Carneiro、
+Nathan Carter、Eduardo Cavazos、Amine Chaieb、Joe Corneli、William DeMeo、
+Marcus Klaas de Vries、Ben Dyer、Gabriel Ebner、Anthony Hart、Simon Hudon、Sean Leather、
+Assia Mahboubi、Gihan Marasingha、Patrick Massot、Christopher John Mazey、
+Sebastian Ullrich、Floris van Doorn、Daniel Velleman、Théo Zimmerman、Paul Chisholm、Chris Lovett
+以及 Siddhartha Gadgil 对本文做出的贡献。有关我们杰出的贡献者的最新名单，
+请参见 [Lean 证明器](https://github.com/leanprover/)和 [Lean 社区](https://github.com/leanprover-community/)。