Lean命名规则

Lean命名规则

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

核心原则

Lean的命名规则遵循以下核心原则：

• 语义清晰：名称应准确反映实体用途（如list_length优于n）
• 一致性：同类实体使用相同命名模式（如类型参数总用希腊字母）
• 可读性：避免缩写歧义（推荐index而非idx）
• 层级表达：通过命名体现抽象层次（基础函数用全称，局部变量可简化）

基本规范

1. 变量与函数

• 使用蛇形命名法（snake_case）
• 名称应为完整英文单词或标准数学符号
• 避免单字符命名（数学公式除外）

-- 推荐
def square_root (x : Float) : Float := 
  Float.sqrt x

-- 不推荐
def sqrt (n : Float) : Float := 
  Float.sqrt n

2. 类型与构造子

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

-- 正确示例
inductive BinaryTree (α : Type) where
  | Leaf 
  | Node (left : BinaryTree α) (value : α) (right : BinaryTree α)

3. 类型参数

• 使用希腊字母表示类型参数
• 常见约定：
  • α β γ：任意类型
  • ι：索引类型
  • σ τ：状态类型

def swap_pair {α β : Type} (p : α × β) : β × α := 
  (p.2, p.1)

特殊约定

1. 定理命名

• 使用描述性名称表达定理内容
• 常见模式：
  • noun_verb_property（如list_reverse_involutive）
  • property_of_noun（如commutativity_of_add）

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]

2. 类型类实例

• 添加inst前缀
• 遵循inst[ParentClass]_[Description]模式

instance instMonadOption : Monad Option where
  pure x := some x
  bind mx f := Option.bind mx f

命名空间管理

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

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

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

namespace LinearAlgebra

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

end LinearAlgebra

数学符号命名

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

符号	命名规则	示例
$\mathrm{\forall }$	\all	∀ x, P x
$\mathrm{\exists }$	\ex	∃ x, x > 0
$\times$	\times	ℕ × ℤ

实际案例

观察Mathlib中的典型命名：

-- 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

常见错误

错误示例	问题	修正方案
def f (x : Nat) := x+1	无意义名称	def succ (n : Nat) := n+1
structure myTp	错误大小写	structure MyType
def λ (x : α) : α := x	使用关键字	def id_func (x : α) : α := x

最佳实践总结

1. 始终优先选择描述性名称
2. 遵循社区既定约定（如Mathlib规范）
3. 在局部作用域允许简短命名
4. 定期使用#lint检查命名问题
5. 保持与依赖库的命名风格一致

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