概述

Lean 是一個交互式定理證明器（Interactive Theorem Prover, ITP），也是一門通用函數式編程語言。

Lean 項目由微軟 Redmond 研究院的 Leonardo de Moura 在 2013 年發起。Lean 是在 Apache 2.0 許可協議 下發布的，這是一個允許他人自由使用和擴展代碼和數學庫的許可性開源許可證。

Lean4 于 2021 年發布，為 Lean 定理證明器的重新實現。

Lean 作為一門獨特的語言，兼具 數學和編程 兩方面的特性。

• 作為交互式定理證明器，Lean 提供了嚴格的邏輯框架，數學家可以將數學定理轉換成代碼，并嚴格驗證這些定理的正確性。
• 作為通用函數式編程語言，它具有 依賴類型 的 嚴格 的 純函數式 語言性質。

Apache 2.0 是一個寬松的開源許可證，它允許自由使用、修改和分發軟件（包括商業用途），但要求保留版權和許可聲明，提供修改說明，且不提供任何擔保，并包含明確的專利授權。

參考文檔

• 官方文檔
• Lean 中文社區
• Lean3 基礎
• 《Theorem Proving in Lean》，官方強烈建議閱讀 ，中文翻譯
• 《Functional Programming in Lean》，使用 Lean 4 作為編程語言的通俗易懂的介紹，沒有假設任何函數式編程的背景，編程語言學習教程，建議閱讀，中文翻譯
• 《Mathematics in Lean》
• 《Lean 參考手冊》

運行程序

Lean 是為交互式使用而設計的，而不是作為批處理模式系統（在批處理模式系統中，整個文件被輸入，然后轉換為目標代碼或錯誤消息）。

Lean 的交互式開發是指通過 Lean 的交互式環境（如Lean4 的 VS Code 擴展）逐步構建和驗證代碼或證明的過程。用戶可以在編寫代碼的同時，實時查看 Lean 的反饋，從而快速發現和修正錯誤。

當你編寫代碼時，Lean會實時進行類型檢查并提供反饋。

Lean 源文件處理過程

Lean 命令行工具

• elan：Lean 的版本管理工具，用于安裝、管理和切換不同版本的 Lean，類似于 Rust 的 rustup 或 Node.js 的 nvm。
• lake（Lean Make）：Lean 的包管理器和構建器，已集成到 Lean 4 核心倉庫中。用于創建 Lean 項目，構建 Lean 包,編譯 Lean 可執行文件等。
• lean：Lean 語言本身的核心組件，負責實際的代碼編譯和語言服務器協議（LSP）支持，用戶不需要直接與 lean 交互。

elan 命令行工具

# 輸出版本號來測試安裝是否成功
elan --version   # 更新 elan
elan self update# 顯示已安裝的 Lean 版本
elan show        # 下載指定 Lean 版本，所有版本可見 https://github.com/leanprover/lean4/releases
elan install leanprover/lean4:v4.21.0# 切換默認的 Lean 版本
# 切換到 leanprover/lean4:v4.21.0
elan default leanprover/lean4:v4.21.0# 設置在當前目錄下使用的 Lean 版本
elan override set leanprover/lean4:v4.21.0
# info: info: override toolchain for 'xxx' set to 'leanprover/lean4:v4.21.0'# 采用某個版本的 lean 運行 hello.lean文件，等價于直接使用某個版本的lean運行：lean --run hello.lean
elan run leanprover/lean4:v4.21.0 lean --run hello.lean

lean 命令行工具

# 查看 Lean 版本號
lean --version# 編譯并輸出結果
lean example.lean# 執行 Lean 文件中的代碼，會執行文件中的 main 函數（如果存在），并輸出結果。等價于：elan run leanprover/lean4:v4.21.0 lean --run hello.lean 命令運行
lean --run example.lean

lake 命令行工具

# 在當前目錄新創建一個 hello_world 的項目（創建一個名為 hello_world 的目錄并初始化項目架構）
lake new hello_world# 可將當前目錄初始化為項目包
lake init# 構建當前項目，結果將放置在 .lake/build/bin 目錄下
lake build# 清理構建文件，會刪除 build 目錄
lake clean# 更新依賴
lake update

運行單文件程序

Hello, world!

運行 Lean 程序最簡單的方法是使用 Lean 可執行文件的 --run 選項。創建一個名為 Hello.lean 的文件并輸入以下內容：

