编辑“︁Lean基本操作符”︁

{{DISPLAYTITLE:Lean基本操作符}}

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

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

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

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

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

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

<syntaxhighlight lang="lean">
#eval true ∧ false  -- 逻辑与，输出false
#eval true ∨ false  -- 逻辑或，输出true
#eval ¬true         -- 逻辑非，输出false

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

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

<syntaxhighlight lang="lean">
-- 函数类型箭头
#check Nat → Nat  -- 输入Nat返回Nat的函数类型

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

-- 类型宇宙层级
#check Type   -- Type : Type 1
#check Type 1 -- Type 1 : Type 2
</syntaxhighlight>

== 集合论操作符 ==
处理集合和关系时常用：

<syntaxhighlight lang="lean">
-- 集合成员关系
#check 1 ∈ ({1, 2, 3} : Set Nat)

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

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

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

<syntaxhighlight lang="lean">
-- 函数组合
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
</syntaxhighlight>

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

<mermaid>
flowchart LR
    A["最高优先级"] --> B[函数应用]
    B --> C[一元操作符 - ~ ¬]
    C --> D[^]
    D --> E[* / %]
    E --> F[+ -]
    F --> G[::]
    G --> H[++]
    H --> I[关系操作符 = ≠ < > ≤ ≥ ∈ ⊆]
    I --> J[∧]
    J --> K[∨]
    K --> L[→]
    L --> M["最低优先级: ↔"]
</mermaid>

== 实际应用案例 ==
=== 数学证明示例 ===
<syntaxhighlight lang="lean">
example (a b : Nat) : a + b = b + a := by
  apply Nat.add_comm  -- 使用加法交换律
</syntaxhighlight>

=== 算法实现示例 ===
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 常见错误与陷阱 ==
1. '''混淆=和:='''：
   - `=`用于命题等式
   - `:=`用于定义绑定

2. '''忽略操作符优先级'''：
   <syntaxhighlight lang="lean">
   #eval 1 + 2 * 3   -- 输出7，不是9
   </syntaxhighlight>

3. '''过度依赖Unicode'''：虽然美观但可能降低可读性：
   <syntaxhighlight lang="lean">
   -- 可读性较差
   #check ∀ ε > 0, ∃ δ > 0, ∀ x, |x| < δ → |f x| < ε
   </syntaxhighlight>

== 高级主题 ==
=== 自定义操作符 ===
Lean允许定义新操作符：
<syntaxhighlight lang="lean">
infixl:65 " ⊕ " => fun x y => x + y + 1
#eval 2 ⊕ 3  -- 输出6
</syntaxhighlight>

=== 重载操作符 ===
通过类型类可以重载操作符：
<syntaxhighlight lang="lean">
instance : Mul Nat where
  mul a b := a + b  -- 将*重载为加法(仅为示例)

#eval 2 * 3  -- 输出5
</syntaxhighlight>

== 总结 ==
Lean的操作符系统结合了传统数学符号和类型论特有的构造，提供了丰富的表达力。掌握这些操作符需要理解：
* 基础算术和逻辑操作符
* 类型论特有的构造(如∀和→)
* 操作符优先级和结合性规则
* 自定义和重载操作符的能力

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

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