翻译-Lean Language Reference-05-文件与模块

Lean 中最小的编译单元是单个文件， 文件可以通过文件名将其他文件导入。换句话说， 文件名和文件夹结构在 Lean 代码中是有重要意义的。

每个文件都有一个导入名称 Import Name， 导入名称由 文件的文件名和 Lean 被启动的方式 所共同决定： Lean 有一系列的根目录 Root Directory， Lean 会在当中查找代码；而 文件的导入名称则是文件名相对于根目录的路径， 文件名省略 .lean 后缀， 分隔符则是点号（.）而非斜杠（/）。 举个例子，如果 Lean 是以 Projects/MyLib/src 作为根目录启动的， 那么文件 Projects/MyLib/src/Literature/Novel/SciFi.lean 就可以通过 Literature.Novel.SciFi 来导入。

5.1. 编码与表示 Encoding and Representation

Lean 的文件都是 Unicode 文本文件，编码方式为 UTF-8。 文件内的每一行都可以通过下述两种字符串结束：要么是 单个换行符（ \n，Unicode 'LINE FEED (LF)' (U+000A)），要么则是 单个回车符后跟单个换行符（ \r\n，Unicode 'CARRIAGE RETURN (CR)' (U+000D) 后跟 'LINE FEED (LF)' (U+000A)）。 即便如此，在解析或比较文件时 Lean 都会对行末进行规范处理， 因此所有文件在被比较时都会按照每行末尾为 \n 的情况进行分析。

5.2. 具体语法 Concrete Syntax

Lean 的具体语法是可扩展的。 在像 Lean 这样的语言中， 想一次性完全描述语法是不可能的， 因为除了 新常量声明、 新归纳声明以外， 库还可能包含新的语法定义。 与其在此处完全描述语言，不如先描述整体框架，至于 各个语言构造的具体语法则会在相关章节中被详细介绍。

5.2.1. 空白 Whitespace

Lean 中的词法单元可通过任意数目的空白 Whitespace 分隔。 空白可以是 单个空格（ ，Unicode 'SPACE (SP)' (U+0020)），或者是 一个有效的换行符序列，或者是 一个注释； 而 制表符（Tab）以及 没有被新的行尾随的回车符（Carriage Return） 都不能算是有效的空白。

5.2.2. 注释 Comments

注释 Comment 是文件中 那些不是空白却会被当作空白进行处理的部分。注释有两种语法：

• 行内注释 Line Comment

  一个不会作为词法单元出现的字符串 -- 将被用于开启行内注释。 从初始的 - 开始算起到换行符为止的所有字符都会被视作是空白。

• 区块注释 Block Comment

  一个不会作为词法单元出现且没有被 - 尾随的 /- 将被用于开启区块注释。 区块注释会一直延续，直至首个用于终止的 -/ 被找到为止。 多个区块注释可以嵌套，并且只有当所有嵌套的区块注释都被终止后 -/ 才会终止最外层的区块注释。

/-- 和 /-! 开启的是文档注释而非普通注释：文档注释 同样也以 -/ 作为结束，并且 也可能含有嵌套的区块注释。 尽管文档注释看起来与普通注释很相似， 但是它们拥有自己的语法范畴，它们的有效位置由 Lean 的语法所决定。

5.2.3. 关键字与标识符 Keywords and Identifiers

一个标识符 Identifier 包含一个或多个标识符组件。 多个标识符组件由 . 分隔。

标识符组件包含 一个（类似）字母的字符或者是 一个下划线（_）， 然后尾随零或多个标识符后续字符。其中 字母字符可以是 （大、小写）英文字母，而 类似字母的字符 包含一系列非英语字母的字母脚本，包括 在 Lean 中广泛使用的希腊字母脚本、 科普特字母以及 Unicode 字母符号块中的成员；后者如 Mathematical Double-Struck 中的字符（包括 ℕ 和 ℤ）和缩写、 Latin-1 Supplement 中的字母（除去 × 和 ÷）以及 Latin Extended-A 中的字母。 标识符后续字符可以是 字母字符、 类似字母的字符、 下划线（_）、 感叹号（!）、 问号（?）、 下标或者是 单引号（'）。 另外下划线在单独出现时并不构成一个有效的标识符。

