与Lean的交互

您现在已经熟悉了依赖类型理论的基本知识，既作为定义数学对象的语言，也作为构建证明的语言。您唯一缺少的是定义新数据类型的机制。在下一章中，我们将填补这个空白，引入“归纳数据类型”的概念。但是首先，在本章中，我们暂时离开类型论的机制，探索与Lean交互的一些实用方面。

这里的信息并不都是对您立即有用的。我们建议您快速浏览本节以了解Lean的功能，并根据需要再回头查看。

导入文件

Lean的前端目标是解释用户输入，构造形式化表达式，并检查其形式是否正确。Lean还支持使用各种编辑器，提供持续的检查和反馈。更多信息可以在 Lean文档页上找到。

Lean标准库中的定义和定理分布在多个文件中。用户可能还希望使用其他库，或者跨多个文件开发自己的项目。当Lean启动时，它会自动导入Init文件夹中的库内容，其中包括一些基本定义和构造。因此，我们在这里介绍的大部分示例都可以直接使用。

但是，如果要使用其他文件，您需要手动导入它们，即在文件开头使用import语句。例如，命令

import data.nat.basic

导入了Lean的标准库中的data.nat.basic文件中的内容。

import Bar.Baz.Blah

引入文件 Bar/Baz/Blah.olean，其中描述被解释为相对于 Lean 的 搜索路径 的路径。关于如何确定搜索路径的信息可以在文档页上找到。默认情况下，它包括标准库目录以及（在一些上下文中）用户本地项目的根目录。也可以指定相对于当前目录的导入；例如，导入是传递的。换句话说，如果你导入了 Foo 和 Foo 导入了 Bar，那么你也可以访问 Bar 的内容，不需要显式导入它。

关于节的更多信息

Lean 提供了各种节区的机制来帮助结构化一个理论。你在变量和节区中看到，section 命令不仅可以将理论的相关元素进行分组，还可以声明作为定义和定理的参数的变量，根据需要插入。请记住，“variable”命令的目的是声明用于定理的变量，如下面的例子所示：

section
variable (x y : Nat)

def double := x + x

#check double y
#check double (2 * x)

attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm

theorem t1 : double (x + y) = double x + double y := by
  simp [double]

#check t1 y
#check t1 (2 * x)

theorem t2 : double (x * y) = double x * y := by
  simp [double, Nat.add_mul]

end

"double"的定义不需要将"x"声明为参数；LEAN会自动检测到这种依赖并自动插入。同样，LEAN也会自动检测到在"t1"和"t2"中出现的"x"，并在那里自动插入。请注意，"double"的参数中没有"y"。变量仅在实际使用它们的声明中包含。

更多关于命名空间

在LEAN中，标识符由分层的名称表示，例如"Foo.Bar.baz"。在命名空间中，我们看到LEAN提供了处理层级名称的机制。命令"namespace foo"会在每个定义和定理的名称前面加上"foo"，直到遇到"end foo"为止。然后，命令"open foo"会为以"foo"为前缀的定义和定理创建临时的别名。

namespace Foo
def bar : Nat := 1
end Foo

open Foo

#check bar
#check Foo.bar

下面是LEAN 定理证明定义的翻译:

定义1.1 定理

一个“定理”是一个希望通过具体推演来证明的断言。我们在一个解释内容的上下文中讨论定理，在这个上下文中，我们相信至少有一种方法可以根据定理是否正确的情况来评判。一个定理的“证明”是一个使定理被普遍接受的论据。

定义1.2 命题

一个“命题”是一个可以被证明为真或假的断言。在一段特定的解释内容的上下文中，我们可以根据命题是否正确对其进行判断。命题的证明是一个论据，通过该论据我们可以得出命题的真实性或虚假性。

定义1.3 假设

一个“假设”是一个我们暂时认为是真的断言，但我们并不确定它是否真实。当我们提出假设时，我们接受它的约束，并将其用于进一步的推理和论证。在证明中，我们会明确列出所有的假设，并在推理的每一步中采用恰当的假设。

定义1.4 定理证明的结构

