Lean 4中的定理证明

作者：Jeremy Avigad，Leonardo de Moura，Soonho Kong和Sebastian Ullrich，社区成员们贡献了这个版本的文本

本文的版本假定你正在使用Lean 4。请参考Lean 4手册的安装指南来安装Lean。这本书的第一个版本是为Lean 2写的，Lean 3的版本在这里可用。

引言

计算机与定理证明

形式验证涉及使用逻辑和计算方法来建立以确切的数学术语表达的声明。这些声明可以包括普通的数学定理，以及硬件或软件、网络协议、机械和混合系统符合其规范的声明。实际上，验证数学内容和验证系统正确性之间没有明确的界限：形式验证要求用数学术语描述硬件和软件系统，这时验证其正确性就变成了定理证明的一种形式。相反，数学定理的证明可能需要进行漫长的计算，这种情况下验证定理的真实性就需要验证计算是否按照预期进行。

支持数学断言的黄金标准是提供一个证明，在逻辑学的20世纪发展中，表明大多数，如果不是所有传统证明方法都可以归约为若干基础系统中的一小组公理和规则。通过这种归约，计算机可以帮助建立一个声明的两种方式：它可以帮助寻找一个证明，也可以帮助验证一个所谓的证明是正确的。

自动定理证明专注于“寻找”方面。解析定理证明器、表格定理证明器、快速可满足性求解器等提供了在命题和一阶逻辑中建立公式有效性的方法。其他系统提供了针对特定语言和领域的搜索和决策过程，比如整数或实数上的线性或非线性表达式。像SMT（“可满足性模理论”）这样的体系结构结合了领域通用的搜索方法和领域特定的过程。计算机代数系统和专业的数学软件包提供了进行数学计算、建立数学边界或找到数学对象的方法。计算也可以看作是一种证明，这些系统也有助于建立数学断言。

自动推理系统追求强大和高效，常常以可靠性的代价。这些系统可能存在错误，很难确保它们提供的结果是正确的。相反，交互定理证明注重定理证明的“验证”方面，要求每个断言都必须有一个适当公理的证明来支持。这设置了一个非常高的标准：每个推理规则和每个步骤都必须经过证明，否则就无法接受。 为了证明计算的正确性，必须依据先前的定义和定理，一直追溯到基本公理和规则。事实上，大多数这样的系统提供了完整的“证明对象”，可以传递给其他系统进行独立检查。构建这样的证明通常需要用户提供更多的输入和交互，但它允许您获得更深入和更复杂的证明。

Lean 定理证明器旨在弥合交互式和自动化定理证明之间的差距，通过将自动化工具和方法置于支持用户交互和构建完全规范化的公理证明的框架中。其目标是支持数学推理和复杂系统的推理，并验证在这两个领域中的断言。

Lean 的基本逻辑具有计算解释，因此 Lean 可以被看作一种编程语言。更重要的是，它可以被看作是一种具有精确语义的编写程序的系统，以及对程序计算的函数进行推理。Lean 还具有作为其自己的元编程语言的机制，这意味着可以使用 Lean 实现自动化，并使用 Lean 扩展 Lean 的功能。Lean 的这些方面在与本教程相伴的教程中进行了探讨，即在 Lean 4 中编程，尽管该系统的计算方面也会在这里出现。

关于 Lean

Lean 项目由 Leonardo de Moura 在2013年于微软研究院 Redmond 发起。这是一个持续的、长期的努力，其中大部分自动化的潜力只会逐渐实现。Lean 以Apache 2.0 许可证发布，这是一种自由的开源许可证，允许其他人自由使用和扩展代码和数学库。

要在计算机上安装 Lean，请使用快速入门指南。Lean 的源代码和构建 Lean 的说明可在https://github.com/leanprover/lean4/找到。

本教程描述的是当前版本的 Lean，即 Lean 4。

关于本书

本书旨在教你在 Lean 中开发和验证证明。您将获得大部分背景信息， 为了完成这个任务，你需要掌握的知识并不仅限于 Lean 本身。首先，你将学习 Lean 所基于的逻辑系统，它是一个强大到可以证明几乎任何传统数学定理，同时又以自然方式表达这些定理的 依赖类型论 的版本。具体来说，Lean 是基于一个被称为带递归类型的构造演算的版本。Lean 不仅能够定义数学对象并在依赖类型论中表达数学断言，还可以作为写证明的语言。

由于完整的公理证明过程非常复杂，证明定理的挑战在于让计算机尽可能填充尽可能多的细节。你将学习各种支持这一过程的方法，包括依赖类型论中的术语重写、Lean 的自动化方法来简化术语和表达式，以及支持灵活形式的代数推理的规范化和类型推断方法。

最后，你还将学习一些 Lean 特有的功能，包括与系统交互的语言以及 Lean 提供的管理复杂理论和数据的机制。

在整个文本中，你会找到类似下面这样的 Lean 代码示例：

theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
  fun hpq : p ∧ q =>
  have hp : p := And.left hpq
  have hq : q := And.right hpq
  show q ∧ p from And.intro hq hp

如果您在 VS Code 中阅读这本书，您会看到一个名为 "try it!" 的按钮。点击这个按钮会将示例代码复制到编辑器中，并提供足够的上下文使代码正确编译。您可以在编辑器中输入内容并修改示例代码，Lean 会在您输入时持续检查结果并提供反馈。我们建议您在阅读后继章节时运行示例并尝试自己编写代码。您可以使用命令 "Lean 4: Open Documentation View" 在 VS Code 中打开本书。

致谢

本教程是一个在 Github 上维护的开放存取项目。许多人为这个项目做出了贡献，提供了修正、建议、示例和文本。我们要感谢 Ulrik Buchholz、Kevin Buzzard、Mario Carneiro、Nathan Carter、Eduardo Cavazos、Amine Chaieb、Joe Corneli、William DeMeo、Marcus Klaas de Vries、Ben Dyer、Gabriel Ebner、 Anthony Hart、Simon Hudon、Sean Leather、Assia Mahboubi、Gihan Marasingha、Patrick Massot、Christopher John Mazey、Sebastian Ullrich、Floris van Doorn、 Daniel Velleman、Théo Zimmerman、Paul Chisholm、Chris Lovett 和 Siddhartha Gadgil 对他们的贡献表示感谢。请参阅 lean prover 和 lean community 以获取我们杰出贡献者的最新列表。

依赖类型理论

依赖类型理论是一种强大和表达力强的语言，您可以在其中表达复杂的数学断言，编写复杂的硬件和软件规范，并以一种自然和统一的方式进行推理。Lean基于一种称为“构造计算”的依赖类型理论的版本，其中有一个可数层次的非累积宇宙和归纳类型。通过本章的学习，您将对这些内容有深入的了解。

简单类型理论

“类型理论”得名于每个表达式都有一个关联的类型。例如，在给定的上下文中，x + 0 可能表示一个自然数，而 f 可能表示自然数上的函数。对于那些喜欢精确定义的人来说，Lean中的自然数是一个任意精度的无符号整数。

以下是您可以在Lean中声明对象并检查它们类型的一些示例。

/- Define some constants. -/

def m : Nat := 1       -- m is a natural number
def n : Nat := 0
def b1 : Bool := true  -- b1 is a Boolean
def b2 : Bool := false

/- Check their types. -/

#check m            -- output: Nat
#check n
#check n + 0        -- Nat
#check m * (n + 0)  -- Nat
#check b1           -- Bool
#check b1 && b2     -- "&&" is the Boolean and
#check b1 || b2     -- Boolean or
#check true         -- Boolean "true"

/- Evaluate -/

#eval 5 * 4         -- 20
#eval m + 2         -- 3
#eval b1 && b2      -- false

任何位于/-和-/之间的文本都被视为注释块，Lean会忽略它们。同样，两个短横线--表示该行剩余部分是注释，也会被忽略。注释块可以嵌套，这样可以像许多编程语言一样“注释掉”代码块。

def关键字将新的常量符号声明到工作环境中。在上面的示例中，def m : Nat := 1定义了一个名为m的类型为Nat的新常量，其值为1。#check命令要求Lean报告它们的类型；在Lean中，查询系统信息的辅助命令通常以井号（#）符号开头。#eval命令要求Lean评估给定的表达式。你可以自己尝试声明一些常量和对一些表达式进行类型检查。以这种方式声明新对象是对系统进行实验的好方法。

简单类型理论的强大之处在于你可以用其他类型组合出新的类型。例如，如果a和b是类型，a -> b表示从a到b的函数类型，a × b表示由a的元素和b的元素组成的对的类型，也被称为笛卡尔积。注意，×是一个Unicode符号。合理使用Unicode可以提高可读性，而且所有现代编辑器都对其有很好的支持。在Lean标准库中，经常使用希腊字母表示类型，使用Unicode符号→作为->的更紧凑版本。

#check Nat → Nat      -- type the arrow as "\to" or "\r"
#check Nat -> Nat     -- alternative ASCII notation

#check Nat × Nat      -- type the product as "\times"
#check Prod Nat Nat   -- alternative notation

#check Nat → Nat → Nat
#check Nat → (Nat → Nat)  --  same type as above

#check Nat × Nat → Nat
#check (Nat → Nat) → Nat -- a "functional"

#check Nat.succ     -- Nat → Nat
#check (0, 1)       -- Nat × Nat
#check Nat.add      -- Nat → Nat → Nat

#check Nat.succ 2   -- Nat
#check Nat.add 3    -- Nat → Nat
#check Nat.add 5 2  -- Nat
#check (5, 9).1     -- Nat
#check (5, 9).2     -- Nat

#eval Nat.succ 2   -- 3
#eval Nat.add 5 2  -- 7
#eval (5, 9).1     -- 5
#eval (5, 9).2     -- 9

再试试看一次你自己的例子。

让我们来看一些基本的语法。你可以通过输入\to或\r或\->来插入Unicode箭头→。你也可以使用ASCII替代形式->，因此表达式Nat -> Nat和Nat → Nat的意思是相同的。这两个表达式都表示将自然数作为输入并返回自然数作为输出的函数类型。使用Unicode符号×表示笛卡尔积，输入方式为\times。通常你会使用小写希腊字母α、β和γ来表示类型的范围。你可以使用\a、\b和\g输入这些特定的字母。

这里还有一些需要注意的地方。首先，函数f应用到值x的表示方式是f x（例如，Nat.succ 2）。其次，在编写类型表达式时，箭头向右关联；例如，Nat.add的类型是Nat → Nat → Nat，它等同于Nat → (Nat → Nat)。因此，你可以将Nat.add看作是一个接受自然数并返回另一个接受自然数并返回自然数的函数。在类型理论中，这通常比将Nat.add编写为接受一对自然数作为输入并返回自然数作为输出的函数更方便。例如，它允许你对函数Nat.add进行“部分应用”。上面的示例说明了Nat.add 3的类型是Nat → Nat，也就是说，Nat.add 3返回一个“等待”第二个参数n的函数，等价于Nat.add 3 n。

你已经看到，如果有m : Nat和n : Nat，那么(m, n)表示m和n的有序对，其类型为 输入Nat × Nat。这样可以创建一对自然数。反过来，如果你有p: Nat × Nat，那么你可以写成p.1: Nat和p.2: Nat。这样可以提取出它的两个组成部分。

类型作为对象

Lean的依赖类型理论扩展了简单类型理论的一种方法是，类型本身——如Nat和Bool——也是一等公民，也就是说它们本身也是对象。为了实现这一点，它们每一个也必须有一种类型。

#check Nat               -- Type
#check Bool              -- Type
#check Nat → Bool        -- Type
#check Nat × Bool        -- Type
#check Nat → Nat         -- ...
#check Nat × Nat → Nat
#check Nat → Nat → Nat
#check Nat → (Nat → Nat)
#check Nat → Nat → Bool
#check (Nat → Nat) → Nat

你可以看到上面每个表达式都是一个“Type”类型的对象。你还可以声明新的类型常量：

def α : Type := Nat
def β : Type := Bool
def F : Type → Type := List
def G : Type → Type → Type := Prod

#check α        -- Type
#check F α      -- Type
#check F Nat    -- Type
#check G α      -- Type → Type
#check G α β    -- Type
#check G α Nat  -- Type

正如上面的例子所示，您已经看到了一个类型为Type → Type → Type的函数的实例，即笛卡尔积Prod：

def α : Type := Nat
def β : Type := Bool

#check Prod α β       -- Type
#check α × β          -- Type

#check Prod Nat Nat   -- Type
#check Nat × Nat      -- Type

这是另一个例子：给定任何类型α，类型List α表示类型α元素的列表的类型。

def α : Type := Nat

#check List α    -- Type
#check List Nat  -- Type

鉴于Lean中的每个表达式都有一种类型，自然而然的是问：Type本身有什么类型？

#check Type      -- Type 1

您实际上已经遇到了Lean类型系统中最微妙的一个方面。Lean的基础底层具有无限层次的类型：

#check Type     -- Type 1
#check Type 1   -- Type 2
#check Type 2   -- Type 3
#check Type 3   -- Type 4
#check Type 4   -- Type 5

将Type 0看作“小型”或“普通”类型的宇宙。 Type 1则是一个更大的类型宇宙，它包含Type 0作为一个元素，而Type 2是一个更大的类型宇宙，它包含Type 1作为一个元素。列表是无限的，所以对于每个自然数n，都有一个Type n。Type是Type 0的缩写：

#check Type
#check Type 0

以下的表格可能有助于具体说明所讨论的关系。

沿着x轴的运动代表了宇宙的变化，而沿着y轴的运动代表了所谓的“度”的变化。

然而，一些操作需要对类型宇宙进行多态处理。例如，“List α”应该对于任何类型“α”都有意义，无论“α”位于哪个类型宇宙中。这解释了函数“List”的类型注释：

#check List    -- Type u_1 → Type u_1

在这里，u_1是一个范围在类型级别上的变量。#check命令的输出表明，只要α具有类型Type n，那么List α也具有类型Type n。函数Prod同样是多态的：

#check Prod    -- Type u_1 → Type u_2 → Type (max u_1 u_2)

要定义多态常量，Lean允许你使用universe命令来显式地声明宇宙变量：

universe u

def F (α : Type u) : Type u := Prod α α

#check F    -- Type u → Type u

当定义 F 时，您可以通过提供宇宙参数来避免使用 universe 命令。

def F.{u} (α : Type u) : Type u := Prod α α

#check F    -- Type u → Type u

函数抽象和评估

Lean提供了fun（或λ）关键字来从表达式中创建一个函数，如下所示：

#check fun (x : Nat) => x + 5   -- Nat → Nat
#check λ (x : Nat) => x + 5     -- λ and fun mean the same thing
#check fun x : Nat => x + 5     -- Nat inferred
#check λ x : Nat => x + 5       -- Nat inferred

您可以通过传递所需的参数来评估 lambda 函数：

#eval (λ x : Nat => x + 5) 10    -- 15

将另一个表达式创建为函数的过程称为lambda抽象。假设您有变量x : α，并且可以构建表达式t : β，那么表达式fun (x : α) => t，或等价地说，λ (x : α) => t，是类型为α → β的对象。可以将其视为从α到β的函数，将任何值x映射到值t。

以下是一些更多示例

#check fun x : Nat => fun y : Bool => if not y then x + 1 else x + 2
#check fun (x : Nat) (y : Bool) => if not y then x + 1 else x + 2
#check fun x y => if not y then x + 1 else x + 2   -- Nat → Bool → Nat

Lean将最后三个例子解释为相同的表达式；在最后一个表达式中，Lean从表达式“如果不是y，则x + 1，否则x + 2“中推断出x和y的类型。

一些在数学中常见的函数操作示例可以用lambda抽象来描述：

def f (n : Nat) : String := toString n
def g (s : String) : Bool := s.length > 0

#check fun x : Nat => x        -- Nat → Nat
#check fun x : Nat => true     -- Nat → Bool
#check fun x : Nat => g (f x)  -- Nat → Bool
#check fun x => g (f x)        -- Nat → Bool

思考一下这些表达式的含义。表达式fun x : Nat => x代表了Nat上的恒等函数，表达式fun x : Nat => true代表了始终返回true的常数函数，而fun x : Nat => g (f x)代表了f和g的复合函数。通常情况下，你可以省略类型注释，让Lean来自动推断。因此，例如，你可以写成fun x => g (f x)而不是fun x : Nat => g (f x)。

你可以将函数作为参数传递，并通过给它们命名为f和g来在实现中使用这些函数：

#check fun (g : String → Bool) (f : Nat → String) (x : Nat) => g (f x)
-- (String → Bool) → (Nat → String) → Nat → Bool

您还可以将类型作为参数传递：

#check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)

最后一个表达式，例如，表示一个接受三个类型α，β和γ，以及两个函数g：β→γ和f：α→β的函数，并返回g和f的复合函数。（理解该函数的类型需要了解依赖积，下文将对其进行解释。）

λ表达式的一般形式是fun x：α => t，其中变量x是一个“绑定变量”：它实际上是一个占位符，其“作用域”不延伸到表达式t之外。例如，表达式fun（b：β）（x：α）=> b中的变量b与之前声明的常量b无关。事实上，该表达式表示与fun（u：β）（z：α）=> u相同的函数。

形式上，对于通过重新命名绑定变量可以相同的表达式称为“α等价”，并被认为是“相同的”。Lean识别这种等价性。

注意，将项t：α→β应用到项s：α上会得到一个表达式t s：β。回到前面的例子并为了清晰起见对绑定变量重新命名，注意以下表达式的类型：

#check (fun x : Nat => x) 1     -- Nat
#check (fun x : Nat => true) 1  -- Bool

def f (n : Nat) : String := toString n
def g (s : String) : Bool := s.length > 0

#check
  (fun (α β γ : Type) (u : β → γ) (v : α → β) (x : α) => u (v x)) Nat String Bool g f 0
  -- Bool

如预期，表达式 (fun x : Nat => x) 1 的类型是 Nat。 事实上，更多的是这样：将表达式 (fun x : Nat => x) 应用于 1 应该会“返回”值 1。而且，的确如此：

#eval (fun x : Nat => x) 1     -- 1
#eval (fun x : Nat => true) 1  -- true

你将会看到这些术语是如何评估的。现在，请注意，这是依赖类型理论的一个重要特征：每个术语都具有计算行为，并支持一种归约化概念。原则上，归约到相同值的两个术语被称为定义上相等。它们被 Lean 的类型检查器视为"相同"，而 Lean 尽其所能识别和支持这些等同。

Lean 是一种完整的编程语言。它有一个生成二进制可执行文件和一个交互式解释器的编译器。你可以使用 #eval 命令执行表达式，这是测试函数的首选方法。

定义

记住，def 关键字提供了一种声明新命名对象的重要方式。

def double (x : Nat) : Nat :=
  x + x

如果你了解其他编程语言中的函数工作方式，这样可能更容易理解。名称“double”被定义为接受类型为“Nat”的输入参数“x”的函数，调用的结果是“x + x”，因此它返回类型为“Nat”。然后，您可以使用以下方法调用此函数：

# def double (x : Nat) : Nat :=
#  x + x
#eval double 3    -- 6

在这种情况下，您可以将def视为一种命名的lambda。 下面的代码会产生相同的结果：

def double : Nat → Nat :=
  fun x => x + x

#eval double 3    -- 6

当Lean有足够信息可以推断出类型时，您可以省略类型声明。类型推断是Lean的重要部分。

def double :=
  fun (x : Nat) => x + x

定义的一般形式是 def foo : α := bar，其中 α 是从表达式 bar 返回的类型。Lean 通常可以推断出类型 α，但明确写出它通常是一个好主意。这样可以明确你的意图，如果定义的右侧没有匹配的类型，Lean 会报错。

右侧的 bar 可以是任何表达式，不仅仅是一个 lambda。因此，def 也可用于简单地命名一个值，如下所示：

def pi := 3.141592654

def 可以接收多个输入参数。让我们创建一个能够将两个自然数相加的函数：

def add (x y : Nat) :=
  x + y

#eval add 3 2               -- 5

参数列表可以这样分隔：

# def double (x : Nat) : Nat :=
#  x + x
def add (x : Nat) (y : Nat) :=
  x + y

#eval add (double 3) (7 + 9)  -- 22

请注意，我们在这里调用了double函数来创建add函数的第一个参数。

您可以在def之内使用其他更有趣的表达式。

def greater (x y : Nat) :=
  if x > y then x
  else y

您可以猜到这个会做什么。

