Deploying to gh-pages from @ e872f0f 🚀

introduction.html

@@ -184,11 +184,13 @@ <h2 id="计算机和定理证明"><a class="header" href="#计算机和定理证
 mathematical bounds, or finding mathematical objects. A calculation can be viewed as a proof as well, and these systems,
 too, help establish mathematical claims.
 -->
-<p><strong>自动定理证明（Automated theorem proving）</strong> 着眼于「寻找」证明。归结（Resolution）定理证明器、
-<strong>表格法（tableau）</strong> 定理证明器、 <strong>快速可满足性求解器（Fast satisfiability solvers）</strong>
+<p><strong>自动定理证明（Automated theorem proving）</strong> 着眼于「寻找」证明。
+<strong>归结原理（Resolution）</strong> 定理证明器、<strong>表格法（tableau）</strong> 定理证明器、
+<strong>快速可满足性求解器（Fast satisfiability solvers）</strong>
 等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法；
 还有些系统为特定的语言和问题提供搜索和决策程序，
-例如整数或实数上的线性或非线性表达式；像 <strong>SMT（Satisfiability modulo theories）</strong>
+例如整数或实数上的线性或非线性表达式；
+像 <strong>SMT（Satisfiability modulo theories，可满足性模理论）</strong>
 这样的架构将通用的搜索方法与特定领域的程序相结合；
 计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段，
 这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。</p>
@@ -203,7 +205,7 @@ <h2 id="计算机和定理证明"><a class="header" href="#计算机和定理证
 allows you to obtain deeper and more complex proofs.
 -->
 <p>自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有 bug，
-而且很难保证它们所提供的结果是正确的。相比之下， <strong>交互式定理证明器（Interactive theorem proving）</strong>
+而且很难保证它们所提供的结果是正确的。相比之下，<strong>交互式定理证明器（Interactive theorem proving）</strong>
 侧重于「验证」证明，要求每个命题都有合适的公理基础的证明来支持。
 这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明，
 一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的「证明对象」，
@@ -228,7 +230,7 @@ <h2 id="计算机和定理证明"><a class="header" href="#计算机和定理证
 -->
 <p>Lean 的底层逻辑有一个计算的解释，与此同时 Lean 可以被视为一种编程语言。
 更重要的是，它可以被看作是一个编写具有精确语义的程序的系统，
-以及对程序所表示的计算功能进行推理。Lean 中也有机制使它能够作为它自己的 <strong>元编程语言</strong> ，
+以及对程序所表示的计算功能进行推理。Lean 中也有机制使它能够作为它自己的 <strong>元编程语言</strong>，
 这意味着你可以使用 Lean 本身实现自动化和扩展 Lean 的功能。
 Lean 的这些方面将在本教程的配套教程
 <a href="https://www.leanprover.cn/fp-lean-zh/">Lean 4函数式编程</a>中进行探讨，本书只介绍计算方面。</p>
@@ -281,7 +283,7 @@ <h2 id="关于本书"><a class="header" href="#关于本书">关于本书</a></h
 -->
 <p>由于完全深入细节的公理证明十分复杂，定理证明的难点在于让计算机尽可能多地填补证明细节。
 你将通过<a href="dependent_type_theory.html">依值类型论</a>语言来学习各种方法实现自动证明，例如项重写，
-以及 Lean 中的项和表达式的自动简化方法。同样， <strong>繁饰（Elaboration）</strong>
+以及 Lean 中的项和表达式的自动简化方法。同样，<strong>繁饰（Elaboration）</strong>
 和 <strong>类型推断（Type inference）</strong> 的方法，可以用来支持灵活的代数推理。</p>
 <!--
 Finally, you will learn about features that are specific to Lean, including the language you use to communicate

print.html

@@ -198,11 +198,13 @@ <h2 id="计算机和定理证明"><a class="header" href="#计算机和定理证
 mathematical bounds, or finding mathematical objects. A calculation can be viewed as a proof as well, and these systems,
 too, help establish mathematical claims.
 -->
