编辑“︁Lean语法基础”︁

= Lean语法基础 =

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

== 基本语法元素 ==

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

<syntaxhighlight lang="lean">
-- 全局常量
def pi : Float := 3.14159

-- 局部绑定
let x := 10
</syntaxhighlight>

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

<syntaxhighlight lang="lean">
-- 简单函数
def add (x y : Nat) : Nat := x + y

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

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

<syntaxhighlight lang="lean">
-- 类型标注示例
def greet (name : String) : String := "Hello, " ++ name
</syntaxhighlight>

== 控制结构 ==

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

<syntaxhighlight lang="lean">
def max (a b : Nat) : Nat :=
  if a > b then a else b
</syntaxhighlight>

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

<syntaxhighlight lang="lean">
-- 递归计算阶乘
def factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * factorial n
</syntaxhighlight>

== 数据结构 ==

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

<syntaxhighlight lang="lean">
-- 列表
def numbers : List Nat := [1, 2, 3]

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

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

<syntaxhighlight lang="lean">
-- 定义结构体
structure Point where
  x : Float
  y : Float

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

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

<syntaxhighlight lang="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]
</syntaxhighlight>

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

<syntaxhighlight lang="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]
</syntaxhighlight>

== 图表辅助说明 ==  
以下是一个Mermaid流程图，展示Lean函数的执行过程：

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

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

<math>\sum_{i=1}^n i = \frac{n(n+1)}{2}</math>  

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

<syntaxhighlight lang="lean">
theorem sum_formula (n : Nat) : (List.range n).sum = n * (n - 1) / 2 := by
  sorry  -- 证明暂略
</syntaxhighlight>

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

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean基础]]