chunks,引理辅助终止

chunks.dfy

Dafny 4.11.0 全绿的完整答案版。引理辅助终止(lemma-assisted termination)——termination 系列的最终形态。带 ★ 的是考点。

先备好两块积木:

include "../core-list.dfy"

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

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

第一步：先证 length_drop

★ 先证一个关于 drop 的长度引理:drop 掉 n 个之后,长度要么归零(n 太大),要么正好减 n。空证明 {} 即过——Dafny 对这种跟着函数结构走的引理会自动归纳。

lemma length_drop<T>(n:nat, l:list<T>)
  ensures length(drop(n,l)) == if n >= length(l) then 0 else length(l) - n
{}

chunks 的行为与陷阱

chunks(2, [1,2,3,4]) == [[1,2], [3,4]]
chunks(3, [1,2])     == [[1,2]]
chunks(2, [1,2,3])   == [[1,2], [3]]
chunks(0, [1,2,3])   == ??

最后一行就是陷阱:没有 requires 0 < n 就是无限个空块,永不终止。

第二步：三件套合体

★★ 三件套合体,缺一个都过不了:

1. requires 0 < n —— 安全前置条件:排除 n == 0 的死循环
2. decreases length(l) —— 递归喂的是 drop(n,l),不是 l 的结构子项,所以 decreases l 没用,得用数值量 length(l)
3. 函数体内调用引理 —— Dafny 自己看不出 length(drop(n,l)) < length(l),在递归调用之前调一下 length_drop(n,l),把这条等式喂进它的"云",终止检查立刻通过。

引理调用后接分号再写表达式,这是函数体里合法的"语句表达式"语法。等价的啰嗦写法(考场上也认):

assert length(drop(n,l)) < length(l) by { length_drop(n,l); }

function chunks<T>(n : nat, l:list<T>) : list<list<T>>
  requires 0 < n
  decreases length(l)
{
    match l
    case Nil => Nil
    case _ =>
        length_drop(n, l);
        Cons(take(n,l), chunks(n, drop(n,l)))
}

手动展开一遍

chunks(3, [1,2]) == Cons(take(3, [1,2]), chunks(3, drop(3, [1,2])))
                 == Cons([1,2], chunks(3, []))
                 == Cons([1,2], [])
                 == [[1,2]]