Lean语言数学之旅——环境配置和一些基础概念

前言

雖然數學是嚴謹的，但是承載著數學知識的自然語言並不嚴謹。

編寫計算機程序並通過編譯，就好比編寫數學證明並通過程序的檢查。使用編程語言作為數學證明的載體，就能允許引入對證明過程的形式化檢查，減少出錯的可能。Lean語言就是這樣一種能夠對數學證明進行形式化檢查的編程語言。

因為對“形式化證明”這一概念感興趣，我花了一些時間，學習了Lean語言，在這個過程中也遇到了許多困難。我想將我的學習體驗和經驗借本文分享給讀者。希望後來者能夠更順利地體會到Lean語言和數學定理形式化的有趣之處。

Lean語言難在哪裡呢？

對數學知識有一定要求： 正常來說，人們是先學會 \(1+1=2\)，然後才學習阿貝爾群；先學習微積分、概率論，然後才學習測度論。使用常見的數學工具並不需要你掌握更深層的數學知識。但做數學定理的形式化時，總需要用戶對一些更底層的理論有所了解。
一個嚴格的證明可能會很冗長： 數學理論的形式化往往是一個查找API手冊的過程，你得翻一翻Mathlib文檔，看看這個定理可能是什麼名字，是不是在Mathlib中有現成可用的證明。你編寫的形式化證明可能會比自然語言更冗長，可讀性差。

我希望能夠借這篇文章，記錄下大大小小的一些“坑”，把重要的概念記錄下來，以便後來者參考。

環境安裝

和Python、Javascript等脚本語言不同，Lean 4並沒有内置一個交互式的REPL（Read-Eval-Print Loop）程序。官方推薦使用VSCode等編輯器來交互式地編寫Lean 4程序。推薦讀者閱讀 Get started with Lean，根據文檔配置好環境。

Note

如果生活在中國大陸，你可能需要先配置好代理地址，才能安裝Lean。例如，

export http_proxy=127.0.0.1:7890
export https_proxy=127.0.0.1:7890
# 請根據你的具體代理設置完成👆以上配置。

然後執行

bash -c 'curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:stable || (echo && read -n 1 -s -r -p "Install failed, press ENTER to continue...")'

如果順利的話，該代碼將會下載安裝elan和lean程序，把它們放在 ~/.elan/bin。你可能需要重新啓動shell，或者關閉重連VSCode來使用Lean。

執行以下命令

lean --version

如果你看到程序打印了Lean的版本，説明Lean的安裝成功了。如果elan下載的lean不是你需要的版本，你可以執行

elan toolchain install leanprover/lean4:v4.15.0

這裏假設4.15.0是你想要的版本。

elan default leanprover/lean4:v4.15.0

執行上面這條語句可以將指定的版本設置為默認。

#eval Lean.versionString  -- 請檢查你的Lean版本，看看是否和預期的一致。

#eval "Hello, World!"     -- 像這樣處於兩條橫桿右邊的是行內注釋

👆這就是Lean語言的Hello world程序。將它保存在一個以 .lean 為後綴的文本文件中，如果環境配置正常，你會在VsCode的Lean Infoview頁面中看到輸出。

在Lean中，-- 符號右側的文本是行內注釋；成對的 /- 和 -/ 符號包裹住的是多行注釋。

Note

你已經把環境搭好了。現在你也許可以多搜集和大概瀏覽一些參考資料。我推薦：

Theorem Proving in Lean：這本書比較適合那些喜歡在使用電器之前，完整地將説明書過一遍的人。
Mathematics in Lean：適合那些希望立即能將Lean用於數學問題的人。遺憾的是這本書現在還難稱完整，無法完全覆蓋全部數學概念。

自動證明策略

雖然Lean也可以作為通用編程語言來使用，但其核心功能和設計目標主要還是作為數學領域的自動證明器。

下面的例子展示了自動證明器的工作。

example : 1 + 1 = 2 := by simp  -- 證明了1 + 1 = 2

在上面的例子中，simp 是Lean的自動證明策略，能輔助我們完成一些簡單證明。

除了使用自動證明器，我們也可以顯式地引用現有的命題來構造證明。例如：

example : 1 = 1 := rfl -- 引用`rfl`命題

這裡我們引用了 rfl，即自反律。自反律表明任何值都於自身相等。

