Lab02,手写归纳三件套,自动归纳,take/drop,二叉树

12 minute read Published: 2026-08-31

hello2.dfy：总览

本文件的主题只有两个:①递归数据类型上的递归函数怎么写(列表、树);②关于它们的引理怎么证明——什么时候 {} 就够,什么时候必须自己动手。第 2 点是整门课的心脏。 代码与原件逐字相同,验证结果:24 verified, 0 errors。

泛型与链表,正式版

<T> 是类型参数:定义一次,对任何元素类型都成立。读定义:一个 list<T> 的值,要么是 Nil(空表),要么是 Cons(hd, tl)——一个头元素 hd(类型 T),拼上剩余的表 tl(类型是自己!递归就藏在这)。字段起了名字 hd / tl,于是有两套取字段的方法:match 模式匹配(本文件主用),点选择器 l.hd、l.tl(zipPartial 处示范)。[5, 3] 这个表 = Cons(5, Cons(3, Nil)),没有方括号语法糖,一切都是构造子。

递归函数的标准骨架,往后所有函数都长这样:match 按构造子分情况(穷尽两种);Nil 不递归,直接给答案(基础情况);Cons 处理头,对更小的尾递归(递归情况)。停机为什么自动通过:递归调用作用在 xs 上,它是 l 的结构组成部分,结构递归 Dafny 免检放行。

datatype list<T> = Nil | Cons(hd : T, tl : list<T>)

function length<T>(l : list<T>) : nat
{
    match l
    case Nil => 0
    case Cons(_, xs) => 1 + length(xs)
}

// 拼接：把 l1 整个走一遍，走到底（Nil）时接上 l2。只对 l1 做 match。
function append<T>(l1 : list<T>, l2 : list<T>) : list<T>
{
    match l1
    case Nil => l2
    case Cons(x, xs) => Cons(x, append(xs, l2))
}

function min(a : nat, b : nat) : nat
{
    if a < b then a else b
}

take 与 drop

两个新知识点:

◆ match 也能用在数字上:case 0 匹配零,case _ 匹配"其余一切"(_ 是通配模式)。等价于 if n == 0 then ... else ...,纯风格选择。进入 case _ 分支后,Dafny 知道 n != 0,所以 n - 1 仍是合法的 nat。

◆ 嵌套 match 的归属规则:一旦开了内层 match,后续的 case 全部属于最里层的那个 match——缩进只是给人看的,Dafny 不看缩进。这里两个内层 case 都属于 match l,恰好是想要的。若想"回到外层继续写 case",必须给内层加花括号划界(下文 zipPartialLength 有示范)。这是嵌套 match 唯一的坑,先记住。

语义:n 和 l 谁先耗尽,谁说了算——take(5, [1,2]) == [1,2]。drop 与 take 严格互补——同一个输入,take 拿走的和 drop 留下的拼起来是原表(这句话就是下面 takeDropAppend 引理的内容)。注意 drop 的 case 0 => l:一个都不丢,整表返回。

function take<T>(n : nat, l : list<T>) : list<T>
{
    match n
    case 0 => Nil
    case _ =>
        match l
        case Nil => Nil
        case Cons(x, xs) => Cons(x, take(n-1, xs))
}

function drop<T>(n : nat, l : list<T>) : list<T>
{
    match n
    case 0 => l
    case _ =>
        match l
        case Nil => Nil
        case Cons(x, xs) => drop(n-1, xs)
}

反转:反转尾巴,再把头接到末尾。把单个元素接到末尾没有专门操作,只能 append 一个单元素表 Cons(x, Nil)。代价备注:append 是 O(长度),每层递归都做一次,整体 O(n²)。课程不考效率,但你应该看得出来。

function reverse<T>(l : list<T>) : list<T>
{
    match l
    case Nil => Nil
    case Cons(x, xs) => append(reverse(xs), Cons (x, Nil))
}

zip、unzip、zipPartial

zip:两表并成一表对。◆ 两个类型参数 <A, B>:两表元素类型可以不同,结果是"二元组的表"。◆ 对元组做 match:match (l1, l2) 把两个值捆在一起匹配,模式也写成对儿。case 从上往下试,第一个匹配上的生效——后两行的 _ 通配:(Nil, _) 此时只可能是 (Nil, Cons ...),因为 (Nil, Nil) 已被第一行截走。语义:短的一方耗尽即停(截断)。

function zip<A, B>(l1 : list<A>, l2 : list<B>) : list<(A, B)>
{
    match (l1, l2)
    case (Nil, Nil) => Nil
    case (Cons(x, xs), Cons(y, ys)) => Cons((x,y), zip(xs, ys))
    case (Nil, _) => Nil
    case (_, Nil) => Nil
}

unzip:一表对拆成两表。三个新语法点,都在 Cons 分支里:◆ 嵌套模式 Cons((x, y), rest)——外层拆 Cons,同时把头元素(一个二元组)也拆开,一步到位;◆ 表达式里的 var 配元组模式 var (xs, ys) := unzip(rest);——递归结果就地拆成两个名字;◆ 返回元组:直接写 (Cons(x, xs), Cons(y, ys)),"返回两个东西"就这么表达。