您还可以定义一个以另一个函数作为输入的函数。 以下代码调用给定的函数两次，将第一次调用的输出传递给第二次调用的函数：

# def double (x : Nat) : Nat :=
#  x + x
def doTwice (f : Nat → Nat) (x : Nat) : Nat :=
  f (f x)

#eval doTwice double 2   -- 8

现在来稍微抽象一点，你也可以指定类似类型参数的参数：

def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)

这意味着 compose 是一个函数，它以任意两个函数作为输入参数，只要这些函数都只接受一个输入。 类型代数 β → γ 和 α → β 意味着第二个函数的输出类型必须与第一个函数的输入类型匹配 - 这是有道理的，否则这两个函数将无法组合。

compose 还接受第三个参数，类型为 α，它用于调用第二个函数（本地命名为 f），并将该函数的结果（类型为 β）作为输入传递给第一个函数（本地命名为 g）。第一个函数返回类型 γ，因此它也是 compose 函数的返回类型。

compose 还非常通用，可以适用于任何类型 α β γ。这意味着 compose 可以组合几乎任何两个函数，只要它们每个函数都只接受一个参数，并且第二个函数的输出类型与第一个函数的输入类型匹配。例如：

# def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
#  g (f x)
# def double (x : Nat) : Nat :=
#  x + x
def square (x : Nat) : Nat :=
  x * x

#eval compose Nat Nat Nat double square 3  -- 18

本地定义

Lean 还允许您使用 let 关键字引入“本地”定义。表达式 let a := t1; t2 在定义上等于通过将 t2 中的每个出现的 a 替换为 t1 的结果。

#check let y := 2 + 2; y * y   -- Nat
#eval  let y := 2 + 2; y * y   -- 16

def twice_double (x : Nat) : Nat :=
  let y := x + x; y * y

#eval twice_double 2   -- 16

在这里，twice_double x 在定义上等于 (x + x) * (x + x)。

您可以通过链接 let 语句来组合多个赋值：

#check let y := 2 + 2; let z := y + y; z * z   -- Nat
#eval  let y := 2 + 2; let z := y + y; z * z   -- 64

当使用换行符时，可以省略;。

def t (x : Nat) : Nat :=
  let y := x + x
  y * y

请注意，表达式let a := t1; t2的含义与表达式(fun a => t2) t1非常相似，但两者并不相同。在第一个表达式中，你应该将t2中的每个a实例视为t1的一种语法缩写。在第二个表达式中，a是一个变量，且fun a => t2表达式必须独立于a的值而有意义。let结构是一种更强的缩写方法，存在着let a := t1; t2的形式表达式，无法表示为(fun a => t2) t1。作为练习，尝试理解为什么下面的foo定义可以通过类型检查，但bar定义不能。

def foo := let a := Nat; fun x : a => x + 2
/-
  def bar := (fun a => fun x : a => x + 2) Nat
-/

变量和部分

考虑以下三个函数定义:

def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)

def doTwice (α : Type) (h : α → α) (x : α) : α :=
  h (h x)

def doThrice (α : Type) (h : α → α) (x : α) : α :=
  h (h (h x))

Lean提供了variable命令，使这样的声明看起来更简洁：

variable (α β γ : Type)

def compose (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)

def doTwice (h : α → α) (x : α) : α :=
  h (h x)

def doThrice (h : α → α) (x : α) : α :=
  h (h (h x))

你可以声明任何类型的变量，不仅仅是Type本身：

variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)

def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))

#print compose
#print doTwice
#print doThrice

打印它们会发现这三组定义具有完全相同的效果。

variable命令指示Lean将已声明的变量按名称作为绑定变量插入到引用它们的定义中。Lean足够聪明以确定在定义中明确或隐式使用的变量。因此，当你编写定义时，可以将α、β、γ、g、f、h和x视为固定对象，并让Lean自动为你抽象定义。

以这种方式声明的变量将在您正在使用的文件的末尾保持有效范围。然而，有时候限制变量的范围是有用的。因此，Lean提供了section的概念：

section useful
  variable (α β γ : Type)
  variable (g : β → γ) (f : α → β) (h : α → α)
  variable (x : α)

  def compose := g (f x)
  def doTwice := h (h x)
  def doThrice := h (h (h x))
end useful

当部分关闭时，变量超出作用域，不能再被引用。

您不必对部分中的行进行缩进。您也不必为部分命名，也就是说，您可以使用一个匿名的 "section" / "end" 对。但是，如果您命名了一个部分，那么您必须使用相同的名称关闭它。部分也可以嵌套，这使您可以逐步声明新的变量。

命名空间

Lean 为您提供将定义分组到嵌套的分层 "命名空间" 中的能力：

namespace Foo
  def a : Nat := 5
  def f (x : Nat) : Nat := x + 7

  def fa : Nat := f a
  def ffa : Nat := f (f a)

  #check a
  #check f
  #check fa
  #check ffa
  #check Foo.fa
end Foo

-- #check a  -- error
-- #check f  -- error
#check Foo.a
#check Foo.f
#check Foo.fa
#check Foo.ffa

open Foo

#check a
#check f
#check fa
#check Foo.fa

当你声明你正在使用命名空间Foo时，你声明的每个标识符都有一个以"Foo."为前缀的全名。在命名空间内，你可以通过更短的名称引用标识符，但是一旦你结束了命名空间，就必须使用更长的名称。 与section不同，命名空间需要一个名称。在根级别只有一个匿名命名空间。

open命令将较短的名称带入当前上下文中。通常，当您导入一个模块时，您会想要打开其中一个或多个包含的命名空间，以便访问短标识符。但有时，当它们与您想要使用的另一个命名空间中的标识符发生冲突时，您可能希望将此信息保护在完全限定的名称中。因此，命名空间为您提供了在工作环境中管理名称的方法。

例如，Lean将涉及列表的定义和定理分组到一个名为List的命名空间中。

#check List.nil
#check List.cons
#check List.map

命令“打开列表”允许您使用较短的名称：

open List

#check nil
#check cons
#check map

与章节类似，命名空间可以嵌套：

namespace Foo
  def a : Nat := 5
  def f (x : Nat) : Nat := x + 7

  def fa : Nat := f a

  namespace Bar
    def ffa : Nat := f (f a)

    #check fa
    #check ffa
  end Bar

  #check fa
  #check Bar.ffa
end Foo

#check Foo.fa
#check Foo.Bar.ffa

open Foo

#check fa
#check Bar.ffa

已关闭的命名空间可以在以后重新打开，甚至在另一个文件中：

namespace Foo
  def a : Nat := 5
  def f (x : Nat) : Nat := x + 7

  def fa : Nat := f a
end Foo

#check Foo.a
#check Foo.f

namespace Foo
  def ffa : Nat := f (f a)
end Foo

像章节一样，嵌套的命名空间必须按照打开的顺序闭合。命名空间和章节有不同的用途：命名空间用于组织数据，而章节用于声明插入定义的变量。章节还可用于限定诸如"set_option"和"open"之类命令的作用范围。

然而，在很多方面，"namespace ... end"块与"section ... end"块的行为相同。特别是，如果在命名空间中使用"variable"命令，其作用域限制于该命名空间。类似地，如果在命名空间中使用"open"命令，其效果将在命名空间关闭时消失。

何为依赖类型理论的"依赖"之处？

简单解释就是，类型可以依赖于参数。你已经看到了一个很好的例子：类型"List α"依赖于参数"α"，而这种依赖性正是"List Nat"和"List Bool"之间的区别所在。再举一个例子，考虑类型"Vector α n"，表示长度为"n"的由"α"类型元素构成的向量。这个类型依赖于两个参数：向量中元素的类型("α : Type")以及向量的长度("n : Nat")。

假设你希望编写一个名为"cons"的函数，它可以将一个新元素插入到列表的头部。那么"cons"应该具有什么类型？这样的函数是多态的：你期望对于"Nat"、"Bool"或任意类型"α"，"cons"函数的行为都相同。因此，将类型作为"cons"的第一个参数是有道理的，这样对于任何类型"α"，"cons α"就是类型为"α"的列表插入函数。换句话说，对于每个"α"，"cons α"是一个接受元素"a : α"和列表"as : List α"，并返回一个新列表的函数，因此你有"cons α a as : List α"。

很明显，"cons α"应该具有类型"α → List α → List α"。但是"cons"应该具有什么类型呢？第一个猜测可能是"Type → α → list α → list α"，但仔细思考后，这并不是合适的类型。 观点：这个表达式中的α并不指代任何东西，而应该指代类型Type的参数。换句话说，假设函数的第一个参数是α : Type，那么接下来的两个元素的类型分别是α和List α。这些类型会根据第一个参数α的变化而变化。

def cons (α : Type) (a : α) (as : List α) : List α :=
  List.cons a as

#check cons Nat        -- Nat → List Nat → List Nat
#check cons Bool       -- Bool → List Bool → List Bool
#check cons            -- (α : Type) → α → List α → List α

这是依赖函数类型或依赖箭头类型的一个示例。给定α：Type和β：α → Type，可以将β看作是α上的一组类型，即为每个a：α定义一个类型β a。在这种情况下，类型(a：α) → β a表示具有以下性质的函数f的类型：对于每个a：α，f a 是β a的一个元素。换句话说，函数f返回的值的类型取决于其输入。

注意，对于任何表达式β：Type，表达式(a：α) → β都是有意义的。当β依赖于a（例如前一段中的表达式β a）时，(a：α) → β表示了一个依赖函数类型。而当β不依赖于a时，(a：α) → β与类型α → β没有区别。实际上，在依赖类型理论（以及 Lean）中，当β不依赖于a时，α → β只是(a：α) → β的一种记法。

回到列表的示例，您可以使用#check命令来检查以下List函数的类型。@符号以及圆括号和花括号之间的区别将在接下来解释。

#check @List.cons    -- {α : Type u_1} → α → List α → List α
#check @List.nil     -- {α : Type u_1} → List α
#check @List.length  -- {α : Type u_1} → List α → Nat
#check @List.append  -- {α : Type u_1} → List α → List α → List α

正如依赖函数类型 (a : α) → β a 通过允许 β 依赖于 α，泛化了函数类型 α → β 的概念，依赖笛卡尔积类型 (a : α) × β a 以相同的方式泛化了笛卡尔积 α × β。依赖积类型也被称为 sigma 类型，你也可以将它们写作 Σ a : α, β a。你可以使用 ⟨a, b⟩ 或 Sigma.mk a b 来创建一个依赖对。

universe u v

def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
  ⟨a, b⟩

def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a :=
  Sigma.mk a b

def h1 (x : Nat) : Nat :=
  (f Type (fun α => α) Nat x).2

#eval h1 5 -- 5

def h2 (x : Nat) : Nat :=
  (g Type (fun α => α) Nat x).2

#eval h2 5 -- 5

上述的函数 f 和 g 表示相同的函数。

隐式参数

假设我们有一个列表的实现，如下所示：

# universe u
# def Lst (α : Type u) : Type u := List α
# def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
# def Lst.nil (α : Type u) : Lst α := List.nil
# def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst          -- Type u_1 → Type u_1
#check Lst.cons     -- (α : Type u_1) → α → Lst α → Lst α
#check Lst.nil      -- (α : Type u_1) → Lst α
#check Lst.append   -- (α : Type u_1) → Lst α → Lst α → Lst α

然后，您可以按照以下方式构建Nat的列表。

# universe u
# def Lst (α : Type u) : Type u := List α
# def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
# def Lst.nil (α : Type u) : Lst α := List.nil
# def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
# #check Lst          -- Type u_1 → Type u_1
# #check Lst.cons     -- (α : Type u_1) → α → Lst α → Lst α
# #check Lst.nil      -- (α : Type u_1) → Lst α
# #check Lst.append   -- (α : Type u_1) → Lst α → Lst α → Lst α
#check Lst.cons Nat 0 (Lst.nil Nat)

def as : Lst Nat := Lst.nil Nat
def bs : Lst Nat := Lst.cons Nat 5 (Lst.nil Nat)

#check Lst.append Nat as bs

因为构造函数在类型上是多态的，我们不得不反复插入类型“Nat”作为参数。但是这些信息是冗余的：可以推断出参数“α”是“Lst.cons Nat 5 (Lst.nil Nat)”这个表达式的第一个参数，因为第二个参数“5”的类型是“Nat”。类似地，可以从“Lst.cons”函数期望在该位置有一个类型为“Lst α”的元素这一事实推断出“Lst.nil Nat”中的参数，而不是从该表达式中的其他任何信息中推断出来。

这是依赖类型理论的一个核心特点：项携带了大量信息，并且通常可以从上下文中推断出其中一些信息。在Lean中，可以使用下划线“_”来指定系统应该自动填充信息。这被称为“隐式参数”。

# universe u
# def Lst (α : Type u) : Type u := List α
# def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
# def Lst.nil (α : Type u) : Lst α := List.nil
# def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
# #check Lst          -- Type u_1 → Type u_1
# #check Lst.cons     -- (α : Type u_1) → α → Lst α → Lst α
# #check Lst.nil      -- (α : Type u_1) → Lst α
# #check Lst.append   -- (α : Type u_1) → Lst α → Lst α → Lst α
#check Lst.cons _ 0 (Lst.nil _)

def as : Lst Nat := Lst.nil _
def bs : Lst Nat := Lst.cons _ 5 (Lst.nil _)

#check Lst.append _ as bs

这仍然是繁琐的，然而，要键入所有这些下划线。当函数接受一个通常可以从上下文中推断出的参数时，Lean允许您指定该参数默认情况下应该保留为隐式。这可以通过将参数放置在花括号中来完成，如下所示：

universe u
def Lst (α : Type u) : Type u := List α