def main : IO Unit := IO.println "Hello, world!"

然后，在命令行運行：

lean --run Hello.lean

該程序會在顯示 Hello, world! 后退出。

驗證 Lean4 證明

創建一個名為 proof.lean 的文件并輸入以下內容：

-- proof.lean
# 成功證明
theorem my_first_theorem : 1 + 1 = 2 := bysimp# 失敗證明
theorem my_false_theorem : 1 + 1 = 1 := bysimp# 錯誤語法
theorem my_syntax_error_themore 1 + 1 = 2 := bysimp

在終端中運行：lean proof.lean，返回錯誤信息：

hello.lean:5:40: error: unsolved goals
? False
hello.lean:8:31: error: unexpected token; expected ':'

上圖右側的 InfoView 是 Lean 的主要交互式組件。它可用于檢查證明目標、預期類型和診斷，以及為 Lean 代碼呈現稱為“小部件”的任意用戶界面。

打開 Lean 文檔時，InfoView 會自動顯示在文本文檔旁邊。若未自動顯示，可手動點擊顯示。

運行多文件項目

一個由包含 main 定義的單個文件組成的 Lean 程序可以使用 lean --run FILE 運行。雖然這可能是開始使用簡單程序的好方法，但大多數程序最終都會升級為多文件項目，在運行之前應該對其進行編譯。

使用 VS Code 創建項目

項目結構

• Main.lean: 是 Lean 編譯器將查找 main 活動的文件。
• {Project Name}.lean 和 {Project Name}/Basic.lean: 是程序支持庫的腳手架。
• lakefile.toml: 項目的配置文件，用于定義依賴和構建選項。
• lean-toolchain: 指定Lean版本的文件。
• lake-manifest.json: 自動生成的文件，記錄項目的依賴關系。

Note: lake 生成的項目結構可能變動，以最新版本為準

在 VS Code 中構建項目

構建后在項目的 .lake/build/bin 目錄下會生成項目的二進制可執行文件 hello_world.exe，可點擊運行。

在 VS Code 中通過 Create Standalone Project 菜單創建項目的過程其實是調用 lake new 命令的過程。而通過 Project: Build Project 構建項目可的過程其實是調用 lake build 命令的過程。

# 創建項目
$ lake new hello_world# 構建項目
$ lake build# 運行
$ ./.lake/build/bin/hello_world.exe
Hello, world!

Lean 模塊與導入

在 Lean 中，模塊是一個包含相關定義和聲明的代碼單元。模塊可以包含函數、類型、定理等內容。通過將代碼組織成模塊，你可以更好地管理代碼結構，避免命名沖突，并提高代碼的可重用性。

-- Math.lean, 通過 namespace 關鍵字定義 Math 模塊，其中包含了兩個函數 add 和 sub。要使用這些函數，需要通過模塊名來訪問,例如 Math.add
namespace Math
def add (a b : Nat) : Nat := a + b
def sub (a b : Nat) : Nat := a - b
end Math-- test.lean 使用 import 關鍵字來導入 Math 模塊
import Math
#eval Math.add 2 3  -- 輸出: 5----------------------------------------------------------------------------
-- Math.lean, 不使用 namespace 關鍵字，import 后可直接使用，不需要模塊名
def add (a b : Nat) : Nat := a + b
def sub (a b : Nat) : Nat := a - b-- test.lean 使用 import 關鍵字來導入 Math 模塊
import Math
#eval add 2 3  -- 輸出: 5

Lean4 基礎語法

注釋

單行注釋使用 -- 注釋符

注釋塊使用 /- 和 -/ 之間的文本組成了一個注釋塊

/- 
定義一些常數
檢查類型
-/-- 這一行是個注釋
def m : Nat := 1       -- m 是自然數
#check m            -- 輸出: Nat

注釋會被 Lean 的編譯器忽略。

表達式求值

在 Lean 中，程序首先是表達式，思考計算的主要方式是對表達式求值。

在 Lean 中，程序的工作方式與數學表達式相同。變量一旦被賦予一個值，就不能再被重新賦值。求值表達式不會產生副作用。如果兩個表達式的值相同，那么用一個表達式替換另一個表達式并不會導致程序計算出不同的結果。

要讓 Lean 對一個表達式求值，請在編輯器中的表達式前面加上 #eval，然后它會返回結果。通常可以將光標或鼠標指針放在 #eval 上查看結果。例如

