翻译-Lean Language Reference-13-项

13.1. 标识符 Identifiers

$x:ident

标识符项是对某个名称的调用。

标识符的具体词法规定 在 Lean 的具体语法 一节中 有详细说明。

标识符也会出现在它们绑定名称时所处的语境，比如 let 和 fun； 然而这些绑定出现处本身并不能构成完整的项。标识符到名称的映射并不简单： 在模块任意位置里可能有多个命名空间被打开，其中 可能有多个区段变量，也 可能有局部绑定。 此外标识符也可能包含多个由点分隔的原子标识符；点 既用于分隔命名空间和它们的内容， 也用于分隔变量和字段或者是用字段表示法调用的函数。 这就造成了歧义，因为标识符 A.B.C.D.e.f 可能指代以下任意一种情况：

• 命名空间 A.B.C.D.e 中的名称 f (比如 e 当中 where 块里定义的函数项)。

• 常量 A.B.C.D.e 类型为 T，然后 作为实参被塞给函数项 T.f

• 结构常量 A.B.C.D.e 的字段 f 的投影。

• 结构常量 A 的一系列字段 B、C、D、e 的投影 B.C.D.e， 然后再作为实参塞给函数项 f，并以字段表示法书写函数项的应用。

• 如果命名空间 Q 被打开了， 那么它可能是上述任何一种情况并以 Q 作为前缀； 比如命名空间 Q.A.B.C.D.e 中的名称 f。

上述列表只列出了一小部分情况。 任给一个标识符，阐述器都必须查明 该标识符究竟指代哪（几）个名称、 尾部的内容究竟是字段还是函数项应用的字段表示。 这就是名称的解析 Resolving。

某些全局环境中的声明在第一次被引用时会被惰性创建。 如果在解析标识符的过程中 既创建了这样的声明， 又产生了对它的引用， 那么该解析就可被称作名称的实现 Realizing。 名称解析和实现的规则是相同的，因此 尽管本小节仅提及名称解析， 但它也同样适用于名称实现。

名称解析受下述因素影响：

• 预解析 Pre-Resolved 名称被附加到标识符上。

• 宏作用域被附加到标识符上。

• 作用域内的局部绑定。 作为 let rec 阐述的一部分被创建的辅助声明也囊括在内。

• 位于被当前模块传递导入的模块当中， 由 export 创建的别名。

• 当前区段作用域，尤其是当前命名空间、已打开的命名空间、区段变量。

标识符的任何前缀都可以被解析为一组名称。 那些没被包含在解析过程中的后缀随后会被当作字段投影或按字段表示法处理。 较长前缀的解析优先级高于较短的前缀；也就是说， 标识符中被当作字段表示法处理的部分会尽可能地少。 标识符前缀可能是以下列表中的任何一项， 列表当中上方条目的优先级高于下方条目：

1. 一个局部受缚变量，其名称完全等同于标识符前缀（包括宏作用域）， 其中内层局部绑定名称的优先级高于外层局部绑定。

2. 一个局部辅助声明， 其名称完全等同于标识符前缀。

3. 一个区段变量， 其名称完全等同于标识符前缀。

4. 一个全局名称，其名称要么 等同于将当前命名空间的前缀附加到标识符前缀上，要么就是 拥有一个别名，该别名位于当前命名空间的某个前缀当中（其中较长前缀的优先级高于较短前缀）。

5. 一个全局名称， 其名称完全等同于标识符前缀，且 其通过 open 命令引入作用域。

如果标识符被解析为多个名称， 那么阐述器就会尝试使用所有名称。 如果恰好有一个成功， 那么它就会被用作该标识符的含义。 如果有多个成功或者全部失败， 那么就会报错。

def x := "global"
#eval
  let x := "local"
  x
  -- 前缀 x : 2 个标识符（分别是局部受缚变量、全局常量），优先考虑局部
-- "local"

#eval
  let x := "outer"
  let x := "inner"
  x
  -- 前缀 x : 2 个标识符（都是两个局部受缚变量），优先考虑近的
-- "inner"

namespace A
def x := "A.x"
namespace B
namespace C
def x := "A.B.C.x"

