3. 命题与证明3. Propositions and Proofs🔗
到目前为止，你已经看到了一些在 Lean 中定义对象和函数的方法。在本章中，我们将开始解释如何用依值类型论（dependent type theory）的语言来书写数学断言和证明。By now, you have seen some ways of defining objects and functions in
Lean. In this chapter, we will begin to explain how to write
mathematical assertions and proofs in the language of dependent type
theory as well.
3.1. 命题即类型（Propositions as Types）3.1. Propositions as Types🔗
在依值类型论语言中证明关于已定义对象的断言的一种策略，是在定义语言之上叠加一个断言语言和一个证明语言。但没有理由以这种方式增加语言的层次：依值类型论灵活且富有表现力，我们没有理由不能在同一个通用框架中表示断言和证明。One strategy for proving assertions about objects defined in the
language of dependent type theory is to layer an assertion language
and a proof language on top of the definition language. But there is
no reason to multiply languages in this way: dependent type theory is
flexible and expressive, and there is no reason we cannot represent
assertions and proofs in the same general framework.
例如，我们可以引入一个新类型 Prop（命题宇宙）来表示命题，并引入构造子来从其他命题构建新命题。For example, we could introduce a new type, Prop, to represent
propositions, and introduce constructors to build new propositions
from others.
然后，我们可以为每个 p : Prop 引入另一个类型 Proof p，作为 p 的证明类型。一个"公理（axiom）"就是这样一个类型的常量。We could then introduce, for each element p : Prop, another type
Proof p, for the type of proofs of p. An “axiom” would be a
constant of such a type.
然而，除了公理之外，我们还需要规则来从旧证明构建新证明。例如，在许多命题逻辑的证明系统中，我们有肯定前件（modus ponens）规则：In addition to axioms, however, we would also need rules to build new
proofs from old ones. For example, in many proof systems for
propositional logic, we have the rule of modus ponens:
从 Implies p q 的一个证明和 p 的一个证明，我们得到 q 的一个证明。From a proof of Implies p q and a proof of p, we obtain a proof of q.
我们可以如下表示：We could represent this as follows:
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
命题逻辑的自然 deduction（自然演绎）系统通常也依赖以下规则：Systems of natural deduction for propositional logic also typically rely on the following rule:
假设，在将 p 作为假设的前提下，我们有一个 q 的证明。那么我们可以"取消"这个假设，并得到 Implies p q 的一个证明。Suppose that, assuming p as a hypothesis, we have a proof of q. Then we can “cancel” the hypothesis and obtain a proof of Implies p q.
我们可以如下呈现：We could render this as follows:
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。This approach would provide us with a reasonable way of building assertions and proofs.
Determining that an expression t is a correct proof of assertion p would then
simply be a matter of checking that t has type Proof p.
然而，可以进行一些简化。首先，我们可以通过将 Proof p 与 p 本身合并来避免重复书写术语 Proof。换句话说，每当我们有 p : Prop 时，我们可以将 p 解释为一个类型，即其证明的类型。然后我们可以将 t : p 解读为断言 t 是 p 的一个证明。Some simplifications are possible, however. To start with, we can
avoid writing the term Proof repeatedly by conflating Proof p
with p itself. In other words, whenever we have p : Prop, we
can interpret p as a type, namely, the type of its proofs. We can
then read t : p as the assertion that t is a proof of p.
此外，一旦我们做出了这种等同，蕴含的规则表明我们可以在 Implies p q 和 p → q 之间来回转换。换句话说，命题 p 和 q 之间的蕴含对应于存在一个函数，它将 p 的任何元素映射到 q 的一个元素。结果，连接词 Implies 的引入完全是多余的：我们可以使用依值类型论中通常的函数空间构造子 p → q 作为我们的蕴含概念。Moreover, once we make this identification, the rules for implication
show that we can pass back and forth between Implies p q and
p → q. In other words, implication between propositions p and q
corresponds to having a function that takes any element of p to an
element of q. As a result, the introduction of the connective
Implies is entirely redundant: we can use the usual function space
constructor p → q from dependent type theory as our notion of
implication.
这就是构造演算（Calculus of Constructions）中所采用的方法，因此在 Lean 中也是如此。自然演绎证明系统中蕴含的规则恰好对应于支配函数抽象和应用的规则，这是 Curry-Howard 同构（Curry-Howard isomorphism）的一个实例，有时也被称为命题即类型（propositions-as-types）范式。实际上，类型 Prop 是 Sort 0 的语法糖，也就是上一章描述的类型层次结构的最底层。此外，Type u 也只是 Sort (u+1) 的语法糖。Prop 有一些特殊特性，但和其他类型宇宙一样，它在箭头构造子下封闭：如果我们有 p q : Prop，那么 p → q : Prop。This is the approach followed in the Calculus of Constructions, and
hence in Lean as well. The fact that the rules for implication in a
proof system for natural deduction correspond exactly to the rules
governing abstraction and application for functions is an instance of
the Curry-Howard isomorphism, sometimes known as the
propositions-as-types paradigm. In fact, the type Prop is
syntactic sugar for Sort 0, the very bottom of the type hierarchy
described in the last chapter. Moreover, Type u is also just
syntactic sugar for Sort (u+1). Prop has some special
features, but like the other type universes, it is closed under the
arrow constructor: if we have p q : Prop, then p → q : Prop.
至少有两种思考命题即类型的方式。对于某些持构造性逻辑和数学观点的人来说，这是对命题含义的忠实呈现：一个命题 p 代表一种数据类型，即构成证明的数据类型的规范。那么 p 的一个证明就是一个正确类型的对象 t : p。There are at least two ways of thinking about propositions as
types. To some who take a constructive view of logic and mathematics,
this is a faithful rendering of what it means to be a proposition: a
proposition p represents a sort of data type, namely, a
specification of the type of data that constitutes a proof. A proof of
p is then simply an object t : p of the right type.
不倾向于这种意识形态的人，则可以将其视为一种简单的编码技巧。对于每个命题 p，我们关联一个类型，如果 p 为假则该类型为空，如果 p 为真则该类型只有一个元素，比如 *。在后一种情况下，我们说（与 p 关联的）类型是可居的（inhabited）。恰好，函数应用和抽象的规则可以方便地帮助我们跟踪 Prop 中哪些元素是可居的。因此，构造一个元素 t : p 告诉我们 p 确实是真。你可以将 p 的居留者视为"p 为真的事实"。p → q 的一个证明利用"p 为真的事实"来得到"q 为真的事实"。Those not inclined to this ideology can view it, rather, as a simple
coding trick. To each proposition p we associate a type that is
empty if p is false and has a single element, say *, if p
is true. In the latter case, let us say that (the type associated
with) p is inhabited. It just so happens that the rules for
function application and abstraction can conveniently help us keep
track of which elements of Prop are inhabited. So constructing an
element t : p tells us that p is indeed true. You can think of
the inhabitant of p as being the “fact that p is true.” A
proof of p → q uses “the fact that p is true” to obtain “the
fact that q is true.”
实际上，如果 p : Prop 是任意命题，Lean 的内核将任意两个元素 t1 t2 : p 视为定义上相等，就像它将 (fun x => t) s 和 t[s/x] 视为定义上相等一样。这被称为证明不相关性（proof irrelevance），并且与上一段的解释一致。这意味着，尽管我们可以将证明 t : p 视为依值类型论语言中的普通对象，但它们除了 p 为真这一事实之外，不携带任何其他信息。Indeed, if p : Prop is any proposition, Lean's kernel treats any
two elements t1 t2 : p as being definitionally equal, much the
same way as it treats (fun x => t) s and t[s/x] as
definitionally equal. This is known as proof irrelevance, and is
consistent with the interpretation in the last paragraph. It means
that even though we can treat proofs t : p as ordinary objects in
the language of dependent type theory, they carry no information
beyond the fact that p is true.
我们建议的两种思考命题即类型（propositions-as-types）范式的方式存在根本性差异。从构造性观点来看，证明是由依值类型论中合适的表达式表示（denoted）的抽象数学对象。相比之下，如果我们按照上面描述的编码技巧来思考，那么这些表达式本身并不表示任何有趣的东西。相反，正是我们能够写出它们并检查它们是否良好类型化这一事实，确保了所讨论的命题为真。换句话说，这些表达式本身就是证明。The two ways we have suggested thinking about the
propositions-as-types paradigm differ in a fundamental way. From the
constructive point of view, proofs are abstract mathematical objects
that are denoted by suitable expressions in dependent type
theory. In contrast, if we think in terms of the coding trick
described above, then the expressions themselves do not denote
anything interesting. Rather, it is the fact that we can write them
down and check that they are well-typed that ensures that the
proposition in question is true. In other words, the expressions
themselves are the proofs.
在下面的叙述中，我们将在两种说法之间来回切换，有时说一个表达式"构造"、"产生"或"返回"一个命题的证明，有时则简单地说它"是"这样一个证明。这类似于计算机科学家有时模糊语法和语义之间的区别，有时说一个程序"计算"某个函数，有时则把这个程序说成"是"该函数本身。In the exposition below, we will slip back and forth between these two
ways of talking, at times saying that an expression “constructs” or
“produces” or “returns” a proof of a proposition, and at other times
simply saying that it “is” such a proof. This is similar to the way
that computer scientists occasionally blur the distinction between
syntax and semantics by saying, at times, that a program “computes” a
certain function, and at other times speaking as though the program
“is” the function in question.
无论如何，真正重要的只有最终结果。为了在依值类型论的语言中形式化地表达一个数学断言，我们需要展示一个项 p : Prop。为了证明那个断言，我们需要展示一个项 t : p。Lean 作为证明助手的任务，就是帮助我们构造这样的项 t，并验证它是否良好形式化且具有正确的类型。In any case, all that really matters is the bottom line. To formally
express a mathematical assertion in the language of dependent type
theory, we need to exhibit a term p : Prop. To prove that
assertion, we need to exhibit a term t : p. Lean's task, as a
proof assistant, is to help us to construct such a term, t, and to
verify that it is well-formed and has the correct type.
3.2. 以命题即类型的方式工作（Working with Propositions as Types）3.2. Working with Propositions as Types🔗
在命题即类型（propositions-as-types）范式中，仅涉及 → 的定理可以使用 λ 抽象（lambda abstraction）和应用来证明。在 Lean 中，theorem（定理）命令引入一个新定理：In the propositions-as-types paradigm, theorems involving only →
can be proved using lambda abstraction and application. In Lean, the
theorem command introduces a new theorem:
set_option linter.unusedVariables false
---
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 为真。Compare this proof to the expression fun x : α => fun y : β => x
of type α → β → α, where α and β are data types.
This describes the function that takes arguments x and y
of type α and β, respectively, and returns x.
The proof of t1 has the same form, the only difference being that
p and q are elements of Prop rather than Type.
Intuitively, our proof of
p → q → p assumes p and q are true, and uses the first
hypothesis (trivially) to establish that the conclusion, p, is
true.
注意，theorem（定理）命令实际上是 def（定义）命令的一个版本：根据命题与类型的对应关系，证明定理 p → q → p 实际上与定义关联类型的一个元素是同一回事。对于内核类型检查器来说，两者之间没有区别。Note that the theorem command is really a version of the
def command: under the propositions and types
correspondence, proving the theorem p → q → p is really the same
as defining an element of the associated type. To the kernel type
checker, there is no difference between the two.
然而，定义和定理之间存在一些实用上的差异。在正常情况下，永远不需要"展开"定理的"定义"；根据证明不相关性（proof irrelevance），该定理的任意两个证明都是定义上相等的。一旦定理的证明完成，通常我们只需要知道证明存在即可；证明具体是什么并不重要。鉴于这一事实，Lean 将证明标记为不可归约的（irreducible），这向解析器（更准确地说是精化器（elaborator））提示在处理文件时通常不需要展开它们。实际上，Lean 通常能够并行处理和检查证明，因为评估一个证明的正确性不需要知道另一个证明的细节。此外，在定义的主体中引用的段变量（section variables）会自动添加为参数，但只有定理类型中引用的变量才会被添加。这是因为证明一个语句的方式不应影响被证明的语句。There are a few pragmatic differences between definitions and
theorems, however. In normal circumstances, it is never necessary to
unfold the “definition” of a theorem; by proof irrelevance, any two
proofs of that theorem are definitionally equal. Once the proof of a
theorem is complete, typically we only need to know that the proof
exists; it doesn't matter what the proof is. In light of that fact,
Lean tags proofs as irreducible, which serves as a hint to the
parser (more precisely, the elaborator) that there is generally no
need to unfold them when processing a file. In fact, Lean is generally
able to process and check proofs in parallel, since assessing the
correctness of one proof does not require knowing the details of
another. Additionally, section variables
that are referred to in the body of a definition are automatically added as
parameters, but only the variables referred to in a theorem's type are added.
This is because the way in which a statement is proved should not influence
the statement that is being proved.
与定义一样，#print（打印）命令会显示定理的证明：As with definitions, the #print command will show you the proof of
a theorem:
theorem t1 : p → q → p := fun hp : p => fun hq : q => hp
theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp#print t1theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp
注意，λ 抽象 hp : p 和 hq : q 可以被视为在 t1 的证明中的临时假设。Lean 还允许我们使用 show（显示）语句明确指定最终项 hp 的类型：Notice that the lambda abstractions hp : p and hq : q can be
viewed as temporary assumptions in the proof of t1. Lean also
allows us to specify the type of the final term hp, explicitly,
with a show statement:
theorem t1 : p → q → p :=
fun hp : p =>
fun hq : q =>
show p from hp
添加这样的额外信息可以提高证明的清晰度，并有助于在编写证明时发现错误。show 命令除了注释类型之外不做任何事，并且在内部，我们所见过的所有 t1 的表示都产生相同的项。Adding such extra information can improve the clarity of a proof and
help detect errors when writing a proof. The show command does
nothing more than annotate the type, and, internally, all the
presentations of t1 that we have seen produce the same term.
与普通定义一样，我们可以将 λ 抽象的变量移到冒号的左边：As with ordinary definitions, we can move the lambda-abstracted
variables to the left of the colon:
theorem t1 (hp : p) (hq : q) : p := hp
theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp#print t1theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp
我们可以像函数应用一样使用定理 t1：We can use the theorem t1 just as a function application:
theorem t1 (hp : p) (hq : q) : p := hp
axiom hp : p
theorem t2 : q → p := t1 hp
axiom（公理）声明假定了给定类型的元素的存在，可能损害逻辑一致性。例如，我们可以用它来假定空类型 False 有一个元素：The axiom declaration postulates the existence of an
element of the given type and may compromise logical consistency. For
example, we can use it to postulate that the empty type False has an
element:
声明一个"公理" hp : p 相当于声明 p 为真，以 hp 为证。将定理 t1 : p → q → p 应用于事实 hp : p（即 p 为真）得到定理 t1 hp : q → p。Declaring an “axiom” hp : p is tantamount to declaring that p
is true, as witnessed by hp. Applying the theorem
t1 : p → q → p to the fact hp : p that p is true yields the theorem
t1 hp : q → p.
回顾一下，我们也可以如下编写定理 t1：Recall that we can also write theorem t1 as follows:
set_option linter.unusedVariables false
theorem t1 {p q : Prop} (hp : p) (hq : q) : p := hp
theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp#print t1theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp
t1 的类型现在是 ∀ {p q : Prop}, p → q → p。我们可以将其解读为断言"“对于每一对命题 p q，我们有 p → q → p”。例如，我们可以将所有参数移到冒号的右边：The type of t1 is now ∀ {p q : Prop}, p → q → p. We can read
this as the assertion “for every pair of propositions p q, we have
p → q → p.” For example, we can move all parameters to the right
of the colon:
set_option linter.unusedVariables false
theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q : Prop} (hp : p) (hq : q) => hp
如果 p 和 q 已经被声明为变量（variables），Lean 会自动为我们泛化它们：If p and q have been declared as variables, Lean will
generalize them for us automatically:
variable {p q : Prop}
theorem t1 : p → q → p := fun (hp : p) (unused variable `hq`
Note: This linter can be disabled with `set_option linter.unusedVariables false`hq : q) => hp
当我们这样泛化 t1 后，我们可以将其应用于不同的命题对，以获得一般定理的不同实例。When we generalize t1 in such a way, we can then apply it to
different pairs of propositions, to obtain different instances of the
general theorem.
set_option linter.unusedVariables false
theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp
variable (p q r s : Prop)
t1 p q : p → q → p#check t1 p qt1 p q : p → q → p
t1 r s : r → s → r#check t1 r st1 r s : r → s → r
t1 (r → s) (s → r) : (r → s) → (s → r) → r → s#check t1 (r → s) (s → r)t1 (r → s) (s → r) : (r → s) → (s → r) → r → s
variable (h : r → s)
t1 (r → s) (s → r) h : (s → r) → r → s#check t1 (r → s) (s → r) ht1 (r → s) (s → r) h : (s → r) → r → s
再次使用命题即类型（propositions-as-types）对应关系，类型为 h 的变量，其类型为 r → s，可以被视为假设或前提，即 r → s 成立。Once again, using the propositions-as-types correspondence, the
variable h of type r → s can be viewed as the hypothesis, or
premise, that r → s holds.
作为另一个例子，让我们考虑上一章讨论的组合函数，现在使用命题而不是类型。As another example, let us consider the composition function discussed
in the last chapter, now with propositions instead of types.
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 表达的是什么？As a theorem of propositional logic, what does t2 say?
注意，使用数字 Unicode 下标通常很有用，就像我们在本例中做的那样，通过输入 \0、\1、\2……来作为假设。Note that it is often useful to use numeric Unicode subscripts,
entered as \0, \1, \2, ..., for hypotheses, as we did in
this example.
3.3. 命题逻辑（Propositional Logic）3.3. Propositional Logic🔗
Lean 定义了所有标准逻辑连接词及其符号。命题连接词带有如下符号：Lean defines all the standard logical connectives and notation. The propositional connectives come with the following notation:
它们都取值于 Prop。They all take values in Prop.
运算优先级如下：一元否定 ¬ 绑定最强，然后是 ∧，然后是 ∨，然后是 →，最后是 ↔。例如，a ∧ b → c ∨ d ∧ e 意思是 (a ∧ b) → (c ∨ (d ∧ e))。请记住 → 是右结合的（现在参数是 Prop 的元素而不是其他 Type，这并没有改变），其他二元连接词也是如此。所以如果我们有 p q r : Prop，表达式 p → q → r 解读为"“如果 p，那么如果 q，则 r”。这正好是 p ∧ q → r 的"“柯里化”形式。The order of operations is as follows: unary negation ¬ binds most
strongly, then ∧, then ∨, then →, and finally ↔. For
example, a ∧ b → c ∨ d ∧ e means (a ∧ b) → (c ∨ (d ∧ e)).
Remember that → associates to the right (nothing changes
now that the arguments are elements of Prop, instead of some other
Type), as do the other binary connectives. So if we have
p q r : Prop, the expression p → q → r reads “if p, then if q,
then r.” This is just the “curried” form of p ∧ q → r.
在上一章中，我们观察到 λ 抽象可以被视为 → 的"“引入规则”。在当前设置中，它展示了如何"“引入”或确立一个蕴含。应用可以被视为"“消去规则”，展示了如何在证明中"“消去”或使用一个蕴含。其他命题连接词在 Lean 的库中定义，并自动导入。每个连接词都带有其规范的引入和消去规则。In the last chapter we observed that lambda abstraction can be viewed
as an “introduction rule” for →. In the current setting, it shows
how to “introduce” or establish an implication. Application can be
viewed as an “elimination rule,” showing how to “eliminate” or use an
implication in a proof. The other propositional connectives are
defined in Lean's library, and are automatically imported. Each connective
comes with its canonical introduction and elimination rules.
3.3.1. 合取（Conjunction）3.3.1. Conjunction🔗
表达式 And.intro h1 h2 使用证明 h1 : p 和 h2 : q 构建 p ∧ q 的一个证明。通常将 And.intro 描述为且引入（and-introduction）规则。在下一个例子中，我们使用 And.intro 来创建 p → q → p ∧ q 的一个证明。The expression And.intro h1 h2 builds a proof of p ∧ q using
proofs h1 : p and h2 : q. It is common to describe
And.intro as the and-introduction rule. In the next example we
use And.intro to create a proof of p → q → p ∧ q.
example（示例）命令声明一个定理而不命名它，也不将其存储在永久上下文中。本质上，它只检查给定的项是否具有指定的类型。它便于演示，我们将经常使用它。The example command states a theorem without naming it or storing
it in the permanent context. Essentially, it just checks that the
given term has the indicated type. It is convenient for illustration,
and we will use it often.
表达式 And.left h 从证明 h : p ∧ q 创建 p 的一个证明。类似地，And.right h 是 q 的一个证明。它们通常被称为左且消去和右且消去（and-elimination）规则。The expression And.left h creates a proof of p from a proof
h : p ∧ q. Similarly, And.right h is a proof of q. They
are commonly known as the left and right and-elimination rules.
我们现在可以用以下证明项来证明 p ∧ q → q ∧ p。We can now prove p ∧ q → q ∧ p with the following proof term.
注意，且引入和且消去类似于笛卡尔积的配对和投影操作。区别在于，给定 hp : p 和 hq : q，And.intro hp hq 的类型是 p ∧ q : Prop，而给定 a : α 和 b : β，Prod.mk a b 的类型是 α × β : Type。Prod 不能与 Prop 一起使用，而 And 不能与 Type 一起使用。∧ 和 × 之间的相似性是 Curry-Howard 同构的另一个实例，但与蕴含和函数空间构造子不同，∧ 和 × 在 Lean 中是分开处理的。然而，根据这个类比，我们刚刚构建的证明类似于交换一对元素的函数。Notice that and-introduction and and-elimination are similar to the
pairing and projection operations for the Cartesian product. The
difference is that given hp : p and hq : q, And.intro hp hq has type
p ∧ q : Prop, while given a : α and b : β, Prod.mk a b has type
α × β : Type. Prod cannot be used with Props, and And cannot be used with Types.
The similarity between ∧ and × is another instance
of the Curry-Howard isomorphism, but in contrast to implication and
the function space constructor, ∧ and × are treated separately
in Lean. With the analogy, however, the proof we have just constructed
is similar to a function that swaps the elements of a pair.
我们将在结构体与记录（Structures and Records）中看到，Lean 中的某些类型是结构体（structures），也就是说，该类型由一个单一的规范构造子（constructor）定义，该构造子从一系列合适的参数中构建类型的一个元素。对于每个 p q : Prop，p ∧ q 就是一个例子：构造元素的规范方式是向合适的参数 hp : p 和 hq : q 应用 And.intro。在这些情况下，当相关类型是归纳类型并且可以从上下文中推断出来时，Lean 允许我们使用匿名构造子（anonymous constructor）符号 ⟨arg1, arg2, ...⟩。特别是，我们经常可以写 ⟨hp, hq⟩ 而不是 And.intro hp hq：We will see in Structures and Records that certain
types in Lean are structures, which is to say, the type is defined
with a single canonical constructor which builds an element of the
type from a sequence of suitable arguments. For every p q : Prop,
p ∧ q is an example: the canonical way to construct an element is
to apply And.intro to suitable arguments hp : p and
hq : q. Lean allows us to use anonymous constructor notation
⟨arg1, arg2, ...⟩ in situations like these, when the relevant type is an
inductive type and can be inferred from the context. In particular, we
can often write ⟨hp, hq⟩ instead of And.intro hp hq:
这些尖括号分别通过输入 \< 和 \> 得到。These angle brackets are obtained by typing \< and \>, respectively.
Lean 提供了另一个有用的语法工具。给定一个归纳类型 Foo（可能应用于某些参数）的表达式 e，符号 e.bar 是 Foo.bar e 的简写。这提供了一种无需打开命名空间就能访问函数的便捷方式。例如，以下两个表达式意思相同：Lean provides another useful syntactic gadget. Given an expression
e of an inductive type Foo (possibly applied to some
arguments), the notation e.bar is shorthand for Foo.bar e.
This provides a convenient way of accessing functions without opening
a namespace. For example, the following two expressions mean the same
thing:
因此，给定 h : p ∧ q，我们可以写 h.left 来代替 And.left h，写 h.right 来代替 And.right h。因此，我们可以方便地将上面的示例证明重写如下：As a result, given h : p ∧ q, we can write h.left for
And.left h and h.right for And.right h. We can therefore
rewrite the sample proof above conveniently as follows:
简洁和晦涩之间只有一线之隔，以这种方式省略信息有时会使证明更难阅读。但对于像上面这样直接的构造，当 h 的类型和构造的目标都很明显时，这种符号既清晰又有效。There is a fine line between brevity and obfuscation, and omitting
information in this way can sometimes make a proof harder to read. But
for straightforward constructions like the one above, when the type of
h and the goal of the construction are salient, the notation is
clean and effective.
像"And"这样的构造经常被嵌套使用。Lean 也允许你展平右结合的嵌套构造子，因此这两个证明是等价的：It is common to iterate constructions like “And.” Lean also allows you
to flatten nested constructors that associate to the right, so that
these two proofs are equivalent:
这通常也很有用。This is often useful as well.
3.3.2. 析取（Disjunction）3.3.2. Disjunction🔗
表达式 Or.intro_left q hp 从证明 hp : p 创建 p ∨ q 的一个证明。类似地，Or.intro_right p hq 使用证明 hq : q 创建 p ∨ q 的一个证明。这些是左或引入和右或引入（or-introduction）规则。The expression Or.intro_left q hp creates a proof of p ∨ q
from a proof hp : p. Similarly, Or.intro_right p hq creates a
proof for p ∨ q using a proof hq : q. These are the left and
right or-introduction rules.
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）规则稍微复杂一些。其思想是，我们可以通过证明 r 在 p 下成立以及 r 在 q 下成立来从 p ∨ q 证明 r。换句话说，这是一种情况分析证明。在表达式 Or.elim hpq hpr hqr 中，Or.elim 接受三个参数：hpq : p ∨ q、hpr : p → r 和 hqr : q → r，并产生 r 的一个证明。在下面的例子中，我们使用 Or.elim 来证明 p ∨ q → q ∨ p。The or-elimination rule is slightly more complicated. The idea is
that we can prove r from p ∨ q, by showing that r follows
from p and that r follows from q. In other words, it is a
proof by cases. In the expression Or.elim hpq hpr hqr, Or.elim
takes three arguments, hpq : p ∨ q, hpr : p → r and
hqr : q → r, and produces a proof of r. In the following example, we use
Or.elim to prove 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)
在大多数情况下，Or.intro_right 和 Or.intro_left 的第一个参数可以由 Lean 自动推断。因此，Lean 提供了 Or.inr 和 Or.inl，它们可以视为 Or.intro_right _ 和 Or.intro_left _ 的简写。因此，上面的证明项可以更简洁地写成：In most cases, the first argument of Or.intro_right and
Or.intro_left can be inferred automatically by Lean. Lean
therefore provides Or.inr and Or.inl which can be viewed as
shorthand for Or.intro_right _ and Or.intro_left _. Thus the
proof term above could be written more concisely:
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 的类型。但在更长的版本中使用类型注释可以使证明更具可读性，并有助于捕获和调试错误。Notice that there is enough information in the full expression for
Lean to infer the types of hp and hq as well. But using the
type annotations in the longer version makes the proof more readable,
and can help catch and debug errors.
因为 Or 有两个构造子，我们不能使用匿名构造子符号。但我们仍然可以写 h.elim 来代替 Or.elim h：Because Or has two constructors, we cannot use anonymous
constructor notation. But we can still write h.elim instead of
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)
再次强调，你应该自行判断这样的缩写是增强了可读性还是降低了可读性。Once again, you should exercise judgment as to whether such
abbreviations enhance or diminish readability.
3.3.3. 否定与假（Negation and Falsity）3.3.3. Negation and Falsity🔗
否定 ¬p 实际上被定义为 p → False，因此我们通过从 p 推导出矛盾来得到 ¬p。类似地，表达式 hnp hp 从 hp : p 和 hnp : ¬p 产生 False 的一个证明。下一个例子使用这两条规则来产生 (p → q) → ¬q → ¬p 的一个证明。（符号 ¬ 通过输入 \not 或 \neg 得到。）Negation, ¬p, is actually defined to be p → False, so we
obtain ¬p by deriving a contradiction from p. Similarly, the
expression hnp hp produces a proof of False from hp : p
and hnp : ¬p. The next example uses both these rules to produce a
proof of (p → q) → ¬q → ¬p. (The symbol ¬ is produced by
typing \not or \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 的简称），或爆炸原理（principle of explosion）。The connective False has a single elimination rule,
False.elim, which expresses the fact that anything follows from a
contradiction. This rule is sometimes called ex falso (short for ex
falso sequitur quodlibet), or the principle of explosion.
从假推出的任意事实 q 是 False.elim 中的一个隐式参数，会自动推断。这种从矛盾假设推导出任意事实的模式非常常见，由 absurd 表示。The arbitrary fact, q, that follows from falsity is an implicit
argument in False.elim and is inferred automatically. This
pattern, deriving an arbitrary fact from contradictory hypotheses, is
quite common, and is represented by absurd.
variable (p q : Prop)
example (hp : p) (hnp : ¬p) : q := absurd hp hnp
例如，以下是 ¬p → q → (q → p) → r 的一个证明：Here, for example, is a proof of ¬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。Incidentally, just as False has only an elimination rule, True
has only an introduction rule, True.intro : True. In other words,
True is simply true, and has a canonical proof, True.intro.
3.3.4. 逻辑等价（Logical Equivalence）3.3.4. Logical Equivalence🔗
表达式 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 的一个证明：The expression Iff.intro h1 h2 produces a proof of p ↔ q from
h1 : p → q and h2 : q → p. The expression Iff.mp h
produces a proof of p → q from h : p ↔ q. Similarly,
Iff.mpr h produces a proof of q → p from h : p ↔ q. Here is a proof
of p ∧ q ↔ q ∧ p:
我们可以使用匿名构造子符号从正向和反向的证明构建 p ↔ q 的一个证明，我们也可以在 mp 和 mpr 上使用 . 符号。因此，前面的例子可以简洁地写成如下形式：We can use the anonymous constructor notation to construct a proof of
p ↔ q from proofs of the forward and backward directions, and we
can also use . notation with mp and mpr. The previous
examples can therefore be written concisely as follows:
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
3.4. 引入辅助子目标（Introducing Auxiliary Subgoals）3.4. Introducing Auxiliary Subgoals🔗
这是一个介绍 Lean 提供的另一个有助于构建长证明的工具的好地方，即 have（拥有）构造，它在证明中引入一个辅助子目标。这里有一个小例子，改编自上一节：This is a good place to introduce another device Lean offers to help
structure long proofs, namely, the have construct, which
introduces an auxiliary subgoal in a proof. Here is a small example,
adapted from the last section:
在内部，表达式 have h : p := s; t 产生项 (fun (h : p) => t) s。换句话说，s 是 p 的一个证明，t 是在假设 h : p 下对期望结论的一个证明，两者通过 λ 抽象和应用组合在一起。这个简单的工具在构建长证明时非常有用，因为我们可以使用中间的 have 作为通向最终目标的垫脚石。Internally, the expression have h : p := s; t produces the term
(fun (h : p) => t) s. In other words, s is a proof of p,
t is a proof of the desired conclusion assuming h : p, and the
two are combined by a lambda abstraction and application. This simple
device is extremely useful when it comes to structuring long proofs,
since we can use intermediate have's as stepping stones leading to
the final goal.
Lean 还支持一种结构化的从目标向后推理的方式，它模拟了通常数学中的"只需证明（suffices to show）"构造。下一个例子只是将前面证明中的最后两行交换了位置。Lean also supports a structured way of reasoning backwards from a
goal, which models the “suffices to show” construction in ordinary
mathematics. The next example simply permutes the last two lines in
the previous proof.
写 suffices hq : q 给我们留下两个目标。首先，我们必须通过证明在额外假设 hq : q 下原始目标 q ∧ p 来说明证明 q 确实足够了。最后，我们必须证明 q。Writing suffices hq : q leaves us with two goals. First, we have
to show that it indeed suffices to show q, by proving the original
goal of q ∧ p with the additional hypothesis hq : q. Finally,
we have to show q.
3.5. 经典逻辑（Classical Logic）3.5. Classical Logic🔗
我们目前所见到的引入和消去规则都是构造性的，也就是说，它们反映了基于命题即类型（propositions-as-types）对应的逻辑连接词的计算理解。普通的经典逻辑在此基础上增加了排中律（law of the excluded middle），p ∨ ¬p。要使用这个原理，你必须打开 classical 命名空间。The introduction and elimination rules we have seen so far are all
constructive, which is to say, they reflect a computational
understanding of the logical connectives based on the
propositions-as-types correspondence. Ordinary classical logic adds to
this the law of the excluded middle, p ∨ ¬p. To use this
principle, you have to open the classical namespace.
直观上，构造性的"Or"非常强：断言 p ∨ q 相当于知道哪一个成立。如果 RH 代表黎曼猜想，经典数学家愿意断言 RH ∨ ¬RH，即使我们还不能断言其中任何一个选言支。Intuitively, the constructive “Or” is very strong: asserting p ∨ q
amounts to knowing which is the case. If RH represents the Riemann
hypothesis, a classical mathematician is willing to assert
RH ∨ ¬RH, even though we cannot yet assert either disjunct.
排中律的一个结果是双重否定消去原理：One consequence of the law of the excluded middle is the principle of
double-negation elimination:
open Classical
theorem dne {p : Prop} (h : ¬¬p) : p :=
Or.elim (em p)
(fun hp : p => hp)
(fun hnp : ¬p => absurd hnp h)
双重否定消去允许我们通过假设 ¬p 并推导出 False 来证明任意命题 p，因为这样就相当于证明了 ¬¬p。换句话说，双重否定消允许我们进行反证法（proof by contradiction），这在构造逻辑中通常是不允许的。作为练习，你可以尝试证明其逆命题，即证明 em 可以从 dne 推出。Double-negation elimination allows one to prove any proposition,
p, by assuming ¬p and deriving False, because that amounts
to proving ¬¬p. In other words, double-negation elimination allows
one to carry out a proof by contradiction, something which is not
generally possible in constructive logic. As an exercise, you might
try proving the converse, that is, showing that em can be proved
from dne.
经典公理还为你提供了额外的证明模式，可以通过诉诸 em 来证明。例如，你可以进行情况分析证明：The classical axioms also give you access to additional patterns of
proof that can be justified by appeal to em. For example, one can
carry out a proof by cases:
open Classical
variable (p : Prop)
example (h : ¬¬p) : p :=
byCases
(fun h1 : p => h1)
(fun h1 : ¬p => absurd h1 h)
或者你可以进行反证法证明：Or you can carry out a proof by contradiction:
open Classical
variable (p : Prop)
example (h : ¬¬p) : p :=
byContradiction
(fun h1 : ¬p =>
show False from h h1)
如果你不习惯构造性思维，可能需要一些时间来感受经典推理在何处被使用。在下面的例子中需要它，因为从构造性的角度来看，知道 p 和 q 并非同时为真，并不一定能告诉你哪一个为假：If you are not used to thinking constructively, it may take some time
for you to get a sense of where classical reasoning is used. It is
needed in the following example because, from a constructive
standpoint, knowing that p and q are not both true does not
necessarily tell you which one is false:
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 在此类上下文中支持使用经典推理而不依赖于排中律。We will see later that there are situations in constructive logic
where principles like excluded middle and double-negation elimination
are permissible, and Lean supports the use of classical reasoning in
such contexts without relying on excluded middle.
用于支持经典推理的完整公理列表在公理与计算（Axioms and Computation）中讨论。The full list of axioms that are used in Lean to support classical
reasoning are discussed in Axioms and Computation.
3.6. 命题有效性示例（Examples of Propositional Validities）3.6. Examples of Propositional Validities🔗
Lean 的标准库包含了许多命题逻辑有效语句的证明，你都可以在自己的证明中自由使用它们。以下列表包含一些常见的恒等式。Lean's standard library contains proofs of many valid statements of
propositional logic, all of which you are free to use in proofs of
your own. The following list includes a number of common identities.
交换律：Commutativity:
-
p ∧ q ↔ q ∧ pp ∧ q ↔ q ∧ p
-
p ∨ q ↔ q ∨ pp ∨ q ↔ q ∨ p
结合律：Associativity:
-
(p ∧ q) ∧ r ↔ p ∧ (q ∧ r)(p ∧ q) ∧ r ↔ p ∧ (q ∧ r)
-
(p ∨ q) ∨ r ↔ p ∨ (q ∨ r)(p ∨ q) ∨ r ↔ p ∨ (q ∨ r)
分配律：Distributivity:
-
p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)
-
p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)
其他性质：Other properties:
-
(p → (q → r)) ↔ (p ∧ q → r)(p → (q → r)) ↔ (p ∧ q → r)
-
((p ∨ q) → r) ↔ (p → r) ∧ (q → r)((p ∨ q) → r) ↔ (p → r) ∧ (q → r)
-
¬(p ∨ q) ↔ ¬p ∧ ¬q¬(p ∨ q) ↔ ¬p ∧ ¬q
-
¬p ∨ ¬q → ¬(p ∧ q)¬p ∨ ¬q → ¬(p ∧ q)
-
¬(p ∧ ¬p)¬(p ∧ ¬p)
-
p ∧ ¬q → ¬(p → q)p ∧ ¬q → ¬(p → q)
-
¬p → (p → q)¬p → (p → q)
-
(¬p ∨ q) → (p → q)(¬p ∨ q) → (p → q)
-
p ∨ False ↔ pp ∨ False ↔ p
-
p ∧ False ↔ Falsep ∧ False ↔ False
-
¬(p ↔ ¬p)¬(p ↔ ¬p)
-
(p → q) → (¬q → ¬p)(p → q) → (¬q → ¬p)
这些需要经典推理：These require classical reasoning:
-
(p → r ∨ s) → ((p → r) ∨ (p → s))(p → r ∨ s) → ((p → r) ∨ (p → s))
-
¬(p ∧ q) → ¬p ∨ ¬q¬(p ∧ q) → ¬p ∨ ¬q
-
¬(p → q) → p ∧ ¬q¬(p → q) → p ∧ ¬q
-
(p → q) → (¬p ∨ q)(p → q) → (¬p ∨ q)
-
(¬q → ¬p) → (p → q)(¬q → ¬p) → (p → q)
-
p ∨ ¬pp ∨ ¬p
-
(((p → q) → p) → p)(((p → q) → p) → p)
标识符 sorry 神奇地产生任何命题的证明，或提供任何数据类型的对象。当然，作为一种证明方法它是不健全的——例如，你可以用它来证明 False——并且当文件使用或导入依赖于它的定理时，Lean 会发出严重警告。但它在逐步构建长证明时非常有用。从顶部开始向下编写证明，使用 sorry 来填充子证明。确保 Lean 接受了带有所有 sorry 的项；如果没有，说明存在需要纠正的错误。然后回过头来，将每个 sorry 替换为实际的证明，直到没有剩余。The sorry identifier magically produces a proof of anything, or
provides an object of any data type at all. Of course, it is unsound
as a proof method—for example, you can use it to prove False—and
Lean produces severe warnings when files use or import theorems
which depend on it. But it is very useful for building long proofs
incrementally. Start writing the proof from the top down, using
sorry to fill in subproofs. Make sure Lean accepts the term with
all the sorry's; if not, there are errors that you need to
correct. Then go back and replace each sorry with an actual proof,
until no more remain.
这是另一个有用的技巧。你可以使用下划线 _ 作为占位符，而不是使用 sorry。回想一下，这告诉 Lean 该参数是隐式的，应该自动填充。如果 Lean 尝试这样做但失败了，它会返回一条错误消息"“不知道如何合成占位符”，后跟它期望的项的类型以及上下文中所有可用的对象和假设。换句话说，对于每个未解析的占位符，Lean 会报告当时需要填充的子目标。然后你可以通过逐步填充这些占位符来构建证明。Here is another useful trick. Instead of using sorry, you can use
an underscore _ as a placeholder. Recall this tells Lean that
the argument is implicit, and should be filled in automatically. If
Lean tries to do so and fails, it returns with an error message “don't
know how to synthesize placeholder,” followed by the type of
the term it is expecting, and all the objects and hypotheses available
in the context. In other words, for each unresolved placeholder, Lean
reports the subgoal that needs to be filled at that point. You can
then construct a proof by incrementally filling in these placeholders.
作为参考，以下是两个取自上面列表的有效性示例证明。For reference, here are two sample proofs of validities taken from the
list above.
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)
3.7. 练习（Exercises）3.7. Exercises
证明以下恒等式，将 sorry 占位符替换为实际证明。Prove the following identities, replacing the sorry placeholders with actual proofs.
variable (p q r : Prop)
-- commutativity of ∧ and ∨
declaration uses 'sorry'example : p ∧ q ↔ q ∧ p := sorry
declaration uses 'sorry'example : p ∨ q ↔ q ∨ p := sorry
-- associativity of ∧ and ∨
declaration uses 'sorry'example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry
declaration uses 'sorry'example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry
-- distributivity
declaration uses 'sorry'example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := sorry
declaration uses 'sorry'example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := sorry
-- other properties
declaration uses 'sorry'example : (p → (q → r)) ↔ (p ∧ q → r) := sorry
declaration uses 'sorry'example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := sorry
declaration uses 'sorry'example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := sorry
declaration uses 'sorry'example : ¬p ∨ ¬q → ¬(p ∧ q) := sorry
declaration uses 'sorry'example : ¬(p ∧ ¬p) := sorry
declaration uses 'sorry'example : p ∧ ¬q → ¬(p → q) := sorry
declaration uses 'sorry'example : ¬p → (p → q) := sorry
declaration uses 'sorry'example : (¬p ∨ q) → (p → q) := sorry
declaration uses 'sorry'example : p ∨ False ↔ p := sorry
declaration uses 'sorry'example : p ∧ False ↔ False := sorry
declaration uses 'sorry'example : (p → q) → (¬q → ¬p) := sorry
证明以下恒等式，将 sorry 占位符替换为实际证明。这些需要经典推理。Prove the following identities, replacing the sorry placeholders
with actual proofs. These require classical reasoning.
open Classical
variable (p q r : Prop)
declaration uses 'sorry'example : (p → q ∨ r) → ((p → q) ∨ (p → r)) := sorry
declaration uses 'sorry'example : ¬(p ∧ q) → ¬p ∨ ¬q := sorry
declaration uses 'sorry'example : ¬(p → q) → p ∧ ¬q := sorry
declaration uses 'sorry'example : (p → q) → (¬p ∨ q) := sorry
declaration uses 'sorry'example : (¬q → ¬p) → (p → q) := sorry
declaration uses 'sorry'example : p ∨ ¬p := sorry
declaration uses 'sorry'example : (((p → q) → p) → p) := sorry
证明 ¬(p ↔ ¬p) 而不使用经典逻辑。Prove ¬(p ↔ ¬p) without using classical logic.
