Ltac 是 Coq 内置的 tactic 脚本语言，负责将零散的交互式证明步骤组合成可复用的自动化脚本。与 Gallina 的静态类型系统不同，Ltac 是动态类型的：tactic 表达式在运行时对当前证明状态求值，失败时会触发回溯，而非编译期报错。这一特性既带来了灵活性，也引入了难以诊断的错误行为。本篇覆盖 match goal、repeat、try、first、solve、idtac、fail 的语义，以及如何用 Ltac 关键字定义可复用的 tactic 组合子。前置阅读：本系列《基础 tactic 全景》和《搜索与自动化》；理论背景见形式化方法系列《依值类型——从命题逻辑到一阶逻辑》。

Ltac 的位置与定位

Coq 的证明引擎分三层：内核（kernel）验证证明项（proof term）的类型正确性；精化引擎（elaboration engine）把 tactic 序列翻译成证明项；Ltac 是在精化引擎之上运行的元语言，负责描述"如何生成 tactic 序列"。

Ltac 表达式的求值结果是一个 tactic 或一段证明片段。因为 Ltac 不走类型检查，错误只在运行时暴露。这是 Ltac 与 Ltac2（类型安全）、Mtac2（单子风格）最根本的区别；第 08 篇会对比两者。

一个最小的 Ltac 定义：

1
2
Ltac my_trivial :=
  simpl; auto.

my_trivial 是一个新 tactic，相当于把 simpl 和 auto 串联执行。在任何证明里可以直接写 my_trivial. 调用它。

基本控制结构

try

try t 执行 tactic t；若 t 失败，try t 视为成功且不修改证明状态。

1
2
3
4
5
6
7
Lemma try_demo : forall n : nat, n + 0 = n.
Proof.
  intro n.
  (* omega 能处理，ring 也能处理，假设想先用 ring *)
  try ring.   (* ring 对含变量的 nat 加法可能失败，try 保证不中断 *)
  lia.
Qed.

try 的典型用途：在 repeat 循环里执行一批"可能不适用"的 tactic，跳过对当前目标无效的那些。

repeat

repeat t 反复执行 t 直到 t 失败为止。若 t 每次执行都成功，repeat t 不会终止，因此 t 必须在有限步内失败。

1
2
3
4
5
(* 把所有 /\ 拆开 *)
Ltac split_all_and :=
  repeat match goal with
         | [ H : ?A /\ ?B |- _ ] => destruct H
         end.

repeat 加 match goal 是 Ltac 中最常见的组合模式：每一轮扫描所有假设，找到一个匹配就执行对应动作，直到没有假设能匹配为止。

first

first [ t1 | t2 | ... | tn ] 依次尝试 t1、t2……，返回第一个成功的 tactic 的结果；所有分支都失败时，first 失败。

1
2
3
4
5
Ltac dispatch :=
  first [ assumption
        | reflexivity
        | lia
        | tauto ].

dispatch 按优先级试四种快速关闭目标的方式。这是减少冗余 try 嵌套的标准写法。

solve

solve [ t1 | t2 | ... ] 语义上等价于 first [ t1 | t2 | ... ]，但有额外约束：成功的分支必须完全关闭当前目标（不留子目标）；若某分支成功但留有子目标，solve 视该分支失败并继续尝试下一个。

1
2
Ltac close_goal :=
  solve [ assumption | reflexivity | tauto | lia ].

solve 适合放在 repeat 的最后一步，确保每次迭代要么彻底完成子目标，要么完全回退。

idtac 与 fail

idtac 永远成功，不修改证明状态，可选传一个字符串作为调试输出：

1
idtac "reached branch A".

fail 永远失败，可携带一个整数（回溯深度）和一条错误消息：

1
fail 0 "no applicable rule".

fail 0 在当前层次失败；fail 1 穿透一层 try/repeat 向上传播失败。深度参数在编写嵌套 tactic 时控制错误的传播范围，是 Ltac 中最容易混淆的细节之一。

match goal 模式匹配

match goal with 是 Ltac 的核心构造，允许对当前证明状态做结构化匹配。