标识符的组件也可以被一对法语引号（« 和 »）所包围。 这样的标识符组件可以包含除 » 之外的任意字符， 甚至连 «、. 和换行符都可以。 引号本身不属于标识符组件的一部分，因此 «x» 和 x 表示同一个标识符。然而， «Nat.add» 是一个单一组件的标识符，而 Nat.add 则拥有两个组件。

某些潜在的标识符组件可能是保留关键字。 具体的保留关键字集合取决于当前被激活的语法扩展集合，而后者又取决于 已导入的文件集合以及 已开启的命名空间集合； 因此想要为整个 Lean 语言枚举保留关键字是不可能的。 在大多数语法语境中，这些关键字要想作为标识符组件使用就必须包裹在法语引号内。 那些允许关键字在不使用法语引号的情况下作为标识符使用的语境——比如归纳项构造子的名称， 则被称作是原始标识符 Raw Identifier 语境。

那些包含一或多个 . 的标识符（意味着它们包含多个标识符组件） 被称为分层标识符 Hierarchical Identifiers。 分层标识符 既可用于表示导入名称， 也可用于表示命名空间中的名称。

5.3. 结构 Structure

module ::=
    header command*

如果文件的头部以 module 开始，那么它就构成一个模块。 模块可以更加精细地决定哪些信息将会被暴露给用户。

5.3.1. 头部 Headers

文件的头部列出了那些在当前模块之前应该被阐述的模块。 他们包含的声明在当前模块中将会是可见的。

header ::=
    module? -- 这个 module 是关键字
    import*

header ::= ...
  | module?
    prelude
    import*

如果 prelude 关键字存在， 那么便意味着该文件是 Lean 前导库 Prelude 的一部分， 前导库是那些无需显式导入就可以使用的代码—— 它不应该在 Lean 自身实现之外被使用。

prelude ::=
    prelude -- 这个 prelude 是关键字

import ::= ...
  | import ident

import ::= ...
  | public? meta? import all? ident

5.3.2. 命令 Commands

命令 Command 是 Lean 中的顶层语句。命令可以是 归纳类型声明、 定理、 函数常量声明，也可以是 形如 open 或 variable 这样的命名空间修饰符，或者是 形如 #check 这样的交互式查询。 命令的语法可由用户扩展， 命令甚至还可以添加新的语法以用于解析后续命令。 具体的 Lean 命令不会在这里全部列出， 而是会在本手册的相应章节中进行详细介绍。

5.4. 模块与可见性 Modules and Visibility

一个模块 Module是一个文件，只不过其已主动选择 在公有信息和私有信息之间进行区分。 Lean 会确保对私有信息做出的修改不会影响到 仅导入其公有信息的下游用户。这种约束的好处有：

• 大幅缩短平均构建时间 Much-Improved Average Build Times

  如果对文件做出的修改只会影响非导出信息（例如证明、注释和文档字符串）， 那么就不会触发在这些文件外部的重新构建。即便依赖文件必须被重新构建， 那些不会被影响（由其 import 注解所决定）的文件也会被跳过。

• 掌控 API 的演变 Control Over API Evolution

  库的作者可以确信：对非导出信息做出的修改都不会影响到自己的库的下游用户。 只要一个函数的签名被暴露，那么任何涉及到该函数展开的定义等价性的东西下游用户就都无法依赖。 这意味着库作者可以随心所欲地采纳高效的算法，不必为用户代码被意外破坏而操心。

• 避免意外展开 Avoiding Accidental Unfolding

  对那些当中常量可被展开的作用域进行限制 既可以避免那些应该被更具体的定理所替代的归约， 也可以避免那些实际上并非必要的无效归约。 这提高了证明被阐述的速度。

• 更小的可执行文件 Smaller Executables

  将编译期代码和运行期代码分离 可以让 Lean 对死代码进行更积极的消除， 从而确保诸如策略这样的元程序不会进入最终的二进制文件。

• 降低内存占用 Reduced Memory Usage

  在进行导入时排除掉诸如证明之类的私有信息 可以同时提高 Lean 在构建和编辑项目时的内存使用效率。 将 mathlib4 移植到模块系统中的实践表明： 在进一步最小化导入之前就可以节省将近 50% 的内存。

模块包含两个独立的作用域： 公有作用域 Public Scope 包含那些在导入该模块的其他模块中可见的信息，而 私有作用域 Private Scope 则包含那些通常只在模块内部才可见的信息。 一些可以是私有或公有的信息的例子包括：