一个定理证明由以下几个部分组成：

1. 证明的起点(基础)：一个证明的起点是一个已知的、被普遍接受的事实或真理，它不需要被证明。我们可以从一个证明的起点开始进行推理。
2. 步骤：一个证明是由一系列有条理的步骤组成的。每一步都使用推理规则将某个断言转化为另一个断言。每一步的正确性都可以被证明，并且必须根据前一步的结果建立。
3. 结论：一个证明的结论是一个表明定理确认为真的最后的断言。存在许多可能的推理路径可以得出同一个结论，但是在证明中我们只需要关注一个。

定义1.5 推理规则

推理规则是一种逻辑工具，用于在论证过程中从给定断言推导出新的断言。常见的推理规则包括引入和排除规则。推理规则必须合乎逻辑并且正确使用。

定义1.6 证明的策略

证明的策略是指在证明过程中应用的推理规则和方法。选择一个适当的策略是证明定理的关键。了解不同的策略和如何运用它们对于有效的证明是至关重要的。

定义1.7 反证法

反证法是一种证明方法，其中我们假设定理不成立，然后通过推理证明这个假设是不可行的。如果我们最终得出了一个矛盾的结论或违反已知事实的结果，则我们可以确定定理是成立的。

定义1.8 归纳证明

归纳证明是一种证明方法，其中我们首先证明一个断言在某个基础情形下成立，然后在递归地证明该断言在所有后续情形下也成立。归纳证明常用于处理具有可复制结构的问题，并且需要通过基础情形的推理来逐步扩展到更复杂的情形。

定义1.9 直接证明

直接证明是一种证明方法，其中我们根据定理的前提使用推理规则逐步推导出结论。直接证明通常是最常见和直观的证明方法之一。

补充说明：

上述定义和解释是根据 LEAN 定理证明的一些常见术语和概念进行描述。这些定义和概念为理解证明的结构和方法提供了基础。在实际应用中，根据具体问题的特点和要求，证明的方法和策略可能会有所不同。在进行定理证明时，确保逻辑正确性、严谨性和清晰性是非常重要的。

def Foo.bar : Nat := 1

在LEAN中，"LEAN"被视为一个宏，并展开为

namespace Foo
def bar : Nat := 1
end Foo

尽管定理和定义的名称必须是唯一的，但用于标识它们的别名可以不唯一。当我们打开一个命名空间时，标识符可能是模糊的。Lean试图使用类型信息来消除上下文中的歧义，但您始终可以通过给出完整的名称来消除歧义。为此，字符串 _root_ 是对空前缀的显式描述。

def String.add (a b : String) : String :=
  a ++ b

def Bool.add (a b : Bool) : Bool :=
  a != b

def add (α β : Type) : Type := Sum α β

open Bool
open String
-- #check add -- ambiguous
#check String.add           -- String → String → String
#check Bool.add             -- Bool → Bool → Bool
#check _root_.add           -- Type → Type → Type

#check add "hello" "world"  -- String
#check add true false       -- Bool
#check add Nat Nat          -- Type

我们可以使用 protected 关键字阻止创建较短的别名：

protected def Foo.bar : Nat := 1

open Foo

-- #check bar -- error
#check Foo.bar

这通常用于像 Nat.rec 和 Nat.recOn 这样的名称，以防止常见名称的重载。

open 命令允许多种变体。命令可以接受以下参数：

open Nat (succ zero gcd)
#check zero     -- Nat
#eval gcd 15 6  -- 3

创建仅对列出的标识符创建别名。命令

open Nat hiding succ gcd
#check zero     -- Nat
-- #eval gcd 15 6  -- error
#eval Nat.gcd 15 6  -- 3

在 Nat 命名空间中为除了所列标识符之外的所有内容创建别名。

open Nat renaming mul → times, add → plus
#eval plus (times 2 2) 3  -- 7

创建别名把 Nat.mul 重命名为 times，把 Nat.add 重命名为 plus。

有时候从一个命名空间导出别名到另一个命名空间或顶层是很有用的。这个命令可以实现：

export Nat (succ add sub)

