证明一个编译器是对的

这是毕业作品。做完这一节，你手里有一个迷你编译器，以及一条被 Lean 检查过的定理：对任何算式，编译出来的指令算出的结果，都和直接算这个算式一样。

不是“测了很多算式都对”，是全部。

用到的全是前面学过的东西：定义函数、对结构做归纳、卡住时找引理。

开始之前

• 学过对列表做归纳，知道引理是什么
• 新建一个文件 Compiler.lean，下面的代码按顺序写进去

第 1 步：定义算式，以及它“应该”等于几

一个算式要么是一个数，要么是两个算式相加，要么是两个算式相乘：

inductive Expr where
  | num : Nat → Expr
  | add : Expr → Expr → Expr
  | mul : Expr → Expr → Expr

inductive 定义一种新的数据，列出它所有可能的形状。

直接算出一个算式的值：

def eval : Expr → Nat
  | .num n => n
  | .add a b => eval a + eval b
  | .mul a b => eval a * eval b

eval 就是“正确答案”的定义。后面的编译器对不对，以它为准。

拿 2 + 3 × 4 试一下：

def demo : Expr := .add (.num 2) (.mul (.num 3) (.num 4))

#eval eval demo

14

• eval demo 算出 14

第 2 步：定义一台只认三种指令的机器

这台机器有一个栈，也就是一摞数，只能从顶上放和取。指令有三种：

inductive Instr where
  | push : Nat → Instr
  | add
  | mul

• push n：把 n 放到栈顶。
• add：取出栈顶的两个数，把它们的和放回去。
• mul：取出栈顶的两个数，把它们的积放回去。

运行一串指令：

def run : List Instr → List Nat → List Nat
  | [], stack => stack
  | .push n :: rest, stack => run rest (n :: stack)
  | .add :: rest, b :: a :: stack => run rest ((a + b) :: stack)
  | .mul :: rest, b :: a :: stack => run rest ((a * b) :: stack)
  | _ :: rest, stack => run rest stack

run 指令 栈 返回运行完之后的栈。最后一行处理栈里不够两个数的情况：跳过这条指令。

• Instr 和 run 没有报错

第 3 步：写编译器

把算式翻译成指令。一个数就是 push；加法是先算左边、再算右边、最后 add：

def compile : Expr → List Instr
  | .num n => [.push n]
  | .add a b => compile a ++ compile b ++ [.add]
  | .mul a b => compile a ++ compile b ++ [.mul]

把刚才的算式编译出来，在空栈上运行：

#eval run (compile demo) []

[14]

栈顶是 14，和 eval demo 一样。但这只是一个算式。

• run (compile demo) [] 得到 [14]

第 4 步：写下要证的那句话

“编译器是对的”得先说清楚是什么意思：

theorem compile_correct (e : Expr) (s : List Nat) :
    run (compile e) s = eval e :: s

读出来：对任何算式 e 和任何初始的栈 s，运行 e 编译出的指令，结果是在 s 的顶上多了一个数，这个数正是 eval e。

这一步比证明本身更要紧。第一节说过：Lean 检查的是你写下的这句话。这句话写对了，证明才有意义。

注意它说的是“任何初始的栈 s”，没有只说空栈。原因马上就会看到。

• 我能用自己的话讲出 compile_correct 在声称什么

第 5 步：先证帮手

compile 的结果是几段指令拼起来的。要推理它，得先知道：运行两段拼起来的指令，等于先运行第一段，再在它留下的栈上运行第二段。

theorem run_append (p q : List Instr) (s : List Nat) :
    run (p ++ q) s = run q (run p s) := by
  induction p generalizing s with
  | nil =>
    rfl
  | cons i rest ih =>
    cases i <;> rcases s with _ | ⟨b, _ | ⟨a, s⟩⟩ <;> simp [run, ih]

这是对指令列表 p 的归纳。有两处新东西：

