分析基礎(chǔ)機(jī)器證明系統(tǒng)

目錄
前言
致謝
符號匯集
第1章引言1
1.1概述1
1.1.1證明輔助工具Coq1
1.1.2形式化數(shù)學(xué)2
1.1.3分析基礎(chǔ)3
1.1.4第三代微積分5
1.1.5本書結(jié)構(gòu)安排7
1.2基本Coq指令清單及邏輯預(yù)備知識7
1.3集合與映射的一些基本概念13
第2章分析基礎(chǔ)的形式化系統(tǒng)實(shí)現(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補(bǔ)充材料:有限數(shù)的定義及性質(zhì)40
2.2分?jǐn)?shù)44
2.2.1定義和等價(jià)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í)數(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補(bǔ)充材料:實(shí)數(shù)運(yùn)算的一些性質(zhì)151
2.4.7補(bǔ)充材料:實(shí)數(shù)序列的一些性質(zhì)166
2.5復(fù)數(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共軛復(fù)數(shù)193
2.5.7絕對值195
2.5.8和與積200
2.5.9冪237
2.5.10將實(shí)數(shù)編排在復(fù)數(shù)系統(tǒng)中245
第3章實(shí)數(shù)完備性等價(jià)命題的機(jī)器證明251
3.1確界存在定理251
3.1.1用Dedekind基本定理證明確界存在定理251
3.1.2用確界存在定理證明Dedekind基本定理254
3.2單調(diào)有界定理255
3.3閉區(qū)間套定理256
3.4有限覆蓋定理258
3.5聚點(diǎn)原理264
3.6列緊性定理268
3.7Cauchy收斂準(zhǔn)則272
3.8用Cauchy收斂準(zhǔn)則證明Dedekind基本定理275
第4章閉區(qū)間上連續(xù)函數(shù)性質(zhì)的機(jī)器證明283
4.1基本定義283
4.2有界性定理290
4.3*值定理293
4.4介值定理295
4.5一致連續(xù)性定理300
第5章第三代微積分的形式化實(shí)現(xiàn)306
5.1預(yù)備知識307
5.1.1基本定義307
5.1.2一些引理308
5.2導(dǎo)數(shù)和定積分的初等定義315
5.3積分與微分的新視角324
5.4微積分系統(tǒng)的基本定理346
第6章總結(jié)與注記370
參考文獻(xiàn)375
附錄Coq指令說明386
A.1Coq專用術(shù)語386
A.2Coq證明指令387
A.3集成策略390
索引393
表索引
表1.1書中涉及常用Coq指令簡表8
表1.2書中涉及常用Coq術(shù)語的基本含義13
表6.1分析基礎(chǔ)形式化系統(tǒng)代碼量統(tǒng)計(jì)370
表6.2實(shí)數(shù)完備性及其等價(jià)命題形式系統(tǒng)化代碼量統(tǒng)計(jì)371
表6.3閉區(qū)間上連續(xù)函數(shù)性質(zhì)形式化系統(tǒng)代碼量統(tǒng)計(jì)371
表6.4第三代微積分形式化系統(tǒng)代碼量統(tǒng)計(jì)371
圖索引
圖1.1Landau《分析基礎(chǔ)》的德文-英文版和中文版封面4
圖3.1實(shí)數(shù)完備性定理的等價(jià)性251
圖3.2實(shí)數(shù)的定義與完備性總覽圖282
圖6.1Dedekind基本定理的證明截圖372
圖6.2計(jì)算機(jī)軟件著作權(quán)登記證書373