1.6.1. 链表🔗

Lean 的标准库包含一个规范的链表数据类型，称为 List，以及使其更便于使用的特殊语法。 列表用方括号编写。 例如，包含小于 10 的质数的列表可以写成：

在幕后，List 是一个归纳数据类型，定义如下：

标准库中的实际定义略有不同，因为它使用了尚未介绍的功能，但本质上是相似的。 这个定义说 List 接受单个类型作为其参数，就像 PPoint 一样。 这个类型是存储在列表中的条目的类型。 根据构造器，List α 可以用 nil 或 cons 构建。 构造器 nil 表示空列表，构造器 cons 用于非空列表。 cons 的第一个参数是列表的头部，第二个参数是它的尾部。 包含 n 个条目的列表包含 n 个 cons 构造器，其中最后一个以 nil 作为其尾部。

primesUnder10 示例可以通过直接使用 List 的构造器更明确地编写：

这两个定义完全等价，但 primesUnder10 比 explicitPrimesUnder10 更容易阅读。

使用 List 的函数可以用与使用 Nat 的函数大致相同的方式定义。 实际上，将链表视为每个 succ 构造器都悬挂着额外数据字段的 Nat 是一种思考方式。 从这个角度来看，计算列表长度的过程就是将每个 cons 替换为 succ，将最后的 nil 替换为 zero。 正如 replaceX 将点字段的类型作为参数一样，length 接受列表条目的类型。 例如，如果列表包含字符串，那么第一个参数是 String：length String ["Sourdough", "bread"]。 它应该像这样计算：

length 的定义既是多态的（因为它将列表条目类型作为参数），也是递归的（因为它引用自身）。 通常，函数遵循数据的形状：递归数据类型导致递归函数，多态数据类型导致多态函数。

诸如 xs 和 ys 之类的名称通常用来表示未知值的列表。 名称中的 s 表示它们是复数，所以它们读作"exes"和"whys"而不是"x s"和"y s"。

为了更容易阅读列表上的函数，方括号记法 [] 可以用来对 nil 进行模式匹配，中缀 :: 可以用来代替 cons：

1.6.2. 隐式参数🔗

replaceX 和 length 使用起来都有些繁琐，因为类型参数通常由后续值唯一确定。 实际上，在大多数语言中，编译器完全能够自行确定类型参数，只是偶尔需要用户的帮助。 Lean 也是如此。 在定义函数时，可以通过将参数包装在花括号而不是圆括号中来声明参数为 隐式的。 例如，具有隐式类型参数的 replaceX 版本如下所示：

它可以与 natOrigin 一起使用而无需明确提供 Nat，因为 Lean 可以从后续参数中 推断 α 的值：

{ x := 5, y := 0 }

类似地，length 可以重新定义为隐式接受条目类型：

这个 length 函数可以直接应用于 primesUnder10：

4

在标准库中，Lean 将此函数称为 List.length，这意味着用于结构字段访问的点语法也可以用来查找列表的长度：

4

正如 C# 和 Java 有时需要明确提供类型参数一样，Lean 并不总是能够找到隐式参数。 在这些情况下，可以使用它们的名称来提供它们。 例如，只适用于整数列表的 List.length 版本可以通过将 α 设置为 Int 来指定：

List.length : List Int → Nat

1.6.3. 更多内置数据类型🔗

除了列表之外，Lean 的标准库还包含许多其他结构体和归纳数据类型，可用于各种场景。

some 2

don't know how to synthesize implicit argument 'α'
  @List.nil ?m.3
context:
⊢ Type ?u.61664

don't know how to synthesize implicit argument 'α'
  @_root_.List.head? ?m.3 []
context:
⊢ Type ?u.61664

none

none

1.6.4. 你可能遇到的消息🔗

并非所有可定义的结构或归纳类型都可以具有类型 Type。 特别是，如果构造器将任意类型作为参数，那么归纳类型必须具有不同的类型。 这些错误通常会说一些关于"宇宙层级"的内容。 例如，对于这个归纳类型：

Lean 给出以下错误：

Invalid universe level in constructor `MyType.ctor`: Parameter `α` has type
  Type
at universe level
  2
which is not less than or equal to the inductive type's resulting universe level
  1

后面的章节描述了为什么会这样，以及如何修改定义使其工作。 现在，尝试将类型作为整个归纳类型的参数，而不是构造器的参数。

