交互式定理证明与程序开发 Coq归纳构造演算的艺术PDF电子书下载

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