# 第一个程序与第一个证明

> def/#eval/#check、theorem 与 by、Infoview 读法，以及「错误信息怎么读」。

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/first-steps
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

## 三个诊断命令

写 Lean 时最常用的三条命令，它们不产生任何代码，只在编辑器里给你反馈：

```lean
#eval 2 + 3          -- 5          求值
#check 2 + 3         -- 2 + 3 : Nat  查类型
#print Nat.add       --            看定义
```

| 命令 | 作用 |
| --- | --- |
| `#eval` | **计算**表达式的值 |
| `#check` | 显示表达式的**类型**，不求值 |
| `#print` | 显示某个名字的**定义** |

`#check` 是学 Lean 时用得最多的——**遇到任何不确定的东西，先 `#check` 一下**。

## 第一个程序

```lean
def hello : String := "Hello, Lean 4!"

#eval hello          -- "Hello, Lean 4!"
```

`def 名字 : 类型 := 值`。类型可以省略（Lean 会推断），但**公开的定义建议写全**：

```lean
def answer := 42            -- 推断为 Nat
def answer' : Nat := 42     -- 显式，更清晰
```

带参数：

```lean
def double (n : Nat) : Nat := n * 2

#eval double 21      -- 42
```

**函数调用不用括号**：写 `double 21` 而不是 `double(21)`。这是 ML 系语言的惯例，多参数时更明显：

```lean
def add (a : Nat) (b : Nat) : Nat := a + b

#eval add 3 4        -- 7
```

同类型参数可以合并写：

```lean
def add (a b : Nat) : Nat := a + b
```

## 可执行程序

```lean
def main : IO Unit :=
  IO.println "Hello from Lean!"
```

