分析基础机器证明系统

本书利用交互式定理证明工具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 证明辅助工具Coq
1.1.2 形式化数学
1.1.3 分析基础
1.1.4 第三代微积分
1.1.5 本书结构安排
1.2 基本Coq指令清单及逻辑预备知识
1.3 集合与映射的一些基本概念
第2章 分析基础的形式化系统实现
2.1 自然数
2.1.1 公理
2.1.2 加法
2.1.3 序
2.1.4 乘法
2.1.5 补充材料：有限数的定义及性质
2.2 分数
2.2.1 定义和等价
2.2.2 序
2.2.3 加法
2.2.4 乘法
2.2.5 有理数和整数
2.3 分割
2.3.1 定义
2.3.2 序
2.3.3 加法
2.3.4 乘法
2.3.5 有理分割和整分割
2.4 实数
2.4.1 定义
2.4.2 序
2.4.3 加法
2.4.4 乘法
2.4.5 Dedekind基本定理
2.4.6 补充材料：实数运算的一些性质
2.4.7 补充材料：实数序列的一些性质
2.5 复数
2.5.1 定义
2.5.2 加法
2.5.3 乘法
2.5.4 减法
2.5.5 除法
2.5.6 共轭复数
2.5.7 绝对值
2.5.8 和与积
2.5.9 幂
2.5.10 将实数编排在复数系统中
第3章 实数完备性等价命题的机器证明
3.1 确界存在定理
3.1.1 用Dedekind基本定理证明确界存在定理
3.1.2 用确界存在定理证明Dedekind基本定理
3.2 单调有界定理
3.3 闭区间套定理
3.4 有限覆盖定理
3.5 聚点原理
3.6 列紧性定理
3.7 Cauchy收敛准则
3.8 用Cauchy收敛准则证明Dedekind基本定理
第4章 闭区间上连续函数性质的机器证明
4.1 基本定义
4.2 有界性定理
4.3 最值定理
4.4 介值定理
4.5 一致连续性定理
第5章 第三代微积分的形式化实现
5.1 预备知识
5.1.1 基本定义
5.1.2 一些引理
5.2 导数和定积分的初等定义
5.3 积分与微分的新视角
5.4 微积分系统的基本定理
第6章 总结与注记
参考文献
附录 Coq指令说明
A.1 Coq专用术语
A.2 Coq证明指令
A.3 集成策略
索引