1 概述
................................................................ 1
1.1 表达式、类型和函数.............................................. 1
1.2 命题和证明...................................................... 2
1.3 命题和类型...................................................... 3
1.4 规范说明和已验证的程序.......................................... 4
1.5 一个排序的例子.................................................. 4
1.5.1 归纳定义.................................................. 4
1.5.2 “包含相同元素”的关系..................................... 5
1.5.3 排序程序的规范说明........................................ 5
1.5.4 一个辅助函数.............................................. 6
1.5.5 排序函数主程序............................................ 6
1.6 学习Coq ........................................................ 7
1.7 本书内容........................................................ 8
1.8 词法约定........................................................ 9
2 类型和表达式
....................................................... 11
2.1 第一步.......................................................... 11
2.1.1 项、表达式和类型.......................................... 11
2.1.2 解释辖域.................................................. 12
2.1.3 类型检查.................................................. 13
2.2 游戏规则........................................................ 15
2.2.1 简单类型.................................................. 15
2.2.2 标识符、环境、上下文....................................... 16
2.2.3 表达式及其类型............................................ 17
2.2.4 自由和约束变元；α-变换.................................... 24
2.3 声明和定义...................................................... 25
2.3.1 全局声明和定义............................................ 25
2.3.2 Section 和局部变量......................................... 26
2.4 计算............................................................ 29
2.4.1 替换...................................................... 30
2.4.2 归约规则.................................................. 30
2.4.3 归约序列.................................................. 32
2.4.4 可转换性.................................................. 32
2.5 类型、大类和类型空间............................................ 32
2.5.1 Set 大类.................................................. 33
2.5.2 类型空间.................................................. 34
2.5.3 规范说明的定义和声明...................................... 35
2.6 实现规范说明.................................................... 36
3 命题和证明
......................................................... 39
3.1 最小命题逻辑.................................................... 41
3.1.1 命题和证明................................................ 41
3.1.2 目标和证明策略............................................ 42
3.1.3 第一个目标制导的证明...................................... 42
3.2 类型规则和证明策略的联系........................................ 46
3.2.1 命题构造规则.............................................. 46
3.2.2 推理规则和证明策略........................................ 47
3.3 一个交互式证明的结构............................................ 51
3.3.1 激活目标处理系统.......................................... 51
3.3.2 一个交互式证明的当前阶段.................................. 52
3.3.3 取消操作.................................................. 52
3.3.4 证明的正常结束............................................ 52
3.4 证明无关性...................................................... 53
3.4.1 Theorem 和De.nition 的分析比较............................ 53
3.4.2 证明策略有助于构造程序吗.................................. 54
3.5 Sections 和证明.................................................. 55
3.6 证明策略的结合.................................................. 56
3.6.1 泛证明策略................................................ 56
3.6.2 证明维护问题.............................................. 59
3.7 命题逻辑的完备性................................................ 61
3.7.1 一个完备的证明策略集...................................... 61
3.7.2 不可证命题................................................ 62
3.8 其他证明策略.................................................... 62
3.8.1 cut 和assert 策略........................................... 62
3.8.2 自动证明策略.............................................. 64
3.9 一种新的抽象方式................................................ 65
4 依赖积
.............................................................. 67
4.1 依赖类型的优点.................................................. 67
4.1.1 对A→B 类型的扩展........................................ 68
4.1.2 关于绑定.................................................. 71
目录XIII
4.1.3 一种新的构造.............................................. 72
4.2 类型规则和依赖积................................................ 74
4.2.1 函数应用的类型规则........................................ 74
4.2.2 关于抽象的类型规则........................................ 77
4.2.3 类型推导.................................................. 80
4.2.4 转换规则.................................................. 83
4.2.5 依赖积和可转换性次序...................................... 83
4.3 * 依赖积的表达能力.............................................. 83
4.3.1 积的构造规则.............................................. 84
4.3.2 依赖类型.................................................. 84
4.3.3 多态...................................................... 86
4.3.4 Coq 系统中的相等性........................................ 90
4.3.5 高阶类型.................................................. 91
5 常用逻辑
............................................................ 95
5.1 依赖积的实用方面................................................ 95
5.1.1 exact 和assumption......................................... 95
5.1.2 intro 策略................................................. 96
5.1.3 apply 策略................................................. 98
5.1.4 unfold 策略................................................ 104
5.2 逻辑联结词...................................................... 105
5.2.1 引入和消去规则............................................ 106
5.2.2 反证法.................................................... 107
5.2.3 否定...................................................... 108
5.2.4 合取和析取................................................ 110
5.2.5 关于repeat 高阶策略........................................ 112
5.2.6 存在量词.................................................. 112
5.3 等价性与重写.................................................... 113
5.3.1 证明等式.................................................. 113
5.3.2 使用等式：重写证明策略.................................... 114
5.3.3 * pattern 策略............................................. 116
5.3.4 * 条件重写................................................ 117
5.3.5 搜索用于重写的定理........................................ 118
5.3.6 用于等式的其他证明策略.................................... 118
5.4 策略总结表...................................................... 119
5.5 *** 非直谓定义.................................................. 119
5.5.1 警告...................................................... 119
5.5.2 True 和False............................................... 119
5.5.3 莱布尼兹等价.............................................. 120
5.5.4 其他一些联结词和量词...................................... 122
5.5.5 书写非直谓定义的指导原则.................................. 123
6 归纳数据类型
....................................................... 125
6.1 非递归类型...................................................... 125
6.1.1 枚举类型.................................................. 125
6.1.2 简单的推理与计算.......................................... 127
6.1.3 elim 策略.................................................. 128
6.1.4 模式匹配.................................................. 129
6.1.5 记录类型.................................................. 132
6.1.6 带变体的记录.............................................. 134
6.2 分情形推理...................................................... 135
6.2.1 case 证明策略.............................................. 135
6.2.2 矛盾等式.................................................. 137
6.2.3 单射的构造子.............................................. 140
6.2.4 归纳类型和等式............................................ 142
6.2.5 * case 的使用准则........................................... 143
6.3 递归类型........................................................ 147
6.3.1 一个归纳类型—–自然数..................................... 147
6.3.2 在自然数上做归纳证明...................................... 148
6.3.3 递归编程.................................................. 150
6.3.4 构造子的形态变化.......................................... 152
6.3.5 ** 具有函数域的类型....................................... 155
6.3.6 在递归函数上完成证明...................................... 157
6.3.7 匿名递归函数（.x）......................................... 159
6.4 多态类型........................................................ 159
6.4.1 多态列表.................................................. 160
6.4.2 option 类型................................................ 162
6.4.3 二元组类型................................................ 163
6.4.4 不相交和的类型............................................ 164
6.5 * 依赖归纳类型.................................................. 165
6.5.1 一阶数据做参数............................................ 165
6.5.2 可变依赖归纳类型.......................................... 165
6.6 * 空类型........................................................ 167
6.6.1 非依赖空类型.............................................. 167
6.6.2 依赖空类型................................................ 169
7 证明策略和自动化证明
............................................... 171
7.1 用于归纳类型的证明策略.......................................... 171
7.1.1 分情况讨论和递归.......................................... 171
目录XV
7.1.2 变换...................................................... 172
7.2 auto 和eauto 证明策略............................................ 174
7.2.1 证明策略库管理命令：Hint................................... 174
7.2.2 * eauto 证明策略........................................... 177
7.3 针对重写的自动证明策略.......................................... 177
7.3.1 autorewrite 证明策略........................................ 177
7.3.2 subst 证明策略............................................. 178
7.4 和数相关的证明策略.............................................. 179
7.4.1 ring 证明策略.............................................. 179
7.4.2 omega 证明策略............................................ 181
7.4.3 .eld 证明策略.............................................. 182
7.4.4 fourier 证明策略............................................ 182
7.5 其他决策过程.................................................... 183
7.6 ** 策略定义语言................................................. 184
7.6.1 策略中的变元.............................................. 184
7.6.2 模式匹配.................................................. 185
7.6.3 在已经定义过的策略中使用归约.............................. 191
8 归纳谓词
............................................................ 193
8.1 归纳属性........................................................ 193
8.1.1 几个例子.................................................. 193
8.1.2 归纳谓词和逻辑程序设计.................................... 195
8.1.3 对归纳定义的建议.......................................... 195
8.1.4 排序列表.................................................. 196
8.2 归纳属性和逻辑连接词............................................ 198
8.2.1 表示真值.................................................. 199
8.2.2 表示矛盾式................................................ 199
8.2.3 表示合取.................................................. 199
8.2.4 表示析取.................................................. 200
8.2.5 表示存在量词.............................................. 200
8.2.6 表示等价.................................................. 200
8.2.7 *** 异构等式............................................... 201
8.2.8 一个奇特的归纳原理? ....................................... 205
8.3 归纳特性的推理.................................................. 206
8.3.1 结构化intros ............................................... 206
8.3.2 constructor 策略............................................ 207
8.3.3 * 在归纳谓词上做归纳....................................... 207
8.3.4 * 对le 进行归纳............................................ 209
8.4 * 归纳关系和函数................................................ 213
8.4.1 表示阶乘函数.............................................. 213
8.4.2 ** 表示一个语言的语义...................................... 218
8.4.3 ** 语义属性证明............................................ 220
8.5 * elim 行为的详细阐述............................................ 223
8.5.1 实例化变元................................................ 223
8.5.2 转置...................................................... 225
9* 函数及其规范
..................................................... 231
9.1 用于规范的归纳类型.............................................. 231
9.1.1 “子集”类型.............................................. 231
9.1.2 嵌套的子集类型............................................ 233
9.1.3 有认证的不相交和.......................................... 234
9.1.4 混合不相交和.............................................. 235
9.2 强规范.......................................................... 235
9.2.1 良规函数.................................................. 236
9.2.2 将函数构造为证明.......................................... 236
9.2.3 偏函数的前置条件.......................................... 237
9.2.4 ** 对前置条件的证明....................................... 238
9.2.5 ** 增强规范............................................... 239
9.2.6 *** 最小规范增强.......................................... 240
9.2.7 re.ne 策略................................................. 243
9.3 结构递归的变种形式.............................................. 245
9.3.1 多步结构递归.............................................. 245
9.3.2 简化步骤.................................................. 249
9.3.3 多参数递归函数............................................ 250
9.4 ** 二进制除法................................................... 254
9.4.1 弱规范的除法.............................................. 254
9.4.2 良规的二进制除法.......................................... 259
10 * 程序抽取和命令式程序设计
......................................... 263
10.1 抽取到函数式语言程序............................................ 263
10.1.1 Extraction 命令............................................ 263
10.1.2 抽取机制.................................................. 264
10.1.3 Prop、Set 和抽取........................................... 272
10.2 描述命令式程序.................................................. 274
10.2.1 工具Why ................................................. 274
10.2.2 *** Why 的内部工作原理.................................... 277
目录XVII
11 * 实例分析
......................................................... 285
11.1 二叉搜索树...................................................... 285
11.1.1 数据结构.................................................. 286
11.1.2 一个直接的存在判定方法.................................... 286
11.1.3 搜索树的描述.............................................. 287
11.2 描述程序........................................................ 289
11.2.1 查找...................................................... 289
11.2.2 插入一个数................................................ 289
11.2.3 ** 删除一个数............................................. 290
11.3 辅助引理........................................................ 290
11.4 规范说明的实现.................................................. 291
11.4.1 查找判定的实现............................................ 291
11.4.2 插入...................................................... 294
11.4.3 删除元素.................................................. 298
11.5 可能的改进...................................................... 299
11.6 另一个实例...................................................... 300
12 * 模块系统
.......................................................... 301
12.1 签名............................................................ 301
12.2 模块............................................................ 303
12.2.1 构造一个模块.............................................. 304
12.2.2 一个例子：Keys ............................................ 304
12.2.3 参数化模块（函子）......................................... 307
12.3 可判定序关系理论................................................ 310
12.3.1 用函子丰富理论............................................ 311
12.3.2 字典序函子................................................ 313
12.4 一个字典模块.................................................... 315
12.4.1 丰富了的实现.............................................. 315
12.4.2 用函子构造字典............................................ 316
12.4.3 一个简单的实现............................................ 316
12.4.4 一个高效的实现............................................ 318
12.5 结论............................................................ 321
13 ** 无穷对象和证明
................................................. 323
13.1 余归纳类型...................................................... 323
13.1.1 CoInductive 命令........................................... 323
13.1.2 余归纳类型的特殊性质...................................... 323
13.1.3 无限列表（流）............................................. 324
13.1.4 惰性列表.................................................. 324
13.1.5 惰性二叉树................................................ 325
13.2 辅助余归纳类型的技术............................................ 325
13.2.1 构造有限对象.............................................. 325
13.2.2 模式匹配.................................................. 326
13.3 构造无穷对象.................................................... 327
13.3.1 一个失败的尝试............................................ 327
13.3.2 CoFixpoint 命令............................................ 328
13.3.3 余递归函数示例............................................ 329
13.3.4 一些错误的定义............................................ 331
13.4 展开技术........................................................ 332
13.4.1 系统性分解................................................ 333
13.4.2 分解引理的使用............................................ 334
13.4.3 化简对余归函数的调用...................................... 335
13.5 余归纳类型上的归纳谓词.......................................... 336
13.6 余归纳谓词...................................................... 338
13.6.1 无穷序列谓词.............................................. 338
13.6.2 构造无限证明.............................................. 338
13.6.3 违反Guard 约束............................................ 340
13.6.4 消去技术.................................................. 342
13.7 互模拟等价...................................................... 343
13.7.1 bisimilar 谓词.............................................. 344
13.7.2 互模拟等价的使用.......................................... 345
13.8 Park 原理....................................................... 346
13.9LTL............................................................ 347
13.10一个实例：状态迁移系统.......................................... 350
13.11结论............................................................ 351
14 ** 归纳类型基础
................................................... 353
14.1 形成规则........................................................ 353
14.1.1 归纳类型.................................................. 353
14.1.2 构造子.................................................... 355
14.1.3 归纳原理的构造............................................ 358
14.1.4 递归子的类型.............................................. 360
14.1.5 谓词的归纳原理............................................ 366
14.1.6 Scheme 命令............................................... 368
14.2 *** 模式匹配和证明上的递归...................................... 369
14.2.1 模式匹配的约束............................................ 369
14.2.2 放宽约束.................................................. 370
14.2.3 递归...................................................... 372
14.3 互引归纳类型.................................................... 374
目录XIX
14.3.1 树和森林.................................................. 374
14.3.2 使用互引归纳证明.......................................... 376
14.3.3 *** 树和树列表............................................ 378
15 * 一般递归
.......................................................... 381
15.1 有界递归........................................................ 381
15.2 ** 良基递归函数................................................. 384
15.2.1 良基关系.................................................. 384
15.2.2 可访问性证明.............................................. 385
15.2.3 整合良基关系.............................................. 386
15.2.4 良基递归.................................................. 387
15.2.5 递归子well_founded_induction.............................. 387
15.2.6 良基欧氏除法.............................................. 388
15.2.7 嵌套递归.................................................. 391
15.3 ** 用迭代法实现通用递归......................................... 393
15.3.1 与递归函数相关的泛函...................................... 393
15.3.2 终止性证明................................................ 394
15.3.3 构造具体函数.............................................. 397
15.3.4 证明不动点方程............................................ 397
15.3.5 使用不动点方程............................................ 399
15.3.6 讨论...................................................... 399
15.4 *** 在人为谓词上递归............................................ 400
15.4.1 定义人为谓词.............................................. 400
15.4.2 逆转定理.................................................. 401
15.4.3 定义函数.................................................. 401
15.4.4 证明该函数的特性.......................................... 402
16 * 自反证明
......................................................... 405
16.1 引言............................................................ 405
16.2 直接的计算证明.................................................. 406
16.3 ** 借助代数计算的证明........................................... 409
16.3.1 基于结合律的证明.......................................... 409
16.3.2 把类型和操作符通用化...................................... 413
16.3.3 *** 交换律：变量排序....................................... 416
16.4 结论............................................................ 419
附录
................................................................... 421 插入排序............................................................ 421
参考文献
............................................................... 427
索引
................................................................... 433
Coq 及它的库........................................................ 433
书中的示例.......................................................... 437