#eval 5 + 2

用于向系統詢問信息的輔助命令都以井號(#)開頭。
#eval 命令讓 Lean 計算表達式的值。#check 命令要求 Lean 給出它的類型。

雖然普通的數學符號和大多數編程語言都使用括號（例如 f(x)）來表示函數調用，但 Lean 只是將參數寫在函數后邊（例如 f x）。例如

#eval String.append "Hello, " "Lean!"            -- 輸出: "Hello, Lean!"

其中函數的多個參數只是寫在函數后面用空格隔開。

就像算術運算的順序需要在表達式中使用括號（如 (1 + 2) * 5）表示一樣，當函數的參數需要通過另一個函數調用來計算時，括號也是必需的。例如，在

#eval String.append "great " (String.append "oak " "tree")

Lean 條件表達式使用 if、then 和 else 編寫。例如

#eval String.append "it is " (if 1 > 2 then "yes" else "no")===>
"it is no"

變量和定義

定義

在 Lean 中，需使用 def 關鍵字引入定義。例如，若要定義名稱 hello 來引用字符串 “Hello”，請編寫：

def hello := "Hello"-- 定義了一個 Nat 類型的新常量 m，其值為 1。
def m : Nat := 1

Lean 還允許你使用 let 關鍵字來引入「局部定義」。表達式 let a := t1; t2 定義等價于把 表達式 t2 中所有的 a 替換成 t1 的結果。

#check let y := 2 + 2; y * y   -- Nat
#eval  let y := 2 + 2; y * y   -- 16def twice_double (x : Nat) : Nat :=let y := x + x; y * y#eval twice_double 2   -- 16-- 可以連續使用多個 let 命令來進行多次替換
#check let y := 2 + 2; let z := y + y; z * z   -- Nat
#eval  let y := 2 + 2; let z := y + y; z * z   -- 64-- 換行可以省略分號
def t (x : Nat) : Nat :=let y := x + xy * y#eval t 3
===>
36

在 Lean 中，使用冒號加等號運算符 := 而非 = 來定義新名稱。這是因為 = 用于描述現有表達式之間的相等性，而使用兩個不同的運算符有助于避免混淆。

類型

Lean 中的每個程序都必須有一個類型。特別是，每個表達式在求值之前都必須具有類型。這是使用 冒號運算符（:） 完成的，例如

#eval (1 + 2 : Nat)

在這里，Nat 是自然數的類型，它們是任意精度的無符號整數。在 Lean 中，Nat 是非負整數字面量的默認類型。當答案原本為負數時，Nat 上的減法運算會返回 0。例如，

#eval 1 - 2===>
0

若要使用可以表示負整數的類型，請直接使用 Int

#eval (1 - 2 : Int)===>
-1

若要檢查表達式的類型而不求值，請使用 #check 而非 #eval。例如：

#check (1 - 2 : Int)       -- 會輸出 1 - 2 : Int 而不會實際執行減法運算。

Lean 中的基本類型

Lean提供了幾種基本類型，以下是一些常見的類型：

• Nat：自然數類型，表示非負整數。
• Int：整數類型，表示正負整數。
• Float：浮點數（小數）類型
• Bool：布爾類型，表示true或false。
• String：字符串類型，表示文本數據。
• Unit：單元類型，通常用于表示沒有返回值的函數

def a : Nat := 1          -- a 是自然數
def b : Bool := true      -- b 是布爾型
def c : Int := -5         -- c 是整數
def d : Float := 5.3         -- d 是浮點數
def e : String := "test"  -- d 是字符串def doNothing : Unit := ()

Lean可以根據上下文自動推斷出類型。

-- Lean可以推斷出myNat的類型是Nat
def myNat := 42#check myNat

在Lean中，函數也是一種類型。函數類型 描述了輸入和輸出的類型。
例如，一個接受Nat并返回Nat的函數的類型是 Nat → Nat。接受兩個 Nat 并返回一個 Nat 的函數的類型為 Nat → Nat → Nat。

-- 定義一個函數，接受一個Nat并返回它的平方
-- 定義 square 的 類型是 函數（即 Nat → Nat），
def square : Nat → Nat :=fun n => n * n-- 函數類型，輸出 square : Nat → Nat
#check square-- 調用函數
#eval square 5  -- 輸出: 25--------------------------------------------------
-- 定義一個求和函數
def sum : Nat → Nat -> Nat :=fun a b => a + b-- 函數類型，輸出 sum : Nat → Nat → Nat
#check sum-- 調用函數
#eval sum 3 4		 -- 輸出: 7-----------------------------------------------------
def double (a : Nat) : Nat := 2 * a-- compose 是一個函數，它接受兩個函數 f 和 g 和一個 n，并返回一個新的函數，該函數首先應用 g，然后應用 f。
def compose : (Nat → Nat) → (Nat → Nat) → Nat → Nat :=fun f g n => f (g n)#eval compose square double 5		-- 輸出: 100

類型本身（如 Nat 和 Bool 這些東西）也是對象，因此也具有類型。

#check Nat               -- Type
#check Nat → Bool        -- Type

在 Lean 中，類型是語言的一等部分——它們與其他表達式一樣都是表達式，這意味著定義可以引用類型，就像它們可以引用其他值一樣。

如果 String 輸入起來太長，可以定義一個簡寫 Str，然后就可以使用 Str 而非 String 作為定義的類型：

def Str : Type := String
def aStr : Str := "This is a string."

變量

Lean 提供 variable 指令來聲明變量。

variable (n : Nat)
#check nvariable (α β γ : Type)--  α  和 β 是類型，α → β 表示從 α 到 β  的函數類型
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)