在当前命名空间中为 succ，add 和 sub 创建别名，以便在打开命名空间时可以使用这些别名。如果该命令在命名空间之外使用，则这些别名将导出到顶层命名空间。

属性

Lean 的主要功能是将用户输入转换为形式化表达式，然后通过内核进行检查，最后存储在环境中以供以后使用。但是，一些命令对环境产生其他影响，例如为环境中的对象分配属性、定义符号表示法或声明类型类的实例，如 Type Classes 章节 中所述。这些命令大多具有全局影响，也就是说，它们不仅在当前文件中生效，而且在导入了该文件的任何文件中都生效。但是，这种命令通常支持 local 修饰符，表示它们仅在当前section 或 namespace 关闭之前，或当前文件结束之前生效。

在 Using the Simplifier 章节 中，我们看到定理可以使用 [simp] 属性进行注释，这样它们就可以被简化器使用。下面的例子定义了列表上的前缀关系，证明了该关系是自反的，并将 [simp] 属性赋予了该定理。

def isPrefix (l₁ : List α) (l₂ : List α) : Prop :=
  ∃ t, l₁ ++ t = l₂

@[simp] theorem List.isPrefix_self (as : List α) : isPrefix as as :=
  ⟨[], by simp⟩

example : isPrefix [1, 2, 3] [1, 2, 3] := by
  simp

之后，简化器通过将 isPrefix [1, 2, 3] [1, 2, 3] 重写为 True 来证明它。

也可以在定义之后的任何时候分配属性：

# def isPrefix (l₁ : List α) (l₂ : List α) : Prop :=
#  ∃ t, l₁ ++ t = l₂
theorem List.isPrefix_self (as : List α) : isPrefix as as :=
  ⟨[], by simp⟩

attribute [simp] List.isPrefix_self

在所有这些情况下，属性在引入声明所在文件的任何文件中都保持有效。添加local修饰符限制了作用域：

# def isPrefix (l₁ : List α) (l₂ : List α) : Prop :=
#  ∃ t, l₁ ++ t = l₂
section

theorem List.isPrefix_self (as : List α) : isPrefix as as :=
  ⟨[], by simp⟩

attribute [local simp] List.isPrefix_self

example : isPrefix [1, 2, 3] [1, 2, 3] := by
  simp

end

-- Error:
-- example : isPrefix [1, 2, 3] [1, 2, 3] := by
--  simp

另一个例子中，我们可以使用 instance 命令将符号 ≤ 赋予关系 isPrefix。该命令将在 第10章 类型类 中详细解释，它通过向关联的定义添加一个 [instance] 属性来实现。

def isPrefix (l₁ : List α) (l₂ : List α) : Prop :=
  ∃ t, l₁ ++ t = l₂

instance : LE (List α) where
  le := isPrefix

theorem List.isPrefix_self (as : List α) : as ≤ as :=
  ⟨[], by simp⟩

该定理的证明也可以是本地的：

**定理：LEAN 定理证明可以在本地完成。**

*证明：*
为了证明这个定理，我们需要展示一个本地证明的步骤。假设我们有一个 LEAN 环境设置在我们的本地计算机上。

1. 在本地计算机上安装 LEAN 环境。可以从 LEAN 的官方网站下载并按照说明进行安装。

2. 创建一个 LEAN 项目。可以使用 LEAN 提供的命令行工具 `leanproject` 来创建一个新的项目。

3. 在项目中创建一个新的 LEAN 文件并命名为 `proof.lean`。

