6260 notes: shadowing、ghost、集合引理、take/drop

12 minute read Published: 2026-08-19

alistmaps.dfy

include "../core-list.dfy"

// "dictionaries" are lists of integers (the keys), coupled
// with the values, which can be anything (generic/polymorphic)
type dict<V> = list<(int,V)>

function lookup<V>(key:int, dict:dict<V>) : option<V>
{
    match dict
    case Nil => None
    case Cons((j,v), rest) => if j == key then Some(v)
                              else lookup(key,rest)
}

function insert<V>(key : int, value : V, dict : dict<V>) : dict<V>
{
    Cons((key,value), dict)
}

lemma lookup_insert<V>(d:dict<V>, k:int, v:V)
  ensures lookup(k,insert(k,v,d)) == Some(v) {}

shadowing：新绑定压在旧绑定上面

插入已存在的键时,旧条目原地不动,变成永远查不到的僵尸——lookup 从头扫,总是先撞到新条目就返回了。语义上,"当前生效的绑定"由位置决定:越靠头越新,lookup 取第一个匹配 = 取最新写入。

这套"新绑定压在旧绑定上面"的结构,以后你在编译器和解释器里会反复遇到,它就是作用域环境(environment)的标准实现——进入内层作用域 Cons 新绑定,离开时丢掉头部,旧绑定自动恢复。

maplists.dfy

include "../core-list.dfy"

type intmap<V> = list<(int,V)>

ghost predicate member<T>(i :T, l : list<T>)
{
    match l
    case Nil => false
    case Cons(j,js) => i == j || member(i,js)
}

function keys<V>(m:intmap<V>) : list<int>
{
    match m
    case Nil => Nil
    case Cons((k,_), kvs) => Cons(k,keys(kvs))
}

function insert<V>(m : intmap<V>, k:int, v:V) : intmap<V>
{
    Cons((k,v), m)
}

function lookup<V>(m : intmap<V>, k:int) : option<V>
{
    match m
    case Nil => None
    case Cons((j,v), jvs) => if k == j then Some(v) else lookup(jvs, k)
}

lemma member_lookup<V>(m : intmap<V>, k : int, v : V)
  requires member((k,v), m)
  ensures exists u :: lookup(m,k) == Some(u)
{}

lemma lookup_some<V>(m : intmap<V>, k : int, v : V)
  ensures lookup(m,k) == Some(v) ==> member(k,keys(m))
{}

ghost：隔开验证世界与运行世界的墙

关键是 ghost 这个词。它宣布:这个定义只存在于验证世界,不存在于运行世界。编译成真实程序时,ghost 的东西全部被抹掉,不生成任何代码。它的用途是当规格语言——你拿它来陈述性质("这个键是成员"),而不是拿它来计算。

为什么要这个区分?因为规格追求"陈述得清楚",实现追求"跑得快",两者经常不是同一个定义。规格里你可以随便写 O(n) 的 member、甚至写根本不可执行的量词,反正它不用跑;实现那边该怎么优化怎么优化,最后用 lemma 证明实现符合规格。ghost 就是把这两个世界隔开的墙。这份代码里 member 只出现在 lemma 的 requires/ensures 里,从不被 insert/lookup 调用——它就是纯规格。

keys：模式匹配 = 解构 + 给成分起名

Cons 有两个槽位:头部元素、剩余列表。case Cons((k,_), kvs) 把头部拆成 (k,_),把剩余列表绑定到 kvs 这个名字上。

keys 的意义在 lookup_some 里:它让你能用 member(k, keys(m)) 说出**"键 k 出现在字典 m 里"**这句话。

member_lookup：把 ensures 削弱到刚好为真

ensures 里的 exists u :: P(u) 读作**"存在某个 u 使 P(u) 成立"**。整条 lemma:如果 (k,v) 在列表里,那么 lookup(m,k) 一定查得到某个值。

细品这个"某个"。为什么不直接写 ensures lookup(m,k) == Some(v)?因为那是假的——shadowing。(k,v) 可以躺在列表深处,而它前面压着一条更新的 (k, v'),lookup 会先撞到 v' 就返回。你拥有 (k,v) 这个成员资格,只能保证"查这个键不会落空",不能保证"查到的就是你那个 v"。

这条 lemma 的 ensures 被精确地削弱到刚好为真的程度——这是写规格的核心手艺:不是把你希望的写上去,而是把成立的写上去。上次说旧条目是"僵尸",这条 lemma 就是僵尸语义的正式化:僵尸能证明键活着,但发不出自己的声音。

lookup_some：双向锚定

两条合起来,把 lookup(可执行的实现)和 member(ghost 的规格)双向锚定:lookup 不会凭空捏造键,也不会漏掉存在的键。这就是"用 lemma 证明实现符合规格"的具体样子。

setlists.dfy

定义

include "../core-list.dfy"

// OK
predicate member(i:int, s:lset)
{
    match s
    case Nil => false
    case Cons(hd, tl) => hd == i || member(i, tl)
}

function insert(i:int, s:lset) : lset
{
    Cons(i, s)
}

function union (A : lset, B : lset) : lset //并集
{
    match A
    case Nil => B
    case Cons(hd, tl) => Cons(hd, union(tl, B))
}

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))
}

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)
}

