Ltac 解决了"把 tactic 序列抽象成可复用脚本"的问题，但它是一门无类型的动态语言——变量绑定在运行时才解析，错误在 backtracking 时悄悄吞掉，定义期不做任何静态检查。Ltac2 是 Coq 8.14 引入、8.19 稳定下来的替代方案，把 tactic 编程从"解释型脚本"升级为"有类型的函数式语言"。本篇是系列第 08 篇，前置阅读建议先过一遍《深入 Coq 02：目标窗口与 tactic 交互模型》和第 07 篇（Ltac 编程：match goal/repeat/try/first/solve）。

Ltac 的动态类型问题

Ltac 的 match goal 子句在运行时匹配当前目标，成功的子句继续执行，失败的子句触发 backtracking 退到上一个选择点。这套设计对于简单的"try 一批 tactic，哪个行用哪个"场景相当便利，但有几类问题在复杂 tactic 里难以调试。

变量绑定完全动态是其中一个根本问题。Ltac 里的 ?x 是 pattern variable，绑定到证明项中的子术语；x 也可以是外部 Gallina 项，二者在语法层面无法区分，只靠运行时上下文决定。

错误模式不透明是另一个常见陷阱。下面这段 Ltac 会在 bar 失败时静默 backtrack 到 foo，而不给出任何提示：

1
2
Ltac my_tac :=
  first [ bar | foo ].

如果 bar 本应成功但因为内部某个 tactic 名拼错而抛出"No such tactic"，first 会把这个错误当作普通失败处理，最终用 foo 的结果掩盖掉真正的 bug。

Ltac 函数同样不做参数类型检查。Ltac f x := ... 里的 x 可以传任何东西——constr、ident、tactic，全部合法，运行时才爆。

Ltac2 对这三类问题的回答是：引入一套 ML 风格的静态类型系统，让错误尽可能在定义时暴露，而不是在某个大型证明的第 300 步 backtrack 后才出现。

Ltac2 基础语法

Ltac2 需要导入标准库才能使用完整功能集：

1
2
From Ltac2 Require Import Ltac2.
From Ltac2 Require Import Message.

From Ltac2 Require Import Ltac2 同时导入 Ltac2.Init 和最常用的操作原语。

函数定义

1
2
Ltac2 greet () :=
  Message.print (Message.of_string "hello from Ltac2").

greet 的类型是 unit -> unit。括号里的 () 是 ML 风格的 unit 参数，Ltac2 函数必须显式接受 unit 才能"延迟求值"——若写成 Ltac2 greet := ...，则 greet 是一个值，而非一个延迟执行的 tactic。

调用：

1
2
3
4
Goal True.
  ltac2:(greet ()).
  trivial.
Qed.

ltac2:(...) 是在传统 tactic 证明脚本里嵌入 Ltac2 表达式的语法。

核心类型

Ltac2 的类型系统覆盖了 tactic 编程所需的几类基本值：

类型 说明 示例
unit 无信息值，tactic 的默认返回类型 ()
constr Gallina 表达式（证明项或类型） '(1 + 1 = 2)
ident 标识符 @foo
int 机器整数 42
string 字符串 "hello"
'a list 多态列表 [1; 2; 3]
'a option 可选值 Some x, None
exn 异常 Tactic_failure None

constr 是 Ltac2 里最特殊的类型。Gallina 表达式在 Ltac2 里用反引号包裹：`(nat)、`(forall n : nat, n + 0 = n)。在文字上下文里也可以用单引号：'nat、'(S n)。

变量绑定与作用域

Ltac2 的局部变量用 let ... in 引入，和 OCaml 语法完全对齐：

1
2
3
4
5
Ltac2 show_type (t : constr) : unit :=
  let msg := Message.concat
               (Message.of_string "type: ")
               (Message.of_constr t) in
  Message.print msg.

这里 t 是静态类型为 constr 的参数，传错类型在定义时就会报错，而不是在运行时抛出神秘的 Ltac failure。

模式匹配 constr 与 goal

Ltac2 的 match! 和 match! goal 是对应 Ltac match 和 match goal 的带类型版本。

匹配 constr

1
2
3
4
5
Ltac2 is_nat_eq (t : constr) : bool :=
  match! t with
  | @eq nat _ _ => true
  | _           => false
  end.

@eq nat _ _ 是带显式参数的模式，匹配形如 x = y（x y 类型为 nat）的 Gallina 项。_ 是通配符，不绑定变量。

匹配目标