def Lst.cons {α : Type u} (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil {α : Type u} : Lst α := List.nil
def Lst.append {α : Type u} (as bs : Lst α) : Lst α := List.append as bs

#check Lst.cons 0 Lst.nil

def as : Lst Nat := Lst.nil
def bs : Lst Nat := Lst.cons 5 Lst.nil

#check Lst.append as bs

所做的改变仅限于在声明变量时将“α：Type u”用大括号括起来。我们还可以在函数定义中使用这种语法：

universe u
def ident {α : Type u} (x : α) := x

#check ident         -- ?m → ?m
#check ident 1       -- Nat
#check ident "hello" -- String
#check @ident        -- {α : Type u_1} → α → α

这使得给 ident 的第一个参数隐式。符号上，这隐藏了类型的规格，使其看起来好像 ident 只是简单地接受任意类型的参数。事实上，标准库中的函数 id 就是以这种方式精确定义的。我们在这里选择了一个非传统的名称，只是为了避免名称冲突。

当使用 variable 命令声明变量时，变量也可以被指定为隐式的：

universe u

section
  variable {α : Type u}
  variable (x : α)
  def ident := x
end

#check ident
#check ident 4
#check ident "hello"

这里对“ident”的定义与上面的定义有相同的效果。

Lean 对于实例化隐含参数有非常复杂的机制，我们将看到它们可以用来推断函数类型、谓词甚至证明。实例化术语中的这些“洞”或“占位符”的过程通常被称为推导。隐含参数的存在意味着有时可能没有足够的信息来精确确定表达式的含义。像“id”或“List.nil”这样的表达式被称为多态，因为它们可以在不同的上下文中具有不同的含义。

可以通过写成“(e : T)”来指定表达式“e”的类型“T”。这指示 Lean 的推导器在尝试解析隐含参数时使用值“T”作为“e”的类型。在下面的第二组示例中，这一机制被用来指定表达式“id”和“List.nil”的期望类型：

#check List.nil               -- List ?m
#check id                     -- ?m → ?m

#check (List.nil : List Nat)  -- List Nat
#check (id : Nat → Nat)       -- Nat → Nat

Lean 中的数字是重载的，但是当无法推断出数字的类型时，Lean 默认认为它是一个自然数。因此，下面的前两个“#check”命令中的表达式会以相同的方式进行解释，而第三个“#check”命令将“2”解释为一个整数。

#check 2            -- Nat
#check (2 : Nat)    -- Nat
#check (2 : Int)    -- Int

有时候，我们可能会发现自己处于这样一种情况：我们声明一个函数的参数为隐式的，但现在希望明确提供该参数。如果 foo 是这样一个函数，那么符号 @foo 表示具有所有参数都明确的相同函数。

#check @id        -- {α : Type u_1} → α → α
#check @id Nat    -- Nat → Nat
#check @id Bool   -- Bool → Bool

#check @id Nat 1     -- Nat
#check @id Bool true -- Bool

请注意，现在第一个#check命令将不插入任何占位符，而是显示标识符id的类型。此外，输出还指示第一个参数是隐含的。

命题和证明

到目前为止，您已经了解了在Lean中定义对象和函数的一些方法。在本章中，我们将开始解释如何使用依赖类型理论的语言编写数学断言和证明。

命题作为类型

在依赖类型理论的语言中证明关于对象的断言的一种策略是在定义语言之上叠加一个断言语言和一个证明语言。但是没有理由以这种方式增加语言的数量：依赖类型理论是灵活且表达能力强的，我们没有理由不能在相同的普遍框架中表示命题和证明。

例如，我们可以引入一个新的类型“Prop”来表示命题，并引入构造函数从其他命题构建新的命题。

# def Implies (p q : Prop) : Prop := p → q
#check And     -- Prop → Prop → Prop
#check Or      -- Prop → Prop → Prop
#check Not     -- Prop → Prop
#check Implies -- Prop → Prop → Prop

variable (p q r : Prop)
#check And p q                      -- Prop
#check Or (And p q) r               -- Prop
#check Implies (And p q) (And q p)  -- Prop

然后我们可以为每个元素p: Prop引入另一个类型Proof p，表示p的证明类型。"公理"将是这种类型的一个常量。

# def Implies (p q : Prop) : Prop := p → q
# structure Proof (p : Prop) : Type where
#   proof : p
#check Proof   -- Proof : Prop → Type

axiom and_comm (p q : Prop) : Proof (Implies (And p q) (And q p))

variable (p q : Prop)
#check and_comm p q     -- Proof (Implies (And p q) (And q p))

除了公理，我们还需要规则来从旧证明中构建新证明。例如，在许多命题逻辑的证明系统中，我们有演绎法则：

从证明"蕴含 p q"和证明"p"，我们获得证明"q"。

我们可以表示如下：

# def Implies (p q : Prop) : Prop := p → q
# structure Proof (p : Prop) : Type where
#   proof : p
axiom modus_ponens : (p q : Prop) → Proof (Implies p q) → Proof p → Proof q

对于命题逻辑的自然推理系统，通常还依赖于以下规则：

假设我们有一个假设为 p 的证明，那么我们可以“取消”这个假设并得到一个 Implies p q 的证明。

# def Implies (p q : Prop) : Prop := p → q
# structure Proof (p : Prop) : Type where
#   proof : p
axiom implies_intro : (p q : Prop) → (Proof p → Proof q) → Proof (Implies p q)

这种方法将为我们提供一个合理的建立断言和证明的方式。确定表达式 "t" 是断言 "p" 的正确证明，只是简单地检查 "t" 是否具有类型 "Proof p"。

然而，我们可以进行一些简化。首先，我们可以通过将 "Proof p" 与 "p" 本身混淆来避免重复写入术语 "Proof"。换句话说，每当我们有 "p：Prop" 时，我们可以将 "p" 解释为一个类型，即其证明的类型。然后，我们可以将 "t：p" 读作 "t" 是 "p" 的证明的断言。

此外，一旦我们进行了这种识别，含蓄规则表明我们可以在 "Implies p q" 和 "p → q" 之间来回传递。换句话说，命题 "p" 和 "q" 之间的蕴含对应于具有将 "p" 的任何元素映射到 "q" 的元素的函数。因此，引入连词 "Implies" 是完全冗余的：我们可以使用依赖类型理论中的通常函数空间构造器 "p → q" 作为蕴涵的概念。

这是"构造演算"和"依赖类型理论"中遵循的方法，因此也是Lean中遵循的方法。证明系统中蕴含的规则完全对应于函数的抽象和应用的规则，这是 Curry-Howard 同构（有时被称为 命题即类型 范式）的一个实例。实际上，类型 "Prop" 是 "Sort 0" 的语法糖，表示类型层次结构中的最底层，如上一章所述。此外，"Type u" 也只是 "Sort (u+1)" 的语法糖。"Prop" 具有一些特殊功能，但与其他类型宇宙一样，它在箭头构造器下是封闭的：如果我们有 "p q: Prop"，那么 "p → q: Prop"。

有至少两种将命题看作类型的方式。对于那些对逻辑和数学持建设性观点的人来说，这是对 "p" 作为命题所代表的内容的忠实呈现：命题 "p" 表示一种数据类型，即一种结构。 构成证明的数据类型规范。那么，p的证明简单地说就是一个正确类型的对象t：p。 对于不倾向于这种意识形态的人来说，可以将其视为一种简单的编码技巧。对于每个命题p，我们关联一个类型，如果p为假，则该类型为空，如果p为真，则该类型有一个元素，比如*。在后一种情况下，我们可以说（与之关联的）p是“被赋值的”。恰好这种类型与函数应用和抽象的规则相吻合，方便我们跟踪“Prop”中的哪些元素是被赋值的。因此，构建一个元素t：p告诉我们，p的确是真的。你可以把p的元素想象成“p为真的事实”。p→q的证明使用“p为真的事实”来得出“q为真的事实”。

实际上，如果p：Prop是任何命题，Lean核心将任意两个元素t1 t2：p视为定义上相等，就像它将（fun x => t）s和t[s/x]视为定义上相等一样。这被称为proof irrelevance，与上段的解释一致。这意味着尽管我们可以将t：p的证明视为依赖类型理论语言中的普通对象，但它们除了p为真这个事实之外没有任何信息。

我们建议的两种思考命题即类型范式的方式在根本上有所不同。从建设性的角度来看，证明是一种抽象的数学对象，由依赖类型理论中的合适表达式来“表示”。相反，如果我们根据上述描述的编码技巧来思考，那么表达式本身并没有表示任何有趣的东西。相反，我们能够书写并检查它们是否具有良好类型的事实来确保所讨论的命题为真。换句话说，表达式本身就是证明。

在下面的阐述中，我们将在这两种说法之间来回切换，有时会说一个表达式“构造”或 "产生"或"返回"一个命题的证明，有时候只是说它"是"这样的一个证明。这类似于计算机科学家有时混淆语法和语义之间的区别，他们有时会说一个程序"计算"某个函数，有时又会说程序"是"该函数。

不管怎样，真正重要的是最终结果。为了在依赖类型理论的语言中形式化地表达一个数学断言，我们需要展示一个p : Prop的术语。为了证明这个断言，我们需要展示一个t: p的术语。作为一个证明助手，Lean的任务是帮助我们构造这样的术语t，并验证它的正确性和类型是否正确。

以类型为命题的方式处理命题

在以类型为命题的范式中，只涉及→的定理可以使用lambda抽象和应用来证明。在Lean中，theorem命令引入一个新的定理：

variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p := fun hp : p => fun hq : q => hp

将这个证明与类型为α → β → α的表达式fun x:α => fun y:β => x进行比较，其中α和β是数据类型。 这描述了一个函数，它接受类型为α和β的参数x和y，然后返回x。 t1的证明具有相同的形式，唯一不同之处在于p和q是Prop而不是Type的元素。 直观地说，我们对p → q → p的证明假设p和q为真，并使用第一个假设（平凡地）来证明结论p为真。

请注意，theorem命令实际上是def命令的一个版本：在命题和类型的对应关系下，证明p → q → p实际上就是定义相关类型的元素。对于核心类型检查器来说，这两者之间没有区别。

然而，定义和定理之间存在一些实际上的差异。在正常情况下，从来不需要展开定理的“定义”；根据证明不可区分性，该定理的任意两个证明在定义上是相等的。一旦定理的证明完成，通常我们只需要知道该证明存在；无关乎证明是什么。基于这个事实，Lean将证明标记为不可约，这是对解析器（更准确地说是对编译器）的一种提示，即在处理文件时通常不需要展开它。实际上，由于评估一个证明的正确性不需要了解另一个证明的细节，Lean通常能够并行处理和检查证明。

与定义一样，#print命令将显示您的证明。

# variable {p : Prop}
# variable {q : Prop}
theorem t1 : p → q → p := fun hp : p => fun hq : q => hp

#print t1

注意，lambda抽象“hp: p”和“hq: q”可以被视为在证明“t1”时的临时假设。Lean还允许我们使用“show”语句明确指定最终项“hp”的类型。

# variable {p : Prop}
# variable {q : Prop}
theorem t1 : p → q → p :=
  fun hp : p =>
  fun hq : q =>
  show p from hp

添加这样的额外信息可以提高证明的清晰度，帮助在书写证明时检测错误。show命令除了注释类型外，内部还有所有我们见过的t1的表示产生相同的术语。

和普通定义一样，我们可以将抽象的变量移到冒号的左边：

# variable {p : Prop}
# variable {q : Prop}
theorem t1 (hp : p) (hq : q) : p := hp

#print t1    -- p → q → p

现在我们可以将定理“t1”视为函数应用。

# variable {p : Prop}
# variable {q : Prop}
theorem t1 (hp : p) (hq : q) : p := hp

axiom hp : p

theorem t2 : q → p := t1 hp

在这里，“axiom”声明假设存在给定类型的元素，并可能妥协逻辑一致性。例如，我们可以用它假设空类型 False 有一个元素。

axiom unsound : False
-- Everything follows from false
theorem ex : 1 = 0 :=
  False.elim unsound

声明公理“hp : p”等同于声明“p”是真的，并由“hp”证实。将定理“t1 : p → q → p”应用于事实“hp : p”即“p”是真的，可以得到定理“t1 hp : q → p”。

回顾一下，我们也可以将定理“t1”写为以下形式：

theorem t1 {p q : Prop} (hp : p) (hq : q) : p := hp

#print t1

t1 的类型现在是 ∀ {p q : Prop}, p → q → p。我们可以理解为断言：“对于每一对命题 p q，我们有 p → q → p。” 例如，我们可以将所有参数移到冒号的右边：

theorem t1 : ∀ {p q : Prop}, p → q → p :=
  fun {p q : Prop} (hp : p) (hq : q) => hp

如果p和q已被声明为变量，Lean会自动为我们进行泛化处理：

variable {p q : Prop}

theorem t1 : p → q → p := fun (hp : p) (hq : q) => hp

实际上，通过命题即类型对应，我们可以将“p”成立的假设“hp”声明为另一个变量：

variable {p q : Prop}
variable (hp : p)

theorem t1 : q → p := fun (hq : q) => hp

Lean检测到证明使用了"hq"并自动添加"hp : p"作为前提条件。在所有情况下，命令“#print t1”仍然产生“∀ p q : Prop, p → q → p”。请记住，这种类型也可以写作"∀ (p q : Prop) (hp : p) (hq : q), p"，因为箭头只表示目标不依赖于绑定变量的箭头类型。

当我们以这种方式推广"t1"时，我们可以将它应用于不同的命题对，以得到常规定理的不同实例。

theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp

variable (p q r s : Prop)

#check t1 p q                -- p → q → p
#check t1 r s                -- r → s → r
#check t1 (r → s) (s → r)    -- (r → s) → (s → r) → r → s

variable (h : r → s)
#check t1 (r → s) (s → r) h  -- (s → r) → r → s

再次，利用命题与类型对应的关系，类型为r → s的变量h可视为假设或前提，即r → s成立的假设。

以另一个示例为例，让我们考虑上一章中讨论的复合函数，现在使用命题而不是类型。

variable (p q r s : Prop)

theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r :=
  fun h₃ : p =>
  show r from h₁ (h₂ h₃)

作为命题逻辑的定理，t2是什么意思？

请注意，使用数值Unicode下标作为假设经常非常有用，可以输入为\0、\1、\2、...，就像我们在这个示例中所做的一样。

命题逻辑

Lean定义了所有标准的逻辑连接词和符号。命题连接词使用以下符号表示：

它们都取值为Prop。

variable (p q : Prop)

#check p → q → p ∧ q
#check ¬p → p ↔ False
#check p ∨ q → q ∨ p

运算顺序如下：一元否定 ¬ 最强，然后是 ∧，然后是 ∨，然后是 →，最后是 ↔。例如，a ∧ b → c ∨ d ∧ e 的意思是 (a ∧ b) → (c ∨ (d ∧ e))。请记住，→ 是从右向左结合的（精确来说，现在的参数是 Prop 类型，而不是其他类型），其他二元连结词也是如此。因此，如果我们有 p q r : Prop，表达式 p → q → r 表示 "如果 p，那么如果 q，就 r。" 这只是 p ∧ q → r 的 "柯里化" 形式。

在上一章中，我们观察到 lambda 抽象可以被视为 → 的 "引入规则"。在当前设置中，它展示了如何 "引入" 或建立一个蕴涵。应用可以被视为一种 "消去规则"，展示了如何在证明中 "消去" 或使用一个蕴涵。其他命题连结词在 Lean 的库文件 Prelude.core 中定义（有关库层次结构的更多信息，请参见 importing files），每个连结词都带有其规范的引入和消去规则。

合取（conjunction）

表达式 And.intro h1 h2 使用证明 h1 : p 和 h2 : q 构建了一个 p ∧ q 的证明。通常将 And.intro 称为 合取引入 规则。在下一个示例中，我们使用 And.intro 创建了一个 p → q → p ∧ q 的证明。

variable (p q : Prop)

example (hp : p) (hq : q) : p ∧ q := And.intro hp hq

#check fun (hp : p) (hq : q) => And.intro hp hq

example命令陈述了一个定理，但没有为它命名或将其存储在永久上下文中。实质上，它只是检查给定的项是否具有指定的类型。它非常方便用于说明，并且我们经常会使用它。

表达式And.left h从证明h : p ∧ q中创建了一个关于“p”的证明。同样，And.right h是一个关于“q”的证明。它们通常称为左和右的and-消除规则。

variable (p q : Prop)

example (h : p ∧ q) : p := And.left h
example (h : p ∧ q) : q := And.right h

我们现在可以使用以下证明项证明“p ∧ q → q ∧ p”。

variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  And.intro (And.right h) (And.left h)

注意，安德引入和安德消除类似于笛卡尔乘积的配对和投影操作。不同之处在于给定hp：p和hq：q，And.intro hp hq的类型是p ∧ q：Prop，而Prod hp hq的类型是p × q：Type。∧和×之间的类似性是另一个Curry-Howard同构的例子，但与蕴含和函数空间构造器不同的是，∧和×在Lean中是分开处理的。然而，通过这个类比，我们刚刚构建的证明类似于将一对元素交换的函数。

我们将在结构和记录章节中看到，在Lean中，某些类型是结构，这意味着该类型是用单个规范的构造器定义的，该构造器从一系列合适的参数构建类型的元素。对于每个p q：Prop，p ∧ q就是一个例子：构建元素的规范方法是将适当的参数hp：p和hq：q应用到And.intro中。Lean允许我们在这种情况下使用匿名构造器表示法⟨arg1, arg2, ...⟩，当相关类型是归纳类型并且可以从上下文中推断出时。特别地，我们可以经常写成⟨hp, hq⟩而不是And.intro hp hq：

variable (p q : Prop)
variable (hp : p) (hq : q)

#check (⟨hp, hq⟩ : p ∧ q)

这些尖括号可以通过键入\<和\>来获得。

Lean还提供了另一个有用的语法工具。给定一个表达式e，它的归纳类型是Foo（可能应用了一些参数），记号e.bar是Foo.bar e的简写。这提供了一种方便的方式来访问函数而不需要打开命名空间。例如，以下两个表达式表示相同的意思：

variable (xs : List Nat)

#check List.length xs
#check xs.length

因此，鉴于“h：p ∧ q”，我们可以用“h.left”表示“And.left h”，用“h.right”表示“And.right h”。因此，我们可以方便地将上述示例证明重写为：

variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  ⟨h.right, h.left⟩

简洁和混淆之间有一条微妙的界线，以这种方式省略信息有时会使证明更难阅读。但对于像上面那样的直接构造，当“h”的类型和构造的目标明显时，这种表示法是简洁而有效的。

在 Lean 中，常见的迭代构造方式是 “And”。Lean 还允许将右结合的嵌套构造方式展平，所以这两个证明是等效的：

variable (p q : Prop)

example (h : p ∧ q) : q ∧ p ∧ q :=
  ⟨h.right, ⟨h.left, h.right⟩⟩

example (h : p ∧ q) : q ∧ p ∧ q :=
  ⟨h.right, h.left, h.right⟩

这也常常很有用。

析取

表达式Or.intro_left q hp根据证明hp : p创建了一个p ∨ q的证明。类似地，Or.intro_right p hq使用证明hq : q创建了一个p ∨ q的证明。这些是左右析取引入规则。

variable (p q : Prop)
example (hp : p) : p ∨ q := Or.intro_left q hp
example (hq : q) : p ∨ q := Or.intro_right p hq

*or-elimination（或消去）*规则稍微复杂一些。其思路是我们可以从p ∨ q证明出r，通过展示r从p和r从q都可以得到。换句话说，这是一种根据情况证明的方式。在表达式Or.elim hpq hpr hqr中，Or.elim接受三个参数，hpq : p ∨ q，hpr : p → r 和 hqr : q → r，然后得到r的证明。在下面的例子中，我们使用Or.elim来证明p ∨ q → q ∨ p。

variable (p q r : Prop)

example (h : p ∨ q) : q ∨ p :=
  Or.elim h
    (fun hp : p =>
      show q ∨ p from Or.intro_right q hp)
    (fun hq : q =>
      show q ∨ p from Or.intro_left p hq)

在大多数情况下，Lean可以自动推断出Or.intro_right和Or.intro_left的第一个参数。因此，Lean提供了Or.inr和Or.inl，可以看作是Or.intro_right _和Or.intro_left _的简写形式。因此，上述证明项可以更简洁地编写为：

variable (p q r : Prop)

example (h : p ∨ q) : q ∨ p :=
  Or.elim h (fun hp => Or.inr hp) (fun hq => Or.inl hq)

请注意，完整表达式中有足够的信息供Lean推断hp和hq的类型。但是，使用更长版本中的类型注释可以使证明更可读，并且可以帮助捕捉和调试错误。

由于Or有两个构造函数，我们无法使用匿名构造函数表示法。但是我们仍然可以写h.elim而不是Or.elim h：

variable (p q r : Prop)

example (h : p ∨ q) : q ∨ p :=
  h.elim (fun hp => Or.inr hp) (fun hq => Or.inl hq)

再次，你应该行使判断力来确定这些缩写符是否增强或减弱了可读性。

否定和谬误

否定，¬p，实际上被定义为 p → False，因此我们可以通过从 p 推导出一个矛盾来获得 ¬p。类似地，表达式 hnp hp 从 hp : p 和 hnp : ¬p 中产生了一个 False 的证明。下一个例子使用了这两条规则来产生一个 (p → q) → ¬q → ¬p 的证明。（符号 ¬ 通过输入 \not 或者 \neg 获取。）

variable (p q : Prop)

example (hpq : p → q) (hnq : ¬q) : ¬p :=
  fun hp : p =>
  show False from hnq (hpq hp)

逻辑连词False具有一个单一的消解规则，False.elim，它表达了任何事物都可以从矛盾中推导出来的事实。有时将此规则称为ex falso（ex falso sequitur quodlibet的缩写）或者爆炸原理。

variable (p q : Prop)

example (hp : p) (hnp : ¬p) : q := False.elim (hnp hp)

absurd是从矛盾的假设中推导出任意事实的模式，被应用在False.elim这个函数中，并且会自动推断出这个任意事实q。这种模式是相当常见的。

variable (p q : Prop)

example (hp : p) (hnp : ¬p) : q := absurd hp hnp

以下是¬p → q → (q → p) → r的一个证明示例：

首先，我们假设¬p为真（设置前提）。

接下来，我们假设q也为真（设置前提）。

然后，假设q → p为真（设置前提）。

根据前提¬p和设置的q → p，我们可以得出p为假（通过逻辑推理）。

再根据前提q和得出的p为假，我们可以得出q → p为假（通过逻辑推理）。

根据前提q → p为假和设置的q → p，我们可以得出¬q为真（通过逻辑推理）。

最后，根据前提¬q和设置的¬p，我们可以得出r为真（通过逻辑推理）。

因此，我们可以得出结论：¬p → q → (q → p) → r为真。

variable (p q r : Prop)

example (hnp : ¬p) (hq : q) (hqp : q → p) : r :=
  absurd (hqp hq) hnp

顺便说一下，就像False只有一个消除规则一样，True只有一个引入规则，即True.intro : true。换句话说，True就是真，它有一个规范的证明，即True.intro。

逻辑等价

表达式Iff.intro h1 h2从h1 : p → q和h2 : q → p中产生了p ↔ q的证明。表达式Iff.mp h从h : p ↔ q中产生了p → q的证明。类似地，Iff.mpr h从h : p ↔ q中产生了q → p的证明。这是一个p ∧ q ↔ q ∧ p的证明：

variable (p q : Prop)

theorem and_swap : p ∧ q ↔ q ∧ p :=
  Iff.intro
    (fun h : p ∧ q =>
     show q ∧ p from And.intro (And.right h) (And.left h))
    (fun h : q ∧ p =>
     show p ∧ q from And.intro (And.right h) (And.left h))

#check and_swap p q    -- p ∧ q ↔ q ∧ p

variable (h : p ∧ q)
example : q ∧ p := Iff.mp (and_swap p q) h

我们可以使用匿名构造函数表示法从前向和后向的证明来构造p ↔ q的证明，还可以使用.表示法与mp和mpr。因此，前面的示例可以简洁地写成如下形式：

variable (p q : Prop)

theorem and_swap : p ∧ q ↔ q ∧ p :=
  ⟨ fun h => ⟨h.right, h.left⟩, fun h => ⟨h.right, h.left⟩ ⟩

example (h : p ∧ q) : q ∧ p := (and_swap p q).mp h

介绍辅助子目标

这是一个介绍Lean提供的帮助组织长证明的另一种方法的好地方，即“have”结构，在证明中引入了一个辅助子目标。这里有一个小例子，根据上一节进行了调整：

variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  have hp : p := h.left
  have hq : q := h.right
  show q ∧ p from And.intro hq hp

内部表达式have h : p := s; t会生成(fun (h : p) => t) s。换句话说，s是p的证明，t是在假设h : p下所需结论的证明，并且通过lambda抽象和应用将两者组合在一起。这个简单的方法在构建长证明时非常有用，因为我们可以使用中间的have作为通往最终目标的跳板。

Lean还支持一种从目标向后推理的结构化方法，这种方法模拟了普通数学中的“足够展示”构造。下一个例子只是对之前证明中的最后两行进行了排列。

variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  have hp : p := h.left
  suffices hq : q from And.intro hq hp
  show q from And.right h

写 suffices hq: q 可以让我们达到两个目标。首先，我们必须证明确实只需证明q，通过证明带有额外假设hq：q 的原始目标q ∧ p。最后，我们必须证明q。

经典逻辑

到目前为止，我们所看到的引入和消除规则都是建设性的，也就是说，它们反映了基于命题即类型对应的逻辑连词的计算理解。普通的经典逻辑在此基础上添加了排中律，p ∨ ¬p。要使用这个原则，你必须打开经典命名空间。

open Classical

variable (p : Prop)
#check em p

直观上，构造性的“或”非常强大：断言“p ∨ q”等同于知道哪种情况成立。如果“RH”代表黎曼猜想(Riemann hypothesis)，一个经典的数学家愿意断言“RH ∨ ¬RH”，即使我们还不能断言任何一个分离部分。

排中律的一个结果是双重否定消除原则：

open Classical

theorem dne {p : Prop} (h : ¬¬p) : p :=
  Or.elim (em p)
    (fun hp : p => hp)
    (fun hnp : ¬p => absurd hnp h)

双重否定消除允许我们证明任何命题“p”，通过假设“¬p”并推导出“false”，因为这等同于证明“¬¬p”。换句话说，双重否定消除允许我们进行一个证明通过矛盾，这在建构性逻辑中通常是不可能的。作为一个练习，你可以尝试证明逆命题，即从“dne”证明“em”是可以的。

经典公理还给你提供了通过使用“em”的辅助证明的其他模式。例如，我们可以通过分情况进行证明：

open Classical
variable (p : Prop)

example (h : ¬¬p) : p :=
  byCases
    (fun h1 : p => h1)
    (fun h1 : ¬p => absurd h1 h)

或者你可以采用反证法来进行证明：

open Classical
variable (p : Prop)

example (h : ¬¬p) : p :=
  byContradiction
    (fun h1 : ¬p =>
     show False from h h1)

如果你不习惯进行建设性思维，可能需要一些时间才能意识到在哪些情况下使用了经典推理。在以下示例中需要使用经典推理，因为从建设性的观点来看，知道“p”和“q”不同时真实并不能告诉你哪一个是假的：

# open Classical
# variable (p q : Prop)
example (h : ¬(p ∧ q)) : ¬p ∨ ¬q :=
  Or.elim (em p)
    (fun hp : p =>
      Or.inr
        (show ¬q from
          fun hq : q =>
          h ⟨hp, hq⟩))
    (fun hp : ¬p =>
      Or.inl hp)

我们稍后将会看到，在建设性逻辑中确实存在一些情况下，排中律和双重否定消除等原则是可以使用的，并且Lean支持在这样的上下文中使用经典推理而不依赖于排中律。

在Lean中用于支持经典推理的完整公理列表在《公理与计算》中进行了讨论。

命题有效性的示例

Lean的标准库中包含了许多命题逻辑的有效陈述的证明，您可以自由地在您自己的证明中使用它们。下面的列表包括了一些常见的等式。

交换律：

1. p ∧ q ↔ q ∧ p
2. p ∨ q ↔ q ∨ p

结合律：

3. (p ∧ q) ∧ r ↔ p ∧ (q ∧ r)
4. (p ∨ q) ∨ r ↔ p ∨ (q ∨ r)

分配律：

5. p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)
6. p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)

