Lean语法基础

Lean语法基础

简介

Lean语法基础是学习Lean编程语言的核心部分，它涵盖了Lean的基本语法结构、表达式、命令和类型系统。Lean是一种函数式编程语言，同时也支持定理证明，其语法设计简洁但功能强大，适合数学形式化验证和通用编程。本节将详细介绍Lean的语法规则，帮助初学者和进阶用户掌握其基本构造。

基本语法元素

变量与常量

在Lean中，变量和常量通过`def`或`let`关键字声明。`def`用于定义全局常量，而`let`用于局部绑定。

-- 全局常量
def pi : Float := 3.14159

-- 局部绑定
let x := 10

函数定义

Lean使用`def`定义函数，支持多参数和显式类型标注。

-- 简单函数
def add (x y : Nat) : Nat := x + y

-- 带类型推断的函数
def multiply x y := x * y

类型系统

Lean拥有强大的依赖类型系统。基本类型包括`Nat`（自然数）、`Int`（整数）、`Float`（浮点数）和`String`（字符串）。

-- 类型标注示例
def greet (name : String) : String := "Hello, " ++ name

控制结构

条件语句

Lean支持`if-then-else`表达式，其语法与其他语言类似。

def max (a b : Nat) : Nat :=
  if a > b then a else b

循环与递归

Lean鼓励使用递归而非循环，因为它是函数式语言的核心特性。

-- 递归计算阶乘
def factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

数据结构

列表与元组

列表是Lean中常用的数据结构，通过`List`类型表示。元组则用于固定长度的异构集合。

-- 列表
def numbers : List Nat := [1, 2, 3]

-- 元组
def person : (String × Nat) := ("Alice", 25)

结构体与记录

Lean通过`structure`关键字定义结构体，支持字段和默认值。

-- 定义结构体
structure Point where
  x : Float
  y : Float

-- 创建实例
def origin : Point := { x := 0.0, y := 0.0 }

定理证明语法

Lean不仅是一门编程语言，还是一个交互式定理证明器。以下是一个简单命题的证明示例：

-- 证明加法交换律
theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a
  case zero => simp
  case succ a ih => simp [Nat.add_succ, ih]

实际案例

以下是一个完整的Lean程序，演示如何实现和验证一个简单的数学函数：

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

-- 验证 fib 2 = 1
example : fib 2 = 1 := by simp [fib]

图表辅助说明

以下是一个Mermaid流程图，展示Lean函数的执行过程：

graph TD A[定义函数] --> B[输入参数] B --> C{是否匹配模式?} C -->|是| D[返回结果] C -->|否| E[递归调用] E --> C

数学公式支持

Lean的语法与数学符号紧密结合。例如，求和公式可以表示为：

$\sum _{i=1}^{n}i=\frac{n(n+1)}{2}$

在Lean中，该公式的证明如下：

theorem sum_formula (n : Nat) : (List.range n).sum = n * (n - 1) / 2 := by
  sorry  -- 证明暂略

总结

本节介绍了Lean的基本语法，包括变量、函数、类型系统、控制结构和数据结构。通过代码示例和实际案例，读者可以逐步掌握Lean的核心语法规则。后续章节将进一步深入探讨Lean的高级特性，如类型类和元编程。