合取与双向蕴涵

Introduction

数学里经常要证明「A 当且仅当 B」。在 Lean 里这写成 `A ↔ B`。 `P ↔ Q` 其实就是 `(P → Q) ∧ (Q → P)` 的简写——即「P 推 Q」且「Q 推 P」。本关目标：证明 **P 且 Q 等价于 Q 且 P**（「且」交换律）。这很直观吧？但要写出形式化证明，你需要学会： - 怎么证明一个 ↔ （用 **constructor** 拆成两个方向） - 怎么构造一个 ∧（用 **⟨...⟩** 把两样东西包起来）

本关学到的新东西

策略 (Tactics)

constructor把 ↔ 或 ∧ 的证明拆成多个子目标

⟨⟩ 构造构造一个合取命题。⟨hq, hp⟩ 表示「hq 并且 hp」

概念 (Concepts)

双向蕴涵 (↔)「当且仅当」——P ↔ Q 等于 (P→Q) ∧ (Q→P)

子目标 (·)当一个证明分成多部分时，用 · 或缩进来表示每部分

证明目标

当前目标

P Q : Prop

⊢P ∧ Q ↔ Q ∧ P

分步提示

1.`constructor` 把 ↔ 拆成两个目标：(1) P∧Q → Q∧P 和 (2) Q∧P → P∧Q。
2.先证方向一：`intro h` 拿到 P∧Q，`rcases h with ⟨hp, hq⟩` 拆开，然后 `exact ⟨hq, hp⟩` 把 hq 和 hq 包成 Q∧P。
3.方向二几乎一样，只是换一下顺序。两部分的证明都可以写成一行。
4.注意 `·` 是一个缩进点，表示下一个子目标。在编辑器里可以不用，但推荐加上。

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

Lean 代码编辑器