variable 命令指示 Lean 將聲明的變量作為綁定變量插入定義中，這些定義通過名稱引用它們。

variable 命令的意義在于聲明變量，以便在定理中使用。

當以 variable 的方式聲明時，變量將一直保持存在，直到所處理的文件結束。然而，有時需要限制變量的作用范圍。Lean 提供了小節標記 section 來實現這個目的：

section usefulvariable (α β γ : Type)variable (g : β → γ) (f : α → β) (h : α → α)variable (x : α)def compose := g (f x)def doTwice := h (h x)def doThrice := h (h (h x))
end useful

當一個小節結束后，變量不再發揮作用。
你也不需要命名一個小節，也就是說，你可以使用一個匿名的 section /end 對。但是，如果你確實命名了一個小節，你必須使用相同的名字關閉它。小節也可以嵌套，這允許你逐步增加聲明新變量。

sectionvariable (α : Type)variable (h : α → α)	-- h 函數類型variable (x : α)def doTwice := h (h x)
enddef t (x : Nat) : Nat :=let y := x + xy * y-- fun α h x => h (h x)
#print doTwice#eval doTwice Nat t 2
===>
1024

定義函數

在 Lean 中有多種方法可以定義函數，最簡單的就是在定義的類型之前寫上函數的參數，并用空格分隔。例如，可以編寫一個將其參數加 1 的函數：

def add1 (n : Nat) : Nat := n + 1def maximum (n : Nat) (k : Nat) : Nat :=if n < k thenkelse n#eval maximum 2 5
===>
5

def double (x : Nat) : Nat :=x + x

名字 double 被定義為一個函數，它接受一個類型為 Nat 的輸入參數 x，其結果是x + x，因此它返回類型 Nat。然后你可以調用這個函數:

#eval double 3    -- 6

Lean 中的函數是一等的值，這意味著它們可以作為參數傳遞給其他函數、保存在變量中，并像任何其他值一樣使用。

Lean 創建函數的主要方式有三種

• 匿名函數使用 fun (或 λ) 關鍵字編寫。例如，一個交換 Point 字段的函數可以寫成 fun (point : Point) => { x := point.y, y := point.x : Point }。

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

• 非常簡單的匿名函數通過在括號內放置一個或多個間點 · 來編寫。 每個間點都是函數的一個參數，用括號限定其主體。 例如，一個從其參數中減去 1 的函數可以寫成 (· - 1) 而非 fun x => x - 1。
• 函數可以用 def 或 let 定義，方法是添加參數列表或使用模式匹配記法。

命名規則

在Lean中，命名規則主要涉及變量、函數和類型的命名。以下是一些基本的命名原則：

• 變量命名：使用小寫字母和下劃線（_）分隔單詞，例如 my_variable。
• 函數命名：與變量命名類似，使用小寫字母和下劃線分隔單詞，例如 calculate_sum。
• 類型命名：使用大寫字母開頭的駝峰命名法，例如 MyType。

命名空間

Lean 可以讓你把定義放進一個「命名空間」（namespace）里，并且命名空間也是層次化的：