-<p><strong>自动定理证明（Automated theorem proving）</strong> 着眼于「寻找」证明。归结（Resolution）定理证明器、
-<strong>表格法（tableau）</strong> 定理证明器、 <strong>快速可满足性求解器（Fast satisfiability solvers）</strong>
+<p><strong>自动定理证明（Automated theorem proving）</strong> 着眼于「寻找」证明。
+<strong>归结原理（Resolution）</strong> 定理证明器、<strong>表格法（tableau）</strong> 定理证明器、
+<strong>快速可满足性求解器（Fast satisfiability solvers）</strong>
 等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法；
 还有些系统为特定的语言和问题提供搜索和决策程序，
-例如整数或实数上的线性或非线性表达式；像 <strong>SMT（Satisfiability modulo theories）</strong>
+例如整数或实数上的线性或非线性表达式；
+像 <strong>SMT（Satisfiability modulo theories，可满足性模理论）</strong>
 这样的架构将通用的搜索方法与特定领域的程序相结合；
 计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段，
 这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。</p>
@@ -217,7 +219,7 @@ <h2 id="计算机和定理证明"><a class="header" href="#计算机和定理证
 allows you to obtain deeper and more complex proofs.
 -->
 <p>自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有 bug，
-而且很难保证它们所提供的结果是正确的。相比之下， <strong>交互式定理证明器（Interactive theorem proving）</strong>
+而且很难保证它们所提供的结果是正确的。相比之下，<strong>交互式定理证明器（Interactive theorem proving）</strong>
 侧重于「验证」证明，要求每个命题都有合适的公理基础的证明来支持。
 这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明，
 一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的「证明对象」，
@@ -242,7 +244,7 @@ <h2 id="计算机和定理证明"><a class="header" href="#计算机和定理证
 -->
 <p>Lean 的底层逻辑有一个计算的解释，与此同时 Lean 可以被视为一种编程语言。
 更重要的是，它可以被看作是一个编写具有精确语义的程序的系统，
-以及对程序所表示的计算功能进行推理。Lean 中也有机制使它能够作为它自己的 <strong>元编程语言</strong> ，
+以及对程序所表示的计算功能进行推理。Lean 中也有机制使它能够作为它自己的 <strong>元编程语言</strong>，
 这意味着你可以使用 Lean 本身实现自动化和扩展 Lean 的功能。
 Lean 的这些方面将在本教程的配套教程
 <a href="https://www.leanprover.cn/fp-lean-zh/">Lean 4函数式编程</a>中进行探讨，本书只介绍计算方面。</p>
@@ -295,7 +297,7 @@ <h2 id="关于本书"><a class="header" href="#关于本书">关于本书</a></h
 -->
 <p>由于完全深入细节的公理证明十分复杂，定理证明的难点在于让计算机尽可能多地填补证明细节。
 你将通过<a href="dependent_type_theory.html">依值类型论</a>语言来学习各种方法实现自动证明，例如项重写，
-以及 Lean 中的项和表达式的自动简化方法。同样， <strong>繁饰（Elaboration）</strong>
+以及 Lean 中的项和表达式的自动简化方法。同样，<strong>繁饰（Elaboration）</strong>
 和 <strong>类型推断（Type inference）</strong> 的方法，可以用来支持灵活的代数推理。</p>
 <!--
 Finally, you will learn about features that are specific to Lean, including the language you use to communicate
@@ -10688,7 +10690,7 @@ <h1 id="类型类"><a class="header" href="#类型类">类型类</a></h1>
 `structure` to `class` in the example above, the type of `Add.add` becomes:
 -->
 <p>类型类的主要思想是使诸如 <code>Add a</code> 之类的参数变为隐含的，
-并使用用户定义实例的数据库通过称为类型类求解的过程自动合成所需的实例。
+并使用用户定义实例的数据库通过称为类型类解析的过程自动合成所需的实例。
 在 Lean 中，通过在以上示例中将 <code>structure</code> 更改为 <code>class</code>，<code>Add.add</code> 的类型会变为：</p>
 <pre><code class="language-lean"><span class="boring">namespace Ex
 </span>class Add (a : Type) where