语法：

1
2
3
4
5
match goal with
| [ pat1 : T1, pat2 : T2, ... |- goal_pat ] => tactic
| ...
| [ |- _ ] => fallback_tactic
end

方括号内是对假设区（context）的匹配；|- 右侧是对当前目标的匹配；_ 是通配符。

以问号前缀开头的标识符（?A、?T、?n）是 Ltac 的元变量（meta-variable），在匹配时绑定到对应的 Coq 项，之后可在 tactic 分支里使用。

基本示例

拆解任意合取假设：

1
2
3
4
Ltac break_and :=
  match goal with
  | [ H : ?A /\ ?B |- _ ] => destruct H as [?HA ?HB]
  end.

这里 ?A 和 ?B 匹配合取的两个分量，?HA/?HB 是新引入假设的名称模式（以 ? 开头的名称会自动生成唯一标识符）。

对假设区和目标同时匹配：

1
2
3
4
Ltac apply_from_context :=
  match goal with
  | [ H : ?A -> ?B, HA : ?A |- ?B ] => exact (H HA)
  end.

当假设区同时有 H : A -> B 和 HA : A，且目标是 B 时，直接构造证明项 H HA 完成目标。

match goal 的回溯行为

match goal 遇到匹配分支时，先尝试执行分支体；若分支体失败，match goal 会回退到该分支，继续寻找下一个匹配。这与 Gallina 的 match 不同——Gallina 不回溯。

1
2
3
4
5
6
Ltac find_equality :=
  match goal with
  | [ H : ?X = ?Y |- _ ] =>
      (* 先尝试直接用 H 完成目标 *)
      rewrite H; reflexivity
  end.

若 rewrite H; reflexivity 失败（例如目标里 X 出现了不止一次，且替换后 reflexivity 无法闭合），match goal 会继续扫描假设区，尝试下一个 = 假设。

match context 与 match reverse

Coq 8.x 提供 match goal 和等价写法 match context 来匹配假设区。两者语义相同，match context 名称更明确，可视为别名。

match reverse goal with 则从假设区的末尾向前扫描（而非默认的从前向后）。当最新引入的假设在末尾，且通常更相关时，match reverse 能减少无效尝试：

1
2
3
4
Ltac use_last_hyp :=
  match reverse goal with
  | [ H : _ |- _ ] => exact H
  end.

构建自定义自动化 tactic

prop_auto 是一个处理命题逻辑的小型自动化 tactic，目标是覆盖 /\、\/、~、-> 的常见目标形式。

第一步：关闭简单目标

1
2
Ltac prop_close :=
  first [ assumption | exact I | reflexivity ].

exact I 用于目标是 True 的情形（I : True 是 Coq 预定义的证明）。

第二步：拆解假设

1
2
3
4
5
6
7
Ltac prop_destruct :=
  match goal with
  | [ H : ?A /\ ?B |- _ ] => destruct H
  | [ H : ?A \/ ?B |- _ ] => destruct H
  | [ H : exists _, _ |- _ ] => destruct H
  | [ H : False |- _ ] => destruct H
  end.

第三步：分解目标

1
2
3
4
5
6
Ltac prop_split :=
  match goal with
  | [ |- ?A /\ ?B ] => split
  | [ |- ?A <-> ?B ] => split
  | [ |- exists x, _ ] => eexists
  end.

第四步：处理蕴含与否定

1
2
3
4
5
6
Ltac prop_intro :=
  match goal with
  | [ |- ?A -> ?B ] => intro
  | [ |- ~ ?A     ] => intro
  | [ |- forall _, _ ] => intro
  end.

组合成完整 tactic

1
2
3
4
5
6
7
Ltac prop_auto :=
  repeat (
    prop_close
    || prop_destruct
    || prop_intro
    || prop_split
  ).

|| 是 Ltac 的"有焦点的 or"（focused or）：先尝试左侧，失败时尝试右侧；与 first [...] 在此语境下等价，但语法更简洁。

测试效果：

1
2
3
4
5
6
7
8
9
10
11
12
13
Lemma prop_auto_demo :
  forall A B C : Prop,
    (A -> B) -> (B -> C) -> A -> C.
