跳到主要内容

Lean 语法基础

Lean是一种功能强大的编程语言和交互式定理证明器，广泛应用于数学证明和形式化验证。对于初学者来说，掌握Lean的基础语法是迈向高级应用的第一步。本文将逐步介绍Lean的核心语法，并通过代码示例和实际案例帮助你快速入门。

1. 变量声明​

在Lean中，变量声明使用 let 关键字。变量可以是任何类型，Lean的类型系统会自动推断类型，但你也可以显式指定类型。

lean
-- 自动推断类型
let x := 42

-- 显式指定类型
let y : Nat := 10
备注

Nat 是Lean中的自然数类型，表示非负整数。

2. 函数定义​

函数是Lean中的核心概念之一。你可以使用 def 关键字定义函数。函数可以有参数和返回值，Lean会根据返回值自动推断函数类型。

lean
-- 定义一个简单的加法函数
def add (x y : Nat) : Nat :=
  x + y

-- 调用函数
#eval add 3 5  -- 输出: 8
提示

#eval 是Lean中的一个命令，用于计算表达式的值并输出结果。

3. 类型系统​

Lean的类型系统非常强大，支持多种类型，包括基本类型（如 Nat、Int、Bool）和复合类型（如列表、元组等）。你可以使用 : 来指定变量的类型。

lean
-- 基本类型
let a : Nat := 10
let b : Bool := true

-- 复合类型
let lst : List Nat := [1, 2, 3]
警告

Lean的类型系统是静态的，这意味着类型在编译时就已经确定，不能在运行时改变。

4. 模式匹配​

模式匹配是Lean中处理数据结构的强大工具。你可以使用 match 关键字对数据进行模式匹配。

lean
-- 定义一个函数，使用模式匹配处理列表
def head (lst : List Nat) : Nat :=
  match lst with
  | [] => 0
  | h :: _ => h

-- 调用函数
#eval head [1, 2, 3]  -- 输出: 1
#eval head []         -- 输出: 0
注意

如果列表为空，模式匹配中的 [] 分支会返回 0，这是一种简单的错误处理方式。

5. 实际案例：斐波那契数列​

让我们通过一个实际案例来展示Lean语法的应用。我们将定义一个函数来计算斐波那契数列的第n项。

lean
-- 定义斐波那契函数
def fib (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | _ + 2 => fib (n - 1) + fib (n - 2)

-- 调用函数
#eval fib 10  -- 输出: 55
备注

这个实现虽然简单，但对于较大的 n 值效率较低。在实际应用中，可以使用更高效的算法。

6. 总结​

本文介绍了Lean编程语言的基础语法，包括变量声明、函数定义、类型系统和模式匹配。通过这些基础概念，你可以开始编写简单的Lean程序，并逐步探索更高级的功能。

7. 附加资源与练习​

  • 练习1: 尝试定义一个函数 multiply，接受两个 Nat 类型的参数并返回它们的乘积。
  • 练习2: 使用模式匹配定义一个函数 is_empty，判断一个列表是否为空。
  • 附加资源: 参考Lean官方文档，了解更多关于类型系统和高级功能的内容。

通过不断练习和探索，你将能够熟练掌握Lean的语法，并应用于更复杂的数学证明和编程任务中。