翻译-Lean Language Reference-07-常量声明

下述命令在 Lean 中用于名称定义：

• def

• abbrev

• example

• theorem

• opaque

上述所有命令会根据签名对一个项进行展开。 除了 example 命令会丢弃结果以外， 其他命令都会将 Lean 核心语言中的结果表达式保存到环境中以供将来使用。 instance 命令的用法在实例声明一节中会详细介绍。

7.1. 声明修饰器 Modifiers

常量声明可以接收一连串的声明修饰器 Modifier，这些修饰器都是可选的。 修饰器会改变常量声明的某些解释。例如： 它们可以为常量添加文档注释，或者是 改变常量的作用域。 修饰器的顺序是固定的， 但并非所有声明都可以接纳每种修饰器。

declModifiers ::=
  docComment?
  attributes?
  visibility?
  noncomputable?
  unsafe?
  (partial | nonrec)?

文档注释 Documentation Comment 用于为其所修饰的声明提供源码内 API 文档。 文档注释其实不是普通注释： 如果将文档注释放在无法作为文档被处理的位置， 那么就会引发语法错误。此外在某些 需要提供文本内容但是使用字符串转义又会过于繁琐的地方 也可以使用文档注释——比如 #guard_msgs 命令所期望的消息内容，

docComment ::=
  /--
  ...
  -/

属性是一个可扩展的修饰器集合，用于将额外的信息与声明关联起来。 关于属性的详细说明请参见专门的章节。

如果一个声明被标记为 private， 那么对应的名称在声明所处模块之外是无法被访问的。 如果一个声明被标记为 protected， 那么即便其命名空间被打开也不会将其引入到作用域中。

被 noncomputable 修饰的函数 不会被编译，也 无法被执行。 满足以下情况的函数肯定是不可计算的： 如果它们使用了不可计算的推理原则来产生与其返回结果相关的数据——比如 选择公理 排中律，或者是 如果它们使用了 Lean 中的某些特性， 这些特性为了效率原因而被排除在代码生成之外， 比如归纳项的递归子。 即便不可计算函数无法被编译和执行， 他们在规范和推理中依然非常有用。

尽管不可计算函数无法被编译和执行， 但是在规约 Specification 和推理中它们却非常有用，

unsafe 标记可以使 声明免于内核检查，并且允许它 访问那些可能破坏 Lean 安全性保证的特性。 使用 unsafe 标记 必须非常小心谨慎，并且 最好确保自己对 Lean 内部机制有透彻的理解。

7.2. 头部、类型签名 Headers and Signatures

常量声明的头部 Header 包含了 待声明的常量名称，如果可能的话 还会附带其类型签名。 常量的类型签名 Signature 指定了常量的使用方式。 类型签名中所包含的信息不仅只有 类型本身，还包括诸如 宇宙层级形参以及 可选形参的默认值等信息。 在 Lean 中， 类型签名在不同种类的常量声明里 都是以一致的格式书写的。

7.2.1. 常量名称 Declaration Names

大部分常量声明的头部都以待声明的常量名称开头， 名称后可能还跟着与之对应的类型签名——即 常量的形参和函数返回类型。 待声明名称包含一个标识符，其后 可能还尾随一个或多个宇宙层级形参。

declId ::=
    ident

declId ::= ...
  | ident.{ident, ident,*}

example 不包含待声明名称；此外对实例声明而言待声明名称是可选的。

7.2.2. 类型签名 Parameters and Types

在待声明名称之后可能会出现类型签名。 类型签名指定了 待声明常量的形参以及 函数返回类型。

declSig ::=
    (ident | hole | bracketedBinder)* : term

optDeclSig ::=
    (ident | hole | bracketedBinder)* (: term)?

形参可以是以下三种形式中的任意一种：

• 一个标识符 ident，被用于命名一个形参，但并不提供类型信息。 这些形参的类型推导必须在阐述中完成。

• 一个下划线 _，用于指代一个在局部作用域中无法通过名称访问的形参。 这些形参的类型推导也必须在阐述中完成。

• 一个括号绑定器 bracketedBinder，其可以指定一个或多个形参的各个方面，包括它们的 名称、类型、默认值，以及它们是否为 显式的、 隐式的、 严格隐式的、 实例隐式的。

7.2.3. 括号绑定器 Bracketed Parameter Bindings

非标识符且非下划线的形参统称为括号绑定器 Bracketed Binder， 因为它们的每一种语法形式都含有方括号、花括号或圆括号。 所有括号绑定器都指定了形参的类型， 并且大多数都会包含形参的名称。 那些使用下划线 (_) 代替名称的形参则是匿名形参。

bracketedBinder ::=
    ((ident | hole) (ident | hole)* : term)

bracketedBinder ::= ...
  | ((ident | hole) (ident | hole)* : term := term)

bracketedBinder ::= ...
  | {(ident | hole) (ident | hole)* : term}