predicate subset(A : lset, B : lset) //子集
{
    match A
    case Nil => true
    case Cons(hd, tl) => member(hd, B) && subset(tl, B)
}

bool 是一等公民

if b then true else false 这类模式暴露的是一个思维习惯:你还在把 bool 当"需要用 if 检查的东西",而不是本身就可以直接返回、直接组合的值。布尔表达式是一等公民,||、&&、! 就是它的运算,如同 +、* 之于整数——你不会写 if x + y == x + y then x + y。

递归不是剥的工具，match 才是

写 intersect 时要"A 列表里除了 hd 的剩下部分"——就是 tl。case Cons(hd, tl) 这个模式匹配干的事:把 A 拆成头 hd 和尾 tl,两个名字当场就绑好了,伸手就能用。不需要递归去"剥",match 这一下已经剥完了——递归不是剥的工具,match 才是;递归是拿着剥出来的 tl 继续干活。

引理

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

lemma member_delete(i:int, j:int, A:lset)
  ensures member(j, delete(i, A)) <==> i != j && member(j, A)
{}

lemma member_inter(x:int, A:lset, B:lset)
  ensures member(x, intersect(A, B)) <==> member (x, A) && member(x, B)
{}

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);
}

// feels like it should work
lemma member_union(x : int, A : lset, B : lset)
  ensures member(x, union(A, B)) <==> member(x, A) || member(x, B)
{}

lemma subset_union(A : lset, B : lset)
  ensures subset(A, union(A, B))
{
    match A
    case Nil =>
    case Cons(hd, tl) =>
        subset_union(tl, B);
        subset_widen(tl, hd, union(tl,B));
}

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);
}

lemma subset_trans(A : lset, B : lset, C : lset)
  requires subset(A, B) && subset(B, C)
  ensures subset(A, C)
  decreases A
{
    match A
    case Nil =>
    case Cons(hd, tl) =>
        member_subset(hd, B, C);
        subset_trans(tl, B, C);
}

lemma 是定理，不是函数

先注意:没有返回类型。lemma 不计算任何东西,它是一条定理。参数也不是"输入",而是数学陈述里的全称变量——member_insert 整条读作:对任意 int x、对任意 int y、对任意 lset A,都有 member(x, insert(y, A)) ⟺ x == y ∨ member(x, A)。参数表就是"对任意……"那一串。

lemma 名字(参数 = 全称变量)
  requires 前提   // 可选:定理的"若"
  ensures 结论    // 定理的"则"
{ 证明体 }        // 空 {} = 交给自动化

**调用 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,先别读 ensures 的内容,自问:

量化了谁?——参数表:这条定理对什么东西普遍成立
有没有前提?——requires:无条件真理还是条件真理
谈论的是谁和谁的关系?——ensures 里出现了哪几个函数:member_insert 连接 member 和 insert,lookup_some 连接 lookup、keys 和 member

member_delete：i != j 站错了位置

第一版:

ensures member(j, A) <==> member(j, delete(i, A)) && i != j

反例:i = j = 3,A = [3]。i != j 站错了位置:它被放在右边当结论的一部分,于是这条 lemma 在主张"j 在 A 里就能推出 i ≠ j"。它该去约束左边:

ensures member(j, delete(i, A)) <==> i != j && member(j, A)

读作:"删完之后 j 还在 ⟺ j 不是被删的那个,且 j 本来就在"。

规格的松紧：三次翻车

maplists 那次:ensures 写 Some(v) 是太强(shadowing 让它为假),只能退到 exists u;
member_insert 那次:单向蕴含 member(i, s) ==> member(i, insert(i, s)) 是太弱(拦不住错误实现);
今天:漏掉 i != j 这个前提,又是太强——多主张了一种它罩不住的情形。

member_subset：空真与合法的自我调用

case Nil => 什么都不写。A 空,member(x, Nil) 是 false,蕴含空真,solver 一眼看穿,分支留空即可。

凭什么允许 lemma 调用自己?和函数递归同一条纪律——参数必须变小。

subset_union：参数表由命题决定