#eval x
-- "A.B.C.x"
-- 前缀 x : 2 个标识符（位于命名空间 C 的前缀 A.B.C、A 中），优先考虑命名空间前缀更长的

end C
#eval x
-- "A.x"

structure A where
  y : String
deriving Repr

structure B where
  y : A
deriving Repr

def y : B := ⟨⟨"shorter"⟩⟩
def y.y : A := ⟨"longer"⟩

#eval y.y.y
-- "longer"
-- 前缀 y.y.y : 无标识符
-- 前缀 y.y : 1 个标识符（最后的 .y 为结构项投影），优先考虑标识符前缀更长的
-- 前缀 y : 1 个标识符，最后的 .y.y 为结构项投影

namespace A
def x := "A.x"
end A

namespace B
def x := "B.x"
namespace C
open A
#eval x
-- "B.x"
-- 前缀 x : 2 个标识符（分别位于当前命名空间 B.C 的前缀 B 以及已打开的命名空间 A），优先考虑当前命名空间的前缀

def A.x := "A.x"
def B.x := "B.x"
open A
open B
#eval x
-- Ambiguous term
--   x
-- Possible interpretations:
--   B.x : String  
--   A.x : String

def C.x := "C.x"
def D.x := 3
open C
open D
#eval (x : String)
-- "C.x"

13.1.1. 先导 . Leading .

如果一个标识符是以点号（.）开头的， 那么在对该标识符进行名称解析时会借助 阐述器所预期的表达式的类型，而非借助 当前命名空间以及一系列已开启的命名空间。 函数项应用的字段表示与此相关： 在对标识符进行名称解析时，名称调用的先导点号表示 Leading Dot Notation 用的是标识符的预期类型，而 字段表示法则用的是紧跟在点前面的项所被推断出的类型。

以点号 . 开头的标识符会在与预期类型同名的命名空间中被查找， 如果项的预期类型形如一个常量被应用于零个或多个实参， 那么它的命名空间就是该常量的名称。 如果项的预期类型并非常量的应用（比如一个函数项、一个元变量或者一个宇宙）， 那么它就没有命名空间。

如果标识符的名称无法在预期类型对应的命名空间中被找到， 但是该常量可以被进一步展开为另一个常量， 那么后者的命名空间就会被调查； 这个过程会被重复进行，直至 遇到某个不再是函数常量应用的东西，或者是 该常量无法再被继续展开 为止。

#eval show List Unit from .replicate 3 ()
-- [(), (), ()]

def MyList α := List α
#eval show MyList Unit from .replicate 3 ()
-- [(), (), ()]

13.2. 函数类型 Function Types

Lean 的函数类型描述的不仅仅只有函数项的定义域和陪域， 它们还为函数项被应用处的阐述提供了指导：实参当中 一部分是通过 合一或者是类型类实例合成来自动发现的， 一部分则是带默认值的可选参数， 剩下的则应是通过自定义的策略脚本来合成的。 此外它们的语法还支持函数项柯里化的缩写。

term ::= ...
  | (ident : term) → term

term ::= ...
  | term → term

term ::= ...
  | (ident* : term) → term

term ::= ...
  | (ident* : term := term) → term
term ::= ...
  | (ident* : term := by tacticSeq) → term
term ::= ...
  | {ident* : term} → term
term ::= ...
  | [term] → term
term ::= ...
  | [ident : term] → term
term ::= ...
  | ⦃ident* : term⦄ → term

13.3. 函数项的构造 Functions

函数类型下的项可通过函数抽象语法来构造。 这是通过 fun 关键字来开启的。

函数抽象在其他社群中也被称作 lambda， 源于 Alonzo Church 为其创建的记号； 又或者被称作是匿名函数， 因为它们不需要在全局环境中被命名。

尽管函数项的构造在 Lean 的核心类型理论中只允许绑定单个形参名称， 但是在高层次的 Lean 语法中函数项的写法却相当灵活。

term ::= ...
  | fun ident => term

term ::= ...
  | fun ident : term => term

通过 def 声明的函数常量最后都会被脱糖变成 fun 的形式；此外， 归纳声明会引入函数类型下新的值（比如归纳类型构造子、归纳项构造子等）， 而这些项本身无法仅由 fun 来构造。

