蕴涵与全称量词

Introduction

数学中我们常说「对任意 x，都有 ...」。这在 Lean 里用 **∀** 表示。本关要证明一个「显然」的命题：**对任意命题 a，a → a**。说白了就是：不管 a 是什么命题，如果 a 成立，那么 a 成立。这里出现了两个量词：`∀ a : Prop` 和 `a → a`。有趣的是，**intro 对两者都管用**——你马上会看到。

本关学到的新东西

策略 (Tactics)

intro (对 ∀)intro 也可以引入 ∀ 量词，和引入 → 的前提一样

概念 (Concepts)

全称量词 (∀)「对所有」——∀ x, P(x) 表示对任意 x，P(x) 成立

Prop 宇宙a : Prop 说明 a 是一个命题，intro 可以引入任意类型

证明目标

当前目标

⊢∀ a : Prop, a → a

分步提示

1.用 `intro a` 引入命题变量 a。这一步相当于说「取任意一个命题，叫它 a」。
2.现在目标变成了 `a → a`。和第一关一样，用 `intro h` 引入前提 h: a。
3.目标变成了 a，手里有 h: a，用 `exact h` 完成。

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

Lean 代码编辑器