4. 在 `proof.lean` 文件中，导入需要用到的 LEAN 库。

   ```lean
   import tactic

5. 添加一个定理声明并给定其名称和陈述。例如：

   theorem my_theorem : 1 + 1 = 2 :=
   begin
     sorry
   end
   

   这个定理声明声明了 "1 + 1 = 2"。

6. 编写证明脚本。使用 tactic 编写证明脚本的过程类似于将传统的数学证明转化为形式化证明的步骤。例如：

   theorem my_theorem : 1 + 1 = 2 :=
   begin
     exact rfl
   end
   

   这个证明脚本使用了 exact rfl 来表示证明是显然的。

7. 运行 LEAN 环境中的验证器。使用 LEAN 提供的命令行工具 lean 来验证证明脚本的正确性。

8. 如果验证通过，那么我们成功地在本地完成了 LEAN 定理证明。如果验证失败，可以根据错误提示进行修正。

因此，我们证明了该定理可以在本地完成，只需在本地计算机设置 LEAN 环境并按照上述步骤进行操作即可。

通过以上步骤，我们证明了该定理可以在本地完成。

```lean
# def isPrefix (l₁ : List α) (l₂ : List α) : Prop :=
#   ∃ t, l₁ ++ t = l₂
def instLe : LE (List α) :=
  { le := isPrefix }

section
attribute [local instance] instLe

example (as : List α) : as ≤ as :=
  ⟨[], by simp⟩

end

-- Error:
-- example (as : List α) : as ≤ as :=
--  ⟨[], by simp⟩

在下面的 注释 部分，我们将讨论 Lean 的定义符号的机制，并且可以看到它们也支持 local 修饰符。然而，在 设置选项 部分中，我们将讨论 Lean 的设置选项的机制，它不遵循这个模式：选项只能在局部范围内进行设置，也就是说，它们的作用域始终限定在当前节或当前文件中。

更多关于隐含参数

在 隐含参数 部分中，我们看到如果 Lean 将一个项 t 的类型显示为 {x : α} → β x，那么花括号表示 x 已被标记为 隐含参数。这意味着每当你写下 t 时，会插入一个占位符或者说“空洞”，这样 t 就会被替换为 @t _。如果你不希望这样发生，你必须写成 @t。

请注意，隐含参数会被急切地插入。假设我们定义一个带有如上所示参数的函数 f (x : Nat) {y : Nat} (z : Nat)。然后，当我们不带其他参数写出表达式 f 7 时，它将被解析为 f 7 _。Lean 提供了一个更弱的注解 {{y : Nat}}，它指定一个占位符只能在后续的显式参数之前添加。这个注解还可以用 ⦃y : Nat⦄ 的形式来写，其中 unicode 括号分别键入为 \{{ 和 \}}。使用这个注解，表达式 f 7 将被解析为原样，而 f 7 3 将被解析为 f 7 _ 3，正如使用强注解时一样。

为了说明这种差异，考虑下面的例子，它展示了一个自反的欧几里得关系既是对称的又是传递的。

def reflexive {α : Type u} (r : α → α → Prop) : Prop :=
  ∀ (a : α), r a a

def symmetric {α : Type u} (r : α → α → Prop) : Prop :=
  ∀ {a b : α}, r a b → r b a

def transitive {α : Type u} (r : α → α → Prop) : Prop :=
  ∀ {a b c : α}, r a b → r b c → r a c

def euclidean {α : Type u} (r : α → α → Prop) : Prop :=
  ∀ {a b c : α}, r a b → r a c → r b c

theorem th1 {α : Type u} {r : α → α → Prop}
            (reflr : reflexive r) (euclr : euclidean r)
            : symmetric r :=
  fun {a b : α} =>
  fun (h : r a b) =>
  show r b a from euclr h (reflr _)

theorem th2 {α : Type u} {r : α → α → Prop}
            (symmr : symmetric r) (euclr : euclidean r)
            : transitive r :=
  fun {a b c : α} =>
  fun (rab : r a b) (rbc : r b c) =>
  euclr (symmr rab) rbc

theorem th3 {α : Type u} {r : α → α → Prop}
            (reflr : reflexive r) (euclr : euclidean r)
            : transitive r :=
 @th2 _ _ (@th1 _ _ reflr @euclr) @euclr

variable (r : α → α → Prop)
variable (euclr : euclidean r)

#check euclr  -- r ?m1 ?m2 → r ?m1 ?m3 → r ?m2 ?m3

