编辑“︁Lean第一个程序”︁

{{DISPLAYTITLE:Lean第一个程序}}

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

== 环境准备 ==
在开始前，请确保已安装：
* Lean 4工具链（通过[https://leanprover.github.io/lean4/doc/setup.html 官方指南]）
* 支持Lean的编辑器（如VS Code + Lean插件）

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

<syntaxhighlight lang="lean">
-- 定义主函数
def main : IO Unit := 
  IO.println "Hello, Lean World!"
</syntaxhighlight>

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

=== 运行结果 ===
通过命令行执行：
<syntaxhighlight lang="bash">
lean --run Hello.lean
</syntaxhighlight>
输出：
<syntaxhighlight>
Hello, Lean World!
</syntaxhighlight>

== 核心概念详解 ==
=== 表达式结构 ===
Lean采用表达式语法（Expression-oriented），所有代码都会求值为某个值。例如：

<syntaxhighlight lang="lean">
-- 简单的数学表达式
#eval 2 + 3 * 4  -- 输出: 14

-- 字符串连接
#eval "Lean" ++ " " ++ "4"  -- 输出: "Lean 4"
</syntaxhighlight>

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

<syntaxhighlight lang="lean">
-- 显式类型声明
def answer : Nat := 42

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

=== 定理证明示例 ===
展示Lean作为证明助手的特性：

<syntaxhighlight lang="lean">
-- 证明1 + 1 = 2
theorem one_plus_one : 1 + 1 = 2 := by
  rfl  -- 使用反射性策略
</syntaxhighlight>

== 实际应用案例 ==
=== 数学问题求解 ===
计算斐波那契数列：

<syntaxhighlight lang="lean">
def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+2 => fib (n+1) + fib n

#eval fib 10  -- 输出: 55
</syntaxhighlight>

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

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

== 交互式编程 ==
Lean提供交互式开发环境，使用<code>#check</code>和<code>#eval</code>命令：

<syntaxhighlight lang="lean">
#check Nat → Nat  -- 输出: Type → Type
#eval 2^10       -- 输出: 1024
</syntaxhighlight>

== 常见问题 ==
{| class="wikitable"
|-
! 问题 !! 解决方案
|-
| 找不到lean命令 || 检查PATH环境变量或重新安装Lean
|-
| 类型不匹配错误 || 使用<code>#check</code>检查表达式类型
|-
| 定理证明卡住 || 尝试<code>simp</code>或<code>induction</code>策略
|}

== 进阶学习路径 ==
* 函数式编程范式
* 依赖类型系统
* 元编程与宏系统
* 大型数学库Mathlib的使用

== 可视化辅助 ==
<mermaid>
graph TD
    A[编写Lean代码] --> B[类型检查]
    B --> C{通过?}
    C -->|是| D[编译执行]
    C -->|否| E[错误修正]
    D --> F[输出结果]
</mermaid>

== 数学公式支持 ==
Lean可以表示复杂数学概念，例如欧拉公式：
<math>e^{i\pi} + 1 = 0</math>

对应的Lean代码：
<syntaxhighlight lang="lean">
import Mathlib.Data.Complex.Exponential

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

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

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