term ::= ...
  | fun ident ident* => term
term ::= ...
  | fun ident ident* : term => term

term ::= ...
  | fun (ident* : term) =>term

本小节中提到的 => 都可以替换为 ↦。

构造函数项时也可以通过模式匹配语法来声明形参， 如此便不必再引入一个局部变量然后再对其进行模式匹配。 在模式匹配相关的小节中有详细介绍。

13.3.1. 隐式形参 Implicit Parameters

Lean 允许在构造函数项时声明隐式形参，这意味着 Lean 自己就可以为函数项提供实参，用户无需操心。 隐式形参有以下三种类别：

• 普通隐式形参 Ordinary Implicit Parameters

  普通隐式形参需要 Lean 通过合一来确定对应实参的值。换句话说， 函数项的所有被调用处都应该有一个潜在的实参值与之对应， 如此使得完整的函数项调用是类型良好的。Lean 的阐述器会尽可能地 为函数项的每个隐式形参的所有出现找到对应的值。 普通隐式形参声明用花括号（{ 和 }）包裹。

• 严格隐式形参 Strict Implicit Parameters

  严格隐式形参与普通隐式形参完全相同，唯一的区别是 只有在为函数项被调用处提供了后续的显式实参后 Lean 才会尝试去寻找该严格隐式形参对应实参的值。 严格隐式形参写在双花括号（⦃ 和 ⦄，或 {{ 和 }}）中。

• 实例隐式形参 Instance Implicit Parameters

  实例隐式形参对应的实参是通过类型类实例合成来寻找的。 实例隐式形参写在方括号（[ 和 ]）中。 与其他隐式形参不同的是，不带 : 的实例隐式形参声明指定的是 该形参的类型，而非 该形参的名称。 此外只允许为实例隐式形参指定单个名称。 另外大多数实例隐式形参声明都会直接省略形参名称， 这是因为被合成为函数项实参的实例 即便是没被显式命名在函数体内也已经是直接可用的了。

def f {α : Type} : α → α := fun x => x
def g ⦃α : Type⦄ : α → α := fun x => x

example : f 2 = g 2 := rfl

example := f
-- don't know how to synthesize implicit argument `α`
--   @f ?m.3
-- context:
-- ⊢ Type

example := g

term ::= ...
  | fun funBinder funBinder* => term

funBinder ::= ...
  | ident

funBinder ::= ...
  | ([anonymous]ident ident*)

funBinder ::= ...
  | ([anonymous]ident ident* : term)

funBinder ::= ...
  | {ident ident*}
funBinder ::= ...
  | {ident ident* : term}

funBinder ::= ...
  | ⦃ident ident*⦄
funBinder ::= ...
  | ⦃ident* : term⦄

funBinder ::= ...
  | [term]
funBinder ::= ...
  | [ident : term]

Lean 的核心语言并不会区别对待普通隐式、实例隐式和显式形参： 各种不同的函数项和函数类型在底层都是定义等价的。 这种区别只有在阐述的过程中才能被观察到。

如果一个函数项的预期类型包含了隐式形参， 但是括号绑定器中却没有显示地写出这些隐式形参， 那么最终生成的函数带有的形参数量可能会多于代码绑定器中体现出的数量。 因为隐式形参可能会被自动添加进去。

#check (fun x => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α

#check (fun {α} x => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α
#check (fun {α} (x : α) => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α
#check (fun {α : Type} (x : α) => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α

13.4. 函数项的应用 Function Application

函数项的应用通常是通过并列的方式来书写的： 实参位于函数项后，两者间至少存在一个空格。 在 Lean 的类型理论中，所有函数项都会 接收一个实参并 产生一个唯一与该实参对应的值。 所有函数项的应用本质上都是单个函数与 单个实参的组合。 多个实参的情况则通过柯里化来表示。

面向用户的高层次项语言 会将函数与一个或多个实参视为一个统一的整体，并且还 支持如 隐式实参、 可选实参、 具名实参等附加功能，外加普通的 位置实参 阐述器会将这些东西转换为核心类型理论里更为简单的模型。