@@ -10705,7 +10707,7 @@ <h1 id="类型类"><a class="header" href="#类型类">类型类</a></h1>
 Similarly, we can register instances by:
 -->
 <p>其中方括号表示类型为 <code>Add a</code> 的参数是  <strong>实例隐式的</strong> ，
-即，它应该使用类型类求解合成。这个版本的 <code>add</code> 是 Haskell 项
+即，它应该使用类型类解析合成。这个版本的 <code>add</code> 是 Haskell 项
 <code>add :: Add a =&gt; a -&gt; a -&gt; a</code> 的 Lean 类比。
 同样，我们可以通过以下方式注册实例：</p>
 <pre><code class="language-lean"><span class="boring">namespace Ex
@@ -10726,8 +10728,8 @@ <h1 id="类型类"><a class="header" href="#类型类">类型类</a></h1>
 the goal of `Add Nat`, and typeclass resolution will synthesize the instance for `Nat` above.
 We can now reimplement `double` using an instance implicit by:
 -->
-<p>接着对于 <code>n : Nat</code> 和 <code>m : Nat</code>，项 <code>Add.add n m</code> 触发了类型类求解，
-目标为 <code>Add Nat</code>，且类型类求解将综合上面 <code>Nat</code> 的实例。
+<p>接着对于 <code>n : Nat</code> 和 <code>m : Nat</code>，项 <code>Add.add n m</code> 触发了类型类解析，
+目标为 <code>Add Nat</code>，且类型类解析将综合上面 <code>Nat</code> 的实例。
 现在，我们可以通过隐式的实例重新实现 <code>double</code> 了：</p>
 <pre><code class="language-lean"><span class="boring">namespace Ex
 </span><span class="boring">class Add (a : Type) where
@@ -10924,7 +10926,7 @@ <h2 id="链接实例"><a class="header" href="#链接实例">链接实例</a></h
 and is useful for triggering the type class resolution procedure when the expected type is an instance.
 -->
 <p>Lean 标准库包含了定义 <code>inferInstance</code>，它的类型为 <code>{α : Sort u} → [i : α] → α</code>，
-它在期望的类型是一个实例时触发类型类求解过程十分有用。</p>
+它在期望的类型是一个实例时触发类型类解析过程十分有用。</p>
 <pre><code class="language-lean">#check (inferInstance : Inhabited Nat) -- Inhabited Nat
 
 def foo : Inhabited (Nat × Nat) :=
@@ -11621,7 +11623,7 @@ <h2 id="类型类推断的管理"><a class="header" href="#类型类推断的管
 <p>如果你使用的是 VS Code，可以通过将鼠标悬停在相关的定理或定义上，
 或按 <code>Ctrl-Shift-Enter</code> 打开消息窗口来阅读结果。在 Emacs 中，
 你可以使用 <code>C-c C-x</code> 在你的文件中运行一个独立的 Lean 进程，
-并且在每次触发类型类求解过程时，输出缓冲区都会显示一个跟踪。</p>
+并且在每次触发类型类解析过程时，输出缓冲区都会显示一个跟踪。</p>
 <!--
 You can also limit the search using the following options:
 -->
@@ -11636,7 +11638,7 @@ <h2 id="类型类推断的管理"><a class="header" href="#类型类推断的管
 Option `synthInstance.maxSize` is the maximum number of instances used
 to construct a solution in the type class instance synthesis procedure.
 -->
-<p>选项 <code>synthInstance.maxHeartbeats</code> 指定每个类型类求解问题可能出现的心跳（Heartbeat）次数上限。
+<p>选项 <code>synthInstance.maxHeartbeats</code> 指定每个类型类解析问题可能出现的心跳（Heartbeat）次数上限。
 心跳是（小）内存分配的次数（以千为单位），0 表示没有上限。
 选项 <code>synthInstance.maxSize</code> 是用于构建类型类实例合成过程中解的实例个数。</p>
 <!--
