内容简介：
本书利用交互式定理证明工具Coq, 在朴素集合论的基础上, 从Peano五条公设出发, 完整实现Landau著名的《分析基础》中实数理论的形式化系统,包括对该专著中全部5个公设、73条定义和301个定理的Coq 描述, 其中依次构造了自然数、分数、分割、实数和复数, 并建立了Dedekind实数完备性定理, 从而迅速而自然地给出数学分析的坚实基础. 在分析基础形式化系统下, 进而给出Dedekind实数完备性定理与它的几个著名等价命题间等价性的机器证明, 这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等, 基于实数的完备性定理, 作为应用, 进一步给出闭区间上连续函数的重要性质——有界性定理、最值定理、介值定理、一致连续性定理——的机器证明. 另外, 还给出林群和张景中提出的第三代微积分——即不用极限的微积分——的形式化系统实现. 在我们开发的系统中, 全部定理无例外地给出Coq的机器证明代码, 所有形式化过程已被Coq验证, 并在计算机上运行通过, 体现了基于Coq 的数学定理机器证明具有可读性和交互性的特点, 其证明过程规范、严谨、可靠. 该系统可方便地应用于数学分析相关理论的形式化构建.
本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或研究生教材, 也可供从事人工智能相关科研工作者参考.
目录：
“数学机械化丛书”前言
前言
致谢
符号汇集
表索引
图索引
第1章 引言1
1.1概述1
1.1.1证明辅助工具Coq 1
1.1.2形式化数学2
1.1.3分析基础3
1.1.4第三代微积分5
1.1.5本书结构安排7
1.2基本Coq指令清单及逻辑预备知识7
1.3集合与映射的一些基本概念13
第2章 分析基础的形式化系统实现19
2.1自然数19
2.1.1公理19
2.1.2加法22
2.1.3序26
2.1.4乘法36
2.1.5补充材料:有限数的定义及性质40
2.2分数44
2.2.1定义和等价44
2.2.2序46
2.2.3加法51
2.2.4乘法56
2.2.5有理数和整数61
2.3分割83
2.3.1定义83
2.3.2序86
2.3.3加法89
2.3.4乘法97
2.3.5有理分割和整分割106
2.4实数118
2.4.1定义118
2.4.2序.119
2.4.3加法125
2.4.4乘法139
2.4.5 Dedekind基本定理146
2.4.6补充材料:实数运算的一些性质151
2.4.7补充材料:实数序列的一些性质166
2.5复数175
2.5.1定义175
2.5.2加法177
2.5.3乘法181
2.5.4减法186
2.5.5除法188
2.5.6共轭复数193
2.5.7绝对值195
2.5.8和与积200
2.5.9幂237
2.5.10将实数编排在复数系统中245
第3章 实数完备性等价命题的机器证明251
3.1确界存在定理251
3.1.1用Dedekind基本定理证明确界存在定理251
3.1.2用确界存在定理证明Dedekind基本定理254
3.2单调有界定理255
3.3闭区间套定理256
3.4有限覆盖定理258
3.5聚点原理264
3.6列紧性定理268
3.7 Cauchy收敛准则272
3.8用Cauchy收敛准则证明Dedekind基本定理275
第4章 闭区间上连续函数性质的机器证明283
4.1基本定义283
4.2有界性定理290
4.3最值定理293
4.4介值定理295
4.5一致连续性定理300
第5章 第三代微积分的形式化实现306
5.1预备知识307
5.1.1基本定义307
5.1.2一些引理308
5.2导数和定积分的初等定义315
5.3积分与微分的新视角324
5.4微积分系统的基本定理346
第6章 总结与注记370
参考文献375
附录Coq指令说明386
A.1 Coq专用术语386
A.2 Coq证明指令387
A.3集成策略390
索引393
表索引
表1.1书中涉及常用Coq指令简表8
表1.2书中涉及常用Coq术语的基本含义13
表6.1分析基础形式化系统代码量统计370
表6.2实数完备性及其等价命题形式系统化代码量统计371
表6.3闭区间上连续函数性质形式化系统代码量统计371
表6.4第三代微积分形式化系统代码量统计371
图索引
图1.1 Landau《分析基础》的德文-英文版和中文版封面4
图3.1实数完备性定理的等价性251
图3.2实数的定义与完备性总览图282
图6.1 Dedekind基本定理的证明截图372
图6.2计算机软件著作权登记证书373
