函数 · Lean 4 从入门到精通

lambda 与 fun、三种参数绑定（显式/隐式/实例）、命名参数与默认值、递归与终止性。

定义方式

-- 1. def
def double (n : Nat) : Nat := n * 2

-- 2. lambda（匿名函数）
def double' : Nat → Nat := fun n => n * 2

-- 3. λ 是 fun 的同义词
def double'' : Nat → Nat := λ n => n * 2

Lean 4 用 =>，不是 Lean 3 的逗号。

fun n => n * 2      -- ✅ Lean 4
-- λ n, n * 2       -- ❌ Lean 3 语法，报错

这是从 Lean 3 教程迁移时最先撞上的差异。

多参数 lambda：

#check fun (a b : Nat) => a + b     -- Nat → Nat → Nat
#eval  (fun a b => a + b) 3 4       -- 7

三种参数绑定

这是 Lean 与多数语言最不同的地方之一。

括号	名称	调用时
`(x : α)`	显式	必须给
`{x : α}`	隐式	由 Lean 从其他参数推断
`[Inst α]`	实例隐式	由类型类推断求解
`⦃x : α⦄`	严格隐式	仅当后面还有显式参数时才推断

隐式参数

def myId {α : Type} (a : α) : α := a

#eval myId 42          -- 不用写 α，Lean 从 42 推断出 Nat
#eval myId "hi"

如果 α 是显式的，每次调用都要写 myId Nat 42——极其啰嗦。类型参数几乎总是隐式的。

需要显式指定时，用 @ 关闭所有隐式：

#check @myId               -- {α : Type} → α → α
#eval  @myId Nat 42        -- 42

或用命名参数只指定某一个：

#eval myId (α := Nat) 42

@ 是排查类型问题的利器。 当 Lean 推断出你不期望的隐式参数时，@f 能看到完整签名，#check @f 常常一眼看出问题。

实例隐式

def sum3 [Add α] (a b c : α) : α := a + b + c

[Add α] 表示「需要 α 上的加法实例，由类型类系统去找」。详见类型类。

命名参数与默认值

def greet (name : String) (greeting : String := "Hello") : String :=
  s!"{greeting}, {name}!"

#eval greet "Lean"                      -- "Hello, Lean!"
#eval greet "Lean" "Hi"                 -- "Hi, Lean!"
#eval greet (name := "Lean") (greeting := "Hey")

:= 在参数位置表示默认值。命名参数还允许乱序传参。

另有自动填充的参数：

def f (n : Nat) (h : n > 0 := by decide) : Nat := n

:= by tactic 表示「这个参数由该 tactic 自动构造」——常用于自动满足的证明义务。

模式匹配

def isZero : Nat → Bool
  | 0     => true
  | _ + 1 => false

方程式风格：直接对参数分情况，不写 fun。这是 Lean 里最常用的函数定义方式。

match 表达式形式：

def isZero' (n : Nat) : Bool :=
  match n with
  | 0     => true
  | _ + 1 => false

多参数同时匹配：

def bothZero : Nat → Nat → Bool
  | 0, 0 => true
  | _, _ => false

匹配是穷尽性检查的——漏掉情况会报错：

def bad : Nat → Bool
  | 0 => true
  -- error: missing cases: (Nat.succ _)

这是 Lean 相对多数语言的重要保障：不可能有「忘记处理某个 case」的 bug。

递归与终止性

def factorial : Nat → Nat
  | 0     => 1
  | n + 1 => (n + 1) * factorial n

Lean 必须确信递归会终止——否则可以构造出任意命题的「证明」，系统就不一致了。

结构递归（参数严格变小）会被自动接受。复杂情况需要帮忙：

termination_by

def gcd' (a b : Nat) : Nat :=
  if h : b = 0 then a
  else gcd' b (a % b)
termination_by b
decreasing_by
  simp_wf
  exact Nat.mod_lt _ (Nat.pos_of_ne_zero h)

termination_by 指出「哪个量在变小」。
decreasing_by 提供「它确实在变小」的证明。

写不出终止性证明时，先怀疑函数本身。 大多数情况下是递归结构确实有问题，而不是 Lean 太笨。

实在需要非终止函数（如解释器主循环），用 partial def：

partial def loop (n : Nat) : Nat := loop (n + 1)

代价是该函数不能用于证明——Lean 不会展开它的定义，只把它当一个不透明的黑箱。写程序可以，写数学不行。

结构化递归的辅助

def fib : Nat → Nat
  | 0     => 0
  | 1     => 1
  | n + 2 => fib n + fib (n + 1)

多步的结构递归 Lean 也能自动处理。

要注意这个朴素实现是指数复杂度——#eval fib 40 会跑很久。高效版本用累加器：

def fibFast (n : Nat) : Nat :=
  go n 0 1
where
  go : Nat → Nat → Nat → Nat
    | 0,     a, _ => a
    | n + 1, a, b => go n b (a + b)

where 定义局部辅助函数——比在顶层污染命名空间干净。

也可以用 let rec：

def fibFast' (n : Nat) : Nat :=
  let rec go : Nat → Nat → Nat → Nat
    | 0,     a, _ => a
    | n + 1, a, b => go n b (a + b)
  go n 0 1

函数组合与管道

def addOne (n : Nat) : Nat := n + 1
def timesTwo (n : Nat) : Nat := n * 2

#eval (addOne ∘ timesTwo) 5     -- 11  先 ×2 再 +1
#eval (5 |> timesTwo |> addOne) -- 11  管道，从左往右读
#eval addOne <| timesTwo 5      -- 11  <| 相当于省括号

记号	输入	含义
`∘`	`\comp`	函数组合，右边先执行
`\|>`	直接打	管道，左边的值送进右边的函数
`<\|`	直接打	反向应用，避免写括号

<| 特别有用——它让 f (g (h x)) 可以写成 f <| g <| h x。

匿名构造子与投影

structure Point where
  x : Nat
  y : Nat

def p : Point := ⟨1, 2⟩       -- 匿名构造子，⟨⟩ 是 \< \>
#eval p.x                      -- 1，点记法投影
#eval p.1                      -- 1，位置投影

. 记法有个强大的用法叫广义字段记法：

def l : List Nat := [1, 2, 3]
#eval l.length          -- 等价于 List.length l
#eval l.map (· * 2)     -- 等价于 List.map (· * 2) l

x.f a 会被解释成 T.f x a（T 是 x 的类型）。这让代码读起来像面向对象，实际是纯函数调用。

中心点记法

#eval [1, 2, 3].map (· * 2)        -- [2, 4, 6]
#eval [1, 2, 3].filter (· > 1)     -- [2, 3]

·（\.）是占位符，(· * 2) 等价于 fun x => x * 2。作用域是最近的括号：

(· + ·)          -- fun a b => a + b
(f · x)          -- fun a => f a x

写短 lambda 时非常简洁，是 Lean 代码里的常见风格。

下一篇：归纳类型与结构体。

函数

本页目录