其他属性：

7. (p → (q → r)) ↔ (p ∧ q → r)
8. ((p ∨ q) → r) ↔ (p → r) ∧ (q → r)
9. ¬(p ∨ q) ↔ ¬p ∧ ¬q
10. ¬p ∨ ¬q → ¬(p ∧ q)
11. ¬(p ∧ ¬p)
12. p ∧ ¬q → ¬(p → q)
13. ¬p → (p → q)
14. (¬p ∨ q) → (p → q)
15. p ∨ False ↔ p
16. p ∧ False ↔ False
17. ¬(p ↔ ¬p)
18. (p → q) → (¬q → ¬p)

以下需要经典推理：

19. (p → r ∨ s) → ((p → r) ∨ (p → s))

20. ¬(p ∧ q) → ¬p ∨ ¬q

21. ¬(p → q) → p ∧ ¬q

22. (p → q) → (¬p ∨ q)

23. (p → q) → (¬p ∨ q)

24. (¬q → ¬p) → (p → q)

25. (¬q → ¬p) → (p → q)

26. p ∨ ¬p

27. p ∨ ¬p

28. (((p → q) → p) → p)

29. (((p → q) → p) → p)

sorry 不知何故可以生成任何结论的证明，或提供任何数据类型的对象。当然，这种证明方法是不可行的——例如，你可以用它证明False——当使用或导入依赖于sorry的定理时，Lean会产生严重的警告。但是，它非常有用于逐步构建较长的证明。从上到下编写证明，使用sorry填充子证明。确保Lean接受带有所有sorry的项；如果不接受，则需要纠正错误。然后，逐个将sorry替换为实际的证明，直到没有剩下为止。

这里还有另一个有用的技巧。你可以使用下划线_作为占位符，而不是使用sorry。回想一下，这告诉Lean参数是隐式的，并且应该自动填充。如果Lean尝试并失败，它会返回一个错误消息"don't know how to synthesize placeholder"，后跟它期望的项的类型以及上下文中提供的所有对象和假设。换句话说，对于每个未解决的占位符，Lean报告需要在该点填写的子目标。然后，您可以通过逐步填写这些占位符来构造证明。

作为参考，这里有两个从上面列表中取出的有效性的示例证明。

open Classical

-- distributivity
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
  Iff.intro
    (fun h : p ∧ (q ∨ r) =>
      have hp : p := h.left
      Or.elim (h.right)
        (fun hq : q =>
          show (p ∧ q) ∨ (p ∧ r) from Or.inl ⟨hp, hq⟩)
        (fun hr : r =>
          show (p ∧ q) ∨ (p ∧ r) from Or.inr ⟨hp, hr⟩))
    (fun h : (p ∧ q) ∨ (p ∧ r) =>
      Or.elim h
        (fun hpq : p ∧ q =>
          have hp : p := hpq.left
          have hq : q := hpq.right
          show p ∧ (q ∨ r) from ⟨hp, Or.inl hq⟩)
        (fun hpr : p ∧ r =>
          have hp : p := hpr.left
          have hr : r := hpr.right
          show p ∧ (q ∨ r) from ⟨hp, Or.inr hr⟩))

-- an example that requires classical reasoning
example (p q : Prop) : ¬(p ∧ ¬q) → (p → q) :=
  fun h : ¬(p ∧ ¬q) =>
  fun hp : p =>
  show q from
    Or.elim (em q)
      (fun hq : q => hq)
      (fun hnq : ¬q => absurd (And.intro hp hnq) h)

练习

证明下面的恒等式，将“sorry”占位符替换为实际的证明。

variable (p q r : Prop)

-- commutativity of ∧ and ∨
example : p ∧ q ↔ q ∧ p := sorry
example : p ∨ q ↔ q ∨ p := sorry

-- associativity of ∧ and ∨
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry

-- distributivity
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := sorry
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := sorry

-- other properties
example : (p → (q → r)) ↔ (p ∧ q → r) := sorry
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := sorry
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := sorry
example : ¬p ∨ ¬q → ¬(p ∧ q) := sorry
example : ¬(p ∧ ¬p) := sorry
example : p ∧ ¬q → ¬(p → q) := sorry
example : ¬p → (p → q) := sorry
example : (¬p ∨ q) → (p → q) := sorry
example : p ∨ False ↔ p := sorry
example : p ∧ False ↔ False := sorry
example : (p → q) → (¬q → ¬p) := sorry

证明以下恒等式，用实际的证明来替换 "sorry" 占位符。这些恒等式需要经典的推理方法。

1. 恒等式：(a + b = b + a)，对于任意实数 (a) 和 (b) 成立。

证明：根据实数的加法交换律，我们知道对于任意实数 (a) 和 (b)，有 (a + b = b + a)。因此，恒等式成立。

2. 恒等式：(a - b = -b + a)，对于任意实数 (a) 和 (b) 成立。

证明：根据实数的加法逆元定义，我们有 (b + (-b) = 0)。然后，根据实数的加法单位元定义，我们有 (0 + a = a)。结合这两个等式，我们可以得出 (b + (-b) + a = a)。进一步化简，我们可以得出 ((-b) + a = a - b)。因此，恒等式成立。

3. 恒等式：(a \cdot b = b \cdot a)，对于任意实数 (a) 和 (b) 成立。

证明：根据实数的乘法交换律，我们知道对于任意实数 (a) 和 (b)，有 (a \cdot b = b \cdot a)。因此，恒等式成立。

4. 恒等式：(a \div b = \frac{1}{b} \cdot a)，对于任意实数 (a) 和 (b) 成立。

证明：由于除法可以转换为乘法的倒数运算，我们可以将 (a \div b) 转化为 (a \cdot \frac{1}{b})。根据实数的乘法交换律，我们知道对于任意实数 (a) 和 (b)，有 (a \cdot \frac{1}{b} = \frac{1}{b} \cdot a)。因此，恒等式成立。

这些证明使用了实数运算的基本性质和定义，因此都是合理的。

open Classical

variable (p q r : Prop)

example : (p → q ∨ r) → ((p → q) ∨ (p → r)) := sorry
example : ¬(p ∧ q) → ¬p ∨ ¬q := sorry
example : ¬(p → q) → p ∧ ¬q := sorry
example : (p → q) → (¬p ∨ q) := sorry
example : (¬q → ¬p) → (p → q) := sorry
example : p ∨ ¬p := sorry
example : (((p → q) → p) → p) := sorry

证明 ¬(p ↔ ¬p) 而不使用经典逻辑。

让我们使用直觉istic逻辑证明这个表达式。

假设 p为真，即 p=True。那么根据双向蕴含的定义，p ↔ ¬p表达式得到真值:

(p ↔ ¬p) 
≡ (True ↔ ¬True)  
≡ (True ↔ False)
≡ False

同样地，如果我们假设 p为假，即 p=False，我们会得到相同的结果:

(p ↔ ¬p) 
≡ (False ↔ ¬False)  
≡ (False ↔ True)
≡ False

由于p可以取True或False的值，并且p ↔ ¬p的结果总是False，我们可以确定该表达式是真的，即 ¬(p ↔ ¬p) 为真。

全称量化

注意，如果 α 是任意类型，我们可以将 α 上的一元谓词 p 表示为类型为 α → Prop 的对象。在这种情况下，给定 x:α，p x 表示 p 对于 x 成立的断言。类似地，对象 r ：α → α → Prop 表示 α 上的二元关系：给定 x y : α，r x y 表示 x 和 y 有关系的断言。

全称量化符号 ∀ x : α, p x 被认为表示了“对于每个 x : α ， p x 成立”的断言。和命题联结词一样，在自然推理系统中，“对于所有”受到引入规则和消除规则的制约。非正式地说，引入规则如下：

在一个假设为 x : α 的上下文中给定 p x 的证明，我们可以得到一个证明 ∀ x : α, p x。

消除规则如下：

给定一个证明 ∀ x : α, p x 和任意项 t : α，我们可以得到一个证明 p t。

和蕴含的情况相同，类型为命题的项来进行解释。回想一下依赖箭头类型的引入和消除规则：

给定类型为 β x 的项 t，在一个假设为 x : α 的上下文中我们有 (fun x : α => t) : (x : α) → β x。

消除规则如下：

给定一个类型为 (x : α) → β x 的项 s 和任意项 t : α，我们有 s t : β t。

在 p x 的类型为 Prop 的情况下，如果我们将 (x : α) → β x 替换为 ∀ x : α, p x，我们可以将这些规则解释为关于全称量化的构建证明的正确规则。 因此，Constructions计算将依赖箭头类型与forall表达式等同起来。如果 p 是任何表达式，那么 ∀ x : α, p 不过是 (x : α) → p 的别名，前者在 p 是命题的情况下比后者更加自然。通常情况下，表达式 p 会依赖于 x : α。回想一下，在普通函数空间的情况下，我们可以将 α → β 解释为 (x : α) → β 的特殊情况，其中 β 不依赖于 x。类似地，我们可以将命题之间的蕴含关系 p → q 视为 ∀ x : p, q 的特殊情况，其中表达式 q 不依赖于 x。

下面是一个展示命题即类型对应关系如何实践的例子。

example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ y : α, p y :=
  fun h : ∀ x : α, p x ∧ q x =>
  fun y : α =>
  show p y from (h y).left

作为一项符号约定，我们将全称量词的作用范围设定为最宽，因此需要用括号将量词限制在上述示例的前提中。证明 ∀ y : α, p y 的经典方式是取一个任意的 y，并证明 p y。这是引入规则。现在，假设 h 的类型是 ∀ x : α, p x ∧ q x，那么表达式 h y 的类型是 p y ∧ q y。这是消去规则。取左合取项即得到所需结论，即 p y。

请记住，只要变量的绑定不同，表达式即被认为是等价的。因此，例如，在假设和结论中可以使用相同的变量 x，并在证明中用不同的变量 z 实例化它：

example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ x : α, p x :=
  fun h : ∀ x : α, p x ∧ q x =>
  fun z : α =>
  show p z from And.left (h z)

另一个例子是我们如何表达一个关系 r 是可传递的：

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

这里，我们定义了一个函数 transitive，它接受一个类型为 α 的参数，以及一个从 α 到 α 到命题的关系 r。函数的类型为 Prop，即表示命题的类型。在函数体内，我们使用了一个全称量化的命题，即对于任意的 a、b、c，如果 r a b 和 r b c 成立，那么 r a c 也成立。这个定义就表达了关系 r 是可传递的这一事实。

variable (α : Type) (r : α → α → Prop)
variable (trans_r : ∀ x y z, r x y → r y z → r x z)

variable (a b c : α)
variable (hab : r a b) (hbc : r b c)

#check trans_r    -- ∀ (x y z : α), r x y → r y z → r x z
#check trans_r a b c
#check trans_r a b c hab
#check trans_r a b c hab hbc

考虑这里发生了什么。当我们使用值 a b c 实例化 trans_r 时，我们得到了一个证明，即 r a b → r b c → r a c。将其应用于“假设”hab : r a b，我们得到了一个蕴含的证明 r b c → r a c。最后，将其应用于假设hbc，我们得到了一个结论的证明r a c。

在这种情况下，如果从 hab hbc 可以推断出 a b c，那么提供这些参数可能会很繁琐。因此，通常会将这些参数设为隐式的：

variable (α : Type) (r : α → α → Prop)
variable (trans_r : ∀ {x y z}, r x y → r y z → r x z)

variable (a b c : α)
variable (hab : r a b) (hbc : r b c)

#check trans_r
#check trans_r hab
#check trans_r hab hbc

好处是我们可以简单地写trans_r hab hbc来证明r a c。缺点是Lean没有足够的信息来推断表达式trans_r和trans_r hab的参数类型。第一个#check命令的输出是r ?m.1 ?m.2 → r ?m.2 ?m.3 → r ?m.1 ?m.3，表示在这种情况下隐式参数未指定。

以下是如何使用等价关系进行基本推理的示例：

variable (α : Type) (r : α → α → Prop)

variable (refl_r : ∀ x, r x x)
variable (symm_r : ∀ {x y}, r x y → r y x)
variable (trans_r : ∀ {x y z}, r x y → r y z → r x z)

example (a b c d : α) (hab : r a b) (hcb : r c b) (hcd : r c d) : r a d :=
  trans_r (trans_r hab (symm_r hcb)) hcd

为了熟悉使用全称量词，你应该尝试一下这节末尾的一些练习题。

正是依赖箭头类型的类型规则，尤其是普遍量化符号，使得 Prop 与其他类型有所区别。假设我们有 α : Sort i 和 β : Sort j，其中表达式 β 可能依赖于变量 x : α。然后 (x : α) → β 是 Sort (imax i j) 的一个元素，其中 imax i j 是如果 j 不为0，则为 i 和 j 的最大值，否则为0。

思路如下。如果 j 不是 0，那么 (x : α) → β 是 Sort (max i j) 的一个元素。换句话说，从 α 到 β 的依赖函数的类型 "存在" 在索引为 i 和 j 的最大值的宇宙中。然而，假设 β 是 Sort 0，即属于 Prop 的一个元素。在这种情况下，无论 α 生活在哪种类型宇宙中， (x : α) → β 也是 Sort 0 的一个元素。换句话说，如果 β 是依赖于 α 的命题，那么 ∀ x : α, β 再次是一个命题。这反映了将 Prop 解释为命题类型而不是数据类型的含义，并且正是这使得 Prop 不可谓的。

术语 "头等预测" 起源于二十世纪转折时期的基础研究，当时像庞加莱和罗素这样的逻辑学家归咎于集合论悖论，原因是当我们通过量化集合来定义属性时，就出现了 "恶性循环"。请注意，如果 α 是任意类型，我们可以构造类型 α → Prop，表示所有关于 α 的谓词的类型（α 的 "幂类型"）。Prop 的不可预测性意味着我们可以形成量化整个 α → Prop 的命题。特别地，我们可以通过量化所有关于 α 的谓词来定义关于 α 的谓词。 关于 Lean 定理证明

在 Lean 的定理证明库中，等式（equality） 是其中的一个最基本的关系。在 归纳类型（Inductive Types）章节 中，我们将解释 *等式是如何从 Lean 逻辑框架的基本元素中定义出来的。在此期间，我们将解释如何使用它。

当然，等式的一个基本性质就是它是一个等价关系：

#check Eq.refl    -- ∀ (a : ?m.1), a = a
#check Eq.symm    -- ?m.2 = ?m.3 → ?m.3 = ?m.2
#check Eq.trans   -- ?m.2 = ?m.3 → ?m.3 = ?m.4 → ?m.2 = ?m.4

我们可以通过告诉 Lean 不插入隐式参数（在这里显示为元变量）来使输出更易读。

universe u

#check @Eq.refl.{u}   -- ∀ {α : Sort u} (a : α), a = a
#check @Eq.symm.{u}   -- ∀ {α : Sort u} {a b : α}, a = b → b = a
#check @Eq.trans.{u}  -- ∀ {α : Sort u} {a b c : α}, a = b → b = c → a = c

LEᴀɴ θᴇᴏʀᴇᴍ-7: 给定一个类型A和x, y : A，表达式x = y（即x和y相等）类型为Pro p。

证明：通过引入类型 A，我们可以实例化上述引理以证明它对于任何类型 A 是成立的。假设A是一个类型，并且x, y : A是 A 上的任意两个元素。我们的目标是证明x = y是一个命题。

根据上述引理的定义，我们需要实例化它的类型为Type (max u v)，其中 u 和 v 是x和y所在的宇宙的级别。在此证明中，我们将使用它们的级别作为我们实例化的宇宙 u 和 v 的值。

此外，我们还需要为此引理提供其他的参数，例如x和y的类型，即A。此外，我们还需要提供一个以证明x = y的证据构造函数。

在这种情况下，由于我们没有提供任何特定的x和y的值，我们不能使用等价关系（=）的构造函数。相反，我们只需要证明在任何情况下，当x和y都被视为命题时，它们是相等的。

因此，我们可以确定x = y的类型为Prop，它是Type的一个子类型，用于表示命题。通过此推理，我们完成了对x = y是一个命题的证明。

因此，我们可以得出结论：对于任何类型A和x, y : A，表达式x = y是一个命题。

variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd

我们还可以使用投影符号表示：

# variable (α : Type) (a b c d : α)
# variable (hab : a = b) (hcb : c = b) (hcd : c = d)
example : a = d := (hab.trans hcb.symm).trans hcd

自反比它看起来更强大。回想一下，构造演算中的项具有计算解释，并且逻辑框架将具有共同还原的项视为相同。因此，一些非平凡的等式可以通过自反来证明：

variable (α β : Type)

example (f : α → β) (a : α) : (fun x => f x) a = f a := Eq.refl _
example (a : α) (b : β) : (a, b).1 = a := Eq.refl _
example : 2 + 3 = 5 := Eq.refl _

这个框架的这个特性非常重要，因此库为Eq.refl _定义了一个记号rfl：

# variable (α β : Type)
example (f : α → β) (a : α) : (fun x => f x) a = f a := rfl
example (a : α) (b : β) : (a, b).1 = a := rfl
example : 2 + 3 = 5 := rfl

然而，等式远不止是一种等价关系。它具有重要的性质，即每个命题都尊重等价关系，也就是说我们可以在不改变真值的情况下替换相等的表达式。换句话说，给定 h1: a = b 和 h2: p a，我们可以使用替换操作Eq.subst h1 h2 构建一个证明 p b。

example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2

第二个表达式中的三角形是在 Eq.subst 和 Eq.symm 之上构建的宏，你可以通过键入 \t 来输入它。

规则 Eq.subst 用于定义以下辅助规则，它们执行更明确的替换。它们旨在处理可应用项，即形如 s t 的项。具体来说，congrArg 可以用于替换参数，congrFun 可以用于替换被应用的项，congr 可以一次替换两者。

variable (α : Type)
variable (a b : α)
variable (f g : α → Nat)
variable (h₁ : a = b)
variable (h₂ : f = g)

example : f a = f b := congrArg f h₁
example : f a = g a := congrFun h₂ a
example : f a = g b := congr h₂ h₁

Lean 的库中包含大量常见的恒等式，比如这些：

• 对称律（Symmetry）：对于任意两个对象 P 和 Q，如果 P 等于 Q，那么 Q 也等于 P。
• 传递律（Transitivity）：对于任意三个对象 P、Q 和 R，如果 P 等于 Q，且 Q 等于 R，那么 P 等于 R。
• 自反性（Reflexivity）：对于任意对象 P，P 等于 P。
• 加法的单位元（Addition Identity）：对于任意对象 P，P 加 0 等于 P。
• 加法的逆元（Addition Inverse）：对于任意对象 P，存在一个对象 Q，使得 P 加 Q 等于 0。
• 乘法的单位元（Multiplication Identity）：对于任意对象 P，P 乘 1 等于 P。
• 乘法的逆元（Multiplication Inverse）：对于任意对象 P，如果 P 不等于 0，那么存在一个对象 Q，使得 P 乘 Q 等于 1。
• 乘法的分配律（Multiplication Distributivity）：对于任意三个对象 P、Q 和 R，(P 加 Q) 乘 R 等于 P 乘 R 加 Q 乘 R。