• 名称 Names

  常量（比如由 def 声明的常量、归纳类型构造子、归纳项构造子等） 可以是私有的或者是公有的。公有常量的类型只能引用公有名称。

• 声明 Definitions

  一个公有声明可以被暴露 Exposed，也可以不被暴露。 如果一个公有声明没有被暴露， 那么它就无法在仅能访问公有作用域的语境中被展开。 用户此时必须依赖于公有作用域中所提供的与该声明有关的定理。

每个声明都有默认的可见性规则。一般来说 所有名称默认都是私有的，除非它们是在公有区段中被声明的。 即便是公有名称也通常会将声明的主体放置在私有作用域中，并且 即便是那些位于被暴露声明中的证明也会保持私有。 各个声明命令的具体可见性规则都与声明命令本身一起在相关章节中进行介绍。

module

def greeting (name : String) : String := -- 名称私有，主体私有，未暴露
  s!"Hello, {name}"

module
import Greet.Create
def greetTwice (name1 name2 : String) : String := -- 名称私有，主体私有，未暴露
  greeting name1 ++ "\n" ++ greeting name2
-- Unknown identifier `greeting`

module

public def greeting (name : String) : String := -- 名称公有，主体私有，未暴露
  s!"Hello, {name}"

module
import Greet.Create
def greetTwice (name1 name2 : String) : String := -- 名称私有，主体私有，未暴露
  greeting name1 ++ "\n" ++ greeting name2

module

public def greeting (name : String) : String := -- 名称公有，主体私有，未暴露
  s!"Hello, {name}"

module
import Greet.Create
def greetTwice (name1 name2 : String) : String := -- 名称私有，主体私有，未暴露
  greeting name1 ++ "\n" ++ greeting name2

theorem greetTwice_is_greet_twice {name1 name2 : String} 
  :  greetTwice name1 name2 = "Hello, " ++ name1 ++ "\n" ++ "Hello, " ++ name2 
  := by simp [greetTwice, greeting] -- 名称私有，主体私有，未暴露
-- Invalid simp theorem `greeting`: 
-- Expected a definition with an exposed body

module
@[expose]
public def greeting (name : String) : String := -- 名称公有，主体私有，被暴露
  s!"Hello, {name}"

module
import Greet.Create
def greetTwice (name1 name2 : String) : String := -- 名称私有，主体私有，未暴露
  greeting name1 ++ "\n" ++ greeting name2

theorem greetTwice_is_greet_twice {name1 name2 : String} 
  :  greetTwice name1 name2 = "Hello, " ++ name1 ++ "\n" ++ "Hello, " ++ name2 
  := by simp [greetTwice, greeting, toString] -- 名称私有，主体私有，未暴露
     grind [String.append_assoc]

module

public def incr : Nat → Nat -- 名称公有，主体私有，未暴露
  | 0 => 1
  | n + 1 => incr n + 1

public theorem incr_eq_plus1 : incr = (· + 1) := by -- 名称公有，主体私有
  funext n
  induction n <;> simp [incr, *]

从普通文件过渡到模块时可以考虑使用选项 backward.privateInPublic： 在其被设置为 true 时，私有声明会被导出，即便它们的名称在将被导入进的模块中是不可访问的。 但是它们可以在自身声明所处模块的公有部分中被引用。这样的引用会导致警告， 除非选项 backward.privateInPublic.warn 被设置为 false。 这些警告可以被用来定位并最终消除这些引用，从而允许禁用 backward.privateInPublic。类似地， backward.proofsInPublic 会导致使用 by 创建的证明都变成公有的而非私有的； 这可以使 by 填充其预期类型中的元变量。 大多数 backward.proofsInPublic 的使用场景 也要求启用 backward.privateInPublic。

module

set_option backward.privateInPublic true

def drop2 (xs : List α) : List α := xs.drop 2

public def f 
  (xs : List α) 
  (transform : List α → List α := drop2) 
  : List α 
  :=transform xs
-- Private declaration `drop2` accessed publicly; 
-- this is allowed only because the `backward.privateInPublic` option is enabled. 
-- 
-- Disable `backward.privateInPublic.warn` to silence this warning.

module
import L.Defs

def xs := [1, 2, 3]

set_option pp.explicit true in
#check f xs
-- @f Nat xs (@drop2✝ Nat) : List Nat

structure Half (n : Nat) where
  val : Nat
  ok : val + val = n


