From f6a076dd77d046b491f944a053cd15650233ee35 Mon Sep 17 00:00:00 2001 From: subfish-zhou Date: Fri, 21 Jun 2024 23:38:46 +0200 Subject: [PATCH] update induction_and_reduction --- induction_and_recursion.md | 594 ++++++++++++++++++++++++++++++++++++- inductive_types.md | 34 +-- introduction.md | 4 +- structures_and_records.md | 8 +- 4 files changed, 615 insertions(+), 25 deletions(-) diff --git a/induction_and_recursion.md b/induction_and_recursion.md index 22b3ec5..d657208 100644 --- a/induction_and_recursion.md +++ b/induction_and_recursion.md @@ -1,6 +1,12 @@ + +归纳和递归 +======================= + + + +在上一章中，我们看到归纳定义提供了在 Lean 中引入新类型的强大手段。此外，构造器和递归器提供了在这些类型上定义函数的唯一手段。命题即类型的对应关系，意味着归纳法是证明的基本方法。 + +Lean 提供了定义递归函数、执行模式匹配和编写归纳证明的自然方法。它允许你通过指定它应该满足的方程来定义一个函数，它允许你通过指定如何处理可能出现的各种情况来证明一个定理。在它内部，这些描述被「方程编译器」程序「编译」成原始递归器。方程编译器不是可信代码库的一部分；它的输出包括由内核独立检查的项。 + +模式匹配 +---------------- + + + +对示意图模式的解释是编译过程的第一步。我们已经看到，`casesOn` 递归器可以通过分情况讨论来定义函数和证明定理，根据归纳定义类型所涉及的构造器。但是复杂的定义可能会使用几个嵌套的 ``casesOn`` 应用，而且可能很难阅读和理解。模式匹配提供了一种更方便的方法，并且为函数式编程语言的用户所熟悉。 + +考虑一下自然数的归纳定义类型。每个自然数要么是 ``zero``，要么是 ``succ x``，因此你可以通过在每个情况下指定一个值来定义一个从自然数到任意类型的函数： ```lean open Nat @@ -46,7 +68,11 @@ def isZero : Nat → Bool | succ x => false ``` + + +用来定义这些函数的方程在定义上是成立的： ```lean # open Nat @@ -66,7 +92,11 @@ example : sub1 7 = 6 := rfl example (x : Nat) : isZero (x + 3) = false := rfl ``` + + +我们可以用一些更耳熟能详的符号，而不是 ``zero`` 和 ``succ``： ```lean def sub1 : Nat → Nat @@ -78,12 +108,18 @@ def isZero : Nat → Bool | x+1 => false ``` + + +因为加法和零符号已经被赋予 `[matchPattern]` 属性，它们可以被用于模式匹配。Lean 简单地将这些表达式规范化，直到显示构造器 ``zero`` 和 ``succ``。 + +模式匹配适用于任何归纳类型，如乘积和 Option 类型： ```lean def swap : α × β → β × α @@ -97,8 +133,12 @@ def bar : Option Nat → Nat | none => 0 ``` + + +在这里，我们不仅用它来定义一个函数，而且还用它来进行逐情况证明： ```lean # namespace Hidden @@ -112,7 +152,11 @@ theorem not_not : ∀ (b : Bool), not (not b) = b # end Hidden ``` + + +模式匹配也可以用来解构归纳定义的命题： ```lean example (p q : Prop) : p ∧ q → q ∧ p @@ -123,11 +167,17 @@ example (p q : Prop) : p ∨ q → q ∨ p | Or.inr hq => Or.inl hq ``` + + +这样解决带逻辑连接词的命题就很紧凑。 + +在所有这些例子中，模式匹配被用来进行单一情况的区分。更有趣的是，模式可以涉及嵌套的构造器，如下面的例子。 ```lean def sub2 : Nat → Nat @@ -136,6 +186,7 @@ def sub2 : Nat → Nat | x+2 => x ``` + + +方程编译器首先对输入是 ``zero`` 还是 ``succ x`` 的形式进行分类讨论，然后对 `x` 是 ``zero`` 还是 ``succ x`` 的形式进行分类讨论。它从提交给它的模式中确定必要的情况拆分，如果模式不能穷尽情况，则会引发错误。同时，我们可以使用算术符号，如下面的版本。在任何一种情况下，定义方程都是成立的。 ```lean # def sub2 : Nat → Nat @@ -156,11 +210,15 @@ example : sub2 (x+2) = x := rfl example : sub2 5 = 3 := rfl ``` + + +你可以写 ``#print sub2`` 来看看这个函数是如何被编译成递归器的。（Lean 会告诉你 `sub2` 已经被定义为内部辅助函数 `sub2.match_1`，但你也可以把它打印出来）。Lean 使用这些辅助函数来编译 `match` 表达式。实际上，上面的定义被扩展为 ```lean def sub2 : Nat → Nat := @@ -171,7 +229,11 @@ def sub2 : Nat → Nat := | x+2 => x ``` + + +下面是一些嵌套模式匹配的例子： ```lean example (p q : α → Prop) @@ -185,9 +247,13 @@ def foo : Nat × Nat → Nat | (m+1, n+1) => 2 ``` + + +方程编译器可以按顺序处理多个参数。例如，将前面的例子定义为两个参数的函数会更自然： ```lean def foo : Nat → Nat → Nat @@ -196,7 +262,11 @@ def foo : Nat → Nat → Nat | m+1, n+1 => 2 ``` + + +另一例： ```lean def bar : List Nat → List Nat → Nat @@ -206,11 +276,17 @@ def bar : List Nat → List Nat → Nat | a :: as, b :: bs => a + b ``` + + +这些模式是由逗号分隔的。 + +在下面的每个例子中，尽管其他参数包括在模式列表中，但只对第一个参数进行了分割。 ```lean # namespace Hidden @@ -228,6 +304,7 @@ def cond : Bool → α → α → α # end Hidden ``` + + +还要注意的是，当定义中不需要一个参数的值时，你可以用下划线来代替。这个下划线被称为**通配符模式**，或**匿名变量**。与方程编译器之外的用法不同，这里的下划线并**不**表示一个隐参数。使用下划线表示通配符在函数式编程语言中是很常见的，所以 Lean 采用了这种符号。[通配符和重叠模式](#通配符和重叠模式)一节阐述了通配符的概念，而[不可访问模式](#不可访问模式)一节解释了你如何在模式中使用隐参数。 + +正如[归纳类型](./inductive_types.md)一章中所描述的，归纳数据类型可以依赖于参数。下面的例子使用模式匹配定义了 ``tail`` 函数。参数 ``α : Type`` 是一个参数，出现在冒号之前，表示它不参与模式匹配。Lean 也允许参数出现在 ``:`` 之后，但它不能对其进行模式匹配。 ```lean def tail1 {α : Type u} : List α → List α @@ -254,6 +336,7 @@ def tail2 : {α : Type u} → List α → List α | α, a :: as => as ``` + + +尽管参数 ``α`` 在这两个例子中的位置不同，但在这两种情况下，它的处理方式是一样的，即它不参与情况分割。 + +Lean也可以处理更复杂的模式匹配形式，其中从属类型的参数对各种情况构成了额外的约束。这种**依值模式匹配**的例子在[依值模式匹配](#依值模式匹配)一节中考虑。 + + + +通配符和重叠模式 +---------------------------------- + + +考虑上节的一个例子： ```lean def foo : Nat → Nat → Nat @@ -275,7 +373,11 @@ def foo : Nat → Nat → Nat | m+1, n+1 => 2 ``` + + +也可以表述成 ```lean def foo : Nat → Nat → Nat @@ -284,11 +386,15 @@ def foo : Nat → Nat → Nat | m, n => 2 ``` + + +在第二种表述中，模式是重叠的；例如，一对参数 ``0 0`` 符合所有三种情况。但是Lean通过使用第一个适用的方程来处理这种模糊性，所以在这个例子中，最终结果是一样的。特别是，以下方程在定义上是成立的： ```lean # def foo : Nat → Nat → Nat @@ -301,7 +407,11 @@ example : foo (m+1) 0 = 1 := rfl example : foo (m+1) (n+1) = 2 := rfl ``` + + +由于不需要``m``和``n``的值，我们也可以用通配符模式代替。 ```lean def foo : Nat → Nat → Nat @@ -310,6 +420,7 @@ def foo : Nat → Nat → Nat | _, _ => 2 ``` + +你可以检查这个 ``foo`` 的定义是否满足与之前相同的定义特性。 + +一些函数式编程语言支持**不完整的模式**。在这些语言中，解释器对不完整的情况产生一个异常或返回一个任意的值。我们可以使用 ``Inhabited`` （含元素的）类型类来模拟任意值的方法。粗略的说，``Inhabited α`` 的一个元素是对 ``α`` 拥有一个元素的见证；在[类型类](./type_classes.md)中，我们将看到 Lean 可以被告知合适的基础类型是含元素的，并且可以自动推断出其他构造类型是含元素的。在此基础上，标准库提供了一个任意元素``arbitrary``，任何含元素的类型。 + +我们还可以使用类型`Option α`来模拟不完整的模式。我们的想法是对所提供的模式返回`some a`，而对不完整的情况使用`none`。下面的例子演示了这两种方法。 + + + +```lean +def f1 : Nat → Nat → Nat + | 0, _ => 1 + | _, 0 => 2 + | _, _ => default -- 不完整的模式 + +example : f1 0 0 = 1 := rfl +example : f1 0 (a+1) = 1 := rfl +example : f1 (a+1) 0 = 2 := rfl +example : f1 (a+1) (b+1) = default := rfl + +def f2 : Nat → Nat → Option Nat + | 0, _ => some 1 + | _, 0 => some 2 + | _, _ => none -- 不完整的模式 + example : f2 0 0 = some 1 := rfl example : f2 0 (a+1) = some 1 := rfl example : f2 (a+1) 0 = some 2 := rfl example : f2 (a+1) (b+1) = none := rfl ``` + + +方程编译器是很智能的。如果你遗漏了以下定义中的任何一种情况，错误信息会告诉你遗漏了哪个。 ```lean def bar : Nat → List Nat → Bool → Nat @@ -366,7 +512,11 @@ def bar : Nat → List Nat → Bool → Nat | a+1, b :: _, _ => a + b ``` + + +某些情况也可以用「if ... then ... else」代替 ``casesOn``。 ```lean def foo : Char → Nat @@ -377,9 +527,15 @@ def foo : Char → Nat #print foo.match_1 ``` + + +结构化递归和归纳 +---------------------------------- + + +方程编译器的强大之处在于，它还支持递归定义。在接下来的三节中，我们将分别介绍。 + +- 结构性递归定义 +- 良基的递归定义 +- 相互递归的定义 + +一般来说，方程编译器处理以下形式的输入。 + ``` def foo (a : α) : (b : β) → γ | [patterns₁] => t₁ @@ -397,6 +563,7 @@ def foo (a : α) : (b : β) → γ | [patternsₙ] => tₙ ``` + + +这里 `(a : α)` 是一个参数序列，`(b : β)` 是进行模式匹配的参数序列，`γ` 是任何类型，它可以取决于 `a` 和 `b `。每一行应该包含相同数量的模式，对应于 `β` 的每个元素。正如我们所看到的，模式要么是一个变量，要么是应用于其他模式的构造器，要么是一个正规化为该形式的表达式（其中非构造器用 ``[matchPattern]`` 属性标记）。构造器的出现会提示情况拆分，构造器的参数由给定的变量表示。在[依值模式匹配](#依值模式匹配)一节中，我们将看到有时有必要在模式中包含明确的项，这些项需要进行表达式类型检查，尽管它们在模式匹配中没有起到作用。由于这个原因，这些被称为「不可访问的模式」。但是在[依值模式匹配](#依值模式匹配)一节之前，我们将不需要使用这种不可访问的模式。 + +正如我们在上一节所看到的，项 `t₁,...,tₙ` 可以利用任何一个参数 `a`，以及在相应模式中引入的任何一个变量。使得递归和归纳成为可能的是，它们也可以涉及对 ``foo`` 的递归调用。在本节中，我们将处理**结构性递归**，其中 `foo` 的参数出现在 `:=` 的右侧，是左侧模式的子项。我们的想法是，它们在结构上更小，因此在归纳类型中出现在更早的阶段。下面是上一章的一些结构递归的例子，现在用方程编译器来定义。 ```lean open Nat @@ -442,6 +614,7 @@ def mul : Nat → Nat → Nat | n, zero => zero | n, succ m => add (mul n m) n ``` + + +``zero_add`` 的证明清楚地表明，归纳证明实际上是 Lean 中的一种递归形式。 + +上面的例子表明，``add``的定义方程具有定义意义，`` mul``也是如此。方程编译器试图确保在任何可能的情况下都是这样，就像直接的结构归纳法一样。然而，在其他情况下，约简只在命题上成立，也就是说，它们是必须明确应用的方程定理。方程编译器在内部生成这样的定理。用户不能直接使用它们;相反，``simp``策略被配置为在必要时使用它们。因此，对`zero_add`的以下两种证明都成立： ```lean open Nat @@ -467,11 +645,15 @@ theorem zero_add : ∀ n, add zero n = n | succ n => by simp [add, zero_add] ``` + + +与模式匹配定义一样，结构递归或归纳的参数可能出现在冒号之前。在处理定义之前，简单地将这些参数添加到本地上下文中。例如，加法的定义也可以写成这样: ```lean open Nat @@ -480,7 +662,11 @@ def add (m : Nat) : Nat → Nat | succ n => succ (add m n) ``` + + +你也可以用 ``match`` 来写上面的例子。 ```lean open Nat @@ -490,7 +676,11 @@ def add (m n : Nat) : Nat := | succ n => succ (add m n) ``` + + +一个更有趣的结构递归的例子是斐波那契函数 ``fib``。 ```lean def fib : Nat → Nat @@ -505,12 +695,16 @@ example : fib (n + 2) = fib (n + 1) + fib n := rfl example : fib 7 = 21 := rfl ``` + + +这里，``fib`` 函数在 ``n + 2`` （定义上等于 ``succ (succ n)`` ）处的值是根据 ``n + 1`` （定义上等价于 ``succ n`` ）和 ``n`` 处的值定义的。然而，这是一种众所周知的计算斐波那契函数的低效方法，其执行时间是 ``n`` 的指数级。这里有一个更好的方法: ```lean def fibFast (n : Nat) : Nat := @@ -523,7 +717,12 @@ where #eval fibFast 100 ``` + + +下面是相同的定义，使用 ``let rec`` 代替 ``where``。 + ```lean def fibFast (n : Nat) : Nat := @@ -533,6 +732,7 @@ def fibFast (n : Nat) : Nat := (loop n).2 ``` + + +在这两种情况下，Lean都会生成辅助函数 ``fibFast.loop``。 + +为了处理结构递归，方程编译器使用**值过程**（course-of-values）递归，使用由每个归纳定义类型自动生成的常量 `below` 和 `brecOn`。你可以通过查看 ``Nat.below`` 和 ``Nat.brecOn`` 的类型来了解它是如何工作的。 ```lean variable (C : Nat → Type u) @@ -551,6 +756,7 @@ variable (C : Nat → Type u) #check (@Nat.brecOn C : (n : Nat) → ((n : Nat) → @Nat.below C n → C n) → C n) ``` + + +类型 ``@Nat.below C (3 : nat)`` 是一个存储着 ``C 0``，``C 1``，和 ``C 2`` 中元素的数据结构。值过程递归由 ``Nat.brecOn`` 实现。它根据该函数之前的所有值，定义类型为 ``(n : Nat) → C n`` 的依值函数在特定输入 ``n`` 时的值，表示为 ``@Nat.below C n`` 的一个元素。 + +值过程递归是方程编译器用来向 Lean 内核证明函数终止的技术之一。它不会像其他函数式编程语言编译器一样影响编译递归函数的代码生成器。回想一下，`#eval fib ` 是 `` 的指数。另一方面，`#reduce fib ` 是有效的，因为它使用了发送到内核的基于 `brecOn` 结构的定义。 + +```lean +def fib : Nat → Nat + | 0 => 1 + | 1 => 1 + | n+2 => fib (n+1) + fib n + +-- #eval fib 50 -- 这个很慢 +#reduce fib 50 -- 用这个，这个快 + +#print fib +``` + + + +另一个递归定义的好例子是列表的 ``append`` 函数。 ```lean def append : List α → List α → List α @@ -584,7 +813,11 @@ def append : List α → List α → List α example : append [1, 2, 3] [4, 5] = [1, 2, 3, 4, 5] := rfl ``` + + +这里是另一个：它将第一个列表中的元素和第二个列表中的元素分别相加，直到两个列表中的一个用尽。 ```lean def listAdd [Add α] : List α → List α → List α @@ -596,12 +829,25 @@ def listAdd [Add α] : List α → List α → List α -- [5, 7, 9] ``` + + +你可以在章末练习中尝试类似的例子。 + + +局域递归声明 +--------- + + +可以使用``let rec``关键字定义局域递归声明。 ```lean def replicate (n : Nat) (a : α) : List α := @@ -614,6 +860,7 @@ def replicate (n : Nat) (a : α) : List α := -- {α : Type} → α → Nat → List α → List α ``` + + +Lean为每个 ``let rec`` 创建一个辅助声明。在上面的例子中，它对于出现在 ``replicate`` 的 ``let rec loop`` 创建了声明 ``replication.loop``。请注意，Lean 通过添加 ``let rec`` 声明中出现的任何局部变量作为附加参数来「关闭」声明。例如，局部变量 ``a`` 出现在 ``let rec`` 循环中。 + +你也可以在策略证明模式中使用 ``let rec``，并通过归纳来创建证明。 ```lean # def replicate (n : Nat) (a : α) : List α := @@ -637,8 +889,12 @@ theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by exact aux n [] ``` + + +还可以在定义后使用 ``where`` 子句引入辅助递归声明。Lean将它们转换为 ``let rec``。 ```lean def replicate (n : Nat) (a : α) : List α := @@ -658,9 +914,15 @@ where | n+1 => simp [replicate.loop, aux n, Nat.add_succ, Nat.succ_add] ``` + +良基递归和归纳 +------------------------------------ + + + +当不能使用结构递归时，我们可以使用良基递归（well-founded recursion）来证明终止性。我们需要一个良基关系和一个证明每个递归调用相对于该关系都是递减的证明。依值类型理论具有足够的表达能力来编码和证明良基递归。让我们从理解其工作原理所需的逻辑背景开始。 + +Lean 的标准库定义了两个谓词，``Acc r a`` 和 ``WellFounded r``，其中 ``r`` 是一个在类型 ``α`` 上的二元关系，而 ``a`` 是类型 ``α`` 的一个元素。 ```lean variable (α : Sort u) @@ -679,6 +946,7 @@ variable (r : α → α → Prop) #check (WellFounded r : Prop) ``` + + +首先 ``Acc`` 是一个归纳定义的谓词。根据定义，``Acc r x`` 等价于 +``∀ y, r y x → Acc r y``。如果你把 ``r y x`` 考虑成一种序关系 ``y ≺ x``，那么 ``Acc r x`` 说明 ``x`` 在下文中可访问， +从某种意义上说，它的所有前继都是可访问的。特别地，如果 ``x`` 没有前继，它是可访问的。给定任何类型 ``α``，我们应该能够通过首先为 ``α`` 的所有前继元素赋值，递归地为 ``α`` 的每个可访问元素赋值。 + +使用 ``WellFounded r`` 来声明 ``r`` 是良基的，即说明该类型的每个元素都是可访问的。根据上述考虑，如果 ``r`` 是类型 ``α`` 上的一个成立良好的关系，那么对于关系 ``r``，我们应该有一个关于 ``α`` 的成立良好的递归原则。确实，我们这样做了：标准库定义了 ``WellFounded.fix``，它正好满足这个目的。 ```lean noncomputable def f {α : Sort u} @@ -705,6 +980,7 @@ noncomputable def f {α : Sort u} : (x : α) → C x := WellFounded.fix h F ``` + + +这里有一大堆字，但我们熟悉第一块：类型 ``α``，关系 ``r``和假设 ``h``，即 ``r`` 是有良基的。变量' ``C`` 代表递归定义的动机：对于每个元素 ``x : α``，我们想构造一个 ``C x`` 的元素。函数 ``F`` 提供了这样做的归纳方法：它告诉我们如何构造一个元素 ``C x``，给定 ``C y`` 的元素对于 ``x`` 的每个 ``y``。 + +注意 ``WellFounded.fix`` 和归纳法原理一样有效。它说如果 ``≺`` 是良基的，而你想要证明 ``∀ x, C x``，那么只要证明对于任意的 ``x``，如果我们有 ``∀ y ≺ x, C y``，那么我们就有 ``C x`` 就足够了。 + +在上面的例子中，我们使用了修饰符 `noncomputable`，因为代码生成器目前不支持 `WellFounded.fix`。函数 `WellFounded.fix` 是 Lean 用来证明函数终止的另一个工具。 + +Lean 知道自然数上通常的序 ``<`` 是良基的。它还知道许多从其他东西中构造新的良基的序的方法，例如字典序。 + +下面是标准库中自然数除法的定义。 ```lean open Nat @@ -747,6 +1034,7 @@ noncomputable def div := WellFounded.fix (measure id).wf div.F #reduce div 8 2 -- 4 ``` + + +这个定义有点难以理解。这里递归在 ``x``上， ``div.F x f : Nat → Nat`` 为固定的 ``x`` 返回「除以 ``y``」函数。你要记住 ``div.F`` 的第二个参数 ``f`` 是递归的具体实现，这个函数对所有小于 ``x`` 的自然数 ``x₁`` 返回「除以 ``y``」函数。 + +繁饰器（Elaborator）可以使这样的定义更加方便。它接受下列内容: ```lean def div (x y : Nat) : Nat := @@ -766,6 +1059,7 @@ def div (x y : Nat) : Nat := 0 ``` + + +当 Lean 遇到递归定义时，它首先尝试结构递归，失败时才返回到良基递归。Lean 使用 `decreasing_tactic` 来显示递归应用会越来越小。上面例子中的辅助命题 `x - y < x` 应该被视为这种策略的提示。 + +``div`` 的定义公式不具有定义性，但我们可以使用 `unfold` 策略展开 ``div``。我们使用 [`conv`](./conv.md) 来选择要展开的 ``div`` 应用。 + + +```lean +# def div (x y : Nat) : Nat := +# if h : 0 < y ∧ y ≤ x then +# have : x - y < x := Nat.sub_lt (Nat.lt_of_lt_of_le h.1 h.2) h.1 +# div (x - y) y + 1 +# else +# 0 +example (x y : Nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := by + conv => lhs; unfold div -- 展开方程左侧的div + example (x y : Nat) (h : 0 < y ∧ y ≤ x) : div x y = div (x - y) y + 1 := by conv => lhs; unfold div simp [h] ``` + + +下面的示例与此类似：它将任何自然数转换为二进制表达式，表示为0和1的列表。我们必须提供递归调用正在递减的证据，我们在这里用 ``sorry`` 来做。``sorry`` 并不会阻止解释器成功地对函数求值。 ```lean def natToBin : Nat → List Nat @@ -809,12 +1129,16 @@ def natToBin : Nat → List Nat #eval natToBin 1234567 ``` + + +最后一个例子，我们观察到Ackermann函数可以直接定义，因为它可以被自然数上字典序的良基性证明。`termination_by` 子句指示 Lean 使用字典序。这个子句实际上是将函数参数映射到类型为 `Nat × Nat` 的元素。然后，Lean 使用类型类解析来合成类型为 `WellFoundedRelation (Nat × Nat)` 的元素。 ```lean def ack : Nat → Nat → Nat @@ -824,16 +1148,24 @@ def ack : Nat → Nat → Nat termination_by x y => (x, y) ``` + + +注意，在上面的例子中使用了字典序，因为实例 `WellFoundedRelation (α × β)` 使用了字典序。Lean还定义了实例 ```lean instance (priority := low) [SizeOf α] : WellFoundedRelation α := sizeOfWFRel ``` + + +在下面的例子中，我们通过显示 `as.size - i` 在递归应用中是递减的来证明它会终止。 ```lean def takeWhile (p : α → Bool) (as : Array α) : Array α := @@ -851,9 +1183,15 @@ where termination_by as.size - i ``` + + +注意，辅助函数 `go` 在这个例子中是递归的，但 `takeWhile` 不是。 + +默认情况下，Lean 使用 `decreasing_tactic` 来证明递归应用正在递减。修饰词 `decreasing_by` 允许我们提供自己的策略。这里有一个例子。 ```lean theorem div_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x := @@ -867,8 +1205,13 @@ def div (x y : Nat) : Nat := decreasing_by apply div_lemma; assumption ``` + + +注意 `decreasing_by` 不是 `termination_by` 的替代，它们是互补的。 `termination_by` 用于指定一个良基关系， `decreasing_by` 用于提供我们自己的策略来显示递归应用正在递减。在下面的示例中，我们将同时使用它们。 + + +```lean +def ack : Nat → Nat → Nat + | 0, y => y+1 + | x+1, 0 => ack x 1 + | x+1, y+1 => ack x (ack (x+1) y) +termination_by x y => (x, y) +decreasing_by + all_goals simp_wf -- 展开良基的递归辅助定义 + · apply Prod.Lex.left; simp_arith + · apply Prod.Lex.right; simp_arith + · apply Prod.Lex.left; simp_arith +``` + + + +我们可以使用 `decreasing_by sorry` 来指示 Lean 「相信」函数可以终止。 ```lean def natToBin : Nat → List Nat @@ -894,8 +1256,13 @@ decreasing_by sorry #eval natToBin 1234567 ``` + + +回想一下，使用 `sorry` 相当于使用一个新的公理，应该避免使用。在下面的例子中，我们用 `sorry` 来证明 `False`。命令 `#print axioms` 显示，`unsound` 依赖于用于实现 `sorry` 的不健全公理 `sorryAx`。 + + +```lean +def unsound (x : Nat) : False := + unsound (x + 1) +decreasing_by sorry + +#check unsound 0 +-- `unsound 0` 是 `False` 的一个证明 + +#print axioms unsound +-- 'unsound' 依赖于公理：[sorryAx] +``` + + +总结： + +- 如果没有 `termination_by`，良基关系（可能）可以这样被导出：选择一个参数，然后使用类型类解析为该参数的类型合成一个良基关系。 + +- 如果指定了 `termination_by`，它将函数的参数映射为类型 `α`，并再次使用类型类解析。 回想一下，`β × γ` 的默认实例是基于 `β` 和 `γ`的良基关系的字典序。 +- +- `Nat` 的默认良基关系实例是 `<`。 +- 默认情况下，策略 `decreasing_tactic` 用于显示递归应用小于选择的良基关系。如果 `decreasing_tactic` 失败，错误信息包括剩余目标 `... |- G`。注意，`decreasing_tactic` 使用 `assumption`。所以，你可以用 `have` 表达式来证明目标 `G`。你也可以使用 `decreasing_by` 来提供你自己的策略。 + + + +相互递归 ---------------- + + +Lean 还提供相互递归定义，语法类似相互归纳类型。例子： ```lean mutual @@ -946,9 +1346,9 @@ theorem even_eq_not_odd : ∀ a, even a = not (odd a) := by . simp [even, odd, *] ``` -What makes this a mutual definition is that ``even`` is defined recursively in terms of ``odd``, while ``odd`` is defined recursively in terms of ``even``. Under the hood, this is compiled as a single recursive definition. The internally defined function takes, as argument, an element of a sum type, either an input to ``even``, or an input to ``odd``. It then returns an output appropriate to the input. To define that function, Lean uses a suitable well-founded measure. The internals are meant to be hidden from users; the canonical way to make use of such definitions is to use ``simp`` (or `unfold`), as we did above. +这是一个相互的定义，因为 ``even`` 是用 ``odd`` 递归定义的，而 ``odd`` 是用 ``even`` 递归定义的。在底层，它被编译为单个递归定义。内部定义的函数接受sum类型的元素作为参数，可以是 ``even`` 的输入，也可以是 ``odd`` 的输入。然后，它返回与输入相适应的输出。为了定义这个功能，Lean 使用了一个合适的、良基的度量。内部是对用户隐藏的；使用这些定义的规范方法是使用 ``simp`` （或 `unfold`），正如我们上面所做的那样。 -Mutual recursive definitions also provide natural ways of working with mutual and nested inductive types. Recall the definition of ``Even`` and ``Odd`` as mutual inductive predicates as presented before. +相互递归定义还提供了处理相互和嵌套归纳类型的自然方法。回想一下前面提到的 ``Even`` 和 ``Odd`` 作为相互归纳谓词的定义。 ```lean mutual @@ -961,7 +1361,11 @@ mutual end ``` + + +构造器``even_zero``、``even_succ`` 和 ``odd_succ`` 提供了显示数字是偶数还是奇数的积极方法。我们需要利用归纳类型是由这些构造器生成的这一事实来知道零不是奇数，并且后两个含义是相反的。像往常一样，构造器保存在以定义的类型命名的命名空间中，并且命令 ``open Even Odd`` 允许我们更方便地访问它们。 ```lean # mutual @@ -983,7 +1387,11 @@ theorem odd_of_even_succ : ∀ n, Even (n + 1) → Odd n | _, even_succ n h => h ``` + + +另一个例子，假设我们使用嵌套归纳类型来归纳定义一组项，这样，项要么是常量(由字符串给出名称)，要么是将常量应用于常量列表的结果。 ```lean inductive Term where @@ -991,7 +1399,11 @@ inductive Term where | app : String → List Term → Term ``` + + +然后，我们可以使用一个相互递归的定义来计算在一个项中出现的常量的数量，以及在一个项列表中出现的常量的数量。 ```lean # inductive Term where @@ -1016,7 +1428,11 @@ def sample := app "f" [app "g" [const "x"], const "y"] end Term ``` + + +作为最后一个例子，我们定义了一个函数 `replaceConst a b e`，它将项 `e` 中的常数 `a` 替换为 `b`，然后证明常数的数量是相同的。注意，我们的证明使用了相互递归（即归纳法）。 ```lean # inductive Term where @@ -1058,9 +1474,15 @@ mutual end ``` + +依值模式匹配 +-------------------------- + + + +我们在[模式匹配](#模式匹配)一节中考虑的所有模式匹配示例都可以很容易地使用 ``casesOn`` 和 ``recOn`` 来编写。然而，对于索引归纳族，如 ``Vector α n``，通常不是这种情况，因为区分情况要对索引的值施加约束。如果没有方程编译器，我们将需要大量的样板代码来定义非常简单的函数，例如使用递归定义 ``map``、``zip`` 和 ``unzip``。为了理解其中的困难，考虑一下如何定义一个函数 ``tail``，它接受一个向量 ``v : Vector α (succ n)`` 并删除第一个元素。首先想到的可能是使用 ``casesOn`` 函数: ```lean inductive Vector (α : Type u) : Nat → Type u @@ -1093,11 +1518,17 @@ namespace Vector end Vector ``` + + +但是在 ``nil`` 的情况下我们应该返回什么值呢？有趣的事情来了：如果 ``v`` 具有 ``Vector α (succ n)`` 类型，它「不能」为nil，但很难告诉 ``casesOn``。 + +一种解决方案是定义一个辅助函数: ```lean # inductive Vector (α : Type u) : Nat → Type u @@ -1116,6 +1547,7 @@ def tail (v : Vector α (n+1)) : Vector α n := # end Vector ``` + + +在 ``nil`` 的情况下，``m`` 被实例化为 ``0``，``noConfusion`` 利用了 ``0 = succ n`` 不能出现的事实。否则，``v`` 的形式为 ``a :: w``，我们可以简单地将 ``w``从长度 ``m`` 的向量转换为长度 ``n``的向量后返回 ``w``。 + +定义 ``tail`` 的困难在于维持索引之间的关系。 ``tailAux`` 中的假设 ``e : m = n + 1`` 用于传达 ``n`` 与与小前提相关的索引之间的关系。此外，``zero = n + 1`` 的情况是不可达的，而放弃这种情况的规范方法是使用 ``noConfusion``。 + +然而，``tail`` 函数很容易使用递归方程来定义，并且方程编译器会自动为我们生成所有样板代码。下面是一些类似的例子: ```lean # inductive Vector (α : Type u) : Nat → Type u @@ -1156,9 +1595,13 @@ def zip : {n : Nat} → Vector α n → Vector β n → Vector (α × β) n # end Vector ``` + + +注意，对于「不可达」的情况，例如 ``head nil``，我们可以省略递归方程。为索引族自动生成的定义远非直截了当。例如: ```lean # inductive Vector (α : Type u) : Nat → Type u @@ -1174,13 +1617,23 @@ def map (f : α → β → γ) : {n : Nat} → Vector α n → Vector β n → V # end Vector ``` + + +与 ``tail`` 函数相比，``map`` 函数手工定义更加繁琐。我们鼓励您尝试使用 ``recOn``、``casesOn`` 和 ``noConfusion``。 + + +不可访问模式 +------------------ + + +有时候，依值匹配模式中的参数对定义来说并不是必需的，但是必须包含它来适当地确定表达式的类型。Lean 允许用户将这些子项标记为「不可访问」以进行模式匹配。例如，当左侧出现的项既不是变量也不是构造器应用时，这些注解是必不可少的，因为它们不适合用于模式匹配的目标。我们可以将这种不可访问的模式视为模式的「不关心」组件。你可以通过写 ``.(t)`` 来声明子项不可访问。如果不可访问的模式可以被推断出来，你也可以写 ``_``。 + +下面的例子中，我们声明了一个归纳类型，它定义了「在 ``f`` 的像中」的属性。您可以将 ``ImageOf f b`` 类型的元素视为 ``b`` 位于 ``f`` 的像中的证据，构造器``imf`` 用于构建此类证据。然后，我们可以定义任何函数 ``f`` 的「逆」，逆函数将 ``f`` 的像中的任何元素赋给映射到它的元素。类型规则迫使我们为第一个参数写 ``f a``，但是这个项既不是变量也不是构造器应用，并且在模式匹配定义中没有作用。为了定义下面的函数 ``inverse``，我们必须将 ``f a`` 标记为不可访问。 ```lean inductive ImageOf {α β : Type u} (f : α → β) : β → Type u where @@ -1218,6 +1676,7 @@ def inverse' {f : α → β} : (b : β) → ImageOf f b → α | _, imf a => a ``` + + +在上面的例子中，不可访问记号清楚地表明 ``f`` 不是一个模式匹配变量。 + +不可访问模式可用于澄清和控制使用依值模式匹配的定义。考虑函数 ``Vector.add`` 的以下定义，假设该类型有满足结合律的加法函数，它将一个类型的两个元素向量相加: ```lean inductive Vector (α : Type u) : Nat → Type u @@ -1241,6 +1705,7 @@ def add [Add α] : {n : Nat} → Vector α n → Vector α n → Vector α n end Vector ``` + + +参数 ``{n : Nat}`` 出现在冒号之后，因为它不能在整个定义中保持固定。在实现这个定义时，方程编译器首先区分第一个参数是 ``0`` 还是 ``n+1``。对接下来的两个参数嵌套地区分情况，在每种情况下，方程编译器都会排除与第一个模式不兼容的情况。 + +但事实上，在第一个参数上不需要区分情况；当我们对第二个参数区分情况时，``Vector`` 的 ``casesOn`` 消去器会自动抽象该参数，并将其替换为 ``0`` 和 ``n + 1``。使用不可访问的模式，我们可以提示方程编译器不要在 ``n`` 上区分情况。 ```lean # inductive Vector (α : Type u) : Nat → Type u @@ -1266,6 +1736,7 @@ def add [Add α] : {n : Nat} → Vector α n → Vector α n → Vector α n # end Vector ``` + + +将位置标记为不可访问模式首先告诉方程编译器，参数的形式应该从其他参数所构成的约束中推断出来，其次，第一个参数不应该参与模式匹配。 + +为简便起见，不可访问的模式 `.(_)` 可以写成 `_`。 ```lean # inductive Vector (α : Type u) : Nat → Type u @@ -1285,12 +1761,16 @@ def add [Add α] : {n : Nat} → Vector α n → Vector α n → Vector α n # end Vector ``` + + +如前所述，参数 ``{n : Nat}`` 是模式匹配的一部分，因为它不能在整个定义中保持固定。在以前的 Lean 版本中，用户经常发现必须包含这些额外的判别符是很麻烦的。因此，Lean 4 实现了一个新特性，**判别精炼**（discriminant refinement），它自动为我们包含了这些额外的判别。 ```lean # inductive Vector (α : Type u) : Nat → Type u @@ -1303,8 +1783,12 @@ def add [Add α] {n : Nat} : Vector α n → Vector α n → Vector α n # end Vector ``` + + +当与「自动绑定隐式」特性结合使用时，你可以进一步简化声明并这样写： ```lean # inductive Vector (α : Type u) : Nat → Type u @@ -1317,8 +1801,12 @@ def add [Add α] : Vector α n → Vector α n → Vector α n # end Vector ``` + + +使用这些新特性，您可以更紧凑地编写在前几节中定义的其他向量函数，如下所示: ```lean # inductive Vector (α : Type u) : Nat → Type u @@ -1344,11 +1832,20 @@ def zip : Vector α n → Vector β n → Vector (α × β) n # end Vector ``` + +Match 表达式 +----------------- + + + +Lean 还提供「match-with」表达式，它在很多函数式语言中都能找到。 ```lean def isNotZero (m : Nat) : Bool := @@ -1357,9 +1854,13 @@ def isNotZero (m : Nat) : Bool := | n+1 => true ``` + + +这看起来与普通的模式匹配定义没有太大的不同，但关键是 ``match`` 可以在表达式中的任何地方使用，并带有任意参数。 ```lean def isNotZero (m : Nat) : Bool := @@ -1377,7 +1878,11 @@ def filter (p : α → Bool) : List α → List α example : filter isNotZero [1, 0, 0, 3, 0] = [1, 3] := rfl ``` + + +另一例： ```lean def foo (n : Nat) (b c : Bool) := @@ -1392,8 +1897,12 @@ def foo (n : Nat) (b c : Bool) := example : foo 7 true false = 9 := rfl ``` + + +Lean 使用内建的 ``match`` 来实现系统所有地方的模式匹配。因此，这四种定义具有相同的净效果。 ```lean def bar₁ : Nat × Nat → Nat @@ -1410,7 +1919,11 @@ def bar₄ (p : Nat × Nat) : Nat := let (m, n) := p; m + n ``` + + +这些变体在解构命题中也是同样有用的： ```lean variable (p q : Nat → Prop) @@ -1433,10 +1946,19 @@ example (h₀ : ∃ x, p x) (h₁ : ∃ y, q y) ⟨x, y, px, qy⟩ ``` + +局域递归声明 +--------- + + + +可以通过 `let rec` 关键字定义局域递归声明。 ```lean def replicate (n : Nat) (a : α) : List α := @@ -1449,6 +1971,7 @@ def replicate (n : Nat) (a : α) : List α := -- {α : Type} → α → Nat → List α → List α ``` + + +Lean 对每个 `let rec`创建一个辅助声明。上例中，它为出现在 `replicate` 中的 `let rec loop` 创建了一个声明 `replicate.loop`。注意到，Lean 通过添加任意的出现在 `let rec` 声明中的局域变量作为附加参数来「关闭」声明。例如，局域变量 `a` 出现在 `let rec loop` 当中。 + +也在策略模式中可使用 `let rec` 来建立归纳证明。 ```lean # def replicate (n : Nat) (a : α) : List α := @@ -1472,8 +2000,12 @@ theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by exact aux n [] ``` + + +也可以用 `where` 语句在定义后面引入辅助递归声明，Lean 自动把它们转译成 `let rec`。 ```lean def replicate (n : Nat) (a : α) : List α := @@ -1493,9 +2025,15 @@ where | n+1 => simp [replicate.loop, aux n, Nat.add_succ, Nat.succ_add] ``` + + +练习 +--------- + + +1. 打开命名空间 ``Hidden`` 以避免命名冲突，并使用方程编译器定义自然数的加法、乘法和幂运算。然后用方程编译器派生出它们的一些基本属性。 + +2. 类似地，使用方程编译器定义列表上的一些基本操作(如 ``reverse`` 函数)，并通过归纳法证明关于列表的定理（例如对于任何列表 ``xs``，``reverse (reverse xs) = xs`` ）。 + +3. 定义您自己的函数来对自然数执行值的过程递归。同样，看看你是否能弄清楚如何定义 ``WellFounded.fix``。 + +4. 按照[依值模式匹配](#依值模式匹配)中的例子，定义一个追加（append）两个向量的函数。提示：你必须定义一个辅助函数。 + +5. 考虑以下类型的算术表达式。这个想法是，``var n`` 是一个变量 ``vₙ``，``const n`` 是一个常量，它的值是 ``n``。 ```lean inductive Expr where @@ -1532,10 +2081,17 @@ def sampleExpr : Expr := plus (times (var 0) (const 7)) (times (const 2) (var 1)) ``` + + +此处 ``sampleExpr`` 表示 ``(v₀ * 7) + (2 * v₁)``。 + +写一个函数来计算这些表达式，对每个``var n``赋值``v n``. + + +```lean +# inductive Expr where +# | const : Nat → Expr +# | var : Nat → Expr +# | plus : Expr → Expr → Expr +# | times : Expr → Expr → Expr +# deriving Repr +# open Expr +# def sampleExpr : Expr := +# plus (times (var 0) (const 7)) (times (const 2) (var 1)) +def eval (v : Nat → Nat) : Expr → Nat + | const n => sorry + | var n => v n + | plus e₁ e₂ => sorry + | times e₁ e₂ => sorry + +def sampleVal : Nat → Nat + | 0 => 5 + | 1 => 6 + | _ => 0 + +-- 如果答案是47说明你写的对。 +-- #eval eval sampleVal sampleExpr +``` + + +实现「常数融合」，这是一个将 ``5 + 7`` 等子术语化简为 ``12`` 的过程。使用辅助函数 ``simpConst``，定义一个函数「fuse」:为了化简加号或乘号，首先递归地化简参数，然后应用 ``simpConst`` 尝试化简结果。 ```lean # inductive Expr where @@ -1596,4 +2182,8 @@ theorem fuse_eq (v : Nat → Nat) sorry ``` + + +最后两个定理表明，定义保持值不变。 diff --git a/inductive_types.md b/inductive_types.md index 1cc0854..27e6d85 100644 --- a/inductive_types.md +++ b/inductive_types.md @@ -77,11 +77,11 @@ elaborate and complex examples. 我们的直觉是，每个构造器都指定了一种建立新的对象``Foo``的方法，可能是由以前构造的值构成。``Foo``类型只不过是由以这种方式构建的对象组成。归纳式声明中的第一个字符也可以用逗号而不是``|``来分隔构造器。 -我们将在下面看到，构造器的参数可以包括``Foo``类型的对象，但要遵守一定的“正向性”约束，即保证``Foo``的元素是自下而上构建的。粗略地说，每个`...`可以是由``Foo``和以前定义的类型构建的任何箭头类型，其中``Foo``如果出现，也只是作为依值箭头类型的“目标”。 +我们将在下面看到，构造器的参数可以包括``Foo``类型的对象，但要遵守一定的「正向性」约束，即保证``Foo``的元素是自下而上构建的。粗略地说，每个`...`可以是由``Foo``和以前定义的类型构建的任何箭头类型，其中``Foo``如果出现，也只是作为依值箭头类型的「目标」。 我们将提供一些归纳类型的例子。我们还把上述方案稍微扩展，即相互定义的归纳类型，以及所谓的*归纳族*。 -就像逻辑连接词一样，每个归纳类型都有引入规则，说明如何构造该类型的一个元素；还有消去规则，说明如何在另一个构造中“使用”该类型的一个元素。其实逻辑连接词也是归纳类型结构的例子。你已经看到了归纳类型的引入规则：它们只是在类型的定义中指定的构造器。消去规则提供了类型上的递归原则，其中也包括作为一种特殊情况的归纳原则。 +就像逻辑连接词一样，每个归纳类型都有引入规则，说明如何构造该类型的一个元素；还有消去规则，说明如何在另一个构造中「使用」该类型的一个元素。其实逻辑连接词也是归纳类型结构的例子。你已经看到了归纳类型的引入规则：它们只是在类型的定义中指定的构造器。消去规则提供了类型上的递归原则，其中也包括作为一种特殊情况的归纳原则。 在下一章中，我们将介绍Lean的函数定义包，它提供了更方便的方法来定义归纳类型上的函数并进行归纳证明。但是由于归纳类型的概念是如此的基本，我们觉得从低级的、实践的理解开始是很重要的。我们将从归纳类型的一些基本例子开始，然后逐步上升到更详细和复杂的例子。 @@ -167,7 +167,7 @@ We will use the `match` expression to define a function from ``Weekday`` to the natural numbers: --> -把``sunday``、``monday``、... 、``saturday``看作是``Weekday``的不同元素，没有其他有区别的属性。消去规则``Weekday.rec``，与``Weekday``类型及其构造器一起定义。它也被称为**递归器**（Recursor），它是使该类型“归纳”的原因：它允许我们通过给每个构造器分配相应的值来定义`Weekday`的函数。直观的说，归纳类型是由构造器详尽地生成的，除了它们构造的元素外，没有其他元素。 +把``sunday``、``monday``、... 、``saturday``看作是``Weekday``的不同元素，没有其他有区别的属性。消去规则``Weekday.rec``，与``Weekday``类型及其构造器一起定义。它也被称为**递归器**（Recursor），它是使该类型「归纳」的原因：它允许我们通过给每个构造器分配相应的值来定义`Weekday`的函数。直观的说，归纳类型是由构造器详尽地生成的，除了它们构造的元素外，没有其他元素。 我们将使用`match`表达式来定义一个从``Weekday``到自然数的函数： @@ -253,7 +253,7 @@ Lean to generate a function that converts `Weekday` objects into text. This function is used by the `#eval` command to display `Weekday` objects. --> -> 译者注：此处详细解释一下递归器`rec`。递归器作为归纳类型的消去规则，用于构造归纳类型到其他类型的函数。从最朴素的集合论直觉上讲，枚举类型的函数只需要规定每个元素的对应，也就是`match`的方式，但是要注意，`match`并不像其他Lean关键字那样是一种简单的语法声明，它实际上是一种功能，而这并不是类型论自带的功能。因此`match`需要一个类型论实现，也就是递归器。现在我们通过`#check @Weekday.rec`命令的输出来看递归器是如何工作的。首先回忆`@`是显式参数的意思。递归器是一个复杂的函数，输入的信息有1）motive：一个“目的”函数，表明想要拿当前类型构造什么类型。这个输出类型足够一般所以在u上；2）motive函数对所有枚举元素的输出值(这里就显得它非常“递归”)。这两点是准备工作，下面是这个函数的实际工作：输入一个具体的属于这个枚举类型的项`t`，输出结果`motive t`。下文在非枚举类型中，会直接用到这些递归器，届时可以更清晰地看到它们如何被使用。 +> 译者注：此处详细解释一下递归器`rec`。递归器作为归纳类型的消去规则，用于构造归纳类型到其他类型的函数。从最朴素的集合论直觉上讲，枚举类型的函数只需要规定每个元素的对应，也就是`match`的方式，但是要注意，`match`并不像其他Lean关键字那样是一种简单的语法声明，它实际上是一种功能，而这并不是类型论自带的功能。因此`match`需要一个类型论实现，也就是递归器。现在我们通过`#check @Weekday.rec`命令的输出来看递归器是如何工作的。首先回忆`@`是显式参数的意思。递归器是一个复杂的函数，输入的信息有1）motive：一个「目的」函数，表明想要拿当前类型构造什么类型。这个输出类型足够一般所以在u上；2）motive函数对所有枚举元素的输出值(这里就显得它非常「递归」)。这两点是准备工作，下面是这个函数的实际工作：输入一个具体的属于这个枚举类型的项`t`，输出结果`motive t`。下文在非枚举类型中，会直接用到这些递归器，届时可以更清晰地看到它们如何被使用。 当声明一个归纳数据类型时，你可以使用`deriving Repr`来指示Lean生成一个函数，将`Weekday`对象转换为文本。这个函数被`#eval`命令用来显示`Weekday`对象。 @@ -429,7 +429,7 @@ enumerated type. 下面的[归纳类型的策略](#归纳类型的策略)一节将介绍额外的策略，这些策略是专门为利用归纳类型而设计。 -命题即类型的对应原则下，我们可以使用``match``来证明定理和定义函数。换句话说，逐情况证明是一种逐情况定义的另一表现形式，其中被“定义”的是一个证明而不是一段数据。 +命题即类型的对应原则下，我们可以使用``match``来证明定理和定义函数。换句话说，逐情况证明是一种逐情况定义的另一表现形式，其中被「定义」的是一个证明而不是一段数据。 Lean库中的`Bool`类型是一个枚举类型的实例。 @@ -455,7 +455,7 @@ suggest defining boolean operations ``and``, ``or``, ``not`` on the binary operation like ``and`` using `match`: --> -（为了运行这个例子，我们把它们放在一个叫做``Hidden``的命名空间中，这样像``Bool``这样的名字就不会和标准库中的 ``Bool``冲突。这是必要的，因为这些类型是Lean“启动工作”的一部分，在系统启动时被自动导入）。 +（为了运行这个例子，我们把它们放在一个叫做``Hidden``的命名空间中，这样像``Bool``这样的名字就不会和标准库中的 ``Bool``冲突。这是必要的，因为这些类型是Lean「启动工作」的一部分，在系统启动时被自动导入）。 作为一个练习，你应该思考这些类型的引入和消去规则的作用。作为进一步的练习，我们建议在``Bool``类型上定义布尔运算 ``and``、``or``、``not``，并验证其共性。提示，你可以使用`match`来定义像`and`这样的二元运算： @@ -490,7 +490,7 @@ constructed argument. Consider the definitions of the product type and sum type in the library: --> -枚举类型是归纳类型的一种非常特殊的情况，其中构造器根本不需要参数。一般来说，“构造”可以依赖于数据，然后在构造参数中表示。考虑一下库中的乘积类型和求和类型的定义: +枚举类型是归纳类型的一种非常特殊的情况，其中构造器根本不需要参数。一般来说，「构造」可以依赖于数据，然后在构造参数中表示。考虑一下库中的乘积类型和求和类型的定义: ```lean # namespace Hidden @@ -572,7 +572,7 @@ output value in terms of ``b``. 参数`motive`是用来指定你要构造的对象的类型，它是一个依值的函数，`_`是被自动推断出的类型，此处即`Bool × Nat`。函数`cond`是一个布尔条件：`cond b t1 t2`，如果`b`为真，返回`t1`，否则返回`t2`。函数`prod_example`接收一个由布尔值`b`和一个数字`n`组成的对，并根据`b`为真或假返回`2 * n`或`2 * n + 1`。 -相比之下，求和类型有*两个*构造器`inl`和`inr`（表示“从左引入”和“从右引入”），每个都需要**一个**（显式的）参数。要在``Sum α β``上定义一个函数，我们必须处理两种情况：要么输入的形式是``inl a``，由此必须依据``a``指定一个输出值；要么输入的形式是``inr b``，由此必须依据``b``指定一个输出值。 +相比之下，求和类型有*两个*构造器`inl`和`inr`（表示「从左引入」和「从右引入」），每个都需要**一个**（显式的）参数。要在``Sum α β``上定义一个函数，我们必须处理两种情况：要么输入的形式是``inl a``，由此必须依据``a``指定一个输出值；要么输入的形式是``inr b``，由此必须依据``b``指定一个输出值。 ```lean def sum_example (s : Sum Nat Nat) : Nat := @@ -648,7 +648,7 @@ well as its projections, at the same time. 这些定义的结果与本节前面给出的定义基本相同。 -像``Prod``这样只有一个构造器的类型是纯粹的合取型：构造器只是将参数列表打包成一块数据，基本上是一个元组，后续参数的类型可以取决于初始参数的类型。我们也可以把这样的类型看作是一个“记录”或“结构体”。在Lean中，关键词``structure``可以用来同时定义这样一个归纳类型以及它的投影。 +像``Prod``这样只有一个构造器的类型是纯粹的合取型：构造器只是将参数列表打包成一块数据，基本上是一个元组，后续参数的类型可以取决于初始参数的类型。我们也可以把这样的类型看作是一个「记录」或「结构体」。在Lean中，关键词``structure``可以用来同时定义这样一个归纳类型以及它的投影。 ```lean # namespace Hidden @@ -776,7 +776,7 @@ types is inhabited, and that the type of functions to an inhabited type is inhabited. --> -在依值类型论的语义中，没有内置的部分函数的概念。一个函数类型``α → β``或一个依值函数类型``(a : α) → β``的每个元素都被假定为在每个输入端有一个值。``Option``类型提供了一种表示部分函数的方法。`Option β`的一个元素要么是`none`，要么是`some b`的形式，用于某个值`b : β`。因此我们可以认为`α → Option β`类型的元素`f`是一个从`α`到`β`的部分函数：对于每一个`a : α`，`f a`要么返回`none`，表示`f a`是“未定义”，要么返回`some b`。 +在依值类型论的语义中，没有内置的部分函数的概念。一个函数类型``α → β``或一个依值函数类型``(a : α) → β``的每个元素都被假定为在每个输入端有一个值。``Option``类型提供了一种表示部分函数的方法。`Option β`的一个元素要么是`none`，要么是`some b`的形式，用于某个值`b : β`。因此我们可以认为`α → Option β`类型的元素`f`是一个从`α`到`β`的部分函数：对于每一个`a : α`，`f a`要么返回`none`，表示`f a`是「未定义」，要么返回`some b`。 `Inhabited α`的一个元素只是证明了`α`有一个元素的事实。稍后，我们将看到``Inhabited``是Lean中*类型类*的一个例子：Lean可以被告知合适的基础类型是含有元素的，并且可以在此基础上自动推断出其他构造类型是含有元素的。 @@ -906,7 +906,7 @@ very type being defined. A canonical example is the type ``Nat`` of natural numbers: --> -到目前为止，我们所看到的归纳定义的类型都是“无趣的”：构造器打包数据并将其插入到一个类型中，而相应的递归器则解压数据并对其进行操作。当构造器作用于被定义的类型中的元素时，事情就变得更加有趣了。一个典型的例子是自然数``Nat``类型： +到目前为止，我们所看到的归纳定义的类型都是「无趣的」：构造器打包数据并将其插入到一个类型中，而相应的递归器则解压数据并对其进行操作。当构造器作用于被定义的类型中的元素时，事情就变得更加有趣了。一个典型的例子是自然数``Nat``类型： ```lean # namespace Hidden @@ -938,7 +938,7 @@ next argument to the recursor specifies a value for ``f (succ n)`` in terms of ``n`` and ``f n``. If we check the type of the recursor, --> -有两个构造器，我们从``zero : Nat``开始；它不需要参数，所以我们一开始就有了它。相反，构造器`succ`只能应用于先前构造的`Nat`。将其应用于``zero``，得到``succ zero : Nat``。再次应用它可以得到`succ (succ zero) : Nat`，依此类推。直观地说，`Nat`是具有这些构造器的“最小”类型，这意味着它是通过从`zero`开始并重复应用`succ`这样无穷无尽地（并且自由地）生成的。 +有两个构造器，我们从``zero : Nat``开始；它不需要参数，所以我们一开始就有了它。相反，构造器`succ`只能应用于先前构造的`Nat`。将其应用于``zero``，得到``succ zero : Nat``。再次应用它可以得到`succ (succ zero) : Nat`，依此类推。直观地说，`Nat`是具有这些构造器的「最小」类型，这意味着它是通过从`zero`开始并重复应用`succ`这样无穷无尽地（并且自由地）生成的。 和以前一样，``Nat``的递归器被设计用来定义一个从``Nat``到任何域的依值函数`f`，也就是一个`(n : nat) → motive n`的元素`f`，其中`motive : Nat → Sort u`。它必须处理两种情况：一种是输入为``zero``的情况，另一种是输入为 ``succ n``的情况，其中``n : Nat``。在第一种情况下，我们只需指定一个适当类型的目标值，就像以前一样。但是在第二种情况下，递归器可以假设在`n`处的`f`的值已经被计算过了。因此，递归器的下一个参数是以`n`和`f n`来指定`f (succ n)`的值。 @@ -1251,7 +1251,7 @@ and the remainder, ``t``, is known as the "tail." As an exercise, prove the following: --> -一个``α``类型的元素列表，要么是空列表``nil``，要么是一个元素``h : α``，后面是一个列表``t : List α``。第一个元素`h`，通常被称为列表的“头”，最后一个`t`，被称为“尾”。 +一个``α``类型的元素列表，要么是空列表``nil``，要么是一个元素``h : α``，后面是一个列表``t : List α``。第一个元素`h`，通常被称为列表的「头」，最后一个`t`，被称为「尾」。 作为一个练习，请证明以下内容： @@ -1509,7 +1509,7 @@ zero or the successor of some number." The result is functionally equivalent to the following: --> -可以认为这是在说“把``m + 3 * k``是零或者某个数字的后继的情况拆开”。其结果在功能上等同于以下： +可以认为这是在说「把``m + 3 * k``是零或者某个数字的后继的情况拆开」。其结果在功能上等同于以下： ```lean open Nat @@ -1950,7 +1950,7 @@ inductive definitions, for example, the principles of supported by Lean. --> -在类型论文献中，有对归纳定义的进一步推广，例如，“归纳-递归”和“归纳-归纳”的原则。这些东西Lean暂不支持。 +在类型论文献中，有对归纳定义的进一步推广，例如，「归纳-递归」和「归纳-归纳」的原则。这些东西Lean暂不支持。 -我们现在考虑两个经常有用的归纳类型的推广，Lean通过“编译”它们来支持上述更原始的归纳类型种类。换句话说，Lean解析了更一般的定义，在此基础上定义了辅助的归纳类型，然后使用辅助类型来定义我们真正想要的类型。下一章将介绍Lean的方程编译器，它需要有效地利用这些类型。尽管如此，在这里描述这些声明还是有意义的，因为它们是普通归纳定义的直接变形。 +我们现在考虑两个经常有用的归纳类型的推广，Lean通过「编译」它们来支持上述更原始的归纳类型种类。换句话说，Lean解析了更一般的定义，在此基础上定义了辅助的归纳类型，然后使用辅助类型来定义我们真正想要的类型。下一章将介绍Lean的方程编译器，它需要有效地利用这些类型。尽管如此，在这里描述这些声明还是有意义的，因为它们是普通归纳定义的直接变形。 首先，Lean支持**相互定义**的归纳类型。这个想法是，我们可以同时定义两个（或更多）归纳类型，其中每个类型都指代其他类型。 diff --git a/introduction.md b/introduction.md index abdc6ae..4078c02 100644 --- a/introduction.md +++ b/introduction.md @@ -45,7 +45,7 @@ mathematical bounds, or finding mathematical objects. A calculation can be viewe too, help establish mathematical claims. --> -**自动定理证明**（Automated theorem proving）着眼于 "寻找" 证明。归结(Resolution)定理证明器、表格法(tableau)定理证明器、快速可满足性求解器(Fast satisfiability solvers)等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法；还有些系统为特定的语言和问题提供搜索和决策程序，例如整数或实数上的线性或非线性表达式；像SMT（Satisfiability modulo theories）这样的架构将通用的搜索方法与特定领域的程序相结合；计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段，这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。 +**自动定理证明**（Automated theorem proving）着眼于「寻找」证明。归结（Resolution）定理证明器、表格法（tableau）定理证明器、快速可满足性求解器（Fast satisfiability solvers）等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法；还有些系统为特定的语言和问题提供搜索和决策程序，例如整数或实数上的线性或非线性表达式；像SMT（Satisfiability modulo theories）这样的架构将通用的搜索方法与特定领域的程序相结合；计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段，这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。 -自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有bug，而且很难保证它们所提供的结果是正确的。相比之下，**交互式定理证明器**（Interactive theorem proving）侧重于 "验证" 证明，要求每个命题都有合适的公理基础的证明来支持。这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明，一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的 "证明对象"，可以传给其他系统并独立检查。构建这样的证明通常需要用户更多的输入和交互，但它可以让你获得更深入、更复杂的证明。 +自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有bug，而且很难保证它们所提供的结果是正确的。相比之下，**交互式定理证明器**（Interactive theorem proving）侧重于「验证」证明，要求每个命题都有合适的公理基础的证明来支持。这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明，一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的「证明对象」，可以传给其他系统并独立检查。构建这样的证明通常需要用户更多的输入和交互，但它可以让你获得更深入、更复杂的证明。 -结构体命令本质上是定义归纳数据类型的“前端”。每个``structure``声明都会引入一个同名的命名空间。一般形式如下: +结构体命令本质上是定义归纳数据类型的「前端」。每个``structure``声明都会引入一个同名的命名空间。一般形式如下: ``` structure where @@ -81,7 +81,7 @@ theorems. Here are some of the constructions generated for the declaration above. --> -类型``Point``的值是使用``Point.mk a b``创建的，并且点``p``的字段可以使用``Point.x p``和``Point.y p``。结构体命令还生成有用的递归子和定理。下面是为上述声明生成的一些结构体方法。 +类型``Point``的值是使用``Point.mk a b``创建的，并且点``p``的字段可以使用``Point.x p``和``Point.y p``。结构体命令还生成有用的递归器和定理。下面是为上述声明生成的一些结构体方法。 -只要可以从期望的类型推断出结构体的名称，后缀``: structure-type``就可以省略。例如，我们使用这种表示法来定义“Point”。字段的指定顺序无关紧要，因此下面的所有表达式定义相同的Point。 +只要可以从期望的类型推断出结构体的名称，后缀``: structure-type``就可以省略。例如，我们使用这种表示法来定义「Point」。字段的指定顺序无关紧要，因此下面的所有表达式定义相同的Point。 ```lean structure Point (α : Type u) where