这些恒等式是数学中经常使用的基本原理，在 Lean 中被用来构建更复杂的证明。

variable (a b c : Nat)

example : a + 0 = a := Nat.add_zero a
example : 0 + a = a := Nat.zero_add a
example : a * 1 = a := Nat.mul_one a
example : 1 * a = a := Nat.one_mul a
example : a + b = b + a := Nat.add_comm a b
example : a + b + c = a + (b + c) := Nat.add_assoc a b c
example : a * b = b * a := Nat.mul_comm a b
example : a * b * c = a * (b * c) := Nat.mul_assoc a b c
example : a * (b + c) = a * b + a * c := Nat.mul_add a b c
example : a * (b + c) = a * b + a * c := Nat.left_distrib a b c
example : (a + b) * c = a * c + b * c := Nat.add_mul a b c
example : (a + b) * c = a * c + b * c := Nat.right_distrib a b c

注意，Nat.mul_add 和 Nat.add_mul 是 Nat.left_distrib 和 Nat.right_distrib 的另外两个名字。上述性质都是针对自然数（类型为 Nat）而言的。

这里是一个在自然数中使用替换、结合律和分配律进行计算的例子。

example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
  have h1 : (x + y) * (x + y) = (x + y) * x + (x + y) * y :=
    Nat.mul_add (x + y) x y
  have h2 : (x + y) * (x + y) = x * x + y * x + (x * y + y * y) :=
    (Nat.add_mul x y x) ▸ (Nat.add_mul x y y) ▸ h1
  h2.trans (Nat.add_assoc (x * x + y * x) (x * y) (y * y)).symm

注意到Eq.subst的第二个隐式参数，它提供了进行替换的上下文，类型为α → Prop。因此，推断此谓词需要一个高阶一致性实例。在完整的一般情况下，确定一个高阶一致性是否存在是不可判定的，而Lean在最佳情况下只能对这个问题提供不完美和近似的解决方案。因此，Eq.subst并不总能做到您希望的那样。宏h ▸ e使用了更有效的启发式方法来计算这个隐式参数，在应用Eq.subst失败的情况下通常会成功。

由于等式推理是如此常见和重要，Lean提供了一些机制来更有效地进行推理。下一节提供了一些语法，使您能够以更自然和清晰的方式编写计算证明。但是，更重要的是，等式推理还得到了术语重写器、简化器和其他类型的自动化支持。术语重写器和简化器在下一节中简要介绍，然后在下一章中详细描述。

计算证明

计算证明就是一个由中间结果构成的链条，这些中间结果可以通过基本原理（如等式的传递性）进行组合。在Lean中，计算证明以关键字calc开始，具有以下语法：

calc
  <expr>_0  'op_1'  <expr>_1  ':='  <proof>_1
  '_'       'op_2'  <expr>_2  ':='  <proof>_2
  ...
  '_'       'op_n'  <expr>_n  ':='  <proof>_n

注意，calc 关系的所有缩进都相同。每个 <proof>_i 都是 <expr>_{i-1} op_i <expr>_i 的一个证明。

我们还可以在第一个关系（紧跟着 <expr>_0 的右边）中使用 _，这有助于对齐关系/证明对的序列：

calc <expr>_0 
    '_' 'op_1' <expr>_1 ':=' <proof>_1
    '_' 'op_2' <expr>_2 ':=' <proof>_2
    ...
    '_' 'op_n' <expr>_n ':=' <proof>_n

这里是一个例子：

variable (a b c d e : Nat)
variable (h1 : a = b)
variable (h2 : b = c + 1)
variable (h3 : c = d)
variable (h4 : e = 1 + d)

theorem T : a = e :=
  calc
    a = b      := h1
    _ = c + 1  := h2
    _ = d + 1  := congrArg Nat.succ h3
    _ = 1 + d  := Nat.add_comm d 1
    _ = e      := Eq.symm h4

这种证明方法在与simp和rewrite策略结合使用时效果最好，这些策略将在下一章中详细讨论。例如，使用rw缩写为rewrite，上面的证明可以写作如下：

# variable (a b c d e : Nat)
# variable (h1 : a = b)
# variable (h2 : b = c + 1)
# variable (h3 : c = d)
# variable (h4 : e = 1 + d)
theorem T : a = e :=
  calc
    a = b      := by rw [h1]
    _ = c + 1  := by rw [h2]
    _ = d + 1  := by rw [h3]
    _ = 1 + d  := by rw [Nat.add_comm]
    _ = e      := by rw [h4]

实际上，rw 策略使用给定的等式（可以是假设、定理名或复杂的项）来“重写”目标。如果这样做将目标缩减为恒等式 t = t，则该策略将应用自反性来证明它。

重写可以按顺序应用，因此上述证明可以简化为以下形式：

# variable (a b c d e : Nat)
# variable (h1 : a = b)
# variable (h2 : b = c + 1)
# variable (h3 : c = d)
# variable (h4 : e = 1 + d)
theorem T : a = e :=
  calc
    a = d + 1  := by rw [h1, h2, h3]
    _ = 1 + d  := by rw [Nat.add_comm]
    _ = e      := by rw [h4]

甚至这样：

# variable (a b c d e : Nat)
# variable (h1 : a = b)
# variable (h2 : b = c + 1)
# variable (h3 : c = d)
# variable (h4 : e = 1 + d)
theorem T : a = e :=
  by rw [h1, h2, h3, Nat.add_comm, h4]

相反，simp策略通过重复应用给定的等式，以任意顺序和任何适用的位置，重写目标。它还使用了之前在系统中声明过的其他规则，并明智地应用交换律以避免循环。因此，我们可以通过以下方式证明该定理：

# variable (a b c d e : Nat)
# variable (h1 : a = b)
# variable (h2 : b = c + 1)
# variable (h3 : c = d)
# variable (h4 : e = 1 + d)
theorem T : a = e :=
  by simp [h1, h2, h3, Nat.add_comm, h4]

我们将在下一章讨论关于 rw 和 simp 的变化。

calc 命令可以配置成支持某种形式的可传递性的任意关系。甚至可以组合不同的关系。

example (a b c d : Nat) (h1 : a = b) (h2 : b ≤ c) (h3 : c + 1 < d) : a < d :=
  calc
    a = b     := h1
    _ < b + 1 := Nat.lt_succ_self b
    _ ≤ c + 1 := Nat.succ_le_succ h2
    _ < d     := h3

您可以通过添加 Trans 类型类的新实例来，“教” calc 新的传递性定理。类型类的介绍稍后会给出，但下面的小例子演示了如何使用新的 Trans 实例来扩展 calc 表示法。

class Trans (α : Type) : Type :=
  (trans : α → α → α)

instance add_trans : Trans nat :=
  ⟨λ a b, a + b⟩

instance mul_trans : Trans nat :=
  ⟨λ a b, a * b⟩

instance concat_trans : Trans string :=
  ⟨λ a b, a ++ b⟩

def calc {α : Type} [Trans α] := α

notation `⟦` a `⟧` := calc.eval a

infixl:1 "×" => Trans.trans
infixl:0 "+" => Trans.trans

def add_example : nat :=
  ⟦2 + 3 * 4⟧

def mul_example : nat :=
  ⟦2 × 3 + 4⟧

def concat_example : string :=
  ⟦"Hello, " ++ "World!"⟧

#reduce add_example
#reduce mul_example
#reduce concat_example

上述代码通过为 nat 和 string 类型分别创建了 Trans 实例 add_trans、mul_trans 和 concat_trans。这些实例定义了 trans 方法，该方法将两个值合并为一个值。

然后，我们定义了 calc 函数，该函数接受一个类型参数 α 和一个 Trans 实例。该函数通过 α 和 Trans 实例来确定要使用的运算符。

接下来，我们定义了 add_example、mul_example 和 concat_example 三个示例，它们使用了 calc 表示法来计算不同类型的表达式。

最后，我们使用 #reduce 命令分别计算了这三个示例。

def divides (x y : Nat) : Prop :=
  ∃ k, k*x = y

def divides_trans (h₁ : divides x y) (h₂ : divides y z) : divides x z :=
  let ⟨k₁, d₁⟩ := h₁
  let ⟨k₂, d₂⟩ := h₂
  ⟨k₁ * k₂, by rw [Nat.mul_comm k₁ k₂, Nat.mul_assoc, d₁, d₂]⟩

def divides_mul (x : Nat) (k : Nat) : divides x (k*x) :=
  ⟨k, rfl⟩

instance : Trans divides divides divides where
  trans := divides_trans

example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) :=
  calc
    divides x y     := h₁
    _ = z           := h₂
    divides _ (2*z) := divides_mul ..

infix:50 " ∣ " => divides

example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) :=
  calc
    x ∣ y   := h₁
    _ = z   := h₂
    _ ∣ 2*z := divides_mul ..

上面的例子还清楚地表明，即使您没有关于您的关系的中缀表示法，也可以使用calc。最后，我们注意到上面的例子中的垂直线符号∣是Unicode版本的。我们使用Unicode来确保不重载match .. with表达式中使用的ASCII字符|。

使用calc，我们可以以一种更自然和明了的方式编写上一节中的证明。

example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
  calc
    (x + y) * (x + y) = (x + y) * x + (x + y) * y  := by rw [Nat.mul_add]
    _ = x * x + y * x + (x + y) * y                := by rw [Nat.add_mul]
    _ = x * x + y * x + (x * y + y * y)            := by rw [Nat.add_mul]
    _ = x * x + y * x + x * y + y * y              := by rw [←Nat.add_assoc]

这里值得考虑使用一种叫 calc 的替代符号表示法。当第一个表达式占据了这么多空间时，在第一个关系中使用 _ 自然会对齐所有关系：

example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
  calc (x + y) * (x + y)
    _ = (x + y) * x + (x + y) * y       := by rw [Nat.mul_add]
    _ = x * x + y * x + (x + y) * y     := by rw [Nat.add_mul]
    _ = x * x + y * x + (x * y + y * y) := by rw [Nat.add_mul]
    _ = x * x + y * x + x * y + y * y   := by rw [←Nat.add_assoc]

这里 Nat.add_assoc 前面的箭头告诉 rewrite 在相反的方向上使用这个等式（你可以用 \l 输入它或者用 ASCII 码的等价表示 <-）。如果我们追求简洁， rw 和 simp 都可以单独完成这个任务：

example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
  by rw [Nat.mul_add, Nat.add_mul, Nat.add_mul, ←Nat.add_assoc]

example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
  by simp [Nat.mul_add, Nat.add_mul, Nat.add_assoc]

存在量化器

最后，考虑存在量化器，可以写作 exists x : α, p x 或者 ∃ x : α, p x。实际上，这两个版本都是更冗长表达式的便利缩写，即 Exists (fun x : α => p x)，在 Lean 的库中已经定义好了。

正如你现在所期望的那样，这个库包含引入规则和消除规则。引入规则很直接：要证明 ∃ x : α, p x，只需提供一个合适的项 t 和一个证明 p t。以下是一些例子：

example : ∃ x : Nat, x > 0 :=
  have h : 1 > 0 := Nat.zero_lt_succ 0
  Exists.intro 1 h

example (x : Nat) (h : x > 0) : ∃ y, y < x :=
  Exists.intro 0 h

example (x y z : Nat) (hxy : x < y) (hyz : y < z) : ∃ w, x < w ∧ w < z :=
  Exists.intro y (And.intro hxy hyz)

#check @Exists.intro

当上下文中的类型清晰时，我们可以使用匿名构造符号 ⟨t, h⟩ 来表示 Exists.intro t h。

example : ∃ x : Nat, x > 0 :=
  have h : 1 > 0 := Nat.zero_lt_succ 0
  ⟨1, h⟩

example (x : Nat) (h : x > 0) : ∃ y, y < x :=
  ⟨0, h⟩

example (x y z : Nat) (hxy : x < y) (hyz : y < z) : ∃ w, x < w ∧ w < z :=
  ⟨y, hxy, hyz⟩

注意，Exists.intro具有隐式参数：Lean必须推断出结论中的谓词p：α → Prop，即∃x，p x。这不是一个简单的事情。例如，如果我们有hg：g 0 0 = 0并写Exists.intro 0 hg，则谓词p可能有很多可能的值，对应于定理∃ x，g x x = x、∃ x，g x x = 0、∃ x，g x 0 = x等。Lean使用上下文推断哪一个是合适的。以下示例说明了此情况，在其中我们将选项pp.explicit设置为true，以要求Lean的漂亮打印机显示隐式参数。

variable (g : Nat → Nat → Nat)
variable (hg : g 0 0 = 0)

theorem gex1 : ∃ x, g x x = x := ⟨0, hg⟩
theorem gex2 : ∃ x, g x 0 = x := ⟨0, hg⟩
theorem gex3 : ∃ x, g 0 0 = x := ⟨0, hg⟩
theorem gex4 : ∃ x, g x x = 0 := ⟨0, hg⟩

set_option pp.explicit true  -- display implicit arguments
#print gex1
#print gex2
#print gex3
#print gex4

我们可以将 Exists.intro 视为一种信息隐藏的操作，因为它隐藏了对断言主体的见证。 存在消去规则 Exists.elim 执行相反的操作。 它允许我们从 ∃ x : α，p x 来证明一个命题 q，通过展示对于任意值 w，q 从 p w 推导出来。 粗略地说，由于我们知道存在满足 p x 的 x，我们可以给它一个名字，比如 w。 如果 q 不提及 w，那么展示 q 从 p w 推导出来等价于展示 q 从任何这样的 x 的存在推导出来。 这是一个例子：

variable (α : Type) (p q : α → Prop)

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  Exists.elim h
    (fun w =>
     fun hw : p w ∧ q w =>
     show ∃ x, q x ∧ p x from ⟨w, hw.right, hw.left⟩)

对于存在消去规则，与“或”消去法进行比较可能会有所帮助：命题“∃ x : α, p x”可以被看作命题“p a”的一个大的析取，其中“a”遍历整个“α”。请注意，匿名构造符号“⟨w, hw.right, hw.left⟩”是一个嵌套构造应用的缩写；我们同样可以写作“⟨w, ⟨hw.right, hw.left⟩⟩”。

注意，存在命题与Σ类型非常相似，正如在依赖类型部分中所描述的那样。区别在于给定“a : α”和“h : p a”，术语“Exists.intro a h”的类型为“(∃ x : α, p x) : Prop”，而“Sigma.mk a h”的类型为“(Σ x : α, p x) : Type”。∃和Σ之间的相似性是柯里-霍华德同构的另一个例子。

Lean提供了一种更方便的方法来通过“match”表达式消去存在量词：

variable (α : Type) (p q : α → Prop)

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  match h with
  | ⟨w, hw⟩ => ⟨w, hw.right, hw.left⟩

match表达式是Lean函数定义系统的一部分，它提供了定义复杂函数的便捷且表达力强的方法。再次地，正是Curry-Howard同构使得我们能够利用这个机制来编写证明。match语句将存在断言“解构”为组件w和hw，然后可以在语句的主体中使用它们来证明命题。我们可以为匹配中使用的类型添加注释以增加清晰度：

# variable (α : Type) (p q : α → Prop)
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  match h with
  | ⟨(w : α), (hw : p w ∧ q w)⟩ => ⟨w, hw.right, hw.left⟩

我们甚至可以使用 match 语句同时分解合取式：

variables P Q R : Prop

example (h : P ∧ Q ∧ R) : P ∧ Q :=
match h with ⟨hp, hq, _⟩ :=
  ⟨hp, hq⟩
end

在这个例子中，我们假设了一个命题 P、Q 和 R 构成的合取式 h，我们想要证明 P ∧ Q。我们使用 match 语句来分解合取式 h，并将分解得到的 P 和 Q 分别命名为 hp 和 hq。然后我们使用构造子 ⟨⟩ 来重新构建合取式，得到证明 ⟨hp, hq⟩。最后我们使用 match 语句的结束符号 end 表示 match 语句结束。由于我们只关心 P 和 Q，所以我们对 R 不做任何处理。因此，我们成功地将合取式 h 分解为 P 和 Q。

# variable (α : Type) (p q : α → Prop)
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  match h with
  | ⟨w, hpw, hqw⟩ => ⟨w, hqw, hpw⟩

Lean 还提供了一种模式匹配的 let 表达式：

# variable (α : Type) (p q : α → Prop)
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  let ⟨w, hpw, hqw⟩ := h
  ⟨w, hqw, hpw⟩

这实质上只是上述 match 构造的一种替代表示方法。Lean 甚至允许我们在 fun 表达式中使用隐式 match：

# variable (α : Type) (p q : α → Prop)
example : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x :=
  fun ⟨w, hpw, hqw⟩ => ⟨w, hqw, hpw⟩

我们将在 归纳与递归章节 中看到，所有这些变体都是更一般的模式匹配结构的实例。

在下面的示例中，我们将 is_even a 定义为 ∃ b, a = 2 * b，然后我们证明两个偶数的和仍然是一个偶数。

def is_even (a : Nat) := ∃ b, a = 2 * b

theorem even_plus_even (h1 : is_even a) (h2 : is_even b) : is_even (a + b) :=
  Exists.elim h1 (fun w1 (hw1 : a = 2 * w1) =>
  Exists.elim h2 (fun w2 (hw2 : b = 2 * w2) =>
    Exists.intro (w1 + w2)
      (calc a + b
        _ = 2 * w1 + 2 * w2 := by rw [hw1, hw2]
        _ = 2 * (w1 + w2)   := by rw [Nat.mul_add])))

使用本章描述的各种工具——匹配语句、匿名构造函数和“rewrite”策略，我们可以将此证明简洁地写成如下形式：

# def is_even (a : Nat) := ∃ b, a = 2 * b
theorem even_plus_even (h1 : is_even a) (h2 : is_even b) : is_even (a + b) :=
  match h1, h2 with
  | ⟨w1, hw1⟩, ⟨w2, hw2⟩ => ⟨w1 + w2, by rw [hw1, hw2, Nat.mul_add]⟩

正如构造上的“或”比经典上的“或”更强，构造上的“存在”也比经典上的“存在”更强。举个例子，以下蕴含关系需要经典的推理，因为从构造的角度来看，知道并非每个“x”满足“¬p”并不等同于找到一个特定的“x”满足“p”。

open Classical
variable (p : α → Prop)

example (h : ¬ ∀ x, ¬ p x) : ∃ x, p x :=
  byContradiction
    (fun h1 : ¬ ∃ x, p x =>
      have h2 : ∀ x, ¬ p x :=
        fun x =>
        fun h3 : p x =>
        have h4 : ∃ x, p x := ⟨x, h3⟩
        show False from h1 h4
      show False from h h2)

以下是一些涉及存在量词的常见等式。在下面的练习中，我们鼓励您尽可能证明更多的等式。我们也让您自行确定哪些是非构造性的，因此需要某种形式的古典推理。

open Classical

variable (α : Type) (p q : α → Prop)
variable (r : Prop)

example : (∃ x : α, r) → r := sorry
example (a : α) : r → (∃ x : α, r) := sorry
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r := sorry
example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) := sorry

example : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) := sorry
example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) := sorry
example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) := sorry
example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := sorry

example : (∀ x, p x → r) ↔ (∃ x, p x) → r := sorry
example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r := sorry
example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) := sorry

请注意，第二个示例和最后两个示例需要作出假设：至少存在一个类型为 α 的元素 a。

以下是两个较难示例的解决方案：

open Classical

variable (α : Type) (p q : α → Prop)
variable (a : α)
variable (r : Prop)

example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
  Iff.intro
    (fun ⟨a, (h1 : p a ∨ q a)⟩ =>
      Or.elim h1
        (fun hpa : p a => Or.inl ⟨a, hpa⟩)
        (fun hqa : q a => Or.inr ⟨a, hqa⟩))
    (fun h : (∃ x, p x) ∨ (∃ x, q x) =>
      Or.elim h
        (fun ⟨a, hpa⟩ => ⟨a, (Or.inl hpa)⟩)
        (fun ⟨a, hqa⟩ => ⟨a, (Or.inr hqa)⟩))

example : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
  Iff.intro
    (fun ⟨b, (hb : p b → r)⟩ =>
     fun h2 : ∀ x, p x =>
     show r from hb (h2 b))
    (fun h1 : (∀ x, p x) → r =>
     show ∃ x, p x → r from
       byCases
         (fun hap : ∀ x, p x => ⟨a, λ h' => h1 hap⟩)
         (fun hnap : ¬ ∀ x, p x =>
          byContradiction
            (fun hnex : ¬ ∃ x, p x → r =>
              have hap : ∀ x, p x :=
                fun x =>
                byContradiction
                  (fun hnp : ¬ p x =>
                    have hex : ∃ x, p x → r := ⟨x, (fun hp => absurd hp hnp)⟩
                    show False from hnex hex)
              show False from hnap hap)))

关于证明语言的更多内容

我们已经看到，“fun”、“have”和“show”等关键字使得我们可以编写形式化证明项，这些证明项与非形式化的数学证明结构相似。在本节中，我们将讨论一些通常方便的证明语言的其他特性。

首先，我们可以使用匿名的“have”表达式引入辅助目标，而无需为其添加标签。我们可以使用关键字“this”引用以这种方式引入的最后一个表达式：

variable (f : Nat → Nat)
variable (h : ∀ x : Nat, f x ≤ f (x + 1))

example : f 0 ≤ f 3 :=
  have : f 0 ≤ f 1 := h 0
  have : f 0 ≤ f 2 := Nat.le_trans this (h 1)
  show f 0 ≤ f 3 from Nat.le_trans this (h 2)

通常证明会从一个事实转移到另一个事实，这样可以有效地消除大量标签的混乱。

当目标可以被推断出来时，我们还可以要求 Lean 通过写入“by assumption”来填充证明：

# variable (f : Nat → Nat)
# variable (h : ∀ x : Nat, f x ≤ f (x + 1))
example : f 0 ≤ f 3 :=
  have : f 0 ≤ f 1 := h 0
  have : f 0 ≤ f 2 := Nat.le_trans (by assumption) (h 1)
  show f 0 ≤ f 3 from Nat.le_trans (by assumption) (h 2)

这样告诉 Lean 使用 assumption 策略，该策略通过在局部上下文中找到合适的假设来证明目标。我们将在下一章中更多地了解 assumption 策略。

我们也可以要求 Lean 在证明中填入 ‹p›，其中 p 是我们想要 Lean 在上下文中找到的命题的证明。你可以使用 \f< 和 \f> 输入这些引号。字母 "f" 代表 "French"，因为这些 unicode 符号也可以用作法语引号。实际上，该符号在 Lean 中的表示方式如下：

notation "‹" p "›" => show p by assumption

这种方法比使用“假设”的方法更加稳健，因为需要推断的假设的类型是明确给出的。它使得证明更容易阅读。下面是一个更详细的示例：

variable (f : Nat → Nat)
variable (h : ∀ x : Nat, f x ≤ f (x + 1))

example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 :=
  fun _ : f 0 ≥ f 1 =>
  fun _ : f 1 ≥ f 2 =>
  have : f 0 ≥ f 2 := Nat.le_trans ‹f 1 ≥ f 2› ‹f 0 ≥ f 1›
  have : f 0 ≤ f 2 := Nat.le_trans (h 0) (h 1)
  show f 0 = f 2 from Nat.le_antisymm this ‹f 0 ≥ f 2›

请记住，在这种情况下你可以使用法语引号来引用“任何”上下文中的内容，不仅仅限于匿名引入的事物。它的使用也不限于命题，尽管将其用于数据有些奇怪：

example (n : Nat) : Nat := ‹Nat›

以后我们将展示如何使用 Lean 的宏系统扩展证明语言。

练习

1. 证明以下等价关系：

variable (α : Type) (p q : α → Prop)

example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := sorry
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) := sorry
example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x := sorry

你也应该尝试理解为什么在最后一个例子中无法推导出反向蕴含。

2. 当一个组成公式的部分不依赖于量化变量时，通常可以将其从普遍量词外部提取出来。尝试证明以下命题（第二个命题的一个方向需要使用经典逻辑）：

variable (α : Type) (p q : α → Prop)
variable (r : Prop)

example : α → ((∀ x : α, r) ↔ r) := sorry
example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := sorry
example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := sorry

3. 考虑“理发师悖论”，即在某个城镇中存在一个（男性）理发师，他为所有不给自己刮脸的男人刮脸，而仅仅为这些男人刮脸。证明这是一个矛盾的陈述：

Assume that such a barber exists in the town. Let's denote this barber as B. 假设这个城镇中存在这样一位理发师。我们用 B 表示这个理发师。

Now, we consider the question of whether B shaves himself or not. There are two possibilities: 现在，我们考虑 B 是否给自己刮脸。有两种可能性：

1. If B shaves himself, then according to the statement of the paradox, B should not shave himself since he only shaves the men who do not shave themselves. This leads to a contradiction because B cannot simultaneously shave himself and not shave himself. 如果 B 给自己刮脸，根据悖论陈述，B 不应该给自己刮脸，因为他只为不给自己刮脸的男人刮脸。这会导致一个矛盾，因为 B 不能同时给自己刮脸和不给自己刮脸。

2. If B does not shave himself, then according to the statement of the paradox, B should shave himself since he shaves all the men who do not shave themselves. Again, this leads to a contradiction because B cannot simultaneously shave himself and not shave himself. 如果 B 不给自己刮脸，根据悖论陈述，B 应该给自己刮脸，因为他为所有不给自己刮脸的男人刮脸。同样，这会导致一个矛盾，因为 B 不能同时给自己刮脸和不给自己刮脸。

In both cases, we arrive at a contradiction. Therefore, it is impossible for such a barber to exist in the town. This paradox demonstrates the self-referential nature of the barber's statement and the logical inconsistency it leads to. 无论哪种情况，我们都得到了一个矛盾。因此，在这个城镇中不可能存在这样一位理发师。这个悖论展示了理发师陈述的自我参照性质以及由此引发的逻辑不一致性。

variable (men : Type) (barber : men)
variable (shaves : men → men → Prop)

example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := sorry

4. 记住，如果没有任何参数，类型为 Prop 的表达式只是一个断言。请填写下面的 prime 和 Fermat_prime 的定义，并构建每个给定的断言。例如，您可以通过断言对于每个自然数 n，存在一个大于 n 的质数来表明存在无穷多个质数。哥德巴赫猜想认为，每个大于5的奇数都可以被三个质数相加。如果需要的话，请查找 Fermat 质数的定义或其它陈述的定义。

def even (n : Nat) : Prop := sorry

def prime (n : Nat) : Prop := sorry

def infinitely_many_primes : Prop := sorry

def Fermat_prime (n : Nat) : Prop := sorry

def infinitely_many_Fermat_primes : Prop := sorry

def goldbach_conjecture : Prop := sorry

def Goldbach's_weak_conjecture : Prop := sorry

def Fermat's_last_theorem : Prop := sorry

翻译

5. 尽可能证明存在量词部分列出的所有恒等式。

在这里，我们将尝试证明 Existential Quantifier 部分列出的一些恒等式。

1. ∃x P(x) ∨ ∃x Q(x) ⇔ ∃x (P(x) ∨ Q(x))*

假设存在某个元素 x，它满足性质 P(x) 或者存在某个元素 x，它满足性质 Q(x)。我们想要证明：存在某个元素 x，它同时满足 P(x) 或 Q(x)。

根据 Logic 中的合取分配律，我们可以将此恒等式拆分为两个分支进行证明。

分支1：假设存在某个元素 x，它满足性质 P(x)。那么存在某个元素 x，它同时满足 P(x) 或 Q(x)。

分支2：假设存在某个元素 x，它满足性质 Q(x)。那么存在某个元素 x，它同时满足 P(x) 或 Q(x)。

根据合取分配律，我们可以得出：存在某个元素 x，它同时满足 P(x) 或 Q(x)。因此，恒等式成立。

2. ∃x P(x) ∧ ∃x Q(x) ⇔ ∃x (P(x) ∧ Q(x))*

假设存在某个元素 x，它满足性质 P(x) 和存在某个元素 x，它满足性质 Q(x)。我们想要证明：存在某个元素 x，它同时满足 P(x) 和 Q(x)。

根据 Logic 中的析取分配律，我们可以将此恒等式拆分为两个分支进行证明。

分支1：假设存在某个元素 x，它满足性质 P(x)。那么存在某个元素 x，它同时满足 P(x) 和 Q(x)。

分支2：假设存在某个元素 x，它满足性质 Q(x)。那么存在某个元素 x，它同时满足 P(x) 和 Q(x)。

根据析取分配律，我们可以得出：存在某个元素 x，它同时满足 P(x) 和 Q(x)。因此，恒等式成立。

3. ¬(∃x P(x)) ⇔ ∀x ¬P(x)*

假设不存在任何元素 x，它满足性质 P(x)。我们想要证明：对于所有的元素 x，它都不满足性质 P(x)。

根据 Logic 中否定的存在量词规则，我们可以得出：对于所有的元素 x，它都不满足性质 P(x)。因此，恒等式成立。

4. ∀x (P(x)∨ Q(x)) ⇔ (∀x P(x)) ∨ (∀x Q(x))*

对于所有的元素 x，它满足性质 P(x) 或 Q(x)。我们想要证明：对于所有的元素 x，它满足性质 P(x) 或对于所有的元素 x，它满足性质 Q(x)。

根据 Logic 中析取的全称量词规则，我们可以将此恒等式拆分为两个分支进行证明。

分支1：对于所有的元素 x，它满足性质 P(x)。那么对于所有的元素 x，它满足性质 P(x) 或对于所有的元素 x，它满足性质 Q(x)。

分支2：对于所有的元素 x，它满足性质 Q(x)。那么对于所有的元素 x，它满足性质 P(x) 或对于所有的元素 x，它满足性质 Q(x)。

根据析取的全称量词规则，我们可以得出：对于所有的元素 x，它满足性质 P(x) 或对于所有的元素 x，它满足性质 Q(x)。因此，恒等式成立。

这是我们能够证明的一些存在量词部分列出的恒等式。其他的恒等式可能需要使用不同的推理法则或证明方式来完成。

策略

在这一章中，我们将介绍一种构建证明的替代方法，使用 策略。证明项是数学证明的一种表示；策略是一种命令或指令，描述如何构建这样的证明。简单地说，您可能开始一个数学证明时会说“为了证明正向推理，展开定义，应用前一个引理，并化简。”就像这些是告诉读者如何找到相关证明的指示一样，策略是告诉 Lean 如何构建一个证明项的指令。它们自然地支持一种逐步编写证明的风格，您可以将证明分解并逐步处理目标。

我们将由一系列策略组成的证明称为“策略样式”证明，以与我们目前已经见过的编写证明项的方式相对比，后者被称为“术语样式”证明。每种样式都有其优点和缺点。例如，策略样式的证明可能更难阅读，因为它们要求读者预测或猜测每个指令的结果。但它们也可以更短更容易编写。此外，策略为使用 Lean 的自动化提供了一个入口，因为自动化过程本身也是策略。

进入策略模式

从概念上讲，陈述一个定理或引入一个have语句都会创建一个目标，即构造一个具有预期类型的项。例如，下面的代码会创建一个目标，需要构造一个类型为p ∧ q ∧ p的项，在上下文中有常数p q : Prop，hp : p和hq : q：

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p :=
  sorry

你可以将这个目标写成以下形式：

    p : Prop, q : Prop, hp : p, hq : q ⊢ p ∧ q ∧ p

确实，在上面的例子中，如果你将 "sorry" 替换为空白符号，Lean 将报告这个目标没有被解决。

通常，你可以通过编写一个明确的术语来达成这个目标。然而，当需要一个术语的地方，Lean 允许我们插入一个 by <tactics> 块，其中 <tactics> 是一系列通过分号或换行符分隔的命令。你可以通过以下方式证明上述定理：

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p :=
  by apply And.intro
     exact hp
     apply And.intro
     exact hq
     exact hp

我们通常将 by 关键字放在前一行，并将上面的示例写为：

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
  apply And.intro
  exact hp
  apply And.intro
  exact hq
  exact hp

apply策略将一个表达式应用于一个被视为具有零个或多个参数的函数。它将当前目标的结论与表达式进行统一，并为剩余的参数创建新的子目标，前提是后续参数不依赖于它们。在上面的例子中，命令 apply And.intro 生成了两个子目标：

    case left
    p q : Prop
    hp : p
    hq : q
    ⊢ p

    case right
    p q : Prop
    hp : p
    hq : q
    ⊢ q ∧ p

第一个目标通过命令 exact hp 实现。exact 命令是 apply 的一种变体，用于指示给定的表达式应该完全填充目标。在策略证明中使用它是好的做法，因为它的失败会提示出现了问题。与 apply 相比，exact 更可靠，因为在处理应用的表达式时，解析器会考虑目标的预期类型。然而，在这种情况下，apply 也同样适用。

您可以使用 #print 命令查看生成的证明项（proof term）：

# theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
#  apply And.intro
#  exact hp
#  apply And.intro
#  exact hq
#  exact hp
#print test

你可以逐步编写一个策略脚本。在 VS Code 中，按下 Ctrl-Shift-Enter 可以打开一个窗口显示消息，当光标在策略块中时，该窗口会显示当前的目标。在 Emacs 中，按下 C-c C-g 会在任意行的末尾显示目标，或者在不完整的证明中将光标放在最后一个策略的第一个字符之后以查看剩余的目标。如果证明不完整，关键字 by 将会被一个红色波浪线标记，错误消息中也会包含剩余的目标。

策略命令可以接受复合表达式，而不仅仅是单个标识符。下面是前面证明的较短版本：

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
  apply And.intro hp
  exact And.intro hq hp

不出意外，它产生了完全相同的证明术语。

# theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
#  apply And.intro hp
#  exact And.intro hq hp
#print test

多个策略应用可以通过分号连接在一行上写出。

这是因为 Lean 每行只执行一个策略应用，但是可以通过在每个策略应用之间添加分号来在一行中一次性应用多个策略。这种写法能够提高代码的紧凑性和可读性。

在 Lean 中，策略（tactic）是一种用于构造和变换证明的指令。它们可以被应用于目标（goal）或者证明的间断点（proof state）。策略的应用会改变目标或证明的状态，并且可以用于引入、消去、重写等操作。使用策略可以帮助我们更有效地构建证明。

例如，假设我们有两个策略 tac1 和 tac2，并且我们想在当前的目标上依次应用这两个策略。我们可以在一行中使用分号将它们连接起来，如下所示：

tac1; tac2

这将首先应用 tac1 策略，然后将 tac2 策略应用于产生的证明状态。通过这种方式，我们可以在一行中一次性应用多个策略，简化证明过程。

总而言之，通过在 Lean 中使用分号来连接多个策略的应用，我们可以在一行上写出多个策略的代码，提高代码的紧凑性和可读性。

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
  apply And.intro hp; exact And.intro hq hp

可能会产生多个子目标的策略通常会给它们加上标签。例如，策略 apply And.intro 将第一个子目标标记为 left，第二个子目标标记为 right。对于 apply 策略，标签是从 And.intro 声明中使用的参数名推断出来的。您可以使用记法 case <tag> => <tactics> 来结构化您的策略。以下是我们在本章中第一个策略证明的结构化版本。

Lemma and_commutative :
  forall P Q : Prop, P /\ Q -> Q /\ P.
Proof.
  intros P Q H.
  apply And.intro as left.
  case left.
    intros p q.
    apply And.intro.
      exact q.
      exact p.
Qed.

这个例子中，我们给 apply And.intro 的第一个子目标加上了标签 left。然后，我们根据标签来结构化策略并进行证明。在 case left 中，我们使用了 intros p q 来引入标记为 left 的子目标的假设，并使用 apply And.intro 来继续证明。最后，我们使用了 exact 策略来完成证明。

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
  apply And.intro
  case left => exact hp
  case right =>
    apply And.intro
    case left => exact hq
    case right => exact hp

你可以使用case符号在解决left之前解决子目标right：

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
  apply And.intro
  case right =>
    apply And.intro
    case left => exact hq
    case right => exact hp
  case left => exact hp

请注意，Lean 将其他目标隐藏在 case 块中。我们称之为“聚焦”在所选目标上。此外，如果所选目标在 case 块结束时没有完全解决，Lean 会报错。

对于简单的子目标来说，可能没有必要使用标签选择子目标，但你可能仍然希望结构化证明。Lean 还提供了“bullet”符号的记法. <策略>（或 · <策略>）用于结构化证明。

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
  apply And.intro
  . exact hp
  . apply And.intro
    . exact hq
    . exact hp

基本策略

除了 apply 和 exact 外，另一个有用的策略是 intro，它引入了一个假设。接下来是一个在前一章中我们在命题逻辑中证明的恒等式的例子，现在我们将使用策略来证明它。

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro h
    apply Or.elim (And.right h)
    . intro hq
      apply Or.inl
      apply And.intro
      . exact And.left h
      . exact hq
    . intro hr
      apply Or.inr
      apply And.intro
      . exact And.left h
      . exact hr
  . intro h
    apply Or.elim h
    . intro hpq
      apply And.intro
      . exact And.left hpq
      . apply Or.inl
        exact And.right hpq
    . intro hpr
      apply And.intro
      . exact And.left hpr
      . apply Or.inr
        exact And.right hpr

intro 命令可以更一般地用于引入任意类型的变量：

example (α : Type) : α → α := by
  intro a
  exact a

example (α : Type) : ∀ x : α, x = x := by
  intro x
  exact Eq.refl x

可以使用它来介绍几个变量：

example : ∀ a b c : Nat, a = b → a = c → c = b := by
  intro a b c h₁ h₂
  exact Eq.trans (Eq.symm h₂) h₁

正如apply策略用于交互式构建函数应用一样，intro策略用于交互式构建函数抽象（例如，fun x => e形式的项）。与lambda抽象记法一样，intro策略允许我们使用隐式的match。

