前一章你已经看到了在Lean中定义对象和函数的一些方法。在本章中，我们还将开始解释如何用依值类型论的语言来编写数学命题和证明。
命题即类型证明在依值类型论语言中定义的对象的断言（assertion）的一种策略是在定义语言之上分层断言语言和证明语言。但是，没有理由以这种方式重复使用多种语言：依值类型论是灵活和富有表现力的，我们也没有理由不能在同一个总框架中表示断言和证明。
例如，我们可引入一种新类型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 → Propvariable (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的证明的类型。“公理”是这个类型中的常值。
structure Proof (p : Prop) : Type where proof : p#check Proof -- Proof : Prop → Typeaxiom 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))然而，除了公理之外，我们还需要从旧证明中建立新证明的规则。例如，在许多命题逻辑的证明系统中，我们有肯定前件式（modus ponens）推理规则:
如果能证明Implies p q和p，则能证明q。
我们可以如下地表示它：
axiom modus_ponens : (p q : Prop) → Proof (Implies p q) → Proof p → Proof q命题逻辑的自然演绎系统通常也依赖于以下规则：
当假设p成立时，如果我们能证明q. 则我们能证明Implies p q.
我们可以如下地表示它：
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作为我们的蕴含概念。
这是在构造演算（Calculus of Constructions）中遵循的方法，因此在Lean中也是如此。自然演绎证明系统中的蕴含规则与控制函数抽象（abstraction）和应用（application）的规则完全一致，这是Curry-Howard同构的一个实例，有时也被称为命题即类型。事实上，类型Prop是上一章描述的类型层次结构的最底部Sort 0的语法糖。此外，Type u也只是Sort (u+1)的语法糖。Prop有一些特殊的特性，但像其他类型宇宙一样，它在箭头构造子下是封闭的:如果我们有p q : Prop，那么p → q : Prop。
至少有两种将命题作为类型来思考的方法。对于那些对逻辑和数学中的构造主义者来说，这是对命题含义的忠实诠释：命题p代表了一种数据类型，即构成证明的数据类型的说明。p的证明就是正确类型的对象t : p。
非构造主义者可以把它看作是一种简单的编码技巧。对于每个命题p，我们关联一个类型，如果p为假，则该类型为空，如果p为真，则有且只有一个元素，比如*。在后一种情况中，让我们说(与之相关的类型)p被占据（inhabited）。恰好，函数应用和抽象的规则可以方便地帮助我们跟踪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这与上一章中常量函数的定义完全相同，唯一的区别是参数是Prop的元素，而不是Type的元素。直观地说，我们对p → q → p的证明假设p和q为真，并使用第一个假设(平凡地)建立结论p为真。
请注意，theorem命令实际上是def命令的一个翻版：在命题和类型对应下，证明定理p → q → p实际上与定义关联类型的元素是一样的。对于内核类型检查器，这两者之间没有区别。
然而，定义和定理之间有一些实用的区别。正常情况下，永远没有必要展开一个定理的“定义”；通过证明无关性，该定理的任何两个证明在定义上都是相等的。一旦一个定理的证明完成，通常我们只需要知道该证明的存在；证明是什么并不重要。鉴于这一事实，Lean将证明标记为不可还原（irreducible），作为对解析器（更确切地说，是繁饰器）的提示，在处理文件时一般不需要展开它。事实上，Lean通常能够并行地处理和检查证明，因为评估一个证明的正确性不需要知道另一个证明的细节。
和定义一样，#print命令可以展示一个定理的证明。
theorem t1 : p → q → p := fun hp : p => fun hq : q => hp#print t1注意，lambda抽象hp : p和hq : q可以被视为t1的证明中的临时假设。Lean还允许我们通过show语句明确指定最后一个项hp的类型。
theorem t1 : p → q → p := fun hp : p => fun hq : q => show p from hp --试试改成 show q from hp 会怎样？添加这些额外的信息可以提高证明的清晰度，并有助于在编写证明时发现错误。show命令只是注释类型，而且在内部，我们看到的所有关于t1的表示都产生了相同的项。
与普通定义一样，我们可以将lambda抽象的变量移到冒号的左边：
theorem t1 (hp : p) (hq : q) : p := hp#print t1 -- p → q → p现在我们可以把定理t1作为一个函数应用。
theorem t1 (hp : p) (hq : q) : p := hpaxiom hp : ptheorem t2 : q → p := t1 hp这里，axiom