term ::= ...
  | term argument+
  | term argument* ..

argument ::= ...
  | term
  | ((ident | _:ident) :=term)

核心语言中的函数类型决定了实参在最终函数项应用表达式里的位置。 函数类型里包含了它们所期待的形参的名称。在 Lean 的核心语言中， 非依值函数类型也会被编码为依值函数类型，只不过对于后者而言 形参名称不会出现在函数类型的陪域中；此外 形参名称在内部会被选中，使其无法被写成具名实参的名称， 这对预防意外捕获至关重要。

函数项的每个形参都拥有一个名称。 通过递归遍历函数项实参的不同种类， Lean 会从实参列表中选中实参。方式如下：

• 如果形参名称与具名实参的名称匹配， 那么该实参将被选中。

• 如果形参是普通隐式的， 那么一个新的元变量将被创建并被选中，元变量类型为该形参的类型。

• 如果形参是实例隐式的， 那么一个新的元变量将被创建并被插入，元变量类型为该形参的类型。 实例元变量稍后将会被合成。

• 如果形参是严格隐式的， 并且还存在任何未被选中的具名实参或位置实参， 那么一个新的元变量将被创建并被选中，元变量类型为该形参的类型。

• 如果形参是显式的，那么接下来的位置实参将被选中并被阐述。 如果没有位置实参的话，那么：

  • 如果形参为可选的， 那么其默认值将作为实参被选中。

  • 如果形参为自动的， 那么与之关联的策略脚本将被执行以构造实参。

  • 如果形参既不是可选的又不是自动的， 并且

    • 如果省略号没有， 那么一个新的变量将作为实参被选中。

    • 如果省略号存在， 那么一个新的元变量将被选中，同隐式形参的情形。

存在一个特殊情况：当 函数项的应用出现在模式中，并且 省略号存在时， 可选实参和自动实参 不会被插入， 而是会变成通用模式（_）。

如果函数项应用表达式的类型不是函数类型并且还有剩余实参， 那么会有报错； 如果所有实参都被插入完后还存在省略号， 那么缺失的实参就会被统统设置为新的元变量， 就好像这些实参是隐式的一样； 如果新变量名称是为了缺失的显式位置实参而绑定的， 那么整个函数项应用表达式就会被包裹在一个 fun 表达式中来绑定这些名称； 最后，实例合成会被启用， 元变量会被尽可能多地求解：

1. 完整的函数项应用表达式的类型会被推断出来。 这可能导致一些元变量被求解，因为类型推断过程中会发生合一。

2. 实例元变量会被合成。 只有在 被推断出的类型是个元变量，并且 该元变量是某个实例输出的参数时， 默认实例才会被使用。

3. 如果预期类型存在， 那么其会与被推断出的类型进行合一； 然而由此合一所产生的错误会被丢弃。 如果预期类型和被推断出的类型是相等的， 那么合一可以解决剩余的隐式实参元变量。 如果它们不相等，则不会抛出错误， 因为周围的阐述器可能可以插入类型强制转换或单子提升。

def sum3 (x y z : Nat) : Nat := x + y + z

#check sum3 4 3 8
-- sum3 4 3 8 : Nat

#check sum3 (x := 4) (y := 3) (z := 8)
-- sum3 4 3 8 : Nat

#check sum3 (y := 3) (x := 4) (z := 8)
-- sum3 4 3 8 : Nat

#check sum3 (y := 3) 8 (x := 4)
-- sum3 4 3 8 : Nat

#check sum3 8 (y := 3) (x := 4) 
-- sum3 4 3 8 : Nat

#check sum3 (y := 3)
-- fun x ↦ sum3 x 3 : Nat → Nat → Nat
-- fun x ↦ sum3 x 3 : (x z : Nat) → Nat

#check (sum3 (y := 3)) (x := 4)
-- (fun x ↦ sum3 x 3) 4 : Nat → Nat
-- (fun x ↦ sum3 x 3) 4 : (z : Nat) → Nat