@@ -11727,7 +11729,7 @@ <h2 id="使用类型泛型进行强制转换"><a class="header" href="#使用类
 <!--
 In Lean, coercions are implemented on top of the type class resolution framework. We define a coercion from ``α`` to ``β`` by declaring an instance of ``Coe α β``. For example, we can define a coercion from ``Bool`` to ``Prop`` as follows:
 -->
-<p>在 Lean 中，强制转换在类型类求解框架的基础上实现。我们通过声明 <code>Coe α β</code> 的实例，
+<p>在 Lean 中，强制转换在类型类解析框架的基础上实现。我们通过声明 <code>Coe α β</code> 的实例，
 定义从 <code>α</code> 到 <code>β</code> 的强制转换。例如，以下内容可以定义从 <code>Bool</code> 到 <code>Prop</code> 的强制转换：</p>
 <pre><code class="language-lean">instance : Coe Bool Prop where
   coe b := b = true
@@ -11765,7 +11767,7 @@ <h2 id="使用类型泛型进行强制转换"><a class="header" href="#使用类
 We can use the notation ``↑`` to force a coercion to be introduced in a particular place. It is also helpful to make our intent clear, and work around limitations of the coercion resolution system.
 -->
 <p>我们可以使用符号 <code>↑</code> 在特定位置强制引入强制转换。
-这也有助于明确我们的意图，并解决强制转换求解系统中的限制。</p>
+这也有助于明确我们的意图，并解决强制转换解析系统中的限制。</p>
 <pre><code class="language-lean"><span class="boring">def Set (α : Type u) := α → Prop
 </span><span class="boring">def Set.empty {α : Type u} : Set α := fun _ =&gt; False
 </span><span class="boring">def Set.mem (a : α) (s : Set α) : Prop := s a

type_classes.html

@@ -208,7 +208,7 @@ <h1 id="类型类"><a class="header" href="#类型类">类型类</a></h1>
 `structure` to `class` in the example above, the type of `Add.add` becomes:
 -->
 <p>类型类的主要思想是使诸如 <code>Add a</code> 之类的参数变为隐含的，
-并使用用户定义实例的数据库通过称为类型类求解的过程自动合成所需的实例。
+并使用用户定义实例的数据库通过称为类型类解析的过程自动合成所需的实例。
 在 Lean 中，通过在以上示例中将 <code>structure</code> 更改为 <code>class</code>，<code>Add.add</code> 的类型会变为：</p>
 <pre><code class="language-lean"><span class="boring">namespace Ex
 </span>class Add (a : Type) where
@@ -225,7 +225,7 @@ <h1 id="类型类"><a class="header" href="#类型类">类型类</a></h1>
 Similarly, we can register instances by:
 -->
 <p>其中方括号表示类型为 <code>Add a</code> 的参数是  <strong>实例隐式的</strong> ，
-即，它应该使用类型类求解合成。这个版本的 <code>add</code> 是 Haskell 项
+即，它应该使用类型类解析合成。这个版本的 <code>add</code> 是 Haskell 项
 <code>add :: Add a =&gt; a -&gt; a -&gt; a</code> 的 Lean 类比。
 同样，我们可以通过以下方式注册实例：</p>
 <pre><code class="language-lean"><span class="boring">namespace Ex
@@ -246,8 +246,8 @@ <h1 id="类型类"><a class="header" href="#类型类">类型类</a></h1>
 the goal of `Add Nat`, and typeclass resolution will synthesize the instance for `Nat` above.
 We can now reimplement `double` using an instance implicit by:
 -->
-<p>接着对于 <code>n : Nat</code> 和 <code>m : Nat</code>，项 <code>Add.add n m</code> 触发了类型类求解，
-目标为 <code>Add Nat</code>，且类型类求解将综合上面 <code>Nat</code> 的实例。
+<p>接着对于 <code>n : Nat</code> 和 <code>m : Nat</code>，项 <code>Add.add n m</code> 触发了类型类解析，
+目标为 <code>Add Nat</code>，且类型类解析将综合上面 <code>Nat</code> 的实例。
 现在，我们可以通过隐式的实例重新实现 <code>double</code> 了：</p>
 <pre><code class="language-lean"><span class="boring">namespace Ex
 </span><span class="boring">class Add (a : Type) where