`main` 的类型是 `IO Unit`——一个「执行后产生副作用、返回空」的动作。[Monad 那一章](https://daiw.org/manual/lean4/monads)会讲清 `IO` 是什么。

```bash
lake exe myproject
```

## 第一个证明

```lean
theorem two_plus_two : 2 + 2 = 4 := by
  rfl
```

拆开看：

| 部分 | 含义 |
| --- | --- |
| `theorem` | 声明一个定理（与 `def` 几乎等价，见下） |
| `two_plus_two` | 定理的名字 |
| `2 + 2 = 4` | **要证的命题**——它同时是这个定理的「类型」 |
| `:=` | 「它的证明是」 |
| `by` | 进入 **tactic 模式** |
| `rfl` | 一个 tactic：「两边按定义相等」 |

`rfl` 是 reflexivity（自反性）——它能证明 `a = a` 形式的命题，且允许两边**按定义化简后**相等。`2 + 2` 与 `4` 在 `Nat` 上定义计算后确实是同一个项，所以 `rfl` 成功。

### theorem 与 def 的关系

```lean
def two_plus_two' : 2 + 2 = 4 := by rfl     -- 也合法！
```

**`theorem` 与 `def` 在类型检查层面几乎相同**。差别是工程性的：

- `theorem` 的内容被标记为**不可展开**（proof irrelevance 相关优化），编译时不生成代码。
- `def` 会参与计算与代码生成。

约定是：**类型是命题（`Prop`）时用 `theorem`，是数据时用 `def`**。这个区分在[命题即类型](https://daiw.org/manual/lean4/propositions-as-types)一章会讲透。

## 两种证明模式

### term 模式：直接给出证明项

```lean
theorem my_id (p : Prop) (hp : p) : p := hp
```

读作：「给定命题 `p` 和一个 `p` 的证明 `hp`，我要证 `p`——证明就是 `hp` 本身。」

**这就是一个普通的函数定义**。它接受参数、返回值，只不过参数是「证明」，返回的也是「证明」。

### tactic 模式：用 `by` 一步步构造

```lean
theorem my_id' (p : Prop) (hp : p) : p := by
  exact hp
```

`by` 后面是一串 **tactic**，每条指令改变当前的证明状态，直到目标被完全解决。

两种模式**可以混用**：

```lean
theorem mixed (p q : Prop) (hp : p) (hq : q) : p ∧ q :=
  ⟨hp, by exact hq⟩
```

**实践中绝大多数证明用 tactic 模式**——复杂证明写成 term 几乎不可读。

## 读 Infoview

这是最重要的技能。把光标放在 tactic 之间：

```lean
theorem example_state (a b : Nat) (h : a = b) : b = a := by
  -- 光标放这里，Infoview 显示：
  --   a b : Nat
  --   h : a = b
  --   ⊢ b = a
  exact h.symm
```

Infoview 显示的叫 **证明状态（goal state）**：

```text
a b : Nat        ← 局部上下文：有哪些东西可用
h : a = b        ← 包括假设（它们也是「有类型的项」）
⊢ b = a          ← 目标：要构造一个这个类型的项
```

`⊢` 读作 turnstile，左边是「已有的」，右边是「要证的」。

<Callout type="info">
  **读证明状态的正确方式：「我手上有这些项，要造出一个类型为目标的项。」**

  注意 `h : a = b` 与 `a b : Nat` 在形式上完全一样——都是 `某个名字 : 某个类型`。假设与数据在 Lean 里没有本质区别，这正是「命题即类型」的直接体现。
</Callout>

多个目标时会依次列出，用 `case` 或 `·`（focus dot）分别处理：

```lean
theorem two_goals (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp      -- 第一个目标
  · exact hq      -- 第二个目标
```

`·` 是圆点（U+00B7），VS Code 里输入 `\.` 自动补全。

## Unicode 输入

Lean 大量使用 Unicode 符号。编辑器扩展提供**反斜杠缩写**：

| 输入 | 得到 | 含义 |
| --- | --- | --- |
| `\to` 或 `\r` | `→` | 函数箭头 / 蕴含 |
| `\and` | `∧` | 合取 |
| `\or` | `∨` | 析取 |
| `\not` | `¬` | 否定 |
| `\iff` | `↔` | 当且仅当 |
| `\forall` 或 `\all` | `∀` | 全称量词 |
| `\exists` 或 `\ex` | `∃` | 存在量词 |
| `\Nat` | `ℕ` | 自然数 |
| `\lam` | `λ` | lambda |
| `\<` `\>` | `⟨` `⟩` | 匿名构造子 |
| `\.` | `·` | focus dot |
| `\l` | `←` | 反向（`rw` 用） |

输入缩写后按空格或 Tab 转换。**不记得某个符号怎么打**：把光标放在它上面，编辑器会提示缩写。

ASCII 替代大多存在（`->` 对 `→`、`/\` 对 `∧`、`fun` 对 `λ`），但社区惯例是用 Unicode。

## 错误信息怎么读

最常见的三类错误：

### type mismatch

```lean
def bad : Nat := "hello"
```

```text
type mismatch
  "hello"
has type
  String : Type
but is expected to have type
  Nat : Type
```

**结构固定**：给的是什么、它是什么类型、期望什么类型。从下往上读最快。

### unknown identifier

```text
unknown identifier 'foo'
```

名字拼错，或所在的模块没 `import`，或需要 `open` 某个命名空间。

### unsolved goals

```lean
theorem incomplete (n : Nat) : n + 0 = n := by
  skip
```

```text
error: unsolved goals
n : Nat
⊢ n + 0 = n
```

**tactic 跑完了但目标还在**。错误信息里会把剩余目标完整打印出来——这是最有用的一类错误，它直接告诉你还差什么。

<Callout type="warn">
  Lean 的错误信息有时会很长（尤其涉及类型类推断失败或 `simp` 循环）。**先看第一行的错误类型，再看最后的具体项**，中间的展开细节通常可以跳过。
</Callout>

## sorry

```lean
theorem hard_thing (n : Nat) : n * 0 = 0 := by
  sorry
```

`sorry` 是「先欠着」——它能通过类型检查，但会产生一个**警告**，且该定理会被标记为「使用了 sorry」。

它是开发过程中的重要工具：先用 `sorry` 把整个证明骨架搭起来，再逐个填坑。

<Callout type="warn">
  **`sorry` 会传染**：任何用到含 `sorry` 定理的定理，也是不可信的。Lean 会一路标记。

  检查一个定理是否真的完成，用：

  ```lean
  #print axioms hard_thing
  ```

  输出里若有 `sorryAx` 就说明没证完。CI 里应该检查这一点。
</Callout>

下一篇：[类型与项](https://daiw.org/manual/lean4/types-terms)。