abbrev two := Half.mk _ <| by
  show 2 + 2 = 4
  rfl

module         -- two 变成 reducible private
public section -- two 变成 reducible public

structure Half (n : Nat) where
  val : Nat
  ok : val + val = n


abbrev two := Half.mk _ <| by
  show 2 + 2 = 4
  rfl
-- tactic execution is stuck, goal contains metavariables
--   ?m.3 + ?m.3 = ?m.5

module         -- two 变成 reducible private
public section -- two 变成 reducible public

structure Half (n : Nat) where
  val : Nat
  ok : val + val = n

set_option backward.proofsInPublic true in
abbrev two := Half.mk _ <| by
  show 2 + 2 = 4
  rfl

module         -- two 变成 reducible private
public section -- two 变成 reducible public

structure Half (n : Nat) where
  val : Nat
  ok : val + val = n


abbrev two : Half 4 := Half.mk 2 <| by
  rfl

模块的私有作用域可以通过 all 修饰符以被导入到另一个模块中。默认情况下 只有在被导入的模块和当前模块都来自同一个 Lake 包时这才会被允许， 因为它的主要目的是允许将定义和证明分离到不同的模块中以便对库进行内部组织。 Lake 包或库的选项 allowImportAll 可以被设置为 允许其他包通过 import all 访问当前包的私有作用域。 被导入的私有作用域包括被导入模块的私有导入，其中囊括了嵌套的 import all。 如此当前模块可访问的私有作用域集合便是 import all 声明的传递闭包。

模块系统的 import all 比没有模块系统的 import 更加强大。 它使得被导入的私有定义可以直接通过名称访问，就好像 它们是在当前模块中被定义的一样。一个次要的使用场景是访问库中多个模块中的代码， 这些代码不应该被提供给下游消费者，同时也允许测试访问那些不属于公共 API 的信息。

module

public inductive Tree (α : Type u) : Type u where
  | leaf
  | branch (left : Tree α) (val : α) (right : Tree α)

public def Tree.count : Tree α → Nat
  | .leaf => 0
  | .branch left _ right => left.count + 1 + right.count

module
public import Tree.Basic
theorem Tree.count_leaf_eq_zero : count (.leaf : Tree α) = 0 := by
  simp [count]
-- Invalid simp theorem `count`: 
-- Expected a definition with an exposed body

module

public inductive Tree (α : Type u) : Type u where
  | leaf
  | branch (left : Tree α) (val : α) (right : Tree α)

public def Tree.count : Tree α → Nat
  | .leaf => 0
  | .branch left _ right => left.count + 1 + right.count

module
import all Tree.Basic
public import Tree.Basic
theorem Tree.count_leaf_eq_zero : count (.leaf : Tree α) = 0 := by
  simp [count]

5.4.1. 元程序阶段 The Meta Phase

Lean 当中的声明会产生两种表示： 一是类型理论表示，用于形式化推理； 二是编译表示，用于执行。 编译表示被用于生成机器码，但 它们也可以直接通过解释器执行。 在阐述过程中运行的代码（比如策略或宏）是声明的编译形式。 如果编译表示发生了变化，那么任何由其创建的代码 就可能不再是最新的，并且 必须被重新运行。 由于编译器执行了非平凡的优化， 对函数的传递依赖链中的任何声明所做出的修改 都可能在原则上使其编译表示失效。这意味着由模块所导出的 元程序会引入比普通声明更强的耦合。此外， 元程序会在构造普通项的过程中运行；因此在被使用之前 它们必须被完全定义和编译。毕竟，没有主体的函数定义是无法运行的。 元程序运行的时期被称为元程序阶段 Metaprogramming Phase，通常简称为 元阶段 Meta Phase。

模块不仅能区分公有信息和私有信息一样， 它们还可以区分元阶段中可用的代码和普通代码。 任何被作为编译期执行入口点的声明都必须带有 meta 修饰符， 以此表明该声明可被用作元程序。 在如 syntax、 macro、 elab 这样的内置的元程序语法中，这一切会自动完成； 但是在手动 应用如 app_delab 这样的元编程属性或者是 创建辅助声明时， 就可能需要显式地完成。 元声明只能在与执行有关的位置访问（从而调用）其他元定义； 非元定义同样也只能在与执行有关的位置访问其他非元定义。

module

open Lean

variable [Monad m] [MonadRef m] [MonadQuotation m]

