把引理当语句调用

4 minute read Published: 2026-08-18

nat-inductions.dfy

function sumUpTo(m:nat) : nat
{
    if m == 0 then 0 else m + sumUpTo(m - 1)
}

lemma sumUpTo_results()
  // test on arguments 2, 3 and 100, a conjunctive claim
  ensures sumUpTo(2) == 3
  ensures sumUpTo(3) == 6
  ensures sumUpTo(100) == 5050
  //ensures triangle(100) == 5050
  { triangle(100); }

method Main()
{
    print "sum(2) ==", sumUpTo(2), "\n";
    print "sum(3) ==", sumUpTo(3), "\n";
    print "sum(100) == ", sumUpTo(100), "\n";
}

// what's the formula?
lemma triangle(m:nat)
    ensures sumUpTo(m) == (1 + m) * m / 2
    {}

//因为递归函数sumUpTo虽然逻辑绝对正确，但它是O(N)的计算复杂度。在实际工程和算法优化中，我们更希望用一个O(1)的数学公式直接算出结果。

题面：闭式解作为 ensures

lemma 名字() —— 不能原样调用这行字，要调用函数。

写出自然数求和的闭式解（Closed-form expression），并将其作为这个引理的后置条件（ensures clause）。因为递归函数 sumUpTo 虽然逻辑绝对正确，但它是 O(N) 的计算复杂度，在实际工程和算法优化中，我们更希望一个 O(1) 的数学公式直接算出结果。

为什么一个 ensures 就够

为什么只写了一个 ensures 声明，Dafny 就能知道它是对的？

这依赖于数学归纳法（Mathematical Induction）。当在引理中写下这个契约时，Z3 求解器会自动利用函数的递归结构进行结构归纳证明：① 证明 Base Case ② 证明 Inductive Step

function 与 lemma 的本质区别

①function：它是一个纯粹的数学映射，它接收参数，并且返回一个具体的值，因此可以放在等式里，或者 ensures 这样的布尔表达式上下文中使用。

②lemma（引理）：它本质上是一个 Ghost Method（幽灵方法/证明过程）。引理不返回任何值。它的作用是在被调用时，向当前的证明上下文中注入它所保证的数学真理。

类型错误：triangle(100) == 5050

triangle(100) == 5050，是在试图获取一个引理的"返回值"并将其与数字进行比较。这在类型和语义上是完全错误的，好比在问编译器："勾股定理"这个概念本身等于几？

正确手法：将引理作为语句调用

要让 Z3 利用证明好的公式，必须将引理作为一个可执行的语句，放在代码块的内部，也就是花括号 {} 里，而不是作为契约（Contract）放在 ensures 后面。

把 triangle(100); 放在 {} 时，Z3 的运行逻辑：

  1. 它看到 triangle(100) 的调用，立刻去查阅 triangle 引理的定义，发现这个引理保证了（ensures）对于传入的参数 m，必定有 sumUpTo(m) == (1+m) * m / 2。
  2. 它将实参 100 代入，瞬间推导出一个绝对成立的真理：sumUpTo(100) == 5050，并把这真理加入到了当前的"已知上下文（context）"中。
  3. 接着，它回头去验证第 10 行那个曾因燃料耗尽而报错的 ensures sumUpTo(100) == 5050。这一次它不再需要递归展开一百次，因为上下文中已经存在这个事实。
  4. 匹配成功，红线消失。

pl-lemmas.dfy

lemma imp_conj_equiv(p:bool, q:bool, r:bool)
// ensures p ==> q ==> r ...
// 1. Exportation Law
    ensures (p ==> (q ==> r)) <==> ((p && q) ==> r)

// de-morgan : (¬(A ∧ B) ⇔ ¬A ∨ ¬B) ∧ (¬(A ∨ B) ⇔ ¬A ∧ ¬B)
// 2. De Morgan's Laws
    ensures !(p && q) <==> (!p || !q)
    ensures !(p || q) <==> (!p && !q)

// 3. Distributive Laws
// and-distributes over or
    ensures (p && (q || r)) <==> ((p && q) || (p && r))

// or-distributes over and
    ensures (p || (q && r)) <==> ((p || q) && (p || r))

// implication is just fancy disjunction
// 4. Implication is just fancy disjunction
    ensures (p ==> q) <==> (!p || q)
    {}