命题和证明

到目前为止，您已经了解了在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) 为真。