1. 介紹

1.1 計算機與定理證明

形式驗證包括使用邏輯和計算方法， 以此建立以精確數學術語表達的論述。這些論述可以包括普通的數學定理，以及硬體或軟體，網路協議以及機械和混合系統滿足其規範的要求的論述。實際上，在驗證一個數學定理和驗證系統的正確性之間沒有明顯的區別：形式驗證需要用數學術語描述硬體和軟體系統，此時建立關於它們正確性的宣告成為一種定理證明形式。相反，數學定理的證明可能需要冗長的計算，在這種情況下，驗證定理的真實性需要驗證計算是否完成它應該做的事情。

支援數學論述的黃金標準是提供證明，二十世紀的邏輯發展表明大多數（如果不是全部）傳統證明方法可以在許多基礎系統中的任何一箇中簡化為一小組公理和規則。 通過這種減少，計算機可以通過兩種方式幫助建立論述：它可以幫助首先找到證明，並且可以幫助驗證論述的證明是正確的。

自動定理證明側重於“發現”方面。 求解型定理證明，表格型定理證明，快速可滿足性求解等提供了在命題邏輯和一階邏輯中建立公式有效性的方法。 其他系統為特定語言和域提供搜尋過程和決策過程，例如整數或實數上的線性或非線性表示式。 像SMT ("satisfiability modulo theories") 這樣的架構（“可滿足性模數理論”）將領域一般搜尋方法與特定領域的程式相結合。 計算機代數系統和專用數學軟體包提供了執行數學計算，建立數學界限或查詢數學物件的手段。 計算也可以被視為證明，這些系統也有助於建立數學論述。

自動推理系統追求功率和效率，通常以保證穩健性為代價。 這樣的系統可能存在缺陷，並且可能難以確保它們提供的結果是正確的。 相反，互動式定理證明側重於定理證明的“驗證”方面，要求在合適的公理基礎中證明支援每一個主張。 這就設定了一個非常高的標準：每個推理規則和計算的每一步都必須通過訴諸先前的定義和定理來證明，一直到基本公理和規則。 事實上，大多數此類系統提供了完全精心設計的“證明物件”，可以與其他系統進行通訊並進行獨立檢查。 構建此類證明通常需要來自使用者的更多輸入和互動，但它允許我們獲得更深入和更復雜的證明。

精益定理證明者（ Lean Theorem Prover）旨在通過在支援使用者互動和構建完全指定的公理證明的框架中設定自動化工具和方法來彌合互動式和自動化定理證明之間的差距。 目標是支援複雜系統的數學推理和推理，並驗證兩個方面中的論述。

1.2   關於 Lean

精益專案( Lean project)由Leonardo de Moura於2012年在Microsoft Research Redmond推出。這是一項持續的長期努力，自動化的大部分潛力只會逐漸實現。 Lean是在Apache 2.0許可下發布的，這是一個許可的開源許可證，允許其他人自由使用和擴充套件程式碼和數學庫。

目前有兩種使用精益(Lean)的方法。 第一種是從網上執行它：一個Javascript版本的Lean，一個標準的定義和定理庫，一個編輯器實際上下載到你的瀏覽器並在那裡執行。 這為開始試驗系統提供了一種快捷方便的方法。

使用精益(Lean)的第二種方法是在您的計算機上本地安裝和執行它。 本機版本比Web版本快得多，並且在其他方面也更靈活。 它帶有一個Emacs模式，為編寫和除錯校樣提供強大的支援，更適合嚴肅使用。

1.3關於本書

本書旨在教您開發和驗證精益(Lean)證明。 為了做到這一點，您需要的大部分背景資訊都不是Lean特有的。 首先，我們將解釋Lean所依據的邏輯系統，一種依賴型別理論的版本，其功能足以證明幾乎任何傳統的數學定理，並且表達足以以自然的方式進行。 我們不僅將解釋如何定義數學物件並在依賴型別理論中表達數學斷言，還將解釋如何將其用作編寫證明的語言。

事實上，精益支援兩種版本的依賴型理論。 第一種是稱為誘導結構微積分[1,2]或CIC的系統的變體。 這是Lean標準庫使用的系統，也是本教程的重點。 第二版依賴型理論實現了同倫型理論的公理框架，我們將在後面的章節中討論。

因為完全詳細的公理證明是如此複雜，定理證明的挑戰是讓計算機儘可能多地填寫細節。 我們將描述在依賴型理論中支援這種情況的各種方法。 例如，我們將討論術語重寫，以及Lean自動簡化術語和表示式的自動化方法。 類似地，我們將討論精化和型別推斷的方法，它們可用於支援靈活的代數推理形式。

最後，當然，我們將討論精益特有的功能，包括與系統通訊的語言，以及精益管理複雜理論和資料的機制。

如果您在Lean的線上教程系統中閱讀本書，您將在右側看到精簡編輯器的副本，其下方有一個輸出緩衝區。 在任何時候，您都可以在編輯器中輸入內容，按“播放”按鈕，然後檢視精益的響應。 請注意，如果您願意，可以調整各種視窗的大小。

在整個文字中，您將找到如下所示的精益程式碼示例：

theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
assume Hpq : p ∧ q,
have Hp : p, from and.elim_left Hpq,
have Hq : q, from and.elim_right Hpq,
show q ∧ p, from and.intro Hq Hp

 再一次，如果你在網上看書，你會看到一個按鈕，上面寫著“自己試試”。 按下按鈕將示例複製到具有足夠周圍上下文的精益編輯器中，以使示例正確編譯，然後執行精益。 我們建議您在完成後續章節時自行執行示例並嘗試使用程式碼。

1.4致謝

本教程是在Github上維護的開放式訪問專案。 許多人為這項工作做出了貢獻，提供了更正，建議，示例和文字。 我們感謝Ulrik Buchholz，Nathan Carter，Amine Chaieb，Floris van Doorn，Anthony Hart，Sean Leather，Christopher John Mazey，Daniel Velleman和ThéoZimmerman的貢獻，我們向那些無意中遺漏了我們名字的人道歉。

參考文獻