setlists.dfy：全局图景（Lecture 06）
lset 就是 list<int>:拿一条整数列表冒充"集合"。 文件分上下两半:上半是 function/predicate——集合操作的实现;下半是 lemma——证明这些实现之间满足该有的数学关系。
每条 lemma 都长成同一个模样:member(x, 某操作的结果) ⟺ 用 member 和原料表达的等价说法。也就是说,member 是裁判:一个操作做得对不对,全看它对"谁是成员"这件事的影响是否符合集合论的定义。
※ 原文件里 12 条中有 2 条过不了验证(subset_union 空体、subset_trans 缺一步),修复处均已标注。全文件在 Dafny 4.11.0 下验证通过:14 verified, 0 errors。
member：裁判本人
i 在 s 里吗?空表里谁都不在;非空表:要么 i 就是头,要么去尾巴里继续找。
include "../core-list.dfy"
predicate member(i:int, s:lset)
{
match s
case Nil => false
case Cons(hd, tl) => hd == i || member(i, tl)
}if b then true else false 这类模式暴露的是一个思维习惯:你还在把 bool 当"需要用 if 检查的东西",而不是本身就可以直接返回、直接组合的值。布尔表达式是一等公民,||、&&、! 就是它的运算,如同 +、* 之于整数——你不会写 if x + y == x + y then x + y。
四个操作：insert、union、delete、intersect
insert 不查重——列表里允许重复元素,只要 member 的行为对,"集合"的门面就没破。delete 因此要删掉 i 的所有出现,删一次不够:命中头之后丢弃头、继续在尾里删。
// insert：直接把 i 摞在最前面。
function insert(i:int, s:lset) : lset
{
Cons(i, s)
}
// union（并集）：把 A 的元素逐个搬到 B 前面。
function union (A : lset, B : lset) : lset
{
match A
case Nil => B
case Cons(hd, tl) => Cons(hd, union(tl, B))
}
// delete：删掉 i 的所有出现。
function delete(i:int, A : lset) : lset
{
match A
case Nil => Nil
case Cons(hd, tl) =>
if i == hd then delete(i, tl)
else Cons(hd, delete(i, tl))
}
// intersect（交集）：A 里逐个检查，只留下同时也在 B 里的。
function intersect(A : lset, B : lset) : lset
{
match A
case Nil => Nil
case Cons(hd, tl) =>
if member(hd, B) then Cons(hd, intersect(tl, B))
else intersect(tl, B)
}"A 列表里除了 hd 的剩下部分"——就是 tl。case Cons(hd, tl) 这个模式匹配干的事:把 A 拆成头 hd 和尾 tl,两个名字当场就绑好了,伸手就能用。不需要递归去"剥",match 这一下已经剥完了——递归不是剥的工具,match 才是;递归是拿着剥出来的 tl 继续干活。
subset：空真打底
A 的每个元素都在 B 里。空集是任何集合的子集(空真)。
predicate subset(A : lset, B : lset)
{
match A
case Nil => true
case Cons(hd, tl) => member(hd, B) && subset(tl, B)
}下半场：定理的统一套路
空 {} 能过的,是 Dafny 自动归纳够得着的;需要写证明体的,都遵循同一个套路——对 A 做 match,Nil 分支留空,Cons 分支递归调用自己(= 归纳假设),必要时再搬一条别的 lemma 来补缺的那块事实。
member_insert：调用 lemma = 实例化定理
读作:x 在 insert(y, A) 里 ⟺ x 就是 y,或 x 本来就在 A 里。
lemma member_insert(x : int, y:int, A : lset)
//ensures member(i , s) ==> member(i, insert(i , s)) ← 旧版：单向蕴含太弱，拦不住错误实现
ensures member(x, insert(y, A)) <==> x == y || member(x, A)
{}先注意:没有返回类型。lemma 不计算任何东西,它是一条定理。参数也不是"输入",而是数学陈述里的全称变量——整条 lemma 读作:对任意 int x、对任意 int y、对任意 lset A,都有 member(x, insert(y, A)) ⟺ x == y ∨ member(x, A)。参数表就是"对任意……"那一串。
调用 lemma = 实例化定理。 function 调用是"算一下";lemma 调用是"把一般定理套到具体对象上"。在证明体里写 member_insert(3, 5, myset);,意思是:把那条 ∀ 定理里的 x、y、A 分别替换成 3、5、myset,于是此后 solver 就知道了 member(3, insert(5, myset)) <==> 3 == 5 || member(3, myset) 这个具体事实。没有任何计算发生,发生的是"一条知识进入了当前证明的视野"。
每见一个 lemma 的三问:量化了谁?(参数表)有没有前提?(requires)谈论的是谁和谁的关系?(ensures 里出现了哪几个函数)
member_delete：i != j 站错位置
读作:删完 i 之后 j 还在 ⟺ j 不是被删的那个,且 j 本来就在。
旧版写成 member(j, A) <==> member(j, delete(i, A)) && i != j——取 i = j = 3、A = [3] 即翻车。i != j 站错了位置:它被放在右边当结论的一部分,于是这条 lemma 在主张"j 在 A 里就能推出 i ≠ j";它该去约束左边。
lemma member_delete(i:int, j:int, A:lset)
//ensures member(j, A) <==> member(j, delete(i, A)) && i != j ← 旧版：i != j 站错位置
ensures member(j, delete(i, A)) <==> i != j && member(j, A)
{}member_inter 与 member_union：空体即过
x 在交集里 ⟺ x 同时在 A 和 B 里;x 在 A∪B 里 ⟺ x 在 A 里或在 B 里。定理说的就是"我们的实现兑现了教科书定义"——自动归纳够得着,空体即过。
lemma member_inter(x:int, A:lset, B:lset)
ensures member(x, intersect(A, B)) <==> member (x, A) && member(x, B)
{}
lemma member_union(x : int, A : lset, B : lset)
ensures member(x, union(A, B)) <==> member(x, A) || member(x, B)
{}member_subset：第一条带 requires
读作:若 A ⊆ B,则 x ∈ A ⟹ x ∈ B——这其实就是"子集"的语义。第一条带 requires 的:这是条件真理。
为什么空 {} 不够、要写证明体? subset 是沿着 A 递归定义的,所以证明也得沿着 A 归纳。Cons 分支里递归调用自己,传入更小的 tl——这一步的含义是"援引归纳假设"。
lemma member_subset(x:int, A:lset, B:lset)
requires subset(A, B)
ensures member(x, A) ==> member(x, B)
{
match A
case Nil =>
case Cons(hd, tl) => member_subset(x, tl, B);
// 拼图：若 x == hd，requires 展开后直接有 member(hd,B)；
// 若 x 在 tl 里，归纳假设（上面那行调用）给出 x 在 B 里。两路都通。
}case Nil => 什么都不写:A 空,member(x, Nil) 是 false,蕴含空真,solver 一眼看穿,分支留空即可。凭什么允许 lemma 调用自己?和函数递归同一条纪律——参数必须变小。
subset_union：A 出现两次,自动归纳使不上劲
读作:A 永远是 A∪B 的子集。 ※ 原文件此处是空 {}——验证失败(postcondition could not be proved)。
为什么空体不行? 结论 subset(A, union(A,B)) 里,A 出现了两次,归纳时两处得同步变小,Dafny 的自动归纳在这种形状上使不上劲,得手写。
Cons 分支的账,目标展开为两块:member(hd, Cons(hd, union(tl,B)))——头就在头上,显然真;subset(tl, Cons(hd, union(tl,B)))——这块是缺口。归纳假设(递归调用)只给到 subset(tl, union(tl,B)),右边少了个 Cons(hd,·)。于是搬来下面的 subset_widen(先用后证,Dafny 不在乎文件顺序):"子集关系不怕右边多塞一个元素"。两步接上,缺口闭合。
参数 C 通篇未用——老师的 stub 就长这样,保持原样,不删。
lemma subset_union(A : lset, B : lset, C : lset)
ensures subset(A, union(A, B))
{
match A
case Nil =>
case Cons(hd, tl) =>
subset_union(tl, B, C); // 归纳假设：subset(tl, union(tl,B))
subset_widen(tl, hd, union(tl, B)); // 加宽右侧：subset(tl, Cons(hd, union(tl,B)))
}subset_widen 与 subset_refl：互相搭肩膀
subset_widen 读作:若 A ⊆ B,往 B 头上再塞一个 y,A 仍是其子集——右边只会变大,子集关系不会因此坏掉。沿 A 归纳,标准套路。
subset_refl 读作:任何集合都是自己的子集(自反性)。Cons 分支要两步:归纳假设给 subset(tl, tl),但目标需要 subset(tl, Cons(hd, tl))——右边比左边多个 hd,正是 subset_widen 管的事。lemma 之间就这样互相搭肩膀。
lemma subset_widen(A: lset, y: int, B: lset)
requires subset(A, B)
ensures subset(A, Cons(y, B))
{
match A
case Nil =>
case Cons(hd, tl) => subset_widen(tl, y, B);
}
lemma subset_refl(A : lset)
ensures subset(A, A)
{
match A
case Nil =>
case Cons(hd, tl) => subset_refl(tl); subset_widen(tl, hd, tl);
}subset_trans：缺的是 member_subset
读作:子集关系可传递——A ⊆ B 且 B ⊆ C,则 A ⊆ C。 ※ 原文件的 Cons 分支只有 subset_trans(tl, B, C) 一行——验证失败。
差在哪? 目标 subset(Cons(hd,tl), C) 展开为两块:member(hd, C)——缺的就是它;subset(tl, C)——归纳假设已覆盖。手里有什么?requires 展开给出 member(hd, B),以及 subset(B, C)。从"hd ∈ B 且 B ⊆ C"到"hd ∈ C"——这正是 member_subset 那条定理。实例化 member_subset(hd, B, C),缺口闭合。
回看 member_subset 的三问:量化了 x、A、B;前提 subset(A,B);连接 member 与 subset。此刻正是它登场的形状。
lemma subset_trans(A : lset, B : lset, C : lset)
requires subset(A, B) && subset(B, C)
ensures subset(A, C)
{
match A
case Nil =>
case Cons(hd, tl) =>
member_subset(hd, B, C); // 修复：补上 hd ∈ C 这块拼图
subset_trans(tl, B, C); // 归纳假设：subset(tl, C)
}