结果被分解为以下几个小步骤：th1 证明了一个既是反身性又是欧几里得性的关系是对称的，而 th2 证明了一个既是对称性又是欧几里得性的关系是传递的。然后 th3 结合了这两个结果。但请注意，我们必须手动禁用 th1、th2 和 euclr 中的隐式参数，否则会插入太多的隐式参数。如果使用弱隐式参数，问题将得到解决：

def reflexive {α : Type u} (r : α → α → Prop) : Prop :=
  ∀ (a : α), r a a

def symmetric {α : Type u} (r : α → α → Prop) : Prop :=
  ∀ {{a b : α}}, r a b → r b a

def transitive {α : Type u} (r : α → α → Prop) : Prop :=
  ∀ {{a b c : α}}, r a b → r b c → r a c

def euclidean {α : Type u} (r : α → α → Prop) : Prop :=
  ∀ {{a b c : α}}, r a b → r a c → r b c

theorem th1 {α : Type u} {r : α → α → Prop}
            (reflr : reflexive r) (euclr : euclidean r)
            : symmetric r :=
  fun {a b : α} =>
  fun (h : r a b) =>
  show r b a from euclr h (reflr _)

theorem th2 {α : Type u} {r : α → α → Prop}
            (symmr : symmetric r) (euclr : euclidean r)
            : transitive r :=
  fun {a b c : α} =>
  fun (rab : r a b) (rbc : r b c) =>
  euclr (symmr rab) rbc

theorem th3 {α : Type u} {r : α → α → Prop}
            (reflr : reflexive r) (euclr : euclidean r)
            : transitive r :=
  th2 (th1 reflr euclr) euclr

variable (r : α → α → Prop)
variable (euclr : euclidean r)

#check euclr  -- euclidean r

有一种隐式参数用方括号 [ 和 ] 表示，它们用于类型类，如在类型类章节中所解释的。

表示法

Lean 中的标识符可以包含任何字母数字字符，包括希腊字符（除了 ∀ , Σ 和 λ ，它们在依赖类型理论中有特殊含义）。它们还可以包含下标，在输入所需的下标字符之后输入 \_。

Lean 的解析器是可扩展的，也就是说，我们可以定义新的表示法。

Lean 的语法可以在每个级别上由用户进行扩展和定制，从基本的“mixfix”表示法到定制的展开器。实际上，所有内置的语法都是使用相同的机制和 API 进行解析和处理的。在本节中，我们将描述和解释各种扩展点。

虽然引入新的表示法在编程语言中是相对少见的特性，有时甚至因其可能模糊代码而受到批评，但它是形式化的无价工具，可以简洁地表示所述领域的已建立惯例和表示法。超越基本表示法，Lean 的能力通过 (行为良好的) 宏将常见的样板代码分解出来，并嵌入整个定制的领域专用语言（DSL）来以文本方式高效和可读地编码子问题，可以极大地有益于程序员和证明工程师。

表示法和优先级

最基本的语法扩展命令允许引入新的（或重载现有的）前缀、中缀和后缀运算符。

infixl:65   " + " => HAdd.hAdd  -- left-associative
infix:50    " = " => Eq         -- non-associative
infixr:80   " ^ " => HPow.hPow  -- right-associative
prefix:100  "-"   => Neg.neg
# set_option quotPrecheck false
postfix:max "⁻¹"  => Inv.inv

在描述运算符类型（其 "结合性"）的初始命令名称后，我们给出了由冒号 : 隔开的运算符的 解析优先级，然后是用双引号括起的新的或现有的标记（空格用于漂亮的打印），然后是箭头 => 后该运算符应该转换为的函数。

优先级是一个自然数，描述运算符与其参数的"紧密程度"，编码了操作的顺序。我们可以通过查看上述展开的命令来更清楚地说明这一点：

notation:65 lhs:65 " + " rhs:66 => HAdd.hAdd lhs rhs
notation:50 lhs:51 " = " rhs:51 => Eq lhs rhs
notation:80 lhs:81 " ^ " rhs:80 => HPow.hPow lhs rhs
notation:100 "-" arg:100 => Neg.neg arg
# set_option quotPrecheck false
notation:1024 arg:1024 "⁻¹" => Inv.inv arg  -- `max` is a shorthand for precedence 1024

