From 83dede9428cdc959d9bf7fd2e075174ab4f27eca Mon Sep 17 00:00:00 2001 From: Oling Cat Date: Wed, 26 Jun 2024 02:27:19 +0800 Subject: [PATCH 1/3] tail-recursion: done --- functional-programming-lean/src/SUMMARY.md | 2 +- functional-programming-lean/src/next-steps.md | 35 +-- .../src/programs-proofs.md | 35 ++- .../src/programs-proofs/tail-recursion.md | 220 +++++++++++++++++- .../src/tactics-induction-proofs.md | 4 +- 5 files changed, 278 insertions(+), 18 deletions(-) diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md index 4b86132..1796191 100644 --- a/functional-programming-lean/src/SUMMARY.md +++ b/functional-programming-lean/src/SUMMARY.md @@ -70,4 +70,4 @@ - [特殊类型](programs-proofs/special-types.md) - [总结](programs-proofs/summary.md) -[接下来做什么](next-steps.md) +[下一步](next-steps.md) diff --git a/functional-programming-lean/src/next-steps.md b/functional-programming-lean/src/next-steps.md index 90ba1ed..775f29d 100644 --- a/functional-programming-lean/src/next-steps.md +++ b/functional-programming-lean/src/next-steps.md @@ -1,10 +1,13 @@ # 下一步 + -本书介绍了 Lean 中函数式编程的基本知识，包括一些互动定理证明的内容。使用依赖类型的函数式语言（如 Lean）是一个深奥的主题，内容丰富。根据您的兴趣，以下资源可能对学习 Lean 4 有用。 + +本书介绍了 Lean 中函数式编程的基本知识，包括一些互动定理证明的内容。使用依值类型的函数式语言（如 Lean）是一个深奥的主题，内容丰富。根据您的兴趣，以下资源可能对学习 Lean 4 有用。 ### 学习 Lean + + Lean 4 本身在以下资源中有详细描述： [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/) 是一本关于使用 Lean 编写证明的教程。 @@ -26,13 +30,15 @@ Lean 4 本身在以下资源中有详细描述： 然而，继续学习 Lean 的最佳方式是开始阅读和编写代码，在遇到困难时查阅文档。此外，[Lean Zulip](https://leanprover.zulipchat.com/) 是结识其他 Lean 用户、寻求帮助和帮助他人的好地方。 ### 标准库 + + Lean 自带的库相对较小。Lean 是自托管的，所包含的代码仅够实现 Lean 本身。对于许多应用来说，需要更大的标准库。 [std4](https://github.com/leanprover/std4) 是一个正在开发中的标准库，包含许多数据结构、策略、类型类实例和函数，这些都超出了 Lean 编译器本身的范围。要使用 std4，第一步是找到与您使用的 Lean 4 版本兼容的提交记录（即其中的 lean-toolchain 文件与您的项目匹配）。然后，将以下内容添加到您的 lakefile.lean 顶层，其中 COMMIT_HASH 是适当的版本： @@ -41,34 +47,37 @@ Lean 自带的库相对较小。Lean 是自托管的，所包含的代码仅够 require std from git "https://github.com/leanprover/std4/" @ "COMMIT_HASH" ``` + ### Lean 中的数学 + + 大多数数学资源是为 Lean 3 编写的。在[社区](https://leanprover-community.github.io/learn.html)网站上可以找到许多这样的资源。要开始在 Lean 4 中进行数学研究，最简单的方法可能是参与将数学库 mathlib 从 Lean 3 迁移到 Lean 4 的过程。有关更多信息，请参阅 [mathlib4 的 README](https://github.com/leanprover-community/mathlib4). -### 在计算机科学中使用依赖类型 +### 在计算机科学中使用依值类型 + + Coq 是一种与 Lean 有许多共同点的语言。对于计算机科学家来说，[Software Foundations](https://softwarefoundations.cis.upenn.edu/)系列教材提供了一个很好的介绍，介绍了 Coq 在计算机科学中的应用。Lean 和 Coq 的基本思想非常相似，编程技巧在两个语言之间是可以相互转移的。 -### 使用依赖类型编程 +### 使用依值类型编程 + -对于有兴趣学习使用索引族和依赖类型来构建程序的程序员来说，Edwin Brady 的[Type Driven Development with Idris](https://www.manning.com/books/type-driven-development-with-idris)提供了一个很好的介绍。像 Coq 一样，Idris 是 Lean 的近亲语言，但是它缺乏策略。 -### 理解依赖类型 +对于有兴趣学习使用索引族和依值类型来构建程序的程序员来说，Edwin Brady 的[Type Driven Development with Idris](https://www.manning.com/books/type-driven-development-with-idris)提供了一个很好的介绍。像 Coq 一样，Idris 是 Lean 的近亲语言，但是它缺乏策略。 + +### 理解依值类型 + -[The Little Typer](https://thelittletyper.com/)是一本为没有正式学习过逻辑或编程语言理论，但希望理解依赖类型理论核心思想的程序员准备的书。虽然上述所有资源都旨在实现尽可能的实用，但这本书通过从头开始构建基础，使用仅来自编程的概念来呈现依赖类型理论的方法。 - -免责声明：《Functional Programming in Lean》的作者也是《The Little Typer》的作者之一。 - - - - +[The Little Typer](https://thelittletyper.com/)是一本为没有正式学习过逻辑或编程语言理论，但希望理解依值类型理论核心思想的程序员准备的书。虽然上述所有资源都旨在实现尽可能的实用，但这本书通过从头开始构建基础，使用仅来自编程的概念来呈现依值类型理论的方法。 +免责声明：《Functional Programming in Lean》的作者也是《The Little Typer》的作者之一。 diff --git a/functional-programming-lean/src/programs-proofs.md b/functional-programming-lean/src/programs-proofs.md index ccae925..d3f4f0d 100644 --- a/functional-programming-lean/src/programs-proofs.md +++ b/functional-programming-lean/src/programs-proofs.md @@ -1,28 +1,59 @@ + +# 编程、证明与性能 + + + +本章是关于编程的。程序不仅需要计算出正确的结果，还需要高效地执行。 +为了编写高效的功能程序，了解如何适当地使用数据结构， +以及如何考虑运行程序所需的时间和空间非常重要。 + +本章也是关于证明的。在 Lean 中进行高效编程最重要的数据结构体之一是数组， +但安全使用数组需要证明数组索引在边界内。此外，大多数有趣的数组算法并不遵循结构化递归模式。 +相反，它们会遍历数组。虽然这些算法会停机，但 Lean 不一定能够自动检查这一点。 +证明可以用来展示程序为什么会停机。 + + + +重写程序使其运行得更快通常会导致代码更难理解。证明还可以表明两个程序始终会计算出相同的答案， +即使它们使用不同的算法或实现技术。通过这种方式，缓慢、直白的程序可以作为快速、复杂版本的规范。 + +将证明和编程相结合，可以使程序既安全又高效。证明允许省略运行时边界检查， +它们使许多测试变得不必要，并且它们在不引入任何运行时性能开销的情况下为程序提供了极高的置信度。 +然而，证明程序的定理可能是耗时且昂贵的，因此其他工具通常更经济。 + + - - +交互式定理证明是一个深刻的话题。本章仅提供一个示例，面向在 Lean 中编程时出现的证明。 +大多数有趣的定理与编程没有密切关系。请参阅 [下一步](next-steps.md) 以获取更多学习资源的列表。 +然而，就像学习编程一样，在学习编写证明时，没有什么是可以替代实践经验的——是时候开始了！ diff --git a/functional-programming-lean/src/programs-proofs/tail-recursion.md b/functional-programming-lean/src/programs-proofs/tail-recursion.md index 662222e..d4b1f08 100644 --- a/functional-programming-lean/src/programs-proofs/tail-recursion.md +++ b/functional-programming-lean/src/programs-proofs/tail-recursion.md @@ -1,148 +1,366 @@ + +# 尾递归 + + + +虽然 Lean 的 `do`-记法允许使用传统的循环语法，例如 `for` 和 `while`， +但这些结构在幕后会被翻译为递归函数的调用。在大多数编程语言中， +递归函数相对于循环有一个关键缺点：循环不消耗堆栈空间， +而递归函数消耗与递归调用次数成正比的栈空间。栈空间通常是有限的， +通常有必要将以递归函数自然表达的算法，重写为用显式可变堆来分配栈的循环。 + +在函数式编程中，情况通常相反。以可变循环自然表达的程序可能会消耗栈空间， +而将它们重写为递归函数可以使它们快速运行。这是函数式编程语言的一个关键方面： +**尾调用消除（Tail-call Elimination）**。尾调用是从一个函数到另一个函数的调用， +可以编译成一个普通的跳转，替换当前的栈帧而非压入一个新的栈帧， +而尾调用消除就是实现此转换的过程。 + + + +尾调用消除不仅仅是一种可选的优化。它的存在是编写高效函数式代码的基础部分。 +为了使其有效，它必须是可靠的。程序员必须能够可靠地识别尾调用， +并且他们必须相信编译器会消除它们。 + + +函数 `NonTail.sum` 将 `Nat` 列表的内容加起来: + ```lean {{#example_decl Examples/ProgramsProofs/TCO.lean NonTailSum}} ``` + + + + + +将此函数应用于列表 `[1, 2, 3]` 会产生以下求值步骤： + ```lean {{#example_eval Examples/ProgramsProofs/TCO.lean NonTailSumOneTwoThree}} ``` + + + +在求值步骤中，括号表示对 `NonTail.sum` 的递归调用。换句话说，要加起来这三个数字， +程序必须首先检查列表是否非空。要将列表的头部（`1`）加到列表尾部的和上， +首先需要计算列表尾部的和： + ```lean {{#example_eval Examples/ProgramsProofs/TCO.lean NonTailSumOneTwoThree 1}} ``` + + + +但是要计算列表尾部的和，程序必须检查它是否为空，然而它不是。 +尾部本身是一个列表，头部为 `2`。结果步骤正在等待 `NonTail.sum [3]` 的返回： + ```lean {{#example_eval Examples/ProgramsProofs/TCO.lean NonTailSumOneTwoThree 2}} ``` + + +运行时调用栈的重点在于跟踪值 `1`、`2` 和 `3`，以及一个指令将它们加到递归调用的结果上。 +随着递归调用的完成，控制权返回到发出调用的栈帧，于是每一步的加法都被执行了。 +存储列表的头部和将它们相加的指令并不是免费的；它占用的空间与列表的长度成正比。 + + + +函数 `Tail.sum` 也将 `Nat` 列表的内容加起来： + ```lean {{#example_decl Examples/ProgramsProofs/TCO.lean TailSum}} ``` + + + +将其应用于列表 `[1, 2, 3]` 会产生以下求值步骤： + ```lean {{#example_eval Examples/ProgramsProofs/TCO.lean TailSumOneTwoThree}} ``` + + +The internal helper function calls itself recursively, but it does so in a way where nothing needs to be remembered in order to compute the final result. +When `Tail.sumHelper` reaches its base case, control can be returned directly to `Tail.sum`, because the intermediate invocations of `Tail.sumHelper` simply return the results of their recursive calls unmodified. +In other words, a single stack frame can be re-used for each recursive invocation of `Tail.sumHelper`. +Tail-call elimination is exactly this re-use of the stack frame, and `Tail.sumHelper` is referred to as a _tail-recursive function_. +内部的辅助函数以递归方式调用自身，但它以一种新的方式执行此操作，无需记住任何内容即可计算最终结果。 +当 `Tail.sumHelper` 达到其基本情况时，控制权可以直接返回到 `Tail.sum`， +因为 `Tail.sumHelper` 的中间调用只是返回其递归调用的结果，而不会修改结果。 +换句话说，可以为 `Tail.sumHelper` 的每个递归调用重新使用一个栈帧。 +尾调用消除正是这种栈帧的重新使用，而 `Tail.sumHelper` +被称为 **尾递归函数（Tail-Recursive Function）**。 + + + +`Tail.sumHelper` 的第一个参数包含所有其他需要在调用栈中跟踪的信息，即到目前为止遇到的数字的总和。 +在每个递归调用中，此参数都会使用新信息进行更新，而非将新信息添加到调用栈中。 +替换调用栈中信息的 `soFar` 等参数称为 **累加器（Accumulator）**。 + +在撰写本文时，在作者的计算机上，当传入包含 216,856 个或更多条目的列表时， +`NonTail.sum` 会因栈溢出而崩溃。另一方面，`Tail.sum` 可以对包含 +100,000,000 个元素的列表求和，而不会发生栈溢出。由于在运行 `Tail.sum` +时不需要压入新的栈帧，因此它完全等同于一个 `while` 循环，其中一个可变变量保存当前列表。 +在每次递归调用中，栈上的函数参数都会被简单地替换为列表的下一个节点。 + +## 尾部与非尾部位置 + + + +`Tail.sumHelper` 是尾递归的原因在于递归调用处于 **尾部位置**。 +非正式地说，当调用者不需要以任何方式修改返回值，而是会直接返回它时， +函数调用就处于尾部位置。更正式地说，尾部位置可以显式地为表达式定义。 + +如果 `match`-表达式处于尾部位置，那么它的每个分支也处于尾部位置。 +一旦 `match` 选择了一个分支，控制权就会立即传递给它。 +与此类似，如果 `if` 表达式本身处于尾部位置，那么 `if` 表达式的两个分支都处于尾部位置。 +最后，如果 `let` 表达式处于尾部位置，那么它的主体也是如此。 + + + +所有其他位置都不处于尾部位置。函数或构造子的参数不处于尾部位置， +因为求值必须跟踪会应用到参数值的函数或构造子。内部函数的主体不处于尾部位置， +因为控制权甚至可能不会传递给它：函数主体在函数被调用之前不会被求值。 +与此类似，函数类型的函数主体不处于尾部位置。要求值 `(x : α) → E` 中的 `E`， +就有必要跟踪结果，结果的类型必须有 `(x : α) → ...` 包裹在其周围。 + +在 `NonTail.sum` 中，递归调用不在尾部位置，因为它是一个 `+` 的参数。 +在 `Tail.sumHelper` 中，递归调用在尾部位置，因为它紧跟在模式匹配之后， +而模式匹配本身是函数的主体。 + + + +在撰写本文时，Lean 仅消除了递归函数中的直接尾部调用。 +这意味着在 `f` 的定义中对 `f` 的尾部调用将被消除，但对其他函数 `g` 的尾部调用不会被消除。 +当然，消除其他函数的尾部调用以节省栈帧是可行的，但这尚未在 Lean 中实现。 + +## 反转列表 + + + +函数 `NonTail.reverse` 通过将每个子列表的头部追加到结果的末尾来反转列表： + ```lean {{#example_decl Examples/ProgramsProofs/TCO.lean NonTailReverse}} ``` + + + +使用它来反转 `[1, 2, 3]` 会产生以下步骤： + ```lean {{#example_eval Examples/ProgramsProofs/TCO.lean NonTailReverseSteps}} ``` + + +尾递归版本会在每一步的累加器上使用 `x :: ·` 而非 `· ++ [x]`： + ```lean {{#example_decl Examples/ProgramsProofs/TCO.lean TailReverse}} ``` + + + +这是因为在使用 `NonTail.reverse` 计算时保存在每个栈帧中的上下文从基本情况开始应用。 +每个「记住的」上下文片段都按照后进先出的顺序执行。 +另一方面，累加器传递版本从列表中的第一个条目而非原始基本情况开始修改累加器， +如以下归约步骤所示： + ```lean {{#example_eval Examples/ProgramsProofs/TCO.lean TailReverseSteps}} ``` + + + +换句话说，非尾递归版本从基本情况开始，从右到左通过列表修改递归结果。 +列表中的条目以先入先出的顺序影响累加器。带有累加器的尾递归版本从列表的头部开始， +从左到右通过列表修改初始累加器值。 + +由于加法满足交换律，因此无需在 `Tail.sum` 中对此进行处理。 +列表追加不满足交换律，因此必须注意要找到一个在相反方向运行时具有相同效果的操作。 +在 `NonTail.reverse` 中，在递归结果后追加 `[x]` 与以逆序构建结果时将 `x` 添加到列表开头类似。 + + + +## 多个递归调用 + + +在 `BinTree.mirror` 的定义中，有两个递归调用： + ```lean {{#example_decl Examples/Monads/Conveniences.lean mirrorNew}} ``` + + + +就像命令式语言通常会对 `reverse` 和 `sum` 等函数使用 while 循环一样， +它们通常会对这种遍历使用递归函数。此函数无法直接通过累加器传递风格重写为尾递归函数。 + +通常，如果每个递归步骤需要多个递归调用，那么将很难使用累加器传递样式。 +这种困难类似于使用循环和显式数据结构重写递归函数的困难，增加了说服 Lean 函数终止的复杂性。 +但是，就像在 `BinTree.mirror` 中一样，多个递归调用通常表示一个数据结构， +其构造子具有多次递归出现的情况。在这些情况下，结构的深度通常与其整体大小成对数关系， +这使得栈和堆之间的权衡不那么明显。有一些系统化的技术可以使这些函数成为尾递归， +例如使用 **续体传递风格（Continuation-Passing Style）**，但它们超出了本章的范围。 + + + +## 练习 + + +将以下所有非尾递归的函数翻译成累加器传递的尾递归函数： ```lean -{{#example_decl Examples/ProgramsProofs/TCO.lean NonTailLength}} +{{#example_decl Examples/ProgramsProofs/TCO.lean NonTailLength}} ``` ```lean {{#example_decl Examples/ProgramsProofs/TCO.lean NonTailFact}} ``` + + +`NonTail.filter` 的翻译应当产生一个程序，它通过尾递归占用常量栈空间， +运行时间与输入列表的长度成线性相关。相对于原始情况来说，常数因子的开销是可以接受的： + ```lean {{#example_decl Examples/ProgramsProofs/TCO.lean NonTailFilter}} ``` diff --git a/functional-programming-lean/src/tactics-induction-proofs.md b/functional-programming-lean/src/tactics-induction-proofs.md index 789f6dd..4e93d10 100644 --- a/functional-programming-lean/src/tactics-induction-proofs.md +++ b/functional-programming-lean/src/tactics-induction-proofs.md @@ -501,6 +501,7 @@ theorem BinTree.mirror_count (t : BinTree α) : t.mirror.count = t.count := by ``` ### 练习 + 1. 使用**induction...with** 策略证明 **plusR_succ_left**。 2. 重写 **plus_succ_left** 的证明，使用 **<;>** 并写成一行。 -3. 使用列表归纳证明列表追加是结合的：**theorem List.append_assoc (xs ys zs : List α) : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs** \ No newline at end of file +3. 使用列表归纳证明列表追加是结合的：**theorem List.append_assoc (xs ys zs : List α) : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs** + From f7bc4eedff3670689a6429f222dac633a1e4ab0c Mon Sep 17 00:00:00 2001 From: Oling Cat Date: Thu, 27 Jun 2024 02:54:41 +0800 Subject: [PATCH 2/3] tail-recursion-proofs: done --- functional-programming-lean/po/zh-CN.po | 8 +- .../programs-proofs/tail-recursion-proofs.md | 349 +++++++++++++++++- 2 files changed, 349 insertions(+), 8 deletions(-) diff --git a/functional-programming-lean/po/zh-CN.po b/functional-programming-lean/po/zh-CN.po index 8095f07..42aa89d 100644 --- a/functional-programming-lean/po/zh-CN.po +++ b/functional-programming-lean/po/zh-CN.po @@ -24534,7 +24534,7 @@ msgstr "" "`rfl` 策略无法在此处应用，因为 `NonTail.sum` 和 `Tail.sum` " "在定义上不相等。然而，函数可以以不止定义相等的方式相等。还可以通过证明两个函数对相同输入产生相等输出，来证明它们相等。换句话说，\\\\( f = g " "\\\\) 可以通过证明 \\\\( f(x) = g(x) \\\\) 对于所有可能的输入 \\\\( x \\\\) 来证明。此原理称为 " -"_函数扩展性_。函数扩展性正是 `NonTail.sum` 等于 `Tail.sum` 的原因：它们都对数字列表求和。" +"_函数外延性_。函数外延性正是 `NonTail.sum` 等于 `Tail.sum` 的原因：它们都对数字列表求和。" #: src/programs-proofs/tail-recursion-proofs.md:27 #, fuzzy @@ -24546,7 +24546,7 @@ msgid "" "equal:" msgstr "" "在 Lean 的策略语言中，使用 `funext` " -"调用函数扩展性，后跟一个用于任意参数的名称。任意参数作为假设添加到上下文中，目标变为要求证明应用于此参数的函数相等：" +"调用函数外延性，后跟一个用于任意参数的名称。任意参数作为假设添加到上下文中，目标变为要求证明应用于此参数的函数相等：" #: src/programs-proofs/tail-recursion-proofs.md:40 #, fuzzy @@ -24830,7 +24830,7 @@ msgid "" "The actual proof requires only a little additional work to get the goal to " "match the helper's type. The first step is still to invoke function " "extensionality:" -msgstr "实际证明只需要一些额外的工作即可使目标与辅助类型的匹配。第一步仍然是调用函数扩展性：" +msgstr "实际证明只需要一些额外的工作即可使目标与辅助类型的匹配。第一步仍然是调用函数外延性：" #: src/programs-proofs/tail-recursion-proofs.md:415 #, fuzzy @@ -27510,7 +27510,7 @@ msgid "" "statement that relates arbitrary initial accumulator values to the final " "result of the original function is needed." msgstr "" -"通常，证明两个函数相等是使用函数扩展性（`funext` " +"通常，证明两个函数相等是使用函数外延性（`funext` " "策略）完成的，即如果两个函数对每个输入返回相同的值，则它们相等。如果函数是递归的，那么归纳通常是证明其输出相同的好方法。通常，函数的递归定义将对一个特定参数进行递归调用；这个参数是归纳的一个好选择。在某些情况下，归纳假设不够充分。解决这个问题通常需要考虑如何构建定理陈述的更通用版本，以提供足够充分的归纳假设。特别是，为了证明一个函数等价于一个累加器传递版本，需要一个将任意初始累加器值与原始函数的最终结果联系起来的定理陈述。" #: src/programs-proofs/summary.md:46 diff --git a/functional-programming-lean/src/programs-proofs/tail-recursion-proofs.md b/functional-programming-lean/src/programs-proofs/tail-recursion-proofs.md index 3e24da0..b1bb7f5 100644 --- a/functional-programming-lean/src/programs-proofs/tail-recursion-proofs.md +++ b/functional-programming-lean/src/programs-proofs/tail-recursion-proofs.md @@ -1,244 +1,528 @@ + +# 证明等价 + + + +重写为使用尾递归和累加器的程序可能看起来与原始程序非常不同。 +原始递归函数通常更容易理解，但它有在运行时耗尽栈的风险。 +在用示例测试程序的两个版本以排除简单错误后，可以使用证明来一劳永逸地证明二者是等价的。 + + +## 证明 `sum` 相等 + + +要证明 `sum` 的两个版本相等，首先用桩（stub）证明编写定理的陈述： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq0}} ``` + + + +正如预期，Lean 描述了一个未解决的目标： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEq0}} ``` + + +`rfl` 策略无法在此处应用，因为 `NonTail.sum` 和 `Tail.sum` 在定义上不相等。 +然而，函数除了定义相等外还存在更多相等的方式。还可以通过证明两个函数对相同输入产生相等输出， +来证明它们相等。换句话说，可以通过证明「对于所有可能的输入 \\( x \\)， +都有 \\( f(x) = g(x) \\)」来证明 \\( f = g \\)。此原理称为 **函数外延性（Function Extensionality）**。 +函数外延性正是 `NonTail.sum` 等于 `Tail.sum` 的原因：它们都对数字列表求和。 + + +在 Lean 的策略语言中，可使用 `funext` 调用函数外延性，后跟一个用于任意参数的名称。 +任意参数会作为假设添加到语境中，目标变为证明应用于此参数的函数相等： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq1}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEq1}} ``` + + +此目标可通过对参数 `xs` 进行归纳来证明。当应用于空列表时，`sum` 函数都返回 `0`，这是基本情况。 +在输入列表的开头添加一个数字会让两个函数都将该数字添加到结果中，这是归纳步骤。 +调用 `induction` 策略会产生两个目标： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq2a}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEq2a}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEq2b}} ``` + + +`nil` 的基本情况可以使用 `rfl` 解决，因为当传递空列表时，两个函数都返回 `0`： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq3}} ``` + + +解决归纳步骤的第一步是简化目标，要求 `simp` 展开 `NonTail.sum` 和 `Tail.sum`： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq4}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEq4}} ``` + + + +展开 `Tail.sum` 会发现它直接委托给了 `Tail.sumHelper`，它也应该被简化： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq5}} ``` + + + +在结果目标中，`sumHelper` 执行了一步计算并将 `y` 加到累加器上： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEq5}} ``` + + + +使用归纳假设重写会从目标中删除所有 `NonTail.sum` 的引用： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq6}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEq6}} ``` + + + +这个新目标表明，将某个数字加到列表的和中与在 `sumHelper` 中使用该数字作为初始累加器相同。 +为了清晰起见，这个新目标可以作为独立的定理来证明： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEqHelperBad0}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEqHelperBad0}} ``` + + + +这又是一次归纳证明，其中基本情况使用 `rfl` 证明： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEqHelperBad1}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEqHelperBad1}} ``` + + + +由于这是一个归纳步骤，因此目标应该被简化，直到它与归纳假设 `ih` 匹配。 +简化，然后使用 `Tail.sum` 和 `Tail.sumHelper` 的定义，得到以下结果： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEqHelperBad2}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEqHelperBad2}} ``` + + + +理想情况下，归纳假设可以用来替换 `Tail.sumHelper (y + n) ys`，但它们不匹配。 +归纳假设可用于 `Tail.sumHelper n ys`，而非 `Tail.sumHelper (y + n) ys`。 +换句话说，这个证明到这里被卡住了。 + +## 第二次尝试 + + + +与其试图弄清楚证明，不如退一步思考。为什么函数的尾递归版本等于非尾递归版本？ +从根本上讲，在列表中的每个条目中，累加器都会增加与递归结果中添加的量相同的值。 +这个见解可以用来写一个优雅的证明。 +重点在于，归纳证明必须设置成归纳假设可以应用于 **任何** 累加器值。 + + +放弃之前的尝试，这个见解可以编码为以下陈述： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper0}} ``` + + + +在这个陈述中，非常重要的是 `n` 是冒号后面类型的组成部分。 +产生的目标以 `∀ (n : Nat)` 开头，这是「对于所有 `n`」的缩写： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper0}} ``` + + + +使用归纳策略会产生包含这个「对于所有（for all）」语句的目标： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper1a}} ``` + + + +在 `nil` 情况下，目标是： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper1a}} ``` + + + +对于 `cons` 的归纳步骤，归纳假设和具体目标都包含「对于所有 `n`」： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper1b}} ``` + + + +换句话说，目标变得更难证明，但归纳假设相应地更加有用。 + +对于以「对于所有 \\( x \\)」开头的陈述的数学证明应该假设存在任意的 \\( x \\)， +并证明该阐述。「任意」意味着不假设 \\( x \\) 的任何额外性质，因此结果语句将适用于 **任何** \\( x \\)。 +在 Lean 中，「对于所有」语句是一个依值函数：无论将其应用于哪个特定值，它都将返回命题的证据。 +类似地，选择任意 \\( x \\) 的过程与使用 `fun x => ...` 相同。在策略语言中， +选择任意 \\( x \\) 的过程是使用 `intro` 策略执行的，当策略脚本完成后，它会在幕后生成函数。 +`intro` 策略应当被提供用于此任意值的名称。 + + + +在 `nil` 情况下使用 `intro` 策略会从目标中移除 `∀ (n : Nat),`，并添加假设 `n : Nat`： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper2}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper2}} ``` + + + +此命题等式的两边在定义上等于 `n`，因此 `rfl` 就足够了： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper3}} ``` -The `cons` goal also contains a "for all": + +`cons` 目标也包含一个「对于所有」： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper3}} ``` + + + +这这里建议使用 `intro`。 + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper4}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper4}} ``` + + + +现在，证明目标包含应用于 `y :: ys` 的 `NonTail.sum` 和 `Tail.sumHelper`。 +简化器可以使下一步更清晰： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper5}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper5}} ``` + + + +此目标非常接近于匹配归纳假设。它不匹配的方面有两个： + + * 等式的左侧是 `n + (y + NonTail.sum ys)`，但归纳假设需要左侧是一个添加到 `NonTail.sum ys` 的数字。 + 换句话说，此目标应重写为 `(n + y) + NonTail.sum ys`，这是有效的，因为自然数加法满足结合律。 + * 当左侧重写为 `(y + n) + NonTail.sum ys` 时，右侧的累加器参数应为 `n + y` 而非 `y + n` 以进行匹配。 + 此重写是有效的，因为加法也满足交换律。 + + +The associativity and commutativity of addition have already been proved in Lean's standard library. +The proof of associativity is named `{{#example_in Examples/ProgramsProofs/TCO.lean NatAddAssoc}}`, and its type is `{{#example_out Examples/ProgramsProofs/TCO.lean NatAddAssoc}}`, while the proof of commutativity is called `{{#example_in Examples/ProgramsProofs/TCO.lean NatAddComm}}` and has type `{{#example_out Examples/ProgramsProofs/TCO.lean NatAddComm}}`. +Normally, the `rw` tactic is provided with an expression whose type is an equality. +However, if the argument is instead a dependent function whose return type is an equality, it attempts to find arguments to the function that would allow the equality to match something in the goal. +There is only one opportunity to apply associativity, though the direction of the rewrite must be reversed because the right side of the equality in `{{#example_in Examples/ProgramsProofs/TCO.lean NatAddAssoc}}` is the one that matches the proof goal: + +加法的结合律和交换律已在 Lean 的标准库中得到证明。结合律的证明名为 +`{{#example_in Examples/ProgramsProofs/TCO.lean NatAddAssoc}}`， +其类型为 `{{#example_out Examples/ProgramsProofs/TCO.lean NatAddAssoc}}`， +而交换律的证明称为 `{{#example_in Examples/ProgramsProofs/TCO.lean NatAddComm}}`， +其类型为 `{{#example_out Examples/ProgramsProofs/TCO.lean NatAddComm}}`。 +通常，`rw` 策略会提供一个类型为等式的表达式。但是，如果参数是一个返回类型为等式的相关函数， +它会尝试查找函数的参数，以便等式可以匹配目标中的某个内容。 +虽然必须反转重写方向，但只有一种机会应用结合律， +因为 `{{#example_in Examples/ProgramsProofs/TCO.lean NatAddAssoc}}` +中等式的右侧是与证明目标匹配的： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper6}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper6}} ``` + + + +然而，直接使用 `{{#example_in Examples/ProgramsProofs/TCO.lean NatAddComm}}` +重写会导致错误的结果。`rw` 策略猜测了错误的重写位置，导致了意料之外的目标： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper7}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper7}} ``` + + + +可以通过显式地将 `y` 和 `n` 作为参数提供给 `Nat.add_comm` 来解决此问题： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper8}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper8}} ``` + + + +现在目标与归纳假设相匹配了。特别是，归纳假设的类型是一个依值函数类型。 +将 `ih` 应用于 `n + y` 会产生刚好期望的类型。如果其参数具有期望的类型， +`exact` 策略会完成证明目标： + ```leantac {{#example_decl Examples/ProgramsProofs/TCO.lean nonTailEqHelperDone}} ``` + + +实际的证明只需要一些额外的工作即可使目标与辅助函数的类型相匹配。 +第一步仍然是调用函数外延性： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqReal0}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqReal0}} ``` + + + +下一步是展开 `Tail.sum`，暴露出 `Tail.sumHelper`： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqReal1}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqReal1}} ``` + + + +完成这一步后，类型已经近乎匹配了。但是，辅助类型在左侧有一个额外的加数。 +换句话说，证明目标是 `NonTail.sum xs = Tail.sumHelper 0 xs`， +但将 `non_tail_sum_eq_helper_accum` 应用于 `xs` 和 `0` 会产生类型 +`0 + NonTail.sum xs = Tail.sumHelper 0 xs`。 +另一个标准库证明 `{{#example_in Examples/ProgramsProofs/TCO.lean NatZeroAdd}}` 的类型为 +`{{#example_out Examples/ProgramsProofs/TCO.lean NatZeroAdd}}`。 +将此函数应用于 `NonTail.sum xs` 会产生类型为 +`{{#example_out Examples/ProgramsProofs/TCO.lean NatZeroAddApplied}}` 的表达式， +因此从右往左重写会产生期望的目标： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqReal2}} ``` + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqReal2}} ``` + + + +最后，可以使用辅助定理来完成证明： + ```leantac {{#example_decl Examples/ProgramsProofs/TCO.lean nonTailEqRealDone}} ``` + +此证明演示了在证明「累加器传递尾递归函数等于非尾递归版本」时可以使用的通用模式。 +第一步是发现起始累加器参数和最终结果之间的关系。 +例如，以 `n` 的累加器开始 `Tail.sumHelper` 会导致最终的和被添加到 `n` 中， +而以 `ys` 的累加器开始 `Tail.reverseHelper` 会导致最终反转的列表被前置到 `ys` 中。 +第二步是将此关系写成定理陈述，并通过归纳法证明它。虽然在实践中， +累加器总是用一些中性值（Neutral，即幺元，例如 `0` 或 `[]`）初始化， +但允许起始累加器为任何值的更通用的陈述是获得足够强的归纳假设所需要的。 +最后，将此辅助定理与实际的初始累加器值一起使用会产生期望的证明。 +例如，在 `non_tail_sum_eq_tail_sum` 中，累加器指定为 `0`。 +这可能需要重写目标以使中性初始累加器值出现在正确的位置。 - + +## 练习 + + + +### 热身 + + +使用 `induction` 策略编写你自己的 `Nat.zero_add`、`Nat.add_assoc` 和 `Nat.add_comm` 的证明。 + + +### 更多累加器证明 + + + +#### 反转列表 + + +将 `sum` 的证明调整为 `NonTail.reverse` 和 `Tail.reverse` 的证明。 +第一步是思考传递给 `Tail.reverseHelper` 的累加器值与非尾递归反转之间的关系。 +正如在 `Tail.sumHelper` 中将数字添加到累加器中与将其添加到整体的和中相同， +在 `Tail.reverseHelper` 中使用 `List.cons` 将新条目添加到累加器中相当于对整体结果进行了一些更改。 +用纸和笔尝试三个或四个不同的累加器值，直到关系变得清晰。 +使用此关系来证明一个合适的辅助定理。然后，写下整体定理。 +因为 `NonTail.reverse` 和 `Tail.reverse` 是多态的，所以声明它们的相等性需要使用 +`@` 来阻止 Lean 尝试找出为 `α` 使用哪种类型。一旦 `α` 被视为一个普通参数， +`funext` 应该与 `α` 和 `xs` 一起调用： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean reverseEqStart}} ``` + + + +这会产生一个合适的目标： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean reverseEqStart}} ``` - + +#### 阶乘 + + + +通过找到累加器和结果之间的关系并证明一个合适的辅助定理， +证明上一节练习中的 `NonTail.factorial` 等于你的尾递归版本的解决方案。 From 5019b3ba1af3867ebb69c02351d08806147f3e0d Mon Sep 17 00:00:00 2001 From: Oling Cat Date: Sun, 30 Jun 2024 04:11:27 +0800 Subject: [PATCH 3/3] programs-proofs: done --- functional-programming-lean/po/zh-CN.po | 14 +- functional-programming-lean/src/SUMMARY.md | 2 +- .../src/getting-to-know/conveniences.md | 6 +- .../getting-to-know/datatypes-and-patterns.md | 2 +- .../src/hello-world/running-a-program.md | 2 +- .../src/hello-world/step-by-step.md | 2 +- functional-programming-lean/src/next-steps.md | 82 ++- .../src/programs-proofs/arrays-termination.md | 330 ++++++++++- .../src/programs-proofs/fin.md | 67 +++ .../src/programs-proofs/inequalities.md | 520 +++++++++++++++++- .../src/programs-proofs/insertion-sort.md | 485 +++++++++++++++- .../src/programs-proofs/special-types.md | 82 +++ .../src/programs-proofs/summary.md | 149 +++++ .../src/type-classes/coercion.md | 2 +- .../src/type-classes/out-params.md | 2 +- .../src/type-classes/polymorphism.md | 2 +- .../src/type-classes/pos.md | 4 +- 17 files changed, 1704 insertions(+), 49 deletions(-) diff --git a/functional-programming-lean/po/zh-CN.po b/functional-programming-lean/po/zh-CN.po index 42aa89d..a3bd995 100644 --- a/functional-programming-lean/po/zh-CN.po +++ b/functional-programming-lean/po/zh-CN.po @@ -20231,7 +20231,7 @@ msgid "" "When pattern matching refines the type of a program in addition to " "discovering the structure of a value, it is called _dependent pattern " "matching_." -msgstr "当模式匹配除了发现值结构体之外还细化程序的类型时，它被称为 _依赖模式匹配_。" +msgstr "当模式匹配除了发现值结构体之外还细化程序的类型时，它被称为 _依值模式匹配_。" #: src/dependent-types/indexed-families.md:113 #, fuzzy @@ -20554,7 +20554,7 @@ msgid "" "`NatOrBool.bool.asType`, and these compute to the actual types `Nat` and " "`Bool`." msgstr "" -"对 `t` 进行依赖模式匹配可以分别将预期结果类型 `t.asType` 优化为 `NatOrBool.nat.asType` 和 " +"对 `t` 进行依值模式匹配可以分别将预期结果类型 `t.asType` 优化为 `NatOrBool.nat.asType` 和 " "`NatOrBool.bool.asType`，它们计算为实际类型 `Nat` 和 `Bool`。" #: src/dependent-types/universe-pattern.md:40 @@ -21081,7 +21081,7 @@ msgid "" "the `Repr` instances for `Int`, `String`, and `Bool` to be used:" msgstr "" "可以使用相同技术编写 `Repr` 实例。`Repr` 类的函数被称为 " -"`reprPrec`，因为它旨在在显示值时考虑运算符优先级等因素。通过依赖模式匹配细化类型，可以使用 `Int`、`String` 和 `Bool` 的" +"`reprPrec`，因为它旨在在显示值时考虑运算符优先级等因素。通过依值模式匹配细化类型，可以使用 `Int`、`String` 和 `Bool` 的" " `Repr` 实例中的 `reprPrec` 函数：" #: src/dependent-types/typed-queries.md:81 @@ -23656,7 +23656,7 @@ msgstr "" "在策略语言中，可以有多个目标。每个目标由一个类型和一些假设组成。这些类似于使用下划线作为占位符——目标中的类型表示要证明的内容，而假设表示范围内可以使用的内容。在目标" " `case zero` 的情况下，没有假设，类型为 `Nat.zero = Nat.plusR 0 Nat.zero`——这是定理陈述，其中 `0` " "代替了 `k`。在目标 `case succ` 中，有两个假设，分别命名为 `n✝` 和 `n_ih✝`。在幕后，`induction` " -"策略创建了一个依赖模式匹配，它细化了整体类型，`n✝` 表示模式中 `Nat.succ` 的参数。假设 `n_ih✝` 表示在 `n✝` " +"策略创建了一个依值模式匹配，它细化了整体类型，`n✝` 表示模式中 `Nat.succ` 的参数。假设 `n_ih✝` 表示在 `n✝` " "上递归调用生成函数的结果。它的类型是定理的整体类型，只是用 `n✝` 代替了 `k`。作为目标 `case succ` " "的一部分要实现的类型是整体定理陈述，其中 `Nat.succ n✝` 代替了 `k`。" @@ -25159,8 +25159,8 @@ msgid "" "dependent pattern matching is `cases`, which has a syntax similar to that of" " `induction`:" msgstr "" -"此错误发生是因为 `n + 2` 与 `5` 在定义上不相等。在普通的函数定义中，可以对假设 `three` 使用依赖模式匹配来将 `n` 细化为 " -"`3`。`cases` 是依赖模式匹配的策略等价物，其语法类似于 `induction`：" +"此错误发生是因为 `n + 2` 与 `5` 在定义上不相等。在普通的函数定义中，可以对假设 `three` 使用依值模式匹配来将 `n` 细化为 " +"`3`。`cases` 是依值模式匹配的策略等价物，其语法类似于 `induction`：" #: src/programs-proofs/arrays-termination.md:136 #, fuzzy @@ -25926,7 +25926,7 @@ msgid "" "programs. Because `lst` has at least two entries, they can be exposed with " "`match`, which also refines the type through dependent pattern matching:" msgstr "" -"模式匹配在策略脚本中与在程序中一样有效。因为`lst`至少有两个条目，所以它们可以用`match`暴露出来，它还通过依赖模式匹配来细化类型：" +"模式匹配在策略脚本中与在程序中一样有效。因为`lst`至少有两个条目，所以它们可以用`match`暴露出来，它还通过依值模式匹配来细化类型：" #: src/programs-proofs/inequalities.md:509 #, fuzzy diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md index 1796191..7f305eb 100644 --- a/functional-programming-lean/src/SUMMARY.md +++ b/functional-programming-lean/src/SUMMARY.md @@ -63,7 +63,7 @@ - [编程、证明与性能](programs-proofs.md) - [尾递归](programs-proofs/tail-recursion.md) - [证明等价](programs-proofs/tail-recursion-proofs.md) - - [数组与停机](programs-proofs/arrays-termination.md) + - [数组与停机性](programs-proofs/arrays-termination.md) - [更多不等式](programs-proofs/inequalities.md) - [安全数组索引](programs-proofs/fin.md) - [插入排序与数组可变性](programs-proofs/insertion-sort.md) diff --git a/functional-programming-lean/src/getting-to-know/conveniences.md b/functional-programming-lean/src/getting-to-know/conveniences.md index f7253c1..f677daa 100644 --- a/functional-programming-lean/src/getting-to-know/conveniences.md +++ b/functional-programming-lean/src/getting-to-know/conveniences.md @@ -870,7 +870,7 @@ Adding an annotation, such as in `{{#example_in Examples/Intro.lean pointPosWith ## String Interpolation --> -## 字符串内插 +## 字符串插值 -在 Lean 中，在字符串前加上 `s!` 会触发 **内插（Interpolation）** ， +在 Lean 中，在字符串前加上 `s!` 会触发 **插值（Interpolation）** ， 其中字符串中大括号内的表达式会被其值替换。这类似于 Python 中的 `f` 字符串和 C# 中以 `$` 为前缀的字符串。例如， @@ -901,7 +901,7 @@ Not all expressions can be interpolated into a string. For instance, attempting to interpolate a function results in an error. --> -并非所有的表达式都可以内插到字符串中。例如，尝试内插一个函数会产生错误。 +并非所有的表达式都可以插值到字符串中。例如，尝试插值一个函数会产生错误。 ```lean {{#example_in Examples/Intro.lean interpolationOops}} diff --git a/functional-programming-lean/src/getting-to-know/datatypes-and-patterns.md b/functional-programming-lean/src/getting-to-know/datatypes-and-patterns.md index 669bfa8..f2298fe 100644 --- a/functional-programming-lean/src/getting-to-know/datatypes-and-patterns.md +++ b/functional-programming-lean/src/getting-to-know/datatypes-and-patterns.md @@ -486,5 +486,5 @@ This topic is explored in [the final chapter](../programs-proofs/inequalities.md --> 此消息表示 `div` 需要手动证明停机。这个主题在 -[最后一章](../programs-proofs/inequalities.md#division-as-iterated-subtraction) +[最后一章](../programs-proofs/inequalities.md#用减法迭代表示除法) 中进行了探讨。 diff --git a/functional-programming-lean/src/hello-world/running-a-program.md b/functional-programming-lean/src/hello-world/running-a-program.md index 56fcb3c..806d817 100644 --- a/functional-programming-lean/src/hello-world/running-a-program.md +++ b/functional-programming-lean/src/hello-world/running-a-program.md @@ -349,5 +349,5 @@ Finally, the last line in the program is: It uses [string interpolation](../getting-to-know/conveniences.md#string-interpolation) to insert the provided name into a greeting string, writing the result to `stdout`. --> -它使用[字符串内插](../getting-to-know/conveniences.md#string-interpolation) +它使用[字符串插值](../getting-to-know/conveniences.md#字符串插值) 将提供的名称插入到问候字符串中，并将结果写入到 `stdout`。 diff --git a/functional-programming-lean/src/hello-world/step-by-step.md b/functional-programming-lean/src/hello-world/step-by-step.md index 3446f57..28bbb37 100644 --- a/functional-programming-lean/src/hello-world/step-by-step.md +++ b/functional-programming-lean/src/hello-world/step-by-step.md @@ -86,7 +86,7 @@ Statements that consist only of expressions do not introduce any new variables. 该代码块中的第一个语句 `{{#include ../../../examples/hello-name/HelloName.lean:line3}}` 由一个表达式组成。要执行一个表达式，首先要对其进行求值。在这种情况下，`IO.FS.Stream.putStrLn` 的类型为 `IO.FS.Stream → String → IO Unit`。这意味着它是一个接受流和字符串并返回 `IO` 活动的函数。 -该表达式使用[访问器记法](../getting-to-know/structures.md#behind-the-scenes)进行函数调用。 +该表达式使用[访问器记法](../getting-to-know/structures.md#幕后)进行函数调用。 此函数应用于两个参数：标准输出流和字符串。表达式的值为一个 `IO` 活动， 该活动将字符串和换行符写入输出流。得到此值后，下一步是执行它，这会导致字符串和换行符写入到 `stdout`。仅由表达式组成的语句不会引入任何新变量。 diff --git a/functional-programming-lean/src/next-steps.md b/functional-programming-lean/src/next-steps.md index 775f29d..c513ab5 100644 --- a/functional-programming-lean/src/next-steps.md +++ b/functional-programming-lean/src/next-steps.md @@ -1,10 +1,20 @@ + + # 下一步 -本书介绍了 Lean 中函数式编程的基本知识，包括一些互动定理证明的内容。使用依值类型的函数式语言（如 Lean）是一个深奥的主题，内容丰富。根据您的兴趣，以下资源可能对学习 Lean 4 有用。 +本书介绍了 Lean 中函数式编程的基本知识，包括一些互动定理证明的内容。 +使用依值类型的函数式语言（如 Lean）是一个深奥的主题，内容丰富。 +根据您的兴趣，以下资源可能对学习 Lean 4 有用。 + + ### 学习 Lean @@ -17,17 +27,28 @@ How To Prove It With Lean is a Lean-based accompaniment to the well-regarded tex Metaprogramming in Lean 4 provides an overview of Lean's extension mechanisms, from infix operators and notations to macros, custom tactics, and full-on custom embedded languages. Functional Programming in Lean may be interesting to readers who enjoy jokes about recursion. However, the best way to continue learning Lean is to start reading and writing code, consulting the documentation when you get stuck. Additionally, the Lean Zulip is an excellent place to meet other Lean users, ask for help, and help others. - --> Lean 4 本身在以下资源中有详细描述： -[Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/) 是一本关于使用 Lean 编写证明的教程。 -[Lean 4 Manual](https://lean-lang.org/lean4/doc/)提供了该语言及其功能的参考资料。虽然在撰写本文时它仍未完成，但它比本书更详细地描述了 Lean 的许多方面。 -[How To Prove It With Lean](https://djvelleman.github.io/HTPIwL/)是著名教材[How To Prove It](https://www.cambridge.org/highereducation/books/how-to-prove-it/6D2965D625C6836CD4A785A2C843B3DA)的 Lean 版伴随读物，介绍了如何编写纸笔数学证明。 -[Metaprogramming in Lean 4](https://github.com/arthurpaulino/lean4-metaprogramming-book)概述了 Lean 的扩展机制，从中缀运算符和符号到宏、自定义策略和完整的自定义嵌入式语言。 -[Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)可能对喜欢递归笑话的读者感兴趣。 -然而，继续学习 Lean 的最佳方式是开始阅读和编写代码，在遇到困难时查阅文档。此外，[Lean Zulip](https://leanprover.zulipchat.com/) 是结识其他 Lean 用户、寻求帮助和帮助他人的好地方。 +[Lean 4 定理证明](https://www.leanprover.cn/tp-lean-zh/) +是一本关于使用 Lean 编写证明的教程。 +[Lean 4 手册](https://www.leanprover.cn/lean4/) +提供了 Lean 语言及其功能的参考资料。虽然在撰写本文时它仍未完成， +但它比本书更详细地描述了 Lean 的许多方面。 +[怎样用 Lean 证明数学题](https://djvelleman.github.io/HTPIwL/)是著名教材 +[怎样证明数学题](https://book.douban.com/subject/3810450/)的 Lean 版伴随读物， +介绍了如何编写纸笔数学证明。 +[Lean 4 元编程](https://www.leanprover.cn/lean4-mp/)概述了 Lean 的扩展机制， +从中缀运算符和符号到宏、自定义策略和完整的自定义嵌入式语言。 +[Lean 函数式编程](https://www.leanprover.cn/tp-lean-zh/)可能对喜欢递归笑话的读者来说很有趣。 +然而，继续学习 Lean 的最佳方式是开始阅读和编写代码，在遇到困难时查阅文档。 +此外，[Lean Zulip](https://leanprover.zulipchat.com/) 是结识其他 Lean 用户、 +寻求帮助和帮助他人的好地方。 + + ### 标准库 @@ -39,22 +60,38 @@ std4 is an in-progress standard library that includes many data structures, tact To use std4, the first step is to find a commit in its history that's compatible with the version of Lean 4 that you're using (that is, one in which the lean-toolchain file matches the one in your project). Then, add the following to the top level of your lakefile.lean, where COMMIT_HASH is the appropriate version: --> -Lean 自带的库相对较小。Lean 是自托管的，所包含的代码仅够实现 Lean 本身。对于许多应用来说，需要更大的标准库。 +Lean 自带的库相对较小。Lean 是自托管的，所包含的代码仅够实现 Lean 本身。 +对于许多应用来说，需要更大的标准库。 -[std4](https://github.com/leanprover/std4) 是一个正在开发中的标准库，包含许多数据结构、策略、类型类实例和函数，这些都超出了 Lean 编译器本身的范围。要使用 std4，第一步是找到与您使用的 Lean 4 版本兼容的提交记录（即其中的 lean-toolchain 文件与您的项目匹配）。然后，将以下内容添加到您的 lakefile.lean 顶层，其中 COMMIT_HASH 是适当的版本： +[std4](https://github.com/leanprover/std4) 是一个正在开发中的标准库， +包含许多数据结构、策略、类型类实例和函数，这些都超出了 Lean 编译器本身的范围。 +要使用 std4，第一步是找到与您使用的 Lean 4 版本兼容的提交记录（即其中的 lean-toolchain +文件与您的项目匹配）。然后，将以下内容添加到您的 lakefile.lean 顶层， +其中 COMMIT_HASH 是适当的版本： ```lean require std from git "https://github.com/leanprover/std4/" @ "COMMIT_HASH" ``` -### Lean 中的数学 + + +### Lean 形式化数学 -大多数数学资源是为 Lean 3 编写的。在[社区](https://leanprover-community.github.io/learn.html)网站上可以找到许多这样的资源。要开始在 Lean 4 中进行数学研究，最简单的方法可能是参与将数学库 mathlib 从 Lean 3 迁移到 Lean 4 的过程。有关更多信息，请参阅 [mathlib4 的 README](https://github.com/leanprover-community/mathlib4). +大多数数学资源是为 Lean 3 编写的。 +在[社区](https://leanprover-community.github.io/learn.html)网站上可以找到许多这样的资源。 +要开始在 Lean 4 中进行数学研究，最简单的方法可能是参与将数学库 mathlib 从 Lean 3 迁移到 Lean 4 的过程。 +有关更多信息，请参阅 [mathlib4 的 README](https://github.com/leanprover-community/mathlib4). + + ### 在计算机科学中使用依值类型 @@ -62,7 +99,14 @@ Most resources for mathematicians are written for Lean 3. A wide selection are a Coq is a language that has a lot in common with Lean. For computer scientists, the Software Foundations series of interactive textbooks provides an excellent introduction to applications of Coq in computer science. The fundamental ideas of Lean and Coq are very similar, and skills are readily transferable between the systems. --> -Coq 是一种与 Lean 有许多共同点的语言。对于计算机科学家来说，[Software Foundations](https://softwarefoundations.cis.upenn.edu/)系列教材提供了一个很好的介绍，介绍了 Coq 在计算机科学中的应用。Lean 和 Coq 的基本思想非常相似，编程技巧在两个语言之间是可以相互转移的。 +Coq 是一种与 Lean 有许多共同点的语言。对于计算机科学家来说， +[软件基础](https://coq-zh.github.io/SF-zh/)系列教材提供了一个很好的介绍， +介绍了 Coq 在计算机科学中的应用。Lean 和 Coq 的基本思想非常相似， +编程技巧在两个语言之间是可以相互转换的。 + + ### 使用依值类型编程 @@ -70,7 +114,13 @@ Coq 是一种与 Lean 有许多共同点的语言。对于计算机科学家来 For programmers who are interested in learning to use indexed families and dependent types to structure programs, Edwin Brady's Type Driven Development with Idris provides an excellent introduction. Like Coq, Idris is a close cousin of Lean, though it lacks tactics. --> -对于有兴趣学习使用索引族和依值类型来构建程序的程序员来说，Edwin Brady 的[Type Driven Development with Idris](https://www.manning.com/books/type-driven-development-with-idris)提供了一个很好的介绍。像 Coq 一样，Idris 是 Lean 的近亲语言，但是它缺乏策略。 +对于有兴趣学习使用索引族和依值类型来构建程序的程序员来说，Edwin Brady 的 +[Idris 类型驱动开发](https://www.manning.com/books/type-driven-development-with-idris) +提供了一个很好的介绍。和 Coq 一样，Idris 是 Lean 的近亲语言，但是它缺乏策略。 + + ### 理解依值类型 @@ -78,6 +128,8 @@ For programmers who are interested in learning to use indexed families and depen The Little Typer is a book for programmers who haven't formally studied logic or the theory of programming languages, but who want to build an understanding of the core ideas of dependent type theory. While all of the above resources aim to be as practical as possible, The Little Typer presents an approach to dependent type theory where the very basics are built up from scratch, using only concepts from programming. Disclaimer: the author of Functional Programming in Lean is also an author of The Little Typer. --> -[The Little Typer](https://thelittletyper.com/)是一本为没有正式学习过逻辑或编程语言理论，但希望理解依值类型理论核心思想的程序员准备的书。虽然上述所有资源都旨在实现尽可能的实用，但这本书通过从头开始构建基础，使用仅来自编程的概念来呈现依值类型理论的方法。 +[The Little Typer](https://thelittletyper.com/) 是一本为没有正式学习过逻辑或编程语言理论， +但希望理解依值类型论核心思想的程序员准备的书。虽然上述所有资源都旨在实现尽可能的实用， +但这本书通过从头开始构建基础，使用仅来自编程的概念来呈现依值类型理论的方法。 免责声明：《Functional Programming in Lean》的作者也是《The Little Typer》的作者之一。 diff --git a/functional-programming-lean/src/programs-proofs/arrays-termination.md b/functional-programming-lean/src/programs-proofs/arrays-termination.md index 8595bc4..813d0f1 100644 --- a/functional-programming-lean/src/programs-proofs/arrays-termination.md +++ b/functional-programming-lean/src/programs-proofs/arrays-termination.md @@ -1,246 +1,572 @@ + +# 数组与停机性 + + + +为了编写高效的代码，选择合适的数据结构非常重要。链表有它的用途：在某些应用程序中， +共享列表的尾部非常重要。但是，大多数可变长有序数据集合的用例都能由数组更好地提供服务， +数组既有较少的内存开销，又有更好的局部性。 + + +然而，数组相对于列表来说有两个缺点： + + 1. 数组是通过索引访问的，而非通过模式匹配，这为维护安全性增加了 + [证明义务](../props-proofs-indexing.md)。 + 2. 从左到右处理整个数组的循环是一个尾递归函数，但它没有会在每次调用时递减的参数。 + + +高效地使用数组需要知道如何向 Lean 证明数组索引在范围内， +以及如何证明接近数组大小的数组索引也会使程序停机。这两个都使用不等式命题，而非命题等式表示。 + + + +## 不等式 + +由于不同的类型有不同的序概念，不等式需要由两个类来控制，分别称为 `LE` 和 `LT`。 +[标准类型类](../type-classes/standard-classes.md#相等性与有序性) +一节中的表格描述了这些类与语法的关系： + + + +| 表达式 | 脱糖结果 | 类名 | |------------|------------|------------| | `{{#example_in Examples/Classes.lean ltDesugar}}` | `{{#example_out Examples/Classes.lean ltDesugar}}` | `LT` | | `{{#example_in Examples/Classes.lean leDesugar}}` | `{{#example_out Examples/Classes.lean leDesugar}}` | `LE` | | `{{#example_in Examples/Classes.lean gtDesugar}}` | `{{#example_out Examples/Classes.lean gtDesugar}}` | `LT` | | `{{#example_in Examples/Classes.lean geDesugar}}` | `{{#example_out Examples/Classes.lean geDesugar}}` | `LE` | + + +换句话说，一个类型可以定制 `<` 和 `≤` 运算符的含义，而 `>` 和 `≥` 可以从 +`<` 和 `≤` 中派生它们的含义。`LT` 和 `LE` 类具有返回命题而非 `Bool` 的方法： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean less}} ``` + + +`Nat` 的 `LE` 实例会委托给 `Nat.le`： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean LENat}} ``` + + +定义 `Nat.le` 需要 Lean 中尚未介绍的一个特性：它是一个归纳定义的关系。 + + + +### 归纳定义的命题、谓词和关系 + +`Nat.le` 是一个 **归纳定义的关系（Inductively-Defined Relation）**。 +就像 `inductive` 可以用来创建新的数据类型一样，它也可以用来创建新的命题。 +当一个命题接受一个参数时，它被称为 **谓词（Predicate）**，它可能对某些潜在参数为真， +但并非对所有参数都为真。接受多个参数的命题称为 **关系（Relation）**。" + + + +每个归纳定义命题的构造子都是证明它的方法。换句话说，命题的声明描述了它为真的不同形式的证据。 +一个没有参数且只有一个构造子的命题很容易证明： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean EasyToProve}} ``` + + + +证明包括使用其构造子： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean fairlyEasy}} ``` + + + +实际上，命题 `True` 应该总是很容易证明，它的定义就像 `EasyToProve`： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean True}} ``` + + +不带参数的归纳定义命题远不如归纳定义的数据类型有趣。 +这是因为数据本身很有趣——自然数 `3` 不同于数字 `35`，而订购了 3 个披萨的人如果 +30 分钟后收到 35 个披萨会很沮丧。命题的构造子描述了命题可以为真的方式， +但一旦命题被证明，就不需要知道它使用了哪些底层构造子。 +这就是为什么 `Prop` 宇宙中最有趣的归纳定义类型带参数的原因。 + + +归纳定义谓词 `IsThree` 陈述它有三个参数： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean IsThree}} ``` + + +这里使用的机制就像[索引族，如 `HasCol`](../dependent-types/typed-queries.md#列指针)， +只不过结果类型是一个可以被证明的命题，而非可以被使用的数据。 + + + +使用此谓词，可以证明三确实等于三： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean threeIsThree}} ``` + + + +类似地，`IsFive` 是一个谓词，它陈述了其参数为 `5`： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean IsFive}} ``` + + +如果一个数字是三，那么将它加二的结果应该是五。这可以表示为定理陈述： + ```leantac {{#example_in Examples/ProgramsProofs/Arrays.lean threePlusTwoFive0}} ``` + + + +由此产生的目标具有函数类型： + ```output error {{#example_out Examples/ProgramsProofs/Arrays.lean threePlusTwoFive0}} ``` + + + +因此，`intro` 策略可用于将参数转换为假设： + ```leantac {{#example_in Examples/ProgramsProofs/Arrays.lean threePlusTwoFive1}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Arrays.lean threePlusTwoFive1}} ``` + + + +假设 `n` 为三，则应该可以使用 `IsFive` 的构造子来完成证明： + ```leantac {{#example_in Examples/ProgramsProofs/Arrays.lean threePlusTwoFive1a}} ``` + + + +然而，这会产生一个错误： + ```output error {{#example_out Examples/ProgramsProofs/Arrays.lean threePlusTwoFive1a}} ``` + + + +出现此错误是因为 `n + 2` 与 `5` 在定义上不相等。在普通的函数定义中， +可以对假设 `three` 使用依值模式匹配来将 `n` 细化为 `3`。 +依值模式匹配的策略等价为 `cases`，其语法类似于 `induction`： + ```leantac {{#example_in Examples/ProgramsProofs/Arrays.lean threePlusTwoFive2}} ``` + + + +在剩余情况下，`n` 已细化为 `3`： + ```output error {{#example_out Examples/ProgramsProofs/Arrays.lean threePlusTwoFive2}} ``` + + + +由于 `3 + 2` 在定义上等于 `5`，因此构造子现在适用了： + ```leantac {{#example_decl Examples/ProgramsProofs/Arrays.lean threePlusTwoFive3}} ``` + + +标准假命题 `False` 没有构造子，因此无法提供直接证据。 +为 `False` 提供证据的唯一方法是假设本身不可能，类似于用 `nomatch` +来标记类型系统认为无法访问的代码。如 [插曲中的证明一节](../props-proofs-indexing.md#连词) +所述，否定 `Not A` 是 `A → False` 的缩写。`Not A` 也可以写成 `¬A`。 + + +四不是三： + ```leantac {{#example_in Examples/ProgramsProofs/Arrays.lean fourNotThree0}} ``` + + + +初始证明目标包含 `Not`： + ```output error {{#example_out Examples/ProgramsProofs/Arrays.lean fourNotThree0}} ``` + + + +可以使用 `simp` 显示出它实际上是一个函数类型： + ```leantac {{#example_in Examples/ProgramsProofs/Arrays.lean fourNotThree1}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Arrays.lean fourNotThree1}} ``` + + + +因为目标是一个函数类型，所以 `intro` 可用于将参数转换为假设。 +无需保留 `simp`，因为 `intro` 可以展开 `Not` 本身的定义： + ```leantac {{#example_in Examples/ProgramsProofs/Arrays.lean fourNotThree2}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Arrays.lean fourNotThree2}} ``` + + + +在此证明中，`cases` 策略直接解决了目标： + ```leantac {{#example_decl Examples/ProgramsProofs/Arrays.lean fourNotThreeDone}} ``` + + +就像对 `Vect String 2` 的模式匹配不需要包含 `Vect.nil` 的情况一样， +对 `IsThree 4` 的情况证明不需要包含 `isThree` 的情况。 + + + +### 自然数不等式 + + +`Nat.le` 的定义有一个参数和一个索引： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean NatLe}} ``` + + + +参数 `n` 应该是较小的数字，而索引应该是大于或等于 `n` 的数字。 +当两个数字相等时使用 `refl` 构造子，而当索引大于 `n` 时使用 `step` 构造子。 + + +从证据的视角来看，证明 \\( n \leq k \\) 需要找到一些数字 \\( d \\) 使得 \\( n + d = m \\)。 +在 Lean 中，证明由 \\( d \\) 个 `Nat.le.step` 实例包裹的 `Nat.le.refl` 构造子组成。 +每个 `step` 构造子将其索引参数加一，因此 \\( d \\) 个 `step` 构造子将 \\( d \\) 加到较大的数字上。 +例如，证明四小于或等于七由 `refl` 周围的三个 `step` 组成： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean four_le_seven}} ``` + + +严格小于关系通过在左侧数字上加一来定义： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean NatLt}} ``` + + + +证明四严格小于七由 `refl` 周围的两个 `step` 组成： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean four_lt_seven}} ``` + + + +这是因为 `4 < 7` 等价于 `5 ≤ 7`。 + +## 停机性证明 + + + +函数 `Array.map` 接受一个函数和一个数组，它将接受的函数应用于输入数组的每个元素后，返回产生的新数组。 +将其写成尾递归函数遵循通常的累加器模式，即将输入委托给一个函数，该函数将输出的数组传递给累加器。 +累加器用空数组初始化。传递累加器的辅助函数还接受一个参数来跟踪数组中的当前索引，该索引从 `0` 开始： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean ArrayMap}} ``` + + +辅助函数应在每次迭代时检查索引是否仍在范围内。如果是，则应再次循环， +将转换后的元素添加到累加器的末尾，并将索引加 `1`。如果不是，则应终止并返回累加器。 +此代码的最初实现会失败，因为 Lean 无法证明数组索引有效： + ```lean {{#example_in Examples/ProgramsProofs/Arrays.lean mapHelperIndexIssue}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Arrays.lean mapHelperIndexIssue}} ``` + + + +然而，条件表达式已经检查了有效数组索引所要求的精确条件（即 `i < arr.size`）。 +为 `if` 添加一个名称可以解决此问题，因为它添加了一个前提供数组索引策略使用： + ```lean {{#example_in Examples/ProgramsProofs/Arrays.lean arrayMapHelperTermIssue}} ``` + + + +然而，Lean 不接受修改后的程序，因为递归调用不是针对输入构造子之一的参数进行的。 +实际上，累加器和索引都在增长，而非缩小： + ```output error {{#example_out Examples/ProgramsProofs/Arrays.lean arrayMapHelperTermIssue}} ``` + + +尽管如此，此函数仍然会停机，因此简单地将其标记为 `partial` 非常不妥。 + + + +为什么 `arrayMapHelper` 会停机？每次迭代都会检查索引 `i` 是否仍在数组 `arr` 的范围内。 +如果是，则 `i` 将增加并且循环将重复。如果不是，则程序将停机。因为 `arr.size` 是一个有限数， +所以 `i` 只可以增加有限次。即使函数的每个参数在每次调用时都不会减少，`arr.size - i` 也会减小到零。 + + +可以通过在定义的末尾提供 `termination_by` 子句来指示 Lean 使用另一个表达式判定停机。 +`termination_by` 子句有两个组成部分：函数参数的名称和使用这些名称的表达式， +该表达式应在每次调用时减少。对于 `arrayMapHelper`，最终定义如下所示： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean ArrayMapHelperOk}} ``` + + +类似的停机证明可用于编写 `Array.find`，这是一个在数组中查找满足布尔函数的第一个元素， +并返回该元素及其索引的函数： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean ArrayFind}} ``` + + + +同样，辅助函数会停机，因为随着 `i` 的增加，`arr.size - i` 会减少： + ```lean {{#example_decl Examples/ProgramsProofs/Arrays.lean ArrayFindHelper}} ``` + +并非所有停机参数都像这个参数一样简单。但是，在所有停机证明中， +都会出现「基于函数的参数找出在每次调用时都会减少的某个表达式」这种基本结构。 +有时，为了弄清楚函数为何停机，可能需要一点创造力，有时 Lean 需要额外的证明才能接受停机参数。 - + + +## 练习 + + + * 使用尾递归累加器传递函数和 `termination_by` 子句在数组上实现 `ForM (Array α)` 实例。 + * 使用 **不需要** `termination_by` 子句的尾递归累加器传递函数实现一个用于反转数组的函数。 + * 使用恒等单子中的 `for ... in ...` 循环重新实现 `Array.map`、`Array.find` 和 `ForM` 实例， + 并比较结果代码。 + * 使用恒等单子中的 `for ... in ...` 循环重新实现数组反转。将其与尾递归函数的版本进行比较。 diff --git a/functional-programming-lean/src/programs-proofs/fin.md b/functional-programming-lean/src/programs-proofs/fin.md index 9968c40..e59a904 100644 --- a/functional-programming-lean/src/programs-proofs/fin.md +++ b/functional-programming-lean/src/programs-proofs/fin.md @@ -1,49 +1,116 @@ + +# 安全数组索引 + + + +`Array` 和 `Nat` 的 `GetElem` 实例需要证明提供的 `Nat` 小于数组。 +在实践中，这些证明通常最终会连同索引一起传递给函数。 +与其分别传递索引和证明，可以使用名为 `Fin` 的类型将索引和证明捆绑到单个值中。 +这可以使代码更易阅。此外，许多对数组的内置操作将其索引参数作为 `Fin` 而非 `Nat`， +因此使用这些内置操作需要了解如何使用 `Fin`。 + + +类型 `Fin n` 表示严格小于 `n` 的数字。换句话说，`Fin 3` 描述 `0`、`1` 和 `2`， +而 `Fin 0` 没有任何值。`Fin` 的定义类似于 `Subtype`，因为 `Fin n` 是一个包含 `Nat` +和小于 `n` 的证明的结构体： + ```lean {{#example_decl Examples/ProgramsProofs/Fin.lean Fin}} ``` + + +Lean 包含 `ToString` 和 `OfNat` 的实例，允许将 `Fin` 值方便地用作数字。 +换句话说，`{{#example_in Examples/ProgramsProofs/Fin.lean fiveFinEight}}` +的输出为 `{{#example_out Examples/ProgramsProofs/Fin.lean fiveFinEight}}`， +而非类似 `{val := 5, isLt := _}` 的值。 + +当提供的数字大于边界时，`OfNat` 实例对于 `Fin` 不会失败，而是返回一个对边界取模的值。 +这意味着 `#eval (45 : Fin 10)` 的结果是 `5`，而非编译时错误。 + + + +在返回类型中，将 `Fin` 作为找到的索引返回，能够让它与其所在的数据结构的连接更加清晰。 +[上一节](./arrays-termination.md#proving-termination)中的 `Array.find` 返回一个索引， +调用者不能立即使用它来执行数组查找，因为有关其有效性的信息已丢失。 +更具体类型的值可以直接使用，而不会使程序变得复杂得多： + ```lean {{#example_decl Examples/ProgramsProofs/Fin.lean ArrayFindHelper}} {{#example_decl Examples/ProgramsProofs/Fin.lean ArrayFind}} ``` + +## 练习 + + + +编写一个函数 `Fin.next? : Fin n → Option (Fin n)` 当 `Fin` 在边界内时返回下一个最大的 `Fin`， +否则返回 `none`。检查 + ```lean {{#example_in Examples/ProgramsProofs/Fin.lean nextThreeFin}} ``` + + + +会输出 + ```output info {{#example_out Examples/ProgramsProofs/Fin.lean nextThreeFin}} ``` + + + +而 + ```lean {{#example_in Examples/ProgramsProofs/Fin.lean nextSevenFin}} ``` + + + +会输出 + ```output info {{#example_out Examples/ProgramsProofs/Fin.lean nextSevenFin}} ``` diff --git a/functional-programming-lean/src/programs-proofs/inequalities.md b/functional-programming-lean/src/programs-proofs/inequalities.md index ad2ab09..972651e 100644 --- a/functional-programming-lean/src/programs-proofs/inequalities.md +++ b/functional-programming-lean/src/programs-proofs/inequalities.md @@ -1,385 +1,856 @@ + +# 更多不等式 + + + +Lean 的内置证明自动化足以检查 `arrayMapHelper` 和 `findHelper` 是否停机。 +所需要做的就是提供一个值随着每次递归调用而减小的表达式。 +但是，Lean 的内置自动化不是万能的，它通常需要一些帮助。 + + +## 归并排序 -One example of a function whose termination proof is non-trivial is merge sort on `List`. -Merge sort consists of two phases: first, a list is split in half. -Each half is sorted using merge sort, and then the results are merged using a function that combines two sorted lists into a larger sorted list. -The base cases are the empty list and the singleton list, both of which are already considered to be sorted. +一个停机证明非平凡的函数示例是 `List` 上的归并排序。归并排序包含两个阶段： +首先，将列表分成两半。使用归并排序对每一半进行排序， +然后使用一个将两个已排序列表合并为一个更大的已排序列表的函数合并结果。 +基本情况是空列表和单元素列表，它们都被认为已经排序。 + + +要合并两个已排序列表，需要考虑两个基本情况： + + 1. 如果一个输入列表为空，则结果是另一个列表。 + 2. 如果两个列表都不为空，则应比较它们的头部。该函数的结果是两个头部中较小的一个， + 后面是合并两个列表的剩余项的结果。 + + +这在任何列表上都不是结构化递归。递归停机是因为在每次递归调用中都会从两个列表中的一个中删除一个项， +但它可能是任何一个列表。`termination_by` 子句使用两个列表长度的和作为递减值： + ```lean {{#example_decl Examples/ProgramsProofs/Inequalities.lean merge}} ``` + + +除了使用列表的长度外，还可以提供一个包含两个列表的偶对： + ```lean {{#example_decl Examples/ProgramsProofs/Inequalities.lean mergePairTerm}} ``` + + + +它有效是因为 Lean 有一个内置的数据大小概念，通过一个称为 `WellFoundedRelation` +的类型类来表示。如果偶对中的第一个或第二个项缩小，偶对的实例会自动认为它们会变小。 + + +分割列表的一个简单方法是将输入列表中的每个项添加到两个交替的输出列表中： + ```lean {{#example_decl Examples/ProgramsProofs/Inequalities.lean splitList}} ``` + + +归并排序检查是否已达到基本情况。如果是，则返回输入列表。 +如果不是，则分割输入，并合并对每一半排序的结果： + ```lean {{#example_in Examples/ProgramsProofs/Inequalities.lean mergeSortNoTerm}} ``` + + + +Lean 的模式匹配编译器能够判断由测试 `xs.length < 2` 的 `if` 引入的前提 `h` +排除了长度超过一个条目的列表，因此没有「缺少情况」的错误。 +然而，即使此程序总是停机，它也不是结构化递归的： + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean mergeSortNoTerm}} ``` + + + +它能停机的原因是 `splitList` 总是返回比其输入更短的列表。 +因此，`halves.fst` 和 `halves.snd` 的长度小于 `xs` 的长度。 +这可以使用 `termination_by` 子句来表示： + ```lean {{#example_in Examples/ProgramsProofs/Inequalities.lean mergeSortGottaProveIt}} ``` + + + +有了这个子句，错误信息就变了。Lean 不会抱怨函数不是结构化递归的， +而是指出它无法自动证明 `(splitList xs).fst.length < xs.length`： + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean mergeSortGottaProveIt}} ``` + + +## 分割列表使其变短 + +还需要证明 `(splitList xs).snd.length < xs.length`。由于 `splitList` +在向两个列表添加条目之间交替进行，因此最简单的方法是同时证明这两个语句， +这样证明的结构就可以遵循用于实现 `splitList` 的算法。换句话说，最简单的方法是证明 +`∀(lst : List), (splitList lst).fst.length < lst.length ∧ (splitList lst).snd.length < lst.length`。 + + + +不幸的是，这个陈述是错误的。特别是， +`{{#example_in Examples/ProgramsProofs/Inequalities.lean splitListEmpty}}` 是 +`{{#example_out Examples/ProgramsProofs/Inequalities.lean splitListEmpty}}`。 +两个输出列表的长度都是 `0`，这并不小于输入列表的长度 `0`。类似地， +`{{#example_in Examples/ProgramsProofs/Inequalities.lean splitListOne}}` 求值为 +`([\"basalt\"], [])`，而 `["basalt"]` 并不比 `["basalt"]` 短。然而， +`{{#example_in Examples/ProgramsProofs/Inequalities.lean splitListTwo}}` 求值为 +`{{#example_out Examples/ProgramsProofs/Inequalities.lean splitListTwo}}`， +这两个输出列表都比输入列表短。 + + + +输出列表的长度始终小于或等于输入列表的长度，但仅当输入列表至少包含两个条目时， +它们才严格更短。事实证明，最容易证明前一个陈述，然后将其扩展到后一个陈述。 +从定理的陈述开始： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le0}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le0}} ``` + + + +由于 `splitList` 在列表上是结构化递归的，因此证明应使用归纳法。 +`splitList` 中的结构化递归非常适合归纳证明：归纳法的基本情况与递归的基本情况匹配， +归纳步骤与递归调用匹配。`induction` 策略给出了两个目标： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le1a}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le1a}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le1b}} ``` + + +可以通过调用简化器并指示它展开 `splitList` 的定义来证明 `nil` 情况的目标， +因为空列表的长度小于或等于空列表的长度。类似地，在 `cons` 情况下使用 `splitList` +简化会在目标中的长度周围放置 `Nat.succ`： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le2}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le2}} ``` + + +这是因为对 `List.length` 的调用消耗了列表 `x :: xs` 的头部，将其转换为 `Nat.succ`， +既在输入列表的长度中，也在第一个输出列表的长度中。 + + + +在 Lean 中编写 `A ∧ B` 是 `And A B` 的缩写。 +`And` 是 `Prop` 宇宙中的一个结构体类型： + ```lean {{#example_decl Examples/ProgramsProofs/Inequalities.lean And}} ``` + + + +换句话说，`A ∧ B` 的证明包括应用于 `left` 字段中 `A` 的证明和应用于 `right` +字段中 `B` 的证明的 `And.intro` 构造子。 + +`cases` 策略允许证明依次考虑数据类型的每个构造子或命题的每个潜在证明。 +它对应于没有递归的 `match` 表达式。对结构体使用 `cases` 会导致结构体被分解， +并为结构体的每个字段添加一个假设，就像模式匹配表达式提取结构体的字段以用于程序中一样。 +由于结构体只有一个构造子，因此对结构体使用 `cases` 不会产生额外的目标。 + + + +由于 `ih` 是 +`List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs` +的一个证明，使用 `cases ih` 会产生一个 `List.length (splitList xs).fst ≤ List.length xs` 的假设 +和一个 `List.length (splitList xs).snd ≤ List.length xs` 的假设: + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le3}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le3}} ``` + + +由于证明的目标也是一个 `And`，因此可以使用 `constructor` 策略应用 `And.intro`， +从而为每个参数生成一个目标： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le4}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le4}} ``` + + +`left` 目标与 `left✝` 假设非常相似，除了目标用 `Nat.succ` 包装不等式的两侧。 +同样，`right` 目标类似于 `right✝` 假设，除了目标仅将 `Nat.succ` 添加到输入列表的长度。 +现在是时候证明 `Nat.succ` 的这些包装保留了陈述的真值了。 + + +### 两边同时加一 + +对于 `left` 目标，要证明的语句是 `Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m`。 +换句话说，如果 `n ≤ m`，那么在两边都加一并不会改变这一事实。为什么这是真的？ +证明 `n ≤ m` 是一个 `Nat.le.refl` 构造子，周围有 `m - n` 个 `Nat.le.step` 构造子的实例。 +在两边都加一只是意味着 `refl` 应用于比之前大一的数，并且具有相同数量的 `step` 构造子。 + + + +更形式化地说，证明是通过归纳法来证明 `n ≤ m` 的证据。如果证据是 `refl`，则 `n = m`， +因此 `Nat.succ n = Nat.succ m`，并且可以再次使用 `refl`。 +如果证据是 `step`，则归纳假设提供了 `Nat.succ n ≤ Nat.succ m` 的证据， +并且目标是证明 `Nat.succ n ≤ Nat.succ (Nat.succ m)`。 +这可以通过将 `step` 与归纳假设一起使用来完成。 + + +在 Lean 中，该定理陈述为： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean succ_le_succ0}} ``` + + + +错误信息对其进行了概括： + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean succ_le_succ0}} ``` + + +第一步是使用 `intro` 策略，将假设 `n ≤ m` 引入作用域并为其命名： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean succ_le_succ1}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean succ_le_succ1}} ``` + + +由于证明是通过归纳法对证据 `n ≤ m` 进行的，因此下一个策略是 `induction h`： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean succ_le_succ3}} ``` + + + +这会产生两个目标，每个目标对应于 `Nat.le` 的一个构造子： + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean succ_le_succ3}} ``` + + + +`refl` 的目标可以使用 `refl` 本身来解决，`constructor` 策略会选择它。 +`step` 的目标还需要使用 `step` 构造子： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean succ_le_succ4}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean succ_le_succ4}} ``` + + + +该目标不再使用 `≤` 运算符显示，但它等价于归纳假设 `ih`。 +`assumption` 策略会自动选择一个满足目标的假设，证明完毕： + ```leantac {{#example_decl Examples/ProgramsProofs/Inequalities.lean succ_le_succ5}} ``` + + +写成递归函数，证明如下： + ```lean {{#example_decl Examples/ProgramsProofs/Inequalities.lean succ_le_succ_recursive}} ``` + + +将基于策略的归纳证明与这个递归函数进行比较是有指导意义的。哪些证明步骤对应于定义的哪些部分？ + + + +### 在较大的一侧加一 + + +证明 `splitList_shorter_le` 所需的第二个不等式是 `∀(n m : Nat), n ≤ m → n ≤ Nat.succ m`。 +这个证明几乎与 `Nat.succ_le_succ` 相同。同样，传入的假设 `n ≤ m` 基本上跟踪了 `n` 和 `m` +在 `Nat.le.step` 构造子数量上的差异。因此，证明应该在基本情况下添加一个额外的 `Nat.le.step`。 +证明可以写成： + ```leantac {{#example_decl Examples/ProgramsProofs/Inequalities.lean le_succ_of_le}} ``` + + +为了揭示幕后发生的事情，`apply` 和 `exact` 策略可用于准确指示正在应用哪个构造子。 +`apply` 策略通过应用一个返回类型匹配的函数或构造子来解决当前目标， +为每个未提供的参数创建新的目标，而如果需要任何新目标，`exact` 就会失败： + ```leantac {{#example_decl Examples/ProgramsProofs/Inequalities.lean le_succ_of_le_apply}} ``` + + +证明可以简化： + ```leantac {{#example_decl Examples/ProgramsProofs/Inequalities.lean le_succ_of_le_golf}} ``` + + +在这个简短的策略脚本中，由 `induction` 引入的两个目标都使用 +`repeat (first | constructor | assumption)` 来解决。策略 `first | T1 | T2 | ... | Tn` +表示按顺序尝试 `T1` 到 `Tn`，然后使用第一个成功的策略。 +换句话说，`repeat (first | constructor | assumption)` 会尽可能地应用构造子， +然后尝试使用假设来解决目标。 + + + +最后，证明可以写成一个递归函数： + ```lean {{#example_decl Examples/ProgramsProofs/Inequalities.lean le_succ_of_le_recursive}} ``` + + +每种证明风格都适用于不同的情况。详细的证明脚本在初学者阅读代码或证明步骤提供某种见解的情况下很有用。 +简短、高度自动化的证明脚本通常更容易维护，因为自动化通常在面对定义和数据类型的细微更改时既灵活又健壮。 +递归函数通常从数学证明的角度来看更难理解，也更难维护，但对于开始使用交互式定理证明的程序员来说， +它可能是一个有用的桥梁。 + + +### 完成证明 + + +现在已经证明了两个辅助定理，`splitList_shorter_le` 的其余部分将很快完成。 +当前的证明状态有两个目标，用于 `And` 的左侧和右侧： + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le4}} ``` + + +目标以 `And` 结构体的字段命名。这意味着 `case` 策略（不要与 `cases` 混淆）可以依次关注于每个目标： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le5a}} ``` + + + +现在不再是一个错误列出两个未解决的目标，而是有两个错误信息， +每个 `skip` 上一个。对于`left`目标，可以使用`Nat.succ_le_succ`： + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le5a}} ``` + + + +在右侧目标中，`Nat.le_suc_of_le` 适合： + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le5b}} ``` + + + +这两个定理都包含前提条件 `n ≤ m`。它们可以作为 `left✝` 和 `right✝` 假设找到， +这意味着 `assumption` 策略可以处理最终目标： + ```leantac {{#example_decl Examples/ProgramsProofs/Inequalities.lean splitList_shorter_le}} ``` + + +下一步是返回到证明归并排序停机所需的实际定理：只要一个列表至少有两个条目， +则分割它的两个结果都严格短于它。 + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean splitList_shorter_start}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_start}} ``` + + + +模式匹配在策略脚本中与在程序中一样有效。因为 `lst` 至少有两个条目， +所以它们可以用 `match` 暴露出来，它还通过依值模式匹配来细化类型： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean splitList_shorter_1}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_1}} ``` + + + +使用 `splitList` 简化会删除 `x` 和 `y`，导致列表的计算长度每个都获得 `Nat.succ`： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean splitList_shorter_2}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_2}} ``` + + + +用 `simp_arith` 替换 `simp` 会删除这些 `Nat.succ` 构造子， +因为 `simp_arith` 利用了 `n + 1 < m + 1` 意味着 `n < m` 的事实： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean splitList_shorter_2b}} ``` + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean splitList_shorter_2b}} ``` + + + +此目标现在匹配 `splitList_shorter_le`，可用于结束证明： + ```leantac {{#example_decl Examples/ProgramsProofs/Inequalities.lean splitList_shorter}} ``` + + +证明 `mergeSort` 停机所需的事实可以从结果 `And` 中提取出来： + ```leantac {{#example_decl Examples/ProgramsProofs/Inequalities.lean splitList_shorter_sides}} ``` + + +## 归并排序停机证明 + +归并排序有两个递归调用，一个用于 `splitList` 返回的每个子列表。 +每个递归调用都需要证明传递给它的列表的长度短于输入列表的长度。 +通常分两步编写停机证明会更方便：首先，写下允许 Lean 验证停机的命题，然后证明它们。 +否则，可能会投入大量精力来证明命题，却发现它们并不是所需的在更小的输入上建立递归调用的内容。 + + + +`sorry` 策略可以证明任何目标，即使是错误的目标。它不适用于生产代码或最终证明， +但它是一种便捷的方法，可以提前「勾勒出」证明或程序。任何使用 `sorry` 的定义或定理都会附有警告。 + + +使用 `sorry` 的 `mergeSort` 停机论证的初始草图可以通过将 Lean 无法证明的目标复制到 +`have` 表达式中来编写。在 Lean 中，`have` 类似于 `let`。使用 `have` 时，名称是可选的。 +通常，`let` 用于定义引用关键值的名称，而 `have` 用于局部证明命题， +当 Lean 在寻找「数组查找是否在范围内」或「函数是否停机」的证据时，可以找到这些命题。 + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean mergeSortSorry}} ``` + + + +警告位于名称 `mergeSort` 上： + ```output warning {{#example_out Examples/ProgramsProofs/Inequalities.lean mergeSortSorry}} ``` + + +因为没有错误，所以建议的命题足以建立停机证明。 + + + +证明从应用辅助定理开始： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean mergeSortNeedsGte}} ``` + + + +两个证明都失败了，因为 `splitList_shorter_fst` 和 `splitList_shorter_snd` +都需要证明 `xs.length ≥ 2`： + ```output error {{#example_out Examples/ProgramsProofs/Inequalities.lean mergeSortNeedsGte}} ``` + + + +要检查这是否足以完成证明，请使用 `sorry` 添加它并检查错误： + ```leantac {{#example_in Examples/ProgramsProofs/Inequalities.lean mergeSortGteStarted}} ``` + + + +同样，只会有一个警告。 + ```output warning {{#example_out Examples/ProgramsProofs/Inequalities.lean mergeSortGteStarted}} ``` + + +有一个有希望的假设可用：`h : ¬List.length xs < 2`，它来自 `if`。 +显然，如果不是 `xs.length < 2`，那么 `xs.length ≥ 2`。 +Lean 库以 `Nat.ge_of_not_lt` 的名称提供了此定理。程序现在已完成： + ```leantac {{#example_decl Examples/ProgramsProofs/Inequalities.lean mergeSort}} ``` + + +该函数可以在示例上进行测试： + ```lean {{#example_in Examples/ProgramsProofs/Inequalities.lean mergeSortRocks}} ``` + ```output info {{#example_out Examples/ProgramsProofs/Inequalities.lean mergeSortRocks}} ``` + ```lean {{#example_in Examples/ProgramsProofs/Inequalities.lean mergeSortNumbers}} ``` + ```output info {{#example_out Examples/ProgramsProofs/Inequalities.lean mergeSortNumbers}} ``` + + +## 用减法迭代表示除法 + +正如乘法是迭代的加法，指数是迭代的乘法，除法可以理解为迭代的减法。 +[本书中对递归函数的第一个描述](../getting-to-know/datatypes-and-patterns.md#递归函数) +给出了除法的一个版本，当除数不为零时停机，但 Lean 并不接受。证明除法终止需要使用关于不等式的事实。 + + + +第一步是细化除法的定义，使其需要证据证明除数不为零： + ```lean {{#example_in Examples/ProgramsProofs/Div.lean divTermination}} ``` + + + +由于增加了参数，错误信息会稍长一些，但它包含基本相同的信息： + ```output error {{#example_out Examples/ProgramsProofs/Div.lean divTermination}} ``` + + +`div` 的这个定义会停机，因为第一个参数 `n` 在每次递归调用时都更小。 +这可以使用 `termination_by` 子句来表示： + ```lean {{#example_in Examples/ProgramsProofs/Div.lean divRecursiveNeedsProof}} ``` + + + +现在，错误仅限于递归调用： + ```output error {{#example_out Examples/ProgramsProofs/Div.lean divRecursiveNeedsProof}} ``` + +This can be proved using a theorem from the standard library, `Nat.sub_lt`. +This theorem states that (the curly braces indicate that `n` and `k` are implicit arguments). +Using this theorem requires demonstrating that both `n` and `k` are greater than zero. +Because `k > 0` is syntactic sugar for `0 < k`, the only necessary goal is to show that `0 < n`. +There are two possibilities: either `n` is `0`, or it is `n' + 1` for some other `Nat` `n'`. +But `n` cannot be `0`. +The fact that the `if` selected the second branch means that `¬ n < k`, but if `n = 0` and `k > 0` then `n` must be less than `k`, which would be a contradiction. +This, `n = Nat.succ n'`, and `Nat.succ n'` is clearly greater than `0`. +这可以使用标准库中的定理 `Nat.sub_lt` 来证明。该定理指出 +`{{#example_out Examples/ProgramsProofs/Div.lean NatSubLt}}` +（花括号表示 `n` 和 `k` 是隐式参数）。使用此定理需要证明 `n` 和 `k` 都大于零。 +因为 `k > 0` 是 `0 < k` 的语法糖，所以唯一必要的目标是证明 `0 < n`。 +有两种可能性：`n` 为 `0`，或它为某个其他 `Nat n'` 的 `n' + 1`。 +但 `n` 不能为 `0`。`if` 选择第二个分支的事实意味着 `¬ n < k`， +但如果 `n = 0` 且 `k > 0`，则 `n` 必须小于 `k`，这将会产生矛盾。 +在这里，`n = Nat.succ n'`，而 `Nat.succ n'` 明显大于 `0`。 + + + +`div` 的完整定义，包括停机证明： + ```leantac {{#example_decl Examples/ProgramsProofs/Div.lean div}} ``` - + + +## 练习 + + +证明以下定理： + + * 对于所有的自然数 \\( n \\)，\\( 0 < n + 1 \\)。 + * 对于所有的自然数 \\( n \\)，\\( 0 \\leq n \\)。 + * 对于所有的自然数 \\( n \\) 和 \\( k \\)，\\( (n + 1) - (k + 1) = n - k \\) + * 对于所有的自然数 \\( n \\) 和 \\( k \\), 若 \\( k < n \\) 则 \\( n \neq 0 \\) + * 对于所有的自然数 \\( n \\)，\\( n - n = 0 \\) + * 对于所有的自然数 \\( n \\) 和 \\( k \\)，若 \\( n + 1 < k \\) 则 \\( n < k \\) diff --git a/functional-programming-lean/src/programs-proofs/insertion-sort.md b/functional-programming-lean/src/programs-proofs/insertion-sort.md index 062049c..bd0f9b0 100644 --- a/functional-programming-lean/src/programs-proofs/insertion-sort.md +++ b/functional-programming-lean/src/programs-proofs/insertion-sort.md @@ -1,334 +1,723 @@ + +# 插入排序与数组可变性 + + + +虽然插入排序的最差时间复杂度并不是最优，但它仍然有一些有用的属性： + + * 它简单明了，易于实现和理解 + * 它是一种原地排序算法，不需要额外的空间来运行 + * 它是一种稳定排序 + * 当输入已经排序得差不多时，它很快 + + +原地算法在 Lean 中特别有用，因为它管理内存的方式。 +在某些情况下，会复制数组的操作通常可以优化为直接修改。这包括交换数组中的元素。 + + + +大多数语言和具有自动内存管理的运行时系统，包括 JavaScript、JVM 和 .NET，都使用跟踪垃圾回收。 +当需要回收内存时，系统从许多 **根**（例如调用栈和全局值）开始， +然后通过递归地追踪指针来确定可以到达哪些值。任何无法到达的值都会被释放，从而释放内存。 + + +引用计数是追踪式垃圾回收的替代方法，它被许多语言使用，包括 Python、Swift 和 Lean。 +在引用计数系统中，内存中的每个对象都有一个字段来跟踪对它的引用数。 +当建立一个新引用时，计数器会增加。当一个引用不再存在时，计数器会减少。 +当计数器达到零时，对象会立即被释放。 + +与追踪式垃圾回收器相比，引用计数有一个主要的缺点：循环引用会导致内存泄漏。 +如果对象 \\( A \\) 引用对象 \\( B \\)，而对象 \\( B \\) 引用对象 \\( A \\)， +它们将永远不会被释放，即使程序中没有其他内容引用 \\( A \\) 或 \\( B \\)。 +循环引用要么是由不受控制的递归引起的，要么是由可变引用引起的。由于 Lean 不支持这两者， +因此不可能构造循环引用。 + + +引用计数意味着 Lean 运行时系统用于分配和释放数据结构的原语可以检查引用计数是否即将降至零， +并重新使用现有对象而非分配一个新对象。当使用大型数组时，这一点尤其重要。 + +针对 Lean 数组的插入排序的实现应满足以下条件： + + 1. Lean 应当接受没有 `partial` 标注的函数 + 2. 若传递了一个没有其他引用的数组，它应原地修改数组，而非分配一个新数组 + + + +第一个条件很容易检查：如果 Lean 接受该定义，则满足该条件。 +然而，第二个条件需要一种测试方法。Lean 提供了一个名为 `dbgTraceIfShared` 的内置函数，其签名如下： + ```lean {{#example_in Examples/ProgramsProofs/InsertionSort.lean dbgTraceIfSharedSig}} ``` + ```output info {{#example_out Examples/ProgramsProofs/InsertionSort.lean dbgTraceIfSharedSig}} ``` + + + +它以一个字符串和一个值作为参数，如果该值有多个引用，则使用该字符串打印一条消息到标准错误， +并返回该值。严格来说，它不是一个纯函数。 +但是，它仅在开发期间用于检查函数实际上能够重用内存而非分配和复制。 + + +在学习使用 `dbgTraceIfShared` 时，重要的是要知道 `#eval` 会报告的值比已编译的代码中共享的值更多， +这可能会令人困惑。重要的是使用 `lake` 构建可执行文件，而非在编辑器中进行实验。 + +插入排序由两个循环组成。外层循环将指针从左向右移动到要排序的数组中。 +每次迭代后，指针左边的数组区域都会被排序，而右边的区域可能尚未被排序。 +内层循环获取指针指向的元素，并将其向左移动，直到找到合适的位置并恢复循环不变式。 +换句话说，每次迭代都会将数组的下一个元素插入到已排序区域的合适位置。 + + + +## 内层循环 + + +插入排序的内层循环可以实现为一个尾递归函数，该函数将数组和要插入的元素的索引作为参数。 +要插入的元素会与它左边的元素反复交换，直到左边的元素更小或到达数组的开头。 +内层循环会在用来索引数组的 `Fin` 中的 `Nat` 上进行结构化递归： + ```leantac {{#example_decl Examples/ProgramsProofs/InsertionSort.lean insertSorted}} ``` + + +若索引 `i` 为 `0`，则插入到已排序区域的元素已到达该区域的开头，并且是最小的。 +若索引为 `i' + 1`，则应将 `i'` 处的元素与 `i` 处的元素进行比较。 +请注意，虽然 `i` 是 `Fin arr.size`，但 `i'` 只是一个 `Nat`，因为它是由 `i` 的 `val` 字段产生的。 +因此，在使用 `i'` 对 `arr` 进行索引之前，有必要证明 `i' < arr.size`。 + + + +省略带有证明 `i' < arr.size` 的 `have` 表达式，将显示以下目标： + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insertSortedNoProof}} ``` + + +提示 `Nat.lt_of_succ_lt` 是 Lean 标准库中的一个定理。 +它的签名可以通过 `#check Nat.lt_of_succ_lt` 查看： + ```output info {{#example_out Examples/ProgramsProofs/InsertionSort.lean lt_of_succ_lt_type}} ``` + + + +换句话说，它指出如果 `n + 1 < m`，则 `n < m`。传递给 `simp` 的 `*` 会使其将 +`Nat.lt_of_succ_lt` 与 `i` 中的 `isLt` 字段结合起来以获得最终证明。 -Having established that `i'` can be used to look up the element to the left of the element being inserted, the two elements are looked up and compared. + + +在确定 `i'` 可用于查找要插入元素左侧的元素后，就要查找并比较这两个元素。 +若左侧元素小于或等于要插入的元素，则循环结束并且不变量被恢复。 +若左侧元素大于要插入的元素，则交换元素并重新开始内层循环。 +`Array.swap` 将其两个索引都作为 `Fin`，并且利用 `have` 建立 `i' < arr.size` 的 `by assumption`。 +在内层循环的下一轮中要检查的索引也是 `i'`，但在这种情况下 `by assumption` 并足够。 +这是因为该证明是针对原始数组 `arr` 编写的，而非交换两个元素的结果。 +`simp` 策略的数据库包含这样一个事实：交换数组的两个元素不会改变其大小， +并且 `[*]` 参数会指示它额外使用 `have` 引入的假设。 + + + +## 外层循环 + + +插入排序的外层循环将指针从左向右移动，在每次迭代中调用 `insertSorted` +将指针处的元素插入到数组中正确的位置。循环的基本形式类似于 `Array.map` 的实现： + ```lean {{#example_in Examples/ProgramsProofs/InsertionSort.lean insertionSortLoopTermination}} ``` + + + +它产生的错误也与在 `Array.map` 上没有 `termination_by` 子句时发生的错误相同， +因为没有在每次递归调用时都会减少的参数： + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insertionSortLoopTermination}} ``` + + +在构建停机证明之前，可以使用 `partial` 修饰符测试定义以确保它返回预期的答案： + ```lean {{#example_decl Examples/ProgramsProofs/InsertionSort.lean partialInsertionSortLoop}} ``` + ```lean {{#example_in Examples/ProgramsProofs/InsertionSort.lean insertionSortPartialOne}} ``` + ```output info {{#example_out Examples/ProgramsProofs/InsertionSort.lean insertionSortPartialOne}} ``` + ```lean {{#example_in Examples/ProgramsProofs/InsertionSort.lean insertionSortPartialTwo}} ``` + ```output info {{#example_out Examples/ProgramsProofs/InsertionSort.lean insertionSortPartialTwo}} ``` + + +### 停机性 + + +同样，该函数会停机是因为正在处理的索引和数组大小之差在每次递归调用时都会减小。 +然而，这一次，Lean 不接受 `termination_by`： + ```lean {{#example_in Examples/ProgramsProofs/InsertionSort.lean insertionSortLoopProof1}} ``` + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insertionSortLoopProof1}} ``` + + + +问题在于 Lean 无法知道 `insertSorted` 返回的数组与传递给它的数组大小相同。 +为了证明 `insertionSortLoop` 会停机，首先有必要证明 `insertSorted` 不会改变数组的大小。 +将未经证明的停机条件从错误消息复制到函数中，并使用 `sorry`「证明」它，可以暂时接受该函数： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insertionSortLoopSorry}} ``` + ```output warning {{#example_out Examples/ProgramsProofs/InsertionSort.lean insertionSortLoopSorry}} ``` + + +由于 `insertSorted` 在要插入的元素的索引上是结构化递归的，所以应该通过索引归纳进行证明。 +在基本情况下，数组返回不变，因此其长度肯定不会改变。对于归纳步骤， +归纳假设是在下一个更小的索引上的递归调用不会改变数组的长度。 +这里有两种情况需要考虑：要么元素已完全插入到已排序区域中，并且数组返回不变， +在这种情况下长度也不会改变，要么元素在递归调用之前与下一个元素交换。 +然而，在数组中交换两个元素不会改变它的大小， +并且归纳假设指出以下一个索引的递归调用返回的数组与其参数大小相同。因此，大小仍然保持不变。 + + +将自然语言的定理陈述翻译为 Lean，并使用本章中的技术进行操作，足以证明基本情况并在归纳步骤中取得进展： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_0}} ``` + + + +在归纳步骤中使用 `insertSorted` 的简化揭示了 `insertSorted` 中的模式匹配： + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_0}} ``` + + + +当面对包含 `if` 或 `match` 的目标时，`split` 策略（不要与归并排序定义中使用的 `split` 函数混淆） +会用一个新目标替换原目标，用于控制流的每条路径： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_1}} ``` + + + +此外，每个新目标都有一个假设，表明哪个分支导致了该目标，在本例中命名为 `heq✝`： + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_1}} ``` + + + +与其为这两个简单情况编写证明，不如在 `split` 后添加 `<;> try rfl`， +这样这两个直接的情况会立即消失，只留下一个目标： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_2}} ``` + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_2}} ``` + +不幸的是，归纳假设不足以证明这个目标。归纳假设指出对 `arr` 调用 `insertSorted` 不会改变大小， +但证明目标是要证明用交换的结果来进行递归调用的结果不会改变大小。成功完成证明需要一个归纳假设， +该假设适用于传递给 `insertSorted` 的任何数组，以及作为参数的更小的索引。 + + + +可以使用 `induction` 策略的 `generalizing` 选项来获得强归纳假设。 +此选项会将语境中的附加假设引入到一个语句中，该语句用于生成基本情况、归纳假设和在归纳步骤中显示的目标。 +对 `arr` 进行推广会产生更强的假设： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_3}} ``` + + + +在生成的证明目标中，`arr` 现在是归纳假设中「对于所有」语句的一部分： + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_3}} ``` + + +然而，整个证明开始变得难以控制。下一步是引入一个变量表示交换结果的长度， +证明它等于 `arr.size`，然后证明这个变量也等于递归调用产生的数组的长度。 +之后可以将这些相等语句链接在一起来证明目标。 +然而，仔细地重新表述定理的陈述要容易得多，这样归纳假设就能自动变得足够强，变量也会被引入。 +重新表述的陈述如下： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_0}} ``` + + + +这个版本的定理陈述更容易证明，原因有以下几个： + 1. 与其将索引及其有效性证明捆绑在 `Fin` 中，不如将索引放在数组之前。 + 这使得归纳假设可以自然地推广到整个数组，并证明 `i` 在范围内。 + 2. 引入了一个抽象长度 `len` 来表示 `array.size`。证明自动化通常更擅长处理显式相等性陈述。 + + + +生成的证明状态显示了将要用于生成归纳假设的语句，以及基本情况和归纳步骤的目标： + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_0}} ``` + + +将该语句与 `induction` 策略产生的目标进行比较： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_1a}} ``` + + + +在基本情况下，每个 `i` 的出现都会被替换为 `0`。使用 `intro` 引入每个假设， +然后使用 `insertSorted` 简化就能证明目标，因为在索引 `zero` 处的 `insertSorted` 会返回其参数不变： + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_1a}} ``` + + + +在归纳步骤中，归纳假设具有恰当的强度。它对 **任何** 数组都适用，只要该数组的长度为 `len`： + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_1b}} ``` + + +在基本情况下，`simp` 将目标简化为 `arr.size = len`： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_2}} ``` + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_2}} ``` + + + +这可以使用假设 `hLen` 来证明。向 `simp` 添加 `*` 参数指示它额外使用假设，这解决了目标： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_2b}} ``` + + +在归纳步骤中，引入假设并简化目标会再次产生包含模式匹配的目标： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_3}} ``` + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_3}} ``` + + + +使用 `split` 策略会为每个模式生成一个目标。同样，前两个目标来自没有递归调用的分支，因此不需要归纳假设： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_4}} ``` + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_4}} ``` + + + +在 `split` 产生的每个目标中运行 `try assumption` 会消除两个非递归目标： + ```leantac {{#example_in Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_5}} ``` + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_5}} ``` + + +对于证明目标的全新表述，其中常量 `len` 用于递归函数中涉及的所有数组的长度， +恰好属于 `simp` 可以解决的问题类型。最终的证明目标可以通过 `simp [*]` 来解决， +因为将数组的长度与 `len` 联系起来的假设很重要： + ```leantac {{#example_decl Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo_6}} ``` + + +最后，因为 `simp [*]` 可以使用假设，所以 `try assumption` 一行可以用 `simp [*]` 替换来缩短证明： + ```leantac {{#example_decl Examples/ProgramsProofs/InsertionSort.lean insert_sorted_size_eq_redo}} ``` + + +现在可以使用这个证明来替换 `insertionSortLoop` 中的 `sorry`。 +将 `arr.size` 作为定理的 `len` 参数会导致最终结论为 `(insertSorted arr ⟨i, isLt⟩).size = arr.size`， +因此重写以一个非常易于管理的证明目标结束： + ```leantacnorfl {{#example_in Examples/ProgramsProofs/InsertionSort.lean insertionSortLoopRw}} ``` + ```output error {{#example_out Examples/ProgramsProofs/InsertionSort.lean insertionSortLoopRw}} ``` + + + +证明 `{{#example_in Examples/ProgramsProofs/InsertionSort.lean sub_succ_lt_self_type}}` +是 Lean 标准库的一部分，其类型为 +`{{#example_out Examples/ProgramsProofs/InsertionSort.lean sub_succ_lt_self_type}}` +它刚好就是我们所需要的： + ```leantacnorfl {{#example_decl Examples/ProgramsProofs/InsertionSort.lean insertionSortLoop}} ``` - + +## 驱动函数 + + + +插入排序本身会调用 `insertionSortLoop`，以将数组中已排序区域与未排序区域的分界索引初始化为 `0`： + ```lean {{#example_decl Examples/ProgramsProofs/InsertionSort.lean insertionSort}} ``` + + +一些快速测试表明该函数至少不是明显错误的： + ```lean {{#example_in Examples/ProgramsProofs/InsertionSort.lean insertionSortNums}} ``` + ```output info {{#example_out Examples/ProgramsProofs/InsertionSort.lean insertionSortNums}} ``` + ```lean {{#example_in Examples/ProgramsProofs/InsertionSort.lean insertionSortStrings}} ``` + ```output info {{#example_out Examples/ProgramsProofs/InsertionSort.lean insertionSortStrings}} ``` + +## 它真的是插入排序吗？ + + + +插入排序被 **定义** 为原地排序算法。尽管它具有二次最差运行时间，但它仍然有用， +因为它是一种稳定的排序算法，不会分配额外的空间，并且可以有效处理几乎已排序的数据。 +如果内层循环的每次迭代都分配一个新数组，那么该算法就不会真正成为插入排序。 + +Lean 的数组操作（例如 `Array.set` 和 `Array.swap`）会检查所讨论的数组的引用计数是否大于 1。 +如果是，则该数组对代码的多个部分可见，这意味着它必须被复制。 +否则，Lean 将不再是一种纯函数式语言。但是，当引用计数恰好为 1 时，没有其他潜在的值观察者。 +在这种情况下，数组原语会就地改变数组。程序其他不知道的部分不会对它造成破坏。 + + + +Lean 的证明逻辑在纯函数式程序的级别上，而非在底层实现上工作。 +这意味着发现程序是否不必要地复制了数据的最好方法是测试它。 +在需要改变的每个点添加对 `dbgTraceIfShared` 的调用，当所讨论的值有多个引用时， +它会将提供的消息打印到 `stderr`。 + + +插入排序刚好有一个地方有复制而非改变的风险：调用 `Array.swap`。将 `arr.swap ⟨i', by assumption⟩ i` +替换为 `((dbgTraceIfShared "array to swap" arr).swap ⟨i', by assumption⟩ i)` +会让程序在无法改变数组时发出 `shared RC array to swap`。然而，对程序的这一更改也会更改证明， +因为现在调用了一个附加函数。由于 `dbgTraceIfShared` 直接返回其第二个参数， +因此将其添加到对 `simp` 的调用中足以修复证明。 + + +插入排序的完整形式化验证代码为： + ```leantacnorfl {{#include ../../../examples/Examples/ProgramsProofs/InstrumentedInsertionSort.lean:InstrumentedInsertionSort}} ``` + +要检查形式化验证是否实际起作用，需要一点技巧。首先，当所有参数在编译时都已知时， +Lean 编译器会积极地优化函数调用。仅仅编写一个将 `insertionSort` 应用于大数组的程序是不够的， +因为生成的编译代码可能只包含已排序的数组作为常量。确保编译器不会优化排序例程的最简单方法是从 +`stdin` 读取数组。其次，编译器会执行死代码消除。如果从未使用 `let` 绑定的变量， +则向程序中添加额外的 `let` 并不一定会导致运行代码中更多的引用。为了确保不会完全消除额外的引用， +重点在于确保以某种方式使用了额外的引用。 + + + +测试形式化验证代码的第一步是编写 `getLines`，它从标准输入读取一行数组： + ```lean {{#include ../../../examples/Examples/ProgramsProofs/InstrumentedInsertionSort.lean:getLines}} ``` + + +`IO.FS.Stream.getLine` 返回一行完整的文本，包括结尾的换行。当到达文件结尾标记时，它返回空字符串 `""`。 + + + +接下来，需要两个单独的 `main` 例程。两者都从标准输入读取要排序的数组， +确保在编译时不会用它们的返回值替换对 `insertionSort` 的调用。然后两者都打印到控制台， +确保对 `insertionSort` 的调用不会被完全优化掉。其中一个只打印排序后的数组， +而另一个同时打印排序后的数组和原始数组。第二个函数应该触发一个警告， +即 `Array.swap` 必须分配一个新数组： + ```lean {{#include ../../../examples/Examples/ProgramsProofs/InstrumentedInsertionSort.lean:mains}} ``` + + +实际的 `main` 只需根据提供的命令行参数选择两个 main 活动二者之一： + ```lean {{#include ../../../examples/Examples/ProgramsProofs/InstrumentedInsertionSort.lean:main}} ``` + + +在没有参数的情况下运行它会产生预期的用法信息： + ``` $ {{#command {sort-demo} {sort-sharing} {./run-usage} {sort}}} {{#command_out {sort-sharing} {./run-usage} }} ``` + + +`test-data` 文件包含以下岩石： + ``` {{#file_contents {sort-sharing} {sort-demo/test-data}}} ``` + + +对这些岩石使用形式化验证的插入排序，结果按字母顺序打印出来： + ``` $ {{#command {sort-demo} {sort-sharing} {sort --unique < test-data}}} {{#command_out {sort-sharing} {sort --unique < test-data} }} ``` + + +然而，保留对原始数组的引用的版本会导致对 `Array.swap` 的第一次调用在 `stderr` +上发出通知（即 `shared RC array to swap`）： + ``` $ {{#command {sort-demo} {sort-sharing} {sort --shared < test-data}}} {{#command_out {sort-sharing} {sort --shared < test-data} }} ``` + + +仅出现一个 `shared RC` 通知这一事实意味着数组仅被复制了一次。 +这是因为由对 `Array.swap` 的调用产生的副本本身是唯一的，因此不需要进行进一步的复制。 +在命令式语言中，由于忘记在按引用传递数组之前显式复制数组，可能会导致微妙的 Bug。 +在运行 `sort --shared` 时，数组会安需复制，以保持 Lean 程序的纯函数语义，但仅此而已。 + + +## 其他可变性的机会 + +当引用唯一时，使用修改而非复制并不仅限于数组更新操作。 +Lean 还会尝试「回收」引用计数即将降至零的构造函数，重新使用它们而不是分配新数据。 +这意味着，例如，`List.map` 将原地修改链表，至少在无人能注意到的情况下。 +优化 Lean 代码中的热循环最重要的步骤之一是确保被修改的数据不会被从多个位置引用。 + + + +## 练习 + + + * 编写一个反转数组的函数。测试如果输入数组的引用计数为一，则你的函数不会分配一个新数组。 + + -* Implement either merge sort or quicksort for arrays. Prove that your implementation terminates, and test that it doesn't allocate more arrays than expected. This is a challenging exercise! - - + * 为数组实现归并排序或快速排序。证明你的实现会停机，并测试它不会分配比预期更多的数组。 + 这是一个具有挑战性的练习！ diff --git a/functional-programming-lean/src/programs-proofs/special-types.md b/functional-programming-lean/src/programs-proofs/special-types.md index f3ec654..fd14196 100644 --- a/functional-programming-lean/src/programs-proofs/special-types.md +++ b/functional-programming-lean/src/programs-proofs/special-types.md @@ -1,18 +1,40 @@ + +# 特殊类型 + + + +理解数据在内存中的表示非常重要。通常，可以从数据类型的定义中理解它的表示。 +每个构造子对应于内存中的一个对象，该对象有一个包含标记和引用计数的头。 +构造子的参数分别由指向其他对象的指针表示。换句话说，`List` 实际上是一个链表， +从 `structure` 中提取一个字段实际上只是跟随一个指针。 + + +然而，这个规则有一些重要的例外。编译器对许多类型进行了特殊处理。 +例如，类型 `UInt32` 被定义为 `Fin (2 ^ 32)`，但在运行时它会被替换为基于机器字的实际原生实现。 +类似地，尽管 `Nat` 的定义暗示了一个类似于 `List Unit` 的实现， +但实际的运行时表示会对足够小的数字使用立即（immediate）机器字， +对较大的数字则使用高效的任意精度算术库。Lean 编译器会将使用模式匹配的定义转换为与其表示对应的适当操作， +并且对加法和减法等操作的调用会被映射到底层算术库中的快速操作。 +毕竟，加法不应该花费与加数大小成线性的时间。 + +由于某些类型具有特殊表示，因此在使用它们时需要小心。 +这些类型中的大多数由编译器特殊处理的 `structure` 组成。对于这些结构体， +直接使用构造子或字段访问器可能会触发从高效表示到方便证明的低效表示的昂贵转换。 +例如，`String` 被定义为包含字符列表的结构体，但字符串的运行时表示使用了 UTF-8， +而非指向字符的指针链表。将构造子应用于字符列表会创建一个以 UTF-8 编码它们的字节数组， +而访问结构体的字段需要线性时间来解码 UTF-8 的表示并分配一个链表。数组的表示方式类似。 +从逻辑角度来看，数组是包含数组元素列表的结构体，但运行时表示则是一个动态大小的数组。 +在运行时，构造子会将列表转换为数组，而字段访问器则会在数组中分配一个链表。 +编译器用高效的版本替换了各种数组操作，这些版本在可能的情况下会改变数组，而非分配一个新的数组。 + + + +类型本身和命题的证明都会从编译后的代码中完全擦除。换句话说，它们不会占用任何空间， +证明过程中可能执行的任何计算也同样会被擦除， +这意味着证明可以利用字符串和数组作为归纳定义列表的简便接口，包括使用归纳法来证明它们， +而不会在程序运行时施加缓慢的转换步骤。对于这些内置类型，数据的简便逻辑表示并不意味着程序一定会很慢。 + +如果一个结构体类型只有一个非类型，非证明的字段，那么构造子自身会在运行时消失， +并被替换为其单个参数。换句话说，其子类型与其底层类型完全相同，不会带有额外的间接层。 +同样，`Fin` 在内存中只是 `Nat`，并且可以创建单字段结构体来跟踪 `Nat` 或 `String` 的不同用法， +而无需支付性能损失。如果一个构造子没有非类型，非证明的参数，那么该构造子也会消失， +并被一个常量值替换，否则指针将用于该常量值。这意味着 `true`、`false` 和 `none` 是常量值， +而非指向堆分配对象的指针。 + +以下类型拥有特殊的表示： + + + +| 类型 | 逻辑表示 | 运行时表示 | +|------|----------|------------| +| `Nat` | 一元类型，每个 `Nat.succ` 都有一个指针 | 高效的任意精度整数 | +| `Int` | 和类型，带有表示正负值的构造子，每个包含一个 `Nat` | 高效的任意精度整数 | +| `UInt8`、`UInt16`、`UInt32`、`UInt64` | 带有合适边界的 `Fin` | 固定精度的机器整数 | +| `Char` | `UInt32` 以及与之配对的它是有效码位的证明 | 一般字符 | +| `String` | 在名为 `data` 的字段中包含 `List Char` 的结构体 | UTF-8 编码的字符串 | +| `Array α` | 在名为 `data` 的字段中包含 `List α` 的结构体 | 指向 `α` 值的指针打包的数组 | +| `Sort u` | 一个类型 | 完全擦除 | +| 命题的证明 | 当命题被视为证据类型时，命题所暗示的任何数据 | 完全擦除 | + + +## 练习 + +[`Pos` 的 定义](../type-classes/pos.html) 并没有利用 Lean 将 `Nat` 编译成高效类型的优势。 +在运行时，它本质上是一个链表。或者，可以定义一个子类型，允许在内部使用 Lean 的快速 `Nat` 类型， +如 [子类型的开头部分](../functor-applicative-monad/applicative.md#subtypes) 中所述。 +在运行时，证明将被擦除。由于结果结构体只有一个数据字段，因此它会表示为该字段， +这意味着 `Pos` 的这种新表示与 `Nat` 的表示相同。 + + + +在证明定理 `∀ {n k : Nat}, n ≠ 0 → k ≠ 0 → n + k ≠ 0` 之后，为 `Pos` 这种新的表示定义 +`ToString` 和 `Add` 的实例。然后，定义 `Mul` 的实例，在此过程中证明任何必要的定理。 diff --git a/functional-programming-lean/src/programs-proofs/summary.md b/functional-programming-lean/src/programs-proofs/summary.md index 8d44d1d..627a159 100644 --- a/functional-programming-lean/src/programs-proofs/summary.md +++ b/functional-programming-lean/src/programs-proofs/summary.md @@ -1,94 +1,243 @@ + +# 总结 + + + +## 尾递归 + +尾递归是一种递归，其中递归调用的结果会立即返回，而非以其他方式使用。 +这些递归调用称为「尾调用」。尾调用很有趣，因为它们可以编译成跳转指令而非调用指令， +并且可以重新使用当前栈帧，而非压入新的一帧。换句话说，尾递归函数实际上就是循环。 + + + +使递归函数更快的常用方法是使用累加器传递风格对其进行重写。 +它不使用调用栈来记住如何处理递归调用的结果，而是使用一个名为「累加器」的附加参数来收集此信息。 +例如，用于反转列表的尾递归函数的累加器按相反顺序包含已经处理过的列表项。 + +在 Lean 中，只有自尾调用（self-tail-call）会被优化为循环。 +换句话说，两个以互相尾调用结束的函数不会被优化。 + + + +## 引用计数与原地更新 + + +与 Java、C# 和大多数 JavaScript 实现中那样使用跟踪垃圾收集器不同， +Lean 使用引用计数进行内存管理。这意味着内存中的每个值都包含一个字段， +该字段跟踪引用它的其他值的数量，并且运行时系统在引用出现或消失时维护这些计数。 +引用计数也用在了 Python、PHP 和 Swift 中。 + +当要求分配一个新对象时，Lean 的运行时系统能够回收引用计数降为零的现有对象。 +此外，如果数组的引用计数为一，则数组操作（如 `Array.set` 和 `Array.swap`）将修改原数组， +而非分配一个修改后的副本。如果 `Array.swap` 持有对数组的唯一引用， +那么程序的其他部分就无法分辨它是被改变了还是被复制了。 + + + +在 Lean 中编写高效的代码需要使用尾递归，并小心确保大数组被唯一使用。 +虽然可以通过检查函数的定义来识别尾调用，但了解一个值是否被唯一引用可能需要阅读整个程序。 +调试辅助函数 `dbgTraceIfShared` 可以用在程序的关键位置来检查一个值是否被共享。 + + +## 证明程序的正确性 + +以累加器传递样式重写程序，或进行其他使程序运行更快的转换，也可能会让程序更难理解。 +保留程序的原始版本（正确性更加明显）是有用的，然后将其用作优化版本的可执行规范。 +虽然单元测试等技术在 Lean 中与在任何其他语言中一样有效， +但 Lean 还允许使用数学证明来完全确保函数的两个版本对 **所有** 可能的输入返回相同的结果。 + + + +通常，证明两个函数相等是使用函数外延性（`funext` 策略）完成的， +即如果两个函数对每个输入返回相同的值，则它们相等。如果函数是递归的， +那么归纳法通常是证明其输出相同的好方法。通常，函数的递归定义将对一个特定参数进行递归调用； +这个参数是归纳的一个好选择。在某些情况下，归纳假设不够充分。 +解决这个问题通常需要考虑如何构建定理陈述的更通用版本，以提供足够充分的归纳假设。 +特别是，为了证明一个函数等价于一个累加器传递版本， +需要一个将任意初始累加器值与原始函数的最终结果联系起来的定理陈述。 + + +## 安全的数组索引 + +类型 `Fin n` 表示严格小于 `n` 的自然数。`Fin` 是「有限」的缩写。 +与子类型一样，`Fin n` 是一个包含 `Nat` 和证明这个 `Nat` 小于 `n` 的结构体。 +不存在类型为 `Fin 0` 的值。 + + + +如果 `arr` 是一个 `Array α`，那么 `Fin arr.size` 总是包含一个适合作为 `arr` 索引的数字。 +许多内置数组运算符（例如 `Array.swap`）会将 `Fin` 值作为参数，而非独立的证明对象。 + + +Lean 为 `Fin` 提供了大多数有用的数字类型类的实例。`Fin` 的 `OfNat` 实例会执行模运算， +而非在提供的数字大于 `Fin` 可接受的数字时在编译时失败。 + +## 临时性证明 + + + +有时，当某个陈述实际上尚未被证明，而假装它已被证明是有用的。 +这在确保一个陈述的证明是否适用于某些任务时很有用，例如在另一个证明中重写、 +确定数组访问是否安全、或显示递归调用是在比原始参数更小的值上进行的。 +花时间证明某件事，却发现其他一些证明更有用，这是非常令人沮丧的。 + + +`sorry` 策略使 Lean 临时接受一个陈述，就好像它是真正的证明一样。 +它可以看作类似于在 C# 中抛出 `NotImplementedException` 的桩（stub）方法。 +任何依赖于 `sorry` 的证明都会在 Lean 中包含一个警告。 + +小心！`sorry` 策略可以证明 **任何** 陈述，甚至是错误的陈述。 +证明 `3 < 2` 可能会导致数组越界访问持续到运行时，意外地使程序崩溃。 +在开发过程中使用 `sorry` 很方便，但将其保留在代码中很危险。 + + + +## 停机证明 + + +当一个递归函数不使用结构体递归时，Lean 无法自动确定它是否停机。 +在这些情况下，该函数可以用 `partial` 标记为偏函数。但是，也可以提供证明函数停机的证明。 + +偏函数有一个关键的缺点：它们不能在类型检查或证明中展开。 +这意味着 Lean 作为交互式定理证明器的价值不能应用于它们。 +此外，证明一个预期停机的函数实际上总是停机，可以消除更多潜在的 bug 来源。 + + + +递归函数末尾允许的 `termination_by` 子句可用于指定递归函数停机的原因。 +该子句将函数的参数映射到一个表达式，该表达式预期在每次递归调用时都会变小。 +可能减小的表达式的示例包括不断增长的数组索引与数组大小之间的差、 +每次递归调用时减半的列表长度，或一对列表，其中恰好一个在每次递归调用时都会缩小。 + + +Lean 包含的证明自动化可以自动确定某些表达式在每次调用时都会缩小，但许多有趣的程序需要手动证明。 +这些证明可以使用 `have` 提供，`have` 是 `let` 的一个版本，旨在局部提供证明而非值。 + + +编写递归函数的一个好方法是从声明它们为 `partial` 开始，并通过测试调试它们， +直到它们返回正确的答案。然后，可以删除 `partial` 并用 `termination_by` 子句替换它。 +Lean 会在需要证明的每个递归调用上放置错误高亮，其中包含需要证明的语句。 +每个这样的语句都可以放在 `have` 中，证明为 `sorry`。 +如果 Lean 接受该程序并且它仍然通过测试，最后一步就是实际证明使 Lean 接受它的定理。 +这种方法可以防止浪费时间来证明一个有缺陷的程序的停机性。 diff --git a/functional-programming-lean/src/type-classes/coercion.md b/functional-programming-lean/src/type-classes/coercion.md index 42fb732..66f81fb 100644 --- a/functional-programming-lean/src/type-classes/coercion.md +++ b/functional-programming-lean/src/type-classes/coercion.md @@ -343,7 +343,7 @@ Rather than have two kinds of `if` expression, the Lean standard library defines --> 另一个有用的 `CoeSort` 使用场景是它可以让 `Bool` 和 `Prop` 建立联系。 -就像在[有序性和等价性那一节](standard-classes.md#equality-and-ordering)我们提到的，Lean 的 `if` 表达式需要条件为一个可判定的命题而不是一个 `Bool`。 +就像在[有序性和等价性那一节](./standard-classes#相等性与有序性)我们提到的，Lean 的 `if` 表达式需要条件为一个可判定的命题而不是一个 `Bool`。 然而，程序通常需要能够根据布尔值进行分支。 Lean 标准库并没有定义两种 `if` 表达式，而是定义了一种从 `Bool` 到命题的强制转换，即该 `Bool` 值等于 `true`： ```lean diff --git a/functional-programming-lean/src/type-classes/out-params.md b/functional-programming-lean/src/type-classes/out-params.md index a01b8ba..0b9cf29 100644 --- a/functional-programming-lean/src/type-classes/out-params.md +++ b/functional-programming-lean/src/type-classes/out-params.md @@ -35,7 +35,7 @@ The `HAdd` class takes three type parameters: the two argument types and the ret Instances of `HAdd Nat Pos Pos` and `HAdd Pos Nat Pos` allow ordinary addition notation to be used to mix the types: --> -就像在[重载加法](pos.md#overloaded-addition)那一节提到的，Lean 提供了名为 `HAdd` 的类型类来重载异质加法。 +就像在[重载加法](./pos#重载加法)一节提到的，Lean 提供了名为 `HAdd` 的类型类来重载异质加法。 `HAdd` 类接受三个类型参数：两个参数的类型和一个返回类型。 `HAdd Nat Pos Pos` 和 `HAdd Pos Nat Pos` 的实例可以让常规加法符号可以接受不同类型。 diff --git a/functional-programming-lean/src/type-classes/polymorphism.md b/functional-programming-lean/src/type-classes/polymorphism.md index 6f6a1d7..fcb398e 100644 --- a/functional-programming-lean/src/type-classes/polymorphism.md +++ b/functional-programming-lean/src/type-classes/polymorphism.md @@ -277,7 +277,7 @@ Write an instance of `OfNat` for the even number datatype from the [previous sec For the base instance, it is necessary to write `OfNat Even Nat.zero` instead of `OfNat Even 0`. --> -为[上一节的练习题](pos.md#even-numbers)中的偶数数据类型写一个使用递归实例搜索的 `OfNat` 实例。 +为[上一节的练习题](pos#偶数)中的偶数数据类型写一个使用递归实例搜索的 `OfNat` 实例。 对于基本实例，有必要编写 `OfNat Even Nat.zero` 而不是 `OfNat Even 0`。 -## 重载加法运算符 +## 重载加法