From 48d4a5152d28c6a49bbb7d596ed5008372b11714 Mon Sep 17 00:00:00 2001 From: subfish-zhou Date: Mon, 17 Jun 2024 22:07:24 +0200 Subject: [PATCH 1/2] update inductive_type --- SUMMARY.md | 2 +- inductive_types.md | 527 +++++++++++++++++++++++++++++++++++++++++++++ introduction.md | 4 + 3 files changed, 532 insertions(+), 1 deletion(-) diff --git a/SUMMARY.md b/SUMMARY.md index fa71aa9..df06bc8 100644 --- a/SUMMARY.md +++ b/SUMMARY.md @@ -22,7 +22,7 @@ [Lean 4 定理证明](./title_page.md) -- [介绍](./introduction.md) +- [简介](./introduction.md) - [依值类型论](./dependent_type_theory.md) - [命题与证明](./propositions_and_proofs.md) - [量词与等价](./quantifiers_and_equality.md) diff --git a/inductive_types.md b/inductive_types.md index a406623..a29664f 100644 --- a/inductive_types.md +++ b/inductive_types.md @@ -1,6 +1,12 @@ + +归纳类型 +=============== + + + +我们已经看到Lean的形式基础包括基本类型，``Prop, Type 0, Type 1, Type 2, ...``，并允许形成依值函数类型，``(x : α) → β``。在例子中，我们还使用了额外的类型，如``Bool``、``Nat``和``Int``，以及类型构造器，如``List``和乘积``×``。事实上，在Lean的库中，除了宇宙之外的每一个具体类型和除了依值箭头之外的每一个类型构造器都是一个被称为*归纳类型*的类型构造的一般类别的实例。值得注意的是，仅用类型宇宙、依值箭头类型和归纳类型就可以构建一个内涵丰富的数学大厦；其他一切都源于这些。 + +直观地说，一个归纳类型是由一个指定的构造器列表建立起来的。在Lean中，指定这种类型的语法如下： ``` inductive Foo where @@ -25,6 +36,7 @@ inductive Foo where | constructorₙ : ... → Foo ``` + + +我们的直觉是，每个构造器都指定了一种建立新的对象``Foo``的方法，可能是由以前构造的值构成。``Foo``类型只不过是由以这种方式构建的对象组成。归纳式声明中的第一个字符也可以用逗号而不是``|``来分隔构造器。 + +我们将在下面看到，构造器的参数可以包括``Foo``类型的对象，但要遵守一定的“正向性”约束，即保证``Foo``的元素是自下而上构建的。粗略地说，每个`...`可以是由``Foo``和以前定义的类型构建的任何箭头类型，其中``Foo``如果出现，也只是作为依值箭头类型的“目标”。 +我们将提供一些归纳类型的例子。我们还把上述方案稍微扩展，即相互定义的归纳类型，以及所谓的*归纳族*。 + +就像逻辑连接词一样，每个归纳类型都有引入规则，说明如何构造该类型的一个元素；还有消去规则，说明如何在另一个构造中“使用”该类型的一个元素。其实逻辑连接词也是归纳类型结构的例子。你已经看到了归纳类型的引入规则：它们只是在类型的定义中指定的构造器。消去规则提供了类型上的递归原则，其中也包括作为一种特殊情况的归纳原则。 + +在下一章中，我们将介绍Lean的函数定义包，它提供了更方便的方法来定义归纳类型上的函数并进行归纳证明。但是由于归纳类型的概念是如此的基本，我们觉得从低级的、实践的理解开始是很重要的。我们将从归纳类型的一些基本例子开始，然后逐步上升到更详细和复杂的例子。 + + + +枚举式类型 +---------------- + + +最简单的归纳类型是一个具有有限的、可枚举的元素列表的类型。 ```lean inductive Weekday where @@ -78,8 +110,12 @@ inductive Weekday where | saturday : Weekday ``` + + +``inductive``命令创建了一个新类型``Weekday``。构造器都在``Weekday``命名空间中。 ```lean # inductive Weekday where @@ -99,7 +135,11 @@ open Weekday #check monday ``` + + +在声明`Weekday`的归纳类型时，可以省略`: Weekday`。 ```lean inductive Weekday where @@ -112,6 +152,7 @@ inductive Weekday where | saturday ``` + + +把``sunday``、``monday``、... 、``saturday``看作是``Weekday``的不同元素，没有其他有区别的属性。消去规则``Weekday.rec``，与``Weekday``类型及其构造器一起定义。它也被称为**递归器**（Recursor），它是使该类型“归纳”的原因：它允许我们通过给每个构造器分配相应的值来定义`Weekday`的函数。直观的说，归纳类型是由构造器详尽地生成的，除了它们构造的元素外，没有其他元素。 + +我们将使用`match`表达式来定义一个从``Weekday``到自然数的函数： ```lean # inductive Weekday where @@ -151,8 +197,12 @@ def numberOfDay (d : Weekday) : Nat := #eval numberOfDay Weekday.tuesday -- 3 ``` + + +注意，`match`表达式是使用你声明归纳类型时生成的递归器`Weekday.rec`来编译的。 ```lean # inductive Weekday where @@ -197,9 +247,15 @@ set_option pp.all true -/ ``` + + +> 译者注：此处详细解释一下递归器`rec`。递归器作为归纳类型的消去规则，用于构造归纳类型到其他类型的函数。从最朴素的集合论直觉上讲，枚举类型的函数只需要规定每个元素的对应，也就是`match`的方式，但是要注意，`match`并不像其他Lean关键字那样是一种简单的语法声明，它实际上是一种功能，而这并不是类型论自带的功能。因此`match`需要一个类型论实现，也就是递归器。现在我们通过`#check @Weekday.rec`命令的输出来看递归器是如何工作的。首先回忆`@`是显式参数的意思。递归器是一个复杂的函数，输入的信息有1）motive：一个“目的”函数，表明想要拿当前类型构造什么类型。这个输出类型足够一般所以在u上；2）motive函数对所有枚举元素的输出值(这里就显得它非常“递归”)。这两点是准备工作，下面是这个函数的实际工作：输入一个具体的属于这个枚举类型的项`t`，输出结果`motive t`。下文在非枚举类型中，会直接用到这些递归器，届时可以更清晰地看到它们如何被使用。 + +当声明一个归纳数据类型时，你可以使用`deriving Repr`来指示Lean生成一个函数，将`Weekday`对象转换为文本。这个函数被`#eval`命令用来显示`Weekday`对象。 ```lean inductive Weekday where @@ -217,12 +273,18 @@ open Weekday #eval tuesday -- Weekday.tuesday ``` + + +将与某一结构相关的定义和定理归入同名的命名空间通常很有用。例如，我们可以将``numberOfDay``函数放在``Weekday``命名空间中。然后当我们打开命名空间时，我们就可以使用较短的名称。 + +我们可以定义从``Weekday``到``Weekday``的函数： ```lean # inductive Weekday where @@ -264,9 +326,13 @@ example : next (previous tuesday) = tuesday := end Weekday ``` + + +我们如何证明``next (previous d) = d``对于任何Weekday``d``的一般定理？你可以使用`match`来为每个构造器提供一个证明： ```lean # inductive Weekday where @@ -308,7 +374,11 @@ def next_previous (d : Weekday) : next (previous d) = d := | saturday => rfl ``` + + +用策略证明更简洁：（复习：组合器`tac1 <;> tac2`，意为将`tac2`应用于策略`tac1`产生的每个子目标。） ```lean # inductive Weekday where @@ -343,6 +413,7 @@ def next_previous (d : Weekday) : next (previous d) = d := by cases d <;> rfl ``` + + +下面的[归纳类型的策略](#归纳类型的策略)一节将介绍额外的策略，这些策略是专门为利用归纳类型而设计。 + +命题即类型的对应原则下，我们可以使用``match``来证明定理和定义函数。换句话说，逐情况证明是一种逐情况定义的另一表现形式，其中被“定义”的是一个证明而不是一段数据。 + +Lean库中的`Bool`类型是一个枚举类型的实例。 ```lean # namespace Hidden @@ -363,6 +441,7 @@ inductive Bool where # end Hidden ``` + + +（为了运行这个例子，我们把它们放在一个叫做``Hidden``的命名空间中，这样像``Bool``这样的名字就不会和标准库中的 ``Bool``冲突。这是必要的，因为这些类型是Lean“启动工作”的一部分，在系统启动时被自动导入）。 + +作为一个练习，你应该思考这些类型的引入和消去规则的作用。作为进一步的练习，我们建议在``Bool``类型上定义布尔运算 ``and``、``or``、``not``，并验证其共性。提示，你可以使用`match`来定义像`and`这样的二元运算： ```lean # namespace Hidden @@ -384,16 +468,29 @@ def and (a b : Bool) : Bool := # end Hidden ``` + +同样地，大多数等式可以通过引入合适的`match`，然后使用``rfl``来证明。 + + + +带参数的构造器 +--------------------------- + + +枚举类型是归纳类型的一种非常特殊的情况，其中构造器根本不需要参数。一般来说，“构造”可以依赖于数据，然后在构造参数中表示。考虑一下库中的乘积类型和求和类型的定义: ```lean # namespace Hidden @@ -406,6 +503,7 @@ inductive Sum (α : Type u) (β : Type v) where # end Hidden ``` + + +思考一下这些例子中发生了什么。乘积类型有一个构造器``Prod.mk``，它需要两个参数。要在``Prod α β``上定义一个函数，我们可以假设输入的形式是``Prod.mk a b``，而我们必须指定输出，用``a``和``b``来表示。我们可以用它来定义``Prod``的两个投影。标准库定义的符号``α × β``表示``Prod α β``，``(a, b)``表示``Prod.mk a b``。 ```lean # namespace Hidden @@ -429,6 +530,7 @@ def snd {α : Type u} {β : Type v} (p : Prod α β) : β := # end Hidden ``` + + +函数``fst``接收一个对``p``。``match``将`p`解释为一个对``Prod.mk a b``。还记得在[依值类型论](./dependent_type_theory.md)中，为了给这些定义以最大的通用性，我们允许类型``α``和``β``属于任何宇宙。 + +下面是另一个例子，我们用递归器`Prod.casesOn`代替`match`。 ```lean def prod_example (p : Bool × Nat) : Nat := @@ -445,6 +552,7 @@ def prod_example (p : Bool × Nat) : Nat := #eval prod_example (false, 3) ``` + + +参数`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``指定一个输出值。 ```lean def sum_example (s : Sum Nat Nat) : Nat := @@ -471,6 +584,7 @@ def sum_example (s : Sum Nat Nat) : Nat := #eval sum_example (Sum.inr 3) ``` + + +这个例子与前面的例子类似，但现在输入到`sum_example`的内容隐含了`inl n`或`inr n`的形式。在第一种情况下，函数返回``2 * n``，第二种情况下，它返回``2 * n + 1``。 + +注意，乘积类型取决于参数`α β : Type`，这些参数是构造器和`Prod`的参数。Lean会检测这些参数何时可以从构造器的参数或返回类型中推断出来，并在这种情况下使其隐式。 + +在[定义自然数](#定义自然数)一节中，我们将看到当归纳类型的构造器从归纳类型本身获取参数时会发生什么。本节考虑的例子暂时不是这样：每个构造器只依赖于先前指定的类型。 + +一个有多个构造器的类型是析取的：``Sum α β``的一个元素要么是``inl a``的形式，要么是``inl b``的形式。一个有多个参数的构造器引入了合取信息：从``Prod.mk a b``的元素``Prod α β``中我们可以提取``a``*和*``b``。一个任意的归纳类型可以包括这两个特征：拥有任意数量的构造器，每个构造器都需要任意数量的参数。 + +和函数定义一样，Lean的归纳定义语法可以让你把构造器的命名参数放在冒号之前： ```lean # namespace Hidden @@ -509,6 +634,7 @@ inductive Sum (α : Type u) (β : Type v) where # end Hidden ``` + + +这些定义的结果与本节前面给出的定义基本相同。 + +像``Prod``这样只有一个构造器的类型是纯粹的合取型：构造器只是将参数列表打包成一块数据，基本上是一个元组，后续参数的类型可以取决于初始参数的类型。我们也可以把这样的类型看作是一个“记录”或“结构体”。在Lean中，关键词``structure``可以用来同时定义这样一个归纳类型以及它的投影。 ```lean # namespace Hidden @@ -526,6 +657,7 @@ structure Prod (α : Type u) (β : Type v) where # end Hidden ``` + + +这个例子同时引入了归纳类型``Prod``，它的构造器``mk``，通常的消去子（``rec``和``recOn``），以及投影``fst``和``snd``。 + +如果你没有命名构造器，Lean使用`mk`作为默认值。例如，下面定义了一个记录，将一个颜色存储为RGB值的三元组： ```lean structure Color where @@ -545,10 +682,16 @@ def yellow := Color.mk 255 255 0 #eval Color.red yellow ``` + + +``yellow``的定义形成了有三个值的记录，而投影``Color.red``则返回红色成分。 + +如果你在每个字段之间加一个换行符，就可以不用括号。 ```lean structure Color where @@ -558,10 +701,14 @@ structure Color where deriving Repr ``` + + +``structure``命令对于定义代数结构特别有用，Lean提供了大量的基础设施来支持对它们的处理。例如，这里是一个半群的定义： ```lean structure Semigroup where @@ -570,9 +717,15 @@ structure Semigroup where mul_assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c) ``` + + +更多例子见[结构体和记录](./structures_and_records.md)。 + +我们已经讨论了依值乘积类型`Sigma`： ```lean # namespace Hidden @@ -581,7 +734,11 @@ inductive Sigma {α : Type u} (β : α → Type v) where # end Hidden ``` + + +库中另两个归纳类型的例子： ```lean # namespace Hidden @@ -594,6 +751,7 @@ inductive Inhabited (α : Type u) where # end Hidden ``` + + +在依值类型论的语义中，没有内置的部分函数的概念。一个函数类型``α → β``或一个依值函数类型``(a : α) → β``的每个元素都被假定为在每个输入端有一个值。``Option``类型提供了一种表示部分函数的方法。`Option β`的一个元素要么是`none`，要么是`some b`的形式，用于某个值`b : β`。因此我们可以认为`α → Option β`类型的元素`f`是一个从`α`到`β`的部分函数：对于每一个`a : α`，`f a`要么返回`none`，表示`f a`是“未定义”，要么返回`some b`。 + +`Inhabited α`的一个元素只是证明了`α`有一个元素的事实。稍后，我们将看到``Inhabited``是Lean中*类型族*的一个例子：Lean可以被告知合适的基础类型是含有元素的，并且可以在此基础上自动推断出其他构造类型是含有元素的。 +作为练习，我们鼓励你建立一个从``α``到``β``和``β``到``γ``的部分函数的组合概念，并证明其行为符合预期。我们也鼓励你证明``Bool``和``Nat``是含有元素的，两个含有元素的类型的乘积是含有元素的，以及到一个含有元素的类型的函数类型是含有元素的。 + + + +归纳定义的命题 +-------------------------------- + + +归纳定义的类型可以存在于任何类型宇宙中，包括最底层的类型，`Prop`。事实上，这正是逻辑连接词的定义方式。 ```lean # namespace Hidden @@ -640,6 +814,7 @@ inductive Or (a b : Prop) : Prop where # end Hidden ``` + + +你应该想一想这些是如何产生你已经看到的引入和消去规则的。有一些规则规定了归纳类型的消去子可以去消去什么，或者说，哪些类型可以成为递归器的目标。粗略地说，``Prop``中的归纳类型的特点是，只能消去成``Prop``中的其他类型。这与以下理解是一致的：如果``p : Prop``，一个元素``hp : p``不携带任何数据。然而，这个规则有一个小的例外，我们将在[归纳族](#归纳族)一节中讨论。 + +甚至存在量词也是归纳式定义的： ```lean # namespace Hidden @@ -659,6 +839,7 @@ inductive Exists {α : Sort u} (p : α → Prop) : Prop where # end Hidden ``` + + +请记住，符号``∃ x : α, p``是``Exists (fun x : α => p)``的语法糖。 + +`False`, `True`, `And`和`Or`的定义与`Empty`, `Unit`, `Prod`和`Sum`的定义完全类似。不同的是，第一组产生的是`Prop`的元素，第二组产生的是`Type u`的元素，适用于某些`u`。类似地，``∃ x : α, p``是``Σ x : α, p``的``Prop``值的变体。 + +这里可以提到另一个归纳类型，表示为`{x : α // p}`，它有点像`∃ x : α, P`和`Σ x : α, P`之间的混合。 ```lean # namespace Hidden @@ -679,7 +867,11 @@ inductive Subtype {α : Type u} (p : α → Prop) where # end Hidden ``` + + +事实上，在Lean中，``Subtype``是用结构体命令定义的。 ```lean # namespace Hidden @@ -689,19 +881,32 @@ structure Subtype {α : Sort u} (p : α → Prop) where # end Hidden ``` + + +符号`{x : α // p x}`是``Subtype (fun x : α => p x)``的语法糖。它仿照集合理论中的子集表示法：`{x : α // p x}`表示具有属性`p`的`α`元素的集合。 + +定义自然数 +---------------------------- + + + +到目前为止，我们所看到的归纳定义的类型都是“无趣的”：构造器打包数据并将其插入到一个类型中，而相应的递归器则解压数据并对其进行操作。当构造器作用于被定义的类型中的元素时，事情就变得更加有趣了。一个典型的例子是自然数``Nat``类型： ```lean # namespace Hidden @@ -711,6 +916,7 @@ inductive Nat where # end Hidden ``` + + +有两个构造器，我们从``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)`的值。 + +如果我们检查递归器的类型： ```lean # namespace Hidden @@ -740,7 +953,11 @@ terms of ``n`` and ``f n``. If we check the type of the recursor, # end Hidden ``` + + +你会得到： ``` {motive : Nat → Sort u} @@ -749,6 +966,7 @@ you find the following: → (t : Nat) → motive t ``` + + +隐参数``motive``，是被定义的函数的陪域。在类型论中，通常说``motive``是消去/递归的**目的**，因为它描述了我们希望构建的对象类型。接下来的两个参数指定了如何计算零和后继的情况，如上所述。它们也被称为小前提``minor premises``。最后，``t : Nat``，是函数的输入。它也被称为大前提``major premise``。 + +`Nat.recOn`与`Nat.rec`类似，但大前提发生在小前提之前。 ``` @Nat.recOn : @@ -767,11 +990,15 @@ The `Nat.recOn` is similar to `Nat.rec` but the major premise occurs before the → motive t ``` + + +例如，考虑自然数上的加法函数``add m n``。固定`m`，我们可以通过递归来定义`n`的加法。在基本情况下，我们将`add m zero`设为`m`。在后续步骤中，假设`add m n`的值已经确定，我们将`add m (succ n)`定义为`succ (add m n)`。 ```lean # namespace Hidden @@ -791,9 +1018,13 @@ open Nat # end Hidden ``` + + +将这些定义放入一个命名空间``Nat``是很有用的。然后我们可以继续在这个命名空间中定义熟悉的符号。现在加法的两个定义方程是成立的： ```lean # namespace Hidden @@ -818,6 +1049,7 @@ end Nat # end Hidden ``` + + +我们将在[类型族](./type_classes.md)一章中解释``instance``命令如何工作。我们以后的例子将使用Lean自己的自然数版本。 + +然而，证明像``zero + m = m``这样的事实，需要用归纳法证明。如上所述，归纳原则只是递归原则的一个特例，其中陪域``motive n``是``Prop``的一个元素。它代表了熟悉的归纳证明模式：要证明``∀ n, motive n``，首先要证明``motive 0``，然后对于任意的``n``，假设``ih : motive n``并证明``motive (succ n)``。 ```lean # namespace Hidden @@ -844,10 +1081,14 @@ theorem zero_add (n : Nat) : 0 + n = n := # end Hidden ``` + + +请注意，当``Nat.recOn``在证明中使用时，它实际上是变相的归纳原则。``rewrite``和``simp``策略在这样的证明中往往非常有效。在这种情况下，证明可以化简成： ```lean # namespace Hidden @@ -860,11 +1101,15 @@ theorem zero_add (n : Nat) : 0 + n = n := # end Hidden ``` + + +另一个例子，让我们证明加法结合律，``∀ m n k, m + n + k = m + (n + k)``。(我们定义的符号`+`是向左结合的，所以`m + n + k`实际上是`(m + n) + k`。) 最难的部分是确定在哪个变量上做归纳。由于加法是由第二个参数的递归定义的，``k``是一个很好的猜测，一旦我们做出这个选择，证明几乎是顺理成章的： ```lean # namespace Hidden @@ -882,7 +1127,11 @@ theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) := # end Hidden ``` + + +你又可以化简证明： ```lean open Nat @@ -892,7 +1141,11 @@ theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) := (fun k ih => by simp [Nat.add_succ, ih]) ``` + + +假设我们试图证明加法交换律。选择第二个参数做归纳法，我们可以这样开始： ```lean open Nat @@ -907,8 +1160,12 @@ theorem add_comm (m n : Nat) : m + n = n + m := _ = succ n + m := sorry) ``` + + +在这一点上，我们看到我们需要另一个事实，即``succ (n + m) = succ n + m``。你可以通过对``m``的归纳来证明这一点： ```lean open Nat @@ -924,7 +1181,11 @@ theorem succ_add (n m : Nat) : succ n + m = succ (n + m) := _ = succ (n + succ m) := rfl) ``` + + +然后你可以用``succ_add``代替前面证明中的``sorry``。然而，证明可以再次压缩： ```lean # namespace Hidden @@ -941,12 +1202,21 @@ theorem add_comm (m n : Nat) : m + n = n + m := # end Hidden ``` + + +其他递归数据类型 +-------------------------- + + +让我们再考虑一些归纳定义类型的例子。对于任何类型``α``，在库中定义了``α``的元素列表``List α``类型。 ```lean # namespace Hidden @@ -972,12 +1242,18 @@ end List # end Hidden ``` + + +一个``α``类型的元素列表，要么是空列表``nil``，要么是一个元素``h : α``，后面是一个列表``t : List α``。第一个元素`h`，通常被称为列表的“头”，最后一个`t`，被称为“尾”。 + +作为一个练习，请证明以下内容： ```lean # namespace Hidden @@ -1004,10 +1280,16 @@ theorem append_assoc (as bs cs : List α) # end Hidden ``` + + +还可以尝试定义函数``length : {α : Type u} → List α → Nat``，返回一个列表的长度，并证明它的行为符合我们的期望（例如，``length (append as bs) = length as + length bs``）。 + +另一个例子，我们可以定义二叉树的类型： ```lean inductive BinaryTree where @@ -1015,7 +1297,11 @@ inductive BinaryTree where | node : BinaryTree → BinaryTree → BinaryTree ``` + + +事实上，我们甚至可以定义可数多叉树的类型： ```lean inductive CBTree where @@ -1037,9 +1323,15 @@ def omega : CBTree := end CBTree ``` + +归纳类型的策略 +--------------------------- + + + +归纳类型在Lean中有最根本的重要性，因此设计了一些方便使用的策略，这里讲几种。 + +``cases``策略适用于归纳定义类型的元素，正如其名称所示：它根据每个可能的构造器分解元素。在其最基本的形式中，它被应用于局部环境中的元素`x`。然后，它将目标还原为``x``被每个构成体所取代的情况。 ```lean example (p : Nat → Prop) (hz : p 0) (hs : ∀ n, p (Nat.succ n)) : ∀ n, p n := by @@ -1058,6 +1355,7 @@ example (p : Nat → Prop) (hz : p 0) (hs : ∀ n, p (Nat.succ n)) : ∀ n, p n . apply hs -- goal is a : Nat ⊢ p (succ a) ``` + + +还有一些额外的修饰功能。首先，``cases``允许你使用``with``子句来选择每个选项的名称。例如在下一个例子中，我们为``succ``的参数选择`m`这个名字，这样第二个情况就指的是`succ m`。更重要的是，cases策略将检测局部环境中任何依赖于目标变量的项目。它将这些元素还原，进行拆分，并重新引入它们。在下面的例子中，注意假设`h : n ≠ 0`在第一个分支中变成`h : 0 ≠ 0`，在第二个分支中变成`h : succ m ≠ 0`。 ```lean open Nat @@ -1081,7 +1382,11 @@ example (n : Nat) (h : n ≠ 0) : succ (pred n) = n := by rfl ``` + + +``cases``可以用来产生数据，也可以用来证明命题。 ```lean def f (n : Nat) : Nat := by @@ -1091,7 +1396,11 @@ example : f 0 = 3 := rfl example : f 5 = 7 := rfl ``` + + +再一次，cases将被还原，分隔，然后在背景中重新引入依赖。 ```lean def Tuple (α : Type) (n : Nat) := @@ -1107,7 +1416,11 @@ example : f myTuple = 7 := rfl ``` + + +下面是一个带有参数的多个构造器的例子。 ```lean inductive Foo where @@ -1120,8 +1433,12 @@ def silly (x : Foo) : Nat := by | bar2 c d e => exact e ``` + + +每个构造器的备选项不需要按照构造器的声明顺序来求解。 ```lean # inductive Foo where @@ -1133,9 +1450,13 @@ def silly (x : Foo) : Nat := by | bar1 a b => exact b ``` + + +`with`的语法对于编写结构化证明很方便。Lean还提供了一个补充的`case`策略，它允许你专注于目标分配变量名。 ```lean # inductive Foo where @@ -1147,7 +1468,11 @@ def silly (x : Foo) : Nat := by case bar2 c d e => exact e ``` + + +``case``策略很聪明，它将把构造器与适当的目标相匹配。例如，我们可以按照相反的顺序填充上面的目标： ```lean # inductive Foo where @@ -1159,10 +1484,14 @@ def silly (x : Foo) : Nat := by case bar1 a b => exact b ``` + + +你也可以使用``cases``伴随一个任意的表达式。假设该表达式出现在目标中，cases策略将概括该表达式，引入由此产生的全称变量，并对其进行处理。 ```lean open Nat @@ -1174,9 +1503,13 @@ example (p : Nat → Prop) (hz : p 0) (hs : ∀ n, p (succ n)) (m k : Nat) apply hs -- goal is a : Nat ⊢ p (succ a) ``` + + +可以认为这是在说“把``m + 3 * k``是零或者某个数字的后继的情况拆开”。其结果在功能上等同于以下： ```lean open Nat @@ -1189,6 +1522,7 @@ example (p : Nat → Prop) (hz : p 0) (hs : ∀ n, p (succ n)) (m k : Nat) apply hs -- goal is a : Nat ⊢ p (succ a) ``` + + +注意，表达式``m + 3 * k``被``generalize``删除了；重要的只是它的形式是``0``还是``succ a``。这种形式的``cases``*不会*恢复任何同时提到方程中的表达式的假设（在本例中是`m + 3 * k`）。如果这样的术语出现在一个假设中，而你也想对其进行概括，你需要明确地恢复``revert``它。 + +如果你所涉及的表达式没有出现在目标中，``cases``策略使用``have``来把表达式的类型放到上下文中。下面是一个例子： ```lean example (p : Prop) (m n : Nat) @@ -1208,11 +1547,15 @@ example (p : Prop) (m n : Nat) case inr hge => exact h₂ hge ``` + + +定理``Nat.lt_or_ge m n``说``m < n ∨ m ≥ n``，很自然地认为上面的证明是在这两种情况下的分割。在第一个分支中，我们有假设``h₁ : m < n``，在第二个分支中，我们有假设``h₂ : m ≥ n``。上面的证明在功能上等同于以下： ```lean example (p : Prop) (m n : Nat) @@ -1223,11 +1566,17 @@ example (p : Prop) (m n : Nat) case inr hge => exact h₂ hge ``` + + +在前两行之后，我们有``h : m < n ∨ m ≥ n``作为假设，我们只需在此基础上做cases。 + +下面是另一个例子，我们利用自然数相等的可判定性，对`m = n`和`m ≠ n`的情况进行拆分。 ```lean #check Nat.sub_self @@ -1238,6 +1587,7 @@ example (m n : Nat) : m - n = 0 ∨ m ≠ n := by | inr hne => apply Or.inr; exact hne ``` + + +如果你``open Classical``，你可以对任何命题使用排中律。但是使用[类型族](./type_classes.md)推理，Lean实际上可以找到相关的决策程序，这意味着你可以在可计算函数中使用情况拆分。 + +正如``cases``项可以用来进行分情况证明，``induction``项可以用来进行归纳证明。其语法与`cases`相似，只是参数只能是局部上下文中的一个项。下面是一个例子： ```lean # namespace Hidden @@ -1258,7 +1613,11 @@ theorem zero_add (n : Nat) : 0 + n = n := by # end Hidden ``` + + +和``cases``一样，我们可以使用``case``代替`with`。 ```lean # namespace Hidden @@ -1269,7 +1628,11 @@ theorem zero_add (n : Nat) : 0 + n = n := by # end Hidden ``` + + +更多例子： ```lean # namespace Hidden @@ -1290,8 +1653,12 @@ theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) := by # end Hidden ``` + + +`induction`策略也支持用户定义的具有多个目标（又称主前提）的归纳原则。 ```lean /- @@ -1318,7 +1685,11 @@ example (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by assumption ``` + + +你也可以在策略中使用`match`符号： ```lean example : p ∨ q → q ∨ p := by @@ -1328,7 +1699,11 @@ example : p ∨ q → q ∨ p := by | Or.inr h2 => apply Or.inl; exact h2 ``` + + +为了方便起见，模式匹配已经被整合到诸如`intro`和`funext`等策略中。 ```lean example : s ∧ q ∧ r → p ∧ r → q ∧ p := by @@ -1344,12 +1719,16 @@ example : rw [Nat.add_comm] ``` + + +我们用最后一个策略来结束本节，这个策略旨在促进归纳类型的工作，即``injection``注入策略。归纳类型的元素是自由生成的，也就是说，构造器是注入式的，并且有不相交的作用范围。``injection``策略是为了利用这一事实： ```lean open Nat @@ -1361,11 +1740,17 @@ example (m n k : Nat) (h : succ (succ m) = succ (succ n)) rw [h''] ``` + + +该策略的第一个实例在上下文中加入了``h' : succ m = succ n``，第二个实例加入了``h'' : m = n``。 + +``injection``策略还可以检测不同构造器被设置为相等时产生的矛盾，并使用它们来关闭目标。 ```lean open Nat @@ -1380,11 +1765,21 @@ example (h : 7 = 4) : False := by contradiction ``` + + +如第二个例子所示，``contradiction``策略也能检测出这种形式的矛盾。 + +归纳族 +------------------ + + + +我们几乎已经完成了对Lean所接受的全部归纳定义的描述。到目前为止，你已经看到Lean允许你用任何数量的递归构造器引入归纳类型。事实上，一个归纳定义可以引入一个有索引的归纳类型的**族**（Family）。 + +归纳族是一个由以下形式的同时归纳定义的有索引的家族： ``` inductive foo : ... → Sort u where @@ -1402,6 +1802,7 @@ inductive foo : ... → Sort u where | constructorₙ : ... → foo ... ``` + + +与普通的归纳定义不同，它构造了某个``Sort u``的元素，更一般的版本构造了一个函数``... → Sort u``，其中``...``表示一串参数类型，也称为**索引**。然后，每个构造器都会构造一个家族中某个成员的元素。一个例子是``Vector α n``的定义，它是长度为``n``的``α``元素的向量的类型： ```lean # namespace Hidden @@ -1418,11 +1822,17 @@ inductive Vector (α : Type u) : Nat → Type u where # end Hidden ``` + + +注意，``cons``构造器接收``Vector α n``的一个元素，并返回``Vector α (n+1)``的一个元素，从而使用家族中的一个成员的元素来构建另一个成员的元素。 + +一个更奇特的例子是由Lean中相等类型的定义： ```lean # namespace Hidden @@ -1431,6 +1841,7 @@ inductive Eq {α : Sort u} (a : α) : α → Prop where # end Hidden ``` + + +对于每个固定的``α : Sort u``和``a : α``，这个定义构造了一个``Eq a x``的类型族，由``x : α``索引。然而，只有一个构造器`refl`，它是`Eq a a`的一个元素，构造器后面的大括号告诉Lean要把`refl`的参数明确化。直观地说，在`x`是`a`的情况下，构建`Eq a x`证明的唯一方法是使用自反性。请注意，`Eq a a`是`Eq a x`这个类型家族中唯一的类型。由Lean产生的消去规则如下： ```lean universe u v @@ -1447,11 +1861,17 @@ universe u v → motive a rfl → {b : α} → (h : a = b) → motive b h) ``` + + +一个显著的事实是，所有关于相等的基本公理都来自构造器`refl`和消去子`Eq.rec`。然而，相等的定义是不典型的，见[公理化细节](#公理化细节)一节的讨论。 + +递归器`Eq.rec`也被用来定义代换： ```lean # namespace Hidden @@ -1460,7 +1880,11 @@ theorem subst {α : Type u} {a b : α} {p : α → Prop} (h₁ : Eq a b) (h₂ : # end Hidden ``` + + +可以使用`match`定义`subst`。 ```lean # namespace Hidden @@ -1470,8 +1894,12 @@ theorem subst {α : Type u} {a b : α} {p : α → Prop} (h₁ : Eq a b) (h₂ : # end Hidden ``` + + +实际上，Lean使用基于`Eq.rec`的定义来编译`match`表达式。 ```lean # namespace Hidden @@ -1489,11 +1917,17 @@ set_option pp.all true # end Hidden ``` + + +使用递归器或`match`与`h₁ : a = b`，我们可以假设`a`和`b`相同，在这种情况下，`p b`和`p a`相同。 + +证明``Eq``的对称和传递性并不难。在下面的例子中，我们证明`symm`，并留下`trans`和`congr` （congruence）定理作为练习。 ```lean # namespace Hidden @@ -1509,14 +1943,24 @@ theorem congr {α β : Type u} {a b : α} (f : α → β) (h : Eq a b) : Eq (f a # end Hidden ``` + +在类型论文献中，有对归纳定义的进一步推广，例如，“归纳-递归”和“归纳-归纳”的原则。这些东西Lean暂不支持。 + + + +公理化细节 +----------------- + + +我们已经通过例子描述了归纳类型和它们的语法。本节为那些对公理基础感兴趣的人提供额外的信息。 + +我们已经看到，归纳类型的构造器需要**参量**（parameter，与argument都有“参数”译义，为区别此处译为参量）——即在整个归纳构造过程中保持固定的参数——和**索引**，即同时在构造中的类型族的参数。每个构造器都应该有一个类型，其中的参数类型是由先前定义的类型、参量和索引类型以及当前正在定义的归纳族建立起来的。要求是，如果后者存在，它只**严格正向**出现。这意味着它所出现的构造器的任何参数都是一个依值箭头类型，其中定义中的归纳类型只作为结果类型出现，其中的索引是以常量和先前的参数来给出。 + +既然一个归纳类型对于某些``u``来说存在于在``Sort u``中，那么我们有理由问**哪些**宇宙层次的``u``可以被实例化。归纳类型族 ``C``的定义中的每个构造器``c``的形式为 ``` c : (a : α) → (b : β[a]) → C a p[a,b] ``` + + +其中`a`是一列数据类型的参量，`b`是一列构造器的参数，`p[a, b]`是索引，用于确定构造所处的归纳族的元素。（请注意，这种描述有些误导，因为构造器的参数可以以任何顺序出现，只要依赖关系是合理的）。对``C``的宇宙层级的约束分为两种情况，取决于归纳类型是否被指定落在``Prop``（即``Sort 0``）。 + +我们首先考虑归纳类型*不*指定落在``Prop``的情况。那么宇宙等级`u'`被限制为满足以下条件： + +> 对于上面的每个构造器`c`，以及序列`β[a]`中的每个`βk[a]`，如果`βk[a] : Sort v`，我们有`u`≥`v`。 + +换句话说，宇宙等级``u``被要求至少与代表构造器参数的每个类型的宇宙等级一样大。 +当归纳类型被指定落在``Prop``中时，对构造器参数的宇宙等级没有任何限制。但是这些宇宙等级对消去规则有影响。一般来说，对于``Prop``中的归纳类型，消去规则的motive被要求在``Prop``中。 + +这最后一条规则有一个例外：当只有一个构造器，并且每个构造器参数都在`Prop`中或者是一个索引时，我们可以从一个归纳定义的`Prop`中消除到一个任意的`Sort`。直观的说，在这种情况下，消除并不利用任何信息，而这些信息并不是由参数类型被栖息这一简单的事实所提供的。这种特殊情况被称为*单子消除*（singleton elimination）。 + +我们已经在`Eq.rec`的应用中看到了单子消除的作用，这是归纳定义的相等类型的消去子。我们可以使用一个元素``h : Eq a b``来将一个元素``t' : p a``转换为``p b``，即使``p a``和``p b``是任意类型，因为转换并不产生新的数据；它只是重新解释了我们已经有的数据。单子消除法也用于异质等价和良基的递归，这将在[归纳和递归](./induction_and_recursion.md)一章中讨论。 + + + +相互和嵌套的归纳类型 +--------------------------------- + + +我们现在考虑两个经常有用的归纳类型的推广，Lean通过“编译”它们来支持上述更原始的归纳类型种类。换句话说，Lean解析了更一般的定义，在此基础上定义了辅助的归纳类型，然后使用辅助类型来定义我们真正想要的类型。下一章将介绍Lean的方程编译器，它需要有效地利用这些类型。尽管如此，在这里描述这些声明还是有意义的，因为它们是普通归纳定义的直接变形。 + +首先，Lean支持**相互定义**的归纳类型。这个想法是，我们可以同时定义两个（或更多）归纳类型，其中每个类型都指代其他类型。 ```lean mutual @@ -1616,6 +2094,7 @@ mutual end ``` + + +在这个例子中，同时定义了两种类型：一个自然数`n`如果是`0`或比`Even`多一个，就是`Odd`；如果是比`Odd`多一个，就是`Even`。在下面的练习中，要求你写出细节。 + +相互的归纳定义也可以用来定义有限树的符号，节点由`α`的元素标记： ```lean mutual @@ -1635,6 +2119,7 @@ mutual end ``` + + +有了这个定义，我们可以通过给出一个``α``的元素和一个子树列表（可能是空的）来构造``Tree α``的元素。子树列表由`TreeList α`类型表示，它被定义为空列表`nil`，或者是一棵树的`cons`和`TreeList α`的一个元素。 + +然而，这个定义在工作中是不方便的。如果子树的列表是由``List (Tree α)``类型给出的，那就更好了，尤其是Lean的库中包含了一些处理列表的函数和定理。我们可以证明``TreeList α``类型与``List (Tree α)``是*同构*的，但是沿着这个同构关系来回翻译结果是很乏味的。 + +事实上，Lean允许我们定义我们真正想要的归纳类型： ```lean inductive Tree (α : Type u) where | mk : α → List (Tree α) → Tree α ``` + + +这就是所谓的**嵌套**归纳类型。它不属于上一节给出的归纳类型的严格规范，因为`Tree`不是严格意义上出现在`mk`的参数中，而是嵌套在`List`类型构造器中。然后Lean在其内核中自动建立了``TreeList α``和``List (Tree α)``之间的同构关系，并根据同构关系定义了``Tree``的构造器。 + +练习 +--------- + + + +1. 尝试定义自然数的其他运算，如乘法、前继函数（定义`pred 0 = 0`）、截断减法（当`m`大于或等于`n`时，`n - m = 0`）和乘方。然后在我们已经证明的定理的基础上，尝试证明它们的一些基本属性。 + +由于其中许多已经在Lean的核心库中定义，你应该在一个名为``Hidden``或类似的命名空间中工作，以避免名称冲突。 + +2. 定义一些对列表的操作，如``length``函数或``reverse``函数。证明一些属性，比如下面这些。 + + a. ``length (s ++ t) = length s + length t`` + + b. ``length (reverse t) = length t`` + + c. ``reverse (reverse t) = t`` + +3. 定义一个归纳数据类型，由以下构造器建立的项组成。 + + - `const n`，一个表示自然数`n`的常数 + - `var n`，一个变量，编号为`n` + - `plus s t`，表示`s`和`t`的总和 + - `times s t`，表示`s`和`t`的乘积 + + 递归地定义一个函数，根据变量的赋值来计算任何这样的项。 + +4. 同样，定义命题公式的类型，以及关于这类公式类型的函数：求值函数、衡量公式复杂性的函数，以及用另一个公式替代给定变量的函数。 diff --git a/introduction.md b/introduction.md index 9548104..ccc30f6 100644 --- a/introduction.md +++ b/introduction.md @@ -1,4 +1,8 @@ + + +简介 ============ +转换策略模式 +========================= + + + +在策略块中，可以使用关键字`conv`进入转换模式(conversion mode)。这种模式允许在假设和目标内部，甚至在函数抽象和依赖箭头内部移动，以应用重写或简化步骤。 + + +基本导航和重写 +------- + + +作为第一个例子，让我们证明`(a b c : Nat) : a * (b * c) = a * (c * b)`（本段中的例子有些刻意设计，因为其他策略可以立即完成它们）。首次简单的尝试是尝试`rw [Nat.mul_comm]`，但这将目标转化为`b * c * a = a * (c * b)`，因为它作用于项中出现的第一个乘法。有几种方法可以解决这个问题，其中一个方法是 + +```lean +example (a b c : Nat) : a * (b * c) = a * (c * b) := by + rw [Nat.mul_comm b c] +``` + +不过本节介绍一个更精确的工具：转换模式。下面的代码块显示了每行之后的当前目标。 ```lean example (a b c : Nat) : a * (b * c) = a * (c * b) := by @@ -33,6 +58,7 @@ example (a b c : Nat) : a * (b * c) = a * (c * b) := by rw [Nat.mul_comm] ``` + + +上面这段涉及三个导航指令： + +- `lhs`（left hand side）导航到关系（此处是等式）左边。同理`rhs`导航到右边。 +- `congr`创建与当前头函数的(非依赖的和显式的)参数数量一样多的目标（此处的头函数是乘法）。 +- `skip`走到下一个目标。 + +一旦到达相关目标，我们就可以像在普通策略模式中一样使用`rw`。 + +使用转换模式的第二个主要原因是在约束器下重写。假设我们想证明`(fun x : Nat => 0 + x) = (fun x => x)`。首次简单的尝试`rw [zero_add]`是失败的。报错： ``` error: tactic 'rewrite' failed, did not find instance of the pattern @@ -56,7 +93,13 @@ error: tactic 'rewrite' failed, did not find instance of the pattern ⊢ (fun x => 0 + x) = fun x => x ``` +（错误：'rewrite'策略失败了，没有找到目标表达式中的模式0 + ?n） + + + +解决方案为： ```lean example : (fun x : Nat => 0 + x) = (fun x => x) := by @@ -66,34 +109,59 @@ example : (fun x : Nat => 0 + x) = (fun x => x) := by rw [Nat.zero_add] ``` + + +其中`intro x`是导航命令，它进入了`fun`约束器。这个例子有点刻意，你也可以这样做： ```lean example : (fun x : Nat => 0 + x) = (fun x => x) := by funext x; rw [Nat.zero_add] ``` + + +或者这样： ```lean example : (fun x : Nat => 0 + x) = (fun x => x) := by simp ``` + + +所有这些也可以用`conv at h`从局部上下文重写一个假设`h`。 + +模式匹配 +------- + + + +使用上面的命令进行导航可能很无聊。使用下面的模式匹配来简化它： ```lean example (a b c : Nat) : a * (b * c) = a * (c * b) := by conv in b * c => rw [Nat.mul_comm] ``` + + +这是下面代码的语法糖： ```lean example (a b c : Nat) : a * (b * c) = a * (c * b) := by @@ -102,17 +170,30 @@ example (a b c : Nat) : a * (b * c) = a * (c * b) := by rw [Nat.mul_comm] ``` + + +当然也可以用通配符： ```lean example (a b c : Nat) : a * (b * c) = a * (c * b) := by conv in _ * c => rw [Nat.mul_comm] ``` + +结构化转换策略 +------- + + + +大括号和`.`也可以在`conv`模式下用于结构化策略。 ```lean example (a b c : Nat) : (0 + a) * (b * c) = a * (c * b) := by @@ -123,10 +204,19 @@ example (a b c : Nat) : (0 + a) * (b * c) = a * (c * b) := by . rw [Nat.mul_comm] ``` + + +转换模式中的其他策略 +---------- + + +- `arg i`进入一个应用的第`i`个非独立显式参数。 ```lean example (a b c : Nat) : a * (b * c) = a * (c * b) := by @@ -139,9 +229,15 @@ example (a b c : Nat) : a * (b * c) = a * (c * b) := by rw [Nat.mul_comm] ``` + + +- `args`是`congr`的替代品。 + +- `simp`将简化器应用于当前目标。它支持常规策略模式中的相同选项。 ```lean def f (x : Nat) := @@ -154,7 +250,11 @@ example (g : Nat → Nat) (h₁ : g x = x + 1) (h₂ : x > 0) : g x = f x := by exact h₁ ``` + + +- `enter [1, x, 2, y]`是`arg`和`intro`使用给定参数的宏。 ``` syntax enterArg := ident <|> group("@"? num) @@ -166,6 +266,7 @@ macro_rules | `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*])) ``` + + +- `done`会失败如果有未解决的目标。 + +- `traceState`显示当前策略状态。 + +- `whnf` put term in weak head normal form. + +- `tactic => `回到常规策略模式。这对于退出`conv`模式不支持的目标，以及应用自定义的一致性和扩展性引理很有用。 ```lean example (g : Nat → Nat → Nat) @@ -192,7 +302,11 @@ example (g : Nat → Nat → Nat) . tactic => exact h₂ ``` + + +- `apply `是`tactic => apply `的语法糖。 ```lean example (g : Nat → Nat → Nat) diff --git a/dependent_type_theory.md b/dependent_type_theory.md index b99a9df..a23a4eb 100644 --- a/dependent_type_theory.md +++ b/dependent_type_theory.md @@ -1264,7 +1264,7 @@ and the difference between the round and curly braces will be explained momentarily. --> -这就是*依值函数类型*，或者*依值箭头类型*的一个例子。给定``α : Type``和``β : α → Type``，把``β``考虑成``α``之上的类型族，也就是说，对于每个``a : α``都有类型``β a``。在这种情况下，类型``(a : α) → β a``表示的是具有如下性质的函数``f``的类型：对于每个``a : α``，``f a``是``β a``的一个元素。换句话说，``f``返回值的类型取决于其输入。 +这就是*依值函数类型*，或者*依值箭头类型*的一个例子。给定``α : Type``和``β : α → Type``，把``β``考虑成``α``之上的类型类，也就是说，对于每个``a : α``都有类型``β a``。在这种情况下，类型``(a : α) → β a``表示的是具有如下性质的函数``f``的类型：对于每个``a : α``，``f a``是``β a``的一个元素。换句话说，``f``返回值的类型取决于其输入。 注意到``(a : α) → β``对于任意表达式``β : Type``都有意义。当``β``的值依赖于``a``（例如，在前一段的表达式``β a``），``(a : α) → β``表示一个依值函数类型。当``β``的值不依赖于``a``，``(a : α) → β``与类型``α → β``无异。实际上，在依值类型论（以及Lean）中，``α → β``表达的意思就是当``β``的值不依赖于``a``时的``(a : α) → β``。【注】 diff --git a/inductive_types.md b/inductive_types.md index a29664f..1cc0854 100644 --- a/inductive_types.md +++ b/inductive_types.md @@ -668,7 +668,7 @@ example, the following defines a record to store a color as a triple of RGB values: --> -这个例子同时引入了归纳类型``Prod``，它的构造器``mk``，通常的消去子（``rec``和``recOn``），以及投影``fst``和``snd``。 +这个例子同时引入了归纳类型``Prod``，它的构造器``mk``，通常的消去器（``rec``和``recOn``），以及投影``fst``和``snd``。 如果你没有命名构造器，Lean使用`mk`作为默认值。例如，下面定义了一个记录，将一个颜色存储为RGB值的三元组： @@ -778,7 +778,7 @@ type is inhabited. 在依值类型论的语义中，没有内置的部分函数的概念。一个函数类型``α → β``或一个依值函数类型``(a : α) → β``的每个元素都被假定为在每个输入端有一个值。``Option``类型提供了一种表示部分函数的方法。`Option β`的一个元素要么是`none`，要么是`some b`的形式，用于某个值`b : β`。因此我们可以认为`α → Option β`类型的元素`f`是一个从`α`到`β`的部分函数：对于每一个`a : α`，`f a`要么返回`none`，表示`f a`是“未定义”，要么返回`some b`。 -`Inhabited α`的一个元素只是证明了`α`有一个元素的事实。稍后，我们将看到``Inhabited``是Lean中*类型族*的一个例子：Lean可以被告知合适的基础类型是含有元素的，并且可以在此基础上自动推断出其他构造类型是含有元素的。 +`Inhabited α`的一个元素只是证明了`α`有一个元素的事实。稍后，我们将看到``Inhabited``是Lean中*类型类*的一个例子：Lean可以被告知合适的基础类型是含有元素的，并且可以在此基础上自动推断出其他构造类型是含有元素的。 作为练习，我们鼓励你建立一个从``α``到``β``和``β``到``γ``的部分函数的组合概念，并证明其行为符合预期。我们也鼓励你证明``Bool``和``Nat``是含有元素的，两个含有元素的类型的乘积是含有元素的，以及到一个含有元素的类型的函数类型是含有元素的。 @@ -828,7 +828,7 @@ will discuss below, in [Section Inductive Families](#inductive-families). Even the existential quantifier is inductively defined: --> -你应该想一想这些是如何产生你已经看到的引入和消去规则的。有一些规则规定了归纳类型的消去子可以去消去什么，或者说，哪些类型可以成为递归器的目标。粗略地说，``Prop``中的归纳类型的特点是，只能消去成``Prop``中的其他类型。这与以下理解是一致的：如果``p : Prop``，一个元素``hp : p``不携带任何数据。然而，这个规则有一个小的例外，我们将在[归纳族](#归纳族)一节中讨论。 +你应该想一想这些是如何产生你已经看到的引入和消去规则的。有一些规则规定了归纳类型的消去器可以去消去什么，或者说，哪些类型可以成为递归器的目标。粗略地说，``Prop``中的归纳类型的特点是，只能消去成``Prop``中的其他类型。这与以下理解是一致的：如果``p : Prop``，一个元素``hp : p``不携带任何数据。然而，这个规则有一个小的例外，我们将在[归纳族](#归纳族)一节中讨论。 甚至存在量词也是归纳式定义的： @@ -1061,7 +1061,7 @@ pattern of an inductive proof: to prove ``∀ n, motive n``, first prove ``motiv and then, for arbitrary ``n``, assume ``ih : motive n`` and prove ``motive (succ n)``. --> -我们将在[类型族](./type_classes.md)一章中解释``instance``命令如何工作。我们以后的例子将使用Lean自己的自然数版本。 +我们将在[类型类](./type_classes.md)一章中解释``instance``命令如何工作。我们以后的例子将使用Lean自己的自然数版本。 然而，证明像``zero + m = m``这样的事实，需要用归纳法证明。如上所述，归纳原则只是递归原则的一个特例，其中陪域``motive n``是``Prop``的一个元素。它代表了熟悉的归纳证明模式：要证明``∀ n, motive n``，首先要证明``motive 0``，然后对于任意的``n``，假设``ih : motive n``并证明``motive (succ n)``。 @@ -1600,7 +1600,7 @@ induction. The syntax is similar to that of ``cases``, except that the argument can only be a term in the local context. Here is an example: --> -如果你``open Classical``，你可以对任何命题使用排中律。但是使用[类型族](./type_classes.md)推理，Lean实际上可以找到相关的决策程序，这意味着你可以在可计算函数中使用情况拆分。 +如果你``open Classical``，你可以对任何命题使用排中律。但是使用[类型类](./type_classes.md)推理，Lean实际上可以找到相关的决策程序，这意味着你可以在可计算函数中使用情况拆分。 正如``cases``项可以用来进行分情况证明，``induction``项可以用来进行归纳证明。其语法与`cases`相似，只是参数只能是局部上下文中的一个项。下面是一个例子： @@ -1852,7 +1852,7 @@ Note that ``Eq a a`` is the only inhabited type in the family of types ``Eq a x``. The elimination principle generated by Lean is as follows: --> -对于每个固定的``α : Sort u``和``a : α``，这个定义构造了一个``Eq a x``的类型族，由``x : α``索引。然而，只有一个构造器`refl`，它是`Eq a a`的一个元素，构造器后面的大括号告诉Lean要把`refl`的参数明确化。直观地说，在`x`是`a`的情况下，构建`Eq a x`证明的唯一方法是使用自反性。请注意，`Eq a a`是`Eq a x`这个类型家族中唯一的类型。由Lean产生的消去规则如下： +对于每个固定的``α : Sort u``和``a : α``，这个定义构造了一个``Eq a x``的类型类，由``x : α``索引。然而，只有一个构造器`refl`，它是`Eq a a`的一个元素，构造器后面的大括号告诉Lean要把`refl`的参数明确化。直观地说，在`x`是`a`的情况下，构建`Eq a x`证明的唯一方法是使用自反性。请注意，`Eq a a`是`Eq a x`这个类型家族中唯一的类型。由Lean产生的消去规则如下： ```lean universe u v @@ -1869,7 +1869,7 @@ definition of equality is atypical, however; see the discussion in [Section Axio The recursor ``Eq.rec`` is also used to define substitution: --> -一个显著的事实是，所有关于相等的基本公理都来自构造器`refl`和消去子`Eq.rec`。然而，相等的定义是不典型的，见[公理化细节](#公理化细节)一节的讨论。 +一个显著的事实是，所有关于相等的基本公理都来自构造器`refl`和消去器`Eq.rec`。然而，相等的定义是不典型的，见[公理化细节](#公理化细节)一节的讨论。 递归器`Eq.rec`也被用来定义代换： @@ -1987,9 +1987,9 @@ inductive types is of the form 我们已经通过例子描述了归纳类型和它们的语法。本节为那些对公理基础感兴趣的人提供额外的信息。 -我们已经看到，归纳类型的构造器需要**参量**（parameter，与argument都有“参数”译义，为区别此处译为参量）——即在整个归纳构造过程中保持固定的参数——和**索引**，即同时在构造中的类型族的参数。每个构造器都应该有一个类型，其中的参数类型是由先前定义的类型、参量和索引类型以及当前正在定义的归纳族建立起来的。要求是，如果后者存在，它只**严格正向**出现。这意味着它所出现的构造器的任何参数都是一个依值箭头类型，其中定义中的归纳类型只作为结果类型出现，其中的索引是以常量和先前的参数来给出。 +我们已经看到，归纳类型的构造器需要**参量**（parameter，与argument都有“参数”译义，为区别此处译为参量）——即在整个归纳构造过程中保持固定的参数——和**索引**，即同时在构造中的类型类的参数。每个构造器都应该有一个类型，其中的参数类型是由先前定义的类型、参量和索引类型以及当前正在定义的归纳族建立起来的。要求是，如果后者存在，它只**严格正向**出现。这意味着它所出现的构造器的任何参数都是一个依值箭头类型，其中定义中的归纳类型只作为结果类型出现，其中的索引是以常量和先前的参数来给出。 -既然一个归纳类型对于某些``u``来说存在于在``Sort u``中，那么我们有理由问**哪些**宇宙层次的``u``可以被实例化。归纳类型族 ``C``的定义中的每个构造器``c``的形式为 +既然一个归纳类型对于某些``u``来说存在于在``Sort u``中，那么我们有理由问**哪些**宇宙层次的``u``可以被实例化。归纳类型类 ``C``的定义中的每个构造器``c``的形式为 ``` c : (a : α) → (b : β[a]) → C a p[a,b] @@ -2052,7 +2052,7 @@ discussed in a [Chapter Induction and Recursion](./induction_and_recursion.md#we 这最后一条规则有一个例外：当只有一个构造器，并且每个构造器参数都在`Prop`中或者是一个索引时，我们可以从一个归纳定义的`Prop`中消除到一个任意的`Sort`。直观的说，在这种情况下，消除并不利用任何信息，而这些信息并不是由参数类型被栖息这一简单的事实所提供的。这种特殊情况被称为*单子消除*（singleton elimination）。 -我们已经在`Eq.rec`的应用中看到了单子消除的作用，这是归纳定义的相等类型的消去子。我们可以使用一个元素``h : Eq a b``来将一个元素``t' : p a``转换为``p b``，即使``p a``和``p b``是任意类型，因为转换并不产生新的数据；它只是重新解释了我们已经有的数据。单子消除法也用于异质等价和良基的递归，这将在[归纳和递归](./induction_and_recursion.md)一章中讨论。 +我们已经在`Eq.rec`的应用中看到了单子消除的作用，这是归纳定义的相等类型的消去器。我们可以使用一个元素``h : Eq a b``来将一个元素``t' : p a``转换为``p b``，即使``p a``和``p b``是任意类型，因为转换并不产生新的数据；它只是重新解释了我们已经有的数据。单子消除法也用于异质等价和良基的递归，这将在[归纳和递归](./induction_and_recursion.md)一章中讨论。 -Lean的主要功能是把用户的输入翻译成形式化的表达式，由内核检查其正确性，然后存储在环境中供以后使用。但是有些命令对环境有其他的影响，或者给环境中的对象分配属性，定义符号，或者声明类型族的实例，如[类型族](./type_classes.md)一章所述。这些命令大多具有全局效应，也就是说，它们不仅在当前文件中保持有效，而且在任何导入它的文件中也保持有效。然而，这类命令通常支持``local``修饰符，这表明它们只在当前``section``或``namespace``关闭前或当前文件结束前有效。 +Lean的主要功能是把用户的输入翻译成形式化的表达式，由内核检查其正确性，然后存储在环境中供以后使用。但是有些命令对环境有其他的影响，或者给环境中的对象分配属性，定义符号，或者声明类型类的实例，如[类型类](./type_classes.md)一章所述。这些命令大多具有全局效应，也就是说，它们不仅在当前文件中保持有效，而且在任何导入它的文件中也保持有效。然而，这类命令通常支持``local``修饰符，这表明它们只在当前``section``或``namespace``关闭前或当前文件结束前有效。 在[简化](./tactics.md#简化)一节中，我们看到可以用`[simp]`属性来注释定理，这使它们可以被简化器使用。下面的例子定义了列表的前缀关系，证明了这种关系是自反的，并为该定理分配了`[simp]`属性。 @@ -394,7 +394,7 @@ be explained in [Chapter Type Classes](./type_classes.md), works by assigning an ``[instance]`` attribute to the associated definition. --> -另一个例子，我们可以使用`instance`命令来给`isPrefix`关系分配符号`≤`。该命令将在[类型族](./type_classes.md)中解释，它的工作原理是给相关定义分配一个`[instance]`属性。 +另一个例子，我们可以使用`instance`命令来给`isPrefix`关系分配符号`≤`。该命令将在[类型类](./type_classes.md)中解释，它的工作原理是给相关定义分配一个`[instance]`属性。 ```lean def isPrefix (l₁ : List α) (l₂ : List α) : Prop := @@ -577,7 +577,7 @@ brackets, ``[`` and ``]``. These are used for type classes, as explained in [Chapter Type Classes](./type_classes.md). --> -还有第三种隐式参数，用方括号表示，``[``和``]``。这些是用于类型族的，在[类型族](./type_classes.md)中解释。 +还有第三种隐式参数，用方括号表示，``[``和``]``。这些是用于类型类的，在[类型类](./type_classes.md)中解释。 -你可以通过添加`Trans`类型族（Type class）的新实例来“教给”`calc`新的传递性定理。稍后将介绍类型族，但下面的小示例将演示如何使用新的`Trans`实例扩展`calc`表示法。 +你可以通过添加`Trans`类型类（Type class）的新实例来“教给”`calc`新的传递性定理。稍后将介绍类型类，但下面的小示例将演示如何使用新的`Trans`实例扩展`calc`表示法。 ```lean def divides (x y : Nat) : Prop := diff --git a/structures_and_records.md b/structures_and_records.md index b3a0c1c..be26e03 100644 --- a/structures_and_records.md +++ b/structures_and_records.md @@ -1,6 +1,12 @@ + +结构体和记录 +====================== + + + +我们已经看到Lean的基本系统包括归纳类型。此外，显然仅基于类型宇宙、依赖箭头类型和归纳类型，就有可能构建一个坚实的数学大厦；其他的一切都是由此而来。Lean标准库包含许多归纳类型的实例(例如，``Nat``，``Prod``，``List``)，甚至逻辑连接词也是使用归纳类型定义的。 + +回忆一下，只包含一个构造器的非递归归纳类型被称为**结构体**（structure）或**记录**（record）。乘积类型是一种结构体，依值乘积(Sigma)类型也是如此。一般来说，每当我们定义一个结构体``S``时，我们通常定义*投影*（projection）函数来“析构”（destruct）``S``的每个实例并检索存储在其字段中的值。``prod.pr1``和``prod.pr2``，分别返回乘积对中的第一个和第二个元素的函数，就是这种投影的例子。 + +在编写程序或形式化数学时，定义包含许多字段的结构体是很常见的。Lean中可用``structure``命令实现此过程。当我们使用这个命令定义一个结构体时，Lean会自动生成所有的投影函数。``structure``命令还允许我们根据以前定义的结构体定义新的结构体。此外，Lean为定义给定结构体的实例提供了方便的符号。 + +声明结构体 +-------------------- + + + +结构体命令本质上是定义归纳数据类型的“前端”。每个``structure``声明都会引入一个同名的命名空间。一般形式如下: ``` structure where :: ``` + + +大多数部分不是必要的。例子： ```lean structure Point (α : Type u) where mk :: (x : α) (y : α) ``` + + +类型``Point``的值是使用``Point.mk a b``创建的，并且点``p``的字段可以使用``Point.x p``和``Point.y p``。结构体命令还生成有用的递归子和定理。下面是为上述声明生成的一些结构体方法。 + + +```lean +# structure Point (α : Type u) where +# mk :: (x : α) (y : α) +#check Point -- 类型 +#check @Point.rec -- 消去器（eliminator） +#check @Point.mk -- 构造器 +#check @Point.x -- 投影 +#check @Point.y -- 投影 +``` + + + + +如果没有提供构造器名称，则默认的构造函数名为``mk``。如果在每个字段之间添加换行符，也可以避免字段名周围的括号。 ```lean structure Point (α : Type u) where @@ -73,9 +125,13 @@ structure Point (α : Type u) where y : α ``` + + +下面是一些使用生成的结构的简单定理和表达式。像往常一样，您可以通过使用命令``open Point``来避免前缀``Point``。 ```lean # structure Point (α : Type u) where @@ -93,9 +149,13 @@ example (a b : α) : y (mk a b) = b := rfl ``` + + +给定``p : Point Nat``，符号``p.x``是``Point.x p``的缩写。这提供了一种方便的方式来访问结构体的字段。 ```lean # structure Point (α : Type u) where @@ -108,6 +168,7 @@ def p := Point.mk 10 20 #eval p.y -- 20 ``` + + +点记号不仅方便于访问记录的投影，而且也方便于应用同名命名空间中定义的函数。回想一下[合取](./propositions_and_proofs.md#_conjunction)一节，如果``p``具有``Point``类型，那么表达式``p.foo``被解释为``Point.foo p``，假设``foo``的第一个非隐式参数具有类型``Point``，表达式``p.add q``因此是``Point.add p q``的缩写。可见下面的例子。 ```lean structure Point (α : Type u) where @@ -131,6 +195,7 @@ def q : Point Nat := Point.mk 3 4 #eval p.add q -- {x := 4, y := 6} ``` + + +在下一章中，您将学习如何定义一个像``add``这样的函数，这样它就可以通用地为``Point α``的元素工作，而不仅仅是``Point Nat``，只要假设``α``有一个关联的加法操作。 + +更一般地，给定一个表达式``p.foo x y z``其中`p : Point`，Lean会把``p``以``Point``为类型插入到``Point.foo``的第一个参数。例如，下面是标量乘法的定义，``p.smul 3``被解释为``Point.smul 3 p``。 ```lean # structure Point (α : Type u) where @@ -154,8 +224,12 @@ def p : Point Nat := Point.mk 1 2 #eval p.smul 3 -- {x := 3, y := 6} ``` + + +对``List.map``函数使用类似的技巧很常用。它接受一个列表作为它的第二个非隐式参数: ```lean #check @List.map @@ -166,16 +240,29 @@ def f : Nat → Nat := fun x => x * x #eval xs.map f -- [1, 4, 9] ``` + +此处``xs.map f``被解释为``List.map f xs``。 + + + +对象 +------- + + +我们一直在使用构造器创建结构体类型的元素。对于包含许多字段的结构，这通常是不方便的，因为我们必须记住字段定义的顺序。因此，Lean为定义结构体类型的元素提供了以下替代符号。 ``` { ( := )* : structure-type } @@ -183,11 +270,15 @@ notations for defining elements of a structure type. { ( := )* } ``` + + +只要可以从期望的类型推断出结构体的名称，后缀``: structure-type``就可以省略。例如，我们使用这种表示法来定义“Point”。字段的指定顺序无关紧要，因此下面的所有表达式定义相同的Point。 ```lean structure Point (α : Type u) where @@ -202,9 +293,13 @@ example : Point Nat := { y := 20, x := 10 } ``` + + +如果一个字段的值没有指定，Lean会尝试推断它。如果不能推断出未指定的字段，Lean会标记一个错误，表明相应的占位符无法合成。 ```lean structure MyStruct where @@ -216,6 +311,7 @@ structure MyStruct where #check { a := 10, b := true : MyStruct } ``` + + +**记录更新**（Record update）是另一个常见的操作，相当于通过修改旧记录中的一个或多个字段的值来创建一个新的记录对象。通过在字段赋值之前添加注释``s with``，Lean允许您指定记录规范中未赋值的字段，该字段应从之前定义的结构对象``s``中获取。如果提供了多个记录对象，那么将按顺序访问它们，直到Lean找到一个包含未指定字段的记录对象。如果在访问了所有对象之后仍未指定任何字段名，Lean将引发错误。 ```lean structure Point (α : Type u) where @@ -254,11 +353,20 @@ example : r.y = 2 := rfl example : r.z = 5 := rfl ``` + +继承 +----------- + + + +我们可以通过添加新的字段来**扩展**现有的结构体。这个特性允许我们模拟一种形式的**继承**。 ```lean structure Point (α : Type u) where @@ -272,8 +380,12 @@ structure ColorPoint (α : Type u) extends Point α where c : Color ``` + + +在下一个例子中，我们使用多重继承定义一个结构体，然后使用父结构的对象定义一个对象。 ```lean structure Point (α : Type u) where