apply：反向推理的艺术

Introduction

目前为止，我们的证明都是从前提推到结论（前向推理）。但数学家常常**反着来**：看到目标，问「什么东西能推出它？」 `apply` 就是干这个的——它把目标替换成另一个更容易的目标。本关目标：证明 **蕴涵的传递性**。如果 P → Q 且 Q → R，那么 P → R。直观上：P 推 Q，Q 推 R，所以 P 推 R。用 `apply` 可以从目标 `R` 反推到 `Q`，再反推到 `P`——你就拿到了 P，完成。

本关学到的新东西

策略 (Tactics)

apply把目标 B 替换成 A，前提是需要一个 A → B 的引理

概念 (Concepts)

反向推理 (backward)从目标出发，找什么能推出它。和 intro 的前向推理互补

传递性 (transitivity)如果 A→B 且 B→C，则 A→C

证明目标

当前目标

P Q R : Prop

hpq : P → Q

hqr : Q → R

hP : P

⊢P → R

分步提示

1.目标现在是 `R`。手里有 `hqr : Q → R`。用 `apply hqr` 试试。
2.`apply hqr` 把目标从 `R` 变成了 `Q`（因为 `hqr` 说「如果 Q 则 R」）。
3.目标变成 `Q` 了。手里有 `hpq : P → Q`，再 `apply hpq`——目标变成 `P`。
4.目标变成 `P`。手上正好有 `hP : P`，`exact hP` 收工！

怎么玩：编辑器里有预写代码。直接点 运行 ▶ 看效果，或修改代码后运行。卡住了看左侧的提示。

Lean 代码编辑器