分析基礎機器證明系統(tǒng)

目錄
前言
致謝
符號匯集
第1章引言1
1.1概述1
1.1.1證明輔助工具Coq1
1.1.2形式化數(shù)學2
1.1.3分析基礎3
1.1.4第三代微積分5
1.1.5本書結構安排7
1.2基本Coq指令清單及邏輯預備知識7
1.3集合與映射的一些基本概念13
第2章分析基礎的形式化系統(tǒng)實現(xiàn)19
2.1自然數(shù)19
2.1.1公理19
2.1.2加法22
2.1.3序26
2.1.4乘法36
2.1.5補充材料:有限數(shù)的定義及性質40
2.2分數(shù)44
2.2.1定義和等價44
2.2.2序46
2.2.3加法51
2.2.4乘法56
2.2.5有理數(shù)和整數(shù)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實數(shù)118
2.4.1定義118
2.4.2序.119
2.4.3加法125
2.4.4乘法139
2.4.5Dedekind基本定理146
2.4.6補充材料:實數(shù)運算的一些性質151
2.4.7補充材料:實數(shù)序列的一些性質166
2.5復數(shù)175
2.5.1定義175
2.5.2加法177
2.5.3乘法181
2.5.4減法186
2.5.5除法188
2.5.6共軛復數(shù)193
2.5.7絕對值195
2.5.8和與積200
2.5.9冪237
2.5.10將實數(shù)編排在復數(shù)系統(tǒng)中245
第3章實數(shù)完備性等價命題的機器證明251
3.1確界存在定理251
3.1.1用Dedekind基本定理證明確界存在定理251
3.1.2用確界存在定理證明Dedekind基本定理254
3.2單調有界定理255
3.3閉區(qū)間套定理256
3.4有限覆蓋定理258
3.5聚點原理264
3.6列緊性定理268
3.7Cauchy收斂準則272
3.8用Cauchy收斂準則證明Dedekind基本定理275
第4章閉區(qū)間上連續(xù)函數(shù)性質的機器證明283
4.1基本定義283
4.2有界性定理290
4.3*值定理293
4.4介值定理295
4.5一致連續(xù)性定理300
第5章第三代微積分的形式化實現(xiàn)306
5.1預備知識307
5.1.1基本定義307
5.1.2一些引理308
5.2導數(shù)和定積分的初等定義315
5.3積分與微分的新視角324
5.4微積分系統(tǒng)的基本定理346
第6章總結與注記370
參考文獻375
附錄Coq指令說明386
A.1Coq專用術語386
A.2Coq證明指令387
A.3集成策略390
索引393
表索引
表1.1書中涉及常用Coq指令簡表8
表1.2書中涉及常用Coq術語的基本含義13
表6.1分析基礎形式化系統(tǒng)代碼量統(tǒng)計370
表6.2實數(shù)完備性及其等價命題形式系統(tǒng)化代碼量統(tǒng)計371
表6.3閉區(qū)間上連續(xù)函數(shù)性質形式化系統(tǒng)代碼量統(tǒng)計371
表6.4第三代微積分形式化系統(tǒng)代碼量統(tǒng)計371
圖索引
圖1.1Landau《分析基礎》的德文-英文版和中文版封面4
圖3.1實數(shù)完備性定理的等價性251
圖3.2實數(shù)的定義與完備性總覽圖282
圖6.1Dedekind基本定理的證明截圖372
圖6.2計算機軟件著作權登記證書373