Proof.
  prop_auto.
Qed.

Lemma prop_auto_demo2 :
  forall A B : Prop,
    A /\ B -> B /\ A.
Proof.
  prop_auto.
Qed.

查看生成的证明项

1
2
3
4
5
6
Lemma prop_auto_demo3 :
  forall A B : Prop, A /\ B -> A.
Proof.
  prop_auto.
  Show Proof.
Qed.

Show Proof. 在证明进行中显示当前已构建的证明项，输出类似：

1
2
3
4
(fun (A B : Prop) (H : A /\ B) =>
  match H with
  | conj a _ => a
  end)

这验证了 prop_auto 没有绕过内核检查：Ltac 生成的每一步 tactic 最终仍翻译成合法的 Gallina 项由内核验证。

失败尝试与正确解法对比

场景：对所有数值等式进行自动化替换

失败尝试：

1
2
3
4
Ltac subst_all_fail :=
  repeat match goal with
         | [ H : ?x = ?y |- _ ] => subst H
         end.

问题：subst 要求等式的一侧必须是变量，不能是任意表达式。若假设是 H : 2 + 2 = 4，subst H 会失败；但失败后 match goal 会重新匹配同一个 H，造成无限循环而不是回溯——因为 match goal 在同一假设上反复匹配而不前进。

正确解法：用 revert/clear 或显式排除非变量等式：

1
2
3
4
5
6
7
Ltac subst_vars :=
  repeat match goal with
         | [ H : ?x = _ |- _ ] =>
             is_var x; subst x
         | [ H : _ = ?x |- _ ] =>
             is_var x; subst x
         end.

is_var x 是 Ltac 内置的守卫（guard），当 x 是变量时成功，否则失败。加上这个守卫，match goal 只匹配"变量 = 表达式"形式的等式，避免死循环。

Ltac 的陷阱

动态类型带来的隐藏错误

Ltac 对 tactic 体不做类型检查。拼错 tactic 名称、传错参数类型，都只在运行时报错：

1
2
Ltac bad_tactic :=
  destruct_not_defined.  (* 编译期不报错，运行时才报 "Unknown tactic" *)

定义 bad_tactic 本身不会报错，因为 Coq 在定义 Ltac 时只做词法解析，不验证内部引用的 tactic 是否存在。

回溯语义的混淆

match goal 的回溯只发生在分支体失败时，而不是分支体"部分完成"时。若分支体执行了修改证明状态的 tactic 后失败，已执行的修改会被回退（Coq 的证明引擎支持回溯快照）。但若分支体调用了 idtac 或打印了调试信息，这些副作用仍然保留，状态本身被回退但输出不会消失，容易造成调试时的混乱。

调试技术

idtac 配合字符串输出追踪执行路径：

1
2
3
4
5
6
Ltac debug_dispatch :=
  first [
    (idtac "trying assumption"; assumption)
  | (idtac "trying lia"; lia)
  | (idtac "all failed"; fail "no rule applies")
  ].

Set Ltac Debug. 命令开启 Ltac 内置调试器，在 CoqIDE 的终端窗口或 coqtop 里逐步显示每个分支的匹配情况和成败记录：

1
Set Ltac Debug.

关闭：

1
Unset Ltac Debug.

Set Ltac Profiling. 则统计每个 tactic 的调用次数和耗时，用于诊断 repeat 循环中的性能问题：

1
2
3
Set Ltac Profiling.
(* ... 执行证明 ... *)
Show Ltac Profile.

完整示例：list_solver

以下 in_solver tactic 针对 In 和 ++ 相关命题，集中了 match goal、repeat、fail 的典型用法：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
Require Import List.
Import ListNotations.

(* 目标：证明关于 In 和 ++ 的简单命题 *)