在深入介紹自動證明技巧之前，我們先認識一下Lean語言中的一些基礎概念。

基礎類型

在類型理論中，每個表達式都有對應的類型（type）。

Lean的 Nat 類型是一個具有無限精度的無符號整數類型。當你在Lean中寫下一個正整數但不指定類型時，Nat 是默認類型。

#eval 1 - 2  -- 0
#check 1 - 2 -- Nat

在上面的代碼中，#eval 指令用於求值，而 #check 指令檢查值的類型。注意當計算 1 - 2 時，因為使用的是 Nat 類型，所以返回值會被截斷為 0。

Nat 類型能存儲任意大的自然數：

-- 就算是這麼大的一個數也能正常存儲，這是Lean語言區別於Python、C等通用編程語言的一點。
#eval (9876543210987654321098765432109876543210 : Nat)

Nat 也可以寫成 ℕ，用 \N 即可在受支持的編輯器中打出 ℕ 符號。

#check Nat
-- 在文件開頭使用import Mathlib.Data.Nat.Defs後，你便能使用ℕ代表Nat。
-- #check ℕ

Lean也提供了 Int 類型，表示整數。與 Nat 相同，Int 類型同樣是無限精度，無溢出的。

#eval -1     -- -1
#check -1    -- Int
#eval (1 - 2 : Int)
#check (1 - 2 : Int)
#eval (9876543210987654321098765432109876543210 : Int)

類似C、Python等編程語言，Lean作為一種通用編程語言，當然也提供了有限精度的整形、浮點型。

#check (255 : UInt32)
#check (-255 : Int32)
#check (0.5 : Float)

（意外的是，作為常見的基礎類型，Int32在我編寫本文時前幾個月才作為新功能進入Lean 4😂 可見Lean 4距離成熟的通用編程語言還有距離。）

Lean也提供了 Bool 類型，表示布爾值。

#check (False : Bool)

類型的組合

新類型可以由舊類型組合而來。例如設 a 和 b 為舊類型，那麽可以構造類型 a -> b 或者 a → b 來表示一個從 a 映射到 b 的函數，a × b 表示由 a 中的元素和 b 中的元素構成的二元組，這也被稱爲笛卡爾積（Cartesian product）。笛卡爾積也可以通過 Prod 函數得到：

#check Prod Nat Nat

Lean允許使用Unicode字符。可以通過輸入 \to 或 \r 得到 →，通過輸入 \a \b \g 得到 α β γ，通過輸入 \times 得到 ×。

section
  variable (a b c α β γ : Nat)
  -- 自然數到自然數的映射
  #check Nat → Nat
  -- 兩種笛卡爾積的表示方式
  #check (Nat × Nat)
  #check Prod Nat Nat
end

上面的代碼中，section 和 end 的使用是為了限制variable的範圍。在section結束後，我們就不能再使用 a b c α β γ 等變量了。

函數的類型

以 x 為輸入的函數 f 記爲 f x，而不是 f(x)。函數的類型形如 Nat -> Nat。

舉個例子：自然數加法函數 Nat.add 的類型為 Nat -> Nat -> Nat，其中的箭頭是右結合的，因此該類型等同於 Nat -> (Nat -> Nat)。

#eval Nat.add 1 1
#check Nat.add

結合性

結合性（Associativity）是運算符的一個屬性。右結合説明同樣的運算符連續出現時，應該將運算符的右側視為一個整體。

Nat.add 的類型為 Nat -> (Nat -> Nat)，這説明 Nat.add 函數可以視爲輸入一個自然數，返回一個函數，這個函數將輸入的自然數與先前那個自然數相加然後返回。這表明我們可將部分參數應用於一個函數，得到一個新函數，例如 Nat.add 3 具有類型 Nat -> Nat。

#check Nat.add     -- 是一個函數
#check Nat.add 1   -- 還是函數
#check Nat.add 1 1 -- 是一個自然數

請看下面這段代碼：

def add_one := Nat.add 1
#eval add_one 1

其中 def 關鍵詞用於提供定義。這裡 add_one 被定義為將輸入的自然數映射為等於它加1的那個自然數。

類型是Lean語言的第一公民，我們可以對類型作運算，得到新的類型。

