交互式定理证明与程序开发

1 概述

1.1 表达式、类型和函数

1.2 命题和证明

1.3 命题和类型

1.4 规范说明和已验证的程序

1.5 一个排序的例子

1.5.1 归纳定义

1.5.2 “包含相同元素”的关系

1.5.3 排序程序的规范说明

1.5.4 一个辅助函数

1.5.5 排序函数主程序

1.6 学习Coq

1.7 本书内容

1.8 词法约定

2 类型和表达式

2.1 第一步

2.1.1 项、表达式和类型

2.1.2 解释辖域

2.1.3 类型检查

2.2 游戏规则

2.2.1 简单类型

2.2.2 标识符、环境、上下文

2.2.3 表达式及其类型

2.2.4 自由和约束变元；α-变换

2.3 声明和定义

2.3.1 全局声明和定义

2.3.2 Section 和局部变量

2.4 计算

2.4.1 替换

2.4.2 归约规则

2.4.3 归约序列

2.4.4 可转换性

2.5 类型、大类和类型空间

2.5.1 Set 大类

2.5.2 类型空间

2.5.3 规范说明的定义和声明

2.6 实现规范说明

3 命题和证明

3.1 最小命题逻辑

3.1.1 命题和证明

3.1.2 目标和证明策略

3.1.3 第一个目标制导的证明

3.2 类型规则和证明策略的联系

3.2.1 命题构造规则

3.2.2 推理规则和证明策略

3.3 一个交互式证明的结构

3.3.1 激活目标处理系统

3.3.2 一个交互式证明的当前阶段

3.3.3 取消操作

3.3.4 证明的正常结束

3.4 证明无关性

3.4.1 Theorem 和De.nition 的分析比较

3.4.2 证明策略有助于构造程序吗

3.5 Sections 和证明

3.6 证明策略的结合

3.6.1 泛证明策略

3.6.2 证明维护问题

3.7 命题逻辑的完备性

3.7.1 一个完备的证明策略集

3.7.2 不可证命题

3.8 其他证明策略

3.8.1 cut 和assert 策略

3.8.2 自动证明策略

3.9 一种新的抽象方式

4 依赖积

4.1 依赖类型的优点

4.1.1 对A→B 类型的扩展

4.1.2 关于绑定

4.1.3 一种新的构造

4.2 类型规则和依赖积

4.2.1 函数应用的类型规则

4.2.2 关于抽象的类型规则

4.2.3 类型推导

4.2.4 转换规则

4.2.5 依赖积和可转换性次序

4.3 * 依赖积的表达能力

4.3.1 积的构造规则

4.3.2 依赖类型

4.3.3 多态

4.3.4 Coq 系统中的相等性

4.3.5 高阶类型

5 常用逻辑

5.1 依赖积的实用方面

5.1.1 exact 和assumption

5.1.2 intro 策略

5.1.3 apply 策略

5.1.4 unfold 策略

5.2 逻辑联结词

5.2.1 引入和消去规则

5.2.2 反证法

5.2.3 否定

5.2.4 合取和析取

5.2.5 关于repeat 高阶策略

5.2.6 存在量词

5.3 等价性与重写

5.3.1 证明等式

5.3.2 使用等式：重写证明策略

5.3.3 * pattern 策略

5.3.4 * 条件重写

5.3.5 搜索用于重写的定理

5.3.6 用于等式的其他证明策略

5.4 策略总结表

5.5 *** 非直谓定义

5.5.1 警告

5.5.2 True 和False

5.5.3 莱布尼兹等价

5.5.4 其他一些联结词和量词

5.5.5 书写非直谓定义的指导原则

6 归纳数据类型

6.1 非递归类型

6.1.1 枚举类型

6.1.2 简单的推理与计算

6.1.3 elim 策略

6.1.4 模式匹配

6.1.5 记录类型

6.1.6 带变体的记录

6.2 分情形推理

6.2.1 case 证明策略

6.2.2 矛盾等式

6.2.3 单射的构造子

6.2.4 归纳类型和等式

6.2.5 * case 的使用准则

6.3 递归类型