#check let x := 8 ; sum3 (z := x)
-- let x := 8;
-- fun x_1 y ↦ sum3 x_1 y x : Nat → Nat
-- fun x_1 y ↦ sum3 x_1 y x : (x y : Nat) → Nat

#check (let x := 8 ; sum3 (z := x)) (x := 4)
-- (let x := 8;
--  fun x_1 y ↦ sum3 x_1 y x) 4
-- : Nat → Nat
-- : (y : Nat) → Nat

set_option pp.piBinderNames true in
#check let x := 8 ; sum3 (z := x)
-- let x := 8;
-- fun x_1 y ↦ sum3 x_1 y x : Nat → Nat
-- fun x_1 y ↦ sum3 x_1 y x : (x y : Nat) → Nat

可选形参和自动形参 都不是 Lean 核心类型理论内的概念。 它们分别是通过 optParam 和 autoParam 两个零件所实现的：

optParam.{u} (α : Sort u) (default : α) : Sort u

autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u

13.4.1. 广义字段表示法 Generalized Field Notation

结构字段相关的小节里 提到了结构项投影的一种简便写法，即字段表示法。 与字段表示法类似，广义字段表示法通常形如 一个项后面跟着 一个点（.）再加 一个标识符。 三者之间没有空格。

term ::= ...
  | term.ident

如果一个项的类型形如某个常量被应用于零或多个实参上， 那么无论该项是结构项还是类型类实例（它们都拥有字段）， 其作为实参传入给某个函数项的过程都可以写成字段形式。像这种将 非结构项投影函数的应用写成形如结构项投影的做法我们称作是函数项应用的广义字段表示 Generalized Field Notation。

点后面的标识符会在项类型对应的命名空间中进行查找，命名空间的名称即类型常量的名称。 如果类型并不是形如某个常量的应用（如元变量或宇宙），那么它就没有命名空间，广义字段表示法也就无法使用。 作为一种特殊情况，如果表达式是一个函数项，那么广义字段表示法就会在 Function 命名空间中进行查找； 如此 Nat.add.uncurry 其实就相当于 Function.uncurry Nat.add。

如果字段没有被找到但是常量可以被展开并产生一个类型， 那么这套分析过程就会再针对新类型继续执行。

当一个函数项被读取到时， 点前面的项会变成函数项的一个实参。具体点说， 它会变成函数项的首个类型匹配成功的显式实参。 此后函数项应用的阐述过程就和普通情况一样了。

def Username := String

def Username.validate (name : Username) : Except String Unit := do
  if " ".isPrefixOf name then
    throw "Unexpected leading whitespace"
  if name.any notOk then
    throw "Unexpected character"
  return ()
where
  notOk (c : Char) : Bool :=
    !c.isAlpha &&
    !c.isDigit &&
    !c ∈ ['_', ' ']

def adminUser : Username := "admin"

#eval "admin".validate
-- Invalid field `validate`: The environment does not contain 
-- `String.validate`, so it is not possible to 
-- project the field `validate` from an expression
--   "admin"
-- of type `String`

#eval adminUser.validate
-- Except.ok ()

#eval adminUser.any (· == 'm')
-- true

attr ::= ...
  | pp_nodot

def Nat.half : Nat → Nat
  | 0 | 1 => 0
  | n + 2 => n.half + 1
#check Nat.half Nat.zero
-- Nat.zero.half : Nat

attribute [pp_nodot] Nat.half
#check Nat.half Nat.zero
-- Nat.half Nat.zero : Nat

13.4.2. 管道语法 Pipeline Syntax

管道表示 Pipeline Notation提供了另一种书写函数项应用的方式。 连续使用的管道符号可以借助解析优先级来 实现嵌套的函数项应用（位置实参），从而不必使用嵌套的圆括号。

term ::= ...
  | term <| term

term ::= ...
  | term |> term

右管道表示直观地演示了数据的流向： 左侧的数据被传递给第一个函数项，然后 应用结果再被传递给第二个函数项，依此类推；而 左管道表示则与前者相反。

#eval "Hello!" |> String.toList |> List.reverse |> List.head!
-- '!'

#eval List.head! <| List.reverse <| String.toList <| "Hello!"
-- '!'

term ::= ...
  | term |>.ident