function unzip<A, B>(l : list<(A, B)>) : (list<A>, list<B>)
{
    match l
    case Nil => (Nil, Nil)
    case Cons((x, y), rest) =>
        var (xs, ys) := unzip(rest);
        (Cons(x, xs), Cons(y, ys))
}

zipPartial:等长版 zip,示范 match 之外的另一套拆值工具。◆ 判别器 l.Nil? / l.Cons?:返回 bool,"这个值是不是用该构造子造的"。◆ 选择器 l.hd / l.tl:取字段,前提是验证器必须能证明 l 确实是 Cons 造的。

现在看 requires 如何撑起整个函数体:else 分支里已知 l1 是 Cons,l1.hd、l1.tl 合法。但 l2.hd 呢?函数体没检查过 l2!——验证器替你推理:length(l1) == length(l2),而 l1 是 Cons ⟹ length(l1) ≥ 1 ⟹ length(l2) ≥ 1 ⟹ l2 不可能是 Nil。requires 不只是拦调用者,它是函数体内每一步"有定义"证明的原材料。删掉它,l2.hd 立刻报错。

function zipPartial<A, B>(l1 : list<A>, l2 : list<B>) : list<(A, B)>
  requires length(l1) == length(l2)
{
    if l1.Nil? then Nil
    else Cons((l1.hd, l2.hd), zipPartial(l1.tl, l2.tl))
}

下半场总纲：{} 与手写归纳三件套

一条 ensures P(x) 的引理,配上 {} 空体,含义是:"验证器,请你自己证明 P 对一切 x 成立"。验证器的武器有两件:(1) 把函数按定义展开、做代数(交给 SMT 求解器);(2) 自动归纳:对参数按结构做数学归纳。所以 {} 通过 ≠ 命题显然,而是"自动归纳恰好够用"。

自动归纳是启发式的,会失手。失手时,你手写证明。手写归纳的固定三件套,认准了:

match 参数——亲手按结构分情况;
基础分支留空——该分支的验证义务简单,SMT 直接过;
递归分支调用自己——lemma 在证明里调用自己 = "引用归纳假设"。调用 dropLength(n-1, xs) 的效果是:把它的 ensures 在 (n-1, xs) 上的实例作为已知事实注入当前上下文。停机检查同样适用于引理:参数在变小,所以这不是循环论证。

补一条位置规则:lemma 体是语句的地盘,这里的 match 是语句 match——case 右边放语句(可以是零条),不需要产出值。和 function 里的表达式 match 同形不同职。

四条空体引理

高斯求和:0+1+...+n 的两倍等于 n(n+1)。{} 通过——自动归纳对 nat 参数 n 做归纳,代数部分 SMT 收尾。纸上要写半页的归纳证明,这里一个空括号。先享受,别习惯。

lengthAppend:拼接的长度 = 长度之和。这条引理 lab03 会作为"给定弹药"再次出现——已证的引理可以在别的证明里调用,这是搭建证明库的起点。 takeLength:take 的长度 = min(n, 表长),两个参数同时递减的递归,自动归纳依然拿下。sub:nat 上的减法工具——nat 不允许负数,a - b 在 a < b 时越界,sub 把这种情况截到 0(数学上叫 monus),为 dropLength 的表述服务。

function sumUpTo(n : nat) : nat
{
    if n == 0 then 0 else n + sumUpTo(n - 1)
}

lemma triangle(n : nat)
  ensures 2 * sumUpTo(n) == n * (n + 1)
{}

lemma lengthAppend<T>(l1 : list<T>, l2 : list<T>)
  ensures length(append(l1, l2)) == length(l1) + length(l2)
{}

lemma takeLength<T>(n : nat, l : list<T>)
  ensures length(take(n, l)) == min(n, length(l))
{}

function sub(a: nat, b: nat): nat {
    if a < b then 0 else a - b
}

dropLength：第一次手写证明,逐行读

这条自动归纳失手了({} 不过),三件套上场:① match l 按结构分两案;② case Nil 空——drop(n, Nil) == Nil,sub(0, n) == 0,SMT 展开定义即得;③ case Cons 再按 n 分两案(if 是语句 if,带花括号):n == 0 时 drop(0, l) == l,两边直接相等,空体即过;n > 0 时 drop(n, Cons(x,xs)) 按定义 == drop(n-1, xs),要它的长度,正是本引理在更小输入 (n-1, xs) 上的内容——于是调用 dropLength(n - 1, xs) 把归纳假设注入,SMT 接着把 sub 的账算平。

为什么这条自动不行、上面几条却行?诚实的回答:自动归纳是启发式,目标形状与函数递归形状对不齐时(这里 ensures 右边是 sub(length(l), n),一个复合调用)就容易失手。不必深究它的内部标准——要掌握的是:失手时,你能自己写。

