assert-proofs.dfy
当空 {} 不够用时,你的第一件武器是 assert。上个文件里证明体全是空的,因为定理太简单;这个文件展示 Dafny 自动化卡住之后怎么办。
assert P; 是写在证明体里的一条语句,两件事同时发生:
- 要求 Dafny 当场证明 P 为真(证不出来它会报错);
- 一旦证出来,P 就成为一条"已知事实",摆在求解器眼前,供证明后续目标时使用。
所以 assert 的用法本质是铺垫:把结论拆成一块求解器啃得动的中间踏脚石,先让它站上去,再让它够到最终的 ensures。
例一：二次方程,空体侥幸
已知 (x-2)(x+6) == x² + 4x - 12。定理说:若 x² + 4x - 12 == 0,则 x 只能是 2 或 -6。Dafny 对二次的非线性算术还应付得来,空 {} 直接通过。
lemma solve_quadratic(x:int)
requires x * x + 4 * x - 12 == 0
ensures x == 2 || x == -6
{}例二：三次方程,喂因式分解
构造方式:(x - 3)(x - 2)(x + 6) = (x² - 5x + 6)(x + 6) = x³ + x² - 24x + 36。
为什么空 {} 这次不行? 乘法(非线性算术)是 SMT 求解器的天然弱项。二次它侥幸搞定,三次的乘法量级把自动化推过了极限——空证明体直接超时(Dafny 4.11.0 实测:1 time out)。
破局思路:求解器展开不了 x³,但它擅长两件事——(a) 验证一个给定的代数恒等式(两边展开比对,机械活);(b) 用**"整数乘积为 0 ⟹ 至少一个因子为 0"这类推理。所以用 assert 把因式分解形式喂**给它:
- 它验证恒等式 (x-3)(x-2)(x+6) == x³ + x² - 24x + 36;
- requires 说右边 == 0,于是左边乘积 == 0;
- 乘积为 0 ⟹ x-3、x-2、x+6 至少一个为 0 ⟹ ensures。
人负责提供"往哪个方向看",机器负责机械核算——这就是 assert 证明的标准分工。
lemma solve_poly(x : int)
requires x * x * x + x * x - 24 * x + 36 == 0
ensures x == 3 || x == 2 || x == -6
{
// 原文件此处为空(超时),补上这一行后全文件验证通过:
assert (x - 3) * (x - 2) * (x + 6) == x * x * x + x * x - 24 * x + 36;
}例三：整数除法,喂带余除法
定理读作:对任意自然数 x, y, z(z > 0),x < y/z 当且仅当 (x+1)·z ≤ y。直觉:y/z 是"y 里装得下几个完整的 z";x 严格小于这个个数,等价于说"哪怕再多一个(x+1 个)z,也仍然装得进 y"。
喂给它的踏脚石是除法的定义性等式(带余除法):y == (y/z) * z + y % z,其中 y % z 是余数,且 0 ≤ y % z < z(这条 Dafny 自己知道)。有了这条等式,两个方向都变成纯粹的不等式代数:
- (⟸) 若 (x+1)z ≤ y == (y/z)z + 余数 < (y/z)z + z = (y/z + 1)z,两边除掉 z 得 x+1 < y/z + 1,即 x < y/z。
- (⟹) 若 x < y/z,则 x+1 ≤ y/z,故 (x+1)z ≤ (y/z)z ≤ y。
这些代数求解器自己能走完——它缺的只是那条起点等式,因为它默认不会主动展开 / 和 % 的定义。
lemma xltdiv(x:nat, y:nat, z:nat)
requires 0 < z
ensures x < y / z <==> (x + 1) * z <= y
{
assert y == (y/z) * z + y % z ;
}