lemma,谓词,等价关系,逻辑优先级

6 minute read Published: 2026-08-17

lemma 的骨架

lemma Name(参数)
    requires 前提条件   // "假设这些成立"
    ensures  结论      // "那么我保证这个成立"
{
}

花括号里是证明过程。很多时候留空，Dafny 自己就能推出来。

符号与整数除法

<==> 读作"当且仅当"。

/ 是整数除法，向下取整。7/2 = 3。

谓词（predicate）

返回 bool 的函数有个专门的名字叫谓词（predicate）：它接收若干个项（terms，这里是三个整数），然后告诉你是或否。函数体就是一个表达式，如 x % z == y % z 本身就是返回值。

等价关系的三条性质

数学上，一个关系要称得上"等价关系"，必须同时满足三条性质：

  1. 自反（reflexive）：任何 x 都与自己等价
  2. 对称（symmetric）：x 与 y 等价，则 y 与 x 等价
  3. 传递（transitive）：w 与 x 等价，x 与 y 等价，则 w 与 y 等价

怀疑一个关系有没有这些性质，不要靠感觉，写成 lemma 让验证器检查。

(Lecture05) equalmod-pred.dfy 还需多练。

function 与 method

①function：活在逻辑世界，纯粹，无副作用，可以出现在 requires/ensures 里。

②method：活在运行世界，可以打印，可以有可变状态，但不能直接被规约引用。

验证器的边界

验证器展开递归是有燃料（fuel）限制的，默认只肯展开几层。

证明擅长的是符号性、全称性的命题：测试验证有限个具体点，证明覆盖无限的全空间；各干各的活，别拿证明器当计算器使。

fact-testing.dfy

function fact(n : nat) : nat
{
    if n < 2 then 1 else n * fact(n-1)
}

lemma fact3()
  ensures fact(3) == 6
{}

lemma fact6_big()
  ensures fact(6) > 10
{}

method Main()
{
    print "fact(20) == ", fact(20), "\n";
}

// testing on concrete values using proof is not
// really what proof is good at...

// lemma fact20

// Symbolic results are better (factorials are never zero)

这个文件是在讲一个方法论问题:用证明器做"测试"的边界在哪里。逐层看。

第 1–4 行,递归定义阶乘。 if n < 2 then 1 else n * fact(n-1),教科书写法。注意参数和返回值都是 nat,这很关键——自然数类型天然排除了负数,所以 Dafny 能自动确认递归会终止(n 每次减一,不会无限跌落),也不用担心 n - 1 变负。

第 6–12 行,用 lemma 当测试用例。 fact(3) == 6、fact(6) > 10,空花括号就过了。这相当于单元测试,但比单元测试强:普通测试是"运行一次看结果",这里是编译期就被数学确认。Dafny 靠展开递归定义来验证——fact(3) 展开成 3 × 2 × 1,具体数字,算就完了。

第 14–17 行,method Main()。 注意 function 和 method 的分野,这是 Dafny 的核心设计:function 活在逻辑世界,纯粹、无副作用,可以出现在 requires/ensures 里;method 活在运行世界,可以打印、可以有可变状态,但不能直接被规约引用。想真正"跑"出 fact(20) 的值,就得用 method 打印。

第 19–24 行是本文件的题眼。 为什么注释掉了 lemma fact20?课上教授试过证 fact(20) == 2432902008176640000 这类具体断言,验证器搞不定。原因在于验证器展开递归是有燃料 (fuel) 限制的——默认只肯展开几层,fact(3) 三层它愿意,fact(20) 二十层它就拒绝陪你玩了,而强行展开也会让求解器在巨大的算式里迷路。运行程序算 fact(20) 瞬间出结果,证明它反而费劲——这就是第 19 行说的"用证明去测具体值,不是证明擅长的事"。

而第 24 行给出了正确的用法:证明擅长的是符号性、全称性的命题。"阶乘永远大于零"覆盖无穷多个 n,测试永远测不完,证明却一行搞定:

lemma factPositive(n: nat)
  ensures fact(n) > 0
{}

这个 Dafny 能自动过,因为它会对递归结构做归纳:n < 2 时是 1,大于零;否则是正数乘正数。

一句话总结这堂课埋的对比:测试验证有限个具体点,证明覆盖无限的全空间;各干各的活,别拿证明器当计算器使。这个认识后面做归纳证明时会反复用到。

写规约的优先级

写规约时宁可括号冗余，不要赌解析规则。

优先级：

  1. 最紧：&& 和 ||（同级，且不能裸混，要加括号）
  2. 中间：==>
  3. 最松：<==>