1
2
3
4
5
6
7
Ltac2 clear_trivial_hyps () : unit :=
  match! goal with
  | [ h : True |- _ ] =>
      let h' := Control.hyp h in
      Std.clear [h]
  | [ |- _ ] => ()
  end.

Control.hyp h 把假设名称 h（类型 ident）解引用为对应的 constr。Std.clear 对应 Ltac 里的 clear tactic，但接受 ident list 而非字符串。

注意这里没有 Ltac 的隐式 backtracking——Ltac2 的 match! 只匹配第一个成功分支，不会在当前分支失败后自动尝试下一个。如果需要 backtracking 语义，要显式用 Control.backtrack_tactic_failure。

错误处理：显式而非静默

Ltac2 用 ML 标准的异常机制处理错误，而不是通过 backtracking 吞掉失败。

Ltac 的静默失败

1
2
3
(* Ltac 版本：apply_or_assumption *)
Ltac apply_or_assumption term :=
  first [ apply term | assumption ].

如果 term 拼错成不存在的名字，apply term 抛出"No such lemma"，first 把它当作普通失败，然后尝试 assumption。最终证明可能意外通过，但用的是 assumption 而非预期的 apply term，只有证明项审计才能发现差异。

Ltac2 的显式错误

1
2
3
4
5
6
7
8
Ltac2 apply_or_assumption (term : constr) : unit :=
  Control.plus
    (fun () => Std.apply true true [(term, Std.NoBindings)] None)
    (fun e  =>
       match e with
       | Tactic_failure _ => Std.assumption ()
       | _                => Control.zero e
       end).

Control.plus 是 Ltac2 的 backtracking 组合子：第一个参数先执行，失败后把异常传给第二个参数的 handler。handler 里对异常做模式匹配——只有 Tactic_failure 类型的错误才走 assumption，其他错误（如 Not_found、Constr.cast 类型不匹配等）重新抛出。这样，把 lemma 名拼错会在调用点产生清晰的错误，而不是静默降级。

Ltac vs Ltac2：对照示例

以"对所有假设尝试 exact"为例对比两种写法。

Ltac 版本

1
2
3
4
Ltac exact_any :=
  match goal with
  | [ h : ?T |- ?T ] => exact h
  end.

这段代码没有类型信息，?T 是 unification variable，匹配运行时目标类型。如果多个假设类型相同，Ltac 会按顺序 backtrack 尝试，但不保证选择顺序，也不报告"哪个假设被用了"。

Ltac2 版本

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Ltac2 exact_any () : unit :=
  let hyps := Control.hyps () in
  let rec try_hyps hs :=
    match hs with
    | []      => Control.zero (Tactic_failure (Some (Message.of_string "no matching hyp")))
    | h :: rest =>
        let (name, _, ty) := h in
        Control.plus
          (fun () =>
             let goal := Control.goal () in
             if Constr.equal ty goal
             then Std.exact false (Control.hyp name)
             else Control.zero (Tactic_failure None))
          (fun _ => try_hyps rest)
    end
  in
  try_hyps hyps.

Control.hyps () 返回类型为 (ident * constr option * constr) list 的假设列表，每项是 (名称, body, 类型) 三元组。Constr.equal 做语法等价检查（不做 unification）。整个函数的类型签名在定义时就固定下来。

捕获定义时错误

Ltac2 的类型检查在定义处理时运行，类型不匹配直接阻断编译，不等到 tactic 被调用：

1
2
3
4
(* 错误示例：类型不匹配 *)
Ltac2 bad_tac (n : int) : unit :=
  Std.exact false n.
  (* 错误：Std.exact 期望 constr，得到 int *)

对应的 Ltac 写法：

1
2
3
4
(* Ltac 版本：定义时不报错 *)
Ltac bad_tac n :=
  exact n.
(* 运行时才会报 "not a term" *)

以 “检查目标是否是 _ /\ _ 并条件性拆开” 为例，说明这一差异。

失败尝试（Ltac2 定义时报错）：

1
2
3
4
5
6
7
8
9
(* 尝试用 constr 模式匹配来决定是否 split *)
Ltac2 maybe_split () : unit :=
  let g := Control.goal () in
  match! g with
  | ?a /\ ?b =>
      (* 错误：a 和 b 是 constr，但这里写成了 Gallina 变量 *)
      split
  | _ => ()
  end.

上面这段代码本身结构正确，但若忘记导入 Ltac2.Notations 而直接使用 split（普通 tactic 名），Coq 8.19 会报 Unbound value split——因为在 Ltac2 上下文里，split 不是自动可见的 Ltac1 tactic，需要显式桥接或使用 Std.split。