partial def revArrays : Syntax → m Term
  | `(#[$xs,*]) => `(#[$((xs : Array Term).reverse),*])
  | other => do
    match other with
    | .node k i args =>
      pure ⟨.node k i (← args.mapM revArrays)⟩
    | _ => pure ⟨other⟩

macro "rev!" e:term : term => do
  revArrays e
-- Invalid `meta` definition 
-- `_aux___macroRules_termRev!__1`, `revArrays` not marked `meta`

module

open Lean

variable [Monad m] [MonadRef m] [MonadQuotation m]

meta partial def revArrays : Syntax → m Term
  | `(#[$xs,*]) => `(#[$((xs : Array Term).reverse),*])
  | other => do
    match other with
    | .node k i args =>
      pure ⟨.node k i (← args.mapM revArrays)⟩
    | _ => pure ⟨other⟩

macro "rev!" e:term : term => do
  revArrays e

#eval rev! #[1, 2, 3]
-- #[3, 2, 1]

那些原先不处于元阶段的库可通过使用 meta import 以被导入到元阶段中。 当一个模块在元阶段被导入时，其所有的定义都会在元阶段变得可用，无论它们是否被标记为 meta。 另外不存在“元元阶段”。除了可以使被导入模块的公有内容在元阶段变得可用之外， meta import 还意味着：如果被导入模块的编译表示发生了变化， 那么当前模块就必须被重新构建以确保修改过的元程序会被重新运行。 如果一个声明在两个阶段中都必须可用， 那么它就必须被置于一个独立的模块中，并且在两个阶段中都会被导入。

module

open Lean

variable [Monad m] [MonadRef m] [MonadQuotation m]

meta def toPalindrome (xs : Array α) : Array α := xs ++ xs.reverse

meta partial def palArrays : Syntax → m Term
  | `(#[$xs,*]) => `(#[$(toPalindrome (xs : Array Term)),*])
  | other => do
    match other with
    | .node k i args =>
      pure ⟨.node k i (← args.mapM palArrays)⟩
    | _ => pure ⟨other⟩

macro "pal!" e:term : term => do
  palArrays e

#check pal! (#[1, 2, 3] ++ [6, 7, 8])
-- #[1, 2, 3, 3, 2, 1] ++ [6, 7, 8] : Array Nat

public def colors := toPalindrome #["red", "green", "blue"]
-- Invalid definition `colors`, 
-- may not access declaration `toPalindrome` marked as `meta`

module

public def toPalindrome (xs : Array α) : Array α := xs ++ xs.reverse

module

meta import Phases.Pal
import Phases.Pal

open Lean

variable [Monad m] [MonadRef m] [MonadQuotation m]

meta partial def palArrays : Syntax → m Term
  | `(#[$xs,*]) => `(#[$(toPalindrome (xs : Array Term)),*])
  | other => do
    match other with
    | .node k i args =>
      pure ⟨.node k i (← args.mapM palArrays)⟩
    | _ => pure ⟨other⟩

local macro "pal!" e:term : term => do
  palArrays e

#check pal! (#[1, 2, 3] ++ [6, 7, 8])

public def colors := toPalindrome #["red", "green", "blue"]

另外如果被导入的声明可能会在当前模块之外的编译期被执行（也就是说 该声明可以被当前模块中的某个公有元声明访问），那么该导入就必须是公有的。 我们可以使用 public meta import 来实现这一点。 如果声明已经被声明为 meta，那么 public import 就足够了。

与声明有所不同的是，大多数元程序默认都是公有的，这意味着 在实际情况中大多数 meta import 都是 public 的。 当然也有例外情况，比如一个声明被导入仅仅是为了能在局部元程序（比如 那些用 local syntax、local macro 或 local elab 声明的东西）中使用。

As a guideline, it is usually preferable to keep the amount of meta annotations as small as possible. This avoids locking otherwise-reusable declarations into the meta phase and it helps the build system avoid more rebuilds. Thus, when a metaprogram depends on other code that does not itself need to be marked meta, this other code should be placed in a separate module and not marked meta. Only the final module that actually registers a metaprogram needs the helpers to be in the meta phase. This module should use public meta import to import those helpers and then define its metaprograms using built-in syntax like elab, using meta def, or using meta section.

索引 Index

术语

语法

常量

定理

公理

归纳

结构

类

选项

属性

例子