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

图书标准信息

• 作者 [德]伯托特、[德]卡斯特兰 著；顾明 译
• 出版社 清华大学出版社
• 出版时间 2010-01
• 版次 1
• ISBN 9787302208136
• 定价 59.00元
• 装帧 平装
• 开本 16开
• 纸张 其他
• 页数 432页
• 正文语种 简体中文

【内容简介】

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

【目录】

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.2Section和局部变量
2.4计算
2.4.1替换
2.4.2归约规则
2.4.3归约序列
2.4.4可转换性
2.5类型、大类和类型空间
2.5.1Set大类
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.1Theorem和De.nition的分析比较
3.4.2证明策略有助于构造程序吗
3.5Sections和证明
3.6证明策略的结合
3.6.1泛证明策略
3.6.2证明维护问题
3.7命题逻辑的完备性
3.7.1一个完备的证明策略集
3.7.2不可证命题
3.8其他证明策略
3.8.1cut和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.4Coq系统中的相等性
4.3.5高阶类型

5常用逻辑
5.1依赖积的实用方面
5.1.1exact和assumption
5.1.2intro策略
5.1.3apply策略
5.1.4unfold策略
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.2True和False
5.5.3莱布尼兹等价
5.5.4其他一些联结词和量词
5.5.5书写非直谓定义的指导原则

6归纳数据类型
6.1非递归类型
6.1.1枚举类型
6.1.2简单的推理与计算
6.1.3elim策略
6.1.4模式匹配
6.1.5记录类型
6.1.6带变体的记录
6.2分情形推理
6.2.1case证明策略
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.2option类型
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.2auto和eauto证明策略
7.2.1证明策略库管理命令：Hint
7.2.2*eauto证明策略
7.3针对重写的自动证明策略
7.3.1autorewrite证明策略
7.3.2subst证明策略
7.4和数相关的证明策略
7.4.1ring证明策略
7.4.2omega证明策略
7.4.3.eld证明策略
7.4.4fourier证明策略
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.2constructor策略
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.7re.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.1Extraction命令
10.1.2抽取机制
10.1.3Prop、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.1CoInductive命令
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.2CoFixpoint命令
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.1bisimilar谓词
13.7.2互模拟等价的使用
13.8Park原理
13.9LTL
13.10一个实例：状态迁移系统
13.11结论

14**归纳类型基础
14.1形成规则
14.1.1归纳类型
14.1.2构造子
14.1.3归纳原理的构造
14.1.4递归子的类型
14.1.5谓词的归纳原理
14.1.6Scheme命令
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及它的库
书中的示例