《互動式定理證明與程式開發Coq歸納構造演算的藝術》是2009年出版的圖書，作者是Yves Bertot,Pierre Casteran等。
基本介紹
- 書名：互動式定理證明與程式開發：Coq歸納構造演算的藝術
- 作者：Yves Bertot,Pierre Casteran等
- ISBN：9787302208136
- 定價：59元
- 出版時間：2009年11月25日
- 裝幀：平裝
圖書簡介,目錄,
圖書簡介
Coq是一個用於驗證定理的證明是否正確的計算機工具。這些定理可能涉及到普通數學、證明理論或程式驗證。
我們的主要目標是從實踐的角度來理解Coq系統及其基本理論：歸納構造演算（theCalculusofInductiveConstructions）。因此，這本書中包含了大量的例子，所有這些例子都可以在計算機上執行。為了教學目的，一些例子解釋了錯誤或笨拙的用法以及避免這些問題的準則。我們也儘量分解對話（dialogues）以便讀者能夠通過紙筆或直接在Coq上對其進行重現。有時，我們會給出一些綜合表達式；它們乍看起來讓人生畏，但事實上也是在Coq證明輔助工具的幫助下得到的。讀者應該在試驗時對它們進行分解、修改、了解其結構，並獲得一種實際的感受。
本書有一個相關網站1，讀者可以從該網站下載並執行所有證明的例子。我們也提供了書中200個練習的答案，以備不時之需。這本書及其網站使用的工具都是2004年初發布的CoqV82。
用戶對Coq中已證明的定理的信心來自於構造演算（CalculusofInductiveConstructions）的性質。構造演算是一個形式系統。以λ演算和類型（typing）的觀點來看，它結合了邏輯中的一些最新進展。這個演算的主要性質已在此處給出，因為我們相信結合理論和實踐的知識是使用Coq全部表達能力的一條最好的路徑。
我們的主要目標是從實踐的角度來理解Coq系統及其基本理論：歸納構造演算（theCalculusofInductiveConstructions）。因此，這本書中包含了大量的例子，所有這些例子都可以在計算機上執行。為了教學目的，一些例子解釋了錯誤或笨拙的用法以及避免這些問題的準則。我們也儘量分解對話（dialogues）以便讀者能夠通過紙筆或直接在Coq上對其進行重現。有時，我們會給出一些綜合表達式；它們乍看起來讓人生畏，但事實上也是在Coq證明輔助工具的幫助下得到的。讀者應該在試驗時對它們進行分解、修改、了解其結構，並獲得一種實際的感受。
本書有一個相關網站1，讀者可以從該網站下載並執行所有證明的例子。我們也提供了書中200個練習的答案，以備不時之需。這本書及其網站使用的工具都是2004年初發布的CoqV82。
用戶對Coq中已證明的定理的信心來自於構造演算（CalculusofInductiveConstructions）的性質。構造演算是一個形式系統。以λ演算和類型（typing）的觀點來看，它結合了邏輯中的一些最新進展。這個演算的主要性質已在此處給出，因為我們相信結合理論和實踐的知識是使用Coq全部表達能力的一條最好的路徑。
目錄
窗體頂端
1概述................1
1.1表達式、類型和函式.........1
1.2命題和證明.................2
1.3命題和類型.................3
1.4規範說明和已驗證的程式.....4
1.5一個排序的例子.............4
1.5.1歸納定義.............4
1.5.2“包含相同元素”的關係5
1.5.3排序程式的規範說明...5
1.5.4一個輔助函式.........6
1.5.5排序函式主程式.......6
1.6學習Coq...................7
1.7本書內容...................8
1.8詞法約定...................9
2類型和表達式...........11
2.1第一步.....................11
2.1.1項、表達式和類型.....11
2.1.2解釋轄域.............12
2.1.3類型檢查.............13
2.2遊戲規則...................15
2.2.1簡單類型.............15
2.2.2標識符、環境、上下文..16
2.2.3表達式及其類型.......17
2.2.4自由和約束變元；α-變換...........24
2.3聲明和定義..........25
2.3.1全局聲明和定義.......25
2.3.2Section和局部變數....26
2.4計算.......................29
2.4.1替換.................30
2.4.2歸約規則.............30
2.4.3歸約序列.............32
2.4.4可轉換性.............32
2.5類型、大類和類型空間.......32
2.5.1Set大類.............33
2.5.2類型空間.............34
2.5.3規範說明的定義和聲明.35
2.6實現規範說明...............36
3命題和證明.......39
3.1最小命題邏輯........41
3.1.1命題和證明...........41
3.1.2目標和證明策略.......42
3.1.3第一個目標制導的證明.42
3.2類型規則和證明策略的聯繫...46
3.2.1命題構造規則.........46
3.2.2推理規則和證明策略...47
3.3一個互動式證明的結構.......51
3.3.1激活目標處理系統.....51
3.3.2一個互動式證明的當前階段........52
3.3.3取消操作.............52
3.3.4證明的正常結束.......52
3.4證明無關性.................53
3.4.1Theorem和De.nition的分析比較.........53
3.4.2證明策略有助於構造程式嗎...........54
3.5Sections和證明.............55
3.6證明策略的結合.............56
3.6.1泛證明策略...........56
3.6.2證明維護問題.........59
3.7命題邏輯的完備性...........61
3.7.1一個完備的證明策略集.61
3.7.2不可證命題...........62
3.8其他證明策略...............62
3.8.1cut和assert策略......62
3.8.2自動證明策略.........64
3.9一種新的抽象方式...........65
4依賴積..........67
4.1依賴類型的優點.............67
4.1.1對A→B類型的擴展...68
4.1.2關於綁定.............71
目錄XIII
4.1.3一種新的構造.........72
4.2類型規則和依賴積...........74
4.2.1函式套用的類型規則...74
4.2.2關於抽象的類型規則...77
4.2.3類型推導........80
4.2.4轉換規則........83
4.2.5依賴積和可轉換性次序..........83
4.3*依賴積的表達能力....83
4.3.1積的構造規則....84
4.3.2依賴類型........84
4.3.3多態............86
4.3.4Coq系統中的相等性............90
4.3.5高階類型........91
5常用邏輯....95
5.1依賴積的實用方面......95
5.1.1exact和assumption.............95
5.1.2intro策略.......96
5.1.3apply策略.......98
5.1.4unfold策略......104
5.2邏輯聯結詞............105
5.2.1引入和消去規則..106
5.2.2反證法..........107
5.2.3否定............108
5.2.4合取和析取......110
5.2.5關於repeat高階策略............112
5.2.6存在量詞........112
5.3等價性與重寫..........113
5.3.1證明等式........113
5.3.2使用等式：重寫證明策略........114
5.3.3*pattern策略...116
5.3.4*條件重寫......117
5.3.5搜尋用於重寫的定理............118
5.3.6用於等式的其他證明策略........118
5.4策略總結表............119
5.5***非直謂定義........119
5.5.1警告............119
5.5.2True和False.....119
5.5.3萊布尼茲等價....120
5.5.4其他一些聯結詞和量詞..........122
5.5.5書寫非直謂定義的指導原則......123
6歸納數據類型
.............125
6.1非遞歸類型............125
6.1.1枚舉類型........125
6.1.2簡單的推理與計算127
6.1.3elim策略........128
6.1.4模式匹配........129
6.1.5記錄類型........132
6.1.6帶變體的記錄....134
6.2分情形推理............135
6.2.1case證明策略....135
6.2.2矛盾等式........137
6.2.3單射的構造子....140
6.2.4歸納類型和等式..142
6.2.5*case的使用準則.143
6.3遞歸類型147
6.3.1一個歸納類型—–自然數.........147
6.3.2在自然數上做歸納證明..........148
6.3.3遞歸編程........150
6.3.4構造子的形態變化152
6.3.5**具有函式域的類型...........155
6.3.6在遞歸函式上完成證明..........157
6.3.7匿名遞歸函式（.x）.............159
6.4多態類型159
6.4.1多態列表........160
6.4.2option類型......162
6.4.3二元組類型......163
6.4.4不相交和的類型164
6.5*依賴歸納類型..165
6.5.1一階數據做參數165
6.5.2可變依賴歸納類型..165
6.6*空類型167
6.6.1非依賴空類型..167
6.6.2依賴空類型169
7證明策略和自動化證明
...171
7.1用於歸納類型的證明策略..171
7.1.1分情況討論和遞歸..171
目錄XV
7.1.2變換..172
7.2auto和eauto證明策略174
7.2.1證明策略庫管理命令：Hint...174
7.2.2*eauto證明策略...177
7.3針對重寫的自動證明策略..177
7.3.1autorewrite證明策略177
7.3.2subst證明策略.178
7.4和數相關的證明策略..179
7.4.1ring證明策略..179
7.4.2omega證明策略181
7.4.3.eld證明策略..182
7.4.4fourier證明策略182
7.5其他決策過程183
7.6**策略定義語言.184
7.6.1策略中的變元..184
7.6.2模式匹配..185
7.6.3在已經定義過的策略中使用歸約..191
8歸納謂詞
193
8.1歸納屬性193
8.1.1幾個例子..193
8.1.2歸納謂詞和邏輯程式設計195
8.1.3對歸納定義的建議..195
8.1.4排序列表..196
8.2歸納屬性和邏輯連線詞198
8.2.1表示真值..199
8.2.2表示矛盾式199
8.2.3表示合取..199
8.2.4表示析取..200
8.2.5表示存在量詞..200
8.2.6表示等價..200
8.2.7***異構等式...201
8.2.8一個奇特的歸納原理?...205
8.3歸納特性的推理..206
8.3.1結構化intros...206
8.3.2constructor策略207
8.3.3*在歸納謂詞上做歸納...207
8.3.4*對le進行歸納209
8.4*歸納關係和函式213
8.4.1表示階乘函式..213
8.4.2**表示一個語言的語義..218
8.4.3**語義屬性證明220
8.5*elim行為的詳細闡述223
8.5.1實例化變元223
8.5.2轉置..225
9*函式及其規範
.231
9.1用於規範的歸納類型..231
9.1.1“子集”類型..231
9.1.2嵌套的子集類型233
9.1.3有認證的不相交和..234
9.1.4混合不相交和..235
9.2強規範..235
9.2.1良規函式..236
9.2.2將函式構造為證明..236
9.2.3偏函式的前置條件..237
9.2.4**對前置條件的證明...238
9.2.5**增強規範...239
9.2.6***最小規範增強..240
9.2.7re.ne策略.243
9.3結構遞歸的變種形式..245
9.3.1多步結構遞歸..245
9.3.2簡化步驟..249
9.3.3多參數遞歸函式250
9.4**二進制除法...254
9.4.1弱規範的除法..254
9.4.2良規的二進制除法..259
10*程式抽取和命令式程式設計..263
10.1抽取到函式式語言程式..263
10.1.1Extraction命令..263
10.1.2抽取機制..264
10.1.3Prop、Set和抽取.272
10.2描述命令式程式..274
10.2.1工具Why.274
10.2.2***Why的內部工作原理277
11*實例分析285
11.1二叉搜尋樹285
11.1.1數據結構..286
11.1.2一個直接的存在判定方法286
11.1.3搜尋樹的描述.287
11.2描述程式..289
11.2.1查找289
11.2.2插入一個數289
11.2.3**刪除一個數290
11.3輔助引理..290
11.4規範說明的實現..291
11.4.1查找判定的實現..291
11.4.2插入294
11.4.3刪除元素..298
11.5可能的改進299
11.6另一個實例300
12*模組系統
.301
12.1簽名301
12.2模組303
12.2.1構造一個模組.304
12.2.2一個例子：Keys..304
12.2.3參數化模組（函子）..307
12.3可判定序關係理論310
12.3.1用函子豐富理論..311
12.3.2字典序函子313
12.4一個字典模組.315
12.4.1豐富了的實現.315
12.4.2用函子構造字典..316
12.4.3一個簡單的實現..316
12.4.4一個高效的實現..318
12.5結論321
13**無窮對象和證明
.323
13.1餘歸納類型323
13.1.1CoInductive命令.323
13.1.2餘歸納類型的特殊性質..323
13.1.3無限列表（流）324
13.1.4惰性列表..324
13.1.5惰性二叉樹325
13.2輔助余歸納類型的技術..325
13.2.1構造有限對象.325
13.2.2模式匹配..326
13.3構造無窮對象.327
13.3.1一個失敗的嘗試..327
13.3.2CoFixpoint命令..328
13.3.3餘遞歸函式示例..329
13.3.4一些錯誤的定義..331
13.4展開技術..332
13.4.1系統性分解333
13.4.2分解引理的使用..334
13.4.3化簡對余歸函式的調用..335
13.5餘歸納類型上的歸納謂詞336
13.6餘歸納謂詞338
13.6.1無窮序列謂詞.338
13.6.2構造無限證明.338
13.6.3違反Guard約束..340
13.6.4消去技術..342
13.7互模擬等價343
13.7.1bisimilar謂詞.344
13.7.2互模擬等價的使用345
13.8Park原理.346
13.9LTL347
13.10一個實例：狀態遷移系統350
13.11結論351
14**歸納類型基礎
353
14.1形成規則..353
14.1.1歸納類型..353
14.1.2構造子.355
14.1.3歸納原理的構造..358
14.1.4遞歸子的類型.360
14.1.5謂詞的歸納原理..366
14.1.6Scheme命令..368
14.2***模式匹配和證明上的遞歸..369
14.2.1模式匹配的約束..369
14.2.2放寬約束..370
14.2.3遞歸372
14.3互引歸納類型.374
目錄XIX
14.3.1樹和森林..374
14.3.2使用互引歸納證明376
14.3.3***樹和樹列表..378
15*一般遞歸
.381
15.1有界遞歸..381
15.2**良基遞歸函式.384
15.2.1良基關係..384
15.2.2可訪問性證明.385
15.2.3整合良基關係.386
15.2.4良基遞歸..387
15.2.5遞歸子387
15.2.6良基歐氏除法.388
15.2.7嵌套遞歸..391
15.3**用疊代法實現通用遞歸..393
15.3.1與遞歸函式相關的泛函..393
15.3.2終止性證明394
15.3.3構造具體函式.397
15.3.4證明不動點方程..397
15.3.5使用不動點方程..399
15.3.6討論399
15.4***在人為謂詞上遞歸..400
15.4.1定義人為謂詞.400
15.4.2逆轉定理..401
15.4.3定義函式..401
15.4.4證明該函式的特性402
16*自反證明
405
16.1引言405
16.2直接的計算證明..406
16.3**藉助代數計算的證明.409
16.3.1基於結合律的證明409
16.3.2把類型和操作符通用化..413
16.3.3***交換律：變數排序416
16.4結論419
附錄
.421 插入排序421
參考文獻
427
索引
.433
Coq及它的庫..433
書中的示例.437
