Lean基本操作符

简介[编辑 | 编辑源代码]

Lean基本操作符是Lean定理证明器中进行逻辑运算、数学计算和类型操作的基础符号系统。这些操作符构成了Lean语言的核心表达力，涵盖了从简单的算术运算到复杂的类型论构造。理解这些操作符对于编写正确的Lean代码和形式化数学证明至关重要。

算术操作符[编辑 | 编辑源代码]

Lean支持标准的数学运算符号，其优先级和结合性与常规数学一致：

-- 基本算术运算
#eval 2 + 3   -- 加法，输出5
#eval 5 - 2   -- 减法，输出3
#eval 4 * 3   -- 乘法，输出12
#eval 9 / 2   -- 除法，输出4.5
#eval 9 % 2   -- 取模，输出1
#eval 2 ^ 3   -- 幂运算，输出8

比较操作符[编辑 | 编辑源代码]

比较操作符返回布尔值(`true`/`false`)：

#eval 3 = 3   -- 等于，输出true
#eval 3 ≠ 2   -- 不等于(Unicode符号)，输出true
#eval 3 < 5   -- 小于，输出true
#eval 4 > 4   -- 大于，输出false
#eval 4 ≤ 5  -- 小于等于(Unicode符号)，输出true
#eval 4 ≥ 5  -- 大于等于(Unicode符号)，输出false

逻辑操作符[编辑 | 编辑源代码]

Lean使用标准逻辑操作符，注意短路求值特性：

#eval true ∧ false  -- 逻辑与，输出false
#eval true ∨ false  -- 逻辑或，输出true
#eval ¬true         -- 逻辑非，输出false

-- 短路求值示例
def willCrash : Bool := (1/0 = 0)  -- 会崩溃
#eval false ∧ willCrash  -- 输出false，不会计算willCrash

类型论操作符[编辑 | 编辑源代码]

Lean作为依赖类型语言，有特殊的类型操作符：

-- 函数类型箭头
#check Nat → Nat  -- 输入Nat返回Nat的函数类型

-- 依赖乘积类型(Pi类型)
#check ∀ (n : Nat), n = n  -- 全称量化命题

-- 类型宇宙层级
#check Type   -- Type : Type 1
#check Type 1 -- Type 1 : Type 2

集合论操作符[编辑 | 编辑源代码]

处理集合和关系时常用：

-- 集合成员关系
#check 1 ∈ ({1, 2, 3} : Set Nat)

-- 子集关系
#check {1, 2} ⊆ {1, 2, 3}

-- 集合运算
#check {1, 2} ∪ {2, 3}  -- 并集
#check {1, 2} ∩ {2, 3}  -- 交集

高阶操作符[编辑 | 编辑源代码]

这些操作符在函数式编程中特别重要：

-- 函数组合
def double (x : Nat) := x * 2
def square (x : Nat) := x * x
#check double ∘ square  -- 函数组合类型为Nat → Nat

-- 柯里化/反柯里化
#check fun x y => x + y      -- Nat → Nat → Nat
#check fun (p : Nat × Nat) => p.1 + p.2  -- Nat × Nat → Nat

优先级与结合性[编辑 | 编辑源代码]

Lean操作符的优先级和结合性规则如下表所示：

实际应用案例[编辑 | 编辑源代码]

数学证明示例[编辑 | 编辑源代码]

example (a b : Nat) : a + b = b + a := by
  apply Nat.add_comm  -- 使用加法交换律

算法实现示例[编辑 | 编辑源代码]

def isPrime (n : Nat) : Bool :=
  if n < 2 then false
  else
    let rec check (i : Nat) : Bool :=
      if i * i > n then true
      else if n % i = 0 then false
      else check (i + 1)
    check 2

常见错误与陷阱[编辑 | 编辑源代码]

1. 混淆=和:=：

  - `=`用于命题等式
  - `:=`用于定义绑定

2. 忽略操作符优先级：

   #eval 1 + 2 * 3   -- 输出7，不是9

3. 过度依赖Unicode：虽然美观但可能降低可读性：

   -- 可读性较差
   #check ∀ ε > 0, ∃ δ > 0, ∀ x, |x| < δ → |f x| < ε

高级主题[编辑 | 编辑源代码]

自定义操作符[编辑 | 编辑源代码]

Lean允许定义新操作符：

infixl:65 " ⊕ " => fun x y => x + y + 1
#eval 2 ⊕ 3  -- 输出6

重载操作符[编辑 | 编辑源代码]

通过类型类可以重载操作符：

instance : Mul Nat where
  mul a b := a + b  -- 将*重载为加法(仅为示例)

#eval 2 * 3  -- 输出5

总结[编辑 | 编辑源代码]

Lean的操作符系统结合了传统数学符号和类型论特有的构造，提供了丰富的表达力。掌握这些操作符需要理解：

基础算术和逻辑操作符
类型论特有的构造(如∀和→)
操作符优先级和结合性规则
自定义和重载操作符的能力

通过实践和不断练习，这些操作符将成为形式化数学和编程的强大工具。