名字和形式"neither here nor there"，重要的是命题。所以结论不变：ensures 里没有 C，它就不该在参数表里。

take-drop.dfy

include "../core-list.dfy"

function take<T> (n:nat, l : list<T>) : list<T>
{
    if n == 0 then Nil
    else
        match l
        case Nil => Nil
        case Cons(h,t) => Cons(h, take(n-1, t))
}

function drop<T>(n:nat, l : list<T>) : list<T>
{
    if n == 0 then l
    else
        match l
        case Nil => Nil
        case Cons(h, t) => drop((n-1), t)
}

信任递归调用（recursive leap of faith）

不再想"下一个在哪",而是想"drop(n-1, t) 这个表达式,就是'从 t 里丢掉 n-1 个'这件事的全部答案,我不需要知道它内部怎么够到每个元素,我只需要相信它兑现自己的合同,然后决定当前这一层怎么用它"。

写循环的人盯着迭代:指针挪到哪了、还剩几个。写递归的人只回答两问:最小的情形答案是什么;大一号的情形怎么由小一号的答案拼出来。

这个"信任"就是归纳假设

写递归时信任 drop(n-1, t) 会给出正确结果,和写证明时调用 member_subset(x, tl, B) 拿来归纳假设,是同一个动作在两个世界的投影——定义世界里叫递归调用,证明世界里叫实例化定理,合法性都由**"参数变小"**担保。为什么这门课让你反复体会"证明的形状追随定义的形状"?因为它们根本就是一体两面。

nat 递归的标准姿势

递归第一次不在列表上变小,而是在两个参数上同时变小。以后写 nat 上的递归,"先挡掉 0 再减 1" 的形状就是标准姿势。

take_drop：第一版的两处类型错

lemma take_drop<T>(n:nat, l: list<T>)
  ensures append(take(n, l), drop(n, l)) == l
{}

第一版写的是:

ensures Cons(take(n, l), drop(n, l)) <==> l

Cons 的合同你早上背过:第一个槽位放一个元素(T),第二个槽位放一条列表。而 take(n, l) 返回的是一整条列表——你把一条列表塞进了"单个元素"的槽位。类型对不上。列表世界里,"造"的动作有三个,各管各的——Cons(元素, 列表) 戴一顶帽子,append(列表, 列表) 接两条链子,(a, b) 根本不造列表、造的是 tuple。

<==> 是"当且仅当",它的两端必须是 bool——今天你用它连的都是 member(...) 这种谓词,所以顺。可 Cons(...) 和 l 是两条列表,是数据不是命题。问"两条列表是否相同",用的是 ==——数据相等;<==> 是真值等价。

take.dfy

include "../core-list.dfy"

// take with signature:
function take<T> (n:nat, l : list<T>) : list<T>

// and what's the right lemma to prove about the
// length of take(n,l) ?

// take + append:
// - take n elements from an append

// take equals Nil when?

{
    if n == 0 then Nil
    else
        match l
        case Nil => Nil
        case Cons(h, t) => Cons(h, take((n-1), t))
}

/*
function length<T>(l: list<T>): nat
{
    match l
    case Nil => 0
    case Cons(h, t) => 1 + length(t)
}
*/

lemma takeLength<T>(n:nat, l:list<T>)
  ensures length(take(n, l)) == if n <= length(l) then n else length(l)
{
    if n == 0 {
    } else {
        match l
        case Nil =>
        case Cons(h, t) => takeLength(n-1, t);
    }
}

takeLength：错误的 ensures 与反例

requires n >= 0 是废话,n : nat 类型已经担保了。

ensures 第一版:

ensures length(take(n, l)) + n == length(l)

反例:取 n = 5,l = [1]:take(5, [1]) 有多少给多少,是 [1],长度 1;左边 1 + 5 = 6,右边 1。炸了。

真命题是什么?take 的长度是"n 和列表长度里较小的那个":

ensures length(take(n, l)) == if n <= length(l) then n else length(l)

证明体第一版：参数没变小

{
    case l
    match Nil =>
    match Cons(h, t) => takeWhole(n, l);
}

takeWhole(n, l)——递归调用原样传了 l。这正是 intersect 翻车的同一跤,而且这次你知道后果的名字:参数没变小,归纳假设非法,termination 拒收。

证明的形状追随定义的形状

归纳调用必须踩着 t 下去,而且这条 lemma 的归纳还得跟着 take 的定义走——take 同时在拆 n 和 l,证明就得同样分岔。对照 take 的函数体看:if 对 if,match 对 match,take(n-1, t) 对 takeLength(n-1, t)——定义怎么分支,证明就怎么分支;定义怎么递归,归纳假设就怎么实例化。