setlists.dfy（lecture08）
本文件真正要教的一个错误:原文件的证明体里写的是 union(tl, B);——一个函数调用被当作语句摆在了证明体里。这正是那个反复出现的错类:把一种构造塞进了不属于它的语法位置。修复见文末。
member 与 union：委托给 append
member 与 Lecture06 版逻辑相同,只是变量取名不同——j / rest 而非 hd / tl。名字随便取,match 当场绑定。
本版的独特之处:union 不自己递归,而是委托给 append——"并集"就是把两条列表首尾相接。允许重复元素,所以拼接即可:集合的门面由 member 维护,不由存储形态维护。
对照 L06 版你会发现:那边的 union 函数体和这里的 append 一模一样——同一段递归,两个名字。
include "../core-list.dfy"
predicate member(i:int, A:lset)
{
match A
case Nil => false
case Cons(j,rest) => j == i || member(i, rest)
}
function union (A : lset, B : lset) : lset
{
append(A,B)
}
// append：沿 A 递归，把 A 的元素逐个搬到 B 前面。
function append2 (A : lset, B : lset) : lset
{
match A
case Nil => B
case Cons(hd, tl) => Cons(hd, append2(tl, B))
}feels like it should work：果然有诈
讲义原注释语带保留,果然有诈。定理读作:对任意 x、A、B:x ∈ A∪B ⟺ x ∈ A 或 x ∈ B。
为什么空 {} 不够? 实测空体验证失败。L06 版里同一条定理空体就能过,差别在于这里多了一层间接——union 只是 append 的别名,Dafny 的自动归纳被这层转手挡住了,得手写归纳。
病灶：函数调用站在语句的位置
Cons 分支原本写的是 case Cons(hd, tl) => union(tl, B);,Dafny 报错:
expected method call, found expression病根用三分类说:证明体是语句的世界;union(tl, B) 是一个表达式——它算出一个列表,然后呢?没有然后。表达式不能光秃秃地站在语句的位置上;而且就算能站,"算一下并集"对证明毫无贡献——证明缺的从来不是值,是知识。
修复：一字之差,天壤之别
该站在这里的是 lemma 调用:member_union(x, tl, B);。这是递归调用自己 = 援引归纳假设——它把定理实例化到更小的 rest 上,让"member(x, union(tl,B)) ⟺ member(x,tl) ∨ member(x,B)"这条知识进入求解器视野。剩下的账它自己能算:
union(Cons(hd,tl), B) 展开（经 append）为 Cons(hd, union(tl,B))
x ∈ 左边 ⟺ x == hd ∨ x ∈ union(tl,B)
⟺ x == hd ∨ x ∈ tl ∨ x ∈ B （用归纳假设）
⟺ x ∈ Cons(hd,tl) ∨ x ∈ B ✓一字之差:函数名 union → lemma 名 member_union。函数调用是"算一下";lemma 调用是"一条知识进场"。证明体里永远要的是后者。(合法性同一条纪律:参数必须变小——tl ⊂ A。)
lemma member_union(x : int, A : lset, B : lset)
ensures member(x,union(A,B)) <==> member(x,A) || member(x,B)
{
match A
case Nil =>
case Cons(hd, tl) => member_union(x, tl, B); // 修复：函数调用 → lemma 调用
}