wfSet,良构不变量,引理调引理

uniq-set.dfy

Dafny 4.11.0 全绿的完整答案版。抄写顺序 = 文件顺序 = 难度顺序。带 ★ 的是考点,考前一天只复习 ★。

本文件要证的五条引理:

member(x,insert(y,A)) <==> x == y || member(x,A)
member(x,delete(y,A)) <==> x != y && member(x,A)
member(x,union(A,B)) <==> member(x,A) || member(x,B)
member(x,inter(A,B)) <==> member(x,A) && member(x,B)
member(x,A) && subset(A,B) ==> member(x,B)

member 与 wfSet：良构不变量

wf 是 well-formed(良构)的缩写:头不在尾里,且尾自身良构——整条列表无重复。

include "../core-list.dfy"

predicate member(x : int, A : lset)
{
    match A
    case Nil => false
    case Cons(y,ys) => x == y || member(x,ys)
}

predicate wfSet( A : lset)
{
    match A
    case Nil => true
    case Cons(x,xs) => !member(x,xs) && wfSet(xs)
}

insert：让 member 把门

★ 设计:让 member 把门,不在集合里才 Cons,insert 天生不制造重复。代价换来的好处:insert 不递归 => 下面两条引理不需要归纳,Dafny 展开一层定义就能自己看出来,空体 {} 即可通过。

★ requires 不能删:A 自己带病(如 [1,1]),insert 救不回来。

function insert(x: int, A: lset): lset
{
    if member(x, A) then A else Cons(x, A)
}

lemma member_insert(x: int, y: int, A: lset)
  ensures member(x, insert(y, A)) <==> x == y || member(x, A)
{
}

lemma wfSet_insert(x: int, A: lset)
  requires wfSet(A)
  ensures wfSet(insert(x, A))
{
}

delete：真归纳的起点

★ 规格 member_delete 没带 wf 前提 => 实现必须"删干净":命中头之后尾巴还要继续删(x==y 分支里仍递归),不能只删第一个。

★ 归纳的标准形状:match 拆结构,对尾巴调用引理自己 = 归纳假设。delete 是递归函数,所以这里开始必须真归纳,空体不算你的功。

function delete(x: int, A: lset): lset
{
    match A
    case Nil => Nil
    case Cons(y, ys) => if x == y then delete(x, ys) else Cons(y, delete(x, ys))
}

lemma member_delete(x: int, y: int, A: lset)
  ensures member(x, delete(y, A)) <==> x != y && member(x, A)
{
    match A
    case Nil =>
    case Cons(z, zs) =>
        member_delete(x, y, zs);
}

wfSet_delete：第一次"引理调引理"

★★ Cons 分支缺的事实是 !member(y, delete(x, ys)),由 member_delete(y, x, ys) 提供——注意实参顺序:问的是"头 y 在不在删完 x 的尾巴里",所以 y 在前 x 在后。喂反必红。

lemma wfSet_delete(x: int, A: lset)
  requires wfSet(A)
  ensures wfSet(delete(x, A))
{
    match A
    case Nil =>
    case Cons(y, ys) =>
        wfSet_delete(x, ys);      // 归纳假设:尾巴删完仍良构
        member_delete(y, x, ys);  // 弹药:头 y 不会出现在删完的尾巴里
}

inter：只需要 A 干净

以 A 为骨架过滤:头在 B 里才留下。

★ 只需要 wfSet(A):结果的骨架全部来自 A,B 脏不脏无所谓。

function inter(A: lset, B: lset): lset
{
    match A
    case Nil => Nil
    case Cons(x, xs) => if member(x, B) then Cons(x, inter(xs, B)) else inter(xs, B)
}

lemma member_inter(x: int, A: lset, B: lset)
  ensures member(x, inter(A, B)) <==> member(x, A) && member(x, B)
{
    match A
    case Nil =>
    case Cons(y, ys) =>
        member_inter(x, ys, B);
}

lemma wfSet_inter(A: lset, B: lset)
  requires wfSet(A)
  ensures wfSet(inter(A, B))
{
    match A
    case Nil =>
    case Cons(x, xs) =>
        wfSet_inter(xs, B);
        member_inter(x, xs, B);  // 弹药:x 不在 xs 里 => x 不在 inter(xs,B) 里
}

subset：单向 ==>

A 的每个头都得在 B 里。

★ 这条是单向 ==>,不是 <==>:x 在 B 里推不回"x 在 A 里"。

predicate subset(A: lset, B: lset)
{
    match A
    case Nil => true
    case Cons(x, xs) => member(x, B) && subset(xs, B)
}

lemma member_subset(x: int, A: lset, B: lset)
  ensures member(x, A) && subset(A, B) ==> member(x, B)
{
    match A
    case Nil =>
    case Cons(y, ys) =>
        member_subset(x, ys, B);
}

union：这次 A、B 都要干净

逐个把 A 的元素垒到 B 前面:已在 B 里就跳过(和 insert 同一个把门思路)。

★ 这次 A、B 都要干净:Nil 分支直接返回 B,B 的病没人治。(对比 inter 只要 A 干净——差别全在 Nil 分支返回什么。)

function union(A: lset, B: lset): lset
{
    match A
    case Nil => B
    case Cons(x, xs) => if member(x, B) then union(xs, B) else Cons(x, union(xs, B))
}

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(y, ys) =>
        member_union(x, ys, B);
}

lemma wfSet_union(A: lset, B: lset)
  requires wfSet(A) && wfSet(B)
  ensures wfSet(union(A, B))
{
    match A
    case Nil =>
    case Cons(x, xs) =>
        wfSet_union(xs, B);
        member_union(x, xs, B);  // 弹药:x 既不在 xs 也不在 B => 不在 union(xs,B)
}

card：势只在良构时有意义

就是数长度。注意它对 [1,1] 会数出 2:"势"只在 wfSet 成立时才有集合意义——这正是良构不变量存在的理由。

function card(A: lset): nat
{
    match A
    case Nil => 0
    case Cons(_, xs) => 1 + card(xs)
}