原来，第一个代码块中的所有命令实际上都是将更通用的 notation 命令转换为命令 宏。我们将在下面学习如何编写这样的宏。notation 命令不仅接受单个令牌，还接受带有优先级的令牌序列和命名的术语占位符，这些占位符可以在 => 的右侧引用，并将被在那个位置解析的相应术语替换掉。具有优先级 p 的占位符只接受至少在该位置具有优先级 p 的记法。因此，字符串 a + b + c 不能被解析为等同于 a + (b + c)，因为 infixl 记法的右手操作数的优先级比记法本身大 1。相反，infixr 使用记法的优先级作为右手操作数的优先级，因此 a ^ b ^ c 可以 被解析为 a ^ (b ^ c)。请注意，如果我们直接使用 notation 来引入中缀记法，例如

# set_option quotPrecheck false
notation:65 lhs:65 " ~ " rhs:65 => wobble lhs rhs

当优先级无法足够确定结合性时，Lean 的解析器将默认为右结合性。更准确地说，当存在歧义的文法时，Lean 的解析器遵循本地的最长解析规则：在解析 a ~ 中的右侧时，在当前优先级允许的情况下，它将继续解析，不仅停留在 b，还会解析 ~ c。因此，该术语等价于 a ~ (b ~ c)。

如上所述，notation 命令允许我们自由地定义任意的混合采用语法，可以自由地混合标记和占位符。

# set_option quotPrecheck false
notation:max "(" e ")" => e
notation:10 Γ " ⊢ " e " : " τ => Typing Γ e τ

如果两个符号重叠，我们再次应用最长的解析规则：

notation:65 a " + " b:66 " + " c:66 => a + b - c
#eval 1 + 2 + 3  -- 0

Lean中，自然数类型Nat与整数类型Int不同。但是有一个名为Int.ofNat的函数，它将自然数嵌入整数中，也就是说我们可以在需要时将任何自然数视为整数。Lean有机制来检测和插入这种类型的强制转换。

variable (m n : Nat)
variable (i j : Int)

#check i + m      -- i + Int.ofNat m : Int
#check i + m + j  -- i + Int.ofNat m + j : Int
#check i + m + n  -- i + Int.ofNat m + Int.ofNat n : Int

显示信息

有多种方式可以查询 Lean 的当前状态以及当前上下文中可用的对象和定理的信息。你已经见过其中两种最常见的方式，#check 和 #eval。请记住，#check 通常与 @ 运算符一起使用，该运算符使定理或定义的所有参数显式。此外，你还可以使用 #print 命令来获取有关任何标识符的信息。如果标识符表示定义或定理，Lean 将打印符号的类型和定义。如果它是一个常量或一个公理，Lean 将指示这个事实，并显示类型。

-- examples with equality
#check Eq
#check @Eq
#check Eq.symm
#check @Eq.symm

#print Eq.symm

-- examples with And
#check And
#check And.intro
#check @And.intro

-- a user-defined function
def foo {α : Type u} (x : α) : α := x

#check foo
#check @foo
#print foo

设置选项

Lean维护了许多内部变量，用户可以通过设置这些变量来控制其行为。设置语法如下所示：

set_option <name> <value>

一组非常有用的选项可以控制 Lean 的 pretty-printer 显示项的方式。以下选项接受 true 或 false 作为输入：

pp.explicit  : display implicit arguments
pp.universes : display hidden universe parameters
pp.notation  : display output using defined notations

作为一个例子，以下设置会产生更长的输出：

set_option pp.explicit true
set_option pp.universes true
set_option pp.notation false

#check 2 + 2 = 4
#reduce (fun x => x + 2) = (fun x => x + 3)
#check (fun x => x + 1) 1

命令“set_option pp.all true”一次性进行了这些设置，而“set_option pp.all false”则恢复到先前的值。在调试证明或理解晦涩的错误信息时，Pretty Printing（美化输出）附加信息通常非常有用。然而，太多的信息可能会让人不知所措，在普通交互中，Lean的默认设置通常就足够了。