@@ -444,7 +444,7 @@ <h2 id="链接实例"><a class="header" href="#链接实例">链接实例</a></h
 and is useful for triggering the type class resolution procedure when the expected type is an instance.
 -->
 <p>Lean 标准库包含了定义 <code>inferInstance</code>，它的类型为 <code>{α : Sort u} → [i : α] → α</code>，
-它在期望的类型是一个实例时触发类型类求解过程十分有用。</p>
+它在期望的类型是一个实例时触发类型类解析过程十分有用。</p>
 <pre><code class="language-lean">#check (inferInstance : Inhabited Nat) -- Inhabited Nat
 
 def foo : Inhabited (Nat × Nat) :=
@@ -1141,7 +1141,7 @@ <h2 id="类型类推断的管理"><a class="header" href="#类型类推断的管
 <p>如果你使用的是 VS Code，可以通过将鼠标悬停在相关的定理或定义上，
 或按 <code>Ctrl-Shift-Enter</code> 打开消息窗口来阅读结果。在 Emacs 中，
 你可以使用 <code>C-c C-x</code> 在你的文件中运行一个独立的 Lean 进程，
-并且在每次触发类型类求解过程时，输出缓冲区都会显示一个跟踪。</p>
+并且在每次触发类型类解析过程时，输出缓冲区都会显示一个跟踪。</p>
 <!--
 You can also limit the search using the following options:
 -->
@@ -1156,7 +1156,7 @@ <h2 id="类型类推断的管理"><a class="header" href="#类型类推断的管
 Option `synthInstance.maxSize` is the maximum number of instances used
 to construct a solution in the type class instance synthesis procedure.
 -->
-<p>选项 <code>synthInstance.maxHeartbeats</code> 指定每个类型类求解问题可能出现的心跳（Heartbeat）次数上限。
+<p>选项 <code>synthInstance.maxHeartbeats</code> 指定每个类型类解析问题可能出现的心跳（Heartbeat）次数上限。
 心跳是（小）内存分配的次数（以千为单位），0 表示没有上限。
 选项 <code>synthInstance.maxSize</code> 是用于构建类型类实例合成过程中解的实例个数。</p>
 <!--
@@ -1247,7 +1247,7 @@ <h2 id="使用类型泛型进行强制转换"><a class="header" href="#使用类
 <!--
 In Lean, coercions are implemented on top of the type class resolution framework. We define a coercion from ``α`` to ``β`` by declaring an instance of ``Coe α β``. For example, we can define a coercion from ``Bool`` to ``Prop`` as follows:
 -->
-<p>在 Lean 中，强制转换在类型类求解框架的基础上实现。我们通过声明 <code>Coe α β</code> 的实例，
+<p>在 Lean 中，强制转换在类型类解析框架的基础上实现。我们通过声明 <code>Coe α β</code> 的实例，
 定义从 <code>α</code> 到 <code>β</code> 的强制转换。例如，以下内容可以定义从 <code>Bool</code> 到 <code>Prop</code> 的强制转换：</p>
 <pre><code class="language-lean">instance : Coe Bool Prop where
   coe b := b = true
@@ -1285,7 +1285,7 @@ <h2 id="使用类型泛型进行强制转换"><a class="header" href="#使用类
 We can use the notation ``↑`` to force a coercion to be introduced in a particular place. It is also helpful to make our intent clear, and work around limitations of the coercion resolution system.
 -->
 <p>我们可以使用符号 <code>↑</code> 在特定位置强制引入强制转换。
-这也有助于明确我们的意图，并解决强制转换求解系统中的限制。</p>
+这也有助于明确我们的意图，并解决强制转换解析系统中的限制。</p>
 <pre><code class="language-lean"><span class="boring">def Set (α : Type u) := α → Prop
 </span><span class="boring">def Set.empty {α : Type u} : Set α := fun _ =&gt; False
 </span><span class="boring">def Set.mem (a : α) (s : Set α) : Prop := s a