类型与命题

Introduction

上一关我们证明了「S → S」，但 S 是什么？为什么 S 既是「类型」又是「命题」？在 Lean 里，**命题就是类型**。`P ∧ Q → P` 这个命题，其实也是一个类型——如果你能构造出这个类型的一个元素（写一个证明），你就证明了它。本关的目标：证明 **「如果 P 且 Q，那么 P」**。这比上一关多了一个新东西：`∧`（合取/「且」）。我们需要学会怎么把 `P ∧ Q` 拆开，拿出里面的 P。

本关学到的新东西

策略 (Tactics)

rcases拆解一个结构（如 ∧），把里面的各部分拿出来

概念 (Concepts)

合取 (∧)「且」——P ∧ Q 表示 P 和 Q 同时成立

Prop命题类型。P : Prop 表示 P 是一个命题

⟨⟩ 模式匹配用来拆解结构。⟨hp, hq⟩ 表示把 P∧Q 拆成 hp 和 hq

证明目标

当前目标

P Q : Prop

⊢P ∧ Q → P

分步提示

1.第一步和上一关一样：用 `intro h` 把前提 P ∧ Q 拿到手里。
2.现在你手里有 `h : P ∧ Q`，需要把它拆开。用 `rcases h with ⟨hp, hq⟩` —— 这会把 h 拆成两个独立的条件：hp: P 和 hq: Q。
3.你的目标是 P。正好手里有 hp: P，直接 `exact hp` 即可。

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

Lean 代码编辑器