term ::= ...
    | term |>.fieldIdx

e |>.f arg 是 (e).f arg 的语法糖，但是后者可能要使用圆括号来避免歧义。

#eval #[1, 2, 3] |> Array.push 4
-- failed to synthesize instance of type class
--   OfNat (Array ?m.4) 4
-- numerals are polymorphic in Lean, but the numeral `4` cannot be used in a context where the expected type is
--   Array ?m.4
-- due to the absence of the instance above
-- 
-- Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

#eval #[1, 2, 3] |>.push 4
-- #[1, 2, 3, 4]

#eval #[1, 2, 3] |>.push 4 |>.reverse |>.push 0 |>.reverse
-- #[0, 1, 2, 3, 4]

13.10. 类型注解 Type Ascriptions

类型注解显式地为项添加类型信息， 它们是为 Lean 指明项的预期类型的一种方式。 被注解的这个类型必须定义等同于 Lean 基于项所处语境所推断出的类型。 类型注解不仅仅用于记录程序：

• 程序文本可能没有足够的信息用于推断项的类型。 类型注解是提供类型信息的一种方式。

• 项被推断出的类型可能与用户预期类型不符 程序文本可能包含足够的信息用于推导项的类型， 但推导出的类型可能不是用户所期待的。

• 项的预期类型会驱动 Lean 插入类型强制转换， 而类型注解是控制强制转换插入位置的一种方式。

term ::= ...
  | ([anonymous]term : term)

某些地方需要的类型注解可能会很冗长，比如策略证明或者是 do 代码块。 在上述情况中类型后缀注解可能会难以阅读，因为必须用到圆括号；此外 项的类型对于理解证明和 do 代码块是至关重要的。 在这些情况下，前缀版本的类型注解可能更易于阅读。

term ::= ...
  | show term from term

term ::= ...
  | show term by tacticSeq

example (n : Nat) := by
  induction n
  next => rfl
  next n' ih =>
    simp only [HAdd.hAdd, Add.add, Nat.add] at *
    rewrite [ih]
    rfl
-- Invalid rewrite argument: Expected an
--   equality or
--   iff proof or
--   definition name, 
-- but `ih` is a proof of
--   0 ≍ n'

example (n : Nat) := show 0 + n = n by
  induction n
  next => rfl
  next n' ih =>
    simp only [HAdd.hAdd, Add.add, Nat.add] at *
    rewrite [ih]
    rfl

example := do
  return 5
-- typeclass instance problem is stuck
--   Pure ?m.12
-- 
-- Note: Lean will not try to resolve this typeclass instance problem 
-- because the type argument to `Pure` is a metavariable. 
-- This argument must be fully determined 
-- before Lean will try to resolve the typeclass.
-- 
-- Hint: Adding type annotations and supplying implicit arguments to functions 
-- can give Lean more information for typeclass resolution. For example, 
-- if you have a variable `x` that you intend to be a `Nat`, 
-- but Lean reports it as having an unresolved type like `?m`, 
-- replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.

example := show StateM String _ from do
  return 5

类型前缀注解和 show 之间有个很重要的差异： 普通的类型后缀注解改变了项的预期类型， 这可能会改变项的阐述方式；在被阐述后 Lean 会推断出结果项的类型，并 将被推断出的类型用于后续的阐述任务。 另一方面，show 会阐述为一个项， 其推断出的类型就是被注解的类型。 广义字段表示方式 可以用来观察到这样的差异，其中被注解的类型 只有在使用 show 时才会被用于解析字段。

def Colors := List String

#check ([] : Colors)
-- [] : List String

#check (show Colors from [])
-- have this := [];
-- this : Colors

def Colors.hasYellow (cs : Colors) : Bool :=
  cs.any (·.toLower == "yellow")

#eval ([] : Colors).hasYellow
-- Invalid field `hasYellow`: The environment 
-- does not contain `List.hasYellow`, so 
-- it is not possible to project the field `hasYellow` 
-- from an expression
--   []
-- of type `List String`

#eval (show Colors from []).hasYellow
-- false

索引 Index

术语

语法

常量

定理

公理

结构

选项

属性

例子