欢迎来到 Lean

Introduction

欢迎！这是你的第一个 Lean 证明。 Lean 是一种**交互式定理证明器**——你可以像写代码一样写数学证明，计算机会帮你检查每一步是否正确。本关我们要证明一个最简单不过的命题：**如果 S 成立，那么 S 成立**。听起来很废话？没错——但重点是学会两个最基本的操作： - 把「如果 P 则 Q」的假设 P 拿出来（这叫 **intro**） - 用手里已有的东西直接完成证明（这叫 **exact**）右侧编辑器里已经帮你写好了框架。你只需要理解每一行在干什么，然后点击 **运行 ▶** 即可。

本关学到的新东西

策略 (Tactics)

intro引入一个前提（假设），把 → 左边的东西拿到手里

exact当你手里有和目标一模一样的东西时，直接用它完成证明

概念 (Concepts)

命题 (Prop)可以判断真假的东西，比如「1+1=2」「S → S」

蕴涵 (→)「如果 A 则 B」，用 intro 处理它

证明目标

当前目标

S : Type

⊢S → S

分步提示

1.`intro hS` 的意思是：引入前提 S，给它起名叫 `hS`。现在我们的目标从「S → S」变成了「S」——因为前面已经有假设 hS: S 了。
2.`exact hS` 的意思是：我们的目标刚好就是 `hS`，直接用！

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

Lean 代码编辑器