如果……那么……

做完这一节，你能证明“如果 p 那么 r”这一类命题，并且看得懂 Lean 每一步给你的目标状态。

只用三个策略：intro、apply、exact。

学完你能做什么

• 读懂目标状态：横线上面是手里有的，⊢ 后面是要证的
• 用 exact 交出一个现成的证明
• 用 apply 倒着推，用 intro 收下假设

先看懂目标状态

写证明时，Lean 随时告诉你现在的处境。比如：

p q : Prop
hp : p
hpq : p → q
⊢ q

• p q : Prop：p 和 q 是两个命题，可以是任何一句话。
• hp : p：你手里有一个 p 成立的证明，名字叫 hp。
• hpq : p → q：你手里有“如果 p 那么 q”的证明，名字叫 hpq。
• ⊢ q：要证的是 q。

⊢ 上面的都是你能用的，叫假设。⊢ 后面的是目标。在 VS Code 里，把光标放在证明的某一行，右边的 Lean Infoview 面板就显示这一行之前的状态。

第 1 步：exact，手里正好有

目标是 p，手里正好有 p 的证明，直接交出去：

example (p : Prop) (hp : p) : p := by
  exact hp

你应该看到：没有报错。

交错了东西会怎样？手里是 p，目标是 q：

example (p q : Prop) (hp : p) : q := by
  exact hp

你应该看到：

Type mismatch
hp
has type
p
but is expected to have type
q

这是你以后最常见到的报错。它说的是：你给的是 p 的证明，这里要的是 q 的证明。

• 我知道 exact 要求给出的东西和目标完全对得上

第 2 步：apply，倒着推

目标是 q，手里有 hpq : p → q。它说“有 p 就有 q”。那么只要证出 p 就够了：

example (p q : Prop) (hp : p) (hpq : p → q) : q := by
  apply hpq
  exact hp

apply hpq 之后，目标从 q 变成了 p。这是倒着推：我要 q，谁能给我 q？hpq 能，但它要先拿到 p。于是问题变成证 p。

• 我知道 apply 会把目标换成“用这条规则还需要什么”

第 3 步：intro，收下“如果”

目标本身是“如果 p 那么 q”的时候，先假设 p 成立，再去证 q。intro 做的就是这件事：

example (p : Prop) : p → p := by
  intro hp
  exact hp

intro hp 把目标 p → p 里的前半截挪到上面，变成假设 hp : p，目标只剩后半截 p。名字 hp 是你起的。

• 我知道目标是 A → B 时，第一步通常是 intro

动手：把两条规则接起来

三个策略合起来用一次。已知“有 p 就有 q”和“有 q 就有 r”，证明“有 p 就有 r”。

动手证把两个“如果……那么……”接起来状态和报错由 Lean 4.35.0 生成

theorem imp_chain (p q r : Prop) (hpq : p → q) (hqr : q → r) : p → r := by
  intro hp
  apply hqr
  apply hpq
  exact hp

练习里的证明，写成代码是这样：

theorem imp_chain (p q r : Prop) (hpq : p → q) (hqr : q → r) : p → r := by
  intro hp
  apply hqr
  apply hpq
  exact hp

注意顺序：先 apply hqr，后 apply hpq。因为是倒着推的，目标是 r，离 r 最近的规则是 hqr。

检查点

• 给我一个目标状态，我能指出哪些是假设、哪个是目标
• 我能说出 exact、apply、intro 各自什么时候用
• 我在练习里证完了 imp_chain
• 我看得懂 Type mismatch 报错在说什么

没成功？

apply 之后目标没有变成我想的样子。 apply 只看规则的最后一截能不能对上目标。hpq : p → q 只能用在目标是 q 的时候。

intro 报错。 目标不是“如果……那么……”的形状时，没有东西可以收下。先看一眼 ⊢ 后面是什么。

下一节

命题不只有“如果……那么……”，还有“且”和“或”。下一节学怎么拆开它们、怎么拼出它们。