类似地，如果构造器的参数是一个以正在定义的数据类型为参数的函数，那么定义会被拒绝。 例如：

产生消息：

(kernel) arg #1 of 'MyType.ctor' has a non positive occurrence of the datatypes being declared

出于技术原因，允许这些数据类型可能会破坏 Lean 的内部逻辑，使其不适合用作定理证明器。

接受两个参数的递归函数不应该对对进行匹配，而应该独立地匹配每个参数。 否则，Lean 中检查递归调用是否在较小值上进行的机制无法看到输入值与递归调用中的参数之间的连接。 例如，这个确定两个列表是否具有相同长度的函数被拒绝：

错误消息是：

fail to show termination for
  sameLength
with errors
failed to infer structural recursion:
Not considering parameter α of sameLength:
  it is unchanged in the recursive calls
Not considering parameter β of sameLength:
  it is unchanged in the recursive calls
Cannot use parameter xs:
  failed to eliminate recursive application
    sameLength xs' ys'
Cannot use parameter ys:
  failed to eliminate recursive application
    sameLength xs' ys'


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
              xs ys
1) 1816:28-46  ?  ?
Please use `termination_by` to specify a decreasing measure.

问题可以通过嵌套模式匹配来解决：

下一节描述的同时匹配是解决问题的另一种方式，通常更优雅。

忘记归纳类型的参数也会产生令人困惑的消息。 例如，当参数 α 没有在 ctor 的类型中传递给 MyType 时：

Lean 用以下错误回复：

type expected, got
  (MyType : Type → Type)

错误消息是说 MyType 的类型，即 Type → Type，本身并不描述类型。 MyType 需要一个参数才能成为真正的类型。

当在其他上下文中省略类型参数时，可能出现相同的消息，比如在定义的类型签名中：

type expected, got
  (MyType : Type → Type)

评估使用多态类型的表达式可能会触发 Lean 无法显示值的情况。 #eval 命令评估提供的表达式，使用表达式的类型来确定如何显示结果。 对于某些类型，例如函数，此过程失败，但 Lean 完全能够自动生成大多数其他类型的显示代码。 例如，不需要为 WoodSplittingTool 提供任何特定的显示代码：

WoodSplittingTool.axe

Lean 在这里使用的自动化存在限制。 allTools 是所有三个工具的列表：

评估它会导致错误：

could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
  List WoodSplittingTool

这是因为 Lean 试图使用内置表中的代码来显示列表，但此代码要求 WoodSplittingTool 的显示代码已经存在。 可以通过指示 Lean 在定义数据类型时生成此显示代码，而不是在 #eval 的最后时刻作为一部分来解决此错误，方法是向其定义添加 deriving Repr：

评估 Firewood 列表成功：

[Firewood.birch, Firewood.pine, Firewood.beech]

1.6.5. 练习🔗

• 编写一个函数来查找列表中的最后一个条目。它应该返回一个 Option。

• 编写一个函数，查找列表中满足给定谓词的第一个条目。从 def List.findFirst? {α : Type} (xs : List α) (predicate : α → Bool) : Option α := … 开始定义。

• 编写一个函数 Prod.switch，它交换偶对中的两个字段。从 def Prod.switch {α β : Type} (pair : α × β) : β × α := … 开始定义。

• 使用自定义数据类型重写 PetName 示例，并将其与使用 Sum 的版本进行比较。

• 编写一个函数 zip，将两个列表合并为一个列表对。结果列表的长度应与最短输入列表的长度相同。从 def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) := … 开始定义。

• 编写一个多态函数 take，返回列表中的前 n 个条目，其中 n 是一个 Nat。如果列表包含少于 n 个条目，则结果列表应为整个输入列表。#eval take 3 ["bolete", "oyster"] 应该产生 ["bolete", "oyster"]，而 ["bolete"]#eval take 1 ["bolete", "oyster"] 应该产生 ["bolete"]。

• 使用类型和算术之间的类比，编写一个函数，将乘法分配到和上。换句话说，它应该具有类型 α × (β ⊕ γ) → (α × β) ⊕ (α × γ)。

• 使用类型和算术之间的类比，编写一个函数，将乘法分配到和上。换句话说，它应该具有类型 Bool × α → α ⊕ α。