存在量词：有没有这样的东西？

Introduction

数学里不只说「对所有 x...」，也常说「存在一个 x...」。 `∃ x, P x` 读作「存在 x 使得 P(x) 成立」。本关目标：证明 **存在一个自然数 n，使得 n + 0 = 0**。这太简单了——n = 0 就行。但关键是要学会： - 怎么**构造**一个 ∃ 证明（提供「见证」`witness`） - 怎么**使用**一个 ∃ 假设（用 `rcases` 把见证拿出来）新策略 `refine` 比 `exact` 更灵活：它可以留下 `?_` 占位符表示「这个子目标等会儿再证」。

本关学到的新东西

策略 (Tactics)

refine部分构造证明。用 ?_ 表示「待填充的子目标」

refine ⟨w, ?_⟩对 ∃ 提供见证 w，留下一个需要证明的洞

概念 (Concepts)

存在量词 (∃)「存在」——∃ x, P x 表示至少有一个 x 使 P(x) 成立

见证 (witness)证明 ∃ 时需要明确给出一个具体的值

洞 (?_ 占位符)告诉 Lean「这里我知道要填什么，具体证明等会儿再写」

证明目标

当前目标

⊢∃ n : Nat, n + 0 = 0

分步提示

1.用 `refine ⟨0, ?_⟩` 告诉 Lean：「见证」是 n = 0，然后我还要证明 0 + 0 = 0。
2.`?_` 是一个「洞」——Lean 会把它变成一个新的子目标。运行后你会发现目标变成了 `0 + 0 = 0`。
3.现在目标是 `0 + 0 = 0`。根据自然数加法的定义，零加任何数等于它本身。直接用 `rfl` 就完成了。

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

Lean 代码编辑器