Lean第一个程序

简介[编辑 | 编辑源代码]

Lean第一个程序是初学者进入Lean定理证明系统的关键第一步。Lean是一种函数式编程语言和交互式定理证明器，由微软研究院开发。本节将引导用户完成编写、编译和运行第一个Lean程序的全过程，同时解释核心语法结构和编程范式。

环境准备[编辑 | 编辑源代码]

在开始前，请确保已安装：

Lean 4工具链（通过官方指南）
支持Lean的编辑器（如VS Code + Lean插件）

Hello World程序[编辑 | 编辑源代码]

以下是Lean 4中最基础的程序示例：

-- 定义主函数
def main : IO Unit := 
  IO.println "Hello, Lean World!"

代码解析[编辑 | 编辑源代码]

1. def 关键字声明一个新定义 2. main 是程序入口点名称 3. IO Unit 表示这是一个有IO副作用的函数，返回Unit类型（类似void） 4. := 是定义符号 5. IO.println 是标准输出函数

运行结果[编辑 | 编辑源代码]

通过命令行执行：

lean --run Hello.lean

输出：

Hello, Lean World!

核心概念详解[编辑 | 编辑源代码]

表达式结构[编辑 | 编辑源代码]

Lean采用表达式语法（Expression-oriented），所有代码都会求值为某个值。例如：

-- 简单的数学表达式
#eval 2 + 3 * 4  -- 输出: 14

-- 字符串连接
#eval "Lean" ++ " " ++ "4"  -- 输出: "Lean 4"

类型系统[编辑 | 编辑源代码]

Lean拥有强大的类型推导系统：

-- 显式类型声明
def answer : Nat := 42

-- 类型推导示例
def double (x : Nat) := x * 2

定理证明示例[编辑 | 编辑源代码]

展示Lean作为证明助手的特性：

-- 证明1 + 1 = 2
theorem one_plus_one : 1 + 1 = 2 := by
  rfl  -- 使用反射性策略

实际应用案例[编辑 | 编辑源代码]

数学问题求解[编辑 | 编辑源代码]

计算斐波那契数列：

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+2 => fib (n+1) + fib n

#eval fib 10  -- 输出: 55

算法验证[编辑 | 编辑源代码]

验证列表反转函数的正确性：

def reverse {α : Type} (xs : List α) : List α :=
  match xs with
  | [] => []
  | x :: xs => reverse xs ++ [x]

theorem reverse_length {α : Type} (xs : List α) : 
  (reverse xs).length = xs.length := by
  induction xs with
  | nil => simp [reverse]
  | cons x xs ih => simp [reverse, ih]

交互式编程[编辑 | 编辑源代码]

Lean提供交互式开发环境，使用#check和#eval命令：

#check Nat → Nat  -- 输出: Type → Type
#eval 2^10       -- 输出: 1024

常见问题[编辑 | 编辑源代码]

问题	解决方案
找不到lean命令	检查PATH环境变量或重新安装Lean
类型不匹配错误	使用`#check`检查表达式类型
定理证明卡住	尝试`simp`或`induction`策略

进阶学习路径[编辑 | 编辑源代码]

函数式编程范式
依赖类型系统
元编程与宏系统
大型数学库Mathlib的使用

可视化辅助[编辑 | 编辑源代码]

数学公式支持[编辑 | 编辑源代码]

Lean可以表示复杂数学概念，例如欧拉公式： $e^{i π} + 1 = 0$

对应的Lean代码：

import Mathlib.Data.Complex.Exponential

#check exp (π * I) + 1 = 0  -- 类型检查通过

总结[编辑 | 编辑源代码]

本节通过"Hello World"程序介绍了Lean的基本语法结构、类型系统和交互式开发环境。后续章节将深入探讨函数定义、类型理论和定理证明等高级主题。