• generalizing s：让归纳假设对任何栈都成立。每执行一条指令栈都在变，只对一个固定的栈成立的假设用不上。这也是上一步的定理要写“任何栈 s”的原因。
• 最后一行：按第一条指令是哪一种、栈里有零个、一个还是至少两个数，把所有情况都列出来，每种情况都交给 simp。<;> 的意思是“对产生的每个目标都做后面这一步”。

这一行现在不必全懂。知道它在做“分情况，每种都化简”就够了。

• run_append 通过了

第 6 步：证明编译器是对的

对算式的形状做归纳。算式有三种形状，所以有三个分支；加法和乘法各有两个子算式，所以各有两个归纳假设。你来走一遍：

动手证证明编译器是对的状态和报错由 Lean 4.35.0 生成

theorem compile_correct (e : Expr) (s : List Nat) : run (compile e) s = eval e :: s := by
  induction e generalizing s with
  | num n =>
    rfl
  | add a b iha ihb =>
    simp [compile, run_append, iha, ihb, run, eval]
  | mul a b iha ihb =>
    simp [compile, run_append, iha, ihb, run, eval]

写进文件：

theorem compile_correct (e : Expr) (s : List Nat) :
    run (compile e) s = eval e :: s := by
  induction e generalizing s with
  | num n =>
    rfl
  | add a b iha ihb =>
    simp [compile, run_append, iha, ihb, run, eval]
  | mul a b iha ihb =>
    simp [compile, run_append, iha, ihb, run, eval]

你应该看到：没有报错。

加法那一支里发生的事：compile 展开成三段指令；run_append 把“运行三段”拆成一段一段地运行；iha 说第一段运行完栈顶多了 eval a，ihb 说第二段运行完又多了 eval b；最后的 add 把它们加起来，正好是 eval (.add a b)。

• compile_correct 通过了

第 7 步：故意写一个错的编译器

验证有没有用，看它能不能抓住错误。把加法编译错：右边的算式不编译，左边的编译两遍。

def badCompile : Expr → List Instr
  | .num n => [.push n]
  | .add a _ => badCompile a ++ badCompile a ++ [.add]
  | .mul a b => badCompile a ++ badCompile b ++ [.mul]

theorem bad_correct (e : Expr) (s : List Nat) :
    run (badCompile e) s = eval e :: s := by
  induction e generalizing s with
  | num n =>
    rfl
  | add a b iha ihb =>
    simp [badCompile, run_append, iha, ihb, run, eval]
  | mul a b iha ihb =>
    simp [badCompile, run_append, iha, ihb, run, eval]

你应该看到：加法那一支证不过去，报错以这一行开头：

unsolved goals

这个错的编译器，对 1 + 1、2 + 2 这样左右相同的算式算出来全是对的。只测这几个，测试会通过。证明不会。

• 我看到了错的编译器证不过去

检查点

• 我的 Compiler.lean 从头到尾没有报错
• 我能说出 eval、run、compile 各自是什么
• 我能读出 compile_correct 这句话的意思
• 我知道为什么需要 run_append 这条引理
• 我见过一个测试能蒙混过去、证明过不去的错误

没成功？

compile_correct 报错说不认识 run_append。 引理要写在前面。

加法分支剩下目标没证完。 对照 simp 方括号里的六项，一个都不能少。尤其是 run_append，没有它，拼接起来的指令拆不开。

归纳假设用不上。 看 induction e 后面有没有写 generalizing s。

你做到了什么

你定义了一门小语言的含义，写了一个编译器，并且证明了它保持含义不变。验证一个程序，做的都是这三件事：写下“对”是什么意思，写程序，证明程序满足它。

接下来可以自己试的：

• 给 Expr 加一种形状，比如减法。Lean 会告诉你哪些函数和证明需要补上新的一支。
• 把 compile 里 a 和 b 的顺序对调，再看 compile_correct。加法那一支会剩下一个目标：eval b + eval a = eval a + eval b。这句话是真的，用上一章的 Nat.add_comm 就能补上。换成减法呢？剩下的那句话还是真的吗？