namespace Foodef a : Nat := 5def f (x : Nat) : Nat := x + 7def fa : Nat := f adef ffa : Nat := f (f a)#check a#check f#check fa#check ffa#check Foo.fa
end Foo-- #check a  -- error
-- #check f  -- error
#check Foo.a
#check Foo.f
#check Foo.fa
#check Foo.ffa

Lean 把和列表相關的定義和定理都放在了命名空間 List 之中。

#check List.nil
#check List.cons
#check List.map

open List 命令允許你使用短一點的名字：

open List#check nil
#check cons
#check map

命名空間也是可以嵌套。

命名空間和小節有不同的用途：命名空間組織數據，小節聲明變量，以便在定義中插入。

數據類型

• 和類型（Sum Types）：表示“或”關系，即一個值可以是多種類型中的一種。
• 積類型（Product Types）：表示“與”關系，即一個值由多個類型的值組合而成。
• 遞歸類型（Recursive Datatype）：可以包含自身實例的類型，大多數經典的數據結構（例如樹和列表）具有遞歸結構，其中列表的尾部本身是一個列表，或者二叉樹的左右分支本身是二叉樹。

遞歸和類型稱為歸納類型（Inductive Datatype），因為可以用數學歸納法來證明有關它們的陳述。

許多內置類型實際上是標準庫中的歸納類型。例如，Bool 就是一個歸納類型：

inductive Bool where| false : Bool| true : Bool

這個例子定義了一個名為 Bool 的歸納類型，它有兩個構造器：true 和 false, 分別表示布爾值“真”和“假”。每個構造器都不接受參數，并且都返回 Bool 類型。

其中 | 符號主要用于表示“或”的含義，inductive 關鍵字用于定義歸納類型，這是一種通過構造器遞歸定義的數據類型。

inductive 歸納類型名 : 額外參數 -> 類型 
| 構造器1 (參數1 : 類型1, ...) : 返回類型 :=
| 構造器2 (參數2 : 類型2, ...) : 返回類型 :=
...

歸納數據類型允許是遞歸的，事實上，Nat 就是這樣的數據類型的一個例子，因為 succ 需要另一個 Nat。

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

一個簡單的二叉樹數據結構

-- 定義二叉樹數據結構
inductive Tree (α : Type) where| leaf : Tree α| node : Tree α → α → Tree α → Tree α-- 創建一個具體的樹
def myTree : Tree Nat :=Tree.node (Tree.node Tree.leaf 1 Tree.leaf) 2 (Tree.node Tree.leaf 3 Tree.leaf)#eval myTree

在這個定義中，Tree 是一個類型構造器，它接受一個類型 α 并返回一個二叉樹類型。leaf 表示一個空樹，node 表示一個包含左子樹、節點值和右子樹的樹。

在這個例子中，myTree 是一個包含自然數的二叉樹，其結構如下：

結構體

定義一個結構體會向 Lean 引入一個全新的類型，該類型不能化簡為任何其他類型。它允許將不同類型的數據組合在一起，形成一個新的數據類型。例如，一個點可以用笛卡爾坐標或極坐標表示，每個都是一對浮點數。

笛卡爾點 是一個結構體，它有兩個 Float 字段，稱為 x 和 y。它使用 structure 關鍵字聲明。

structure Point wherex : Floaty : Float
deriving Repr

聲明之后，Point 就是一個新的結構體類型了。最后一行寫著 deriving Repr，它要求 Lean 生成代碼以顯示類型為 Point 的值。此代碼用于 #eval 顯示求值結果以供程序員使用

創建結構體類型值通常的方法是在大括號內為其所有字段提供值。笛卡爾平面的原點是 x 和 y 均為零的點：

def origin : Point := { x := 0.0, y := 0.0 }

使用點記法提取結構體的各個字段

#eval origin
===>
{ x := 0.000000, y := 0.000000 }#eval origin.x
===>
0.000000#eval origin.y
===>
0.000000

兩點之間的距離（即其 x 和 y 分量之差的平方和的平方根）可以寫成：

def distance (p1 : Point) (p2 : Point) : Float :=Float.sqrt (((p2.x - p1.x) ^ 2.0) + ((p2.y - p1.y) ^ 2.0))#eval distance { x := 1.0, y := 2.0 } { x := 5.0, y := -1.0 }
===>
5.000000

結構體更新不會修改原始結構體

