概述

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 证明的主力。