3.3.1. 例 1：Nat.add 2 3🔗

app
├── app
│   ├── const `Nat.add []
│   └── lit (Literal.natVal 2)
└── lit (Literal.natVal 3)

Lean 4 中多参数函数是 curried 的：f a b 表示为 app (app f a) b。

3.3.2. 例 2：fun n : Nat => n + 1🔗

lam `n (const `Nat [])
  (app (app (const `HAdd.hAdd [...]) (bvar 0)) (lit 1))
  BinderInfo.default

注意 body 中用 bvar 0 指代最近的绑定变量 n——这是 de Bruijn 索引。

3.3.3. 例 3：∀ n : Nat, n = n🔗

forallE `n (const `Nat [])
  (app (app (app (const `Eq [...]) (const `Nat [])) (bvar 0)) (bvar 0))
  BinderInfo.default

∀ 和 → 都用 forallE；如果 body 不引用绑定变量（即 bvar 0 不出现），那就是 →。

3.4.1. match_expr🔗

match_expr goalType with
| Eq α lhs rhs =>
  -- goalType 是 @Eq α lhs rhs
  logInfo m!"This is an equality: {← ppExpr lhs} = {← ppExpr rhs}"
| And p q =>
  -- goalType 是 And p q
  logInfo m!"This is a conjunction"
| _ =>
  logInfo m!"Unknown shape"

match_expr 按 head constant 匹配：Eq α lhs rhs 匹配 @Eq α lhs rhs，自动解开所有 app。

3.4.2. let_expr🔗

用于 do 块中的 pattern matching（类似 let some x := ... | return）：

let_expr Eq α lhs rhs := goalType | throwError "not an equality"
-- 到这里 lhs, rhs 就是绑定好的 Expr

let_expr 在 tactic 代码中用得更多，因为失败时可以直接跳出。

3.5.1. 手动构造🔗

-- 构造 @Eq Nat a b
let eqExpr := mkApp3 (mkConst ``Eq) (mkConst ``Nat) a b

-- 构造 @Eq.refl Nat a  (即 rfl 的证明项)
let rflExpr := mkApp2 (mkConst ``Eq.refl) (mkConst ``Nat) a

常用构造函数：

• mkConst n：常量引用

• mkApp f a：单参数应用

• mkApp2/3/4/5/6：多参数应用

• mkAppN f #[a,b,c]：数组参数应用

• mkLambda n bi t body：构造 λ 表达式

• mkForall n bi t body：构造 ∀ 表达式

3.5.2. 用引号构造（quotation）🔗

在 TermElabM / TacticM 中，可以用 quotation + elabTerm 从语法直接构造：