Lean 提供了一種便捷的語法，用于替換結構體中的一些字段，同時保留其他字段。通過在結構體初始化中使用 with 關鍵字，未更改字段的源代碼寫在 with 之前，而新字段寫在 with 之后。

def zeroX (p : Point) : Point :={ p with x := 0 }def fourAndThree : Point :={ x := 4.3, y := 3.4 }#eval fourAndThree
===>
{ x := 4.300000, y := 3.400000 }#eval zeroX fourAndThree
===>
{ x := 0.000000, y := 3.400000 }#eval fourAndThree
===>
{ x := 4.300000, y := 3.400000 }

構造子

與 Java 或 Python 等語言中的構造函數不同，Lean 中的構造子（Constructor）不是在初始化數據類型時運行的任意代碼。相反，構造子只會收集要存儲在新分配的數據結構中的數據。

structure Point wherex : Floaty : Float
deriving Repr-- 輸出 { x := 1.5, y := 2.8 } : Point
#check Point.mk 1.5 2.8

其中 mk 為默認構造子，要覆蓋結構體的構造子名稱，請在開頭寫出新的名稱后跟兩個冒號。例如，要使用 Point.point 而非 Point.mk，請編寫：

structure Point wherepoint ::x : Floaty : Float
deriving Repr-- 輸出 { x := 1.5, y := 2.8 } : Point
#check Point.point 1.5 2.8

模式匹配

模式匹配是一種根據數據的形狀或結構來匹配和處理數據的技術。它通常用于處理遞歸數據結構（如列表、樹等）或枚舉類型。通過模式匹配，我們可以輕松地提取數據中的特定部分，并根據不同的情況執行不同的操作。

在Lean4中，模式匹配通常與match表達式一起使用。match表達式允許我們根據輸入值的不同模式來執行不同的代碼塊。

模式匹配語法

match expression with
| pattern1 => result1
| pattern2 => result2
...
| patternN => resultN

其中，expression是要匹配的值，pattern1到patternN是不同的模式，result1到resultN是對應模式匹配成功時返回的結果。

def isZero (n : Nat) : Bool :=match n with| 0 => true| Nat.succ k => false-- 或者
def isZero : Nat → Bool
| 0 => true
| _ => false
-- 其中 _ 為占位，表示預期根據上下文推斷的未知術語

示例：計算列表長度

def length {α : Type} : List α → Nat
| [] => 0
| _ :: xs => 1 + length xs#eval length [1, 2, 3]        -- 輸出: 3

示例：計算n的階乘

def factorial : Nat → Nat| 0 => 1| n + 1 => (n + 1) * factorial n#eval factorial 5  -- 120

在這個例子中，factorial 函數通過模式匹配來計算自然數的階乘。當輸入為 0 時，返回 1；否則，遞歸計算 n + 1 的階乘。

多態

和大多數語言一樣，Lean 中的類型可以接受參數。例如，類型 List Nat 描述自然數列表，List String 描述字符串列表，List (List Point) 描述點列表的列表。這與 C# 或 Java 中的 List、List 或 List<List> 非常相似。

在函數式編程中，術語多態（Polymorphism）通常指將類型作為參數的數據類型和定義。

Point 的多態版本稱為 PPoint，它可以將類型作為參數，然后將該類型用于兩個字段：

structure PPoint (α : Type) wherex : αy : α
deriving Reprdef natOrigin : PPoint Nat := { x := Nat.zero, y := Nat.zero }
#eval natOrigin
===>
{ x := 0, y := 0 }def nOrigin : PPoint Nat := { x := 1, y := 2 }
#eval nOrigin
===>
{ x := 0, y := 0 }

在此示例中，期望的兩個字段都是 Nat。就和通過用其參數值替換其參數變量來調用函數一樣，向 PPoint 傳入類型參數 Nat 會產生一個結構體，其中字段 x 和 y 具有類型 Nat，因為參數名稱 α 已被參數類型 Nat 替換。

List 列表

Lean 中的列表是一個有序的集合，其中每個元素都具有相同的類型。

列表的基本結構是遞歸的：一個列表要么是空的（[]），要么是一個元素與另一個列表的組合（a :: as）。

列表的類型定義為 List α，其中 α 是列表中元素的類型。

-- 定義一個整數列表
def myList : List Int := [1, 2, 3, 4, 5]

使用下標索引來訪問列表中的值，注意 索引從0開始。