正确解法：

1
2
3
4
5
6
Ltac2 maybe_split () : unit :=
  let g := Control.goal () in
  match! g with
  | _ /\ _ => Std.split (Std.ByValue None)
  | _       => ()
  end.

Std.split 接受一个 Std.or_and_intro_pattern option，传 Std.ByValue None 表示不指定 intro 模式，直接生成两个子目标，等价于原生 tactic split。

互操作：Ltac 与 Ltac2 相互调用

Ltac2 提供了双向桥接机制，存量的 Ltac 代码不需要全量重写。

Ltac2 调用 Ltac1

1
2
Ltac2 call_ltac1 () : unit :=
  ltac1:(omega).

ltac1:(...) 引入一段 Ltac1 代码片段。括号内是完整的 Ltac1 tactic 表达式，返回 unit（忽略 Ltac1 的结果）。

传递 Ltac2 变量给 Ltac1：

1
2
Ltac2 apply_via_ltac1 (t : constr) : unit :=
  ltac1:(t |- apply t) (Ltac1.of_constr t).

Ltac1.of_constr 把 constr 封装为 Ltac1 值，注入到 ltac1:(...) 的绑定列表里。

Ltac1 调用 Ltac2

1
2
Ltac call_ltac2 :=
  ltac2:(maybe_split ()).

ltac2:(...) 在 Ltac1 上下文里嵌入 Ltac2 代码，和前面在普通 Goal 证明里的用法一致。

Show Proof 与证明项审计

在 Ltac2 驱动的证明里，Show Proof. 同样有效，证明项与 tactic 无关，最终都是 Gallina 项：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
Goal forall (P Q : Prop), P /\ Q -> Q /\ P.
Proof.
  ltac2:(
    intro P; intro Q; intro H;
    destruct H as [hp hq];
    split;
    [ exact hq | exact hp ]
  ).
  Show Proof.
  (* 输出类似：
     fun (P Q : Prop) (H : P /\ Q) =>
       match H with
       | conj hp hq => conj hq hp
       end
  *)
Qed.

Print Assumptions. 可以检查证明是否悄悄依赖了公理：

1
2
Print Assumptions Nat.add_comm.
(* 输出：Closed under the global context *)

如果输出 Closed under the global context，说明证明不依赖任何额外公理，仅由 CIC 内置规则推导。若输出包含 Classical.classic 或 FunctionalExtensionality.functional_extensionality_dep，则说明用了经典逻辑或函数外延性公理。

生态现状

Coq 8.14 引入 Ltac2 实验特性，8.19（2024 年发布）将其标记为稳定。当前状态：

  • coq-stdlib 的部分 tactic 开始用 Ltac2 重写，例如 Tactics.v 里的若干辅助 tactic。
  • MathComp 2.x 尚未大规模迁移，仍以 SSReflect + Ltac1 为主，但社区已有零星 Ltac2 封装层。
  • coq-ltac2 独立包已并入 Coq 核心，不需要额外 opam 安装，From Ltac2 Require Import Ltac2 即可使用。
  • Coq Platform（一键安装包）8.19 版本包含完整 Ltac2 支持。

现阶段的实际建议：对新写的 tactic 库优先用 Ltac2，尤其是涉及术语操作（constr 解构、ident 列表遍历）的场景；对已有的 Ltac1 tactic 库，通过 ltac2:(...) / ltac1:(...) 桥接逐步迁移，不必一次性重写。

练习

练习 1

用 Ltac2 编写 auto_intro，功能：若当前目标以 forall 开头，则执行 intro，否则不做任何操作。要求在 Ltac2 定义时通过类型检查（不能用 ltac1:(intro) 绕过）。

提示：Control.goal () 返回当前目标的 constr；用 match! ... with | forall _ : _, _ => ... | _ => () end 匹配 forall 形式。

练习 2

用 Ltac2 实现 count_hyps : unit -> int，返回当前上下文里假设的个数。用 List.length 和 Control.hyps 组合完成，不调用 Ltac1。

练习 3

下面这段 Ltac1 tactic 存在静默失败风险：

1
2
Ltac safe_rewrite h :=
  first [ rewrite h | rewrite <- h | idtac ].

用 Ltac2 重写 safe_rewrite，使得：当 rewrite h 和 rewrite <- h 都失败时，打印一条提示信息（用 Message.print）而非静默通过，然后继续（不中止证明）。

参考资料