bracketedBinder ::= ...
  | ⦃(ident | hole) (ident | hole)* : term⦄

bracketedBinder ::= ...
  | {{(ident | hole) (ident | hole)* : term}}

bracketedBinder ::= ...
  | [(ident :)? term]

形参始终处于冒号后的返回结果类型注解表达式的作用域内， 它们同样也处于声明主体表达式的作用域内；与之相对的是， 仅在返回结果类型注解表达式中绑定的名称只在该区域内有效。 可见形参的名称实际上被使用了两次，分别

• 作为返回结果类型注解表达式中的名称—— 作为依赖函数类型的一部分被绑定；

• 作为声明主体表达式中的名称—— 它们被一个 fun 所绑定。

def add (n : Nat) : (k : Nat) → Nat
  | 0 => n
  | k' + 1 => 1 + add n k'

def mustBeEqual (n : Nat) : (k : Nat) → n = k → String :=
  fun _ =>
    fun
    | rfl => s!"Equal - both are {n}!"

函数项应用相关章节内有 可选、 自动、 隐式以及 实例隐式 形参的详细说明。

7.2.4. 自动声明的隐式形参 Automatic Implicit Parameters

类型签名中出现的其他未绑定名称在默认情况下可能会被自动转换为隐式形参。 这些行为被称作是 隐式形参的自动声明 Automatic Declaration of Implicit Parameter。 这种情况会在下述情况中发生： 形参不是正在被应用的函数，并且 形参的类型以及它们的任何顺序约束 在类型签名中都有充足的信息来推断。 这个过程是迭代的： 如果新插入隐式形参的类型推断包含了无法被唯一确定的依赖项， 那么这些依赖项将进一步被替换为隐式形参。

至于那些无法与类型签名中写出的名称对应上的的隐式形参， 它们将会被自动赋予类似于证明中无法访问的假设的名称， 这些名称无法被访问。在类型签名中它们会被加上一个匕首符号 (✝) 。 这可以防止 Lean 随意选择的名称成为 API 的一部分， 从而被用作具名参数。

set_option autoImplicit true

def map (f : α → β) : (xs : List α) → List β
  | [] => []
  | x :: xs => f x :: map f xs

#check List.map
-- List.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} 
--   (f : α → β) (l : List α) : 
--   List β

set_option autoImplicit false

def map (f : α → β) : (xs : List α) → List β
  | [] => []
  | x :: xs => f x :: map f xs
-- Unknown identifier `α`
-- 
-- Note: It is not possible to treat `α` 
-- as an implicitly bound variable here 
-- because the `autoImplicit` option is set to `false`.
-- 
-- Unknown identifier `β`
-- 
-- Note: It is not possible to treat `β` 
-- as an implicitly bound variable here 
-- because the `autoImplicit` option is set to `false`.

set_option autoImplicit false

def map.{u, v} {α : Type u} {β : Type v}
    (f : α → β) :
    (xs : List α) → List β
  | [] => []
  | x :: xs => f x :: map f xs

set_option autoImplicit false

def map {α β} (f : α → β) :
    (xs : List α) → List β
  | [] => []
  | x :: xs => f x :: map f xs

set_option autoImplicit true
structure AtLeast (i : Fin n) where
  val : Nat
  val_gt_i : val ≥ i.val

def AtLeast.add (x y : AtLeast i) : AtLeast i :=
  AtLeast.mk (x.val + y.val) <| by
    cases x
    cases y
    dsimp only
    omega

#check AtLeast.add
-- AtLeast.add {n✝ : Nat} {i : Fin n✝} 
-- (x y : AtLeast i) : AtLeast i

隐式形参自动声明会在 由区段变量声明所导致的形参插入之后发生。 区段变量所对应的形参具有与对应变量相同的名称，即便 它们无法与类型签名中直接写出的名称对应上，并且 禁用隐式形参自动声明也不会影响那些对应于区段变量的形参； 然而在隐式形参自动声明功能被启用时， 那些包含其他原本未受绑定的变量的区段变量声明会接收额外的区段变量， 这些区段变量遵循与隐式形参相同的规则。

隐式形参自动声明是由两个选项控制的； 默认情况下隐式形参自动声明是宽松的， 这意味着任何未绑定的标识符都可能成为自动插入的候选项。 将 relaxedAutoImplicit 选项设置为 false 会 禁用宽松模式，并且在选择自动插入的候选项时 只会考虑那些由单个字符后跟零个或多个数字组成的标识符。

set_option autoImplicit true
set_option relaxedAutoImplicit true

inductive Answer where
  | yes
  | maybe
  | no

def select (choices : α × α × α) : Asnwer →  α -- Asnwer 这里有问题
  | .yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2
-- Invalid dotted identifier notation: 
-- The expected type of `.yes`
--   Asnwer
-- is not of the form `C ...` or `... → C ...` 
-- where C is a constant

