chunks 的人话描述：两处校准
drop 给的不是"子集"，是剩余的后段：顺序不变、位置连续的尾巴。集合不讲顺序，列表讲——量词一上来，用词的松紧直接决定命题写不写得出。
停机点不是"tl 为 Nil"，是传给下一层的 l 为 Nil。chunks(3, [1,2]) 里 l = [1,2] 还是 Cons，这一层照常切，把 drop 吐出的 [] 抛给下一层，下一层撞上 case Nil 才停。差一层。
通往 Nil 的路有两条：长度不整除时，最后一块不足 n 个；恰好整除时，最后一块是满的。殊途同归，都以 drop 交出 Nil 收尾：
chunks(2, [1,2,3,4])
= Cons([1,2], chunks(2, [3,4]))
= Cons([1,2], Cons([3,4], chunks(2, []))) // 最后一块是满的
= Cons([1,2], Cons([3,4], Nil))注意 Nil 的一物二用：输入端的 Nil 是"没有元素可切了"；case Nil => Nil 返回的 Nil 类型是 list<list<T>>，是输出端那串块列表的收口。输入见底的那一刻，恰好为输出钉上末节。
义务即命题：lemma 从哪来
命题不是猜出来的，是机器报给你的。 先写 decreases length(l)，跑。红字背后的证明义务精确到一行——递归调用点上需要 length(drop(n,l)) < length(l)，且上下文已知 l != Nil、n >= 1。这句就是命题，一字不多。
还有个笨而准的招：把 assert length(drop(n,l)) < length(l); 插进函数体。它证不出，但红得很有指向性——assert 的内容原样抬出去，就是 lemma 的 ensures。
判断引理够不够，标准不是感觉，是能否封住那条义务。护栏由反例逼出：不加 requires，取 l = Nil 就是 0 < 0，假命题，Dafny 直接拒收。
"趋近 Nil"不是 lemma 的活。 lemma 只交一步的事实（切一刀，变短）；"一直变短不会永远变下去"是 nat 良基性的活，decreases 机制自带。终止检查恰恰不展开：每个递归调用只查一次"这一步降了没有"，无穷的部分由良基性兜底。
四件事各归其位：命题由红字口述，护栏由反例逼出，强弱由归纳假设的需要定夺，收敛由 decreases 白送。 没有一件靠猜。
更强的引理反而好证
对调用者：够用就好，越弱越通用。对归纳证明本身：更强的命题意味着更肥的归纳假设，反而好证——等式在归纳步里严丝合缝，不等式有时接不上力。
requires 是门票，所有调用者都要买，包括证明体里的自己。两条车道，选一条走到底，别各撕一半缝在一起：
// 车道A・等式版：天生全定义，不需要任何 requires，自我调用畅通无阻
lemma length_drop<T>(n: nat, l: list<T>)
ensures length(drop(n,l)) == if n >= length(l) then 0 else length(l) - n
{
match l // drop match 谁，我 match 谁
case Nil => // drop 的 Nil 分支不递归，我也不递归，自动
case Cons(hd, tl) =>
if n > 0 { // drop 在 n>0 时才递归，我也只在这时
length_drop(n - 1, tl); // ★ 实参照抄 drop(n-1, t)，这就是归纳假设
}
}
// 车道B・不等式版：requires 留着，归纳步开门前要替下一层验票
lemma drop_shrinks<T>(n: nat, l: list<T>)
requires 0 < n && l != Nil
ensures length(drop(n, l)) < length(l)
{
match l
case Nil => // 被 requires 排除，留空
case Cons(hd, tl) =>
if 0 < n - 1 && tl != Nil { // 调用自己也得过自己的 requires
drop_shrinks(n - 1, tl);
}
}无前置条件的引理，归纳起来最省心。 写完把车道A的体子换成空 {} 再跑——照样绿：Dafny 的自动归纳替简单引理代劳的，正是上面这套动作。它代劳不了的场合，你已经会自己上了。
红字读法：先看署名
署名 Parser 的红，是语法都没解析过去，压根没轮到验证器。Parser 错误永远优先修——语法不通，后面所有验证类报错都是废纸；两条红同时出现，往往不是两个病，是一个病和它的影子。
典型病例：decreases 塞进函数体。病根是位置——decreases 和 requires、ensures 是一族的规格从句，住在函数头和 { 之间；函数体里只住表达式。
function chunks<T>(n : nat, l:list<T>) : list<list<T>>
requires 0 < n
decreases length(l) // ← 户口在这儿，与 requires 并排
{
match l
case Nil => Nil
case _ =>
length_drop(n, l);
Cons(take(n,l), chunks(n, drop(n,l)))
}修完 Parser 那条消失，termination 那条留下——这回它是正主：length(drop(n,l)) < length(l) 机器自己够不着。当"变小"本身需要归纳才能知道时，把它证成引理，在递归调用前用"语句 ; 表达式"喂给终止检查。
归纳证明，抄被证函数的作业
证明体的形状 = 函数体的形状：它 match 什么你就 match 什么，它 if 什么你就 if 什么；自我调用的实参，一字不差照抄函数递归调用的实参。drop 的递归步是 (n-1, t)，引理的自我调用就必须是 length_drop(n-1, tl)。
为什么必须？定义只给一步等式 drop(n, Cons(h,t)) == drop(n-1, t)，这是连接"关于 (n,l) 的目标"和"关于 (n-1,tl) 的假设"的唯一桥墩。调用自己 = 把归纳假设作为既成事实摆进上下文；验证器把定义展开一步，一步等式加归纳假设，目标合龙。归纳假设是无穷展开的替身——你只交一步，剩下的账由更小的案子递归地兜着。
典型翻车：对函数的输出做归纳，如 length_drop(n, drop(n-1, l))——它给的假设是关于一个嵌套怪物的，目标里根本没有这个东西，桥修到了河中央。"传更小的参数"没错，但"更小"必须是函数自己走向的那个更小。
表达式的国度，语句的国度
函数体是表达式的国度：if c then e1 else e2 是产出值的式子，没有分号，没有花括号块。lemma 体是语句的国度：if c { 语句 } else { 语句 }，能住的只有语句——assert、引理调用、if、match、calc、var。光秃秃的布尔表达式不是语句，得穿上 assert 才算话。
lemma 是证明不是计算，没有东西可以返回——它的"产出"就是 ensures 那句话本身。不需要帮忙的分支就留空：空白的意思是"这一步展开一次定义机器自己行"，你只在机器够不着的地方递话，别处沉默即金。
分号的判法不用背位置：分号属于语句，不属于花括号，像句号属于句子。 花括号只是墙，墙内每句话各带各的句号，墙本身前后都不沾分号。语句要分号，块不要。
两条杂账顺手记下：ensures 描述的是外面调用时的参数，函数肚子里的中间变量（如体内的 n-1）不许漏到规格上——漏了就是把 n = 1 时的假话写进合同。引理的 decreases 跟着它模仿的函数走，默认猜测就够，多写是画蛇添足。
ensures 抄结局，不抄过程
ensures 的形状可以抄，但抄的不是函数的代码，是函数行为的结局清单：drop 只有两种下场（掏空 / 剩 length(l) - n），闭式规格就分两种情况作答。
照"抄函数体"的字面去做，迟早写出把定义复读一遍的恒真式——机器秒绿，但对调用者毫无新信息。规格的价值恰恰在于它说了一句定义没有直接说、要靠归纳才能兑现的话。"抄结局，不抄过程"，六个字记死。
函数体、证明体、规格常常共用同一副 case 骨架，根源同一个：数据和行为长什么形状，关于它的一切话语就长什么形状。 于是规则收束为一句：函数在哪里递归，你就在哪里开门引用归纳假设；函数在哪里一步到底，你就在哪里闭嘴。（那扇 if n > 0 的门必须写：一来 drop 只在 n > 0 时才递归，二来它挡住 n-1 在 n == 0 时下溢。）
这门学科到底要你做什么
一句话：把"我声称某件事成立"写成机器能检查的形式，然后让机器点头。 交付物是一份全绿的文件，外加一件绿保证不了的事——你写的命题确实是题目要的那句话。失分只有两种死法：命题翻译错了，或者证明欠着账。
把 SMT 求解器想成一个不知疲倦但毫无想象力的审计员：它会展开有限步定义、做线性算术、按构造子分案；它永远不会做的只有一样——出主意。归纳是主意，调引理是主意，交 witness 是主意。主意是你的活，验账是它的活。
判断准则只有一问：这个主张，靠"展开定义几步"够不够得着？ 具体数值、几步可见的性质、结构递归的终止——免费。关于递归函数对所有输入的性质——归纳，你写；结论要用另一个已证事实——lemma 调用，你写；中间隔着审计员看不见的一跳——assert 搭桥，你写。
实操上根本不用事前判断：命题写好，证明体先放空 {}，跑。 绿了白捡；红了，红字就是账单，写着卡在哪一步。所谓"会证明"，不是未卜先知，是跟审计员讨价还价的熟练度。（讲师承诺过：机器证不动的怪东西不会拿来考——考场上每一道红都付得起。）
为什么拿列表开刀
有些代码错不起。 测试的本质是抽查——Dijkstra 的老话：测试只能证明 bug 存在，永远不能证明 bug 不存在。飞控、起搏器、密码库、内核、智能合约需要全查：对所有输入数学地成立。seL4 内核整个被证明过，CompCert 编译器被证明不会编错，AWS 用形式化方法验证网络配置。
列表是最小的带无穷性的结构——定义两行，实例无穷，归纳、终止、引理这套器械一样不缺。拿它练如解剖课用青蛙：目标从来不是青蛙，是刀法。 将来面对的是红黑树的不变量、并发协议的状态机、内存模型——同一套刀法。
这门课真正教的是三问：写 requires 是被迫回答"我到底假设了什么"，写 ensures 是"我到底承诺了什么"，写 decreases 是"这为什么会结束"。三问带到任何语言、任何系统设计里都成立。 顺带，证明在这里第一次成为可迭代、可调试的活动：两秒机器裁决，错了改，改了再跑。
归纳与递归：同构
不是同一个东西，也不是巧合的相似——同一个结构的两面。递归是造东西的方式，方向是拆：从大拆到小，拆到 Nil 见底。归纳是证东西的方式，方向是垒：基例加归纳步，垒遍所有列表。
datatype list<T> = Nil | Cons(T, list<T>) 一行同时规定三件事：值怎么造、函数怎么写、性质怎么证。 对应精确到逐条：递归的基例 ↔ 归纳的基例；递归调用 ↔ 归纳假设；终止性（拆有限步必见底）↔ 合法性（垒有限步够得着任何列表）。
在 Dafny 里这不是比喻，是写法：
lemma P_holds<T>(l: list<T>)
ensures P(l)
{
match l
case Nil => // 基例：通常 Dafny 自动搞定
case Cons(h, t) =>
P_holds(t); // ← 调用自己 = "归纳假设成立"
}为什么允许引用自己？和函数递归同一个理由——lemma 也有 decreases，t 比 l 小，小案子先结，大案子引用小案子，不算循环论证。写归纳证明 = 照着函数的递归结构，把证明体也递归地写一遍。
六句总结
- 当"变小"本身需要归纳才能知道时，把它证成引理，在递归调用前用"语句;表达式"喂给终止检查。
- 语句以分号收尾，块不用。
- ensures 抄函数的结局，不抄过程。
- 命题带"对所有"、且展开有限步够不着时，才需要引理和归纳。
- lemma 体抄函数体的骨架，只在函数递归处调用自己（实参照抄），其余分支留白。
- 规格永远说外面那次调用的参数，体内的中间变量不许外漏。
附：符号贴着它修饰的东西；写下来的文字，要经得起作者不在场的阅读。
通用五步循环
每个 .dfy 文件都走这五步：
- 只看签名，先造句。 把函数或 lemma 翻译成一句完整中文："对所有的……，只要……，就有……"。造不出来，说明题目没懂，回去看定义。
- 合上原文，自己写。 卡住的位置就是真正的缺口——看答案里对应的那一行，只看那一行，继续写。
dafny verify跑绿。 不许目测正确，机器说了算。- 故意弄坏。 删 decreases、删 assert、注释掉 lemma 调用，看红字长什么脸，再修回来。
- 口头收账。 一句话说出"这个文件教了我什么招"。说不出来，重走一遍。