example (α : Type) (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
  intro ⟨w, hpw, hqw⟩
  exact ⟨w, hqw, hpw⟩

你还可以像 match 表达式一样提供多个选择。

example (α : Type) (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := by
  intro
  | ⟨w, Or.inl h⟩ => exact ⟨w, Or.inr h⟩
  | ⟨w, Or.inr h⟩ => exact ⟨w, Or.inl h⟩

intros 策略可以在没有参数的情况下使用，此时它会选择变量的名称并引入尽可能多的变量。您即将看到一个示例。

assumption 策略会查找上下文中与当前目标匹配的假设，如果找到匹配的假设，则应用该假设。

example (x y z w : Nat) (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := by
  apply Eq.trans h₁
  apply Eq.trans h₂
  assumption   -- applied h₃

必要时，它会统一结论中的元变量：

example (x y z w : Nat) (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := by
  apply Eq.trans
  assumption      -- solves x = ?b with h₁
  apply Eq.trans
  assumption      -- solves y = ?h₂.b with h₂
  assumption      -- solves z = w with h₃

下面的示例使用 intros 命令自动引入三个变量和两个假设：

example : ∀ a b c : Nat, a = b → a = c → c = b := by
  intros
  apply Eq.trans
  apply Eq.symm
  assumption
  assumption

请注意，默认情况下，Lean 自动生成的名称是不可访问的。这么做的目的是确保你的策略证明不依赖于自动生成的名称，从而使其更加健壮。但是，你可以使用组合子 unhygienic 来取消此限制。

example : ∀ a b c : Nat, a = b → a = c → c = b := by unhygienic
  intros
  apply Eq.trans
  apply Eq.symm
  exact a_2
  exact a_1

你还可以使用 rename_i 策略来重命名上下文中最近不可访问的名称。 在下面的例子中，策略 rename_i h1 _ h2 重命名了上下文中最后三个假设中的两个。

example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := by
  intros
  rename_i h1 _ h2
  apply Eq.trans
  apply Eq.symm
  exact h2
  exact h1

rfl 策略是 exact rfl 的语法糖。

example (y : Nat) : (fun x : Nat => 0) y = 0 :=
  by rfl

repeat 组合子可以用来多次应用一种策略。

example : ∀ a b c : Nat, a = b → a = c → c = b := by
  intros
  apply Eq.trans
  apply Eq.symm
  repeat assumption

有时候，另一种有用的策略是revert策略，从某种意义上说，它是intro的逆向操作。

example (x : Nat) : x = x := by
  revert x
  -- goal is ⊢ ∀ (x : Nat), x = x
  intro y
  -- goal is y : Nat ⊢ y = y
  rfl

将一个假设移动到目标中，可以得到一个蕴含关系：

H : P
============================
P

In Lean, we can write this as:

example (P : Prop) (H : P) : P := H

Here, P represents a proposition (an assertion or a statement), and H represents a proof or evidence for P. The goal is to prove P using the hypothesis H. In Lean, the example keyword is used to introduce a new theorem or lemma. The proof is simply the hypothesis H itself, as it already provides the evidence needed to prove P. Therefore, by applying H as the proof, we can conclude that P is true.

example (x y : Nat) (h : x = y) : y = x := by
  revert h
  -- goal is x y : Nat ⊢ x = y → y = x
  intro h₁
  -- goal is x y : Nat, h₁ : x = y ⊢ y = x
  apply Eq.symm
  assumption

但是 revert 更加聪明，不仅会还原上下文中的一个元素，还会还原依赖于它的所有后续元素。例如，在上面的例子中，还原 x 会同时带回 h：

example (x y : Nat) (h : x = y) : y = x := by
  revert x
  -- goal is y : Nat ⊢ ∀ (x : Nat), x = y → y = x
  intros
  apply Eq.symm
  assumption

您也可以一次撤销多个上下文元素:

example (x y : Nat) (h : x = y) : y = x := by
  revert x y
  -- goal is ⊢ ∀ (x y : Nat), x = y → y = x
  intros
  apply Eq.symm
  assumption

你只能 revert 本地上下文中的一个元素，也就是局部变量或假设。但是你可以使用 generalize 策略，将目标中的任意表达式替换为一个新的变量。

example : 3 = 3 := by
  generalize 3 = x
  -- goal is x : Nat ⊢ x = x
  revert x
  -- goal is ⊢ ∀ (x : Nat), x = x
  intro y
  -- goal is y : Nat ⊢ y = y
  rfl

上述表示法中的助记符是，通过将 "3" 设置为一个任意变量 "x"，对目标进行泛化。注意：并非每个泛化都能保持目标的有效性。在这里，"generalize" 替换了一个可以使用 "rfl" 证明的目标，变为了一个不可证明的目标：

example : 2 + 3 = 5 := by
  generalize 3 = x
  -- goal is x : Nat ⊢ 2 + x = 5
  admit

在这个例子中，admit 策略是 sorry 证明项的类比。它关闭当前的目标，并产生通常的警告，表明sorry 已被使用。为了保留先前目标的有效性，generalize 策略允许我们记录3被x替代的事实。您只需要提供一个标签，generalize 将使用它来将分配存储在本地上下文中：

example : 2 + 3 = 5 := by
  generalize h : 3 = x
  -- goal is x : Nat, h : 3 = x ⊢ 2 + x = 5
  rw [← h]

rewrite 策略使用 h 来再次用 3 替换 x。下面将讨论 rewrite 策略。

更多策略

有一些附加的策略对于构造和析构命题和数据很有用。例如，当应用于形式为 p ∨ q 的目标时，你可以使用诸如 apply Or.inl 和 apply Or.inr 的策略。反过来，cases 策略可以用于分解一个或关系。

example (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  cases h with
  | inl hp => apply Or.inr; exact hp
  | inr hq => apply Or.inl; exact hq

注意，语法与 match 表达式中使用的语法相似。 新的子目标可以以任何顺序解决。

example (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  cases h with
  | inr hq => apply Or.inl; exact hq
  | inl hp => apply Or.inr; exact hp

你也可以使用一个（非结构化的）不带 with 的 cases 结构以及为每个分支使用一个策略。

example (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  cases h
  apply Or.inr
  assumption
  apply Or.inl
  assumption

(unstructured) cases 在你可以使用同一个策略关闭多个子目标时特别有用。

example (p : Prop) : p ∨ p → p := by
  intro h
  cases h
  repeat assumption

您还可以使用组合符号tac1 <;> tac2，将tac2应用于tac1产生的每个子目标。

example (p : Prop) : p ∨ p → p := by
  intro h
  cases h <;> assumption

您可以将 cases 策略与 case 和 . 符号结合使用。

example (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  cases h
  . apply Or.inr
    assumption
  . apply Or.inl
    assumption

example (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  cases h
  case inr h =>
    apply Or.inl
    assumption
  case inl h =>
    apply Or.inr
    assumption

example (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  cases h
  case inr h =>
    apply Or.inl
    assumption
  . apply Or.inr
    assumption

cases策略也可以用于分解合取式。

在 Lean 中，合取式是由逻辑“与”操作符∧连接的两个或多个命题。使用cases策略来分解合取式，可以把一个合取式分解为多个子目标，并分别处理每个子目标。

下面是一个示例：

example (P Q : Prop) : P ∧ Q → (P → Q) :=
begin
  intro h,
  cases h with hP hQ,
  intro h'P,
  exact hQ
end

在这个例子中，我们假设P和Q是命题，P ∧ Q是一个合取式。我们的目标是证明P ∧ Q蕴含P → Q。首先使用intro策略引入前提假设h : P ∧ Q，然后使用cases策略分解合取式，得到两个子目标：hP : P和hQ : Q。接着，使用intro策略引入新的前提假设h'P : P，最后使用exact策略证明Q，从而完成了证明。

通过使用cases策略，在拥有合取式的证明中可以更方便地处理每个子目标，从而推导出相应的结论。

example (p q : Prop) : p ∧ q → q ∧ p := by
  intro h
  cases h with
  | intro hp hq => constructor; exact hq; exact hp

在这个例子中，cases策略应用后只有一个目标，h : p ∧ q 被一对假设hp : p 和 hq : q 替换。constructor策略应用了合取的唯一构造子And.intro。通过使用这些策略，前一节中的一个例子可以重写如下：

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro h
    cases h with
    | intro hp hqr =>
      cases hqr
      . apply Or.inl; constructor <;> assumption
      . apply Or.inr; constructor <;> assumption
  . intro h
    cases h with
    | inl hpq =>
      cases hpq with
      | intro hp hq => constructor; exact hp; apply Or.inl; exact hq
    | inr hpr =>
      cases hpr with
      | intro hp hr => constructor; exact hp; apply Or.inr; exact hr

你将在 归纳类型章节 中看到，这些策略非常通用。 cases 策略可以用于分解归纳定义类型的任何元素；constructor 总是应用归纳定义类型的第一个可用构造函数。例如，你可以使用 cases 和 constructor 来处理存在量词的情况：

example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := by
  intro h
  cases h with
  | intro x px => constructor; apply Or.inl; exact px

在这里，constructor 策略将存在量化命题的第一个组成部分 x 的值留下隐含。它由一个元变量表示，应该在后面被实例化。在前面的例子中，元变量的正确值由策略 exact px 决定，因为 px 的类型是 p x。如果您想明确指定对存在量词的见证，可以使用 exists 策略替代：

example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := by
  intro h
  cases h with
  | intro x px => exists x; apply Or.inl; exact px

这里是另一个例子：

example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
  intro h
  cases h with
  | intro x hpq =>
    cases hpq with
    | intro hp hq =>
      exists x

这些策略同样适用于数据和命题。在下一个示例中，它们被用来定义函数，用于交换乘积类型和求和类型的组成部分：

def swap_pair : α × β → β × α := by
  intro p
  cases p
  constructor <;> assumption

def swap_sum : Sum α β → Sum β α := by
  intro p
  cases p
  . apply Sum.inr; assumption
  . apply Sum.inl; assumption

请注意，我们选择的变量名称之前，这些定义与对于合取和析取的相应命题的证明完全相同。cases策略也可以对自然数进行情况分析：

open Nat
example (P : Nat → Prop) (h₀ : P 0) (h₁ : ∀ n, P (succ n)) (m : Nat) : P m := by
  cases m with
  | zero    => exact h₀
  | succ m' => exact h₁ m'

在归纳类型的策略一节中详细讨论了cases策略和它的伙伴induction策略。

contradiction策略在当前目标的假设中搜索矛盾。

example (p q : Prop) : p ∧ ¬ p → q := by
  intro h
  cases h
  contradiction

你还可以在策略块中使用 match。

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro h
    match h with
    | ⟨_, Or.inl _⟩ => apply Or.inl; constructor <;> assumption
    | ⟨_, Or.inr _⟩ => apply Or.inr; constructor <;> assumption
  . intro h
    match h with
    | Or.inl ⟨hp, hq⟩ => constructor; exact hp; apply Or.inl; exact hq
    | Or.inr ⟨hp, hr⟩ => constructor; exact hp; apply Or.inr; exact hr

你可以将 intro h 与 match h ... 结合起来，将之前的例子写成以下形式：

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro
    | ⟨hp, Or.inl hq⟩ => apply Or.inl; constructor <;> assumption
    | ⟨hp, Or.inr hr⟩ => apply Or.inr; constructor <;> assumption
  . intro
    | Or.inl ⟨hp, hq⟩ => constructor; assumption; apply Or.inl; assumption
    | Or.inr ⟨hp, hr⟩ => constructor; assumption; apply Or.inr; assumption

构造策略证明

策略通常提供了一种有效的建立证明的方法，但是长串的指令可能会掩盖论证的结构。在本节中，我们描述一些方法，帮助为策略样式的证明提供结构，使得这样的证明更易读和稳定。

Lean的证明写作语法的一个好处是可以混合使用术语样式和策略样式的证明，并且可以自由地在两者之间切换。例如，策略apply和exact都需要任意术语，你可以使用have、show等方式来编写这些术语。相反，当编写一个任意的Lean术语时，你总是可以通过插入一个by块来调用策略模式。下面是一个有点玩具化的例子：

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
  intro h
  exact
    have hp : p := h.left
    have hqr : q ∨ r := h.right
    show (p ∧ q) ∨ (p ∧ r) by
      cases hqr with
      | inl hq => exact Or.inl ⟨hp, hq⟩
      | inr hr => exact Or.inr ⟨hp, hr⟩

以下是一个更自然的例子：

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro h
    cases h.right with
    | inl hq => exact Or.inl ⟨h.left, hq⟩
    | inr hr => exact Or.inr ⟨h.left, hr⟩
  . intro h
    cases h with
    | inl hpq => exact ⟨hpq.left, Or.inl hpq.right⟩
    | inr hpr => exact ⟨hpr.left, Or.inr hpr.right⟩

实际上，Coq 中有一种名为show的策略，类似于证明项中的show表达式。它在策略模式下，用于声明即将解决的目标的类型。

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro h
    cases h.right with
    | inl hq =>
      show (p ∧ q) ∨ (p ∧ r)
      exact Or.inl ⟨h.left, hq⟩
    | inr hr =>
      show (p ∧ q) ∨ (p ∧ r)
      exact Or.inr ⟨h.left, hr⟩
  . intro h
    cases h with
    | inl hpq =>
      show p ∧ (q ∨ r)
      exact ⟨hpq.left, Or.inl hpq.right⟩
    | inr hpr =>
      show p ∧ (q ∨ r)
      exact ⟨hpr.left, Or.inr hpr.right⟩

show策略可以用于将一个目标重写为在定义上等价的形式：

theorem show_tactic : ∀ (P : Prop), P → P :=
begin
  intro P,
  show P, -- 使用 show 策略
  exact id, -- 使用 id 函数将目标转化为定义上等价的形式
end

该例子证明了对于任意命题 P，如果已知 P 成立，那么 P 也成立。在证明的过程中，我们使用了 show 策略，将目标 P 重写为定义上等价的形式。通过使用 exact id 策略，我们将目标转化为一个恒等函数 id，从而完成了证明。

example (n : Nat) : n + 1 = Nat.succ n := by
  show Nat.succ n = Nat.succ n
  rfl

还有一种“have”策略，它引入一个新的子目标，就像写证明项时一样：

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
  intro ⟨hp, hqr⟩
  show (p ∧ q) ∨ (p ∧ r)
  cases hqr with
  | inl hq =>
    have hpq : p ∧ q := And.intro hp hq
    apply Or.inl
    exact hpq
  | inr hr =>
    have hpr : p ∧ r := And.intro hp hr
    apply Or.inr
    exact hpr

和证明项一样，你可以在 have 策略中省略标签，这种情况下默认的标签 this 会被使用：

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
  intro ⟨hp, hqr⟩
  show (p ∧ q) ∨ (p ∧ r)
  cases hqr with
  | inl hq =>
    have : p ∧ q := And.intro hp hq
    apply Or.inl
    exact this
  | inr hr =>
    have : p ∧ r := And.intro hp hr
    apply Or.inr
    exact this

在策略have中可以省略类型声明，因此可以写成have hp := h.left和have hqr := h.right。实际上，使用这个记号，甚至可以同时省略类型和标签，这种情况下，新的事实会被引入并以标签this命名。

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
  intro ⟨hp, hqr⟩
  cases hqr with
  | inl hq =>
    have := And.intro hp hq
    apply Or.inl; exact this
  | inr hr =>
    have := And.intro hp hr
    apply Or.inr; exact this

Lean 还提供了一个 let 策略，类似于 have 策略，但是用于引入局部定义而不是辅助事实。它是证明项中的 let 的策略模拟。

example : ∃ x, x + 2 = 8 := by
  let a : Nat := 3 * 2
  exists a

与 have 类似，你可以通过写成 let a := 3 * 2 的形式来省略类型的定义。let 和 have 的不同之处在于，let 在上下文中引入了一个局部定义，因此局部声明的定义可以在证明中展开。

我们使用.来创建嵌套的策略块。在嵌套块中，Lean 关注第一个目标，并在块结束时生成错误，如果此目标未被完全解决。这对于指示由策略引入的多个子目标的单独证明是有帮助的。. 的符号对空白字符敏感，并依赖缩进来检测策略块的结束。或者，你可以使用花括号和分号来定义策略块。

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  { intro h;
    cases h.right;
    { show (p ∧ q) ∨ (p ∧ r);
      exact Or.inl ⟨h.left, ‹q›⟩ }
    { show (p ∧ q) ∨ (p ∧ r);
      exact Or.inr ⟨h.left, ‹r›⟩ } }
  { intro h;
    cases h;
    { show p ∧ (q ∨ r);
      rename_i hpq;
      exact ⟨hpq.left, Or.inl hpq.right⟩ }
    { show p ∧ (q ∨ r);
      rename_i hpr;
      exact ⟨hpr.left, Or.inr hpr.right⟩ } }

使用缩进来结构化证明是很有用的：每当一个策略产生超过一个子目标时，我们会用块来将剩余的子目标分隔开，并进行缩进。因此，如果将定理 foo 应用于一个目标产生了四个子目标，那么我们期望证明的样子是这样的：

  apply foo
  . <proof of first goal>
  . <proof of second goal>
  . <proof of third goal>
  . <proof of final goal>

好的，下面是关于 LEAN 定理证明的文章的中文翻译：

LEAN 定理证明

引言

在数学和逻辑学中，定理证明是一种通过逻辑推理来证明数学命题的过程。而 LEAN 是一个支持形式化证明的交互式定理证明系统。在本文中，我们将介绍如何在 LEAN 中使用构造性数学来证明定理。

LEAN 简介

LEAN 是一种基于依赖类型理论的交互式定理证明系统。它的设计目标是支持数学家和计算机科学家进行形式化证明，并提供严谨的证明检查机制。

构造性数学

构造性数学是一种数学分支，它要求每个数学命题的证明都必须能够提供一个具体的构造过程。与传统数学不同，构造性数学注重于证明的可执行性。

LEAN 中的构造性证明

在 LEAN 中，我们可以使用构造性数学的方法来证明定理。首先，我们需要定义一些基本的概念和符号，然后利用这些定义来构造一个具体的证明过程。

定理证明的过程

在 LEAN 中，定理证明的过程通常分为以下几个步骤：

1. 定义概念和符号；
2. 陈述待证明的定理；
3. 给出证明的主要思路和策略；
4. 逐步展开证明过程，使用合适的规则和定理；
5. 最后，通过 LEAN 的证明检查机制来验证证明的正确性。

LEAN 中的规则和定理

LEAN 中有许多已知的数学定理和规则，可以在证明中使用。这些定理和规则是经过验证和严格审查的，可以确保证明的正确性。

示例

下面是一个简单的 LEAN 定理证明的示例：

定理：对于任意两个整数 a 和 b，存在一个整数 c，使得 a + b = c。

证明：我们可以使用引理 “整数的加法是满射” 来证明这个定理。根据这个引理，在整数集上的加法运算是满射的，即对于任意一个整数 c，总存在两个整数 a 和 b，使得 a + b = c。因此，我们可以得出结论，对于任意两个整数 a 和 b，存在一个整数 c，使得 a + b = c。

结论

LEAN 是一个强大的定理证明系统，可以帮助数学家和计算机科学家形式化地证明定理。通过使用构造性数学的方法，在 LEAN 中进行定理证明可以提高证明的可执行性和严谨性。

希望本文对您理解 LEAN 定理证明有所帮助！

  apply foo
  case <tag of first goal>  => <proof of first goal>
  case <tag of second goal> => <proof of second goal>
  case <tag of third goal>  => <proof of third goal>
  case <tag of final goal>  => <proof of final goal>

LEAN 定理证明

引言

Lean 是一款交互式证明助手和通用编程语言。它的设计目标是支持高效的定理证明和正确的程序开发。Lean 使用了基于类型论的直观、可理解的逻辑体系，并提供了一套表达式语言和工具来进行定理证明。

在 Lean 中，定理证明是通过构造一个证明对象来完成的。证明对象是一个具有严密结构的表达式，可以描述证明中的逻辑推导过程。Lean 的类型检查器可以验证证明对象的正确性，并确保其与推导过程完全一致。

下面我们将使用 Lean 来证明一个简单的定理。

定理及证明

定理：对于任意自然数 n，存在自然数 m，使得 n < m。

证明：我们使用归纳法来证明这个定理。

• 基础情况：令 n = 0，我们可以选择 m = 1。此时显然有 0 < 1 成立。
• 归纳步骤：假设对于某个自然数 k，存在自然数 m，使得 k < m 成立。我们要证明对于 k + 1，也存在一个自然数 m'，使得 k + 1 < m' 成立。

根据归纳假设，存在一个自然数 m，使得 k < m 成立。我们可以令 m' = m + 1，那么有：

k + 1 < m + 1

根据自然数的性质，我们知道 m + 1 也是一个自然数。因此，对于任意自然数 k，都可以找到一个自然数 m'，使得 k + 1 < m' 成立。

综上所述，我们完成了对于任意自然数 n，存在自然数 m，使得 n < m 的证明。

结论

Lean 是一款强大的定理证明助手，可以帮助人们进行形式化证明。通过使用 Lean，我们可以确保证明的正确性和一致性，并充分发挥计算机的计算能力来辅助证明过程。Lean 的设计使得定理证明更加直观和可理解，同时也提供了丰富的工具和库来支持证明的开发和共享。

  apply foo
  { <proof of first goal>  }
  { <proof of second goal> }
  { <proof of third goal>  }
  { <proof of final goal>  }

策略组合子是从旧策略中生成新策略的操作。在“by”块中已经隐式包含了一个顺序组合子：

example (p q : Prop) (hp : p) : p ∨ q :=
  by apply Or.inl; assumption

这里，apply Or.inl; assumption 的功能上等同于一个单一的策略，它首先应用 apply Or.inl，然后应用 assumption。

在 t₁ <;> t₂ 中，<;> 运算符提供了一个并行版本的序列化操作：t₁ 应用于当前目标，然后 t₂ 应用于所有生成的子目标：

example (p q : Prop) (hp : p) (hq : q) : p ∧ q :=
  by constructor <;> assumption

这在目标的结果可以以统一的方式完成或者至少在所有目标上可以统一取得进展时特别有用。

first | t₁ | t₂ | ... | tₙ 依次应用每个 tᵢ，直到其中一个成功或全部失败为止：

example (p q : Prop) (hp : p) : p ∨ q := by
  first | apply Or.inl; assumption | apply Or.inr; assumption

example (p q : Prop) (hq : q) : p ∨ q := by
  first | apply Or.inl; assumption | apply Or.inr; assumption

在第一个例子中，左分支成功，而在第二个例子中，右分支成功。 在接下来的三个例子中，相同的复合策略在每种情况下都成功。

example (p q r : Prop) (hp : p) : p ∨ q ∨ r :=
  by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)

example (p q r : Prop) (hq : q) : p ∨ q ∨ r :=
  by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)

example (p q r : Prop) (hr : r) : p ∨ q ∨ r :=
  by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)

该策略试图立即通过假设来解决左边的析取；如果失败，则尝试专注于右边的析取；如果这也行不通，则调用假设策略。

到目前为止，你肯定已经注意到策略可能会失败。事实上，正是“失败”状态导致第一个组合子回溯并尝试下一个策略。try组合子构建了一种总是成功的策略，尽管可能是以一种微不足道的方式：try t执行t并报告成功，即使t失败。它等同于first | t | skip，其中skip是一个什么都不做的策略（但成功地这么做）。在下一个示例中，第二个constructor在右边的合取q ∧ r上成功（请记住，析取和合取与右结合），但在第一个上失败。try策略确保了顺序组合成功。

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by
  constructor <;> (try constructor) <;> assumption

小心：repeat (try t) 将会无限循环，因为内部 tactic 永远不会失败。

在证明中，通常会有多个目标待证明。并行序列是一种可以将单个 tactic 应用于多个目标的方式，但也有其他的方式可以实现这一点。例如，all_goals t 将会将t 应用于所有待证明的目标：

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by
  constructor
  all_goals (try constructor)
  all_goals assumption

在这种情况下，any_goals策略提供了一种更强大的解决方案。它类似于all_goals，但是只要其参数在至少一个目标上成功，它就会成功。

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by
  constructor
  any_goals constructor
  any_goals assumption

by 块下面的第一个策略是重复地分割连词：

example (p q r : Prop) (hp : p) (hq : q) (hr : r) :
      p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat (any_goals constructor)
  all_goals assumption

实际上，我们可以将完整的策略压缩为一行代码：

example (p q r : Prop) (hp : p) (hq : q) (hr : r) :
      p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat (any_goals (first | constructor | assumption))

组合子 focus t 确保 t 只影响当前的目标，暂时隐藏其他目标。因此，如果 t 通常只影响当前目标，那么 focus (all_goals t) 的效果与 t 相同。

重写

rewrite 策略（简写为 rw）和 simp 策略在 Calculational Proofs 中简要介绍过。在本节和下一节中，我们将更详细地讨论它们。

rewrite 策略提供了一种基本的机制，用于对目标和假设应用替换，方便且高效地处理等式。这个策略的最基本形式是 rewrite [t]，其中 t 是一个类型为等式的项。例如，t 可以是上下文中的一个假设 h : x = y，也可以是一个通用的引理，如 add_comm : ∀ x y, x + y = y + x，在这种情况下，rewrite 策略尝试找到适当的 x 和 y 的实例化；或者它可以是任何断言具体或通用等式的复合项。在下面的示例中，我们使用这种基本形式，使用一个假设来重写目标。

example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
  rw [h₂] -- replace k with 0
  rw [h₁] -- replace f 0 with 0

在上面的例子中，第一次使用 rw 将目标 f k = 0 中的 k 替换为 0。然后，第二次使用将 f 0 替换为 0。该策略会自动关闭形如 t = t 的目标。下面是使用复合表达式进行重写的一个例子：

example (x y : Nat) (p : Nat → Prop) (q : Prop) (h : q → x = y)
        (h' : p y) (hq : q) : p x := by
  rw [h hq]; assumption

在这里，h hq 建立了方程 x = y。

多个重写可以使用表示法rw [t_1, ..., t_n]进行组合， 这只是 rw [t_1]; ...; rw [t_n] 的简写。前面的例子可以写成以下形式：

example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
  rw [h₂, h₁]

默认情况下，rw在前向推导中使用等式，将左手边与一个表达式匹配，并用右手边替换它。符号←t可以用来指示该策略在逆向推导中使用等式t。

example (f : Nat → Nat) (a b : Nat) (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := by
  rw [←h₁, h₂]

在这个例子中，术语 ←h₁ 指示重写器将 b 替换为 a。在编辑器中，您可以输入向后箭头 \l。您还可以使用 ascii 等价物 <-。

有时，恒等式的左侧能够与模式中的多个子项匹配，此时 rw 策略会在遍历表达式时选择第一个匹配项。如果这不是您想要的那个，请使用额外的参数来指定适当的子项。

example (a b c : Nat) : a + b + c = a + c + b := by
  rw [Nat.add_assoc, Nat.add_comm b, ← Nat.add_assoc]

example (a b c : Nat) : a + b + c = a + c + b := by
  rw [Nat.add_assoc, Nat.add_assoc, Nat.add_comm b]

example (a b c : Nat) : a + b + c = a + c + b := by
  rw [Nat.add_assoc, Nat.add_assoc, Nat.add_comm _ b]

在上面的第一个例子中，第一步将 a + b + c 重写为 a + (b + c)。接下来的步骤将交换律应用于项 b + c；如果不指定参数，该策略会将 a + (b + c) 重写为 (b + c) + a。最后一步将逆向应用结合律，将 a + (c + b) 重写为 a + c + b。接下来的两个例子将结合律应用于双方，将括号移至右边，然后交换b和c。请注意，最后一个例子通过指定 Nat.add_comm 的第二个参数来指定重写应该在右侧进行。

默认情况下，rewrite 策略只会影响目标。rw [t] at h 的符号将重写t 应用于假设h。

example (f : Nat → Nat) (a : Nat) (h : a + 0 = 0) : f a = f 0 := by
  rw [Nat.add_zero] at h
  rw [h]

第一步，rw [Nat.add_zero] at h，将假设 a + 0 = 0 重写为 a = 0。 然后，使用新的假设 a = 0 将目标重写为 f 0 = f 0。

rewrite 策略不仅限于命题。 在下面的例子中，我们使用 rw [h] at t 将假设 t : Tuple α n 重写为 t : Tuple α 0。

def Tuple (α : Type) (n : Nat) :=
  { as : List α // as.length = n }

example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := by
  rw [h] at t
  exact t

使用化简器

而 rewrite 被设计为一个操作目标的手术工具，化简器则提供了一种更强大的自动化形式。Lean 库中的许多恒等式都被标记为 [simp] 属性，而 simp 策略则使用它们来迭代地重写表达式中的子项。

example (x y z : Nat) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by
  simp

example (x y z : Nat) (p : Nat → Prop) (h : p (x * y))
        : p ((x + 0) * (0 + y * 1 + z * 0)) := by
  simp; assumption

在第一个例子中，目标中的等式左边被简化为使用涉及0和1的常见等式，将目标减少为x * y = x * y。此时，simp应用了自反性来完成它。在第二个例子中，simp将目标减少为p (x * y)，此时假设h完成它。以下是一些关于列表的额外例子：

open List

example (xs : List Nat)
        : reverse (xs ++ [1, 2, 3]) = [3, 2, 1] ++ reverse xs := by
  simp

example (xs ys : List α)
        : length (reverse (xs ++ ys)) = length xs + length ys := by
  simp [Nat.add_comm]

与rw一样，您可以使用关键字at来简化一个假设：

example (x y z : Nat) (p : Nat → Prop)
        (h : p ((x + 0) * (0 + y * 1 + z * 0))) : p (x * y) := by
  simp at h; assumption

此外，您可以使用“通配符”星号来简化所有的假设和目标证明：

attribute [local simp] Nat.mul_comm Nat.mul_assoc Nat.mul_left_comm
attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm

example (w x y z : Nat) (p : Nat → Prop)
        (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
  simp at *; assumption

example (x y z : Nat) (p : Nat → Prop)
        (h₁ : p (1 * x + y)) (h₂ : p (x * z * 1))
        : p (y + 0 + x) ∧ p (z * x) := by
  simp at * <;> constructor <;> assumption

对于交换律和结合律可适用的操作，比如自然数的乘法，简化器使用这两个定理来重写表达式，以及左交换律。对于乘法操作来说，左交换律可以表示为：x * (y * z) = y * (x * z)。local修饰符告诉简化器在当前文件（或部分或命名空间）中使用这些规则。看起来交换律和左交换律可能会引发循环的问题。但是简化器可以检测到那些可以使它们的参数互换的恒等式，并使用一种被称为有序重写的技术。这意味着系统会维护一个内部的项排序，并且仅在应用恒等式后顺序会减少的情况下才使用它。对于上述提到的三个恒等式，这会使得表达式中所有的括号都与其右侧相关，并且表达式以一种规范（尽管有些主观）的方式进行排序。因此，关于结合性和交换性等价的两个表达式将被重写成相同的规范形式。

# attribute [local simp] Nat.mul_comm Nat.mul_assoc Nat.mul_left_comm
# attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm
example (w x y z : Nat) (p : Nat → Prop)
        : x * y + z * w * x = x * w * z + y * x := by
  simp

example (w x y z : Nat) (p : Nat → Prop)
        (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
  simp; simp at h; assumption

与 rewrite 类似，您可以向 simp 发送一个包含一般引理、局部假设、待展开的定义和复合表达式的事实列表。simp 策略还识别 ←t 语法，就像 rewrite 一样。无论哪种情况，附加规则被添加到用于简化术语的标识集合中。

def f (m n : Nat) : Nat :=
  m + n + m

example {m n : Nat} (h : n = 1) (h' : 0 = m) : (f m n) = n := by
  simp [h, ←h', f]

常见的一种方法是使用局部假设来简化目标：

example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
  simp [h₁, h₂]

当简化时使用在本地环境中出现的所有假设，我们可以使用通配符符号 * ：

example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
  simp [*]

下面是另一个例子：

example (u w x y z : Nat) (h₁ : x = y + z) (h₂ : w = u + x)
        : w = z + y + u := by
  simp [*, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]

简化器还会进行命题重写。例如，使用前提p，它将p ∧ q重写为q，将p ∨ q重写为true，然后通过简单证明来证明这些重写。重复这样的重写可以产生非平凡的命题推理。

example (p q : Prop) (hp : p) : p ∧ q ↔ q := by
  simp [*]

example (p q : Prop) (hp : p) : p ∨ q := by
  simp [*]

example (p q r : Prop) (hp : p) (hq : q) : p ∧ (q ∨ r) := by
  simp [*]

下面的示例会简化所有的假设，然后使用它们来证明目标。

example (u w x x' y y' z : Nat) (p : Nat → Prop)
        (h₁ : x + 0 = x') (h₂ : y + 0 = y')
        : x + y + 0 = x' + y' := by
  simp at *
  simp [*]

一件使得简化器特别有用的事情是它的功能可以随着库的发展而增长。举个例子，假设我们定义了一个列表操作，它通过将其输入的反向追加到结果中来将其对称化：

def symmetrize {α : Type} : list α → list α
| [] := []
| (h::t) := (h::t) ++ (symmetrize t)

This operation can be used to define the symmetric closure of a relation:

这个操作可以用来定义一个关系的对称闭包：

def symmetric_closure {α : Type} (r : α → α → Prop) : α → α → Prop :=
λ a b, symmetrize [(a, b)] ⊆ r

The definition of symmetric_closure makes use of the symmetrize operation to add all pairs of elements that are already related by r, as well as all pairs related by r in reverse order.

symmetric_closure 的定义使用了 symmetrize 操作，它通过添加所有在 r 中已经相关的元素对，以及所有按相反顺序相关的元素对，来生成对称闭包。

In Lean, we can prove that symmetric_closure is indeed the smallest relation that is contained in r and is symmetric:

在 Lean 中，我们可以证明 symmetric_closure 确实是包含在 r 中且对称的最小关系：

lemma symmetric_closure_is_smallest {α : Type} (r : α → α → Prop)
(sr : symmetric_closure r ≤ r)
(h : symmetric r)
: symmetric_closure r ≤ r :=
begin
  intros a b hab,
  cases hab with hb hr,
  { exact sr hb },
  { have hba : (b, a) ∈ symmetric_closure r,
    { rw symmetrize_append,
      apply mem_union_right,
      exact hr },
    exact sr hba }
end

The proof starts by assuming that symmetric_closure r is already a subset of r. Then, for any pair of elements a and b that are in symmetric_closure r, we need to show that a and b are related by r. We consider two cases:

证明首先假设 symmetric_closure r 已经是 r 的子集。然后，对于任意在 symmetric_closure r 中的元素对 a 和 b，我们需要证明 a 和 b 是由 r 相关的。我们分两种情况讨论：

• If a and b are already related by r, then we can directly conclude that a and b are related by r.

如果 a 和 b 已经由 r 相关，则我们可以直接得出 a 和 b 是由 r 相关的。

• If a and b are not related by r, then we need to show that (b, a) is in symmetric_closure r. This can be done by applying the symmetrize operation to the pair (a, b) and using the fact that r is symmetric.

如果 a 和 b 没有被 r 相关，则我们需要证明 (b, a) 在 symmetric_closure r 中。这可以通过对元素对 (a, b) 应用 symmetrize 操作，并利用 r 是对称的事实来完成。

def mk_symm (xs : List α) :=
  xs ++ xs.reverse

对于任意列表 xs，reverse (mk_symm xs) 等于 mk_symm xs，可以通过展开定义很容易证明：

lemma reverse_mk_symm {α : Type*} (xs : list α) :
  reverse (mk_symm xs) = mk_symm xs :=
begin
  -- 使用反转的定义展开目标
  unfold reverse,
  -- 我们需要对被反转的列表进行归纳
  induction xs with x xs ih,
  -- Base case: 空列表
  { refl },
  -- Inductive case: xs = x :: xs
  -- 我们需要简化（simplification）来处理理论项
  { simp only [mk_symm_cons, reverse_append, ih],
    -- 在获得感兴趣的等式之前简化，这里是反转一个列表的等式
    rw [reverse_singleton, append_nil] }
end

因此，我们通过对定义进行展开和归纳来证明这个结论。

# def mk_symm (xs : List α) :=
#  xs ++ xs.reverse
theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
  simp [mk_symm]

我们现在可以使用该定理来证明新的结果：

# def mk_symm (xs : List α) :=
#  xs ++ xs.reverse
# theorem reverse_mk_symm (xs : List α)
#        : (mk_symm xs).reverse = mk_symm xs := by
#  simp [mk_symm]
example (xs ys : List Nat)
        : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
  simp [reverse_mk_symm]

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p (mk_symm ys ++ xs.reverse) := by
  simp [reverse_mk_symm] at h; assumption

但通常情况下，使用 reverse_mk_symm 是正确的做法，如果用户不必显式地调用它会很方便。你可以通过在定义定理时将其标记为简化规则来实现这一点：

# def mk_symm (xs : List α) :=
#  xs ++ xs.reverse
@[simp] theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
  simp [mk_symm]

example (xs ys : List Nat)
        : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
  simp

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p (mk_symm ys ++ xs.reverse) := by
  simp at h; assumption

符号@[simp]声明reverse_mk_symm具有[simp]属性，并可以更明确地拼写出来：

# def mk_symm (xs : List α) :=
#  xs ++ xs.reverse
theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
  simp [mk_symm]

attribute [simp] reverse_mk_symm

example (xs ys : List Nat)
        : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
  simp

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p (mk_symm ys ++ xs.reverse) := by
  simp at h; assumption

定理的属性可以在定理声明之后的任何时间应用：

# def mk_symm (xs : List α) :=
#  xs ++ xs.reverse
theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
  simp [mk_symm]

example (xs ys : List Nat)
        : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
  simp [reverse_mk_symm]

attribute [simp] reverse_mk_symm

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p (mk_symm ys ++ xs.reverse) := by
  simp at h; assumption

然而，一旦属性被应用，就没有办法永久地移除它；它会在引入该属性所在文件的任何文件中保持存在。正如我们将在属性一节中进一步讨论的那样，可以使用local修饰符将属性的作用域限定为当前文件或部分。

# def mk_symm (xs : List α) :=
#  xs ++ xs.reverse
theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
  simp [mk_symm]

section
attribute [local simp] reverse_mk_symm

example (xs ys : List Nat)
        : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
  simp

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p (mk_symm ys ++ xs.reverse) := by
  simp at h; assumption
end

在该部分之外，简化器将不再默认使用 reverse_mk_sym。

请注意，我们讨论的各种 simp 选项 -- 给出一个明确的规则列表，使用 at 来指定位置 -- 可以结合使用，但它们列出的顺序是固定的。在编辑器中，您可以通过将光标置于 simp 标识符上以查看与之关联的文档字符串来查看正确的顺序。

还有两个有用的修饰符。默认情况下，simp 包含了所有使用 [simp] 属性标记过的定理。使用 simp only 可以排除这些默认规则，允许您使用更明确的规则列表。在下面的示例中，减号和 only 被用来阻止应用 reverse_mk_sym。

def mk_symm (xs : List α) :=
  xs ++ xs.reverse
@[simp] theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
  simp [mk_symm]

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p (mk_symm ys ++ xs.reverse) := by
  simp at h; assumption

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p ((mk_symm ys).reverse ++ xs.reverse) := by
  simp [-reverse_mk_symm] at h; assumption

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p ((mk_symm ys).reverse ++ xs.reverse) := by
  simp only [List.reverse_append] at h; assumption

simp策略有许多配置选项。例如，我们可以通过以下方式启用上下文简化。

example : if x = 0 then y + x = y else x ≠ 0 := by
  simp (config := { contextual := true })

当 contextual := true 时，当简化 y + x = y 时，simp 使用了 x = 0 这一事实，而在简化另一分支时使用了 x ≠ 0。这里是另一个例子。

import data.complex.basic

theorem complex.mul_zero (a : ℂ) : a * 0 = 0 :=
begin
  simp,
end

这个定理表明对于任意复数 a，a * 0 等于 0。在证明过程中，我们使用了 simp 策略，并设置 contextual := true。这样一来，在简化 a * 0 的过程中，simp 会使用 0 = 0 * 0 这一事实，从而将 a * 0 简化为 0。

example : ∀ (x : Nat) (h : x = 0), y + x = y := by
  simp (config := { contextual := true })

另一个有用的配置选项是 arith := true，它可以启用算术化简。它非常有用，以至于 simp_arith 是 simp (config := { arith := true }) 的缩写。

example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by
  simp_arith

分割策略

split 策略适用于拆分嵌套的 if-then-else 和 match 表达式。对于一个具有 n 个 case 的 match 表达式，split 策略最多生成 n 个子目标。下面是一个例子。

def f (x y z : Nat) : Nat :=
  match x, y, z with
  | 5, _, _ => y
  | _, 5, _ => y
  | _, _, 5 => y
  | _, _, _ => 1

example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := by
  intros
  simp [f]
  split
  . contradiction
  . contradiction
  . contradiction
  . rfl

我们可以将上述证明的策略压缩如下。

Proof.
  intros H.
  induction H as [x Hx|y Hy Hz].
  - apply Hx.
  - apply Hy.
Defined.

Proof.(证明) intros H. induction H as [x Hx|y Hy Hz].

• apply Hx.
• apply Hy. Defined.

# def f (x y z : Nat) : Nat :=
#  match x, y, z with
#  | 5, _, _ => y
#  | _, 5, _ => y
#  | _, _, 5 => y
#  | _, _, _ => 1
example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := by
  intros; simp [f]; split <;> first | contradiction | rfl

策略 split <;> first | contradiction | rfl 首先应用 split 策略， 然后对于每个生成的子目标，尝试 contradiction，如果 contradiction 失败，则尝试 rfl。 和 simp 类似，我们可以将 split 应用于特定的假设。

def g (xs ys : List Nat) : Nat :=
  match xs, ys with
  | [a, b], _ => a+b+1
  | _, [b, c] => b+1
  | _, _      => 1

example (xs ys : List Nat) (h : g xs ys = 0) : False := by
  simp [g] at h; split at h <;> simp_arith at h

可扩展的策略

在下面的例子中，我们使用syntax命令来定义triv符号。然后，我们使用macro_rules命令来指定在使用triv时应该执行哪些操作。你可以提供不同的展开方式，策略解释器将尝试它们直到找到一个成功的。

-- Define a new tactic notation
syntax "triv" : tactic

macro_rules
  | `(tactic| triv) => `(tactic| assumption)

example (h : p) : p := by
  triv

-- You cannot prove the following theorem using `triv`
-- example (x : α) : x = x := by
--  triv

-- Let's extend `triv`. The tactic interpreter
-- tries all possible macro extensions for `triv` until one succeeds
macro_rules
  | `(tactic| triv) => `(tactic| rfl)

example (x : α) : x = x := by
  triv

example (x : α) (h : p) : x = x ∧ p := by
  apply And.intro <;> triv

-- We now add a (recursive) extension
macro_rules | `(tactic| triv) => `(tactic| apply And.intro <;> triv)

example (x : α) (h : p) : x = x ∧ p := by
  triv

习题

1. 回到 Chapter Propositions and Proofs 和 Chapter Quantifiers and Equality，尽量用策略证明重新做一遍已有的习题，使用适当的 rw 和 simp。

2. 使用策略组合器获得以下命题的一行证明：

example (p q r : Prop) (hp : p)
        : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := by
  admit

与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