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和Definition的分析比较 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
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.2True和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匿名递归函数（fix） 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
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 field证明策略 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 refine策略 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
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.9 LTL 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
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