Ltac in_solver :=
  repeat match goal with
  (* 关闭 In (x :: l) 目标：先试 x 在头部 *)
  | [ |- In ?x (?x :: _) ] =>
      left; reflexivity
  (* 再试 x 在尾部 *)
  | [ |- In ?x (_ :: ?l) ] =>
      right
  (* In l1 ++ l2 分情况 *)
  | [ H : In ?x ?l1 |- In ?x (?l1 ++ _) ] =>
      apply in_or_app; left; exact H
  | [ H : In ?x ?l2 |- In ?x (_ ++ ?l2) ] =>
      apply in_or_app; right; exact H
  (* 假设是 False 直接关闭 *)
  | [ H : False |- _ ] =>
      destruct H
  | [ H : In _ [] |- _ ] =>
      inversion H
  | [ |- In ?x [] ] =>
      fail "cannot prove In x []"
  end.

Lemma in_app_demo :
  forall (x : nat) (l1 l2 : list nat),
    In x l1 -> In x (l1 ++ l2).
Proof.
  intros x l1 l2 H.
  in_solver.
Qed.

Lemma in_cons_demo :
  forall (x y : nat) (l : list nat),
    x = y \/ In x l -> In x (y :: l).
Proof.
  intros x y l [Heq | HIn].
  - rewrite Heq. in_solver.
  - in_solver.
Qed.

Print Assumptions in_app_demo. 可验证该定理不依赖额外公理：

1
2
Print Assumptions in_app_demo.
(* Axioms: none *)

参数化 tactic 与高阶 tactic

Ltac 定义支持参数，参数可以是 Coq 项、tactic 或整数：

1
2
3
4
5
6
7
8
9
10
11
12
13
(* 接受一个 tactic 参数，在目标上先尝试 t，再尝试 auto *)
Ltac try_then_auto t :=
  first [ t | auto ].

(* 接受一个 Coq 项参数，用该项重写后化简 *)
Ltac rw_then_simpl h :=
  rewrite h; simpl.

(* 接受 tactic 参数（高阶 tactic） *)
Ltac on_all_hyps tac :=
  repeat match goal with
         | [ H : _ |- _ ] => tac H; clear H
         end.

调用方式：

1
2
3
Proof.
  on_all_hyps ltac:(fun H => try (rewrite H)).
Qed.

ltac:(...) 是 Coq 8.5+ 的 tactic-in-term 语法，允许在 Gallina 项位置嵌入 Ltac 表达式，也可用于将匿名 tactic 传给高阶 tactic 参数。

与 Ltac2 的边界

Ltac 的动态类型性质在大型证明库（MathComp、Iris）中已造成明显的维护困难：错误消息不具体、调试费时、tactic 之间的契约全靠文档约定而非类型。Ltac2 在 Coq 8.13+ 正式可用，提供静态类型、模式匹配穷尽性检查和更清晰的失败语义。从工程角度，新写的自动化 tactic 应优先考虑 Ltac2；Ltac 的知识在读已有代码（CompCert、MathComp 旧版）时仍然必要。第 08 篇会系统对比两者的设计取舍。

练习

练习 1（基础）：定义 Ltac clear_trivial tactic，清除上下文中所有形如 H : True 和 H : ?x = ?x 的假设，然后对以下引理使用它：

1
2
3
4
5
6
7
8
Lemma ex1 :
  forall A : Prop, True -> A = A -> A -> A.
Proof.
  intros A H1 H2 H3.
  (* 使用 clear_trivial 后只剩 H3 : A *)
  clear_trivial.
  exact H3.
Qed.

练习 2（中级）：定义 Ltac contradict_hyps tactic，检测上下文中是否同时存在 H1 : P 和 H2 : ~ P（对任意命题 P），若存在则用 exact (H2 H1) 关闭任意目标。测试：

1
2
3
4
5
6
Lemma ex2 :
  forall P Q : Prop, P -> ~ P -> Q.
Proof.
  intros P Q HP HNP.
  contradict_hyps.
Qed.

练习 3（进阶）：定义 Ltac invert_all tactic，对上下文中所有归纳类型的假设依次执行 inversion，并在每次 inversion 后执行 subst。注意：需要防止对已处理过的假设重复调用 inversion 导致无限循环。提示：可用 clear H 或 move H at top 结合 match reverse goal 控制扫描顺序。

参考资料