let e ← elabTerm (← `(Nat.add 2 3)) none
-- e 是精化后的 Expr

这更方便，但有额外开销（要走一遍 elaboration）。在性能敏感的 tactic 中，手动 mkApp 更好。

3.7.1. 类型相关🔗

inferType (e : Expr) : MetaM Expr         -- 推断 e 的类型
isDefEq (a b : Expr) : MetaM Bool          -- a 和 b 定义等价？（可能触发 unification）
whnf (e : Expr) : MetaM Expr               -- 弱头范式
isProof (e : Expr) : MetaM Bool            -- e 是证明项？
isProp (e : Expr) : MetaM Bool             -- e 的类型是 Prop？

3.7.2. 结构分析🔗

Expr.getAppFn (e : Expr) : Expr            -- 获取应用头（剥掉所有 app）
Expr.getAppArgs (e : Expr) : Array Expr    -- 获取所有参数
Expr.isApp (e : Expr) : Bool               -- 是 app？
Expr.isConst (e : Expr) : Bool             -- 是 const？
Expr.constName (e : Expr) : Name           -- const 的名字（前提：isConst）

3.7.3. 替换与遍历🔗

kabstract (e : Expr) (t : Expr) : MetaM Expr  -- 把 e 中匹配 t 的子项抽象为 bvar（支持 occurrences 控制）
replace (e : Expr) (f : Expr → Option Expr) : Expr  -- 自定义替换
Expr.foldlM (init : α) (f : α → Expr → MetaM α) (e : Expr) : MetaM α  -- 遍历

3.9.1. 失败 1：match_expr 匹配不上，明明目标看起来是对的🔗

match_expr 按 head constant 匹配，但 whnf 没有自动调用。如果目标被 let 或 abbrev 包了一层，需要先 whnf：

-- [示意]
let target ← whnf (← goal.getType)  -- 先规约
match_expr target with
| Eq α lhs rhs => ...
| _ => throwError "not an equality"

3.9.2. 失败 2：Expr.constName panic🔗

constName 在表达式不是 const 时会 panic。安全做法是先检查：

-- [示意]
if e.isConst then
  let name := e.constName
  ...

或用 Expr.constName? 返回 Option Name。

3.9.3. 失败 3：fvar 泄漏出 telescope 回调🔗

forallTelescope 里创建的 fvar 只在回调内有效。如果你把它存到外面的变量里再使用，会得到 unknown free variable 错误。

-- [示意] 错误做法
let mut leaked : Expr := default
forallTelescope goalType fun fvars body => do
  leaked := fvars[0]!  -- ❌ fvar 会在回调结束后失效
-- 在这里用 leaked 会出错

正确做法：把需要的结果在回调内计算完，只返回不含 fvar 的值。

3.9.4. 失败 4：手动 mkApp 参数个数错🔗

mkApp3 (mkConst Eq) a b 会构造出类型错误的表达式（Eq 需要 3 个参数：类型 α、lhs、rhs）。这类错误不会立即 panic，而是在后续 isDefEq 或 check 时才报 type mismatch。

建议：用 mkEq、mkEqRefl 等高层 API，而不是手动数参数。

3.10.1. 练习 2.1（热身）：用 #check @Eq 观察 Expr 结构🔗

在 VS Code 中运行：

观察每个常量需要几个参数。这能帮你理解为什么 match_expr 写 Eq α lhs rhs（3 个参数）而 And p q（2 个参数）。

3.10.2. 练习 2.2（热身）：打印目标的 head constant🔗

写一个 tactic，打印当前目标的 head constant 名字：

import Lean
open Lean Elab Tactic Meta

和 Ch1 的 trace_goal 一样，这类只打印信息不改变目标的 tactic 可能触发 "tactic does nothing" 警告，可以忽略。

3.10.3. 练习 2.3（debug）：找出 match_expr 失败的原因🔗

以下 tactic 想匹配 ∀ x, P x 形式的目标，但总是走到 _ 分支。为什么？

-- 这段代码有逻辑错误
import Lean
open Lean Elab Tactic Meta

elab "check_forall" : tactic => do
  let goal ← getMainGoal
  goal.withContext do
    let target ← goal.getType
    match_expr target with
    | ForAll _ _ => logInfo "Found a forall!"
    | _ => logInfo "Not a forall"

example : ∀ n : Nat, n = n := by
  check_forall   -- 为什么输出 "Not a forall"？
  intro n; rfl

提示：match_expr 匹配的是 head constant（如 Eq、And），而 ∀ 不是一个常量——它是 Expr.forallE 构造子。要检查 ∀，应该用普通的 Expr.isForall 或直接 match 构造子。

3.10.4. 练习 2.4（综合）：实现 show_structure tactic🔗

写一个 show_structure tactic，对当前目标做以下分类并打印：

• 如果是等式 a = b：打印 "Equality: {a} = {b}"

• 如果是合取 P ∧ Q：打印 "Conjunction: {P} ∧ {Q}"

• 如果是 ∀ 类型：打印 "Forall" 和绑定变量的类型

• 否则：打印 "Other: {target}"

测试用例：

-- [可运行] 实现 show_structure 后测试
example : 1 + 1 = 2 := by show_structure; norm_num
example : True ∧ True := by show_structure; exact ⟨trivial, trivial⟩
example : ∀ n : Nat, n = n := by show_structure; intro n; rfl
example : True := by show_structure; trivial

下一章：用 Expr 和 TacticM 写出你的第一个有用的 tactic。