要查找列表中的第一個條目（如果存在），請使用 List.head?。

def primesUnder10 : List Nat := [2, 3, 5, 7]#eval primesUnder10
===>
[2, 3, 5, 7]#eval primesUnder10[0]
===>
2#eval primesUnder10[3]
===>
7-- 第一個元素
#eval primesUnder10.head?
===>
2-- 最后一個元素
#eval primesUnder10.getLast?
===>
7-- 獲取除第一個元素外的剩余部分
#eval  primesUnder10.tail 
===>
[3, 5, 7]-- 鏈表長度
#eval primesUnder10.length
===>
4#eval ([] : List Int).length
===>
0

Lean 的命名約定是使用后綴 ? 定義可能失敗的操作，用于返回 Option 的版本，！ 用于在提供無效輸入時崩潰的版本，D 用于在操作在其他情況下失敗時返回默認值的版本。例如，head 要求調用者提供數學證據證明列表不為空，head? 返回 Option，head! 在傳遞空列表時使程序崩潰，headD 采用一個默認值，以便在列表為空時返回。問號和感嘆號是名稱的一部分，而不是特殊語法。

#eval [].head? (α := Int)
===>
none#eval ([] : List Int).head?
===>
none-- 列表為空時返回默認值5
#eval [].headD 5
===>
5

列表的遞歸性質
列表在 Lean 中是遞歸定義的，這意味著你可以使用遞歸函數來處理列表。例如，以下是一個計算列表長度的遞歸函數：

def len {α : Type} : List α → Nat| [] => 0| _ :: tail => 1 + len tail#eval len [1,2,3]   -- 3

其中 _ :: tail 表示列表 有 一個元素 _ 與 另一個列表 tail 的組合。

Option 可選類型

許多語言都有一個 null 值來表示沒有值。Lean 沒有為現有類型配備一個特殊的 null 值，而是提供了一個名為 Option 的數據類型，為其他類型配備了一個缺失值指示器。

例如，一個可為空的 Int 由 Option Int 表示，一個可為空的字符串列表由類型 Option (List String) 表示。

def getLast (args : List String) : Option String := args.getLast?

Prod 積類型

Prod 結構體，即積（Product）的簡寫，是一種將兩個值連接在一起的通用方法。例如，Prod Nat String 包含一個 Nat 和一個 String。

Prod 非常類似于 C# 的元組、 C++ 中的 tuple。

def fives : String × Int := ("five", 5)
#eval fives
===>
("five", 5)def sevens : String × Int × Nat := ("VII", 7, 4 + 3)
#eval sevens
===>
("VII", 7, 7)def sevens2 : String × (Int × Nat) := ("VII", (7, 4 + 3))
#eval sevens
("VII", 7, 7)

Lean4 定理證明初探

Lean的核心思想是將數學證明轉化為計算機可以理解和驗證的形式化證明。

Lean 證明的基本結構

• 定義：定義數學對象或概念。
• 定理聲明：聲明要證明的定理。
• 證明構造：通過一系列步驟構造證明。

示例：證明 1 + 1 = 2

-- 定義加法
def add : Nat → Nat → Nat| Nat.zero, n => n| Nat.succ m, n => Nat.succ (add m n)-- 定理聲明, 定理的聲明通常使用 theorem 關鍵字
theorem one_plus_one_eq_two : add (Nat.succ Nat.zero) (Nat.succ Nat.zero) = Nat.succ (Nat.succ Nat.zero) :=-- 證明構造rfl

我們首先定義了自然數 Nat 加法函數 add。然后，我們聲明了一個定理 one_plus_one_eq_two，并使用 rfl（自反性）來證明它。

備注：rfl 是 Lean 中的一個內置策略，用于證明兩個表達式在定義上相等。

示例：證明 2 * (x + y) = 2 * x + 2 * y

section
variable (x y : Nat)def double := x + x#check double y
#check double (2 * x)attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm-- 證明: 2 * (x + y) = 2 * x + 2 * y
theorem t1 : double (x + y) = double x + double y := bysimp [double]#check t1 y
#check t1 (2 * x)-- 證明: 2 * (x * y) = 2 * x * y 
theorem t2 : double (x * y) = double x * y:= bysimp [double, Nat.add_mul]end

by 表示采用策略編寫證明，simp 策略，即「化簡（Simplify）」的縮寫，是 Lean 證明的主力。