6.3.1 一个归纳类型——自然数

6.3.2 在自然数上做归纳证明

6.3.3 递归编程

6.3.4 构造子的形态变化

6.3.5 ** 具有函数域的类型

6.3.6 在递归函数上完成证明

6.3.7 匿名递归函数（.x）

6.4 多态类型

6.4.1 多态列表

6.4.2 option 类型

6.4.3 二元组类型

6.4.4 不相交和的类型

6.5 * 依赖归纳类型

6.5.1 一阶数据做参数

6.5.2 可变依赖归纳类型

6.6 * 空类型

6.6.1 非依赖空类型

6.6.2 依赖空类型

7 证明策略和自动化证明

7.1 用于归纳类型的证明策略

7.1.1 分情况讨论和递归

7.1.2 变换

7.2 auto 和eauto 证明策略

7.2.1 证明策略库管理命令：Hint

7.2.2 * eauto 证明策略

7.3 针对重写的自动证明策略

7.3.1 autorewrite 证明策略

7.3.2 subst 证明策略

7.4 和数相关的证明策略

7.4.1 ring 证明策略

7.4.2 omega 证明策略

7.4.3 .eld 证明策略

7.4.4 fourier 证明策略

7.5 其他决策过程

7.6 ** 策略定义语言

7.6.1 策略中的变元

7.6.2 模式匹配

7.6.3 在已经定义过的策略中使用归约

8 归纳谓词

8.1 归纳属性

8.1.1 几个例子

8.1.2 归纳谓词和逻辑程序设计

8.1.3 对归纳定义的建议

8.1.4 排序列表

8.2 归纳属性和逻辑连接词

8.2.1 表示真值

8.2.2 表示矛盾式

8.2.3 表示合取

8.2.4 表示析取

8.2.5 表示存在量词

8.2.6 表示等价

8.2.7 *** 异构等式

8.2.8 一个奇特的归纳原理?

8.3 归纳特性的推理

8.3.1 结构化intros

8.3.2 constructor 策略

8.3.3 * 在归纳谓词上做归纳

8.3.4 * 对le 进行归纳

8.4 * 归纳关系和函数

8.4.1 表示阶乘函数

8.4.2 ** 表示一个语言的语义

8.4.3 ** 语义属性证明

8.5 * elim 行为的详细阐述

8.5.1 实例化变元

8.5.2 转置

9* 函数及其规范

9.1 用于规范的归纳类型

9.1.1 “子集”类型

9.1.2 嵌套的子集类型

9.1.3 有认证的不相交和

9.1.4 混合不相交和

9.2 强规范

9.2.1 良规函数

9.2.2 将函数构造为证明

9.2.3 偏函数的前置条件

9.2.4 ** 对前置条件的证明

9.2.5 ** 增强规范

9.2.6 *** 最小规范增强

9.2.7 re.ne 策略

9.3 结构递归的变种形式

9.3.1 多步结构递归

9.3.2 简化步骤

9.3.3 多参数递归函数

9.4 ** 二进制除法

9.4.1 弱规范的除法

9.4.2 良规的二进制除法

10 * 程序抽取和命令式程序设计

10.1 抽取到函数式语言程序

10.1.1 Extraction 命令

10.1.2 抽取机制

10.1.3 Prop、Set 和抽取

10.2 描述命令式程序

10.2.1 工具Why

10.2.2 *** Why 的内部工作原理

11 * 实例分析

11.1 二叉搜索树

11.1.1 数据结构

11.1.2 一个直接的存在判定方法

11.1.3 搜索树的描述

11.2 描述程序

11.2.1 查找

11.2.2 插入一个数

11.2.3 ** 删除一个数

11.3 辅助引理

11.4 规范说明的实现

11.4.1 查找判定的实现

11.4.2 插入

11.4.3 删除元素

11.5 可能的改进

11.6 另一个实例

12 * 模块系统

12.1 签名

12.2 模块

12.2.1 构造一个模块

12.2.2 一个例子：Keys

12.2.3 参数化模块（函子）

12.3 可判定序关系理论

12.3.1 用函子丰富理论

