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

    Coqf381是一个定理证明辅助工具，学生、研究人员和工程人员可以使用它来表达规范说明（specification），开发满足规范说明的程序。 Coq非常适合于开发那些在电信、运输、能源和银行等领域需要绝对可信的程序，这些领域中的程序需要严格地符合规范说明，需要对这些程序进行形式化的验证。在本书中，我们将看到Coq这样的定理证明辅助工具如何使这一工作变得简单。
    Coq系统不仅可以用来开发安全程序，还可以被数学家用来开发证明。Coq系统提供一种具有很强表达能力的逻辑，通常被称为高阶逻辑（higher-0rder，logic：）。证明以交互的方式进行开发，并尽可能地借助自动搜索工具的帮助。Coq的应用领域也很广泛，比如，在逻辑、自动机理论、计算语言学和算法学中都有涉及（参见111）。
    Coq系统亦可被用作一个逻辑框架。在该框架下，我们可以为新的逻辑提供公理，并基于这些逻辑来开发证明。比如，我们可以使用∞口为模态逻辑、时序逻辑、面向资源的逻辑等逻辑系统开发推理系统，也可以为命令式程序开发推理系统。计算机辅助定理证明工具是一个大家族，除Coq之外，还有很多享有盛誉的工具，那就是可以从证明中牛成可靠的程序和模块。在这一章里，我们将非形式化地介绍Coq的主要特性。严格的定义和准确的符号将在后而的章节中给出。这里，我们仅使用一些在数学或程序设计语言中常用的符号。
    1.1表达式、类型和函数
    Coq的规范说明语言Gallina可以描述程序设计语言中的常用类型和程序。
    一个标识符的类型通常由声明（declaration）和一些规则来描述.后者使用类型规则从较简单的类型出发构造复合类型，每个类型规则表达了类型的子部分同类型的整体结构之间的联系。例如，给定与集合Z相对应的整数类型z，已知常量一6的类型是整数，若声明一个类型为z的变量z，则表达式－6z也是整数类型z的。但是，给定一个bool常量true，表达式“true×－6”就不是一个合法的表达式。在Gallina语言中，除整数类型z和布尔类型 bool之外，存在各种各样的类型。我们经常会使用自然数类型nat，它是包含常数0和调用后继函数所得到的值的最小类型。

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 及它的库
书中的示例