lemma dropLength<T>(n: nat, l: list<T>)
  ensures length(drop(n, l)) == sub(length(l), n)
{
    match l
    case Nil =>
    case Cons(x, xs) =>
        if n == 0 {
        } else {
            dropLength(n - 1, xs);
        }
}

take 和 drop 互补:前 n 个拼上剩下的 == 原表。证明结构与 dropLength 完全同构——同一副骨架,换一条命题。自己遮住下面,先默写一遍再对照。

lemma takeDropAppend<T>(n : nat, l : list<T>)
  ensures append(take(n, l), drop(n, l)) == l
{
    match l
    case Nil =>
    case Cons(x, xs) =>
        if n == 0 {
        } else {
            takeDropAppend(n-1, xs);
        }
}

unzipLength 与 zipPartialLength

unzip 保长:两个输出表的长度都等于输入长度。◆ 一条引理可以写多条 ensures,全部都要成立。◆ .0 / .1 取的是 unzip 返回的那个元组的分量。证明:对"二元组的表"归纳,模式还是那副骨架——只是这次不需要对 n 分案。(pair 这个名字没被用到,写 _ 也行。)

lemma unzipLength<A, B>(l: list<(A, B)>)
  ensures length(unzip(l).0) == length(l)
  ensures length(unzip(l).1) == length(l)
{
    match l
    case Nil =>
    case Cons(pair, xs) =>
        unzipLength(xs);
}

等长 zip 保长。看点是两表同步下降的归纳:拆完 l1 还要拆 l2,于是 lemma 体里嵌套 match。◆ 内层 match l2 加了花括号——回收 take 那里埋的伏笔:语句 match 用花括号明确划出自己的 case 范围,杜绝归属歧义。嵌套时养成加花括号的习惯。 ◆ 内层 case Nil 留空,但这个分支根本不可能发生:l1 是 Cons ⟹ 两表等长 ⟹ l2 非空。不可达分支下前提自相矛盾,任何验证义务都自动成立,空着即可。("不可达分支可以留空/省略"这件事,lab04 的 nth 会玩得更彻底。)

lemma zipPartialLength<A, B>(l1: list<A>, l2: list<B>)
  requires length(l1) == length(l2)
  ensures length(zipPartial(l1, l2)) == length(l1)
{
    match l1
    case Nil =>
    case Cons(x, xs) =>
        match l2 {
            case Nil =>
            case Cons(y, ys) =>
                zipPartialLength(xs, ys);
        }
}

二叉树：第二种递归数据类型

与 list 对照着看:list 的 Cons 里有一个自引用字段(tl);tree 的 Node 里有两个(left、right)。一切随之加倍:函数递归两次,归纳假设也有两条。

datatype tree<T> = Leaf | Node(left : tree<T>, val : T, right : tree<T>)

// 节点数：Leaf 不算，Node 算 1，加上左右子树各自的节点数。
function treeSize<T>(t: tree<T>): nat {
    match t
    case Leaf => 0
    case Node(l, _, r) => 1 + treeSize(l) + treeSize(r)
}

// 镜像：左右子树互换，并且递归地各自也镜像。
function mirror<T>(t: tree<T>): tree<T> {
    match t
    case Leaf => Leaf
    case Node(l, v, r) => Node(mirror(r), v, mirror(l))
}

镜像不改变节点数。树上的手写归纳:Node 分支引用两条归纳假设——左子树一条、右子树一条,缺一不可。之后 SMT 用加法交换律收尾。镜像两次 = 原树(镜像是自逆的),同一副树上归纳的骨架。

lemma mirrorSize<T>(t: tree<T>)
  ensures treeSize(mirror(t)) == treeSize(t)
{
    match t
    case Leaf =>
    case Node(l, v, r) =>
        mirrorSize(l);
        mirrorSize(r);
}

lemma mirrorMirror<T>(t: tree<T>)
  ensures mirror(mirror(t)) == t
{
    match t
    case Leaf =>
    case Node(l, v, r) =>
        mirrorMirror(l);
        mirrorMirror(r);
}

深度:到最深 Leaf 的路径长,走更深的那边——max。深度 ≤ 节点数(每往下走一层至少消耗一个节点):骨架第三次出现,两条归纳假设到手后,剩下的是 max(a,b) ≤ a + b 级别的算术,SMT 的份内事。到此为止你见过五条树引理/表引理长着同一张脸——这副骨架就是考试要默写的东西。

function max(a: nat, b: nat): nat {
    if a >= b then a else b
}

function maxDepth<T>(t: tree<T>): nat {
    match t
    case Leaf => 0
    case Node(l, _, r) => 1 + max(maxDepth(l), maxDepth(r))
}

lemma depthAndSize<T>(t : tree<T>)
  ensures maxDepth(t) <= treeSize(t)
{
    match t
    case Leaf =>
    case Node(l, _, r) =>
        depthAndSize(l);
        depthAndSize(r);
}