12.3.2 字典序函子

12.4 一个字典模块

12.4.1 丰富了的实现

12.4.2 用函子构造字典

12.4.3 一个简单的实现

12.4.4 一个高效的实现

12.5 结论

13 ** 无穷对象和证明

13.1 余归纳类型

13.1.1 CoInductive 命令

13.1.2 余归纳类型的特殊性质

13.1.3 无限列表（流）

13.1.4 惰性列表

13.1.5 惰性二叉树

13.2 辅助余归纳类型的技术

13.2.1 构造有限对象

13.2.2 模式匹配

13.3 构造无穷对象

13.3.1 一个失败的尝试

13.3.2 CoFixpoint 命令

13.3.3 余递归函数示例

13.3.4 一些错误的定义

13.4 展开技术

13.4.1 系统性分解

13.4.2 分解引理的使用

13.4.3 化简对余归函数的调用

13.5 余归纳类型上的归纳谓词

13.6 余归纳谓词

13.6.1 无穷序列谓词

13.6.2 构造无限证明

13.6.3 违反Guard 约束

13.6.4 消去技术

13.7 互模拟等价

13.7.1 bisimilar 谓词

13.7.2 互模拟等价的使用

13.8 Park 原理

13.9 LTL

13.10 一个实例：状态迁移系统

13.11 结论

14 ** 归纳类型基础

14.1 形成规则

14.1.1 归纳类型

14.1.2 构造子

14.1.3 归纳原理的构造

14.1.4 递归子的类型

14.1.5 谓词的归纳原理

14.1.6 Scheme 命令

14.2 *** 模式匹配和证明上的递归

14.2.1 模式匹配的约束

14.2.2 放宽约束

14.2.3 递归

14.3 互引归纳类型

14.3.1 树和森林

14.3.2 使用互引归纳证明

14.3.3 *** 树和树列表

15 * 一般递归

15.1 有界递归

15.2 ** 良基递归函数

15.2.1 良基关系

15.2.2 可访问性证明

15.2.3 整合良基关系

15.2.4 良基递归

15.2.5 递归子well_founded_induction

15.2.6 良基欧氏除法

15.2.7 嵌套递归

15.3 ** 用迭代法实现通用递归

15.3.1 与递归函数相关的泛函

15.3.2 终止性证明

15.3.3 构造具体函数

15.3.4 证明不动点方程

15.3.5 使用不动点方程

15.3.6 讨论

15.4 *** 在人为谓词上递归

15.4.1 定义人为谓词

15.4.2 逆转定理

15.4.3 定义函数

15.4.4 证明该函数的特性

16 * 自反证明

16.1 引言

16.2 直接的计算证明

16.3 ** 借助代数计算的证明

16.3.1 基于结合律的证明

16.3.2 把类型和操作符通用化

16.3.3 *** 交换律：变量排序

16.4 结论

附录

插入排序

参考文献

索引

Coq 及它的库

书中的示例

《交互式定理证明与程序开发：Coq归纳构造演算的艺术》的主要目标是从实践的角度来理解Coq系统及其基本理论，即归纳构造演算。这《交互式定理证明与程序开发：Coq归纳构造演算的艺术》给出了大量的例子，所有例子都町以在计算机上执行。从《交互式定理证明与程序开发：Coq归纳构造演算的艺术》配套网站可以下载并执行所有证明的例子，而且还提供了书中200个练习的答案。 Coq是一个用于验证定理的证明是否正确的计算机工具。在推理和编程方面，Coq的语言都拥有足够强大的能力和表达能力，可以构造简单的项，执行简单的证明，直到建立完整的理论，学习复杂的算法。 这《交互式定理证明与程序开发：Coq归纳构造演算的艺术》是·本很有价值的教材，它为初学者提供基础训练，为有经验的人提供必要的专业知识，帮助学习者开发有实用价值的数学证明。

过程感知的信息系统
软件测试：跨越整个软件开发生命周期
软件测试实践：成为一个高效能的测试专家
机器视觉算法与应用
数值方法（c++描述）
web技术
UML安全系统开发