select.{u_1, u_2}
  {α : Type u_1}
  {Asnwer : Sort u_2}
  (choices : α × α × α) :
  Asnwer → α

set_option autoImplicit true
set_option relaxedAutoImplicit false

def select (choices : α × α × α) : Asnwer →  α -- Asnwer 这里有问题
  | .yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2
-- Unknown identifier `Asnwer`
-- 
-- Note: It is not possible to treat `Asnwer` as an implicitly bound variable here 
-- because it has multiple characters while the `relaxedAutoImplicit` option 
-- is set to `false`.

set_option autoImplicit true
set_option relaxedAutoImplicit false

def select (choices : α × α × α) : Answer →  α
  | .yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2

set_option autoImplicit false
set_option relaxedAutoImplicit false

def select (choices : α × α × α) : Answer →  α -- 四个 α 有问题
  | .yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2
-- Unknown identifier `α`
-- 
-- Note: It is not possible to treat `α` as an implicitly bound variable here 
-- because the `autoImplicit` option is set to `false`.

7.3. 常量声明 Definitions

常量声明会将一个新的常量添加到全局环境中，该常量的名称对应于一个项。 作为 Lean 核心语言中定义等价性的一部分，这个新的常量可以通过 δ 归约 展开为它所对应的定义。在阐述器中，这种替换是由常量的可归约性所控制的。 新的常量可以是宇宙多态的，在这种情况下， 每个实例都可以通过不同的宇宙层级参数来实例化它。

函数常量声明可以是递归的。为了保持 Lean 类型理论 作为逻辑的一致性，递归函数要么 得对内核不透明（比如将它们声明为 partial），要么就 得被证明满足可以停机性（证明需要用到递归定义一节中介绍的策略）。

常量声明的头部和主体会一起被阐述。 如果头部没有被完整地指定（比如缺少了形参类型或者是缺少了返回结果类型）， 那么主体可能会提供足够的信息使得阐述器可以重建缺失的部分。然而， 实例隐式形参的指定必须在头部或者是作为区段变量完成。

command ::= ...
  | declModifiers
    def declId optDeclSig := term

command ::= ...
  | declModifiers
    def declId optDeclSig
      (| term => term)*

command ::= ...
  | declModifiers
    def declId optDeclSig where
      structInstField*

command ::= ...
  | declModifiers
    abbrev declId optDeclSig := term

command ::= ...
  | declModifiers
    abbrev declId optDeclSig
      (| term => term)*

command ::= ...
  | declModifiers
    abbrev declId optDeclSig where
      structInstField*

不透明常量 Opaque Constant 是那些在内核中不受 δ 归约影响的已声明常量。 它们在指定某个函数的存在性时非常有用。 与公理有所不同的是，不透明声明只能用于居留类型， 因此它们不会引入不一致性；同样 与公理有所不同的是，类型的居留项会被用于编译后的代码中。 implemented_by 属性可以用来指示编译器 在编译不透明常量时 发起对某个其他函数的调用。

command ::= ...
  | declModifiers
    opaque declId declSig := term

command ::= ...
  | declModifiers
    opaque declId declSig

7.4. 定理声明 Theorems

由于命题是类型， 其下的居留项可被视为证明， 因此从技术层面讲定理和定义非常相似。然而， 由于它们的使用场景有很大不同，在许多细节上它们也有所区别：

• 定理的陈述必须是一个命题，而 常量的类型可以位于任意宇宙中。

• 定理的头部（也就是定理的陈述）会在声明主体被阐述之前被完整地阐述。 区段变量只有在头部中被提及时（或者它们的依赖项被提及时）才会成为定理的形参。 这可以预防更改证明时不小心改动定理陈述的情形。

• 定理是默认不可归约的。 因为同一命题的所有证明都是定义等价的， 基本没必要去展开一个定理。

定理可能是递归的，前提是它们满足与递归函数声明相同的条件。不过 更常见的做法是使用如 induction 或 fun_induction 这样的策略。

command ::= ...
  | declModifiers
    theorem declId declSig := term

command ::= ...
  | declModifiers
    theorem declId declSig
      (| term => term)*

command ::= ...
  | declModifiers
    theorem declId declSig where
      structInstField*

7.5. 例子声明 Example Declarations

例子也是一种常量声明，只不过 其是匿名的，并且 会被阐述然后被丢弃。例子 在开发过程中用于增量测试，并且 可以让文件更容易理解。

command ::= ...
  | declModifiers
    example optDeclSig := term

command ::= ...
  | declModifiers
    example optDeclSig
      (| term => term)*

command ::= ...
  | declModifiers
    example optDeclSig where
      structInstField*

7.6. Recursive Definitions

索引 Index

术语

语法

常量

定理

公理

归纳

结构

类型类

选项

属性

例子