编辑“︁Lean命名规则”︁

= Lean命名规则 =

'''Lean命名规则'''是Lean编程语言中用于标识符（如变量、函数、类型等）命名的规范体系。良好的命名习惯能显著提升代码可读性、维护性，并帮助开发者更好地表达代码意图。本条目将系统介绍Lean的命名约定及其背后的设计哲学。

== 核心原则 ==
Lean的命名规则遵循以下核心原则：
* '''语义清晰'''：名称应准确反映实体用途（如<code>list_length</code>优于<code>n</code>）
* '''一致性'''：同类实体使用相同命名模式（如类型参数总用希腊字母）
* '''可读性'''：避免缩写歧义（推荐<code>index</code>而非<code>idx</code>）
* '''层级表达'''：通过命名体现抽象层次（基础函数用全称，局部变量可简化）

== 基本规范 ==
=== 1. 变量与函数 ===
* 使用'''蛇形命名法'''（snake_case）
* 名称应为完整英文单词或标准数学符号
* 避免单字符命名（数学公式除外）

<syntaxhighlight lang="lean">
-- 推荐
def square_root (x : Float) : Float := 
  Float.sqrt x

-- 不推荐
def sqrt (n : Float) : Float := 
  Float.sqrt n
</syntaxhighlight>

=== 2. 类型与构造子 ===
* 类型使用'''帕斯卡命名法'''（PascalCase）
* 构造子同样使用PascalCase
* 单构造子类型建议添加后缀`.type`

<syntaxhighlight lang="lean">
-- 正确示例
inductive BinaryTree (α : Type) where
  | Leaf 
  | Node (left : BinaryTree α) (value : α) (right : BinaryTree α)
</syntaxhighlight>

=== 3. 类型参数 ===
* 使用希腊字母表示类型参数
* 常见约定：
** <code>α β γ</code>：任意类型
** <code>ι</code>：索引类型
** <code>σ τ</code>：状态类型

<syntaxhighlight lang="lean">
def swap_pair {α β : Type} (p : α × β) : β × α := 
  (p.2, p.1)
</syntaxhighlight>

== 特殊约定 ==
=== 1. 定理命名 ===
* 使用描述性名称表达定理内容
* 常见模式：
** <code>noun_verb_property</code>（如<code>list_reverse_involutive</code>）
** <code>property_of_noun</code>（如<code>commutativity_of_add</code>）

<syntaxhighlight lang="lean">
theorem reverse_reverse {α : Type} (xs : List α) : 
  xs.reverse.reverse = xs := by
  induction xs with
  | nil => simp
  | cons h t ih => simp [List.reverse_cons, ih]
</syntaxhighlight>

=== 2. 类型类实例 ===
* 添加<code>inst</code>前缀
* 遵循<code>inst[ParentClass]_[Description]</code>模式

<syntaxhighlight lang="lean">
instance instMonadOption : Monad Option where
  pure x := some x
  bind mx f := Option.bind mx f
</syntaxhighlight>

== 命名空间管理 ==
Lean采用分层命名空间体系：

<mermaid>
graph TD
    A[Root] --> B[Mathlib]
    B --> C[Algebra]
    B --> D[Analysis]
    C --> E[Ring]
    C --> F[Group]
</mermaid>

* 使用<code>namespace</code>/<code>end</code>划分逻辑单元
* 嵌套命名空间用<code>.</code>分隔
* 避免全局命名污染

<syntaxhighlight lang="lean">
namespace LinearAlgebra

def dot_product (u v : Vector ℝ) : ℝ := 
  ∑ i, u[i] * v[i]

end LinearAlgebra
</syntaxhighlight>

== 数学符号命名 ==
对于数学结构，Lean支持Unicode符号命名：

{| class="wikitable"
! 符号 !! 命名规则 !! 示例
|-
| <math>\forall</math> || <code>\all</code> || <code>∀ x, P x</code>
|-
| <math>\exists</math> || <code>\ex</code> || <code>∃ x, x > 0</code>
|-
| <math>\times</math> || <code>\times</code> || <code>ℕ × ℤ</code>
|}

== 实际案例 ==
观察Mathlib中的典型命名：

<syntaxhighlight lang="lean">
-- Data.List.Basic
theorem map_map {α β γ : Type} (g : β → γ) (f : α → β) (xs : List α) :
  (xs.map f).map g = xs.map (g ∘ f) := by
  induction xs <;> simp [*]

-- Algebra.Group.Defs
class Group (G : Type u) extends Mul G, One G, Inv G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)
  one_mul : ∀ a : G, 1 * a = a
  mul_one : ∀ a : G, a * 1 = a
  mul_left_inv : ∀ a : G, a⁻¹ * a = 1
</syntaxhighlight>

== 常见错误 ==
{| class="wikitable"
! 错误示例 !! 问题 !! 修正方案
|-
| <code>def f (x : Nat) := x+1</code> || 无意义名称 || <code>def succ (n : Nat) := n+1</code>
|-
| <code>structure myTp</code> || 错误大小写 || <code>structure MyType</code>
|-
| <code>def λ (x : α) : α := x</code> || 使用关键字 || <code>def id_func (x : α) : α := x</code>
|}

== 最佳实践总结 ==
# 始终优先选择描述性名称
# 遵循社区既定约定（如Mathlib规范）
# 在局部作用域允许简短命名
# 定期使用<code>#lint</code>检查命名问题
# 保持与依赖库的命名风格一致

通过系统遵循这些规则，您的Lean代码将获得更好的可维护性和数学表达力。

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