#check Nat         -- Nat : Type
#check Bool        -- Bool : Type
#check Nat -> Bool -- Nat → Bool : Type
#check Nat × Nat   -- Nat × Nat : Type

從例子中可以看到，Lean中的每一個類型的類型都是 Type。那麽，Type 的類型是什麼呢？

#check Type        -- Type : Type 1
#check Type 1      -- Type 1 : Type 2
#check Type 2      -- Type 2 : Type 3
#check Type 3      -- Type 3 : Type 4

Type 0，等同於 Type 可以視為”普通”類型所在的集合，Type 1 是一個更大的、包含 Type 0 作為元素的集合，……以此類推。Type n 的列表是無窮的。

多態

一些類型，例如 List α 的類型由 α 決定。List 的類型為：

#check List

Prod 函數的類型是：

#check Prod

顯式定義多態常量的語法使用 universe 命令：

namespace a
  universe u
  def F (α : Type u) : Type u := Prod α α
  #check F
end a

也可以通過使用universe參數的方法來迴避 universe 命令的使用：

namespace b
  def F.{u} (α : Type u) : Type u := Prod α α
  #check F
end b

上面兩個例子中，我使用了 namespace 和 end 語句來避免 u 和 F 的重複定義。類似其它通用編程語言，Lean語言的namespace能夠避免不同的定義的撞名。

函數定義與求值

Lean可以使用 fun 或 λ 關鍵詞創建函數：

#check fun (x : Nat) => x + 5   -- Nat → Nat
#check λ (x : Nat) => x + 5     -- λ and fun mean the same thing
#check fun x => x + 5     -- Nat inferred
#check λ x => x + 5       -- Nat inferred

給函數傳入參數即可求值：

#eval (λ x : Nat => x + 5) 10
#eval (fun x : Nat => x + 5) 10

請注意理解這個例子：下面兩個函數的類型都是 Nat → Bool → Nat

#check fun x : Nat => fun y : Bool => if not y then x + 1 else x + 2
#check fun (x : Nat) (y : Bool) => if not y then x + 1 else x + 2

第一個函數接收一個自然數 x，然後返回一個函數，該函數接收一個布爾值 y，然後返回一個自然數。因此其類型為 Nat → Bool → Nat，本質上與第二個接收多個參數函數的類型相同。

定義和局部定義

定義使用 def 關鍵詞，局部定義使用 let 關鍵詞。我們可以在函數內使用局部定義，例如

def NatAdd (a : Nat) (b : Nat) :=
  let f := (λ (x : Nat) => a + x)
  (f b)
#eval NatAdd 1 2

上面的例子中，f 是一個局部定義的函數，可以在 NatAdd 函數的後續計算中使用。

歸納類型

在Lean4中，归纳类型（inductive type）是一种通过列举构造函数定义的类型。

最簡單的歸納類型是枚舉類型。下面的 Weekday 類型包含七種可能的值，對應於一週的七天。它們的區別僅在於構造函數的不同。

inductive Weekday where
  | sunday : Weekday
  | monday : Weekday
  | tuesday : Weekday
  | wednesday : Weekday
  | thursday : Weekday
  | friday : Weekday
  | saturday : Weekday

#check Weekday.sunday
#check Weekday.monday

作為歸納類型Weekday的構造函數，它們被定義在名為Weekday的命名空間下。只要使用open指令打開對應的命名空間，我們就可以直接使用構造函數的名稱。

open Weekday

#check sunday
#check monday

對於歸納類型，我們可以使用match語句，對歸納類型中的每個構造函數進行匹配。

def numberOfDay (d : Weekday) : Nat :=
  match d with
  | sunday    => 1
  | monday    => 2
  | tuesday   => 3
  | wednesday => 4
  | thursday  => 5
  | friday    => 6
  | saturday  => 7

實際上自然數也可以用歸納類型表示。#print 指令可以打印類型的定義。

#print Nat

輸出為：

inductive Nat
  | zero : Nat
  | succ (n : Nat) : Nat

可以看到實際上Nat是一種歸納類型。Nat（自然數）是這樣定義的：

0是一個自然數
對於任意一個自然數n，succ n 是n的”下一個數”，也是一個自然數

至此，本文介紹了一些Lean語言中的基礎概念。後續文章將介紹如何應用Lean語言證明一些數學定理。